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 ;
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
Instruction-Location of
SCM+FSA 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 Instruction-Location of SCM+FSA 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 Instruction-Location of SCM+FSA st
( ( i = a =0_goto l or i = a >0_goto l ) & b1 = {a} ) & ex a being Int-Location ex l being Instruction-Location of SCM+FSA 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 Instruction-Location of SCM+FSA 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 Instruction-Location of SCM+FSA 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 Instruction-Location of SCM+FSA 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
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
Instruction-Location of
SCM+FSA 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 :
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 ;
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 :
theorem Th36:
theorem Th37:
theorem Th38:
:: deftheorem Def4 defines UsedInt*Loc SF_MASTR:def 4 :
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 :
:: deftheorem Def6 defines FirstNotIn SF_MASTR:def 6 :
theorem Th52:
theorem
:: deftheorem Def7 defines FirstNotUsed SF_MASTR:def 7 :
theorem Th54:
theorem
theorem
theorem
theorem
begin
:: deftheorem Def8 defines First*NotIn SF_MASTR:def 8 :
theorem Th59:
theorem
:: deftheorem Def9 defines First*NotUsed SF_MASTR:def 9 :
theorem Th61:
theorem
theorem
begin
theorem Th64:
theorem Th65:
theorem Th66:
theorem Th67:
theorem Th68:
theorem
theorem Th70:
theorem
theorem Th72:
theorem