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)),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)),s)) = DataPart (Initialized s)
let a be read-write Int-Location ; :: thesis: ( s . a <= 0 implies DataPart (IExec ((while>0 (a,I)),s)) = DataPart (Initialized s) )
set D = Int-Locations \/ FinSeq-Locations;
set Is = Initialized s;
set s1 = (Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)));
set s2 = Comput ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),1);
set s3 = Comput ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),2);
set s4 = Comput ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),3);
set s5 = Comput ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),4);
set i = a >0_goto 4;
A1: 1 in dom (while>0 (a,I)) by SCMFSA_9:10;
while>0 (a,I) c= (while>0 (a,I)) +* (Start-At (0,SCM+FSA)) by SCMFSA8A:9;
then A2: dom (while>0 (a,I)) c= dom ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))) by GRFUNC_1:8;
A3: (Comput ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),1)) . 1 = ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))) . 1 by AMI_1:54
.= ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))) . 1 by A2, A1, FUNCT_4:14
.= (while>0 (a,I)) . 1 by A1, COMPOS_1:145
.= goto 2 by SCMFSA_9:11 ;
IC SCM+FSA in dom ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))) by COMPOS_1:141;
then A4: IC ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))) = IC ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))) by FUNCT_4:14
.= 0 by COMPOS_1:142 ;
A5: 0 in dom (while>0 (a,I)) by SCMFSA_9:10;
then A6: ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))) . 0 = ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))) . 0 by A2, FUNCT_4:14
.= (while>0 (a,I)) . 0 by A5, COMPOS_1:145
.= a >0_goto 4 by SCMFSA_9:11 ;
then A7: CurInstr ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))) = a >0_goto 4 by A4, COMPOS_1:38;
A8: Comput ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),(0 + 1)) = Following ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),0))) by EXTPRO_1:4
.= Following ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))) by EXTPRO_1:3
.= Exec ((a >0_goto 4),((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))) by A4, A6, COMPOS_1:38 ;
set loc5 = (card I) + 5;
A9: 2 in dom (while>0 (a,I)) by SCMFSA_9:37;
A10: (Comput ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),2)) . 2 = ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))) . 2 by AMI_1:54
.= ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))) . 2 by A2, A9, FUNCT_4:14
.= (while>0 (a,I)) . 2 by A9, COMPOS_1:145
.= goto 3 by SCMFSA_9:41 ;
A11: IC (Initialized s) = 0 by SCMFSA6C:3;
A12: (card I) + 5 in dom (while>0 (a,I)) by SCMFSA_9:38;
not a in dom ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))) by SCMFSA6B:12;
then A13: ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))) . a = (Initialized s) . a by FUNCT_4:12;
A14: 3 in dom (while>0 (a,I)) by SCMFSA_9:37;
assume s . a <= 0 ; :: thesis: DataPart (IExec ((while>0 (a,I)),s)) = DataPart (Initialized s)
then (Initialized s) . a <= 0 by SCMFSA6C:3;
then A15: IC (Comput ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),1)) = succ 0 by A4, A8, A13, SCMFSA_2:97
.= 0 + 1 ;
T: ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))) = ProgramPart (Comput ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),1)) by AMI_1:123;
A16: Comput ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),(1 + 1)) = Following ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),1))) by EXTPRO_1:4
.= Exec ((goto 2),(Comput ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),1))) by A15, A3, T, COMPOS_1:38 ;
then A17: IC (Comput ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),2)) = 2 by SCMFSA_2:95;
Y: (ProgramPart (Comput ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),2))) /. (IC (Comput ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),2))) = (Comput ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),2)) . (IC (Comput ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),2))) by COMPOS_1:38;
T: ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))) = ProgramPart (Comput ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),2)) by AMI_1:123;
A18: Comput ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),(2 + 1)) = Following ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),2))) by EXTPRO_1:4
.= Exec ((goto 3),(Comput ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),2))) by A16, A10, Y, T, SCMFSA_2:95 ;
A19: (Comput ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),3)) . 3 = ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))) . 3 by AMI_1:54
.= ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))) . 3 by A2, A14, FUNCT_4:14
.= (while>0 (a,I)) . 3 by A14, COMPOS_1:145
.= goto ((card I) + 5) by SCMFSA_9:40 ;
Y: (ProgramPart (Comput ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),3))) /. (IC (Comput ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),3))) = (Comput ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),3)) . (IC (Comput ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),3))) by COMPOS_1:38;
T: ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))) = ProgramPart (Comput ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),3)) by AMI_1:123;
A20: Comput ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),(3 + 1)) = Following ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),3))) by EXTPRO_1:4
.= Exec ((goto ((card I) + 5)),(Comput ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),3))) by A18, A19, Y, T, SCMFSA_2:95 ;
Y: (ProgramPart (Comput ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),4))) /. (IC (Comput ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),4))) = (Comput ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),4)) . (IC (Comput ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),4))) by COMPOS_1:38;
TX: ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))) = ProgramPart (Comput ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),4)) by AMI_1:123;
(Comput ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),4)) . ((card I) + 5) = ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))) . ((card I) + 5) by AMI_1:54
.= ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))) . ((card I) + 5) by A2, A12, FUNCT_4:14
.= (while>0 (a,I)) . ((card I) + 5) by A12, COMPOS_1:145
.= halt SCM+FSA by SCMFSA_9:39 ;
then A21: CurInstr ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),4))) = halt SCM+FSA by A20, Y, TX, SCMFSA_2:95;
then A22: ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))) halts_on (Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))) by EXTPRO_1:30;
Y: (ProgramPart (Comput ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),3))) /. (IC (Comput ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),3))) = (Comput ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),3)) . (IC (Comput ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),3))) by COMPOS_1:38;
A23: CurInstr ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),3))) = goto ((card I) + 5) by A18, A19, Y, T, SCMFSA_2:95;

