let I be InitHalting good 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 )
set D = Int-Locations \/ FinSeq-Locations;
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: 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: ( f . t <= k + 1 implies while>0 (a,I) is_halting_onInit b₁ )
assume A4: 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 A4, XXREAL_0:1;
hence while>0 (a,I) is_halting_onInit t by A3, INT_1:20; :: thesis: verum

end;

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

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

now

consider m being Element of NAT such that
A17: CurInstr ((ProgramPart (Comput ((ProgramPart (t +* (Initialized (while>0 (a,I))))),(t +* (Initialized (while>0 (a,I)))),((LifeSpan ((ProgramPart (t +* (Initialized I))),(t +* (Initialized I)))) + 3)))),(Comput ((ProgramPart (Comput ((ProgramPart (t +* (Initialized (while>0 (a,I))))),(t +* (Initialized (while>0 (a,I)))),((LifeSpan ((ProgramPart (t +* (Initialized I))),(t +* (Initialized I)))) + 3)))),(Comput ((ProgramPart (t +* (Initialized (while>0 (a,I))))),(t +* (Initialized (while>0 (a,I)))),((LifeSpan ((ProgramPart (t +* (Initialized I))),(t +* (Initialized I)))) + 3))),m))) = halt SCM+FSA by A16, A15, EXTPRO_1:30;
T: ProgramPart (t +* (Initialized (while>0 (a,I)))) = ProgramPart (Comput ((ProgramPart (t +* (Initialized (while>0 (a,I))))),(t +* (Initialized (while>0 (a,I)))),((LifeSpan ((ProgramPart (t +* (Initialized I))),(t +* (Initialized I)))) + 3))) by AMI_1:123;
take mm = ((LifeSpan ((ProgramPart (t +* (Initialized I))),(t +* (Initialized I)))) + 3) + m; :: thesis: CurInstr ((ProgramPart (t +* (Initialized (while>0 (a,I))))),(Comput ((ProgramPart (t +* (Initialized (while>0 (a,I))))),(t +* (Initialized (while>0 (a,I)))),mm))) = halt SCM+FSA
thus CurInstr ((ProgramPart (t +* (Initialized (while>0 (a,I))))),(Comput ((ProgramPart (t +* (Initialized (while>0 (a,I))))),(t +* (Initialized (while>0 (a,I)))),mm))) = halt SCM+FSA by A17, T, EXTPRO_1:5; :: thesis: verum

end;

then ProgramPart (t +* (Initialized (while>0 (a,I)))) halts_on t +* (Initialized (while>0 (a,I))) by EXTPRO_1:30;
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: 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;

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

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 A19;
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