:: SF_MASTR semantic presentation

theorem Th1: :: SF_MASTR:1

for b₁, b₂, b₃ being set
for b₄ being Function st b₄ . b₁ = b₄ . b₂ holds
b₄ . b₃ = (b₄ * ((id (dom b₄)) +* b₁,b₂)) . b₃

proof end;

theorem Th2: :: SF_MASTR:2

for b₁, b₂ being set
for b₃ being Function st ( b₁ in dom b₃ implies ( b₂ in dom b₃ & b₃ . b₁ = b₃ . b₂ ) ) holds
b₃ = b₃ * ((id (dom b₃)) +* b₁,b₂)

proof end;

registration

let c₁ be finite set ;
let c₂ be set ;
cluster -> finite M4(a₁,a₂);
coherence

proof end;

end;

registration

let c₁ be finite set ;
let c₂ be set ;
let c₃ be Function of c₁, Fin c₂;
cluster Union a₃ -> 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 Th3: :: SF_MASTR:3

canceled;

theorem Th4: :: SF_MASTR:4

canceled;

theorem Th5: :: SF_MASTR:5

for b₁, b₂, b₃, b₄ being Int-Location st b₁ := b₂ = b₃ := b₄ holds
( b₁ = b₃ & b₂ = b₄ )

proof end;

theorem Th6: :: SF_MASTR:6

for b₁, b₂, b₃, b₄ being Int-Location st AddTo b₁,b₂ = AddTo b₃,b₄ holds
( b₁ = b₃ & b₂ = b₄ )

proof end;

theorem Th7: :: SF_MASTR:7

for b₁, b₂, b₃, b₄ being Int-Location st SubFrom b₁,b₂ = SubFrom b₃,b₄ holds
( b₁ = b₃ & b₂ = b₄ )

proof end;

theorem Th8: :: SF_MASTR:8

for b₁, b₂, b₃, b₄ being Int-Location st MultBy b₁,b₂ = MultBy b₃,b₄ holds
( b₁ = b₃ & b₂ = b₄ )

proof end;

theorem Th9: :: SF_MASTR:9

for b₁, b₂, b₃, b₄ being Int-Location st Divide b₁,b₂ = Divide b₃,b₄ holds
( b₁ = b₃ & b₂ = b₄ )

proof end;

theorem Th10: :: SF_MASTR:10

for b₁, b₂ being Instruction-Location of SCM+FSA st goto b₁ = goto b₂ holds
b₁ = b₂

proof end;

theorem Th11: :: SF_MASTR:11

for b₁, b₂ being Int-Location
for b₃, b₄ being Instruction-Location of SCM+FSA st b₁ =0_goto b₃ = b₂ =0_goto b₄ holds
( b₁ = b₂ & b₃ = b₄ )

proof end;

theorem Th12: :: SF_MASTR:12

for b₁, b₂ being Int-Location
for b₃, b₄ being Instruction-Location of SCM+FSA st b₁ >0_goto b₃ = b₂ >0_goto b₄ holds
( b₁ = b₂ & b₃ = b₄ )

proof end;

theorem Th13: :: SF_MASTR:13

for b₁, b₂, b₃, b₄ being Int-Location
for b₅, b₆ being FinSeq-Location st b₁ := b₅,b₂ = b₃ := b₆,b₄ holds
( b₂ = b₄ & b₁ = b₃ & b₅ = b₆ )

proof end;

theorem Th14: :: SF_MASTR:14

for b₁, b₂, b₃, b₄ being Int-Location
for b₅, b₆ being FinSeq-Location st b₅,b₁ := b₂ = b₆,b₃ := b₄ holds
( b₁ = b₃ & b₂ = b₄ & b₅ = b₆ )

proof end;

theorem Th15: :: SF_MASTR:15

for b₁, b₂ being Int-Location
for b₃, b₄ being FinSeq-Location st b₁ :=len b₃ = b₂ :=len b₄ holds
( b₁ = b₂ & b₃ = b₄ )

