consider f being Function of (TS SCM-AE),(Funcs (NAT,( the InstructionsF of SCM ^omega))) such that
A1:
( ( for t being Terminal of SCM-AE ex g being sequence of ( the InstructionsF of SCM ^omega) st
( g = f . (root-tree t) & ( for n being Element of NAT holds g . n = H3(t,n) ) ) ) & ( for nt being NonTerminal of SCM-AE
for t1, t2 being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
ex g, f1, f2 being sequence of ( the InstructionsF of SCM ^omega) st
( g = f . (nt -tree (t1,t2)) & f1 = f . t1 & f2 = f . t2 & ( for n being Element of NAT holds g . n = H2(nt,f1,f2,n) ) ) ) )
from BINTREE1:sch 5();
take
f
; ( ( for t being Terminal of SCM-AE ex g being sequence of ( the InstructionsF of SCM ^omega) st
( g = f . (root-tree t) & ( for n being Nat holds g . n = <%((dl. n) := (@ t))%> ) ) ) & ( for nt being NonTerminal of SCM-AE
for t1, t2 being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
ex g, f1, f2 being sequence of ( the InstructionsF of SCM ^omega) st
( g = f . (nt -tree (t1,t2)) & f1 = f . t1 & f2 = f . t2 & ( for n being Nat holds g . n = ((f1 . (In (n,NAT))) ^ (f2 . (In ((n + 1),NAT)))) ^ (Selfwork (nt,n)) ) ) ) )
( ( for t being Terminal of SCM-AE ex g being sequence of ( the InstructionsF of SCM ^omega) st
( g = f . (root-tree t) & ( for n being Nat holds g . n = <%((dl. n) := (@ t))%> ) ) ) & ( for nt being NonTerminal of SCM-AE
for t1, t2 being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
ex g, f1, f2 being sequence of ( the InstructionsF of SCM ^omega) st
( g = f . (nt -tree (t1,t2)) & f1 = f . t1 & f2 = f . t2 & ( for n being Nat holds g . n = ((f1 . (In (n,NAT))) ^ (f2 . (In ((n + 1),NAT)))) ^ (Selfwork (nt,n)) ) ) ) )
proof
thus
for
t being
Terminal of
SCM-AE ex
g being
sequence of
( the InstructionsF of SCM ^omega) st
(
g = f . (root-tree t) & ( for
n being
Nat holds
g . n = <%((dl. n) := (@ t))%> ) )
for nt being NonTerminal of SCM-AE
for t1, t2 being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
ex g, f1, f2 being sequence of ( the InstructionsF of SCM ^omega) st
( g = f . (nt -tree (t1,t2)) & f1 = f . t1 & f2 = f . t2 & ( for n being Nat holds g . n = ((f1 . (In (n,NAT))) ^ (f2 . (In ((n + 1),NAT)))) ^ (Selfwork (nt,n)) ) )
thus
for
nt being
NonTerminal of
SCM-AE for
t1,
t2 being
bin-term for
rtl,
rtr being
Symbol of
SCM-AE st
rtl = root-label t1 &
rtr = root-label t2 &
nt ==> <*rtl,rtr*> holds
ex
g,
f1,
f2 being
sequence of
( the InstructionsF of SCM ^omega) st
(
g = f . (nt -tree (t1,t2)) &
f1 = f . t1 &
f2 = f . t2 & ( for
n being
Nat holds
g . n = ((f1 . (In (n,NAT))) ^ (f2 . (In ((n + 1),NAT)))) ^ (Selfwork (nt,n)) ) )
verumproof
let nt be
NonTerminal of
SCM-AE;
for t1, t2 being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
ex g, f1, f2 being sequence of ( the InstructionsF of SCM ^omega) st
( g = f . (nt -tree (t1,t2)) & f1 = f . t1 & f2 = f . t2 & ( for n being Nat holds g . n = ((f1 . (In (n,NAT))) ^ (f2 . (In ((n + 1),NAT)))) ^ (Selfwork (nt,n)) ) )let t1,
t2 be
bin-term;
for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
ex g, f1, f2 being sequence of ( the InstructionsF of SCM ^omega) st
( g = f . (nt -tree (t1,t2)) & f1 = f . t1 & f2 = f . t2 & ( for n being Nat holds g . n = ((f1 . (In (n,NAT))) ^ (f2 . (In ((n + 1),NAT)))) ^ (Selfwork (nt,n)) ) )let rtl,
rtr be
Symbol of
SCM-AE;
( rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> implies ex g, f1, f2 being sequence of ( the InstructionsF of SCM ^omega) st
( g = f . (nt -tree (t1,t2)) & f1 = f . t1 & f2 = f . t2 & ( for n being Nat holds g . n = ((f1 . (In (n,NAT))) ^ (f2 . (In ((n + 1),NAT)))) ^ (Selfwork (nt,n)) ) ) )
assume A4:
(
rtl = root-label t1 &
rtr = root-label t2 &
nt ==> <*rtl,rtr*> )
;
ex g, f1, f2 being sequence of ( the InstructionsF of SCM ^omega) st
( g = f . (nt -tree (t1,t2)) & f1 = f . t1 & f2 = f . t2 & ( for n being Nat holds g . n = ((f1 . (In (n,NAT))) ^ (f2 . (In ((n + 1),NAT)))) ^ (Selfwork (nt,n)) ) )
consider g,
f1,
f2 being
sequence of
( the InstructionsF of SCM ^omega) such that A5:
(
g = f . (nt -tree (t1,t2)) &
f1 = f . t1 &
f2 = f . t2 )
and A6:
for
n being
Element of
NAT holds
g . n = H2(
nt,
f1,
f2,
n)
by A4, A1;
take
g
;
ex f1, f2 being sequence of ( the InstructionsF of SCM ^omega) st
( g = f . (nt -tree (t1,t2)) & f1 = f . t1 & f2 = f . t2 & ( for n being Nat holds g . n = ((f1 . (In (n,NAT))) ^ (f2 . (In ((n + 1),NAT)))) ^ (Selfwork (nt,n)) ) )
take
f1
;
ex f2 being sequence of ( the InstructionsF of SCM ^omega) st
( g = f . (nt -tree (t1,t2)) & f1 = f . t1 & f2 = f . t2 & ( for n being Nat holds g . n = ((f1 . (In (n,NAT))) ^ (f2 . (In ((n + 1),NAT)))) ^ (Selfwork (nt,n)) ) )
take
f2
;
( g = f . (nt -tree (t1,t2)) & f1 = f . t1 & f2 = f . t2 & ( for n being Nat holds g . n = ((f1 . (In (n,NAT))) ^ (f2 . (In ((n + 1),NAT)))) ^ (Selfwork (nt,n)) ) )
thus
(
g = f . (nt -tree (t1,t2)) &
f1 = f . t1 &
f2 = f . t2 )
by A5;
for n being Nat holds g . n = ((f1 . (In (n,NAT))) ^ (f2 . (In ((n + 1),NAT)))) ^ (Selfwork (nt,n))
let n be
Nat;
g . n = ((f1 . (In (n,NAT))) ^ (f2 . (In ((n + 1),NAT)))) ^ (Selfwork (nt,n))
g . n = H2(
nt,
f1,
f2,
n)
by A6;
hence
g . n = ((f1 . (In (n,NAT))) ^ (f2 . (In ((n + 1),NAT)))) ^ (Selfwork (nt,n))
;
verum
end;
end;
hence
( ( for t being Terminal of SCM-AE ex g being sequence of ( the InstructionsF of SCM ^omega) st
( g = f . (root-tree t) & ( for n being Nat holds g . n = <%((dl. n) := (@ t))%> ) ) ) & ( for nt being NonTerminal of SCM-AE
for t1, t2 being bin-term
for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds
ex g, f1, f2 being sequence of ( the InstructionsF of SCM ^omega) st
( g = f . (nt -tree (t1,t2)) & f1 = f . t1 & f2 = f . t2 & ( for n being Nat holds g . n = ((f1 . (In (n,NAT))) ^ (f2 . (In ((n + 1),NAT)))) ^ (Selfwork (nt,n)) ) ) ) )
; verum