A1:
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 aux,
n,
k be
Element of
NAT ;
:: thesis: for s being State-consisting of n,n,k, SCM-Compile (root-tree t),aux, <*> 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 = Computation s,(i + 1) & i + 1 = len (SCM-Compile (root-tree t),aux) & IC (Computation s,i) = il. (n + i) & IC u = il. (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
State-consisting of
n,
n,
k,
SCM-Compile (root-tree t),
aux,
<*> 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 = Computation s,(i + 1) & i + 1 = len (SCM-Compile (root-tree t),aux) & IC (Computation s,i) = il. (n + i) & IC u = il. (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 = Computation s,(i + 1) & i + 1 = len (SCM-Compile (root-tree t),aux) & IC (Computation s,i) = il. (n + i) & IC u = il. (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 = Computation s,(i + 1) & i + 1 = len (SCM-Compile (root-tree t),aux) & IC (Computation s,i) = il. (n + i) & IC u = il. (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 =
Computation s,1;
:: thesis: ( u = Computation s,(i + 1) & i + 1 = len (SCM-Compile (root-tree t),aux) & IC (Computation s,i) = il. (n + i) & IC u = il. (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 = Computation s,
(i + 1)
;
:: thesis: ( i + 1 = len (SCM-Compile (root-tree t),aux) & IC (Computation s,i) = il. (n + i) & IC u = il. (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) ) )
A2:
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: ( IC (Computation s,i) = il. (n + i) & IC u = il. (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) ) )
A3:
(
len <*((dl. aux) := (@ t))*> = 1 &
0 < 1 &
n + 0 = n &
<*((dl. aux) := (@ t))*> . (0 + 1) = (dl. aux) := (@ t) )
by FINSEQ_1:57;
then A4:
(
s = Computation s,
0 &
IC s = il. n &
s . (il. n) = (dl. aux) := (@ t) )
by A2, AMI_1:13, SCM_1:def 1;
hence
IC (Computation s,i) = il. (n + i)
;
:: thesis: ( IC u = il. (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
IC u = il. (n + (i + 1))
by A4, SCM_1:18;
:: 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 A3, A4, SCM_1:18
.=
(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:52;
hence
s . (dl. dn) = u . (dl. dn)
by A3, A4, SCM_1:18;
:: thesis: verum
end;
A5:
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 A6:
(
nt ==> <*(root-label tl),(root-label tr)*> &
S2[
tl] &
S2[
tr] )
;
:: thesis: S2[nt -tree tl,tr]
let aux,
n,
k be
Element of
NAT ;
:: thesis: for s being State-consisting of n,n,k, SCM-Compile (nt -tree tl,tr),aux, <*> 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 = Computation s,(i + 1) & i + 1 = len (SCM-Compile (nt -tree tl,tr),aux) & IC (Computation s,i) = il. (n + i) & IC u = il. (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
State-consisting of
n,
n,
k,
SCM-Compile (nt -tree tl,tr),
aux,
<*> 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 = Computation s,(i + 1) & i + 1 = len (SCM-Compile (nt -tree tl,tr),aux) & IC (Computation s,i) = il. (n + i) & IC u = il. (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 A7:
aux > max_Data-Loc_in (nt -tree tl,tr)
;
:: thesis: ex i being Element of NAT ex u being State of SCM st
( u = Computation s,(i + 1) & i + 1 = len (SCM-Compile (nt -tree tl,tr),aux) & IC (Computation s,i) = il. (n + i) & IC u = il. (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) ) )
A8:
SCM-Compile (nt -tree tl,tr),
aux = ((SCM-Compile tl,aux) ^ (SCM-Compile tr,(aux + 1))) ^ (Selfwork nt,aux)
by A6, Th10;
then A9:
SCM-Compile (nt -tree tl,tr),
aux = (SCM-Compile tl,aux) ^ ((SCM-Compile tr,(aux + 1)) ^ (Selfwork nt,aux))
by FINSEQ_1:45;
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) &
max_Data-Loc_in tr <= max_Data-Loc_in (nt -tree tl,tr) )
by XXREAL_0:25;
then A10:
(
max_Data-Loc_in tl < aux &
max_Data-Loc_in tr < aux )
by A7, XXREAL_0:2;
then A11:
max_Data-Loc_in tr < aux + 1
by NAT_1:13;
s is
State-consisting of
n,
n,
k,
SCM-Compile tl,
aux,
<*> INT
by A9, Th1;
then consider i1 being
Element of
NAT ,
u1 being
State of
SCM such that A12:
(
u1 = Computation s,
(i1 + 1) &
i1 + 1
= len (SCM-Compile tl,aux) &
IC (Computation s,i1) = il. (n + i1) &
IC u1 = il. (n + (i1 + 1)) &
u1 . (dl. aux) = tl @ s & ( for
dn being
Element of
NAT st
dn < aux holds
s . (dl. dn) = u1 . (dl. dn) ) )
by A6, A10;
u1 is
State-consisting of
n + (i1 + 1),
n + (i1 + 1),
k,
(SCM-Compile tr,(aux + 1)) ^ (Selfwork nt,aux),
<*> INT
by A9, A12, 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 A13:
(
u2 = Computation u1,
(i2 + 1) &
i2 + 1
= len (SCM-Compile tr,(aux + 1)) &
IC (Computation u1,i2) = il. ((n + (i1 + 1)) + i2) &
IC u2 = il. ((n + (i1 + 1)) + (i2 + 1)) &
u2 . (dl. (aux + 1)) = tr @ u1 & ( for
dn being
Element of
NAT st
dn < aux + 1 holds
u1 . (dl. dn) = u2 . (dl. dn) ) )
by A6, A11;
A14:
u2 = Computation s,
((i1 + 1) + (i2 + 1))
by A12, A13, AMI_1:51;
A15:
(nt -tree tl,tr) @ s = nt -Meaning_on (tl @ s),
(tr @ s)
by Th7;
A17:
aux < aux + 1
by NAT_1:13;
A18:
len ((SCM-Compile tl,aux) ^ (SCM-Compile tr,(aux + 1))) = (i1 + 1) + (i2 + 1)
by A12, A13, FINSEQ_1:35;
per cases
( nt = [0 ,0 ] or nt = [0 ,1] or nt = [0 ,2] or nt = [0 ,3] or nt = [0 ,4] )
by Th3;
suppose
nt = [0 ,0 ]
;
:: thesis: ex i being Element of NAT ex u being State of SCM st
( u = Computation s,(i + 1) & i + 1 = len (SCM-Compile (nt -tree tl,tr),aux) & IC (Computation s,i) = il. (n + i) & IC u = il. (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 A19:
(
Selfwork nt,
aux = <*(AddTo (dl. aux),(dl. (aux + 1)))*> &
nt -Meaning_on (tl @ s),
(tr @ s) = (tl @ s) + (tr @ s) )
by Def8, Def10;
take i =
(i1 + 1) + (i2 + 1);
:: thesis: ex u being State of SCM st
( u = Computation s,(i + 1) & i + 1 = len (SCM-Compile (nt -tree tl,tr),aux) & IC (Computation s,i) = il. (n + i) & IC u = il. (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 =
Computation s,
(i + 1);
:: thesis: ( u = Computation s,(i + 1) & i + 1 = len (SCM-Compile (nt -tree tl,tr),aux) & IC (Computation s,i) = il. (n + i) & IC u = il. (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 = Computation s,
(i + 1)
;
:: thesis: ( i + 1 = len (SCM-Compile (nt -tree tl,tr),aux) & IC (Computation s,i) = il. (n + i) & IC u = il. (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) ) )A20:
len (Selfwork nt,aux) = 1
by A19, FINSEQ_1:57;
then
len (SCM-Compile (nt -tree tl,tr),aux) = ((i1 + 1) + (i2 + 1)) + 1
by A8, A18, FINSEQ_1:35;
then
i < len (SCM-Compile (nt -tree tl,tr),aux)
by NAT_1:13;
then A21:
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 A8, A18, A19, FINSEQ_1:59
;
thus
i + 1
= len (SCM-Compile (nt -tree tl,tr),aux)
by A8, A18, A20, FINSEQ_1:35;
:: thesis: ( IC (Computation s,i) = il. (n + i) & IC u = il. (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 (Computation s,i) = il. (n + i)
by A12, A13, AMI_1:51;
:: thesis: ( IC u = il. (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 u =
il. ((n + i) + 1)
by A13, A14, A21, SCM_1:19
.=
il. (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 A13, A14, A21, SCM_1:19
.=
(u1 . (dl. aux)) + (tr @ u1)
by A13, A17
.=
(nt -tree tl,tr) @ s
by A12, A15, A16, A19, 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 A22:
dn < aux
;
:: thesis: s . (dl. dn) = u . (dl. dn)then
dl. dn <> dl. aux
by AMI_3:52;
then A23:
u . (dl. dn) = u2 . (dl. dn)
by A13, A14, A21, SCM_1:19;
dn < aux + 1
by A22, NAT_1:13;
then
u1 . (dl. dn) = u2 . (dl. dn)
by A13;
hence
s . (dl. dn) = u . (dl. dn)
by A12, A22, A23;
:: thesis: verum end; suppose
nt = [0 ,1]
;
:: thesis: ex i being Element of NAT ex u being State of SCM st
( u = Computation s,(i + 1) & i + 1 = len (SCM-Compile (nt -tree tl,tr),aux) & IC (Computation s,i) = il. (n + i) & IC u = il. (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 A24:
(
Selfwork nt,
aux = <*(SubFrom (dl. aux),(dl. (aux + 1)))*> &
nt -Meaning_on (tl @ s),
(tr @ s) = (tl @ s) - (tr @ s) )
by Def8, Def10;
take i =
(i1 + 1) + (i2 + 1);
:: thesis: ex u being State of SCM st
( u = Computation s,(i + 1) & i + 1 = len (SCM-Compile (nt -tree tl,tr),aux) & IC (Computation s,i) = il. (n + i) & IC u = il. (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 =
Computation s,
(i + 1);
:: thesis: ( u = Computation s,(i + 1) & i + 1 = len (SCM-Compile (nt -tree tl,tr),aux) & IC (Computation s,i) = il. (n + i) & IC u = il. (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 = Computation s,
(i + 1)
;
:: thesis: ( i + 1 = len (SCM-Compile (nt -tree tl,tr),aux) & IC (Computation s,i) = il. (n + i) & IC u = il. (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) ) )A25:
len (Selfwork nt,aux) = 1
by A24, FINSEQ_1:57;
then
len (SCM-Compile (nt -tree tl,tr),aux) = ((i1 + 1) + (i2 + 1)) + 1
by A8, A18, FINSEQ_1:35;
then
i < len (SCM-Compile (nt -tree tl,tr),aux)
by NAT_1:13;
then A26:
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 A8, A18, A24, FINSEQ_1:59
;
thus
i + 1
= len (SCM-Compile (nt -tree tl,tr),aux)
by A8, A18, A25, FINSEQ_1:35;
:: thesis: ( IC (Computation s,i) = il. (n + i) & IC u = il. (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 (Computation s,i) = il. (n + i)
by A12, A13, AMI_1:51;
:: thesis: ( IC u = il. (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 u =
il. ((n + i) + 1)
by A13, A14, A26, SCM_1:20
.=
il. (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 A13, A14, A26, SCM_1:20
.=
(u1 . (dl. aux)) - (tr @ u1)
by A13, A17
.=
(nt -tree tl,tr) @ s
by A12, A15, A16, A24, 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 A27:
dn < aux
;
:: thesis: s . (dl. dn) = u . (dl. dn)then
dl. dn <> dl. aux
by AMI_3:52;
then A28:
u . (dl. dn) = u2 . (dl. dn)
by A13, A14, A26, SCM_1:20;
dn < aux + 1
by A27, NAT_1:13;
then
u1 . (dl. dn) = u2 . (dl. dn)
by A13;
hence
s . (dl. dn) = u . (dl. dn)
by A12, A27, A28;
:: thesis: verum end; suppose
nt = [0 ,2]
;
:: thesis: ex i being Element of NAT ex u being State of SCM st
( u = Computation s,(i + 1) & i + 1 = len (SCM-Compile (nt -tree tl,tr),aux) & IC (Computation s,i) = il. (n + i) & IC u = il. (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:
(
Selfwork nt,
aux = <*(MultBy (dl. aux),(dl. (aux + 1)))*> &
nt -Meaning_on (tl @ s),
(tr @ s) = (tl @ s) * (tr @ s) )
by Def8, Def10;
take i =
(i1 + 1) + (i2 + 1);
:: thesis: ex u being State of SCM st
( u = Computation s,(i + 1) & i + 1 = len (SCM-Compile (nt -tree tl,tr),aux) & IC (Computation s,i) = il. (n + i) & IC u = il. (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 =
Computation s,
(i + 1);
:: thesis: ( u = Computation s,(i + 1) & i + 1 = len (SCM-Compile (nt -tree tl,tr),aux) & IC (Computation s,i) = il. (n + i) & IC u = il. (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 = Computation s,
(i + 1)
;
:: thesis: ( i + 1 = len (SCM-Compile (nt -tree tl,tr),aux) & IC (Computation s,i) = il. (n + i) & IC u = il. (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:
len (Selfwork nt,aux) = 1
by A29, FINSEQ_1:57;
then
len (SCM-Compile (nt -tree tl,tr),aux) = ((i1 + 1) + (i2 + 1)) + 1
by A8, A18, 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
.=
MultBy (dl. aux),
(dl. (aux + 1))
by A8, A18, A29, FINSEQ_1:59
;
thus
i + 1
= len (SCM-Compile (nt -tree tl,tr),aux)
by A8, A18, A30, FINSEQ_1:35;
:: thesis: ( IC (Computation s,i) = il. (n + i) & IC u = il. (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 (Computation s,i) = il. (n + i)
by A12, A13, AMI_1:51;
:: thesis: ( IC u = il. (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 u =
il. ((n + i) + 1)
by A13, A14, A31, SCM_1:21
.=
il. (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 A13, A14, A31, SCM_1:21
.=
(u1 . (dl. aux)) * (tr @ u1)
by A13, A17
.=
(nt -tree tl,tr) @ s
by A12, A15, A16, A29, 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 A32:
dn < aux
;
:: thesis: s . (dl. dn) = u . (dl. dn)then
dl. dn <> dl. aux
by AMI_3:52;
then A33:
u . (dl. dn) = u2 . (dl. dn)
by A13, A14, A31, SCM_1:21;
dn < aux + 1
by A32, NAT_1:13;
then
u1 . (dl. dn) = u2 . (dl. dn)
by A13;
hence
s . (dl. dn) = u . (dl. dn)
by A12, A32, A33;
:: thesis: verum end; suppose
nt = [0 ,3]
;
:: thesis: ex i being Element of NAT ex u being State of SCM st
( u = Computation s,(i + 1) & i + 1 = len (SCM-Compile (nt -tree tl,tr),aux) & IC (Computation s,i) = il. (n + i) & IC u = il. (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 A34:
(
Selfwork nt,
aux = <*(Divide (dl. aux),(dl. (aux + 1)))*> &
nt -Meaning_on (tl @ s),
(tr @ s) = (tl @ s) div (tr @ s) )
by Def8, Def10;
take i =
(i1 + 1) + (i2 + 1);
:: thesis: ex u being State of SCM st
( u = Computation s,(i + 1) & i + 1 = len (SCM-Compile (nt -tree tl,tr),aux) & IC (Computation s,i) = il. (n + i) & IC u = il. (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 =
Computation s,
(i + 1);
:: thesis: ( u = Computation s,(i + 1) & i + 1 = len (SCM-Compile (nt -tree tl,tr),aux) & IC (Computation s,i) = il. (n + i) & IC u = il. (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 = Computation s,
(i + 1)
;
:: thesis: ( i + 1 = len (SCM-Compile (nt -tree tl,tr),aux) & IC (Computation s,i) = il. (n + i) & IC u = il. (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) ) )A35:
len (Selfwork nt,aux) = 1
by A34, FINSEQ_1:57;
then
len (SCM-Compile (nt -tree tl,tr),aux) = ((i1 + 1) + (i2 + 1)) + 1
by A8, A18, FINSEQ_1:35;
then
i < len (SCM-Compile (nt -tree tl,tr),aux)
by NAT_1:13;
then A36:
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 A8, A18, A34, FINSEQ_1:59
;
aux <> aux + 1
;
then A37:
dl. aux <> dl. (aux + 1)
by AMI_3:52;
thus
i + 1
= len (SCM-Compile (nt -tree tl,tr),aux)
by A8, A18, A35, FINSEQ_1:35;
:: thesis: ( IC (Computation s,i) = il. (n + i) & IC u = il. (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 (Computation s,i) = il. (n + i)
by A12, A13, AMI_1:51;
:: thesis: ( IC u = il. (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 u =
il. ((n + i) + 1)
by A13, A14, A36, A37, SCM_1:22
.=
il. (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 A13, A14, A36, A37, SCM_1:22
.=
(u1 . (dl. aux)) div (tr @ u1)
by A13, A17
.=
(nt -tree tl,tr) @ s
by A12, A15, A16, A34, 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 A38:
dn < aux
;
:: thesis: s . (dl. dn) = u . (dl. dn)then A39:
dl. dn <> dl. aux
by AMI_3:52;
A40:
dn < aux + 1
by A38, NAT_1:13;
then
dl. dn <> dl. (aux + 1)
by AMI_3:52;
then A41:
u . (dl. dn) = u2 . (dl. dn)
by A13, A14, A36, A37, A39, SCM_1:22;
u1 . (dl. dn) = u2 . (dl. dn)
by A13, A40;
hence
s . (dl. dn) = u . (dl. dn)
by A12, A38, A41;
:: thesis: verum end; suppose
nt = [0 ,4]
;
:: thesis: ex i being Element of NAT ex u being State of SCM st
( u = Computation s,(i + 1) & i + 1 = len (SCM-Compile (nt -tree tl,tr),aux) & IC (Computation s,i) = il. (n + i) & IC u = il. (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 A42:
(
Selfwork nt,
aux = <*(Divide (dl. aux),(dl. (aux + 1))),((dl. aux) := (dl. (aux + 1)))*> &
nt -Meaning_on (tl @ s),
(tr @ s) = (tl @ s) mod (tr @ s) )
by Def8, Def10;
set i =
(i1 + 1) + (i2 + 1);
set u =
Computation s,
(((i1 + 1) + (i2 + 1)) + 1);
take k =
((i1 + 1) + (i2 + 1)) + 1;
:: thesis: ex u being State of SCM st
( u = Computation s,(k + 1) & k + 1 = len (SCM-Compile (nt -tree tl,tr),aux) & IC (Computation s,k) = il. (n + k) & IC u = il. (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 =
Computation s,
(k + 1);
:: thesis: ( v = Computation s,(k + 1) & k + 1 = len (SCM-Compile (nt -tree tl,tr),aux) & IC (Computation s,k) = il. (n + k) & IC v = il. (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 = Computation s,
(k + 1)
;
:: thesis: ( k + 1 = len (SCM-Compile (nt -tree tl,tr),aux) & IC (Computation s,k) = il. (n + k) & IC v = il. (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) ) )A43:
len (Selfwork nt,aux) = 2
by A42, FINSEQ_1:61;
then A44:
len (SCM-Compile (nt -tree tl,tr),aux) = ((i1 + 1) + (i2 + 1)) + (1 + 1)
by A8, A18, FINSEQ_1:35;
hence
k + 1
= len (SCM-Compile (nt -tree tl,tr),aux)
;
:: thesis: ( IC (Computation s,k) = il. (n + k) & IC v = il. (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) ) )A45:
dom (Selfwork nt,aux) = Seg 2
by A43, FINSEQ_1:def 3;
A46:
( 1
in Seg 2 & 2
in Seg 2 )
by FINSEQ_1:4, TARSKI:def 2;
(
0 < 2 &
((i1 + 1) + (i2 + 1)) + 0 = (i1 + 1) + (i2 + 1) )
;
then
(i1 + 1) + (i2 + 1) < len (SCM-Compile (nt -tree tl,tr),aux)
by A44, XREAL_1:8;
then A47:
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 A8, A18, A42, A45, A46, FINSEQ_1:def 7
.=
Divide (dl. aux),
(dl. (aux + 1))
by FINSEQ_1:61
;
k < len (SCM-Compile (nt -tree tl,tr),aux)
by A44, XREAL_1:8;
then A48:
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 A8, A18, A42, A45, A46, FINSEQ_1:def 7
.=
(dl. aux) := (dl. (aux + 1))
by FINSEQ_1:61
;
aux <> aux + 1
;
then A49:
dl. aux <> dl. (aux + 1)
by AMI_3:52;
hence A50:
IC (Computation s,k) =
il. ((n + ((i1 + 1) + (i2 + 1))) + 1)
by A13, A14, A47, SCM_1:22
.=
il. (n + k)
;
:: thesis: ( IC v = il. (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 =
il. ((n + k) + 1)
by A48, SCM_1:18
.=
il. (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) =
(Computation s,(((i1 + 1) + (i2 + 1)) + 1)) . (dl. (aux + 1))
by A48, A50, SCM_1:18
.=
(u2 . (dl. aux)) mod (u2 . (dl. (aux + 1)))
by A13, A14, A47, A49, SCM_1:22
.=
(u1 . (dl. aux)) mod (tr @ u1)
by A13, A17
.=
(nt -tree tl,tr) @ s
by A12, A15, A16, A42, 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 A51:
dn < aux
;
:: thesis: s . (dl. dn) = v . (dl. dn)then A52:
dl. dn <> dl. aux
by AMI_3:52;
A53:
dn < aux + 1
by A51, NAT_1:13;
then
dl. dn <> dl. (aux + 1)
by AMI_3:52;
then A54:
(Computation s,(((i1 + 1) + (i2 + 1)) + 1)) . (dl. dn) = u2 . (dl. dn)
by A13, A14, A47, A49, A52, SCM_1:22;
u1 . (dl. dn) = u2 . (dl. dn)
by A13, A53;
then
s . (dl. dn) = (Computation s,(((i1 + 1) + (i2 + 1)) + 1)) . (dl. dn)
by A12, A51, A54;
hence
s . (dl. dn) = v . (dl. dn)
by A48, A50, A52, SCM_1:18;
:: thesis: verum end;
end;
thus
for term being bin-term holds S2[term]
from BINTREE1:sch 2(A1, A5); :: thesis: verum