A1: for nt being NonTerminal of SCM-AE
for tl, tr being bin-term st nt ==> <*(),()*> & S2[tl] & S2[tr] holds
S2[nt -tree (tl,tr)]
proof
let nt be NonTerminal of SCM-AE; :: thesis: for tl, tr being bin-term st nt ==> <*(),()*> & S2[tl] & S2[tr] holds
S2[nt -tree (tl,tr)]

let tl, tr be bin-term; :: thesis: ( nt ==> <*(),()*> & S2[tl] & S2[tr] implies S2[nt -tree (tl,tr)] )
assume that
A2: nt ==> <*(),()*> and
A3: S2[tl] and
A4: S2[tr] ; :: thesis: S2[nt -tree (tl,tr)]
let F be Instruction-Sequence of SCM; :: thesis: for aux, n being Element of NAT st Shift ((SCM-Compile ((nt -tree (tl,tr)),aux)),n) c= F holds
for s being b2 -started State of SCM st aux > max_Data-Loc_in (nt -tree (tl,tr)) holds
ex i being Element of NAT ex u being State of SCM st
( u = Comput (F,s,(i + 1)) & i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )

let aux, n be Element of NAT ; :: thesis: ( Shift ((SCM-Compile ((nt -tree (tl,tr)),aux)),n) c= F implies for s being n -started State of SCM st aux > max_Data-Loc_in (nt -tree (tl,tr)) holds
ex i being Element of NAT ex u being State of SCM st
( u = Comput (F,s,(i + 1)) & i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) ) )

assume A5: Shift ((SCM-Compile ((nt -tree (tl,tr)),aux)),n) c= F ; :: thesis: for s being n -started State of SCM st aux > max_Data-Loc_in (nt -tree (tl,tr)) holds
ex i being Element of NAT ex u being State of SCM st
( u = Comput (F,s,(i + 1)) & i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )

let s be n -started State of SCM; :: thesis: ( aux > max_Data-Loc_in (nt -tree (tl,tr)) implies ex i being Element of NAT ex u being State of SCM st
( u = Comput (F,s,(i + 1)) & i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) ) )

assume A6: aux > max_Data-Loc_in (nt -tree (tl,tr)) ; :: thesis: ex i being Element of NAT ex u being State of SCM st
( u = Comput (F,s,(i + 1)) & i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )

A7: max_Data-Loc_in (nt -tree (tl,tr)) = max ((),()) by Th10;
then max_Data-Loc_in tl <= max_Data-Loc_in (nt -tree (tl,tr)) by XXREAL_0:25;
then A8: max_Data-Loc_in tl < aux by ;
max_Data-Loc_in tr <= max_Data-Loc_in (nt -tree (tl,tr)) by ;
then A9: max_Data-Loc_in tr < aux by ;
then A10: max_Data-Loc_in tr < aux + 1 by NAT_1:13;
A11: SCM-Compile ((nt -tree (tl,tr)),aux) = ((SCM-Compile (tl,aux)) ^ (SCM-Compile (tr,(aux + 1)))) ^ (Selfwork (nt,aux)) by ;
then SCM-Compile ((nt -tree (tl,tr)),aux) = (SCM-Compile (tl,aux)) ^ ((SCM-Compile (tr,(aux + 1))) ^ (Selfwork (nt,aux))) by AFINSQ_1:27;
then Shift ((SCM-Compile (tl,aux)),n) c= F by ;
then consider i1 being Element of NAT , u1 being State of SCM such that
A12: u1 = Comput (F,s,(i1 + 1)) and
A13: i1 + 1 = len (SCM-Compile (tl,aux)) and
IC (Comput (F,s,i1)) = n + i1 and
A14: IC u1 = n + (i1 + 1) and
A15: u1 . (dl. aux) = tl @ s and
A16: for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u1 . (dl. dn) by A3, A8;
A17: u1 is n + (i1 + 1) -started State of SCM by ;
SCM-Compile ((nt -tree (tl,tr)),aux) = (SCM-Compile (tl,aux)) ^ ((SCM-Compile (tr,(aux + 1))) ^ (Selfwork (nt,aux))) by ;
then Shift (((SCM-Compile (tr,(aux + 1))) ^ (Selfwork (nt,aux))),(n + (i1 + 1))) c= F by ;
then Shift ((SCM-Compile (tr,(aux + 1))),(n + (i1 + 1))) c= F by AFINSQ_1:82;
then consider i2 being Element of NAT , u2 being State of SCM such that
A18: u2 = Comput (F,u1,(i2 + 1)) and
A19: i2 + 1 = len (SCM-Compile (tr,(aux + 1))) and
IC (Comput (F,u1,i2)) = (n + (i1 + 1)) + i2 and
A20: IC u2 = (n + (i1 + 1)) + (i2 + 1) and
A21: u2 . (dl. (aux + 1)) = tr @ u1 and
A22: for dn being Element of NAT st dn < aux + 1 holds
u1 . (dl. dn) = u2 . (dl. dn) by A4, A10, A17;
A23: u2 = Comput (F,s,((i1 + 1) + (i2 + 1))) by ;
A24: now :: thesis: for n being Element of NAT st n <= max_Data-Loc_in tr holds
s . (dl. n) = u1 . (dl. n)
let n be Element of NAT ; :: thesis: ( n <= max_Data-Loc_in tr implies s . (dl. n) = u1 . (dl. n) )
assume n <= max_Data-Loc_in tr ; :: thesis: s . (dl. n) = u1 . (dl. n)
then n < aux by ;
hence s . (dl. n) = u1 . (dl. n) by A16; :: thesis: verum
end;
A25: aux < aux + 1 by NAT_1:13;
A26: (nt -tree (tl,tr)) @ s = nt -Meaning_on ((tl @ s),(tr @ s)) by Th5;
A27: len ((SCM-Compile (tl,aux)) ^ (SCM-Compile (tr,(aux + 1)))) = (i1 + 1) + (i2 + 1) by ;
not not nt = [0,0] & ... & not nt = [0,4] by Th1;
per cases then ( nt = [0,0] or nt = [0,1] or nt = [0,2] or nt = [0,3] or nt = [0,4] ) ;
suppose A28: nt = [0,0] ; :: thesis: ex i being Element of NAT ex u being State of SCM st
( u = Comput (F,s,(i + 1)) & i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )

then A29: nt -Meaning_on ((tl @ s),(tr @ s)) = (tl @ s) + (tr @ s) by Def8;
take i = (i1 + 1) + (i2 + 1); :: thesis: ex u being State of SCM st
( u = Comput (F,s,(i + 1)) & i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )

take u = Comput (F,s,(i + 1)); :: thesis: ( u = Comput (F,s,(i + 1)) & i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )

thus u = Comput (F,s,(i + 1)) ; :: thesis: ( i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )

A30: Selfwork (nt,aux) = <%(AddTo ((dl. aux),(dl. (aux + 1))))%> by ;
then A31: len (Selfwork (nt,aux)) = 1 by AFINSQ_1:34;
hence i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) by ; :: thesis: ( IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )

thus IC (Comput (F,s,i)) = n + i by ; :: thesis: ( IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )

len (SCM-Compile ((nt -tree (tl,tr)),aux)) = ((i1 + 1) + (i2 + 1)) + 1 by ;
then i < len (SCM-Compile ((nt -tree (tl,tr)),aux)) by NAT_1:13;
then i in dom (SCM-Compile ((nt -tree (tl,tr)),aux)) by AFINSQ_1:86;
then A32: F . (n + i) = (SCM-Compile ((nt -tree (tl,tr)),aux)) . i by
.= AddTo ((dl. aux),(dl. (aux + 1))) by ;
hence IC u = (n + i) + 1 by
.= n + (i + 1) ;
:: thesis: ( u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )

thus u . (dl. aux) = (u2 . (dl. aux)) + (u2 . (dl. (aux + 1))) by
.= (u1 . (dl. aux)) + (tr @ u1) by
.= (nt -tree (tl,tr)) @ s by A15, A26, A24, A29, Th11 ; :: thesis: for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn)

