:: SF_MASTR semantic presentation

theorem Th1: :: SF_MASTR:1

for x, y, a being set
for f being Function st f . x = f . y holds
f . a = (f * ((id (dom f)) +* x,y)) . a

proof end;

theorem Th2: :: SF_MASTR:2

for x, y being set
for f being Function st ( x in dom f implies ( y in dom f & f . x = f . y ) ) holds
f = f * ((id (dom f)) +* x,y)

proof end;

registration

let A be finite set ;
let B be set ;
cluster -> finite M4(A,B);
coherence

proof end;

end;

registration

let A be finite set ;
let B be set ;
let f be Function of A, Fin B;
cluster Union f -> finite ;
coherence

proof end;

end;

registration

cluster Int-Locations -> non empty ;
coherence by SCMFSA_2:9;

end;

registration

cluster FinSeq-Locations -> non empty ;
coherence by SCMFSA_2:10;

end;

theorem :: SF_MASTR:3

canceled;

theorem :: SF_MASTR:4

canceled;

theorem Th5: :: SF_MASTR:5

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

proof end;

theorem Th6: :: SF_MASTR:6

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

proof end;

theorem Th7: :: SF_MASTR:7

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

proof end;

theorem Th8: :: SF_MASTR:8

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

proof end;

theorem Th9: :: SF_MASTR:9

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

proof end;

theorem :: SF_MASTR:10

for l1, l2 being Instruction-Location of SCM+FSA st goto l1 = goto l2 holds
l1 = l2

proof end;

theorem Th11: :: SF_MASTR:11

for a1, a2 being Int-Location
for l1, l2 being Instruction-Location of SCM+FSA st a1 =0_goto l1 = a2 =0_goto l2 holds
( a1 = a2 & l1 = l2 )

proof end;

theorem Th12: :: SF_MASTR:12

for a1, a2 being Int-Location
for l1, l2 being Instruction-Location of SCM+FSA st a1 >0_goto l1 = a2 >0_goto l2 holds
( a1 = a2 & l1 = l2 )

proof end;

theorem Th13: :: SF_MASTR:13

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 )

proof end;

theorem Th14: :: SF_MASTR:14

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 )

proof end;

theorem Th15: :: SF_MASTR:15

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 Th16: :: SF_MASTR:16

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

proof end;

uniqueness

proof end;

consistency by ENUMSET1:def 3;

end;

:: deftheorem Def1 defines UsedIntLoc SF_MASTR:def 1 :

theorem Th17: :: SF_MASTR:17

UsedIntLoc (halt SCM+FSA ) = {}

proof end;

theorem Th18: :: SF_MASTR:18

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 Th19: :: SF_MASTR:19

for l being Instruction-Location of SCM+FSA holds UsedIntLoc (goto l) = {}

proof end;

theorem Th20: :: SF_MASTR:20

for a being Int-Location
for l being Instruction-Location of SCM+FSA
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 Th21: :: SF_MASTR:21

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}

proof end;

theorem Th22: :: SF_MASTR:22

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 p be programmed FinPartState of SCM+FSA ;
func UsedIntLoc p -> Subset of Int-Locations means :Def2: :: SF_MASTR:def 2
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 ) & it = Union (UIL * p) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines UsedIntLoc SF_MASTR:def 2 :

registration

let p be programmed FinPartState of SCM+FSA ;
cluster UsedIntLoc p -> finite ;
coherence

proof end;

end;

theorem Th23: :: SF_MASTR:23

for i being Instruction of SCM+FSA
for p being programmed FinPartState of SCM+FSA st i in rng p holds
UsedIntLoc i c= UsedIntLoc p

proof end;

theorem :: SF_MASTR:24

for p, r being programmed FinPartState of SCM+FSA holds UsedIntLoc (p +* r) c= (UsedIntLoc p) \/ (UsedIntLoc r)

proof end;

theorem Th25: :: SF_MASTR:25

for p, r being programmed FinPartState of SCM+FSA st dom p misses dom r holds
UsedIntLoc (p +* r) = (UsedIntLoc p) \/ (UsedIntLoc r)

proof end;

theorem Th26: :: SF_MASTR:26

for p being programmed FinPartState of SCM+FSA
for k being Nat holds UsedIntLoc p = UsedIntLoc (Shift p,k)

proof end;

theorem Th27: :: SF_MASTR:27

for i being Instruction of SCM+FSA
for k being Nat holds UsedIntLoc i = UsedIntLoc (IncAddr i,k)

proof end;

theorem Th28: :: SF_MASTR:28

for p being programmed FinPartState of SCM+FSA
for k being Nat holds UsedIntLoc p = UsedIntLoc (IncAddr p,k)

proof end;

theorem Th29: :: SF_MASTR:29

for I being Macro-Instruction
for k being Nat holds UsedIntLoc I = UsedIntLoc (ProgramPart (Relocated I,k))

proof end;

theorem Th30: :: SF_MASTR:30

