SF_MASTR: Memory handling for SCM+FSA

theorem Th1: :: SF_MASTR:1

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

proof end;

theorem Th2: :: SF_MASTR:2

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

proof end;

theorem Th3: :: SF_MASTR:3

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

proof end;

theorem Th4: :: SF_MASTR:4

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

proof end;

theorem Th5: :: SF_MASTR:5

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

proof end;

theorem :: SF_MASTR:6

for l1, l2 being Nat st goto l1 = goto l2 holds
l1 = l2

proof end;

theorem Th7: :: SF_MASTR:7

for a1, a2 being Int-Location
for l1, l2 being 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 Nat st a1 >0_goto l1 = a2 >0_goto l2 holds
( a1 = a2 & l1 = l2 )

proof end;

theorem Th9: :: SF_MASTR:9

for a1, a2, b1, b2 being Int-Location
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, a2, b1, b2 being Int-Location
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 )

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 )

proof end;

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) ) & it = {a,b} ) if InsCode i in {1,2,3,4,5}
ex a being Int-Location ex l being 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

proof end;

uniqueness

proof end;

consistency by ENUMSET1:def 3;

end;

:: deftheorem Def1 defines UsedIntLoc SF_MASTR:def 1 :

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}

proof end;

theorem Th15: :: SF_MASTR:15

for l being Nat holds UsedIntLoc (goto l) = {}

proof end;

theorem Th16: :: SF_MASTR:16

for a being Int-Location
for l being 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 a, b 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}

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}

proof end;

definition

let X be set ;

func UsedILoc X -> Subset of Int-Locations equals :: SF_MASTR:def 2
union { (UsedIntLoc i) where i is Instruction of SCM+FSA : i in X } ;

coherence

proof end;

end;

:: deftheorem defines UsedILoc SF_MASTR:def 2 :

registration

let X be finite set ;

cluster UsedILoc X -> finite ;

coherence

proof end;

end;

definition

let p be Function;

func UsedILoc p -> Subset of Int-Locations equals :: SF_MASTR:def 3
UsedILoc (rng p);

coherence ;

end;

:: deftheorem defines UsedILoc SF_MASTR:def 3 :

registration

let p be preProgram of SCM+FSA;

cluster UsedILoc p -> finite ;

coherence ;

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= UsedILoc p by Lm1;

theorem :: SF_MASTR:20

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

proof end;

theorem Th21: :: SF_MASTR:21

for p, r being preProgram of SCM+FSA st dom p misses dom r holds
UsedILoc (p +* r) = (UsedILoc p) \/ (UsedILoc r)

proof end;

theorem Th22: :: SF_MASTR:22

for p being preProgram of SCM+FSA
for k being Nat holds UsedILoc p = UsedILoc (Shift (p,k))

proof end;

theorem Th23: :: SF_MASTR:23

for i being Instruction of SCM+FSA
for k being 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 Nat holds UsedILoc p = UsedILoc (IncAddr (p,k))

proof end;

theorem Th25: :: SF_MASTR:25

for I being Program of
for k being Nat holds UsedILoc I = UsedILoc (Reloc (I,k))

proof end;

theorem Th26: :: SF_MASTR:26

for I being Program of holds UsedILoc I = UsedILoc (Directed I)

proof end;

theorem Th27: :: SF_MASTR:27

for I, J being Program of holds UsedILoc (I ";" J) = (UsedILoc I) \/ (UsedILoc J)

proof end;

theorem Th28: :: SF_MASTR:28

for i being Instruction of SCM+FSA holds UsedILoc (Macro i) = UsedIntLoc i

proof end;

theorem :: SF_MASTR:29

for i being Instruction of SCM+FSA
for J being Program of holds UsedILoc (i ";" J) = (UsedIntLoc i) \/ (UsedILoc J)

proof end;

theorem :: SF_MASTR:30

for j being Instruction of SCM+FSA
for I being Program of holds UsedILoc (I ";" j) = (UsedILoc I) \/ (UsedIntLoc j)

proof end;

theorem :: SF_MASTR:31

for i, j being Instruction of SCM+FSA holds UsedILoc (i ";" j) = (UsedIntLoc i) \/ (UsedIntLoc j)

proof end;

definition

let i be Instruction of SCM+FSA;

func UsedInt*Loc i -> Element of Fin FinSeq-Locations means :Def4: :: SF_MASTR:def 4
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

proof end;

uniqueness

proof end;

consistency ;

end;

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

theorem Th32: :: SF_MASTR:32

for a, b being Int-Location
for l being 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 a, b 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}

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}

proof end;

definition

let X be set ;

func UsedI*Loc X -> Subset of FinSeq-Locations equals :: SF_MASTR:def 5
union { (UsedInt*Loc i) where i is Instruction of SCM+FSA : i in X } ;

coherence

proof end;

end;

:: deftheorem defines UsedI*Loc SF_MASTR:def 5 :

:: deftheorem defines UsedI*Loc SF_MASTR:def 6 :

registration

let X be finite set ;

cluster UsedI*Loc X -> finite ;

coherence

proof end;

end;

registration

let p be preProgram of SCM+FSA;

cluster UsedI*Loc p -> finite ;

coherence ;

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= UsedI*Loc p by Lm4;