let dn be Element of NAT ; :: thesis: ( dn < aux implies s . (dl. dn) = u . (dl. dn) )
assume A33: dn < aux ; :: thesis: s . (dl. dn) = u . (dl. dn)
then dn < aux + 1 by NAT_1:13;
then A34: u1 . (dl. dn) = u2 . (dl. dn) by A22;
dl. dn <> dl. aux by ;
then u . (dl. dn) = u2 . (dl. dn) by ;
hence s . (dl. dn) = u . (dl. dn) by ; :: thesis: verum
end;
suppose A35: nt = [0,1] ; :: thesis: ex i being Element of NAT ex u being State of SCM st
( u = Comput (F,s,(i + 1)) & i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )

then A36: nt -Meaning_on ((tl @ s),(tr @ s)) = (tl @ s) - (tr @ s) by Def8;
take i = (i1 + 1) + (i2 + 1); :: thesis: ex u being State of SCM st
( u = Comput (F,s,(i + 1)) & i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )

take u = Comput (F,s,(i + 1)); :: thesis: ( u = Comput (F,s,(i + 1)) & i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )

thus u = Comput (F,s,(i + 1)) ; :: thesis: ( i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )

A37: Selfwork (nt,aux) = <%(SubFrom ((dl. aux),(dl. (aux + 1))))%> by ;
then A38: len (Selfwork (nt,aux)) = 1 by AFINSQ_1:34;
hence i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) by ; :: thesis: ( IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )

thus IC (Comput (F,s,i)) = n + i by ; :: thesis: ( IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )

len (SCM-Compile ((nt -tree (tl,tr)),aux)) = ((i1 + 1) + (i2 + 1)) + 1 by ;
then i < len (SCM-Compile ((nt -tree (tl,tr)),aux)) by NAT_1:13;
then i in dom (SCM-Compile ((nt -tree (tl,tr)),aux)) by AFINSQ_1:86;
then A39: F . (n + i) = (SCM-Compile ((nt -tree (tl,tr)),aux)) . i by
.= SubFrom ((dl. aux),(dl. (aux + 1))) by ;
hence IC u = (n + i) + 1 by
.= n + (i + 1) ;
:: thesis: ( u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )

thus u . (dl. aux) = (u2 . (dl. aux)) - (u2 . (dl. (aux + 1))) by
.= (u1 . (dl. aux)) - (tr @ u1) by
.= (nt -tree (tl,tr)) @ s by A15, A26, A24, A36, Th11 ; :: thesis: for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn)

let dn be Element of NAT ; :: thesis: ( dn < aux implies s . (dl. dn) = u . (dl. dn) )
assume A40: dn < aux ; :: thesis: s . (dl. dn) = u . (dl. dn)
then dn < aux + 1 by NAT_1:13;
then A41: u1 . (dl. dn) = u2 . (dl. dn) by A22;
dl. dn <> dl. aux by ;
then u . (dl. dn) = u2 . (dl. dn) by ;
hence s . (dl. dn) = u . (dl. dn) by ; :: thesis: verum
end;
suppose A42: nt = [0,2] ; :: thesis: ex i being Element of NAT ex u being State of SCM st
( u = Comput (F,s,(i + 1)) & i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )

then A43: nt -Meaning_on ((tl @ s),(tr @ s)) = (tl @ s) * (tr @ s) by Def8;
take i = (i1 + 1) + (i2 + 1); :: thesis: ex u being State of SCM st
( u = Comput (F,s,(i + 1)) & i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )

take u = Comput (F,s,(i + 1)); :: thesis: ( u = Comput (F,s,(i + 1)) & i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )

thus u = Comput (F,s,(i + 1)) ; :: thesis: ( i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )

A44: Selfwork (nt,aux) = <%(MultBy ((dl. aux),(dl. (aux + 1))))%> by ;
then A45: len (Selfwork (nt,aux)) = 1 by AFINSQ_1:34;
hence i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) by ; :: thesis: ( IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )

thus IC (Comput (F,s,i)) = n + i by ; :: thesis: ( IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )

len (SCM-Compile ((nt -tree (tl,tr)),aux)) = ((i1 + 1) + (i2 + 1)) + 1 by ;
then i < len (SCM-Compile ((nt -tree (tl,tr)),aux)) by NAT_1:13;
then i in dom (SCM-Compile ((nt -tree (tl,tr)),aux)) by AFINSQ_1:86;
then A46: F . (n + i) = (SCM-Compile ((nt -tree (tl,tr)),aux)) . i by
.= MultBy ((dl. aux),(dl. (aux + 1))) by ;
hence IC u = (n + i) + 1 by
.= n + (i + 1) ;
:: thesis: ( u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )

thus u . (dl. aux) = (u2 . (dl. aux)) * (u2 . (dl. (aux + 1))) by
.= (u1 . (dl. aux)) * (tr @ u1) by
.= (nt -tree (tl,tr)) @ s by A15, A26, A24, A43, Th11 ; :: thesis: for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn)

let dn be Element of NAT ; :: thesis: ( dn < aux implies s . (dl. dn) = u . (dl. dn) )
assume A47: dn < aux ; :: thesis: s . (dl. dn) = u . (dl. dn)
then dn < aux + 1 by NAT_1:13;
then A48: u1 . (dl. dn) = u2 . (dl. dn) by A22;
dl. dn <> dl. aux by ;
then u . (dl. dn) = u2 . (dl. dn) by ;
hence s . (dl. dn) = u . (dl. dn) by ; :: thesis: verum
end;
suppose A49: nt = [0,3] ; :: thesis: ex i being Element of NAT ex u being State of SCM st
( u = Comput (F,s,(i + 1)) & i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )

take i = (i1 + 1) + (i2 + 1); :: thesis: ex u being State of SCM st
( u = Comput (F,s,(i + 1)) & i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )

take u = Comput (F,s,(i + 1)); :: thesis: ( u = Comput (F,s,(i + 1)) & i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )

thus u = Comput (F,s,(i + 1)) ; :: thesis: ( i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )

A50: Selfwork (nt,aux) = <%(Divide ((dl. aux),(dl. (aux + 1))))%> by ;
then A51: len (Selfwork (nt,aux)) = 1 by AFINSQ_1:34;
hence i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) by ; :: thesis: ( IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )

len (SCM-Compile ((nt -tree (tl,tr)),aux)) = ((i1 + 1) + (i2 + 1)) + 1 by ;
then i < len (SCM-Compile ((nt -tree (tl,tr)),aux)) by NAT_1:13;
then i in dom (SCM-Compile ((nt -tree (tl,tr)),aux)) by AFINSQ_1:86;
then A52: F . (n + i) = (SCM-Compile ((nt -tree (tl,tr)),aux)) . i by
.= Divide ((dl. aux),(dl. (aux + 1))) by ;
thus IC (Comput (F,s,i)) = n + i by ; :: thesis: ( IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )

A53: nt -Meaning_on ((tl @ s),(tr @ s)) = (tl @ s) div (tr @ s) by ;
aux <> aux + 1 ;
then A54: dl. aux <> dl. (aux + 1) by AMI_3:10;
hence IC u = (n + i) + 1 by
.= n + (i + 1) ;
:: thesis: ( u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )

thus u . (dl. aux) = (u2 . (dl. aux)) div (u2 . (dl. (aux + 1))) by
.= (u1 . (dl. aux)) div (tr @ u1) by
.= (nt -tree (tl,tr)) @ s by A15, A26, A24, A53, Th11 ; :: thesis: for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn)

let dn be Element of NAT ; :: thesis: ( dn < aux implies s . (dl. dn) = u . (dl. dn) )
assume A55: dn < aux ; :: thesis: s . (dl. dn) = u . (dl. dn)
then A56: dn < aux + 1 by NAT_1:13;
then A57: dl. dn <> dl. (aux + 1) by AMI_3:10;
A58: u1 . (dl. dn) = u2 . (dl. dn) by ;
dl. dn <> dl. aux by ;
then u . (dl. dn) = u2 . (dl. dn) by ;
hence s . (dl. dn) = u . (dl. dn) by ; :: thesis: verum
end;
suppose A59: nt = [0,4] ; :: thesis: ex i being Element of NAT ex u being State of SCM st
( u = Comput (F,s,(i + 1)) & i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )

then A60: nt -Meaning_on ((tl @ s),(tr @ s)) = (tl @ s) mod (tr @ s) by Def8;
set i = (i1 + 1) + (i2 + 1);
set u = Comput (F,s,(((i1 + 1) + (i2 + 1)) + 1));
take k = ((i1 + 1) + (i2 + 1)) + 1; :: thesis: ex u being State of SCM st
( u = Comput (F,s,(k + 1)) & k + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) & IC (Comput (F,s,k)) = n + k & IC u = n + (k + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )

