let P be Instruction-Sequence of SCM+FSA; :: thesis: for I being really-closed MacroInstruction of SCM+FSA
for s being State of SCM+FSA st ex f being Function of ,NAT st
for k being Nat holds
( ( f . ((StepWhile>0 (a,P,s,I)) . k) <> 0 implies ( f . ((StepWhile>0 (a,P,s,I)) . (k + 1)) < f . ((StepWhile>0 (a,P,s,I)) . k) & I is_halting_onInit (StepWhile>0 (a,P,s,I)) . k,P +* (while>0 (a,I)) ) ) & ((StepWhile>0 (a,P,s,I)) . (k + 1)) . () = 1 & ( f . ((StepWhile>0 (a,P,s,I)) . k) = 0 implies ((StepWhile>0 (a,P,s,I)) . k) . a <= 0 ) & ( ((StepWhile>0 (a,P,s,I)) . k) . a <= 0 implies f . ((StepWhile>0 (a,P,s,I)) . k) = 0 ) ) holds
while>0 (a,I) is_halting_onInit 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 ex f being Function of ,NAT st
for k being Nat holds
( ( f . ((StepWhile>0 (a,P,s,I)) . k) <> 0 implies ( f . ((StepWhile>0 (a,P,s,I)) . (k + 1)) < f . ((StepWhile>0 (a,P,s,I)) . k) & I is_halting_onInit (StepWhile>0 (a,P,s,I)) . k,P +* (while>0 (a,I)) ) ) & ((StepWhile>0 (a,P,s,I)) . (k + 1)) . () = 1 & ( f . ((StepWhile>0 (a,P,s,I)) . k) = 0 implies ((StepWhile>0 (a,P,s,I)) . k) . a <= 0 ) & ( ((StepWhile>0 (a,P,s,I)) . k) . a <= 0 implies f . ((StepWhile>0 (a,P,s,I)) . k) = 0 ) ) holds
while>0 (a,I) is_halting_onInit s,P

let a be read-write Int-Location; :: thesis: for s being State of SCM+FSA st ex f being Function of ,NAT st
for k being Nat holds
( ( f . ((StepWhile>0 (a,P,s,I)) . k) <> 0 implies ( f . ((StepWhile>0 (a,P,s,I)) . (k + 1)) < f . ((StepWhile>0 (a,P,s,I)) . k) & I is_halting_onInit (StepWhile>0 (a,P,s,I)) . k,P +* (while>0 (a,I)) ) ) & ((StepWhile>0 (a,P,s,I)) . (k + 1)) . () = 1 & ( f . ((StepWhile>0 (a,P,s,I)) . k) = 0 implies ((StepWhile>0 (a,P,s,I)) . k) . a <= 0 ) & ( ((StepWhile>0 (a,P,s,I)) . k) . a <= 0 implies f . ((StepWhile>0 (a,P,s,I)) . k) = 0 ) ) holds
while>0 (a,I) is_halting_onInit s,P

let s be State of SCM+FSA; :: thesis: ( ex f being Function of ,NAT st
for k being Nat holds
( ( f . ((StepWhile>0 (a,P,s,I)) . k) <> 0 implies ( f . ((StepWhile>0 (a,P,s,I)) . (k + 1)) < f . ((StepWhile>0 (a,P,s,I)) . k) & I is_halting_onInit (StepWhile>0 (a,P,s,I)) . k,P +* (while>0 (a,I)) ) ) & ((StepWhile>0 (a,P,s,I)) . (k + 1)) . () = 1 & ( f . ((StepWhile>0 (a,P,s,I)) . k) = 0 implies ((StepWhile>0 (a,P,s,I)) . k) . a <= 0 ) & ( ((StepWhile>0 (a,P,s,I)) . k) . a <= 0 implies f . ((StepWhile>0 (a,P,s,I)) . k) = 0 ) ) implies while>0 (a,I) is_halting_onInit s,P )

