let P be Instruction-Sequence of SCM+FSA; :: thesis: for I being really-closed MacroInstruction of SCM+FSA
for a being read-write Int-Location
for s being State of SCM+FSA st ( for k being Nat holds I is_halting_on (StepWhile=0 (a,I,P,s)) . k,P +* (while=0 (a,I)) ) & ex f being Function of (product (the_Values_of SCM+FSA)),NAT st
for k being Nat holds
( ( f . ((StepWhile=0 (a,I,P,s)) . (k + 1)) < f . ((StepWhile=0 (a,I,P,s)) . k) or f . ((StepWhile=0 (a,I,P,s)) . k) = 0 ) & ( f . ((StepWhile=0 (a,I,P,s)) . k) = 0 implies ((StepWhile=0 (a,I,P,s)) . k) . a <> 0 ) & ( ((StepWhile=0 (a,I,P,s)) . k) . a <> 0 implies f . ((StepWhile=0 (a,I,P,s)) . k) = 0 ) ) holds
while=0 (a,I) is_halting_on s,P
let I be really-closed MacroInstruction of SCM+FSA ; :: thesis: for a being read-write Int-Location
for s being State of SCM+FSA st ( for k being Nat holds I is_halting_on (StepWhile=0 (a,I,P,s)) . k,P +* (while=0 (a,I)) ) & ex f being Function of (product (the_Values_of SCM+FSA)),NAT st
for k being Nat holds
( ( f . ((StepWhile=0 (a,I,P,s)) . (k + 1)) < f . ((StepWhile=0 (a,I,P,s)) . k) or f . ((StepWhile=0 (a,I,P,s)) . k) = 0 ) & ( f . ((StepWhile=0 (a,I,P,s)) . k) = 0 implies ((StepWhile=0 (a,I,P,s)) . k) . a <> 0 ) & ( ((StepWhile=0 (a,I,P,s)) . k) . a <> 0 implies f . ((StepWhile=0 (a,I,P,s)) . k) = 0 ) ) holds
while=0 (a,I) is_halting_on s,P
let a be read-write Int-Location; :: thesis: for s being State of SCM+FSA st ( for k being Nat holds I is_halting_on (StepWhile=0 (a,I,P,s)) . k,P +* (while=0 (a,I)) ) & ex f being Function of (product (the_Values_of SCM+FSA)),NAT st
for k being Nat holds
( ( f . ((StepWhile=0 (a,I,P,s)) . (k + 1)) < f . ((StepWhile=0 (a,I,P,s)) . k) or f . ((StepWhile=0 (a,I,P,s)) . k) = 0 ) & ( f . ((StepWhile=0 (a,I,P,s)) . k) = 0 implies ((StepWhile=0 (a,I,P,s)) . k) . a <> 0 ) & ( ((StepWhile=0 (a,I,P,s)) . k) . a <> 0 implies f . ((StepWhile=0 (a,I,P,s)) . k) = 0 ) ) holds
while=0 (a,I) is_halting_on s,P
let s be State of SCM+FSA; :: thesis: ( ( for k being Nat holds I is_halting_on (StepWhile=0 (a,I,P,s)) . k,P +* (while=0 (a,I)) ) & ex f being Function of (product (the_Values_of SCM+FSA)),NAT st
for k being Nat holds
( ( f . ((StepWhile=0 (a,I,P,s)) . (k + 1)) < f . ((StepWhile=0 (a,I,P,s)) . k) or f . ((StepWhile=0 (a,I,P,s)) . k) = 0 ) & ( f . ((StepWhile=0 (a,I,P,s)) . k) = 0 implies ((StepWhile=0 (a,I,P,s)) . k) . a <> 0 ) & ( ((StepWhile=0 (a,I,P,s)) . k) . a <> 0 implies f . ((StepWhile=0 (a,I,P,s)) . k) = 0 ) ) implies while=0 (a,I) is_halting_on s,P )
assume A1: for k being Nat holds I is_halting_on (StepWhile=0 (a,I,P,s)) . k,P +* (while=0 (a,I)) ; :: thesis: ( for f being Function of (product (the_Values_of SCM+FSA)),NAT holds
not for k being Nat holds
( ( f . ((StepWhile=0 (a,I,P,s)) . (k + 1)) < f . ((StepWhile=0 (a,I,P,s)) . k) or f . ((StepWhile=0 (a,I,P,s)) . k) = 0 ) & ( f . ((StepWhile=0 (a,I,P,s)) . k) = 0 implies ((StepWhile=0 (a,I,P,s)) . k) . a <> 0 ) & ( ((StepWhile=0 (a,I,P,s)) . k) . a <> 0 implies f . ((StepWhile=0 (a,I,P,s)) . k) = 0 ) ) or while=0 (a,I) is_halting_on s,P )
set s1 = Initialize s;
set P1 = P +* (while=0 (a,I));
A2: (P +* (while=0 (a,I))) +* (while=0 (a,I)) = P +* (while=0 (a,I)) ;
given f being Function of (product (the_Values_of SCM+FSA)),NAT such that A3: for k being Nat holds
( ( f . ((StepWhile=0 (a,I,P,s)) . (k + 1)) < f . ((StepWhile=0 (a,I,P,s)) . k) or f . ((StepWhile=0 (a,I,P,s)) . k) = 0 ) & ( f . ((StepWhile=0 (a,I,P,s)) . k) = 0 implies ((StepWhile=0 (a,I,P,s)) . k) . a <> 0 ) & ( ((StepWhile=0 (a,I,P,s)) . k) . a <> 0 implies f . ((StepWhile=0 (a,I,P,s)) . k) = 0 ) ) ; :: thesis: while=0 (a,I) is_halting_on s,P
deffunc H₁( Nat) -> Element of NAT = f . ((StepWhile=0 (a,I,P,s)) . $1);
A4: for k being Nat holds
( H₁(k + 1) < H₁(k) or H₁(k) = 0 ) by A3;
consider m being Nat such that
A5: H₁(m) = 0 and
A6: for n being Nat st H₁(n) = 0 holds
m <= n from NAT_1:sch 17(A4);
defpred S₁[ Nat] means ( $1 + 1 <= m implies ex k being Nat st (StepWhile=0 (a,I,P,s)) . ($1 + 1) = Comput ((P +* (while=0 (a,I))),(Initialize s),k) );

