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
for k being Element of NAT st s . a = k & ( ProperTimesBody a,J,s,p or J is parahalting ) & ( s . (intloc 0) = 1 or not a is read-only ) holds
DataPart (IExec ((times (a,J)),p,s)) = DataPart ((StepTimes (a,J,p,s)) . k)
let p be Instruction-Sequence of SCM+FSA; :: thesis: for a being Int-Location
for J being good Program of SCM+FSA
for k being Element of NAT st s . a = k & ( ProperTimesBody a,J,s,p or J is parahalting ) & ( s . (intloc 0) = 1 or not a is read-only ) holds
DataPart (IExec ((times (a,J)),p,s)) = DataPart ((StepTimes (a,J,p,s)) . k)
let a be Int-Location ; :: thesis: for J being good Program of SCM+FSA
for k being Element of NAT st s . a = k & ( ProperTimesBody a,J,s,p or J is parahalting ) & ( s . (intloc 0) = 1 or not a is read-only ) holds
DataPart (IExec ((times (a,J)),p,s)) = DataPart ((StepTimes (a,J,p,s)) . k)
let J be good Program of SCM+FSA; :: thesis: for k being Element of NAT st s . a = k & ( ProperTimesBody a,J,s,p or J is parahalting ) & ( s . (intloc 0) = 1 or not a is read-only ) holds
DataPart (IExec ((times (a,J)),p,s)) = DataPart ((StepTimes (a,J,p,s)) . k)
let k be Element of NAT ; :: thesis: ( s . a = k & ( ProperTimesBody a,J,s,p or J is parahalting ) & ( s . (intloc 0) = 1 or not a is read-only ) implies DataPart (IExec ((times (a,J)),p,s)) = DataPart ((StepTimes (a,J,p,s)) . k) )
set I = J;
assume A1: s . a = k ; :: thesis: ( ( not ProperTimesBody a,J,s,p & not J is parahalting ) or ( not s . (intloc 0) = 1 & a is read-only ) or DataPart (IExec ((times (a,J)),p,s)) = DataPart ((StepTimes (a,J,p,s)) . k) )
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 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)))));
(Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))) . (intloc 0) = (Initialized s) . (intloc 0) by SCMFSA_2:63
.= 1 by SCMFSA6A:38 ;
then A2: DataPart (Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s)))) = DataPart (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))) by SCMFSA8C:7;
set WH = while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0)))));
assume A3: ( ProperTimesBody a,J,s,p or J is parahalting ) ; :: thesis: ( ( not s . (intloc 0) = 1 & a is read-only ) or DataPart (IExec ((times (a,J)),p,s)) = DataPart ((StepTimes (a,J,p,s)) . k) )
then A4: ProperTimesBody a,J,s,p by Th15;
assume A5: ( s . (intloc 0) = 1 or not a is read-only ) ; :: thesis: DataPart (IExec ((times (a,J)),p,s)) = DataPart ((StepTimes (a,J,p,s)) . k)
A6: 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)))) ;
A7: 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 A8: k < s . a by A1, A4, A5, A6, Th18;
then A9: ((StepTimes (a,J,p,s)) . k) . (intloc 0) = 1 by A3, Th15, Th16;
then A10: DataPart ((StepTimes (a,J,p,s)) . k) = DataPart (Initialized ((StepTimes (a,J,p,s)) . k)) by SCMFSA8C:7;
A11: J is_closed_on (StepTimes (a,J,p,s)) . k,p +* (times* (a,J)) by A4, A8, Def4;
then A12: J is_closed_on Initialized ((StepTimes (a,J,p,s)) . k),p +* (times* (a,J)) by A9, Th4;
J is_halting_on (StepTimes (a,J,p,s)) . k,p +* (times* (a,J)) by A4, A8, Def4;
then A13: J is_halting_on Initialized ((StepTimes (a,J,p,s)) . k),p +* (times* (a,J)) by A11, A9, Th5;
A14: 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 A15: J ';' (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))) is_closed_on Initialized ((StepTimes (a,J,p,s)) . k),p +* (times* (a,J)) by A12, A13, 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 A10, 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 A12, A13, A14, 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 A10, A15, SCMFSA8B:5; :: thesis: verum
end;
then A16: 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 A2, SCMFSA9A:34;
A17: 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 A1;
deffunc H1( 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
A18: for x being Element of product the Object-Kind of SCM+FSA holds f . x = H1(x) from FUNCT_2:sch 4();
 A19: for x being State of SCM+FSA holds f . x = H1(x)
proof
let x be State of SCM+FSA; :: thesis: f . x = H1(x)
reconsider x = x as Element of product the Object-Kind of SCM+FSA by CARD_3:107;
f . x = H1(x) by A18;
hence f . x = H1(x) ; :: thesis: verum
end;
take f ; :: according to SCMFSA9A:def 5 :: thesis: for b1 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)))))) . b1) <= 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)))))) . (b1 + 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)))))) . b1) . (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 A2, A7, SCMFSA9A:34;
then A20: ((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 A2, A7, SCMFSA9A:34;
then A21: ((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 A22: 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 A23: k - k < (s . a) - k by XREAL_1:9;
A24: (((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) + k = s . a by A4, A5, A22, Th17;
A25: k + 1 <= sa by A22, NAT_1:13;
then A26: (k + 1) - (k + 1) <= (s . a) - (k + 1) by XREAL_1:9;
A27: (((StepTimes (a,J,p,s)) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) + (k + 1) = s . a by A4, A5, A25, Th17;
then A28: s . a = ((((StepTimes (a,J,p,s)) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J)))) + 1) + k ;
A29: 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 A19
.= ((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 A21, A27, A26, 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 A19
.= ((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 A20, A24, A23, 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 A24, A28, A29, 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, A4, A5, A6, A20, Th18; :: thesis: verum
end;
end;
end;
A30: 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 A31: ((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)))))) )
A32: 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 A2, A7, SCMFSA9A:34;
then A33: ((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 A34: 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 A7, A31, 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 A32, 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 A7, A31, A33, 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 A32, A34, SCMFSA8B:5; :: thesis: verum
end;
then consider K being Element of NAT such that
A35: ExitsAtWhile>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 and
A36: ((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 and
A37: for i being Element of NAT st ((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)))))) . i) . (1 -stRWNotIn ({a} \/ (UsedIntLoc J))) <= 0 holds
K <= i and
DataPart (Comput ((p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))))))),(Initialize (Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))),(LifeSpan ((p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(J ';' (SubFrom ((1 -stRWNotIn ({a} \/ (UsedIntLoc J))),(intloc 0))))))),(Initialize (Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedIntLoc J))) := a),(Initialized s))))))))) = 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) by A17, SCMFSA9A:def 6;
A38: 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 by A30, A17, SCMFSA9A:27;
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 A30, A17, SCMFSA9A:27;
then A39: 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 A2, A38, SCMFSA8B:5;
A40: DataPart (IExec ((while>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))))) = 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)))))) . (ExitsAtWhile>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))))))) by A30, A17, SCMFSA9A:36;
A41: 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 A2, A7, SCMFSA9A:34;
((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 by A1, A4, A5, A6, Th18;
then ((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 A16, SCMFSA6A:7;
then A42: K <= k by A37;
then A43: (((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)))) + K = k by A1, A4, A5, A6, Th17;
K - K <= k - K by A42, XREAL_1:9;
then A44: ((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 A36, A41, A43, SCMFSA6A:7;
A45: (((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)))) + K = k by A41, A43, SCMFSA6A:7;
A46: now
let x be Int-Location ; :: thesis: (IExec ((times (a,J)),p,s)) . x = ((StepTimes (a,J,p,s)) . k) . x
thus (IExec ((times (a,J)),p,s)) . x = (IExec ((while>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))))) . x by A2, A38, A39, SCMFSA8B:3, SFMASTR1:14
.= ((StepTimes (a,J,p,s)) . k) . x by A40, A35, A16, A45, A44, SCMFSA6A:7 ; :: thesis: verum
end;
now
let x be FinSeq-Location ; :: thesis: (IExec ((times (a,J)),p,s)) . x = ((StepTimes (a,J,p,s)) . k) . x
thus (IExec ((times (a,J)),p,s)) . x = (IExec ((while>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))))) . x by A2, A38, A39, SCMFSA8B:3, SFMASTR1:15
.= ((StepTimes (a,J,p,s)) . k) . x by A40, A35, A16, A45, A44, SCMFSA6A:7 ; :: thesis: verum
end;
hence DataPart (IExec ((times (a,J)),p,s)) = DataPart ((StepTimes (a,J,p,s)) . k) by A46, SCMFSA6A:7; :: thesis: verum