let s be State of SCM+FSA ; for a being Int-Location
for J being good Program of SCM+FSA
for k being Element of NAT st s . a = k & ( ProperTimesBody a,J,s or J is parahalting ) & ( s . (intloc 0 ) = 1 or not a is read-only ) holds
DataPart (IExec (times a,J),s) = DataPart ((StepTimes a,J,s) . k)
let a be Int-Location ; for J being good Program of SCM+FSA
for k being Element of NAT st s . a = k & ( ProperTimesBody a,J,s or J is parahalting ) & ( s . (intloc 0 ) = 1 or not a is read-only ) holds
DataPart (IExec (times a,J),s) = DataPart ((StepTimes a,J,s) . k)
let J be good Program of SCM+FSA ; for k being Element of NAT st s . a = k & ( ProperTimesBody a,J,s or J is parahalting ) & ( s . (intloc 0 ) = 1 or not a is read-only ) holds
DataPart (IExec (times a,J),s) = DataPart ((StepTimes a,J,s) . k)
let k be Element of NAT ; ( s . a = k & ( ProperTimesBody a,J,s or J is parahalting ) & ( s . (intloc 0 ) = 1 or not a is read-only ) implies DataPart (IExec (times a,J),s) = DataPart ((StepTimes a,J,s) . k) )
set I = J;
assume A1:
s . a = k
; ( ( not ProperTimesBody a,J,s & not J is parahalting ) or ( not s . (intloc 0 ) = 1 & a is read-only ) or DataPart (IExec (times a,J),s) = DataPart ((StepTimes a,J,s) . k) )
set ST = StepTimes a,J,s;
set au = 1 -stRWNotIn ({a} \/ (UsedIntLoc J));
set ISu = J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ));
set s1 = Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s);
set Is1 = Initialized (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized 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),(Initialized s));
set ISW = StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialized (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)));
(Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)) . (intloc 0 ) =
(Initialized s) . (intloc 0 )
by SCMFSA_2:89
.=
1
by SCMFSA6C:3
;
then A2:
DataPart (Initialized (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))) = DataPart (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))
by SCMFSA8C:27;
set WH = while>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 )));
assume A3:
( ProperTimesBody a,J,s or J is parahalting )
; ( ( not s . (intloc 0 ) = 1 & a is read-only ) or DataPart (IExec (times a,J),s) = DataPart ((StepTimes a,J,s) . k) )
then A4:
ProperTimesBody a,J,s
by Th15;
assume A5:
( s . (intloc 0 ) = 1 or not a is read-only )
; DataPart (IExec (times a,J),s) = DataPart ((StepTimes a,J,s) . k)
A6:
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),(Initialized s))
;
A7:
ProperBodyWhile>0 1 -stRWNotIn ({a} \/ (UsedIntLoc J)),J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 )), Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)
proof
let k be
Element of
NAT ;
SCMFSA9A:def 4 ( ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized 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),(Initialized 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),(Initialized 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),(Initialized s))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) > 0
;
( 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),(Initialized 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),(Initialized s))) . k )
then A8:
k < s . a
by A1, A4, A5, A6, Th18;
then A9:
((StepTimes a,J,s) . k) . (intloc 0 ) = 1
by A3, Th15, Th16;
then A10:
DataPart ((StepTimes a,J,s) . k) = DataPart (Initialized ((StepTimes a,J,s) . k))
by SCMFSA8C:27;
A11:
J is_closed_on (StepTimes a,J,s) . k
by A4, A8, Def3;
then A12:
J is_closed_on Initialized ((StepTimes a,J,s) . k)
by A9, Th4;
J is_halting_on (StepTimes a,J,s) . k
by A4, A8, Def3;
then A13:
J is_halting_on Initialized ((StepTimes a,J,s) . k)
by A11, A9, Th5;
A14:
Macro (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 )) is_closed_on IExec J,
((StepTimes a,J,s) . k)
by SCMFSA7B:24;
then A15:
J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 )) is_closed_on Initialized ((StepTimes a,J,s) . k)
by A12, A13, SFMASTR1:3;
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 ))),(Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))) . k
by A10, SCMFSA8B:6;
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),(Initialized s))) . k
Macro (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 )) is_halting_on IExec J,
((StepTimes a,J,s) . k)
by SCMFSA7B:25;
then
J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 )) is_halting_on Initialized ((StepTimes a,J,s) . k)
by A12, A13, A14, SFMASTR1:4;
hence
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),(Initialized s))) . k
by A10, A15, SCMFSA8B:8;
verum
end;
then A16:
DataPart ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialized (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized 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),(Initialized s))) . k)
by A2, SCMFSA9A:40;
A17:
WithVariantWhile>0 1 -stRWNotIn ({a} \/ (UsedIntLoc J)),J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 )), Initialized (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))
proof
reconsider sa =
s . a as
Element of
NAT by A1;
deffunc H1(
State 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 B18:
for
x being
Element of
product the
Object-Kind 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 Element of NAT holds
( not f . ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialized (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))) . b1) <= f . ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialized (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))) . (b1 + 1)) or ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialized (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))) . b1) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) <= 0 )
let k be
Element of
NAT ;
( not f . ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialized (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))) . k) <= f . ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialized (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))) . (k + 1)) or ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialized (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized 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 ))),(Initialized (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized 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),(Initialized s))) . k)
by A2, A7, SCMFSA9A:40;
then A19:
((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialized (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized 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),(Initialized 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 ))),(Initialized (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized 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),(Initialized s))) . (k + 1))
by A2, A7, SCMFSA9A:40;
then A20:
((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialized (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized 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),(Initialized s))) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))
by SCMFSA6A:38;
per cases
( k < s . a or k >= s . a )
;
suppose A21:
k < s . a
;
( not f . ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialized (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))) . k) <= f . ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialized (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))) . (k + 1)) or ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialized (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) <= 0 )then A22:
k - k < (s . a) - k
by XREAL_1:11;
A23:
(((StepTimes a,J,s) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) + k = s . a
by A4, A5, A21, Th17;
A24:
k + 1
<= sa
by A21, NAT_1:13;
then A25:
(k + 1) - (k + 1) <= (s . a) - (k + 1)
by XREAL_1:11;
A26:
(((StepTimes a,J,s) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) + (k + 1) = s . a
by A4, A5, A24, Th17;
then A27:
s . a = ((((StepTimes a,J,s) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) + 1) + k
;
A28:
f . ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialized (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))) . (k + 1)) =
abs (((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialized (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))))
by A18
.=
((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))
by A20, A26, A25, ABSVALUE:def 1
;
f . ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialized (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))) . k) =
abs (((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialized (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))))
by A18
.=
((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))
by A19, A23, A22, ABSVALUE:def 1
;
hence
( not
f . ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialized (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))) . k) <= f . ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialized (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))) . (k + 1)) or
((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialized (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) <= 0 )
by A23, A27, A28, NAT_1:13;
verum end; suppose
k >= s . a
;
( not f . ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialized (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))) . k) <= f . ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialized (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))) . (k + 1)) or ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialized (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized 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 ))),(Initialized (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))) . k) <= f . ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialized (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))) . (k + 1)) or
((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialized (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) <= 0 )
by A1, A4, A5, A6, A19, Th18;
verum end;
end;
A29:
ProperBodyWhile>0 1 -stRWNotIn ({a} \/ (UsedIntLoc J)),J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 )), Initialized (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))
proof
let k be
Element of
NAT ;
SCMFSA9A:def 4 ( ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialized (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized 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 ))),(Initialized (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized 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 ))),(Initialized (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))) . k ) )
assume A30:
((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialized (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) > 0
;
( 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 ))),(Initialized (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized 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 ))),(Initialized (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))) . k )
A31:
DataPart ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialized (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized 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),(Initialized s))) . k)
by A2, A7, SCMFSA9A:40;
then A32:
((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) = ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialized (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))
by SCMFSA6A:38;
then A33:
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),(Initialized s))) . k
by A7, 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 ))),(Initialized (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))) . k
by A31, SCMFSA8B:6;
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 ))),(Initialized (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized 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),(Initialized s))) . k
by A7, A30, A32, SCMFSA9A:def 4;
hence
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 ))),(Initialized (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))) . k
by A31, A33, SCMFSA8B:8;
verum
end;
then consider K being Element of NAT such that
A34:
ExitsAtWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialized (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))) = K
and
A35:
((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialized (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))) . K) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) <= 0
and
A36:
for i being Element of NAT st ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialized (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))) . i) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) <= 0 holds
K <= i
and
DataPart (Comput (ProgramPart ((Initialized (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))) +* ((while>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))),((Initialized (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))) +* ((while>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 )))) +* (Start-At 0 ,SCM+FSA ))),(LifeSpan (ProgramPart ((Initialized (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))) +* ((while>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 )))) +* (Start-At 0 ,SCM+FSA )))),((Initialized (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))) +* ((while>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 )))) +* (Start-At 0 ,SCM+FSA ))))) = DataPart ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialized (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))) . K)
by A17, SCMFSA9A:def 6;
A37:
while>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))) is_closed_on Initialized (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))
by A29, A17, SCMFSA9A:33;
while>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))) is_halting_on Initialized (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))
by A29, A17, SCMFSA9A:33;
then A38:
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),(Initialized s)
by A2, A37, SCMFSA8B:8;
A39:
DataPart (IExec (while>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 )))),(Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))) = DataPart ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialized (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))) . (ExitsAtWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialized (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))
by A29, A17, SCMFSA9A:42;
A40:
DataPart ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialized (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized 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),(Initialized s))) . K)
by A2, A7, SCMFSA9A:40;
((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) = 0
by A1, A4, A5, A6, Th18;
then
((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialized (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) = 0
by A16, SCMFSA6A:38;
then A41:
K <= k
by A36;
then A42:
(((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))) . K) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) + K = k
by A1, A4, A5, A6, Th17;
K - K <= k - K
by A41, XREAL_1:11;
then A43:
((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialized (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))) . K) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) = 0
by A35, A40, A42, SCMFSA6A:38;
A44:
(((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialized (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))) . K) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) + K = k
by A40, A42, SCMFSA6A:38;
now hereby for x being FinSeq-Location holds (IExec (times a,J),s) . x = ((StepTimes a,J,s) . k) . x
let x be
Int-Location ;
(IExec (times a,J),s) . x = ((StepTimes a,J,s) . k) . xthus (IExec (times a,J),s) . x =
(IExec (while>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 )))),(Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))) . x
by A2, A37, A38, SCMFSA8B:6, SFMASTR1:15
.=
((StepTimes a,J,s) . k) . x
by A39, A34, A16, A44, A43, SCMFSA6A:38
;
verum
end; let x be
FinSeq-Location ;
(IExec (times a,J),s) . x = ((StepTimes a,J,s) . k) . xthus (IExec (times a,J),s) . x =
(IExec (while>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 )))),(Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))) . x
by A2, A37, A38, SCMFSA8B:6, SFMASTR1:16
.=
((StepTimes a,J,s) . k) . x
by A39, A34, A16, A44, A43, SCMFSA6A:38
;
verum
hence
DataPart (IExec (times a,J),s) = DataPart ((StepTimes a,J,s) . k)
by SCMFSA6A:38; verum