set D = Int-Locations \/ FinSeq-Locations ;
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))),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))),s) . b = (s . b) + ((s . c) * (s . a)) )
assume A1:
( a <> b & a <> c & b <> c )
; :: thesis: ( not s . a >= 0 or (IExec (Times a,(Macro (AddTo b,c))),s) . b = (s . b) + ((s . c) * (s . a)) )
assume A2:
s . a >= 0
; :: thesis: (IExec (Times a,(Macro (AddTo b,c))),s) . b = (s . b) + ((s . c) * (s . a))
set P = Times a,(Macro (AddTo b,c));
defpred S1[ Element of NAT ] means for s being State of SCM+FSA st s . a = $1 holds
(IExec (Times a,(Macro (AddTo b,c))),s) . b = (s . b) + ((s . c) * (s . a));
reconsider I = Macro (AddTo b,c) as parahalting good Program of SCM+FSA by Th99, SCMFSA7B:13;
A3:
S1[ 0 ]
proof
let s be
State of
SCM+FSA ;
:: thesis: ( s . a = 0 implies (IExec (Times a,(Macro (AddTo b,c))),s) . b = (s . b) + ((s . c) * (s . a)) )
set s0 =
Initialize s;
assume A4:
s . a = 0
;
:: thesis: (IExec (Times a,(Macro (AddTo b,c))),s) . b = (s . b) + ((s . c) * (s . a))
then
(
(Initialize s) . (intloc 0 ) = 1 &
(Initialize s) . a = 0 )
by SCMFSA6C:3;
then A5:
DataPart (IExec (Times a,I),(Initialize s)) = DataPart (Initialize s)
by Th123;
thus (IExec (Times a,(Macro (AddTo b,c))),s) . b =
(IExec (Times a,(Macro (AddTo b,c))),(Initialize s)) . b
by Th17
.=
(Initialize s) . b
by A5, SCMFSA6A:38
.=
(s . b) + ((s . c) * (s . a))
by A4, SCMFSA6C:3
;
:: thesis: verum
end;
A6:
for k being Element of NAT st S1[k] holds
S1[k + 1]
proof
let k be
Element of
NAT ;
:: thesis: ( S1[k] implies S1[k + 1] )
assume A7:
S1[
k]
;
:: thesis: S1[k + 1]
let s be
State of
SCM+FSA ;
:: thesis: ( s . a = k + 1 implies (IExec (Times a,(Macro (AddTo b,c))),s) . b = (s . b) + ((s . c) * (s . a)) )
assume A8:
s . a = k + 1
;
:: thesis: (IExec (Times a,(Macro (AddTo b,c))),s) . b = (s . b) + ((s . c) * (s . a))
A9:
(IExec (I ';' (SubFrom a,(intloc 0 ))),s) . b =
(Exec (SubFrom a,(intloc 0 )),(IExec I,s)) . b
by SCMFSA6C:7
.=
(IExec I,s) . b
by A1, SCMFSA_2:91
.=
(Exec (AddTo b,c),(Initialize s)) . b
by SCMFSA6C:6
.=
((Initialize s) . b) + ((Initialize s) . c)
by SCMFSA_2:90
.=
((Initialize s) . b) + (s . c)
by SCMFSA6C:3
.=
(s . b) + (s . c)
by SCMFSA6C:3
;
A10:
(IExec (I ';' (SubFrom a,(intloc 0 ))),s) . c =
(Exec (SubFrom a,(intloc 0 )),(IExec I,s)) . c
by SCMFSA6C:7
.=
(IExec I,s) . c
by A1, SCMFSA_2:91
.=
(Exec (AddTo b,c),(Initialize s)) . c
by SCMFSA6C:6
.=
(Initialize s) . c
by A1, SCMFSA_2:90
.=
s . c
by SCMFSA6C:3
;
I does_not_destroy a
by A1, Th77, SCMFSA7B:13;
then A11:
(
(IExec (I ';' (SubFrom a,(intloc 0 ))),s) . a = (s . a) - 1 &
DataPart (IExec (Times a,I),s) = DataPart (IExec (Times a,I),(IExec (I ';' (SubFrom a,(intloc 0 ))),s)) )
by A8, Th124;
then (IExec (Times a,I),(IExec (I ';' (SubFrom a,(intloc 0 ))),s)) . b =
((s . b) + (s . c)) + ((s . c) * ((s . a) - 1))
by A7, A8, A9, A10
.=
(s . b) + ((s . c) * (s . a))
;
hence
(IExec (Times a,(Macro (AddTo b,c))),s) . b = (s . b) + ((s . c) * (s . a))
by A11, SCMFSA6A:38;
:: thesis: verum
end;
A12:
for k being Element of NAT holds S1[k]
from NAT_1:sch 1(A3, A6);
reconsider sa = s . a as Element of NAT by A2, INT_1:16;
S1[sa]
by A12;
hence
(IExec (Times a,(Macro (AddTo b,c))),s) . b = (s . b) + ((s . c) * (s . a))
; :: thesis: verum