let k be Element of NAT ; :: thesis: for p being autonomic FinPartState of SCM
for s1, s2 being State of SCM st IC in dom p & NPP p c= s1 & NPP (Relocated (p,k)) c= s2 holds
for P1, P2 being the Instructions of SCM -valued ManySortedSet of NAT st ProgramPart p c= P1 & Reloc ((ProgramPart p),k) c= P2 holds
for i being Element of 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 autonomic FinPartState of SCM; :: thesis: for s1, s2 being State of SCM st IC in dom p & NPP p c= s1 & NPP (Relocated (p,k)) c= s2 holds
for P1, P2 being the Instructions of SCM -valued ManySortedSet of NAT st ProgramPart p c= P1 & Reloc ((ProgramPart p),k) c= P2 holds
for i being Element of 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: ( IC in dom p & NPP p c= s1 & NPP (Relocated (p,k)) c= s2 implies for P1, P2 being the Instructions of SCM -valued ManySortedSet of NAT st ProgramPart p c= P1 & Reloc ((ProgramPart p),k) c= P2 holds
for i being Element of 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: IC in dom p and
A2: NPP p c= s1 and
A3: NPP (Relocated (p,k)) c= s2 ; :: thesis: for P1, P2 being the Instructions of SCM -valued ManySortedSet of NAT st ProgramPart p c= P1 & Reloc ((ProgramPart p),k) c= P2 holds
for i being Element of 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)) )
B1: IC in dom (NPP p) by A1, COMPOS_1:179;
B2: NPP p c= s1 by A2;
let P1, P2 be the Instructions of SCM -valued ManySortedSet of NAT ; :: thesis: ( ProgramPart p c= P1 & Reloc ((ProgramPart p),k) c= P2 implies for i being Element of 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 A4: ( ProgramPart p c= P1 & Reloc ((ProgramPart p),k) c= P2 ) ; :: thesis: for i being Element of 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)) )
A5: Reloc ((ProgramPart p),k) c= P2 by A4;
A8: ProgramPart p c= P1 by A4;
set s3 = s1 +* (DataPart s2);
defpred S1[ Element of 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)) );
A9: not p is NAT -defined by A1, COMPOS_1:19;
A10: NPP p c= s1 +* (DataPart s2) by A2, A3, COMPOS_1:203;
A126: for i being Element of NAT st S1[i] holds
S1[i + 1]
proof
set DPp = DataPart p;
let i be Element of NAT ; :: thesis: ( S1[i] implies S1[i + 1] )
assume that
A11: (IC (Comput (P1,s1,i))) + k = IC (Comput (P2,s2,i)) and
A12: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = CurInstr (P2,(Comput (P2,s2,i))) and
A13: (Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart p)) and
A14: 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 4;
then A15: dom (Comput (P2,s2,(i + 1))) = ({(IC )} \/ (Data-Locations SCM)) \/ NAT by COMPOS_1:160;
set Cs3i1 = Comput (P1,(s1 +* (DataPart s2)),(i + 1));
A16: dom (DataPart (Comput (P2,s2,i))) = Data-Locations SCM by COMPOS_1:50;
A17: dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) = Data-Locations SCM by COMPOS_1:50;
A18: dom (DataPart (Comput (P2,s2,(i + 1)))) = Data-Locations SCM by COMPOS_1:50;
A19: now
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
A20: x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) and
A21: (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 A20, A21, FUNCT_1:70
.= (DataPart (Comput (P2,s2,(i + 1)))) . x by A17, A18, A20, FUNCT_1:70 ; :: thesis: verum
end;
A22: dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),i))) = Data-Locations SCM by COMPOS_1:50;
A23: now
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
A24: x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) and
A25: ( (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 A22, A17, A24, FUNCT_1:70;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A14, A16, A17, A19, A24, A25, FUNCT_1:70; :: thesis: verum
end;
A26: now
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 SCM by AMI_3:72, AMI_3:def 2;
hence d in dom (DataPart s) by COMPOS_1:50; :: thesis: verum
end;
A27: now
let d be Data-Location ; :: thesis: (Comput (P1,(s1 +* (DataPart s2)),i)) . d = (Comput (P2,s2,i)) . d
A28: d in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),i))) by A26;
hence (Comput (P1,(s1 +* (DataPart s2)),i)) . d = (DataPart (Comput (P1,(s1 +* (DataPart s2)),i))) . d by FUNCT_1:70
.= (Comput (P2,s2,i)) . d by A14, A28, FUNCT_1:70 ;
:: 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 4;
then A29: dom (Comput (P1,s1,(i + 1))) = ({(IC )} \/ (Data-Locations SCM)) \/ NAT by COMPOS_1:160;
dom (DataPart p) = (dom p) /\ (Data-Locations SCM) by RELAT_1:90;
then A30: dom (DataPart p) c= {(IC )} \/ (Data-Locations SCM) by XBOOLE_1:10, XBOOLE_1:17;
A31: dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) = (dom (Comput (P1,s1,(i + 1)))) /\ (dom (DataPart p)) by RELAT_1:90
.= dom (DataPart p) by A29, A30, XBOOLE_1:10, XBOOLE_1:28 ;
A32: now
reconsider loc = IC (Comput (P1,s1,(i + 1))) as Element of NAT ;
assume A33: (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 ;
A34: loc in dom (ProgramPart p) by A9, AMISTD_5:def 4, A8, B2;
A35: loc + k in dom (Reloc ((ProgramPart p),k)) by A34, COMPOS_1:158;
A36: dom P2 = NAT by PARTFUN1:def 4;
dom P1 = NAT by PARTFUN1:def 4;
then CurInstr (P1,(Comput (P1,s1,(i + 1)))) = P1 . loc by PARTFUN1:def 8
.= (ProgramPart p) . loc by A34, GRFUNC_1:8, A4
.= (ProgramPart p) . loc ;
hence IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = (Reloc ((ProgramPart p),k)) . (loc + k) by A34, COMPOS_1:122
.= P2 . (IC (Comput (P2,s2,(i + 1)))) by A33, A35, A5, GRFUNC_1:8
.= CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A36, PARTFUN1:def 8 ;
:: thesis: verum
end;
set I = CurInstr (P1,(Comput (P1,s1,i)));
A37: Comput (P2,s2,(i + 1)) = Following (P2,(Comput (P2,s2,i))) by EXTPRO_1:4
.= Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P2,s2,i))) ;
dom (Comput (P2,s2,i)) = the carrier of SCM by PARTFUN1:def 4;
then A38: dom (Comput (P2,s2,i)) = ({(IC )} \/ (Data-Locations SCM)) \/ NAT by COMPOS_1:160;
dom (Comput (P1,s1,i)) = the carrier of SCM by PARTFUN1:def 4;
then A39: dom (Comput (P1,s1,i)) = ({(IC )} \/ (Data-Locations SCM)) \/ NAT by COMPOS_1:160;
A40: dom ((Comput (P1,s1,i)) | (dom (DataPart p))) = (dom (Comput (P1,s1,i))) /\ (dom (DataPart p)) by RELAT_1:90
.= dom (DataPart p) by A39, A30, XBOOLE_1:10, XBOOLE_1:28 ;
A41: Comput (P1,(s1 +* (DataPart s2)),(i + 1)) = Following (P1,(Comput (P1,(s1 +* (DataPart s2)),i))) by EXTPRO_1:4
.= Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,(s1 +* (DataPart s2)),i))) by A2, A9, A10, AMISTD_5:7, A4 ;
A42: dom (DataPart p) = dom (DataPart (Relocated (p,k))) by COMPOS_1:115;
then A43: dom ((Comput (P2,s2,(i + 1))) | (dom (DataPart (Relocated (p,k))))) = (dom (Comput (P2,s2,(i + 1)))) /\ (dom (DataPart p)) by RELAT_1:90
.= dom (DataPart p) by A15, A30, XBOOLE_1:10, XBOOLE_1:28 ;
A44: now
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
A45: ( d = x & d in dom (DataPart p) ) and
A46: (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 A31, A45, A46, FUNCT_1:70
.= ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A42, A43, A45, FUNCT_1:70 ; :: thesis: verum
end;
A47: dom ((Comput (P2,s2,i)) | (dom (DataPart (Relocated (p,k))))) = (dom (Comput (P2,s2,i))) /\ (dom (DataPart p)) by A42, RELAT_1:90
.= dom (DataPart p) by A38, A30, XBOOLE_1:10, XBOOLE_1:28 ;
A48: now
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
A49: d = x and
A50: d in dom (DataPart p) and
A51: ( (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 A42, A40, A47, A50, FUNCT_1:70;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = (Comput (P2,s2,(i + 1))) . d by A13, A31, A49, A50, A51, FUNCT_1:70
.= ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A42, A43, A49, A50, FUNCT_1:70 ;
:: thesis: verum
end;
reconsider j = IC (Comput (P1,s1,i)) as Element of NAT ;
A52: Comput (P1,s1,(i + 1)) = Following (P1,(Comput (P1,s1,i))) by EXTPRO_1:4
.= Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i))) ;
A53: succ ((IC (Comput (P1,s1,i))) + k) = (j + k) + 1 by NAT_1:39
.= (j + 1) + k
.= (succ (IC (Comput (P1,s1,i)))) + k by NAT_1:39 ;
per cases ( 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 ) by AMI_5:36, NAT_1:33;
suppose InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 0 ; :: thesis: S1[i + 1]
then A54: CurInstr (P1,(Comput (P1,s1,i))) = halt SCM by AMI_5:46;
thus (IC (Comput (P1,s1,(i + 1)))) + k = (IC (Comput (P1,s1,i))) + k by A52, A54, EXTPRO_1:def 3
.= IC (Comput (P2,s2,(i + 1))) by A11, A37, A54, A12, 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 A32; :: 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))) )
A55: Comput (P2,s2,(i + 1)) = Comput (P2,s2,i) by A37, A54, A12, EXTPRO_1:def 3;
hence (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A13, A52, A54, 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 A14, A41, A54, A55, 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
A56: CurInstr (P1,(Comput (P1,s1,i))) = da := db by AMI_5:47;
A57: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = da := db by A56, COMPOS_1:92;
A58: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = succ (IC (Comput (P1,s1,i))) by A56, AMI_3:8;
hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A11, A12, A52, A37, A53, A57, AMI_3:8; :: 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 A11, A12, A32, A52, A37, A53, A57, A58, AMI_3:8; :: 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))) )
A59: (Comput (P1,(s1 +* (DataPart s2)),i)) . db = (Comput (P2,s2,i)) . db by A27;
now
DataPart p c= p by RELAT_1:88;
then A60: dom (DataPart p) c= dom p by GRFUNC_1:8;
let x be set ; :: 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 A61: 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 SCM by RELAT_1:87;
then x in Data-Locations SCM by A31, A61;
then reconsider d = x as Data-Location by AMI_3:72, AMI_3:def 2;
per cases ( da = d or da <> d ) ;
suppose A62: 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 A12, A52, A37, A56, A57, AMI_3:8;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A2, A9, A10, A31, A44, A56, A59, A61, A60, A62, AMI_5:88, A4; :: 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 A12, A52, A37, A56, A57, AMI_3:8;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A31, A48, A61; :: thesis: verum
end;
end;
end;
then (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A42, A31, A43, GRFUNC_1:8;
hence (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A42, A31, A43, GRFUNC_1:9; :: thesis: DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1)))
now
let x be set ; :: 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 A63: 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 A17, AMI_3:72, AMI_3:def 2;
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 A12, A37, A41, A56, A57, AMI_3:8;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A27, A19, A63; :: 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 A12, A37, A41, A56, A57, AMI_3:8;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A23, A63; :: thesis: verum
end;
end;
end;
then DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1))) by A17, A18, GRFUNC_1:8;
hence DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) by A17, A18, GRFUNC_1:9; :: 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
A64: CurInstr (P1,(Comput (P1,s1,i))) = AddTo (da,db) by AMI_5:48;
A65: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = AddTo (da,db) by A64, COMPOS_1:92;
A66: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = succ (IC (Comput (P1,s1,i))) by A64, AMI_3:9;
hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A11, A12, A52, A37, A53, A65, AMI_3:9; :: 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 A11, A12, A32, A52, A37, A53, A65, A66, AMI_3:9; :: 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))) )
A67: ( (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 A27;
now
DataPart p c= p by RELAT_1:88;
then A68: dom (DataPart p) c= dom p by GRFUNC_1:8;
let x be set ; :: 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 A69: 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 SCM by RELAT_1:87;
then x in Data-Locations SCM by A31, A69;
then reconsider d = x as Data-Location by AMI_3:72, AMI_3:def 2;
per cases ( da = d or da <> d ) ;
suppose A70: 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 A12, A52, A37, A64, A65, AMI_3:9;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A2, A9, A10, A31, A44, A64, A67, A69, A68, A70, AMI_5:89, A4; :: 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 A12, A52, A37, A64, A65, AMI_3:9;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A31, A48, A69; :: thesis: verum
end;
end;
end;
then (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A42, A31, A43, GRFUNC_1:8;
hence (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A42, A31, A43, GRFUNC_1:9; :: thesis: DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1)))
now
let x be set ; :: 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 A71: 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 A17, AMI_3:72, AMI_3:def 2;
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 A12, A37, A41, A64, A65, AMI_3:9;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A19, A67, A71; :: 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 A12, A37, A41, A64, A65, AMI_3:9;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A23, A71; :: thesis: verum
end;
end;
end;
then DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1))) by A17, A18, GRFUNC_1:8;
hence DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) by A17, A18, GRFUNC_1:9; :: 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
A72: CurInstr (P1,(Comput (P1,s1,i))) = SubFrom (da,db) by AMI_5:49;
A73: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = SubFrom (da,db) by A72, COMPOS_1:92;
A74: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = succ (IC (Comput (P1,s1,i))) by A72, AMI_3:10;
hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A11, A12, A52, A37, A53, A73, AMI_3:10; :: 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 A11, A12, A32, A52, A37, A53, A73, A74, AMI_3:10; :: 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))) )
A75: ( (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 A27;
now
DataPart p c= p by RELAT_1:88;
then A76: dom (DataPart p) c= dom p by GRFUNC_1:8;
let x be set ; :: 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 A77: 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 SCM by RELAT_1:87;
then x in Data-Locations SCM by A31, A77;
then reconsider d = x as Data-Location by AMI_3:72, AMI_3:def 2;
per cases ( da = d or da <> d ) ;
suppose A78: 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 A12, A52, A37, A72, A73, AMI_3:10;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A2, A9, A10, A31, A44, A72, A75, A77, A76, A78, AMI_5:90, A4; :: 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 A12, A52, A37, A72, A73, AMI_3:10;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A31, A48, A77; :: thesis: verum
end;
end;
end;
then (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A42, A31, A43, GRFUNC_1:8;
hence (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A42, A31, A43, GRFUNC_1:9; :: thesis: DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1)))
now
let x be set ; :: 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 A79: 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 A17, AMI_3:72, AMI_3:def 2;
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 A12, A37, A41, A72, A73, AMI_3:10;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A19, A75, A79; :: 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 A12, A37, A41, A72, A73, AMI_3:10;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A23, A79; :: thesis: verum
end;
end;
end;
then DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1))) by A17, A18, GRFUNC_1:8;
hence DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) by A17, A18, GRFUNC_1:9; :: 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
A80: CurInstr (P1,(Comput (P1,s1,i))) = MultBy (da,db) by AMI_5:50;
A81: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = MultBy (da,db) by A80, COMPOS_1:92;
A82: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = succ (IC (Comput (P1,s1,i))) by A80, AMI_3:11;
hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A11, A12, A52, A37, A53, A81, AMI_3:11; :: 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 A11, A12, A32, A52, A37, A53, A81, A82, AMI_3:11; :: 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))) )
A83: ( (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 A27;
now
DataPart p c= p by RELAT_1:88;
then A84: dom (DataPart p) c= dom p by GRFUNC_1:8;
let x be set ; :: 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 A85: 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 SCM by RELAT_1:87;
then x in Data-Locations SCM by A31, A85;
then reconsider d = x as Data-Location by AMI_3:72, AMI_3:def 2;
per cases ( da = d or da <> d ) ;
suppose A86: 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 A12, A52, A37, A80, A81, AMI_3:11;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A2, A9, A10, A31, A44, A80, A83, A85, A84, A86, AMI_5:91, A4; :: 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 A12, A52, A37, A80, A81, AMI_3:11;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A31, A48, A85; :: thesis: verum
end;
end;
end;
then (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A42, A31, A43, GRFUNC_1:8;
hence (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A42, A31, A43, GRFUNC_1:9; :: thesis: DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1)))
now
let x be set ; :: 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 A87: 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 A17, AMI_3:72, AMI_3:def 2;
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 A12, A37, A41, A80, A81, AMI_3:11;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A19, A83, A87; :: 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 A12, A37, A41, A80, A81, AMI_3:11;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A23, A87; :: thesis: verum
end;
end;
end;
then DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1))) by A17, A18, GRFUNC_1:8;
hence DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) by A17, A18, GRFUNC_1:9; :: 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
A88: CurInstr (P1,(Comput (P1,s1,i))) = Divide (da,db) by AMI_5:51;
A89: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = Divide (da,db) by A88, COMPOS_1:92;
A90: ( (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 A27;
per cases ( da <> db or da = db ) ;
suppose A91: da <> db ; :: thesis: S1[i + 1]
A92: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = succ (IC (Comput (P1,s1,i))) by A88, AMI_3:12;
hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A11, A12, A52, A37, A53, A89, AMI_3:12; :: 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 A11, A12, A32, A52, A37, A53, A89, A92, AMI_3:12; :: 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
DataPart p c= p by RELAT_1:88;
then A93: dom (DataPart p) c= dom p by GRFUNC_1:8;
let x be set ; :: 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 A94: 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 SCM by RELAT_1:87;
then x in Data-Locations SCM by A31, A94;
then reconsider d = x as Data-Location by AMI_3:72, AMI_3:def 2;
per cases ( da = d or db = d or ( da <> d & db <> d ) ) ;
suppose A95: da = d ; :: thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1
then A96: ( (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 A12, A52, A37, A88, A89, A91, AMI_3:12;
((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 A2, A9, A10, A31, A88, A91, A94, A93, A95, AMI_5:92, A4;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = (Comput (P2,s2,(i + 1))) . d by A90, A94, A96, FUNCT_1:70
.= ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A42, A31, A43, A94, FUNCT_1:70 ;
:: thesis: verum
end;
suppose A97: 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 A12, A52, A37, A88, A89, AMI_3:12;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A2, A9, A10, A31, A44, A88, A90, A94, A93, A97, AMI_5:93, A4; :: 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 A12, A52, A37, A88, A89, AMI_3:12;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A31, A48, A94; :: thesis: verum
end;
end;
end;
then (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A42, A31, A43, GRFUNC_1:8;
hence (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A42, A31, A43, GRFUNC_1:9; :: thesis: DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1)))
now
let x be set ; :: 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 A98: 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 A17, AMI_3:72, AMI_3:def 2;
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 A12, A37, A41, A88, A89, A91, AMI_3:12;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A19, A90, A98; :: 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 A12, A37, A41, A88, A89, AMI_3:12;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A19, A90, A98; :: 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 A12, A37, A41, A88, A89, AMI_3:12;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A23, A98; :: thesis: verum
end;
end;
end;
then DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1))) by A17, A18, GRFUNC_1:8;
hence DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) by A17, A18, GRFUNC_1:9; :: thesis: verum
end;
suppose A99: da = db ; :: thesis: S1[i + 1]
A100: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = succ (IC (Comput (P1,s1,i))) by A88, AMI_3:12;
hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A11, A12, A52, A37, A53, A89, AMI_3:12; :: 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 A11, A12, A32, A52, A37, A53, A89, A100, AMI_3:12; :: 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
let x be set ; :: 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 A101: 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 SCM by RELAT_1:87;
then x in Data-Locations SCM by A31, A101;
then reconsider d = x as Data-Location by AMI_3:72, AMI_3:def 2;
per cases ( da = d or da <> d ) ;
suppose A102: da = d ; :: thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1
A103: ( ((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 A42, A31, A40, A47, A101, FUNCT_1:70;
A104: ( ((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 A42, A31, A43, A101, FUNCT_1:70;
(Comput (P2,s2,(i + 1))) . d = ((Comput (P2,s2,i)) . da) mod ((Comput (P2,s2,i)) . db) by A12, A37, A89, A99, A102, AMI_3:12;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A13, A52, A88, A99, A102, A103, A104, AMI_3:12; :: 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 A12, A52, A37, A88, A89, A99, AMI_3:12;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A31, A48, A101; :: thesis: verum
end;
end;
end;
then (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A42, A31, A43, GRFUNC_1:8;
hence (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A42, A31, A43, GRFUNC_1:9; :: thesis: DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1)))
now
let x be set ; :: 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 A105: 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 A17, AMI_3:72, AMI_3:def 2;
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 A12, A37, A41, A88, A89, A99, AMI_3:12;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A19, A90, A105; :: 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 A12, A37, A41, A88, A89, A99, AMI_3:12;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A23, A105; :: thesis: verum
end;
end;
end;
then DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1))) by A17, A18, GRFUNC_1:8;
hence DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) by A17, A18, GRFUNC_1:9; :: thesis: verum
end;
end;
end;
suppose InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 6 ; :: thesis: S1[i + 1]
then consider loc being Element of NAT such that
A106: CurInstr (P1,(Comput (P1,s1,i))) = SCM-goto loc by AMI_5:52;
A107: CurInstr (P2,(Comput (P2,s2,i))) = SCM-goto (loc + k) by A12, A106, Th1;
thus (IC (Comput (P1,s1,(i + 1)))) + k = loc + k by A52, A106, AMI_3:13
.= IC (Comput (P2,s2,(i + 1))) by A37, A107, AMI_3:13 ; :: 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 A32; :: 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
let x be set ; :: 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 A108: 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 SCM by RELAT_1:87;
then x in Data-Locations SCM by A31, A108;
then reconsider d = x as Data-Location by AMI_3:72, AMI_3:def 2;
( (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d ) by A52, A37, A106, A107, AMI_3:13;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A31, A48, A108; :: thesis: verum
end;
then (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A42, A31, A43, GRFUNC_1:8;
hence (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A42, A31, A43, GRFUNC_1:9; :: thesis: DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1)))
now
let x be set ; :: 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 A109: 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 A17, AMI_3:72, AMI_3:def 2;
( (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 A37, A41, A106, A107, AMI_3:13;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A23, A109; :: thesis: verum
end;
then DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1))) by A17, A18, GRFUNC_1:8;
hence DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) by A17, A18, GRFUNC_1:9; :: thesis: verum
end;
suppose InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 7 ; :: thesis: S1[i + 1]
then consider loc being Element of NAT , da being Data-Location such that
A110: CurInstr (P1,(Comput (P1,s1,i))) = da =0_goto loc by AMI_5:53;
A111: now
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 A52, A110, AMI_3:14; :: thesis: verum
end;
case (Comput (P1,s1,i)) . da <> 0 ; :: thesis: (IC (Comput (P1,s1,(i + 1)))) + k = succ (IC (Comput (P2,s2,i)))
hence (IC (Comput (P1,s1,(i + 1)))) + k = succ (IC (Comput (P2,s2,i))) by A11, A52, A53, A110, AMI_3:14; :: thesis: verum
end;
end;
end;
A112: CurInstr (P2,(Comput (P2,s2,i))) = da =0_goto (loc + k) by A12, A110, Th2;
A113: now
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 A37, A112, AMI_3:14; :: thesis: verum
end;
case (Comput (P2,s2,i)) . da <> 0 ; :: thesis: IC (Comput (P2,s2,(i + 1))) = succ (IC (Comput (P2,s2,i)))
hence IC (Comput (P2,s2,(i + 1))) = succ (IC (Comput (P2,s2,i))) by A37, A112, AMI_3:14; :: thesis: verum
end;
end;
end;
A114: (Comput (P1,(s1 +* (DataPart s2)),i)) . da = (Comput (P2,s2,i)) . da by A27;
A115: now
per cases ( loc <> succ (IC (Comput (P1,s1,i))) or loc = succ (IC (Comput (P1,s1,i))) ) ;
suppose loc <> succ (IC (Comput (P1,s1,i))) ; :: 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 A2, A9, A10, A110, A114, A111, A113, AMI_5:94, A4; :: thesis: verum
end;
suppose loc = succ (IC (Comput (P1,s1,i))) ; :: 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 A11, A53, A111, A113; :: 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 A32, A115; :: 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
let x be set ; :: 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 A116: 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 SCM by RELAT_1:87;
then x in Data-Locations SCM by A31, A116;
then reconsider d = x as Data-Location by AMI_3:72, AMI_3:def 2;
( (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d ) by A52, A37, A110, A112, AMI_3:14;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A31, A48, A116; :: thesis: verum
end;
then (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A42, A31, A43, GRFUNC_1:8;
hence (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A42, A31, A43, GRFUNC_1:9; :: thesis: DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1)))
now
let x be set ; :: 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 A117: 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 A17, AMI_3:72, AMI_3:def 2;
( (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 A37, A41, A110, A112, AMI_3:14;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A23, A117; :: thesis: verum
end;
then DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1))) by A17, A18, GRFUNC_1:8;
hence DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) by A17, A18, GRFUNC_1:9; :: thesis: verum
end;
suppose InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 8 ; :: thesis: S1[i + 1]
then consider loc being Element of NAT , da being Data-Location such that
A118: CurInstr (P1,(Comput (P1,s1,i))) = da >0_goto loc by AMI_5:54;
A119: now
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 A52, A118, AMI_3:15; :: thesis: verum
end;
case (Comput (P1,s1,i)) . da <= 0 ; :: thesis: (IC (Comput (P1,s1,(i + 1)))) + k = succ (IC (Comput (P2,s2,i)))
hence (IC (Comput (P1,s1,(i + 1)))) + k = succ (IC (Comput (P2,s2,i))) by A11, A52, A53, A118, AMI_3:15; :: thesis: verum
end;
end;
end;
A120: CurInstr (P2,(Comput (P2,s2,i))) = da >0_goto (loc + k) by A12, A118, Th3;
A121: now
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 A37, A120, AMI_3:15; :: thesis: verum
end;
case (Comput (P2,s2,i)) . da <= 0 ; :: thesis: IC (Comput (P2,s2,(i + 1))) = succ (IC (Comput (P2,s2,i)))
hence IC (Comput (P2,s2,(i + 1))) = succ (IC (Comput (P2,s2,i))) by A37, A120, AMI_3:15; :: thesis: verum
end;
end;
end;
A122: (Comput (P1,(s1 +* (DataPart s2)),i)) . da = (Comput (P2,s2,i)) . da by A27;
A123: now
per cases ( loc <> succ (IC (Comput (P1,s1,i))) or loc = succ (IC (Comput (P1,s1,i))) ) ;
suppose loc <> succ (IC (Comput (P1,s1,i))) ; :: 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 A2, A9, A10, A118, A122, A119, A121, AMI_5:95, A4; :: thesis: verum
end;
suppose loc = succ (IC (Comput (P1,s1,i))) ; :: 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 A11, A53, A119, A121; :: 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 A32, A123; :: 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
let x be set ; :: 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 A124: 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 SCM by RELAT_1:87;
then x in Data-Locations SCM by A31, A124;
then reconsider d = x as Data-Location by AMI_3:72, AMI_3:def 2;
( (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d ) by A52, A37, A118, A120, AMI_3:15;
hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A31, A48, A124; :: thesis: verum
end;
then (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A42, A31, A43, GRFUNC_1:8;
hence (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A42, A31, A43, GRFUNC_1:9; :: thesis: DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1)))
now
let x be set ; :: 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 A125: 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 A17, AMI_3:72, AMI_3:def 2;
( (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 A37, A41, A118, A120, AMI_3:15;
hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A23, A125; :: thesis: verum
end;
then DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1))) by A17, A18, GRFUNC_1:8;
hence DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) by A17, A18, GRFUNC_1:9; :: thesis: verum
end;
end;
end;
B127: DataPart (NPP p) c= NPP p by RELAT_1:88;
A129: DataPart p = DataPart (Relocated (p,k)) by COMPOS_1:115;
A130: IC in dom (Relocated (p,k)) by COMPOS_1:119;
then B130: IC in dom (NPP (Relocated (p,k))) by COMPOS_1:179;
now
thus (IC (Comput (P1,s1,0))) + k = (IC s1) + k by EXTPRO_1:3
.= (IC (NPP p)) + k by A2, GRFUNC_1:8, B1
.= (IC p) + k by A1, COMPOS_1:72
.= IC (Relocated (p,k)) by A1, COMPOS_1:120
.= IC (NPP (Relocated (p,k))) by A130, COMPOS_1:72
.= IC s2 by A3, GRFUNC_1:8, B130
.= IC (Comput (P2,s2,0)) by EXTPRO_1:3 ; :: 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 (NPP p) as Element of NAT ;
A131: IC (NPP p) = IC s1 by A2, GRFUNC_1:8, B1;
then IC (NPP p) = IC (Comput (P1,s1,0)) by EXTPRO_1:3;
then A132: loc in dom (ProgramPart p) by A9, AMISTD_5:def 4, A8, B2;
A133: (IC (NPP p)) + k in dom (Reloc ((ProgramPart p),k)) by A132, COMPOS_1:158;
IC in dom (Relocated (p,k)) by COMPOS_1:119;
then B134: IC in dom (NPP (Relocated (p,k))) by COMPOS_1:179;
A135: (ProgramPart p) . (IC (NPP p)) = P1 . (IC s1) by A131, A132, GRFUNC_1:8, A4;
dom P2 = NAT by PARTFUN1:def 4;
then A136: CurInstr (P2,(Comput (P2,s2,0))) = P2 . (IC (Comput (P2,s2,0))) by PARTFUN1:def 8
.= P2 . (IC s2) by EXTPRO_1:3
.= P2 . (IC (NPP (Relocated (p,k)))) by A3, GRFUNC_1:8, B134
.= P2 . (IC (Relocated (p,k))) by GRFUNC_1:8, B134
.= P2 . ((IC p) + k) by A1, COMPOS_1:120
.= P2 . ((IC (NPP p)) + k) by A1, COMPOS_1:72
.= (Reloc ((ProgramPart p),k)) . ((IC (NPP p)) + k) by A133, GRFUNC_1:8, A4 ;
A137: dom P1 = NAT by PARTFUN1:def 4;
CurInstr (P1,(Comput (P1,s1,0))) = CurInstr (P1,s1) by EXTPRO_1:3
.= P1 . (IC s1) by A137, PARTFUN1:def 8 ;
hence IncAddr ((CurInstr (P1,(Comput (P1,s1,0)))),k) = CurInstr (P2,(Comput (P2,s2,0))) by A132, A135, A136, COMPOS_1:122; :: 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)) )
A138: dom (DataPart s2) = Data-Locations SCM by COMPOS_1:50;
DataPart p = DataPart (NPP p) by COMPOS_1:73;
then X1: DataPart p c= s1 by A2, B127, XBOOLE_1:1;
DataPart (Relocated (p,k)) c= NPP (Relocated (p,k)) by COMPOS_1:169;
then X2: DataPart p c= s2 by A3, A129, XBOOLE_1:1;
thus (Comput (P1,s1,0)) | (dom (DataPart p)) = s1 | (dom (DataPart p)) by EXTPRO_1:3
.= DataPart p by GRFUNC_1:64, X1
.= s2 | (dom (DataPart p)) by GRFUNC_1:64, X2
.= (Comput (P2,s2,0)) | (dom (DataPart p)) by EXTPRO_1:3 ; :: 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)) by EXTPRO_1:3
.= DataPart s2 by A138, FUNCT_4:24
.= DataPart (Comput (P2,s2,0)) by EXTPRO_1:3 ; :: thesis: verum
end;
then A139: S1[ 0 ] ;
thus for i being Element of NAT holds S1[i] from NAT_1:sch 1(A139, A126); :: thesis: verum