A7: now :: thesis: for k being Nat st S₁[k] holds
S₁[k + 1]

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A8: S₁[k] ; :: thesis: S₁[k + 1]

now :: thesis: ( (k + 1) + 1 <= m implies ex m being Element of NAT st (StepWhile=0 (a,I,P,s)) . ((k + 1) + 1) = Comput ((P +* (while=0 (a,I))),(Initialize s),m) )

set sk1 = (StepWhile=0 (a,I,P,s)) . (k + 1);
set sk = (StepWhile=0 (a,I,P,s)) . k;
assume A9: (k + 1) + 1 <= m ; :: thesis: ex m being Element of NAT st (StepWhile=0 (a,I,P,s)) . ((k + 1) + 1) = Comput ((P +* (while=0 (a,I))),(Initialize s),m)
k + 0 < k + (1 + 1) by XREAL_1:6;
then k < m by A9, XXREAL_0:2;
then H₁(k) <> 0 by A6;
then A10: ((StepWhile=0 (a,I,P,s)) . k) . a = 0 by A3;
A11: I is_halting_on (StepWhile=0 (a,I,P,s)) . k,P +* (while=0 (a,I)) by A1;
(k + 1) + 0 < (k + 1) + 1 by XREAL_1:6;
then consider n being Nat such that
A12: (StepWhile=0 (a,I,P,s)) . (k + 1) = Comput ((P +* (while=0 (a,I))),(Initialize s),n) by A8, A9, XXREAL_0:2;
take m = n + ((LifeSpan (((P +* (while=0 (a,I))) +* I),(Initialize ((StepWhile=0 (a,I,P,s)) . (k + 1))))) + 2); :: thesis: (StepWhile=0 (a,I,P,s)) . ((k + 1) + 1) = Comput ((P +* (while=0 (a,I))),(Initialize s),m)
A13: (P +* (while=0 (a,I))) +* (while=0 (a,I)) = P +* (while=0 (a,I)) ;
(StepWhile=0 (a,I,P,s)) . (k + 1) = Comput ((P +* (while=0 (a,I))),(Initialize ((StepWhile=0 (a,I,P,s)) . k)),((LifeSpan (((P +* (while=0 (a,I))) +* I),(Initialize ((StepWhile=0 (a,I,P,s)) . k)))) + 2)) by Def1;
then IC ((StepWhile=0 (a,I,P,s)) . (k + 1)) = 0 by A11, A10, Th4, A13;
hence (StepWhile=0 (a,I,P,s)) . ((k + 1) + 1) = Comput ((P +* (while=0 (a,I))),(Initialize s),m) by A12, Th7; :: thesis: verum

end;

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

end;

A14: S₁[ 0 ]

proof