set D = Data-Locations ;
given f being Function of ,NAT such that A1: for k being Nat holds
( ( f . ((StepWhile>0 (a,P,s,I)) . k) <> 0 implies ( f . ((StepWhile>0 (a,P,s,I)) . (k + 1)) < f . ((StepWhile>0 (a,P,s,I)) . k) & I is_halting_onInit (StepWhile>0 (a,P,s,I)) . k,P +* (while>0 (a,I)) ) ) & ((StepWhile>0 (a,P,s,I)) . (k + 1)) . () = 1 & ( f . ((StepWhile>0 (a,P,s,I)) . k) = 0 implies ((StepWhile>0 (a,P,s,I)) . k) . a <= 0 ) & ( ((StepWhile>0 (a,P,s,I)) . k) . a <= 0 implies f . ((StepWhile>0 (a,P,s,I)) . k) = 0 ) ) ; :: thesis: while>0 (a,I) is_halting_onInit s,P
set s1 = Initialized s;
set P1 = P +* (while>0 (a,I));
A2: (P +* (while>0 (a,I))) +* (while>0 (a,I)) = P +* (while>0 (a,I)) ;
deffunc H1( Nat) -> Element of NAT = f . ((StepWhile>0 (a,P,s,I)) . \$1);
A3: for k being Nat holds
( H1(k + 1) < H1(k) or H1(k) = 0 ) by A1;
consider m being Nat such that
A4: H1(m) = 0 and
A5: for n being Nat st H1(n) = 0 holds
m <= n from reconsider m = m as Nat ;
defpred S1[ Nat] means ( \$1 + 1 <= m implies ex k being Nat st (StepWhile>0 (a,P,s,I)) . (\$1 + 1) = Comput ((P +* (while>0 (a,I))),(),k) );
A6: S1[ 0 ]
proof
assume 0 + 1 <= m ; :: thesis: ex k being Nat st (StepWhile>0 (a,P,s,I)) . (0 + 1) = Comput ((P +* (while>0 (a,I))),(),k)
take n = (LifeSpan (((P +* (while>0 (a,I))) +* I),())) + 2; :: thesis: (StepWhile>0 (a,P,s,I)) . (0 + 1) = Comput ((P +* (while>0 (a,I))),(),n)
thus (StepWhile>0 (a,P,s,I)) . (0 + 1) = Comput ((P +* (while>0 (a,I))),(),n) by Th8; :: thesis: verum
end;
A7: now :: thesis: for i being Nat st i < m holds
I is_halting_onInit (StepWhile>0 (a,P,s,I)) . i,P +* (while>0 (a,I))
let i be Nat; :: thesis: ( i < m implies I is_halting_onInit (StepWhile>0 (a,P,s,I)) . i,P +* (while>0 (a,I)) )
assume i < m ; :: thesis: I is_halting_onInit (StepWhile>0 (a,P,s,I)) . i,P +* (while>0 (a,I))
then H1(i) <> 0 by A5;
hence I is_halting_onInit (StepWhile>0 (a,P,s,I)) . i,P +* (while>0 (a,I)) by A1; :: thesis: verum
end;
A8: now :: thesis: for k being Nat st S1[k] holds
S1[k + 1]
let k be Nat; :: thesis: ( S1[k] implies S1[k + 1] )
assume A9: S1[k] ; :: thesis: S1[k + 1]
now :: thesis: ( (k + 1) + 1 <= m implies ex m being Element of NAT st (StepWhile>0 (a,P,s,I)) . ((k + 1) + 1) = Comput ((P +* (while>0 (a,I))),(),m) )
set sk = (StepWhile>0 (a,P,s,I)) . k;
set sk1 = (StepWhile>0 (a,P,s,I)) . (k + 1);
assume A10: (k + 1) + 1 <= m ; :: thesis: ex m being Element of NAT st (StepWhile>0 (a,P,s,I)) . ((k + 1) + 1) = Comput ((P +* (while>0 (a,I))),(),m)
(k + 1) + 0 < (k + 1) + 1 by XREAL_1:6;
then consider n being Nat such that
A11: (StepWhile>0 (a,P,s,I)) . (k + 1) = Comput ((P +* (while>0 (a,I))),(),n) by ;
A12: ((StepWhile>0 (a,P,s,I)) . (k + 1)) . () = 1 by A1;
k + 0 < k + (1 + 1) by XREAL_1:6;
then A13: k < m by ;
then A14: I is_halting_onInit (StepWhile>0 (a,P,s,I)) . k,P +* (while>0 (a,I)) by A7;
H1(k) <> 0 by ;
then A15: ((StepWhile>0 (a,P,s,I)) . k) . a > 0 by A1;
take m = n + ((LifeSpan (((P +* (while>0 (a,I))) +* I),(Initialized ((StepWhile>0 (a,P,s,I)) . (k + 1))))) + 2); :: thesis: (StepWhile>0 (a,P,s,I)) . ((k + 1) + 1) = Comput ((P +* (while>0 (a,I))),(),m)
A16: (P +* (while>0 (a,I))) +* (while>0 (a,I)) = P +* (while>0 (a,I)) ;
A17: (StepWhile>0 (a,P,s,I)) . (k + 1) = Comput ((P +* (while>0 (a,I))),(Initialized ((StepWhile>0 (a,P,s,I)) . k)),((LifeSpan (((P +* (while>0 (a,I))) +* I),(Initialized ((StepWhile>0 (a,P,s,I)) . k)))) + 2)) by Def1;
IC ((StepWhile>0 (a,P,s,I)) . (k + 1)) = 0 by A17, A14, A15, Th4, A16;
then (StepWhile>0 (a,P,s,I)) . ((k + 1) + 1) = Comput ((P +* (while>0 (a,I))),(),(n + ((LifeSpan (((P +* (while>0 (a,I))) +* I),(Initialized ((StepWhile>0 (a,P,s,I)) . (k + 1))))) + 2))) by ;
hence (StepWhile>0 (a,P,s,I)) . ((k + 1) + 1) = Comput ((P +* (while>0 (a,I))),(),m) ; :: thesis: verum
end;
hence S1[k + 1] ; :: thesis: verum
end;
A18: for k being Nat holds S1[k] from NAT_1:sch 2(A6, A8);
per cases ( m = 0 or m <> 0 ) ;
suppose m = 0 ; :: thesis: while>0 (a,I) is_halting_onInit s,P
then ((StepWhile>0 (a,P,s,I)) . 0) . a <= 0 by A1, A4;
then s . a <= 0 by Def1;
hence while>0 (a,I) is_halting_onInit s,P by SCM_HALT:73; :: thesis: verum
end;
suppose m <> 0 ; :: thesis: while>0 (a,I) is_halting_onInit s,P
then consider i being Nat such that
A19: m = i + 1 by NAT_1:6;
reconsider i = i as Nat ;
set si = (StepWhile>0 (a,P,s,I)) . i;
set sm = (StepWhile>0 (a,P,s,I)) . m;
set sm1 = Initialized ((StepWhile>0 (a,P,s,I)) . m);
set sm2 = Initialize ((StepWhile>0 (a,P,s,I)) . m);
A20: i < m by ;
i < m by ;
then H1(i) <> 0 by A5;
then A21: ((StepWhile>0 (a,P,s,I)) . i) . a > 0 by A1;
A22: I is_halting_onInit (StepWhile>0 (a,P,s,I)) . i,P +* (while>0 (a,I)) by ;
(StepWhile>0 (a,P,s,I)) . m = Comput ((P +* (while>0 (a,I))),(Initialized ((StepWhile>0 (a,P,s,I)) . i)),((LifeSpan (((P +* (while>0 (a,I))) +* I),(Initialized ((StepWhile>0 (a,P,s,I)) . i)))) + 2)) by ;
then IC ((StepWhile>0 (a,P,s,I)) . m) = 0 by A22, A21, Th4, A2;
then A23: Start-At (0,SCM+FSA) c= (StepWhile>0 (a,P,s,I)) . m by MEMSTR_0:30;
((StepWhile>0 (a,P,s,I)) . (i + 1)) . () = 1 by A1;
then A24: Initialized ((StepWhile>0 (a,P,s,I)) . m) = Initialize ((StepWhile>0 (a,P,s,I)) . m) by ;
set p = (LifeSpan (((P +* (while>0 (a,I))) +* I),())) + 3;
m = i + 1 by A19;
then consider n being Nat such that
A25: (StepWhile>0 (a,P,s,I)) . m = Comput ((P +* (while>0 (a,I))),(),n) by A18;
A26: Initialized ((StepWhile>0 (a,P,s,I)) . m) = (StepWhile>0 (a,P,s,I)) . m by ;
((StepWhile>0 (a,P,s,I)) . m) . a <= 0 by A1, A4;
then while>0 (a,I) is_halting_onInit (StepWhile>0 (a,P,s,I)) . m,P +* (while>0 (a,I)) by SCM_HALT:73;
then P +* (while>0 (a,I)) halts_on Initialized ((StepWhile>0 (a,P,s,I)) . m) ;
then consider j being Nat such that
A27: CurInstr ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),((StepWhile>0 (a,P,s,I)) . m),j))) = halt SCM+FSA by A26;
A28: Comput ((P +* (while>0 (a,I))),(),(j + n)) = Comput ((P +* (while>0 (a,I))),(Comput ((P +* (while>0 (a,I))),(),n)),j) by EXTPRO_1:4;
P +* (while>0 (a,I)) halts_on Initialized s by ;
hence while>0 (a,I) is_halting_onInit s,P ; :: thesis: verum
end;
end;