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

theorem :: AMISTD_5:1

for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated AMI-Struct over N
for I being Instruction of S st I is jump-only holds
for k being Nat holds IncAddr (I,k) is jump-only by COMPOS_0:def 9;

registration

let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated halting with_explicit_jumps AMI-Struct over N;
let I be IC-relocable Instruction of S;
let k be Nat;

cluster IncAddr (I,k) -> IC-relocable ;

coherence
IncAddr (I,k) is IC-relocable

proof end;

end;

definition

let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N;
let I be Instruction of S;

attr I is relocable means :Def1: :: AMISTD_5:def 1
for j, k being Nat
for s being State of S holds Exec ((IncAddr (I,(j + k))),(IncIC (s,k))) = IncIC ((Exec ((IncAddr (I,j)),s)),k);

end;

:: deftheorem Def1 defines relocable AMISTD_5:def 1 :
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for I being Instruction of S holds
( I is relocable iff for j, k being Nat
for s being State of S holds Exec ((IncAddr (I,(j + k))),(IncIC (s,k))) = IncIC ((Exec ((IncAddr (I,j)),s)),k) );

registration

let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N;

cluster relocable -> IC-relocable for M3( the InstructionsF 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 with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over 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 with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N holds
( S is relocable iff for I being Instruction of S holds I is relocable );

theorem Th2: :: AMISTD_5:2

for N being with_zero set
for I being Instruction of (STC N)
for s being State of (STC N)
for k being Nat holds Exec (I,(IncIC (s,k))) = IncIC ((Exec (I,s)),k)

proof end;

definition

let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N;

attr S is IC-recognized means :: AMISTD_5:def 3
for q being NAT -defined the InstructionsF of S -valued finite non halt-free Function
for p being b₁ -autonomic FinPartState of S st not p is empty holds
IC in dom p;

end;

:: deftheorem defines IC-recognized AMISTD_5:def 3 :
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N holds
( S is IC-recognized iff for q being NAT -defined the InstructionsF of b₂ -valued finite non halt-free Function
for p being b₃ -autonomic FinPartState of S st not p is empty holds
IC in dom p );

theorem Th3: :: AMISTD_5:3

for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N holds
( S is IC-recognized iff for q being NAT -defined the InstructionsF of b₂ -valued finite non halt-free Function
for p being b₃ -autonomic FinPartState of S st DataPart p <> {} holds
IC in dom p )

proof end;

registration

let N be with_zero set ;

cluster NonZero (STC N) -> empty ;

coherence
Data-Locations is empty

proof end;

end;

registration

let N be with_zero set ;
let p be PartState of (STC N);

cluster DataPart p -> empty ;

coherence
DataPart p is empty ;

end;

registration

let N be with_zero set ;

cluster STC N -> relocable IC-recognized ;

coherence
( STC N is IC-recognized & STC N is relocable )

proof end;

end;

registration

let N be with_zero set ;

cluster non empty with_non-empty_values IC-Ins-separated halting standard relocable IC-recognized for AMI-Struct over N;

existence
ex b₁ being non empty with_non-empty_values IC-Ins-separated halting standard AMI-Struct over N st
( b₁ is relocable & b₁ is IC-recognized )

proof end;

end;

registration

let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated halting relocable AMI-Struct over N;

cluster -> relocable for M3( the InstructionsF of S);

coherence
for b₁ being Instruction of S holds b₁ is relocable by Def2;

end;

theorem Th4: :: AMISTD_5:4

for k being Nat
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting relocable AMI-Struct over N
for INS being Instruction of S
for s being State of S holds Exec ((IncAddr (INS,k)),(IncIC (s,k))) = IncIC ((Exec (INS,s)),k)

proof end;

theorem Th5: :: AMISTD_5:5

for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting relocable AMI-Struct over N
for INS being Instruction of S
for s being State of S
for j, k being Nat st IC s = j + k holds
Exec (INS,(DecIC (s,k))) = DecIC ((Exec ((IncAddr (INS,k)),s)),k)

proof end;

registration

let N be with_zero set ;

cluster non empty with_non-empty_values IC-Ins-separated halting relocable IC-recognized for AMI-Struct over N;

existence
ex b₁ being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N st
( b₁ is relocable & b₁ is IC-recognized )

proof end;

end;

theorem Th6: :: AMISTD_5:6

for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting IC-recognized AMI-Struct over N
for q being NAT -defined the InstructionsF of b₂ -valued finite non halt-free Function
for p being non empty b₃ -autonomic FinPartState of S holds IC in dom p

proof end;

definition

let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N;

attr S is CurIns-recognized means :Def4: :: AMISTD_5:def 4
for q being NAT -defined the InstructionsF of S -valued finite non halt-free Function
for p being non empty b₁ -autonomic FinPartState of S
for s being State of S st p c= s holds
for P being Instruction-Sequence of S st q c= P holds
for i being Nat holds IC (Comput (P,s,i)) in dom q;

end;

:: deftheorem Def4 defines CurIns-recognized AMISTD_5:def 4 :
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N holds
( S is CurIns-recognized iff for q being NAT -defined the InstructionsF of b₂ -valued finite non halt-free Function
for p being non empty b₃ -autonomic FinPartState of S
for s being State of S st p c= s holds
for P being Instruction-Sequence of S st q c= P holds
for i being Nat holds IC (Comput (P,s,i)) in dom q );

registration

let N be with_zero set ;

cluster STC N -> CurIns-recognized ;

coherence
STC N is CurIns-recognized

proof end;

end;

registration

let N be with_zero set ;

cluster non empty with_non-empty_values IC-Ins-separated halting relocable IC-recognized CurIns-recognized for AMI-Struct over N;

existence
ex b₁ being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N st
( b₁ is relocable & b₁ is IC-recognized & b₁ is CurIns-recognized )

proof end;

end;

theorem :: AMISTD_5:7

for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting IC-recognized CurIns-recognized AMI-Struct over N
for q being NAT -defined the InstructionsF of b₂ -valued finite non halt-free Function
for p being non empty b₃ -autonomic FinPartState of S
for s1, s2 being State of S st p c= s1 & p c= s2 holds
for P1, P2 being Instruction-Sequence of S st q c= P1 & q c= P2 holds
for i being 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 with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting relocable IC-recognized CurIns-recognized AMI-Struct over N
for k being Nat
for q being NAT -defined the InstructionsF of b₂ -valued finite non halt-free Function
for p being b₄ -autonomic FinPartState of S st IC in dom p holds
for s being State of S st p c= s holds
for P being Instruction-Sequence of S st q c= P holds
for i being Nat holds Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i) = IncIC ((Comput (P,s,i)),k)

