:: SCMFSA_5 semantic presentation

definition

let p be FinPartState of SCM+FSA ;
let k be Nat;
func Relocated p,k -> FinPartState of SCM+FSA equals :: SCMFSA_5:def 1
((Start-At ((IC p) + k)) +* (IncAddr (Shift (ProgramPart p),k),k)) +* (DataPart p);
correctness ;

end;

:: deftheorem defines Relocated SCMFSA_5:def 1 :

Lm1: the Instruction-Locations of SCM+FSA misses Int-Locations \/ FinSeq-Locations
by SCMFSA_2:13, SCMFSA_2:14, XBOOLE_1:70;

theorem Th1: :: SCMFSA_5:1

for p being FinPartState of SCM+FSA
for k being Nat holds DataPart (Relocated p,k) = DataPart p

proof end;

theorem Th2: :: SCMFSA_5:2

for p being FinPartState of SCM+FSA
for k being Nat holds ProgramPart (Relocated p,k) = IncAddr (Shift (ProgramPart p),k),k

proof end;

theorem Th3: :: SCMFSA_5:3

for k being Nat
for p being FinPartState of SCM+FSA holds dom (ProgramPart (Relocated p,k)) = { (insloc (j + k)) where j is Nat : insloc j in dom (ProgramPart p) }

proof end;

theorem Th4: :: SCMFSA_5:4

for p being FinPartState of SCM+FSA
for k being Nat
for l being Instruction-Location of SCM+FSA holds
( l in dom p iff l + k in dom (Relocated p,k) )

proof end;

theorem Th5: :: SCMFSA_5:5

for p being FinPartState of SCM+FSA
for k being Nat holds IC SCM+FSA in dom (Relocated p,k)

proof end;

theorem Th6: :: SCMFSA_5:6

for p being FinPartState of SCM+FSA
for k being Nat holds IC (Relocated p,k) = (IC p) + k

proof end;

theorem Th7: :: SCMFSA_5:7

for p being FinPartState of SCM+FSA
for k being Nat
for loc being Instruction-Location of SCM+FSA
for I being Instruction of SCM+FSA st loc in dom (ProgramPart p) & I = p . loc holds
IncAddr I,k = (Relocated p,k) . (loc + k)

proof end;

theorem Th8: :: SCMFSA_5:8

for p being FinPartState of SCM+FSA
for k being Nat holds Start-At ((IC p) + k) c= Relocated p,k

proof end;

theorem Th9: :: SCMFSA_5:9

for s being data-only FinPartState of SCM+FSA
for p being FinPartState of SCM+FSA
for k being Nat st IC SCM+FSA in dom p holds
Relocated (p +* s),k = (Relocated p,k) +* s

proof end;

theorem Th10: :: SCMFSA_5:10

for k being Nat
for p being autonomic FinPartState of SCM+FSA
for s1, s2 being State of SCM+FSA st p c= s1 & Relocated p,k c= s2 holds
p c= s1 +* (s2 | (Int-Locations \/ FinSeq-Locations ))

proof end;

theorem :: SCMFSA_5:11

for k being Nat
for p being autonomic FinPartState of SCM+FSA st IC SCM+FSA in dom p holds
for s being State of SCM+FSA st p c= s holds
for i being Nat holds (Computation (s +* (Relocated p,k))) . i = (((Computation s) . i) +* (Start-At ((IC ((Computation s) . i)) + k))) +* (ProgramPart (Relocated p,k))

proof end;

Lm2: for s being State of SCM+FSA holds dom (s | (Int-Locations \/ FinSeq-Locations )) = Int-Locations \/ FinSeq-Locations

proof end;

theorem Th12: :: SCMFSA_5:12

for k being Nat
for p being autonomic FinPartState of SCM+FSA
for s1, s2, s3 being State of SCM+FSA st IC SCM+FSA in dom p & p c= s1 & Relocated p,k c= s2 & s3 = s1 +* (s2 | (Int-Locations \/ FinSeq-Locations )) holds
for i being Nat holds
( (IC ((Computation s1) . i)) + k = IC ((Computation s2) . i) & IncAddr (CurInstr ((Computation s1) . i)),k = CurInstr ((Computation s2) . i) & ((Computation s1) . i) | (dom (DataPart p)) = ((Computation s2) . i) | (dom (DataPart (Relocated p,k))) & ((Computation s3) . i) | (Int-Locations \/ FinSeq-Locations ) = ((Computation s2) . i) | (Int-Locations \/ FinSeq-Locations ) )

proof end;

theorem Th13: :: SCMFSA_5:13

for p being autonomic FinPartState of SCM+FSA
for k being Nat st IC SCM+FSA in dom p holds
( p is halting iff Relocated p,k is halting )

proof end;

theorem Th14: :: SCMFSA_5:14

for k being Nat
for p being autonomic FinPartState of SCM+FSA st IC SCM+FSA in dom p holds
for s being State of SCM+FSA st Relocated p,k c= s holds
for i being Nat holds (Computation s) . i = ((((Computation (s +* p)) . i) +* (Start-At ((IC ((Computation (s +* p)) . i)) + k))) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated p,k))

proof end;

theorem Th15: :: SCMFSA_5:15

for k being Nat
for p being FinPartState of SCM+FSA st IC SCM+FSA in dom p holds
for s being State of SCM+FSA st p c= s & Relocated p,k is autonomic holds
for i being Nat holds (Computation s) . i = ((((Computation (s +* (Relocated p,k))) . i) +* (Start-At ((IC ((Computation (s +* (Relocated p,k))) . i)) -' k))) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p)

proof end;

theorem Th16: :: SCMFSA_5:16

for p being FinPartState of SCM+FSA st IC SCM+FSA in dom p holds
for k being Nat holds
( p is autonomic iff Relocated p,k is autonomic )

proof end;

theorem Th17: :: SCMFSA_5:17

for p being autonomic halting FinPartState of SCM+FSA st IC SCM+FSA in dom p holds
for k being Nat holds DataPart (Result p) = DataPart (Result (Relocated p,k))

proof end;

theorem :: SCMFSA_5:18

for F being PartFunc of FinPartSt SCM+FSA , FinPartSt SCM+FSA
for p being FinPartState of SCM+FSA st IC SCM+FSA in dom p & F is data-only holds
for k being Nat holds
( p computes F iff Relocated p,k computes F )

proof end;