let s be State of SCM+FSA; for p being Instruction-Sequence of SCM+FSA
for a being Int-Location
for J being really-closed good MacroInstruction of SCM+FSA st 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 Int-Location
for J being really-closed good MacroInstruction of SCM+FSA st 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 Int-Location; for J being really-closed good MacroInstruction of SCM+FSA st 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 really-closed good MacroInstruction of SCM+FSA ; ( 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:
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 au = 1 -stRWNotIn ({a} \/ (UsedILoc J));
set ISu = J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)));
set WH = while>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))));
set s1 = Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s));
set Is1 = Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)));
set SW = StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))));
set ISW = StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))));
A2:
Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)) = IExec ((Macro ((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a)),p,s)
by SCMFSA6C:5;
(Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))) . (intloc 0) =
(Initialized s) . (intloc 0)
by SCMFSA_2:63
.=
1
by SCMFSA_M:9
;
then A3:
DataPart (Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))) = DataPart (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))
by SCMFSA_M:19;
assume A4:
( ProperTimesBody a,J,s,p or J is parahalting )
; times (a,J) is_halting_on s,p
then A5:
ProperTimesBody a,J,s,p
by Th11;
A6:
Macro ((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a) is_halting_on Initialized s,p
by SCMFSA7B:19;
per cases
( s . a < 0 or 0 <= s . a )
;
suppose A7:
s . a < 0
;
times (a,J) is_halting_on s,pA8:
(
a = intloc 0 or
a is
read-write )
by SCMFSA_M:def 2;
A9:
(Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) =
(Initialized s) . a
by SCMFSA_2:63
.=
s . a
by A1, A8, SCMFSA_M:9, SCMFSA_M:37
;
while>0 (
(1 -stRWNotIn ({a} \/ (UsedILoc J))),
(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))))
is_halting_on Exec (
((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),
(Initialized s)),
p
by A7, A9, SCMFSA_9:38;
then
times (
a,
J)
is_halting_on Initialized s,
p
by A2, A6, SFMASTR1:3;
hence
times (
a,
J)
is_halting_on s,
p
by A1, SCMFSA8B:42;
verum end; suppose A10:
0 <= s . a
;
times (a,J) is_halting_on s,pA11:
ProperBodyWhile>0 1
-stRWNotIn ({a} \/ (UsedILoc J)),
J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0))),
Exec (
((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),
(Initialized s)),
p
proof
let k be
Nat;
SCMFSA9A:def 4 ( ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))))) . k) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) <= 0 or J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0))) is_halting_on (StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))))) . k,p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))))) )
assume
((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))))) . k) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) > 0
;
J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0))) is_halting_on (StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))))) . k,p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0))))))
then A12:
k < s . a
by A1, A5, A10, Th14;
then A13:
((StepTimes (a,J,p,s)) . k) . (intloc 0) = 1
by A4, Th11, Th12;
then A14:
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 A5, A12;
then A15:
J is_halting_on Initialized ((StepTimes (a,J,p,s)) . k),
p +* (times* (a,J))
by A13, SCMFSA8B:42;
Macro (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(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 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0))) is_halting_on Initialized ((StepTimes (a,J,p,s)) . k),
p +* (times* (a,J))
by A15, SFMASTR1:3;
hence
J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0))) is_halting_on (StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))))) . k,
p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0))))))
by A14, SCMFSA8B:5;
verum
end; A16:
WithVariantWhile>0 1
-stRWNotIn ({a} \/ (UsedILoc J)),
J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0))),
Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))),
p
proof
reconsider sa =
s . a as
Element of
NAT by A10, INT_1:3;
deffunc H1(
State of
SCM+FSA)
-> Element of
NAT =
|.($1 . (1 -stRWNotIn ({a} \/ (UsedILoc J)))).|;
consider f being
Function of
(product (the_Values_of SCM+FSA)),
NAT such that A17:
for
x being
Element of
product (the_Values_of SCM+FSA) holds
f . x = H1(
x)
from FUNCT_2:sch 4();
A18:
for
x being
State of
SCM+FSA holds
f . x = H1(
x)
take
f
;
SCMFSA9A:def 5 for b1 being set holds
( not f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . b1) <= f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . (b1 + 1)) or ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . b1) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) <= 0 )
let k be
Nat;
( not f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . k) <= f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . (k + 1)) or ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . k) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) <= 0 )
DataPart ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . k) = DataPart ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))))) . k)
by A3, A11, SCMFSA9A:34;
then A19:
((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . k) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) = ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))))) . k) . (1 -stRWNotIn ({a} \/ (UsedILoc J)))
by SCMFSA_M:2;
DataPart ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . (k + 1)) = DataPart ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))))) . (k + 1))
by A3, A11, SCMFSA9A:34;
then A20:
((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) = ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))))) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedILoc J)))
by SCMFSA_M:2;
per cases
( k < s . a or k >= s . a )
;
suppose A21:
k < s . a
;
( not f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . k) <= f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . (k + 1)) or ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . k) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) <= 0 )then A22:
k - k < (s . a) - k
by XREAL_1:9;
A23:
(((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedILoc J)))) + k = s . a
by A1, A5, A21, Th13;
A24:
k + 1
<= sa
by A21, NAT_1:13;
then A25:
(k + 1) - (k + 1) <= (s . a) - (k + 1)
by XREAL_1:9;
A26:
(((StepTimes (a,J,p,s)) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedILoc J)))) + (k + 1) = s . a
by A1, A5, A24, Th13;
then A27:
s . a = ((((StepTimes (a,J,p,s)) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedILoc J)))) + 1) + k
;
A28:
f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . (k + 1)) =
|.(((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedILoc J)))).|
by A18
.=
((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))))) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedILoc J)))
by A20, A26, A25, ABSVALUE:def 1
;
f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . k) =
|.(((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . k) . (1 -stRWNotIn ({a} \/ (UsedILoc J)))).|
by A18
.=
((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))))) . k) . (1 -stRWNotIn ({a} \/ (UsedILoc J)))
by A19, A23, A22, ABSVALUE:def 1
;
hence
( not
f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . k) <= f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . (k + 1)) or
((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . k) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) <= 0 )
by A23, A27, A28, NAT_1:13;
verum end; suppose
k >= s . a
;
( not f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . k) <= f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . (k + 1)) or ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . k) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) <= 0 )hence
( not
f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . k) <= f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . (k + 1)) or
((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . k) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) <= 0 )
by A1, A5, A10, A19, Th14;
verum end; end;
end; A29:
ProperBodyWhile>0 1
-stRWNotIn ({a} \/ (UsedILoc J)),
J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0))),
Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))),
p
proof
let k be
Nat;
SCMFSA9A:def 4 ( ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . k) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) <= 0 or J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0))) is_halting_on (StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . k,p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))))) )
assume A30:
((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . k) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) > 0
;
J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0))) is_halting_on (StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . k,p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0))))))
A31:
DataPart ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . k) = DataPart ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))))) . k)
by A3, A11, SCMFSA9A:34;
then A32:
((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))))) . k) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) = ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . k) . (1 -stRWNotIn ({a} \/ (UsedILoc J)))
by SCMFSA_M:2;
J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0))) is_halting_on (StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))))) . k,
p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0))))))
by A11, A30, A32;
hence
J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0))) is_halting_on (StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . k,
p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0))))))
by A31, SCMFSA8B:5;
verum
end;
while>0 (
(1 -stRWNotIn ({a} \/ (UsedILoc J))),
(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))))
is_halting_on Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))),
p
by A29, A16, SCMFSA9A:27;
then
while>0 (
(1 -stRWNotIn ({a} \/ (UsedILoc J))),
(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))))
is_halting_on Exec (
((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),
(Initialized s)),
p
by A3, SCMFSA8B:5;
then
times (
a,
J)
is_halting_on Initialized s,
p
by A2, A6, SFMASTR1:3;
hence
times (
a,
J)
is_halting_on s,
p
by A1, SCMFSA8B:42;
verum end; end;