proof end;

theorem Th9: :: AMISTD_5:9

for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting relocable IC-recognized CurIns-recognized AMI-Struct over N
for k being Nat
for q being NAT -defined the InstructionsF of b₂ -valued finite non halt-free Function
for p being b₄ -autonomic FinPartState of S st IC in dom p holds
for s being State of S st IncIC (p,k) c= s holds
for P being Instruction-Sequence of S st Reloc (q,k) c= P holds
for i being Nat holds Comput (P,s,i) = IncIC ((Comput ((P +* q),(s +* p),i)),k)

proof end;

theorem Th10: :: AMISTD_5:10

for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting relocable IC-recognized CurIns-recognized AMI-Struct over N
for k being Nat
for q being NAT -defined the InstructionsF of b₂ -valued finite non halt-free Function
for p being non empty FinPartState of S st IC in dom p holds
for s being State of S st p c= s & IncIC (p,k) is Reloc (q,k) -autonomic holds
for P being Instruction-Sequence of S st q c= P holds
for i being Nat holds Comput (P,s,i) = DecIC ((Comput ((P +* (Reloc (q,k))),(s +* (IncIC (p,k))),i)),k)

proof end;

theorem Th11: :: AMISTD_5:11

for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting relocable IC-recognized CurIns-recognized AMI-Struct over N
for q being NAT -defined the InstructionsF of b₂ -valued finite non halt-free Function
for p being non empty FinPartState of S st IC in dom p holds
for k being Nat holds
( p is q -autonomic iff IncIC (p,k) is Reloc (q,k) -autonomic )

proof end;

definition

let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated halting relocable IC-recognized CurIns-recognized AMI-Struct over N;

attr S is relocable1 means :Def5: :: AMISTD_5:def 5
for k being Nat
for q being NAT -defined the InstructionsF of S -valued finite non halt-free Function
for p being non empty b₂ -autonomic FinPartState of S
for s1, s2 being State of S st p c= s1 & IncIC (p,k) c= s2 holds
for P1, P2 being Instruction-Sequence of S st q c= P1 & Reloc (q,k) c= P2 holds
for i being 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 Nat
for q being NAT -defined the InstructionsF of S -valued finite non halt-free Function
for p being non empty b₂ -autonomic FinPartState of S
for s1, s2 being State of S st p c= s1 & IncIC (p,k) c= s2 holds
for P1, P2 being Instruction-Sequence of S st q c= P1 & Reloc (q,k) c= P2 holds
for i being 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 with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting relocable IC-recognized CurIns-recognized AMI-Struct over N holds
( S is relocable1 iff for k being Nat
for q being NAT -defined the InstructionsF of b₂ -valued finite non halt-free Function
for p being non empty b₄ -autonomic FinPartState of S
for s1, s2 being State of S st p c= s1 & IncIC (p,k) c= s2 holds
for P1, P2 being Instruction-Sequence of S st q c= P1 & Reloc (q,k) c= P2 holds
for i being 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 with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting relocable IC-recognized CurIns-recognized AMI-Struct over N holds
( S is relocable2 iff for k being Nat
for q being NAT -defined the InstructionsF of b₂ -valued finite non halt-free Function
for p being non empty b₄ -autonomic FinPartState of S
for s1, s2 being State of S st p c= s1 & IncIC (p,k) c= s2 holds
for P1, P2 being Instruction-Sequence of S st q c= P1 & Reloc (q,k) c= P2 holds
for i being Nat holds (Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart p)) );

