let P be Instruction-Sequence of SCM+FSA; :: thesis: for s being State of SCM+FSA
for a, b, c being read-write Int-Location st a <> b & a <> c & b <> c & s . a >= 0 holds
(IExec ((Times (a,(Macro (AddTo (b,c))))),P,s)) . b = (s . b) + ((s . c) * (s . a))
let s be State of SCM+FSA; :: thesis: for a, b, c being read-write Int-Location st a <> b & a <> c & b <> c & s . a >= 0 holds
(IExec ((Times (a,(Macro (AddTo (b,c))))),P,s)) . b = (s . b) + ((s . c) * (s . a))
let a, b, c be read-write Int-Location ; :: thesis: ( a <> b & a <> c & b <> c & s . a >= 0 implies (IExec ((Times (a,(Macro (AddTo (b,c))))),P,s)) . b = (s . b) + ((s . c) * (s . a)) )
set I2 = Times (a,(Macro (AddTo (b,c))));
defpred S₁[ Nat] means for s being State of SCM+FSA st s . a = $1 holds
(IExec ((Times (a,(Macro (AddTo (b,c))))),P,s)) . b = (s . b) + ((s . c) * (s . a));
reconsider I = Macro (AddTo (b,c)) as good parahalting Program of SCM+FSA by Th99, SCMFSA7B:7;
set D = Data-Locations ;
assume that
A1: a <> b and
A2: a <> c and
A3: b <> c ; :: thesis: ( not s . a >= 0 or (IExec ((Times (a,(Macro (AddTo (b,c))))),P,s)) . b = (s . b) + ((s . c) * (s . a)) )
A4: for k being Element of NAT st S₁[k] holds
S₁[k + 1]

proof

let k be Element of NAT ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A5: S₁[k] ; :: thesis: S₁[k + 1]
let s be State of SCM+FSA; :: thesis: ( s . a = k + 1 implies (IExec ((Times (a,(Macro (AddTo (b,c))))),P,s)) . b = (s . b) + ((s . c) * (s . a)) )
assume A6: s . a = k + 1 ; :: thesis: (IExec ((Times (a,(Macro (AddTo (b,c))))),P,s)) . b = (s . b) + ((s . c) * (s . a))
A7: not I destroys a by A1, Th77, SCMFSA7B:7;
then A8: DataPart (IExec ((Times (a,I)),P,s)) = DataPart (IExec ((Times (a,I)),P,(IExec ((I ';' (SubFrom (a,(intloc 0)))),P,s)))) by A6, Th124;
A9: (IExec ((I ';' (SubFrom (a,(intloc 0)))),P,s)) . c = (Exec ((SubFrom (a,(intloc 0))),(IExec (I,P,s)))) . c by SCMFSA6C:6
.= (IExec (I,P,s)) . c by A2, SCMFSA_2:65
.= (IExec (I,P,s)) . c
.= (Exec ((AddTo (b,c)),(Initialized s))) . c by SCMFSA6C:5
.= (Exec ((AddTo (b,c)),(Initialized s))) . c
.= (Initialized s) . c by A3, SCMFSA_2:64
.= s . c by SCMFSA6C:3 ;
A10: (IExec ((I ';' (SubFrom (a,(intloc 0)))),P,s)) . b = (Exec ((SubFrom (a,(intloc 0))),(IExec (I,P,s)))) . b by SCMFSA6C:6
.= (IExec (I,P,s)) . b by A1, SCMFSA_2:65
.= (IExec (I,P,s)) . b
.= (Exec ((AddTo (b,c)),(Initialized s))) . b by SCMFSA6C:5
.= (Exec ((AddTo (b,c)),(Initialized s))) . b
.= ((Initialized s) . b) + ((Initialized s) . c) by SCMFSA_2:64
.= ((Initialized s) . b) + (s . c) by SCMFSA6C:3
.= (s . b) + (s . c) by SCMFSA6C:3 ;
(IExec ((I ';' (SubFrom (a,(intloc 0)))),P,s)) . a = (s . a) - 1 by A6, A7, Th124;
then (IExec ((Times (a,I)),P,(IExec ((I ';' (SubFrom (a,(intloc 0)))),P,s)))) . b = ((s . b) + (s . c)) + ((s . c) * ((s . a) - 1)) by A5, A6, A10, A9
.= (s . b) + ((s . c) * (s . a)) ;
hence (IExec ((Times (a,(Macro (AddTo (b,c))))),P,s)) . b = (s . b) + ((s . c) * (s . a)) by A8, SCMFSA6A:7; :: thesis: verum

end;

assume s . a >= 0 ; :: thesis: (IExec ((Times (a,(Macro (AddTo (b,c))))),P,s)) . b = (s . b) + ((s . c) * (s . a))
then reconsider sa = s . a as Element of NAT by INT_1:3;
A11: S₁[ 0 ]

proof

let s be State of SCM+FSA; :: thesis: ( s . a = 0 implies (IExec ((Times (a,(Macro (AddTo (b,c))))),P,s)) . b = (s . b) + ((s . c) * (s . a)) )
set s0 = Initialized s;
A12: (Initialized s) . (intloc 0) = 1 by SCMFSA6A:38;
assume A13: s . a = 0 ; :: thesis: (IExec ((Times (a,(Macro (AddTo (b,c))))),P,s)) . b = (s . b) + ((s . c) * (s . a))
then (Initialized s) . a = 0 by SCMFSA6C:3;
then A14: DataPart (IExec ((Times (a,I)),P,(Initialized s))) = DataPart (Initialized s) by A12, Th123;
thus (IExec ((Times (a,(Macro (AddTo (b,c))))),P,s)) . b = (IExec ((Times (a,(Macro (AddTo (b,c))))),P,(Initialized s))) . b
.= (Initialized s) . b by A14, SCMFSA6A:7
.= (s . b) + ((s . c) * (s . a)) by A13, SCMFSA6C:3 ; :: thesis: verum

end;

for k being Element of NAT holds S₁[k] from NAT_1:sch 1(A11, A4);
then S₁[sa] ;
hence (IExec ((Times (a,(Macro (AddTo (b,c))))),P,s)) . b = (s . b) + ((s . c) * (s . a)) ; :: thesis: verum