set D = Int-Locations \/ FinSeq-Locations;
let s be State of SCM+FSA; :: thesis: for I being Program of SCM+FSA
for a being read-write Int-Location st I is_closed_on s & I is_halting_on s & s . a = 0 holds
( IC (Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 3))) = 0 & ( for k being Element of NAT st k <= (LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 3 holds
IC (Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),k)) in dom (while=0 (a,I)) ) )
let I be Program of SCM+FSA; :: thesis: for a being read-write Int-Location st I is_closed_on s & I is_halting_on s & s . a = 0 holds
( IC (Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 3))) = 0 & ( for k being Element of NAT st k <= (LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 3 holds
IC (Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),k)) in dom (while=0 (a,I)) ) )
let a be read-write Int-Location ; :: thesis: ( I is_closed_on s & I is_halting_on s & s . a = 0 implies ( IC (Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 3))) = 0 & ( for k being Element of NAT st k <= (LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 3 holds
IC (Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),k)) in dom (while=0 (a,I)) ) ) )
assume A1: I is_closed_on s ; :: thesis: ( not I is_halting_on s or not s . a = 0 or ( IC (Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 3))) = 0 & ( for k being Element of NAT st k <= (LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 3 holds
IC (Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),k)) in dom (while=0 (a,I)) ) ) )
set sI = s +* (I +* (Start-At (0,SCM+FSA)));
set s1 = s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)));
defpred S1[ Nat] means ( $1 <= LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA))))) implies ( IC (Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),(1 + $1))) = (IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),$1))) + 4 & DataPart (Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),(1 + $1))) = DataPart (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),$1)) ) );
assume A2: I is_halting_on s ; :: thesis: ( not s . a = 0 or ( IC (Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 3))) = 0 & ( for k being Element of NAT st k <= (LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 3 holds
IC (Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),k)) in dom (while=0 (a,I)) ) ) )
A3: now
let k be Element of NAT ; :: thesis: ( S1[k] implies S1[k + 1] )
assume A4: S1[k] ; :: thesis: S1[k + 1]
now
A5: k + 0 < k + 1 by XREAL_1:8;
assume k + 1 <= LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA))))) ; :: thesis: ( IC (Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),((1 + k) + 1))) = (IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),(k + 1)))) + 4 & DataPart (Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),((1 + k) + 1))) = DataPart (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),(k + 1))) )
then k < LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA))))) by A5, XXREAL_0:2;
hence ( IC (Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),((1 + k) + 1))) = (IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),(k + 1)))) + 4 & DataPart (Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),((1 + k) + 1))) = DataPart (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),(k + 1))) ) by A1, A2, A4, Th19; :: thesis: verum
end;
hence S1[k + 1] ; :: thesis: verum
end;
reconsider l = LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA))))) as Element of NAT ;
set loc4 = (card I) + 4;
set i = a =0_goto 4;
set s2 = Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),1);
A6: IC SCM+FSA in dom ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))) by COMPOS_1:141;
A7: IC (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))) = IC ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))) by A6, FUNCT_4:14
.= 0 by COMPOS_1:142 ;
not a in dom ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))) by SCMFSA6B:12;
then A8: (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))) . a = s . a by FUNCT_4:12;
assume A9: s . a = 0 ; :: thesis: ( IC (Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 3))) = 0 & ( for k being Element of NAT st k <= (LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 3 holds
IC (Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),k)) in dom (while=0 (a,I)) ) )
A10: 0 in dom (while=0 (a,I)) by Th10;
Y: (ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))) /. (IC (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))) = (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))) . (IC (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))) by COMPOS_1:38;
while=0 (a,I) c= (while=0 (a,I)) +* (Start-At (0,SCM+FSA)) by SCMFSA8A:9;
then A11: dom (while=0 (a,I)) c= dom ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))) by GRFUNC_1:8;
then (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))) . 0 = ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))) . 0 by A10, FUNCT_4:14
.= (while=0 (a,I)) . 0 by A10, COMPOS_1:145
.= a =0_goto 4 by Th11 ;
then A12: CurInstr ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))) = a =0_goto 4 by A7, Y;
A13: Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),(0 + 1)) = Following ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),0))) by EXTPRO_1:4
.= Following ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))) by EXTPRO_1:3
.= Exec ((a =0_goto 4),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))) by A12 ;
then ( ( for c being Int-Location holds (Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),1)) . c = (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))) . c ) & ( for f being FinSeq-Location holds (Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),1)) . f = (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))) . f ) ) by SCMFSA_2:96;
then A14: DataPart (Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),1)) = DataPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))) by SCMFSA6A:38
.= DataPart s by SCMFSA8A:11
.= DataPart (s +* (I +* (Start-At (0,SCM+FSA)))) by SCMFSA8A:11 ;
A15: IC (Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),1)) = (Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),1)) . (IC SCM+FSA)
.= 4 by A9, A13, A8, SCMFSA_2:96 ;
A16: S1[ 0 ]
proof
assume 0 <= LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA))))) ; :: thesis: ( IC (Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),(1 + 0))) = (IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),0))) + 4 & DataPart (Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),(1 + 0))) = DataPart (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),0)) )
A17: IC SCM+FSA in dom (I +* (Start-At (0,SCM+FSA))) by COMPOS_1:141;
IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),0)) = IC (s +* (I +* (Start-At (0,SCM+FSA)))) by EXTPRO_1:3
.= IC (I +* (Start-At (0,SCM+FSA))) by A17, FUNCT_4:14
.= 0 by COMPOS_1:142 ;
hence ( IC (Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),(1 + 0))) = (IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),0))) + 4 & DataPart (Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),(1 + 0))) = DataPart (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),0)) ) by A15, A14, EXTPRO_1:3; :: thesis: verum
end;
A18: for k being Element of NAT holds S1[k] from NAT_1:sch 1(A16, A3);
 set s4 = Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),(((1 + (LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA))))))) + 1) + 1));
