let I be InitHalting good Program of SCM+FSA; :: thesis: for a being read-write Int-Location st ( for s being State of SCM+FSA
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT st s . a > 0 holds
(IExec (I,P,s)) . a < s . a ) holds
while>0 (a,I) is InitHalting
let a be read-write Int-Location ; :: thesis: ( ( for s being State of SCM+FSA
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT st s . a > 0 holds
(IExec (I,P,s)) . a < s . a ) implies while>0 (a,I) is InitHalting )
set D = Data-Locations SCM+FSA;
defpred S₁[ Element of NAT ] means for t being State of SCM+FSA
for Q being the Instructions of SCM+FSA -valued ManySortedSet of NAT st t . a <= $1 holds
while>0 (a,I) is_halting_onInit t,Q;
assume A1: for s being State of SCM+FSA
for P being the Instructions of SCM+FSA -valued ManySortedSet of NAT st s . a > 0 holds
(IExec (I,P,s)) . a < s . a ; :: thesis: while>0 (a,I) is InitHalting

A2: now

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A3: S₁[k] ; :: thesis: S₁[k + 1]

now

let t be State of SCM+FSA; :: thesis: for Q being the Instructions of SCM+FSA -valued ManySortedSet of NAT st t . a <= k + 1 holds
while>0 (a,I) is_halting_onInit b₂,b₃
let Q be the Instructions of SCM+FSA -valued ManySortedSet of NAT ; :: thesis: ( t . a <= k + 1 implies while>0 (a,I) is_halting_onInit b₁,b₂ )
assume A4: t . a <= k + 1 ; :: thesis: while>0 (a,I) is_halting_onInit b₁,b₂

per cases ( t . a <> k + 1 or t . a = k + 1 ) ;

suppose t . a <> k + 1 ; :: thesis: while>0 (a,I) is_halting_onInit b₁,b₂

then t . a < k + 1 by A4, XXREAL_0:1;
hence while>0 (a,I) is_halting_onInit t,Q by A3, INT_1:20; :: thesis: verum

end;

suppose A5: t . a = k + 1 ; :: thesis: while>0 (a,I) is_halting_onInit b₁,b₂

set l0 = intloc 0;
set Iwhile = Initialized (while>0 (a,I));
set tW0 = t +* (Initialize ((intloc 0) .--> 1));
set QW = Q +* (while>0 (a,I));
set t1 = t +* (Initialize ((intloc 0) .--> 1));
set Q1 = Q +* I;
set Wt = Comput ((Q +* (while>0 (a,I))),(t +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((Q +* I),(t +* (Initialize ((intloc 0) .--> 1))))) + 3));
set A = NAT ;
set It = Comput ((Q +* I),(t +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((Q +* I),(t +* (Initialize ((intloc 0) .--> 1))))));
A6: I is_halting_onInit t,Q by SCM_HALT:36;
then Q +* I halts_on t +* (Initialize ((intloc 0) .--> 1)) by SCM_HALT:def 5;
then A7: Q +* I halts_on t +* (Initialize ((intloc 0) .--> 1)) ;
not intloc 0 in NAT by SCMFSA_2:84;
then not intloc 0 in (dom t) /\ NAT by XBOOLE_0:def 4;
then A8: not intloc 0 in dom (t | NAT) by RELAT_1:90;
A9: I is_closed_onInit t,Q by SCM_HALT:35;
then A10: DataPart (Comput ((Q +* (while>0 (a,I))),(t +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((Q +* I),(t +* (Initialize ((intloc 0) .--> 1))))) + 3))) = DataPart (Comput ((Q +* I),(t +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((Q +* I),(t +* (Initialize ((intloc 0) .--> 1))))))) by A5, A6, Th21;
then A11: (Comput ((Q +* (while>0 (a,I))),(t +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((Q +* I),(t +* (Initialize ((intloc 0) .--> 1))))) + 3))) . (intloc 0) = (Comput ((Q +* I),(t +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((Q +* I),(t +* (Initialize ((intloc 0) .--> 1))))))) . (intloc 0) by SCMFSA6A:38
.= (Result ((Q +* I),(t +* (Initialize ((intloc 0) .--> 1))))) . (intloc 0) by A7, EXTPRO_1:23
.= ((Result ((Q +* I),(t +* (Initialize ((intloc 0) .--> 1))))) +* (t | NAT)) . (intloc 0) by A8, FUNCT_4:12
.= (IExec (I,Q,t)) . (intloc 0) by SCMFSA6B:def 1
.= 1 by SCM_HALT:17 ;
not a in NAT by SCMFSA_2:84;
then not a in (dom t) /\ NAT by XBOOLE_0:def 4;
then A12: not a in dom (t | NAT) by RELAT_1:90;
(Comput ((Q +* (while>0 (a,I))),(t +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((Q +* I),(t +* (Initialize ((intloc 0) .--> 1))))) + 3))) . a = (Comput ((Q +* I),(t +* (Initialize ((intloc 0) .--> 1))),(LifeSpan ((Q +* I),(t +* (Initialize ((intloc 0) .--> 1))))))) . a by A10, SCMFSA6A:38
.= (Result ((Q +* I),(t +* (Initialize ((intloc 0) .--> 1))))) . a by A7, EXTPRO_1:23
.= ((Result ((Q +* I),(t +* (Initialize ((intloc 0) .--> 1))))) +* (t | NAT)) . a by A12, FUNCT_4:12
.= (IExec (I,Q,t)) . a by SCMFSA6B:def 1 ;
then (Comput ((Q +* (while>0 (a,I))),(t +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((Q +* I),(t +* (Initialize ((intloc 0) .--> 1))))) + 3))) . a < k + 1 by A1, A5;
then while>0 (a,I) is_halting_onInit Comput ((Q +* (while>0 (a,I))),(t +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((Q +* I),(t +* (Initialize ((intloc 0) .--> 1))))) + 3)),Q +* (while>0 (a,I)) by A3, INT_1:20;
then (Q +* (while>0 (a,I))) +* (while>0 (a,I)) halts_on (Comput ((Q +* (while>0 (a,I))),(t +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((Q +* I),(t +* (Initialize ((intloc 0) .--> 1))))) + 3))) +* (Initialize ((intloc 0) .--> 1)) by SCM_HALT:def 5;
then A15: (Q +* (while>0 (a,I))) +* (while>0 (a,I)) halts_on (Comput ((Q +* (while>0 (a,I))),(t +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((Q +* I),(t +* (Initialize ((intloc 0) .--> 1))))) + 3))) +* (Initialize ((intloc 0) .--> 1)) ;
A16: (Q +* (while>0 (a,I))) +* (while>0 (a,I)) = Q +* (while>0 (a,I)) by FUNCT_4:99;
IC (Comput ((Q +* (while>0 (a,I))),(t +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((Q +* I),(t +* (Initialize ((intloc 0) .--> 1))))) + 3))) = 0 by A5, A9, A6, Th21;
then A17: (Comput ((Q +* (while>0 (a,I))),(t +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((Q +* I),(t +* (Initialize ((intloc 0) .--> 1))))) + 3))) +* (Initialize ((intloc 0) .--> 1)) = Comput ((Q +* (while>0 (a,I))),(t +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((Q +* I),(t +* (Initialize ((intloc 0) .--> 1))))) + 3)) by A11, Th6;

