A1: for nt being NonTerminal of SCM-AE
for tl, tr being bin-term st nt ==> <*(root-label tl),(root-label tr)*> & S₂[tl] & S₂[tr] holds
S₂[nt -tree (tl,tr)]

proof

let nt be NonTerminal of SCM-AE; :: thesis:
let tl, tr be bin-term; :: thesis:
assume that
A2: nt ==> <*(root-label tl),(root-label tr)*> and
A3: S₂[tl] and
A4: S₂[tr] ; :: thesis:
let F be Instruction-Sequence of SCM; :: thesis:
let aux, n be Element of NAT ; :: thesis:
assume A5: Shift ((SCM-Compile ((nt -tree (tl,tr)),aux)),n) c= F ; :: thesis:
let s be n -started State of SCM; :: thesis:
assume A6: aux > max_Data-Loc_in (nt -tree (tl,tr)) ; :: thesis:
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:

let n be Element of NAT ; :: thesis:
assume n <= max_Data-Loc_in tr ; :: thesis:
then n < aux by A9, XXREAL_0:2;
hence s . (dl. n) = u1 . (dl. n) by A16; :: thesis:

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 A13, A19, AFINSQ_1:17;
not not nt = [0,0] & ... & not nt = [0,4] by Th1;

per cases ;

suppose A28: nt = [0,0] ; :: thesis:

then A29: nt -Meaning_on ((tl @ s),(tr @ s)) = (tl @ s) + (tr @ s) by Def8;
take i = (i1 + 1) + (i2 + 1); :: thesis:
take u = Comput (F,s,(i + 1)); :: thesis:
thus u = Comput (F,s,(i + 1)) ; :: thesis:
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:
thus IC (Comput (F,s,i)) = n + i by A12, A18, A20, EXTPRO_1:4; :: thesis:
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:
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:
let dn be Element of NAT ; :: thesis:
assume A33: dn < aux ; :: thesis:
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:

end;

suppose A35: nt = [0,1] ; :: thesis:

then A36: nt -Meaning_on ((tl @ s),(tr @ s)) = (tl @ s) - (tr @ s) by Def8;
take i = (i1 + 1) + (i2 + 1); :: thesis:
take u = Comput (F,s,(i + 1)); :: thesis:
thus u = Comput (F,s,(i + 1)) ; :: thesis:
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:
thus IC (Comput (F,s,i)) = n + i by A12, A18, A20, EXTPRO_1:4; :: thesis:
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:
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:
let dn be Element of NAT ; :: thesis:
assume A40: dn < aux ; :: thesis:
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:

end;

suppose A42: nt = [0,2] ; :: thesis:

then A43: nt -Meaning_on ((tl @ s),(tr @ s)) = (tl @ s) * (tr @ s) by Def8;
take i = (i1 + 1) + (i2 + 1); :: thesis:
take u = Comput (F,s,(i + 1)); :: thesis:
thus u = Comput (F,s,(i + 1)) ; :: thesis:
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:
thus IC (Comput (F,s,i)) = n + i by A12, A18, A20, EXTPRO_1:4; :: thesis:
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:
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:
let dn be Element of NAT ; :: thesis:
assume A47: dn < aux ; :: thesis:
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:

end;

suppose A49: nt = [0,3] ; :: thesis:

take i = (i1 + 1) + (i2 + 1); :: thesis:
take u = Comput (F,s,(i + 1)); :: thesis:
thus u = Comput (F,s,(i + 1)) ; :: thesis:
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:
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:
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:
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:
let dn be Element of NAT ; :: thesis:
assume A55: dn < aux ; :: thesis:
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:

end;

suppose A59: nt = [0,4] ; :: thesis:

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:
take v = Comput (F,s,(k + 1)); :: thesis:
thus v = Comput (F,s,(k + 1)) ; :: thesis:
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:
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:
hence IC v = (n + k) + 1 by A66, SCM_1:4
.= n + (k + 1) ;
:: thesis:
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:
let dn be Element of NAT ; :: thesis:
assume A70: dn < aux ; :: thesis:
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:

end;

A74: for t being Terminal of SCM-AE holds S₂[ root-tree t]

proof

let t be Terminal of SCM-AE; :: thesis:
let F be Instruction-Sequence of SCM; :: thesis:
let aux, n be Element of NAT ; :: thesis:
assume A75: Shift ((SCM-Compile ((root-tree t),aux)),n) c= F ; :: thesis:
let s be n -started State of SCM; :: thesis:
assume aux > max_Data-Loc_in (root-tree t) ; :: thesis:
take i = 0 ; :: thesis:
take u = Comput (F,s,(0 + 1)); :: thesis:
thus u = Comput (F,s,(i + 1)) ; :: thesis:
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:
A78: s = Comput (F,s,0) by EXTPRO_1:2;
hence IC (Comput (F,s,i)) = n + i by MEMSTR_0:def 12; :: thesis:
( 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:
thus u . (dl. aux) = s . t by A78, A79, SCM_1:4
.= (root-tree t) @ s by Th4 ; :: thesis:
let dn be Element of NAT ; :: thesis:
assume dn < aux ; :: thesis:
then dl. dn <> dl. aux by AMI_3:10;
hence s . (dl. dn) = u . (dl. dn) by A78, A79, SCM_1:4; :: thesis:

end;

for term being bin-term holds S₂[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₄ -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: