:: Memory handling for SCM+FSA
:: by Piotr Rudnicki and Andrzej Trybulec
::
:: Received July 18, 1996
:: Copyright (c) 1996-2012 Association of Mizar Users


begin

theorem Th1: :: SF_MASTR:1
for a1, b1, a2, b2 being Int-Location st a1 := b1 = a2 := b2 holds
( a1 = a2 & b1 = b2 )
proofend;

theorem Th2: :: SF_MASTR:2
for a1, b1, a2, b2 being Int-Location st AddTo (a1,b1) = AddTo (a2,b2) holds
( a1 = a2 & b1 = b2 )
proofend;

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

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

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

theorem :: SF_MASTR:6
for l1, l2 being Element of NAT st goto l1 = goto l2 holds
l1 = l2
proofend;

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

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

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

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

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

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 &amp; f1 = f2 )
proofend;

begin

definition
let i be Instruction of SCM+FSA;
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) ) &amp; 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 ) &amp; 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 ) &amp; 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 ) &amp; 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) ) &amp; b1 = {a,b} ) ) &amp; ( ( 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 ) &amp; b1 = {a} ) ) &amp; ( ( 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 ) &amp; b1 = {a,b} ) ) &amp; ( ( 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 ) &amp; b1 = {a} ) ) &amp; ( 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 = {} ) )
proofend;
uniqueness
 for b1, b2 being Element of Fin Int-Locations holds
( ( InsCode i in {1,2,3,4,5} &amp; 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) ) &amp; b1 = {a,b} ) &amp; 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) ) &amp; b2 = {a,b} ) implies b1 = b2 ) &amp; ( ( InsCode i = 7 or InsCode i = 8 ) &amp; ex a being Int-Location ex l being Element of NAT st
( ( i = a =0_goto l or i = a >0_goto l ) &amp; b1 = {a} ) &amp; ex a being Int-Location ex l being Element of NAT st
( ( i = a =0_goto l or i = a >0_goto l ) &amp; b2 = {a} ) implies b1 = b2 ) &amp; ( ( InsCode i = 9 or InsCode i = 10 ) &amp; ex a, b being Int-Location ex f being FinSeq-Location st
( ( i = b := (f,a) or i = (f,a) := b ) &amp; b1 = {a,b} ) &amp; ex a, b being Int-Location ex f being FinSeq-Location st
( ( i = b := (f,a) or i = (f,a) := b ) &amp; b2 = {a,b} ) implies b1 = b2 ) &amp; ( ( InsCode i = 11 or InsCode i = 12 ) &amp; ex a being Int-Location ex f being FinSeq-Location st
( ( i = a :=len f or i = f :=<0,...,0> a ) &amp; b1 = {a} ) &amp; ex a being Int-Location ex f being FinSeq-Location st
( ( i = a :=len f or i = f :=<0,...,0> a ) &amp; b2 = {a} ) implies b1 = b2 ) &amp; ( 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 ) )
proofend;
consistency
 for b1 being Element of Fin Int-Locations holds
( ( InsCode i in {1,2,3,4,5} &amp; ( 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) ) &amp; 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 ) &amp; b1 = {a} ) ) ) &amp; ( InsCode i in {1,2,3,4,5} &amp; ( 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) ) &amp; 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 ) &amp; b1 = {a,b} ) ) ) &amp; ( InsCode i in {1,2,3,4,5} &amp; ( 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) ) &amp; 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 ) &amp; b1 = {a} ) ) ) &amp; ( ( InsCode i = 7 or InsCode i = 8 ) &amp; ( 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 ) &amp; b1 = {a} ) iff ex a, b being Int-Location ex f being FinSeq-Location st
( ( i = b := (f,a) or i = (f,a) := b ) &amp; b1 = {a,b} ) ) ) &amp; ( ( InsCode i = 7 or InsCode i = 8 ) &amp; ( 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 ) &amp; b1 = {a} ) iff ex a being Int-Location ex f being FinSeq-Location st
( ( i = a :=len f or i = f :=<0,...,0> a ) &amp; b1 = {a} ) ) ) &amp; ( ( InsCode i = 9 or InsCode i = 10 ) &amp; ( 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 ) &amp; 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 ) &amp; 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) ) &amp; b2 = {a,b} ) ) ) &amp; ( ( 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 ) &amp; b2 = {a} ) ) ) &amp; ( ( 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 ) &amp; b2 = {a,b} ) ) ) &amp; ( ( 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 ) &amp; b2 = {a} ) ) ) &amp; ( 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 Th13: :: SF_MASTR:13
UsedIntLoc (halt SCM+FSA) = {}
proofend;

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}
proofend;

