set D = Int-Locations \/ FinSeq-Locations ;
let I be good InitHalting Program of SCM+FSA ; :: thesis: for a being read-write Int-Location st ex f being Function of (product the Object-Kind of SCM+FSA ),INT st
for s, t being State of SCM+FSA holds
( ( f . s > 0 implies f . (IExec I,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 (product the Object-Kind of SCM+FSA ),INT st
for s, t being State of SCM+FSA holds
( ( f . s > 0 implies f . (IExec I,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 )
given f being Function of (product the Object-Kind of SCM+FSA ),INT such that A1: for s, t being State of SCM+FSA holds
( ( f . s > 0 implies f . (IExec I,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 S₁[ Element of NAT ] means for t being State of SCM+FSA st f . t <= $1 holds
while>0 a,I is_halting_onInit t;
A2: S₁[ 0 ]

proof

let t be State of SCM+FSA ; :: thesis: ( f . t <= 0 implies while>0 a,I is_halting_onInit t )
assume f . t <= 0 ; :: thesis: while>0 a,I is_halting_onInit t
then t . a <= 0 by A1;
hence while>0 a,I is_halting_onInit t by Th16; :: thesis: verum

end;

A3: now

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

now

let t be State of SCM+FSA ; :: thesis: ( f . t <= k + 1 implies while>0 a,I is_halting_onInit b₁ )
assume A5: f . t <= k + 1 ; :: thesis: while>0 a,I is_halting_onInit b₁

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

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

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

end;

suppose A6: f . t = k + 1 ; :: thesis: while>0 a,I is_halting_onInit b₁

then A7: not t . a <= 0 by A1;
A8: I is_closed_onInit t by SCM_HALT:35;
A9: I is_halting_onInit t by SCM_HALT:36;
set Iwhile = Initialized (while>0 a,I);
set tW0 = t +* (Initialized (while>0 a,I));
set t1 = t +* (Initialized I);
set Wt = Computation (t +* (Initialized (while>0 a,I))),((LifeSpan (t +* (Initialized I))) + 3);
set A = NAT ;
set It = Computation (t +* (Initialized I)),(LifeSpan (t +* (Initialized I)));
A10: ( IC (Computation (t +* (Initialized (while>0 a,I))),((LifeSpan (t +* (Initialized I))) + 3)) = insloc 0 & DataPart (Computation (t +* (Initialized (while>0 a,I))),((LifeSpan (t +* (Initialized I))) + 3)) = DataPart (Computation (t +* (Initialized I)),(LifeSpan (t +* (Initialized I)))) ) by A7, A8, A9, Th21;
A11: t +* (Initialized I) is halting by A9, SCM_HALT:def 5;
set l0 = intloc 0 ;

now

assume intloc 0 in NAT ; :: thesis: contradiction
then reconsider l0 = intloc 0 as Instruction-Location of SCM+FSA by AMI_1:def 4;
l0 = l0 ;
hence contradiction by SCMFSA_2:84; :: thesis: verum

end;

then not intloc 0 in (dom t) /\ NAT by XBOOLE_0:def 4;
then A12: ( intloc 0 in dom (Result (t +* (Initialized I))) & not intloc 0 in dom (t | NAT ) ) by RELAT_1:90, SCMFSA_2:66;
A13: (Computation (t +* (Initialized (while>0 a,I))),((LifeSpan (t +* (Initialized I))) + 3)) . (intloc 0 ) = (Computation (t +* (Initialized I)),(LifeSpan (t +* (Initialized I)))) . (intloc 0 ) by A10, SCMFSA6A:38
.= (Result (t +* (Initialized I))) . (intloc 0 ) by A11, AMI_1:122
.= ((Result (t +* (Initialized I))) +* (t | NAT )) . (intloc 0 ) by A12, FUNCT_4:12
.= (IExec I,t) . (intloc 0 ) by SCMFSA6B:def 1
.= 1 by SCM_HALT:17 ;
A14: Initialized (while>0 a,I) c= t +* (Initialized (while>0 a,I)) by FUNCT_4:26;
while>0 a,I c= Initialized (while>0 a,I) by SCMFSA6A:26;
then while>0 a,I c= t +* (Initialized (while>0 a,I)) by A14, XBOOLE_1:1;
then while>0 a,I c= Computation (t +* (Initialized (while>0 a,I))),((LifeSpan (t +* (Initialized I))) + 3) by AMI_1:81;
then (Computation (t +* (Initialized (while>0 a,I))),((LifeSpan (t +* (Initialized I))) + 3)) +* (while>0 a,I) = Computation (t +* (Initialized (while>0 a,I))),((LifeSpan (t +* (Initialized I))) + 3) by FUNCT_4:79;
then A15: (Computation (t +* (Initialized (while>0 a,I))),((LifeSpan (t +* (Initialized I))) + 3)) +* (Initialized (while>0 a,I)) = Computation (t +* (Initialized (while>0 a,I))),((LifeSpan (t +* (Initialized I))) + 3) by A10, A13, Th6;
DataPart (Computation (t +* (Initialized (while>0 a,I))),((LifeSpan (t +* (Initialized I))) + 3)) = DataPart (Result (t +* (Initialized I))) by A10, A11, AMI_1:122
.= DataPart ((Result (t +* (Initialized I))) +* (t | NAT )) by SCMFSA8C:35
.= DataPart (IExec I,t) by SCMFSA6B:def 1 ;
then f . (Computation (t +* (Initialized (while>0 a,I))),((LifeSpan (t +* (Initialized I))) + 3)) = f . (IExec I,t) by A1;
then f . (Computation (t +* (Initialized (while>0 a,I))),((LifeSpan (t +* (Initialized I))) + 3)) < k + 1 by A1, A6;
then while>0 a,I is_halting_onInit Computation (t +* (Initialized (while>0 a,I))),((LifeSpan (t +* (Initialized I))) + 3) by A4, INT_1:20;
then A16: (Computation (t +* (Initialized (while>0 a,I))),((LifeSpan (t +* (Initialized I))) + 3)) +* (Initialized (while>0 a,I)) is halting by SCM_HALT:def 5;

now

consider m being Element of NAT such that
A17: CurInstr (Computation (Computation (t +* (Initialized (while>0 a,I))),((LifeSpan (t +* (Initialized I))) + 3)),m) = halt SCM+FSA by A15, A16, AMI_1:def 20;
take mm = ((LifeSpan (t +* (Initialized I))) + 3) + m; :: thesis: CurInstr (Computation (t +* (Initialized (while>0 a,I))),mm) = halt SCM+FSA
thus CurInstr (Computation (t +* (Initialized (while>0 a,I))),mm) = halt SCM+FSA by A17, AMI_1:51; :: thesis: verum

end;

then t +* (Initialized (while>0 a,I)) is halting by AMI_1:def 20;
hence while>0 a,I is_halting_onInit t by SCM_HALT:def 5; :: thesis: verum

end;

end;

end;

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

end;

A18: for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A2, A3);

now

let t be State of SCM+FSA ; :: thesis: while>0 a,I is_halting_onInit b₁

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

suppose f . t <= 0 ; :: thesis: while>0 a,I is_halting_onInit b₁

then t . a <= 0 by A1;
hence while>0 a,I is_halting_onInit t by Th16; :: thesis: verum

end;

suppose f . t > 0 ; :: thesis: while>0 a,I is_halting_onInit b₁

then reconsider n = f . t as Element of NAT by INT_1:16;
S₁[n] by A18;
hence while>0 a,I is_halting_onInit t ; :: thesis: verum

end;

end;

end;

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