let p be Instruction-Sequence of SCM+FSA; for a being read-write Int-Location
for I being MacroInstruction of SCM+FSA
for s being 0 -started State of SCM+FSA st while>0 (a,I) c= p & s . a <= 0 holds
( LifeSpan (p,s) = 3 & ( for k being Nat holds DataPart (Comput (p,s,k)) = DataPart s ) )
let a be read-write Int-Location; for I being MacroInstruction of SCM+FSA
for s being 0 -started State of SCM+FSA st while>0 (a,I) c= p & s . a <= 0 holds
( LifeSpan (p,s) = 3 & ( for k being Nat holds DataPart (Comput (p,s,k)) = DataPart s ) )
let I be MacroInstruction of SCM+FSA ; for s being 0 -started State of SCM+FSA st while>0 (a,I) c= p & s . a <= 0 holds
( LifeSpan (p,s) = 3 & ( for k being Nat holds DataPart (Comput (p,s,k)) = DataPart s ) )
let s be 0 -started State of SCM+FSA; ( while>0 (a,I) c= p & s . a <= 0 implies ( LifeSpan (p,s) = 3 & ( for k being Nat holds DataPart (Comput (p,s,k)) = DataPart s ) ) )
A1:
Start-At (0,SCM+FSA) c= s
by MEMSTR_0:29;
assume that
A2:
while>0 (a,I) c= p
and
A3:
s . a <= 0
; ( LifeSpan (p,s) = 3 & ( for k being Nat holds DataPart (Comput (p,s,k)) = DataPart s ) )
A4:
p +* (while>0 (a,I)) = p
by A2, FUNCT_4:98;
set i = a >0_goto 3;
set s1 = Initialize s;
set p1 = p +* (while>0 (a,I));
A5:
while>0 (a,I) c= p +* (while>0 (a,I))
by FUNCT_4:25;
A6:
IC in dom (Start-At (0,SCM+FSA))
by MEMSTR_0:15;
not a in dom (Start-At (0,SCM+FSA))
by SCMFSA_2:102;
then A7:
(Initialize s) . a = s . a
by FUNCT_4:11;
A8:
1 in dom (while>0 (a,I))
by SCMFSA_X:9;
A9: (p +* (while>0 (a,I))) . 1 =
(while>0 (a,I)) . 1
by A8, FUNCT_4:13
.=
goto 2
by SCMFSA_X:10
;
A10: IC (Initialize s) =
IC (Start-At (0,SCM+FSA))
by A6, FUNCT_4:13
.=
0
by FUNCOP_1:72
;
A11:
(p +* (while>0 (a,I))) /. (IC (Initialize s)) = (p +* (while>0 (a,I))) . (IC (Initialize s))
by PBOOLE:143;
0 in dom (while>0 (a,I))
by AFINSQ_1:65;
then (p +* (while>0 (a,I))) . 0 =
(while>0 (a,I)) . 0
by FUNCT_4:13
.=
a >0_goto 3
by SCMFSA_X:10
;
then A12:
CurInstr ((p +* (while>0 (a,I))),(Initialize s)) = a >0_goto 3
by A10, A11;
A13: Comput ((p +* (while>0 (a,I))),(Initialize s),(0 + 1)) =
Following ((p +* (while>0 (a,I))),(Comput ((p +* (while>0 (a,I))),(Initialize s),0)))
by EXTPRO_1:3
.=
Exec ((a >0_goto 3),(Initialize s))
by A12
;
set loc5 = (card I) + 4;
set s5 = Comput ((p +* (while>0 (a,I))),(Initialize s),3);
set p5 = p +* (while>0 (a,I));
set s4 = Comput ((p +* (while>0 (a,I))),(Initialize s),2);
set p4 = p +* (while>0 (a,I));
set s2 = Comput ((p +* (while>0 (a,I))),(Initialize s),1);
A14:
2 in dom (while>0 (a,I))
by SCMFSA_X:7;
A15: (p +* (while>0 (a,I))) . 2 =
(while>0 (a,I)) . 2
by A14, FUNCT_4:13
.=
goto ((card I) + 4)
by SCMFSA_X:17
;
A16:
(card I) + 4 in dom (while>0 (a,I))
by SCMFSA_X:8;
A17: (p +* (while>0 (a,I))) . ((card I) + 4) =
(while>0 (a,I)) . ((card I) + 4)
by A16, A5, GRFUNC_1:2
.=
halt SCM+FSA
by SCMFSA_X:16
;
A18:
( ( for c being Int-Location holds (Exec ((goto ((card I) + 4)),(Comput ((p +* (while>0 (a,I))),(Initialize s),2)))) . c = (Comput ((p +* (while>0 (a,I))),(Initialize s),2)) . c ) & ( for f being FinSeq-Location holds (Exec ((goto ((card I) + 4)),(Comput ((p +* (while>0 (a,I))),(Initialize s),2)))) . f = (Comput ((p +* (while>0 (a,I))),(Initialize s),2)) . f ) )
by SCMFSA_2:69;
A19:
( ( for c being Int-Location holds (Exec ((goto 2),(Comput ((p +* (while>0 (a,I))),(Initialize s),1)))) . c = (Comput ((p +* (while>0 (a,I))),(Initialize s),1)) . c ) & ( for f being FinSeq-Location holds (Exec ((goto 2),(Comput ((p +* (while>0 (a,I))),(Initialize s),1)))) . f = (Comput ((p +* (while>0 (a,I))),(Initialize s),1)) . f ) )
by SCMFSA_2:69;
A20:
(p +* (while>0 (a,I))) /. (IC (Comput ((p +* (while>0 (a,I))),(Initialize s),1))) = (p +* (while>0 (a,I))) . (IC (Comput ((p +* (while>0 (a,I))),(Initialize s),1)))
by PBOOLE:143;
IC (Comput ((p +* (while>0 (a,I))),(Initialize s),1)) = 0 + 1
by A3, A10, A13, A7, SCMFSA_2:71;
then A21:
CurInstr ((p +* (while>0 (a,I))),(Comput ((p +* (while>0 (a,I))),(Initialize s),1))) = goto 2
by A9, A20;
A22: Comput ((p +* (while>0 (a,I))),(Initialize s),(1 + 1)) =
Following ((p +* (while>0 (a,I))),(Comput ((p +* (while>0 (a,I))),(Initialize s),1)))
by EXTPRO_1:3
.=
Exec ((goto 2),(Comput ((p +* (while>0 (a,I))),(Initialize s),1)))
by A21
;
A23:
(p +* (while>0 (a,I))) /. (IC (Comput ((p +* (while>0 (a,I))),(Initialize s),2))) = (p +* (while>0 (a,I))) . (IC (Comput ((p +* (while>0 (a,I))),(Initialize s),2)))
by PBOOLE:143;
IC (Comput ((p +* (while>0 (a,I))),(Initialize s),2)) = 2
by A22, SCMFSA_2:69;
then A24:
CurInstr ((p +* (while>0 (a,I))),(Comput ((p +* (while>0 (a,I))),(Initialize s),2))) = goto ((card I) + 4)
by A15, A23;
A25: Comput ((p +* (while>0 (a,I))),(Initialize s),(2 + 1)) =
Following ((p +* (while>0 (a,I))),(Comput ((p +* (while>0 (a,I))),(Initialize s),2)))
by EXTPRO_1:3
.=
Exec ((goto ((card I) + 4)),(Comput ((p +* (while>0 (a,I))),(Initialize s),2)))
by A24
;
A26:
(p +* (while>0 (a,I))) /. (IC (Comput ((p +* (while>0 (a,I))),(Initialize s),3))) = (p +* (while>0 (a,I))) . (IC (Comput ((p +* (while>0 (a,I))),(Initialize s),3)))
by PBOOLE:143;
IC (Comput ((p +* (while>0 (a,I))),(Initialize s),3)) = (card I) + 4
by A25, SCMFSA_2:69;
then A27:
CurInstr ((p +* (while>0 (a,I))),(Comput ((p +* (while>0 (a,I))),(Initialize s),3))) = halt SCM+FSA
by A17, A26;
then A28:
p +* (while>0 (a,I)) halts_on Initialize s
by EXTPRO_1:29;
A29:
s = Initialize s
by A1, FUNCT_4:98;
hence A31:
LifeSpan (p,s) = 3
by A29, A27, A28, A4, EXTPRO_1:def 15; for k being Nat holds DataPart (Comput (p,s,k)) = DataPart s
A32:
( ( for c being Int-Location holds (Exec ((a >0_goto 3),(Initialize s))) . c = (Initialize s) . c ) & ( for f being FinSeq-Location holds (Exec ((a >0_goto 3),(Initialize s))) . f = (Initialize s) . f ) )
by SCMFSA_2:71;
then A33:
DataPart (Comput (p,s,1)) = DataPart s
by A29, A13, A4, SCMFSA_M:2;
then
DataPart (Comput (p,s,2)) = DataPart s
by A29, A22, A19, A4, SCMFSA_M:2;
then A34:
DataPart (Comput (p,s,3)) = DataPart s
by A29, A25, A18, A4, SCMFSA_M:2;
let k be Nat; DataPart (Comput (p,s,k)) = DataPart s
( k <= 2 or 2 < k )
;
then A35:
( not not k = 0 & ... & not k = 2 or 2 + 1 <= k )
by NAT_1:13;
per cases
( k = 0 or k = 1 or k = 2 or 3 <= k )
by A35;
suppose
3
<= k
;
DataPart (Comput (p,s,k)) = DataPart sthen
CurInstr (
p,
(Comput (p,s,k)))
= halt SCM+FSA
by A29, A28, A31, A4, EXTPRO_1:36;
hence
DataPart (Comput (p,s,k)) = DataPart s
by A31, A34, EXTPRO_1:24;
verum end;