theorem Th15: :: SF_MASTR:15
for l being Element of NAT holds UsedIntLoc (goto l) = {}
proofend;

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}
proofend;

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}
proofend;

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}
proofend;

definition
let p be Function;
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 ) &amp; it = Union (UIL * p) );
existence
 ex b1 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 ) &amp; b1 = Union (UIL * p) )
proofend;
uniqueness
 for b1, b2 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 ) &amp; b1 = Union (UIL * p) ) &amp; 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 ) &amp; b2 = Union (UIL * p) ) holds
b1 = b2
proofend;
end;

:: 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 InstructionsF of SCM+FSA,(Fin Int-Locations) st
( ( for i being Instruction of SCM+FSA holds UIL . i = UsedIntLoc i ) &amp; b2 = Union (UIL * p) ) );

registration
let p be preProgram of SCM+FSA;
cluster UsedIntLoc p ->  finite ;
coherence
 UsedIntLoc p is finite
proofend;
end;

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
proofend;

theorem :: SF_MASTR:20
for p, r being preProgram of SCM+FSA holds UsedIntLoc (p +* r) c= (UsedIntLoc p) \/ (UsedIntLoc r)
proofend;

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

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

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

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

theorem Th25: :: SF_MASTR:25
for I being Program of
for k being Element of NAT holds UsedIntLoc I = UsedIntLoc (Reloc (I,k))
proofend;

theorem Th26: :: SF_MASTR:26
for I being Program of holds UsedIntLoc I = UsedIntLoc (Directed I)
proofend;

theorem Th27: :: SF_MASTR:27
for I, J being Program of holds UsedIntLoc (I ";" J) = (UsedIntLoc I) \/ (UsedIntLoc J)
proofend;

theorem Th28: :: SF_MASTR:28
for i being Instruction of SCM+FSA holds UsedIntLoc (Macro i) = UsedIntLoc i
proofend;

theorem :: SF_MASTR:29
for i being Instruction of SCM+FSA
for J being Program of holds UsedIntLoc (i ";" J) = (UsedIntLoc i) \/ (UsedIntLoc J)
proofend;

theorem :: SF_MASTR:30
for j being Instruction of SCM+FSA
for I being Program of holds UsedIntLoc (I ";" j) = (UsedIntLoc I) \/ (UsedIntLoc j)
proofend;

theorem :: SF_MASTR:31
for i, j being Instruction of SCM+FSA holds UsedIntLoc (i ";" j) = (UsedIntLoc i) \/ (UsedIntLoc j)
proofend;

begin

definition
let i be Instruction of SCM+FSA;
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 ) &amp; 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 ) &amp; 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 ) &amp; b1 = {f} ) ) &amp; ( ( 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 ) &amp; b1 = {f} ) ) &amp; ( 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 = {} ) )
proofend;
uniqueness
 for b1, b2 being Element of Fin FinSeq-Locations holds