for I being Macro-Instruction holds UsedIntLoc I = UsedIntLoc (Directed I)

proof end;

theorem Th31: :: SF_MASTR:31

for I, J being Macro-Instruction holds UsedIntLoc (I ';' J) = (UsedIntLoc I) \/ (UsedIntLoc J)

proof end;

theorem Th32: :: SF_MASTR:32

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

proof end;

theorem :: SF_MASTR:33

for i being Instruction of SCM+FSA
for J being Macro-Instruction holds UsedIntLoc (i ';' J) = (UsedIntLoc i) \/ (UsedIntLoc J)

proof end;

theorem :: SF_MASTR:34

for j being Instruction of SCM+FSA
for I being Macro-Instruction holds UsedIntLoc (I ';' j) = (UsedIntLoc I) \/ (UsedIntLoc j)

proof end;

theorem :: SF_MASTR:35

for i, j being Instruction of SCM+FSA holds UsedIntLoc (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 :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

proof end;

uniqueness

proof end;

consistency ;

end;

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

theorem Th36: :: SF_MASTR:36

for a, b being Int-Location
for l being Instruction-Location of SCM+FSA
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 Th37: :: SF_MASTR:37

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}

proof end;

theorem Th38: :: SF_MASTR:38

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 p be programmed FinPartState of SCM+FSA ;
func UsedInt*Loc p -> Subset of FinSeq-Locations means :Def4: :: SF_MASTR:def 4
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 ) & it = Union (UIL * p) );
existence

proof end;

uniqueness

proof end;

end;

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

registration

let p be programmed FinPartState of SCM+FSA ;
cluster UsedInt*Loc p -> finite ;
coherence

proof end;

end;

theorem Th39: :: SF_MASTR:39

for i being Instruction of SCM+FSA
for p being programmed FinPartState of SCM+FSA st i in rng p holds
UsedInt*Loc i c= UsedInt*Loc p

proof end;

theorem :: SF_MASTR:40

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

proof end;

theorem Th41: :: SF_MASTR:41

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

proof end;

theorem Th42: :: SF_MASTR:42

for p being programmed FinPartState of SCM+FSA
for k being Nat holds UsedInt*Loc p = UsedInt*Loc (Shift p,k)

proof end;

theorem Th43: :: SF_MASTR:43

for i being Instruction of SCM+FSA
for k being Nat holds UsedInt*Loc i = UsedInt*Loc (IncAddr i,k)

proof end;

theorem Th44: :: SF_MASTR:44

for p being programmed FinPartState of SCM+FSA
for k being Nat holds UsedInt*Loc p = UsedInt*Loc (IncAddr p,k)

proof end;

theorem Th45: :: SF_MASTR:45

for I being Macro-Instruction
for k being Nat holds UsedInt*Loc I = UsedInt*Loc (ProgramPart (Relocated I,k))

proof end;

theorem Th46: :: SF_MASTR:46

for I being Macro-Instruction holds UsedInt*Loc I = UsedInt*Loc (Directed I)

proof end;

theorem Th47: :: SF_MASTR:47

for I, J being Macro-Instruction holds UsedInt*Loc (I ';' J) = (UsedInt*Loc I) \/ (UsedInt*Loc J)

proof end;

theorem Th48: :: SF_MASTR:48

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

proof end;

theorem :: SF_MASTR:49

for i being Instruction of SCM+FSA
for J being Macro-Instruction holds UsedInt*Loc (i ';' J) = (UsedInt*Loc i) \/ (UsedInt*Loc J)

proof end;

theorem :: SF_MASTR:50

for j being Instruction of SCM+FSA
for I being Macro-Instruction holds UsedInt*Loc (I ';' j) = (UsedInt*Loc I) \/ (UsedInt*Loc j)

proof end;

theorem :: SF_MASTR:51

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

proof end;

definition

let IT be Int-Location ;
attr IT is read-only means :Def5: :: SF_MASTR:def 5
IT = intloc 0;

end;

:: deftheorem Def5 defines read-only SF_MASTR:def 5 :

notation

let IT be Int-Location ;
antonym read-write IT for read-only IT;

end;

registration

cluster intloc 0 -> read-only ;
coherence by Def5;

end;

registration

cluster read-write Int-Location ;
existence

proof end;

end;

definition

let L be finite Subset of Int-Locations ;
func FirstNotIn L -> Int-Location means :Def6: :: SF_MASTR:def 6
ex sn being non empty Subset of NAT st
( it = intloc (min sn) & sn = { k where k is Nat : not intloc k in L } );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def6 defines FirstNotIn SF_MASTR:def 6 :

theorem Th52: :: SF_MASTR:52

for L being finite Subset of Int-Locations holds not FirstNotIn L in L

proof end;

theorem :: SF_MASTR:53

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

proof end;

definition

