let p be Instruction-Sequence of SCM+FSA; for s being State of SCM+FSA
for a being read-write Int-Location
for I being really-closed MacroInstruction of SCM+FSA st ProperBodyWhile>0 a,I,s,p & WithVariantWhile>0 a,I,s,p holds
while>0 (a,I) is_halting_on s,p
let s be State of SCM+FSA; for a being read-write Int-Location
for I being really-closed MacroInstruction of SCM+FSA st ProperBodyWhile>0 a,I,s,p & WithVariantWhile>0 a,I,s,p holds
while>0 (a,I) is_halting_on s,p
let a be read-write Int-Location; for I being really-closed MacroInstruction of SCM+FSA st ProperBodyWhile>0 a,I,s,p & WithVariantWhile>0 a,I,s,p holds
while>0 (a,I) is_halting_on s,p
let I be really-closed MacroInstruction of SCM+FSA ; ( ProperBodyWhile>0 a,I,s,p & WithVariantWhile>0 a,I,s,p implies while>0 (a,I) is_halting_on s,p )
assume A1:
for k being Nat st ((StepWhile>0 (a,I,p,s)) . k) . a > 0 holds
I is_halting_on (StepWhile>0 (a,I,p,s)) . k,p +* (while>0 (a,I))
; SCMFSA9A:def 4 ( not WithVariantWhile>0 a,I,s,p or while>0 (a,I) is_halting_on s,p )
set s1 = Initialize s;
set p1 = p +* (while>0 (a,I));
defpred S1[ Nat] means ((StepWhile>0 (a,I,p,s)) . $1) . a <= 0 ;
given f being Function of (product (the_Values_of SCM+FSA)),NAT such that A2:
for k being Nat holds
( f . ((StepWhile>0 (a,I,p,s)) . (k + 1)) < f . ((StepWhile>0 (a,I,p,s)) . k) or ((StepWhile>0 (a,I,p,s)) . k) . a <= 0 )
; SCMFSA9A:def 5 while>0 (a,I) is_halting_on s,p
deffunc H1( Nat) -> Element of NAT = f . ((StepWhile>0 (a,I,p,s)) . $1);
A3:
for k being Nat holds
( H1(k + 1) < H1(k) or S1[k] )
by A2;
consider m being Nat such that
A4:
S1[m]
and
A5:
for n being Nat st S1[n] holds
m <= n
from NAT_1:sch 18(A3);
defpred S2[ 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) );
A6:
now for k being Nat st S2[k] holds
S2[k + 1]let k be
Nat;
( S2[k] implies S2[k + 1] )assume A7:
S2[
k]
;
S2[k + 1]now ( (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;
set pk =
p +* (while>0 (a,I));
assume A8:
(k + 1) + 1
<= m
;
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 A8, XXREAL_0:2;
then A9:
((StepWhile>0 (a,I,p,s)) . k) . a > 0
by A5;
(k + 1) + 0 < (k + 1) + 1
by XREAL_1:6;
then consider n being
Nat such that A10:
(StepWhile>0 (a,I,p,s)) . (k + 1) = Comput (
(p +* (while>0 (a,I))),
(Initialize s),
n)
by A7, A8, XXREAL_0:2;
A11:
(StepWhile>0 (a,I,p,s)) . (k + 1) = Comput (
((p +* (while>0 (a,I))) +* (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 SCMFSA_9:def 5;
take m =
n + ((LifeSpan (((p +* (while>0 (a,I))) +* I),(Initialize ((StepWhile>0 (a,I,p,s)) . (k + 1))))) + 2);
(StepWhile>0 (a,I,p,s)) . ((k + 1) + 1) = Comput ((p +* (while>0 (a,I))),(Initialize s),m)
I is_halting_on (StepWhile>0 (a,I,p,s)) . k,
p +* (while>0 (a,I))
by A1, A9;
then
IC ((StepWhile>0 (a,I,p,s)) . (k + 1)) = 0
by A11, A9, SCMFSA_9:42;
hence
(StepWhile>0 (a,I,p,s)) . ((k + 1) + 1) = Comput (
(p +* (while>0 (a,I))),
(Initialize s),
m)
by A10, SCMFSA_9:45;
verum end; hence
S2[
k + 1]
;
verum end;
A12:
S2[ 0 ]
proof
assume
0 + 1
<= m
;
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;
(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 SCMFSA_9:44;
verum
end;
A13:
for k being Nat holds S2[k]
from NAT_1:sch 2(A12, A6);
per cases
( m = 0 or m <> 0 )
;
suppose A14:
m <> 0
;
while>0 (a,I) is_halting_on s,pset ii =
(LifeSpan (((p +* (while>0 (a,I))) +* I),(Initialize s))) + 2;
set sm =
(StepWhile>0 (a,I,p,s)) . m;
set pm =
p +* (while>0 (a,I));
set sm1 =
Initialize ((StepWhile>0 (a,I,p,s)) . m);
set pm1 =
(p +* (while>0 (a,I))) +* (while>0 (a,I));
consider i being
Nat such that A15:
m = i + 1
by A14, NAT_1:6;
reconsider i =
i as
Element of
NAT by ORDINAL1:def 12;
set si =
(StepWhile>0 (a,I,p,s)) . i;
set psi =
p +* (while>0 (a,I));
A16:
(StepWhile>0 (a,I,p,s)) . m = Comput (
((p +* (while>0 (a,I))) +* (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 A15, SCMFSA_9:def 5;
m = i + 1
by A15;
then consider n being
Nat such that A17:
(StepWhile>0 (a,I,p,s)) . m = Comput (
(p +* (while>0 (a,I))),
(Initialize s),
n)
by A13;
i < m
by A15, NAT_1:13;
then A18:
((StepWhile>0 (a,I,p,s)) . i) . a > 0
by A5;
then
I is_halting_on (StepWhile>0 (a,I,p,s)) . i,
p +* (while>0 (a,I))
by A1;
then
IC ((StepWhile>0 (a,I,p,s)) . m) = 0
by A16, A18, SCMFSA_9:42;
then
Start-At (
0,
SCM+FSA)
c= (StepWhile>0 (a,I,p,s)) . m
by MEMSTR_0:30;
then A19:
Initialize ((StepWhile>0 (a,I,p,s)) . m) = (StepWhile>0 (a,I,p,s)) . m
by FUNCT_4:98;
while>0 (
a,
I)
is_halting_on (StepWhile>0 (a,I,p,s)) . m,
p +* (while>0 (a,I))
by A4, SCMFSA_9:38;
then
(p +* (while>0 (a,I))) +* (while>0 (a,I)) halts_on Initialize ((StepWhile>0 (a,I,p,s)) . m)
by SCMFSA7B:def 7;
then consider j being
Nat such that A20:
CurInstr (
(p +* (while>0 (a,I))),
(Comput ((p +* (while>0 (a,I))),((StepWhile>0 (a,I,p,s)) . m),j)))
= halt SCM+FSA
by A19;
A21:
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 A17, A20, A21;
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;
verum end;