set s3 = Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),((1 + (LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA))))))) + 1));
A19: (card I) + 4 in dom (while=0 (a,I)) by Th13;
set s2 = Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),(1 + (LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA))))))));
S1[l] by A18;
then A20: CurInstr ((ProgramPart (Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),(1 + (LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))))))),(Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),(1 + (LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))))))) = goto ((card I) + 4) by A1, A2, Th20;
T: ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))) = ProgramPart (Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),(1 + (LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA))))))))) by AMI_1:123;
A21: Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),((1 + (LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA))))))) + 1)) = Following ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),(1 + (LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))))))) by EXTPRO_1:4
.= Exec ((goto ((card I) + 4)),(Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),(1 + (LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))))))) by A20, T ;
A22: IC (Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),((1 + (LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA))))))) + 1))) = (Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),((1 + (LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA))))))) + 1))) . (IC SCM+FSA)
.= (card I) + 4 by A21, SCMFSA_2:95 ;
Y: (ProgramPart (Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),((1 + (LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA))))))) + 1)))) /. (IC (Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),((1 + (LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA))))))) + 1)))) = (Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),((1 + (LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA))))))) + 1))) . (IC (Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),((1 + (LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA))))))) + 1)))) by COMPOS_1:38;
(Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),((1 + (LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA))))))) + 1))) . ((card I) + 4) = (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))) . ((card I) + 4) by AMI_1:54
.= ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))) . ((card I) + 4) by A11, A19, FUNCT_4:14
.= (while=0 (a,I)) . ((card I) + 4) by A19, COMPOS_1:145
.= goto 0 by Th21 ;
then A23: CurInstr ((ProgramPart (Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),((1 + (LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA))))))) + 1)))),(Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),((1 + (LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA))))))) + 1)))) = goto 0 by A22, Y;
T: ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))) = ProgramPart (Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),((1 + (LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA))))))) + 1))) by AMI_1:123;
A24: Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),(((1 + (LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA))))))) + 1) + 1)) = Following ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),((1 + (LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA))))))) + 1)))) by EXTPRO_1:4
.= Exec ((goto 0),(Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),((1 + (LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA))))))) + 1)))) by A23, T ;
A25: IC (Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),(((1 + (LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA))))))) + 1) + 1))) = (Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),(((1 + (LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA))))))) + 1) + 1))) . (IC SCM+FSA)
.= 0 by A24, SCMFSA_2:95 ;
hence IC (Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 3))) = 0 ; :: thesis: for k being Element of NAT st k <= (LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 3 holds
IC (Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),k)) in dom (while=0 (a,I))
A26: (((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1) + 1) + 1 = (LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + (2 + 1) ;
A27: now
let k be Element of NAT ; :: thesis: ( k <= (LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 3 & k <> 0 implies IC (Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),b1)) in dom (while=0 (a,I)) )
assume A28: k <= (LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 3 ; :: thesis: ( k <> 0 implies IC (Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),b1)) in dom (while=0 (a,I)) )
assume k <> 0 ; :: thesis: IC (Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),b1)) in dom (while=0 (a,I))
then consider n being Nat such that
A29: k = n + 1 by NAT_1:6;
( k <= (LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1 or k >= ((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1) + 1 ) by NAT_1:13;
then A30: ( k <= (LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1 or k = ((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1) + 1 or k > ((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1) + 1 ) by XXREAL_0:1;
reconsider n = n as Element of NAT by ORDINAL1:def 13;
per cases ( k <= (LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1 or k = ((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1) + 1 or k >= (LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 3 ) by A26, A30, NAT_1:13;
suppose k <= (LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1 ; :: thesis: IC (Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),b1)) in dom (while=0 (a,I))
then n <= LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA))))) by A29, XREAL_1:8;
then A31: IC (Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),(1 + n))) = (IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),n))) + 4 by A18;
reconsider m = IC (Comput ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))),n)) as Element of NAT ;
m in dom I by A1, SCMFSA7B:def 7;
then m < card I by AFINSQ_1:70;
then A32: m + 4 < (card I) + 6 by XREAL_1:10;
card (while=0 (a,I)) = (card I) + 6 by Th4;
hence IC (Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),k)) in dom (while=0 (a,I)) by A29, A31, A32, AFINSQ_1:70; :: thesis: verum
end;
suppose k = ((LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 1) + 1 ; :: thesis: IC (Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),b1)) in dom (while=0 (a,I))
hence IC (Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),k)) in dom (while=0 (a,I)) by A22, Th13; :: thesis: verum
end;
suppose k >= (LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 3 ; :: thesis: IC (Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),b1)) in dom (while=0 (a,I))
then k = (LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 3 by A28, XXREAL_0:1;
hence IC (Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),k)) in dom (while=0 (a,I)) by A25, Th10; :: thesis: verum
end;
end;
end;
now
let k be Element of NAT ; :: thesis: ( k <= (LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 3 implies IC (Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),b1)) in dom (while=0 (a,I)) )
assume A33: k <= (LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 3 ; :: thesis: IC (Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),b1)) in dom (while=0 (a,I))
per cases ( k = 0 or k <> 0 ) ;
suppose k = 0 ; :: thesis: IC (Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),b1)) in dom (while=0 (a,I))
hence IC (Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),k)) in dom (while=0 (a,I)) by A10, A7, EXTPRO_1:3; :: thesis: verum
end;
suppose k <> 0 ; :: thesis: IC (Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),b1)) in dom (while=0 (a,I))
hence IC (Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),k)) in dom (while=0 (a,I)) by A27, A33; :: thesis: verum
end;
end;
end;
hence for k being Element of NAT st k <= (LifeSpan ((ProgramPart (s +* (I +* (Start-At (0,SCM+FSA))))),(s +* (I +* (Start-At (0,SCM+FSA)))))) + 3 holds
IC (Comput ((ProgramPart (s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA))))),(s +* ((while=0 (a,I)) +* (Start-At (0,SCM+FSA)))),k)) in dom (while=0 (a,I)) ; :: thesis: verum