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 ) )
set taI = times (a,J);
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 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),(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)))));
A2: 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)))) ;
A3: ( Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)) = IExec ((Macro ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a)),s) & Macro ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a) is_closed_on Initialized s ) by SCMFSA6C:6, SCMFSA7B:24;
(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))) . (intloc 0) = (Initialized s) . (intloc 0) by SCMFSA_2:89
.= 1 by SCMFSA6C:3 ;
then A4: DataPart (Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))) = DataPart (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))) by SCMFSA8C:27;
assume A5: ( ProperTimesBody a,J,s or J is parahalting ) ; :: thesis: ( times (a,J) is_closed_on s & times (a,J) is_halting_on s )
then A6: ProperTimesBody a,J,s by Th15;
A7: Macro ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a) is_halting_on Initialized s by SCMFSA7B:25;

per cases ( s . a < 0 or 0 <= s . a ) ;

suppose A8: s . a < 0 ; :: thesis: ( times (a,J) is_closed_on s & times (a,J) is_halting_on s )

A9: ( a = intloc 0 or not a is read-only ) by SF_MASTR:def 5;
A10: (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) = (Initialized s) . a by SCMFSA_2:89
.= s . a by A1, A9, SCMFSA6C:3 ;
then A11: 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),(Initialized s)) by A8, SCMFSA_9:43;
then A12: times (a,J) is_closed_on Initialized s by A3, A7, SFMASTR1:3;
hence times (a,J) is_closed_on s by A1, Th4; :: thesis: times (a,J) is_halting_on s
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 A8, A10, SCMFSA_9:43;
then times (a,J) is_halting_on Initialized s by A3, A7, A11, SFMASTR1:4;
hence times (a,J) is_halting_on s by A1, A12, Th5; :: thesis: verum

end;

suppose A13: 0 <= s . a ; :: thesis: ( times (a,J) is_closed_on s & times (a,J) is_halting_on s )

A14: 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 ; :: 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),(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 ; :: 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),(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 A15: k < s . a by A1, A6, A2, A13, Th18;
then A16: ((StepTimes (a,J,s)) . k) . (intloc 0) = 1 by A5, Th15, Th16;
then A17: DataPart ((StepTimes (a,J,s)) . k) = DataPart (Initialized ((StepTimes (a,J,s)) . k)) by SCMFSA8C:27;
A18: J is_closed_on (StepTimes (a,J,s)) . k by A6, A15, Def3;
then A19: J is_closed_on Initialized ((StepTimes (a,J,s)) . k) by A16, Th4;
J is_halting_on (StepTimes (a,J,s)) . k by A6, A15, Def3;
then A20: J is_halting_on Initialized ((StepTimes (a,J,s)) . k) by A18, A16, Th5;
A21: Macro (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))) is_closed_on IExec (J,((StepTimes (a,J,s)) . k)) by SCMFSA7B:24;
then A22: J ';' (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))) is_closed_on Initialized ((StepTimes (a,J,s)) . k) by A19, A20, 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 A17, 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),(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 A19, A20, A21, 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 A17, A22, SCMFSA8B:8; :: thesis: verum

end;

A23: 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 A13, INT_1:16;
deffunc H₁( 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
B24: for x being Element of product the Object-Kind of SCM+FSA holds f . x = H₁(x) from FUNCT_2:sch 4();
A24: for x being State of SCM+FSA holds f . x = H₁(x)

proof

let x be State of SCM+FSA; :: thesis: f . x = H₁(x)
reconsider x = x as Element of product the Object-Kind of SCM+FSA by PBOOLE:155;
f . x = H₁(x) by B24;
hence f . x = H₁(x) ; :: thesis: verum

end;

take f ; :: according to SCMFSA9A:def 5 :: thesis: for b₁ 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)))))) . b₁) <= 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)))))) . (b₁ + 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)))))) . b₁) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) <= 0 )
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)))),(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 A4, A14, SCMFSA9A:40;
then A25: ((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 A4, A14, SCMFSA9A:40;
then A26: ((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 A27: k < s . a ; :: thesis: ( 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 A28: k - k < (s . a) - k by XREAL_1:11;
A29: (((StepTimes (a,J,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) + k = s . a by A1, A6, A27, Th17;
A30: k + 1 <= sa by A27, NAT_1:13;
then A31: (k + 1) - (k + 1) <= (s . a) - (k + 1) by XREAL_1:11;
A32: (((StepTimes (a,J,s)) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) + (k + 1) = s . a by A1, A6, A30, Th17;
then A33: s . a = ((((StepTimes (a,J,s)) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) + 1) + k ;
A34: 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 A24
.= ((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 A26, A32, A31, 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 A24
.= ((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 A25, A29, A28, 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 A29, A33, A34, 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)))),(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, A6, A2, A13, A25, Th18; :: thesis: verum

end;

end;

end;

A35: 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 ; :: according to SCMFSA9A:def 4 :: thesis: ( ((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 A36: ((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 ; :: 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)))),(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 )
A37: 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 A4, A14, SCMFSA9A:40;
then A38: ((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 A39: 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 A14, A36, 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 A37, 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)))),(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 A14, A36, A38, 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 A37, A39, SCMFSA8B:8; :: thesis: verum

end;

then A40: 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),(Initialized s)) by A4, A23, SCMFSA8B:6, SCMFSA9A:33;
then A41: times (a,J) is_closed_on Initialized s by A3, A7, SFMASTR1:3;
hence times (a,J) is_closed_on s by A1, Th4; :: thesis: times (a,J) is_halting_on s
( 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))) & 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 A35, A23, SCMFSA9A:33;
then 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 A4, SCMFSA8B:8;
then times (a,J) is_halting_on Initialized s by A3, A7, A40, SFMASTR1:4;
hence times (a,J) is_halting_on s by A1, A41, Th5; :: thesis: verum

end;

end;