:: by Piotr Rudnicki and Andrzej Trybulec

::

:: Received July 18, 1996

:: Copyright (c) 1996-2012 Association of Mizar Users

begin

theorem Th3: :: SF_MASTR:3

for a1, b1, a2, b2 being Int-Location st SubFrom (a1,b1) = SubFrom (a2,b2) holds

( a1 = a2 & b1 = b2 )

( a1 = a2 & b1 = b2 )

proof end;

theorem Th4: :: SF_MASTR:4

for a1, b1, a2, b2 being Int-Location st MultBy (a1,b1) = MultBy (a2,b2) holds

( a1 = a2 & b1 = b2 )

( a1 = a2 & b1 = b2 )

proof end;

theorem Th5: :: SF_MASTR:5

for a1, b1, a2, b2 being Int-Location st Divide (a1,b1) = Divide (a2,b2) holds

( a1 = a2 & b1 = b2 )

( a1 = a2 & b1 = b2 )

proof end;

theorem Th7: :: SF_MASTR:7

for a1, a2 being Int-Location

for l1, l2 being Element of NAT st a1 =0_goto l1 = a2 =0_goto l2 holds

( a1 = a2 & l1 = l2 )

for l1, l2 being Element of NAT st a1 =0_goto l1 = a2 =0_goto l2 holds

( a1 = a2 & l1 = l2 )

proof end;

theorem Th8: :: SF_MASTR:8

for a1, a2 being Int-Location

for l1, l2 being Element of NAT st a1 >0_goto l1 = a2 >0_goto l2 holds

( a1 = a2 & l1 = l2 )

for l1, l2 being Element of NAT st a1 >0_goto l1 = a2 >0_goto l2 holds

( a1 = a2 & l1 = l2 )

proof end;

theorem Th9: :: SF_MASTR:9

for b1, a1, b2, a2 being Int-Location

for f1, f2 being FinSeq-Location st b1 := (f1,a1) = b2 := (f2,a2) holds

( a1 = a2 & b1 = b2 & f1 = f2 )

for f1, f2 being FinSeq-Location st b1 := (f1,a1) = b2 := (f2,a2) holds

( a1 = a2 & b1 = b2 & f1 = f2 )

proof end;

theorem Th10: :: SF_MASTR:10

for a1, b1, a2, b2 being Int-Location

for f1, f2 being FinSeq-Location st (f1,a1) := b1 = (f2,a2) := b2 holds

( a1 = a2 & b1 = b2 & f1 = f2 )

for f1, f2 being FinSeq-Location st (f1,a1) := b1 = (f2,a2) := b2 holds

( a1 = a2 & b1 = b2 & f1 = f2 )

proof end;

theorem Th11: :: SF_MASTR:11

for a1, a2 being Int-Location

for f1, f2 being FinSeq-Location st a1 :=len f1 = a2 :=len f2 holds

( a1 = a2 & f1 = f2 )

for f1, f2 being FinSeq-Location st a1 :=len f1 = a2 :=len f2 holds

( a1 = a2 & f1 = f2 )

proof end;

theorem Th12: :: SF_MASTR:12

for a1, a2 being Int-Location

for f1, f2 being FinSeq-Location st f1 :=<0,...,0> a1 = f2 :=<0,...,0> a2 holds

( a1 = a2 & f1 = f2 )

for f1, f2 being FinSeq-Location st f1 :=<0,...,0> a1 = f2 :=<0,...,0> a2 holds

( a1 = a2 & f1 = f2 )

proof end;

begin

definition

let i be Instruction of SCM+FSA;

( ( InsCode i in {1,2,3,4,5} implies ex b_{1} 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) ) & b_{1} = {a,b} ) ) & ( ( InsCode i = 7 or InsCode i = 8 ) implies ex b_{1} 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 ) & b_{1} = {a} ) ) & ( ( InsCode i = 9 or InsCode i = 10 ) implies ex b_{1} 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 ) & b_{1} = {a,b} ) ) & ( ( InsCode i = 11 or InsCode i = 12 ) implies ex b_{1} 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 ) & b_{1} = {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 b_{1} being Element of Fin Int-Locations st b_{1} = {} ) )

for b_{1}, b_{2} 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) ) & b_{1} = {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) ) & b_{2} = {a,b} ) implies b_{1} = b_{2} ) & ( ( 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 ) & b_{1} = {a} ) & ex a being Int-Location ex l being Element of NAT st

( ( i = a =0_goto l or i = a >0_goto l ) & b_{2} = {a} ) implies b_{1} = b_{2} ) & ( ( 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 ) & b_{1} = {a,b} ) & ex a, b being Int-Location ex f being FinSeq-Location st

