let I be InitHalting good really-closed MacroInstruction of SCM+FSA ; :: thesis: for a being read-write Int-Location st ex f being Function of ,INT st
for s, t being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA holds
( ( f . s > 0 implies f . (IExec (I,P,s)) < f . s ) & ( DataPart s = DataPart t implies f . s = f . t ) & ( f . s <= 0 implies s . a <= 0 ) & ( s . a <= 0 implies f . s <= 0 ) ) holds
while>0 (a,I) is InitHalting

let a be read-write Int-Location; :: thesis: ( ex f being Function of ,INT st
for s, t being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA holds
( ( f . s > 0 implies f . (IExec (I,P,s)) < f . s ) & ( DataPart s = DataPart t implies f . s = f . t ) & ( f . s <= 0 implies s . a <= 0 ) & ( s . a <= 0 implies f . s <= 0 ) ) implies while>0 (a,I) is InitHalting )

set D = Data-Locations ;
given f being Function of ,INT such that A1: for s, t being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA holds
( ( f . s > 0 implies f . (IExec (I,P,s)) < f . s ) & ( DataPart s = DataPart t implies f . s = f . t ) & ( f . s <= 0 implies s . a <= 0 ) & ( s . a <= 0 implies f . s <= 0 ) ) ; :: thesis: while>0 (a,I) is InitHalting
defpred S1[ Nat] means for t being State of SCM+FSA
for Q being Instruction-Sequence of SCM+FSA st f . t <= \$1 holds
while>0 (a,I) is_halting_onInit t,Q;
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: for t being State of SCM+FSA
for Q being Instruction-Sequence of SCM+FSA st f . t <= k + 1 holds
while>0 (a,I) is_halting_onInit t,Q
let t be State of SCM+FSA; :: thesis: for Q being Instruction-Sequence of SCM+FSA st f . t <= k + 1 holds
while>0 (a,I) is_halting_onInit b2,b3

let Q be Instruction-Sequence of SCM+FSA; :: thesis: ( f . t <= k + 1 implies while>0 (a,I) is_halting_onInit b1,b2 )
assume A4: f . t <= k + 1 ; :: thesis: while>0 (a,I) is_halting_onInit b1,b2
per cases ( f . t <> k + 1 or f . t = k + 1 ) ;
suppose f . t <> k + 1 ; :: thesis: while>0 (a,I) is_halting_onInit b1,b2
then f . t < k + 1 by ;
hence while>0 (a,I) is_halting_onInit t,Q by ; :: thesis: verum
end;
suppose A5: f . t = k + 1 ; :: thesis: while>0 (a,I) is_halting_onInit b1,b2
set l0 = intloc 0;
set tW0 = Initialized t;
set QW = Q +* (while>0 (a,I));
set t1 = Initialized t;
set Q1 = Q +* I;
set Wt = Comput ((Q +* (while>0 (a,I))),(),((LifeSpan ((Q +* I),())) + 2));
set It = Comput ((Q +* I),(),(LifeSpan ((Q +* I),())));
A6: I is_halting_onInit t,Q by SCM_HALT:26;
then A7: Q +* I halts_on Initialized t ;
A8: not t . a <= 0 by A1, A5;
then A9: DataPart (Comput ((Q +* (while>0 (a,I))),(),((LifeSpan ((Q +* I),())) + 2))) = DataPart (Comput ((Q +* I),(),(LifeSpan ((Q +* I),())))) by ;
then A10: (Comput ((Q +* (while>0 (a,I))),(),((LifeSpan ((Q +* I),())) + 2))) . () = (Comput ((Q +* I),(),(LifeSpan ((Q +* I),())))) . () by SCMFSA_M:2
.= (Result ((Q +* I),())) . () by
.= (Result ((Q +* I),())) . ()
.= (IExec (I,Q,t)) . () by SCMFSA6B:def 1
.= 1 by SCM_HALT:9 ;
DataPart (Comput ((Q +* (while>0 (a,I))),(),((LifeSpan ((Q +* I),())) + 2))) = DataPart (Result ((Q +* I),())) by
.= DataPart (Result ((Q +* I),()))
.= DataPart (IExec (I,Q,t)) by SCMFSA6B:def 1 ;
then f . (Comput ((Q +* (while>0 (a,I))),(),((LifeSpan ((Q +* I),())) + 2))) = f . (IExec (I,Q,t)) by A1;
then f . (Comput ((Q +* (while>0 (a,I))),(),((LifeSpan ((Q +* I),())) + 2))) < k + 1 by A1, A5;
then while>0 (a,I) is_halting_onInit Comput ((Q +* (while>0 (a,I))),(),((LifeSpan ((Q +* I),())) + 2)),Q +* (while>0 (a,I)) by ;
then A11: (Q +* (while>0 (a,I))) +* (while>0 (a,I)) halts_on Initialized (Comput ((Q +* (while>0 (a,I))),(),((LifeSpan ((Q +* I),())) + 2))) ;
IC (Comput ((Q +* (while>0 (a,I))),(),((LifeSpan ((Q +* I),())) + 2))) = 0 by ;
then A12: Initialized (Comput ((Q +* (while>0 (a,I))),(),((LifeSpan ((Q +* I),())) + 2))) = Comput ((Q +* (while>0 (a,I))),(),((LifeSpan ((Q +* I),())) + 2)) by ;
now :: thesis: ex mm being set st CurInstr ((Q +* (while>0 (a,I))),(Comput ((Q +* (while>0 (a,I))),(),mm))) = halt SCM+FSA
consider m being Nat such that
A13: CurInstr ((Q +* (while>0 (a,I))),(Comput ((Q +* (while>0 (a,I))),(Comput ((Q +* (while>0 (a,I))),(),((LifeSpan ((Q +* I),())) + 2))),m))) = halt SCM+FSA by ;
take mm = ((LifeSpan ((Q +* I),())) + 2) + m; :: thesis: CurInstr ((Q +* (while>0 (a,I))),(Comput ((Q +* (while>0 (a,I))),(),mm))) = halt SCM+FSA
thus CurInstr ((Q +* (while>0 (a,I))),(Comput ((Q +* (while>0 (a,I))),(),mm))) = halt SCM+FSA by ; :: thesis: verum
end;
then Q +* (while>0 (a,I)) halts_on Initialized t by EXTPRO_1:29;
hence while>0 (a,I) is_halting_onInit t,Q ; :: thesis: verum
end;
end;
end;
hence S1[k + 1] ; :: thesis: verum
end;
A14: S1[ 0 ]
proof
let t be State of SCM+FSA; :: thesis: for Q being Instruction-Sequence of SCM+FSA st f . t <= 0 holds
while>0 (a,I) is_halting_onInit t,Q

let Q be Instruction-Sequence of SCM+FSA; :: thesis: ( f . t <= 0 implies while>0 (a,I) is_halting_onInit t,Q )
assume f . t <= 0 ; :: thesis: while>0 (a,I) is_halting_onInit t,Q
then t . a <= 0 by A1;
hence while>0 (a,I) is_halting_onInit t,Q by SCM_HALT:73; :: thesis: verum
end;
A15: for k being Nat holds S1[k] from NAT_1:sch 2(A14, A2);
now :: thesis: for t being State of SCM+FSA
for Q being Instruction-Sequence of SCM+FSA holds while>0 (a,I) is_halting_onInit t,Q
end;
hence while>0 (a,I) is InitHalting by SCM_HALT:26; :: thesis: verum