:: SCMFSA_5 semantic presentation begin begin theorem Th1: :: SCMFSA_5:1 for k being Element of NAT for q being NAT -defined the InstructionsF of SCM+FSA -valued finite non halt-free Function for p being non empty b2 -autonomic FinPartState of SCM+FSA for s1, s2 being State of SCM+FSA st p c= s1 & IncIC (p,k) c= s2 holds for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & Reloc (q,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)) ) proof let k be Element of NAT ; ::_thesis: for q being NAT -defined the InstructionsF of SCM+FSA -valued finite non halt-free Function for p being non empty b1 -autonomic FinPartState of SCM+FSA for s1, s2 being State of SCM+FSA st p c= s1 & IncIC (p,k) c= s2 holds for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & Reloc (q,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 q be NAT -defined the InstructionsF of SCM+FSA -valued finite non halt-free Function; ::_thesis: for p being non empty q -autonomic FinPartState of SCM+FSA for s1, s2 being State of SCM+FSA st p c= s1 & IncIC (p,k) c= s2 holds for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & Reloc (q,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 non empty q -autonomic FinPartState of SCM+FSA; ::_thesis: for s1, s2 being State of SCM+FSA st p c= s1 & IncIC (p,k) c= s2 holds for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & Reloc (q,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+FSA; ::_thesis: ( p c= s1 & IncIC (p,k) c= s2 implies for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & Reloc (q,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: p c= s1 and A2: IncIC (p,k) c= s2 ; ::_thesis: for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & Reloc (q,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)) ) A3: IC in dom p by AMISTD_5:6; let P1, P2 be Instruction-Sequence of SCM+FSA; ::_thesis: ( q c= P1 & Reloc (q,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: ( q c= P1 & Reloc (q,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 (q,k) c= P2 by A4; A6: q c= P1 by A4; 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)) ); A7: p c= s1 +* (DataPart s2) by A1, A2, MEMSTR_0:61; A8: 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 A9: (IC (Comput (P1,s1,i))) + k = IC (Comput (P2,s2,i)) and A10: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = CurInstr (P2,(Comput (P2,s2,i))) and A11: (Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart p)) and A12: DataPart (Comput (P1,(s1 +* (DataPart s2)),i)) = DataPart (Comput (P2,s2,i)) ; ::_thesis: S1[i + 1] set Cs1i1 = Comput (P1,s1,(i + 1)); set Cs1i = Comput (P1,s1,i); A13: dom (Comput (P1,s1,(i + 1))) = (Data-Locations ) \/ {(IC )} by MEMSTR_0:13; set Cs3i = Comput (P1,(s1 +* (DataPart s2)),i); set Cs2i = Comput (P2,s2,i); A14: dom (Comput (P1,s1,i)) = (Data-Locations ) \/ {(IC )} by MEMSTR_0:13; set Cs2i1 = Comput (P2,s2,(i + 1)); A15: dom (Comput (P2,s2,(i + 1))) = (Data-Locations ) \/ {(IC )} by MEMSTR_0:13; A16: dom (Comput (P2,s2,i)) = (Data-Locations ) \/ {(IC )} by MEMSTR_0:13; set I = CurInstr (P1,(Comput (P1,s1,i))); A17: 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))) ; A18: now__::_thesis:_for_s_being_State_of_SCM+FSA for_d_being_FinSeq-Location_holds_d_in_dom_(DataPart_s) let s be State of SCM+FSA; ::_thesis: for d being FinSeq-Location holds d in dom (DataPart s) let d be FinSeq-Location ; ::_thesis: d in dom (DataPart s) d in FinSeq-Locations by SCMFSA_2:def_5; then d in Data-Locations by SCMFSA_2:100, XBOOLE_0:def_3; hence d in dom (DataPart s) by MEMSTR_0:9; ::_thesis: verum end; A19: now__::_thesis:_for_d_being_FinSeq-Location_holds_(Comput_(P1,(s1_+*_(DataPart_s2)),i))_._d_=_(Comput_(P2,s2,i))_._d let d be FinSeq-Location ; ::_thesis: (Comput (P1,(s1 +* (DataPart s2)),i)) . d = (Comput (P2,s2,i)) . d A20: d in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),i))) by A18; 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 A12, A20, FUNCT_1:47 ; ::_thesis: verum end; set Cs3i1 = Comput (P1,(s1 +* (DataPart s2)),(i + 1)); A21: dom (DataPart (Comput (P2,s2,i))) = Data-Locations by MEMSTR_0:9; A22: dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) = Data-Locations by MEMSTR_0:9; A23: 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 A24: (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 ii = loc as Element of NAT ; A25: ii in dom q by A6, A1, AMISTD_5:def_4; A26: loc + k in dom (Reloc (q,k)) by A25, COMPOS_1:46; A27: dom P2 = NAT by PARTFUN1:def_2; dom P1 = NAT by PARTFUN1:def_2; then CurInstr (P1,(Comput (P1,s1,(i + 1)))) = P1 . loc by PARTFUN1:def_6 .= q . loc by A25, A4, GRFUNC_1:2 .= q . loc ; hence IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = (Reloc (q,k)) . (loc + k) by A25, COMPOS_1:35 .= P2 . (IC (Comput (P2,s2,(i + 1)))) by A24, A26, A5, GRFUNC_1:2 .= CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A27, PARTFUN1:def_6 ; ::_thesis: verum end; A28: now__::_thesis:_for_s_being_State_of_SCM+FSA for_d_being_Int-Location_holds_d_in_dom_(DataPart_s) let s be State of SCM+FSA; ::_thesis: for d being Int-Location holds d in dom (DataPart s) let d be Int-Location; ::_thesis: d in dom (DataPart s) d in Int-Locations by AMI_2:def_16; then d in Data-Locations by SCMFSA_2:100, XBOOLE_0:def_3; hence d in dom (DataPart s) by MEMSTR_0:9; ::_thesis: verum end; A29: now__::_thesis:_for_d_being_Int-Location_holds_(Comput_(P1,(s1_+*_(DataPart_s2)),i))_._d_=_(Comput_(P2,s2,i))_._d let d be Int-Location; ::_thesis: (Comput (P1,(s1 +* (DataPart s2)),i)) . d = (Comput (P2,s2,i)) . d A30: d in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),i))) by A28; 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 A12, A30, FUNCT_1:47 ; ::_thesis: verum end; dom (DataPart p) = (dom p) /\ (Data-Locations ) by RELAT_1:61; then A31: dom (DataPart p) c= {(IC )} \/ (Data-Locations ) by XBOOLE_1:10, XBOOLE_1:17; A32: InsCode (CurInstr (P1,(Comput (P1,s1,i)))) <= 12 by SCMFSA_2:16; A33: 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 A13, A31, XBOOLE_1:28 ; A34: dom (DataPart (Comput (P2,s2,(i + 1)))) = Data-Locations by MEMSTR_0:9; A35: now__::_thesis:_for_x_being_set_st_x_in_dom_((Comput_(P1,(s1_+*_(DataPart_s2)),(i_+_1)))_|_(Data-Locations_))_&_(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 ((Comput (P1,(s1 +* (DataPart s2)),(i + 1))) | (Data-Locations )) & (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 A36: x in dom ((Comput (P1,(s1 +* (DataPart s2)),(i + 1))) | (Data-Locations )) and A37: (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 A36, A37, FUNCT_1:47 .= (DataPart (Comput (P2,s2,(i + 1)))) . x by A22, A34, A36, FUNCT_1:47 ; ::_thesis: verum end; A38: dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),i))) = Data-Locations by MEMSTR_0:9; A39: 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 A40: x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) and A41: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = (Comput (P1,(s1 +* (DataPart s2)),i)) . x and A42: (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 A38, A22, A40, FUNCT_1:47; hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A12, A21, A22, A35, A40, A41, A42, FUNCT_1:47; ::_thesis: verum end; A43: 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, A7, A4, AMISTD_5:7 ; A44: 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 A15, A31, XBOOLE_1:28 ; A45: now__::_thesis:_for_x,_d_being_set_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, d be set ; ::_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 A46: d = x and A47: d in dom (DataPart p) and A48: (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 A33, A46, A47, A48, FUNCT_1:47 .= ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A44, A46, A47, FUNCT_1:47 ; ::_thesis: verum end; A49: dom ((Comput (P1,s1,i)) | (dom (DataPart p))) = (dom (Comput (P1,s1,i))) /\ (dom (DataPart p)) by RELAT_1:61 .= dom (DataPart p) by A14, A31, XBOOLE_1:28 ; 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: dom ((Comput (P2,s2,i)) | (dom (DataPart p))) = (dom (Comput (P2,s2,i))) /\ (dom (DataPart p)) by RELAT_1:61 .= dom (DataPart p) by A16, A31, XBOOLE_1:28 ; A52: now__::_thesis:_for_x,_d_being_set_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, d be set ; ::_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 A53: d = x and A54: d in dom (DataPart p) and A55: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d and A56: (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 A57: ((Comput (P1,s1,i)) | (dom (DataPart p))) . d = (Comput (P1,s1,i)) . d by A49, A54, FUNCT_1:47; ((Comput (P2,s2,i)) | (dom (DataPart p))) . d = (Comput (P2,s2,i)) . d by A51, A54, FUNCT_1:47; hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = (Comput (P2,s2,(i + 1))) . d by A11, A33, A53, A54, A55, A56, A57, FUNCT_1:47 .= ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A44, A53, A54, FUNCT_1:47 ; ::_thesis: verum end; A58: succ ((IC (Comput (P1,s1,i))) + k) = (j + k) + 1 by NAT_1:38 .= (j + 1) + k .= (succ (IC (Comput (P1,s1,i)))) + k by NAT_1:38 ; percases ( 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 or InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 9 or InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 10 or InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 11 or InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 12 ) by A32, NAT_1:36; suppose InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 0 ; ::_thesis: S1[i + 1] then A59: CurInstr (P1,(Comput (P1,s1,i))) = halt SCM+FSA by SCMFSA_2:95; thus (IC (Comput (P1,s1,(i + 1)))) + k = (IC (Comput (P1,s1,i))) + k by A50, A59, EXTPRO_1:def_3 .= IC (Comput (P2,s2,(i + 1))) by A9, A17, A59, A10, 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 A23; ::_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))) ) A60: Comput (P2,s2,(i + 1)) = Comput (P2,s2,i) by A17, A59, A10, EXTPRO_1:def_3; hence (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A11, A50, A59, 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 A12, A43, A59, A60, 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 Int-Location such that A61: CurInstr (P1,(Comput (P1,s1,i))) = da := db by SCMFSA_2:30; A62: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = da := db by A61, COMPOS_0:4; A63: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = succ (IC (Comput (P1,s1,i))) by A61, SCMFSA_2:63; hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A9, A10, A50, A17, A58, A62, SCMFSA_2:63; ::_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 A9, A10, A23, A50, A17, A58, A62, A63, SCMFSA_2:63; ::_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))) ) A64: (Comput (P1,(s1 +* (DataPart s2)),i)) . db = (Comput (P2,s2,i)) . db by A29; now__::_thesis:_for_x_being_set_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 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 ) A65: dom (DataPart p) c= Data-Locations by RELAT_1:58; assume A66: 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 percases ( x in FinSeq-Locations or da = x or ( da <> x & x in Int-Locations ) ) by A33, A66, A65, SCMFSA_2:100, XBOOLE_0:def_3; suppose x in FinSeq-Locations ; ::_thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1 then reconsider d = x as FinSeq-Location by SCMFSA_2:def_5; A67: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A50, A61, SCMFSA_2:63; (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A62, SCMFSA_2:63; hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A33, A52, A66, A67; ::_thesis: verum end; supposeA68: da = x ; ::_thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1 DataPart p c= p by RELAT_1:59; then dom (DataPart p) c= dom p by GRFUNC_1:2; then A69: (Comput (P1,(s1 +* (DataPart s2)),i)) . db = (Comput (P1,s1,i)) . db by A1, A7, A33, A61, A66, A68, A4, SCMFSA_3:5; A70: (Comput (P1,s1,(i + 1))) . x = (Comput (P1,s1,i)) . db by A50, A61, A68, SCMFSA_2:63; (Comput (P2,s2,(i + 1))) . x = (Comput (P2,s2,i)) . db by A10, A17, A62, A68, SCMFSA_2:63; hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A33, A45, A64, A66, A70, A69; ::_thesis: verum end; supposeA71: ( da <> x & x in Int-Locations ) ; ::_thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1 then reconsider d = x as Int-Location by AMI_2:def_16; A72: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A50, A61, A71, SCMFSA_2:63; (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A62, A71, SCMFSA_2:63; hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A33, A52, A66, A72; ::_thesis: verum end; end; end; then (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A33, A44, GRFUNC_1:2; hence (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A33, A44, GRFUNC_1:3; ::_thesis: DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) now__::_thesis:_for_x_being_set_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 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 A73: 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 percases ( x in FinSeq-Locations or da = x or ( da <> x & x in Int-Locations ) ) by A22, A73, SCMFSA_2:100, XBOOLE_0:def_3; suppose x in FinSeq-Locations ; ::_thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 then reconsider f = x as FinSeq-Location by SCMFSA_2:def_5; A74: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . f = (Comput (P1,(s1 +* (DataPart s2)),i)) . f by A43, A61, SCMFSA_2:63; (Comput (P2,s2,(i + 1))) . f = (Comput (P2,s2,i)) . f by A10, A17, A62, SCMFSA_2:63; hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A39, A73, A74; ::_thesis: verum end; supposeA75: da = x ; ::_thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 A76: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . da = (Comput (P1,(s1 +* (DataPart s2)),i)) . db by A43, A61, SCMFSA_2:63; (Comput (P2,s2,(i + 1))) . da = (Comput (P2,s2,i)) . db by A10, A17, A62, SCMFSA_2:63; hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A29, A35, A73, A75, A76; ::_thesis: verum end; supposeA77: ( da <> x & x in Int-Locations ) ; ::_thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 then reconsider d = x as Int-Location by AMI_2:def_16; A78: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A43, A61, A77, SCMFSA_2:63; (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A62, A77, SCMFSA_2:63; hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A39, A73, A78; ::_thesis: verum end; end; end; then DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1))) by A22, A34, GRFUNC_1:2; hence DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) by A22, A34, GRFUNC_1:3; ::_thesis: verum end; suppose InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 2 ; ::_thesis: S1[i + 1] then consider da, db being Int-Location such that A79: CurInstr (P1,(Comput (P1,s1,i))) = AddTo (da,db) by SCMFSA_2:31; A80: (Comput (P1,(s1 +* (DataPart s2)),i)) . db = (Comput (P2,s2,i)) . db by A29; A81: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = AddTo (da,db) by A79, COMPOS_0:4; A82: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = succ (IC (Comput (P1,s1,i))) by A79, SCMFSA_2:64; hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A9, A10, A50, A17, A58, A81, SCMFSA_2:64; ::_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 A9, A10, A23, A50, A17, A58, A81, A82, SCMFSA_2:64; ::_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 by A29; now__::_thesis:_for_x_being_set_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 A84: dom (DataPart p) c= Data-Locations by RELAT_1:58; 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 percases ( x in FinSeq-Locations or da = x or ( da <> x & x in Int-Locations ) ) by A33, A85, A84, SCMFSA_2:100, XBOOLE_0:def_3; suppose x in FinSeq-Locations ; ::_thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1 then reconsider d = x as FinSeq-Location by SCMFSA_2:def_5; A86: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A50, A79, SCMFSA_2:64; (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A81, SCMFSA_2:64; hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A33, A52, A85, A86; ::_thesis: verum end; supposeA87: da = x ; ::_thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1 DataPart p c= p by RELAT_1:59; then A88: dom (DataPart p) c= dom p by GRFUNC_1:2; A89: (Comput (P1,s1,(i + 1))) . x = ((Comput (P1,s1,i)) . da) + ((Comput (P1,s1,i)) . db) by A50, A79, A87, SCMFSA_2:64; (Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . da) + ((Comput (P2,s2,i)) . db) by A10, A17, A81, A87, SCMFSA_2:64; then (Comput (P1,s1,(i + 1))) . x = (Comput (P2,s2,(i + 1))) . x by A1, A7, A33, A79, A83, A80, A85, A87, A89, A88, A4, SCMFSA_3:6; hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A33, A45, A85; ::_thesis: verum end; supposeA90: ( da <> x & x in Int-Locations ) ; ::_thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1 then reconsider d = x as Int-Location by AMI_2:def_16; A91: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A50, A79, A90, SCMFSA_2:64; (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A81, A90, SCMFSA_2:64; hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A33, A52, A85, A91; ::_thesis: verum end; end; end; then (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A33, A44, GRFUNC_1:2; hence (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A33, A44, GRFUNC_1:3; ::_thesis: DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) now__::_thesis:_for_x_being_set_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 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 A92: 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 percases ( x in FinSeq-Locations or da = x or ( da <> x & x in Int-Locations ) ) by A22, A92, SCMFSA_2:100, XBOOLE_0:def_3; suppose x in FinSeq-Locations ; ::_thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 then reconsider d = x as FinSeq-Location by SCMFSA_2:def_5; A93: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A43, A79, SCMFSA_2:64; (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A81, SCMFSA_2:64; hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A39, A92, A93; ::_thesis: verum end; supposeA94: da = x ; ::_thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 then A95: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = ((Comput (P1,(s1 +* (DataPart s2)),i)) . da) + ((Comput (P1,(s1 +* (DataPart s2)),i)) . db) by A43, A79, SCMFSA_2:64; (Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . da) + ((Comput (P2,s2,i)) . db) by A10, A17, A81, A94, SCMFSA_2:64; hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A35, A83, A80, A92, A95; ::_thesis: verum end; supposeA96: ( da <> x & x in Int-Locations ) ; ::_thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 then reconsider d = x as Int-Location by AMI_2:def_16; A97: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A43, A79, A96, SCMFSA_2:64; (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A81, A96, SCMFSA_2:64; hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A39, A92, A97; ::_thesis: verum end; end; end; then DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1))) by A22, A34, GRFUNC_1:2; hence DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) by A22, A34, GRFUNC_1:3; ::_thesis: verum end; suppose InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 3 ; ::_thesis: S1[i + 1] then consider da, db being Int-Location such that A98: CurInstr (P1,(Comput (P1,s1,i))) = SubFrom (da,db) by SCMFSA_2:32; A99: (Comput (P1,(s1 +* (DataPart s2)),i)) . db = (Comput (P2,s2,i)) . db by A29; A100: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = SubFrom (da,db) by A98, COMPOS_0:4; A101: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = succ (IC (Comput (P1,s1,i))) by A98, SCMFSA_2:65; hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A9, A10, A50, A17, A58, A100, SCMFSA_2:65; ::_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 A9, A10, A23, A50, A17, A58, A100, A101, SCMFSA_2:65; ::_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))) ) A102: (Comput (P1,(s1 +* (DataPart s2)),i)) . da = (Comput (P2,s2,i)) . da by A29; now__::_thesis:_for_x_being_set_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 A103: dom (DataPart p) c= Data-Locations by RELAT_1:58; 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 A104: 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 percases ( x in FinSeq-Locations or da = x or ( da <> x & x in Int-Locations ) ) by A33, A104, A103, SCMFSA_2:100, XBOOLE_0:def_3; suppose x in FinSeq-Locations ; ::_thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1 then reconsider d = x as FinSeq-Location by SCMFSA_2:def_5; A105: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A50, A98, SCMFSA_2:65; (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A100, SCMFSA_2:65; hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A33, A52, A104, A105; ::_thesis: verum end; supposeA106: da = x ; ::_thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1 DataPart p c= p by RELAT_1:59; then A107: dom (DataPart p) c= dom p by GRFUNC_1:2; A108: (Comput (P1,s1,(i + 1))) . x = ((Comput (P1,s1,i)) . da) - ((Comput (P1,s1,i)) . db) by A50, A98, A106, SCMFSA_2:65; (Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . da) - ((Comput (P2,s2,i)) . db) by A10, A17, A100, A106, SCMFSA_2:65; then ((Comput (P1,s1,i)) . da) - ((Comput (P1,s1,i)) . db) = (Comput (P2,s2,(i + 1))) . x by A1, A7, A33, A98, A102, A99, A104, A106, A107, A4, SCMFSA_3:7; hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A33, A45, A104, A108; ::_thesis: verum end; supposeA109: ( da <> x & x in Int-Locations ) ; ::_thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1 then reconsider d = x as Int-Location by AMI_2:def_16; A110: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A50, A98, A109, SCMFSA_2:65; (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A100, A109, SCMFSA_2:65; hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A33, A52, A104, A110; ::_thesis: verum end; end; end; then (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A33, A44, GRFUNC_1:2; hence (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A33, A44, GRFUNC_1:3; ::_thesis: DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) now__::_thesis:_for_x_being_set_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 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 A111: 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 percases ( x in FinSeq-Locations or da = x or ( da <> x & x in Int-Locations ) ) by A22, A111, SCMFSA_2:100, XBOOLE_0:def_3; suppose x in FinSeq-Locations ; ::_thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 then reconsider d = x as FinSeq-Location by SCMFSA_2:def_5; A112: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A43, A98, SCMFSA_2:65; (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A100, SCMFSA_2:65; hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A39, A111, A112; ::_thesis: verum end; supposeA113: da = x ; ::_thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 then A114: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = ((Comput (P1,(s1 +* (DataPart s2)),i)) . da) - ((Comput (P1,(s1 +* (DataPart s2)),i)) . db) by A43, A98, SCMFSA_2:65; (Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . da) - ((Comput (P2,s2,i)) . db) by A10, A17, A100, A113, SCMFSA_2:65; hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A35, A102, A99, A111, A114; ::_thesis: verum end; supposeA115: ( da <> x & x in Int-Locations ) ; ::_thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 then reconsider d = x as Int-Location by AMI_2:def_16; A116: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A43, A98, A115, SCMFSA_2:65; (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A100, A115, SCMFSA_2:65; hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A39, A111, A116; ::_thesis: verum end; end; end; then DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1))) by A22, A34, GRFUNC_1:2; hence DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) by A22, A34, GRFUNC_1:3; ::_thesis: verum end; suppose InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 4 ; ::_thesis: S1[i + 1] then consider da, db being Int-Location such that A117: CurInstr (P1,(Comput (P1,s1,i))) = MultBy (da,db) by SCMFSA_2:33; A118: (Comput (P1,(s1 +* (DataPart s2)),i)) . db = (Comput (P2,s2,i)) . db by A29; A119: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = MultBy (da,db) by A117, COMPOS_0:4; A120: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = succ (IC (Comput (P1,s1,i))) by A117, SCMFSA_2:66; hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A9, A10, A50, A17, A58, A119, SCMFSA_2:66; ::_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 A9, A10, A23, A50, A17, A58, A119, A120, SCMFSA_2:66; ::_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))) ) A121: (Comput (P1,(s1 +* (DataPart s2)),i)) . da = (Comput (P2,s2,i)) . da by A29; now__::_thesis:_for_x_being_set_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 A122: dom (DataPart p) c= Data-Locations by RELAT_1:58; 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 A123: 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 percases ( x in FinSeq-Locations or da = x or ( da <> x & x in Int-Locations ) ) by A33, A123, A122, SCMFSA_2:100, XBOOLE_0:def_3; suppose x in FinSeq-Locations ; ::_thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1 then reconsider d = x as FinSeq-Location by SCMFSA_2:def_5; A124: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A50, A117, SCMFSA_2:66; (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A119, SCMFSA_2:66; hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A33, A52, A123, A124; ::_thesis: verum end; supposeA125: da = x ; ::_thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1 DataPart p c= p by RELAT_1:59; then A126: dom (DataPart p) c= dom p by GRFUNC_1:2; A127: (Comput (P1,s1,(i + 1))) . x = ((Comput (P1,s1,i)) . da) * ((Comput (P1,s1,i)) . db) by A50, A117, A125, SCMFSA_2:66; (Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . da) * ((Comput (P2,s2,i)) . db) by A10, A17, A119, A125, SCMFSA_2:66; then (Comput (P1,s1,(i + 1))) . x = (Comput (P2,s2,(i + 1))) . x by A1, A7, A33, A117, A121, A118, A123, A125, A127, A126, A4, SCMFSA_3:8; hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A33, A45, A123; ::_thesis: verum end; supposeA128: ( da <> x & x in Int-Locations ) ; ::_thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1 then reconsider d = x as Int-Location by AMI_2:def_16; A129: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A50, A117, A128, SCMFSA_2:66; (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A119, A128, SCMFSA_2:66; hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A33, A52, A123, A129; ::_thesis: verum end; end; end; then (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A33, A44, GRFUNC_1:2; hence (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A33, A44, GRFUNC_1:3; ::_thesis: DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) now__::_thesis:_for_x_being_set_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 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 A130: 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 percases ( x in FinSeq-Locations or da = x or ( da <> x & x in Int-Locations ) ) by A22, A130, SCMFSA_2:100, XBOOLE_0:def_3; suppose x in FinSeq-Locations ; ::_thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 then reconsider d = x as FinSeq-Location by SCMFSA_2:def_5; A131: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A43, A117, SCMFSA_2:66; (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A119, SCMFSA_2:66; hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A39, A130, A131; ::_thesis: verum end; supposeA132: da = x ; ::_thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 then A133: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = ((Comput (P1,(s1 +* (DataPart s2)),i)) . da) * ((Comput (P1,(s1 +* (DataPart s2)),i)) . db) by A43, A117, SCMFSA_2:66; (Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . da) * ((Comput (P2,s2,i)) . db) by A10, A17, A119, A132, SCMFSA_2:66; hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A35, A121, A118, A130, A133; ::_thesis: verum end; supposeA134: ( da <> x & x in Int-Locations ) ; ::_thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 then reconsider d = x as Int-Location by AMI_2:def_16; A135: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A43, A117, A134, SCMFSA_2:66; (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A119, A134, SCMFSA_2:66; hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A39, A130, A135; ::_thesis: verum end; end; end; then DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1))) by A22, A34, GRFUNC_1:2; hence DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) by A22, A34, GRFUNC_1:3; ::_thesis: verum end; suppose InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 5 ; ::_thesis: S1[i + 1] then consider da, db being Int-Location such that A136: CurInstr (P1,(Comput (P1,s1,i))) = Divide (da,db) by SCMFSA_2:34; A137: (Comput (P1,(s1 +* (DataPart s2)),i)) . db = (Comput (P2,s2,i)) . db by A29; A138: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = Divide (da,db) by A136, COMPOS_0:4; A139: (Comput (P1,(s1 +* (DataPart s2)),i)) . da = (Comput (P2,s2,i)) . da by A29; percases ( da <> db or da = db ) ; supposeA140: da <> db ; ::_thesis: S1[i + 1] A141: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = succ (IC (Comput (P1,s1,i))) by A136, SCMFSA_2:67; hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A9, A10, A50, A17, A58, A138, SCMFSA_2:67; ::_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 A9, A10, A23, A50, A17, A58, A138, A141, SCMFSA_2:67; ::_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_set_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 A142: dom (DataPart p) c= Data-Locations by RELAT_1:58; 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 A143: 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 percases ( ( db <> x & x in FinSeq-Locations ) or da = x or db = x or ( da <> x & db <> x & x in Int-Locations ) ) by A33, A143, A142, SCMFSA_2:100, XBOOLE_0:def_3; suppose ( db <> x & x in FinSeq-Locations ) ; ::_thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1 then reconsider d = x as FinSeq-Location by SCMFSA_2:def_5; A144: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A50, A136, SCMFSA_2:67; (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A138, SCMFSA_2:67; hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A33, A52, A143, A144; ::_thesis: verum end; supposeA145: da = x ; ::_thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1 DataPart p c= p by RELAT_1:59; then dom (DataPart p) c= dom p by GRFUNC_1:2; then A146: ((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, A7, A33, A136, A140, A143, A145, A4, SCMFSA_3:9; A147: (Comput (P1,s1,(i + 1))) . x = ((Comput (P1,s1,i)) . da) div ((Comput (P1,s1,i)) . db) by A50, A136, A140, A145, SCMFSA_2:67; (Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . da) div ((Comput (P2,s2,i)) . db) by A10, A17, A138, A140, A145, SCMFSA_2:67; hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = (Comput (P2,s2,(i + 1))) . x by A139, A137, A143, A147, A146, FUNCT_1:47 .= ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A33, A44, A143, FUNCT_1:47 ; ::_thesis: verum end; supposeA148: db = x ; ::_thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1 DataPart p c= p by RELAT_1:59; then A149: dom (DataPart p) c= dom p by GRFUNC_1:2; A150: (Comput (P1,s1,(i + 1))) . x = ((Comput (P1,s1,i)) . da) mod ((Comput (P1,s1,i)) . db) by A50, A136, A148, SCMFSA_2:67; (Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . da) mod ((Comput (P2,s2,i)) . db) by A10, A17, A138, A148, SCMFSA_2:67; then (Comput (P1,s1,(i + 1))) . x = (Comput (P2,s2,(i + 1))) . x by A1, A7, A33, A136, A139, A137, A143, A148, A150, A149, A4, SCMFSA_3:10; hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A33, A45, A143; ::_thesis: verum end; supposeA151: ( da <> x & db <> x & x in Int-Locations ) ; ::_thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1 then reconsider d = x as Int-Location by AMI_2:def_16; A152: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A50, A136, A151, SCMFSA_2:67; (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A138, A151, SCMFSA_2:67; hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A33, A52, A143, A152; ::_thesis: verum end; end; end; then (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A33, A44, GRFUNC_1:2; hence (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A33, A44, GRFUNC_1:3; ::_thesis: DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) now__::_thesis:_for_x_being_set_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 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 A153: 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 percases ( x in FinSeq-Locations or da = x or db = x or ( da <> x & db <> x & x in Int-Locations ) ) by A22, A153, SCMFSA_2:100, XBOOLE_0:def_3; suppose x in FinSeq-Locations ; ::_thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 then reconsider d = x as FinSeq-Location by SCMFSA_2:def_5; A154: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A43, A136, SCMFSA_2:67; (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A138, SCMFSA_2:67; hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A39, A153, A154; ::_thesis: verum end; supposeA155: da = x ; ::_thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 then A156: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = ((Comput (P1,(s1 +* (DataPart s2)),i)) . da) div ((Comput (P1,(s1 +* (DataPart s2)),i)) . db) by A43, A136, A140, SCMFSA_2:67; (Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . da) div ((Comput (P2,s2,i)) . db) by A10, A17, A138, A140, A155, SCMFSA_2:67; hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A35, A139, A137, A153, A156; ::_thesis: verum end; supposeA157: db = x ; ::_thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 then A158: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = ((Comput (P1,(s1 +* (DataPart s2)),i)) . da) mod ((Comput (P1,(s1 +* (DataPart s2)),i)) . db) by A43, A136, SCMFSA_2:67; (Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . da) mod ((Comput (P2,s2,i)) . db) by A10, A17, A138, A157, SCMFSA_2:67; hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A35, A139, A137, A153, A158; ::_thesis: verum end; supposeA159: ( da <> x & db <> x & x in Int-Locations ) ; ::_thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 then reconsider d = x as Int-Location by AMI_2:def_16; A160: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A43, A136, A159, SCMFSA_2:67; (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A138, A159, SCMFSA_2:67; hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A39, A153, A160; ::_thesis: verum end; end; end; then DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1))) by A22, A34, GRFUNC_1:2; hence DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) by A22, A34, GRFUNC_1:3; ::_thesis: verum end; supposeA161: da = db ; ::_thesis: S1[i + 1] then A162: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = succ (IC (Comput (P1,s1,i))) by A136, SCMFSA_2:68; hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A9, A10, A50, A17, A58, A138, A161, SCMFSA_2:68; ::_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 A9, A10, A23, A50, A17, A58, A138, A161, A162, SCMFSA_2:68; ::_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_set_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 A163: dom (DataPart p) c= Data-Locations by RELAT_1:58; 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 A164: 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 percases ( x in FinSeq-Locations or da = x or ( da <> x & x in Int-Locations ) ) by A33, A164, A163, SCMFSA_2:100, XBOOLE_0:def_3; suppose x in FinSeq-Locations ; ::_thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1 then reconsider d = x as FinSeq-Location by SCMFSA_2:def_5; A165: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A50, A136, A161, SCMFSA_2:68; (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A138, A161, SCMFSA_2:68; hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A33, A52, A164, A165; ::_thesis: verum end; supposeA166: da = x ; ::_thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1 A167: ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x = (Comput (P2,s2,(i + 1))) . x by A33, A44, A164, FUNCT_1:47; A168: ((Comput (P1,s1,i)) | (dom (DataPart p))) . x = (Comput (P1,s1,i)) . x by A33, A49, A164, FUNCT_1:47; A169: ((Comput (P2,s2,i)) | (dom (DataPart p))) . x = (Comput (P2,s2,i)) . x by A33, A51, A164, FUNCT_1:47; A170: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = (Comput (P1,s1,(i + 1))) . x by A164, FUNCT_1:47; (Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . da) mod ((Comput (P2,s2,i)) . db) by A10, A17, A138, A161, A166, SCMFSA_2:68; hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A11, A50, A136, A161, A166, A168, A169, A170, A167, SCMFSA_2:68; ::_thesis: verum end; supposeA171: ( da <> x & x in Int-Locations ) ; ::_thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1 then reconsider d = x as Int-Location by AMI_2:def_16; A172: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A50, A136, A161, A171, SCMFSA_2:68; (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A138, A161, A171, SCMFSA_2:68; hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A33, A52, A164, A172; ::_thesis: verum end; end; end; then (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A33, A44, GRFUNC_1:2; hence (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A33, A44, GRFUNC_1:3; ::_thesis: DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) now__::_thesis:_for_x_being_set_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 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 A173: 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 percases ( x in FinSeq-Locations or da = x or ( da <> x & x in Int-Locations ) ) by A22, A173, SCMFSA_2:100, XBOOLE_0:def_3; suppose x in FinSeq-Locations ; ::_thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 then reconsider d = x as FinSeq-Location by SCMFSA_2:def_5; A174: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A43, A136, A161, SCMFSA_2:68; (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A138, A161, SCMFSA_2:68; hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A39, A173, A174; ::_thesis: verum end; supposeA175: da = x ; ::_thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 then A176: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = ((Comput (P1,(s1 +* (DataPart s2)),i)) . da) mod ((Comput (P1,(s1 +* (DataPart s2)),i)) . db) by A43, A136, A161, SCMFSA_2:68; (Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . da) mod ((Comput (P2,s2,i)) . db) by A10, A17, A138, A161, A175, SCMFSA_2:68; hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A35, A139, A137, A173, A176; ::_thesis: verum end; supposeA177: ( da <> x & x in Int-Locations ) ; ::_thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 then reconsider d = x as Int-Location by AMI_2:def_16; A178: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A43, A136, A161, A177, SCMFSA_2:68; (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A138, A161, A177, SCMFSA_2:68; hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A39, A173, A178; ::_thesis: verum end; end; end; then DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1))) by A22, A34, GRFUNC_1:2; hence DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) by A22, A34, 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 Element of NAT such that A179: CurInstr (P1,(Comput (P1,s1,i))) = goto loc by SCMFSA_2:35; A180: CurInstr (P2,(Comput (P2,s2,i))) = goto (loc + k) by A10, A179, SCMFSA_4:1; thus (IC (Comput (P1,s1,(i + 1)))) + k = loc + k by A50, A179, SCMFSA_2:69 .= IC (Comput (P2,s2,(i + 1))) by A17, A180, SCMFSA_2:69 ; ::_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 A23; ::_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_set_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 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 A181: 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 Int-Locations or x in FinSeq-Locations ) by A33, A181, SCMFSA_2:100, XBOOLE_0:def_3; then A182: ( x is Int-Location or x is FinSeq-Location ) by AMI_2:def_16, SCMFSA_2:def_5; then A183: (Comput (P2,s2,(i + 1))) . x = (Comput (P2,s2,i)) . x by A17, A180, SCMFSA_2:69; (Comput (P1,s1,(i + 1))) . x = (Comput (P1,s1,i)) . x by A50, A179, A182, SCMFSA_2:69; hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A33, A52, A181, A183; ::_thesis: verum end; then (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A33, A44, GRFUNC_1:2; hence (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A33, A44, GRFUNC_1:3; ::_thesis: DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) now__::_thesis:_for_x_being_set_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 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 A184: 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 ( x in Int-Locations or x in FinSeq-Locations ) by A22, SCMFSA_2:100, XBOOLE_0:def_3; then A185: ( x is Int-Location or x is FinSeq-Location ) by AMI_2:def_16, SCMFSA_2:def_5; then A186: (Comput (P2,s2,(i + 1))) . x = (Comput (P2,s2,i)) . x by A17, A180, SCMFSA_2:69; (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = (Comput (P1,(s1 +* (DataPart s2)),i)) . x by A43, A179, A185, SCMFSA_2:69; hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A39, A184, A186; ::_thesis: verum end; then DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1))) by A22, A34, GRFUNC_1:2; hence DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) by A22, A34, GRFUNC_1:3; ::_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 Int-Location such that A187: CurInstr (P1,(Comput (P1,s1,i))) = da =0_goto loc by SCMFSA_2:36; A188: 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_=_succ_(IC_(Comput_(P2,s2,i)))_)_) percases ( (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, A187, SCMFSA_2:70; ::_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 A9, A50, A58, A187, SCMFSA_2:70; ::_thesis: verum end; end; end; A189: CurInstr (P2,(Comput (P2,s2,i))) = da =0_goto (loc + k) by A10, A187, SCMFSA_4:2; A190: 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)))_=_succ_(IC_(Comput_(P2,s2,i)))_)_) percases ( (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 A17, A189, SCMFSA_2:70; ::_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 A17, A189, SCMFSA_2:70; ::_thesis: verum end; end; end; A191: (Comput (P1,(s1 +* (DataPart s2)),i)) . da = (Comput (P2,s2,i)) . da by A29; A192: now__::_thesis:_(IC_(Comput_(P1,s1,(i_+_1))))_+_k_=_IC_(Comput_(P2,s2,(i_+_1))) percases ( 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 A1, A7, A187, A191, A188, A190, A4, SCMFSA_3:11; ::_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 A9, A58, A188, A190; ::_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 A23, A192; ::_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_set_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 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 A193: 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 Int-Locations or x in FinSeq-Locations ) by A33, A193, SCMFSA_2:100, XBOOLE_0:def_3; then A194: ( x is Int-Location or x is FinSeq-Location ) by AMI_2:def_16, SCMFSA_2:def_5; then A195: (Comput (P2,s2,(i + 1))) . x = (Comput (P2,s2,i)) . x by A17, A189, SCMFSA_2:70; (Comput (P1,s1,(i + 1))) . x = (Comput (P1,s1,i)) . x by A50, A187, A194, SCMFSA_2:70; hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A33, A52, A193, A195; ::_thesis: verum end; then (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A33, A44, GRFUNC_1:2; hence (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A33, A44, GRFUNC_1:3; ::_thesis: DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) now__::_thesis:_for_x_being_set_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 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 A196: 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 ( x in Int-Locations or x in FinSeq-Locations ) by A22, SCMFSA_2:100, XBOOLE_0:def_3; then A197: ( x is Int-Location or x is FinSeq-Location ) by AMI_2:def_16, SCMFSA_2:def_5; then A198: (Comput (P2,s2,(i + 1))) . x = (Comput (P2,s2,i)) . x by A17, A189, SCMFSA_2:70; (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = (Comput (P1,(s1 +* (DataPart s2)),i)) . x by A43, A187, A197, SCMFSA_2:70; hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A39, A196, A198; ::_thesis: verum end; then DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1))) by A22, A34, GRFUNC_1:2; hence DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) by A22, A34, GRFUNC_1:3; ::_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 Int-Location such that A199: CurInstr (P1,(Comput (P1,s1,i))) = da >0_goto loc by SCMFSA_2:37; A200: 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_=_succ_(IC_(Comput_(P2,s2,i)))_)_) percases ( (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, A199, SCMFSA_2:71; ::_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 A9, A50, A58, A199, SCMFSA_2:71; ::_thesis: verum end; end; end; A201: CurInstr (P2,(Comput (P2,s2,i))) = da >0_goto (loc + k) by A10, A199, SCMFSA_4:3; A202: 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)))_=_succ_(IC_(Comput_(P2,s2,i)))_)_) percases ( (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 A17, A201, SCMFSA_2:71; ::_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 A17, A201, SCMFSA_2:71; ::_thesis: verum end; end; end; A203: (Comput (P1,(s1 +* (DataPart s2)),i)) . da = (Comput (P2,s2,i)) . da by A29; A204: now__::_thesis:_(IC_(Comput_(P1,s1,(i_+_1))))_+_k_=_IC_(Comput_(P2,s2,(i_+_1))) percases ( 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 A1, A7, A199, A203, A200, A202, A4, SCMFSA_3:12; ::_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 A9, A58, A200, A202; ::_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 A23, A204; ::_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_set_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 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 A205: 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 Int-Locations or x in FinSeq-Locations ) by A33, A205, SCMFSA_2:100, XBOOLE_0:def_3; then A206: ( x is Int-Location or x is FinSeq-Location ) by AMI_2:def_16, SCMFSA_2:def_5; then A207: (Comput (P2,s2,(i + 1))) . x = (Comput (P2,s2,i)) . x by A17, A201, SCMFSA_2:71; (Comput (P1,s1,(i + 1))) . x = (Comput (P1,s1,i)) . x by A50, A199, A206, SCMFSA_2:71; hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A33, A52, A205, A207; ::_thesis: verum end; then (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A33, A44, GRFUNC_1:2; hence (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A33, A44, GRFUNC_1:3; ::_thesis: DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) now__::_thesis:_for_x_being_set_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 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 A208: 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 ( x in Int-Locations or x in FinSeq-Locations ) by A22, SCMFSA_2:100, XBOOLE_0:def_3; then A209: ( x is Int-Location or x is FinSeq-Location ) by AMI_2:def_16, SCMFSA_2:def_5; then A210: (Comput (P2,s2,(i + 1))) . x = (Comput (P2,s2,i)) . x by A17, A201, SCMFSA_2:71; (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = (Comput (P1,(s1 +* (DataPart s2)),i)) . x by A43, A199, A209, SCMFSA_2:71; hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A39, A208, A210; ::_thesis: verum end; then DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1))) by A22, A34, GRFUNC_1:2; hence DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) by A22, A34, GRFUNC_1:3; ::_thesis: verum end; suppose InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 9 ; ::_thesis: S1[i + 1] then consider db, da being Int-Location, f being FinSeq-Location such that A211: CurInstr (P1,(Comput (P1,s1,i))) = da := (f,db) by SCMFSA_2:38; A212: (Comput (P1,(s1 +* (DataPart s2)),i)) . f = (Comput (P2,s2,i)) . f by A19; A213: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = da := (f,db) by A211, COMPOS_0:4; A214: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = succ (IC (Comput (P1,s1,i))) by A211, SCMFSA_2:72; hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A9, A10, A50, A17, A58, A213, SCMFSA_2:72; ::_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 A9, A10, A23, A50, A17, A58, A213, A214, SCMFSA_2:72; ::_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))) ) A215: (Comput (P1,(s1 +* (DataPart s2)),i)) . db = (Comput (P2,s2,i)) . db by A29; now__::_thesis:_for_x_being_set_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 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 ) A216: dom (DataPart p) c= Data-Locations by RELAT_1:58; assume A217: 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 percases ( x in FinSeq-Locations or da = x or ( da <> x & x in Int-Locations ) ) by A33, A217, A216, SCMFSA_2:100, XBOOLE_0:def_3; suppose x in FinSeq-Locations ; ::_thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1 then reconsider d = x as FinSeq-Location by SCMFSA_2:def_5; A218: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A50, A211, SCMFSA_2:72; (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A213, SCMFSA_2:72; hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A33, A52, A217, A218; ::_thesis: verum end; supposeA219: da = x ; ::_thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1 then consider k1 being Element of NAT such that A220: k1 = abs ((Comput (P1,s1,i)) . db) and A221: (Comput (P1,s1,(i + 1))) . x = ((Comput (P1,s1,i)) . f) /. k1 by A50, A211, SCMFSA_2:72; consider k2 being Element of NAT such that A222: k2 = abs ((Comput (P2,s2,i)) . db) and A223: (Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . f) /. k2 by A10, A17, A213, A219, SCMFSA_2:72; DataPart p c= p by RELAT_1:59; then dom (DataPart p) c= dom p by GRFUNC_1:2; then ((Comput (P1,(s1 +* (DataPart s2)),i)) . f) /. k2 = ((Comput (P1,s1,i)) . f) /. k1 by A1, A7, A33, A211, A215, A217, A219, A220, A222, A4, SCMFSA_3:13; hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A33, A45, A212, A217, A221, A223; ::_thesis: verum end; supposeA224: ( da <> x & x in Int-Locations ) ; ::_thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1 then reconsider d = x as Int-Location by AMI_2:def_16; A225: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A50, A211, A224, SCMFSA_2:72; (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A213, A224, SCMFSA_2:72; hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A33, A52, A217, A225; ::_thesis: verum end; end; end; then (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A33, A44, GRFUNC_1:2; hence (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A33, A44, GRFUNC_1:3; ::_thesis: DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) now__::_thesis:_for_x_being_set_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 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 A226: 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 percases ( x in FinSeq-Locations or da = x or ( da <> x & x in Int-Locations ) ) by A22, A226, SCMFSA_2:100, XBOOLE_0:def_3; suppose x in FinSeq-Locations ; ::_thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 then reconsider f = x as FinSeq-Location by SCMFSA_2:def_5; A227: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . f = (Comput (P1,(s1 +* (DataPart s2)),i)) . f by A43, A211, SCMFSA_2:72; (Comput (P2,s2,(i + 1))) . f = (Comput (P2,s2,i)) . f by A10, A17, A213, SCMFSA_2:72; hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A39, A226, A227; ::_thesis: verum end; supposeA228: da = x ; ::_thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 then A229: ex k1 being Element of NAT st ( k1 = abs ((Comput (P1,(s1 +* (DataPart s2)),i)) . db) & (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = ((Comput (P1,(s1 +* (DataPart s2)),i)) . f) /. k1 ) by A43, A211, SCMFSA_2:72; ex k2 being Element of NAT st ( k2 = abs ((Comput (P2,s2,i)) . db) & (Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . f) /. k2 ) by A10, A17, A213, A228, SCMFSA_2:72; hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A35, A215, A212, A226, A229; ::_thesis: verum end; supposeA230: ( da <> x & x in Int-Locations ) ; ::_thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 then reconsider d = x as Int-Location by AMI_2:def_16; A231: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A43, A211, A230, SCMFSA_2:72; (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A213, A230, SCMFSA_2:72; hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A39, A226, A231; ::_thesis: verum end; end; end; then DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1))) by A22, A34, GRFUNC_1:2; hence DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) by A22, A34, GRFUNC_1:3; ::_thesis: verum end; suppose InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 10 ; ::_thesis: S1[i + 1] then consider db, da being Int-Location, f being FinSeq-Location such that A232: CurInstr (P1,(Comput (P1,s1,i))) = (f,db) := da by SCMFSA_2:39; A233: (Comput (P1,(s1 +* (DataPart s2)),i)) . f = (Comput (P2,s2,i)) . f by A19; A234: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = (f,db) := da by A232, COMPOS_0:4; A235: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = succ (IC (Comput (P1,s1,i))) by A232, SCMFSA_2:73; hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A9, A10, A50, A17, A58, A234, SCMFSA_2:73; ::_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))) ) A236: (Comput (P1,(s1 +* (DataPart s2)),i)) . da = (Comput (P2,s2,i)) . da by A29; thus IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A9, A10, A23, A50, A17, A58, A234, A235, SCMFSA_2:73; ::_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))) ) A237: (Comput (P1,(s1 +* (DataPart s2)),i)) . db = (Comput (P2,s2,i)) . db by A29; now__::_thesis:_for_x_being_set_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 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 ) A238: dom (DataPart p) c= Data-Locations by RELAT_1:58; assume A239: 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 percases ( x in Int-Locations or f = x or ( f <> x & x in FinSeq-Locations ) ) by A33, A239, A238, SCMFSA_2:100, XBOOLE_0:def_3; suppose x in Int-Locations ; ::_thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1 then reconsider d = x as Int-Location by AMI_2:def_16; A240: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A50, A232, SCMFSA_2:73; (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A234, SCMFSA_2:73; hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A33, A52, A239, A240; ::_thesis: verum end; supposeA241: f = x ; ::_thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1 then consider k1 being Element of NAT such that A242: k1 = abs ((Comput (P1,s1,i)) . db) and A243: (Comput (P1,s1,(i + 1))) . x = ((Comput (P1,s1,i)) . f) +* (k1,((Comput (P1,s1,i)) . da)) by A50, A232, SCMFSA_2:73; consider k2 being Element of NAT such that A244: k2 = abs ((Comput (P2,s2,i)) . db) and A245: (Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . f) +* (k2,((Comput (P2,s2,i)) . da)) by A10, A17, A234, A241, SCMFSA_2:73; DataPart p c= p by RELAT_1:59; then dom (DataPart p) c= dom p by GRFUNC_1:2; then ((Comput (P1,(s1 +* (DataPart s2)),i)) . f) +* (k2,((Comput (P1,(s1 +* (DataPart s2)),i)) . da)) = ((Comput (P1,s1,i)) . f) +* (k1,((Comput (P1,s1,i)) . da)) by A1, A7, A33, A232, A237, A239, A241, A242, A244, A4, SCMFSA_3:14; hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A33, A45, A236, A233, A239, A243, A245; ::_thesis: verum end; supposeA246: ( f <> x & x in FinSeq-Locations ) ; ::_thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1 then reconsider d = x as FinSeq-Location by SCMFSA_2:def_5; A247: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A50, A232, A246, SCMFSA_2:73; (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A234, A246, SCMFSA_2:73; hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A33, A52, A239, A247; ::_thesis: verum end; end; end; then (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A33, A44, GRFUNC_1:2; hence (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A33, A44, GRFUNC_1:3; ::_thesis: DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) now__::_thesis:_for_x_being_set_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 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 A248: 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 percases ( x in Int-Locations or f = x or ( f <> x & x in FinSeq-Locations ) ) by A22, A248, SCMFSA_2:100, XBOOLE_0:def_3; suppose x in Int-Locations ; ::_thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 then reconsider f = x as Int-Location by AMI_2:def_16; A249: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . f = (Comput (P1,(s1 +* (DataPart s2)),i)) . f by A43, A232, SCMFSA_2:73; (Comput (P2,s2,(i + 1))) . f = (Comput (P2,s2,i)) . f by A10, A17, A234, SCMFSA_2:73; hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A39, A248, A249; ::_thesis: verum end; supposeA250: f = x ; ::_thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 then A251: ex k1 being Element of NAT st ( k1 = abs ((Comput (P1,(s1 +* (DataPart s2)),i)) . db) & (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = ((Comput (P1,(s1 +* (DataPart s2)),i)) . f) +* (k1,((Comput (P1,(s1 +* (DataPart s2)),i)) . da)) ) by A43, A232, SCMFSA_2:73; ex k2 being Element of NAT st ( k2 = abs ((Comput (P2,s2,i)) . db) & (Comput (P2,s2,(i + 1))) . x = ((Comput (P2,s2,i)) . f) +* (k2,((Comput (P2,s2,i)) . da)) ) by A10, A17, A234, A250, SCMFSA_2:73; hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A35, A237, A236, A233, A248, A251; ::_thesis: verum end; supposeA252: ( f <> x & x in FinSeq-Locations ) ; ::_thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 then reconsider d = x as FinSeq-Location by SCMFSA_2:def_5; A253: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A43, A232, A252, SCMFSA_2:73; (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A234, A252, SCMFSA_2:73; hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A39, A248, A253; ::_thesis: verum end; end; end; then DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1))) by A22, A34, GRFUNC_1:2; hence DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) by A22, A34, GRFUNC_1:3; ::_thesis: verum end; suppose InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 11 ; ::_thesis: S1[i + 1] then consider da being Int-Location, f being FinSeq-Location such that A254: CurInstr (P1,(Comput (P1,s1,i))) = da :=len f by SCMFSA_2:40; A255: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = da :=len f by A254, COMPOS_0:4; A256: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = succ (IC (Comput (P1,s1,i))) by A254, SCMFSA_2:74; hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A9, A10, A50, A17, A58, A255, SCMFSA_2:74; ::_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 A9, A10, A23, A50, A17, A58, A255, A256, SCMFSA_2:74; ::_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))) ) A257: (Comput (P1,(s1 +* (DataPart s2)),i)) . f = (Comput (P2,s2,i)) . f by A19; now__::_thesis:_for_x_being_set_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 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 ) A258: dom (DataPart p) c= Data-Locations by RELAT_1:58; assume A259: 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 percases ( x in FinSeq-Locations or da = x or ( da <> x & x in Int-Locations ) ) by A33, A259, A258, SCMFSA_2:100, XBOOLE_0:def_3; suppose x in FinSeq-Locations ; ::_thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1 then reconsider d = x as FinSeq-Location by SCMFSA_2:def_5; A260: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A50, A254, SCMFSA_2:74; (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A255, SCMFSA_2:74; hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A33, A52, A259, A260; ::_thesis: verum end; supposeA261: da = x ; ::_thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1 DataPart p c= p by RELAT_1:59; then dom (DataPart p) c= dom p by GRFUNC_1:2; then A262: len ((Comput (P1,(s1 +* (DataPart s2)),i)) . f) = len ((Comput (P1,s1,i)) . f) by A1, A7, A33, A254, A259, A261, A4, SCMFSA_3:15; A263: (Comput (P1,s1,(i + 1))) . x = len ((Comput (P1,s1,i)) . f) by A50, A254, A261, SCMFSA_2:74; (Comput (P2,s2,(i + 1))) . x = len ((Comput (P2,s2,i)) . f) by A10, A17, A255, A261, SCMFSA_2:74; hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A33, A45, A257, A259, A263, A262; ::_thesis: verum end; supposeA264: ( da <> x & x in Int-Locations ) ; ::_thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1 then reconsider d = x as Int-Location by AMI_2:def_16; A265: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A50, A254, A264, SCMFSA_2:74; (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A255, A264, SCMFSA_2:74; hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A33, A52, A259, A265; ::_thesis: verum end; end; end; then (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A33, A44, GRFUNC_1:2; hence (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A33, A44, GRFUNC_1:3; ::_thesis: DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) now__::_thesis:_for_x_being_set_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 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 A266: 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 percases ( x in FinSeq-Locations or da = x or ( da <> x & x in Int-Locations ) ) by A22, A266, SCMFSA_2:100, XBOOLE_0:def_3; suppose x in FinSeq-Locations ; ::_thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 then reconsider f = x as FinSeq-Location by SCMFSA_2:def_5; A267: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . f = (Comput (P1,(s1 +* (DataPart s2)),i)) . f by A43, A254, SCMFSA_2:74; (Comput (P2,s2,(i + 1))) . f = (Comput (P2,s2,i)) . f by A10, A17, A255, SCMFSA_2:74; hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A39, A266, A267; ::_thesis: verum end; supposeA268: da = x ; ::_thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 then A269: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = len ((Comput (P1,(s1 +* (DataPart s2)),i)) . f) by A43, A254, SCMFSA_2:74; (Comput (P2,s2,(i + 1))) . x = len ((Comput (P2,s2,i)) . f) by A10, A17, A255, A268, SCMFSA_2:74; hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A35, A257, A266, A269; ::_thesis: verum end; supposeA270: ( da <> x & x in Int-Locations ) ; ::_thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 then reconsider d = x as Int-Location by AMI_2:def_16; A271: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A43, A254, A270, SCMFSA_2:74; (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A255, A270, SCMFSA_2:74; hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A39, A266, A271; ::_thesis: verum end; end; end; then DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1))) by A22, A34, GRFUNC_1:2; hence DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) by A22, A34, GRFUNC_1:3; ::_thesis: verum end; suppose InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 12 ; ::_thesis: S1[i + 1] then consider da being Int-Location, f being FinSeq-Location such that A272: CurInstr (P1,(Comput (P1,s1,i))) = f :=<0,...,0> da by SCMFSA_2:41; A273: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = f :=<0,...,0> da by A272, COMPOS_0:4; A274: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = succ (IC (Comput (P1,s1,i))) by A272, SCMFSA_2:75; hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A9, A10, A50, A17, A58, A273, SCMFSA_2:75; ::_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 A9, A10, A23, A50, A17, A58, A273, A274, SCMFSA_2:75; ::_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))) ) A275: (Comput (P1,(s1 +* (DataPart s2)),i)) . da = (Comput (P2,s2,i)) . da by A29; now__::_thesis:_for_x_being_set_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 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 ) A276: dom (DataPart p) c= Data-Locations by RELAT_1:58; assume A277: 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 percases ( x in Int-Locations or f = x or ( f <> x & x in FinSeq-Locations ) ) by A33, A277, A276, SCMFSA_2:100, XBOOLE_0:def_3; suppose x in Int-Locations ; ::_thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1 then reconsider d = x as Int-Location by AMI_2:def_16; A278: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A50, A272, SCMFSA_2:75; (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A273, SCMFSA_2:75; hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A33, A52, A277, A278; ::_thesis: verum end; supposeA279: f = x ; ::_thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1 then consider k1 being Element of NAT such that A280: k1 = abs ((Comput (P1,s1,i)) . da) and A281: (Comput (P1,s1,(i + 1))) . x = k1 |-> 0 by A50, A272, SCMFSA_2:75; consider k2 being Element of NAT such that A282: k2 = abs ((Comput (P2,s2,i)) . da) and A283: (Comput (P2,s2,(i + 1))) . x = k2 |-> 0 by A10, A17, A273, A279, SCMFSA_2:75; DataPart p c= p by RELAT_1:59; then dom (DataPart p) c= dom p by GRFUNC_1:2; then k2 |-> 0 = k1 |-> 0 by A1, A7, A33, A272, A275, A277, A279, A280, A282, A4, SCMFSA_3:16; hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A33, A45, A277, A281, A283; ::_thesis: verum end; supposeA284: ( f <> x & x in FinSeq-Locations ) ; ::_thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1 then reconsider d = x as FinSeq-Location by SCMFSA_2:def_5; A285: (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d by A50, A272, A284, SCMFSA_2:75; (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A273, A284, SCMFSA_2:75; hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A33, A52, A277, A285; ::_thesis: verum end; end; end; then (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A33, A44, GRFUNC_1:2; hence (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A33, A44, GRFUNC_1:3; ::_thesis: DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) now__::_thesis:_for_x_being_set_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 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 A286: 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 percases ( x in Int-Locations or f = x or ( f <> x & x in FinSeq-Locations ) ) by A22, A286, SCMFSA_2:100, XBOOLE_0:def_3; suppose x in Int-Locations ; ::_thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 then reconsider f = x as Int-Location by AMI_2:def_16; A287: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . f = (Comput (P1,(s1 +* (DataPart s2)),i)) . f by A43, A272, SCMFSA_2:75; (Comput (P2,s2,(i + 1))) . f = (Comput (P2,s2,i)) . f by A10, A17, A273, SCMFSA_2:75; hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A39, A286, A287; ::_thesis: verum end; supposeA288: f = x ; ::_thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 then A289: ex k1 being Element of NAT st ( k1 = abs ((Comput (P1,(s1 +* (DataPart s2)),i)) . da) & (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = k1 |-> 0 ) by A43, A272, SCMFSA_2:75; ex k2 being Element of NAT st ( k2 = abs ((Comput (P2,s2,i)) . da) & (Comput (P2,s2,(i + 1))) . x = k2 |-> 0 ) by A10, A17, A273, A288, SCMFSA_2:75; hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A35, A275, A286, A289; ::_thesis: verum end; supposeA290: ( f <> x & x in FinSeq-Locations ) ; ::_thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 then reconsider d = x as FinSeq-Location by SCMFSA_2:def_5; A291: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d by A43, A272, A290, SCMFSA_2:75; (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d by A10, A17, A273, A290, SCMFSA_2:75; hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A39, A286, A291; ::_thesis: verum end; end; end; then DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1))) by A22, A34, GRFUNC_1:2; hence DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) by A22, A34, GRFUNC_1:3; ::_thesis: verum end; end; end; reconsider ii = IC p as Element of NAT ; A292: 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, A292, 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 ; A293: IC p = IC s1 by A1, A3, GRFUNC_1:2; then IC p = IC (Comput (P1,s1,0)) ; then A294: loc in dom q by A6, A1, AMISTD_5:def_4; A295: (IC p) + k in dom (Reloc (q,k)) by A294, COMPOS_1:46; A296: IC in dom (IncIC (p,k)) by MEMSTR_0:52; A297: q . (IC p) = P1 . (IC s1) by A293, A294, A4, GRFUNC_1:2; dom P2 = NAT by PARTFUN1:def_2; then A298: 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, A296, GRFUNC_1:2 .= P2 . ((IC p) + k) by MEMSTR_0:53 .= P2 . ((IC p) + k) .= (Reloc (q,k)) . ((IC p) + k) by A295, A4, GRFUNC_1:2 ; A299: dom P1 = NAT by PARTFUN1:def_2; CurInstr (P1,(Comput (P1,s1,0))) = CurInstr (P1,s1) .= P1 . (IC s1) by A299, PARTFUN1:def_6 ; hence IncAddr ((CurInstr (P1,(Comput (P1,s1,0)))),k) = CurInstr (P2,(Comput (P2,s2,0))) by A298, A294, A297, 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)) ) A300: DataPart p c= p by RELAT_1:59; A301: DataPart p c= s1 by A1, A300, XBOOLE_1:1; A302: DataPart (IncIC (p,k)) = DataPart p by MEMSTR_0:51; DataPart p c= IncIC (p,k) by A302, MEMSTR_0:12; then A303: DataPart p c= s2 by A2, XBOOLE_1:1; thus (Comput (P1,s1,0)) | (dom (DataPart p)) = s1 | (dom (DataPart p)) .= DataPart p by A301, GRFUNC_1:23 .= s2 | (dom (DataPart p)) by A303, 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 PBOOLE:142 .= DataPart (Comput (P2,s2,0)) ; ::_thesis: verum end; then A304: S1[ 0 ] ; thus for i being Element of NAT holds S1[i] from NAT_1:sch_1(A304, A8); ::_thesis: verum end; registration cluster SCM+FSA -> relocable1 relocable2 ; coherence ( SCM+FSA is relocable1 & SCM+FSA is relocable2 ) proof for k being Element of NAT for q being NAT -defined the InstructionsF of SCM+FSA -valued finite non halt-free Function for p being non empty b2 -autonomic FinPartState of SCM+FSA for s1, s2 being State of SCM+FSA st p c= s1 & IncIC (p,k) c= s2 holds for P1, P2 being Instruction-Sequence of SCM+FSA st q c= P1 & Reloc (q,k) c= P2 holds for i being Element of NAT holds IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = CurInstr (P2,(Comput (P2,s2,i))) by Th1; hence SCM+FSA is relocable1 by AMISTD_5:def_5; ::_thesis: SCM+FSA is relocable2 let k be Element of NAT ; :: according to AMISTD_5:def_6 ::_thesis: for b1 being set for b2 being set for b3, b4 being set holds ( not b2 c= b3 or not IncIC (b2,k) c= b4 or for b5, b6 being set holds ( not b1 c= b5 or not Reloc (b1,k) c= b6 or for b7 being Element of NAT holds (Comput (b5,b3,b7)) | (dom (DataPart b2)) = (Comput (b6,b4,b7)) | (dom (DataPart b2)) ) ) let q be NAT -defined the InstructionsF of SCM+FSA -valued finite non halt-free Function; ::_thesis: for b1 being set for b2, b3 being set holds ( not b1 c= b2 or not IncIC (b1,k) c= b3 or for b4, b5 being set holds ( not q c= b4 or not Reloc (q,k) c= b5 or for b6 being Element of NAT holds (Comput (b4,b2,b6)) | (dom (DataPart b1)) = (Comput (b5,b3,b6)) | (dom (DataPart b1)) ) ) let p be non empty q -autonomic FinPartState of SCM+FSA; ::_thesis: for b1, b2 being set holds ( not p c= b1 or not IncIC (p,k) c= b2 or for b3, b4 being set holds ( not q c= b3 or not Reloc (q,k) c= b4 or for b5 being Element of NAT holds (Comput (b3,b1,b5)) | (dom (DataPart p)) = (Comput (b4,b2,b5)) | (dom (DataPart p)) ) ) let s1, s2 be State of SCM+FSA; ::_thesis: ( not p c= s1 or not IncIC (p,k) c= s2 or for b1, b2 being set holds ( not q c= b1 or not Reloc (q,k) c= b2 or for b3 being Element of NAT holds (Comput (b1,s1,b3)) | (dom (DataPart p)) = (Comput (b2,s2,b3)) | (dom (DataPart p)) ) ) assume A1: ( p c= s1 & IncIC (p,k) c= s2 ) ; ::_thesis: for b1, b2 being set holds ( not q c= b1 or not Reloc (q,k) c= b2 or for b3 being Element of NAT holds (Comput (b1,s1,b3)) | (dom (DataPart p)) = (Comput (b2,s2,b3)) | (dom (DataPart p)) ) let P1, P2 be Instruction-Sequence of SCM+FSA; ::_thesis: ( not q c= P1 or not Reloc (q,k) c= P2 or for b1 being Element of NAT holds (Comput (P1,s1,b1)) | (dom (DataPart p)) = (Comput (P2,s2,b1)) | (dom (DataPart p)) ) assume ( q c= P1 & Reloc (q,k) c= P2 ) ; ::_thesis: for b1 being Element of NAT holds (Comput (P1,s1,b1)) | (dom (DataPart p)) = (Comput (P2,s2,b1)) | (dom (DataPart p)) hence for i being Element of NAT holds (Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart p)) by A1, Th1; ::_thesis: verum end; end;