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