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 aux, n, k be Element of NAT ; :: thesis:
let s be State-consisting of n,n,k, SCM-Compile (nt -tree tl,tr),aux, <*> INT ; :: thesis:
assume A5: aux > max_Data-Loc_in (nt -tree tl,tr) ; :: thesis:
A6: max_Data-Loc_in (nt -tree tl,tr) = max (max_Data-Loc_in tl),(max_Data-Loc_in tr) by Th12;
then max_Data-Loc_in tl <= max_Data-Loc_in (nt -tree tl,tr) by XXREAL_0:25;
then A7: max_Data-Loc_in tl < aux by A5, XXREAL_0:2;
max_Data-Loc_in tr <= max_Data-Loc_in (nt -tree tl,tr) by A6, XXREAL_0:25;
then A8: max_Data-Loc_in tr < aux by A5, XXREAL_0:2;
then A9: max_Data-Loc_in tr < aux + 1 by NAT_1:13;
A10: SCM-Compile (nt -tree tl,tr),aux = ((SCM-Compile tl,aux) ^ (SCM-Compile tr,(aux + 1))) ^ (Selfwork nt,aux) by A2, Th10;
then A11: SCM-Compile (nt -tree tl,tr),aux = (SCM-Compile tl,aux) ^ ((SCM-Compile tr,(aux + 1)) ^ (Selfwork nt,aux)) by FINSEQ_1:45;
then s is State-consisting of n,n,k, SCM-Compile tl,aux, <*> INT by Th1;
then consider i1 being Element of NAT , u1 being State of SCM such that
A12: u1 = Computation s,(i1 + 1) and
A13: i1 + 1 = len (SCM-Compile tl,aux) and
IC (Computation s,i1) = il. (n + i1) and
A14: IC u1 = il. (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, A7;
u1 is State-consisting of n + (i1 + 1),n + (i1 + 1),k,(SCM-Compile tr,(aux + 1)) ^ (Selfwork nt,aux), <*> INT by A11, A12, A13, A14, Th2;
then u1 is State-consisting of n + (i1 + 1),n + (i1 + 1),k, SCM-Compile tr,(aux + 1), <*> INT by Th1;
then consider i2 being Element of NAT , u2 being State of SCM such that
A17: u2 = Computation u1,(i2 + 1) and
A18: i2 + 1 = len (SCM-Compile tr,(aux + 1)) and
IC (Computation u1,i2) = il. ((n + (i1 + 1)) + i2) and
A19: IC u2 = il. ((n + (i1 + 1)) + (i2 + 1)) and
A20: u2 . (dl. (aux + 1)) = tr @ u1 and
A21: for dn being Element of NAT st dn < aux + 1 holds
u1 . (dl. dn) = u2 . (dl. dn) by A4, A9;
A22: u2 = Computation s,((i1 + 1) + (i2 + 1)) by A12, A17, AMI_1:51;

A23: now

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

end;

A24: aux < aux + 1 by NAT_1:13;
A25: (nt -tree tl,tr) @ s = nt -Meaning_on (tl @ s),(tr @ s) by Th7;
A26: len ((SCM-Compile tl,aux) ^ (SCM-Compile tr,(aux + 1))) = (i1 + 1) + (i2 + 1) by A13, A18, FINSEQ_1:35;

per cases by Th3;

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

then A28: nt -Meaning_on (tl @ s),(tr @ s) = (tl @ s) + (tr @ s) by Def8;
take i = (i1 + 1) + (i2 + 1); :: thesis:
take u = Computation s,(i + 1); :: thesis:
thus u = Computation s,(i + 1) ; :: thesis:
A29: Selfwork nt,aux = <*(AddTo (dl. aux),(dl. (aux + 1)))*> by A27, Def10;
then A30: len (Selfwork nt,aux) = 1 by FINSEQ_1:57;
hence i + 1 = len (SCM-Compile (nt -tree tl,tr),aux) by A10, A26, FINSEQ_1:35; :: thesis:
thus IC (Computation s,i) = il. (n + i) by A12, A17, A19, AMI_1:51; :: thesis:
len (SCM-Compile (nt -tree tl,tr),aux) = ((i1 + 1) + (i2 + 1)) + 1 by A10, A26, A30, FINSEQ_1:35;
then i < len (SCM-Compile (nt -tree tl,tr),aux) by NAT_1:13;
then A31: s . (il. (n + i)) = (SCM-Compile (nt -tree tl,tr),aux) . (i + 1) by SCM_1:def 1
.= AddTo (dl. aux),(dl. (aux + 1)) by A10, A26, A29, FINSEQ_1:59 ;
hence IC u = il. ((n + i) + 1) by A19, A22, SCM_1:19
.= il. (n + (i + 1)) ;
:: thesis:
thus u . (dl. aux) = (u2 . (dl. aux)) + (u2 . (dl. (aux + 1))) by A19, A22, A31, SCM_1:19
.= (u1 . (dl. aux)) + (tr @ u1) by A20, A21, A24
.= (nt -tree tl,tr) @ s by A15, A25, A23, A28, Th13 ; :: thesis:
let dn be Element of NAT ; :: thesis:
assume A32: dn < aux ; :: thesis:
then dn < aux + 1 by NAT_1:13;
then A33: u1 . (dl. dn) = u2 . (dl. dn) by A21;
dl. dn <> dl. aux by A32, AMI_3:52;
then u . (dl. dn) = u2 . (dl. dn) by A19, A22, A31, SCM_1:19;
hence s . (dl. dn) = u . (dl. dn) by A16, A32, A33; :: thesis:

end;

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

then A35: nt -Meaning_on (tl @ s),(tr @ s) = (tl @ s) - (tr @ s) by Def8;
take i = (i1 + 1) + (i2 + 1); :: thesis:
take u = Computation s,(i + 1); :: thesis:
thus u = Computation s,(i + 1) ; :: thesis:
A36: Selfwork nt,aux = <*(SubFrom (dl. aux),(dl. (aux + 1)))*> by A34, Def10;
then A37: len (Selfwork nt,aux) = 1 by FINSEQ_1:57;
hence i + 1 = len (SCM-Compile (nt -tree tl,tr),aux) by A10, A26, FINSEQ_1:35; :: thesis:
thus IC (Computation s,i) = il. (n + i) by A12, A17, A19, AMI_1:51; :: thesis:
len (SCM-Compile (nt -tree tl,tr),aux) = ((i1 + 1) + (i2 + 1)) + 1 by A10, A26, A37, FINSEQ_1:35;
then i < len (SCM-Compile (nt -tree tl,tr),aux) by NAT_1:13;
then A38: s . (il. (n + i)) = (SCM-Compile (nt -tree tl,tr),aux) . (i + 1) by SCM_1:def 1
.= SubFrom (dl. aux),(dl. (aux + 1)) by A10, A26, A36, FINSEQ_1:59 ;
hence IC u = il. ((n + i) + 1) by A19, A22, SCM_1:20
.= il. (n + (i + 1)) ;
:: thesis:
thus u . (dl. aux) = (u2 . (dl. aux)) - (u2 . (dl. (aux + 1))) by A19, A22, A38, SCM_1:20
.= (u1 . (dl. aux)) - (tr @ u1) by A20, A21, A24
.= (nt -tree tl,tr) @ s by A15, A25, A23, A35, Th13 ; :: thesis:
let dn be Element of NAT ; :: thesis:
assume A39: dn < aux ; :: thesis:
then dn < aux + 1 by NAT_1:13;
then A40: u1 . (dl. dn) = u2 . (dl. dn) by A21;
dl. dn <> dl. aux by A39, AMI_3:52;
then u . (dl. dn) = u2 . (dl. dn) by A19, A22, A38, SCM_1:20;
hence s . (dl. dn) = u . (dl. dn) by A16, A39, A40; :: thesis:

end;

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

then A42: nt -Meaning_on (tl @ s),(tr @ s) = (tl @ s) * (tr @ s) by Def8;
take i = (i1 + 1) + (i2 + 1); :: thesis:
take u = Computation s,(i + 1); :: thesis:
thus u = Computation s,(i + 1) ; :: thesis:
A43: Selfwork nt,aux = <*(MultBy (dl. aux),(dl. (aux + 1)))*> by A41, Def10;
then A44: len (Selfwork nt,aux) = 1 by FINSEQ_1:57;
hence i + 1 = len (SCM-Compile (nt -tree tl,tr),aux) by A10, A26, FINSEQ_1:35; :: thesis:
thus IC (Computation s,i) = il. (n + i) by A12, A17, A19, AMI_1:51; :: thesis:
len (SCM-Compile (nt -tree tl,tr),aux) = ((i1 + 1) + (i2 + 1)) + 1 by A10, A26, A44, FINSEQ_1:35;
then i < len (SCM-Compile (nt -tree tl,tr),aux) by NAT_1:13;
then A45: s . (il. (n + i)) = (SCM-Compile (nt -tree tl,tr),aux) . (i + 1) by SCM_1:def 1
.= MultBy (dl. aux),(dl. (aux + 1)) by A10, A26, A43, FINSEQ_1:59 ;
hence IC u = il. ((n + i) + 1) by A19, A22, SCM_1:21
.= il. (n + (i + 1)) ;
:: thesis:
thus u . (dl. aux) = (u2 . (dl. aux)) * (u2 . (dl. (aux + 1))) by A19, A22, A45, SCM_1:21
.= (u1 . (dl. aux)) * (tr @ u1) by A20, A21, A24
.= (nt -tree tl,tr) @ s by A15, A25, A23, A42, Th13 ; :: thesis:
let dn be Element of NAT ; :: thesis:
assume A46: dn < aux ; :: thesis:
then dn < aux + 1 by NAT_1:13;
then A47: u1 . (dl. dn) = u2 . (dl. dn) by A21;
dl. dn <> dl. aux by A46, AMI_3:52;
then u . (dl. dn) = u2 . (dl. dn) by A19, A22, A45, SCM_1:21;
hence s . (dl. dn) = u . (dl. dn) by A16, A46, A47; :: thesis:

end;

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

take i = (i1 + 1) + (i2 + 1); :: thesis:
take u = Computation s,(i + 1); :: thesis:
thus u = Computation s,(i + 1) ; :: thesis:
A49: Selfwork nt,aux = <*(Divide (dl. aux),(dl. (aux + 1)))*> by A48, Def10;
then A50: len (Selfwork nt,aux) = 1 by FINSEQ_1:57;
hence i + 1 = len (SCM-Compile (nt -tree tl,tr),aux) by A10, A26, FINSEQ_1:35; :: thesis:
len (SCM-Compile (nt -tree tl,tr),aux) = ((i1 + 1) + (i2 + 1)) + 1 by A10, A26, A50, FINSEQ_1:35;
then i < len (SCM-Compile (nt -tree tl,tr),aux) by NAT_1:13;
then A51: s . (il. (n + i)) = (SCM-Compile (nt -tree tl,tr),aux) . (i + 1) by SCM_1:def 1
.= Divide (dl. aux),(dl. (aux + 1)) by A10, A26, A49, FINSEQ_1:59 ;
thus IC (Computation s,i) = il. (n + i) by A12, A17, A19, AMI_1:51; :: thesis:
A52: nt -Meaning_on (tl @ s),(tr @ s) = (tl @ s) div (tr @ s) by A48, Def8;
aux <> aux + 1 ;
then A53: dl. aux <> dl. (aux + 1) by AMI_3:52;
hence IC u = il. ((n + i) + 1) by A19, A22, A51, SCM_1:22
.= il. (n + (i + 1)) ;
:: thesis:
thus u . (dl. aux) = (u2 . (dl. aux)) div (u2 . (dl. (aux + 1))) by A19, A22, A51, A53, SCM_1:22
.= (u1 . (dl. aux)) div (tr @ u1) by A20, A21, A24
.= (nt -tree tl,tr) @ s by A15, A25, A23, A52, Th13 ; :: thesis:
let dn be Element of NAT ; :: thesis:
assume A54: dn < aux ; :: thesis:
then A55: dn < aux + 1 by NAT_1:13;
then A56: dl. dn <> dl. (aux + 1) by AMI_3:52;
A57: u1 . (dl. dn) = u2 . (dl. dn) by A21, A55;
dl. dn <> dl. aux by A54, AMI_3:52;
then u . (dl. dn) = u2 . (dl. dn) by A19, A22, A51, A53, A56, SCM_1:22;
hence s . (dl. dn) = u . (dl. dn) by A16, A54, A57; :: thesis:

end;

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

then A59: nt -Meaning_on (tl @ s),(tr @ s) = (tl @ s) mod (tr @ s) by Def8;
set i = (i1 + 1) + (i2 + 1);
set u = Computation s,(((i1 + 1) + (i2 + 1)) + 1);
take k = ((i1 + 1) + (i2 + 1)) + 1; :: thesis:
take v = Computation s,(k + 1); :: thesis:
thus v = Computation s,(k + 1) ; :: thesis:
A60: 1 in Seg 2 by FINSEQ_1:4, TARSKI:def 2;
A61: Selfwork nt,aux = <*(Divide (dl. aux),(dl. (aux + 1))),((dl. aux) := (dl. (aux + 1)))*> by A58, Def10;
then A62: len (Selfwork nt,aux) = 2 by FINSEQ_1:61;
then A63: dom (Selfwork nt,aux) = Seg 2 by FINSEQ_1:def 3;
A64: len (SCM-Compile (nt -tree tl,tr),aux) = ((i1 + 1) + (i2 + 1)) + (1 + 1) by A10, A26, A62, FINSEQ_1:35;
hence k + 1 = len (SCM-Compile (nt -tree tl,tr),aux) ; :: thesis:
A65: 2 in Seg 2 by FINSEQ_1:4, TARSKI:def 2;
k < len (SCM-Compile (nt -tree tl,tr),aux) by A64, XREAL_1:8;
then A66: s . (il. (n + k)) = (SCM-Compile (nt -tree tl,tr),aux) . (k + 1) by SCM_1:def 1
.= (SCM-Compile (nt -tree tl,tr),aux) . (((i1 + 1) + (i2 + 1)) + (1 + 1))
.= <*(Divide (dl. aux),(dl. (aux + 1))),((dl. aux) := (dl. (aux + 1)))*> . 2 by A10, A26, A61, A63, A65, FINSEQ_1:def 7
.= (dl. aux) := (dl. (aux + 1)) by FINSEQ_1:61 ;
((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:8;
then A67: s . (il. (n + ((i1 + 1) + (i2 + 1)))) = (SCM-Compile (nt -tree tl,tr),aux) . (((i1 + 1) + (i2 + 1)) + 1) by SCM_1:def 1
.= <*(Divide (dl. aux),(dl. (aux + 1))),((dl. aux) := (dl. (aux + 1)))*> . 1 by A10, A26, A61, A63, A60, FINSEQ_1:def 7
.= Divide (dl. aux),(dl. (aux + 1)) by FINSEQ_1:61 ;
aux <> aux + 1 ;
then A68: dl. aux <> dl. (aux + 1) by AMI_3:52;
hence A69: IC (Computation s,k) = il. ((n + ((i1 + 1) + (i2 + 1))) + 1) by A19, A22, A67, SCM_1:22
.= il. (n + k) ;
:: thesis:
hence IC v = il. ((n + k) + 1) by A66, SCM_1:18
.= il. (n + (k + 1)) ;
:: thesis:
thus v . (dl. aux) = (Computation s,(((i1 + 1) + (i2 + 1)) + 1)) . (dl. (aux + 1)) by A66, A69, SCM_1:18
.= (u2 . (dl. aux)) mod (u2 . (dl. (aux + 1))) by A19, A22, A67, A68, SCM_1:22
.= (u1 . (dl. aux)) mod (tr @ u1) by A20, A21, A24
.= (nt -tree tl,tr) @ s by A15, A25, A23, A59, Th13 ; :: thesis:
let dn be Element of NAT ; :: thesis:
assume A70: dn < aux ; :: thesis:
then A71: dl. dn <> dl. aux by AMI_3:52;
A72: dn < aux + 1 by A70, NAT_1:13;
then A73: u1 . (dl. dn) = u2 . (dl. dn) by A21;
dl. dn <> dl. (aux + 1) by A72, AMI_3:52;
then (Computation s,(((i1 + 1) + (i2 + 1)) + 1)) . (dl. dn) = u2 . (dl. dn) by A19, A22, A67, A68, A71, SCM_1:22;
then s . (dl. dn) = (Computation 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:18; :: 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 aux, n, k be Element of NAT ; :: thesis:
let s be State-consisting of n,n,k, SCM-Compile (root-tree t),aux, <*> INT ; :: thesis:
assume aux > max_Data-Loc_in (root-tree t) ; :: thesis:
take i = 0 ; :: thesis:
take u = Computation s,1; :: thesis:
thus u = Computation s,(i + 1) ; :: thesis:
A75: <*((dl. aux) := (@ t))*> . (0 + 1) = (dl. aux) := (@ t) by FINSEQ_1:57;
A76: SCM-Compile (root-tree t),aux = <*((dl. aux) := (@ t))*> by Th9;
hence i + 1 = len (SCM-Compile (root-tree t),aux) by FINSEQ_1:57; :: thesis:
A77: s = Computation s,0 by AMI_1:13;
hence IC (Computation s,i) = il. (n + i) by SCM_1:def 1; :: thesis:
( len <*((dl. aux) := (@ t))*> = 1 & n + 0 = n ) by FINSEQ_1:57;
then A78: ( IC s = il. n & s . (il. n) = (dl. aux) := (@ t) ) by A76, A75, SCM_1:def 1;
hence IC u = il. (n + (i + 1)) by A77, SCM_1:18; :: thesis:
thus u . (dl. aux) = s . t by A75, A77, A78, SCM_1:18
.= (root-tree t) @ s by Th6 ; :: thesis:
let dn be Element of NAT ; :: thesis:
assume dn < aux ; :: thesis:
then dl. dn <> dl. aux by AMI_3:52;
hence s . (dl. dn) = u . (dl. dn) by A75, A77, A78, SCM_1:18; :: thesis:

end;

thus for term being bin-term holds S₂[term] from BINTREE1:sch 2(A74, A1); :: thesis: