let k be Nat; :: thesis: for q being NAT -defined the InstructionsF of SCM -valued finite non halt-free Function
for p being non empty b1 -autonomic FinPartState of SCM
for s1, s2 being State of SCM st p c= s1 & IncIC (p,k) c= s2 holds
for P1, P2 being Instruction-Sequence of SCM 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))) & (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)) )
let q be NAT -defined the InstructionsF of SCM -valued finite non halt-free Function; :: thesis: for p being non empty q -autonomic FinPartState of SCM
for s1, s2 being State of SCM st p c= s1 & IncIC (p,k) c= s2 holds
for P1, P2 being Instruction-Sequence of SCM 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))) & (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)) )
let p be non empty q -autonomic FinPartState of SCM; :: thesis: for s1, s2 being State of SCM st p c= s1 & IncIC (p,k) c= s2 holds
for P1, P2 being Instruction-Sequence of SCM 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))) & (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)) )
let s1, s2 be State of SCM; :: thesis: ( p c= s1 & IncIC (p,k) c= s2 implies for P1, P2 being Instruction-Sequence of SCM 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))) & (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)) ) )
assume that
A1: p c= s1 and
A2: IncIC (p,k) c= s2 ; :: thesis: for P1, P2 being Instruction-Sequence of SCM 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))) & (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)) )
A3: IC in dom p by AMISTD_5:6;
A4: p c= s1 by A1;
let P1, P2 be Instruction-Sequence of SCM; :: thesis: ( q c= P1 & Reloc (q,k) c= P2 implies 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)) ) )
assume A5: ( q c= P1 & Reloc (q,k) c= P2 ) ; :: thesis: 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)) )
A6: Reloc (q,k) c= P2 by A5;
A7: q c= P1 by A5;
set s3 = s1 +* (DataPart s2);
defpred S1[ 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,(s1 +* (DataPart s2)),$1)) = DataPart (Comput (P2,s2,$1)) );
A8: p c= s1 +* (DataPart s2) by A1, A2, MEMSTR_0:61;
A9: for i being Nat st S1[i] holds
S1[i + 1]
proof
set DPp = DataPart p;
let i be Nat; :: thesis: ( S1[i] implies S1[i + 1] )
assume that
A10: (IC (Comput (P1,s1,i))) + k = IC (Comput (P2,s2,i)) and
A11: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = CurInstr (P2,(Comput (P2,s2,i))) and
A12: (Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart p)) and
A13: DataPart (Comput (P1,(s1 +* (DataPart s2)),i)) = DataPart (Comput (P2,s2,i)) ; :: thesis: S1[i + 1]
set Cs2i1 = Comput (P2,s2,(i + 1));
set Cs3i = Comput (P1,(s1 +* (DataPart s2)),i);
set Cs2i = Comput (P2,s2,i);
dom (Comput (P2,s2,(i + 1))) = the carrier of SCM by PARTFUN1:def 2;
then A14: dom (Comput (P2,s2,(i + 1))) = {(IC )} \/ (Data-Locations ) by STRUCT_0:4;
set Cs3i1 = Comput (P1,(s1 +* (DataPart s2)),(i + 1));
A15: dom (DataPart (Comput (P2,s2,i))) = Data-Locations by MEMSTR_0:9;
A16: dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) = Data-Locations by MEMSTR_0:9;
A17: dom (DataPart (Comput (P2,s2,(i + 1)))) = Data-Locations by MEMSTR_0:9;
A18: now :: thesis: for x being set st x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) & (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = (Comput (P2,s2,(i + 1))) . x holds
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
let x be set ; :: thesis: ( x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) & (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = (Comput (P2,s2,(i + 1))) . x implies (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x )
assume that
A19: x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) and
A20: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = (Comput (P2,s2,(i + 1))) . x ; :: thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
thus (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (Comput (P2,s2,(i + 1))) . x by A19, A20, FUNCT_1:47
.= (DataPart (Comput (P2,s2,(i + 1)))) . x by A16, A17, A19, FUNCT_1:47 ; :: thesis: verum
end;
A21: dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),i))) = Data-Locations by MEMSTR_0:9;
A22: now :: thesis: for x being set st x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) & (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = (Comput (P1,(s1 +* (DataPart s2)),i)) . x & (Comput (P2,s2,(i + 1))) . x = (Comput (P2,s2,i)) . x holds
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
let x be set ; :: thesis: ( x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) & (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = (Comput (P1,(s1 +* (DataPart s2)),i)) . x & (Comput (P2,s2,(i + 1))) . x = (Comput (P2,s2,i)) . x implies (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x )
assume that
A23: x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) and
A24: ( (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = (Comput (P1,(s1 +* (DataPart s2)),i)) . x & (Comput (P2,s2,(i + 1))) . x = (Comput (P2,s2,i)) . x ) ; :: thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
(DataPart (Comput (P1,(s1 +* (DataPart s2)),i))) . x = (Comput (P1,(s1 +* (DataPart s2)),i)) . x by A21, A16, A23, FUNCT_1:47;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A13, A15, A16, A18, A23, A24, FUNCT_1:47; :: thesis: verum
end;
A25: now :: thesis: for s being State of SCM
for d being Data-Location holds d in dom (DataPart s)
let s be State of SCM; :: thesis: for d being Data-Location holds d in dom (DataPart s)
let d be Data-Location; :: thesis: d in dom (DataPart s)
d in Data-Locations by AMI_2:def 16, AMI_3:27;
hence d in dom (DataPart s) by MEMSTR_0:9; :: thesis: verum
end;
A26: now :: thesis: for d being Data-Location holds (Comput (P1,(s1 +* (DataPart s2)),i)) . d = (Comput (P2,s2,i)) . d
let d be Data-Location; :: thesis: (Comput (P1,(s1 +* (DataPart s2)),i)) . d = (Comput (P2,s2,i)) . d
A27: d in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),i))) by A25;
hence (Comput (P1,(s1 +* (DataPart s2)),i)) . d = (DataPart (Comput (P1,(s1 +* (DataPart s2)),i))) . d by FUNCT_1:47
.= (Comput (P2,s2,i)) . d by A13, A27, FUNCT_1:47 ;
:: thesis: verum
end;
set Cs1i1 = Comput (P1,s1,(i + 1));
set Cs1i = Comput (P1,s1,i);
dom (Comput (P1,s1,(i + 1))) = the carrier of SCM by PARTFUN1:def 2;
then A28: dom (Comput (P1,s1,(i + 1))) = {(IC )} \/ (Data-Locations ) by STRUCT_0:4;
dom (DataPart p) = (dom p) /\ (Data-Locations ) by RELAT_1:61;
then A29: dom (DataPart p) c= {(IC )} \/ (Data-Locations ) by XBOOLE_1:10, XBOOLE_1:17;
A30: dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) = (dom (Comput (P1,s1,(i + 1)))) /\ (dom (DataPart p)) by RELAT_1:61
.= dom (DataPart p) by A28, A29, XBOOLE_1:28 ;
A31: now :: thesis: ( (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) implies IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) )
reconsider loc = IC (Comput (P1,s1,(i + 1))) as Element of NAT ;
assume A32: (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) ; :: thesis: IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1))))
reconsider kk = loc as Element of NAT ;
A33: loc in dom q by A7, A4, AMISTD_5:def 4;
A34: loc + k in dom (Reloc (q,k)) by A33, COMPOS_1:46;
A35: dom P2 = NAT by PARTFUN1:def 2;
dom P1 = NAT by PARTFUN1:def 2;
then CurInstr (P1,(Comput (P1,s1,(i + 1)))) = P1 . loc by PARTFUN1:def 6
.= q . loc by A33, A5, GRFUNC_1:2
.= q . loc ;
hence IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = (Reloc (q,k)) . (loc + k) by A33, COMPOS_1:35
.= P2 . (IC (Comput (P2,s2,(i + 1)))) by A32, A34, A6, GRFUNC_1:2
.= CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A35, PARTFUN1:def 6 ;
:: thesis: verum
end;
set I = CurInstr (P1,(Comput (P1,s1,i)));
A36: Comput (P2,s2,(i + 1)) = Following (P2,(Comput (P2,s2,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P2,s2,i))) ;
dom (Comput (P2,s2,i)) = the carrier of SCM by PARTFUN1:def 2;
then A37: dom (Comput (P2,s2,i)) = {(IC )} \/ (Data-Locations ) by STRUCT_0:4;
dom (Comput (P1,s1,i)) = the carrier of SCM by PARTFUN1:def 2;
then A38: dom (Comput (P1,s1,i)) = {(IC )} \/ (Data-Locations ) by STRUCT_0:4;
A39: dom ((Comput (P1,s1,i)) | (dom (DataPart p))) = (dom (Comput (P1,s1,i))) /\ (dom (DataPart p)) by RELAT_1:61
.= dom (DataPart p) by A38, A29, XBOOLE_1:28 ;
A40: Comput (P1,(s1 +* (DataPart s2)),(i + 1)) = Following (P1,(Comput (P1,(s1 +* (DataPart s2)),i))) by EXTPRO_1:3
.= Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,(s1 +* (DataPart s2)),i))) by A1, A8, A5, AMISTD_5:7 ;
A41: dom ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) = (dom (Comput (P2,s2,(i + 1)))) /\ (dom (DataPart p)) by RELAT_1:61
.= dom (DataPart p) by A14, A29, XBOOLE_1:28 ;
A42: now :: thesis: for x being set
for d being Data-Location st d = x & d in dom (DataPart p) & (Comput (P1,s1,(i + 1))) . d = (Comput (P2,s2,(i + 1))) . d holds
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
let x be set ; :: thesis: for d being Data-Location st d = x & d in dom (DataPart p) & (Comput (P1,s1,(i + 1))) . d = (Comput (P2,s2,(i + 1))) . d holds
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
let d be Data-Location; :: thesis: ( d = x & d in dom (DataPart p) & (Comput (P1,s1,(i + 1))) . d = (Comput (P2,s2,(i + 1))) . d implies ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x )
assume that
A43: ( d = x & d in dom (DataPart p) ) and
A44: (Comput (P1,s1,(i + 1))) . d = (Comput (P2,s2,(i + 1))) . d ; :: thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
thus ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = (Comput (P2,s2,(i + 1))) . d by A30, A43, A44, FUNCT_1:47
.= ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A41, A43, FUNCT_1:47 ; :: thesis: verum
end;
A45: dom ((Comput (P2,s2,i)) | (dom (DataPart p))) = (dom (Comput (P2,s2,i))) /\ (dom (DataPart p)) by RELAT_1:61
.= dom (DataPart p) by A37, A29, XBOOLE_1:28 ;
A46: now :: thesis: for x being set
for d being Data-Location st d = x & d in dom (DataPart p) & (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d holds
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
let x be set ; :: thesis: for d being Data-Location st d = x & d in dom (DataPart p) & (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d holds
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
let d be Data-Location; :: thesis: ( d = x & d in dom (DataPart p) & (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d implies ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x )
assume that
A47: d = x and
A48: d in dom (DataPart p) and
A49: ( (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d ) ; :: thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
( ((Comput (P1,s1,i)) | (dom (DataPart p))) . d = (Comput (P1,s1,i)) . d & ((Comput (P2,s2,i)) | (dom (DataPart p))) . d = (Comput (P2,s2,i)) . d ) by A39, A45, A48, FUNCT_1:47;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = (Comput (P2,s2,(i + 1))) . d by A12, A30, A47, A48, A49, FUNCT_1:47
.= ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A41, A47, A48, FUNCT_1:47 ;
:: thesis: verum
end;
reconsider j = IC (Comput (P1,s1,i)) as Element of NAT ;
A50: Comput (P1,s1,(i + 1)) = Following (P1,(Comput (P1,s1,i))) by EXTPRO_1:3
.= Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i))) ;
A51: ((IC (Comput (P1,s1,i))) + k) + 1 = (j + k) + 1
.= (j + 1) + k ;
not not InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 0 & ... & not InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 8 by AMI_5:5;
per cases then ( InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 0 or InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 1 or InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 2 or InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 3 or InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 4 or InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 5 or InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 6 or InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 7 or InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 8 ) ;
suppose InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 0 ; :: thesis: S1[i + 1]
then A52: CurInstr (P1,(Comput (P1,s1,i))) = halt SCM by AMI_5:7;
thus (IC (Comput (P1,s1,(i + 1)))) + k = (IC (Comput (P1,s1,i))) + k by A50, A52, EXTPRO_1:def 3
.= IC (Comput (P2,s2,(i + 1))) by A10, A36, A52, A11, EXTPRO_1:def 3 ; :: thesis: ( IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) & (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) )
hence IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A31; :: thesis: ( (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) )
A53: Comput (P2,s2,(i + 1)) = Comput (P2,s2,i) by A36, A52, A11, EXTPRO_1:def 3;
hence (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A12, A50, A52, EXTPRO_1:def 3; :: thesis: DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1)))
thus DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) by A13, A40, A52, A53, EXTPRO_1:def 3; :: thesis: verum
end;
suppose InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 1 ; :: thesis: S1[i + 1]
then consider da, db being Data-Location such that
A54: CurInstr (P1,(Comput (P1,s1,i))) = da := db by AMI_5:8;
A55: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = da := db by A54, COMPOS_0:4;
A56: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = (IC (Comput (P1,s1,i))) + 1 by A54, AMI_3:2;
hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A10, A11, A50, A36, A51, A55, AMI_3:2; :: thesis: ( IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) & (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) )
thus IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A10, A11, A31, A50, A36, A51, A55, A56, AMI_3:2; :: thesis: ( (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) )
A57: (Comput (P1,(s1 +* (DataPart s2)),i)) . db = (Comput (P2,s2,i)) . db by A26;
now :: thesis: for x being object st x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) holds
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
DataPart p c= p by RELAT_1:59;
then A58: dom (DataPart p) c= dom p by GRFUNC_1:2;
let x be object ; :: thesis: ( x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) implies ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1 )
assume A59: x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) ; :: thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1
dom (DataPart p) c= Data-Locations by RELAT_1:58;
then x in Data-Locations by A30, A59;
then reconsider d = x as Data-Location by AMI_2:def 16, AMI_3:27;
per cases ( da = d or da <> d ) ;
suppose A60: da = d ; :: thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1
then ( (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . db & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . db ) by A11, A50, A36, A54, A55, AMI_3:2;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A1, A8, A30, A42, A54, A57, A59, A58, A60, A5, AMI_5:17; :: thesis: verum
end;
suppose da <> d ; :: thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1
then ( (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d ) by A11, A50, A36, A54, A55, AMI_3:2;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A30, A46, A59; :: thesis: verum
end;
end;
end;
then (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A30, A41, GRFUNC_1:2;
hence (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A30, A41, GRFUNC_1:3; :: thesis: DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1)))
now :: thesis: for x being object st x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) holds
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
let x be object ; :: thesis: ( x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) implies (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 )
assume A61: x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) ; :: thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1
then reconsider d = x as Data-Location by A16, AMI_2:def 16, AMI_3:27;
per cases ( da = d or da <> d ) ;
suppose da = d ; :: thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1
then ( (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . db & (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . db ) by A11, A36, A40, A54, A55, AMI_3:2;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A26, A18, A61; :: thesis: verum
end;
suppose da <> d ; :: thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1
then ( (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d ) by A11, A36, A40, A54, A55, AMI_3:2;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A22, A61; :: thesis: verum
end;
end;
end;
then DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1))) by A16, A17, GRFUNC_1:2;
hence DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) by A16, A17, GRFUNC_1:3; :: thesis: verum
end;
suppose InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 2 ; :: thesis: S1[i + 1]
then consider da, db being Data-Location such that
A62: CurInstr (P1,(Comput (P1,s1,i))) = AddTo (da,db) by AMI_5:9;
A63: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = AddTo (da,db) by A62, COMPOS_0:4;
A64: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = (IC (Comput (P1,s1,i))) + 1 by A62, AMI_3:3;
hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A10, A11, A50, A36, A51, A63, AMI_3:3; :: thesis: ( IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) & (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) )
thus IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A10, A11, A31, A50, A36, A51, A63, A64, AMI_3:3; :: thesis: ( (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) )
A65: ( (Comput (P1,(s1 +* (DataPart s2)),i)) . da = (Comput (P2,s2,i)) . da & (Comput (P1,(s1 +* (DataPart s2)),i)) . db = (Comput (P2,s2,i)) . db ) by A26;
now :: thesis: for x being object st x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) holds
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
DataPart p c= p by RELAT_1:59;
then A66: dom (DataPart p) c= dom p by GRFUNC_1:2;
let x be object ; :: thesis: ( x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) implies ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1 )
assume A67: x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) ; :: thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1
dom (DataPart p) c= Data-Locations by RELAT_1:58;
then x in Data-Locations by A30, A67;
then reconsider d = x as Data-Location by AMI_2:def 16, AMI_3:27;
per cases ( da = d or da <> d ) ;
suppose A68: da = d ; :: thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1
then ( (Comput (P1,s1,(i + 1))) . d = ((Comput (P1,s1,i)) . da) + ((Comput (P1,s1,i)) . db) & (Comput (P2,s2,(i + 1))) . d = ((Comput (P2,s2,i)) . da) + ((Comput (P2,s2,i)) . db) ) by A11, A50, A36, A62, A63, AMI_3:3;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A1, A8, A30, A42, A62, A65, A67, A66, A68, A5, AMI_5:18; :: thesis: verum
end;
suppose da <> d ; :: thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1
then ( (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d ) by A11, A50, A36, A62, A63, AMI_3:3;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A30, A46, A67; :: thesis: verum
end;
end;
end;
then (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A30, A41, GRFUNC_1:2;
hence (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A30, A41, GRFUNC_1:3; :: thesis: DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1)))
now :: thesis: for x being object st x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) holds
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
let x be object ; :: thesis: ( x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) implies (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 )
assume A69: x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) ; :: thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1
then reconsider d = x as Data-Location by A16, AMI_2:def 16, AMI_3:27;
per cases ( da = d or da <> d ) ;
suppose da = d ; :: thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1
then ( (Comput (P2,s2,(i + 1))) . d = ((Comput (P2,s2,i)) . da) + ((Comput (P2,s2,i)) . db) & (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = ((Comput (P1,(s1 +* (DataPart s2)),i)) . da) + ((Comput (P1,(s1 +* (DataPart s2)),i)) . db) ) by A11, A36, A40, A62, A63, AMI_3:3;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A18, A65, A69; :: thesis: verum
end;
suppose da <> d ; :: thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1
then ( (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d ) by A11, A36, A40, A62, A63, AMI_3:3;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A22, A69; :: thesis: verum
end;
end;
end;
then DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1))) by A16, A17, GRFUNC_1:2;
hence DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) by A16, A17, GRFUNC_1:3; :: thesis: verum
end;
suppose InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 3 ; :: thesis: S1[i + 1]
then consider da, db being Data-Location such that
A70: CurInstr (P1,(Comput (P1,s1,i))) = SubFrom (da,db) by AMI_5:10;
A71: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = SubFrom (da,db) by A70, COMPOS_0:4;
A72: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = (IC (Comput (P1,s1,i))) + 1 by A70, AMI_3:4;
hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A10, A11, A50, A36, A51, A71, AMI_3:4; :: thesis: ( IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) & (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) )
thus IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A10, A11, A31, A50, A36, A51, A71, A72, AMI_3:4; :: thesis: ( (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) )
A73: ( (Comput (P1,(s1 +* (DataPart s2)),i)) . da = (Comput (P2,s2,i)) . da & (Comput (P1,(s1 +* (DataPart s2)),i)) . db = (Comput (P2,s2,i)) . db ) by A26;
now :: thesis: for x being object st x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) holds
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
DataPart p c= p by RELAT_1:59;
then A74: dom (DataPart p) c= dom p by GRFUNC_1:2;
let x be object ; :: thesis: ( x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) implies ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1 )
assume A75: x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) ; :: thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1
dom (DataPart p) c= Data-Locations by RELAT_1:58;
then x in Data-Locations by A30, A75;
then reconsider d = x as Data-Location by AMI_2:def 16, AMI_3:27;
per cases ( da = d or da <> d ) ;
suppose A76: da = d ; :: thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1
then ( (Comput (P1,s1,(i + 1))) . d = ((Comput (P1,s1,i)) . da) - ((Comput (P1,s1,i)) . db) & (Comput (P2,s2,(i + 1))) . d = ((Comput (P2,s2,i)) . da) - ((Comput (P2,s2,i)) . db) ) by A11, A50, A36, A70, A71, AMI_3:4;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A1, A8, A30, A42, A70, A73, A75, A74, A76, A5, AMI_5:19; :: thesis: verum
end;
suppose da <> d ; :: thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1
then ( (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d ) by A11, A50, A36, A70, A71, AMI_3:4;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A30, A46, A75; :: thesis: verum
end;
end;
end;
then (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A30, A41, GRFUNC_1:2;
hence (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A30, A41, GRFUNC_1:3; :: thesis: DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1)))
now :: thesis: for x being object st x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) holds
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
let x be object ; :: thesis: ( x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) implies (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 )
assume A77: x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) ; :: thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1
then reconsider d = x as Data-Location by A16, AMI_2:def 16, AMI_3:27;
per cases ( da = d or da <> d ) ;
suppose da = d ; :: thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1
then ( (Comput (P2,s2,(i + 1))) . d = ((Comput (P2,s2,i)) . da) - ((Comput (P2,s2,i)) . db) & (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = ((Comput (P1,(s1 +* (DataPart s2)),i)) . da) - ((Comput (P1,(s1 +* (DataPart s2)),i)) . db) ) by A11, A36, A40, A70, A71, AMI_3:4;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A18, A73, A77; :: thesis: verum
end;
suppose da <> d ; :: thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1
then ( (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d ) by A11, A36, A40, A70, A71, AMI_3:4;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A22, A77; :: thesis: verum
end;
end;
end;
then DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1))) by A16, A17, GRFUNC_1:2;
hence DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) by A16, A17, GRFUNC_1:3; :: thesis: verum
end;
suppose InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 4 ; :: thesis: S1[i + 1]
then consider da, db being Data-Location such that
A78: CurInstr (P1,(Comput (P1,s1,i))) = MultBy (da,db) by AMI_5:11;
A79: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = MultBy (da,db) by A78, COMPOS_0:4;
A80: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = (IC (Comput (P1,s1,i))) + 1 by A78, AMI_3:5;
hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A10, A11, A50, A36, A51, A79, AMI_3:5; :: thesis: ( IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) & (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) )
thus IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A10, A11, A31, A50, A36, A51, A79, A80, AMI_3:5; :: thesis: ( (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) )
A81: ( (Comput (P1,(s1 +* (DataPart s2)),i)) . da = (Comput (P2,s2,i)) . da & (Comput (P1,(s1 +* (DataPart s2)),i)) . db = (Comput (P2,s2,i)) . db ) by A26;
now :: thesis: for x being object st x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) holds
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
DataPart p c= p by RELAT_1:59;
then A82: dom (DataPart p) c= dom p by GRFUNC_1:2;
let x be object ; :: thesis: ( x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) implies ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1 )
assume A83: x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) ; :: thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1
dom (DataPart p) c= Data-Locations by RELAT_1:58;
then x in Data-Locations by A30, A83;
then reconsider d = x as Data-Location by AMI_2:def 16, AMI_3:27;
per cases ( da = d or da <> d ) ;
suppose A84: da = d ; :: thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1
then ( (Comput (P1,s1,(i + 1))) . d = ((Comput (P1,s1,i)) . da) * ((Comput (P1,s1,i)) . db) & (Comput (P2,s2,(i + 1))) . d = ((Comput (P2,s2,i)) . da) * ((Comput (P2,s2,i)) . db) ) by A11, A50, A36, A78, A79, AMI_3:5;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A1, A8, A30, A42, A78, A81, A83, A82, A84, A5, AMI_5:20; :: thesis: verum
end;
suppose da <> d ; :: thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1
then ( (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d ) by A11, A50, A36, A78, A79, AMI_3:5;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A30, A46, A83; :: thesis: verum
end;
end;
end;
then (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A30, A41, GRFUNC_1:2;
hence (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A30, A41, GRFUNC_1:3; :: thesis: DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1)))
now :: thesis: for x being object st x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) holds
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
let x be object ; :: thesis: ( x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) implies (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 )
assume A85: x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) ; :: thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1
then reconsider d = x as Data-Location by A16, AMI_2:def 16, AMI_3:27;
per cases ( da = d or da <> d ) ;
suppose da = d ; :: thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1
then ( (Comput (P2,s2,(i + 1))) . d = ((Comput (P2,s2,i)) . da) * ((Comput (P2,s2,i)) . db) & (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = ((Comput (P1,(s1 +* (DataPart s2)),i)) . da) * ((Comput (P1,(s1 +* (DataPart s2)),i)) . db) ) by A11, A36, A40, A78, A79, AMI_3:5;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A18, A81, A85; :: thesis: verum
end;
suppose da <> d ; :: thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1
then ( (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d ) by A11, A36, A40, A78, A79, AMI_3:5;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A22, A85; :: thesis: verum
end;
end;
end;
then DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1))) by A16, A17, GRFUNC_1:2;
hence DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) by A16, A17, GRFUNC_1:3; :: thesis: verum
end;
suppose InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 5 ; :: thesis: S1[i + 1]
then consider da, db being Data-Location such that
A86: CurInstr (P1,(Comput (P1,s1,i))) = Divide (da,db) by AMI_5:12;
A87: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = Divide (da,db) by A86, COMPOS_0:4;
A88: ( (Comput (P1,(s1 +* (DataPart s2)),i)) . da = (Comput (P2,s2,i)) . da & (Comput (P1,(s1 +* (DataPart s2)),i)) . db = (Comput (P2,s2,i)) . db ) by A26;
per cases ( da <> db or da = db ) ;
suppose A89: da <> db ; :: thesis: S1[i + 1]
A90: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = (IC (Comput (P1,s1,i))) + 1 by A86, AMI_3:6;
hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A10, A11, A50, A36, A51, A87, AMI_3:6; :: thesis: ( IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) & (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) )
thus IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A10, A11, A31, A50, A36, A51, A87, A90, AMI_3:6; :: thesis: ( (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) )
now :: thesis: for x being object st x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) holds
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
DataPart p c= p by RELAT_1:59;
then A91: dom (DataPart p) c= dom p by GRFUNC_1:2;
let x be object ; :: thesis: ( x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) implies ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1 )
assume A92: x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) ; :: thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1
dom (DataPart p) c= Data-Locations by RELAT_1:58;
then x in Data-Locations by A30, A92;
then reconsider d = x as Data-Location by AMI_2:def 16, AMI_3:27;
per cases ( da = d or db = d or ( da <> d & db <> d ) ) ;
suppose A93: da = d ; :: thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1
then A94: ( (Comput (P1,s1,(i + 1))) . d = ((Comput (P1,s1,i)) . da) div ((Comput (P1,s1,i)) . db) & (Comput (P2,s2,(i + 1))) . d = ((Comput (P2,s2,i)) . da) div ((Comput (P2,s2,i)) . db) ) by A11, A50, A36, A86, A87, A89, AMI_3:6;
((Comput (P1,(s1 +* (DataPart s2)),i)) . da) div ((Comput (P1,(s1 +* (DataPart s2)),i)) . db) = ((Comput (P1,s1,i)) . da) div ((Comput (P1,s1,i)) . db) by A1, A8, A30, A86, A89, A92, A91, A93, A5, AMI_5:21;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = (Comput (P2,s2,(i + 1))) . d by A88, A92, A94, FUNCT_1:47
.= ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A30, A41, A92, FUNCT_1:47 ;
:: thesis: verum
end;
suppose A95: db = d ; :: thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1
then ( (Comput (P1,s1,(i + 1))) . d = ((Comput (P1,s1,i)) . da) mod ((Comput (P1,s1,i)) . db) & (Comput (P2,s2,(i + 1))) . d = ((Comput (P2,s2,i)) . da) mod ((Comput (P2,s2,i)) . db) ) by A11, A50, A36, A86, A87, AMI_3:6;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A1, A8, A30, A42, A86, A88, A92, A91, A95, A5, AMI_5:22; :: thesis: verum
end;
suppose ( da <> d & db <> d ) ; :: thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1
then ( (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d ) by A11, A50, A36, A86, A87, AMI_3:6;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A30, A46, A92; :: thesis: verum
end;
end;
end;
then (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A30, A41, GRFUNC_1:2;
hence (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A30, A41, GRFUNC_1:3; :: thesis: DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1)))
now :: thesis: for x being object st x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) holds
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
let x be object ; :: thesis: ( x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) implies (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 )
assume A96: x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) ; :: thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1
then reconsider d = x as Data-Location by A16, AMI_2:def 16, AMI_3:27;
per cases ( da = d or db = d or ( da <> d & db <> d ) ) ;
suppose da = d ; :: thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1
then ( (Comput (P2,s2,(i + 1))) . d = ((Comput (P2,s2,i)) . da) div ((Comput (P2,s2,i)) . db) & (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = ((Comput (P1,(s1 +* (DataPart s2)),i)) . da) div ((Comput (P1,(s1 +* (DataPart s2)),i)) . db) ) by A11, A36, A40, A86, A87, A89, AMI_3:6;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A18, A88, A96; :: thesis: verum
end;
suppose db = d ; :: thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1
then ( (Comput (P2,s2,(i + 1))) . d = ((Comput (P2,s2,i)) . da) mod ((Comput (P2,s2,i)) . db) & (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = ((Comput (P1,(s1 +* (DataPart s2)),i)) . da) mod ((Comput (P1,(s1 +* (DataPart s2)),i)) . db) ) by A11, A36, A40, A86, A87, AMI_3:6;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A18, A88, A96; :: thesis: verum
end;
suppose ( da <> d & db <> d ) ; :: thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1
then ( (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d ) by A11, A36, A40, A86, A87, AMI_3:6;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A22, A96; :: thesis: verum
end;
end;
end;
then DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1))) by A16, A17, GRFUNC_1:2;
hence DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) by A16, A17, GRFUNC_1:3; :: thesis: verum
end;
suppose A97: da = db ; :: thesis: S1[i + 1]
A98: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = (IC (Comput (P1,s1,i))) + 1 by A86, AMI_3:6;
hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A10, A11, A50, A36, A51, A87, AMI_3:6; :: thesis: ( IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) & (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) )
thus IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A10, A11, A31, A50, A36, A51, A87, A98, AMI_3:6; :: thesis: ( (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) )
now :: thesis: for x being object st x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) holds
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
let x be object ; :: thesis: ( x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) implies ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1 )
assume A99: x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) ; :: thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1
dom (DataPart p) c= Data-Locations by RELAT_1:58;
then x in Data-Locations by A30, A99;
then reconsider d = x as Data-Location by AMI_2:def 16, AMI_3:27;
per cases ( da = d or da <> d ) ;
suppose A100: da = d ; :: thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1
A101: ( ((Comput (P1,s1,i)) | (dom (DataPart p))) . d = (Comput (P1,s1,i)) . d & ((Comput (P2,s2,i)) | (dom (DataPart p))) . d = (Comput (P2,s2,i)) . d ) by A30, A39, A45, A99, FUNCT_1:47;
A102: ( ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . d = (Comput (P1,s1,(i + 1))) . d & ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . d = (Comput (P2,s2,(i + 1))) . d ) by A30, A41, A99, FUNCT_1:47;
(Comput (P2,s2,(i + 1))) . d = ((Comput (P2,s2,i)) . da) mod ((Comput (P2,s2,i)) . db) by A11, A36, A87, A97, A100, AMI_3:6;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A12, A50, A86, A97, A100, A101, A102, AMI_3:6; :: thesis: verum
end;
suppose da <> d ; :: thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1
then ( (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d ) by A11, A50, A36, A86, A87, A97, AMI_3:6;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A30, A46, A99; :: thesis: verum
end;
end;
end;
then (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A30, A41, GRFUNC_1:2;
hence (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A30, A41, GRFUNC_1:3; :: thesis: DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1)))
now :: thesis: for x being object st x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) holds
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
let x be object ; :: thesis: ( x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) implies (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 )
assume A103: x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) ; :: thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1
then reconsider d = x as Data-Location by A16, AMI_2:def 16, AMI_3:27;
per cases ( da = d or da <> d ) ;
suppose da = d ; :: thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1
then ( (Comput (P2,s2,(i + 1))) . d = ((Comput (P2,s2,i)) . da) mod ((Comput (P2,s2,i)) . db) & (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = ((Comput (P1,(s1 +* (DataPart s2)),i)) . da) mod ((Comput (P1,(s1 +* (DataPart s2)),i)) . db) ) by A11, A36, A40, A86, A87, A97, AMI_3:6;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A18, A88, A103; :: thesis: verum
end;
suppose da <> d ; :: thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1
then ( (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d ) by A11, A36, A40, A86, A87, A97, AMI_3:6;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A22, A103; :: thesis: verum
end;
end;
end;
then DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1))) by A16, A17, GRFUNC_1:2;
hence DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) by A16, A17, GRFUNC_1:3; :: thesis: verum
end;
end;
end;
suppose InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 6 ; :: thesis: S1[i + 1]
then consider loc being Nat such that
A104: CurInstr (P1,(Comput (P1,s1,i))) = SCM-goto loc by AMI_5:13;
A105: CurInstr (P2,(Comput (P2,s2,i))) = SCM-goto (loc + k) by A11, A104, Th1;
thus (IC (Comput (P1,s1,(i + 1)))) + k = loc + k by A50, A104, AMI_3:7
.= IC (Comput (P2,s2,(i + 1))) by A36, A105, AMI_3:7 ; :: thesis: ( IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) & (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) )
hence IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A31; :: thesis: ( (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) )
now :: thesis: for x being object st x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) holds
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
let x be object ; :: thesis: ( x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) implies ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x )
assume A106: x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) ; :: thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
dom (DataPart p) c= Data-Locations by RELAT_1:58;
then x in Data-Locations by A30, A106;
then reconsider d = x as Data-Location by AMI_2:def 16, AMI_3:27;
( (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d ) by A50, A36, A104, A105, AMI_3:7;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A30, A46, A106; :: thesis: verum
end;
then (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A30, A41, GRFUNC_1:2;
hence (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A30, A41, GRFUNC_1:3; :: thesis: DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1)))
now :: thesis: for x being object st x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) holds
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
let x be object ; :: thesis: ( x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) implies (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x )
assume A107: x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) ; :: thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
then reconsider d = x as Data-Location by A16, AMI_2:def 16, AMI_3:27;
( (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d ) by A36, A40, A104, A105, AMI_3:7;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A22, A107; :: thesis: verum
end;
then DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1))) by A16, A17, GRFUNC_1:2;
hence DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) by A16, A17, GRFUNC_1:3; :: thesis: verum
end;
suppose InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 7 ; :: thesis: S1[i + 1]
then consider loc being Nat, da being Data-Location such that
A108: CurInstr (P1,(Comput (P1,s1,i))) = da =0_goto loc by AMI_5:14;
A109: now :: thesis: ( ( (Comput (P1,s1,i)) . da = 0 & (IC (Comput (P1,s1,(i + 1)))) + k = loc + k ) or ( (Comput (P1,s1,i)) . da <> 0 & (IC (Comput (P1,s1,(i + 1)))) + k = (IC (Comput (P2,s2,i))) + 1 ) )
per cases ( (Comput (P1,s1,i)) . da = 0 or (Comput (P1,s1,i)) . da <> 0 ) ;
case (Comput (P1,s1,i)) . da = 0 ; :: thesis: (IC (Comput (P1,s1,(i + 1)))) + k = loc + k
hence (IC (Comput (P1,s1,(i + 1)))) + k = loc + k by A50, A108, AMI_3:8; :: thesis: verum
end;
case (Comput (P1,s1,i)) . da <> 0 ; :: thesis: (IC (Comput (P1,s1,(i + 1)))) + k = (IC (Comput (P2,s2,i))) + 1
hence (IC (Comput (P1,s1,(i + 1)))) + k = (IC (Comput (P2,s2,i))) + 1 by A10, A50, A51, A108, AMI_3:8; :: thesis: verum
end;
end;
end;
A110: CurInstr (P2,(Comput (P2,s2,i))) = da =0_goto (loc + k) by A11, A108, Th2;
A111: now :: thesis: ( ( (Comput (P2,s2,i)) . da = 0 & IC (Comput (P2,s2,(i + 1))) = loc + k ) or ( (Comput (P2,s2,i)) . da <> 0 & IC (Comput (P2,s2,(i + 1))) = (IC (Comput (P2,s2,i))) + 1 ) )
per cases ( (Comput (P2,s2,i)) . da = 0 or (Comput (P2,s2,i)) . da <> 0 ) ;
case (Comput (P2,s2,i)) . da = 0 ; :: thesis: IC (Comput (P2,s2,(i + 1))) = loc + k
hence IC (Comput (P2,s2,(i + 1))) = loc + k by A36, A110, AMI_3:8; :: thesis: verum
end;
case (Comput (P2,s2,i)) . da <> 0 ; :: thesis: IC (Comput (P2,s2,(i + 1))) = (IC (Comput (P2,s2,i))) + 1
hence IC (Comput (P2,s2,(i + 1))) = (IC (Comput (P2,s2,i))) + 1 by A36, A110, AMI_3:8; :: thesis: verum
end;
end;
end;
A112: (Comput (P1,(s1 +* (DataPart s2)),i)) . da = (Comput (P2,s2,i)) . da by A26;
A113: now :: thesis: (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1)))
per cases ( loc <> (IC (Comput (P1,s1,i))) + 1 or loc = (IC (Comput (P1,s1,i))) + 1 ) ;
suppose loc <> (IC (Comput (P1,s1,i))) + 1 ; :: thesis: (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1)))
hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A1, A8, A108, A112, A109, A111, A5, AMI_5:23; :: thesis: verum
end;
suppose loc = (IC (Comput (P1,s1,i))) + 1 ; :: thesis: (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1)))
hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A10, A109, A111; :: thesis: verum
end;
end;
end;
hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) ; :: thesis: ( IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) & (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) )
thus IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A31, A113; :: thesis: ( (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) )
now :: thesis: for x being object st x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) holds
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
let x be object ; :: thesis: ( x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) implies ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x )
assume A114: x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) ; :: thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
dom (DataPart p) c= Data-Locations by RELAT_1:58;
then x in Data-Locations by A30, A114;
then reconsider d = x as Data-Location by AMI_2:def 16, AMI_3:27;
( (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d ) by A50, A36, A108, A110, AMI_3:8;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A30, A46, A114; :: thesis: verum
end;
then (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A30, A41, GRFUNC_1:2;
hence (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A30, A41, GRFUNC_1:3; :: thesis: DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1)))
now :: thesis: for x being object st x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) holds
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
let x be object ; :: thesis: ( x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) implies (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x )
assume A115: x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) ; :: thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
then reconsider d = x as Data-Location by A16, AMI_2:def 16, AMI_3:27;
( (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d ) by A36, A40, A108, A110, AMI_3:8;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A22, A115; :: thesis: verum
end;
then DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1))) by A16, A17, GRFUNC_1:2;
hence DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) by A16, A17, GRFUNC_1:3; :: thesis: verum
end;
suppose InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 8 ; :: thesis: S1[i + 1]
then consider loc being Nat, da being Data-Location such that
A116: CurInstr (P1,(Comput (P1,s1,i))) = da >0_goto loc by AMI_5:15;
A117: now :: thesis: ( ( (Comput (P1,s1,i)) . da > 0 & (IC (Comput (P1,s1,(i + 1)))) + k = loc + k ) or ( (Comput (P1,s1,i)) . da <= 0 & (IC (Comput (P1,s1,(i + 1)))) + k = (IC (Comput (P2,s2,i))) + 1 ) )
per cases ( (Comput (P1,s1,i)) . da > 0 or (Comput (P1,s1,i)) . da <= 0 ) ;
case (Comput (P1,s1,i)) . da > 0 ; :: thesis: (IC (Comput (P1,s1,(i + 1)))) + k = loc + k
hence (IC (Comput (P1,s1,(i + 1)))) + k = loc + k by A50, A116, AMI_3:9; :: thesis: verum
end;
case (Comput (P1,s1,i)) . da <= 0 ; :: thesis: (IC (Comput (P1,s1,(i + 1)))) + k = (IC (Comput (P2,s2,i))) + 1
hence (IC (Comput (P1,s1,(i + 1)))) + k = (IC (Comput (P2,s2,i))) + 1 by A10, A50, A51, A116, AMI_3:9; :: thesis: verum
end;
end;
end;
A118: CurInstr (P2,(Comput (P2,s2,i))) = da >0_goto (loc + k) by A11, A116, Th3;
A119: now :: thesis: ( ( (Comput (P2,s2,i)) . da > 0 & IC (Comput (P2,s2,(i + 1))) = loc + k ) or ( (Comput (P2,s2,i)) . da <= 0 & IC (Comput (P2,s2,(i + 1))) = (IC (Comput (P2,s2,i))) + 1 ) )
per cases ( (Comput (P2,s2,i)) . da > 0 or (Comput (P2,s2,i)) . da <= 0 ) ;
case (Comput (P2,s2,i)) . da > 0 ; :: thesis: IC (Comput (P2,s2,(i + 1))) = loc + k
hence IC (Comput (P2,s2,(i + 1))) = loc + k by A36, A118, AMI_3:9; :: thesis: verum
end;
case (Comput (P2,s2,i)) . da <= 0 ; :: thesis: IC (Comput (P2,s2,(i + 1))) = (IC (Comput (P2,s2,i))) + 1
hence IC (Comput (P2,s2,(i + 1))) = (IC (Comput (P2,s2,i))) + 1 by A36, A118, AMI_3:9; :: thesis: verum
end;
end;
end;
A120: (Comput (P1,(s1 +* (DataPart s2)),i)) . da = (Comput (P2,s2,i)) . da by A26;
A121: now :: thesis: (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1)))
per cases ( loc <> (IC (Comput (P1,s1,i))) + 1 or loc = (IC (Comput (P1,s1,i))) + 1 ) ;
suppose loc <> (IC (Comput (P1,s1,i))) + 1 ; :: thesis: (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1)))
hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A1, A8, A116, A120, A117, A119, A5, AMI_5:24; :: thesis: verum
end;
suppose loc = (IC (Comput (P1,s1,i))) + 1 ; :: thesis: (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1)))
hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A10, A117, A119; :: thesis: verum
end;
end;
end;
hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) ; :: thesis: ( IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) & (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) )
thus IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A31, A121; :: thesis: ( (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) )
now :: thesis: for x being object st x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) holds
((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
let x be object ; :: thesis: ( x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) implies ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x )
assume A122: x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) ; :: thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x
dom (DataPart p) c= Data-Locations by RELAT_1:58;
then x in Data-Locations by A30, A122;
then reconsider d = x as Data-Location by AMI_2:def 16, AMI_3:27;
( (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d ) by A50, A36, A116, A118, AMI_3:9;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A30, A46, A122; :: thesis: verum
end;
then (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A30, A41, GRFUNC_1:2;
hence (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A30, A41, GRFUNC_1:3; :: thesis: DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1)))
now :: thesis: for x being object st x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) holds
(DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
let x be object ; :: thesis: ( x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) implies (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x )
assume A123: x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) ; :: thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x
then reconsider d = x as Data-Location by A16, AMI_2:def 16, AMI_3:27;
( (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d ) by A36, A40, A116, A118, AMI_3:9;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A22, A123; :: thesis: verum
end;
then DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1))) by A16, A17, GRFUNC_1:2;
hence DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) by A16, A17, GRFUNC_1:3; :: thesis: verum
end;
end;
end;
A124: DataPart p c= p by RELAT_1:59;
A125: IC in dom (IncIC (p,k)) by MEMSTR_0:52;
now :: thesis: ( (IC (Comput (P1,s1,0))) + k = IC (Comput (P2,s2,0)) & IncAddr ((CurInstr (P1,(Comput (P1,s1,0)))),k) = CurInstr (P2,(Comput (P2,s2,0))) & (Comput (P1,s1,0)) | (dom (DataPart p)) = (Comput (P2,s2,0)) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),0)) = DataPart (Comput (P2,s2,0)) )
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, A125, GRFUNC_1:2
.= IC (Comput (P2,s2,0)) ; :: thesis: ( IncAddr ((CurInstr (P1,(Comput (P1,s1,0)))),k) = CurInstr (P2,(Comput (P2,s2,0))) & (Comput (P1,s1,0)) | (dom (DataPart p)) = (Comput (P2,s2,0)) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),0)) = DataPart (Comput (P2,s2,0)) )
reconsider loc = IC p as Element of NAT ;
A126: IC p = IC s1 by A1, A3, GRFUNC_1:2;
then IC p = IC (Comput (P1,s1,0)) ;
then A127: loc in dom q by A7, A4, AMISTD_5:def 4;
A128: (IC p) + k in dom (Reloc (q,k)) by A127, COMPOS_1:46;
A129: IC in dom (IncIC (p,k)) by MEMSTR_0:52;
A130: q . (IC p) = P1 . (IC s1) by A126, A127, A5, GRFUNC_1:2;
dom P2 = NAT by PARTFUN1:def 2;
then A131: 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, A129, GRFUNC_1:2
.= P2 . ((IC p) + k) by MEMSTR_0:53
.= P2 . ((IC p) + k)
.= (Reloc (q,k)) . ((IC p) + k) by A128, A5, GRFUNC_1:2 ;
A132: dom P1 = NAT by PARTFUN1:def 2;
CurInstr (P1,(Comput (P1,s1,0))) = CurInstr (P1,s1)
.= P1 . (IC s1) by A132, PARTFUN1:def 6 ;
hence IncAddr ((CurInstr (P1,(Comput (P1,s1,0)))),k) = CurInstr (P2,(Comput (P2,s2,0))) by A127, A130, A131, COMPOS_1:35; :: thesis: ( (Comput (P1,s1,0)) | (dom (DataPart p)) = (Comput (P2,s2,0)) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),0)) = DataPart (Comput (P2,s2,0)) )
A133: dom (DataPart s2) = Data-Locations by MEMSTR_0:9;
A134: DataPart p c= s1 by A1, A124, XBOOLE_1:1;
A135: DataPart (IncIC (p,k)) = DataPart p by MEMSTR_0:51;
DataPart p c= IncIC (p,k) by A135, MEMSTR_0:12;
then A136: DataPart p c= s2 by A2, XBOOLE_1:1;
thus (Comput (P1,s1,0)) | (dom (DataPart p)) = s1 | (dom (DataPart p))
.= DataPart p by A134, GRFUNC_1:23
.= s2 | (dom (DataPart p)) by A136, GRFUNC_1:23
.= (Comput (P2,s2,0)) | (dom (DataPart p)) ; :: thesis: DataPart (Comput (P1,(s1 +* (DataPart s2)),0)) = DataPart (Comput (P2,s2,0))
thus DataPart (Comput (P1,(s1 +* (DataPart s2)),0)) = DataPart (s1 +* (DataPart s2))
.= DataPart s2 by A133, FUNCT_4:23
.= DataPart (Comput (P2,s2,0)) ; :: thesis: verum
end;
then A137: S1[ 0 ] ;
thus for i being Nat holds S1[i] from NAT_1:sch 2(A137, A9); :: thesis: verum