( ( ( InsCode i = 9 or InsCode i = 10 ) &amp; ex a, b being Int-Location ex f being FinSeq-Location st
( ( i = b := (f,a) or i = (f,a) := b ) &amp; b1 = {f} ) &amp; ex a, b being Int-Location ex f being FinSeq-Location st
( ( i = b := (f,a) or i = (f,a) := b ) &amp; b2 = {f} ) implies b1 = b2 ) &amp; ( ( InsCode i = 11 or InsCode i = 12 ) &amp; ex a being Int-Location ex f being FinSeq-Location st
( ( i = a :=len f or i = f :=<0,...,0> a ) &amp; b1 = {f} ) &amp; ex a being Int-Location ex f being FinSeq-Location st
( ( i = a :=len f or i = f :=<0,...,0> a ) &amp; b2 = {f} ) implies b1 = b2 ) &amp; ( InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 or not b1 = {} or not b2 = {} or b1 = b2 ) )
proofend;
consistency
 for b1 being Element of Fin FinSeq-Locations st ( InsCode i = 9 or InsCode i = 10 ) &amp; ( 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 ) &amp; b1 = {f} ) iff ex a being Int-Location ex f being FinSeq-Location st
( ( i = a :=len f or i = f :=<0,...,0> a ) &amp; 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 ) &amp; b2 = {f} ) ) ) &amp; ( ( 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 ) &amp; b2 = {f} ) ) ) &amp; ( InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 or ( b2 = UsedInt*Loc i iff b2 = {} ) ) );

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

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}
proofend;

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}
proofend;

definition
let p be Function;
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 ) &amp; it = Union (UIL * p) );
existence
 ex b1 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 ) &amp; b1 = Union (UIL * p) )
proofend;
uniqueness
 for b1, b2 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 ) &amp; b1 = Union (UIL * p) ) &amp; 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 ) &amp; b2 = Union (UIL * p) ) holds
b1 = b2
proofend;
end;

:: 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 InstructionsF of SCM+FSA,(Fin FinSeq-Locations) st
( ( for i being Instruction of SCM+FSA holds UIL . i = UsedInt*Loc i ) &amp; b2 = Union (UIL * p) ) );

registration
let p be preProgram of SCM+FSA;
cluster UsedInt*Loc p ->  finite ;
coherence
 UsedInt*Loc p is finite
proofend;
end;

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
proofend;

theorem :: SF_MASTR:36
for p, r being preProgram of SCM+FSA holds UsedInt*Loc (p +* r) c= (UsedInt*Loc p) \/ (UsedInt*Loc r)
proofend;

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

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

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

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

theorem Th41: :: SF_MASTR:41
for I being Program of
for k being Element of NAT holds UsedInt*Loc I = UsedInt*Loc (Reloc (I,k))
proofend;

theorem Th42: :: SF_MASTR:42
for I being Program of holds UsedInt*Loc I = UsedInt*Loc (Directed I)
proofend;

theorem Th43: :: SF_MASTR:43
for I, J being Program of holds UsedInt*Loc (I ";" J) = (UsedInt*Loc I) \/ (UsedInt*Loc J)
proofend;

theorem Th44: :: SF_MASTR:44
for i being Instruction of SCM+FSA holds UsedInt*Loc (Macro i) = UsedInt*Loc i
proofend;

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

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

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

begin

definition
canceled;
end;

:: deftheorem  SF_MASTR:def_5_:_
canceled;

theorem :: SF_MASTR:48
for L being finite Subset of Int-Locations holds not FirstNotIn L in L by SCMFSA_M:14;

theorem :: SF_MASTR:49
for m, n being Element of NAT
for L being finite Subset of Int-Locations st FirstNotIn L = intloc m &amp; not intloc n in L holds
m <= n by SCMFSA_M:15;

definition
let p be preProgram of SCM+FSA;
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)} &amp; it = FirstNotIn sil );
existence
 ex b1 being Int-Location ex sil being finite Subset of Int-Locations st
( sil = (UsedIntLoc p) \/ {(intloc 0)} &amp; b1 = FirstNotIn sil )
proofend;
uniqueness
 for b1, b2 being Int-Location st ex sil being finite Subset of Int-Locations st
