A1:
for nt being NonTerminal of SCM-AE

for tl, tr being bin-term st nt ==> <*(root-label tl),(root-label tr)*> & S_{2}[tl] & S_{2}[tr] holds

S_{2}[nt -tree (tl,tr)]
_{2}[ root-tree t]
_{2}[term]
from BINTREE1:sch 2(A74, A1);

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 b_{4} -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

for tl, tr being bin-term st nt ==> <*(root-label tl),(root-label tr)*> & S

S

proof

A74:
for t being Terminal of SCM-AE holds S
let nt be NonTerminal of SCM-AE; :: thesis: for tl, tr being bin-term st nt ==> <*(root-label tl),(root-label tr)*> & S_{2}[tl] & S_{2}[tr] holds

S_{2}[nt -tree (tl,tr)]

let tl, tr be bin-term; :: thesis: ( nt ==> <*(root-label tl),(root-label tr)*> & S_{2}[tl] & S_{2}[tr] implies S_{2}[nt -tree (tl,tr)] )

assume that

A2: nt ==> <*(root-label tl),(root-label tr)*> and

A3: S_{2}[tl]
and

A4: S_{2}[tr]
; :: thesis: S_{2}[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 b_{2} -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 ((max_Data-Loc_in tl),(max_Data-Loc_in tr)) 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 A6, XXREAL_0:2;

max_Data-Loc_in tr <= max_Data-Loc_in (nt -tree (tl,tr)) by A7, XXREAL_0:25;

then A9: max_Data-Loc_in tr < aux by A6, XXREAL_0:2;

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 A2, Th8;

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 A5, AFINSQ_1:82;

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 A14, MEMSTR_0:def 12;

SCM-Compile ((nt -tree (tl,tr)),aux) = (SCM-Compile (tl,aux)) ^ ((SCM-Compile (tr,(aux + 1))) ^ (Selfwork (nt,aux))) by A11, AFINSQ_1:27;

then Shift (((SCM-Compile (tr,(aux + 1))) ^ (Selfwork (nt,aux))),(n + (i1 + 1))) c= F by A5, A13, AFINSQ_1:83;

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 A12, A18, EXTPRO_1:4;

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 A13, A19, AFINSQ_1:17;

not not nt = [0,0] & ... & not nt = [0,4] by Th1;

end;S

let tl, tr be bin-term; :: thesis: ( nt ==> <*(root-label tl),(root-label tr)*> & S

assume that

A2: nt ==> <*(root-label tl),(root-label tr)*> and

A3: S

A4: S

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 b

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 ((max_Data-Loc_in tl),(max_Data-Loc_in tr)) 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 A6, XXREAL_0:2;

max_Data-Loc_in tr <= max_Data-Loc_in (nt -tree (tl,tr)) by A7, XXREAL_0:25;

then A9: max_Data-Loc_in tr < aux by A6, XXREAL_0:2;

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 A2, Th8;

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 A5, AFINSQ_1:82;

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 A14, MEMSTR_0:def 12;

SCM-Compile ((nt -tree (tl,tr)),aux) = (SCM-Compile (tl,aux)) ^ ((SCM-Compile (tr,(aux + 1))) ^ (Selfwork (nt,aux))) by A11, AFINSQ_1:27;

then Shift (((SCM-Compile (tr,(aux + 1))) ^ (Selfwork (nt,aux))),(n + (i1 + 1))) c= F by A5, A13, AFINSQ_1:83;

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 A12, A18, EXTPRO_1:4;

A24: now :: thesis: for n being Element of NAT st n <= max_Data-Loc_in tr holds

s . (dl. n) = u1 . (dl. n)

A25:
aux < aux + 1
by NAT_1:13;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 A9, XXREAL_0:2;

hence s . (dl. n) = u1 . (dl. n) by A16; :: thesis: verum

end;assume n <= max_Data-Loc_in tr ; :: thesis: s . (dl. n) = u1 . (dl. n)

then n < aux by A9, XXREAL_0:2;

hence s . (dl. n) = u1 . (dl. n) by A16; :: thesis: verum

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 A13, A19, AFINSQ_1:17;

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] )
;

