:: Relocable Instructions
:: by Andrzej Trybulec
::
:: Received November 20, 2010
:: Copyright (c) 2010-2011 Association of Mizar Users

begin

theorem :: AMISTD_5:1

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite standard-ins homogeneous regular J/A-independent AMI-Struct of N
for I being Instruction of S st I is jump-only holds
for k being Element of NAT holds IncAddr (I,k) is jump-only

proof end;

registration

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent halting with_explicit_jumps AMI-Struct of N;
let I be IC-relocable Instruction of S;
let k be Element of NAT ;
cluster IncAddr (I,k) -> IC-relocable ;
coherence
IncAddr (I,k) is IC-relocable

proof end;

end;

definition

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent halting AMI-Struct of N;
let I be Instruction of S;
attr I is relocable means :Def1: :: AMISTD_5:def 1
for j, k being natural number
for s being State of S holds NPP (Exec ((IncAddr (I,(j + k))),(IncIC (s,k)))) = NPP (IncIC ((Exec ((IncAddr (I,j)),s)),k));

end;

:: deftheorem Def1 defines relocable AMISTD_5:def 1 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent halting AMI-Struct of N
for I being Instruction of S holds
( I is relocable iff for j, k being natural number
for s being State of S holds NPP (Exec ((IncAddr (I,(j + k))),(IncIC (s,k)))) = NPP (IncIC ((Exec ((IncAddr (I,j)),s)),k)) );

registration

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent halting AMI-Struct of N;
cluster relocable -> IC-relocable Element of the Instructions of S;
coherence
for b₁ being Instruction of S st b₁ is relocable holds
b₁ is IC-relocable

proof end;

end;

definition

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent halting AMI-Struct of N;
attr S is relocable means :Def2: :: AMISTD_5:def 2
for I being Instruction of S holds I is relocable ;

end;

:: deftheorem Def2 defines relocable AMISTD_5:def 2 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent halting AMI-Struct of N holds
( S is relocable iff for I being Instruction of S holds I is relocable );

theorem Th2: :: AMISTD_5:2

for N being non empty with_non-empty_elements set
for I being Instruction of (STC N)
for s being State of (STC N)
for k being natural number holds Exec (I,(IncIC (s,k))) = IncIC ((Exec (I,s)),k)

proof end;

definition

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite realistic halting AMI-Struct of N;
attr S is IC-recognized means :Def3: :: AMISTD_5:def 3
for p being autonomic FinPartState of S st not NPP p is empty holds
IC in dom p;

end;

:: deftheorem Def3 defines IC-recognized AMISTD_5:def 3 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic halting AMI-Struct of N holds
( S is IC-recognized iff for p being autonomic FinPartState of S st not NPP p is empty holds
IC in dom p );

theorem Th3: :: AMISTD_5:3

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic halting AMI-Struct of N holds
( S is IC-recognized iff for p being autonomic FinPartState of S st DataPart p <> {} holds
IC in dom p )

proof end;

registration

let N be non empty with_non-empty_elements set ;
cluster Data-Locations (STC N) -> empty ;
coherence
Data-Locations (STC N) is empty

proof end;

end;

registration

let N be non empty with_non-empty_elements set ;
let p be PartState of (STC N);
cluster DataPart p -> empty ;
coherence
DataPart p is empty ;

end;

registration

let N be non empty with_non-empty_elements set ;
cluster STC N -> relocable IC-recognized ;
coherence
( STC N is IC-recognized & STC N is relocable )

proof end;

end;

registration

let N be non empty with_non-empty_elements set ;
cluster STC N -> proper-halt ;
coherence
STC N is proper-halt

proof end;

end;

registration

let N be non empty with_non-empty_elements set ;
cluster non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent proper-halt halting standard relocable IC-recognized AMI-Struct of N;
existence
ex b₁ being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent halting standard AMI-Struct of N st
( b₁ is relocable & b₁ is IC-recognized & b₁ is proper-halt )

proof end;

end;

registration

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent halting relocable AMI-Struct of N;
cluster -> relocable Element of the Instructions of S;
coherence
for b₁ being Instruction of S holds b₁ is relocable by Def2;

end;

theorem Th4: :: AMISTD_5:4

for k being natural number
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent halting relocable AMI-Struct of N
for INS being Instruction of S
for s being State of S holds NPP (Exec ((IncAddr (INS,k)),(IncIC (s,k)))) = NPP (IncIC ((Exec (INS,s)),k))

proof end;

theorem Th5: :: AMISTD_5:5

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent halting relocable AMI-Struct of N
for INS being Instruction of S
for s being State of S
for j, k being Element of NAT st IC s = j + k holds
NPP (Exec (INS,(DecIC (s,k)))) = NPP (DecIC ((Exec ((IncAddr (INS,k)),s)),k))

proof end;

registration

