let s be State of SCM+FSA; :: thesis: for p being Instruction-Sequence of SCM+FSA
for a being Int-Location
for k being Nat
for J being really-closed good MacroInstruction of SCM+FSA st s . a = k & ( ProperTimesBody a,J,s,p or J is parahalting ) & ( s . (intloc 0) = 1 or a is read-write ) 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 k being Nat
for J being really-closed good MacroInstruction of SCM+FSA st s . a = k & ( ProperTimesBody a,J,s,p or J is parahalting ) & ( s . (intloc 0) = 1 or a is read-write ) holds
DataPart (IExec ((times (a,J)),p,s)) = DataPart ((StepTimes (a,J,p,s)) . k)
let a be Int-Location; :: thesis: for k being Nat
for J being really-closed good MacroInstruction of SCM+FSA st s . a = k & ( ProperTimesBody a,J,s,p or J is parahalting ) & ( s . (intloc 0) = 1 or a is read-write ) holds
DataPart (IExec ((times (a,J)),p,s)) = DataPart ((StepTimes (a,J,p,s)) . k)
let k be Nat; :: thesis: for J being really-closed good MacroInstruction of SCM+FSA st s . a = k & ( ProperTimesBody a,J,s,p or J is parahalting ) & ( s . (intloc 0) = 1 or a is read-write ) holds
DataPart (IExec ((times (a,J)),p,s)) = DataPart ((StepTimes (a,J,p,s)) . k)
let J be really-closed good MacroInstruction of SCM+FSA ; :: thesis: ( s . a = k & ( ProperTimesBody a,J,s,p or J is parahalting ) & ( s . (intloc 0) = 1 or a is read-write ) 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 & not a is read-write ) 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} \/ (UsedILoc J));
reconsider ISu = J ";" (SubFrom ((1 -stRWNotIn ({a} \/ (UsedILoc J))),(intloc 0))) as really-closed MacroInstruction of SCM+FSA ;
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))),ISu,p,(Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))));
set ISW = StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu,p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))));
(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 A2: 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;
set WH = while>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu);
assume A3: ( ProperTimesBody a,J,s,p or J is parahalting ) ; :: thesis: ( ( not s . (intloc 0) = 1 & not a is read-write ) or DataPart (IExec ((times (a,J)),p,s)) = DataPart ((StepTimes (a,J,p,s)) . k) )
then A4: ProperTimesBody a,J,s,p by Th11;
assume A5: ( s . (intloc 0) = 1 or a is read-write ) ; :: thesis: DataPart (IExec ((times (a,J)),p,s)) = DataPart ((StepTimes (a,J,p,s)) . k)
A6: ProperBodyWhile>0 1 -stRWNotIn ({a} \/ (UsedILoc J)),ISu, 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))),ISu,p,(Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))))) . k) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) <= 0 or ISu is_halting_on (StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu,p,(Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))))) . k,p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu)) )
assume ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu,p,(Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))))) . k) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) > 0 ; :: thesis: ISu is_halting_on (StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu,p,(Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))))) . k,p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu))
then A7: k < s . a by A1, A4, A5, Th14;
then A8: ((StepTimes (a,J,p,s)) . k) . (intloc 0) = 1 by A3, Th11, Th12;
then A9: 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 A4, A7;
then A10: J is_halting_on Initialized ((StepTimes (a,J,p,s)) . k),p +* (times* (a,J)) by A8, 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 ISu is_halting_on Initialized ((StepTimes (a,J,p,s)) . k),p +* (times* (a,J)) by A10, SFMASTR1:3;
hence ISu is_halting_on (StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu,p,(Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))))) . k,p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu)) by A9, SCMFSA8B:5; :: thesis: verum
end;
then A11: DataPart ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu,p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . k) = DataPart ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu,p,(Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))))) . k) by A2, SCMFSA9A:34;
A12: WithVariantWhile>0 1 -stRWNotIn ({a} \/ (UsedILoc J)),ISu, Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))),p
proof
reconsider sa = s . a as Element of NAT by A1, ORDINAL1:def 12;
deffunc H1( 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
A13: for x being Element of product (the_Values_of SCM+FSA) holds f . x = H1(x) from FUNCT_2:sch 4();
 A14: 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_Values_of SCM+FSA) by CARD_3:107;
f . x = H1(x) by A13;
hence f . x = H1(x) ; :: thesis: verum
end;
take f ; :: according to SCMFSA9A:def 5 :: thesis: for b1 being set holds
( not f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu,p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . b1) <= f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu,p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . (b1 + 1)) or ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu,p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . b1) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) <= 0 )
let k be Nat; :: thesis: ( not f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu,p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . k) <= f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu,p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . (k + 1)) or ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu,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))),ISu,p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . k) = DataPart ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu,p,(Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))))) . k) by A2, A6, SCMFSA9A:34;
then A15: ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu,p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . k) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) = ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu,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))),ISu,p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . (k + 1)) = DataPart ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu,p,(Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))))) . (k + 1)) by A2, A6, SCMFSA9A:34;
then A16: ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu,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))),ISu,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 A17: k < s . a ; :: thesis: ( not f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu,p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . k) <= f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu,p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . (k + 1)) or ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu,p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . k) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) <= 0 )
then A18: k - k < (s . a) - k by XREAL_1:9;
A19: (((StepTimes (a,J,p,s)) . k) . (1 -stRWNotIn ({a} \/ (UsedILoc J)))) + k = s . a by A4, A5, A17, Th13;
A20: k + 1 <= sa by A17, NAT_1:13;
then A21: (k + 1) - (k + 1) <= (s . a) - (k + 1) by XREAL_1:9;
A22: (((StepTimes (a,J,p,s)) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedILoc J)))) + (k + 1) = s . a by A4, A5, A20, Th13;
then A23: s . a = ((((StepTimes (a,J,p,s)) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedILoc J)))) + 1) + k ;
A24: f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu,p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . (k + 1)) = |.(((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu,p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedILoc J)))).| by A14
.= ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu,p,(Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))))) . (k + 1)) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) by A16, A22, A21, ABSVALUE:def 1 ;
f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu,p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . k) = |.(((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu,p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . k) . (1 -stRWNotIn ({a} \/ (UsedILoc J)))).| by A14
.= ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu,p,(Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))))) . k) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) by A15, A19, A18, ABSVALUE:def 1 ;
hence ( not f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu,p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . k) <= f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu,p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . (k + 1)) or ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu,p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . k) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) <= 0 ) by A19, A23, A24, NAT_1:13; :: thesis: verum
end;
suppose k >= s . a ; :: thesis: ( not f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu,p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . k) <= f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu,p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . (k + 1)) or ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu,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))),ISu,p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . k) <= f . ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu,p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . (k + 1)) or ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu,p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . k) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) <= 0 ) by A1, A4, A5, A15, Th14; :: thesis: verum
end;
end;
end;
A25: ProperBodyWhile>0 1 -stRWNotIn ({a} \/ (UsedILoc J)),ISu, 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))),ISu,p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . k) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) <= 0 or ISu is_halting_on (StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu,p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . k,p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu)) )
assume A26: ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu,p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . k) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) > 0 ; :: thesis: ISu is_halting_on (StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu,p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . k,p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu))
A27: DataPart ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu,p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . k) = DataPart ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu,p,(Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))))) . k) by A2, A6, SCMFSA9A:34;
then A28: ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu,p,(Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))))) . k) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) = ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu,p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . k) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) by SCMFSA_M:2;
ISu is_halting_on (StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu,p,(Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))))) . k,p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu)) by A6, A26, A28;
hence ISu is_halting_on (StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu,p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . k,p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu)) by A27, SCMFSA8B:5; :: thesis: verum
end;
then consider K being Nat such that
A29: ExitsAtWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu,p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))))) = K and
A30: ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu,p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . K) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) <= 0 and
A31: for i being Nat st ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu,p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . i) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) <= 0 holds
K <= i and
DataPart (Comput ((p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu))),(Initialize (Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))))),(LifeSpan ((p +* (while>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu))),(Initialize (Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))))))))) = DataPart ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu,p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . K) by A12, SCMFSA9A:def 6;
while>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu) is_halting_on Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))),p by A25, A12, SCMFSA9A:27;
then A32: while>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu) is_halting_on Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)),p by A2, SCMFSA8B:5;
A33: DataPart (IExec ((while>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu)),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))))) = DataPart ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu,p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . (ExitsAtWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu,p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))))))) by A25, A12, SCMFSA9A:36;
A34: DataPart ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu,p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . K) = DataPart ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu,p,(Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))))) . K) by A2, A6, SCMFSA9A:34;
((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu,p,(Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))))) . k) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) = 0 by A1, A4, A5, Th14;
then ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu,p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . k) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) = 0 by A11, SCMFSA_M:2;
then A35: K <= k by A31;
then A36: (((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu,p,(Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))))) . K) . (1 -stRWNotIn ({a} \/ (UsedILoc J)))) + K = k by A1, A4, A5, Th13;
K - K <= k - K by A35, XREAL_1:9;
then A37: ((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu,p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . K) . (1 -stRWNotIn ({a} \/ (UsedILoc J))) = 0 by A30, A34, A36, SCMFSA_M:2;
A38: (((StepWhile>0 ((1 -stRWNotIn ({a} \/ (UsedILoc J))),ISu,p,(Initialized (Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s)))))) . K) . (1 -stRWNotIn ({a} \/ (UsedILoc J)))) + K = k by A34, A36, SCMFSA_M:2;
A39: now :: thesis: for x being Int-Location holds (IExec ((times (a,J)),p,s)) . x = ((StepTimes (a,J,p,s)) . k) . x
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} \/ (UsedILoc J))),ISu)),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))))) . x by A32, SFMASTR1:14
.= ((StepTimes (a,J,p,s)) . k) . x by A33, A29, A11, A38, A37, SCMFSA_M:2 ; :: thesis: verum
end;
now :: thesis: for x being FinSeq-Location holds (IExec ((times (a,J)),p,s)) . x = ((StepTimes (a,J,p,s)) . k) . x
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} \/ (UsedILoc J))),ISu)),p,(Exec (((1 -stRWNotIn ({a} \/ (UsedILoc J))) := a),(Initialized s))))) . x by A32, SFMASTR1:15
.= ((StepTimes (a,J,p,s)) . k) . x by A33, A29, A11, A38, A37, SCMFSA_M:2 ; :: thesis: verum
end;
hence DataPart (IExec ((times (a,J)),p,s)) = DataPart ((StepTimes (a,J,p,s)) . k) by A39, SCMFSA_M:2; :: thesis: verum