:: RELOC semantic presentation

definition

let c₁ be Instruction-Location of SCM ;
let c₂ be Nat;
func c₁ + c₂ -> Instruction-Location of SCM means :Def1: :: RELOC:def 1
ex b₁ being Nat st
( a₁ = il. b₁ & a₃ = il. (b₁ + a₂) );
existence

proof end;

uniqueness by AMI_3:53;
func c₁ -' c₂ -> Instruction-Location of SCM means :Def2: :: RELOC:def 2
ex b₁ being Nat st
( a₁ = il. b₁ & a₃ = il. (b₁ -' a₂) );
existence

proof end;

uniqueness by AMI_3:53;

end;

:: deftheorem Def1 defines + RELOC:def 1 :

:: deftheorem Def2 defines -' RELOC:def 2 :

theorem Th1: :: RELOC:1

for b₁ being Instruction-Location of SCM
for b₂ being Nat holds (b₁ + b₂) -' b₂ = b₁

proof end;

theorem Th2: :: RELOC:2

for b₁, b₂ being Instruction-Location of SCM
for b₃ being Nat holds
( Start-At (b₁ + b₃) = Start-At (b₂ + b₃) iff Start-At b₁ = Start-At b₂ )

proof end;

theorem Th3: :: RELOC:3

for b₁, b₂ being Instruction-Location of SCM
for b₃ being Nat st Start-At b₁ = Start-At b₂ holds
Start-At (b₁ -' b₃) = Start-At (b₂ -' b₃)

proof end;

definition

let c₁ be Instruction of SCM ;
let c₂ be Nat;
func IncAddr c₁,c₂ -> Instruction of SCM equals :Def3: :: RELOC:def 3
goto ((((@ a₁) jump_address ) @ ) + a₂) if InsCode a₁ = 6
(((@ a₁) cond_address ) @ ) =0_goto ((((@ a₁) cjump_address ) @ ) + a₂) if InsCode a₁ = 7
(((@ a₁) cond_address ) @ ) >0_goto ((((@ a₁) cjump_address ) @ ) + a₂) if InsCode a₁ = 8
otherwise a₁;
correctness ;

end;

:: deftheorem Def3 defines IncAddr RELOC:def 3 :

theorem Th4: :: RELOC:4

for b₁ being Nat holds IncAddr (halt SCM ),b₁ = halt SCM by Def3, AMI_5:37;

theorem Th5: :: RELOC:5

for b₁ being Nat
for b₂, b₃ being Data-Location holds IncAddr (b₂ := b₃),b₁ = b₂ := b₃

proof end;

theorem Th6: :: RELOC:6

for b₁ being Nat
for b₂, b₃ being Data-Location holds IncAddr (AddTo b₂,b₃),b₁ = AddTo b₂,b₃

proof end;

theorem Th7: :: RELOC:7

for b₁ being Nat
for b₂, b₃ being Data-Location holds IncAddr (SubFrom b₂,b₃),b₁ = SubFrom b₂,b₃

proof end;

theorem Th8: :: RELOC:8

for b₁ being Nat
for b₂, b₃ being Data-Location holds IncAddr (MultBy b₂,b₃),b₁ = MultBy b₂,b₃

proof end;

theorem Th9: :: RELOC:9

for b₁ being Nat
for b₂, b₃ being Data-Location holds IncAddr (Divide b₂,b₃),b₁ = Divide b₂,b₃

proof end;

theorem Th10: :: RELOC:10

for b₁ being Nat
for b₂ being Instruction-Location of SCM holds IncAddr (goto b₂),b₁ = goto (b₂ + b₁)

proof end;

theorem Th11: :: RELOC:11

for b₁ being Nat
for b₂ being Instruction-Location of SCM
for b₃ being Data-Location holds IncAddr (b₃ =0_goto b₂),b₁ = b₃ =0_goto (b₂ + b₁)

proof end;

theorem Th12: :: RELOC:12

for b₁ being Nat
for b₂ being Instruction-Location of SCM
for b₃ being Data-Location holds IncAddr (b₃ >0_goto b₂),b₁ = b₃ >0_goto (b₂ + b₁)

proof end;

theorem Th13: :: RELOC:13

for b₁ being Instruction of SCM
for b₂ being Nat holds InsCode (IncAddr b₁,b₂) = InsCode b₁

proof end;

theorem Th14: :: RELOC:14

for b₁, b₂ being Instruction of SCM
for b₃ being Nat st ( InsCode b₂ = 0 or InsCode b₂ = 1 or InsCode b₂ = 2 or InsCode b₂ = 3 or InsCode b₂ = 4 or InsCode b₂ = 5 ) & IncAddr b₁,b₃ = b₂ holds
b₁ = b₂

proof end;

definition

let c₁ be programmed FinPartState of SCM ;
let c₂ be Nat;
func Shift c₁,c₂ -> programmed FinPartState of SCM means :Def4: :: RELOC:def 4
( dom a₃ = { (il. (b₁ + a₂)) where B is Nat : il. b₁ in dom a₁ } & ( for b₁ being Nat st il. b₁ in dom a₁ holds
a₃ . (il. (b₁ + a₂)) = a₁ . (il. b₁) ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def4 defines Shift RELOC:def 4 :

theorem Th15: :: RELOC:15

for b₁ being Instruction-Location of SCM
for b₂ being Nat
for b₃ being programmed FinPartState of SCM st b₁ in dom b₃ holds
(Shift b₃,b₂) . (b₁ + b₂) = b₃ . b₁

proof end;

theorem Th16: :: RELOC:16

for b₁ being programmed FinPartState of SCM
for b₂ being Nat holds dom (Shift b₁,b₂) = { (b₃ + b₂) where B is Instruction-Location of SCM : b₃ in dom b₁ }

proof end;

theorem Th17: :: RELOC:17

for b₁ being programmed FinPartState of SCM
for b₂ being Nat holds dom (Shift b₁,b₂) c= the Instruction-Locations of SCM

proof end;

definition

let c₁ be programmed FinPartState of SCM ;
let c₂ be Nat;
func IncAddr c₁,c₂ -> programmed FinPartState of SCM means :Def5: :: RELOC:def 5
( dom a₃ = dom a₁ & ( for b₁ being Nat st il. b₁ in dom a₁ holds
a₃ . (il. b₁) = IncAddr (pi a₁,(il. b₁)),a₂ ) );
existence

proof end;

uniqueness

proof end;

end;

:: deftheorem Def5 defines IncAddr RELOC:def 5 :

theorem Th18: :: RELOC:18

for b₁ being programmed FinPartState of SCM
for b₂ being Nat
for b₃ being Instruction-Location of SCM st b₃ in dom b₁ holds
(IncAddr b₁,b₂) . b₃ = IncAddr (pi b₁,b₃),b₂

proof end;

theorem Th19: :: RELOC:19

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

proof end;

definition

let c₁ be FinPartState of SCM ;
let c₂ be Nat;
func Relocated c₁,c₂ -> FinPartState of SCM equals :: RELOC:def 6
((Start-At ((IC a₁) + a₂)) +* (IncAddr (Shift (ProgramPart a₁),a₂),a₂)) +* (DataPart a₁);
correctness ;

end;

:: deftheorem Def6 defines Relocated RELOC:def 6 :

theorem Th20: :: RELOC:20

for b₁ being Nat
for b₂ being FinPartState of SCM holds dom (IncAddr (Shift (ProgramPart b₂),b₁),b₁) c= SCM-Instr-Loc

proof end;

theorem Th21: :: RELOC:21

for b₁ being FinPartState of SCM
for b₂ being Nat holds DataPart (Relocated b₁,b₂) = DataPart b₁

proof end;

theorem Th22: :: RELOC:22

for b₁ being FinPartState of SCM
for b₂ being Nat holds ProgramPart (Relocated b₁,b₂) = IncAddr (Shift (ProgramPart b₁),b₂),b₂

proof end;

theorem Th23: :: RELOC:23

for b₁ being Nat
for b₂ being FinPartState of SCM holds dom (ProgramPart (Relocated b₂,b₁)) = { (il. (b₃ + b₁)) where B is Nat : il. b₃ in dom (ProgramPart b₂) }

proof end;

theorem Th24: :: RELOC:24

for b₁ being FinPartState of SCM
for b₂ being Nat
for b₃ being Instruction-Location of SCM holds
( b₃ in dom b₁ iff b₃ + b₂ in dom (Relocated b₁,b₂) )

proof end;

theorem Th25: :: RELOC:25

for b₁ being FinPartState of SCM
for b₂ being Nat holds IC SCM in dom (Relocated b₁,b₂)

proof end;

theorem Th26: :: RELOC:26

for b₁ being FinPartState of SCM
for b₂ being Nat holds IC (Relocated b₁,b₂) = (IC b₁) + b₂

proof end;

theorem Th27: :: RELOC:27

for b₁ being FinPartState of SCM
for b₂ being Nat
for b₃ being Instruction-Location of SCM
for b₄ being Instruction of SCM st b₃ in dom (ProgramPart b₁) & b₄ = b₁ . b₃ holds
IncAddr b₄,b₂ = (Relocated b₁,b₂) . (b₃ + b₂)

proof end;

theorem Th28: :: RELOC:28

for b₁ being FinPartState of SCM
for b₂ being Nat holds Start-At ((IC b₁) + b₂) c= Relocated b₁,b₂

proof end;

theorem Th29: :: RELOC:29

for b₁ being data-only FinPartState of SCM
for b₂ being FinPartState of SCM
for b₃ being Nat st IC SCM in dom b₂ holds
Relocated (b₂ +* b₁),b₃ = (Relocated b₂,b₃) +* b₁

proof end;

theorem Th30: :: RELOC:30

for b₁ being Nat
for b₂ being autonomic FinPartState of SCM
for b₃, b₄ being State of SCM st b₂ c= b₃ & Relocated b₂,b₁ c= b₄ holds
b₂ c= b₃ +* (b₄ | SCM-Data-Loc )

proof end;

theorem Th31: :: RELOC:31

for b₁ being Nat
for b₂ being State of SCM holds Exec (IncAddr (CurInstr b₂),b₁),(b₂ +* (Start-At ((IC b₂) + b₁))) = (Following b₂) +* (Start-At ((IC (Following b₂)) + b₁))

proof end;

theorem Th32: :: RELOC:32

for b₁ being Instruction of SCM
for b₂ being State of SCM
for b₃, b₄ being Nat st IC b₂ = il. (b₃ + b₄) holds
Exec b₁,(b₂ +* (Start-At ((IC b₂) -' b₄))) = (Exec (IncAddr b₁,b₄),b₂) +* (Start-At ((IC (Exec (IncAddr b₁,b₄),b₂)) -' b₄))

proof end;

theorem Th33: :: RELOC:33

for b₁ being Nat
for b₂ being autonomic FinPartState of SCM st IC SCM in dom b₂ holds
for b₃ being State of SCM st b₂ c= b₃ holds
for b₄ being Nat holds (Computation (b₃ +* (Relocated b₂,b₁))) . b₄ = (((Computation b₃) . b₄) +* (Start-At ((IC ((Computation b₃) . b₄)) + b₁))) +* (ProgramPart (Relocated b₂,b₁))

proof end;

theorem Th34: :: RELOC:34

for b₁ being Nat
for b₂ being autonomic FinPartState of SCM
for b₃, b₄, b₅ being State of SCM st IC SCM in dom b₂ & b₂ c= b₃ & Relocated b₂,b₁ c= b₄ & b₅ = b₃ +* (b₄ | SCM-Data-Loc ) holds
for b₆ being Nat holds
( (IC ((Computation b₃) . b₆)) + b₁ = IC ((Computation b₄) . b₆) & IncAddr (CurInstr ((Computation b₃) . b₆)),b₁ = CurInstr ((Computation b₄) . b₆) & ((Computation b₃) . b₆) | (dom (DataPart b₂)) = ((Computation b₄) . b₆) | (dom (DataPart (Relocated b₂,b₁))) & ((Computation b₅) . b₆) | SCM-Data-Loc = ((Computation b₄) . b₆) | SCM-Data-Loc )

proof end;

theorem Th35: :: RELOC:35

for b₁ being autonomic FinPartState of SCM
for b₂ being Nat st IC SCM in dom b₁ holds
( b₁ is halting iff Relocated b₁,b₂ is halting )

proof end;

theorem Th36: :: RELOC:36

for b₁ being Nat
for b₂ being autonomic FinPartState of SCM st IC SCM in dom b₂ holds
for b₃ being State of SCM st Relocated b₂,b₁ c= b₃ holds
for b₄ being Nat holds (Computation b₃) . b₄ = ((((Computation (b₃ +* b₂)) . b₄) +* (Start-At ((IC ((Computation (b₃ +* b₂)) . b₄)) + b₁))) +* (b₃ | (dom (ProgramPart b₂)))) +* (ProgramPart (Relocated b₂,b₁))

proof end;

theorem Th37: :: RELOC:37

for b₁ being Nat
for b₂ being FinPartState of SCM st IC SCM in dom b₂ holds
for b₃ being State of SCM st b₂ c= b₃ & Relocated b₂,b₁ is autonomic holds
for b₄ being Nat holds (Computation b₃) . b₄ = ((((Computation (b₃ +* (Relocated b₂,b₁))) . b₄) +* (Start-At ((IC ((Computation (b₃ +* (Relocated b₂,b₁))) . b₄)) -' b₁))) +* (b₃ | (dom (ProgramPart (Relocated b₂,b₁))))) +* (ProgramPart b₂)

proof end;

theorem Th38: :: RELOC:38

for b₁ being FinPartState of SCM st IC SCM in dom b₁ holds
for b₂ being Nat holds
( b₁ is autonomic iff Relocated b₁,b₂ is autonomic )

proof end;

theorem Th39: :: RELOC:39

for b₁ being autonomic halting FinPartState of SCM st IC SCM in dom b₁ holds
for b₂ being Nat holds DataPart (Result b₁) = DataPart (Result (Relocated b₁,b₂))

proof end;

theorem Th40: :: RELOC:40

for b₁ being PartFunc of FinPartSt SCM , FinPartSt SCM
for b₂ being FinPartState of SCM st IC SCM in dom b₂ & b₁ is data-only holds
for b₃ being Nat holds
( b₂ computes b₁ iff Relocated b₂,b₃ computes b₁ )

proof end;