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 AFINSQ_1:30;
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 = Comput (ProgramPart s),s,(i1 + 1) and
A13: i1 + 1 = len (SCM-Compile tl,aux) and
IC (Comput (ProgramPart s),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, 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 = Comput (ProgramPart u1),u1,(i2 + 1) and
A18: i2 + 1 = len (SCM-Compile tr,(aux + 1)) and
IC (Comput (ProgramPart u1),u1,i2) = (n + (i1 + 1)) + i2 and
A19: IC u2 = (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;
S: ProgramPart s = ProgramPart u1 by A12, AMI_1:144;
then A22: u2 = Comput (ProgramPart s),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, AFINSQ_1:20;

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 = Comput (ProgramPart s),s,(i + 1); :: thesis:
thus u = Comput (ProgramPart s),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 AFINSQ_1:38;
hence i + 1 = len (SCM-Compile (nt -tree tl,tr),aux) by A10, A26, AFINSQ_1:20; :: thesis:
thus IC (Comput (ProgramPart s),s,i) = n + i by A12, A17, A19, AMI_1:51, S; :: thesis:
len (SCM-Compile (nt -tree tl,tr),aux) = ((i1 + 1) + (i2 + 1)) + 1 by A10, A26, A30, AFINSQ_1:20;
then i < len (SCM-Compile (nt -tree tl,tr),aux) by NAT_1:13;
then A31: s . (n + i) = (SCM-Compile (nt -tree tl,tr),aux) . i by SCM_1:def 1
.= AddTo (dl. aux),(dl. (aux + 1)) by A26, A10, A29, AFINSQ_1:40 ;
hence IC u = (n + i) + 1 by A19, A22, SCM_1:19
.= 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 = Comput (ProgramPart s),s,(i + 1); :: thesis:
thus u = Comput (ProgramPart s),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 AFINSQ_1:38;
hence i + 1 = len (SCM-Compile (nt -tree tl,tr),aux) by A10, A26, AFINSQ_1:20; :: thesis:
thus IC (Comput (ProgramPart s),s,i) = n + i by A12, A17, A19, AMI_1:51, S; :: thesis:
len (SCM-Compile (nt -tree tl,tr),aux) = ((i1 + 1) + (i2 + 1)) + 1 by A10, A26, A37, AFINSQ_1:20;
then i < len (SCM-Compile (nt -tree tl,tr),aux) by NAT_1:13;
then A38: s . (n + i) = (SCM-Compile (nt -tree tl,tr),aux) . i by SCM_1:def 1
.= SubFrom (dl. aux),(dl. (aux + 1)) by A10, A26, A36, AFINSQ_1:40 ;
hence IC u = (n + i) + 1 by A19, A22, SCM_1:20
.= 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 = Comput (ProgramPart s),s,(i + 1); :: thesis:
thus u = Comput (ProgramPart s),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 AFINSQ_1:38;
hence i + 1 = len (SCM-Compile (nt -tree tl,tr),aux) by A10, A26, AFINSQ_1:20; :: thesis:
thus IC (Comput (ProgramPart s),s,i) = n + i by A12, A17, A19, AMI_1:51, S; :: thesis:
len (SCM-Compile (nt -tree tl,tr),aux) = ((i1 + 1) + (i2 + 1)) + 1 by A10, A26, A44, AFINSQ_1:20;
then i < len (SCM-Compile (nt -tree tl,tr),aux) by NAT_1:13;
then A45: s . (n + i) = (SCM-Compile (nt -tree tl,tr),aux) . i by SCM_1:def 1
.= MultBy (dl. aux),(dl. (aux + 1)) by A10, A26, A43, AFINSQ_1:40 ;
hence IC u = (n + i) + 1 by A19, A22, SCM_1:21
.= 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 = Comput (ProgramPart s),s,(i + 1); :: thesis:
thus u = Comput (ProgramPart s),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 AFINSQ_1:38;
hence i + 1 = len (SCM-Compile (nt -tree tl,tr),aux) by A10, A26, AFINSQ_1:20; :: thesis:
len (SCM-Compile (nt -tree tl,tr),aux) = ((i1 + 1) + (i2 + 1)) + 1 by A10, A26, A50, AFINSQ_1:20;
then i < len (SCM-Compile (nt -tree tl,tr),aux) by NAT_1:13;
then A51: s . (n + i) = (SCM-Compile (nt -tree tl,tr),aux) . i by SCM_1:def 1
.= Divide (dl. aux),(dl. (aux + 1)) by A10, A26, A49, AFINSQ_1:40 ;
thus IC (Comput (ProgramPart s),s,i) = n + i by A12, A17, A19, AMI_1:51, S; :: 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 = (n + i) + 1 by A19, A22, A51, SCM_1:22
.= 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 = Comput (ProgramPart s),s,(((i1 + 1) + (i2 + 1)) + 1);
take k = ((i1 + 1) + (i2 + 1)) + 1; :: thesis:
take v = Comput (ProgramPart s),s,(k + 1); :: thesis:
thus v = Comput (ProgramPart s),s,(k + 1) ; :: thesis:
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 AFINSQ_1:42;
then A60: 0 in dom (Selfwork nt,aux) by CARD_1:88, TARSKI:def 2;
A64: len (SCM-Compile (nt -tree tl,tr),aux) = ((i1 + 1) + (i2 + 1)) + (1 + 1) by A10, A26, A62, AFINSQ_1:20;
hence k + 1 = len (SCM-Compile (nt -tree tl,tr),aux) ; :: thesis:
A65: 1 in dom (Selfwork nt,aux) by A62, CARD_1:88, TARSKI:def 2;
k < len (SCM-Compile (nt -tree tl,tr),aux) by A64, XREAL_1:8;
then A66: s . (n + k) = (SCM-Compile (nt -tree tl,tr),aux) . k by SCM_1:def 1
.= (Selfwork nt,aux) . 1 by A10, A26, A65, AFINSQ_1:def 4
.= (dl. aux) := (dl. (aux + 1)) by A61, AFINSQ_1:42 ;
((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 . (n + ((i1 + 1) + (i2 + 1))) = (SCM-Compile (nt -tree tl,tr),aux) . (((i1 + 1) + (i2 + 1)) + 0 ) by SCM_1:def 1
.= (Selfwork nt,aux) . 0 by A10, A26, A60, AFINSQ_1:def 4
.= Divide (dl. aux),(dl. (aux + 1)) by A61, AFINSQ_1:42 ;
aux <> aux + 1 ;
then A68: dl. aux <> dl. (aux + 1) by AMI_3:52;
hence A69: IC (Comput (ProgramPart s),s,k) = (n + ((i1 + 1) + (i2 + 1))) + 1 by A19, A22, A67, SCM_1:22
.= n + k ;
:: thesis:
hence IC v = (n + k) + 1 by A66, SCM_1:18
.= n + (k + 1) ;
:: thesis:
thus v . (dl. aux) = (Comput (ProgramPart s),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 (Comput (ProgramPart s),s,(((i1 + 1) + (i2 + 1)) + 1)) . (dl. dn) = u2 . (dl. dn) by A19, A22, A67, A68, A71, SCM_1:22;
then s . (dl. dn) = (Comput (ProgramPart s),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 = Comput (ProgramPart s),s,(0 + 1); :: thesis:
thus u = Comput (ProgramPart s),s,(i + 1) ; :: thesis:
A75: <%((dl. aux) := (@ t))%> . 0 = (dl. aux) := (@ t) by AFINSQ_1:38;
A76: SCM-Compile (root-tree t),aux = <%((dl. aux) := (@ t))%> by Th9;
hence i + 1 = len (SCM-Compile (root-tree t),aux) by AFINSQ_1:38; :: thesis:
A77: s = Comput (ProgramPart s),s,0 by AMI_1:13;
hence IC (Comput (ProgramPart s),s,i) = n + i by SCM_1:def 1; :: thesis:
( len <%((dl. aux) := (@ t))%> = 1 & n + 0 = n ) by AFINSQ_1:38;
then A78: ( IC s = n & s . n = (dl. aux) := (@ t) ) by A76, A75, SCM_1:def 1;
hence IC u = n + (i + 1) by A77, SCM_1:18; :: thesis:
thus u . (dl. aux) = s . t by 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 A77, A78, SCM_1:18; :: thesis:

end;

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