now

let k be Element of NAT ; :: thesis: ( CurInstr ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),k))) = halt SCM+FSA implies 3 + 1 <= k )
TX: ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))) = ProgramPart (Comput ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),k)) by AMI_1:123;
assume A25: CurInstr ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),k))) = halt SCM+FSA ; :: thesis: 3 + 1 <= k
then A26: k <> 2 by A17, A10, TX, COMPOS_1:38;
A27: k <> 0 by A25, A7, EXTPRO_1:3;
xx: k <> 1 by A15, A3, A25, TX, COMPOS_1:38;
3 < k by A27, A26, xx, A23, A25, NAT_1:28;
hence 3 + 1 <= k by INT_1:20; :: thesis: verum

end;

then A28: LifeSpan ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))) = 4 by A21, A22, EXTPRO_1:def 14;
A29: (Initialized s) +* (Initialized (while>0 (a,I))) = (Initialized (Initialized s)) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))) by SCMFSA8A:13
.= (Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))) by SCMFSA8C:15 ;
(Initialized s) . (intloc 0) = 1 by SCMFSA6C:3;
then A30: (Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))) = (Initialized s) +* (while>0 (a,I)) by A29, A11, Th6;

A31: now

let a be Int-Location ; :: thesis: (Initialized s) . a = (Comput ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),4)) . a
thus (Initialized s) . a = ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))) . a by A30, FUNCT_7:132, SCMFSA10:92
.= (Comput ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),1)) . a by A8, SCMFSA_2:97
.= (Comput ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),2)) . a by A16, SCMFSA_2:95
.= (Comput ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),3)) . a by A18, SCMFSA_2:95
.= (Comput ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),4)) . a by A20, SCMFSA_2:95 ; :: thesis: verum

end;

A32: now

let f be FinSeq-Location ; :: thesis: (Initialized s) . f = (Comput ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),4)) . f
thus (Initialized s) . f = ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))) . f by A30, FUNCT_7:132, SCMFSA10:93
.= (Comput ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),1)) . f by A8, SCMFSA_2:97
.= (Comput ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),2)) . f by A16, SCMFSA_2:95
.= (Comput ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),3)) . f by A18, SCMFSA_2:95
.= (Comput ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),4)) . f by A20, SCMFSA_2:95 ; :: thesis: verum

end;

thus DataPart (IExec ((while>0 (a,I)),s)) = DataPart (IExec ((while>0 (a,I)),(Initialized s))) by SCMFSA8C:17
.= DataPart ((Result ((ProgramPart ((Initialized s) +* (Initialized (while>0 (a,I))))),((Initialized s) +* (Initialized (while>0 (a,I)))))) +* ((Initialized s) | NAT)) by SCMFSA6B:def 1
.= DataPart (Result ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))))) by A29, SCMFSA8C:35
.= DataPart (Comput ((ProgramPart ((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA))))),((Initialized s) +* ((while>0 (a,I)) +* (Start-At (0,SCM+FSA)))),4)) by A22, A28, EXTPRO_1:23
.= DataPart (Initialized s) by A31, A32, SCMFSA6A:38 ; :: thesis: verum