let P be Instruction-Sequence of SCM+FSA; for s being State of SCM+FSA
for I being Program 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 Program 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 Program 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 s3 = Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),2);
set s4 = Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),3);
set s5 = Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),4);
set i = a >0_goto 4;
A2:
1 in dom (while>0 (a,I))
by SCMFSA_9:10;
A3: (P +* (while>0 (a,I))) . 1 =
(while>0 (a,I)) . 1
by A2, A1, GRFUNC_1:2
.=
goto 2
by SCMFSA_9:11
;
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 SCMFSA_9:10;
then A5: (P +* (while>0 (a,I))) . 0 =
(while>0 (a,I)) . 0
by A1, GRFUNC_1:2
.=
a >0_goto 4
by SCMFSA_9:11
;
then A6:
CurInstr ((P +* (while>0 (a,I))),(Initialize (Initialized s))) = a >0_goto 4
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)))
by EXTPRO_1:2
.=
Exec ((a >0_goto 4),(Initialize (Initialized s)))
by A4, A5, PBOOLE:143
;
set loc5 = (card I) + 5;
A8:
2 in dom (while>0 (a,I))
by SCMFSA_9:32;
A9: (P +* (while>0 (a,I))) . 2 =
(while>0 (a,I)) . 2
by A8, A1, GRFUNC_1:2
.=
goto 3
by SCMFSA_9:36
;
A11:
(card I) + 5 in dom (while>0 (a,I))
by SCMFSA_9:33;
not a in dom (Start-At (0,SCM+FSA))
by SCMFSA_2:102;
then A12:
(Initialize (Initialized s)) . a = (Initialized s) . a
by FUNCT_4:11;
A13:
3 in dom (while>0 (a,I))
by SCMFSA_9:32;
assume
s . a <= 0
; DataPart (IExec ((while>0 (a,I)),P,s)) = DataPart (Initialized s)
then
(Initialized s) . a <= 0
by SCMFSA6C:3;
then A14: IC (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),1)) =
succ 0
by A4, A7, A12, SCMFSA_2:71
.=
0 + 1
;
A15: 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 A14, A3, PBOOLE:143
;
then A16:
IC (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),2)) = 2
by SCMFSA_2:69;
A17:
(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;
A18: 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 3),(Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),2)))
by A15, A9, A17, SCMFSA_2:69
;
A19: (P +* (while>0 (a,I))) . 3 =
(while>0 (a,I)) . 3
by A13, A1, GRFUNC_1:2
.=
goto ((card I) + 5)
by SCMFSA_9:35
;
A20:
(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;
A21: Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),(3 + 1)) =
Following ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),3)))
by EXTPRO_1:3
.=
Exec ((goto ((card I) + 5)),(Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),3)))
by A18, A19, A20, SCMFSA_2:69
;
A22:
(P +* (while>0 (a,I))) /. (IC (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),4))) = (P +* (while>0 (a,I))) . (IC (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),4)))
by PBOOLE:143;
(P +* (while>0 (a,I))) . ((card I) + 5) =
(while>0 (a,I)) . ((card I) + 5)
by A11, A1, GRFUNC_1:2
.=
halt SCM+FSA
by SCMFSA_9:34
;
then A23:
CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),4))) = halt SCM+FSA
by A21, A22, SCMFSA_2:69;
then A24:
P +* (while>0 (a,I)) halts_on Initialize (Initialized s)
by EXTPRO_1:29;
A25:
(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;
A26:
CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),3))) = goto ((card I) + 5)
by A18, A19, A25, SCMFSA_2:69;
now let k be
Element of
NAT ;
( CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),k))) = halt SCM+FSA implies 3 + 1 <= k )assume A27:
CurInstr (
(P +* (while>0 (a,I))),
(Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),k)))
= halt SCM+FSA
;
3 + 1 <= kthen A28:
k <> 2
by A16, A9, PBOOLE:143;
A29:
k <> 0
by A27, A6, EXTPRO_1:2;
A30:
k <> 1
by A14, A3, A27, PBOOLE:143;
3
< k
by A29, A28, A30, A26, A27, NAT_1:27;
hence
3
+ 1
<= k
by INT_1:7;
verum end;
then A31:
LifeSpan ((P +* (while>0 (a,I))),(Initialize (Initialized s))) = 4
by A23, A24, EXTPRO_1:def 15;
A32: Initialized (Initialized s) =
Initialize (Initialized (Initialized s))
by MEMSTR_0:44
.=
Initialize (Initialized s)
;
A33:
Initialize (Initialized s) = Initialized s
by A32;
A34:
now let a be
Int-Location ;
(Initialized s) . a = (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),4)) . athus (Initialized s) . a =
(Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),1)) . a
by A7, A33, SCMFSA_2:71
.=
(Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),2)) . a
by A15, SCMFSA_2:69
.=
(Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),3)) . a
by A18, SCMFSA_2:69
.=
(Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),4)) . a
by A21, SCMFSA_2:69
;
verum end;
A35:
now let f be
FinSeq-Location ;
(Initialized s) . f = (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),4)) . fthus (Initialized s) . f =
(Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),1)) . f
by A7, A33, SCMFSA_2:71
.=
(Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),2)) . f
by A15, SCMFSA_2:69
.=
(Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),3)) . f
by A18, SCMFSA_2:69
.=
(Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),4)) . f
by A21, 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 A32
.=
DataPart (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),4))
by A24, A31, EXTPRO_1:23
.=
DataPart (Initialized s)
by A34, A35, SCMFSA6A:7
; verum