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_on s,P & s . a > 0 holds
( IC (Comput ((P +* (while>0 (a,I))),(),((LifeSpan ((P +* I),())) + 2))) = 0 & ( for k being Nat st k <= (LifeSpan ((P +* I),())) + 2 holds
IC (Comput ((P +* (while>0 (a,I))),(),k)) in dom (while>0 (a,I)) ) )

set D = Int-Locations \/ FinSeq-Locations;
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_on s,P & s . a > 0 holds
( IC (Comput ((P +* (while>0 (a,I))),(),((LifeSpan ((P +* I),())) + 2))) = 0 & ( for k being Nat st k <= (LifeSpan ((P +* I),())) + 2 holds
IC (Comput ((P +* (while>0 (a,I))),(),k)) in dom (while>0 (a,I)) ) )

let I be really-closed MacroInstruction of SCM+FSA ; :: thesis: for a being read-write Int-Location st I is_halting_on s,P & s . a > 0 holds
( IC (Comput ((P +* (while>0 (a,I))),(),((LifeSpan ((P +* I),())) + 2))) = 0 & ( for k being Nat st k <= (LifeSpan ((P +* I),())) + 2 holds
IC (Comput ((P +* (while>0 (a,I))),(),k)) in dom (while>0 (a,I)) ) )

let a be read-write Int-Location; :: thesis: ( I is_halting_on s,P & s . a > 0 implies ( IC (Comput ((P +* (while>0 (a,I))),(),((LifeSpan ((P +* I),())) + 2))) = 0 & ( for k being Nat st k <= (LifeSpan ((P +* I),())) + 2 holds
IC (Comput ((P +* (while>0 (a,I))),(),k)) in dom (while>0 (a,I)) ) ) )

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),()) implies ( IC (Comput ((P +* (while>0 (a,I))),(),(1 + \$1))) = (IC (Comput ((P +* I),(),\$1))) + 3 & DataPart (Comput ((P +* (while>0 (a,I))),(),(1 + \$1))) = DataPart (Comput ((P +* I),(),\$1)) ) );
assume A1: I is_halting_on s,P ; :: thesis: ( not s . a > 0 or ( IC (Comput ((P +* (while>0 (a,I))),(),((LifeSpan ((P +* I),())) + 2))) = 0 & ( for k being Nat st k <= (LifeSpan ((P +* I),())) + 2 holds
IC (Comput ((P +* (while>0 (a,I))),(),k)) in dom (while>0 (a,I)) ) ) )

A2: 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 A3: S1[k] ; :: thesis: S1[k + 1]
now :: thesis: ( k + 1 <= LifeSpan ((P +* I),()) implies ( IC (Comput ((P +* (while>0 (a,I))),(),((1 + k) + 1))) = (IC (Comput ((P +* I),(),(k + 1)))) + 3 & DataPart (Comput ((P +* (while>0 (a,I))),(),((1 + k) + 1))) = DataPart (Comput ((P +* I),(),(k + 1))) ) )
A4: k + 0 < k + 1 by XREAL_1:6;
assume k + 1 <= LifeSpan ((P +* I),()) ; :: thesis: ( IC (Comput ((P +* (while>0 (a,I))),(),((1 + k) + 1))) = (IC (Comput ((P +* I),(),(k + 1)))) + 3 & DataPart (Comput ((P +* (while>0 (a,I))),(),((1 + k) + 1))) = DataPart (Comput ((P +* I),(),(k + 1))) )
then k < LifeSpan ((P +* I),()) by ;
hence ( IC (Comput ((P +* (while>0 (a,I))),(),((1 + k) + 1))) = (IC (Comput ((P +* I),(),(k + 1)))) + 3 & DataPart (Comput ((P +* (while>0 (a,I))),(),((1 + k) + 1))) = DataPart (Comput ((P +* I),(),(k + 1))) ) by A1, A3, Th13; :: thesis: verum
end;
hence S1[k + 1] ; :: thesis: verum
end;
reconsider l = LifeSpan ((P +* I),()) as Element of NAT by ORDINAL1:def 12;
set loc4 = (card I) + 3;
set i = a >0_goto 3;
set s2 = Comput ((P +* (while>0 (a,I))),(),1);
IC in dom () by MEMSTR_0:15;
then A5: IC () = IC () by FUNCT_4:13
.= 0 by FUNCOP_1:72 ;
not a in dom () by SCMFSA_2:102;
then A6: (Initialize s) . a = s . a by FUNCT_4:11;
assume A7: s . a > 0 ; :: thesis: ( IC (Comput ((P +* (while>0 (a,I))),(),((LifeSpan ((P +* I),())) + 2))) = 0 & ( for k being Nat st k <= (LifeSpan ((P +* I),())) + 2 holds
IC (Comput ((P +* (while>0 (a,I))),(),k)) in dom (while>0 (a,I)) ) )