end;

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) ) )

( 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 A28, Def10;

then A31: len (Selfwork (nt,aux)) = 1 by AFINSQ_1:34;

hence i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) by A11, A27, AFINSQ_1:17; :: 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 A12, A18, A20, EXTPRO_1:4; :: 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 A11, A27, A31, AFINSQ_1:17;

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 A5, VALUED_1:51

.= AddTo ((dl. aux),(dl. (aux + 1))) by A27, A11, A30, AFINSQ_1:36 ;

hence IC u = (n + i) + 1 by A20, A23, SCM_1:5

.= 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 A20, A23, A32, SCM_1:5

.= (u1 . (dl. aux)) + (tr @ u1) by A21, A22, A25

.= (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 A33, AMI_3:10;

then u . (dl. dn) = u2 . (dl. dn) by A20, A23, A32, SCM_1:5;

hence s . (dl. dn) = u . (dl. dn) by A16, A33, A34; :: thesis: verum

end;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 A28, Def10;

then A31: len (Selfwork (nt,aux)) = 1 by AFINSQ_1:34;

hence i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) by A11, A27, AFINSQ_1:17; :: 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 A12, A18, A20, EXTPRO_1:4; :: 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 A11, A27, A31, AFINSQ_1:17;

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 A5, VALUED_1:51

.= AddTo ((dl. aux),(dl. (aux + 1))) by A27, A11, A30, AFINSQ_1:36 ;

hence IC u = (n + i) + 1 by A20, A23, SCM_1:5

.= 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 A20, A23, A32, SCM_1:5

.= (u1 . (dl. aux)) + (tr @ u1) by A21, A22, A25

.= (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 A33, AMI_3:10;

then u . (dl. dn) = u2 . (dl. dn) by A20, A23, A32, SCM_1:5;

hence s . (dl. dn) = u . (dl. dn) by A16, A33, A34; :: thesis: verum

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) ) )

( 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 A35, Def10;

then A38: len (Selfwork (nt,aux)) = 1 by AFINSQ_1:34;

hence i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) by A11, A27, AFINSQ_1:17; :: 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 A12, A18, A20, EXTPRO_1:4; :: 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 A11, A27, A38, AFINSQ_1:17;

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 A5, VALUED_1:51

.= SubFrom ((dl. aux),(dl. (aux + 1))) by A11, A27, A37, AFINSQ_1:36 ;

hence IC u = (n + i) + 1 by A20, A23, SCM_1:6

.= 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 A20, A23, A39, SCM_1:6

.= (u1 . (dl. aux)) - (tr @ u1) by A21, A22, A25

.= (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 A40, AMI_3:10;

then u . (dl. dn) = u2 . (dl. dn) by A20, A23, A39, SCM_1:6;

hence s . (dl. dn) = u . (dl. dn) by A16, A40, A41; :: thesis: verum

end;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 A35, Def10;

then A38: len (Selfwork (nt,aux)) = 1 by AFINSQ_1:34;

hence i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) by A11, A27, AFINSQ_1:17; :: 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 A12, A18, A20, EXTPRO_1:4; :: 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 A11, A27, A38, AFINSQ_1:17;

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 A5, VALUED_1:51

.= SubFrom ((dl. aux),(dl. (aux + 1))) by A11, A27, A37, AFINSQ_1:36 ;

hence IC u = (n + i) + 1 by A20, A23, SCM_1:6

.= 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 A20, A23, A39, SCM_1:6

.= (u1 . (dl. aux)) - (tr @ u1) by A21, A22, A25

.= (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 A40, AMI_3:10;

then u . (dl. dn) = u2 . (dl. dn) by A20, A23, A39, SCM_1:6;

hence s . (dl. dn) = u . (dl. dn) by A16, A40, A41; :: thesis: verum

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) ) )

