:: Relocable Instructions
:: by Andrzej Trybulec
::
:: 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
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 b1 being Instruction of S st b1 is relocable holds
b1 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 b1 -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 b2 -valued finite non halt-free Function
for p being b3 -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 b2 -valued finite non halt-free Function
for p being b3 -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
proof end;
end;

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

registration
let N be with_zero set ;
coherence
( STC N is IC-recognized & STC N is relocable )
proof end;
end;

registration
let N be with_zero set ;
existence
ex b1 being non empty with_non-empty_values IC-Ins-separated halting standard AMI-Struct over N st
( b1 is relocable & b1 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 b1 being Instruction of S holds b1 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 ;
existence
ex b1 being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N st
( b1 is relocable & b1 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 b2 -valued finite non halt-free Function
for p being non empty b3 -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 b1 -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 b2 -valued finite non halt-free Function
for p being non empty b3 -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 ;
coherence
proof end;
end;

registration
let N be with_zero set ;
existence
ex b1 being non empty with_non-empty_values IC-Ins-separated halting AMI-Struct over N st
( b1 is relocable & b1 is IC-recognized & b1 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 b2 -valued finite non halt-free Function
for p being non empty b3 -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 b2 -valued finite non halt-free Function
for p being b4 -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 b2 -valued finite non halt-free Function
for p being b4 -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 b2 -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 b2 -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 b2 -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 b2 -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 ()) = (Comput (P2,s2,i)) | (dom ());
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 b2 -valued finite non halt-free Function
for p being non empty b4 -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 b2 -valued finite non halt-free Function
for p being non empty b4 -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 ()) = (Comput (P2,s2,i)) | (dom ()) );

Lm1: for N being with_zero set
for k being Nat
for q being NAT -defined the InstructionsF of (STC b1) -valued finite non halt-free Function
for p being non empty b3 -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 ;
coherence
( STC N is relocable1 & STC N is relocable2 )
by Lm1;
end;

registration
let N be with_zero set ;
existence
ex b1 being non empty with_non-empty_values IC-Ins-separated halting relocable IC-recognized CurIns-recognized AMI-Struct over N st
( b1 is relocable1 & b1 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 b2 -valued finite non halt-free Function
for p being non empty b3 -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 b2 -valued finite non halt-free Function
for p being non empty b3 -autonomic b3 -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 (),()
for l being Nat
for q being NAT -defined the InstructionsF of b2 -valued finite non halt-free Function
for p being non empty b5 -autonomic b5 -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 b2 -valued finite non halt-free Function
for p being b3 -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 b2 -valued Function holds
( F is k -halting iff for s being b3 -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;
coherence
for b1 being NAT -defined the InstructionsF of S -valued Function st b1 is parahalting holds
b1 is 0 -halting
;
coherence
for b1 being NAT -defined the InstructionsF of S -valued Function st b1 is 0 -halting holds
b1 is parahalting
;
end;