A8: 0 in dom (while>0 (a,I)) by AFINSQ_1:65;
A9: (P +* (while>0 (a,I))) /. (IC ()) = (P +* (while>0 (a,I))) . (IC ()) by PBOOLE:143;
(P +* (while>0 (a,I))) . 0 = (while>0 (a,I)) . 0 by
.= a >0_goto 3 by SCMFSA_X:10 ;
then A10: CurInstr ((P +* (while>0 (a,I))),()) = a >0_goto 3 by A5, A9;
A11: Comput ((P +* (while>0 (a,I))),(),(0 + 1)) = Following ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(),0))) by EXTPRO_1:3
.= Exec ((a >0_goto 3),()) by A10 ;
then ( ( for c being Int-Location holds (Comput ((P +* (while>0 (a,I))),(),1)) . c = () . c ) & ( for f being FinSeq-Location holds (Comput ((P +* (while>0 (a,I))),(),1)) . f = () . f ) ) by SCMFSA_2:71;
then A12: DataPart (Comput ((P +* (while>0 (a,I))),(),1)) = DataPart () by SCMFSA_M:2;
A13: IC (Comput ((P +* (while>0 (a,I))),(),1)) = 3 by ;
A14: S1[ 0 ]
proof
assume 0 <= LifeSpan ((P +* I),()) ; :: thesis: ( IC (Comput ((P +* (while>0 (a,I))),(),(1 + 0))) = (IC (Comput ((P +* I),(),0))) + 3 & DataPart (Comput ((P +* (while>0 (a,I))),(),(1 + 0))) = DataPart (Comput ((P +* I),(),0)) )
A15: IC in dom () by MEMSTR_0:15;
IC (Comput ((P +* I),(),0)) = IC () by
.= 0 by FUNCOP_1:72 ;
hence ( IC (Comput ((P +* (while>0 (a,I))),(),(1 + 0))) = (IC (Comput ((P +* I),(),0))) + 3 & DataPart (Comput ((P +* (while>0 (a,I))),(),(1 + 0))) = DataPart (Comput ((P +* I),(),0)) ) by ; :: thesis: verum
end;
A16: for k being Nat holds S1[k] from NAT_1:sch 2(A14, A2);
set s4 = Comput ((P +* (while>0 (a,I))),(),((1 + (LifeSpan ((P +* I),()))) + 1));
set s3 = Comput ((P +* (while>0 (a,I))),(),(1 + (LifeSpan ((P +* I),()))));
set s2 = Comput ((P +* (while>0 (a,I))),(),(1 + (LifeSpan ((P +* I),()))));
S1[l] by A16;
then A17: CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(),(1 + (LifeSpan ((P +* I),())))))) = goto 0 by ;
A18: CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(),(1 + (LifeSpan ((P +* I),())))))) = goto 0 by A17;
A19: Comput ((P +* (while>0 (a,I))),(),((1 + (LifeSpan ((P +* I),()))) + 1)) = Following ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(),(1 + (LifeSpan ((P +* I),())))))) by EXTPRO_1:3
.= Exec ((),(Comput ((P +* (while>0 (a,I))),(),(1 + (LifeSpan ((P +* I),())))))) by A18 ;
A20: IC (Comput ((P +* (while>0 (a,I))),(),((1 + (LifeSpan ((P +* I),()))) + 1))) = 0 by ;
hence IC (Comput ((P +* (while>0 (a,I))),(),((LifeSpan ((P +* I),())) + 2))) = 0 ; :: thesis: for k being Nat st k <= (LifeSpan ((P +* I),())) + 2 holds
IC (Comput ((P +* (while>0 (a,I))),(),k)) in dom (while>0 (a,I))

