let P be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: 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)
set A = NAT ;
let s be State of SCM+FSA; :: thesis: 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; :: 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 SCM+FSA;
set Is = Initialized s;
set s1 = (Initialized s) +* (Start-At (0,SCM+FSA));
set P1 = P +* (while>0 (a,I));
A1: while>0 (a,I) c= P +* (while>0 (a,I)) by FUNCT_4:26;
set s2 = Comput ((P +* (while>0 (a,I))),((Initialized s) +* (Start-At (0,SCM+FSA))),1);
set s3 = Comput ((P +* (while>0 (a,I))),((Initialized s) +* (Start-At (0,SCM+FSA))),2);
set s4 = Comput ((P +* (while>0 (a,I))),((Initialized s) +* (Start-At (0,SCM+FSA))),3);
set s5 = Comput ((P +* (while>0 (a,I))),((Initialized s) +* (Start-At (0,SCM+FSA))),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:8
.= goto 2 by SCMFSA_9:11 ;
IC in dom (Start-At (0,SCM+FSA)) by COMPOS_1:52;
then A4: IC ((Initialized s) +* (Start-At (0,SCM+FSA))) = IC (Start-At (0,SCM+FSA)) by FUNCT_4:14
.= 0 by COMPOS_1:64 ;
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:8
.= a >0_goto 4 by SCMFSA_9:11 ;
then A6: CurInstr ((P +* (while>0 (a,I))),((Initialized s) +* (Start-At (0,SCM+FSA)))) = a >0_goto 4 by A4, PBOOLE:158;
A7: Comput ((P +* (while>0 (a,I))),((Initialized s) +* (Start-At (0,SCM+FSA))),(0 + 1)) = Following ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),((Initialized s) +* (Start-At (0,SCM+FSA))),0))) by EXTPRO_1:4
.= Following ((P +* (while>0 (a,I))),((Initialized s) +* (Start-At (0,SCM+FSA)))) by EXTPRO_1:3
.= Exec ((a >0_goto 4),((Initialized s) +* (Start-At (0,SCM+FSA)))) by A4, A5, PBOOLE:158 ;
set loc5 = (card I) + 5;
A8: 2 in dom (while>0 (a,I)) by SCMFSA_9:37;
A9: (P +* (while>0 (a,I))) . 2 = (while>0 (a,I)) . 2 by A8, A1, GRFUNC_1:8
.= goto 3 by SCMFSA_9:41 ;
A10: IC (Initialized s) = 0 by SCMFSA6C:3;
A11: (card I) + 5 in dom (while>0 (a,I)) by SCMFSA_9:38;
Start-At (0,SCM+FSA) c= Initialize (while>0 (a,I)) by FUNCT_4:26;
then zz: dom (Start-At (0,SCM+FSA)) c= dom (Initialize (while>0 (a,I))) by RELAT_1:25;
not a in dom (Initialize (while>0 (a,I))) by SCMFSA6B:12;
then not a in dom (Start-At (0,SCM+FSA)) by zz;
then A12: ((Initialized s) +* (Start-At (0,SCM+FSA))) . a = (Initialized s) . a by FUNCT_4:12;
A13: 3 in dom (while>0 (a,I)) by SCMFSA_9:37;
assume s . a <= 0 ; :: thesis: 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))),((Initialized s) +* (Start-At (0,SCM+FSA))),1)) = succ 0 by A4, A7, A12, SCMFSA_2:97
.= 0 + 1 ;
A15: Comput ((P +* (while>0 (a,I))),((Initialized s) +* (Start-At (0,SCM+FSA))),(1 + 1)) = Following ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),((Initialized s) +* (Start-At (0,SCM+FSA))),1))) by EXTPRO_1:4
.= Exec ((goto 2),(Comput ((P +* (while>0 (a,I))),((Initialized s) +* (Start-At (0,SCM+FSA))),1))) by A14, A3, PBOOLE:158 ;
then A16: IC (Comput ((P +* (while>0 (a,I))),((Initialized s) +* (Start-At (0,SCM+FSA))),2)) = 2 by SCMFSA_2:95;
A17: (P +* (while>0 (a,I))) /. (IC (Comput ((P +* (while>0 (a,I))),((Initialized s) +* (Start-At (0,SCM+FSA))),2))) = (P +* (while>0 (a,I))) . (IC (Comput ((P +* (while>0 (a,I))),((Initialized s) +* (Start-At (0,SCM+FSA))),2))) by PBOOLE:158;
A18: Comput ((P +* (while>0 (a,I))),((Initialized s) +* (Start-At (0,SCM+FSA))),(2 + 1)) = Following ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),((Initialized s) +* (Start-At (0,SCM+FSA))),2))) by EXTPRO_1:4
.= Exec ((goto 3),(Comput ((P +* (while>0 (a,I))),((Initialized s) +* (Start-At (0,SCM+FSA))),2))) by A15, A9, A17, SCMFSA_2:95 ;
A19: (P +* (while>0 (a,I))) . 3 = (while>0 (a,I)) . 3 by A13, A1, GRFUNC_1:8
.= goto ((card I) + 5) by SCMFSA_9:40 ;
A20: (P +* (while>0 (a,I))) /. (IC (Comput ((P +* (while>0 (a,I))),((Initialized s) +* (Start-At (0,SCM+FSA))),3))) = (P +* (while>0 (a,I))) . (IC (Comput ((P +* (while>0 (a,I))),((Initialized s) +* (Start-At (0,SCM+FSA))),3))) by PBOOLE:158;
A21: Comput ((P +* (while>0 (a,I))),((Initialized s) +* (Start-At (0,SCM+FSA))),(3 + 1)) = Following ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),((Initialized s) +* (Start-At (0,SCM+FSA))),3))) by EXTPRO_1:4
.= Exec ((goto ((card I) + 5)),(Comput ((P +* (while>0 (a,I))),((Initialized s) +* (Start-At (0,SCM+FSA))),3))) by A18, A19, A20, SCMFSA_2:95 ;
A22: (P +* (while>0 (a,I))) /. (IC (Comput ((P +* (while>0 (a,I))),((Initialized s) +* (Start-At (0,SCM+FSA))),4))) = (P +* (while>0 (a,I))) . (IC (Comput ((P +* (while>0 (a,I))),((Initialized s) +* (Start-At (0,SCM+FSA))),4))) by PBOOLE:158;
(P +* (while>0 (a,I))) . ((card I) + 5) = (while>0 (a,I)) . ((card I) + 5) by A11, A1, GRFUNC_1:8
.= halt SCM+FSA by SCMFSA_9:39 ;
then A23: CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),((Initialized s) +* (Start-At (0,SCM+FSA))),4))) = halt SCM+FSA by A21, A22, SCMFSA_2:95;
then A24: P +* (while>0 (a,I)) halts_on (Initialized s) +* (Start-At (0,SCM+FSA)) by EXTPRO_1:30;
A25: (P +* (while>0 (a,I))) /. (IC (Comput ((P +* (while>0 (a,I))),((Initialized s) +* (Start-At (0,SCM+FSA))),3))) = (P +* (while>0 (a,I))) . (IC (Comput ((P +* (while>0 (a,I))),((Initialized s) +* (Start-At (0,SCM+FSA))),3))) by PBOOLE:158;
A26: CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),((Initialized s) +* (Start-At (0,SCM+FSA))),3))) = goto ((card I) + 5) by A18, A19, A25, SCMFSA_2:95;

now

let k be Element of NAT ; :: thesis: ( CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),((Initialized s) +* (Start-At (0,SCM+FSA))),k))) = halt SCM+FSA implies 3 + 1 <= k )
assume A27: CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),((Initialized s) +* (Start-At (0,SCM+FSA))),k))) = halt SCM+FSA ; :: thesis: 3 + 1 <= k
then A28: k <> 2 by A16, A9, PBOOLE:158;
A29: k <> 0 by A27, A6, EXTPRO_1:3;
A30: k <> 1 by A14, A3, A27, PBOOLE:158;
3 < k by A29, A28, A30, A26, A27, NAT_1:28;
hence 3 + 1 <= k by INT_1:20; :: thesis: verum

end;

then A31: LifeSpan ((P +* (while>0 (a,I))),((Initialized s) +* (Start-At (0,SCM+FSA)))) = 4 by A23, A24, EXTPRO_1:def 14;
A32: (Initialized s) +* (Initialize ((intloc 0) .--> 1)) = Initialize (Initialized (Initialized s)) by SCMFSA8A:13
.= (Initialized s) +* (Start-At (0,SCM+FSA)) ;
(Initialized s) . (intloc 0) = 1 by SCMFSA6C:3;
then A33: (Initialized s) +* (Start-At (0,SCM+FSA)) = Initialized s by A32, A10, Th6;

A34: now

let a be Int-Location ; :: thesis: (Initialized s) . a = (Comput ((P +* (while>0 (a,I))),((Initialized s) +* (Start-At (0,SCM+FSA))),4)) . a
thus (Initialized s) . a = (Comput ((P +* (while>0 (a,I))),((Initialized s) +* (Start-At (0,SCM+FSA))),1)) . a by A7, A33, SCMFSA_2:97
.= (Comput ((P +* (while>0 (a,I))),((Initialized s) +* (Start-At (0,SCM+FSA))),2)) . a by A15, SCMFSA_2:95
.= (Comput ((P +* (while>0 (a,I))),((Initialized s) +* (Start-At (0,SCM+FSA))),3)) . a by A18, SCMFSA_2:95
.= (Comput ((P +* (while>0 (a,I))),((Initialized s) +* (Start-At (0,SCM+FSA))),4)) . a by A21, SCMFSA_2:95 ; :: thesis: verum

end;

A35: now

let f be FinSeq-Location ; :: thesis: (Initialized s) . f = (Comput ((P +* (while>0 (a,I))),((Initialized s) +* (Start-At (0,SCM+FSA))),4)) . f
thus (Initialized s) . f = (Comput ((P +* (while>0 (a,I))),((Initialized s) +* (Start-At (0,SCM+FSA))),1)) . f by A7, A33, SCMFSA_2:97
.= (Comput ((P +* (while>0 (a,I))),((Initialized s) +* (Start-At (0,SCM+FSA))),2)) . f by A15, SCMFSA_2:95
.= (Comput ((P +* (while>0 (a,I))),((Initialized s) +* (Start-At (0,SCM+FSA))),3)) . f by A18, SCMFSA_2:95
.= (Comput ((P +* (while>0 (a,I))),((Initialized s) +* (Start-At (0,SCM+FSA))),4)) . f by A21, SCMFSA_2:95 ; :: thesis: verum

end;

thus DataPart (IExec ((while>0 (a,I)),P,s)) = DataPart (IExec ((while>0 (a,I)),P,(Initialized s))) by SCMFSA8C:17
.= DataPart ((Result ((P +* (while>0 (a,I))),((Initialized s) +* (Initialize ((intloc 0) .--> 1))))) +* ((Initialized s) | NAT)) by SCMFSA6B:def 1
.= DataPart (Result ((P +* (while>0 (a,I))),((Initialized s) +* (Start-At (0,SCM+FSA))))) by A32, COMPOS_1:82
.= DataPart (Comput ((P +* (while>0 (a,I))),((Initialized s) +* (Start-At (0,SCM+FSA))),4)) by A24, A31, EXTPRO_1:23
.= DataPart (Initialized s) by A34, A35, SCMFSA6A:38 ; :: thesis: verum