theorem :: SF_MASTR:36

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

proof end;

theorem Th37: :: SF_MASTR:37

for p, r being preProgram of SCM+FSA st dom p misses dom r holds
UsedI*Loc (p +* r) = (UsedI*Loc p) \/ (UsedI*Loc r)

proof end;

theorem Th38: :: SF_MASTR:38

for p being preProgram of SCM+FSA
for k being Nat holds UsedI*Loc p = UsedI*Loc (Shift (p,k))

proof end;

theorem Th39: :: SF_MASTR:39

for i being Instruction of SCM+FSA
for k being 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 Nat holds UsedI*Loc p = UsedI*Loc (IncAddr (p,k))

proof end;

theorem Th41: :: SF_MASTR:41

for I being Program of
for k being Nat holds UsedI*Loc I = UsedI*Loc (Reloc (I,k))

proof end;

theorem Th42: :: SF_MASTR:42

for I being Program of holds UsedI*Loc I = UsedI*Loc (Directed I)

proof end;

theorem Th43: :: SF_MASTR:43

for I, J being Program of holds UsedI*Loc (I ";" J) = (UsedI*Loc I) \/ (UsedI*Loc J)

proof end;

theorem Th44: :: SF_MASTR:44

for i being Instruction of SCM+FSA holds UsedI*Loc (Macro i) = UsedInt*Loc i

proof end;

theorem :: SF_MASTR:45

for i being Instruction of SCM+FSA
for J being Program of holds UsedI*Loc (i ";" J) = (UsedInt*Loc i) \/ (UsedI*Loc J)

proof end;

theorem :: SF_MASTR:46

for j being Instruction of SCM+FSA
for I being Program of holds UsedI*Loc (I ";" j) = (UsedI*Loc I) \/ (UsedInt*Loc j)

proof end;

theorem :: SF_MASTR:47

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

proof end;

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

definition

let p be preProgram of SCM+FSA;

func FirstNotUsed p -> Int-Location means :Def7: :: SF_MASTR:def 7
ex sil being finite Subset of Int-Locations st
( sil = (UsedILoc p) \/ {(intloc 0)} & it = FirstNotIn sil );

existence

proof end;

uniqueness ;

end;

:: deftheorem Def7 defines FirstNotUsed SF_MASTR:def 7 :

registration

let p be preProgram of SCM+FSA;

cluster FirstNotUsed p -> read-write ;

coherence

proof end;

end;

theorem Th50: :: SF_MASTR:50

for p being preProgram of SCM+FSA holds not FirstNotUsed p in UsedILoc p

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

proof end;

theorem :: SF_MASTR:52

for a being Int-Location
for l being 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 a, b 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 )

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

proof end;

:: deftheorem SF_MASTR:def 8 :

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

definition

let p be preProgram of SCM+FSA;

func First*NotUsed p -> FinSeq-Location means :Def8: :: SF_MASTR:def 9
ex sil being finite Subset of FinSeq-Locations st
( sil = UsedI*Loc p & it = First*NotIn sil );

existence

proof end;

uniqueness ;

end;

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

theorem Th57: :: SF_MASTR:57

for p being preProgram of SCM+FSA holds not First*NotUsed p in UsedI*Loc p

proof end;

theorem :: SF_MASTR:58

for a, b 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

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

proof end;

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

proof end;

theorem :: SF_MASTR:61

for a being Int-Location
for I being Program of
for n being Nat
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA st I c= P & ( for m being Nat st m < n holds
IC (Comput (P,s,m)) in dom I ) & not a in UsedILoc 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

proof end;

theorem :: SF_MASTR:63

for f being FinSeq-Location
for I being Program of
for n being Nat
for s being State of SCM+FSA
for P being Instruction-Sequence of SCM+FSA st I c= P & ( for m being Nat st m < n holds
IC (Comput (P,s,m)) in dom I ) & not f in UsedI*Loc I holds
(Comput (P,s,n)) . f = s . f

proof end;

theorem Th64: :: SF_MASTR:64

proof end;

theorem :: SF_MASTR:65

for I being Program of
for n being 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 | (UsedILoc I) = t | (UsedILoc I) & s | (UsedI*Loc I) = t | (UsedI*Loc I) & ( for m being Nat st m < n holds
IC (Comput (P,s,m)) in dom I ) holds
( ( for m being Nat st m < n holds
IC (Comput (Q,t,m)) in dom I ) & ( for m being Nat st m <= n holds
( IC (Comput (P,s,m)) = IC (Comput (Q,t,m)) & ( for a being Int-Location st a in UsedILoc I holds
(Comput (P,s,m)) . a = (Comput (Q,t,m)) . a ) & ( for f being FinSeq-Location st f in UsedI*Loc I holds
(Comput (P,s,m)) . f = (Comput (Q,t,m)) . f ) ) ) )

proof end;

theorem :: SF_MASTR:66

for I being MacroInstruction of SCM+FSA
for k being Nat holds UsedILoc (I ';' (goto k)) = UsedILoc I

proof end;

theorem :: SF_MASTR:67

for I being MacroInstruction of SCM+FSA
for k being Nat holds UsedI*Loc (I ';' (goto k)) = UsedI*Loc I

proof end;