let p be programmed FinPartState of SCM+FSA ;
func FirstNotUsed p -> Int-Location means :Def7: :: SF_MASTR:def 7
ex sil being finite Subset of Int-Locations st
( sil = (UsedIntLoc p) \/ {(intloc 0)} & it = FirstNotIn sil );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def7 defines FirstNotUsed SF_MASTR:def 7 :

registration

let p be programmed FinPartState of SCM+FSA ;
cluster FirstNotUsed p -> read-write ;
coherence

proof end;

end;

theorem Th54: :: SF_MASTR:54

for p being programmed FinPartState of SCM+FSA holds not FirstNotUsed p in UsedIntLoc p

proof end;

theorem :: SF_MASTR:55

for a, b being Int-Location
for p being programmed FinPartState 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:56

for a being Int-Location
for l being Instruction-Location of SCM+FSA
for p being programmed FinPartState 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:57

for b, a being Int-Location
for f being FinSeq-Location
for p being programmed FinPartState 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:58

for a being Int-Location
for f being FinSeq-Location
for p being programmed FinPartState of SCM+FSA st ( a :=len f in rng p or f :=<0,...,0> a in rng p ) holds
FirstNotUsed p <> a

proof end;

definition

let L be finite Subset of FinSeq-Locations ;
func First*NotIn L -> FinSeq-Location means :Def8: :: SF_MASTR:def 8
ex sn being non empty Subset of NAT st
( it = fsloc (min sn) & sn = { k where k is Nat : not fsloc k in L } );
existence

proof end;

uniqueness ;

end;

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

theorem Th59: :: SF_MASTR:59

for L being finite Subset of FinSeq-Locations holds not First*NotIn L in L

proof end;

theorem :: SF_MASTR:60

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

proof end;

definition

let p be programmed FinPartState of SCM+FSA ;
func First*NotUsed p -> FinSeq-Location means :Def9: :: SF_MASTR:def 9
ex sil being finite Subset of FinSeq-Locations st
( sil = UsedInt*Loc p & it = First*NotIn sil );
existence

proof end;

uniqueness ;

end;

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

theorem Th61: :: SF_MASTR:61

for p being programmed FinPartState of SCM+FSA holds not First*NotUsed p in UsedInt*Loc p

proof end;

theorem :: SF_MASTR:62

for b, a being Int-Location
for f being FinSeq-Location
for p being programmed FinPartState 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:63

for a being Int-Location
for f being FinSeq-Location
for p being programmed FinPartState 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 Th64: :: SF_MASTR:64

for I being Macro-Instruction
for n being Nat holds dom I misses dom (Start-At (insloc n))

proof end;

theorem Th65: :: SF_MASTR:65

for I being Macro-Instruction
for n being Nat holds IC SCM+FSA in dom (I +* (Start-At (insloc n)))

proof end;

theorem Th66: :: SF_MASTR:66

for I being Macro-Instruction
for n being Nat holds (I +* (Start-At (insloc n))) . (IC SCM+FSA ) = insloc n

proof end;

theorem Th67: :: SF_MASTR:67

for I being Macro-Instruction
for n being Nat
for s being State of SCM+FSA st I +* (Start-At (insloc n)) c= s holds
IC s = insloc n

proof end;

theorem Th68: :: SF_MASTR:68

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:69

for a being Int-Location
for I being Macro-Instruction
for n being Nat
for s being State of SCM+FSA st I +* (Start-At (insloc 0)) c= s & ( for m being Nat st m < n holds
IC ((Computation s) . m) in dom I ) & not a in UsedIntLoc I holds
((Computation s) . n) . a = s . a

proof end;

theorem Th70: :: SF_MASTR:70

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:71

for f being FinSeq-Location
for I being Macro-Instruction
for n being Nat
for s being State of SCM+FSA st I +* (Start-At (insloc 0)) c= s & ( for m being Nat st m < n holds
IC ((Computation s) . m) in dom I ) & not f in UsedInt*Loc I holds
((Computation s) . n) . f = s . f

proof end;

theorem Th72: :: SF_MASTR:72

proof end;

theorem :: SF_MASTR:73

for I being Macro-Instruction
for n being Nat
for s, t being State of SCM+FSA st I +* (Start-At (insloc 0)) c= s & I +* (Start-At (insloc 0)) c= t & s | (UsedIntLoc I) = t | (UsedIntLoc I) & s | (UsedInt*Loc I) = t | (UsedInt*Loc I) & ( for m being Nat st m < n holds
IC ((Computation s) . m) in dom I ) holds
( ( for m being Nat st m < n holds
IC ((Computation t) . m) in dom I ) & ( for m being Nat st m <= n holds
( IC ((Computation s) . m) = IC ((Computation t) . m) & ( for a being Int-Location st a in UsedIntLoc I holds
((Computation s) . m) . a = ((Computation t) . m) . a ) & ( for f being FinSeq-Location st f in UsedInt*Loc I holds
((Computation s) . m) . f = ((Computation t) . m) . f ) ) ) )

proof end;