( 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 A42, Def10;

then A45: len (Selfwork (nt,aux)) = 1 by AFINSQ_1:34;

hence i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) by A11, A27, AFINSQ_1:17; :: 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 A12, A18, A20, EXTPRO_1:4; :: 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 A11, A27, A45, AFINSQ_1:17;

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 A5, VALUED_1:51

.= MultBy ((dl. aux),(dl. (aux + 1))) by A11, A27, A44, AFINSQ_1:36 ;

hence IC u = (n + i) + 1 by A20, A23, SCM_1:7

.= 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 A20, A23, A46, SCM_1:7

.= (u1 . (dl. aux)) * (tr @ u1) by A21, A22, A25

.= (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 A47, AMI_3:10;

then u . (dl. dn) = u2 . (dl. dn) by A20, A23, A46, SCM_1:7;

hence s . (dl. dn) = u . (dl. dn) by A16, A47, A48; :: thesis: verum

end;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 A42, Def10;

then A45: len (Selfwork (nt,aux)) = 1 by AFINSQ_1:34;

hence i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) by A11, A27, AFINSQ_1:17; :: 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 A12, A18, A20, EXTPRO_1:4; :: 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 A11, A27, A45, AFINSQ_1:17;

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 A5, VALUED_1:51

.= MultBy ((dl. aux),(dl. (aux + 1))) by A11, A27, A44, AFINSQ_1:36 ;

hence IC u = (n + i) + 1 by A20, A23, SCM_1:7

.= 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 A20, A23, A46, SCM_1:7

.= (u1 . (dl. aux)) * (tr @ u1) by A21, A22, A25

.= (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 A47, AMI_3:10;

then u . (dl. dn) = u2 . (dl. dn) by A20, A23, A46, SCM_1:7;

hence s . (dl. dn) = u . (dl. dn) by A16, A47, A48; :: thesis: verum

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) ) )

( 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 A49, Def10;

then A51: len (Selfwork (nt,aux)) = 1 by AFINSQ_1:34;

hence i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) by A11, A27, AFINSQ_1:17; :: 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 A11, A27, A51, AFINSQ_1:17;

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 A5, VALUED_1:51

.= Divide ((dl. aux),(dl. (aux + 1))) by A11, A27, A50, AFINSQ_1:36 ;

thus IC (Comput (F,s,i)) = n + i by A12, A18, A20, EXTPRO_1:4; :: 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 A49, Def8;

aux <> aux + 1 ;

then A54: dl. aux <> dl. (aux + 1) by AMI_3:10;

hence IC u = (n + i) + 1 by A20, A23, A52, SCM_1:8

.= 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 A20, A23, A52, A54, SCM_1:8

.= (u1 . (dl. aux)) div (tr @ u1) by A21, A22, A25

.= (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 A22, A56;

dl. dn <> dl. aux by A55, AMI_3:10;

then u . (dl. dn) = u2 . (dl. dn) by A20, A23, A52, A54, A57, SCM_1:8;

hence s . (dl. dn) = u . (dl. dn) by A16, A55, A58; :: thesis: verum

end;( 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 A49, Def10;

then A51: len (Selfwork (nt,aux)) = 1 by AFINSQ_1:34;

hence i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) by A11, A27, AFINSQ_1:17; :: 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 A11, A27, A51, AFINSQ_1:17;

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 A5, VALUED_1:51

.= Divide ((dl. aux),(dl. (aux + 1))) by A11, A27, A50, AFINSQ_1:36 ;

thus IC (Comput (F,s,i)) = n + i by A12, A18, A20, EXTPRO_1:4; :: 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 A49, Def8;

aux <> aux + 1 ;

then A54: dl. aux <> dl. (aux + 1) by AMI_3:10;

hence IC u = (n + i) + 1 by A20, A23, A52, SCM_1:8

.= 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 A20, A23, A52, A54, SCM_1:8

.= (u1 . (dl. aux)) div (tr @ u1) by A21, A22, A25

.= (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 A22, A56;

dl. dn <> dl. aux by A55, AMI_3:10;

then u . (dl. dn) = u2 . (dl. dn) by A20, A23, A52, A54, A57, SCM_1:8;

hence s . (dl. dn) = u . (dl. dn) by A16, A55, A58; :: thesis: verum

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) ) )