let N be non empty with_non-empty_elements set ;
cluster non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent proper-halt halting Exec-preserving relocable IC-recognized AMI-Struct of N;
existence
ex b₁ being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent halting Exec-preserving AMI-Struct of N st
( b₁ is relocable & b₁ is IC-recognized & b₁ is proper-halt )

proof end;

end;

theorem Th6: :: AMISTD_5:6

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins halting IC-recognized AMI-Struct of N
for p being non NAT -defined autonomic FinPartState of holds IC in dom p

proof end;

definition

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite realistic halting AMI-Struct of N;
attr S is CurIns-recognized means :Def4: :: AMISTD_5:def 4
for p being non NAT -defined autonomic FinPartState of
for s being State of S st NPP p c= s holds
for P being the Instructions of S -valued ManySortedSet of NAT st ProgramPart p c= P holds
for i being Element of NAT holds IC (Comput (P,s,i)) in dom (ProgramPart p);

end;

:: deftheorem Def4 defines CurIns-recognized AMISTD_5:def 4 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic halting AMI-Struct of N holds
( S is CurIns-recognized iff for p being non NAT -defined autonomic FinPartState of
for s being State of S st NPP p c= s holds
for P being the Instructions of b₂ -valued ManySortedSet of NAT st ProgramPart p c= P holds
for i being Element of NAT holds IC (Comput (P,s,i)) in dom (ProgramPart p) );

registration

let N be non empty with_non-empty_elements set ;
cluster STC N -> CurIns-recognized ;
coherence
STC N is CurIns-recognized

proof end;

end;

theorem :: AMISTD_5:7

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins halting IC-recognized AMI-Struct of N st S is CurIns-recognized holds
for p being non NAT -defined autonomic FinPartState of
for s1, s2 being State of S st NPP p c= s1 & NPP p c= s2 holds
for P1, P2 being the Instructions of b₂ -valued ManySortedSet of NAT st ProgramPart p c= P1 & ProgramPart p c= P2 holds
for i being Element of NAT holds
( IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) & CurInstr (P1,(Comput (P1,s1,i))) = CurInstr (P2,(Comput (P2,s2,i))) )

proof end;

theorem :: AMISTD_5:8

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent halting Exec-preserving relocable IC-recognized AMI-Struct of N st S is CurIns-recognized holds
for k being Element of NAT
for p being autonomic FinPartState of S st IC in dom p holds
for s being State of S st NPP p c= s holds
for P being the Instructions of b₂ -valued ManySortedSet of NAT st ProgramPart p c= P holds
for i being Element of NAT holds NPP (Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (NPP (Relocated (p,k)))),i)) = NPP (IncIC ((Comput (P,s,i)),k))

proof end;

theorem Th9: :: AMISTD_5:9

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent halting Exec-preserving relocable IC-recognized AMI-Struct of N st S is CurIns-recognized holds
for k being Element of NAT
for p being autonomic FinPartState of S st IC in dom p holds
for s being State of S st NPP (Relocated (p,k)) c= s holds
for P being the Instructions of b₂ -valued ManySortedSet of NAT st Reloc ((ProgramPart p),k) c= P holds
for i being Element of NAT holds NPP (Comput (P,s,i)) = NPP (IncIC ((Comput ((P +* (ProgramPart p)),(s +* (NPP p)),i)),k))

proof end;

theorem Th10: :: AMISTD_5:10

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent halting Exec-preserving relocable IC-recognized AMI-Struct of N st S is CurIns-recognized holds
for k being Element of NAT
for p being FinPartState of S st IC in dom p holds
for s being State of S st NPP p c= s & Relocated (p,k) is autonomic holds
for P being the Instructions of b₂ -valued ManySortedSet of NAT st ProgramPart p c= P holds
for i being Element of NAT holds NPP (Comput (P,s,i)) = NPP (DecIC ((Comput ((P +* (Reloc ((ProgramPart p),k))),(s +* (NPP (Relocated (p,k)))),i)),k))

proof end;

theorem Th11: :: AMISTD_5:11

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent halting Exec-preserving relocable IC-recognized AMI-Struct of N st S is CurIns-recognized holds
for p being FinPartState of S st IC in dom p holds
for k being Element of NAT holds
( p is autonomic iff Relocated (p,k) is autonomic )

proof end;

definition

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent halting Exec-preserving relocable IC-recognized AMI-Struct of N;
attr S is relocable1 means :Def5: :: AMISTD_5:def 5
for k being Element of NAT
for p being autonomic FinPartState of S
for s1, s2 being State of S st IC in dom p & NPP p c= s1 & NPP (Relocated (p,k)) c= s2 holds
for P1, P2 being the Instructions of S -valued ManySortedSet of NAT st ProgramPart p c= P1 & Reloc ((ProgramPart p),k) c= P2 holds
for i being Element of NAT holds IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = CurInstr (P2,(Comput (P2,s2,i)));
attr S is relocable2 means :Def6: :: AMISTD_5:def 6
for k being Element of NAT
for p being autonomic FinPartState of S
for s1, s2 being State of S st IC in dom p & NPP p c= s1 & NPP (Relocated (p,k)) c= s2 holds
for P1, P2 being the Instructions of S -valued ManySortedSet of NAT st ProgramPart p c= P1 & Reloc ((ProgramPart p),k) c= P2 holds
for i being Element of NAT holds (Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart p));

