let P be Instruction-Sequence of SCM+FSA; :: thesis: for s being State of SCM+FSA
for I being really-closed MacroInstruction of SCM+FSA
for a being read-write Int-Location st I is_halting_onInit s,P & s . a > 0 holds
( IC (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))) = 0 & DataPart (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))) = DataPart (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s))))) )
let s be State of SCM+FSA; :: thesis: for I being really-closed MacroInstruction of SCM+FSA
for a being read-write Int-Location st I is_halting_onInit s,P & s . a > 0 holds
( IC (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))) = 0 & DataPart (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))) = DataPart (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s))))) )
let I be really-closed MacroInstruction of SCM+FSA ; :: thesis: for a being read-write Int-Location st I is_halting_onInit s,P & s . a > 0 holds
( IC (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))) = 0 & DataPart (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))) = DataPart (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s))))) )
let a be read-write Int-Location; :: thesis: ( I is_halting_onInit s,P & s . a > 0 implies ( IC (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))) = 0 & DataPart (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))) = DataPart (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s))))) ) )
set D = Data-Locations ;
set s0 = Initialized s;
set s1 = Initialize (Initialized s);
set P1 = P +* (while>0 (a,I));
set PI = P +* I;
set s2 = Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),1);
set i = a >0_goto 3;
A1: while>0 (a,I) c= P +* (while>0 (a,I)) by FUNCT_4:25;
defpred S1[ Nat] means ( $1 <= LifeSpan ((P +* I),(Initialize (Initialized s))) implies ( IC (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),(1 + $1))) = (IC (Comput ((P +* I),(Initialize (Initialized s)),$1))) + 3 & DataPart (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),(1 + $1))) = DataPart (Comput ((P +* I),(Initialize (Initialized s)),$1)) ) );
set loc4 = (card I) + 2;
set s3 = Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),((1 + (LifeSpan ((P +* I),(Initialize (Initialized s))))) + 1));
A2: Initialize (Initialized s) = Initialize (Initialized s)
.= Initialize (Initialized s)
.= Initialized s by MEMSTR_0:44 ;
assume I is_halting_onInit s,P ; :: thesis: ( not s . a > 0 or ( IC (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))) = 0 & DataPart (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))) = DataPart (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s))))) ) )
then A3: P +* I halts_on Initialized s ;
A4: I is_halting_on Initialized s,P by A3, A2;
A5: now :: thesis: for k being Nat st S1[k] holds
S1[k + 1]
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A6: S1[k] ; :: thesis: S1[k + 1]
now :: thesis: ( k + 1 <= LifeSpan ((P +* I),(Initialize (Initialized s))) implies ( IC (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),((1 + k) + 1))) = (IC (Comput ((P +* I),(Initialize (Initialized s)),(k + 1)))) + 3 & DataPart (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),((1 + k) + 1))) = DataPart (Comput ((P +* I),(Initialize (Initialized s)),(k + 1))) ) )
A7: k + 0 < k + 1 by XREAL_1:6;
assume k + 1 <= LifeSpan ((P +* I),(Initialize (Initialized s))) ; :: thesis: ( IC (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),((1 + k) + 1))) = (IC (Comput ((P +* I),(Initialize (Initialized s)),(k + 1)))) + 3 & DataPart (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),((1 + k) + 1))) = DataPart (Comput ((P +* I),(Initialize (Initialized s)),(k + 1))) )
then k < LifeSpan ((P +* I),(Initialize (Initialized s))) by A7, XXREAL_0:2;
hence ( IC (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),((1 + k) + 1))) = (IC (Comput ((P +* I),(Initialize (Initialized s)),(k + 1)))) + 3 & DataPart (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),((1 + k) + 1))) = DataPart (Comput ((P +* I),(Initialize (Initialized s)),(k + 1))) ) by A4, A6, SCMFSA_9:39; :: thesis: verum
end;
hence S1[k + 1] ; :: thesis: verum
end;
0 in dom (while>0 (a,I)) by AFINSQ_1:65;
then A8: (P +* (while>0 (a,I))) . 0 = (while>0 (a,I)) . 0 by A1, GRFUNC_1:2
.= a >0_goto 3 by SCMFSA_X:10 ;
IC in dom (Start-At (0,SCM+FSA)) by MEMSTR_0:15;
then A9: IC (Initialize (Initialized s)) = IC (Start-At (0,SCM+FSA)) by FUNCT_4:13
.= 0 by FUNCOP_1:72 ;
A10: 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 A9, A8, PBOOLE:143 ;
then A11: for f being FinSeq-Location holds (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),1)) . f = (Initialize (Initialized s)) . f by SCMFSA_2:71;
for c being Int-Location holds (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),1)) . c = (Initialize (Initialized s)) . c by A10, SCMFSA_2:71;
then A12: DataPart (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),1)) = DataPart (Initialize (Initialized s)) by A11, SCMFSA_M:2
.= DataPart (Initialize (Initialized s)) ;
set s4 = Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),((1 + (LifeSpan ((P +* I),(Initialize (Initialized s))))) + 1));
set s2 = Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),(1 + (LifeSpan ((P +* I),(Initialize (Initialized s))))));
not a in dom (Start-At (0,SCM+FSA)) by SCMFSA_2:102;
then A13: (Initialize (Initialized s)) . a = (Initialized s) . a by FUNCT_4:11;
assume s . a > 0 ; :: thesis: ( IC (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))) = 0 & DataPart (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))) = DataPart (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s))))) )
then A14: (Initialized s) . a > 0 by SCMFSA_M:37;
A15: S1[ 0 ]
proof
assume 0 <= LifeSpan ((P +* I),(Initialize (Initialized s))) ; :: thesis: ( IC (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),(1 + 0))) = (IC (Comput ((P +* I),(Initialize (Initialized s)),0))) + 3 & DataPart (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),(1 + 0))) = DataPart (Comput ((P +* I),(Initialize (Initialized s)),0)) )
A16: IC in dom (Start-At (0,SCM+FSA)) by MEMSTR_0:15;
IC (Comput ((P +* I),(Initialize (Initialized s)),0)) = IC (Initialize (Initialized s))
.= IC (Start-At (0,SCM+FSA)) by A16, FUNCT_4:13
.= 0 by FUNCOP_1:72 ;
hence ( IC (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),(1 + 0))) = (IC (Comput ((P +* I),(Initialize (Initialized s)),0))) + 3 & DataPart (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),(1 + 0))) = DataPart (Comput ((P +* I),(Initialize (Initialized s)),0)) ) by A14, A10, A13, A12, SCMFSA_2:71; :: thesis: verum
end;
for k being Nat holds S1[k] from NAT_1:sch 2(A15, A5);
 then A17: S1[ LifeSpan ((P +* I),(Initialize (Initialized s)))] ;