proof end;

theorem Th16: :: SF_MASTR:16

for b₁, b₂ being Int-Location
for b₃, b₄ being FinSeq-Location st b₃ :=<0,...,0> b₁ = b₄ :=<0,...,0> b₂ holds
( b₁ = b₂ & b₃ = b₄ )

proof end;

definition

let c₁ be Instruction of SCM+FSA ;
func UsedIntLoc c₁ -> Element of Fin Int-Locations means :Def1: :: SF_MASTR:def 1
ex b₁, b₂ being Int-Location st
( ( a₁ = b₁ := b₂ or a₁ = AddTo b₁,b₂ or a₁ = SubFrom b₁,b₂ or a₁ = MultBy b₁,b₂ or a₁ = Divide b₁,b₂ ) & a₂ = {b₁,b₂} ) if InsCode a₁ in {1,2,3,4,5}
ex b₁ being Int-Location ex b₂ being Instruction-Location of SCM+FSA st
( ( a₁ = b₁ =0_goto b₂ or a₁ = b₁ >0_goto b₂ ) & a₂ = {b₁} ) if ( InsCode a₁ = 7 or InsCode a₁ = 8 )
ex b₁, b₂ being Int-Location ex b₃ being FinSeq-Location st
( ( a₁ = b₂ := b₃,b₁ or a₁ = b₃,b₁ := b₂ ) & a₂ = {b₁,b₂} ) if ( InsCode a₁ = 9 or InsCode a₁ = 10 )
ex b₁ being Int-Location ex b₂ being FinSeq-Location st
( ( a₁ = b₁ :=len b₂ or a₁ = b₂ :=<0,...,0> b₁ ) & a₂ = {b₁} ) if ( InsCode a₁ = 11 or InsCode a₁ = 12 )
otherwise a₂ = {} ;
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 b₁, b₂ being Int-Location
for b₃ being Instruction of SCM+FSA st ( b₃ = b₁ := b₂ or b₃ = AddTo b₁,b₂ or b₃ = SubFrom b₁,b₂ or b₃ = MultBy b₁,b₂ or b₃ = Divide b₁,b₂ ) holds
UsedIntLoc b₃ = {b₁,b₂}

proof end;

theorem Th19: :: SF_MASTR:19

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

proof end;

theorem Th20: :: SF_MASTR:20

for b₁ being Int-Location
for b₂ being Instruction-Location of SCM+FSA
for b₃ being Instruction of SCM+FSA st ( b₃ = b₁ =0_goto b₂ or b₃ = b₁ >0_goto b₂ ) holds
UsedIntLoc b₃ = {b₁}

proof end;

theorem Th21: :: SF_MASTR:21

for b₁, b₂ being Int-Location
for b₃ being FinSeq-Location
for b₄ being Instruction of SCM+FSA st ( b₄ = b₁ := b₃,b₂ or b₄ = b₃,b₂ := b₁ ) holds
UsedIntLoc b₄ = {b₂,b₁}

proof end;

theorem Th22: :: SF_MASTR:22

for b₁ being Int-Location
for b₂ being FinSeq-Location
for b₃ being Instruction of SCM+FSA st ( b₃ = b₁ :=len b₂ or b₃ = b₂ :=<0,...,0> b₁ ) holds
UsedIntLoc b₃ = {b₁}

proof end;

definition