( 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 A59, Def10;

then A62: len (Selfwork (nt,aux)) = 2 by AFINSQ_1:38;

then A63: 0 in dom (Selfwork (nt,aux)) by CARD_1:50, TARSKI:def 2;

A64: len (SCM-Compile ((nt -tree (tl,tr)),aux)) = ((i1 + 1) + (i2 + 1)) + (1 + 1) by A11, A27, A62, AFINSQ_1:17;

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 A62, CARD_1:50, TARSKI:def 2;

k < len (SCM-Compile ((nt -tree (tl,tr)),aux)) by A64, XREAL_1:6;

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 A5, VALUED_1:51

.= (Selfwork (nt,aux)) . 1 by A11, A27, A65, AFINSQ_1:def 3

.= (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 A64, XREAL_1:6;

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 A5, VALUED_1:51

.= (Selfwork (nt,aux)) . 0 by A11, A27, A63, AFINSQ_1:def 3

.= 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 A20, A23, A67, SCM_1:8

.= 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 A66, SCM_1:4

.= 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 A66, A69, SCM_1:4

.= (u2 . (dl. aux)) mod (u2 . (dl. (aux + 1))) by A20, A23, A67, A68, SCM_1:8

.= (u1 . (dl. aux)) mod (tr @ u1) by A21, A22, A25

.= (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 A70, NAT_1:13;

then A73: u1 . (dl. dn) = u2 . (dl. dn) by A22;

dl. dn <> dl. (aux + 1) by A72, AMI_3:10;

then (Comput (F,s,(((i1 + 1) + (i2 + 1)) + 1))) . (dl. dn) = u2 . (dl. dn) by A20, A23, A67, A68, A71, SCM_1:8;

then s . (dl. dn) = (Comput (F,s,(((i1 + 1) + (i2 + 1)) + 1))) . (dl. dn) by A16, A70, A73;

hence s . (dl. dn) = v . (dl. dn) by A66, A69, A71, SCM_1:4; :: thesis: verum

end;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 A59, Def10;

then A62: len (Selfwork (nt,aux)) = 2 by AFINSQ_1:38;

then A63: 0 in dom (Selfwork (nt,aux)) by CARD_1:50, TARSKI:def 2;

A64: len (SCM-Compile ((nt -tree (tl,tr)),aux)) = ((i1 + 1) + (i2 + 1)) + (1 + 1) by A11, A27, A62, AFINSQ_1:17;

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 A62, CARD_1:50, TARSKI:def 2;

k < len (SCM-Compile ((nt -tree (tl,tr)),aux)) by A64, XREAL_1:6;

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 A5, VALUED_1:51

.= (Selfwork (nt,aux)) . 1 by A11, A27, A65, AFINSQ_1:def 3

.= (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 A64, XREAL_1:6;

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 A5, VALUED_1:51

.= (Selfwork (nt,aux)) . 0 by A11, A27, A63, AFINSQ_1:def 3

.= 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 A20, A23, A67, SCM_1:8

.= 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 A66, SCM_1:4

.= 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 A66, A69, SCM_1:4

.= (u2 . (dl. aux)) mod (u2 . (dl. (aux + 1))) by A20, A23, A67, A68, SCM_1:8

.= (u1 . (dl. aux)) mod (tr @ u1) by A21, A22, A25

.= (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 A70, NAT_1:13;

then A73: u1 . (dl. dn) = u2 . (dl. dn) by A22;

dl. dn <> dl. (aux + 1) by A72, AMI_3:10;

then (Comput (F,s,(((i1 + 1) + (i2 + 1)) + 1))) . (dl. dn) = u2 . (dl. dn) by A20, A23, A67, A68, A71, SCM_1:8;

then s . (dl. dn) = (Comput (F,s,(((i1 + 1) + (i2 + 1)) + 1))) . (dl. dn) by A16, A70, A73;

hence s . (dl. dn) = v . (dl. dn) by A66, A69, A71, SCM_1:4; :: thesis: verum

proof

for term being bin-term holds S
let t be Terminal of SCM-AE; :: thesis: S_{2}[ root-tree t]

let F be Instruction-Sequence of SCM; :: thesis: for aux, n being Element of NAT st Shift ((SCM-Compile ((root-tree t),aux)),n) c= F holds

for s being b_{2} -started State of SCM st aux > max_Data-Loc_in (root-tree t) 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 ((root-tree t),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (root-tree t) @ 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 ((root-tree t),aux)),n) c= F implies for s being n -started State of SCM st aux > max_Data-Loc_in (root-tree t) 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 ((root-tree t),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (root-tree t) @ s & ( for dn being Element of NAT st dn < aux holds

s . (dl. dn) = u . (dl. dn) ) ) )

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

s . (dl. dn) = u . (dl. dn) ) ) )

