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),(Initialize s);
set Is1 = Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s));
set SW = StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s));
set ISW = StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)));
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),(Initialize s)) ;
A3: ( Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s) = IExec (Macro ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a)),s & Macro ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a) is_closed_on Initialize s ) by SCMFSA6C:6, SCMFSA7B:24;
(Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)) . (intloc 0 ) = (Initialize s) . (intloc 0 ) by SCMFSA_2:89
.= 1 by SCMFSA6C:3 ;
then A4: DataPart (Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s))) = DataPart (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize 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 Initialize 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),(Initialize s)) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) = (Initialize 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),(Initialize s) by A8, SCMFSA_9:43;
then A12: times a,J is_closed_on Initialize 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),(Initialize s) by A8, A10, SCMFSA_9:43;
then times a,J is_halting_on Initialize 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),(Initialize s)

proof

let k be Element of NAT ; :: according to SCMFSA9A:def 4 :: thesis: ( ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) <= 0 or ( J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 )) is_closed_on (StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s))) . k & J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 )) is_halting_on (StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s))) . k ) )
assume ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) > 0 ; :: thesis: ( J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 )) is_closed_on (StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s))) . k & J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 )) is_halting_on (StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s))) . k )
then 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 (Initialize ((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 Initialize ((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 Initialize ((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 Initialize ((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),(Initialize 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),(Initialize 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 Initialize ((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),(Initialize 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 )), Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize 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 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . b₁) <= f . ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . (b₁ + 1)) or ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . 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 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . k) <= f . ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . (k + 1)) or ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) <= 0 )
DataPart ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . k) = DataPart ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s))) . k) by A4, A14, SCMFSA9A:40;
then A25: ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) = ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) by SCMFSA6A:38;
DataPart ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . (k + 1)) = DataPart ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s))) . (k + 1)) by A4, A14, SCMFSA9A:40;
then A26: ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) = ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s))) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) by SCMFSA6A:38;

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

suppose A27: k < s . a ; :: thesis: ( not f . ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . k) <= f . ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . (k + 1)) or ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) <= 0 )

then 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 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . (k + 1)) = abs (((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) by A24
.= ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s))) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) by A26, A32, A31, ABSVALUE:def 1 ;
f . ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . k) = abs (((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) by A24
.= ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) by 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 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . k) <= f . ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . (k + 1)) or ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) <= 0 ) by 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 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . k) <= f . ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . (k + 1)) or ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) <= 0 )

hence ( not f . ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . k) <= f . ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . (k + 1)) or ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) <= 0 ) by A1, 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 )), Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s))

proof

let k be Element of NAT ; :: according to SCMFSA9A:def 4 :: thesis: ( ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) <= 0 or ( J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 )) is_closed_on (StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . k & J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 )) is_halting_on (StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . k ) )
assume A36: ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) > 0 ; :: thesis: ( J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 )) is_closed_on (StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . k & J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 )) is_halting_on (StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . k )
A37: DataPart ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . k) = DataPart ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s))) . k) by 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),(Initialize s))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) = ((StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) by SCMFSA6A:38;
then 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),(Initialize 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 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize 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 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)))) . k
J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 )) is_halting_on (StepWhile>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))),(Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize 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 ))),(Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize 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),(Initialize s) by A4, A23, SCMFSA8B:6, SCMFSA9A:33;
then A41: times a,J is_closed_on Initialize 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 Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)) & while>0 (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom (1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0 ))) is_halting_on Initialize (Exec ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialize s)) ) by 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),(Initialize s) by A4, SCMFSA8B:8;
then times a,J is_halting_on Initialize s by A3, A7, A40, SFMASTR1:4;
hence times a,J is_halting_on s by A1, A41, Th5; :: thesis: verum

end;

end;