Lm1: for N being with_zero set
for k being Nat
for q being NAT -defined the InstructionsF of (STC b₁) -valued finite non halt-free Function
for p being non empty b₃ -autonomic FinPartState of (STC N)
for s1, s2 being State of (STC N) st p c= s1 & IncIC (p,k) c= s2 holds
for P1, P2 being Instruction-Sequence of (STC N) st q c= P1 & Reloc (q,k) c= P2 holds
for i being 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))) )

proof end;

registration

let N be with_zero set ;

cluster STC N -> relocable1 relocable2 ;

coherence
( STC N is relocable1 & STC N is relocable2 ) by Lm1;

end;

registration

let N be with_zero set ;

cluster non empty with_non-empty_values IC-Ins-separated halting relocable IC-recognized CurIns-recognized relocable1 relocable2 for AMI-Struct over N;

existence
ex b₁ being non empty with_non-empty_values IC-Ins-separated halting relocable IC-recognized CurIns-recognized AMI-Struct over N st
( b₁ is relocable1 & b₁ is relocable2 )

proof end;

end;

theorem Th12: :: AMISTD_5:12

for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting relocable IC-recognized CurIns-recognized relocable1 relocable2 AMI-Struct over N
for q being NAT -defined the InstructionsF of b₂ -valued finite non halt-free Function
for p being non empty b₃ -autonomic FinPartState of S
for k being Nat st IC in dom p holds
( p is q -halted iff IncIC (p,k) is Reloc (q,k) -halted )

proof end;

theorem Th13: :: AMISTD_5:13

for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting relocable IC-recognized CurIns-recognized relocable1 relocable2 AMI-Struct over N
for q being NAT -defined the InstructionsF of b₂ -valued finite non halt-free Function
for p being non empty b₃ -autonomic b₃ -halted FinPartState of S st IC in dom p holds
for k being Nat holds DataPart (Result (q,p)) = DataPart (Result ((Reloc (q,k)),(IncIC (p,k))))

proof end;

registration

let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated halting relocable IC-recognized CurIns-recognized relocable1 relocable2 AMI-Struct over N;
let q be NAT -defined the InstructionsF of S -valued finite non halt-free Function;
let p be non empty q -autonomic q -halted FinPartState of S;
let k be Nat;

cluster IncIC (p,k) -> Reloc (q,k) -halted ;

coherence
IncIC (p,k) is Reloc (q,k) -halted

proof end;

end;

theorem :: AMISTD_5:14

for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting relocable IC-recognized CurIns-recognized relocable1 relocable2 AMI-Struct over N
for F being data-only PartFunc of (FinPartSt S),(FinPartSt S)
for l being Nat
for q being NAT -defined the InstructionsF of b₂ -valued finite non halt-free Function
for p being non empty b₅ -autonomic b₅ -halted FinPartState of S st IC in dom p holds
for k being Nat holds
( q,p computes F iff Reloc (q,k), IncIC (p,k) computes F )

proof end;

theorem :: AMISTD_5:15

for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting IC-recognized CurIns-recognized AMI-Struct over N
for q being NAT -defined the InstructionsF of b₂ -valued finite non halt-free Function
for p being b₃ -autonomic FinPartState of S st IC in dom p holds
IC p in dom q

proof end;

definition

let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N;
let k be Nat;
let F be NAT -defined the InstructionsF of S -valued Function;

attr F is k -halting means :: AMISTD_5:def 7
for s being k -started State of S
for P being Instruction-Sequence of S st F c= P holds
P halts_on s;

end;

:: deftheorem defines -halting AMISTD_5:def 7 :
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N
for k being Nat
for F being NAT -defined the InstructionsF of b₂ -valued Function holds
( F is k -halting iff for s being b₃ -started State of S
for P being Instruction-Sequence of S st F c= P holds
P halts_on s );

registration

let N be with_zero set ;
let S be non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N;

cluster Relation-like NAT -defined the InstructionsF of S -valued Function-like parahalting -> NAT -defined the InstructionsF of S -valued 0 -halting for set ;

coherence
for b₁ being NAT -defined the InstructionsF of S -valued Function st b₁ is parahalting holds
b₁ is 0 -halting ;

cluster Relation-like NAT -defined the InstructionsF of S -valued Function-like 0 -halting -> NAT -defined the InstructionsF of S -valued parahalting for set ;

coherence
for b₁ being NAT -defined the InstructionsF of S -valued Function st b₁ is 0 -halting holds
b₁ is parahalting ;

end;