let c₁ be programmed FinPartState of SCM+FSA ;
func UsedIntLoc c₁ -> Subset of Int-Locations means :Def2: :: SF_MASTR:def 2
ex b₁ being Function of the Instructions of SCM+FSA , Fin Int-Locations st
( ( for b₂ being Instruction of SCM+FSA holds b₁ . b₂ = UsedIntLoc b₂ ) & a₂ = Union (b₁ * a₁) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def2 defines UsedIntLoc SF_MASTR:def 2 :

registration

let c₁ be programmed FinPartState of SCM+FSA ;
cluster UsedIntLoc a₁ -> finite ;
coherence

proof end;

end;

theorem Th23: :: SF_MASTR:23

for b₁ being Instruction of SCM+FSA
for b₂ being programmed FinPartState of SCM+FSA st b₁ in rng b₂ holds
UsedIntLoc b₁ c= UsedIntLoc b₂

proof end;

theorem Th24: :: SF_MASTR:24

for b₁, b₂ being programmed FinPartState of SCM+FSA holds UsedIntLoc (b₁ +* b₂) c= (UsedIntLoc b₁) \/ (UsedIntLoc b₂)

proof end;

theorem Th25: :: SF_MASTR:25

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

proof end;

theorem Th26: :: SF_MASTR:26

for b₁ being programmed FinPartState of SCM+FSA
for b₂ being Nat holds UsedIntLoc b₁ = UsedIntLoc (Shift b₁,b₂)

proof end;

theorem Th27: :: SF_MASTR:27

for b₁ being Instruction of SCM+FSA
for b₂ being Nat holds UsedIntLoc b₁ = UsedIntLoc (IncAddr b₁,b₂)

proof end;

theorem Th28: :: SF_MASTR:28

for b₁ being programmed FinPartState of SCM+FSA
for b₂ being Nat holds UsedIntLoc b₁ = UsedIntLoc (IncAddr b₁,b₂)

proof end;

theorem Th29: :: SF_MASTR:29

for b₁ being Macro-Instruction
for b₂ being Nat holds UsedIntLoc b₁ = UsedIntLoc (ProgramPart (Relocated b₁,b₂))

proof end;

theorem Th30: :: SF_MASTR:30

for b₁ being Macro-Instruction holds UsedIntLoc b₁ = UsedIntLoc (Directed b₁)

proof end;

theorem Th31: :: SF_MASTR:31

for b₁, b₂ being Macro-Instruction holds UsedIntLoc (b₁ ';' b₂) = (UsedIntLoc b₁) \/ (UsedIntLoc b₂)

proof end;

theorem Th32: :: SF_MASTR:32

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

proof end;

theorem Th33: :: SF_MASTR:33

for b₁ being Instruction of SCM+FSA
for b₂ being Macro-Instruction holds UsedIntLoc (b₁ ';' b₂) = (UsedIntLoc b₁) \/ (UsedIntLoc b₂)

proof end;

theorem Th34: :: SF_MASTR:34

for b₁ being Instruction of SCM+FSA
for b₂ being Macro-Instruction holds UsedIntLoc (b₂ ';' b₁) = (UsedIntLoc b₂) \/ (UsedIntLoc b₁)

proof end;

theorem Th35: :: SF_MASTR:35

for b₁, b₂ being Instruction of SCM+FSA holds UsedIntLoc (b₁ ';' b₂) = (UsedIntLoc b₁) \/ (UsedIntLoc b₂)

proof end;

definition

let c₁ be Instruction of SCM+FSA ;
func UsedInt*Loc c₁ -> Element of Fin FinSeq-Locations means :Def3: :: SF_MASTR:def 3
ex b₁, b₂ being Int-Location ex b₃ being FinSeq-Location st
( ( a₁ = b₂ := b₃,b₁ or a₁ = b₃,b₁ := b₂ ) & a₂ = {b₃} ) if ( InsCode a₁ = 9 or InsCode a₁ = 10 )
ex b₁ being Int-Location ex b₂ being FinSeq-Location st
( ( a₁ = b₁ :=len b₂ or a₁ = b₂ :=<0,...,0> b₁ ) & a₂ = {b₂} ) if ( InsCode a₁ = 11 or InsCode a₁ = 12 )
otherwise a₂ = {} ;
existence

proof end;

uniqueness

proof end;

consistency ;

end;

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

theorem Th36: :: SF_MASTR:36

for b₁, b₂ being Int-Location
for b₃ being Instruction-Location of SCM+FSA
for b₄ being Instruction of SCM+FSA st ( b₄ = halt SCM+FSA or b₄ = b₁ := b₂ or b₄ = AddTo b₁,b₂ or b₄ = SubFrom b₁,b₂ or b₄ = MultBy b₁,b₂ or b₄ = Divide b₁,b₂ or b₄ = goto b₃ or b₄ = b₁ =0_goto b₃ or b₄ = b₁ >0_goto b₃ ) holds
UsedInt*Loc b₄ = {}

proof end;

theorem Th37: :: SF_MASTR:37

for b₁, b₂ being Int-Location
for b₃ being FinSeq-Location
for b₄ being Instruction of SCM+FSA st ( b₄ = b₁ := b₃,b₂ or b₄ = b₃,b₂ := b₁ ) holds
UsedInt*Loc b₄ = {b₃}

proof end;

theorem Th38: :: SF_MASTR:38

for b₁ being Int-Location
for b₂ being FinSeq-Location
for b₃ being Instruction of SCM+FSA st ( b₃ = b₁ :=len b₂ or b₃ = b₂ :=<0,...,0> b₁ ) holds
UsedInt*Loc b₃ = {b₂}

proof end;

definition

let c₁ be programmed FinPartState of SCM+FSA ;
func UsedInt*Loc c₁ -> Subset of FinSeq-Locations means :Def4: :: SF_MASTR:def 4
ex b₁ being Function of the Instructions of SCM+FSA , Fin FinSeq-Locations st
( ( for b₂ being Instruction of SCM+FSA holds b₁ . b₂ = UsedInt*Loc b₂ ) & a₂ = Union (b₁ * a₁) );
existence

proof end;

uniqueness

proof end;

end;

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

registration

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

proof end;

end;

theorem Th39: :: SF_MASTR:39

for b₁ being Instruction of SCM+FSA
for b₂ being programmed FinPartState of SCM+FSA st b₁ in rng b₂ holds
UsedInt*Loc b₁ c= UsedInt*Loc b₂

proof end;

theorem Th40: :: SF_MASTR:40

for b₁, b₂ being programmed FinPartState of SCM+FSA holds UsedInt*Loc (b₁ +* b₂) c= (UsedInt*Loc b₁) \/ (UsedInt*Loc b₂)

proof end;

theorem Th41: :: SF_MASTR:41

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

proof end;

theorem Th42: :: SF_MASTR:42

for b₁ being programmed FinPartState of SCM+FSA
for b₂ being Nat holds UsedInt*Loc b₁ = UsedInt*Loc (Shift b₁,b₂)

proof end;

theorem Th43: :: SF_MASTR:43

for b₁ being Instruction of SCM+FSA
for b₂ being Nat holds UsedInt*Loc b₁ = UsedInt*Loc (IncAddr b₁,b₂)

proof end;

theorem Th44: :: SF_MASTR:44

for b₁ being programmed FinPartState of SCM+FSA
for b₂ being Nat holds UsedInt*Loc b₁ = UsedInt*Loc (IncAddr b₁,b₂)

proof end;

theorem Th45: :: SF_MASTR:45

for b₁ being Macro-Instruction
for b₂ being Nat holds UsedInt*Loc b₁ = UsedInt*Loc (ProgramPart (Relocated b₁,b₂))

proof end;

theorem Th46: :: SF_MASTR:46

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

proof end;

theorem Th47: :: SF_MASTR:47

for b₁, b₂ being Macro-Instruction holds UsedInt*Loc (b₁ ';' b₂) = (UsedInt*Loc b₁) \/ (UsedInt*Loc b₂)

proof end;

theorem Th48: :: SF_MASTR:48

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

proof end;

theorem Th49: :: SF_MASTR:49

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

proof end;

theorem Th50: :: SF_MASTR:50

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

proof end;

theorem Th51: :: SF_MASTR:51

for b₁, b₂ being Instruction of SCM+FSA holds UsedInt*Loc (b₁ ';' b₂) = (UsedInt*Loc b₁) \/ (UsedInt*Loc b₂)

proof end;

definition

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

end;

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

notation

let c₁ be Int-Location ;
antonym read-write c₁ for read-only c₁;

end;

registration

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

end;

registration

cluster read-write Int-Location ;
existence

proof end;

end;

definition

let c₁ be finite Subset of Int-Locations ;
func FirstNotIn c₁ -> Int-Location means :Def6: :: SF_MASTR:def 6
ex b₁ being non empty Subset of NAT st
( a₂ = intloc (min b₁) & b₁ = { b₂ where B is Nat : not intloc b₂ in a₁ } );
existence

proof end;

uniqueness ;

end;

:: deftheorem Def6 defines FirstNotIn SF_MASTR:def 6 :

theorem Th52: :: SF_MASTR:52

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

proof end;

theorem Th53: :: SF_MASTR:53

for b₁, b₂ being Nat
for b₃ being finite Subset of Int-Locations st FirstNotIn b₃ = intloc b₁ & not intloc b₂ in b₃ holds
b₁ <= b₂

proof end;

definition

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

proof end;

uniqueness ;

end;

:: deftheorem Def7 defines FirstNotUsed SF_MASTR:def 7 :

registration

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

proof end;

end;

theorem Th54: :: SF_MASTR:54

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

proof end;

theorem Th55: :: SF_MASTR:55

for b₁, b₂ being Int-Location
for b₃ being programmed FinPartState of SCM+FSA st ( b₁ := b₂ in rng b₃ or AddTo b₁,b₂ in rng b₃ or SubFrom b₁,b₂ in rng b₃ or MultBy b₁,b₂ in rng b₃ or Divide b₁,b₂ in rng b₃ ) holds
( FirstNotUsed b₃ <> b₁ & FirstNotUsed b₃ <> b₂ )

proof end;

theorem Th56: :: SF_MASTR:56

for b₁ being Int-Location
for b₂ being Instruction-Location of SCM+FSA
for b₃ being programmed FinPartState of SCM+FSA st ( b₁ =0_goto b₂ in rng b₃ or b₁ >0_goto b₂ in rng b₃ ) holds
FirstNotUsed b₃ <> b₁

proof end;

theorem Th57: :: SF_MASTR:57

for b₁, b₂ being Int-Location
for b₃ being FinSeq-Location
for b₄ being programmed FinPartState of SCM+FSA st ( b₁ := b₃,b₂ in rng b₄ or b₃,b₂ := b₁ in rng b₄ ) holds
( FirstNotUsed b₄ <> b₂ & FirstNotUsed b₄ <> b₁ )

proof end;

theorem Th58: :: SF_MASTR:58

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

proof end;

definition

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

proof end;

uniqueness ;

end;

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

theorem Th59: :: SF_MASTR:59

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

proof end;

theorem Th60: :: SF_MASTR:60

for b₁, b₂ being Nat
for b₃ being finite Subset of FinSeq-Locations st First*NotIn b₃ = fsloc b₁ & not fsloc b₂ in b₃ holds
b₁ <= b₂

proof end;

definition

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

proof end;

uniqueness ;

end;

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

theorem Th61: :: SF_MASTR:61

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

proof end;

theorem Th62: :: SF_MASTR:62

for b₁, b₂ being Int-Location
for b₃ being FinSeq-Location
for b₄ being programmed FinPartState of SCM+FSA st ( b₁ := b₃,b₂ in rng b₄ or b₃,b₂ := b₁ in rng b₄ ) holds
First*NotUsed b₄ <> b₃

proof end;

theorem Th63: :: SF_MASTR:63

for b₁ being Int-Location
for b₂ being FinSeq-Location
for b₃ being programmed FinPartState of SCM+FSA st ( b₁ :=len b₂ in rng b₃ or b₂ :=<0,...,0> b₁ in rng b₃ ) holds
First*NotUsed b₃ <> b₂

proof end;

theorem Th64: :: SF_MASTR:64

for b₁ being Macro-Instruction
for b₂ being Nat holds dom b₁ misses dom (Start-At (insloc b₂))

proof end;

theorem Th65: :: SF_MASTR:65

for b₁ being Macro-Instruction
for b₂ being Nat holds IC SCM+FSA in dom (b₁ +* (Start-At (insloc b₂)))

proof end;

theorem Th66: :: SF_MASTR:66

for b₁ being Macro-Instruction
for b₂ being Nat holds (b₁ +* (Start-At (insloc b₂))) . (IC SCM+FSA ) = insloc b₂

proof end;

theorem Th67: :: SF_MASTR:67

for b₁ being Macro-Instruction
for b₂ being Nat
for b₃ being State of SCM+FSA st b₁ +* (Start-At (insloc b₂)) c= b₃ holds
IC b₃ = insloc b₂

proof end;

theorem Th68: :: SF_MASTR:68

for b₁ being Int-Location
for b₂ being Instruction of SCM+FSA
for b₃ being State of SCM+FSA st not b₁ in UsedIntLoc b₂ holds
(Exec b₂,b₃) . b₁ = b₃ . b₁

proof end;

theorem Th69: :: SF_MASTR:69

for b₁ being Int-Location
for b₂ being Macro-Instruction
for b₃ being Nat
for b₄ being State of SCM+FSA st b₂ +* (Start-At (insloc 0)) c= b₄ & ( for b₅ being Nat st b₅ < b₃ holds
IC ((Computation b₄) . b₅) in dom b₂ ) & not b₁ in UsedIntLoc b₂ holds
((Computation b₄) . b₃) . b₁ = b₄ . b₁

proof end;

theorem Th70: :: SF_MASTR:70

for b₁ being FinSeq-Location
for b₂ being Instruction of SCM+FSA
for b₃ being State of SCM+FSA st not b₁ in UsedInt*Loc b₂ holds
(Exec b₂,b₃) . b₁ = b₃ . b₁

proof end;

theorem Th71: :: SF_MASTR:71

for b₁ being FinSeq-Location
for b₂ being Macro-Instruction
for b₃ being Nat
for b₄ being State of SCM+FSA st b₂ +* (Start-At (insloc 0)) c= b₄ & ( for b₅ being Nat st b₅ < b₃ holds
IC ((Computation b₄) . b₅) in dom b₂ ) & not b₁ in UsedInt*Loc b₂ holds
((Computation b₄) . b₃) . b₁ = b₄ . b₁

proof end;

theorem Th72: :: SF_MASTR:72

proof end;

theorem Th73: :: SF_MASTR:73

for b₁ being Macro-Instruction
for b₂ being Nat
for b₃, b₄ being State of SCM+FSA st b₁ +* (Start-At (insloc 0)) c= b₃ & b₁ +* (Start-At (insloc 0)) c= b₄ & b₃ | (UsedIntLoc b₁) = b₄ | (UsedIntLoc b₁) & b₃ | (UsedInt*Loc b₁) = b₄ | (UsedInt*Loc b₁) & ( for b₅ being Nat st b₅ < b₂ holds
IC ((Computation b₃) . b₅) in dom b₁ ) holds
( ( for b₅ being Nat st b₅ < b₂ holds
IC ((Computation b₄) . b₅) in dom b₁ ) & ( for b₅ being Nat st b₅ <= b₂ holds
( IC ((Computation b₃) . b₅) = IC ((Computation b₄) . b₅) & ( for b₆ being Int-Location st b₆ in UsedIntLoc b₁ holds
((Computation b₃) . b₅) . b₆ = ((Computation b₄) . b₅) . b₆ ) & ( for b₆ being FinSeq-Location st b₆ in UsedInt*Loc b₁ holds
((Computation b₃) . b₅) . b₆ = ((Computation b₄) . b₅) . b₆ ) ) ) )

proof end;