( ( i = b := (f,a) or i = (f,a) := b ) & b_{2} = {a,b} ) implies b_{1} = b_{2} ) & ( ( 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 ) & b_{1} = {a} ) & ex a being Int-Location ex f being FinSeq-Location st

( ( i = a :=len f or i = f :=<0,...,0> a ) & b_{2} = {a} ) implies b_{1} = b_{2} ) & ( 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 b_{1} = {} or not b_{2} = {} or b_{1} = b_{2} ) )

for b_{1} 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) ) & b_{1} = {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 ) & b_{1} = {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) ) & b_{1} = {a,b} ) iff ex a, b being Int-Location ex f being FinSeq-Location st

( ( i = b := (f,a) or i = (f,a) := b ) & b_{1} = {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) ) & b_{1} = {a,b} ) iff ex a being Int-Location ex f being FinSeq-Location st

( ( i = a :=len f or i = f :=<0,...,0> a ) & b_{1} = {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 ) & b_{1} = {a} ) iff ex a, b being Int-Location ex f being FinSeq-Location st

( ( i = b := (f,a) or i = (f,a) := b ) & b_{1} = {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 ) & b_{1} = {a} ) iff ex a being Int-Location ex f being FinSeq-Location st

( ( i = a :=len f or i = f :=<0,...,0> a ) & b_{1} = {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 ) & b_{1} = {a,b} ) iff ex a being Int-Location ex f being FinSeq-Location st

( ( i = a :=len f or i = f :=<0,...,0> a ) & b_{1} = {a} ) ) ) )
by ENUMSET1:def 3;

end;
func UsedIntLoc i -> Element of Fin Int-Locations means :Def1: :: SF_MASTR:def 1

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 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 = {} ;

