let s be State of SCM+FSA; :: thesis: for p being Instruction-Sequence of SCM+FSA
for a being Int-Location
for J being good Program of SCM+FSA st s . (intloc 0) = 1 & ( ProperTimesBody a,J,s,p or J is parahalting ) holds
( times (a,J) is_closed_on s,p & times (a,J) is_halting_on s,p )
let p be Instruction-Sequence 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,p or J is parahalting ) holds
( times (a,J) is_closed_on s,p & times (a,J) is_halting_on s,p )
let a be Int-Location ; :: thesis: for J being good Program of SCM+FSA st s . (intloc 0) = 1 & ( ProperTimesBody a,J,s,p or J is parahalting ) holds
( times (a,J) is_closed_on s,p & times (a,J) is_halting_on s,p )
let J be good Program of SCM+FSA; :: thesis: ( s . (intloc 0) = 1 & ( ProperTimesBody a,J,s,p or J is parahalting ) implies ( times (a,J) is_closed_on s,p & times (a,J) is_halting_on s,p ) )
set I = J;
assume A1: s . (intloc 0) = 1 ; :: thesis: ( ( not ProperTimesBody a,J,s,p & not J is parahalting ) or ( times (a,J) is_closed_on s,p & 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} \/ (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)))),p,(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)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))));
A2: StepTimes (a,J,p,s) = StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(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)),p,s) & Macro ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a) is_closed_on Initialized s,p ) by SCMFSA6C:5, SCMFSA7B:18;
B3: Macro ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a) is_halting_on Initialized s,p by SCMFSA7B:19;
(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))) . (intloc 0) = (Initialized s) . (intloc 0) by SCMFSA_2:63
.= 1 by SCMFSA6A:38 ;
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:7;
assume A5: ( ProperTimesBody a,J,s,p or J is parahalting ) ; :: thesis: ( times (a,J) is_closed_on s,p & times (a,J) is_halting_on s,p )
then A6: ProperTimesBody a,J,s,p by Th15;
A7: Macro ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a) is_halting_on Initialized s,p by SCMFSA7B:19;

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

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

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:63
.= s . a by A1, A9, SCMFSA6A:38, 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)),p by A8, SCMFSA_9:38;
then A12: times (a,J) is_closed_on Initialized s,p by A3, B3, SFMASTR1:2;
hence times (a,J) is_closed_on s,p by A1, Th4; :: thesis: times (a,J) is_halting_on s,p
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)),p by A8, A10, SCMFSA_9:38;
then times (a,J) is_halting_on Initialized s,p by A3, A7, A11, SFMASTR1:3;
hence times (a,J) is_halting_on s,p by A1, A12, Th5; :: thesis: verum

end;

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

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)),p

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)))),p,(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)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . k,p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))))) & 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)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . k,p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))))) ) )
assume ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(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)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . k,p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))))) & 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)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . k,p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))))) )
then A15: k < s . a by A1, A6, A2, A13, Th18;
then A16: ((StepTimes (a,J,p,s)) . k) . (intloc 0) = 1 by A5, Th15, Th16;
then A17: DataPart ((StepTimes (a,J,p,s)) . k) = DataPart (Initialized ((StepTimes (a,J,p,s)) . k)) by SCMFSA8C:7;
A18: J is_closed_on (StepTimes (a,J,p,s)) . k,p +* (times* (a,J)) by A6, A15, Def4;
then A19: J is_closed_on Initialized ((StepTimes (a,J,p,s)) . k),p +* (times* (a,J)) by A16, Th4;
J is_halting_on (StepTimes (a,J,p,s)) . k,p +* (times* (a,J)) by A6, A15, Def4;
then A20: J is_halting_on Initialized ((StepTimes (a,J,p,s)) . k),p +* (times* (a,J)) by A18, A16, Th5;
A21: Macro (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))) is_closed_on IExec (J,(p +* (times* (a,J))),((StepTimes (a,J,p,s)) . k)),p +* (times* (a,J)) by SCMFSA7B:18;
then A22: J ';' (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))) is_closed_on Initialized ((StepTimes (a,J,p,s)) . k),p +* (times* (a,J)) by A19, A20, SFMASTR1:2;
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)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . k,p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))))) by A17, SCMFSA8B:3; :: 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)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . k,p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))))))
Macro (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc 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} \/ (UsedIntLoc J))),(intloc 0))) is_halting_on Initialized ((StepTimes (a,J,p,s)) . k),p +* (times* (a,J)) by A19, A20, A21, SFMASTR1:3;
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)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . k,p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))))) by A17, A22, SCMFSA8B:5; :: 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))),p

