let s be State of SCM+FSA; :: thesis: for p being Instruction-Sequence of SCM+FSA
for a being Int-Location
for J being really-closed good MacroInstruction of SCM+FSA st s . (intloc 0) = 1 & ( ProperTimesBody a,J,s,p or J is parahalting ) holds
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 really-closed good MacroInstruction of SCM+FSA st s . (intloc 0) = 1 & ( ProperTimesBody a,J,s,p or J is parahalting ) holds
times (a,J) is_halting_on s,p
let a be Int-Location; :: thesis: for J being really-closed good MacroInstruction of SCM+FSA st s . (intloc 0) = 1 & ( ProperTimesBody a,J,s,p or J is parahalting ) holds
times (a,J) is_halting_on s,p
let J be really-closed good MacroInstruction of SCM+FSA ; :: thesis: ( s . (intloc 0) = 1 & ( ProperTimesBody a,J,s,p or J is parahalting ) implies 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_halting_on s,p )
set taI = times (a,J);
set ST = StepTimes (a,J,p,s);
set au = 1 -stRWNotIn ({a} \/ (UsedILoc J));
set ISu = J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)));
set WH = while>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))));
set s1 = Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s));
set Is1 = Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)));
set SW = StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))));
set ISW = StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))));
A2: Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)) = IExec ((Macro ((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a)),p,s) by SCMFSA6C:5;
(Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))) . (intloc 0) = (Initialized s) . (intloc 0) by SCMFSA_2:63
.= 1 by SCMFSA_M:9 ;
then A3: DataPart (Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))) = DataPart (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))) by SCMFSA_M:19;
assume A4: ( ProperTimesBody a,J,s,p or J is parahalting ) ; :: thesis: times (a,J) is_halting_on s,p
then A5: ProperTimesBody a,J,s,p by Th11;
A6: Macro ((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a) is_halting_on Initialized s,p by SCMFSA7B:19;

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

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

A8: ( a = intloc 0 or a is read-write ) by SCMFSA_M:def 2;
A9: (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) = (Initialized s) . a by SCMFSA_2:63
.= s . a by A1, A8, SCMFSA_M:9, SCMFSA_M:37 ;
while>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0))))) is_halting_on Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)),p by A7, A9, SCMFSA_9:38;
then times (a,J) is_halting_on Initialized s,p by A2, A6, SFMASTR1:3;
hence times (a,J) is_halting_on s,p by A1, SCMFSA8B:42; :: thesis: verum

end;

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

A11: ProperBodyWhile>0 1 -stRWNotIn ({a} \/ (UsedILoc J)),J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0))), Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)),p

proof

let k be Nat; :: according to SCMFSA9A:def 4 :: thesis: ( ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))))) . k) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) <= 0 or J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0))) is_halting_on (StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))))) . k,p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))))) )
assume ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))))) . k) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) > 0 ; :: thesis: J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0))) is_halting_on (StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))))) . k,p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0))))))
then A12: k < s . a by A1, A5, A10, Th14;
then A13: ((StepTimes (a,J,p,s)) . k) . (intloc 0) = 1 by A4, Th11, Th12;
then A14: DataPart ((StepTimes (a,J,p,s)) . k) = DataPart (Initialized ((StepTimes (a,J,p,s)) . k)) by SCMFSA_M:19;
J is_halting_on (StepTimes (a,J,p,s)) . k,p +* (times* (a,J)) by A5, A12;
then A15: J is_halting_on Initialized ((StepTimes (a,J,p,s)) . k),p +* (times* (a,J)) by A13, SCMFSA8B:42;
Macro (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc 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} \/ (UsedILoc J))),(intloc 0))) is_halting_on Initialized ((StepTimes (a,J,p,s)) . k),p +* (times* (a,J)) by A15, SFMASTR1:3;
hence J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0))) is_halting_on (StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))))) . k,p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))))) by A14, SCMFSA8B:5; :: thesis: verum

end;

A16: WithVariantWhile>0 1 -stRWNotIn ({a} \/ (UsedILoc J)),J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0))), Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))),p

proof

reconsider sa = s . a as Element of NAT by A10, INT_1:3;
deffunc H₁( State of SCM+FSA) -> Element of NAT = |.($1 . (1 -stRWNotIn ({a} \/ (UsedILoc J)))).|;
consider f being Function of (product (the_Values_of SCM+FSA)),NAT such that
A17: for x being Element of product (the_Values_of SCM+FSA) holds f . x = H₁(x) from FUNCT_2:sch 4();
A18: 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 A17;
hence f . x = H₁(x) ; :: thesis: verum

end;

take f ; :: according to SCMFSA9A:def 5 :: thesis: for b₁ being set holds
( not f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . b₁) <= f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . (b₁ + 1)) or ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . b₁) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) <= 0 )
let k be Nat; :: thesis: ( not f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . k) <= f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . (k + 1)) or ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . k) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) <= 0 )
DataPart ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . k) = DataPart ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))))) . k) by A3, A11, SCMFSA9A:34;
then A19: ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . k) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) = ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))))) . k) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) by SCMFSA_M:2;
DataPart ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . (k + 1)) = DataPart ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))))) . (k + 1)) by A3, A11, SCMFSA9A:34;
then A20: ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) = ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))))) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) by SCMFSA_M:2;

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

suppose A21: k < s . a ; :: thesis: ( not f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . k) <= f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . (k + 1)) or ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . k) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) <= 0 )

then A22: k - k < (s . a) - k by XREAL_1:9;
A23: (((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedILoc J)))) + k = s . a by A1, A5, A21, Th13;
A24: k + 1 <= sa by A21, NAT_1:13;
then A25: (k + 1) - (k + 1) <= (s . a) - (k + 1) by XREAL_1:9;
A26: (((StepTimes (a,J,p,s)) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedILoc J)))) + (k + 1) = s . a by A1, A5, A24, Th13;
then A27: s . a = ((((StepTimes (a,J,p,s)) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedILoc J)))) + 1) + k ;
A28: f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . (k + 1)) = |.(((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedILoc J)))).| by A18
.= ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))))) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) by A20, A26, A25, ABSVALUE:def 1 ;
f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . k) = |.(((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . k) . (1 -stRWNotIn ({a} \/ (UsedILoc J)))).| by A18
.= ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))))) . k) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) by A19, A23, A22, ABSVALUE:def 1 ;
hence ( not f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . k) <= f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . (k + 1)) or ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . k) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) <= 0 ) by A23, A27, A28, NAT_1:13; :: thesis: verum

end;

suppose k >= s . a ; :: thesis: ( not f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . k) <= f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . (k + 1)) or ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . k) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) <= 0 )

hence ( not f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . k) <= f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . (k + 1)) or ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . k) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) <= 0 ) by A1, A5, A10, A19, Th14; :: thesis: verum

end;

end;

end;

A29: ProperBodyWhile>0 1 -stRWNotIn ({a} \/ (UsedILoc J)),J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0))), Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))),p

proof

let k be Nat; :: according to SCMFSA9A:def 4 :: thesis: ( ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . k) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) <= 0 or J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0))) is_halting_on (StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . k,p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))))) )
assume A30: ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . k) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) > 0 ; :: thesis: J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0))) is_halting_on (StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . k,p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0))))))
A31: DataPart ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . k) = DataPart ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))))) . k) by A3, A11, SCMFSA9A:34;
then A32: ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))))) . k) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) = ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . k) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) by SCMFSA_M:2;
J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0))) is_halting_on (StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))))) . k,p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))))) by A11, A30, A32;
hence J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0))) is_halting_on (StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))),p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . k,p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0)))))) by A31, SCMFSA8B:5; :: thesis: verum

end;

while>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0))))) is_halting_on Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))),p by A29, A16, SCMFSA9A:27;
then while>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0))))) is_halting_on Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)),p by A3, SCMFSA8B:5;
then times (a,J) is_halting_on Initialized s,p by A2, A6, SFMASTR1:3;
hence times (a,J) is_halting_on s,p by A1, SCMFSA8B:42; :: thesis: verum

end;

end;