begin
begin
definition
let i be
Instruction of
SCM+FSA;
func UsedIntLoc i -> Element of
Fin Int-Locations means :
Def1:
ex
a,
b being
Int-Location st
( (
i = a := b or
i = AddTo (
a,
b) or
i = SubFrom (
a,
b) or
i = MultBy (
a,
b) or
i = Divide (
a,
b) ) &
it = {a,b} )
if InsCode i in {1,2,3,4,5} ex
a being
Int-Location ex
l being
Element of
NAT st
( (
i = a =0_goto l or
i = a >0_goto l ) &
it = {a} )
if (
InsCode i = 7 or
InsCode i = 8 )
ex
a,
b being
Int-Location ex
f being
FinSeq-Location st
( (
i = b := (
f,
a) or
i = (
f,
a)
:= b ) &
it = {a,b} )
if (
InsCode i = 9 or
InsCode i = 10 )
ex
a being
Int-Location ex
f being
FinSeq-Location st
( (
i = a :=len f or
i = f :=<0,...,0> a ) &
it = {a} )
if (
InsCode i = 11 or
InsCode i = 12 )
otherwise it = {} ;
existence
( ( InsCode i in {1,2,3,4,5} implies ex b1 being Element of Fin Int-Locations ex a, b being Int-Location st
( ( i = a := b or i = AddTo (a,b) or i = SubFrom (a,b) or i = MultBy (a,b) or i = Divide (a,b) ) & b1 = {a,b} ) ) & ( ( InsCode i = 7 or InsCode i = 8 ) implies ex b1 being Element of Fin Int-Locations ex a being Int-Location ex l being Element of NAT st
( ( i = a =0_goto l or i = a >0_goto l ) & b1 = {a} ) ) & ( ( InsCode i = 9 or InsCode i = 10 ) implies ex b1 being Element of Fin Int-Locations ex a, b being Int-Location ex f being FinSeq-Location st
( ( i = b := (f,a) or i = (f,a) := b ) & b1 = {a,b} ) ) & ( ( InsCode i = 11 or InsCode i = 12 ) implies ex b1 being Element of Fin Int-Locations ex a being Int-Location ex f being FinSeq-Location st
( ( i = a :=len f or i = f :=<0,...,0> a ) & b1 = {a} ) ) & ( InsCode i in {1,2,3,4,5} or InsCode i = 7 or InsCode i = 8 or InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 or ex b1 being Element of Fin Int-Locations st b1 = {} ) )
uniqueness
for b1, b2 being Element of Fin Int-Locations holds
( ( InsCode i in {1,2,3,4,5} & ex a, b being Int-Location st
( ( i = a := b or i = AddTo (a,b) or i = SubFrom (a,b) or i = MultBy (a,b) or i = Divide (a,b) ) & b1 = {a,b} ) & ex a, b being Int-Location st
( ( i = a := b or i = AddTo (a,b) or i = SubFrom (a,b) or i = MultBy (a,b) or i = Divide (a,b) ) & b2 = {a,b} ) implies b1 = b2 ) & ( ( InsCode i = 7 or InsCode i = 8 ) & ex a being Int-Location ex l being Element of NAT st
( ( i = a =0_goto l or i = a >0_goto l ) & b1 = {a} ) & ex a being Int-Location ex l being Element of NAT st
( ( i = a =0_goto l or i = a >0_goto l ) & b2 = {a} ) implies b1 = b2 ) & ( ( InsCode i = 9 or InsCode i = 10 ) & ex a, b being Int-Location ex f being FinSeq-Location st
( ( i = b := (f,a) or i = (f,a) := b ) & b1 = {a,b} ) & ex a, b being Int-Location ex f being FinSeq-Location st
( ( i = b := (f,a) or i = (f,a) := b ) & b2 = {a,b} ) implies b1 = b2 ) & ( ( InsCode i = 11 or InsCode i = 12 ) & ex a being Int-Location ex f being FinSeq-Location st
( ( i = a :=len f or i = f :=<0,...,0> a ) & b1 = {a} ) & ex a being Int-Location ex f being FinSeq-Location st
( ( i = a :=len f or i = f :=<0,...,0> a ) & b2 = {a} ) implies b1 = b2 ) & ( InsCode i in {1,2,3,4,5} or InsCode i = 7 or InsCode i = 8 or InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 or not b1 = {} or not b2 = {} or b1 = b2 ) )
consistency
for b1 being Element of Fin Int-Locations holds
( ( InsCode i in {1,2,3,4,5} & ( InsCode i = 7 or InsCode i = 8 ) implies ( ex a, b being Int-Location st
( ( i = a := b or i = AddTo (a,b) or i = SubFrom (a,b) or i = MultBy (a,b) or i = Divide (a,b) ) & b1 = {a,b} ) iff ex a being Int-Location ex l being Element of NAT st
( ( i = a =0_goto l or i = a >0_goto l ) & b1 = {a} ) ) ) & ( InsCode i in {1,2,3,4,5} & ( InsCode i = 9 or InsCode i = 10 ) implies ( ex a, b being Int-Location st
( ( i = a := b or i = AddTo (a,b) or i = SubFrom (a,b) or i = MultBy (a,b) or i = Divide (a,b) ) & b1 = {a,b} ) iff ex a, b being Int-Location ex f being FinSeq-Location st
( ( i = b := (f,a) or i = (f,a) := b ) & b1 = {a,b} ) ) ) & ( InsCode i in {1,2,3,4,5} & ( InsCode i = 11 or InsCode i = 12 ) implies ( ex a, b being Int-Location st
( ( i = a := b or i = AddTo (a,b) or i = SubFrom (a,b) or i = MultBy (a,b) or i = Divide (a,b) ) & b1 = {a,b} ) iff ex a being Int-Location ex f being FinSeq-Location st
( ( i = a :=len f or i = f :=<0,...,0> a ) & b1 = {a} ) ) ) & ( ( InsCode i = 7 or InsCode i = 8 ) & ( InsCode i = 9 or InsCode i = 10 ) implies ( ex a being Int-Location ex l being Element of NAT st
( ( i = a =0_goto l or i = a >0_goto l ) & b1 = {a} ) iff ex a, b being Int-Location ex f being FinSeq-Location st
( ( i = b := (f,a) or i = (f,a) := b ) & b1 = {a,b} ) ) ) & ( ( InsCode i = 7 or InsCode i = 8 ) & ( InsCode i = 11 or InsCode i = 12 ) implies ( ex a being Int-Location ex l being Element of NAT st
( ( i = a =0_goto l or i = a >0_goto l ) & b1 = {a} ) iff ex a being Int-Location ex f being FinSeq-Location st
( ( i = a :=len f or i = f :=<0,...,0> a ) & b1 = {a} ) ) ) & ( ( InsCode i = 9 or InsCode i = 10 ) & ( InsCode i = 11 or InsCode i = 12 ) implies ( ex a, b being Int-Location ex f being FinSeq-Location st
( ( i = b := (f,a) or i = (f,a) := b ) & b1 = {a,b} ) iff ex a being Int-Location ex f being FinSeq-Location st
( ( i = a :=len f or i = f :=<0,...,0> a ) & b1 = {a} ) ) ) )
by ENUMSET1:def 3;
end;
::
deftheorem Def1 defines
UsedIntLoc SF_MASTR:def 1 :
for i being Instruction of SCM+FSA
for b2 being Element of Fin Int-Locations holds
( ( InsCode i in {1,2,3,4,5} implies ( b2 = UsedIntLoc i iff ex a, b being Int-Location st
( ( i = a := b or i = AddTo (a,b) or i = SubFrom (a,b) or i = MultBy (a,b) or i = Divide (a,b) ) & b2 = {a,b} ) ) ) & ( ( InsCode i = 7 or InsCode i = 8 ) implies ( b2 = UsedIntLoc i iff ex a being Int-Location ex l being Element of NAT st
( ( i = a =0_goto l or i = a >0_goto l ) & b2 = {a} ) ) ) & ( ( InsCode i = 9 or InsCode i = 10 ) implies ( b2 = UsedIntLoc i iff ex a, b being Int-Location ex f being FinSeq-Location st
( ( i = b := (f,a) or i = (f,a) := b ) & b2 = {a,b} ) ) ) & ( ( InsCode i = 11 or InsCode i = 12 ) implies ( b2 = UsedIntLoc i iff ex a being Int-Location ex f being FinSeq-Location st
( ( i = a :=len f or i = f :=<0,...,0> a ) & b2 = {a} ) ) ) & ( InsCode i in {1,2,3,4,5} or InsCode i = 7 or InsCode i = 8 or InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 or ( b2 = UsedIntLoc i iff b2 = {} ) ) );
begin
definition
let i be
Instruction of
SCM+FSA;
existence
( ( ( InsCode i = 9 or InsCode i = 10 ) implies ex b1 being Element of Fin FinSeq-Locations ex a, b being Int-Location ex f being FinSeq-Location st
( ( i = b := (f,a) or i = (f,a) := b ) & b1 = {f} ) ) & ( ( InsCode i = 11 or InsCode i = 12 ) implies ex b1 being Element of Fin FinSeq-Locations ex a being Int-Location ex f being FinSeq-Location st
( ( i = a :=len f or i = f :=<0,...,0> a ) & b1 = {f} ) ) & ( InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 or ex b1 being Element of Fin FinSeq-Locations st b1 = {} ) )
uniqueness
for b1, b2 being Element of Fin FinSeq-Locations holds
( ( ( InsCode i = 9 or InsCode i = 10 ) & ex a, b being Int-Location ex f being FinSeq-Location st
( ( i = b := (f,a) or i = (f,a) := b ) & b1 = {f} ) & ex a, b being Int-Location ex f being FinSeq-Location st
( ( i = b := (f,a) or i = (f,a) := b ) & b2 = {f} ) implies b1 = b2 ) & ( ( InsCode i = 11 or InsCode i = 12 ) & ex a being Int-Location ex f being FinSeq-Location st
( ( i = a :=len f or i = f :=<0,...,0> a ) & b1 = {f} ) & ex a being Int-Location ex f being FinSeq-Location st
( ( i = a :=len f or i = f :=<0,...,0> a ) & b2 = {f} ) implies b1 = b2 ) & ( InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 or not b1 = {} or not b2 = {} or b1 = b2 ) )
consistency
for b1 being Element of Fin FinSeq-Locations st ( InsCode i = 9 or InsCode i = 10 ) & ( InsCode i = 11 or InsCode i = 12 ) holds
( ex a, b being Int-Location ex f being FinSeq-Location st
( ( i = b := (f,a) or i = (f,a) := b ) & b1 = {f} ) iff ex a being Int-Location ex f being FinSeq-Location st
( ( i = a :=len f or i = f :=<0,...,0> a ) & b1 = {f} ) )
;
end;
begin
definition
canceled;
end;
begin
definition
canceled;
end;
begin
theorem
for
I being
Program of
for
n being
Element of
NAT for
s,
t being
State of
SCM+FSA for
P,
Q being
Instruction-Sequence of
SCM+FSA st
I c= P &
I c= Q &
Start-At (
0,
SCM+FSA)
c= s &
Start-At (
0,
SCM+FSA)
c= t &
s | (UsedIntLoc I) = t | (UsedIntLoc I) &
s | (UsedInt*Loc I) = t | (UsedInt*Loc I) & ( for
m being
Element of
NAT st
m < n holds
IC (Comput (P,s,m)) in dom I ) holds
( ( for
m being
Element of
NAT st
m < n holds
IC (Comput (Q,t,m)) in dom I ) & ( for
m being
Element of
NAT st
m <= n holds
(
IC (Comput (P,s,m)) = IC (Comput (Q,t,m)) & ( for
a being
Int-Location st
a in UsedIntLoc I holds
(Comput (P,s,m)) . a = (Comput (Q,t,m)) . a ) & ( for
f being
FinSeq-Location st
f in UsedInt*Loc I holds
(Comput (P,s,m)) . f = (Comput (Q,t,m)) . f ) ) ) )