proof

reconsider sa = s . a as Element of NAT by A13, INT_1:3;
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
A24: for x being Element of product the Object-Kind of SCM+FSA holds f . x = H₁(x) from FUNCT_2:sch 4();
A25: 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 CARD_3:107;
f . x = H₁(x) by A24;
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)))),p,(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)))),p,(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)))),p,(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)))),p,(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)))),p,(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)))),p,(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)))),p,(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)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . k) by A4, A14, SCMFSA9A:34;
then A26: ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(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)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) by SCMFSA6A:7;
DataPart ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(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)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . (k + 1)) by A4, A14, SCMFSA9A:34;
then A27: ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(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)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) by SCMFSA6A:7;

per cases ( k < s . a or k >= s . a ) ;

suppose A28: k < s . a ; :: thesis: ( not f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(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)))),p,(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)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) <= 0 )

then A29: k - k < (s . a) - k by XREAL_1:9;
A30: (((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) + k = s . a by A1, A6, A28, Th17;
A31: k + 1 <= sa by A28, NAT_1:13;
then A32: (k + 1) - (k + 1) <= (s . a) - (k + 1) by XREAL_1:9;
A33: (((StepTimes (a,J,p,s)) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) + (k + 1) = s . a by A1, A6, A31, Th17;
then A34: s . a = ((((StepTimes (a,J,p,s)) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) + 1) + k ;
A35: f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(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)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) by A25
.= ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) by A27, A33, A32, ABSVALUE:def 1 ;
f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(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)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) by A25
.= ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) by A26, A30, A29, ABSVALUE:def 1 ;
hence ( not f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(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)))),p,(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)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) <= 0 ) by A30, A34, A35, 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)))),p,(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)))),p,(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)))),p,(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)))),p,(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)))),p,(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)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) <= 0 ) by A1, A6, A2, A13, A26, Th18; :: thesis: verum

end;

end;

end;

A36: 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))),p

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)))),p,(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)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . k,p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))))) & 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)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . k,p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))))) ) )
assume A37: ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(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)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . k,p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))))) & 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)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . k,p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))))) )
A38: DataPart ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(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)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . k) by A4, A14, SCMFSA9A:34;
then A39: ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))),p,(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)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) by SCMFSA6A:7;
then A40: 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)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . k,p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))))) by A14, A37, 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)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . k,p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))))) by A38, SCMFSA8B:3; :: 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)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . k,p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))))))
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)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))) . k,p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))))) by A14, A37, A39, 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)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))))) . k,p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))))) by A38, A40, SCMFSA8B:5; :: thesis: verum

end;

then A41: 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)),p by A4, A23, SCMFSA8B:3, SCMFSA9A:27;
A42: times (a,J) is_closed_on Initialized s,p by A3, A41, B3, SFMASTR1:2;
hence times (a,J) is_closed_on s,p by A1, Th4; :: thesis: times (a,J) is_halting_on s,p
( 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))),p & 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))),p ) by A36, A23, SCMFSA9A:27;
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)),p by A4, SCMFSA8B:5;
then times (a,J) is_halting_on Initialized s,p by A3, A7, A41, SFMASTR1:3;
hence times (a,J) is_halting_on s,p by A1, A42, Th5; :: thesis: verum

end;

end;