let s be State of SCM+FSA ; :: thesis: for a being Int-Location
for J being good Program of SCM+FSA st s . (intloc 0 ) = 1 & ( ProperTimesBody a,J,s or J is parahalting ) holds
( times a,J is_closed_on s & times a,J is_halting_on s )
let a be Int-Location ; :: thesis: for J being good Program of SCM+FSA st s . (intloc 0 ) = 1 & ( ProperTimesBody a,J,s or J is parahalting ) holds
( times a,J is_closed_on s & times a,J is_halting_on s )
let J be good Program of SCM+FSA ; :: thesis: ( s . (intloc 0 ) = 1 & ( ProperTimesBody a,J,s or J is parahalting ) implies ( times a,J is_closed_on s & times a,J is_halting_on s ) )
set I = J;
assume A1:
s . (intloc 0 ) = 1
; :: thesis: ( ( not ProperTimesBody a,J,s & not J is parahalting ) or ( times a,J is_closed_on s & times a,J is_halting_on s ) )
assume A2:
( ProperTimesBody a,J,s or J is parahalting )
; :: thesis: ( times a,J is_closed_on s & times a,J is_halting_on s )
then A3:
ProperTimesBody a,J,s
by Th15;
set au = 1 -stRWNotIn ({a} \/ (UsedIntLoc J));
set ISu = J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ));
set WH = while>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 )));
set s1 = Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s);
set Is1 = Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s));
set ST = StepTimes a,J,s;
set SW = StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s));
set ISW = StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)));
set taI = times a,J;
A4:
StepTimes a,J,s = StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s))
;
(Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)) . (intloc 0 ) =
(Initialize s) . (intloc 0 )
by SCMFSA_2:89
.=
1
by SCMFSA6C:3
;
then A5:
DataPart (Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s))) = DataPart (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s))
by SCMFSA8C:27;
A6:
Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s) = IExec (Macro ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a)),s
by SCMFSA6C:6;
A7:
Macro ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a) is_closed_on Initialize s
by SCMFSA7B:24;
A8:
Macro ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a) is_halting_on Initialize s
by SCMFSA7B:25;
per cases
( s . a < 0 or 0 <= s . a )
;
suppose A10:
s . a < 0
;
:: thesis: ( times a,J is_closed_on s & times a,J is_halting_on s )A11:
(
a = intloc 0 or not
a is
read-only )
by SF_MASTR:def 5;
A12:
(Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) =
(Initialize s) . a
by SCMFSA_2:89
.=
s . a
by A1, A11, SCMFSA6C:3
;
then A13:
while>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),
(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))) is_closed_on Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),
(Initialize s)
by A10, SCMFSA_9:43;
A14:
while>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),
(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))) is_halting_on Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),
(Initialize s)
by A10, A12, SCMFSA_9:43;
A15:
times a,
J is_closed_on Initialize s
by A6, A7, A8, A13, SFMASTR1:3;
hence
times a,
J is_closed_on s
by A1, Th4;
:: thesis: times a,J is_halting_on s
times a,
J is_halting_on Initialize s
by A6, A7, A8, A13, A14, SFMASTR1:4;
hence
times a,
J is_halting_on s
by A1, A15, Th5;
:: thesis: verum end; suppose A16:
0 <= s . a
;
:: thesis: ( times a,J is_closed_on s & times a,J is_halting_on s )A17:
ProperBodyWhile>0 1
-stRWNotIn ({a} \/ (UsedIntLoc J)),
J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 )),
Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),
(Initialize s)
proof
let k be
Element of
NAT ;
:: according to SCMFSA9A:def 4 :: thesis: ( ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) <= 0 or ( J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 )) is_closed_on (StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s))) . k & J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 )) is_halting_on (StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s))) . k ) )
assume
((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) > 0
;
:: thesis: ( J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 )) is_closed_on (StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s))) . k & J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 )) is_halting_on (StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s))) . k )
then A18:
k < s . a
by A1, A3, A4, A16, Th18;
then A19:
J is_closed_on (StepTimes a,J,s) . k
by A3, Def3;
A20:
J is_halting_on (StepTimes a,J,s) . k
by A3, A18, Def3;
A21:
((StepTimes a,J,s) . k) . (intloc 0 ) = 1
by A2, A18, Th15, Th16;
then A22:
DataPart ((StepTimes a,J,s) . k) = DataPart (Initialize ((StepTimes a,J,s) . k))
by SCMFSA8C:27;
A23:
J is_closed_on Initialize ((StepTimes a,J,s) . k)
by A19, A21, Th4;
A24:
J is_halting_on Initialize ((StepTimes a,J,s) . k)
by A19, A20, A21, Th5;
A26:
Macro (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 )) is_closed_on IExec J,
((StepTimes a,J,s) . k)
by SCMFSA7B:24;
then A27:
J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 )) is_closed_on Initialize ((StepTimes a,J,s) . k)
by A23, A24, SFMASTR1:3;
Macro (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 )) is_halting_on IExec J,
((StepTimes a,J,s) . k)
by SCMFSA7B:25;
then A28:
J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 )) is_halting_on Initialize ((StepTimes a,J,s) . k)
by A23, A24, A26, SFMASTR1:4;
thus
J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 )) is_closed_on (StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s))) . k
by A22, A27, SCMFSA8B:6;
:: thesis: J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 )) is_halting_on (StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s))) . k
thus
J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 )) is_halting_on (StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s))) . k
by A22, A27, A28, SCMFSA8B:8;
:: thesis: verum
end; A29:
ProperBodyWhile>0 1
-stRWNotIn ({a} \/ (UsedIntLoc J)),
J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 )),
Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s))
proof
let k be
Element of
NAT ;
:: according to SCMFSA9A:def 4 :: thesis: ( ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) <= 0 or ( J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 )) is_closed_on (StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . k & J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 )) is_halting_on (StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . k ) )
assume A30:
((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) > 0
;
:: thesis: ( J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 )) is_closed_on (StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . k & J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 )) is_halting_on (StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . k )
A31:
DataPart ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . k) = DataPart ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s))) . k)
by A5, A17, SCMFSA9A:40;
then
((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) = ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))
by SCMFSA6A:38;
then A32:
(
J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 )) is_closed_on (StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s))) . k &
J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 )) is_halting_on (StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s))) . k )
by A17, A30, SCMFSA9A:def 4;
hence
J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 )) is_closed_on (StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . k
by A31, SCMFSA8B:6;
:: thesis: J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 )) is_halting_on (StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . k
thus
J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 )) is_halting_on (StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . k
by A31, A32, SCMFSA8B:8;
:: thesis: verum
end; A33:
WithVariantWhile>0 1
-stRWNotIn ({a} \/ (UsedIntLoc J)),
J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 )),
Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s))
proof
deffunc H1(
Element of
product the
Object-Kind of
SCM+FSA )
-> Element of
NAT =
abs ($1 . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))));
consider f being
Function of
(product the Object-Kind of SCM+FSA ),
NAT such that A34:
for
x being
Element of
product the
Object-Kind of
SCM+FSA holds
f . x = H1(
x)
from FUNCT_2:sch 4();
take
f
;
:: according to SCMFSA9A:def 5 :: thesis: for b1 being Element of NAT holds
( not f . ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . b1) <= f . ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . (b1 + 1)) or ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . b1) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) <= 0 )
reconsider sa =
s . a as
Element of
NAT by A16, INT_1:16;
let k be
Element of
NAT ;
:: thesis: ( not f . ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . k) <= f . ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . (k + 1)) or ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) <= 0 )
DataPart ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . k) = DataPart ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s))) . k)
by A5, A17, SCMFSA9A:40;
then A35:
((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) = ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))
by SCMFSA6A:38;
DataPart ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . (k + 1)) = DataPart ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s))) . (k + 1))
by A5, A17, SCMFSA9A:40;
then A36:
((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) = ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s))) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))
by SCMFSA6A:38;
per cases
( k < s . a or k >= s . a )
;
suppose A37:
k < s . a
;
:: thesis: ( not f . ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . k) <= f . ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . (k + 1)) or ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) <= 0 )then A38:
k + 1
<= sa
by NAT_1:13;
A39:
(((StepTimes a,J,s) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) + k = s . a
by A1, A3, A37, Th17;
A40:
(((StepTimes a,J,s) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) + (k + 1) = s . a
by A1, A3, A38, Th17;
then A41:
s . a = ((((StepTimes a,J,s) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) + 1) + k
;
A42:
(k + 1) - (k + 1) <= (s . a) - (k + 1)
by A38, XREAL_1:11;
A43:
f . ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . (k + 1)) =
abs (((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))))
by A34
.=
((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s))) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))
by A36, A40, A42, ABSVALUE:def 1
;
A44:
k - k < (s . a) - k
by A37, XREAL_1:11;
f . ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . k) =
abs (((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))))
by A34
.=
((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))
by A35, A39, A44, ABSVALUE:def 1
;
hence
( not
f . ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . k) <= f . ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . (k + 1)) or
((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) <= 0 )
by A39, A41, A43, NAT_1:13;
:: thesis: verum end; suppose
k >= s . a
;
:: thesis: ( not f . ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . k) <= f . ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . (k + 1)) or ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) <= 0 )hence
( not
f . ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . k) <= f . ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . (k + 1)) or
((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) <= 0 )
by A1, A3, A4, A16, A35, Th18;
:: thesis: verum end;
end; then A45:
while>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),
(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))) is_closed_on Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s))
by A29, SCMFSA9A:33;
A46:
while>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),
(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))) is_closed_on Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),
(Initialize s)
by A5, A29, A33, SCMFSA8B:6, SCMFSA9A:33;
while>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),
(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))) is_halting_on Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s))
by A29, A33, SCMFSA9A:33;
then A47:
while>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),
(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))) is_halting_on Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),
(Initialize s)
by A5, A45, SCMFSA8B:8;
A49:
times a,
J is_closed_on Initialize s
by A6, A7, A8, A46, SFMASTR1:3;
hence
times a,
J is_closed_on s
by A1, Th4;
:: thesis: times a,J is_halting_on s
times a,
J is_halting_on Initialize s
by A6, A7, A8, A46, A47, SFMASTR1:4;
hence
times a,
J is_halting_on s
by A1, A49, Th5;
:: thesis: verum end;