take v = Comput (F,s,(k + 1)); :: thesis: ( v = Comput (F,s,(k + 1)) & k + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) & IC (Comput (F,s,k)) = n + k & IC v = n + (k + 1) & v . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = v . (dl. dn) ) )

thus v = Comput (F,s,(k + 1)) ; :: thesis: ( k + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) & IC (Comput (F,s,k)) = n + k & IC v = n + (k + 1) & v . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = v . (dl. dn) ) )

A61: Selfwork (nt,aux) = <%(Divide ((dl. aux),(dl. (aux + 1)))),((dl. aux) := (dl. (aux + 1)))%> by ;
then A62: len (Selfwork (nt,aux)) = 2 by AFINSQ_1:38;
then A63: 0 in dom (Selfwork (nt,aux)) by ;
A64: len (SCM-Compile ((nt -tree (tl,tr)),aux)) = ((i1 + 1) + (i2 + 1)) + (1 + 1) by ;
hence k + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) ; :: thesis: ( IC (Comput (F,s,k)) = n + k & IC v = n + (k + 1) & v . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = v . (dl. dn) ) )

A65: 1 in dom (Selfwork (nt,aux)) by ;
k < len (SCM-Compile ((nt -tree (tl,tr)),aux)) by ;
then k in dom (SCM-Compile ((nt -tree (tl,tr)),aux)) by AFINSQ_1:86;
then A66: F . (n + k) = (SCM-Compile ((nt -tree (tl,tr)),aux)) . k by
.= (Selfwork (nt,aux)) . 1 by
.= (dl. aux) := (dl. (aux + 1)) by A61 ;
((i1 + 1) + (i2 + 1)) + 0 = (i1 + 1) + (i2 + 1) ;
then (i1 + 1) + (i2 + 1) < len (SCM-Compile ((nt -tree (tl,tr)),aux)) by ;
then (i1 + 1) + (i2 + 1) in dom (SCM-Compile ((nt -tree (tl,tr)),aux)) by AFINSQ_1:86;
then A67: F . (n + ((i1 + 1) + (i2 + 1))) = (SCM-Compile ((nt -tree (tl,tr)),aux)) . (((i1 + 1) + (i2 + 1)) + 0) by
.= (Selfwork (nt,aux)) . 0 by
.= Divide ((dl. aux),(dl. (aux + 1))) by A61 ;
aux <> aux + 1 ;
then A68: dl. aux <> dl. (aux + 1) by AMI_3:10;
hence A69: IC (Comput (F,s,k)) = (n + ((i1 + 1) + (i2 + 1))) + 1 by
.= n + k ;
:: thesis: ( IC v = n + (k + 1) & v . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = v . (dl. dn) ) )

hence IC v = (n + k) + 1 by
.= n + (k + 1) ;
:: thesis: ( v . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = v . (dl. dn) ) )

thus v . (dl. aux) = (Comput (F,s,(((i1 + 1) + (i2 + 1)) + 1))) . (dl. (aux + 1)) by
.= (u2 . (dl. aux)) mod (u2 . (dl. (aux + 1))) by
.= (u1 . (dl. aux)) mod (tr @ u1) by
.= (nt -tree (tl,tr)) @ s by A15, A26, A24, A60, Th11 ; :: thesis: for dn being Element of NAT st dn < aux holds
s . (dl. dn) = v . (dl. dn)

