let I be good InitHalting Program of SCM+FSA ; :: thesis: for a being read-write Int-Location st ( for s being State of SCM+FSA st s . a > 0 holds
(IExec I,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 st s . a > 0 holds
(IExec I,s) . a < s . a ) implies while>0 a,I is InitHalting )
set D = Int-Locations \/ FinSeq-Locations ;
defpred S₁[ Element of NAT ] means for t being State of SCM+FSA st t . a <= $1 holds
while>0 a,I is_halting_onInit t;
assume A1: for s being State of SCM+FSA st s . a > 0 holds
(IExec I,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: ( t . a <= k + 1 implies while>0 a,I is_halting_onInit b₁ )
assume A4: t . a <= k + 1 ; :: thesis: while>0 a,I is_halting_onInit 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₁

then t . a < 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: t . a = 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 (t +* (Initialized I))) + 3);
set A = NAT ;
set It = Comput (ProgramPart (t +* (Initialized I))),(t +* (Initialized I)),(LifeSpan (t +* (Initialized I)));
A6: I is_halting_onInit t by SCM_HALT:36;
then A7: ProgramPart (t +* (Initialized I)) halts_on t +* (Initialized I) by SCM_HALT:def 5;
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 by SCM_HALT:35;
then A10: DataPart (Comput (ProgramPart (t +* (Initialized (while>0 a,I)))),(t +* (Initialized (while>0 a,I))),((LifeSpan (t +* (Initialized I))) + 3)) = DataPart (Comput (ProgramPart (t +* (Initialized I))),(t +* (Initialized I)),(LifeSpan (t +* (Initialized I)))) by A5, A6, Th21;
then A11: (Comput (ProgramPart (t +* (Initialized (while>0 a,I)))),(t +* (Initialized (while>0 a,I))),((LifeSpan (t +* (Initialized I))) + 3)) . (intloc 0 ) = (Comput (ProgramPart (t +* (Initialized I))),(t +* (Initialized I)),(LifeSpan (t +* (Initialized I)))) . (intloc 0 ) by SCMFSA6A:38
.= (Result (t +* (Initialized I))) . (intloc 0 ) by A7, AMI_1:122
.= ((Result (t +* (Initialized I))) +* (t | NAT )) . (intloc 0 ) by A8, FUNCT_4:12
.= (IExec I,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;
A13: 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 A13, XBOOLE_1:1;
then while>0 a,I c= Comput (ProgramPart (t +* (Initialized (while>0 a,I)))),(t +* (Initialized (while>0 a,I))),((LifeSpan (t +* (Initialized I))) + 3) by AMI_1:81;
then A14: (Comput (ProgramPart (t +* (Initialized (while>0 a,I)))),(t +* (Initialized (while>0 a,I))),((LifeSpan (t +* (Initialized I))) + 3)) +* (while>0 a,I) = Comput (ProgramPart (t +* (Initialized (while>0 a,I)))),(t +* (Initialized (while>0 a,I))),((LifeSpan (t +* (Initialized I))) + 3) by FUNCT_4:79;
(Comput (ProgramPart (t +* (Initialized (while>0 a,I)))),(t +* (Initialized (while>0 a,I))),((LifeSpan (t +* (Initialized I))) + 3)) . a = (Comput (ProgramPart (t +* (Initialized I))),(t +* (Initialized I)),(LifeSpan (t +* (Initialized I)))) . a by A10, SCMFSA6A:38
.= (Result (t +* (Initialized I))) . a by A7, AMI_1:122
.= ((Result (t +* (Initialized I))) +* (t | NAT )) . a by A12, FUNCT_4:12
.= (IExec I,t) . a by SCMFSA6B:def 1 ;
then (Comput (ProgramPart (t +* (Initialized (while>0 a,I)))),(t +* (Initialized (while>0 a,I))),((LifeSpan (t +* (Initialized I))) + 3)) . a < 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 (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 (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 (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 (t +* (Initialized I))) + 3)) = 0 by A5, A9, A6, Th21;
then A16: (Comput (ProgramPart (t +* (Initialized (while>0 a,I)))),(t +* (Initialized (while>0 a,I))),((LifeSpan (t +* (Initialized I))) + 3)) +* (Initialized (while>0 a,I)) = Comput (ProgramPart (t +* (Initialized (while>0 a,I)))),(t +* (Initialized (while>0 a,I))),((LifeSpan (t +* (Initialized I))) + 3) by A11, A14, Th6;

now

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

end;

then ProgramPart (t +* (Initialized (while>0 a,I))) halts_on t +* (Initialized (while>0 a,I)) by AMI_1:146;
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 ] by Th16;
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 ( t . a <= 0 or t . a > 0 ) ;

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

hence while>0 a,I is_halting_onInit t by Th16; :: thesis: verum

end;

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

then reconsider n = t . a 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