end;

:: deftheorem Def5 defines relocable1 AMISTD_5:def 5 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent halting Exec-preserving relocable IC-recognized AMI-Struct of N holds
( S is relocable1 iff for k being Element of NAT
for p being autonomic FinPartState of S
for s1, s2 being State of S st IC in dom p & NPP p c= s1 & NPP (Relocated (p,k)) c= s2 holds
for P1, P2 being the Instructions of b₂ -valued ManySortedSet of NAT st ProgramPart p c= P1 & Reloc ((ProgramPart p),k) c= P2 holds
for i being Element of NAT holds IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = CurInstr (P2,(Comput (P2,s2,i))) );

:: deftheorem Def6 defines relocable2 AMISTD_5:def 6 :
for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent halting Exec-preserving relocable IC-recognized AMI-Struct of N holds
( S is relocable2 iff for k being Element of NAT
for p being autonomic FinPartState of S
for s1, s2 being State of S st IC in dom p & NPP p c= s1 & NPP (Relocated (p,k)) c= s2 holds
for P1, P2 being the Instructions of b₂ -valued ManySortedSet of NAT st ProgramPart p c= P1 & Reloc ((ProgramPart p),k) c= P2 holds
for i being Element of NAT holds (Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart p)) );

Lm1: for N being non empty with_non-empty_elements set
for k being Element of NAT
for p being autonomic FinPartState of (STC N)
for s1, s2 being State of (STC N) st IC in dom p & NPP p c= s1 & NPP (Relocated (p,k)) c= s2 holds
for P1, P2 being the Instructions of (STC b₁) -valued ManySortedSet of NAT st ProgramPart p c= P1 & Reloc ((ProgramPart p),k) c= P2 holds
for i being Element of NAT holds
( (IC (Comput (P1,s1,i))) + k = IC (Comput (P2,s2,i)) & IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = CurInstr (P2,(Comput (P2,s2,i))) & (Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart (Relocated (p,k)))) & DataPart (Comput (P1,(s1 +* (DataPart s2)),i)) = DataPart (Comput (P2,s2,i)) )

proof end;

registration

let N be non empty with_non-empty_elements set ;
cluster STC N -> relocable1 ;
coherence
STC N is relocable1

proof end;

end;

registration

let N be non empty with_non-empty_elements set ;
cluster non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent proper-halt halting Exec-preserving relocable IC-recognized relocable1 AMI-Struct of N;
existence
ex b₁ being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent proper-halt halting Exec-preserving relocable IC-recognized AMI-Struct of N st b₁ is relocable1

proof end;

end;

theorem Th12: :: AMISTD_5:12

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent proper-halt halting Exec-preserving relocable IC-recognized relocable1 AMI-Struct of N st S is relocable1 & S is proper-halt holds
for p being autonomic FinPartState of S
for k being Element of NAT st IC in dom p holds
( p is halting iff Relocated (p,k) is halting )

proof end;

theorem Th13: :: AMISTD_5:13

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent proper-halt halting Exec-preserving relocable IC-recognized relocable1 AMI-Struct of N st S is relocable1 & S is relocable2 & S is CurIns-recognized holds
for p being non program-free autonomic halting FinPartState of S st IC in dom p holds
for k being Element of NAT holds DataPart (Result ((ProgramPart p),p)) = DataPart (Result ((Reloc ((ProgramPart p),k)),(Relocated (p,k))))

proof end;

registration

let N be non empty with_non-empty_elements set ;
let S be non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent proper-halt halting Exec-preserving relocable IC-recognized relocable1 AMI-Struct of N;
let l be Element of NAT ;
let p be l -started autonomic halting FinPartState of S;
let k be Element of NAT ;
cluster Relocated (p,k) -> halting ;
coherence
Relocated (p,k) is halting

proof end;

end;

theorem :: AMISTD_5:14

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins homogeneous regular J/A-independent proper-halt halting Exec-preserving relocable IC-recognized relocable1 AMI-Struct of N st S is CurIns-recognized & S is relocable2 holds
for F being PartFunc of (FinPartSt S),(FinPartSt S)
for l being Element of NAT
for p being b₄ -started non program-free autonomic halting FinPartState of S st IC in dom p & F is data-only holds
for k being Element of NAT holds
( ProgramPart p,p computes F iff Reloc ((ProgramPart p),k), Relocated (p,k) computes F )

proof end;

theorem :: AMISTD_5:15

for N being non empty with_non-empty_elements set
for S being non empty stored-program IC-Ins-separated definite realistic standard-ins halting IC-recognized AMI-Struct of N st S is CurIns-recognized holds
for p being autonomic FinPartState of S st IC in dom p holds
IC p in dom p

proof end;