let P be Instruction-Sequence of SCM+FSA; for s being State of SCM+FSA
for I being MacroInstruction of SCM+FSA
for a being read-write Int-Location st s . a <= 0 holds
DataPart (IExec ((while>0 (a,I)),P,s)) = DataPart (Initialized s)
let s be State of SCM+FSA; for I being MacroInstruction of SCM+FSA
for a being read-write Int-Location st s . a <= 0 holds
DataPart (IExec ((while>0 (a,I)),P,s)) = DataPart (Initialized s)
let I be MacroInstruction of SCM+FSA ; for a being read-write Int-Location st s . a <= 0 holds
DataPart (IExec ((while>0 (a,I)),P,s)) = DataPart (Initialized s)
let a be read-write Int-Location; ( s . a <= 0 implies DataPart (IExec ((while>0 (a,I)),P,s)) = DataPart (Initialized s) )
set D = Data-Locations ;
set Is = Initialized s;
set s1 = Initialize (Initialized s);
set P1 = P +* (while>0 (a,I));
A1:
while>0 (a,I) c= P +* (while>0 (a,I))
by FUNCT_4:25;
set s2 = Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),1);
set s4 = Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),2);
set s5 = Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),3);
set i = a >0_goto 3;
A2:
1 in dom (while>0 (a,I))
by SCMFSA_X:9;
A3: (P +* (while>0 (a,I))) . 1 =
(while>0 (a,I)) . 1
by A2, A1, GRFUNC_1:2
.=
goto 2
by SCMFSA_X:10
;
IC in dom (Start-At (0,SCM+FSA))
by MEMSTR_0:15;
then A4: IC (Initialize (Initialized s)) =
IC (Start-At (0,SCM+FSA))
by FUNCT_4:13
.=
0
by FUNCOP_1:72
;
0 in dom (while>0 (a,I))
by AFINSQ_1:65;
then A5: (P +* (while>0 (a,I))) . 0 =
(while>0 (a,I)) . 0
by A1, GRFUNC_1:2
.=
a >0_goto 3
by SCMFSA_X:10
;
then A6:
CurInstr ((P +* (while>0 (a,I))),(Initialize (Initialized s))) = a >0_goto 3
by A4, PBOOLE:143;
A7: Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),(0 + 1)) =
Following ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),0)))
by EXTPRO_1:3
.=
Following ((P +* (while>0 (a,I))),(Initialize (Initialized s)))
.=
Exec ((a >0_goto 3),(Initialize (Initialized s)))
by A4, A5, PBOOLE:143
;
set loc5 = (card I) + 4;
A8:
2 in dom (while>0 (a,I))
by SCMFSA_X:7;
A9:
(card I) + 4 in dom (while>0 (a,I))
by SCMFSA_X:8;
not a in dom (Start-At (0,SCM+FSA))
by SCMFSA_2:102;
then A10:
(Initialize (Initialized s)) . a = (Initialized s) . a
by FUNCT_4:11;
assume
s . a <= 0
; DataPart (IExec ((while>0 (a,I)),P,s)) = DataPart (Initialized s)
then
(Initialized s) . a <= 0
by SCMFSA_M:37;
then A11:
IC (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),1)) = 0 + 1
by A4, A7, A10, SCMFSA_2:71;
A12: Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),(1 + 1)) =
Following ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),1)))
by EXTPRO_1:3
.=
Exec ((goto 2),(Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),1)))
by A11, A3, PBOOLE:143
;
A13: (P +* (while>0 (a,I))) . 2 =
(while>0 (a,I)) . 2
by A8, A1, GRFUNC_1:2
.=
goto ((card I) + 4)
by SCMFSA_X:17
;
A14:
(P +* (while>0 (a,I))) /. (IC (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),2))) = (P +* (while>0 (a,I))) . (IC (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),2)))
by PBOOLE:143;
A15: Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),(2 + 1)) =
Following ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),2)))
by EXTPRO_1:3
.=
Exec ((goto ((card I) + 4)),(Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),2)))
by A12, A13, A14, SCMFSA_2:69
;
A16:
(P +* (while>0 (a,I))) /. (IC (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),3))) = (P +* (while>0 (a,I))) . (IC (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),3)))
by PBOOLE:143;
(P +* (while>0 (a,I))) . ((card I) + 4) =
(while>0 (a,I)) . ((card I) + 4)
by A9, A1, GRFUNC_1:2
.=
halt SCM+FSA
by SCMFSA_X:16
;
then A17:
CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),3))) = halt SCM+FSA
by A15, A16, SCMFSA_2:69;
then A18:
P +* (while>0 (a,I)) halts_on Initialize (Initialized s)
by EXTPRO_1:29;
A19:
(P +* (while>0 (a,I))) /. (IC (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),2))) = (P +* (while>0 (a,I))) . (IC (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),2)))
by PBOOLE:143;
A20:
CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),2))) = goto ((card I) + 4)
by A12, A13, A19, SCMFSA_2:69;
now for k being Nat st CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),k))) = halt SCM+FSA holds
2 + 1 <= klet k be
Nat;
( CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),k))) = halt SCM+FSA implies 2 + 1 <= k )assume A21:
CurInstr (
(P +* (while>0 (a,I))),
(Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),k)))
= halt SCM+FSA
;
2 + 1 <= kA22:
k <> 0
by A21, A6;
A23:
k <> 1
by A11, A3, A21, PBOOLE:143;
k <> 2
by A20, A21;
then
k <> 0 & ... &
k <> 2
by A22, A23;
then
2
< k
;
hence
2
+ 1
<= k
by INT_1:7;
verum end;
then A24:
LifeSpan ((P +* (while>0 (a,I))),(Initialize (Initialized s))) = 3
by A17, A18, EXTPRO_1:def 15;
A25: Initialized (Initialized s) =
Initialize (Initialized (Initialized s))
by MEMSTR_0:44
.=
Initialize (Initialized s)
;
A26:
Initialize (Initialized s) = Initialized s
by A25;
A27:
now for a being Int-Location holds (Initialized s) . a = (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),3)) . alet a be
Int-Location;
(Initialized s) . a = (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),3)) . athus (Initialized s) . a =
(Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),1)) . a
by A7, A26, SCMFSA_2:71
.=
(Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),2)) . a
by A12, SCMFSA_2:69
.=
(Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),3)) . a
by A15, SCMFSA_2:69
;
verum end;
A28:
now for f being FinSeq-Location holds (Initialized s) . f = (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),3)) . flet f be
FinSeq-Location ;
(Initialized s) . f = (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),3)) . fthus (Initialized s) . f =
(Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),1)) . f
by A7, A26, SCMFSA_2:71
.=
(Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),2)) . f
by A12, SCMFSA_2:69
.=
(Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),3)) . f
by A15, SCMFSA_2:69
;
verum end;
thus DataPart (IExec ((while>0 (a,I)),P,s)) =
DataPart (IExec ((while>0 (a,I)),P,(Initialized s)))
by SCMFSA8C:3
.=
DataPart (Result ((P +* (while>0 (a,I))),(Initialized (Initialized s))))
by SCMFSA6B:def 1
.=
DataPart (Result ((P +* (while>0 (a,I))),(Initialize (Initialized s))))
by A25
.=
DataPart (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),3))
by A18, A24, EXTPRO_1:23
.=
DataPart (Initialized s)
by A27, A28, SCMFSA_M:2
; verum