let s be State of SCM+FSA; for p being Instruction-Sequence of SCM+FSA
for a being read-write Int-Location
for J being good really-closed MacroInstruction of SCM+FSA st not J destroys a & s . (intloc 0) = 1 & ( ProperTimesBody a,J,s,p or J is parahalting ) holds
Times (a,J) is_halting_on s,p
let p be Instruction-Sequence of SCM+FSA; for a being read-write Int-Location
for J being good really-closed MacroInstruction of SCM+FSA st not J destroys a & s . (intloc 0) = 1 & ( ProperTimesBody a,J,s,p or J is parahalting ) holds
Times (a,J) is_halting_on s,p
let a be read-write Int-Location; for J being good really-closed MacroInstruction of SCM+FSA st not J destroys a & s . (intloc 0) = 1 & ( ProperTimesBody a,J,s,p or J is parahalting ) holds
Times (a,J) is_halting_on s,p
let J be good really-closed MacroInstruction of SCM+FSA ; ( not J destroys a & s . (intloc 0) = 1 & ( ProperTimesBody a,J,s,p or J is parahalting ) implies Times (a,J) is_halting_on s,p )
set I = J;
assume A1:
not J destroys a
; ( not s . (intloc 0) = 1 or ( not ProperTimesBody a,J,s,p & not J is parahalting ) or Times (a,J) is_halting_on s,p )
assume A2:
s . (intloc 0) = 1
; ( ( not ProperTimesBody a,J,s,p & not J is parahalting ) or Times (a,J) is_halting_on s,p )
set taI = Times (a,J);
set ST = StepTimes (a,J,p,s);
set ISu = J ";" (SubFrom (a,(intloc 0)));
set WH = while>0 (a,(J ";" (SubFrom (a,(intloc 0)))));
set s1 = Initialized s;
set Is1 = Initialized (Initialized s);
set SW = StepWhile>0 (a,(J ";" (SubFrom (a,(intloc 0)))),p,(Initialized s));
set ISW = StepWhile>0 (a,(J ";" (SubFrom (a,(intloc 0)))),p,(Initialized (Initialized s)));
assume A3:
( ProperTimesBody a,J,s,p or J is parahalting )
; Times (a,J) is_halting_on s,p
then A4:
ProperTimesBody a,J,s,p
by Th50;
per cases
( s . a < 0 or 0 <= s . a )
;
suppose A5:
s . a < 0
;
Times (a,J) is_halting_on s,pA6:
(Initialized s) . a = s . a
by SCMFSA_M:37;
while>0 (
a,
(J ";" (SubFrom (a,(intloc 0)))))
is_halting_on Initialized s,
p
by A5, A6, SCMFSA_9:38;
then
Times (
a,
J)
is_halting_on Initialized s,
p
;
hence
Times (
a,
J)
is_halting_on s,
p
by A2, SCMFSA8B:42;
verum end; suppose A7:
0 <= s . a
;
Times (a,J) is_halting_on s,pA8:
ProperBodyWhile>0 a,
J ";" (SubFrom (a,(intloc 0))),
Initialized s,
p
proof
let k be
Nat;
SCMFSA9A:def 4 ( ((StepWhile>0 (a,(J ";" (SubFrom (a,(intloc 0)))),p,(Initialized s))) . k) . a > 0 implies J ";" (SubFrom (a,(intloc 0))) is_halting_on (StepWhile>0 (a,(J ";" (SubFrom (a,(intloc 0)))),p,(Initialized s))) . k,p +* (while>0 (a,(J ";" (SubFrom (a,(intloc 0)))))) )
assume
((StepWhile>0 (a,(J ";" (SubFrom (a,(intloc 0)))),p,(Initialized s))) . k) . a > 0
;
J ";" (SubFrom (a,(intloc 0))) is_halting_on (StepWhile>0 (a,(J ";" (SubFrom (a,(intloc 0)))),p,(Initialized s))) . k,p +* (while>0 (a,(J ";" (SubFrom (a,(intloc 0))))))
then A9:
k < s . a
by A4, A7, Th53, A1;
then A10:
((StepTimes (a,J,p,s)) . k) . (intloc 0) = 1
by A3, Th50, Th51, A1;
then A11:
DataPart ((StepTimes (a,J,p,s)) . k) = DataPart (Initialized ((StepTimes (a,J,p,s)) . k))
by SCMFSA_M:19;
J is_halting_on (StepTimes (a,J,p,s)) . k,
p +* (Times (a,J))
by A4, A9;
then A12:
J is_halting_on Initialized ((StepTimes (a,J,p,s)) . k),
p +* (Times (a,J))
by A10, SCMFSA8B:42;
Macro (SubFrom (a,(intloc 0))) is_halting_on IExec (
J,
(p +* (Times (a,J))),
((StepTimes (a,J,p,s)) . k)),
p +* (Times (a,J))
by SCMFSA7B:19;
then
J ";" (SubFrom (a,(intloc 0))) is_halting_on Initialized ((StepTimes (a,J,p,s)) . k),
p +* (Times (a,J))
by A12, SFMASTR1:3;
hence
J ";" (SubFrom (a,(intloc 0))) is_halting_on (StepWhile>0 (a,(J ";" (SubFrom (a,(intloc 0)))),p,(Initialized s))) . k,
p +* (while>0 (a,(J ";" (SubFrom (a,(intloc 0))))))
by A11, SCMFSA8B:5;
verum
end; A13:
WithVariantWhile>0 a,
J ";" (SubFrom (a,(intloc 0))),
Initialized (Initialized s),
p
proof
reconsider sa =
s . a as
Element of
NAT by A7, INT_1:3;
deffunc H1(
State of
SCM+FSA)
-> Element of
NAT =
|.($1 . a).|;
consider f being
Function of
(product (the_Values_of SCM+FSA)),
NAT such that A14:
for
x being
Element of
product (the_Values_of SCM+FSA) holds
f . x = H1(
x)
from FUNCT_2:sch 4();
A15:
for
x being
State of
SCM+FSA holds
f . x = H1(
x)
take
f
;
SCMFSA9A:def 5 for k being Nat holds
( f . ((StepWhile>0 (a,(J ";" (SubFrom (a,(intloc 0)))),p,(Initialized (Initialized s)))) . (k + 1)) < f . ((StepWhile>0 (a,(J ";" (SubFrom (a,(intloc 0)))),p,(Initialized (Initialized s)))) . k) or ((StepWhile>0 (a,(J ";" (SubFrom (a,(intloc 0)))),p,(Initialized (Initialized s)))) . k) . a <= 0 )
let k be
Nat;
( f . ((StepWhile>0 (a,(J ";" (SubFrom (a,(intloc 0)))),p,(Initialized (Initialized s)))) . (k + 1)) < f . ((StepWhile>0 (a,(J ";" (SubFrom (a,(intloc 0)))),p,(Initialized (Initialized s)))) . k) or ((StepWhile>0 (a,(J ";" (SubFrom (a,(intloc 0)))),p,(Initialized (Initialized s)))) . k) . a <= 0 )
per cases
( k < s . a or k >= s . a )
;
suppose A16:
k < s . a
;
( f . ((StepWhile>0 (a,(J ";" (SubFrom (a,(intloc 0)))),p,(Initialized (Initialized s)))) . (k + 1)) < f . ((StepWhile>0 (a,(J ";" (SubFrom (a,(intloc 0)))),p,(Initialized (Initialized s)))) . k) or ((StepWhile>0 (a,(J ";" (SubFrom (a,(intloc 0)))),p,(Initialized (Initialized s)))) . k) . a <= 0 )then A17:
k - k < (s . a) - k
by XREAL_1:9;
A18:
(((StepTimes (a,J,p,s)) . k) . a) + k = s . a
by A4, A16, Th52, A1;
A19:
k + 1
<= sa
by A16, NAT_1:13;
then A20:
(k + 1) - (k + 1) <= (s . a) - (k + 1)
by XREAL_1:9;
A21:
(((StepTimes (a,J,p,s)) . (k + 1)) . a) + (k + 1) = s . a
by A4, A19, Th52, A1;
then A22:
s . a = ((((StepTimes (a,J,p,s)) . (k + 1)) . a) + 1) + k
;
A23:
f . ((StepWhile>0 (a,(J ";" (SubFrom (a,(intloc 0)))),p,(Initialized (Initialized s)))) . (k + 1)) =
|.(((StepWhile>0 (a,(J ";" (SubFrom (a,(intloc 0)))),p,(Initialized (Initialized s)))) . (k + 1)) . a).|
by A15
.=
((StepWhile>0 (a,(J ";" (SubFrom (a,(intloc 0)))),p,(Initialized s))) . (k + 1)) . a
by A21, A20, ABSVALUE:def 1
;
f . ((StepWhile>0 (a,(J ";" (SubFrom (a,(intloc 0)))),p,(Initialized (Initialized s)))) . k) =
|.(((StepWhile>0 (a,(J ";" (SubFrom (a,(intloc 0)))),p,(Initialized (Initialized s)))) . k) . a).|
by A15
.=
((StepWhile>0 (a,(J ";" (SubFrom (a,(intloc 0)))),p,(Initialized s))) . k) . a
by A18, A17, ABSVALUE:def 1
;
hence
(
f . ((StepWhile>0 (a,(J ";" (SubFrom (a,(intloc 0)))),p,(Initialized (Initialized s)))) . (k + 1)) < f . ((StepWhile>0 (a,(J ";" (SubFrom (a,(intloc 0)))),p,(Initialized (Initialized s)))) . k) or
((StepWhile>0 (a,(J ";" (SubFrom (a,(intloc 0)))),p,(Initialized (Initialized s)))) . k) . a <= 0 )
by A18, A22, A23, NAT_1:13;
verum end; suppose
k >= s . a
;
( f . ((StepWhile>0 (a,(J ";" (SubFrom (a,(intloc 0)))),p,(Initialized (Initialized s)))) . (k + 1)) < f . ((StepWhile>0 (a,(J ";" (SubFrom (a,(intloc 0)))),p,(Initialized (Initialized s)))) . k) or ((StepWhile>0 (a,(J ";" (SubFrom (a,(intloc 0)))),p,(Initialized (Initialized s)))) . k) . a <= 0 )hence
(
f . ((StepWhile>0 (a,(J ";" (SubFrom (a,(intloc 0)))),p,(Initialized (Initialized s)))) . (k + 1)) < f . ((StepWhile>0 (a,(J ";" (SubFrom (a,(intloc 0)))),p,(Initialized (Initialized s)))) . k) or
((StepWhile>0 (a,(J ";" (SubFrom (a,(intloc 0)))),p,(Initialized (Initialized s)))) . k) . a <= 0 )
by A4, A7, Th53, A1;
verum end; end;
end; A24:
ProperBodyWhile>0 a,
J ";" (SubFrom (a,(intloc 0))),
Initialized (Initialized s),
p
by A8;
while>0 (
a,
(J ";" (SubFrom (a,(intloc 0)))))
is_halting_on Initialized (Initialized s),
p
by A24, A13, Th27;
then
while>0 (
a,
(J ";" (SubFrom (a,(intloc 0)))))
is_halting_on Initialized s,
p
;
then
Times (
a,
J)
is_halting_on Initialized s,
p
;
hence
Times (
a,
J)
is_halting_on s,
p
by A2, SCMFSA8B:42;
verum end; end;