( sil = (UsedIntLoc p) \/ {(intloc 0)} &amp; b1 = FirstNotIn sil ) &amp; ex sil being finite Subset of Int-Locations st
( sil = (UsedIntLoc p) \/ {(intloc 0)} &amp; b2 = FirstNotIn sil ) holds
b1 = b2 ;
end;

:: deftheorem Def6 defines FirstNotUsed SF_MASTR:def_6_:_
 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)} &amp; b2 = FirstNotIn sil ) );

registration
let p be preProgram of SCM+FSA;
cluster FirstNotUsed p ->  read-write ;
coherence
 not FirstNotUsed p is read-only
proofend;
end;

theorem Th50: :: SF_MASTR:50
for p being preProgram of SCM+FSA holds not FirstNotUsed p in UsedIntLoc p
proofend;

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 &amp; FirstNotUsed p <> b )
proofend;

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
proofend;

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 &amp; FirstNotUsed p <> b )
proofend;

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
proofend;

begin

definition
canceled;
end;

:: deftheorem  SF_MASTR:def_7_:_
canceled;

theorem :: SF_MASTR:55
for L being finite Subset of FinSeq-Locations holds not First*NotIn L in L by SCMFSA_M:16;

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 &amp; not fsloc n in L holds
m <= n by SCMFSA_M:17;

definition
let p be preProgram of SCM+FSA;
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 &amp; it = First*NotIn sil );
existence
 ex b1 being FinSeq-Location ex sil being finite Subset of FinSeq-Locations st
( sil = UsedInt*Loc p &amp; b1 = First*NotIn sil )
proofend;
uniqueness
 for b1, b2 being FinSeq-Location st ex sil being finite Subset of FinSeq-Locations st
( sil = UsedInt*Loc p &amp; b1 = First*NotIn sil ) &amp; ex sil being finite Subset of FinSeq-Locations st
( sil = UsedInt*Loc p &amp; b2 = First*NotIn sil ) holds
b1 = b2 ;
end;

:: deftheorem Def8 defines First*NotUsed SF_MASTR:def_8_:_
 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 &amp; b2 = First*NotIn sil ) );

theorem Th57: :: SF_MASTR:57
for p being preProgram of SCM+FSA holds not First*NotUsed p in UsedInt*Loc p
proofend;

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
proofend;

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
proofend;

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
proofend;

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 &amp; ( for m being Element of NAT st m < n holds
IC (Comput (P,s,m)) in dom I ) &amp; not a in UsedIntLoc I holds
(Comput (P,s,n)) . a = s . a
proofend;

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
proofend;

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 &amp; ( for m being Element of NAT st m < n holds
IC (Comput (P,s,m)) in dom I ) &amp; not f in UsedInt*Loc I holds
(Comput (P,s,n)) . f = s . f
proofend;

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) &amp; s | (UsedInt*Loc i) = t | (UsedInt*Loc i) &amp; IC s = IC t holds
( IC (Exec (i,s)) = IC (Exec (i,t)) &amp; (Exec (i,s)) | (UsedIntLoc i) = (Exec (i,t)) | (UsedIntLoc i) &amp; (Exec (i,s)) | (UsedInt*Loc i) = (Exec (i,t)) | (UsedInt*Loc i) )
proofend;

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 &amp; I c= Q &amp; Start-At (0,SCM+FSA) c= s &amp; Start-At (0,SCM+FSA) c= t &amp; s | (UsedIntLoc I) = t | (UsedIntLoc I) &amp; s | (UsedInt*Loc I) = t | (UsedInt*Loc I) &amp; ( 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 ) &amp; ( for m being Element of NAT st m <= n holds
( IC (Comput (P,s,m)) = IC (Comput (Q,t,m)) &amp; ( for a being Int-Location st a in UsedIntLoc I holds
(Comput (P,s,m)) . a = (Comput (Q,t,m)) . a ) &amp; ( for f being FinSeq-Location st f in UsedInt*Loc I holds
(Comput (P,s,m)) . f = (Comput (Q,t,m)) . f ) ) ) )
proofend;