now

consider m being Element of NAT such that
A18: CurInstr ((Q +* (while>0 (a,I))),(Comput ((Q +* (while>0 (a,I))),(Comput ((Q +* (while>0 (a,I))),(t +* (Initialize ((intloc 0) .--> 1))),((LifeSpan ((Q +* I),(t +* (Initialize ((intloc 0) .--> 1))))) + 3))),m))) = halt SCM+FSA by A17, A15, A16, EXTPRO_1:30;
take mm = ((LifeSpan ((Q +* I),(t +* (Initialize ((intloc 0) .--> 1))))) + 3) + m; :: thesis: CurInstr ((Q +* (while>0 (a,I))),(Comput ((Q +* (while>0 (a,I))),(t +* (Initialize ((intloc 0) .--> 1))),mm))) = halt SCM+FSA
thus CurInstr ((Q +* (while>0 (a,I))),(Comput ((Q +* (while>0 (a,I))),(t +* (Initialize ((intloc 0) .--> 1))),mm))) = halt SCM+FSA by A18, EXTPRO_1:5; :: thesis: verum

end;

then Q +* (while>0 (a,I)) halts_on t +* (Initialize ((intloc 0) .--> 1)) by EXTPRO_1:30;
then Q +* (while>0 (a,I)) halts_on t +* (Initialize ((intloc 0) .--> 1)) ;
hence while>0 (a,I) is_halting_onInit t,Q by SCM_HALT:def 5; :: thesis: verum

end;

end;

end;

hence S₁[k + 1] ; :: thesis: verum

end;

A19: S₁[ 0 ] by Th16;
A20: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A19, A2);

now

let t be State of SCM+FSA; :: thesis: for Q being the Instructions of SCM+FSA -valued ManySortedSet of NAT holds while>0 (a,I) is_halting_onInit Q,b₂

per cases ( t . a <= 0 or t . a > 0 ) ;

suppose t . a <= 0 ; :: thesis: for Q being the Instructions of SCM+FSA -valued ManySortedSet of NAT holds while>0 (a,I) is_halting_onInit Q,b₂

hence for Q being the Instructions of SCM+FSA -valued ManySortedSet of NAT holds while>0 (a,I) is_halting_onInit t,Q by Th16; :: thesis: verum

end;

suppose t . a > 0 ; :: thesis: for Q being the Instructions of SCM+FSA -valued ManySortedSet of NAT holds while>0 (a,I) is_halting_onInit Q,b₂

then reconsider n = t . a as Element of NAT by INT_1:16;
S₁[n] by A20;
hence for Q being the Instructions of SCM+FSA -valued ManySortedSet of NAT holds while>0 (a,I) is_halting_onInit t,Q ; :: thesis: verum

end;

end;

end;

hence while>0 (a,I) is InitHalting by SCM_HALT:36; :: thesis: verum