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 ()

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 ()

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 ()

let a be read-write Int-Location; :: thesis: ( s . a <= 0 implies DataPart (IExec ((while>0 (a,I)),P,s)) = DataPart () )
set D = Data-Locations ;
set Is = Initialized s;
set s1 = Initialize ();
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))),(),1);
set s4 = Comput ((P +* (while>0 (a,I))),(),2);
set s5 = Comput ((P +* (while>0 (a,I))),(),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
.= goto 2 by SCMFSA_X:10 ;
IC in dom () by MEMSTR_0:15;
then A4: IC () = IC () 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
.= a >0_goto 3 by SCMFSA_X:10 ;
then A6: CurInstr ((P +* (while>0 (a,I))),()) = a >0_goto 3 by ;
A7: Comput ((P +* (while>0 (a,I))),(),(0 + 1)) = Following ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(),0))) by EXTPRO_1:3
.= Following ((P +* (while>0 (a,I))),())
.= Exec ((a >0_goto 3),()) by ;
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 () by SCMFSA_2:102;
then A10: (Initialize ()) . a = () . a by FUNCT_4:11;
assume s . a <= 0 ; :: thesis: DataPart (IExec ((while>0 (a,I)),P,s)) = DataPart ()
then (Initialized s) . a <= 0 by SCMFSA_M:37;
then A11: IC (Comput ((P +* (while>0 (a,I))),(),1)) = 0 + 1 by ;
A12: Comput ((P +* (while>0 (a,I))),(),(1 + 1)) = Following ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(),1))) by EXTPRO_1:3
.= Exec ((goto 2),(Comput ((P +* (while>0 (a,I))),(),1))) by ;
A13: (P +* (while>0 (a,I))) . 2 = (while>0 (a,I)) . 2 by
.= goto ((card I) + 4) by SCMFSA_X:17 ;
A14: (P +* (while>0 (a,I))) /. (IC (Comput ((P +* (while>0 (a,I))),(),2))) = (P +* (while>0 (a,I))) . (IC (Comput ((P +* (while>0 (a,I))),(),2))) by PBOOLE:143;
A15: Comput ((P +* (while>0 (a,I))),(),(2 + 1)) = Following ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(),2))) by EXTPRO_1:3
.= Exec ((goto ((card I) + 4)),(Comput ((P +* (while>0 (a,I))),(),2))) by ;
A16: (P +* (while>0 (a,I))) /. (IC (Comput ((P +* (while>0 (a,I))),(),3))) = (P +* (while>0 (a,I))) . (IC (Comput ((P +* (while>0 (a,I))),(),3))) by PBOOLE:143;
(P +* (while>0 (a,I))) . ((card I) + 4) = (while>0 (a,I)) . ((card I) + 4) by
.= halt SCM+FSA by SCMFSA_X:16 ;
then A17: CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(),3))) = halt SCM+FSA by ;
then A18: P +* (while>0 (a,I)) halts_on Initialize () by EXTPRO_1:29;
A19: (P +* (while>0 (a,I))) /. (IC (Comput ((P +* (while>0 (a,I))),(),2))) = (P +* (while>0 (a,I))) . (IC (Comput ((P +* (while>0 (a,I))),(),2))) by PBOOLE:143;
A20: CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(),2))) = goto ((card I) + 4) by ;
now :: thesis: for k being Nat st CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(),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))),(),k))) = halt SCM+FSA implies 2 + 1 <= k )
assume A21: CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(),k))) = halt SCM+FSA ; :: thesis: 2 + 1 <= k
A22: k <> 0 by ;
A23: k <> 1 by ;
k <> 2 by ;
then k <> 0 & ... & k <> 2 by ;
then 2 < k ;
hence 2 + 1 <= k by INT_1:7; :: thesis: verum
end;
then A24: LifeSpan ((P +* (while>0 (a,I))),()) = 3 by ;
A25: Initialized () = Initialize () by MEMSTR_0:44
.= Initialize () ;
A26: Initialize () = Initialized s by A25;
A27: now :: thesis: for a being Int-Location holds () . a = (Comput ((P +* (while>0 (a,I))),(),3)) . a
let a be Int-Location; :: thesis: () . a = (Comput ((P +* (while>0 (a,I))),(),3)) . a
thus () . a = (Comput ((P +* (while>0 (a,I))),(),1)) . a by
.= (Comput ((P +* (while>0 (a,I))),(),2)) . a by
.= (Comput ((P +* (while>0 (a,I))),(),3)) . a by ; :: thesis: verum
end;
A28: now :: thesis: for f being FinSeq-Location holds () . f = (Comput ((P +* (while>0 (a,I))),(),3)) . f
let f be FinSeq-Location ; :: thesis: () . f = (Comput ((P +* (while>0 (a,I))),(),3)) . f
thus () . f = (Comput ((P +* (while>0 (a,I))),(),1)) . f by
.= (Comput ((P +* (while>0 (a,I))),(),2)) . f by
.= (Comput ((P +* (while>0 (a,I))),(),3)) . f by ; :: thesis: verum
end;
thus DataPart (IExec ((while>0 (a,I)),P,s)) = DataPart (IExec ((while>0 (a,I)),P,())) by SCMFSA8C:3
.= DataPart (Result ((P +* (while>0 (a,I))),())) by SCMFSA6B:def 1
.= DataPart (Result ((P +* (while>0 (a,I))),())) by A25
.= DataPart (Comput ((P +* (while>0 (a,I))),(),3)) by
.= DataPart () by ; :: thesis: verum