:: SCMFSA_5 semantic presentation

definition
let c1 be FinPartState of SCM+FSA ;
let c2 be Nat;
func Relocated c1,c2 -> FinPartState of SCM+FSA equals :: SCMFSA_5:def 1
((Start-At ((IC a1) + a2)) +* (IncAddr (Shift (ProgramPart a1),a2),a2)) +* (DataPart a1);
correctness
coherence
((Start-At ((IC c1) + c2)) +* (IncAddr (Shift (ProgramPart c1),c2),c2)) +* (DataPart c1) is FinPartState of SCM+FSA ;
;
end;

:: deftheorem Def1 defines Relocated SCMFSA_5:def 1 :
for b1 being FinPartState of SCM+FSA
for b2 being Nat holds Relocated b1,b2 = ((Start-At ((IC b1) + b2)) +* (IncAddr (Shift (ProgramPart b1),b2),b2)) +* (DataPart b1);

Lemma1: 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 b1 being FinPartState of SCM+FSA
for b2 being Nat holds DataPart (Relocated b1,b2) = DataPart b1
proof end;

theorem Th2: :: SCMFSA_5:2
for b1 being FinPartState of SCM+FSA
for b2 being Nat holds ProgramPart (Relocated b1,b2) = IncAddr (Shift (ProgramPart b1),b2),b2
proof end;

theorem Th3: :: SCMFSA_5:3
for b1 being Nat
for b2 being FinPartState of SCM+FSA holds dom (ProgramPart (Relocated b2,b1)) = { (insloc (b3 + b1)) where B is Nat : insloc b3 in dom (ProgramPart b2) }
proof end;

theorem Th4: :: SCMFSA_5:4
for b1 being FinPartState of SCM+FSA
for b2 being Nat
for b3 being Instruction-Location of SCM+FSA holds
( b3 in dom b1 iff b3 + b2 in dom (Relocated b1,b2) )
proof end;

theorem Th5: :: SCMFSA_5:5
for b1 being FinPartState of SCM+FSA
for b2 being Nat holds IC SCM+FSA in dom (Relocated b1,b2)
proof end;

theorem Th6: :: SCMFSA_5:6
for b1 being FinPartState of SCM+FSA
for b2 being Nat holds IC (Relocated b1,b2) = (IC b1) + b2
proof end;

theorem Th7: :: SCMFSA_5:7
for b1 being FinPartState of SCM+FSA
for b2 being Nat
for b3 being Instruction-Location of SCM+FSA
for b4 being Instruction of SCM+FSA st b3 in dom (ProgramPart b1) & b4 = b1 . b3 holds
IncAddr b4,b2 = (Relocated b1,b2) . (b3 + b2)
proof end;

theorem Th8: :: SCMFSA_5:8
for b1 being FinPartState of SCM+FSA
for b2 being Nat holds Start-At ((IC b1) + b2) c= Relocated b1,b2
proof end;

theorem Th9: :: SCMFSA_5:9
for b1 being data-only FinPartState of SCM+FSA
for b2 being FinPartState of SCM+FSA
for b3 being Nat st IC SCM+FSA in dom b2 holds
Relocated (b2 +* b1),b3 = (Relocated b2,b3) +* b1
proof end;

theorem Th10: :: SCMFSA_5:10
for b1 being Nat
for b2 being autonomic FinPartState of SCM+FSA
for b3, b4 being State of SCM+FSA st b2 c= b3 & Relocated b2,b1 c= b4 holds
b2 c= b3 +* (b4 | (Int-Locations \/ FinSeq-Locations ))
proof end;

theorem Th11: :: SCMFSA_5:11
for b1 being Nat
for b2 being autonomic FinPartState of SCM+FSA st IC SCM+FSA in dom b2 holds
for b3 being State of SCM+FSA st b2 c= b3 holds
for b4 being Nat holds (Computation (b3 +* (Relocated b2,b1))) . b4 = (((Computation b3) . b4) +* (Start-At ((IC ((Computation b3) . b4)) + b1))) +* (ProgramPart (Relocated b2,b1))
proof end;

Lemma12: for b1 being State of SCM+FSA holds dom (b1 | (Int-Locations \/ FinSeq-Locations )) = Int-Locations \/ FinSeq-Locations
proof end;

theorem Th12: :: SCMFSA_5:12
for b1 being Nat
for b2 being autonomic FinPartState of SCM+FSA
for b3, b4, b5 being State of SCM+FSA st IC SCM+FSA in dom b2 & b2 c= b3 & Relocated b2,b1 c= b4 & b5 = b3 +* (b4 | (Int-Locations \/ FinSeq-Locations )) holds
for b6 being Nat holds
( (IC ((Computation b3) . b6)) + b1 = IC ((Computation b4) . b6) & IncAddr (CurInstr ((Computation b3) . b6)),b1 = CurInstr ((Computation b4) . b6) & ((Computation b3) . b6) | (dom (DataPart b2)) = ((Computation b4) . b6) | (dom (DataPart (Relocated b2,b1))) & ((Computation b5) . b6) | (Int-Locations \/ FinSeq-Locations ) = ((Computation b4) . b6) | (Int-Locations \/ FinSeq-Locations ) )
proof end;

theorem Th13: :: SCMFSA_5:13
for b1 being autonomic FinPartState of SCM+FSA
for b2 being Nat st IC SCM+FSA in dom b1 holds
( b1 is halting iff Relocated b1,b2 is halting )
proof end;

theorem Th14: :: SCMFSA_5:14
for b1 being Nat
for b2 being autonomic FinPartState of SCM+FSA st IC SCM+FSA in dom b2 holds
for b3 being State of SCM+FSA st Relocated b2,b1 c= b3 holds
for b4 being Nat holds (Computation b3) . b4 = ((((Computation (b3 +* b2)) . b4) +* (Start-At ((IC ((Computation (b3 +* b2)) . b4)) + b1))) +* (b3 | (dom (ProgramPart b2)))) +* (ProgramPart (Relocated b2,b1))
proof end;

theorem Th15: :: SCMFSA_5:15
for b1 being Nat
for b2 being FinPartState of SCM+FSA st IC SCM+FSA in dom b2 holds
for b3 being State of SCM+FSA st b2 c= b3 & Relocated b2,b1 is autonomic holds
for b4 being Nat holds (Computation b3) . b4 = ((((Computation (b3 +* (Relocated b2,b1))) . b4) +* (Start-At ((IC ((Computation (b3 +* (Relocated b2,b1))) . b4)) -' b1))) +* (b3 | (dom (ProgramPart (Relocated b2,b1))))) +* (ProgramPart b2)
proof end;

theorem Th16: :: SCMFSA_5:16
for b1 being FinPartState of SCM+FSA st IC SCM+FSA in dom b1 holds
for b2 being Nat holds
( b1 is autonomic iff Relocated b1,b2 is autonomic )
proof end;

theorem Th17: :: SCMFSA_5:17
for b1 being autonomic halting FinPartState of SCM+FSA st IC SCM+FSA in dom b1 holds
for b2 being Nat holds DataPart (Result b1) = DataPart (Result (Relocated b1,b2))
proof end;

theorem Th18: :: SCMFSA_5:18
for b1 being PartFunc of FinPartSt SCM+FSA , FinPartSt SCM+FSA
for b2 being FinPartState of SCM+FSA st IC SCM+FSA in dom b2 & b1 is data-only holds
for b3 being Nat holds
( b2 computes b1 iff Relocated b2,b3 computes b1 )
proof end;