begin
begin
begin
definition
let a,
b be
Int-Location;
existence
ex b1 being Instruction of SCM+FSA ex A, B being Data-Location st
( a = A & b = B & b1 = A := B )
correctness
uniqueness
for b1, b2 being Instruction of SCM+FSA st ex A, B being Data-Location st
( a = A & b = B & b1 = A := B ) & ex A, B being Data-Location st
( a = A & b = B & b2 = A := B ) holds
b1 = b2;
;
existence
ex b1 being Instruction of SCM+FSA ex A, B being Data-Location st
( a = A & b = B & b1 = AddTo (A,B) )
correctness
uniqueness
for b1, b2 being Instruction of SCM+FSA st ex A, B being Data-Location st
( a = A & b = B & b1 = AddTo (A,B) ) & ex A, B being Data-Location st
( a = A & b = B & b2 = AddTo (A,B) ) holds
b1 = b2;
;
existence
ex b1 being Instruction of SCM+FSA ex A, B being Data-Location st
( a = A & b = B & b1 = SubFrom (A,B) )
correctness
uniqueness
for b1, b2 being Instruction of SCM+FSA st ex A, B being Data-Location st
( a = A & b = B & b1 = SubFrom (A,B) ) & ex A, B being Data-Location st
( a = A & b = B & b2 = SubFrom (A,B) ) holds
b1 = b2;
;
existence
ex b1 being Instruction of SCM+FSA ex A, B being Data-Location st
( a = A & b = B & b1 = MultBy (A,B) )
correctness
uniqueness
for b1, b2 being Instruction of SCM+FSA st ex A, B being Data-Location st
( a = A & b = B & b1 = MultBy (A,B) ) & ex A, B being Data-Location st
( a = A & b = B & b2 = MultBy (A,B) ) holds
b1 = b2;
;
existence
ex b1 being Instruction of SCM+FSA ex A, B being Data-Location st
( a = A & b = B & b1 = Divide (A,B) )
correctness
uniqueness
for b1, b2 being Instruction of SCM+FSA st ex A, B being Data-Location st
( a = A & b = B & b1 = Divide (A,B) ) & ex A, B being Data-Location st
( a = A & b = B & b2 = Divide (A,B) ) holds
b1 = b2;
;
end;
begin
begin
theorem Th67:
for
a,
b being
Int-Location for
s being
State of
SCM+FSA holds
(
(Exec ((Divide (a,b)),s)) . (IC ) = succ (IC s) & (
a <> b implies
(Exec ((Divide (a,b)),s)) . a = (s . a) div (s . b) ) &
(Exec ((Divide (a,b)),s)) . b = (s . a) mod (s . b) & ( for
c being
Int-Location st
c <> a &
c <> b holds
(Exec ((Divide (a,b)),s)) . c = s . c ) & ( for
f being
FinSeq-Location holds
(Exec ((Divide (a,b)),s)) . f = s . f ) )
theorem Th73:
for
g being
FinSeq-Location for
a,
c being
Int-Location for
s being
State of
SCM+FSA holds
(
(Exec (((g,a) := c),s)) . (IC ) = succ (IC s) & ex
k being
Element of
NAT st
(
k = abs (s . a) &
(Exec (((g,a) := c),s)) . g = (s . g) +* (
k,
(s . c)) ) & ( for
b being
Int-Location holds
(Exec (((g,a) := c),s)) . b = s . b ) & ( for
f being
FinSeq-Location st
f <> g holds
(Exec (((g,a) := c),s)) . f = s . f ) )
theorem Th75:
for
g being
FinSeq-Location for
c being
Int-Location for
s being
State of
SCM+FSA holds
(
(Exec ((g :=<0,...,0> c),s)) . (IC ) = succ (IC s) & ex
k being
Element of
NAT st
(
k = abs (s . c) &
(Exec ((g :=<0,...,0> c),s)) . g = k |-> 0 ) & ( for
b being
Int-Location holds
(Exec ((g :=<0,...,0> c),s)) . b = s . b ) & ( for
f being
FinSeq-Location st
f <> g holds
(Exec ((g :=<0,...,0> c),s)) . f = s . f ) )
begin
theorem Th93:
for
I being
set holds
(
I is
Instruction of
SCM+FSA iff (
I = [0,{},{}] or ex
a,
b being
Int-Location st
I = a := b or ex
a,
b being
Int-Location st
I = AddTo (
a,
b) or ex
a,
b being
Int-Location st
I = SubFrom (
a,
b) or ex
a,
b being
Int-Location st
I = MultBy (
a,
b) or ex
a,
b being
Int-Location st
I = Divide (
a,
b) or ex
la being
Element of
NAT st
I = goto la or ex
lb being
Element of
NAT ex
da being
Int-Location st
I = da =0_goto lb or ex
lb being
Element of
NAT ex
da being
Int-Location st
I = da >0_goto lb or ex
b,
a being
Int-Location ex
fa being
FinSeq-Location st
I = a := (
fa,
b) or ex
a,
b being
Int-Location ex
fa being
FinSeq-Location st
I = (
fa,
a)
:= b or ex
a being
Int-Location ex
f being
FinSeq-Location st
I = a :=len f or ex
a being
Int-Location ex
f being
FinSeq-Location st
I = f :=<0,...,0> a ) )
Lm1:
for W being Instruction of SCM+FSA st W is halting holds
W = [0,{},{}]