let dn be Element of NAT ; :: thesis: ( dn < aux implies s . (dl. dn) = v . (dl. dn) )
assume A70: dn < aux ; :: thesis: s . (dl. dn) = v . (dl. dn)
then A71: dl. dn <> dl. aux by AMI_3:10;
A72: dn < aux + 1 by ;
then A73: u1 . (dl. dn) = u2 . (dl. dn) by A22;
dl. dn <> dl. (aux + 1) by ;
then (Comput (F,s,(((i1 + 1) + (i2 + 1)) + 1))) . (dl. dn) = u2 . (dl. dn) by ;
then s . (dl. dn) = (Comput (F,s,(((i1 + 1) + (i2 + 1)) + 1))) . (dl. dn) by ;
hence s . (dl. dn) = v . (dl. dn) by ; :: thesis: verum
end;
end;
end;
A74: for t being Terminal of SCM-AE holds S2[ root-tree t]
proof
let t be Terminal of SCM-AE; :: thesis: S2[ root-tree t]
let F be Instruction-Sequence of SCM; :: thesis: for aux, n being Element of NAT st Shift ((SCM-Compile ((),aux)),n) c= F holds
for s being b2 -started State of SCM st aux > max_Data-Loc_in () holds
ex i being Element of NAT ex u being State of SCM st
( u = Comput (F,s,(i + 1)) & i + 1 = len (SCM-Compile ((),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = () @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )

let aux, n be Element of NAT ; :: thesis: ( Shift ((SCM-Compile ((),aux)),n) c= F implies for s being n -started State of SCM st aux > max_Data-Loc_in () holds
ex i being Element of NAT ex u being State of SCM st
( u = Comput (F,s,(i + 1)) & i + 1 = len (SCM-Compile ((),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = () @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) ) )

assume A75: Shift ((SCM-Compile ((),aux)),n) c= F ; :: thesis: for s being n -started State of SCM st aux > max_Data-Loc_in () holds
ex i being Element of NAT ex u being State of SCM st
( u = Comput (F,s,(i + 1)) & i + 1 = len (SCM-Compile ((),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = () @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )

let s be n -started State of SCM; :: thesis: ( aux > max_Data-Loc_in () implies ex i being Element of NAT ex u being State of SCM st
( u = Comput (F,s,(i + 1)) & i + 1 = len (SCM-Compile ((),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = () @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) ) )

assume aux > max_Data-Loc_in () ; :: thesis: ex i being Element of NAT ex u being State of SCM st
( u = Comput (F,s,(i + 1)) & i + 1 = len (SCM-Compile ((),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = () @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )

take i = 0 ; :: thesis: ex u being State of SCM st
( u = Comput (F,s,(i + 1)) & i + 1 = len (SCM-Compile ((),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = () @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )

take u = Comput (F,s,(0 + 1)); :: thesis: ( u = Comput (F,s,(i + 1)) & i + 1 = len (SCM-Compile ((),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = () @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )

thus u = Comput (F,s,(i + 1)) ; :: thesis: ( i + 1 = len (SCM-Compile ((),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = () @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )

A76: <%((dl. aux) := (@ t))%> . 0 = (dl. aux) := (@ t) ;
A77: SCM-Compile ((),aux) = <%((dl. aux) := (@ t))%> by Th7;
hence i + 1 = len (SCM-Compile ((),aux)) by AFINSQ_1:34; :: thesis: ( IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = () @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )

A78: s = Comput (F,s,0) by EXTPRO_1:2;
hence IC (Comput (F,s,i)) = n + i by MEMSTR_0:def 12; :: thesis: ( IC u = n + (i + 1) & u . (dl. aux) = () @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )

( len <%((dl. aux) := (@ t))%> = 1 & n + 0 = n ) by AFINSQ_1:34;
then i in dom (SCM-Compile ((),aux)) by ;
then A79: ( IC s = n & F . (n + 0) = (dl. aux) := (@ t) ) by ;
hence IC u = n + (i + 1) by ; :: thesis: ( u . (dl. aux) = () @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )

thus u . (dl. aux) = s . t by
.= () @ s by Th4 ; :: thesis: for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn)

let dn be Element of NAT ; :: thesis: ( dn < aux implies s . (dl. dn) = u . (dl. dn) )
assume dn < aux ; :: thesis: s . (dl. dn) = u . (dl. dn)
then dl. dn <> dl. aux by AMI_3:10;
hence s . (dl. dn) = u . (dl. dn) by ; :: thesis: verum
end;
for term being bin-term holds S2[term] from hence for F being Instruction-Sequence of SCM
for term being bin-term
for aux, n being Element of NAT st Shift ((SCM-Compile (term,aux)),n) c= F holds
for s being b4 -started State of SCM st aux > max_Data-Loc_in term holds
ex i being Element of NAT ex u being State of SCM st
( u = Comput (F,s,(i + 1)) & i + 1 = len (SCM-Compile (term,aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = term @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) ) ; :: thesis: verum