assume aux > max_Data-Loc_in (root-tree t) ; :: 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 ((root-tree t),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (root-tree t) @ 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 ((root-tree t),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (root-tree t) @ 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 ((root-tree t),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (root-tree t) @ 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 ((root-tree t),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (root-tree t) @ 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 ((root-tree t),aux) = <%((dl. aux) := (@ t))%> by Th7;

hence i + 1 = len (SCM-Compile ((root-tree t),aux)) by AFINSQ_1:34; :: thesis: ( IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (root-tree t) @ 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) = (root-tree t) @ 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 ((root-tree t),aux)) by A77, AFINSQ_1:86;

then A79: ( IC s = n & F . (n + 0) = (dl. aux) := (@ t) ) by A77, A76, A75, MEMSTR_0:def 12, VALUED_1:51;

hence IC u = n + (i + 1) by A78, SCM_1:4; :: thesis: ( u . (dl. aux) = (root-tree t) @ s & ( for dn being Element of NAT st dn < aux holds

s . (dl. dn) = u . (dl. dn) ) )

thus u . (dl. aux) = s . t by A78, A79, SCM_1:4

.= (root-tree t) @ 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 A78, A79, SCM_1:4; :: thesis: verum

end;let F be Instruction-Sequence of SCM; :: thesis: for aux, n being Element of NAT st Shift ((SCM-Compile ((root-tree t),aux)),n) c= F holds

for s being b

ex i being Element of NAT ex u being State of SCM st

( u = Comput (F,s,(i + 1)) & i + 1 = len (SCM-Compile ((root-tree t),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (root-tree t) @ 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 ((root-tree t),aux)),n) c= F implies for s being n -started State of SCM st aux > max_Data-Loc_in (root-tree t) 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 ((root-tree t),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (root-tree t) @ s & ( for dn being Element of NAT st dn < aux holds

s . (dl. dn) = u . (dl. dn) ) ) )

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

s . (dl. dn) = u . (dl. dn) ) ) )

assume aux > max_Data-Loc_in (root-tree t) ; :: 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 ((root-tree t),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (root-tree t) @ 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 ((root-tree t),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (root-tree t) @ 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 ((root-tree t),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (root-tree t) @ 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 ((root-tree t),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (root-tree t) @ 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 ((root-tree t),aux) = <%((dl. aux) := (@ t))%> by Th7;

hence i + 1 = len (SCM-Compile ((root-tree t),aux)) by AFINSQ_1:34; :: thesis: ( IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (root-tree t) @ 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) = (root-tree t) @ 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 ((root-tree t),aux)) by A77, AFINSQ_1:86;

then A79: ( IC s = n & F . (n + 0) = (dl. aux) := (@ t) ) by A77, A76, A75, MEMSTR_0:def 12, VALUED_1:51;

hence IC u = n + (i + 1) by A78, SCM_1:4; :: thesis: ( u . (dl. aux) = (root-tree t) @ s & ( for dn being Element of NAT st dn < aux holds

s . (dl. dn) = u . (dl. dn) ) )

thus u . (dl. aux) = s . t by A78, A79, SCM_1:4

.= (root-tree t) @ 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 A78, A79, SCM_1:4; :: thesis: verum

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 b

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