A18: Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),((1 + (LifeSpan ((P +* I),(Initialize (Initialized s))))) + 1)) = Following ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),(1 + (LifeSpan ((P +* I),(Initialize (Initialized s)))))))) by EXTPRO_1:3
.= Exec ((goto 0),(Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),(1 + (LifeSpan ((P +* I),(Initialize (Initialized s)))))))) by A4, A17, SCMFSA_9:40 ;
A19: Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),((1 + (LifeSpan ((P +* I),(Initialize (Initialized s))))) + 1)) = Exec ((goto 0),(Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),(1 + (LifeSpan ((P +* I),(Initialize (Initialized s)))))))) by A18;
then A20: for f being FinSeq-Location holds (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),((1 + (LifeSpan ((P +* I),(Initialize (Initialized s))))) + 1))) . f = (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),(1 + (LifeSpan ((P +* I),(Initialize (Initialized s))))))) . f by SCMFSA_2:69;
for c being Int-Location holds (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),((1 + (LifeSpan ((P +* I),(Initialize (Initialized s))))) + 1))) . c = (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),(1 + (LifeSpan ((P +* I),(Initialize (Initialized s))))))) . c by A18, SCMFSA_2:69;
then A21: DataPart (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),((1 + (LifeSpan ((P +* I),(Initialize (Initialized s))))) + 1))) = DataPart (Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),(1 + (LifeSpan ((P +* I),(Initialize (Initialized s))))))) by A20, SCMFSA_M:2;
A22: Initialized s = Initialize (Initialized s) by MEMSTR_0:44;
Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2)) = Comput ((P +* (while>0 (a,I))),(Initialize (Initialized s)),((1 + (LifeSpan ((P +* I),(Initialize (Initialized s))))) + 1)) by A22;
hence IC (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))) = 0 by A19, SCMFSA_2:69; :: thesis: DataPart (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))) = DataPart (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s)))))
A23: Initialize (Initialized s) = Initialized s by MEMSTR_0:44;
thus DataPart (Comput ((P +* (while>0 (a,I))),(Initialized s),((LifeSpan ((P +* I),(Initialized s))) + 2))) = DataPart (Comput ((P +* I),(Initialized s),(LifeSpan ((P +* I),(Initialized s))))) by A23, A17, A21; :: thesis: verum