let P be Instruction-Sequence of SCM+FSA; :: thesis: 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; :: thesis: 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 ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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 :: thesis: 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 <= k

let k be Nat; :: thesis: ( 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 ; :: thesis: 2 + 1 <= k
A22: 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; :: thesis: 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 :: thesis: for a being Int-Location holds (Initialized s) . a = (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),3)) . a

let a be Int-Location; :: thesis: (Initialized s) . a = (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),3)) . a
thus (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 ; :: thesis: verum

end;

A28: now :: thesis: for f being FinSeq-Location holds (Initialized s) . f = (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),3)) . f

let f be FinSeq-Location ; :: thesis: (Initialized s) . f = (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),3)) . f
thus (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 ; :: thesis: 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 ; :: thesis: verum