let f1, f2 be Function of (TS SCM-AE),(Funcs (NAT,( the InstructionsF of SCM ^omega))); :: thesis: ( ( for t being Terminal of SCM-AE ex g being sequence of ( the InstructionsF of SCM ^omega) st

( g = f1 . (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 = f1 . (nt -tree (t1,t2)) & f1 = f1 . t1 & f2 = f1 . 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 = f2 . (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 = f2 . (nt -tree (t1,t2)) & f1 = f2 . t1 & f2 = f2 . t2 & ( for n being Nat holds g . n = ((f1 . (In (n,NAT))) ^ (f2 . (In ((n + 1),NAT)))) ^ (Selfwork (nt,n)) ) ) ) implies f1 = f2 )

assume that

A7: ( ( for t being Terminal of SCM-AE ex g being sequence of ( the InstructionsF of SCM ^omega) st

( g = f1 . (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, g1, g2 being sequence of ( the InstructionsF of SCM ^omega) st

( g = f1 . (nt -tree (t1,t2)) & g1 = f1 . t1 & g2 = f1 . t2 & ( for n being Nat holds g . n = ((g1 . (In (n,NAT))) ^ (g2 . (In ((n + 1),NAT)))) ^ (Selfwork (nt,n)) ) ) ) ) and

A8: ( ( for t being Terminal of SCM-AE ex g being sequence of ( the InstructionsF of SCM ^omega) st

( g = f2 . (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, g1, g2 being sequence of ( the InstructionsF of SCM ^omega) st

( g = f2 . (nt -tree (t1,t2)) & g1 = f2 . t1 & g2 = f2 . t2 & ( for n being Nat holds g . n = ((g1 . (In (n,NAT))) ^ (g2 . (In ((n + 1),NAT)))) ^ (Selfwork (nt,n)) ) ) ) ) ; :: thesis: f1 = f2

A9: ( ( for t being Terminal of SCM-AE ex g being sequence of ( the InstructionsF of SCM ^omega) st

( g = f1 . (root-tree t) & ( for n being Element of NAT holds g . n = H_{3}(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, g1, g2 being sequence of ( the InstructionsF of SCM ^omega) st

( g = f1 . (nt -tree (t1,t2)) & g1 = f1 . t1 & g2 = f1 . t2 & ( for n being Element of NAT holds g . n = H_{2}(nt,g1,g2,n) ) ) ) )

( g = f2 . (root-tree t) & ( for n being Element of NAT holds g . n = H_{3}(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, g1, g2 being sequence of ( the InstructionsF of SCM ^omega) st

( g = f2 . (nt -tree (t1,t2)) & g1 = f2 . t1 & g2 = f2 . t2 & ( for n being Element of NAT holds g . n = H_{2}(nt,g1,g2,n) ) ) ) )

( g = f1 . (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 = f1 . (nt -tree (t1,t2)) & f1 = f1 . t1 & f2 = f1 . 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 = f2 . (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 = f2 . (nt -tree (t1,t2)) & f1 = f2 . t1 & f2 = f2 . t2 & ( for n being Nat holds g . n = ((f1 . (In (n,NAT))) ^ (f2 . (In ((n + 1),NAT)))) ^ (Selfwork (nt,n)) ) ) ) implies f1 = f2 )

assume that

A7: ( ( for t being Terminal of SCM-AE ex g being sequence of ( the InstructionsF of SCM ^omega) st

( g = f1 . (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, g1, g2 being sequence of ( the InstructionsF of SCM ^omega) st

( g = f1 . (nt -tree (t1,t2)) & g1 = f1 . t1 & g2 = f1 . t2 & ( for n being Nat holds g . n = ((g1 . (In (n,NAT))) ^ (g2 . (In ((n + 1),NAT)))) ^ (Selfwork (nt,n)) ) ) ) ) and

A8: ( ( for t being Terminal of SCM-AE ex g being sequence of ( the InstructionsF of SCM ^omega) st

( g = f2 . (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, g1, g2 being sequence of ( the InstructionsF of SCM ^omega) st

( g = f2 . (nt -tree (t1,t2)) & g1 = f2 . t1 & g2 = f2 . t2 & ( for n being Nat holds g . n = ((g1 . (In (n,NAT))) ^ (g2 . (In ((n + 1),NAT)))) ^ (Selfwork (nt,n)) ) ) ) ) ; :: thesis: f1 = f2

A9: ( ( for t being Terminal of SCM-AE ex g being sequence of ( the InstructionsF of SCM ^omega) st

( g = f1 . (root-tree t) & ( for n being Element of NAT holds g . n = H

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, g1, g2 being sequence of ( the InstructionsF of SCM ^omega) st

( g = f1 . (nt -tree (t1,t2)) & g1 = f1 . t1 & g2 = f1 . t2 & ( for n being Element of NAT holds g . n = H

proof

A13:
( ( for t being Terminal of SCM-AE ex g being sequence of ( the InstructionsF of SCM ^omega) st
thus
for t being Terminal of SCM-AE ex g being sequence of ( the InstructionsF of SCM ^omega) st

( g = f1 . (root-tree t) & ( for n being Element of NAT holds g . n = H_{3}(t,n) ) )
:: thesis: 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, g1, g2 being sequence of ( the InstructionsF of SCM ^omega) st

( g = f1 . (nt -tree (t1,t2)) & g1 = f1 . t1 & g2 = f1 . t2 & ( for n being Element of NAT holds g . n = H_{2}(nt,g1,g2,n) ) )

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, g1, g2 being sequence of ( the InstructionsF of SCM ^omega) st

( g = f1 . (nt -tree (t1,t2)) & g1 = f1 . t1 & g2 = f1 . t2 & ( for n being Element of NAT holds g . n = H_{2}(nt,g1,g2,n) ) )
:: thesis: verum

end;( g = f1 . (root-tree t) & ( for n being Element of NAT holds g . n = H

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, g1, g2 being sequence of ( the InstructionsF of SCM ^omega) st

( g = f1 . (nt -tree (t1,t2)) & g1 = f1 . t1 & g2 = f1 . t2 & ( for n being Element of NAT holds g . n = H

proof

thus
for nt being NonTerminal of SCM-AE
let t be Terminal of SCM-AE; :: thesis: ex g being sequence of ( the InstructionsF of SCM ^omega) st

( g = f1 . (root-tree t) & ( for n being Element of NAT holds g . n = H_{3}(t,n) ) )

consider g being sequence of ( the InstructionsF of SCM ^omega) such that

A10: ( g = f1 . (root-tree t) & ( for n being Nat holds g . n = <%((dl. n) := (@ t))%> ) ) by A7;

take g ; :: thesis: ( g = f1 . (root-tree t) & ( for n being Element of NAT holds g . n = H_{3}(t,n) ) )

thus ( g = f1 . (root-tree t) & ( for n being Element of NAT holds g . n = H_{3}(t,n) ) )
by A10; :: thesis: verum

end;( g = f1 . (root-tree t) & ( for n being Element of NAT holds g . n = H

consider g being sequence of ( the InstructionsF of SCM ^omega) such that

A10: ( g = f1 . (root-tree t) & ( for n being Nat holds g . n = <%((dl. n) := (@ t))%> ) ) by A7;

take g ; :: thesis: ( g = f1 . (root-tree t) & ( for n being Element of NAT holds g . n = H

thus ( g = f1 . (root-tree t) & ( for n being Element of NAT holds g . n = H

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, g1, g2 being sequence of ( the InstructionsF of SCM ^omega) st

( g = f1 . (nt -tree (t1,t2)) & g1 = f1 . t1 & g2 = f1 . t2 & ( for n being Element of NAT holds g . n = H

proof

let nt be NonTerminal of SCM-AE; :: thesis: 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, g1, g2 being sequence of ( the InstructionsF of SCM ^omega) st

( g = f1 . (nt -tree (t1,t2)) & g1 = f1 . t1 & g2 = f1 . t2 & ( for n being Element of NAT holds g . n = H_{2}(nt,g1,g2,n) ) )

let t1, t2 be bin-term; :: thesis: for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds

ex g, g1, g2 being sequence of ( the InstructionsF of SCM ^omega) st

( g = f1 . (nt -tree (t1,t2)) & g1 = f1 . t1 & g2 = f1 . t2 & ( for n being Element of NAT holds g . n = H_{2}(nt,g1,g2,n) ) )

let rtl, rtr be Symbol of SCM-AE; :: thesis: ( rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> implies ex g, g1, g2 being sequence of ( the InstructionsF of SCM ^omega) st

( g = f1 . (nt -tree (t1,t2)) & g1 = f1 . t1 & g2 = f1 . t2 & ( for n being Element of NAT holds g . n = H_{2}(nt,g1,g2,n) ) ) )

assume A11: ( rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> ) ; :: thesis: ex g, g1, g2 being sequence of ( the InstructionsF of SCM ^omega) st

( g = f1 . (nt -tree (t1,t2)) & g1 = f1 . t1 & g2 = f1 . t2 & ( for n being Element of NAT holds g . n = H_{2}(nt,g1,g2,n) ) )

consider g, g1, g2 being sequence of ( the InstructionsF of SCM ^omega) such that

A12: ( g = f1 . (nt -tree (t1,t2)) & g1 = f1 . t1 & g2 = f1 . t2 & ( for n being Nat holds g . n = ((g1 . (In (n,NAT))) ^ (g2 . (In ((n + 1),NAT)))) ^ (Selfwork (nt,n)) ) ) by A7, A11;

take g ; :: thesis: ex g1, g2 being sequence of ( the InstructionsF of SCM ^omega) st

( g = f1 . (nt -tree (t1,t2)) & g1 = f1 . t1 & g2 = f1 . t2 & ( for n being Element of NAT holds g . n = H_{2}(nt,g1,g2,n) ) )

take g1 ; :: thesis: ex g2 being sequence of ( the InstructionsF of SCM ^omega) st

( g = f1 . (nt -tree (t1,t2)) & g1 = f1 . t1 & g2 = f1 . t2 & ( for n being Element of NAT holds g . n = H_{2}(nt,g1,g2,n) ) )

take g2 ; :: thesis: ( g = f1 . (nt -tree (t1,t2)) & g1 = f1 . t1 & g2 = f1 . t2 & ( for n being Element of NAT holds g . n = H_{2}(nt,g1,g2,n) ) )

thus ( g = f1 . (nt -tree (t1,t2)) & g1 = f1 . t1 & g2 = f1 . t2 & ( for n being Element of NAT holds g . n = H_{2}(nt,g1,g2,n) ) )
by A12; :: thesis: verum

end;for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds

ex g, g1, g2 being sequence of ( the InstructionsF of SCM ^omega) st

( g = f1 . (nt -tree (t1,t2)) & g1 = f1 . t1 & g2 = f1 . t2 & ( for n being Element of NAT holds g . n = H

let t1, t2 be bin-term; :: thesis: for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds

ex g, g1, g2 being sequence of ( the InstructionsF of SCM ^omega) st

( g = f1 . (nt -tree (t1,t2)) & g1 = f1 . t1 & g2 = f1 . t2 & ( for n being Element of NAT holds g . n = H

let rtl, rtr be Symbol of SCM-AE; :: thesis: ( rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> implies ex g, g1, g2 being sequence of ( the InstructionsF of SCM ^omega) st

( g = f1 . (nt -tree (t1,t2)) & g1 = f1 . t1 & g2 = f1 . t2 & ( for n being Element of NAT holds g . n = H

assume A11: ( rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> ) ; :: thesis: ex g, g1, g2 being sequence of ( the InstructionsF of SCM ^omega) st

( g = f1 . (nt -tree (t1,t2)) & g1 = f1 . t1 & g2 = f1 . t2 & ( for n being Element of NAT holds g . n = H

consider g, g1, g2 being sequence of ( the InstructionsF of SCM ^omega) such that

A12: ( g = f1 . (nt -tree (t1,t2)) & g1 = f1 . t1 & g2 = f1 . t2 & ( for n being Nat holds g . n = ((g1 . (In (n,NAT))) ^ (g2 . (In ((n + 1),NAT)))) ^ (Selfwork (nt,n)) ) ) by A7, A11;

take g ; :: thesis: ex g1, g2 being sequence of ( the InstructionsF of SCM ^omega) st

( g = f1 . (nt -tree (t1,t2)) & g1 = f1 . t1 & g2 = f1 . t2 & ( for n being Element of NAT holds g . n = H

take g1 ; :: thesis: ex g2 being sequence of ( the InstructionsF of SCM ^omega) st

( g = f1 . (nt -tree (t1,t2)) & g1 = f1 . t1 & g2 = f1 . t2 & ( for n being Element of NAT holds g . n = H

take g2 ; :: thesis: ( g = f1 . (nt -tree (t1,t2)) & g1 = f1 . t1 & g2 = f1 . t2 & ( for n being Element of NAT holds g . n = H

thus ( g = f1 . (nt -tree (t1,t2)) & g1 = f1 . t1 & g2 = f1 . t2 & ( for n being Element of NAT holds g . n = H

( g = f2 . (root-tree t) & ( for n being Element of NAT holds g . n = H

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, g1, g2 being sequence of ( the InstructionsF of SCM ^omega) st

( g = f2 . (nt -tree (t1,t2)) & g1 = f2 . t1 & g2 = f2 . t2 & ( for n being Element of NAT holds g . n = H

proof

thus
f1 = f2
from BINTREE1:sch 6(A9, A13); :: thesis: verum
thus
for t being Terminal of SCM-AE ex g being sequence of ( the InstructionsF of SCM ^omega) st

( g = f2 . (root-tree t) & ( for n being Element of NAT holds g . n = H_{3}(t,n) ) )
:: thesis: 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, g1, g2 being sequence of ( the InstructionsF of SCM ^omega) st

( g = f2 . (nt -tree (t1,t2)) & g1 = f2 . t1 & g2 = f2 . t2 & ( for n being Element of NAT holds g . n = H_{2}(nt,g1,g2,n) ) )

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, g1, g2 being sequence of ( the InstructionsF of SCM ^omega) st

( g = f2 . (nt -tree (t1,t2)) & g1 = f2 . t1 & g2 = f2 . t2 & ( for n being Element of NAT holds g . n = H_{2}(nt,g1,g2,n) ) )
:: thesis: verum

end;( g = f2 . (root-tree t) & ( for n being Element of NAT holds g . n = H

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, g1, g2 being sequence of ( the InstructionsF of SCM ^omega) st

( g = f2 . (nt -tree (t1,t2)) & g1 = f2 . t1 & g2 = f2 . t2 & ( for n being Element of NAT holds g . n = H

proof

thus
for nt being NonTerminal of SCM-AE
let t be Terminal of SCM-AE; :: thesis: ex g being sequence of ( the InstructionsF of SCM ^omega) st

( g = f2 . (root-tree t) & ( for n being Element of NAT holds g . n = H_{3}(t,n) ) )

consider g being sequence of ( the InstructionsF of SCM ^omega) such that

A14: ( g = f2 . (root-tree t) & ( for n being Nat holds g . n = <%((dl. n) := (@ t))%> ) ) by A8;

take g ; :: thesis: ( g = f2 . (root-tree t) & ( for n being Element of NAT holds g . n = H_{3}(t,n) ) )

thus ( g = f2 . (root-tree t) & ( for n being Element of NAT holds g . n = H_{3}(t,n) ) )
by A14; :: thesis: verum

end;( g = f2 . (root-tree t) & ( for n being Element of NAT holds g . n = H

consider g being sequence of ( the InstructionsF of SCM ^omega) such that

A14: ( g = f2 . (root-tree t) & ( for n being Nat holds g . n = <%((dl. n) := (@ t))%> ) ) by A8;

take g ; :: thesis: ( g = f2 . (root-tree t) & ( for n being Element of NAT holds g . n = H

thus ( g = f2 . (root-tree t) & ( for n being Element of NAT holds g . n = H

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, g1, g2 being sequence of ( the InstructionsF of SCM ^omega) st

( g = f2 . (nt -tree (t1,t2)) & g1 = f2 . t1 & g2 = f2 . t2 & ( for n being Element of NAT holds g . n = H

proof

let nt be NonTerminal of SCM-AE; :: thesis: 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, g1, g2 being sequence of ( the InstructionsF of SCM ^omega) st

( g = f2 . (nt -tree (t1,t2)) & g1 = f2 . t1 & g2 = f2 . t2 & ( for n being Element of NAT holds g . n = H_{2}(nt,g1,g2,n) ) )

let t1, t2 be bin-term; :: thesis: for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds

ex g, g1, g2 being sequence of ( the InstructionsF of SCM ^omega) st

( g = f2 . (nt -tree (t1,t2)) & g1 = f2 . t1 & g2 = f2 . t2 & ( for n being Element of NAT holds g . n = H_{2}(nt,g1,g2,n) ) )

let rtl, rtr be Symbol of SCM-AE; :: thesis: ( rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> implies ex g, g1, g2 being sequence of ( the InstructionsF of SCM ^omega) st

( g = f2 . (nt -tree (t1,t2)) & g1 = f2 . t1 & g2 = f2 . t2 & ( for n being Element of NAT holds g . n = H_{2}(nt,g1,g2,n) ) ) )

assume A15: ( rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> ) ; :: thesis: ex g, g1, g2 being sequence of ( the InstructionsF of SCM ^omega) st

( g = f2 . (nt -tree (t1,t2)) & g1 = f2 . t1 & g2 = f2 . t2 & ( for n being Element of NAT holds g . n = H_{2}(nt,g1,g2,n) ) )

consider g, g1, g2 being sequence of ( the InstructionsF of SCM ^omega) such that

A16: ( g = f2 . (nt -tree (t1,t2)) & g1 = f2 . t1 & g2 = f2 . t2 & ( for n being Nat holds g . n = ((g1 . (In (n,NAT))) ^ (g2 . (In ((n + 1),NAT)))) ^ (Selfwork (nt,n)) ) ) by A8, A15;

take g ; :: thesis: ex g1, g2 being sequence of ( the InstructionsF of SCM ^omega) st

( g = f2 . (nt -tree (t1,t2)) & g1 = f2 . t1 & g2 = f2 . t2 & ( for n being Element of NAT holds g . n = H_{2}(nt,g1,g2,n) ) )

take g1 ; :: thesis: ex g2 being sequence of ( the InstructionsF of SCM ^omega) st

( g = f2 . (nt -tree (t1,t2)) & g1 = f2 . t1 & g2 = f2 . t2 & ( for n being Element of NAT holds g . n = H_{2}(nt,g1,g2,n) ) )

take g2 ; :: thesis: ( g = f2 . (nt -tree (t1,t2)) & g1 = f2 . t1 & g2 = f2 . t2 & ( for n being Element of NAT holds g . n = H_{2}(nt,g1,g2,n) ) )

thus ( g = f2 . (nt -tree (t1,t2)) & g1 = f2 . t1 & g2 = f2 . t2 & ( for n being Element of NAT holds g . n = H_{2}(nt,g1,g2,n) ) )
by A16; :: thesis: verum

end;for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds

ex g, g1, g2 being sequence of ( the InstructionsF of SCM ^omega) st

( g = f2 . (nt -tree (t1,t2)) & g1 = f2 . t1 & g2 = f2 . t2 & ( for n being Element of NAT holds g . n = H

let t1, t2 be bin-term; :: thesis: for rtl, rtr being Symbol of SCM-AE st rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> holds

ex g, g1, g2 being sequence of ( the InstructionsF of SCM ^omega) st

( g = f2 . (nt -tree (t1,t2)) & g1 = f2 . t1 & g2 = f2 . t2 & ( for n being Element of NAT holds g . n = H

let rtl, rtr be Symbol of SCM-AE; :: thesis: ( rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> implies ex g, g1, g2 being sequence of ( the InstructionsF of SCM ^omega) st

( g = f2 . (nt -tree (t1,t2)) & g1 = f2 . t1 & g2 = f2 . t2 & ( for n being Element of NAT holds g . n = H

assume A15: ( rtl = root-label t1 & rtr = root-label t2 & nt ==> <*rtl,rtr*> ) ; :: thesis: ex g, g1, g2 being sequence of ( the InstructionsF of SCM ^omega) st

( g = f2 . (nt -tree (t1,t2)) & g1 = f2 . t1 & g2 = f2 . t2 & ( for n being Element of NAT holds g . n = H

consider g, g1, g2 being sequence of ( the InstructionsF of SCM ^omega) such that

A16: ( g = f2 . (nt -tree (t1,t2)) & g1 = f2 . t1 & g2 = f2 . t2 & ( for n being Nat holds g . n = ((g1 . (In (n,NAT))) ^ (g2 . (In ((n + 1),NAT)))) ^ (Selfwork (nt,n)) ) ) by A8, A15;

take g ; :: thesis: ex g1, g2 being sequence of ( the InstructionsF of SCM ^omega) st

( g = f2 . (nt -tree (t1,t2)) & g1 = f2 . t1 & g2 = f2 . t2 & ( for n being Element of NAT holds g . n = H

take g1 ; :: thesis: ex g2 being sequence of ( the InstructionsF of SCM ^omega) st

( g = f2 . (nt -tree (t1,t2)) & g1 = f2 . t1 & g2 = f2 . t2 & ( for n being Element of NAT holds g . n = H

take g2 ; :: thesis: ( g = f2 . (nt -tree (t1,t2)) & g1 = f2 . t1 & g2 = f2 . t2 & ( for n being Element of NAT holds g . n = H

thus ( g = f2 . (nt -tree (t1,t2)) & g1 = f2 . t1 & g2 = f2 . t2 & ( for n being Element of NAT holds g . n = H