let P be Instruction-Sequence of SCM+FSA; for I being really-closed MacroInstruction of SCM+FSA
for a being read-write Int-Location
for s being State of SCM+FSA st ex f being Function of (product (the_Values_of SCM+FSA)),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)) . (intloc 0) = 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 ; for a being read-write Int-Location
for s being State of SCM+FSA st ex f being Function of (product (the_Values_of SCM+FSA)),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)) . (intloc 0) = 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; for s being State of SCM+FSA st ex f being Function of (product (the_Values_of SCM+FSA)),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)) . (intloc 0) = 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; ( ex f being Function of (product (the_Values_of SCM+FSA)),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)) . (intloc 0) = 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 (product (the_Values_of SCM+FSA)),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)) . (intloc 0) = 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 ) )
; 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 NAT_1:sch 17(A3);
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))),(Initialized s),k) );
A6:
S1[ 0 ]
proof
assume
0 + 1
<= m
;
ex k being Nat st (StepWhile>0 (a,P,s,I)) . (0 + 1) = Comput ((P +* (while>0 (a,I))),(Initialized s),k)
take n =
(LifeSpan (((P +* (while>0 (a,I))) +* I),(Initialized s))) + 2;
(StepWhile>0 (a,P,s,I)) . (0 + 1) = Comput ((P +* (while>0 (a,I))),(Initialized s),n)
thus
(StepWhile>0 (a,P,s,I)) . (0 + 1) = Comput (
(P +* (while>0 (a,I))),
(Initialized s),
n)
by Th8;
verum
end;
A7:
now 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;
( i < m implies I is_halting_onInit (StepWhile>0 (a,P,s,I)) . i,P +* (while>0 (a,I)) )assume
i < m
;
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;
verum end;
A8:
now for k being Nat st S1[k] holds
S1[k + 1]let k be
Nat;
( S1[k] implies S1[k + 1] )assume A9:
S1[
k]
;
S1[k + 1]now ( (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))),(Initialized s),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
;
ex m being Element of NAT st (StepWhile>0 (a,P,s,I)) . ((k + 1) + 1) = Comput ((P +* (while>0 (a,I))),(Initialized s),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))),
(Initialized s),
n)
by A9, A10, XXREAL_0:2;
A12:
((StepWhile>0 (a,P,s,I)) . (k + 1)) . (intloc 0) = 1
by A1;
k + 0 < k + (1 + 1)
by XREAL_1:6;
then A13:
k < m
by A10, XXREAL_0:2;
then A14:
I is_halting_onInit (StepWhile>0 (a,P,s,I)) . k,
P +* (while>0 (a,I))
by A7;
H1(
k)
<> 0
by A5, A13;
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);
(StepWhile>0 (a,P,s,I)) . ((k + 1) + 1) = Comput ((P +* (while>0 (a,I))),(Initialized s),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))),
(Initialized s),
(n + ((LifeSpan (((P +* (while>0 (a,I))) +* I),(Initialized ((StepWhile>0 (a,P,s,I)) . (k + 1))))) + 2)))
by A11, A12, Th9;
hence
(StepWhile>0 (a,P,s,I)) . ((k + 1) + 1) = Comput (
(P +* (while>0 (a,I))),
(Initialized s),
m)
;
verum end; hence
S1[
k + 1]
;
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
;
while>0 (a,I) is_halting_onInit s,Pthen 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 A19, XREAL_1:29;
i < m
by A19, NAT_1:13;
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 A7, A20;
(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 A19, Def1;
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)) . (intloc 0) = 1
by A1;
then A24:
Initialized ((StepWhile>0 (a,P,s,I)) . m) = Initialize ((StepWhile>0 (a,P,s,I)) . m)
by A19, SCMFSA_M:18;
set p =
(LifeSpan (((P +* (while>0 (a,I))) +* I),(Initialized s))) + 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))),
(Initialized s),
n)
by A18;
A26:
Initialized ((StepWhile>0 (a,P,s,I)) . m) = (StepWhile>0 (a,P,s,I)) . m
by A24, A23, FUNCT_4:98;
((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))),
(Initialized s),
(j + n))
= Comput (
(P +* (while>0 (a,I))),
(Comput ((P +* (while>0 (a,I))),(Initialized s),n)),
j)
by EXTPRO_1:4;
P +* (while>0 (a,I)) halts_on Initialized s
by A25, A27, A28, EXTPRO_1:29;
hence
while>0 (
a,
I)
is_halting_onInit s,
P
;
verum end; end;