begin
begin
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
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 = {} ) ) );
theorem Th17:
theorem Th18:
theorem Th19:
theorem Th20:
theorem Th21:
theorem Th22:
:: deftheorem Def2 defines UsedIntLoc SF_MASTR:def 2 :
for p being Function
for b2 being Subset of Int-Locations holds
( b2 = UsedIntLoc p iff ex UIL being Function of the Instructions of SCM+FSA ,(Fin Int-Locations ) st
( ( for i being Instruction of SCM+FSA holds UIL . i = UsedIntLoc i ) & b2 = Union (UIL * p) ) );
theorem Th23:
theorem
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
theorem
theorem
theorem
begin
definition
let i be
Instruction of
SCM+FSA ;
func UsedInt*Loc i -> Element of
Fin FinSeq-Locations means :
Def3:
ex
a,
b being
Int-Location ex
f being
FinSeq-Location st
( (
i = b := f,
a or
i = f,
a := b ) &
it = {f} )
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 = {f} )
if (
InsCode i = 11 or
InsCode i = 12 )
otherwise it = {} ;
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;
:: deftheorem Def3 defines UsedInt*Loc SF_MASTR:def 3 :
for i being Instruction of SCM+FSA
for b2 being Element of Fin FinSeq-Locations holds
( ( ( InsCode i = 9 or InsCode i = 10 ) implies ( b2 = UsedInt*Loc i iff ex a, b being Int-Location ex f being FinSeq-Location st
( ( i = b := f,a or i = f,a := b ) & b2 = {f} ) ) ) & ( ( InsCode i = 11 or InsCode i = 12 ) implies ( b2 = UsedInt*Loc i iff ex a being Int-Location ex f being FinSeq-Location st
( ( i = a :=len f or i = f :=<0,...,0> a ) & b2 = {f} ) ) ) & ( InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 or ( b2 = UsedInt*Loc i iff b2 = {} ) ) );
theorem Th36:
theorem Th37:
theorem Th38:
:: deftheorem Def4 defines UsedInt*Loc SF_MASTR:def 4 :
for p being Function
for b2 being Subset of FinSeq-Locations holds
( b2 = UsedInt*Loc p iff ex UIL being Function of the Instructions of SCM+FSA ,(Fin FinSeq-Locations ) st
( ( for i being Instruction of SCM+FSA holds UIL . i = UsedInt*Loc i ) & b2 = Union (UIL * p) ) );
theorem Th39:
theorem
theorem Th41:
theorem Th42:
theorem Th43:
theorem Th44:
theorem Th45:
theorem Th46:
theorem Th47:
theorem Th48:
theorem
theorem
theorem
begin
:: deftheorem Def5 defines read-only SF_MASTR:def 5 :
for IT being Int-Location holds
( IT is read-only iff IT = intloc 0 );
:: deftheorem Def6 defines FirstNotIn SF_MASTR:def 6 :
for L being finite Subset of Int-Locations
for b2 being Int-Location holds
( b2 = FirstNotIn L iff ex sn being non empty Subset of NAT st
( b2 = intloc (min sn) & sn = { k where k is Element of NAT : not intloc k in L } ) );
theorem Th52:
theorem
:: deftheorem Def7 defines FirstNotUsed SF_MASTR:def 7 :
for p being preProgram of SCM+FSA
for b2 being Int-Location holds
( b2 = FirstNotUsed p iff ex sil being finite Subset of Int-Locations st
( sil = (UsedIntLoc p) \/ {(intloc 0 )} & b2 = FirstNotIn sil ) );
theorem Th54:
theorem
theorem
theorem
theorem
begin
:: deftheorem Def8 defines First*NotIn SF_MASTR:def 8 :
for L being finite Subset of FinSeq-Locations
for b2 being FinSeq-Location holds
( b2 = First*NotIn L iff ex sn being non empty Subset of NAT st
( b2 = fsloc (min sn) & sn = { k where k is Element of NAT : not fsloc k in L } ) );
theorem Th59:
theorem
:: deftheorem Def9 defines First*NotUsed SF_MASTR:def 9 :
for p being preProgram of SCM+FSA
for b2 being FinSeq-Location holds
( b2 = First*NotUsed p iff ex sil being finite Subset of FinSeq-Locations st
( sil = UsedInt*Loc p & b2 = First*NotIn sil ) );
theorem Th61:
theorem
theorem
begin
theorem Th64:
theorem Th65:
theorem Th66:
theorem Th67:
theorem Th68:
theorem
theorem Th70:
theorem
theorem Th72:
theorem
for
I being
Program of
SCM+FSA for
n being
Element of
NAT for
s,
t being
State of
SCM+FSA st
I +* (Start-At 0 ,SCM+FSA ) c= s &
I +* (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 (ProgramPart s),s,m) in dom I ) holds
( ( for
m being
Element of
NAT st
m < n holds
IC (Comput (ProgramPart t),t,m) in dom I ) & ( for
m being
Element of
NAT st
m <= n holds
(
IC (Comput (ProgramPart s),s,m) = IC (Comput (ProgramPart t),t,m) & ( for
a being
Int-Location st
a in UsedIntLoc I holds
(Comput (ProgramPart s),s,m) . a = (Comput (ProgramPart t),t,m) . a ) & ( for
f being
FinSeq-Location st
f in UsedInt*Loc I holds
(Comput (ProgramPart s),s,m) . f = (Comput (ProgramPart t),t,m) . f ) ) ) )