( ( InsCode i in {1,2,3,4,5} implies ex b

( ( i = a := b or i = AddTo (a,b) or i = SubFrom (a,b) or i = MultBy (a,b) or i = Divide (a,b) ) & b

( ( i = a =0_goto l or i = a >0_goto l ) & b

( ( i = b := (f,a) or i = (f,a) := b ) & b

( ( i = a :=len f or i = f :=<0,...,0> a ) & b

proof end;

uniqueness for b

( ( 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) ) & b

( ( i = a := b or i = AddTo (a,b) or i = SubFrom (a,b) or i = MultBy (a,b) or i = Divide (a,b) ) & b

( ( i = a =0_goto l or i = a >0_goto l ) & b

( ( i = a =0_goto l or i = a >0_goto l ) & b

( ( i = b := (f,a) or i = (f,a) := b ) & b

( ( i = b := (f,a) or i = (f,a) := b ) & b

( ( i = a :=len f or i = f :=<0,...,0> a ) & b

( ( i = a :=len f or i = f :=<0,...,0> a ) & b

proof end;

consistency for b

( ( 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) ) & b

( ( i = a =0_goto l or i = a >0_goto l ) & b

( ( i = a := b or i = AddTo (a,b) or i = SubFrom (a,b) or i = MultBy (a,b) or i = Divide (a,b) ) & b

( ( i = b := (f,a) or i = (f,a) := b ) & b

( ( i = a := b or i = AddTo (a,b) or i = SubFrom (a,b) or i = MultBy (a,b) or i = Divide (a,b) ) & b

( ( i = a :=len f or i = f :=<0,...,0> a ) & b

( ( i = a =0_goto l or i = a >0_goto l ) & b

( ( i = b := (f,a) or i = (f,a) := b ) & b

( ( i = a =0_goto l or i = a >0_goto l ) & b

( ( i = a :=len f or i = f :=<0,...,0> a ) & b

( ( i = b := (f,a) or i = (f,a) := b ) & b

( ( i = a :=len f or i = f :=<0,...,0> a ) & b

:: deftheorem Def1 defines UsedIntLoc SF_MASTR:def 1 :

for i being Instruction of SCM+FSA

for b_{2} being Element of Fin Int-Locations holds

( ( InsCode i in {1,2,3,4,5} implies ( b_{2} = 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) ) & b_{2} = {a,b} ) ) ) & ( ( InsCode i = 7 or InsCode i = 8 ) implies ( b_{2} = 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 ) & b_{2} = {a} ) ) ) & ( ( InsCode i = 9 or InsCode i = 10 ) implies ( b_{2} = UsedIntLoc i iff ex a, b being Int-Location ex f being FinSeq-Location st

( ( i = b := (f,a) or i = (f,a) := b ) & b_{2} = {a,b} ) ) ) & ( ( InsCode i = 11 or InsCode i = 12 ) implies ( b_{2} = UsedIntLoc i iff ex a being Int-Location ex f being FinSeq-Location st

( ( i = a :=len f or i = f :=<0,...,0> a ) & b_{2} = {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 ( b_{2} = UsedIntLoc i iff b_{2} = {} ) ) );

for i being Instruction of SCM+FSA

for b

( ( InsCode i in {1,2,3,4,5} implies ( b

( ( i = a := b or i = AddTo (a,b) or i = SubFrom (a,b) or i = MultBy (a,b) or i = Divide (a,b) ) & b

( ( i = a =0_goto l or i = a >0_goto l ) & b

( ( i = b := (f,a) or i = (f,a) := b ) & b

( ( i = a :=len f or i = f :=<0,...,0> a ) & b

theorem Th14: :: SF_MASTR:14

for a, b being Int-Location

for i being Instruction of SCM+FSA st ( i = a := b or i = AddTo (a,b) or i = SubFrom (a,b) or i = MultBy (a,b) or i = Divide (a,b) ) holds

UsedIntLoc i = {a,b}

for i being Instruction of SCM+FSA st ( i = a := b or i = AddTo (a,b) or i = SubFrom (a,b) or i = MultBy (a,b) or i = Divide (a,b) ) holds

UsedIntLoc i = {a,b}

proof end;

theorem Th16: :: SF_MASTR:16

for a being Int-Location

for l being Element of NAT

for i being Instruction of SCM+FSA st ( i = a =0_goto l or i = a >0_goto l ) holds

UsedIntLoc i = {a}

for l being Element of NAT

for i being Instruction of SCM+FSA st ( i = a =0_goto l or i = a >0_goto l ) holds

UsedIntLoc i = {a}

proof end;

theorem Th17: :: SF_MASTR:17

for b, a being Int-Location

for f being FinSeq-Location

for i being Instruction of SCM+FSA st ( i = b := (f,a) or i = (f,a) := b ) holds

UsedIntLoc i = {a,b}

for f being FinSeq-Location

for i being Instruction of SCM+FSA st ( i = b := (f,a) or i = (f,a) := b ) holds

UsedIntLoc i = {a,b}

proof end;

theorem Th18: :: SF_MASTR:18

for a being Int-Location

for f being FinSeq-Location

for i being Instruction of SCM+FSA st ( i = a :=len f or i = f :=<0,...,0> a ) holds

UsedIntLoc i = {a}

for f being FinSeq-Location

for i being Instruction of SCM+FSA st ( i = a :=len f or i = f :=<0,...,0> a ) holds

UsedIntLoc i = {a}

proof end;

definition

let p be Function;

ex b_{1} being Subset of Int-Locations ex UIL being Function of the InstructionsF of SCM+FSA,(Fin Int-Locations) st

( ( for i being Instruction of SCM+FSA holds UIL . i = UsedIntLoc i ) & b_{1} = Union (UIL * p) )

for b_{1}, b_{2} being Subset of Int-Locations st ex UIL being Function of the InstructionsF of SCM+FSA,(Fin Int-Locations) st

( ( for i being Instruction of SCM+FSA holds UIL . i = UsedIntLoc i ) & b_{1} = Union (UIL * p) ) & ex UIL being Function of the InstructionsF of SCM+FSA,(Fin Int-Locations) st

( ( for i being Instruction of SCM+FSA holds UIL . i = UsedIntLoc i ) & b_{2} = Union (UIL * p) ) holds

b_{1} = b_{2}

end;
func UsedIntLoc p -> Subset of Int-Locations means :Def2: :: SF_MASTR:def 2

ex UIL being Function of the InstructionsF of SCM+FSA,(Fin Int-Locations) st

( ( for i being Instruction of SCM+FSA holds UIL . i = UsedIntLoc i ) & it = Union (UIL * p) );

existence ex UIL being Function of the InstructionsF of SCM+FSA,(Fin Int-Locations) st

( ( for i being Instruction of SCM+FSA holds UIL . i = UsedIntLoc i ) & it = Union (UIL * p) );

ex b

( ( for i being Instruction of SCM+FSA holds UIL . i = UsedIntLoc i ) & b

proof end;

uniqueness for b

( ( for i being Instruction of SCM+FSA holds UIL . i = UsedIntLoc i ) & b

( ( for i being Instruction of SCM+FSA holds UIL . i = UsedIntLoc i ) & b

b

proof end;

:: deftheorem Def2 defines UsedIntLoc SF_MASTR:def 2 :

for p being Function

for b_{2} being Subset of Int-Locations holds

( b_{2} = UsedIntLoc p iff ex UIL being Function of the InstructionsF of SCM+FSA,(Fin Int-Locations) st

( ( for i being Instruction of SCM+FSA holds UIL . i = UsedIntLoc i ) & b_{2} = Union (UIL * p) ) );

for p being Function

for b

( b

( ( for i being Instruction of SCM+FSA holds UIL . i = UsedIntLoc i ) & b

theorem Th19: :: SF_MASTR:19

for i being Instruction of SCM+FSA

for p being preProgram of SCM+FSA st i in rng p holds

UsedIntLoc i c= UsedIntLoc p

for p being preProgram of SCM+FSA st i in rng p holds

UsedIntLoc i c= UsedIntLoc p

proof end;

theorem Th21: :: SF_MASTR:21

for p, r being preProgram of SCM+FSA st dom p misses dom r holds

UsedIntLoc (p +* r) = (UsedIntLoc p) \/ (UsedIntLoc r)

UsedIntLoc (p +* r) = (UsedIntLoc p) \/ (UsedIntLoc r)

proof end;

theorem Th22: :: SF_MASTR:22

for p being preProgram of SCM+FSA

for k being Element of NAT holds UsedIntLoc p = UsedIntLoc (Shift (p,k))

for k being Element of NAT holds UsedIntLoc p = UsedIntLoc (Shift (p,k))

proof end;

theorem Th23: :: SF_MASTR:23

for i being Instruction of SCM+FSA

for k being Element of NAT holds UsedIntLoc i = UsedIntLoc (IncAddr (i,k))

for k being Element of NAT holds UsedIntLoc i = UsedIntLoc (IncAddr (i,k))

proof end;

theorem Th24: :: SF_MASTR:24

for p being preProgram of SCM+FSA

for k being Element of NAT holds UsedIntLoc p = UsedIntLoc (IncAddr (p,k))

for k being Element of NAT holds UsedIntLoc p = UsedIntLoc (IncAddr (p,k))

proof end;

theorem :: SF_MASTR:29

for i being Instruction of SCM+FSA

for J being Program of holds UsedIntLoc (i ";" J) = (UsedIntLoc i) \/ (UsedIntLoc J)

for J being Program of holds UsedIntLoc (i ";" J) = (UsedIntLoc i) \/ (UsedIntLoc J)

proof end;

theorem :: SF_MASTR:30

for j being Instruction of SCM+FSA

for I being Program of holds UsedIntLoc (I ";" j) = (UsedIntLoc I) \/ (UsedIntLoc j)

for I being Program of holds UsedIntLoc (I ";" j) = (UsedIntLoc I) \/ (UsedIntLoc j)

proof end;

begin

definition

let i be Instruction of SCM+FSA;

( ( ( InsCode i = 9 or InsCode i = 10 ) implies ex b_{1} 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 ) & b_{1} = {f} ) ) & ( ( InsCode i = 11 or InsCode i = 12 ) implies ex b_{1} 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 ) & b_{1} = {f} ) ) & ( InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 or ex b_{1} being Element of Fin FinSeq-Locations st b_{1} = {} ) )

for b_{1}, b_{2} 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 ) & b_{1} = {f} ) & ex a, b being Int-Location ex f being FinSeq-Location st

( ( i = b := (f,a) or i = (f,a) := b ) & b_{2} = {f} ) implies b_{1} = b_{2} ) & ( ( 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 ) & b_{1} = {f} ) & ex a being Int-Location ex f being FinSeq-Location st

( ( i = a :=len f or i = f :=<0,...,0> a ) & b_{2} = {f} ) implies b_{1} = b_{2} ) & ( InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 or not b_{1} = {} or not b_{2} = {} or b_{1} = b_{2} ) )

for b_{1} 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 ) & b_{1} = {f} ) iff ex a being Int-Location ex f being FinSeq-Location st

( ( i = a :=len f or i = f :=<0,...,0> a ) & b_{1} = {f} ) )
;

end;
func UsedInt*Loc i -> Element of Fin FinSeq-Locations means :Def3: :: SF_MASTR:def 3

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 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 = {} ;

( ( ( InsCode i = 9 or InsCode i = 10 ) implies ex b

( ( i = b := (f,a) or i = (f,a) := b ) & b

( ( i = a :=len f or i = f :=<0,...,0> a ) & b

proof end;

uniqueness for b

( ( ( 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 ) & b

( ( i = b := (f,a) or i = (f,a) := b ) & b

( ( i = a :=len f or i = f :=<0,...,0> a ) & b

( ( i = a :=len f or i = f :=<0,...,0> a ) & b

proof end;

consistency for b

( ex a, b being Int-Location ex f being FinSeq-Location st

( ( i = b := (f,a) or i = (f,a) := b ) & b

( ( i = a :=len f or i = f :=<0,...,0> a ) & b

:: deftheorem Def3 defines UsedInt*Loc SF_MASTR:def 3 :

for i being Instruction of SCM+FSA

for b_{2} being Element of Fin FinSeq-Locations holds

( ( ( InsCode i = 9 or InsCode i = 10 ) implies ( b_{2} = 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 ) & b_{2} = {f} ) ) ) & ( ( InsCode i = 11 or InsCode i = 12 ) implies ( b_{2} = 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 ) & b_{2} = {f} ) ) ) & ( InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 or ( b_{2} = UsedInt*Loc i iff b_{2} = {} ) ) );

for i being Instruction of SCM+FSA

for b

( ( ( InsCode i = 9 or InsCode i = 10 ) implies ( b

( ( i = b := (f,a) or i = (f,a) := b ) & b

( ( i = a :=len f or i = f :=<0,...,0> a ) & b

theorem Th32: :: SF_MASTR:32

for a, b being Int-Location

for l being Element of NAT

for i being Instruction of SCM+FSA st ( i = halt SCM+FSA or i = a := b or i = AddTo (a,b) or i = SubFrom (a,b) or i = MultBy (a,b) or i = Divide (a,b) or i = goto l or i = a =0_goto l or i = a >0_goto l ) holds

UsedInt*Loc i = {}

for l being Element of NAT

for i being Instruction of SCM+FSA st ( i = halt SCM+FSA or i = a := b or i = AddTo (a,b) or i = SubFrom (a,b) or i = MultBy (a,b) or i = Divide (a,b) or i = goto l or i = a =0_goto l or i = a >0_goto l ) holds

UsedInt*Loc i = {}

proof end;

theorem Th33: :: SF_MASTR:33

for b, a being Int-Location

for f being FinSeq-Location

for i being Instruction of SCM+FSA st ( i = b := (f,a) or i = (f,a) := b ) holds

UsedInt*Loc i = {f}

for f being FinSeq-Location

for i being Instruction of SCM+FSA st ( i = b := (f,a) or i = (f,a) := b ) holds

UsedInt*Loc i = {f}

proof end;

theorem Th34: :: SF_MASTR:34

for a being Int-Location

for f being FinSeq-Location

for i being Instruction of SCM+FSA st ( i = a :=len f or i = f :=<0,...,0> a ) holds

UsedInt*Loc i = {f}

for f being FinSeq-Location

for i being Instruction of SCM+FSA st ( i = a :=len f or i = f :=<0,...,0> a ) holds

UsedInt*Loc i = {f}

proof end;

definition

let p be Function;

ex b_{1} being Subset of FinSeq-Locations ex UIL being Function of the InstructionsF of SCM+FSA,(Fin FinSeq-Locations) st

( ( for i being Instruction of SCM+FSA holds UIL . i = UsedInt*Loc i ) & b_{1} = Union (UIL * p) )

for b_{1}, b_{2} being Subset of FinSeq-Locations st ex UIL being Function of the InstructionsF of SCM+FSA,(Fin FinSeq-Locations) st

( ( for i being Instruction of SCM+FSA holds UIL . i = UsedInt*Loc i ) & b_{1} = Union (UIL * p) ) & ex UIL being Function of the InstructionsF of SCM+FSA,(Fin FinSeq-Locations) st

( ( for i being Instruction of SCM+FSA holds UIL . i = UsedInt*Loc i ) & b_{2} = Union (UIL * p) ) holds

b_{1} = b_{2}

end;
func UsedInt*Loc p -> Subset of FinSeq-Locations means :Def4: :: SF_MASTR:def 4

ex UIL being Function of the InstructionsF of SCM+FSA,(Fin FinSeq-Locations) st

( ( for i being Instruction of SCM+FSA holds UIL . i = UsedInt*Loc i ) & it = Union (UIL * p) );

existence ex UIL being Function of the InstructionsF of SCM+FSA,(Fin FinSeq-Locations) st

( ( for i being Instruction of SCM+FSA holds UIL . i = UsedInt*Loc i ) & it = Union (UIL * p) );

ex b

( ( for i being Instruction of SCM+FSA holds UIL . i = UsedInt*Loc i ) & b

proof end;

uniqueness for b

( ( for i being Instruction of SCM+FSA holds UIL . i = UsedInt*Loc i ) & b

( ( for i being Instruction of SCM+FSA holds UIL . i = UsedInt*Loc i ) & b

b

proof end;

:: deftheorem Def4 defines UsedInt*Loc SF_MASTR:def 4 :

for p being Function

for b_{2} being Subset of FinSeq-Locations holds

( b_{2} = UsedInt*Loc p iff ex UIL being Function of the InstructionsF of SCM+FSA,(Fin FinSeq-Locations) st

( ( for i being Instruction of SCM+FSA holds UIL . i = UsedInt*Loc i ) & b_{2} = Union (UIL * p) ) );

for p being Function

for b

( b

( ( for i being Instruction of SCM+FSA holds UIL . i = UsedInt*Loc i ) & b

theorem Th35: :: SF_MASTR:35

for i being Instruction of SCM+FSA

for p being preProgram of SCM+FSA st i in rng p holds

UsedInt*Loc i c= UsedInt*Loc p

for p being preProgram of SCM+FSA st i in rng p holds

UsedInt*Loc i c= UsedInt*Loc p

proof end;

theorem :: SF_MASTR:36

for p, r being preProgram of SCM+FSA holds UsedInt*Loc (p +* r) c= (UsedInt*Loc p) \/ (UsedInt*Loc r)

proof end;

theorem Th37: :: SF_MASTR:37

for p, r being preProgram of SCM+FSA st dom p misses dom r holds

UsedInt*Loc (p +* r) = (UsedInt*Loc p) \/ (UsedInt*Loc r)

UsedInt*Loc (p +* r) = (UsedInt*Loc p) \/ (UsedInt*Loc r)

proof end;

theorem Th38: :: SF_MASTR:38

for p being preProgram of SCM+FSA

for k being Element of NAT holds UsedInt*Loc p = UsedInt*Loc (Shift (p,k))

for k being Element of NAT holds UsedInt*Loc p = UsedInt*Loc (Shift (p,k))

proof end;

theorem Th39: :: SF_MASTR:39

for i being Instruction of SCM+FSA

for k being Element of NAT holds UsedInt*Loc i = UsedInt*Loc (IncAddr (i,k))

for k being Element of NAT holds UsedInt*Loc i = UsedInt*Loc (IncAddr (i,k))

proof end;

theorem Th40: :: SF_MASTR:40

for p being preProgram of SCM+FSA

for k being Element of NAT holds UsedInt*Loc p = UsedInt*Loc (IncAddr (p,k))

for k being Element of NAT holds UsedInt*Loc p = UsedInt*Loc (IncAddr (p,k))

proof end;

theorem :: SF_MASTR:45

for i being Instruction of SCM+FSA

for J being Program of holds UsedInt*Loc (i ";" J) = (UsedInt*Loc i) \/ (UsedInt*Loc J)

for J being Program of holds UsedInt*Loc (i ";" J) = (UsedInt*Loc i) \/ (UsedInt*Loc J)

proof end;

theorem :: SF_MASTR:46

for j being Instruction of SCM+FSA

for I being Program of holds UsedInt*Loc (I ";" j) = (UsedInt*Loc I) \/ (UsedInt*Loc j)

for I being Program of holds UsedInt*Loc (I ";" j) = (UsedInt*Loc I) \/ (UsedInt*Loc j)

proof end;

theorem :: SF_MASTR:47

for i, j being Instruction of SCM+FSA holds UsedInt*Loc (i ";" j) = (UsedInt*Loc i) \/ (UsedInt*Loc j)

proof end;

begin

definition

canceled;

end;
theorem :: SF_MASTR:48

theorem :: SF_MASTR:49

for m, n being Element of NAT

for L being finite Subset of Int-Locations st FirstNotIn L = intloc m & not intloc n in L holds

m <= n by SCMFSA_M:15;

for L being finite Subset of Int-Locations st FirstNotIn L = intloc m & not intloc n in L holds

m <= n by SCMFSA_M:15;

definition

let p be preProgram of SCM+FSA;

ex b_{1} being Int-Location ex sil being finite Subset of Int-Locations st

( sil = (UsedIntLoc p) \/ {(intloc 0)} & b_{1} = FirstNotIn sil )

for b_{1}, b_{2} being Int-Location st ex sil being finite Subset of Int-Locations st

( sil = (UsedIntLoc p) \/ {(intloc 0)} & b_{1} = FirstNotIn sil ) & ex sil being finite Subset of Int-Locations st

( sil = (UsedIntLoc p) \/ {(intloc 0)} & b_{2} = FirstNotIn sil ) holds

b_{1} = b_{2}
;

end;
func FirstNotUsed p -> Int-Location means :Def6: :: SF_MASTR:def 6

ex sil being finite Subset of Int-Locations st

( sil = (UsedIntLoc p) \/ {(intloc 0)} & it = FirstNotIn sil );

existence ex sil being finite Subset of Int-Locations st

( sil = (UsedIntLoc p) \/ {(intloc 0)} & it = FirstNotIn sil );

ex b

( sil = (UsedIntLoc p) \/ {(intloc 0)} & b

proof end;

uniqueness for b

( sil = (UsedIntLoc p) \/ {(intloc 0)} & b

( sil = (UsedIntLoc p) \/ {(intloc 0)} & b

b

:: deftheorem Def6 defines FirstNotUsed SF_MASTR:def 6 :

for p being preProgram of SCM+FSA

for b_{2} being Int-Location holds

( b_{2} = FirstNotUsed p iff ex sil being finite Subset of Int-Locations st

( sil = (UsedIntLoc p) \/ {(intloc 0)} & b_{2} = FirstNotIn sil ) );

for p being preProgram of SCM+FSA

for b

( b

( sil = (UsedIntLoc p) \/ {(intloc 0)} & b

registration
end;

theorem :: SF_MASTR:51

for a, b being Int-Location

for p being preProgram of SCM+FSA st ( a := b in rng p or AddTo (a,b) in rng p or SubFrom (a,b) in rng p or MultBy (a,b) in rng p or Divide (a,b) in rng p ) holds

( FirstNotUsed p <> a & FirstNotUsed p <> b )

for p being preProgram of SCM+FSA st ( a := b in rng p or AddTo (a,b) in rng p or SubFrom (a,b) in rng p or MultBy (a,b) in rng p or Divide (a,b) in rng p ) holds

( FirstNotUsed p <> a & FirstNotUsed p <> b )

proof end;

theorem :: SF_MASTR:52

for a being Int-Location

for l being Element of NAT

for p being preProgram of SCM+FSA st ( a =0_goto l in rng p or a >0_goto l in rng p ) holds

FirstNotUsed p <> a

for l being Element of NAT

for p being preProgram of SCM+FSA st ( a =0_goto l in rng p or a >0_goto l in rng p ) holds

FirstNotUsed p <> a

proof end;

theorem :: SF_MASTR:53

for b, a being Int-Location

for f being FinSeq-Location

for p being preProgram of SCM+FSA st ( b := (f,a) in rng p or (f,a) := b in rng p ) holds

( FirstNotUsed p <> a & FirstNotUsed p <> b )

for f being FinSeq-Location

for p being preProgram of SCM+FSA st ( b := (f,a) in rng p or (f,a) := b in rng p ) holds

( FirstNotUsed p <> a & FirstNotUsed p <> b )

proof end;

theorem :: SF_MASTR:54

for a being Int-Location

for f being FinSeq-Location

for p being preProgram of SCM+FSA st ( a :=len f in rng p or f :=<0,...,0> a in rng p ) holds

FirstNotUsed p <> a

for f being FinSeq-Location

for p being preProgram of SCM+FSA st ( a :=len f in rng p or f :=<0,...,0> a in rng p ) holds

FirstNotUsed p <> a

proof end;

begin

definition

canceled;

end;
theorem :: SF_MASTR:55

theorem :: SF_MASTR:56

for m, n being Element of NAT

for L being finite Subset of FinSeq-Locations st First*NotIn L = fsloc m & not fsloc n in L holds

m <= n by SCMFSA_M:17;

for L being finite Subset of FinSeq-Locations st First*NotIn L = fsloc m & not fsloc n in L holds

m <= n by SCMFSA_M:17;

definition

let p be preProgram of SCM+FSA;

ex b_{1} being FinSeq-Location ex sil being finite Subset of FinSeq-Locations st

( sil = UsedInt*Loc p & b_{1} = First*NotIn sil )

for b_{1}, b_{2} being FinSeq-Location st ex sil being finite Subset of FinSeq-Locations st

( sil = UsedInt*Loc p & b_{1} = First*NotIn sil ) & ex sil being finite Subset of FinSeq-Locations st

( sil = UsedInt*Loc p & b_{2} = First*NotIn sil ) holds

b_{1} = b_{2}
;

end;
func First*NotUsed p -> FinSeq-Location means :Def8: :: SF_MASTR:def 8

ex sil being finite Subset of FinSeq-Locations st

( sil = UsedInt*Loc p & it = First*NotIn sil );

existence ex sil being finite Subset of FinSeq-Locations st

( sil = UsedInt*Loc p & it = First*NotIn sil );

ex b

( sil = UsedInt*Loc p & b

proof end;

uniqueness for b

( sil = UsedInt*Loc p & b

( sil = UsedInt*Loc p & b

b

:: deftheorem Def8 defines First*NotUsed SF_MASTR:def 8 :

for p being preProgram of SCM+FSA

for b_{2} being FinSeq-Location holds

( b_{2} = First*NotUsed p iff ex sil being finite Subset of FinSeq-Locations st

( sil = UsedInt*Loc p & b_{2} = First*NotIn sil ) );

for p being preProgram of SCM+FSA

for b

( b

( sil = UsedInt*Loc p & b

theorem :: SF_MASTR:58

for b, a being Int-Location

for f being FinSeq-Location

for p being preProgram of SCM+FSA st ( b := (f,a) in rng p or (f,a) := b in rng p ) holds

First*NotUsed p <> f

for f being FinSeq-Location

for p being preProgram of SCM+FSA st ( b := (f,a) in rng p or (f,a) := b in rng p ) holds

First*NotUsed p <> f

proof end;

theorem :: SF_MASTR:59

for a being Int-Location

for f being FinSeq-Location

for p being preProgram of SCM+FSA st ( a :=len f in rng p or f :=<0,...,0> a in rng p ) holds

First*NotUsed p <> f

for f being FinSeq-Location

for p being preProgram of SCM+FSA st ( a :=len f in rng p or f :=<0,...,0> a in rng p ) holds

First*NotUsed p <> f

proof end;

begin

theorem Th60: :: SF_MASTR:60

for c being Int-Location

for i being Instruction of SCM+FSA

for s being State of SCM+FSA st not c in UsedIntLoc i holds

(Exec (i,s)) . c = s . c

for i being Instruction of SCM+FSA

for s being State of SCM+FSA st not c in UsedIntLoc i holds

(Exec (i,s)) . c = s . c

proof end;

theorem :: SF_MASTR:61

for a being Int-Location

for I being Program of

for n being Element of NAT

for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA st I c= P & ( for m being Element of NAT st m < n holds

IC (Comput (P,s,m)) in dom I ) & not a in UsedIntLoc I holds

(Comput (P,s,n)) . a = s . a

for I being Program of

for n being Element of NAT

for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA st I c= P & ( for m being Element of NAT st m < n holds

IC (Comput (P,s,m)) in dom I ) & not a in UsedIntLoc I holds

(Comput (P,s,n)) . a = s . a

proof end;

theorem Th62: :: SF_MASTR:62

for f being FinSeq-Location

for i being Instruction of SCM+FSA

for s being State of SCM+FSA st not f in UsedInt*Loc i holds

(Exec (i,s)) . f = s . f

for i being Instruction of SCM+FSA

for s being State of SCM+FSA st not f in UsedInt*Loc i holds

(Exec (i,s)) . f = s . f

proof end;

theorem :: SF_MASTR:63

for f being FinSeq-Location

for I being Program of

for n being Element of NAT

for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA st I c= P & ( for m being Element of NAT st m < n holds

IC (Comput (P,s,m)) in dom I ) & not f in UsedInt*Loc I holds

(Comput (P,s,n)) . f = s . f

for I being Program of

for n being Element of NAT

for s being State of SCM+FSA

for P being Instruction-Sequence of SCM+FSA st I c= P & ( for m being Element of NAT st m < n holds

IC (Comput (P,s,m)) in dom I ) & not f in UsedInt*Loc I holds

(Comput (P,s,n)) . f = s . f

proof end;

theorem Th64: :: SF_MASTR:64

for i being Instruction of SCM+FSA

for s, t being State of SCM+FSA st s | (UsedIntLoc i) = t | (UsedIntLoc i) & s | (UsedInt*Loc i) = t | (UsedInt*Loc i) & IC s = IC t holds

( IC (Exec (i,s)) = IC (Exec (i,t)) & (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) & (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) )

for s, t being State of SCM+FSA st s | (UsedIntLoc i) = t | (UsedIntLoc i) & s | (UsedInt*Loc i) = t | (UsedInt*Loc i) & IC s = IC t holds

( IC (Exec (i,s)) = IC (Exec (i,t)) & (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) & (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) )

proof end;

theorem :: SF_MASTR:65

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 ) ) ) )

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 ) ) ) )

proof end;