A1: for nt being NonTerminal of SCM-AE
for tl, tr being bin-term st nt ==> <*(root-label tl),(root-label tr)*> & S2[tl] & S2[tr] holds
S2[nt -tree (tl,tr)]
proof
let nt be NonTerminal of SCM-AE; :: thesis: for tl, tr being bin-term st nt ==> <*(root-label tl),(root-label tr)*> & S2[tl] & S2[tr] holds
S2[nt -tree (tl,tr)]
let tl, tr be bin-term; :: thesis: ( nt ==> <*(root-label tl),(root-label tr)*> & S2[tl] & S2[tr] implies S2[nt -tree (tl,tr)] )
assume that
A2: nt ==> <*(root-label tl),(root-label tr)*> and
A3: S2[tl] and
A4: S2[tr] ; :: thesis: S2[nt -tree (tl,tr)]
let F be NAT -defined the Instructions of SCM -valued total Function; :: thesis: for aux, n, k being Element of NAT st Shift ((SCM-Compile ((nt -tree (tl,tr)),aux)),n) c= F holds
for s being b2 -started State-consisting of k, <*> INT 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, k be Element of NAT ; :: thesis: ( Shift ((SCM-Compile ((nt -tree (tl,tr)),aux)),n) c= F implies for s being n -started State-consisting of k, <*> INT 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-consisting of k, <*> INT 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-consisting of k, <*> INT; :: 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 Th12;
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, Th10;
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-consisting of k, <*> INT by A14, MEMSTR_0:def 9, SCM_1:23;
A18: i1 + 1 = card (SCM-Compile (tl,aux)) by A13;
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, A18, 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
A19: u2 = Comput (F,u1,(i2 + 1)) and
A20: i2 + 1 = len (SCM-Compile (tr,(aux + 1))) and
IC (Comput (F,u1,i2)) = (n + (i1 + 1)) + i2 and
A21: IC u2 = (n + (i1 + 1)) + (i2 + 1) and
A22: u2 . (dl. (aux + 1)) = tr @ u1 and
A23: for dn being Element of NAT st dn < aux + 1 holds
u1 . (dl. dn) = u2 . (dl. dn) by A4, A10, A17;
A24: u2 = Comput (F,s,((i1 + 1) + (i2 + 1))) by A12, A19, EXTPRO_1:4;
A25: now
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;
A26: aux < aux + 1 by NAT_1:13;
A27: (nt -tree (tl,tr)) @ s = nt -Meaning_on ((tl @ s),(tr @ s)) by Th7;
A28: len ((SCM-Compile (tl,aux)) ^ (SCM-Compile (tr,(aux + 1)))) = (i1 + 1) + (i2 + 1) by A13, A20, AFINSQ_1:17;
per cases ( nt = [0,0] or nt = [0,1] or nt = [0,2] or nt = [0,3] or nt = [0,4] ) by Th3;
suppose A29: nt = [0,0] ; :: thesis: ex i being Element of NAT ex u being State of SCM st
( u = Comput (F,s,(i + 1)) & i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )
then A30: 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) ) )
A31: Selfwork (nt,aux) = <%(AddTo ((dl. aux),(dl. (aux + 1))))%> by A29, Def10;
then A32: len (Selfwork (nt,aux)) = 1 by AFINSQ_1:34;
hence i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) by A11, A28, 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, A19, A21, 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, A28, A32, 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 NAT_1:44;
then A33: F . (n + i) = (SCM-Compile ((nt -tree (tl,tr)),aux)) . i by A5, FINSEQ_2:146
.= AddTo ((dl. aux),(dl. (aux + 1))) by A28, A11, A31, AFINSQ_1:36 ;
hence IC u = (n + i) + 1 by A21, A24, 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 A21, A24, A33, SCM_1:5
.= (u1 . (dl. aux)) + (tr @ u1) by A22, A23, A26
.= (nt -tree (tl,tr)) @ s by A15, A27, A25, A30, Th13 ; :: 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 A34: dn < aux ; :: thesis: s . (dl. dn) = u . (dl. dn)
then dn < aux + 1 by NAT_1:13;
then A35: u1 . (dl. dn) = u2 . (dl. dn) by A23;
dl. dn <> dl. aux by A34, AMI_3:10;
then u . (dl. dn) = u2 . (dl. dn) by A21, A24, A33, SCM_1:5;
hence s . (dl. dn) = u . (dl. dn) by A16, A34, A35; :: thesis: verum
end;
suppose A36: nt = [0,1] ; :: thesis: ex i being Element of NAT ex u being State of SCM st
( u = Comput (F,s,(i + 1)) & i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )
then A37: 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) ) )
A38: Selfwork (nt,aux) = <%(SubFrom ((dl. aux),(dl. (aux + 1))))%> by A36, Def10;
then A39: len (Selfwork (nt,aux)) = 1 by AFINSQ_1:34;
hence i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) by A11, A28, 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, A19, A21, 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, A28, A39, 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 NAT_1:44;
then A40: F . (n + i) = (SCM-Compile ((nt -tree (tl,tr)),aux)) . i by A5, FINSEQ_2:146
.= SubFrom ((dl. aux),(dl. (aux + 1))) by A11, A28, A38, AFINSQ_1:36 ;
hence IC u = (n + i) + 1 by A21, A24, 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 A21, A24, A40, SCM_1:6
.= (u1 . (dl. aux)) - (tr @ u1) by A22, A23, A26
.= (nt -tree (tl,tr)) @ s by A15, A27, A25, A37, Th13 ; :: 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 A41: dn < aux ; :: thesis: s . (dl. dn) = u . (dl. dn)
then dn < aux + 1 by NAT_1:13;
then A42: u1 . (dl. dn) = u2 . (dl. dn) by A23;
dl. dn <> dl. aux by A41, AMI_3:10;
then u . (dl. dn) = u2 . (dl. dn) by A21, A24, A40, SCM_1:6;
hence s . (dl. dn) = u . (dl. dn) by A16, A41, A42; :: thesis: verum
end;
suppose A43: nt = [0,2] ; :: thesis: ex i being Element of NAT ex u being State of SCM st
( u = Comput (F,s,(i + 1)) & i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )
then A44: 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) ) )
A45: Selfwork (nt,aux) = <%(MultBy ((dl. aux),(dl. (aux + 1))))%> by A43, Def10;
then A46: len (Selfwork (nt,aux)) = 1 by AFINSQ_1:34;
hence i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) by A11, A28, 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, A19, A21, 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, A28, A46, 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 NAT_1:44;
then A47: F . (n + i) = (SCM-Compile ((nt -tree (tl,tr)),aux)) . i by A5, FINSEQ_2:146
.= MultBy ((dl. aux),(dl. (aux + 1))) by A11, A28, A45, AFINSQ_1:36 ;
hence IC u = (n + i) + 1 by A21, A24, 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 A21, A24, A47, SCM_1:7
.= (u1 . (dl. aux)) * (tr @ u1) by A22, A23, A26
.= (nt -tree (tl,tr)) @ s by A15, A27, A25, A44, Th13 ; :: 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 A48: dn < aux ; :: thesis: s . (dl. dn) = u . (dl. dn)
then dn < aux + 1 by NAT_1:13;
then A49: u1 . (dl. dn) = u2 . (dl. dn) by A23;
dl. dn <> dl. aux by A48, AMI_3:10;
then u . (dl. dn) = u2 . (dl. dn) by A21, A24, A47, SCM_1:7;
hence s . (dl. dn) = u . (dl. dn) by A16, A48, A49; :: thesis: verum
end;
suppose A50: nt = [0,3] ; :: thesis: ex i being Element of NAT ex u being State of SCM st
( u = Comput (F,s,(i + 1)) & i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )
take i = (i1 + 1) + (i2 + 1); :: thesis: ex u being State of SCM st
( u = Comput (F,s,(i + 1)) & i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )
take u = Comput (F,s,(i + 1)); :: thesis: ( u = Comput (F,s,(i + 1)) & i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )
thus u = Comput (F,s,(i + 1)) ; :: thesis: ( i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )
A51: Selfwork (nt,aux) = <%(Divide ((dl. aux),(dl. (aux + 1))))%> by A50, Def10;
then A52: len (Selfwork (nt,aux)) = 1 by AFINSQ_1:34;
hence i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) by A11, A28, 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, A28, A52, 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 NAT_1:44;
then A53: F . (n + i) = (SCM-Compile ((nt -tree (tl,tr)),aux)) . i by A5, FINSEQ_2:146
.= Divide ((dl. aux),(dl. (aux + 1))) by A11, A28, A51, AFINSQ_1:36 ;
thus IC (Comput (F,s,i)) = n + i by A12, A19, A21, 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) ) )
A54: nt -Meaning_on ((tl @ s),(tr @ s)) = (tl @ s) div (tr @ s) by A50, Def8;
aux <> aux + 1 ;
then A55: dl. aux <> dl. (aux + 1) by AMI_3:10;
hence IC u = (n + i) + 1 by A21, A24, A53, 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 A21, A24, A53, A55, SCM_1:8
.= (u1 . (dl. aux)) div (tr @ u1) by A22, A23, A26
.= (nt -tree (tl,tr)) @ s by A15, A27, A25, A54, Th13 ; :: 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 A56: dn < aux ; :: thesis: s . (dl. dn) = u . (dl. dn)
then A57: dn < aux + 1 by NAT_1:13;
then A58: dl. dn <> dl. (aux + 1) by AMI_3:10;
A59: u1 . (dl. dn) = u2 . (dl. dn) by A23, A57;
dl. dn <> dl. aux by A56, AMI_3:10;
then u . (dl. dn) = u2 . (dl. dn) by A21, A24, A53, A55, A58, SCM_1:8;
hence s . (dl. dn) = u . (dl. dn) by A16, A56, A59; :: thesis: verum
end;
suppose A60: nt = [0,4] ; :: thesis: ex i being Element of NAT ex u being State of SCM st
( u = Comput (F,s,(i + 1)) & i + 1 = len (SCM-Compile ((nt -tree (tl,tr)),aux)) & IC (Comput (F,s,i)) = n + i & IC u = n + (i + 1) & u . (dl. aux) = (nt -tree (tl,tr)) @ s & ( for dn being Element of NAT st dn < aux holds
s . (dl. dn) = u . (dl. dn) ) )
then A61: 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) ) )
A62: Selfwork (nt,aux) = <%(Divide ((dl. aux),(dl. (aux + 1)))),((dl. aux) := (dl. (aux + 1)))%> by A60, Def10;
then A63: len (Selfwork (nt,aux)) = 2 by AFINSQ_1:38;
then A64: 0 in dom (Selfwork (nt,aux)) by CARD_1:50, TARSKI:def 2;
A65: len (SCM-Compile ((nt -tree (tl,tr)),aux)) = ((i1 + 1) + (i2 + 1)) + (1 + 1) by A11, A28, A63, 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) ) )
A66: 1 in dom (Selfwork (nt,aux)) by A63, CARD_1:50, TARSKI:def 2;
k < len (SCM-Compile ((nt -tree (tl,tr)),aux)) by A65, XREAL_1:6;
then k in dom (SCM-Compile ((nt -tree (tl,tr)),aux)) by NAT_1:44;
then A67: F . (n + k) = (SCM-Compile ((nt -tree (tl,tr)),aux)) . k by A5, FINSEQ_2:146
.= (Selfwork (nt,aux)) . 1 by A11, A28, A66, AFINSQ_1:def 3
.= (dl. aux) := (dl. (aux + 1)) by A62, AFINSQ_1:38 ;
((i1 + 1) + (i2 + 1)) + 0 = (i1 + 1) + (i2 + 1) ;
then (i1 + 1) + (i2 + 1) < len (SCM-Compile ((nt -tree (tl,tr)),aux)) by A65, XREAL_1:6;
then (i1 + 1) + (i2 + 1) in dom (SCM-Compile ((nt -tree (tl,tr)),aux)) by NAT_1:44;
then A68: F . (n + ((i1 + 1) + (i2 + 1))) = (SCM-Compile ((nt -tree (tl,tr)),aux)) . (((i1 + 1) + (i2 + 1)) + 0) by A5, FINSEQ_2:146
.= (Selfwork (nt,aux)) . 0 by A11, A28, A64, AFINSQ_1:def 3
.= Divide ((dl. aux),(dl. (aux + 1))) by A62, AFINSQ_1:38 ;
aux <> aux + 1 ;
then A69: dl. aux <> dl. (aux + 1) by AMI_3:10;
hence A70: IC (Comput (F,s,k)) = (n + ((i1 + 1) + (i2 + 1))) + 1 by A21, A24, A68, 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 A67, 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 A67, A70, SCM_1:4
.= (u2 . (dl. aux)) mod (u2 . (dl. (aux + 1))) by A21, A24, A68, A69, SCM_1:8
.= (u1 . (dl. aux)) mod (tr @ u1) by A22, A23, A26
.= (nt -tree (tl,tr)) @ s by A15, A27, A25, A61, Th13 ; :: 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 A71: dn < aux ; :: thesis: s . (dl. dn) = v . (dl. dn)
then A72: dl. dn <> dl. aux by AMI_3:10;
A73: dn < aux + 1 by A71, NAT_1:13;
then A74: u1 . (dl. dn) = u2 . (dl. dn) by A23;
dl. dn <> dl. (aux + 1) by A73, AMI_3:10;
then (Comput (F,s,(((i1 + 1) + (i2 + 1)) + 1))) . (dl. dn) = u2 . (dl. dn) by A21, A24, A68, A69, A72, SCM_1:8;
then s . (dl. dn) = (Comput (F,s,(((i1 + 1) + (i2 + 1)) + 1))) . (dl. dn) by A16, A71, A74;
hence s . (dl. dn) = v . (dl. dn) by A67, A70, A72, SCM_1:4; :: thesis: verum
end;
end;
end;
A75: for t being Terminal of SCM-AE holds S2[ root-tree t]
proof
let t be Terminal of SCM-AE; :: thesis: S2[ root-tree t]
let F be NAT -defined the Instructions of SCM -valued total Function; :: thesis: for aux, n, k being Element of NAT st Shift ((SCM-Compile ((root-tree t),aux)),n) c= F holds
for s being b2 -started State-consisting of k, <*> INT 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, k be Element of NAT ; :: thesis: ( Shift ((SCM-Compile ((root-tree t),aux)),n) c= F implies for s being n -started State-consisting of k, <*> INT 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 A76: Shift ((SCM-Compile ((root-tree t),aux)),n) c= F ; :: thesis: for s being n -started State-consisting of k, <*> INT 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-consisting of k, <*> INT; :: 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) ) )
A77: <%((dl. aux) := (@ t))%> . 0 = (dl. aux) := (@ t) by AFINSQ_1:34;
A78: SCM-Compile ((root-tree t),aux) = <%((dl. aux) := (@ t))%> by Th9;
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) ) )
A79: s = Comput (F,s,0) by EXTPRO_1:2;
hence IC (Comput (F,s,i)) = n + i by MEMSTR_0:def 9; :: 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 A78, NAT_1:44;
then A80: ( IC s = n & F . (n + 0) = (dl. aux) := (@ t) ) by A78, A77, A76, FINSEQ_2:146, MEMSTR_0:def 9;
hence IC u = n + (i + 1) by A79, 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 A79, A80, SCM_1:4
.= (root-tree t) @ s by Th6 ; :: 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 A79, A80, SCM_1:4; :: thesis: verum
end;
for term being bin-term holds S2[term] from BINTREE1:sch 2(A75, A1);
 hence for F being NAT -defined the Instructions of SCM -valued total Function
for term being bin-term
for aux, n, k being Element of NAT st Shift ((SCM-Compile (term,aux)),n) c= F holds
for s being b4 -started State-consisting of k, <*> INT 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