let s be State of SCM+FSA; :: thesis: for p being Instruction-Sequence of SCM+FSA
for a being read-write Int-Location
for J being good really-closed MacroInstruction of SCM+FSA st not J destroys a & 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 read-write Int-Location
for J being good really-closed MacroInstruction of SCM+FSA st not J destroys a & 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 read-write Int-Location; :: thesis: for J being good really-closed MacroInstruction of SCM+FSA st not J destroys a & 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 good really-closed MacroInstruction of SCM+FSA ; :: thesis: ( not J destroys a & 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: not J destroys a ; :: thesis: ( not s . (intloc 0) = 1 or ( not ProperTimesBody a,J,s,p & not J is parahalting ) or Times (a,J) is_halting_on s,p )
assume A2: 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 ISu = J ";" (SubFrom (a,(intloc 0)));
set WH = while>0 (a,(J ";" (SubFrom (a,(intloc 0)))));
set s1 = Initialized s;
set Is1 = Initialized (Initialized s);
set SW = StepWhile>0 (a,(J ";" (SubFrom (a,(intloc 0)))),p,(Initialized s));
set ISW = StepWhile>0 (a,(J ";" (SubFrom (a,(intloc 0)))),p,(Initialized (Initialized s)));
assume A3: ( ProperTimesBody a,J,s,p or J is parahalting ) ; :: thesis: Times (a,J) is_halting_on s,p
then A4: ProperTimesBody a,J,s,p by Th50;

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

suppose A5: s . a < 0 ; :: thesis: Times (a,J) is_halting_on s,p

A6: (Initialized s) . a = s . a by SCMFSA_M:37;
while>0 (a,(J ";" (SubFrom (a,(intloc 0))))) is_halting_on Initialized s,p by A5, A6, SCMFSA_9:38;
then Times (a,J) is_halting_on Initialized s,p ;
hence Times (a,J) is_halting_on s,p by A2, SCMFSA8B:42; :: thesis: verum

end;

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

A8: ProperBodyWhile>0 a,J ";" (SubFrom (a,(intloc 0))), Initialized s,p

proof

let k be Nat; :: according to SCMFSA9A:def 4 :: thesis: ( ((StepWhile>0 (a,(J ";" (SubFrom (a,(intloc 0)))),p,(Initialized s))) . k) . a > 0 implies J ";" (SubFrom (a,(intloc 0))) is_halting_on (StepWhile>0 (a,(J ";" (SubFrom (a,(intloc 0)))),p,(Initialized s))) . k,p +* (while>0 (a,(J ";" (SubFrom (a,(intloc 0)))))) )
assume ((StepWhile>0 (a,(J ";" (SubFrom (a,(intloc 0)))),p,(Initialized s))) . k) . a > 0 ; :: thesis: J ";" (SubFrom (a,(intloc 0))) is_halting_on (StepWhile>0 (a,(J ";" (SubFrom (a,(intloc 0)))),p,(Initialized s))) . k,p +* (while>0 (a,(J ";" (SubFrom (a,(intloc 0))))))
then A9: k < s . a by A4, A7, Th53, A1;
then A10: ((StepTimes (a,J,p,s)) . k) . (intloc 0) = 1 by A3, Th50, Th51, A1;
then A11: 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, A9;
then A12: J is_halting_on Initialized ((StepTimes (a,J,p,s)) . k),p +* (Times (a,J)) by A10, 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 J ";" (SubFrom (a,(intloc 0))) is_halting_on Initialized ((StepTimes (a,J,p,s)) . k),p +* (Times (a,J)) by A12, SFMASTR1:3;
hence J ";" (SubFrom (a,(intloc 0))) is_halting_on (StepWhile>0 (a,(J ";" (SubFrom (a,(intloc 0)))),p,(Initialized s))) . k,p +* (while>0 (a,(J ";" (SubFrom (a,(intloc 0)))))) by A11, SCMFSA8B:5; :: thesis: verum

end;

A13: WithVariantWhile>0 a,J ";" (SubFrom (a,(intloc 0))), Initialized (Initialized s),p

proof

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

end;

take f ; :: according to SCMFSA9A:def 5 :: thesis: for k being Nat holds
( f . ((StepWhile>0 (a,(J ";" (SubFrom (a,(intloc 0)))),p,(Initialized (Initialized s)))) . (k + 1)) < f . ((StepWhile>0 (a,(J ";" (SubFrom (a,(intloc 0)))),p,(Initialized (Initialized s)))) . k) or ((StepWhile>0 (a,(J ";" (SubFrom (a,(intloc 0)))),p,(Initialized (Initialized s)))) . k) . a <= 0 )
let k be Nat; :: thesis: ( f . ((StepWhile>0 (a,(J ";" (SubFrom (a,(intloc 0)))),p,(Initialized (Initialized s)))) . (k + 1)) < f . ((StepWhile>0 (a,(J ";" (SubFrom (a,(intloc 0)))),p,(Initialized (Initialized s)))) . k) or ((StepWhile>0 (a,(J ";" (SubFrom (a,(intloc 0)))),p,(Initialized (Initialized s)))) . k) . a <= 0 )

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

suppose A16: k < s . a ; :: thesis: ( f . ((StepWhile>0 (a,(J ";" (SubFrom (a,(intloc 0)))),p,(Initialized (Initialized s)))) . (k + 1)) < f . ((StepWhile>0 (a,(J ";" (SubFrom (a,(intloc 0)))),p,(Initialized (Initialized s)))) . k) or ((StepWhile>0 (a,(J ";" (SubFrom (a,(intloc 0)))),p,(Initialized (Initialized s)))) . k) . a <= 0 )

then A17: k - k < (s . a) - k by XREAL_1:9;
A18: (((StepTimes (a,J,p,s)) . k) . a) + k = s . a by A4, A16, Th52, A1;
A19: k + 1 <= sa by A16, NAT_1:13;
then A20: (k + 1) - (k + 1) <= (s . a) - (k + 1) by XREAL_1:9;
A21: (((StepTimes (a,J,p,s)) . (k + 1)) . a) + (k + 1) = s . a by A4, A19, Th52, A1;
then A22: s . a = ((((StepTimes (a,J,p,s)) . (k + 1)) . a) + 1) + k ;
A23: f . ((StepWhile>0 (a,(J ";" (SubFrom (a,(intloc 0)))),p,(Initialized (Initialized s)))) . (k + 1)) = |.(((StepWhile>0 (a,(J ";" (SubFrom (a,(intloc 0)))),p,(Initialized (Initialized s)))) . (k + 1)) . a).| by A15
.= ((StepWhile>0 (a,(J ";" (SubFrom (a,(intloc 0)))),p,(Initialized s))) . (k + 1)) . a by A21, A20, ABSVALUE:def 1 ;
f . ((StepWhile>0 (a,(J ";" (SubFrom (a,(intloc 0)))),p,(Initialized (Initialized s)))) . k) = |.(((StepWhile>0 (a,(J ";" (SubFrom (a,(intloc 0)))),p,(Initialized (Initialized s)))) . k) . a).| by A15
.= ((StepWhile>0 (a,(J ";" (SubFrom (a,(intloc 0)))),p,(Initialized s))) . k) . a by A18, A17, ABSVALUE:def 1 ;
hence ( f . ((StepWhile>0 (a,(J ";" (SubFrom (a,(intloc 0)))),p,(Initialized (Initialized s)))) . (k + 1)) < f . ((StepWhile>0 (a,(J ";" (SubFrom (a,(intloc 0)))),p,(Initialized (Initialized s)))) . k) or ((StepWhile>0 (a,(J ";" (SubFrom (a,(intloc 0)))),p,(Initialized (Initialized s)))) . k) . a <= 0 ) by A18, A22, A23, NAT_1:13; :: thesis: verum

end;

suppose k >= s . a ; :: thesis: ( f . ((StepWhile>0 (a,(J ";" (SubFrom (a,(intloc 0)))),p,(Initialized (Initialized s)))) . (k + 1)) < f . ((StepWhile>0 (a,(J ";" (SubFrom (a,(intloc 0)))),p,(Initialized (Initialized s)))) . k) or ((StepWhile>0 (a,(J ";" (SubFrom (a,(intloc 0)))),p,(Initialized (Initialized s)))) . k) . a <= 0 )

hence ( f . ((StepWhile>0 (a,(J ";" (SubFrom (a,(intloc 0)))),p,(Initialized (Initialized s)))) . (k + 1)) < f . ((StepWhile>0 (a,(J ";" (SubFrom (a,(intloc 0)))),p,(Initialized (Initialized s)))) . k) or ((StepWhile>0 (a,(J ";" (SubFrom (a,(intloc 0)))),p,(Initialized (Initialized s)))) . k) . a <= 0 ) by A4, A7, Th53, A1; :: thesis: verum

end;

end;

end;

A24: ProperBodyWhile>0 a,J ";" (SubFrom (a,(intloc 0))), Initialized (Initialized s),p by A8;
while>0 (a,(J ";" (SubFrom (a,(intloc 0))))) is_halting_on Initialized (Initialized s),p by A24, A13, Th27;
then while>0 (a,(J ";" (SubFrom (a,(intloc 0))))) is_halting_on Initialized s,p ;
then Times (a,J) is_halting_on Initialized s,p ;
hence Times (a,J) is_halting_on s,p by A2, SCMFSA8B:42; :: thesis: verum

end;

end;