let s be State of SCM+FSA; :: thesis: for p being Instruction-Sequence of SCM+FSA
for k being Nat
for a being read-write Int-Location
for J being good really-closed MacroInstruction of SCM+FSA st not J destroys a & s . a = k & ( ProperTimesBody a,J,s,p or J is parahalting ) 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 k being Nat
for a being read-write Int-Location
for J being good really-closed MacroInstruction of SCM+FSA st not J destroys a & s . a = k & ( ProperTimesBody a,J,s,p or J is parahalting ) holds
DataPart (IExec ((Times (a,J)),p,s)) = DataPart ((StepTimes (a,J,p,s)) . k)
let k be Nat; :: thesis: for a being read-write Int-Location
for J being good really-closed MacroInstruction of SCM+FSA st not J destroys a & s . a = k & ( ProperTimesBody a,J,s,p or J is parahalting ) holds
DataPart (IExec ((Times (a,J)),p,s)) = DataPart ((StepTimes (a,J,p,s)) . k)
let a be read-write Int-Location; :: thesis: for J being good really-closed MacroInstruction of SCM+FSA st not J destroys a & s . a = k & ( ProperTimesBody a,J,s,p or J is parahalting ) holds
DataPart (IExec ((Times (a,J)),p,s)) = DataPart ((StepTimes (a,J,p,s)) . k)
let J be good really-closed MacroInstruction of SCM+FSA ; :: thesis: ( not J destroys a & s . a = k & ( ProperTimesBody a,J,s,p or J is parahalting ) implies DataPart (IExec ((Times (a,J)),p,s)) = DataPart ((StepTimes (a,J,p,s)) . k) )
set I = J;
assume A1: not J destroys a ; :: thesis: ( not s . a = k or ( not ProperTimesBody a,J,s,p & not J is parahalting ) or DataPart (IExec ((Times (a,J)),p,s)) = DataPart ((StepTimes (a,J,p,s)) . k) )
assume A2: s . a = k ; :: thesis: ( ( not ProperTimesBody a,J,s,p & not J is parahalting ) or DataPart (IExec ((Times (a,J)),p,s)) = DataPart ((StepTimes (a,J,p,s)) . k) )
set ST = StepTimes (a,J,p,s);
reconsider ISu = J ";" (SubFrom (a,(intloc 0))) as really-closed MacroInstruction of SCM+FSA ;
set s1 = Initialized s;
set Is1 = Initialized (Initialized s);
set SW = StepWhile>0 (a,ISu,p,(Initialized s));
set ISW = StepWhile>0 (a,ISu,p,(Initialized (Initialized s)));
set WH = while>0 (a,ISu);
assume A3: ( ProperTimesBody a,J,s,p or J is parahalting ) ; :: thesis: DataPart (IExec ((Times (a,J)),p,s)) = DataPart ((StepTimes (a,J,p,s)) . k)
then A4: ProperTimesBody a,J,s,p by Th50;
A5: ProperBodyWhile>0 a,ISu, Initialized s,p
proof
let k be Nat; :: according to SCMFSA9A:def 4 :: thesis: ( ((StepWhile>0 (a,ISu,p,(Initialized s))) . k) . a > 0 implies ISu is_halting_on (StepWhile>0 (a,ISu,p,(Initialized s))) . k,p +* (while>0 (a,ISu)) )
assume ((StepWhile>0 (a,ISu,p,(Initialized s))) . k) . a > 0 ; :: thesis: ISu is_halting_on (StepWhile>0 (a,ISu,p,(Initialized s))) . k,p +* (while>0 (a,ISu))
then A6: k < s . a by A2, A4, Th53, A1;
then A7: ((StepTimes (a,J,p,s)) . k) . (intloc 0) = 1 by A3, Th50, Th51, A1;
then A8: 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, A6;
then A9: J is_halting_on Initialized ((StepTimes (a,J,p,s)) . k),p +* (Times (a,J)) by A7, SCMFSA8B:42;
Macro (SubFrom (a,(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 A9, SFMASTR1:3;
hence ISu is_halting_on (StepWhile>0 (a,ISu,p,(Initialized s))) . k,p +* (while>0 (a,ISu)) by A8, SCMFSA8B:5; :: thesis: verum
end;
A10: WithVariantWhile>0 a,ISu, Initialized (Initialized s),p
proof
reconsider sa = s . a as Element of NAT by A2, ORDINAL1:def 12;
deffunc H1( State of SCM+FSA) -> Element of NAT = |.($1 . a).|;
consider f being Function of (product (the_Values_of SCM+FSA)),NAT such that
A11: for x being Element of product (the_Values_of SCM+FSA) holds f . x = H1(x) from FUNCT_2:sch 4();
 A12: 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 A11;
hence f . x = H1(x) ; :: thesis: verum
end;
take f ; :: according to SCMFSA9A:def 5 :: thesis: for k being Nat holds
( f . ((StepWhile>0 (a,ISu,p,(Initialized (Initialized s)))) . (k + 1)) < f . ((StepWhile>0 (a,ISu,p,(Initialized (Initialized s)))) . k) or ((StepWhile>0 (a,ISu,p,(Initialized (Initialized s)))) . k) . a <= 0 )
let k be Nat; :: thesis: ( f . ((StepWhile>0 (a,ISu,p,(Initialized (Initialized s)))) . (k + 1)) < f . ((StepWhile>0 (a,ISu,p,(Initialized (Initialized s)))) . k) or ((StepWhile>0 (a,ISu,p,(Initialized (Initialized s)))) . k) . a <= 0 )
per cases ( k < s . a or k >= s . a ) ;
suppose A13: k < s . a ; :: thesis: ( f . ((StepWhile>0 (a,ISu,p,(Initialized (Initialized s)))) . (k + 1)) < f . ((StepWhile>0 (a,ISu,p,(Initialized (Initialized s)))) . k) or ((StepWhile>0 (a,ISu,p,(Initialized (Initialized s)))) . k) . a <= 0 )
then A14: k - k < (s . a) - k by XREAL_1:9;
A15: (((StepTimes (a,J,p,s)) . k) . a) + k = s . a by A4, A13, Th52, A1;
A16: k + 1 <= sa by A13, NAT_1:13;
then A17: (k + 1) - (k + 1) <= (s . a) - (k + 1) by XREAL_1:9;
A18: (((StepTimes (a,J,p,s)) . (k + 1)) . a) + (k + 1) = s . a by A4, A16, Th52, A1;
then A19: s . a = ((((StepTimes (a,J,p,s)) . (k + 1)) . a) + 1) + k ;
A20: f . ((StepWhile>0 (a,ISu,p,(Initialized (Initialized s)))) . (k + 1)) = |.(((StepWhile>0 (a,ISu,p,(Initialized (Initialized s)))) . (k + 1)) . a).| by A12
.= ((StepWhile>0 (a,ISu,p,(Initialized s))) . (k + 1)) . a by A18, A17, ABSVALUE:def 1 ;
f . ((StepWhile>0 (a,ISu,p,(Initialized (Initialized s)))) . k) = |.(((StepWhile>0 (a,ISu,p,(Initialized (Initialized s)))) . k) . a).| by A12
.= ((StepWhile>0 (a,ISu,p,(Initialized s))) . k) . a by A15, A14, ABSVALUE:def 1 ;
hence ( f . ((StepWhile>0 (a,ISu,p,(Initialized (Initialized s)))) . (k + 1)) < f . ((StepWhile>0 (a,ISu,p,(Initialized (Initialized s)))) . k) or ((StepWhile>0 (a,ISu,p,(Initialized (Initialized s)))) . k) . a <= 0 ) by A15, A19, A20, NAT_1:13; :: thesis: verum
end;
suppose k >= s . a ; :: thesis: ( f . ((StepWhile>0 (a,ISu,p,(Initialized (Initialized s)))) . (k + 1)) < f . ((StepWhile>0 (a,ISu,p,(Initialized (Initialized s)))) . k) or ((StepWhile>0 (a,ISu,p,(Initialized (Initialized s)))) . k) . a <= 0 )
hence ( f . ((StepWhile>0 (a,ISu,p,(Initialized (Initialized s)))) . (k + 1)) < f . ((StepWhile>0 (a,ISu,p,(Initialized (Initialized s)))) . k) or ((StepWhile>0 (a,ISu,p,(Initialized (Initialized s)))) . k) . a <= 0 ) by A2, A4, Th53, A1; :: thesis: verum
end;
end;
end;
A21: ProperBodyWhile>0 a,ISu, Initialized (Initialized s),p by A5;
then consider K being Nat such that
A22: ExitsAtWhile>0 (a,ISu,p,(Initialized (Initialized s))) = K and
A23: ((StepWhile>0 (a,ISu,p,(Initialized (Initialized s)))) . K) . a <= 0 and
A24: for i being Nat st ((StepWhile>0 (a,ISu,p,(Initialized (Initialized s)))) . i) . a <= 0 holds
K <= i and
DataPart (Comput ((p +* (while>0 (a,ISu))),(Initialize (Initialized (Initialized s))),(LifeSpan ((p +* (while>0 (a,ISu))),(Initialize (Initialized (Initialized s))))))) = DataPart ((StepWhile>0 (a,ISu,p,(Initialized (Initialized s)))) . K) by A10, Def6;
A25: DataPart (IExec ((while>0 (a,ISu)),p,(Initialized s))) = DataPart ((StepWhile>0 (a,ISu,p,(Initialized (Initialized s)))) . (ExitsAtWhile>0 (a,ISu,p,(Initialized (Initialized s))))) by A21, A10, Th36;
((StepWhile>0 (a,ISu,p,(Initialized s))) . k) . a = 0 by A2, A4, Th53, A1;
then ((StepWhile>0 (a,ISu,p,(Initialized (Initialized s)))) . k) . a = 0 ;
then A26: K <= k by A24;
then A27: (((StepWhile>0 (a,ISu,p,(Initialized s))) . K) . a) + K = k by A2, A4, Th52, A1;
K - K <= k - K by A26, XREAL_1:9;
then A28: ((StepWhile>0 (a,ISu,p,(Initialized (Initialized s)))) . K) . a = 0 by A23, A27;
A29: (((StepWhile>0 (a,ISu,p,(Initialized (Initialized s)))) . K) . a) + K = k by A27;
A30: 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 (a,ISu)),p,(Initialized s))) . x by SCMFSA8C:3
.= ((StepTimes (a,J,p,s)) . k) . x by A25, A22, A29, A28, 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 (a,ISu)),p,(Initialized s))) . x by SCMFSA8C:3
.= ((StepTimes (a,J,p,s)) . k) . x by A25, A22, A29, A28, SCMFSA_M:2 ; :: thesis: verum
end;
hence DataPart (IExec ((Times (a,J)),p,s)) = DataPart ((StepTimes (a,J,p,s)) . k) by A30, SCMFSA_M:2; :: thesis: verum