:: Relocability for { \bf SCM_FSA }
:: by Andrzej Trybulec and Yatsuka Nakamura
::
:: Received February 22, 1996
:: Copyright (c) 1996-2026 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, AMI_1, SCMFSA_2, AMISTD_2, ARYTM_3, FUNCT_4, XBOOLE_0,
FUNCT_1, RELAT_1, TARSKI, FSM_1, CIRCUIT2, CARD_1, XXREAL_0, EXTPRO_1,
GRAPHSP, AMI_3, ARYTM_1, INT_1, COMPLEX1, PARTFUN1, FINSEQ_1, FINSEQ_2,
NAT_1, RELOC, AMISTD_5, COMPOS_1, FINSET_1;
notations TARSKI, XBOOLE_0, SUBSET_1, FINSET_1, ORDINAL1, NUMBERS, XCMPLX_0,
INT_2, INT_1, NAT_1, PARTFUN1, RELAT_1, FUNCT_1, FINSEQ_1, FINSEQ_2,
FUNCT_4, FUNCT_7, MEMSTR_0, COMPOS_0, COMPOS_1, EXTPRO_1, SCMFSA_2,
XXREAL_0, AMISTD_5;
constructors DOMAIN_1, NAT_D, RELSET_1, FUNCT_7, PRE_POLY, AMISTD_2, SCMFSA_3,
AMISTD_5, AMI_3, SCMFSA_1;
registrations FUNCT_1, XREAL_0, INT_1, SCMFSA_2, ORDINAL1, RELAT_1, AMISTD_2,
SCMFSA10, COMPOS_1, EXTPRO_1, SCMFSA_4, SCMFSA_3, FUNCT_4, FINSEQ_1,
AMI_3, COMPOS_0, NAT_1, MEMSTR_0;
requirements NUMERALS, SUBSET, BOOLE, ARITHM, REAL;
equalities EXTPRO_1, MEMSTR_0, SCMFSA_2;
expansions AMISTD_5;
theorems GRFUNC_1, FUNCT_1, RELAT_1, SCMFSA_2, SCMFSA_3, SCMFSA_4, XBOOLE_0,
XBOOLE_1, PBOOLE, PARTFUN1, COMPOS_1, EXTPRO_1, AMISTD_5, MEMSTR_0,
AMI_2, COMPOS_0;
schemes NAT_1;
begin :: Relocability
reserve j, k, m for Nat;
begin :: Main theorems of relocatability
theorem Th1:
for k being Nat
for q being non halt-free finite
(the InstructionsF of SCM+FSA)-valued NAT-defined Function,
p being q-autonomic non empty FinPartState of
SCM+FSA, s1, s2 being State of SCM+FSA st p c= s1 & IncIC( p,k) c= s2
for P1,P2 being Instruction-Sequence of SCM+FSA
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)) &
Comput(P1,s1,i)|dom DataPart p = Comput(P2,s2,i)|dom DataPart p &
DataPart Comput(P1,s1 +* DataPart s2,i) = DataPart Comput(P2,s2,i)
proof
let k be Nat;
let q be non halt-free finite
(the InstructionsF of SCM+FSA)-valued NAT-defined Function,
p be q-autonomic non empty FinPartState of SCM+FSA, s1,s2 be
State of SCM+FSA such that
A1: p c= s1 and
A2: IncIC( p,k) c= s2;
A3: IC SCM+FSA in dom p by AMISTD_5:6;
let P1,P2 being Instruction-Sequence of SCM+FSA
such that
A4: q c= P1 & Reloc(q,k) c= P2;
A5: Reloc(q,k) c= P2 by A4;
A6: q c= P1 by A4;
set s3 = s1 +* DataPart s2;
defpred Y[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)) &
Comput(P1,s1,$1)|dom DataPart p = Comput(P2,s2,$1)|dom DataPart p &
DataPart Comput(P1,s3,$1) = DataPart Comput(P2,s2,$1);
A7: p c= s3 by A1,A2,MEMSTR_0:61;
A8: for i being Nat st Y[i] holds Y[i+1]
proof
set DPp = DataPart p;
let i be Nat such that
A9: IC Comput(P1,s1,i) + k = IC Comput(P2,s2,i) and
A10: IncAddr (CurInstr(P1,Comput(P1,s1,i)), k)
= CurInstr(P2,Comput(P2,s2,i)) and
A11: Comput(P1,s1,i)|dom DataPart p = Comput(P2,s2,i)|dom DataPart p and
A12: DataPart Comput(P1,s3,i) = DataPart Comput(P2,s2,i);
set Cs1i1 = Comput(P1,s1,i+1);
set Cs1i = Comput(P1,s1,i);
A13: dom Cs1i1 = Data-Locations SCM+FSA \/ {IC SCM+FSA}
by MEMSTR_0:13;
set Cs3i = Comput(P1,s3,i);
set Cs2i = Comput(P2,s2,i);
A14: dom Cs1i = Data-Locations SCM+FSA \/ {IC SCM+FSA}
by MEMSTR_0:13;
set Cs2i1 = Comput(P2,s2,i+1);
A15: dom Cs2i1 = Data-Locations SCM+FSA \/ {IC SCM+FSA}
by MEMSTR_0:13;
A16: dom Cs2i = Data-Locations SCM+FSA \/ {IC SCM+FSA}
by MEMSTR_0:13;
set I = CurInstr(P1, Cs1i);
A17: Cs2i1 = Following(P2,Cs2i) by EXTPRO_1:3
.= Exec (CurInstr(P2, Cs2i), Cs2i);
A18: now
let s be State of SCM+FSA, d be FinSeq-Location;
d in FinSeq-Locations by SCMFSA_2:def 5;
then d in Data-Locations SCM+FSA by SCMFSA_2:100,XBOOLE_0:def 3;
hence d in dom DataPart s by MEMSTR_0:9;
end;
A19: now
let d be FinSeq-Location;
A20: d in dom (DataPart Cs3i) by A18;
hence Cs3i.d = (DataPart Cs3i).d by FUNCT_1:47
.= Cs2i.d by A12,A20,FUNCT_1:47;
end;
set Cs3i1 = Comput(P1,s3,i+1);
A21: dom DataPart Cs2i = Data-Locations SCM+FSA by MEMSTR_0:9;
A22: dom DataPart Cs3i1 = Data-Locations SCM+FSA by MEMSTR_0:9;
A23: now
reconsider loc = IC Cs1i1 as Nat;
assume
A24: IC Comput(P1,s1,i+1) + k = IC Comput(P2,s2,i+1);
reconsider ii = loc as Nat;
A25: ii in dom q by A6,A1,AMISTD_5:def 4;
A26: loc + k in dom Reloc(q, k) by A25,COMPOS_1:46;
A27: 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 A25,A4,GRFUNC_1:2
.= (q).loc;
hence
IncAddr(CurInstr(P1,Comput(P1,s1,i+1)), k)
= Reloc(q,k).(loc+k) by A25,COMPOS_1:35
.= P2.IC Comput(P2,s2,i+1) by A24,A26,A5,GRFUNC_1:2
.= CurInstr(P2,Comput(P2,s2,i+1)) by A27,PARTFUN1:def 6;
end;
A28: now
let s be State of SCM+FSA, d be Int-Location;
d in Int-Locations by AMI_2:def 16;
then d in Data-Locations SCM+FSA by SCMFSA_2:100,XBOOLE_0:def 3;
hence d in dom DataPart s by MEMSTR_0:9;
end;
A29: now
let d be Int-Location;
A30: d in dom DataPart Cs3i by A28;
hence Cs3i.d = (DataPart Cs3i).d by FUNCT_1:47
.= Cs2i.d by A12,A30,FUNCT_1:47;
end;
dom DPp = dom p /\(Data-Locations SCM+FSA) by RELAT_1:61;
then
A31: dom DPp c= {IC SCM+FSA} \/ (Data-Locations SCM+FSA) by XBOOLE_1:10,17;
A32: dom (Cs1i1|dom DPp) = dom Cs1i1 /\ dom DPp by RELAT_1:61
.= dom DPp by A13,A31,XBOOLE_1:28;
A33: dom DataPart Cs2i1 = Data-Locations SCM+FSA by MEMSTR_0:9;
A34: now
let x be object;
assume that
A35: x in dom (Cs3i1|(Data-Locations SCM+FSA)) and
A36: Cs3i1.x = Cs2i1.x;
thus (DataPart Cs3i1).x = Cs2i1.x by A35,A36,FUNCT_1:47
.= (DataPart Cs2i1).x by A22,A33,A35,FUNCT_1:47;
end;
A37: dom DataPart Cs3i = Data-Locations SCM+FSA by MEMSTR_0:9;
A38: now
let x be set;
assume that
A39: x in dom (DataPart Cs3i1) and
A40: Cs3i1.x = Cs3i.x and
A41: Cs2i1.x = Cs2i.x;
(DataPart Cs3i).x = Cs3i.x by A37,A22,A39,FUNCT_1:47;
hence
(DataPart Cs3i1).x = (DataPart Cs2i1).x by A12,A21,A22,A34,A39,A40,A41,
FUNCT_1:47;
end;
A42: Cs3i1 = Following(P1,Cs3i) by EXTPRO_1:3
.= Exec (CurInstr(P1, Cs1i), Cs3i)
by A1,A7,A4,AMISTD_5:7;
A43: dom (Cs2i1|dom DataPart p) = dom Cs2i1 /\ dom DPp by RELAT_1:61
.= dom DPp by A15,A31,XBOOLE_1:28;
A44: now
let x,d be set such that
A45: d = x and
A46: d in dom DPp and
A47: Cs1i1.d = Cs2i1.d;
thus (Cs1i1|dom DPp).x = Cs2i1.d by A32,A45,A46,A47,FUNCT_1:47
.= (Cs2i1|dom DPp).x by A43,A45,A46,FUNCT_1:47;
end;
A48: dom (Cs1i|dom DPp) = dom Cs1i /\ dom DPp by RELAT_1:61
.= dom DPp by A14,A31,XBOOLE_1:28;
reconsider j = IC Cs1i as Nat;
A49: Cs1i1 = Following(P1,Cs1i) by EXTPRO_1:3
.= Exec (CurInstr(P1, Cs1i), Cs1i);
A50: dom (Cs2i|dom DataPart p) = dom Cs2i /\ dom DPp by RELAT_1:61
.= dom DPp by A16,A31,XBOOLE_1:28;
A51: now
let x,d be set such that
A52: d = x and
A53: d in dom DPp and
A54: Cs1i1.d = Cs1i.d and
A55: Cs2i1.d = Cs2i.d;
A56: (Cs1i|dom DPp).d = Cs1i.d by A48,A53,FUNCT_1:47;
(Cs2i|dom DPp).d = Cs2i.d by A50,A53,FUNCT_1:47;
hence (Cs1i1|dom DPp).x = Cs2i1.d by A11,A32,A52,A53,A54,A55,A56,
FUNCT_1:47
.= (Cs2i1|dom DPp).x by A43,A52,A53,FUNCT_1:47;
end;
A57: (IC Cs1i + k)+1 = (j+k+1)
.= (j+1) + k
.= (IC Cs1i + 1) + k;
InsCode I = 0 or ... or InsCode I = 12 by SCMFSA_2:16;
then per cases;
suppose
InsCode I = 0;
then
A58: I = halt SCM+FSA by SCMFSA_2:95;
thus IC Comput(P1,s1,i+1) + k = IC Cs1i + k by A49,A58,EXTPRO_1:def 3
.= IC Comput(P2,s2,i+1)
by A9,A17,A58,A10,EXTPRO_1:def 3;
hence
IncAddr(CurInstr(P1,Comput(P1,s1,i+1)), k)
= CurInstr(P2,Comput(P2,s2,i+1)) by A23;
A59: Cs2i1 = Cs2i by A17,A58,A10,EXTPRO_1:def 3;
hence Comput(P1,s1,i+1)|dom DataPart p
= Comput(P2,s2,i+1)|dom DataPart p by A11,A49,A58,EXTPRO_1:def 3;
thus thesis by A12,A42,A58,A59,EXTPRO_1:def 3;
end;
suppose
InsCode I = 1;
then consider da, db being Int-Location such that
A60: I = da := db by SCMFSA_2:30;
A61: IncAddr(I, k) = da := db by A60,COMPOS_0:4;
A62: Exec(I, Cs1i).IC SCM+FSA = IC Cs1i + 1 by A60,SCMFSA_2:63;
hence
IC Comput(P1,s1,i+1) + k = IC Comput(P2,s2,i+1)
by A9,A10,A49,A17,A57,A61,SCMFSA_2:63;
thus IncAddr(CurInstr(P1,
Comput(P1,s1,i+1)), k)
= CurInstr(P2,Comput(P2,s2,i+1))
by A9,A10,A23,A49,A17,A57,A61,A62,SCMFSA_2:63;
A63: Cs3i.db = Cs2i.db by A29;
now
let x be object;
A64: dom DPp c= Data-Locations SCM+FSA by RELAT_1:58;
assume
A65: x in dom (Cs1i1|dom DPp);
per cases by A32,A65,A64,SCMFSA_2:100,XBOOLE_0:def 3;
suppose
x in FinSeq-Locations;
then reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;
A66: Cs1i1.d = Cs1i.d by A49,A60,SCMFSA_2:63;
Cs2i1.d = Cs2i.d by A10,A17,A61,SCMFSA_2:63;
hence (Cs1i1|dom DPp).x = (Cs2i1|dom DPp).x by A32,A51,A65,A66;
end;
suppose
A67: da = x;
DPp c= p by RELAT_1:59;
then dom DPp c= dom p by GRFUNC_1:2;
then
A68: Cs3i.db = Cs1i.db by A1,A7,A32,A60,A65,A67,A4,SCMFSA_3:5;
A69: Cs1i1.x = Cs1i.db by A49,A60,A67,SCMFSA_2:63;
Cs2i1.x = Cs2i.db by A10,A17,A61,A67,SCMFSA_2:63;
hence (Cs1i1|dom DPp).x = (Cs2i1|dom DPp).x by A32,A44,A63,A65,A69
,A68;
end;
suppose
A70: da <> x & x in Int-Locations;
then reconsider d = x as Int-Location by AMI_2:def 16;
A71: Cs1i1.d = Cs1i.d by A49,A60,A70,SCMFSA_2:63;
Cs2i1.d = Cs2i.d by A10,A17,A61,A70,SCMFSA_2:63;
hence (Cs1i1|dom DPp).x = (Cs2i1|dom DPp).x by A32,A51,A65,A71;
end;
end;
then (Cs1i1|dom DPp) c= (Cs2i1|dom DPp) by A32,A43,GRFUNC_1:2;
hence Comput(P1,s1,i+1)|dom (DataPart p)
= Comput(P2,s2,i+1)|dom DataPart p by A32,A43,GRFUNC_1:3;
now
let x be object;
assume
A72: x in dom (DataPart Cs3i1);
per cases by A22,A72,SCMFSA_2:100,XBOOLE_0:def 3;
suppose
x in FinSeq-Locations;
then reconsider f = x as FinSeq-Location by SCMFSA_2:def 5;
A73: Cs3i1.f = Cs3i.f by A42,A60,SCMFSA_2:63;
Cs2i1.f = Cs2i.f by A10,A17,A61,SCMFSA_2:63;
hence (DataPart Cs3i1).x = (DataPart Cs2i1).x by A38,A72,A73;
end;
suppose
A74: da = x;
A75: Cs3i1.da=Cs3i.db by A42,A60,SCMFSA_2:63;
Cs2i1.da = Cs2i.db by A10,A17,A61,SCMFSA_2:63;
hence (DataPart Cs3i1).x = (DataPart Cs2i1).x by A29,A34,A72,A74,A75;
end;
suppose
A76: da <> x & x in Int-Locations;
then reconsider d = x as Int-Location by AMI_2:def 16;
A77: Cs3i1.d = Cs3i.d by A42,A60,A76,SCMFSA_2:63;
Cs2i1.d = Cs2i.d by A10,A17,A61,A76,SCMFSA_2:63;
hence (DataPart Cs3i1).x = (DataPart Cs2i1).x by A38,A72,A77;
end;
end;
then DataPart Cs3i1 c= DataPart Comput(P2,s2,i+1) by A22,A33,GRFUNC_1:2;
hence thesis by A22,A33,GRFUNC_1:3;
end;
suppose
InsCode I = 2;
then consider da, db being Int-Location such that
A78: I = AddTo(da, db) by SCMFSA_2:31;
A79: Cs3i.db = Cs2i.db by A29;
A80: IncAddr(I, k) = AddTo(da, db) by A78,COMPOS_0:4;
A81: Exec(I, Cs1i).IC SCM+FSA = IC Cs1i + 1 by A78,SCMFSA_2:64;
hence
IC Comput(P1,s1,i+1) + k = IC Comput(P2,s2,i+1)
by A9,A10,A49,A17,A57,A80,SCMFSA_2:64;
thus IncAddr(CurInstr(P1,
Comput(P1,s1,i+1)), k)
= CurInstr(P2,Comput(P2,s2,i+1))
by A9,A10,A23,A49,A17,A57,A80,A81,SCMFSA_2:64;
A82: Cs3i.da = Cs2i.da by A29;
now
A83: dom DPp c= Data-Locations SCM+FSA by RELAT_1:58;
let x be object such that
A84: x in dom (Cs1i1|dom DPp);
per cases by A32,A84,A83,SCMFSA_2:100,XBOOLE_0:def 3;
suppose
x in FinSeq-Locations;
then reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;
A85: Cs1i1.d=Cs1i.d by A49,A78,SCMFSA_2:64;
Cs2i1.d = Cs2i.d by A10,A17,A80,SCMFSA_2:64;
hence (Cs1i1|dom DPp).x = (Cs2i1|dom DPp).x by A32,A51,A84,A85;
end;
suppose
A86: da = x;
DPp c= p by RELAT_1:59;
then
A87: dom DPp c= dom p by GRFUNC_1:2;
A88: Cs1i1.x = Cs1i.da + Cs1i.db by A49,A78,A86,SCMFSA_2:64;
Cs2i1.x = Cs2i.da + Cs2i.db by A10,A17,A80,A86,SCMFSA_2:64;
then Cs1i1.x = Cs2i1.x by A1,A7,A32,A78,A82,A79,A84,A86,A88,A87,A4,
SCMFSA_3:6;
hence (Cs1i1|dom DPp).x = (Cs2i1|dom DPp).x by A32,A44,A84;
end;
suppose
A89: da <> x & x in Int-Locations;
then reconsider d = x as Int-Location by AMI_2:def 16;
A90: Cs1i1.d=Cs1i.d by A49,A78,A89,SCMFSA_2:64;
Cs2i1.d = Cs2i.d by A10,A17,A80,A89,SCMFSA_2:64;
hence (Cs1i1|dom DPp).x = (Cs2i1|dom DPp).x by A32,A51,A84,A90;
end;
end;
then (Cs1i1|dom DPp) c= (Cs2i1|dom DPp) by A32,A43,GRFUNC_1:2;
hence Comput(P1,s1,i+1)|dom (DataPart p)
= Comput(P2,s2,i+1)|dom DataPart p by A32,A43,GRFUNC_1:3;
now
let x be object;
assume
A91: x in dom (DataPart Cs3i1);
per cases by A22,A91,SCMFSA_2:100,XBOOLE_0:def 3;
suppose
x in FinSeq-Locations;
then reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;
A92: Cs3i1.d = Cs3i.d by A42,A78,SCMFSA_2:64;
Cs2i1.d = Cs2i.d by A10,A17,A80,SCMFSA_2:64;
hence (DataPart Cs3i1).x = (DataPart Cs2i1).x by A38,A91,A92;
end;
suppose
A93: da = x;
then
A94: Cs3i1.x = Cs3i.da + Cs3i.db by A42,A78,SCMFSA_2:64;
Cs2i1.x = Cs2i.da + Cs2i.db by A10,A17,A80,A93,SCMFSA_2:64;
hence (DataPart Cs3i1).x = (DataPart Cs2i1).x by A34,A82,A79,A91,A94;
end;
suppose
A95: da <> x & x in Int-Locations;
then reconsider d = x as Int-Location by AMI_2:def 16;
A96: Cs3i1.d = Cs3i.d by A42,A78,A95,SCMFSA_2:64;
Cs2i1.d = Cs2i.d by A10,A17,A80,A95,SCMFSA_2:64;
hence (DataPart Cs3i1).x = (DataPart Cs2i1).x by A38,A91,A96;
end;
end;
then DataPart Cs3i1 c= DataPart Comput(P2,s2,i+1) by A22,A33,GRFUNC_1:2;
hence thesis by A22,A33,GRFUNC_1:3;
end;
suppose
InsCode I = 3;
then consider da, db being Int-Location such that
A97: I = SubFrom(da, db) by SCMFSA_2:32;
A98: Cs3i.db = Cs2i.db by A29;
A99: IncAddr(I, k) = SubFrom(da, db) by A97,COMPOS_0:4;
A100: Exec(I, Cs1i).IC SCM+FSA = IC Cs1i + 1 by A97,SCMFSA_2:65;
hence
IC Comput(P1,s1,i+1) + k = IC Comput(P2,s2,i+1)
by A9,A10,A49,A17,A57,A99,SCMFSA_2:65;
thus IncAddr(CurInstr(P1,
Comput(P1,s1,i+1)), k)
= CurInstr(P2,Comput(P2,s2,i+1))
by A9,A10,A23,A49,A17,A57,A99,A100,SCMFSA_2:65;
A101: Cs3i.da = Cs2i.da by A29;
now
A102: dom DPp c= Data-Locations SCM+FSA by RELAT_1:58;
let x be object such that
A103: x in dom (Cs1i1|dom DPp);
per cases by A32,A103,A102,SCMFSA_2:100,XBOOLE_0:def 3;
suppose
x in FinSeq-Locations;
then reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;
A104: Cs1i1.d = Cs1i.d by A49,A97,SCMFSA_2:65;
Cs2i1.d = Cs2i.d by A10,A17,A99,SCMFSA_2:65;
hence (Cs1i1|dom DPp).x = (Cs2i1|dom DPp).x by A32,A51,A103,A104;
end;
suppose
A105: da = x;
DPp c= p by RELAT_1:59;
then
A106: dom DPp c= dom p by GRFUNC_1:2;
A107: Cs1i1.x = Cs1i.da - Cs1i.db by A49,A97,A105,SCMFSA_2:65;
Cs2i1.x = Cs2i.da - Cs2i.db by A10,A17,A99,A105,SCMFSA_2:65;
then Cs1i.da - Cs1i.db = Cs2i1.x by A1,A7,A32,A97,A101,A98,A103,A105
,A106,A4,SCMFSA_3:7;
hence (Cs1i1|dom DPp).x = (Cs2i1|dom DPp).x by A32,A44,A103,A107;
end;
suppose
A108: da <> x & x in Int-Locations;
then reconsider d = x as Int-Location by AMI_2:def 16;
A109: Cs1i1.d = Cs1i.d by A49,A97,A108,SCMFSA_2:65;
Cs2i1.d = Cs2i.d by A10,A17,A99,A108,SCMFSA_2:65;
hence (Cs1i1|dom DPp).x = (Cs2i1|dom DPp).x by A32,A51,A103,A109;
end;
end;
then (Cs1i1|dom DPp) c= (Cs2i1|dom DPp) by A32,A43,GRFUNC_1:2;
hence Comput(P1,s1,i+1)|dom (DataPart p)
= Comput(P2,s2,i+1)|dom DataPart p by A32,A43,GRFUNC_1:3;
now
let x be object;
assume
A110: x in dom (DataPart Cs3i1);
per cases by A22,A110,SCMFSA_2:100,XBOOLE_0:def 3;
suppose
x in FinSeq-Locations;
then reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;
A111: Cs3i1.d = Cs3i.d by A42,A97,SCMFSA_2:65;
Cs2i1.d = Cs2i.d by A10,A17,A99,SCMFSA_2:65;
hence (DataPart Cs3i1).x = (DataPart Cs2i1).x by A38,A110,A111;
end;
suppose
A112: da = x;
then
A113: Cs3i1.x = Cs3i.da - Cs3i.db by A42,A97,SCMFSA_2:65;
Cs2i1.x = Cs2i.da - Cs2i.db by A10,A17,A99,A112,SCMFSA_2:65;
hence (DataPart Cs3i1).x = (DataPart Cs2i1).x by A34,A101,A98,A110
,A113;
end;
suppose
A114: da <> x & x in Int-Locations;
then reconsider d = x as Int-Location by AMI_2:def 16;
A115: Cs3i1.d = Cs3i.d by A42,A97,A114,SCMFSA_2:65;
Cs2i1.d = Cs2i.d by A10,A17,A99,A114,SCMFSA_2:65;
hence (DataPart Cs3i1).x = (DataPart Cs2i1).x by A38,A110,A115;
end;
end;
then DataPart Cs3i1 c= DataPart Comput(P2,s2,i+1) by A22,A33,GRFUNC_1:2;
hence thesis by A22,A33,GRFUNC_1:3;
end;
suppose
InsCode I = 4;
then consider da, db being Int-Location such that
A116: I = MultBy(da, db) by SCMFSA_2:33;
A117: Cs3i.db = Cs2i.db by A29;
A118: IncAddr(I, k) = MultBy(da, db) by A116,COMPOS_0:4;
A119: Exec(I, Cs1i).IC SCM+FSA = IC Cs1i + 1 by A116,SCMFSA_2:66;
hence
IC Comput(P1,s1,i+1) + k = IC Comput(P2,s2,i+1)
by A9,A10,A49,A17,A57,A118,SCMFSA_2:66;
thus IncAddr(CurInstr(P1,
Comput(P1,s1,i+1)), k)
= CurInstr(P2,Comput(P2,s2,i+1))
by A9,A10,A23,A49,A17,A57,A118,A119,SCMFSA_2:66;
A120: Cs3i.da = Cs2i.da by A29;
now
A121: dom DPp c= Data-Locations SCM+FSA by RELAT_1:58;
let x be object such that
A122: x in dom (Cs1i1|dom DPp);
per cases by A32,A122,A121,SCMFSA_2:100,XBOOLE_0:def 3;
suppose
x in FinSeq-Locations;
then reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;
A123: Cs1i1.d = Cs1i.d by A49,A116,SCMFSA_2:66;
Cs2i1.d = Cs2i.d by A10,A17,A118,SCMFSA_2:66;
hence (Cs1i1|dom DPp).x = (Cs2i1|dom DPp).x by A32,A51,A122,A123;
end;
suppose
A124: da = x;
DPp c= p by RELAT_1:59;
then
A125: dom DPp c= dom p by GRFUNC_1:2;
A126: Cs1i1.x = Cs1i.da * Cs1i.db by A49,A116,A124,SCMFSA_2:66;
Cs2i1.x = Cs2i.da * Cs2i.db by A10,A17,A118,A124,SCMFSA_2:66;
then Cs1i1.x = Cs2i1.x by A1,A7,A32,A116,A120,A117,A122,A124,A126
,A125,A4,SCMFSA_3:8;
hence (Cs1i1|dom DPp).x = (Cs2i1|dom DPp).x by A32,A44,A122;
end;
suppose
A127: da <> x & x in Int-Locations;
then reconsider d = x as Int-Location by AMI_2:def 16;
A128: Cs1i1.d = Cs1i.d by A49,A116,A127,SCMFSA_2:66;
Cs2i1.d = Cs2i.d by A10,A17,A118,A127,SCMFSA_2:66;
hence (Cs1i1|dom DPp).x = (Cs2i1|dom DPp).x by A32,A51,A122,A128;
end;
end;
then (Cs1i1|dom DPp) c= (Cs2i1|dom DPp) by A32,A43,GRFUNC_1:2;
hence Comput(P1,s1,i+1)|dom (DataPart p)
= Comput(P2,s2,i+1)|dom DataPart p by A32,A43,GRFUNC_1:3;
now
let x be object;
assume
A129: x in dom (DataPart Cs3i1);
per cases by A22,A129,SCMFSA_2:100,XBOOLE_0:def 3;
suppose
x in FinSeq-Locations;
then reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;
A130: Cs3i1.d = Cs3i.d by A42,A116,SCMFSA_2:66;
Cs2i1.d = Cs2i.d by A10,A17,A118,SCMFSA_2:66;
hence (DataPart Cs3i1).x = (DataPart Cs2i1).x by A38,A129,A130;
end;
suppose
A131: da = x;
then
A132: Cs3i1.x = Cs3i.da * Cs3i.db by A42,A116,SCMFSA_2:66;
Cs2i1.x = Cs2i.da * Cs2i.db by A10,A17,A118,A131,SCMFSA_2:66;
hence (DataPart Cs3i1).x = (DataPart Cs2i1).x by A34,A120,A117,A129
,A132;
end;
suppose
A133: da <> x & x in Int-Locations;
then reconsider d = x as Int-Location by AMI_2:def 16;
A134: Cs3i1.d = Cs3i.d by A42,A116,A133,SCMFSA_2:66;
Cs2i1.d = Cs2i.d by A10,A17,A118,A133,SCMFSA_2:66;
hence (DataPart Cs3i1).x = (DataPart Cs2i1).x by A38,A129,A134;
end;
end;
then DataPart Cs3i1 c= DataPart Comput(P2,s2,i+1) by A22,A33,GRFUNC_1:2;
hence thesis by A22,A33,GRFUNC_1:3;
end;
suppose
InsCode I = 5;
then consider da, db being Int-Location such that
A135: I = Divide(da, db) by SCMFSA_2:34;
A136: Cs3i.db = Cs2i.db by A29;
A137: IncAddr(I, k) = Divide(da, db) by A135,COMPOS_0:4;
A138: Cs3i.da = Cs2i.da by A29;
per cases;
suppose
A139: da <> db;
A140: Exec(I, Cs1i).IC SCM+FSA = IC Cs1i + 1 by A135,SCMFSA_2:67;
hence
IC Comput(P1,s1,i+1) + k = IC Comput(P2,s2,
i+1) by A9,A10,A49,A17,A57,A137,SCMFSA_2:67;
thus IncAddr(CurInstr(P1,
Comput(P1,s1,i+1)), k)
= CurInstr(P2,Comput(
P2,s2,i+1))
by A9,A10,A23,A49,A17,A57,A137,A140,SCMFSA_2:67;
now
A141: dom DPp c= Data-Locations SCM+FSA by RELAT_1:58;
let x be object such that
A142: x in dom (Cs1i1|dom DPp);
per cases by A32,A142,A141,SCMFSA_2:100,XBOOLE_0:def 3;
suppose
db <> x & x in FinSeq-Locations;
then reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;
A143: Cs1i1.d = Cs1i.d by A49,A135,SCMFSA_2:67;
Cs2i1.d = Cs2i.d by A10,A17,A137,SCMFSA_2:67;
hence (Cs1i1|dom DPp).x = (Cs2i1|dom DPp).x by A32,A51,A142,A143;
end;
suppose
A144: da = x;
DPp c= p by RELAT_1:59;
then dom DPp c= dom p by GRFUNC_1:2;
then
A145: Cs3i.da div Cs3i.db = Cs1i.da div Cs1i.db by A1,A7,A32,A135,A139
,A142,A144,A4,SCMFSA_3:9;
A146: Cs1i1.x = Cs1i.da div Cs1i.db by A49,A135,A139,A144,SCMFSA_2:67;
Cs2i1 .x = Cs2i.da div Cs2i.db by A10,A17,A137,A139,A144,
SCMFSA_2:67;
hence (Cs1i1|dom DPp).x = Cs2i1.x by A138,A136,A142,A146,A145,
FUNCT_1:47
.= (Cs2i1|dom DPp).x by A32,A43,A142,FUNCT_1:47;
end;
suppose
A147: db = x;
DPp c= p by RELAT_1:59;
then
A148: dom DPp c= dom p by GRFUNC_1:2;
A149: Cs1i1.x = Cs1i.da mod Cs1i.db by A49,A135,A147,SCMFSA_2:67;
Cs2i1.x = Cs2i.da mod Cs2i.db by A10,A17,A137,A147,SCMFSA_2:67;
then Cs1i1.x = Cs2i1.x by A1,A7,A32,A135,A138,A136,A142,A147,A149
,A148,A4,SCMFSA_3:10;
hence (Cs1i1|dom DPp).x = (Cs2i1|dom DPp).x by A32,A44,A142;
end;
suppose
A150: da <> x & db <> x & x in Int-Locations;
then reconsider d = x as Int-Location by AMI_2:def 16;
A151: Cs1i1.d = Cs1i.d by A49,A135,A150,SCMFSA_2:67;
Cs2i1.d = Cs2i.d by A10,A17,A137,A150,SCMFSA_2:67;
hence (Cs1i1|dom DPp).x = (Cs2i1|dom DPp).x by A32,A51,A142,A151;
end;
end;
then (Cs1i1|dom DPp) c= (Cs2i1|dom DPp) by A32,A43,GRFUNC_1:2;
hence Comput(P1,s1,i+1)|dom (DataPart p)
= Comput(P2,s2,i+1)|dom DataPart p by A32,A43,GRFUNC_1:3;
now
let x be object;
assume
A152: x in dom (DataPart Cs3i1);
per cases by A22,A152,SCMFSA_2:100,XBOOLE_0:def 3;
suppose
x in FinSeq-Locations;
then reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;
A153: Cs3i1.d = Cs3i.d by A42,A135,SCMFSA_2:67;
Cs2i1.d = Cs2i.d by A10,A17,A137,SCMFSA_2:67;
hence (DataPart Cs3i1).x = (DataPart Cs2i1).x by A38,A152,A153;
end;
suppose
A154: da = x;
then
A155: Cs3i1.x = Cs3i.da div Cs3i.db by A42,A135,A139,SCMFSA_2:67;
Cs2i1.x = Cs2i.da div Cs2i.db by A10,A17,A137,A139,A154,
SCMFSA_2:67;
hence (DataPart Cs3i1).x = (DataPart Cs2i1).x by A34,A138,A136
,A152,A155;
end;
suppose
A156: db = x;
then
A157: Cs3i1.x = Cs3i.da mod Cs3i.db by A42,A135,SCMFSA_2:67;
Cs2i1.x = Cs2i.da mod Cs2i.db by A10,A17,A137,A156,SCMFSA_2:67;
hence (DataPart Cs3i1).x = (DataPart Cs2i1).x by A34,A138,A136
,A152,A157;
end;
suppose
A158: da <> x & db <> x & x in Int-Locations;
then reconsider d = x as Int-Location by AMI_2:def 16;
A159: Cs3i1.d = Cs3i.d by A42,A135,A158,SCMFSA_2:67;
Cs2i1.d = Cs2i.d by A10,A17,A137,A158,SCMFSA_2:67;
hence (DataPart Cs3i1).x = (DataPart Cs2i1).x by A38,A152,A159;
end;
end;
then
DataPart Cs3i1 c= DataPart Comput(P2,s2,i+1) by A22,A33,GRFUNC_1:2;
hence DataPart Cs3i1 = DataPart Comput(P2,s2,i+1) by A22,A33,
GRFUNC_1:3;
end;
suppose
A160: da = db;
then
A161: Exec(I, Cs1i).IC SCM+FSA = IC Cs1i + 1 by A135,SCMFSA_2:68;
hence
IC Comput(P1,s1,i+1) + k = IC Comput(P2,s2,
i+1) by A9,A10,A49,A17,A57,A137,A160,SCMFSA_2:68;
thus IncAddr(CurInstr(P1,
Comput(P1,s1,i+1)), k)
= CurInstr(P2,Comput(
P2,s2,i+1))
by A9,A10,A23,A49,A17,A57,A137,A160,A161,SCMFSA_2:68;
now
A162: dom DPp c= Data-Locations SCM+FSA by RELAT_1:58;
let x be object such that
A163: x in dom (Cs1i1|dom DPp);
per cases by A32,A163,A162,SCMFSA_2:100,XBOOLE_0:def 3;
suppose
x in FinSeq-Locations;
then reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;
A164: Cs1i1.d = Cs1i.d by A49,A135,A160,SCMFSA_2:68;
Cs2i1.d = Cs2i.d by A10,A17,A137,A160,SCMFSA_2:68;
hence (Cs1i1|dom DPp).x = (Cs2i1|dom DPp).x by A32,A51,A163,A164;
end;
suppose
A165: da = x;
A166: (Cs2i1|dom DPp).x = Cs2i1.x by A32,A43,A163,FUNCT_1:47;
A167: (Cs1i|dom DPp).x = Cs1i.x by A32,A48,A163,FUNCT_1:47;
A168: (Cs2i|dom DPp).x = Cs2i.x by A32,A50,A163,FUNCT_1:47;
A169: (Cs1i1|dom DPp).x = Cs1i1.x by A163,FUNCT_1:47;
Cs2i1.x = Cs2i.da mod Cs2i.db by A10,A17,A137,A160,A165,
SCMFSA_2:68;
hence (Cs1i1|dom DPp).x = (Cs2i1|dom DPp).x by A11,A49,A135,A160
,A165,A167,A168,A169,A166,SCMFSA_2:68;
end;
suppose
A170: da <> x & x in Int-Locations;
then reconsider d = x as Int-Location by AMI_2:def 16;
A171: Cs1i1.d = Cs1i.d by A49,A135,A160,A170,SCMFSA_2:68;
Cs2i1.d = Cs2i.d by A10,A17,A137,A160,A170,SCMFSA_2:68;
hence (Cs1i1|dom DPp).x = (Cs2i1|dom DPp).x by A32,A51,A163,A171;
end;
end;
then (Cs1i1|dom DPp) c= (Cs2i1|dom DPp) by A32,A43,GRFUNC_1:2;
hence Comput(P1,s1,i+1)|dom (DataPart p)
= Comput(P2,s2,i+1)|dom DataPart p by A32,A43,GRFUNC_1:3;
now
let x be object;
assume
A172: x in dom (DataPart Cs3i1);
per cases by A22,A172,SCMFSA_2:100,XBOOLE_0:def 3;
suppose
x in FinSeq-Locations;
then reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;
A173: Cs3i1.d = Cs3i.d by A42,A135,A160,SCMFSA_2:68;
Cs2i1.d = Cs2i.d by A10,A17,A137,A160,SCMFSA_2:68;
hence (DataPart Cs3i1).x = (DataPart Cs2i1).x by A38,A172,A173;
end;
suppose
A174: da = x;
then
A175: Cs3i1.x = Cs3i.da mod Cs3i.db by A42,A135,A160,SCMFSA_2:68;
Cs2i1.x = Cs2i.da mod Cs2i.db by A10,A17,A137,A160,A174,
SCMFSA_2:68;
hence (DataPart Cs3i1).x = (DataPart Cs2i1).x by A34,A138,A136
,A172,A175;
end;
suppose
A176: da <> x & x in Int-Locations;
then reconsider d = x as Int-Location by AMI_2:def 16;
A177: Cs3i1.d = Cs3i.d by A42,A135,A160,A176,SCMFSA_2:68;
Cs2i1.d = Cs2i.d by A10,A17,A137,A160,A176,SCMFSA_2:68;
hence (DataPart Cs3i1).x = (DataPart Cs2i1).x by A38,A172,A177;
end;
end;
then
DataPart Cs3i1 c= DataPart Comput(P2,s2,i+1) by A22,A33,GRFUNC_1:2;
hence DataPart Cs3i1 = DataPart Comput(P2,s2,i+1) by A22,A33,
GRFUNC_1:3;
end;
end;
suppose
InsCode I = 6;
then consider loc being Nat such that
A178: I = goto loc by SCMFSA_2:35;
A179: CurInstr(P2, Cs2i) = goto (loc+k) by A10,A178,SCMFSA_4:1;
thus IC Comput(P1,s1,i+1) + k = loc + k by A49,A178,SCMFSA_2:69
.= IC Comput(P2,s2,i+1) by A17,A179,SCMFSA_2:69;
hence
IncAddr(CurInstr(P1,Comput(
P1,s1,i+1)), k)
= CurInstr(P2,Comput(P2,s2,i+1)) by A23;
now
let x be object;
assume
A180: x in dom (Cs1i1|dom DPp);
dom DPp c= Data-Locations SCM+FSA by RELAT_1:58;
then x in Int-Locations or x in FinSeq-Locations by A32,A180,
SCMFSA_2:100,XBOOLE_0:def 3;
then
A181: x is Int-Location or x is FinSeq-Location by AMI_2:def 16
,SCMFSA_2:def 5;
then
A182: Cs2i1.x = Cs2i.x by A17,A179,SCMFSA_2:69;
Cs1i1.x = Cs1i.x by A49,A178,A181,SCMFSA_2:69;
hence (Cs1i1|dom DPp).x = (Cs2i1|dom DPp).x by A32,A51,A180,A182;
end;
then (Cs1i1|dom DPp) c= (Cs2i1|dom DPp) by A32,A43,GRFUNC_1:2;
hence Comput(P1,s1,i+1)|dom (DataPart p)
= Comput(P2,s2,i+1)|dom DataPart p by A32,A43,GRFUNC_1:3;
now
let x be object;
assume
A183: x in dom (DataPart Cs3i1);
then x in Int-Locations or x in FinSeq-Locations
by A22,SCMFSA_2:100,XBOOLE_0:def 3;
then
A184: x is Int-Location or x is FinSeq-Location by AMI_2:def 16
,SCMFSA_2:def 5;
then
A185: Cs2i1.x = Cs2i.x by A17,A179,SCMFSA_2:69;
Cs3i1.x = Cs3i.x by A42,A178,A184,SCMFSA_2:69;
hence (DataPart Cs3i1).x = (DataPart Cs2i1).x by A38,A183,A185;
end;
then DataPart Cs3i1 c= DataPart Comput(P2,s2,i+1) by A22,A33,GRFUNC_1:2;
hence thesis by A22,A33,GRFUNC_1:3;
end;
suppose
InsCode I = 7;
then consider loc being Nat, da being
Int-Location such that
A186: I = da=0_goto loc by SCMFSA_2:36;
A187: now
per cases;
case
Cs1i.da = 0;
hence IC Comput(P1,s1,i+1) + k = loc + k by A49,A186,SCMFSA_2:70;
end;
case
Cs1i.da <> 0;
hence
IC Comput(P1,s1,i+1) + k = (IC Cs2i)+1 by A9,A49,A57,A186,
SCMFSA_2:70;
end;
end;
A188: CurInstr(P2, Cs2i) = da=0_goto (loc+k)
by A10,A186,SCMFSA_4:2;
A189: now
per cases;
case
Cs2i.da = 0;
hence IC Comput(P2,s2,i+1) = loc + k by A17,A188,SCMFSA_2:70;
end;
case
Cs2i.da <> 0;
hence IC Comput(P2,s2,i+1) = IC Cs2i + 1 by A17,A188,SCMFSA_2:70;
end;
end;
A190: Cs3i.da = Cs2i.da by A29;
A191: now
per cases;
suppose
loc <> IC Cs1i + 1;
hence
IC Comput(P1,s1,i+1) + k = IC Comput(P2,s2,
i+1) by A1,A7,A186,A190,A187,A189,A4,SCMFSA_3:11;
end;
suppose
loc = IC Cs1i + 1;
hence
IC Comput(P1,s1,i+1) + k = IC Comput(P2,s2,i+1) by A9,A187,A189;
end;
end;
hence IC Comput(P1,s1,i+1) + k = IC Comput(P2,
s2,i+1);
thus IncAddr(CurInstr(P1,
Comput(P1,s1,i+1)), k)
= CurInstr(P2,Comput(P2,s2,i+1))
by A23,A191;
now
let x be object;
assume
A192: x in dom (Cs1i1|dom DPp);
dom DPp c= Data-Locations SCM+FSA by RELAT_1:58;
then x in Int-Locations or x in FinSeq-Locations by A32,A192,
SCMFSA_2:100,XBOOLE_0:def 3;
then
A193: x is Int-Location or x is FinSeq-Location by AMI_2:def 16
,SCMFSA_2:def 5;
then
A194: Cs2i1.x = Cs2i.x by A17,A188,SCMFSA_2:70;
Cs1i1.x = Cs1i.x by A49,A186,A193,SCMFSA_2:70;
hence (Cs1i1|dom DPp).x = (Cs2i1|dom DPp).x by A32,A51,A192,A194;
end;
then (Cs1i1|dom DPp) c= (Cs2i1|dom DPp) by A32,A43,GRFUNC_1:2;
hence Comput(P1,s1,i+1)|dom (DataPart p)
= Comput(P2,s2,i+1)|dom DataPart p by A32,A43,GRFUNC_1:3;
now
let x be object;
assume
A195: x in dom (DataPart Cs3i1);
then x in Int-Locations or x in FinSeq-Locations
by A22,SCMFSA_2:100,XBOOLE_0:def 3;
then
A196: x is Int-Location or x is FinSeq-Location by AMI_2:def 16
,SCMFSA_2:def 5;
then
A197: Cs2i1.x = Cs2i.x by A17,A188,SCMFSA_2:70;
Cs3i1.x = Cs3i.x by A42,A186,A196,SCMFSA_2:70;
hence (DataPart Cs3i1).x = (DataPart Cs2i1).x by A38,A195,A197;
end;
then DataPart Cs3i1 c= DataPart Comput(P2,s2,i+1) by A22,A33,GRFUNC_1:2;
hence thesis by A22,A33,GRFUNC_1:3;
end;
suppose
InsCode I = 8;
then consider loc being Nat, da being
Int-Location such that
A198: I = da>0_goto loc by SCMFSA_2:37;
A199: now
per cases;
case
Cs1i.da > 0;
hence IC Comput(P1,s1,i+1) + k = loc + k by A49,A198,SCMFSA_2:71;
end;
case
Cs1i.da <= 0;
hence
IC Comput(P1,s1,i+1) + k = (IC Cs2i)+1 by A9,A49,A57,A198,
SCMFSA_2:71;
end;
end;
A200: CurInstr(P2, Cs2i) = da>0_goto (loc+k)
by A10,A198,SCMFSA_4:3;
A201: now
per cases;
case
Cs2i.da > 0;
hence IC Comput(P2,s2,i+1) = loc + k by A17,A200,SCMFSA_2:71;
end;
case
Cs2i.da <= 0;
hence IC Comput(P2,s2,i+1) = IC Cs2i + 1 by A17,A200,SCMFSA_2:71;
end;
end;
A202: Cs3i.da = Cs2i.da by A29;
A203: now
per cases;
suppose
loc <> IC Cs1i + 1;
hence
IC Comput(P1,s1,i+1) + k = IC Comput(P2,s2,i+1)
by A1,A7,A198,A202,A199,A201,A4,SCMFSA_3:12;
end;
suppose
loc = IC Cs1i + 1;
hence
IC Comput(P1,s1,i+1) + k = IC Comput(P2,s2,i+1) by A9,A199,A201;
end;
end;
hence IC Comput(P1,s1,i+1) + k = IC Comput(P2,s2,i+1);
thus IncAddr(CurInstr(P1,
Comput(P1,s1,i+1)), k)
= CurInstr(P2,Comput(P2,s2,i+1))
by A23,A203;
now
let x be object;
assume
A204: x in dom (Cs1i1|dom DPp);
dom DPp c= Data-Locations SCM+FSA by RELAT_1:58;
then x in Int-Locations or x in FinSeq-Locations by A32,A204,
SCMFSA_2:100,XBOOLE_0:def 3;
then
A205: x is Int-Location or x is FinSeq-Location by AMI_2:def 16
,SCMFSA_2:def 5;
then
A206: Cs2i1.x = Cs2i.x by A17,A200,SCMFSA_2:71;
Cs1i1.x = Cs1i.x by A49,A198,A205,SCMFSA_2:71;
hence (Cs1i1|dom DPp).x = (Cs2i1|dom DPp).x by A32,A51,A204,A206;
end;
then (Cs1i1|dom DPp) c= (Cs2i1|dom DPp) by A32,A43,GRFUNC_1:2;
hence Comput(P1,s1,i+1)|dom (DataPart p)
= Comput(P2,s2,i+1)|dom DataPart p by A32,A43,GRFUNC_1:3;
now
let x be object;
assume
A207: x in dom (DataPart Cs3i1);
then x in Int-Locations or x in FinSeq-Locations
by A22,SCMFSA_2:100,XBOOLE_0:def 3;
then
A208: x is Int-Location or x is FinSeq-Location by AMI_2:def 16
,SCMFSA_2:def 5;
then
A209: Cs2i1.x = Cs2i.x by A17,A200,SCMFSA_2:71;
Cs3i1.x = Cs3i.x by A42,A198,A208,SCMFSA_2:71;
hence (DataPart Cs3i1).x = (DataPart Cs2i1).x by A38,A207,A209;
end;
then DataPart Cs3i1 c= DataPart Comput(P2,s2,i+1) by A22,A33,GRFUNC_1:2;
hence thesis by A22,A33,GRFUNC_1:3;
end;
suppose
InsCode I = 9;
then consider
db, da being Int-Location, f being FinSeq-Location such that
A210: I = da := (f,db) by SCMFSA_2:38;
A211: Cs3i.f = Cs2i.f by A19;
A212: IncAddr(I, k) = da := (f,db) by A210,COMPOS_0:4;
A213: Exec(I, Cs1i).IC SCM+FSA = IC Cs1i + 1 by A210,SCMFSA_2:72;
hence
IC Comput(P1,s1,i+1) + k = IC Comput(P2,s2,i+1)
by A9,A10,A49,A17,A57,A212,SCMFSA_2:72;
thus IncAddr(CurInstr(P1,
Comput(P1,s1,i+1)), k)
= CurInstr(P2,Comput(P2,s2,i+1))
by A9,A10,A23,A49,A17,A57,A212,A213,SCMFSA_2:72;
A214: Cs3i.db = Cs2i.db by A29;
now
let x be object;
A215: dom DPp c= Data-Locations SCM+FSA by RELAT_1:58;
assume
A216: x in dom (Cs1i1|dom DPp);
per cases by A32,A216,A215,SCMFSA_2:100,XBOOLE_0:def 3;
suppose
x in FinSeq-Locations;
then reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;
A217: Cs1i1.d = Cs1i.d by A49,A210,SCMFSA_2:72;
Cs2i1.d = Cs2i.d by A10,A17,A212,SCMFSA_2:72;
hence (Cs1i1|dom DPp).x = (Cs2i1|dom DPp).x by A32,A51,A216,A217;
end;
suppose
A218: da = x;
then consider k1 being Nat such that
A219: k1 = |.Cs1i.db.| and
A220: Cs1i1.x = (Cs1i.f)/.k1 by A49,A210,SCMFSA_2:72;
consider k2 being Nat such that
A221: k2 = |.Cs2i.db.| and
A222: Cs2i1.x = (Cs2i.f)/.k2 by A10,A17,A212,A218,SCMFSA_2:72;
DPp c= p by RELAT_1:59;
then dom DPp c= dom p by GRFUNC_1:2;
then (Cs3i.f)/.k2 = (Cs1i.f)/.k1 by A1,A7,A32,A210,A214,A216,A218
,A219,A221,A4,SCMFSA_3:13;
hence
(Cs1i1|dom DPp).x = (Cs2i1|dom DPp).x by A32,A44,A211,A216,A220,A222;
end;
suppose
A223: da <> x & x in Int-Locations;
then reconsider d = x as Int-Location by AMI_2:def 16;
A224: Cs1i1.d = Cs1i.d by A49,A210,A223,SCMFSA_2:72;
Cs2i1.d = Cs2i.d by A10,A17,A212,A223,SCMFSA_2:72;
hence (Cs1i1|dom DPp).x = (Cs2i1|dom DPp).x by A32,A51,A216,A224;
end;
end;
then (Cs1i1|dom DPp) c= (Cs2i1|dom DPp) by A32,A43,GRFUNC_1:2;
hence Comput(P1,s1,i+1)|dom (DataPart p)
= Comput(P2,s2,i+1)|dom DataPart p by A32,A43,GRFUNC_1:3;
now
let x be object;
assume
A225: x in dom (DataPart Cs3i1);
per cases by A22,A225,SCMFSA_2:100,XBOOLE_0:def 3;
suppose
x in FinSeq-Locations;
then reconsider f = x as FinSeq-Location by SCMFSA_2:def 5;
A226: Cs3i1.f = Cs3i.f by A42,A210,SCMFSA_2:72;
Cs2i1.f = Cs2i.f by A10,A17,A212,SCMFSA_2:72;
hence (DataPart Cs3i1).x = (DataPart Cs2i1).x by A38,A225,A226;
end;
suppose
A227: da = x;
then
A228: ex k1 being Nat st k1 = |.Cs3i.db.| & Cs3i1. x =
(Cs3i.f)/.k1 by A42,A210,SCMFSA_2:72;
ex k2 being Nat st k2 = |.Cs2i.db.| & Cs2i1. x =
(Cs2i.f)/.k2 by A10,A17,A212,A227,SCMFSA_2:72;
hence (DataPart Cs3i1).x = (DataPart Cs2i1).x by A34,A214,A211,A225
,A228;
end;
suppose
A229: da <> x & x in Int-Locations;
then reconsider d = x as Int-Location by AMI_2:def 16;
A230: Cs3i1.d = Cs3i.d by A42,A210,A229,SCMFSA_2:72;
Cs2i1.d = Cs2i.d by A10,A17,A212,A229,SCMFSA_2:72;
hence (DataPart Cs3i1).x = (DataPart Cs2i1).x by A38,A225,A230;
end;
end;
then DataPart Cs3i1 c= DataPart Comput(P2,s2,i+1) by A22,A33,GRFUNC_1:2;
hence thesis by A22,A33,GRFUNC_1:3;
end;
suppose
InsCode I = 10;
then consider
db, da being Int-Location, f being FinSeq-Location such that
A231: I = (f,db):=da by SCMFSA_2:39;
A232: Cs3i.f = Cs2i.f by A19;
A233: IncAddr(I, k) = (f,db):=da by A231,COMPOS_0:4;
A234: Exec(I, Cs1i).IC SCM+FSA = IC Cs1i + 1 by A231,SCMFSA_2:73;
hence
IC Comput(P1,s1,i+1) + k = IC Comput(P2,s2,i+1)
by A9,A10,A49,A17,A57,A233,SCMFSA_2:73;
A235: Cs3i.da = Cs2i.da by A29;
thus IncAddr(CurInstr(P1,
Comput(P1,s1,i+1)), k)
= CurInstr(P2,Comput(P2,s2,i+1))
by A9,A10,A23,A49,A17,A57,A233,A234,SCMFSA_2:73;
A236: Cs3i.db = Cs2i.db by A29;
now
let x be object;
A237: dom DPp c= Data-Locations SCM+FSA by RELAT_1:58;
assume
A238: x in dom (Cs1i1|dom DPp);
per cases by A32,A238,A237,SCMFSA_2:100,XBOOLE_0:def 3;
suppose
x in Int-Locations;
then reconsider d = x as Int-Location by AMI_2:def 16;
A239: Cs1i1.d = Cs1i.d by A49,A231,SCMFSA_2:73;
Cs2i1.d = Cs2i.d by A10,A17,A233,SCMFSA_2:73;
hence (Cs1i1|dom DPp).x = (Cs2i1|dom DPp).x by A32,A51,A238,A239;
end;
suppose
A240: f = x;
then consider k1 being Nat such that
A241: k1 = |.Cs1i.db.| and
A242: Cs1i1.x = Cs1i.f +*(k1,Cs1i.da) by A49,A231,SCMFSA_2:73;
consider k2 being Nat such that
A243: k2 = |.Cs2i.db.| and
A244: Cs2i1.x = Cs2i.f +*(k2,Cs2i.da) by A10,A17,A233,A240,SCMFSA_2:73;
DPp c= p by RELAT_1:59;
then dom DPp c= dom p by GRFUNC_1:2;
then Cs3i.f +*(k2,Cs3i.da) = Cs1i.f +*(k1,Cs1i.da) by A1,A7,A32,A231
,A236,A238,A240,A241,A243,A4,SCMFSA_3:14;
hence
(Cs1i1|dom DPp).x = (Cs2i1|dom DPp).x by A32,A44,A235,A232,A238,A242
,A244;
end;
suppose
A245: f <> x & x in FinSeq-Locations;
then reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;
A246: Cs1i1.d = Cs1i.d by A49,A231,A245,SCMFSA_2:73;
Cs2i1.d = Cs2i.d by A10,A17,A233,A245,SCMFSA_2:73;
hence (Cs1i1|dom DPp).x = (Cs2i1|dom DPp).x by A32,A51,A238,A246;
end;
end;
then (Cs1i1|dom DPp) c= (Cs2i1|dom DPp) by A32,A43,GRFUNC_1:2;
hence Comput(P1,s1,i+1)|dom (DataPart p)
= Comput(P2,s2,i+1)|dom DataPart p by A32,A43,GRFUNC_1:3;
now
let x be object;
assume
A247: x in dom (DataPart Cs3i1);
per cases by A22,A247,SCMFSA_2:100,XBOOLE_0:def 3;
suppose
x in Int-Locations;
then reconsider f = x as Int-Location by AMI_2:def 16;
A248: Cs3i1.f = Cs3i.f by A42,A231,SCMFSA_2:73;
Cs2i1.f = Cs2i.f by A10,A17,A233,SCMFSA_2:73;
hence (DataPart Cs3i1).x = (DataPart Cs2i1).x by A38,A247,A248;
end;
suppose
A249: f = x;
then
A250: ex k1 being Nat st k1 = |.Cs3i.db.| & Cs3i1. x =
Cs3i.f +*(k1,Cs3i.da) by A42,A231,SCMFSA_2:73;
ex k2 being Nat st k2 = |.Cs2i.db.| & Cs2i1. x =
Cs2i.f +*(k2,Cs2i.da) by A10,A17,A233,A249,SCMFSA_2:73;
hence (DataPart Cs3i1).x = (DataPart Cs2i1).x by A34,A236,A235,A232
,A247,A250;
end;
suppose
A251: f <> x & x in FinSeq-Locations;
then reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;
A252: Cs3i1.d = Cs3i.d by A42,A231,A251,SCMFSA_2:73;
Cs2i1.d = Cs2i.d by A10,A17,A233,A251,SCMFSA_2:73;
hence (DataPart Cs3i1).x = (DataPart Cs2i1).x by A38,A247,A252;
end;
end;
then DataPart Cs3i1 c= DataPart Comput(P2,s2,i+1) by A22,A33,GRFUNC_1:2;
hence thesis by A22,A33,GRFUNC_1:3;
end;
suppose
InsCode I = 11;
then consider da being Int-Location, f being FinSeq-Location such that
A253: I = da :=len f by SCMFSA_2:40;
A254: IncAddr(I, k) = da :=len f by A253,COMPOS_0:4;
A255: Exec(I, Cs1i).IC SCM+FSA = IC Cs1i + 1 by A253,SCMFSA_2:74;
hence
IC Comput(P1,s1,i+1) + k = IC Comput(P2,s2,i+1)
by A9,A10,A49,A17,A57,A254,SCMFSA_2:74;
thus IncAddr(CurInstr(P1,
Comput(P1,s1,i+1)), k)
= CurInstr(P2,Comput(P2,s2,i+1))
by A9,A10,A23,A49,A17,A57,A254,A255,SCMFSA_2:74;
A256: Cs3i.f = Cs2i.f by A19;
now
let x be object;
A257: dom DPp c= Data-Locations SCM+FSA by RELAT_1:58;
assume
A258: x in dom (Cs1i1|dom DPp);
per cases by A32,A258,A257,SCMFSA_2:100,XBOOLE_0:def 3;
suppose
x in FinSeq-Locations;
then reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;
A259: Cs1i1.d = Cs1i.d by A49,A253,SCMFSA_2:74;
Cs2i1.d = Cs2i.d by A10,A17,A254,SCMFSA_2:74;
hence (Cs1i1|dom DPp).x = (Cs2i1|dom DPp).x by A32,A51,A258,A259;
end;
suppose
A260: da = x;
DPp c= p by RELAT_1:59;
then dom DPp c= dom p by GRFUNC_1:2;
then
A261: len(Cs3i.f) = len(Cs1i.f)
by A1,A7,A32,A253,A258,A260,A4,SCMFSA_3:15;
A262: Cs1i1.x = len(Cs1i.f) by A49,A253,A260,SCMFSA_2:74;
Cs2i1.x = len(Cs2i.f) by A10,A17,A254,A260,SCMFSA_2:74;
hence
(Cs1i1|dom DPp).x = (Cs2i1|dom DPp).x by A32,A44,A256,A258,A262,A261;
end;
suppose
A263: da <> x & x in Int-Locations;
then reconsider d = x as Int-Location by AMI_2:def 16;
A264: Cs1i1.d = Cs1i.d by A49,A253,A263,SCMFSA_2:74;
Cs2i1.d = Cs2i.d by A10,A17,A254,A263,SCMFSA_2:74;
hence (Cs1i1|dom DPp).x = (Cs2i1|dom DPp).x by A32,A51,A258,A264;
end;
end;
then (Cs1i1|dom DPp) c= (Cs2i1|dom DPp) by A32,A43,GRFUNC_1:2;
hence Comput(P1,s1,i+1)|dom (DataPart p)
= Comput(P2,s2,i+1)|dom DataPart p by A32,A43,GRFUNC_1:3;
now
let x be object;
assume
A265: x in dom (DataPart Cs3i1);
per cases by A22,A265,SCMFSA_2:100,XBOOLE_0:def 3;
suppose
x in FinSeq-Locations;
then reconsider f = x as FinSeq-Location by SCMFSA_2:def 5;
A266: Cs3i1.f = Cs3i.f by A42,A253,SCMFSA_2:74;
Cs2i1.f = Cs2i.f by A10,A17,A254,SCMFSA_2:74;
hence (DataPart Cs3i1).x = (DataPart Cs2i1).x by A38,A265,A266;
end;
suppose
A267: da = x;
then
A268: Cs3i1.x = len(Cs3i.f) by A42,A253,SCMFSA_2:74;
Cs2i1.x = len(Cs2i.f) by A10,A17,A254,A267,SCMFSA_2:74;
hence (DataPart Cs3i1).x = (DataPart Cs2i1).x by A34,A256,A265,A268;
end;
suppose
A269: da <> x & x in Int-Locations;
then reconsider d = x as Int-Location by AMI_2:def 16;
A270: Cs3i1.d = Cs3i.d by A42,A253,A269,SCMFSA_2:74;
Cs2i1.d = Cs2i.d by A10,A17,A254,A269,SCMFSA_2:74;
hence (DataPart Cs3i1).x = (DataPart Cs2i1).x by A38,A265,A270;
end;
end;
then DataPart Cs3i1 c= DataPart Comput(P2,s2,i+1) by A22,A33,GRFUNC_1:2;
hence thesis by A22,A33,GRFUNC_1:3;
end;
suppose
InsCode I = 12;
then consider da being Int-Location, f being FinSeq-Location such that
A271: I = f:=<0,...,0>da by SCMFSA_2:41;
A272: IncAddr(I, k) = f:=<0,...,0>da by A271,COMPOS_0:4;
A273: Exec(I, Cs1i).IC SCM+FSA = IC Cs1i + 1 by A271,SCMFSA_2:75;
hence
IC Comput(P1,s1,i+1) + k = IC Comput(P2,s2,i+1)
by A9,A10,A49,A17,A57,A272,SCMFSA_2:75;
thus IncAddr(CurInstr(P1,Comput(P1,s1,i+1)), k)
= CurInstr(P2,Comput(P2,s2,i+1))
by A9,A10,A23,A49,A17,A57,A272,A273,SCMFSA_2:75;
A274: Cs3i.da = Cs2i.da by A29;
now
let x be object;
A275: dom DPp c= Data-Locations SCM+FSA by RELAT_1:58;
assume
A276: x in dom (Cs1i1|dom DPp);
per cases by A32,A276,A275,SCMFSA_2:100,XBOOLE_0:def 3;
suppose
x in Int-Locations;
then reconsider d = x as Int-Location by AMI_2:def 16;
A277: Cs1i1.d = Cs1i.d by A49,A271,SCMFSA_2:75;
Cs2i1.d = Cs2i.d by A10,A17,A272,SCMFSA_2:75;
hence (Cs1i1|dom DPp).x = (Cs2i1|dom DPp).x by A32,A51,A276,A277;
end;
suppose
A278: f = x;
then consider k1 being Nat such that
A279: k1 = |.Cs1i.da.| and
A280: Cs1i1.x = k1 |-> 0 by A49,A271,SCMFSA_2:75;
consider k2 being Nat such that
A281: k2 = |.Cs2i.da.| and
A282: Cs2i1.x = k2 |-> 0 by A10,A17,A272,A278,SCMFSA_2:75;
DPp c= p by RELAT_1:59;
then dom DPp c= dom p by GRFUNC_1:2;
then k2 |-> 0 = k1 |->0 by A1,A7,A32,A271,A274,A276,A278,A279,A281,A4
,SCMFSA_3:16;
hence
(Cs1i1|dom DPp).x = (Cs2i1|dom DPp).x by A32,A44,A276,A280,A282;
end;
suppose
A283: f <> x & x in FinSeq-Locations;
then reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;
A284: Cs1i1.d = Cs1i.d by A49,A271,A283,SCMFSA_2:75;
Cs2i1.d = Cs2i.d by A10,A17,A272,A283,SCMFSA_2:75;
hence (Cs1i1|dom DPp).x = (Cs2i1|dom DPp).x by A32,A51,A276,A284;
end;
end;
then (Cs1i1|dom DPp) c= (Cs2i1|dom DPp) by A32,A43,GRFUNC_1:2;
hence Comput(P1,s1,i+1)|dom (DataPart p)
= Comput(P2,s2,i+1)|dom DataPart p by A32,A43,GRFUNC_1:3;
now
let x be object;
assume
A285: x in dom (DataPart Cs3i1);
per cases by A22,A285,SCMFSA_2:100,XBOOLE_0:def 3;
suppose
x in Int-Locations;
then reconsider f = x as Int-Location by AMI_2:def 16;
A286: Cs3i1.f = Cs3i.f by A42,A271,SCMFSA_2:75;
Cs2i1.f = Cs2i.f by A10,A17,A272,SCMFSA_2:75;
hence (DataPart Cs3i1).x = (DataPart Cs2i1).x by A38,A285,A286;
end;
suppose
A287: f = x;
then
A288: ex k1 being Nat st k1 = |.Cs3i.da.| & Cs3i1. x =
k1 |-> 0 by A42,A271,SCMFSA_2:75;
ex k2 being Nat st k2 = |.Cs2i.da.| & Cs2i1. x =
k2 |-> 0 by A10,A17,A272,A287,SCMFSA_2:75;
hence (DataPart Cs3i1).x = (DataPart Cs2i1).x by A34,A274,A285,A288;
end;
suppose
A289: f <> x & x in FinSeq-Locations;
then reconsider d = x as FinSeq-Location by SCMFSA_2:def 5;
A290: Cs3i1.d = Cs3i.d by A42,A271,A289,SCMFSA_2:75;
Cs2i1.d = Cs2i.d by A10,A17,A272,A289,SCMFSA_2:75;
hence (DataPart Cs3i1).x = (DataPart Cs2i1).x by A38,A285,A290;
end;
end;
then DataPart Cs3i1 c= DataPart Comput(P2,s2,i+1) by A22,A33,GRFUNC_1:2;
hence thesis by A22,A33,GRFUNC_1:3;
end;
end;
reconsider ii = IC p as Nat;
A291: IC SCM+FSA in dom IncIC( p,k) by MEMSTR_0:52;
now
thus IC Comput(P1,s1,0) + k = IC s1 + k
.= IC p + k by A1,A3,GRFUNC_1:2
.= IC p + k
.= IC IncIC( p,k) by MEMSTR_0:53
.= IC s2 by A2,A291,GRFUNC_1:2
.= IC Comput(P2,s2,0);
reconsider loc = IC p as Nat;
A292: IC p = IC s1 by A1,A3,GRFUNC_1:2;
then IC p = IC Comput(P1,s1,0);
then
A293: loc in dom q by A6,A1,AMISTD_5:def 4;
A294: (IC p) + k in dom Reloc(q,k) by A293,COMPOS_1:46;
A295: IC SCM+FSA in dom IncIC( p,k) by MEMSTR_0:52;
A296: (q).IC p = P1.IC s1 by A292,A293,A4,GRFUNC_1:2;
dom P2 = NAT by PARTFUN1:def 2;
then
A297: CurInstr(P2,Comput(P2,s2,0))
= P2.IC Comput(P2,s2,0) by PARTFUN1:def 6
.= P2.IC s2
.= P2.(IC IncIC( p,k)) by A2,A295,GRFUNC_1:2
.= P2.((IC p) +k) by MEMSTR_0:53
.= P2.((IC p) +k)
.= (Reloc(q, k)).((IC p) +k) by A294,A4,GRFUNC_1:2;
A298: dom P1 = NAT by PARTFUN1:def 2;
CurInstr(P1,Comput(P1,s1,0))
= CurInstr(P1,s1)
.= P1.IC s1 by A298,PARTFUN1:def 6;
hence
IncAddr(CurInstr(P1,Comput(P1,s1,0)), k)
= CurInstr(P2,Comput(P2,s2,0)) by A297,A293,A296,COMPOS_1:35;
A299: DataPart p c= p by RELAT_1:59;
A300: DataPart p c= s1 by A1,A299,XBOOLE_1:1;
A301: DataPart IncIC(p,k) = DataPart p by MEMSTR_0:51;
DataPart p c= IncIC(p,k) by A301,MEMSTR_0:12;
then
A302: DataPart p c= s2 by A2,XBOOLE_1:1;
thus Comput(P1,s1,0)|dom (DataPart p) = s1 | dom (DataPart p)
.= DataPart p by A300,GRFUNC_1:23
.= s2 | dom (DataPart p) by A302,GRFUNC_1:23
.= Comput(P2,s2,0)|dom DataPart p;
thus DataPart Comput(P1,s3,0) = DataPart(s1 +* DataPart s2)
.= DataPart s2 by PBOOLE:142
.= DataPart Comput(P2,s2,0);
end;
then
A303: Y[0];
thus for i being Nat holds Y[i] from NAT_1:sch 2(A303,A8);
end;
registration
cluster SCM+FSA -> relocable1 relocable2;
coherence
by Th1;
end;