assume 0 + 1 <= m ; :: thesis: ex k being Nat st (StepWhile=0 (a,I,P,s)) . (0 + 1) = Comput ((P +* (while=0 (a,I))),(Initialize s),k)
take n = (LifeSpan (((P +* (while=0 (a,I))) +* I),(Initialize s))) + 2; :: thesis: (StepWhile=0 (a,I,P,s)) . (0 + 1) = Comput ((P +* (while=0 (a,I))),(Initialize s),n)
thus (StepWhile=0 (a,I,P,s)) . (0 + 1) = Comput ((P +* (while=0 (a,I))),(Initialize s),n) by Th6; :: thesis: verum

end;

A15: for k being Nat holds S₁[k] from NAT_1:sch 2(A14, A7);

now :: thesis: while=0 (a,I) is_halting_on s,P

per cases ( m = 0 or m <> 0 ) ;

suppose m = 0 ; :: thesis: while=0 (a,I) is_halting_on s,P

then ((StepWhile=0 (a,I,P,s)) . 0) . a <> 0 by A3, A5;
then s . a <> 0 by Def1;
hence while=0 (a,I) is_halting_on s,P by Th1; :: thesis: verum

end;

suppose m <> 0 ; :: thesis: while=0 (a,I) is_halting_on s,P

then consider i being Nat such that
A16: m = i + 1 by NAT_1:6;
reconsider m = m, i = i as Element of NAT by ORDINAL1:def 12;
set sm = (StepWhile=0 (a,I,P,s)) . m;
set si = (StepWhile=0 (a,I,P,s)) . i;
i < m by A16, NAT_1:13;
then H₁(i) <> 0 by A6;
then A17: ((StepWhile=0 (a,I,P,s)) . i) . a = 0 by A3;
A18: I is_halting_on (StepWhile=0 (a,I,P,s)) . i,P +* (while=0 (a,I)) by A1;
(StepWhile=0 (a,I,P,s)) . m = Comput ((P +* (while=0 (a,I))),(Initialize ((StepWhile=0 (a,I,P,s)) . i)),((LifeSpan (((P +* (while=0 (a,I))) +* I),(Initialize ((StepWhile=0 (a,I,P,s)) . i)))) + 2)) by A16, Def1;
then (StepWhile=0 (a,I,P,s)) . m is 0 -started by A18, A17, Th4, A2;
then A19: Start-At (0,SCM+FSA) c= (StepWhile=0 (a,I,P,s)) . m by MEMSTR_0:29;
set p = (LifeSpan (((P +* (while=0 (a,I))) +* I),(Initialize s))) + 3;
set sm1 = Initialize ((StepWhile=0 (a,I,P,s)) . m);
consider n being Nat such that
A20: (StepWhile=0 (a,I,P,s)) . m = Comput ((P +* (while=0 (a,I))),(Initialize s),n) by A15, A16;
A21: Initialize ((StepWhile=0 (a,I,P,s)) . m) = (StepWhile=0 (a,I,P,s)) . m by A19, FUNCT_4:98;
((StepWhile=0 (a,I,P,s)) . m) . a <> 0 by A3, A5;
then while=0 (a,I) is_halting_on (StepWhile=0 (a,I,P,s)) . m,P by Th1;
then P +* (while=0 (a,I)) halts_on Initialize ((StepWhile=0 (a,I,P,s)) . m) by SCMFSA7B:def 7;
then P +* (while=0 (a,I)) halts_on Initialize ((StepWhile=0 (a,I,P,s)) . m) ;
then P +* (while=0 (a,I)) halts_on Initialize ((StepWhile=0 (a,I,P,s)) . m) ;
then consider j being Nat such that
A22: CurInstr ((P +* (while=0 (a,I))),(Comput ((P +* (while=0 (a,I))),((StepWhile=0 (a,I,P,s)) . m),j))) = halt SCM+FSA by A21;
A23: Comput ((P +* (while=0 (a,I))),(Initialize s),(n + j)) = Comput ((P +* (while=0 (a,I))),(Comput ((P +* (while=0 (a,I))),(Initialize s),n)),j) by EXTPRO_1:4;
CurInstr ((P +* (while=0 (a,I))),(Comput ((P +* (while=0 (a,I))),(Initialize s),(n + j)))) = halt SCM+FSA by A20, A22, A23;
then P +* (while=0 (a,I)) halts_on Initialize s by EXTPRO_1:29;
hence while=0 (a,I) is_halting_on s,P by SCMFSA7B:def 7; :: thesis: verum

end;

end;

end;

hence while=0 (a,I) is_halting_on s,P ; :: thesis: verum