A21: now :: thesis: for k being Nat st k <= (LifeSpan ((P +* I),())) + 2 & k <> 0 holds
IC (Comput ((P +* (while>0 (a,I))),(),k)) in dom (while>0 (a,I))
let k be Nat; :: thesis: ( k <= (LifeSpan ((P +* I),())) + 2 & k <> 0 implies IC (Comput ((P +* (while>0 (a,I))),(),b1)) in dom (while>0 (a,I)) )
assume A22: k <= (LifeSpan ((P +* I),())) + 2 ; :: thesis: ( k <> 0 implies IC (Comput ((P +* (while>0 (a,I))),(),b1)) in dom (while>0 (a,I)) )
assume k <> 0 ; :: thesis: IC (Comput ((P +* (while>0 (a,I))),(),b1)) in dom (while>0 (a,I))
then consider n being Nat such that
A23: k = n + 1 by NAT_1:6;
( k <= (LifeSpan ((P +* I),())) + 1 or k >= ((LifeSpan ((P +* I),())) + 1) + 1 ) by NAT_1:13;
then A24: ( k <= (LifeSpan ((P +* I),())) + 1 or k = (LifeSpan ((P +* I),())) + 2 ) by ;
reconsider n = n as Element of NAT by ORDINAL1:def 12;
per cases ( k <= (LifeSpan ((P +* I),())) + 1 or k >= (LifeSpan ((P +* I),())) + 2 ) by A24;
suppose k <= (LifeSpan ((P +* I),())) + 1 ; :: thesis: IC (Comput ((P +* (while>0 (a,I))),(),b1)) in dom (while>0 (a,I))
then n <= LifeSpan ((P +* I),()) by ;
then A25: IC (Comput ((P +* (while>0 (a,I))),(),(1 + n))) = (IC (Comput ((P +* I),(),n))) + 3 by A16;
reconsider m = IC (Comput ((P +* I),(),n)) as Element of NAT ;
A26: I c= P +* I by FUNCT_4:25;
IC () = 0 by MEMSTR_0:def 11;
then IC () in dom I by AFINSQ_1:65;
then m in dom I by ;
then m < card I by AFINSQ_1:66;
then A27: m + 3 < (card I) + 5 by XREAL_1:8;
card (while>0 (a,I)) = (card I) + 5 by SCMFSA_X:4;
hence IC (Comput ((P +* (while>0 (a,I))),(),k)) in dom (while>0 (a,I)) by ; :: thesis: verum
end;
suppose k >= (LifeSpan ((P +* I),())) + 2 ; :: thesis: IC (Comput ((P +* (while>0 (a,I))),(),b1)) in dom (while>0 (a,I))
then k = (LifeSpan ((P +* I),())) + 2 by ;
hence IC (Comput ((P +* (while>0 (a,I))),(),k)) in dom (while>0 (a,I)) by ; :: thesis: verum
end;
end;
end;
now :: thesis: for k being Nat st k <= (LifeSpan ((P +* I),())) + 2 holds
IC (Comput ((P +* (while>0 (a,I))),(),k)) in dom (while>0 (a,I))
let k be Nat; :: thesis: ( k <= (LifeSpan ((P +* I),())) + 2 implies IC (Comput ((P +* (while>0 (a,I))),(),b1)) in dom (while>0 (a,I)) )
assume A28: k <= (LifeSpan ((P +* I),())) + 2 ; :: thesis: IC (Comput ((P +* (while>0 (a,I))),(),b1)) in dom (while>0 (a,I))
per cases ( k = 0 or k <> 0 ) ;
suppose k = 0 ; :: thesis: IC (Comput ((P +* (while>0 (a,I))),(),b1)) in dom (while>0 (a,I))
hence IC (Comput ((P +* (while>0 (a,I))),(),k)) in dom (while>0 (a,I)) by A8, A5; :: thesis: verum
end;
suppose k <> 0 ; :: thesis: IC (Comput ((P +* (while>0 (a,I))),(),b1)) in dom (while>0 (a,I))
hence IC (Comput ((P +* (while>0 (a,I))),(),k)) in dom (while>0 (a,I)) by ; :: thesis: verum
end;
end;
end;
hence for k being Nat st k <= (LifeSpan ((P +* I),())) + 2 holds
IC (Comput ((P +* (while>0 (a,I))),(),k)) in dom (while>0 (a,I)) ; :: thesis: verum