set S = Initialize s;
set P = p +* (while>0 (a,I));
set SW = StepWhile>0 (a,I,p,s);
set PW = p +* (while>0 (a,I));
A4:
while>0 (a,I) c= p +* (while>0 (a,I))
by FUNCT_4:25;
A5:
(p +* (while>0 (a,I))) +* (while>0 (a,I)) = p +* (while>0 (a,I))
by FUNCT_4:93;
defpred S1[ Nat] means ((StepWhile>0 (a,I,p,s)) . $1) . a <= 0 ;
consider f being Function of (product the Object-Kind of SCM+FSA),NAT such that
A7:
for k being Element of NAT holds
( f . ((StepWhile>0 (a,I,p,s)) . (k + 1)) < f . ((StepWhile>0 (a,I,p,s)) . k) or S1[k] )
by A2, Def5;
deffunc H1( Nat) -> Element of NAT = f . ((StepWhile>0 (a,I,p,s)) . $1);
A8:
for k being Element of NAT holds
( H1(k + 1) < H1(k) or S1[k] )
by A7;
consider m being Element of NAT such that
A9:
S1[m]
and
A10:
for n being Element of NAT st S1[n] holds
m <= n
from NAT_1:sch 18(A8);
take
m
; ex k being Element of NAT st
( m = k & ((StepWhile>0 (a,I,p,s)) . k) . a <= 0 & ( for i being Element of NAT st ((StepWhile>0 (a,I,p,s)) . i) . a <= 0 holds
k <= i ) & DataPart (Comput ((p +* (while>0 (a,I))),(Initialize s),(LifeSpan ((p +* (while>0 (a,I))),(Initialize s))))) = DataPart ((StepWhile>0 (a,I,p,s)) . k) )
take
m
; ( m = m & ((StepWhile>0 (a,I,p,s)) . m) . a <= 0 & ( for i being Element of NAT st ((StepWhile>0 (a,I,p,s)) . i) . a <= 0 holds
m <= i ) & DataPart (Comput ((p +* (while>0 (a,I))),(Initialize s),(LifeSpan ((p +* (while>0 (a,I))),(Initialize s))))) = DataPart ((StepWhile>0 (a,I,p,s)) . m) )
thus
m = m
; ( ((StepWhile>0 (a,I,p,s)) . m) . a <= 0 & ( for i being Element of NAT st ((StepWhile>0 (a,I,p,s)) . i) . a <= 0 holds
m <= i ) & DataPart (Comput ((p +* (while>0 (a,I))),(Initialize s),(LifeSpan ((p +* (while>0 (a,I))),(Initialize s))))) = DataPart ((StepWhile>0 (a,I,p,s)) . m) )
thus
((StepWhile>0 (a,I,p,s)) . m) . a <= 0
by A9; ( ( for i being Element of NAT st ((StepWhile>0 (a,I,p,s)) . i) . a <= 0 holds
m <= i ) & DataPart (Comput ((p +* (while>0 (a,I))),(Initialize s),(LifeSpan ((p +* (while>0 (a,I))),(Initialize s))))) = DataPart ((StepWhile>0 (a,I,p,s)) . m) )
thus
for n being Element of NAT st ((StepWhile>0 (a,I,p,s)) . n) . a <= 0 holds
m <= n
by A10; DataPart (Comput ((p +* (while>0 (a,I))),(Initialize s),(LifeSpan ((p +* (while>0 (a,I))),(Initialize s))))) = DataPart ((StepWhile>0 (a,I,p,s)) . m)
defpred S2[ Nat] means ( $1 + 1 <= m implies ex k being Element of NAT st (StepWhile>0 (a,I,p,s)) . ($1 + 1) = Comput ((p +* (while>0 (a,I))),(Initialize s),k) );
A11:
ProperBodyWhile>0 a,I,s,p
by A1, Th32;
A12:
now let k be
Element of
NAT ;
( S2[k] implies S2[k + 1] )assume A13:
S2[
k]
;
S2[k + 1]now 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 A14:
(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 A14, XXREAL_0:2;
then A15:
((StepWhile>0 (a,I,p,s)) . k) . a > 0
by A10;
(k + 1) + 0 < (k + 1) + 1
by XREAL_1:6;
then consider n being
Element of
NAT such that A16:
(StepWhile>0 (a,I,p,s)) . (k + 1) = Comput (
(p +* (while>0 (a,I))),
(Initialize s),
n)
by A13, A14, XXREAL_0:2;
A17:
(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)))) + 3))
by A5, SCMFSA_9:def 5;
take m =
n + ((LifeSpan (((p +* (while>0 (a,I))) +* I),(Initialize ((StepWhile>0 (a,I,p,s)) . (k + 1))))) + 3);
(StepWhile>0 (a,I,p,s)) . ((k + 1) + 1) = Comput ((p +* (while>0 (a,I))),(Initialize s),m)
(
I is_closed_on (StepWhile>0 (a,I,p,s)) . k,
p +* (while>0 (a,I)) &
I is_halting_on (StepWhile>0 (a,I,p,s)) . k,
p +* (while>0 (a,I)) )
by A11, A15, Def4;
then
IC ((StepWhile>0 (a,I,p,s)) . (k + 1)) = 0
by A17, A15, SCMFSA_9:42;
hence
(StepWhile>0 (a,I,p,s)) . ((k + 1) + 1) = Comput (
(p +* (while>0 (a,I))),
(Initialize s),
m)
by A16, SCMFSA_9:45;
verum end; hence
S2[
k + 1]
;
verum end;
B18:
IC in dom (Start-At (0,SCM+FSA))
by MEMSTR_0:15;
A19:
S2[ 0 ]
proof
assume
0 + 1
<= m
;
ex k being Element of 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))) + 3;
(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;
A20:
for k being Element of NAT holds S2[k]
from NAT_1:sch 1(A19, A12);
per cases
( m = 0 or m <> 0 )
;
suppose A21:
m = 0
;
DataPart (Comput ((p +* (while>0 (a,I))),(Initialize s),(LifeSpan ((p +* (while>0 (a,I))),(Initialize s))))) = DataPart ((StepWhile>0 (a,I,p,s)) . m)A22:
DataPart (Initialize s) =
DataPart s
by MEMSTR_0:79
.=
DataPart ((StepWhile>0 (a,I,p,s)) . m)
by A21, SCMFSA_9:def 5
;
then
(Initialize s) . a = ((StepWhile>0 (a,I,p,s)) . m) . a
by SCMFSA6A:7;
hence
DataPart (Comput ((p +* (while>0 (a,I))),(Initialize s),(LifeSpan ((p +* (while>0 (a,I))),(Initialize s))))) = DataPart ((StepWhile>0 (a,I,p,s)) . m)
by A9, A22, Th35, A4;
verum end; suppose A23:
m <> 0
;
DataPart (Comput ((p +* (while>0 (a,I))),(Initialize s),(LifeSpan ((p +* (while>0 (a,I))),(Initialize s))))) = DataPart ((StepWhile>0 (a,I,p,s)) . m)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 A24:
m = i + 1
by A23, 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));
A25:
(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)))) + 3))
by A24, A5, SCMFSA_9:def 5;
m = i + 1
by A24;
then consider n being
Element of
NAT such that A26:
(StepWhile>0 (a,I,p,s)) . m = Comput (
(p +* (while>0 (a,I))),
(Initialize s),
n)
by A20;
i < m
by A24, NAT_1:13;
then A27:
((StepWhile>0 (a,I,p,s)) . i) . a > 0
by A10;
then
(
I is_closed_on (StepWhile>0 (a,I,p,s)) . i,
p +* (while>0 (a,I)) &
I is_halting_on (StepWhile>0 (a,I,p,s)) . i,
p +* (while>0 (a,I)) )
by A11, Def4;
then A28:
IC ((StepWhile>0 (a,I,p,s)) . m) = 0
by A25, A27, SCMFSA_9:42;
A29:
IC (Initialize ((StepWhile>0 (a,I,p,s)) . m)) =
IC (Start-At (0,SCM+FSA))
by B18, FUNCT_4:13
.=
IC ((StepWhile>0 (a,I,p,s)) . m)
by A28, FUNCOP_1:72
;
DataPart (Initialize ((StepWhile>0 (a,I,p,s)) . m)) = DataPart ((StepWhile>0 (a,I,p,s)) . m)
by MEMSTR_0:79;
then A31:
Initialize ((StepWhile>0 (a,I,p,s)) . m) = (StepWhile>0 (a,I,p,s)) . m
by A29, MEMSTR_0:78;
while>0 (
a,
I)
is_halting_on (StepWhile>0 (a,I,p,s)) . m,
p +* (while>0 (a,I))
by A9, 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
Element of
NAT such that A32:
CurInstr (
(p +* (while>0 (a,I))),
(Comput ((p +* (while>0 (a,I))),((StepWhile>0 (a,I,p,s)) . m),j)))
= halt SCM+FSA
by A31, A5, EXTPRO_1:29;
A33:
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 A26, A32, A33;
then A34:
Comput (
(p +* (while>0 (a,I))),
(Initialize s),
(LifeSpan ((p +* (while>0 (a,I))),(Initialize s)))) =
Comput (
(p +* (while>0 (a,I))),
(Initialize s),
(n + j))
by EXTPRO_1:24
.=
Comput (
(p +* (while>0 (a,I))),
((StepWhile>0 (a,I,p,s)) . m),
j)
by A26, EXTPRO_1:4
.=
Comput (
(p +* (while>0 (a,I))),
((StepWhile>0 (a,I,p,s)) . m),
(LifeSpan ((p +* (while>0 (a,I))),((StepWhile>0 (a,I,p,s)) . m))))
by A32, EXTPRO_1:24
;
Start-At (
0,
SCM+FSA)
c= (StepWhile>0 (a,I,p,s)) . m
by A31, FUNCT_4:25;
then
(StepWhile>0 (a,I,p,s)) . m is
0 -started
by MEMSTR_0:29;
hence
DataPart (Comput ((p +* (while>0 (a,I))),(Initialize s),(LifeSpan ((p +* (while>0 (a,I))),(Initialize s))))) = DataPart ((StepWhile>0 (a,I,p,s)) . m)
by A9, A34, Th35, A4;
verum end;