:: Relocable Instructions
:: by Andrzej Trybulec
::
:: Received November 20, 2010
:: Copyright (c) 2010-2019 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, ARYTM_1, ARYTM_3, CARD_1, AMI_1, XBOOLE_0, RELAT_1,
TARSKI, FUNCOP_1, GLIB_000, GOBOARD5, AMISTD_1, FUNCT_1, STRUCT_0,
VALUED_1, FSM_1, FUNCT_4, TURING_1, CIRCUIT2, AMISTD_2, PARTFUN1,
EXTPRO_1, NAT_1, RELOC, AMISTD_5, COMPOS_1, MSUALG_1, FINSET_1, QUANTAL1,
MEMSTR_0, SCMFSA6B;
notations TARSKI, XBOOLE_0, XTUPLE_0, SUBSET_1, ORDINAL1, SETFAM_1, MEMBERED,
RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCT_4, PBOOLE, FINSET_1, CARD_1,
NUMBERS, XCMPLX_0, XXREAL_0, NAT_1, CARD_3, FINSEQ_1, FUNCOP_1, NAT_D,
FUNCT_7, VALUED_0, VALUED_1, AFINSQ_1, MEASURE6, STRUCT_0, MEMSTR_0,
COMPOS_0, COMPOS_1, EXTPRO_1, AMISTD_1, AMISTD_2;
constructors WELLORD2, REALSET1, NAT_D, AMISTD_1, XXREAL_2, PRE_POLY,
AFINSQ_1, ORDINAL4, VALUED_1, AMISTD_2, PBOOLE, RELSET_1, FUNCT_7,
FUNCT_4, MEMSTR_0, MEASURE6, XTUPLE_0;
registrations XBOOLE_0, RELAT_1, FUNCT_1, FUNCOP_1, FINSET_1, XREAL_0, NAT_1,
AMISTD_1, FUNCT_4, RELSET_1, GRFUNC_1, ORDINAL1, VALUED_1, COMPOS_1,
EXTPRO_1, AMISTD_2, MEMSTR_0, MEASURE6, COMPOS_0, XTUPLE_0;
requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
definitions EXTPRO_1, AMISTD_1, AMISTD_2;
equalities COMPOS_1, EXTPRO_1, FUNCOP_1, NAT_1, STRUCT_0, MEMSTR_0, COMPOS_0;
expansions EXTPRO_1, AMISTD_1;
theorems AMISTD_1, FUNCOP_1, FUNCT_1, FUNCT_4, GRFUNC_1, RELAT_1, TARSKI,
ZFMISC_1, XBOOLE_0, XBOOLE_1, PBOOLE, PARTFUN1, VALUED_1, COMPOS_1,
EXTPRO_1, NAT_D, AMISTD_2, MEMSTR_0, COMPOS_0;
schemes NAT_1;
begin :: Relocable instructions
theorem
for N be with_zero set
for S be IC-Ins-separated non empty with_non-empty_values AMI-Struct over N
for I be Instruction of S st I is jump-only
for k be Nat holds IncAddr(I,k) is jump-only
by COMPOS_0:def 9;
registration
let N be with_zero set,
S be with_explicit_jumps IC-Ins-separated halting
non empty with_non-empty_values AMI-Struct over N,
I be IC-relocable Instruction of S, k be Nat;
cluster IncAddr(I,k) -> IC-relocable;
coherence
proof
let j,i being Nat, s being State of S;
thus IC Exec(IncAddr(IncAddr(I,k),j),s) + i
= IC Exec(IncAddr(I,k+j),s) + i by COMPOS_0:7
.= IC Exec(IncAddr(I,k+j+i),IncIC(s,i)) by AMISTD_2:def 3
.= IC Exec(IncAddr(I,k+(j+i)),IncIC(s,i))
.= IC Exec(IncAddr(IncAddr(I,k),j+i),IncIC(s,i)) by COMPOS_0:7;
end;
end;
definition
let N be with_zero set,
S be halting
IC-Ins-separated non empty with_non-empty_values AMI-Struct over N,
I be Instruction of S;
attr I is relocable means
:Def1: for j,k being Nat, s being State of S holds
Exec(IncAddr(I,j+k),IncIC(s,k)) = IncIC(Exec(IncAddr(I,j),s),k);
end;
registration
let N be with_zero set,
S be halting IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N;
cluster relocable -> IC-relocable for Instruction of S;
coherence
proof let I be Instruction of S such that
A1: I is relocable;
let j,k be Nat, s be State of S;
reconsider kk=k as Nat;
thus IC Exec(IncAddr(I,j),s) + k
= IC IncIC(Exec(IncAddr(I,j),s),kk) by MEMSTR_0:53
.= IC Exec(IncAddr(I,j+k),IncIC(s,k)) by A1;
end;
end;
definition
let N be with_zero set,
S be halting
IC-Ins-separated non empty with_non-empty_values AMI-Struct over N;
attr S is relocable means
:Def2: for I being Instruction of S holds I is relocable;
end;
theorem Th2:
for N being with_zero set,
I being Instruction of STC N, s be State of STC N,
k being Nat
holds Exec(I,IncIC(s,k)) = IncIC(Exec(I,s),k)
proof
let N being with_zero set,
I being Instruction of STC N, s be State of STC N,
k being Nat;
per cases by AMISTD_1:6;
suppose
A1: InsCode I = 1;
hence Exec(I,IncIC(s,k)) = IncIC(IncIC(s,k),1) by AMISTD_1:20
.= IncIC(s,1+k) by MEMSTR_0:57
.= IncIC(IncIC(s,1),k) by MEMSTR_0:57
.= IncIC(Exec(I,s),k) by A1,AMISTD_1:20;
end;
suppose InsCode I = 0;
then
A2: I is halting by AMISTD_1:4;
hence Exec(I,IncIC(s,k)) = IncIC(s,k)
.= IncIC(Exec(I,s),k) by A2;
end;
end;
definition
let N be with_zero set;
let S be halting IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N;
attr S is IC-recognized means
for q be non halt-free finite
(the InstructionsF of S)-valued NAT-defined Function
for p being q-autonomic
FinPartState of S st p is non empty
holds IC S in dom p;
end;
theorem Th3:
for N being with_zero set
for S being halting IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N
holds S is IC-recognized iff
for q be non halt-free finite
(the InstructionsF of S)-valued NAT-defined Function
for p being q-autonomic
FinPartState of S st DataPart p <> {}
holds IC S in dom p
proof
let N be with_zero set;
let S be halting IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N;
thus S is IC-recognized implies
for q be non halt-free finite
(the InstructionsF of S)-valued NAT-defined Function
for p being q-autonomic FinPartState of S st DataPart p <> {}
holds IC S in dom p
proof assume
A1: S is IC-recognized;
let q be non halt-free finite
(the InstructionsF of S)-valued NAT-defined Function;
let p be q-autonomic FinPartState of S;
assume DataPart p <> {};
then p is non empty;
hence thesis by A1;
end;
assume
A2: for q be non halt-free finite
(the InstructionsF of S)-valued NAT-defined Function
for p being q-autonomic FinPartState of S st DataPart p <> {}
holds IC S in dom p;
let q be non halt-free finite
(the InstructionsF of S)-valued NAT-defined Function;
let p be q-autonomic FinPartState of S;
A3: dom p c= {IC S} \/ dom DataPart p by MEMSTR_0:32;
assume
A4: p is non empty;
per cases;
suppose
A5: IC S in dom p;
thus IC S in dom p by A5;
end;
suppose not IC S in dom p;
then {IC S} misses dom p by ZFMISC_1:50;
then dom DataPart p is non empty by A4,A3,XBOOLE_1:3,73;
then DataPart p is non empty;
hence IC S in dom p by A2;
end;
end;
registration
let N be with_zero set;
cluster Data-Locations STC N -> empty;
coherence
proof
the carrier of STC N = {0} by AMISTD_1:def 7
.= {IC STC N} by AMISTD_1:def 7;
hence thesis by XBOOLE_1:37;
end;
end;
registration
let N be with_zero set;
let p be PartState of STC N;
cluster DataPart p -> empty;
coherence;
end;
registration
let N be with_zero set;
cluster STC N -> IC-recognized relocable;
coherence
proof
for q be non halt-free finite
(the InstructionsF of STC N)-valued NAT-defined Function
for p being q-autonomic
FinPartState of STC N st DataPart p <> {}
holds IC STC N in dom p;
hence STC N is IC-recognized by Th3;
let I be Instruction of STC N;
let j,k be Nat, s be State of STC N;
thus Exec(IncAddr(I,j+k),IncIC(s,k))
= Exec(I,IncIC(s,k)) by COMPOS_0:4
.= IncIC(Exec(I,s),k) by Th2
.= IncIC(Exec(IncAddr(I,j),s),k) by COMPOS_0:4;
end;
end;
registration
let N be with_zero set;
cluster relocable IC-recognized
for standard halting
IC-Ins-separated non empty with_non-empty_values AMI-Struct over N;
existence
proof
take STC N;
thus thesis;
end;
end;
registration
let N be with_zero set;
let S be relocable halting IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N;
cluster -> relocable for Instruction of S;
coherence by Def2;
end;
reserve k for Nat;
theorem Th4:
for N be with_zero set
for S be relocable halting IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N
for INS being Instruction of S, s being State of S
holds Exec(IncAddr(INS,k),IncIC(s,k)) = IncIC(Exec(INS,s),k)
proof
let N be with_zero set;
let S be relocable halting IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N;
let INS be Instruction of S, s be State of S;
thus Exec(IncAddr(INS,k),IncIC(s,k))
= Exec(IncAddr(INS,(0 qua Nat)+k),IncIC(s,k))
.= IncIC(Exec(IncAddr(INS,0),s),k) by Def1
.= IncIC(Exec(INS,s),k) by COMPOS_0:3;
end;
theorem Th5:
for N be with_zero set
for S be relocable halting IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N
for INS being Instruction of S, s being State of S,
j, k being Nat st IC s = j+k
holds Exec(INS, DecIC(s,k)) = DecIC(Exec(IncAddr(INS, k), s),k)
proof
let N be with_zero set;
let S be relocable halting IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N;
let INS be Instruction of S, s be State of S,
j,k be Nat such that
A1: IC s = j+k;
set s1 = s +* Start-At(j,S);
A2: IncIC(s1,k) = s +* Start-At(IC s,S) by A1,MEMSTR_0:58
.= s by MEMSTR_0:31;
thus Exec(INS, DecIC(s,k))
= Exec(INS,s1) by A1,NAT_D:34
.= (Exec(INS,s1) +* Start-At(IC Exec(INS,s1),S)) by MEMSTR_0:31
.= (IncIC(Exec(INS,s1),k) +*
Start-At(IC Exec(INS,s1),S)) by FUNCT_4:114
.= DecIC( IncIC(Exec(INS,s1),k),k) by MEMSTR_0:59
.= DecIC(Exec(IncAddr(INS, k), s),k) by A2,Th4;
end;
registration let N be with_zero set;
cluster relocable IC-recognized
for halting IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N;
existence
proof
take STC N;
thus thesis;
end;
end;
reserve N for with_zero set,
S for IC-recognized
halting IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N;
theorem Th6:
for q be non halt-free finite
(the InstructionsF of S)-valued NAT-defined Function
for p being q-autonomic non empty FinPartState of S
holds IC S in dom p
proof
let q be non halt-free finite
(the InstructionsF of S)-valued NAT-defined Function;
let p be q-autonomic non empty FinPartState of S;
A1: dom p meets {IC S} \/ Data-Locations S by MEMSTR_0:41;
per cases by A1,XBOOLE_1:70;
suppose dom p meets {IC S};
hence thesis by ZFMISC_1:50;
end;
suppose dom p meets Data-Locations S;
then dom p /\ Data-Locations S <> {} by XBOOLE_0:def 7;
then DataPart p <> {} by RELAT_1:38,61;
hence thesis by Th3;
end;
end;
definition let N;
let S be halting IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N;
attr S is CurIns-recognized means
:Def4:
for q be non halt-free finite
(the InstructionsF of S)-valued NAT-defined Function
for p being q-autonomic non empty FinPartState of S
for s being State of S st p c= s
for P being Instruction-Sequence of S
st q c= P
for i being Nat holds IC Comput(P,s,i) in dom q;
end;
registration let N;
cluster STC N -> CurIns-recognized;
coherence
proof
let q be non halt-free finite
(the InstructionsF of STC N)-valued NAT-defined Function;
let p be q-autonomic non empty FinPartState of STC N,
s be State of STC N such that
A1: p c= s;
let P be Instruction-Sequence of STC N such that
A2: q c= P;
let i be Nat;
set Csi = Comput(P,s,i);
set loc = IC Csi;
set loc1 = loc+1;
assume
A3: not IC Comput(P,s,i) in dom q;
the InstructionsF of STC N = {[0,0,0],[1,0,0]} by AMISTD_1:def 7;
then
reconsider I = [1,0,0] as Instruction of STC N by TARSKI:def 2;
set p1 = q +* (loc .--> I);
set p2 = q +* (loc .--> halt STC N);
reconsider P1 = P +* (loc .--> I)
as Instruction-Sequence of STC N;
reconsider P2 = P +* (loc .--> halt STC N)
as Instruction-Sequence of STC N;
A5: loc in dom (loc .--> halt STC N) by TARSKI:def 1;
A7: loc in dom (loc .--> I) by TARSKI:def 1;
A8: dom q misses dom (loc .--> halt STC N) by A3,ZFMISC_1:50;
A9: dom q misses dom (loc .--> I) by A3,ZFMISC_1:50;
A10: p1 c= P1 by A2,FUNCT_4:123;
A11: p2 c= P2 by A2,FUNCT_4:123;
set Cs2i = Comput(P2,s,i), Cs1i = Comput(P1,s,i);
p is not q-autonomic
proof
(loc .--> halt STC N).loc = halt STC N by FUNCOP_1:72;
then
A12: P2.loc = halt STC N by A5,FUNCT_4:13;
(loc .--> I).loc = I by FUNCOP_1:72;
then
A13: P1.loc = I by A7,FUNCT_4:13;
take P1, P2;
q c= p1 by A9,FUNCT_4:32;
hence
A14: q c= P1 by A10,XBOOLE_1:1;
q c= p2 by A8,FUNCT_4:32;
hence
A15: q c= P2 by A11,XBOOLE_1:1;
take s, s;
thus p c= s by A1;
A16: (Cs1i|dom p) = (Csi|dom p) by A14,A2,A1,EXTPRO_1:def 10;
thus p c= s by A1;
A17: (Cs1i|dom p) = (Cs2i|dom p) by A14,A15,A1,EXTPRO_1:def 10;
take k = i+1;
set Cs1k = Comput(P1,s,k);
A18: Cs1k = Following(P1,Cs1i) by EXTPRO_1:3
.= Exec (CurInstr(P1,Cs1i), Cs1i);
InsCode I = 1;
then
A19: IC Exec(I,Cs1i) = IC Cs1i + 1 by AMISTD_1:9;
A20: IC Csi = IC(Csi|dom p) by Th6,FUNCT_1:49;
then IC Cs1i = loc by A16,Th6,FUNCT_1:49;
then
A21: IC Cs1k = loc1 by A19,A18,A13,PBOOLE:143;
set Cs2k = Comput(P2,s,k);
A22: Cs2k = Following(P2,Cs2i) by EXTPRO_1:3
.= Exec (CurInstr(P2,Cs2i), Cs2i);
A23: P2/.IC Cs2i = P2.IC Cs2i by PBOOLE:143;
IC Cs2i = loc by A16,A20,A17,Th6,FUNCT_1:49;
then
A24: IC Cs2k = loc by A22,A12,A23,EXTPRO_1:def 3;
IC(Cs1k|dom p) = IC Cs1k & IC(Cs2k|dom p) = IC Cs2k
by Th6,FUNCT_1:49;
hence thesis by A21,A24;
end;
hence contradiction;
end;
end;
registration let N be with_zero set;
cluster relocable IC-recognized CurIns-recognized
for halting IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N;
existence
proof
take STC N;
thus thesis;
end;
end;
reserve
S for IC-recognized CurIns-recognized
halting IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N;
theorem
for q be non halt-free finite
(the InstructionsF of S)-valued NAT-defined Function
for p being q-autonomic non empty FinPartState of S,
s1,s2 being State of S st p c= s1 & p c= s2
for P1,P2 being Instruction-Sequence of S
st q c= P1 & q c= P2
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
let q be non halt-free finite
(the InstructionsF of S)-valued NAT-defined Function;
let p be q-autonomic non empty FinPartState of S,
s1, s2 be State of S such that
A1: p c= s1 and
A2: p c= s2;
let P1,P2 be Instruction-Sequence of S such that
A3: q c= P1 and
A4: q c= P2;
A5: dom q c= dom P1 by A3,RELAT_1:11;
A6: dom q c= dom P2 by A4,RELAT_1:11;
let i be Nat;
set Cs2i = Comput(P2,s2,i);
set Cs1i = Comput(P1,s1,i);
A7: IC Cs1i in dom q by A3,Def4,A1;
A8: IC Cs2i in dom q by A4,Def4,A2;
thus
A9: IC Cs1i = IC Cs2i
proof
assume
A10: IC Comput(P1,s1,i) <> IC Comput(P2,s2,i);
(Cs1i|dom p).IC S = Cs1i.IC S & (Cs2i|dom p).IC S = Cs2i.IC S
by Th6,FUNCT_1:49;
hence contradiction by A10,A3,A4,A1,A2,EXTPRO_1:def 10;
end;
thus CurInstr(P1,Comput(P1,s1,i))
= P1.IC Cs1i by A7,A5,PARTFUN1:def 6
.= q.IC Cs1i by A7,A3,GRFUNC_1:2
.= P2.IC Cs2i by A8,A4,A9,GRFUNC_1:2
.= CurInstr(P2,Comput(P2,s2,i)) by A8,A6,PARTFUN1:def 6;
end;
reserve S for relocable IC-recognized CurIns-recognized
halting IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N;
theorem
for k being Nat
for q be non halt-free finite
(the InstructionsF of S)-valued NAT-defined Function
for p being q-autonomic FinPartState of S
st IC S in dom p
for s being State of S st p c= s
for P being Instruction-Sequence of S
st q c= P
for i being Nat
holds Comput(P +* Reloc(q,k),s +* IncIC( p,k),i) =
IncIC(Comput(P,s,i),k)
proof
let k be Nat;
let q be non halt-free finite
(the InstructionsF of S)-valued NAT-defined Function;
let p be q-autonomic FinPartState of S such that
A1: IC S in dom p;
let s be State of S such that
A2: p c= s;
let P be Instruction-Sequence of S;
assume
A3: q c= P;
defpred P[Nat] means
Comput(P+*Reloc(q,k),s+*IncIC( p,k),$1) =
IncIC(Comput(P,s,$1),k);
A4: for i being Nat st P[i] holds P[i+1]
proof
let i be Nat such that
A5: Comput(P+*Reloc(q,k),s+*IncIC( p,k),i)
= IncIC(Comput(P,s,i),k);
reconsider kk = IC Comput(P,s,i) as Nat;
A6: IC S in dom Start-At (IC Comput(P,s,i) +k,S) by TARSKI:def 1;
A7: IC (IncIC(Comput(P,s,i),k))
= IC Start-At (IC Comput(P,s,i) +k,S) by A6,FUNCT_4:13
.= IC Comput(P,s,i) + k by FUNCOP_1:72;
p is not empty by A1;
then
A8: IC Comput(P,s,i) in dom q by A3,Def4,A2;
then
A9: IC Comput(P,s,i) in dom IncAddr(q,k) by COMPOS_1:def 21;
A10: q/.kk = q.IC Comput(P,s,i) by A8,PARTFUN1:def 6
.= P.IC Comput(P,s,i) by A8,A3,GRFUNC_1:2;
reconsider kk = IC Comput(P,s,i) as Nat;
A11: (IC Comput(P,s,i) +k)
in dom Reloc(q,k) by A8,COMPOS_1:46;
A12: CurInstr(P+*Reloc(q,k),
Comput(P+*Reloc(q,k),s+*IncIC( p,k),i))
= (P+*Reloc(q,k)).
IC Comput(P+*Reloc(q,k),s+*IncIC( p,k),i)
by PBOOLE:143
.= Reloc(q,k).(IC Comput(P,s,i) +k) by A5,A7,A11,FUNCT_4:13
.= IncAddr(q,k).kk by A9,VALUED_1:def 12
.= IncAddr((q)/.kk,k) by A8,COMPOS_1:def 21
.= IncAddr (CurInstr(P,Comput(P,s,i)),k) by A10,PBOOLE:143;
thus Comput(P+*Reloc(q,k),
s+*IncIC( p,k),i+1)
= Following(P+*Reloc(q,k),
Comput(P+*Reloc(q,k),s+*IncIC( p,k),i))
by EXTPRO_1:3
.= IncIC(Following(P,Comput(P,s,i)),k) by A5,A12,Th4
.= IncIC(Comput(P,s,i+1),k) by EXTPRO_1:3;
end;
A13: IC p = IC s by A2,A1,GRFUNC_1:2;
A14: DataPart p c= p by MEMSTR_0:12;
Comput(P+*Reloc(q,k),s+*IncIC( p,k),0)
= s +* (DataPart p +* Start-At ((IC p) +k,S)) by A1,MEMSTR_0:56
.= s +* DataPart p +* Start-At ((IC p) +k,S) by FUNCT_4:14
.= IncIC(Comput(P,s,0),k) by A13,A14,A2,FUNCT_4:98,XBOOLE_1:1;
then
A15: P[0];
thus for i being Nat holds P[i] from NAT_1:sch 2(A15,A4);
end;
theorem Th9:
for k being Nat
for q be non halt-free finite
(the InstructionsF of S)-valued NAT-defined Function
for p being q-autonomic FinPartState of S st IC S in dom p
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
for i being Nat holds Comput(P,s,i) =
IncIC(Comput(P+*q,s+* p,i),k)
proof
let k be Nat;
let q be non halt-free finite
(the InstructionsF of S)-valued NAT-defined Function;
let p be q-autonomic FinPartState of S such that
A1: IC S in dom p;
let s be State of S such that
A2: IncIC(p,k) c= s;
let P be Instruction-Sequence of S such that
A3: Reloc(q,k) c= P;
defpred Z[Nat] means Comput(P,s,$1) =
IncIC(Comput(P+*q,s+* p,$1),k);
A4: for i being Nat st Z[i] holds Z[i+1]
proof
let i be Nat such that
A5: Comput(P,s,i) =
IncIC(Comput(P+*q,s+* p,i),k);
reconsider kk = IC Comput(P+*q,s+* p,i) as Nat;
A6: IC S in dom (Start-At (IC Comput(P+*q,s+* p,i) +k,S)) by TARSKI:def 1;
A7: p c= s+* p by FUNCT_4:25;
A8: q c= P+*q by FUNCT_4:25;
p is not empty by A1;
then
A9: IC Comput(P+*q,s+* p,i) in dom q by Def4,A7,A8;
then
A10: IC Comput(P+*q,s+* p,i) in dom IncAddr(q,k) by COMPOS_1:def 21;
A11: (IC Comput(P+*q,s+* p,i) +k) in dom Reloc(q,k)
by A9,COMPOS_1:46;
reconsider kk = (IC Comput(P+*q,s+* p,i)) as Nat;
A12: IC Comput(P,s,i)
= IC(Start-At (IC Comput(P+*q,s+* p,i) +k,S)) by A5,A6,FUNCT_4:13
.= IC Comput(P+*q,s+* p,i) + k by FUNCOP_1:72;
A13: q c= P+*q by FUNCT_4:25;
A14: (q)/.kk = (q).kk by A9,PARTFUN1:def 6;
A15: dom(P+*q) = NAT by PARTFUN1:def 2;
dom P = NAT by PARTFUN1:def 2;
then
A16: CurInstr(P,Comput(P,s,i))
= P.IC Comput(P,s,i) by PARTFUN1:def 6
.= Reloc(q,k).IC Comput(P,s,i) by A3,A11,A12,GRFUNC_1:2
.= IncAddr(q,k).kk by A10,A12,VALUED_1:def 12
.= IncAddr((q)/.kk,k) by A9,COMPOS_1:def 21
.= IncAddr(
(P+*q).IC Comput(P+*q,s+* p,i)
,k) by A9,A14,A13,GRFUNC_1:2
.= IncAddr(
CurInstr(P+*q,Comput(P+*q,s+* p,i))
,k) by A15,PARTFUN1:def 6;
thus Comput(P,s,i+1)
= Following(P,Comput(P,s,i)) by EXTPRO_1:3
.= IncIC(Following(P+*q,
Comput(P+*q,s+* p,i)),k) by A5,A16,Th4
.= IncIC(Comput(P+*q,s+* p,i+1),k) by EXTPRO_1:3;
end;
set IP = Start-At (IC p,S);
A17: dom Start-At(IC p,S) = {IC S};
A18: Start-At (IC p + k,S) c= IncIC(p,k) by MEMSTR_0:55;
A19: IC Comput(P+*q,s+* p,0) = IC p by A1,FUNCT_4:13;
set DP = DataPart p;
DataPart IncIC(p,k) c= IncIC(p,k) by RELAT_1:59;
then DataPart IncIC(p,k) c= s by A2,XBOOLE_1:1;
then
A20: DataPart p c= s by MEMSTR_0:51;
set PR = Reloc(q,k);
set IS = Start-At (IC Comput(P+*q,s+* p,0) +k,S);
A21: dom Start-At (IC Comput(P+*q,s+* p,0) +k,S) = {IC S};
Comput(P,s,0)
= s +* IS by A19,A2,A18,FUNCT_4:98,XBOOLE_1:1
.= s +* DP +* IS by A20,FUNCT_4:98
.= s+* DP +* IP +* IS by A21,A17,FUNCT_4:74
.= s +*(DP +* IP) +* IS by FUNCT_4:14
.= IncIC(Comput(P+*q,s+* p,0),k) by A1,MEMSTR_0:26;
then
A22: Z[0];
thus for i being Nat holds Z[i] from NAT_1:sch 2 (A22,A4 );
end;
reserve m,j for Nat;
theorem Th10:
for k being Nat
for q be non halt-free finite
(the InstructionsF of S)-valued NAT-defined Function
for p being non empty FinPartState of S st IC
S in dom p
for s being State of S st p c= s &
IncIC(p,k) is Reloc(q,k)-autonomic
for P being Instruction-Sequence of S
st q c= P
for i being Nat holds Comput(P,s,i)
= DecIC(Comput(P+*Reloc(q,k),s+*IncIC(p,k),i),k)
proof
let k be Nat;
let q be non halt-free finite
(the InstructionsF of S)-valued NAT-defined Function;
let p be non empty FinPartState of S;
assume
A1: IC S in dom p;
then
A2: Start-At (IC p,S) c= p by FUNCOP_1:84;
let s be State of S such that
A3: p c= s and
A4: IncIC(p,k) is Reloc(q,k)-autonomic;
let P be Instruction-Sequence of S such that
A5: q c= P;
defpred Z[Nat] means Comput(P,s,$1) =
DecIC(Comput(P+*Reloc(q,k),s+*IncIC(p,k),$1),k);
A6: for i being Nat st Z[i] holds Z[i+1]
proof
reconsider pp = q as preProgram of S;
let i be Nat such that
A7: Comput(P,s,i) =
DecIC(Comput(P+*Reloc(q,k),s+*IncIC(p,k),i),k);
reconsider kk = IC Comput(P+*Reloc(q,k),s+*IncIC(p,k),
i) as Nat;
reconsider jk = IC Comput(P+*Reloc(q,k),s+*IncIC(p,k),
i) as Nat;
A8: IncIC(p,k) c= s+*IncIC(p,k) by FUNCT_4:25;
A9: Reloc(q,k) c= P+*Reloc(q,k) by FUNCT_4:25;
A10: IC Comput(P+*Reloc(q,k),s+*IncIC(p,k),i) in dom
Reloc(q,k) by A4,Def4,A8,A9;
then
A11: jk in { j+k where j is Nat : j in dom q } by COMPOS_1:33;
A12: IC S in dom (Start-At (IC Comput(P+*Reloc(q,k),s+*
IncIC(p,k),i) -'k,S))
by TARSKI:def 1;
consider j being Nat such that
A13: jk = j+k and
A14: j in dom q by A11;
A15: dom(P+*Reloc(q,k)) = NAT by PARTFUN1:def 2;
A16: Reloc(q,k) c= P+*Reloc(q,k) by FUNCT_4:25;
A17: Reloc(q,k) = IncAddr(Shift(q,k),k) by COMPOS_1:34;
dom Shift(pp, k) = { m+k where m is Nat : m in dom pp} by VALUED_1:def 12;
then
A18: (j+k) in dom Shift(q, k) by A14;
then
A19: IncAddr(Shift(q, k)/.kk,k)
= Reloc(q,
k). IC Comput(P+*Reloc(q,k),s+*IncIC(p,k),i) by A13,A17,COMPOS_1:def 21
.= (P+*Reloc(q,k)).
IC Comput(P+*Reloc(q,k),s+*IncIC(p,k),i)
by A10,A16,GRFUNC_1:2
.= CurInstr(P+*Reloc(q,k),
Comput(P+*Reloc(q,k),s+*IncIC(p,k),i))
by A15,PARTFUN1:def 6;
A20: j+k -' k = j by NAT_D:34;
A21: dom P = NAT by PARTFUN1:def 2;
A22: IC ( DecIC(Comput(P+*Reloc(q,k),s+*IncIC(p,k),i),k)
)
= (Start-At (IC Comput(P+*Reloc(q,k),s+*IncIC(p,k),
i) -'k,S)).IC S
by A12,FUNCT_4:13
.= IC Comput(P+*Reloc(q,k),s+*IncIC(p,k),i) -' k by FUNCOP_1:72;
CurInstr(P,Comput(P,s,i))
= P.IC Comput(P,s,i)
by A21,PARTFUN1:def 6
.= (q).IC Comput(P,s,i)
by A7,A13,A14,A20,A5,A22,GRFUNC_1:2
.= Shift(q, k).
(IC Comput(P+*Reloc(q,k),s+*IncIC(p,k),i))
by A13,A14,A20,A7,A22,VALUED_1:def 12
.= Shift(q, k)/.kk by A13,A18,PARTFUN1:def 6;
then
A23: Comput(P+*Reloc(q,k),s+*IncIC(p,k),i+1)
= Following(P+*Reloc(q,k),
Comput(P+*Reloc(q,k),s+*IncIC(p,k),i)) &
Exec(CurInstr(P,Comput(P,s,i)),
DecIC(Comput(P+*Reloc(q,k),s+*IncIC(p,k),i),k))
= DecIC(Following(P+*Reloc(q,k),
Comput(P+*Reloc(q,k),s +*IncIC(p,k),i)),k)
by A13,A19,Th5,EXTPRO_1:3;
thus Comput(P,s,i+1)
= Following(P,Comput(P,s,i)) by EXTPRO_1:3
.= DecIC(Comput(P+*Reloc(q,k),s+*IncIC(p,k),i+1),k)
by A7,A23;
end;
A24: IC S in dom IncIC(p,k) by MEMSTR_0:52;
A25: IC Comput(P+*Reloc(q,k),s+*IncIC(p,k),0) = IC IncIC(p,k)
by A24,FUNCT_4:13;
A26: DataPart p c= p by RELAT_1:59;
set DP = DataPart p;
set IP = Start-At((IC p)+k,S);
set PP = q;
set IS = Start-At (IC Comput(P+*Reloc(q,k),s+*IncIC(p,k),0) -'k,S);
A27: dom Start-At((IC p)+k,S) = {IC S};
set PR = Reloc(q,k);
set SD = s|(dom Reloc(q,k));
A28: {IC S} misses dom DataPart p by MEMSTR_0:4;
A29: dom Start-At (IC Comput(P+*Reloc(q,k),s+*IncIC(p,k),0
) -'k,S) = {IC S};
A30: dom IP misses dom DP by A28;
A31: IP +* DP = DP +* IP by A30,FUNCT_4:35
.= IncIC(p,k) by A1,MEMSTR_0:56;
Comput(P,s,0)
= s +* Start-At(IC p,S) by A3,A2,FUNCT_4:98,XBOOLE_1:1
.= s +* Start-At (IC p + k -'k,S) by NAT_D:34
.= s +* IS by A25,MEMSTR_0:53
.= s +* DP +* IS by A26,A3,FUNCT_4:98,XBOOLE_1:1
.= s +* DP +* IP +* IS by A29,A27,FUNCT_4:74
.= s +*(DP +* IP) +* IS by FUNCT_4:14
.= DecIC(Comput(P+*Reloc(q,k),s+*IncIC(p,k),0),k)
by A31,A27,A28,FUNCT_4:35;
then
A32: Z[0];
thus for i being Nat holds Z[i] from NAT_1:sch 2 (A32, A6);
end;
theorem Th11:
for q be non halt-free finite
(the InstructionsF of S)-valued NAT-defined Function
for p being non empty FinPartState of S st IC S in dom p
for k being Nat holds
p is q-autonomic iff IncIC(p,k) is Reloc(q,k)-autonomic
proof
let q be non halt-free finite
(the InstructionsF of S)-valued NAT-defined Function;
let p be non empty FinPartState of S such that
A1: IC S in dom p;
let k be Nat;
hereby
assume
A2: p is q-autonomic;
thus IncIC(p,k) is Reloc(q,k)-autonomic
proof
let P,Q be Instruction-Sequence of S such that
A3: Reloc(q,k) c= P and
A4: Reloc(q,k) c= Q;
let s1,s2 be State of S such that
A5: IncIC(p,k) c= s1 and
A6: IncIC(p,k) c= s2;
let i be Nat;
A7: dom (Start-At ((IC Comput(Q+*q,s2+* p,i))+k,S)) = {IC S};
A8: dom(DataPart p) misses
dom (Start-At (IC Comput(Q+*q,s2+* p,i) +k,S))
by MEMSTR_0:4;
A9: dom (Start-At ((IC Comput(P+*q,s1+* p,i))+k,S)) = {IC S};
A10: dom(DataPart p) misses
dom (Start-At (IC Comput(P+*q,s1+* p,i) +k,S))
by MEMSTR_0:4;
A11: q c= P+*q & q c= Q+*q
by FUNCT_4:25;
p c= s1 +* p & p c= s2 +* p by FUNCT_4:25;
then
A12: Comput(P+*q,s1+* p,i)|dom p
= Comput(Q+*q,s2+* p,i) |dom p
by A2,A11;
A13: DataPart p c= p by MEMSTR_0:12;
A14: Comput(P,s1,i)|dom (DataPart p)
= IncIC(Comput(P+*q,s1+* p,i),k) | dom DataPart p by A1,A2,A5,Th9,A3
.= ( Comput(P+*q,s1+* p,i)) | dom (DataPart p)
by A10,FUNCT_4:72
.= ( Comput(Q+*q,s2+* p,i)) | dom (DataPart p)
by A12,A13,RELAT_1:11,153
.= ( IncIC(Comput(Q+*q,s2+* p,i),k))|dom DataPart p by A8,FUNCT_4:72
.= Comput(Q,s2,i)|dom DataPart p by A1,A2,A6,Th9,A4;
A15: {IC S} c= dom p by A1,ZFMISC_1:31;
A16: Start-At (IC Comput(P+*q,s1+* p,i),S)
= Comput(P+*q,s1+* p,i)|{IC S} by MEMSTR_0:18
.= Comput(Q+*q,s2+* p,i)|{IC S}
by A12,A15,RELAT_1:153
.= Start-At (IC Comput(Q+*q,s2+* p,i),S) by MEMSTR_0:18;
A18: Comput(P,s1,i)|dom (Start-At((IC p)+k,S))
= IncIC(Comput(P+*q,s1+* p,i),k)|
dom (Start-At((IC p)+k,S)) by A1,A2,A5,Th9,A3
.= Start-At (IC Comput(P+*q,s1+* p,i) +k,S)
by A9
.= Start-At (IC Comput(Q+*q,s2+* p,i) +k,S)
by A16,MEMSTR_0:21
.= ( IncIC(Comput(Q+*q,s2+* p,i),k))|
dom (Start-At((IC p)+k,S)) by A7
.= Comput(Q,s2,i)|dom (Start-At((IC p)+k,S)) by A1,A2,A6,Th9,A4;
A20: dom p = {IC S} \/ dom DataPart p by A1,MEMSTR_0:24;
A21: Comput(P,s1,i)|dom p
= Comput(P,s1,i)|{IC S}
\/ Comput(P,s1,i)|dom DataPart p by A20,RELAT_1:78
.= Comput(Q,s2,i)|dom p
by A20,A14,A18,RELAT_1:78;
A22: dom IncIC( p,k)
= dom p \/ dom Start-At((IC p)+k,S) by FUNCT_4:def 1;
A23: Comput(P,s1,i)|dom IncIC( p,k)
= Comput(P,s1,i)|dom p
\/ Comput(P,s1,i)|dom Start-At((IC p)+k,S) by A22,RELAT_1:78
.= Comput(Q,s2,i)|dom IncIC( p,k)
by A22,A18,A21,RELAT_1:78;
thus Comput(P,s1,i)|dom IncIC(p,k)
= Comput(Q,s2,i)|dom IncIC(p,k) by A23;
end;
end;
assume
A24: IncIC(p,k) is Reloc(q,k)-autonomic;
A25: DataPart p c= IncIC(p,k) by MEMSTR_0:62;
let P,Q be Instruction-Sequence of S such that
A26: q c= P and
A27: q c= Q;
A28: Reloc(q,k) c= P +* Reloc(q,k) &
Reloc(q,k) c= Q +* Reloc(q,k)
by FUNCT_4:25;
let s1,s2 be State of S such that
A29: p c= s1 and
A30: p c= s2;
let i be Nat;
IncIC(p,k) c= s1 +* IncIC(p,k) &
IncIC(p,k) c= s2 +* IncIC(p,k) by FUNCT_4:25;
then
A31: Comput(P +* Reloc(q,k),s1+*IncIC(p,k),i)|dom IncIC(p,k)
= Comput(Q +* Reloc(q,k),s2+*IncIC(p,k),i)|dom IncIC(p,k)
by A24,A28;
A32: dom (Start-At ((IC Comput(Q +* Reloc(q,k),s2+*IncIC(p,k),i)) -'k,S))
= {IC S};
A33: dom(DataPart p) misses
dom(Start-At (IC Comput(Q+*Reloc(q,k),s2+*IncIC(p,k),i) -'k,S))
by MEMSTR_0:4;
A34: dom (Start-At ((IC Comput(P +* Reloc(q,k),s1+*IncIC(p,k),i)) -'k,S))
= {IC S};
A35: dom(DataPart p) misses
dom(Start-At (IC Comput(P+*Reloc(q,k),s1+*IncIC(p,k),i) -'k,S))
by MEMSTR_0:4;
A36: Comput(P,s1,i)|dom (DataPart p)
= ( DecIC(Comput(P+*Reloc(q,k),s1+*IncIC(p,k)
,i),k)) | dom(DataPart p) by A1,A24,A29,Th10,A26
.= ( Comput(P +* Reloc(q,k),s1+*IncIC(p,k),i)) | dom
(DataPart p) by A35,FUNCT_4:72
.= ( Comput(Q +* Reloc(q,k),s2+*IncIC(p,k),i)) | dom
(DataPart p) by A31,A25,RELAT_1:11,153
.= DecIC(Comput(Q +* Reloc(q,k),s2+*IncIC(p,k),i),k)
| dom(DataPart p) by A33,FUNCT_4:72
.= Comput(Q,s2,i)|dom (DataPart p) by A1,A24,A30,Th10,A27;
IC S in dom IncIC(p,k) by MEMSTR_0:52;
then
A37: {IC S} c= dom IncIC(p,k) by ZFMISC_1:31;
A38: Start-At (IC Comput(P +* Reloc(q,k),s1+*IncIC(p,k),i),
S) = Comput(P+*Reloc(q,k),s1+*
IncIC(p,k),i)|{IC S} by MEMSTR_0:18
.= Comput(Q +* Reloc(q,k),s2+*IncIC(p,k),i)|{IC S}
by A31,A37,RELAT_1:153
.= Start-At (IC Comput(Q +* Reloc(q,k),s2+*IncIC(p,k)
,i),S) by MEMSTR_0:18;
A40: Comput(P,s1,i)|dom (Start-At(IC p,S))
= ( DecIC(Comput(P+*Reloc(q,k),s1+*IncIC(p,k),i),k))
|dom (Start-At(IC p,S)) by A1,A24,A29,Th10,A26
.= Start-At (IC Comput(P +* Reloc(q,k),s1+*IncIC(p,k)
,i) -'k,S) by A34
.= Start-At (IC Comput(Q +* Reloc(q,k),s2+*IncIC(p,k),i) -'k,S)
by A38,MEMSTR_0:22
.= DecIC(Comput(Q +* Reloc(q,k),s2+*IncIC(p,k),i),k)
|dom (Start-At(IC p,S))
by A32
.= Comput(Q,s2,i)|dom Start-At(IC p,S) by A1,A24,A30,Th10,A27;
thus Comput(P,s1,i)|dom p
= Comput(P,s1,i)|dom(Start-At(IC p,S) +*
DataPart p ) by A1,MEMSTR_0:19
.= Comput(P,s1,i)|(dom (Start-At(IC p,S)) \/ dom (DataPart p))
by FUNCT_4:def 1
.= Comput(Q,s2,i)|dom (Start-At(IC p,S)) \/
Comput(Q,s2,i)|dom (DataPart p) by A36,A40,RELAT_1:78
.= Comput(Q,s2,i)|(dom (Start-At(IC p,S)) \/ dom DataPart p)
by RELAT_1:78
.= Comput(Q,s2,i)|dom (Start-At(IC p,S) +* DataPart p) by FUNCT_4:def 1
.= Comput(Q,s2,i)|dom p by A1,MEMSTR_0:19;
end;
definition let N,S;
attr S is relocable1 means
:Def5: for k being Nat
for q be non halt-free finite
(the InstructionsF of S)-valued NAT-defined Function
for p being q-autonomic non empty FinPartState of S,
s1, s2 being State of S st p c= s1 & IncIC( p,k) c= s2
for P1,P2 being Instruction-Sequence of S
st q c= P1 & Reloc(q,k) c= P2
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: for k being Nat
for q be non halt-free finite
(the InstructionsF of S)-valued NAT-defined Function
for p being q-autonomic non empty FinPartState of S,
s1, s2 being State of S st p c= s1 & IncIC( p,k) c= s2
for P1,P2 being Instruction-Sequence of S
st q c= P1 & Reloc(q,k) c= P2
for i being Nat holds
Comput(P1,s1,i)|dom DataPart p = Comput(P2,s2,i)|dom DataPart p;
end;
Lm1: for k being Nat
for q be non halt-free finite
(the InstructionsF of STC N)-valued NAT-defined Function
for p being non empty q-autonomic FinPartState of STC N , s1,
s2 being State of STC N st p c= s1 & IncIC( p,k) c= s2
for P1,P2 being Instruction-Sequence of STC N
st q c= P1 & Reloc(q,k) c= P2
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
let k be Nat;
let q be non halt-free finite
(the InstructionsF of STC N)-valued NAT-defined Function;
let p be non empty q-autonomic FinPartState of STC N,
s1,s2 be State of STC N such that
A1: p c= s1 and
A2: IncIC( p,k) c= s2;
A3: IC STC N in dom p by Th6;
let P1,P2 being Instruction-Sequence of STC N
such that
A4: q c= P1 & Reloc(q,k) c= P2;
set s3 = s1 +* DataPart s2;
defpred Z[Nat] means
IC Comput(P1,s1,$1) + k = IC Comput(P2,s2,$1) &
IncAddr(CurInstr(P1,Comput(P1,s1,$1)), k)
= CurInstr(P2,Comput(P2,s2,$1));
A5: for i be Nat st Z[i] holds Z[i+1]
proof
set DPp = DataPart p;
let i be Nat such that
A6: IC Comput(P1,s1,i) + k = IC Comput(P2,s2,i) and
A7: IncAddr (CurInstr(P1,Comput(P1,s1,i)), k)
= CurInstr(P2,Comput(P2,s2,i));
set Cs2i1 = Comput(P2,s2,i+1);
set Cs3i = Comput(P1,s3,i);
set Cs2i = Comput(P2,s2,i);
set Cs3i1 = Comput(P1,s3,i+1);
set Cs1i1 = Comput(P1,s1,i+1);
set Cs1i = Comput(P1,s1,i);
A8: now
reconsider loc = IC Cs1i1 as Nat;
assume
A9: IC Comput(P1,s1,i+1) + k = IC Comput(P2,s2,i+1);
reconsider kk = loc as Nat;
A10: loc in dom q by Def4,A4,A1;
A11: loc + k in dom Reloc(q, k) by A10,COMPOS_1:46;
A12: dom P2 = NAT by PARTFUN1:def 2;
dom P1 = NAT by PARTFUN1:def 2;
then CurInstr(P1, Cs1i1) = P1.loc by PARTFUN1:def 6
.= (q).loc by A10,A4,GRFUNC_1:2;
hence
IncAddr(CurInstr(P1,Comput(P1,s1,i+1)), k)
= Reloc(q,k).(loc+k) by A10,COMPOS_1:35
.= P2.IC Comput(P2,s2,i+1) by A9,A11,A4,GRFUNC_1:2
.= CurInstr(P2,Comput(P2,s2,i+1)) by A12,PARTFUN1:def 6;
end;
set I = CurInstr(P1, Cs1i);
A13: Cs2i1 = Following(P2,Cs2i) by EXTPRO_1:3
.= Exec (CurInstr(P2, Cs2i), Cs2i);
reconsider j = IC Cs1i as Nat;
A14: Cs1i1 = Following(P1,Cs1i) by EXTPRO_1:3
.= Exec (CurInstr(P1, Cs1i), Cs1i);
A15: the InstructionsF of STC N = {[0,0,0],[1,0,0]} by AMISTD_1:def 7;
per cases by A15,TARSKI:def 2;
suppose
I = [0,0,0];
then
A16: I = halt STC N;
thus IC Comput(P1,s1,i+1) + k = IC Cs1i + k
by A14,A16,EXTPRO_1:def 3
.= IC Comput(P2,s2,i+1) by A6,A13,A16,A7,EXTPRO_1:def 3;
hence
IncAddr(CurInstr(P1,Comput(P1,s1,i+1)), k)
= CurInstr(P2,Comput(P2,s2,i+1)) by A8;
end;
suppose
I = [1,0,0];
then
A17: InsCode I = 1;
then
A18: Exec(I,Cs2i) = IncIC(Cs2i,1) by AMISTD_1:20;
thus IC Comput(P1,s1,i+1) + k = IC Cs1i + 1 + k
by A14,A17,AMISTD_1:9
.= IC Exec(I,Cs2i) by A18,A6,MEMSTR_0:53
.= IC Comput(P2,s2,i+1) by A13,A7,COMPOS_0:4;
hence
IncAddr(CurInstr(P1,Comput(P1,s1,i+1)), k)
= CurInstr(P2,Comput(P2,s2,i+1)) by A8;
end;
end;
A19: IC STC N in dom IncIC( p,k) by MEMSTR_0:52;
now
thus IC Comput(P1,s1,0) + k
= IC p + k by A1,A3,GRFUNC_1:2
.= IC IncIC(p,k) by MEMSTR_0:53
.= IC Comput(P2,s2,0) by A2,A19,GRFUNC_1:2;
reconsider loc = IC p as Nat;
A20: IC p = IC s1 by A1,A3,GRFUNC_1:2;
IC p = IC Comput(P1,s1,0) by A1,A3,GRFUNC_1:2;
then
A21: loc in dom q by Def4,A4,A1;
A22: (IC p) + k in dom Reloc(q,k) by A21,COMPOS_1:46;
A23: IC STC N in dom IncIC( p,k) by MEMSTR_0:52;
A24: (q).IC p = P1.IC s1 by A20,A21,A4,GRFUNC_1:2;
dom P2 = NAT by PARTFUN1:def 2;
then
A25: CurInstr(P2,Comput(P2,s2,0))
= P2.IC Comput(P2,s2,0) by PARTFUN1:def 6
.= P2.IC IncIC( p,k) by A2,A23,GRFUNC_1:2
.= P2.((IC p) +k) by MEMSTR_0:53
.= (Reloc(q, k)).((IC p) +k) by A22,A4,GRFUNC_1:2;
A26: dom P1 = NAT by PARTFUN1:def 2;
CurInstr(P1,Comput(P1,s1,0)) = P1.IC s1 by A26,PARTFUN1:def 6;
hence
IncAddr(CurInstr(P1,Comput(P1,s1,0)), k)
= CurInstr(P2,Comput(P2,s2,0)) by A25,A21,A24,COMPOS_1:35;
end;
then
A27: Z[0];
thus for i being Nat holds Z[i] from NAT_1:sch 2(A27,A5);
end;
registration let N;
cluster STC N -> relocable1 relocable2;
coherence
by Lm1;
end;
registration let N be with_zero set;
cluster relocable1 relocable2
for relocable IC-recognized CurIns-recognized
halting IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N;
existence
proof
take STC N;
thus thesis;
end;
end;
reserve S for relocable1 relocable2
relocable IC-recognized CurIns-recognized halting IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N;
theorem Th12:
for q be non halt-free finite
(the InstructionsF of S)-valued NAT-defined Function
for p being q-autonomic non empty FinPartState of S,
k being Nat st IC S in dom p
holds p is q-halted iff IncIC(p,k) is Reloc(q,k)-halted
proof
let q be non halt-free finite
(the InstructionsF of S)-valued NAT-defined Function;
let p be q-autonomic non empty FinPartState of S,
k be Nat;
assume
IC S in dom p;
hereby
assume
A1: p is q-halted;
thus IncIC(p,k) is Reloc(q,k)-halted
proof
let t be State of S;
assume
A2: IncIC(p,k) c= t;
let P be Instruction-Sequence of S such that
A3: Reloc(q,k) c= P;
reconsider Q = P +* q
as Instruction-Sequence of S;
set s = t +* p;
A4: q c= Q by FUNCT_4:25;
A5: p c= t +* p by FUNCT_4:25;
then Q halts_on s by A1,A4;
then consider u being Nat such that
A6: CurInstr(Q,Comput(Q,s,u)) = halt S;
take u;
dom P = NAT by PARTFUN1:def 2;
hence IC Comput(P,t,u) in dom P;
CurInstr(P,Comput(P,t,u))
= IncAddr(halt S, k) by A2,A6,Def5,A3,A4,A5
.= halt S by COMPOS_0:4;
hence thesis;
end;
end;
assume
A7: IncIC(p,k) is Reloc(q,k)-halted;
let t be State of S;
assume
A8: p c= t;
let P be Instruction-Sequence of S such that
A9: q c= P;
reconsider Q = P +* Reloc(q, k)
as Instruction-Sequence of S;
set s = t +* IncIC(p,k);
A10: Reloc(q,k) c= Q by FUNCT_4:25;
A11: IncIC(p,k) c= t +* IncIC(p,k) by FUNCT_4:25;
then Q halts_on s by A7,A10;
then consider u being Nat such that
A12: CurInstr(Q,Comput(Q,s,u)) = halt S;
take u;
dom P = NAT by PARTFUN1:def 2;
hence IC Comput(P,t,u) in dom P;
IncAddr(CurInstr(P,Comput(P,t,u)), k)
= halt S by A8,A12,Def5,A11,A9,A10
.= IncAddr(halt S,k) by COMPOS_0:4;
hence CurInstr(P,Comput(P,t,u)) = halt S by COMPOS_0:6;
end;
theorem Th13:
for q be non halt-free finite
(the InstructionsF of S)-valued NAT-defined Function
for p being q-halted q-autonomic non empty FinPartState of S
st IC S in dom p
for k being Nat holds DataPart(Result(q, p)) =
DataPart Result(Reloc(q,k),IncIC( p,k))
proof
let q be non halt-free finite
(the InstructionsF of S)-valued NAT-defined Function;
let p be q-halted q-autonomic non empty FinPartState of S
such that
A1: IC S in dom p;
let k be Nat;
consider s being State of S such that
A2: p c= s by PBOOLE:141;
consider P being
Instruction-Sequence of S
such that
A3: q c= P by PBOOLE:145;
A4: IncIC(p,k) is Reloc(q,k)-halted Reloc(q,k)-autonomic by A1,Th12,Th11;
A5: IncIC( p,k) is Autonomy of Reloc(q,k)
by A4,EXTPRO_1:def 12;
P halts_on s by A2,A3,EXTPRO_1:def 11;
then consider j1 being Nat such that
A6: Result(P,s) = Comput(P,s,j1) and
A7: CurInstr(P, Result(P,s)) = halt S by EXTPRO_1:def 9;
consider t being State of S such that
A8: IncIC( p,k) c= t by PBOOLE:141;
consider Q being
Instruction-Sequence of S
such that
A9: Reloc(q,k) c= Q by PBOOLE:145;
Q.(IC Comput(Q,t,j1)) = CurInstr(Q,Comput(Q,t,j1)) by PBOOLE:143
.= IncAddr(CurInstr(P,Comput(P,s,j1)), k)
by Def5,A3,A9,A2,A8
.= halt S by A6,A7,COMPOS_0:4;
then
A10: Result(Q,t) = Comput(Q,t,j1) by EXTPRO_1:7;
A11: Comput(Q,t,j1) | dom DataPart p
= Comput(P,s,j1) | dom DataPart p
by Def6,A9,A3,A8,A2;
A12: DataPart p = DataPart IncIC( p,k) by MEMSTR_0:51;
A13: p is Autonomy of q by EXTPRO_1:def 12;
thus DataPart(Result(q, p))
= DataPart((Result(P,s)) | dom p) by A2,A3,A13,EXTPRO_1:def 13
.= (Result(P,s)) | (dom p /\ Data-Locations S) by RELAT_1:71
.= (Result(P,s)) | dom DataPart p by MEMSTR_0:14
.= (Result(Q,t))|(dom IncIC( p,k) /\ Data-Locations S)
by A6,A10,A11,A12,MEMSTR_0:14
.= ((Result(Q,t)) | dom IncIC( p,k))|Data-Locations S
by RELAT_1:71
.= DataPart Result(Reloc(q,k),IncIC( p,k))
by A5,A9,A8,EXTPRO_1:def 13;
end;
registration let N,S;
let q be non halt-free finite
(the InstructionsF of S)-valued NAT-defined Function;
let p be q-autonomic q-halted non empty FinPartState of S,
k be Nat;
cluster IncIC(p,k) -> Reloc(q,k)-halted;
coherence
proof
IC S in dom p by Th6;
hence thesis by Th12;
end;
end;
theorem
for F being data-only PartFunc of FinPartSt S, FinPartSt S,
l being Nat
for q be non halt-free finite
(the InstructionsF of S)-valued NAT-defined Function,
p being q-autonomic q-halted non empty FinPartState of S
st IC S in dom p
for k being Nat holds q, p computes F
iff Reloc(q,k), IncIC( p,k) computes F
proof
let F be data-only PartFunc of FinPartSt S ,FinPartSt S,
l be Nat;
let q be non halt-free finite
(the InstructionsF of S)-valued NAT-defined Function,
p be q-autonomic q-halted non empty FinPartState of S
such that
A1: IC S in dom p;
let k be Nat;
hereby
assume
A2: q, p computes F;
thus Reloc(q,k), IncIC( p,k) computes F
proof
let x be set;
assume
A3: x in dom F;
then consider d1 being FinPartState of S such that
A4: x = d1 and
A5: p +* d1 is Autonomy of q and
A6: F.d1 c= Result(q, p +* d1) by A2;
dom F c= FinPartSt S by RELAT_1:def 18;
then reconsider d = x as FinPartState of S by A3,MEMSTR_0:76;
reconsider d as data-only FinPartState of S by A3,MEMSTR_0:def 17;
dom(p +* d) = dom p \/ dom d by FUNCT_4:def 1;
then
A7: IC S in dom(p +* d) by A1,XBOOLE_0:def 3;
A8: p+*d is q-autonomic by A4,A5,EXTPRO_1:def 12;
then
A9: IncIC((p +* d) ,k) is Reloc(q,k)-autonomic by A7,Th11;
A10: p+*d is q-halted by A4,A5,EXTPRO_1:def 12;
reconsider pd = p +* d
as q-halted q-autonomic non empty FinPartState of S
by A4,A5,EXTPRO_1:def 12;
A11: DataPart(Result(q, pd))
= DataPart Result(Reloc(q,k),IncIC((p+*d),k)) by A7,Th13
.= DataPart Result(Reloc(q,k),IncIC(p,k) +* d)
by MEMSTR_0:54;
reconsider Fs1 = F.d1 as FinPartState of S by A6;
take d;
thus x=d;
IncIC(p,k) +* d = IncIC(p+*d ,k) by MEMSTR_0:54;
hence IncIC( p,k) +* d is Autonomy of Reloc(q,k)
by A8,A10,A9,EXTPRO_1:def 12;
A12: Fs1 is data-only by A3,A4,MEMSTR_0:def 17;
F.d1 c= DataPart Result(Reloc(q,k),IncIC(p,k) +* d)
by A6,A12,A4,A11,MEMSTR_0:5;
hence F.d c= Result(Reloc(q,k),IncIC( p,k) +* d)
by A4,A12,MEMSTR_0:5;
end;
end;
assume
A13: Reloc(q,k), IncIC( p,k) computes F;
let x be set;
assume
A14: x in dom F;
then consider d1 being FinPartState of S such that
A15: x = d1 and
A16: IncIC(p,k) +* d1 is Autonomy of Reloc(q,k) and
A17: F.d1 c= Result(Reloc(q,k),IncIC(p,k) +* d1)
by A13;
dom F c= FinPartSt S by RELAT_1:def 18;
then reconsider d = x as FinPartState of S by A14,MEMSTR_0:76;
reconsider d as data-only FinPartState of S by A14,MEMSTR_0:def 17;
A18: dom(p +* d) = dom p \/ dom d by FUNCT_4:def 1;
then
A19: IC S in dom(p +* d) by A1,XBOOLE_0:def 3;
A20: IncIC(p,k) +* d = IncIC((p +* d),k) by MEMSTR_0:54;
IncIC(p+*d,k) is Reloc(q,k)-autonomic
by A15,A16,A20,EXTPRO_1:def 12;
then
A21: p +* d is q-autonomic by A19,Th11;
A22: IncIC(p+*d,k) is Reloc(q,k)-halted
by A15,A16,A20,EXTPRO_1:def 12;
A23: p +* d is q-halted by A19,Th12,A21,A22;
reconsider pd = p +* d
as q-halted q-autonomic non empty FinPartState of S
by A19,Th12,A21,A22;
A24: IC S in dom pd by A18,A1,XBOOLE_0:def 3;
A25: DataPart Result(Reloc(q,k),IncIC(p,k) +* d1)
= DataPart Result(Reloc(q,k),IncIC(p +* d,k)) by A15,MEMSTR_0:54
.= DataPart(Result(q, p+*d)) by Th13,A24;
take d;
thus x=d;
thus p +* d is Autonomy of q by A21,A23,EXTPRO_1:def 12;
reconsider Fs1 = F.d1 as FinPartState of S by A17;
A26: Fs1 is data-only by A14,A15,MEMSTR_0:def 17;
then F.d1 c= DataPart Result(q, p +* d)
by A25,A17,MEMSTR_0:5;
hence thesis by A15,A26,MEMSTR_0:5;
end;
reserve S for IC-recognized CurIns-recognized halting IC-Ins-separated
non empty with_non-empty_values AMI-Struct over N;
theorem
for q be non halt-free finite
(the InstructionsF of S)-valued NAT-defined Function
for p being q-autonomic
FinPartState of S st IC S in dom p holds IC p in dom q
proof
let q be non halt-free finite
(the InstructionsF of S)-valued NAT-defined Function;
let p be q-autonomic FinPartState of S;
assume
A1: IC S in dom p;
then
A2: p is non empty;
consider s being State of S such that
A3: p c= s by PBOOLE:141;
set P = (the Instruction-Sequence of S) +* q;
A4: q c= P by FUNCT_4:25;
IC Comput(P,s,0) in dom q by A4,Def4,A2,A3;
hence IC p in dom q by A3,A1,GRFUNC_1:2;
end;
definition
let N be with_zero set;
let S be halting IC-Ins-separated non empty with_non-empty_values
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
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;
registration
let N be with_zero set;
let S be halting IC-Ins-separated non empty with_non-empty_values
AMI-Struct over N;
cluster parahalting -> 0-halting for
NAT-defined (the InstructionsF of S)-valued Function;
coherence;
cluster 0-halting -> parahalting for
NAT-defined (the InstructionsF of S)-valued Function;
coherence;
end;