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;
A4: 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 SCMFSA_M:9 ;
then A5: DataPart (Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))) = DataPart (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))) by SCMFSA_M:19;
assume A6: ( 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 A7: ProperTimesBody a,J,s,p by Th15;
A8: 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 A9: s . a < 0 ; :: thesis: ( times (a,J) is_closed_on s,p & times (a,J) is_halting_on s,p )

A10: ( a = intloc 0 or a is read-write ) by SCMFSA_M:def 2;
A11: (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, A10, SCMFSA_M:9, SCMFSA_M:37 ;
then A12: 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 A9, SCMFSA_9:38;
then A13: times (a,J) is_closed_on Initialized s,p by A3, A4, 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 A9, A11, SCMFSA_9:38;
then times (a,J) is_halting_on Initialized s,p by A3, A8, A12, SFMASTR1:3;
hence times (a,J) is_halting_on s,p by A1, A13, Th5; :: thesis: verum

end;

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

A15: 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 A16: k < s . a by A1, A7, A2, A14, Th18;
then A17: ((StepTimes (a,J,p,s)) . k) . (intloc 0) = 1 by A6, Th15, Th16;
then A18: DataPart ((StepTimes (a,J,p,s)) . k) = DataPart (Initialized ((StepTimes (a,J,p,s)) . k)) by SCMFSA_M:19;
A19: J is_closed_on (StepTimes (a,J,p,s)) . k,p +* (times* (a,J)) by A7, A16, Def4;
then A20: J is_closed_on Initialized ((StepTimes (a,J,p,s)) . k),p +* (times* (a,J)) by A17, Th4;
J is_halting_on (StepTimes (a,J,p,s)) . k,p +* (times* (a,J)) by A7, A16, Def4;
then A21: J is_halting_on Initialized ((StepTimes (a,J,p,s)) . k),p +* (times* (a,J)) by A19, A17, Th5;
A22: 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 A23: J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))) is_closed_on Initialized ((StepTimes (a,J,p,s)) . k),p +* (times* (a,J)) by A20, A21, 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 A18, 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 A20, A21, A22, 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 A18, A23, SCMFSA8B:5; :: thesis: verum

end;

A24: 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 A14, 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_Values_of SCM+FSA)),NAT such that
A25: for x being Element of product (the_Values_of SCM+FSA) holds f . x = H₁(x) from FUNCT_2:sch 4();
A26: 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_Values_of SCM+FSA) by CARD_3:107;
f . x = H₁(x) by A25;
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 A5, A15, 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 -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 SCMFSA_M:2;
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 A5, A15, SCMFSA9A:34;
then A28: ((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 SCMFSA_M:2;

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

suppose A29: 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 A30: k - k < (s . a) - k by XREAL_1:9;
A31: (((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) + k = s . a by A1, A7, A29, Th17;
A32: k + 1 <= sa by A29, NAT_1:13;
then A33: (k + 1) - (k + 1) <= (s . a) - (k + 1) by XREAL_1:9;
A34: (((StepTimes (a,J,p,s)) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) + (k + 1) = s . a by A1, A7, A32, Th17;
then A35: s . a = ((((StepTimes (a,J,p,s)) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) + 1) + k ;
A36: 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 A26
.= ((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 A28, A34, A33, 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 A26
.= ((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 A27, A31, A30, 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 A31, A35, A36, 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, A7, A2, A14, A27, Th18; :: thesis: verum

end;

end;

end;

A37: 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 A38: ((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)))))) )
A39: 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 A5, A15, SCMFSA9A:34;
then A40: ((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 SCMFSA_M:2;
then A41: 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 A15, A38, 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 A39, 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 A15, A38, A40, 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 A39, A41, SCMFSA8B:5; :: thesis: verum

end;

then A42: 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 A5, A24, SCMFSA8B:3, SCMFSA9A:27;
A43: times (a,J) is_closed_on Initialized s,p by A3, A42, A4, 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 A37, A24, 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 A5, SCMFSA8B:5;
then times (a,J) is_halting_on Initialized s,p by A3, A8, A42, SFMASTR1:3;
hence times (a,J) is_halting_on s,p by A1, A43, Th5; :: thesis: verum

end;

end;