:: RELOC semantic presentation begin registration let a, b be Data-Location; clustera := b -> ins-loc-free ; coherence a := b is ins-loc-free ; cluster AddTo (a,b) -> ins-loc-free ; coherence AddTo (a,b) is ins-loc-free ; cluster SubFrom (a,b) -> ins-loc-free ; coherence SubFrom (a,b) is ins-loc-free ; cluster MultBy (a,b) -> ins-loc-free ; coherence MultBy (a,b) is ins-loc-free ; cluster Divide (a,b) -> ins-loc-free ; coherence Divide (a,b) is ins-loc-free ; end; theorem Th1: :: RELOC:1 for k, loc being Nat holds IncAddr ((SCM-goto loc),k) = SCM-goto (loc + k) proof let k, loc be Nat; ::_thesis: IncAddr ((SCM-goto loc),k) = SCM-goto (loc + k) A1: InsCode (IncAddr ((SCM-goto loc),k)) = InsCode (SCM-goto loc) by COMPOS_0:def_9 .= 6 by RECDEF_2:def_1 .= InsCode (SCM-goto (loc + k)) by RECDEF_2:def_1 ; A2: AddressPart (IncAddr ((SCM-goto loc),k)) = AddressPart (SCM-goto loc) by COMPOS_0:def_9 .= {} by RECDEF_2:def_3 .= AddressPart (SCM-goto (loc + k)) by RECDEF_2:def_3 ; A3: JumpPart (IncAddr ((SCM-goto loc),k)) = k + (JumpPart (SCM-goto loc)) by COMPOS_0:def_9; JumpPart (IncAddr ((SCM-goto loc),k)) = JumpPart (SCM-goto (loc + k)) proof thus A4: dom (JumpPart (IncAddr ((SCM-goto loc),k))) = dom (JumpPart (SCM-goto (loc + k))) by A1, COMPOS_0:def_5; :: according to FUNCT_1:def_11 ::_thesis: for b1 being set holds ( not b1 in proj1 (JumpPart (IncAddr ((SCM-goto loc),k))) or (JumpPart (IncAddr ((SCM-goto loc),k))) . b1 = (JumpPart (SCM-goto (loc + k))) . b1 ) A5: JumpPart (SCM-goto loc) = <*loc*> by RECDEF_2:def_2; A6: JumpPart (SCM-goto (loc + k)) = <*(loc + k)*> by RECDEF_2:def_2; let x be set ; ::_thesis: ( not x in proj1 (JumpPart (IncAddr ((SCM-goto loc),k))) or (JumpPart (IncAddr ((SCM-goto loc),k))) . x = (JumpPart (SCM-goto (loc + k))) . x ) assume A7: x in dom (JumpPart (IncAddr ((SCM-goto loc),k))) ; ::_thesis: (JumpPart (IncAddr ((SCM-goto loc),k))) . x = (JumpPart (SCM-goto (loc + k))) . x dom <*(loc + k)*> = {1} by FINSEQ_1:2, FINSEQ_1:38; then A8: x = 1 by A7, A4, A6, TARSKI:def_1; thus (JumpPart (IncAddr ((SCM-goto loc),k))) . x = k + ((JumpPart (SCM-goto loc)) . x) by A3, A7, VALUED_1:def_2 .= loc + k by A5, A8, FINSEQ_1:40 .= (JumpPart (SCM-goto (loc + k))) . x by A6, A8, FINSEQ_1:40 ; ::_thesis: verum end; hence IncAddr ((SCM-goto loc),k) = SCM-goto (loc + k) by A1, A2, COMPOS_0:1; ::_thesis: verum end; theorem Th2: :: RELOC:2 for k, loc being Nat for a being Data-Location holds IncAddr ((a =0_goto loc),k) = a =0_goto (loc + k) proof let k, loc be Nat; ::_thesis: for a being Data-Location holds IncAddr ((a =0_goto loc),k) = a =0_goto (loc + k) let a be Data-Location; ::_thesis: IncAddr ((a =0_goto loc),k) = a =0_goto (loc + k) A1: InsCode (IncAddr ((a =0_goto loc),k)) = InsCode (a =0_goto loc) by COMPOS_0:def_9 .= 7 by RECDEF_2:def_1 .= InsCode (a =0_goto (loc + k)) by RECDEF_2:def_1 ; A2: AddressPart (IncAddr ((a =0_goto loc),k)) = AddressPart (a =0_goto loc) by COMPOS_0:def_9 .= <*a*> by RECDEF_2:def_3 .= AddressPart (a =0_goto (loc + k)) by RECDEF_2:def_3 ; A3: JumpPart (IncAddr ((a =0_goto loc),k)) = k + (JumpPart (a =0_goto loc)) by COMPOS_0:def_9; JumpPart (IncAddr ((a =0_goto loc),k)) = JumpPart (a =0_goto (loc + k)) proof thus A4: dom (JumpPart (IncAddr ((a =0_goto loc),k))) = dom (JumpPart (a =0_goto (loc + k))) by A1, COMPOS_0:def_5; :: according to FUNCT_1:def_11 ::_thesis: for b1 being set holds ( not b1 in proj1 (JumpPart (IncAddr ((a =0_goto loc),k))) or (JumpPart (IncAddr ((a =0_goto loc),k))) . b1 = (JumpPart (a =0_goto (loc + k))) . b1 ) A5: JumpPart (a =0_goto loc) = <*loc*> by RECDEF_2:def_2; A6: JumpPart (a =0_goto (loc + k)) = <*(loc + k)*> by RECDEF_2:def_2; let x be set ; ::_thesis: ( not x in proj1 (JumpPart (IncAddr ((a =0_goto loc),k))) or (JumpPart (IncAddr ((a =0_goto loc),k))) . x = (JumpPart (a =0_goto (loc + k))) . x ) assume A7: x in dom (JumpPart (IncAddr ((a =0_goto loc),k))) ; ::_thesis: (JumpPart (IncAddr ((a =0_goto loc),k))) . x = (JumpPart (a =0_goto (loc + k))) . x dom <*(loc + k)*> = {1} by FINSEQ_1:2, FINSEQ_1:38; then A8: x = 1 by A7, A4, A6, TARSKI:def_1; thus (JumpPart (IncAddr ((a =0_goto loc),k))) . x = k + ((JumpPart (a =0_goto loc)) . x) by A3, A7, VALUED_1:def_2 .= loc + k by A5, A8, FINSEQ_1:40 .= (JumpPart (a =0_goto (loc + k))) . x by A6, A8, FINSEQ_1:40 ; ::_thesis: verum end; hence IncAddr ((a =0_goto loc),k) = a =0_goto (loc + k) by A1, A2, COMPOS_0:1; ::_thesis: verum end; theorem Th3: :: RELOC:3 for k, loc being Nat for a being Data-Location holds IncAddr ((a >0_goto loc),k) = a >0_goto (loc + k) proof let k, loc be Nat; ::_thesis: for a being Data-Location holds IncAddr ((a >0_goto loc),k) = a >0_goto (loc + k) let a be Data-Location; ::_thesis: IncAddr ((a >0_goto loc),k) = a >0_goto (loc + k) A1: InsCode (IncAddr ((a >0_goto loc),k)) = InsCode (a >0_goto loc) by COMPOS_0:def_9 .= 8 by RECDEF_2:def_1 .= InsCode (a >0_goto (loc + k)) by RECDEF_2:def_1 ; A2: AddressPart (IncAddr ((a >0_goto loc),k)) = AddressPart (a >0_goto loc) by COMPOS_0:def_9 .= <*a*> by RECDEF_2:def_3 .= AddressPart (a >0_goto (loc + k)) by RECDEF_2:def_3 ; A3: JumpPart (IncAddr ((a >0_goto loc),k)) = k + (JumpPart (a >0_goto loc)) by COMPOS_0:def_9; JumpPart (IncAddr ((a >0_goto loc),k)) = JumpPart (a >0_goto (loc + k)) proof thus A4: dom (JumpPart (IncAddr ((a >0_goto loc),k))) = dom (JumpPart (a >0_goto (loc + k))) by A1, COMPOS_0:def_5; :: according to FUNCT_1:def_11 ::_thesis: for b1 being set holds ( not b1 in proj1 (JumpPart (IncAddr ((a >0_goto loc),k))) or (JumpPart (IncAddr ((a >0_goto loc),k))) . b1 = (JumpPart (a >0_goto (loc + k))) . b1 ) A5: JumpPart (a >0_goto loc) = <*loc*> by RECDEF_2:def_2; A6: JumpPart (a >0_goto (loc + k)) = <*(loc + k)*> by RECDEF_2:def_2; let x be set ; ::_thesis: ( not x in proj1 (JumpPart (IncAddr ((a >0_goto loc),k))) or (JumpPart (IncAddr ((a >0_goto loc),k))) . x = (JumpPart (a >0_goto (loc + k))) . x ) assume A7: x in dom (JumpPart (IncAddr ((a >0_goto loc),k))) ; ::_thesis: (JumpPart (IncAddr ((a >0_goto loc),k))) . x = (JumpPart (a >0_goto (loc + k))) . x dom <*(loc + k)*> = {1} by FINSEQ_1:2, FINSEQ_1:38; then A8: x = 1 by A7, A4, A6, TARSKI:def_1; thus (JumpPart (IncAddr ((a >0_goto loc),k))) . x = k + ((JumpPart (a >0_goto loc)) . x) by A3, A7, VALUED_1:def_2 .= loc + k by A5, A8, FINSEQ_1:40 .= (JumpPart (a >0_goto (loc + k))) . x by A6, A8, FINSEQ_1:40 ; ::_thesis: verum end; hence IncAddr ((a >0_goto loc),k) = a >0_goto (loc + k) by A1, A2, COMPOS_0:1; ::_thesis: verum end; theorem Th4: :: RELOC:4 for I being Instruction of SCM for k being Element of NAT st ( InsCode I = 0 or InsCode I = 1 or InsCode I = 2 or InsCode I = 3 or InsCode I = 4 or InsCode I = 5 ) holds IncAddr (I,k) = I proof let I be Instruction of SCM; ::_thesis: for k being Element of NAT st ( InsCode I = 0 or InsCode I = 1 or InsCode I = 2 or InsCode I = 3 or InsCode I = 4 or InsCode I = 5 ) holds IncAddr (I,k) = I let k be Element of NAT ; ::_thesis: ( ( InsCode I = 0 or InsCode I = 1 or InsCode I = 2 or InsCode I = 3 or InsCode I = 4 or InsCode I = 5 ) implies IncAddr (I,k) = I ) assume A1: ( InsCode I = 0 or InsCode I = 1 or InsCode I = 2 or InsCode I = 3 or InsCode I = 4 or InsCode I = 5 ) ; ::_thesis: IncAddr (I,k) = I percases ( InsCode I = 0 or InsCode I = 1 or InsCode I = 2 or InsCode I = 3 or InsCode I = 4 or InsCode I = 5 ) by A1; suppose InsCode I = 0 ; ::_thesis: IncAddr (I,k) = I then I = halt SCM by AMI_5:7; hence IncAddr (I,k) = I by COMPOS_0:4; ::_thesis: verum end; suppose InsCode I = 1 ; ::_thesis: IncAddr (I,k) = I then ex da, db being Data-Location st I = da := db by AMI_5:8; hence IncAddr (I,k) = I by COMPOS_0:4; ::_thesis: verum end; suppose InsCode I = 2 ; ::_thesis: IncAddr (I,k) = I then ex da, db being Data-Location st I = AddTo (da,db) by AMI_5:9; hence IncAddr (I,k) = I by COMPOS_0:4; ::_thesis: verum end; suppose InsCode I = 3 ; ::_thesis: IncAddr (I,k) = I then ex da, db being Data-Location st I = SubFrom (da,db) by AMI_5:10; hence IncAddr (I,k) = I by COMPOS_0:4; ::_thesis: verum end; suppose InsCode I = 4 ; ::_thesis: IncAddr (I,k) = I then ex da, db being Data-Location st I = MultBy (da,db) by AMI_5:11; hence IncAddr (I,k) = I by COMPOS_0:4; ::_thesis: verum end; suppose InsCode I = 5 ; ::_thesis: IncAddr (I,k) = I then ex da, db being Data-Location st I = Divide (da,db) by AMI_5:12; hence IncAddr (I,k) = I by COMPOS_0:4; ::_thesis: verum end; end; end; theorem :: RELOC:5 for II, I being Instruction of SCM for k being Element of NAT st ( InsCode I = 0 or InsCode I = 1 or InsCode I = 2 or InsCode I = 3 or InsCode I = 4 or InsCode I = 5 ) & IncAddr (II,k) = I holds II = I proof let II, I be Instruction of SCM; ::_thesis: for k being Element of NAT st ( InsCode I = 0 or InsCode I = 1 or InsCode I = 2 or InsCode I = 3 or InsCode I = 4 or InsCode I = 5 ) & IncAddr (II,k) = I holds II = I let k be Element of NAT ; ::_thesis: ( ( InsCode I = 0 or InsCode I = 1 or InsCode I = 2 or InsCode I = 3 or InsCode I = 4 or InsCode I = 5 ) & IncAddr (II,k) = I implies II = I ) assume that A1: ( InsCode I = 0 or InsCode I = 1 or InsCode I = 2 or InsCode I = 3 or InsCode I = 4 or InsCode I = 5 ) and A2: IncAddr (II,k) = I ; ::_thesis: II = I IncAddr (I,k) = I by A1, Th4; hence II = I by A2, COMPOS_0:6; ::_thesis: verum end; registration cluster SCM -> relocable ; coherence SCM is relocable proof let INS be Instruction of SCM; :: according to AMISTD_5:def_2 ::_thesis: INS is relocable let j, k be Nat; :: according to AMISTD_5:def_1 ::_thesis: for b1 being set holds Exec ((IncAddr (INS,(j + k))),(IncIC (b1,k))) = IncIC ((Exec ((IncAddr (INS,j)),b1)),k) reconsider k = k as Element of NAT by ORDINAL1:def_12; let s be State of SCM; ::_thesis: Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))) = IncIC ((Exec ((IncAddr (INS,j)),s)),k) A1: IC (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) = (IC (Exec ((IncAddr (INS,j)),s))) + k by MEMSTR_0:53 .= IC (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) by AMISTD_2:def_3 ; percases ( InsCode INS = 0 or InsCode INS = 1 or InsCode INS = 2 or InsCode INS = 3 or InsCode INS = 4 or InsCode INS = 5 or InsCode INS = 6 or InsCode INS = 7 or InsCode INS = 8 ) by AMI_5:5, NAT_1:32; suppose InsCode INS = 0 ; ::_thesis: Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))) = IncIC ((Exec ((IncAddr (INS,j)),s)),k) then A2: INS = halt SCM by AMI_5:7; Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))) = Exec (INS,(IncIC (s,k))) by A2, COMPOS_0:4 .= IncIC (s,k) by A2, EXTPRO_1:def_3 .= IncIC ((Exec ((IncAddr (INS,j)),s)),k) by A2, EXTPRO_1:def_3 ; hence Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))) = IncIC ((Exec ((IncAddr (INS,j)),s)),k) ; ::_thesis: verum end; suppose InsCode INS = 1 ; ::_thesis: Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))) = IncIC ((Exec ((IncAddr (INS,j)),s)),k) then consider da, db being Data-Location such that A3: INS = da := db by AMI_5:8; now__::_thesis:_for_d_being_Data-Location_holds_(Exec_((IncAddr_(INS,(j_+_k))),(IncIC_(s,k))))_._d_=_(IncIC_((Exec_((IncAddr_(INS,j)),s)),k))_._d let d be Data-Location; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1 percases ( da = d or da <> d ) ; supposeA4: da = d ; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1 thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A3, COMPOS_0:4 .= (IncIC (s,k)) . db by A3, A4, AMI_3:2 .= s . db by AMI_5:16 .= (Exec (INS,s)) . d by A3, A4, AMI_3:2 .= (Exec ((IncAddr (INS,j)),s)) . d by A3, COMPOS_0:4 .= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by AMI_5:16 ; ::_thesis: verum end; supposeA5: da <> d ; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1 thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A3, COMPOS_0:4 .= (IncIC (s,k)) . d by A3, A5, AMI_3:2 .= s . d by AMI_5:16 .= (Exec (INS,s)) . d by A3, A5, AMI_3:2 .= (Exec ((IncAddr (INS,j)),s)) . d by A3, COMPOS_0:4 .= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by AMI_5:16 ; ::_thesis: verum end; end; end; hence Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))) = IncIC ((Exec ((IncAddr (INS,j)),s)),k) by A1, AMI_5:25; ::_thesis: verum end; suppose InsCode INS = 2 ; ::_thesis: Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))) = IncIC ((Exec ((IncAddr (INS,j)),s)),k) then consider da, db being Data-Location such that A6: INS = AddTo (da,db) by AMI_5:9; now__::_thesis:_for_d_being_Data-Location_holds_(Exec_((IncAddr_(INS,(j_+_k))),(IncIC_(s,k))))_._d_=_(IncIC_((Exec_((IncAddr_(INS,j)),s)),k))_._d let d be Data-Location; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1 percases ( da = d or da <> d ) ; supposeA7: da = d ; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1 thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A6, COMPOS_0:4 .= ((IncIC (s,k)) . da) + ((IncIC (s,k)) . db) by A7, A6, AMI_3:3 .= (s . da) + ((IncIC (s,k)) . db) by AMI_5:16 .= (s . da) + (s . db) by AMI_5:16 .= (Exec (INS,s)) . d by A6, A7, AMI_3:3 .= (Exec ((IncAddr (INS,j)),s)) . d by A6, COMPOS_0:4 .= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by AMI_5:16 ; ::_thesis: verum end; supposeA8: da <> d ; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1 thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A6, COMPOS_0:4 .= (IncIC (s,k)) . d by A6, A8, AMI_3:3 .= s . d by AMI_5:16 .= (Exec (INS,s)) . d by A6, A8, AMI_3:3 .= (Exec ((IncAddr (INS,j)),s)) . d by A6, COMPOS_0:4 .= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by AMI_5:16 ; ::_thesis: verum end; end; end; hence Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))) = IncIC ((Exec ((IncAddr (INS,j)),s)),k) by A1, AMI_5:25; ::_thesis: verum end; suppose InsCode INS = 3 ; ::_thesis: Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))) = IncIC ((Exec ((IncAddr (INS,j)),s)),k) then consider da, db being Data-Location such that A9: INS = SubFrom (da,db) by AMI_5:10; now__::_thesis:_for_d_being_Data-Location_holds_(Exec_((IncAddr_(INS,(j_+_k))),(IncIC_(s,k))))_._d_=_(IncIC_((Exec_((IncAddr_(INS,j)),s)),k))_._d let d be Data-Location; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1 percases ( da = d or da <> d ) ; supposeA10: da = d ; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1 thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A9, COMPOS_0:4 .= ((IncIC (s,k)) . da) - ((IncIC (s,k)) . db) by A10, A9, AMI_3:4 .= (s . da) - ((IncIC (s,k)) . db) by AMI_5:16 .= (s . da) - (s . db) by AMI_5:16 .= (Exec (INS,s)) . d by A9, A10, AMI_3:4 .= (Exec ((IncAddr (INS,j)),s)) . d by A9, COMPOS_0:4 .= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by AMI_5:16 ; ::_thesis: verum end; supposeA11: da <> d ; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1 thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A9, COMPOS_0:4 .= (IncIC (s,k)) . d by A9, A11, AMI_3:4 .= s . d by AMI_5:16 .= (Exec (INS,s)) . d by A9, A11, AMI_3:4 .= (Exec ((IncAddr (INS,j)),s)) . d by A9, COMPOS_0:4 .= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by AMI_5:16 ; ::_thesis: verum end; end; end; hence Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))) = IncIC ((Exec ((IncAddr (INS,j)),s)),k) by A1, AMI_5:25; ::_thesis: verum end; suppose InsCode INS = 4 ; ::_thesis: Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))) = IncIC ((Exec ((IncAddr (INS,j)),s)),k) then consider da, db being Data-Location such that A12: INS = MultBy (da,db) by AMI_5:11; now__::_thesis:_for_d_being_Data-Location_holds_(Exec_((IncAddr_(INS,(j_+_k))),(IncIC_(s,k))))_._d_=_(IncIC_((Exec_((IncAddr_(INS,j)),s)),k))_._d let d be Data-Location; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1 percases ( da = d or da <> d ) ; supposeA13: da = d ; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1 thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A12, COMPOS_0:4 .= ((IncIC (s,k)) . da) * ((IncIC (s,k)) . db) by A13, A12, AMI_3:5 .= (s . da) * ((IncIC (s,k)) . db) by AMI_5:16 .= (s . da) * (s . db) by AMI_5:16 .= (Exec (INS,s)) . d by A12, A13, AMI_3:5 .= (Exec ((IncAddr (INS,j)),s)) . d by A12, COMPOS_0:4 .= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by AMI_5:16 ; ::_thesis: verum end; supposeA14: da <> d ; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1 thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A12, COMPOS_0:4 .= (IncIC (s,k)) . d by A12, A14, AMI_3:5 .= s . d by AMI_5:16 .= (Exec (INS,s)) . d by A12, A14, AMI_3:5 .= (Exec ((IncAddr (INS,j)),s)) . d by A12, COMPOS_0:4 .= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by AMI_5:16 ; ::_thesis: verum end; end; end; hence Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))) = IncIC ((Exec ((IncAddr (INS,j)),s)),k) by A1, AMI_5:25; ::_thesis: verum end; suppose InsCode INS = 5 ; ::_thesis: Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))) = IncIC ((Exec ((IncAddr (INS,j)),s)),k) then consider da, db being Data-Location such that A15: INS = Divide (da,db) by AMI_5:12; now__::_thesis:_for_d_being_Data-Location_holds_(Exec_((IncAddr_(INS,(j_+_k))),(IncIC_(s,k))))_._d_=_(IncIC_((Exec_((IncAddr_(INS,j)),s)),k))_._d let d be Data-Location; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1 percases ( da <> db or da = db ) ; supposeA16: da <> db ; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1 hereby ::_thesis: verum percases ( da = d or db = d or ( da <> d & db <> d ) ) ; supposeA17: da = d ; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A15, COMPOS_0:4 .= ((IncIC (s,k)) . da) div ((IncIC (s,k)) . db) by A16, A17, A15, AMI_3:6 .= (s . da) div ((IncIC (s,k)) . db) by AMI_5:16 .= (s . da) div (s . db) by AMI_5:16 .= (Exec (INS,s)) . d by A15, A16, A17, AMI_3:6 .= (Exec ((IncAddr (INS,j)),s)) . d by A15, COMPOS_0:4 .= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by AMI_5:16 ; ::_thesis: verum end; supposeA18: db = d ; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A15, COMPOS_0:4 .= ((IncIC (s,k)) . da) mod ((IncIC (s,k)) . db) by A18, A15, AMI_3:6 .= (s . da) mod ((IncIC (s,k)) . db) by AMI_5:16 .= (s . da) mod (s . db) by AMI_5:16 .= (Exec (INS,s)) . d by A15, A18, AMI_3:6 .= (Exec ((IncAddr (INS,j)),s)) . d by A15, COMPOS_0:4 .= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by AMI_5:16 ; ::_thesis: verum end; supposeA19: ( da <> d & db <> d ) ; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A15, COMPOS_0:4 .= (IncIC (s,k)) . d by A15, A19, AMI_3:6 .= s . d by AMI_5:16 .= (Exec (INS,s)) . d by A15, A19, AMI_3:6 .= (Exec ((IncAddr (INS,j)),s)) . d by A15, COMPOS_0:4 .= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by AMI_5:16 ; ::_thesis: verum end; end; end; end; supposeA20: da = db ; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1 percases ( da = d or da <> d ) ; supposeA21: da = d ; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1 thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A15, COMPOS_0:4 .= ((IncIC (s,k)) . da) mod ((IncIC (s,k)) . db) by A20, A21, A15, AMI_3:6 .= (s . da) mod ((IncIC (s,k)) . db) by AMI_5:16 .= (s . da) mod (s . db) by AMI_5:16 .= (Exec (INS,s)) . d by A15, A20, A21, AMI_3:6 .= (Exec ((IncAddr (INS,j)),s)) . d by A15, COMPOS_0:4 .= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by AMI_5:16 ; ::_thesis: verum end; supposeA22: da <> d ; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1 thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (Exec (INS,(IncIC (s,k)))) . d by A15, COMPOS_0:4 .= (IncIC (s,k)) . d by A15, A20, A22, AMI_3:6 .= s . d by AMI_5:16 .= (Exec (INS,s)) . d by A15, A20, A22, AMI_3:6 .= (Exec ((IncAddr (INS,j)),s)) . d by A15, COMPOS_0:4 .= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by AMI_5:16 ; ::_thesis: verum end; end; end; end; end; hence Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))) = IncIC ((Exec ((IncAddr (INS,j)),s)),k) by A1, AMI_5:25; ::_thesis: verum end; suppose InsCode INS = 6 ; ::_thesis: Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))) = IncIC ((Exec ((IncAddr (INS,j)),s)),k) then consider loc being Element of NAT such that A23: INS = SCM-goto loc by AMI_5:13; A24: IncAddr (INS,(j + k)) = SCM-goto (loc + (j + k)) by A23, Th1; A25: IncAddr (INS,j) = SCM-goto (loc + j) by A23, Th1; now__::_thesis:_for_d_being_Data-Location_holds_(Exec_((IncAddr_(INS,(j_+_k))),(IncIC_(s,k))))_._d_=_(IncIC_((Exec_((IncAddr_(INS,j)),s)),k))_._d let d be Data-Location; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC (s,k)) . d by A24, AMI_3:7 .= s . d by AMI_5:16 .= (Exec ((IncAddr (INS,j)),s)) . d by A25, AMI_3:7 .= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by AMI_5:16 ; ::_thesis: verum end; hence Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))) = IncIC ((Exec ((IncAddr (INS,j)),s)),k) by A1, AMI_5:25; ::_thesis: verum end; suppose InsCode INS = 7 ; ::_thesis: Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))) = IncIC ((Exec ((IncAddr (INS,j)),s)),k) then consider loc being Element of NAT , da being Data-Location such that A26: INS = da =0_goto loc by AMI_5:14; A27: IncAddr (INS,(j + k)) = da =0_goto (loc + (j + k)) by A26, Th2; A28: IncAddr (INS,j) = da =0_goto (loc + j) by A26, Th2; now__::_thesis:_for_d_being_Data-Location_holds_(Exec_((IncAddr_(INS,(j_+_k))),(IncIC_(s,k))))_._d_=_(IncIC_((Exec_((IncAddr_(INS,j)),s)),k))_._d let d be Data-Location; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC (s,k)) . d by A27, AMI_3:8 .= s . d by AMI_5:16 .= (Exec ((IncAddr (INS,j)),s)) . d by A28, AMI_3:8 .= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by AMI_5:16 ; ::_thesis: verum end; hence Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))) = IncIC ((Exec ((IncAddr (INS,j)),s)),k) by A1, AMI_5:25; ::_thesis: verum end; suppose InsCode INS = 8 ; ::_thesis: Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))) = IncIC ((Exec ((IncAddr (INS,j)),s)),k) then consider loc being Element of NAT , da being Data-Location such that A29: INS = da >0_goto loc by AMI_5:15; A30: IncAddr (INS,(j + k)) = da >0_goto (loc + (j + k)) by A29, Th3; A31: IncAddr (INS,j) = da >0_goto (loc + j) by A29, Th3; now__::_thesis:_for_d_being_Data-Location_holds_(Exec_((IncAddr_(INS,(j_+_k))),(IncIC_(s,k))))_._d_=_(IncIC_((Exec_((IncAddr_(INS,j)),s)),k))_._d let d be Data-Location; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d thus (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . d = (IncIC (s,k)) . d by A30, AMI_3:9 .= s . d by AMI_5:16 .= (Exec ((IncAddr (INS,j)),s)) . d by A31, AMI_3:9 .= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by AMI_5:16 ; ::_thesis: verum end; hence Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))) = IncIC ((Exec ((IncAddr (INS,j)),s)),k) by A1, AMI_5:25; ::_thesis: verum end; end; end; end; begin Lm1: for k being Element of NAT for q being NAT -defined the InstructionsF of SCM -valued finite non halt-free Function for p being non empty b2 -autonomic FinPartState of SCM for s1, s2 being State of SCM st p c= s1 & IncIC (p,k) c= s2 holds for P1, P2 being Instruction-Sequence of SCM st q c= P1 & Reloc (q,k) c= P2 holds for i being 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 -valued finite non halt-free Function for p being non empty b1 -autonomic FinPartState of SCM for s1, s2 being State of SCM st p c= s1 & IncIC (p,k) c= s2 holds for P1, P2 being Instruction-Sequence of SCM st q c= P1 & Reloc (q,k) c= P2 holds for i being 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 -valued finite non halt-free Function; ::_thesis: for p being non empty q -autonomic FinPartState of SCM for s1, s2 being State of SCM st p c= s1 & IncIC (p,k) c= s2 holds for P1, P2 being Instruction-Sequence of SCM st q c= P1 & Reloc (q,k) c= P2 holds for i being 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; ::_thesis: for s1, s2 being State of SCM st p c= s1 & IncIC (p,k) c= s2 holds for P1, P2 being Instruction-Sequence of SCM st q c= P1 & Reloc (q,k) c= P2 holds for i being Element of NAT holds ( (IC (Comput (P1,s1,i))) + k = IC (Comput (P2,s2,i)) & IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = CurInstr (P2,(Comput (P2,s2,i))) & (Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),i)) = DataPart (Comput (P2,s2,i)) ) let s1, s2 be State of SCM; ::_thesis: ( p c= s1 & IncIC (p,k) c= s2 implies for P1, P2 being Instruction-Sequence of SCM st q c= P1 & Reloc (q,k) c= P2 holds for i being 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 A2: p c= s1 and A3: IncIC (p,k) c= s2 ; ::_thesis: for P1, P2 being Instruction-Sequence of SCM st q c= P1 & Reloc (q,k) c= P2 holds for i being 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)) ) A4: IC in dom p by AMISTD_5:6; A5: p c= s1 by A2; let P1, P2 be Instruction-Sequence of SCM; ::_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 A6: ( 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)) ) A7: Reloc (q,k) c= P2 by A6; A8: q c= P1 by A6; set s3 = s1 +* (DataPart s2); defpred S1[ Element of NAT ] means ( (IC (Comput (P1,s1,$1))) + k = IC (Comput (P2,s2,$1)) & IncAddr ((CurInstr (P1,(Comput (P1,s1,$1)))),k) = CurInstr (P2,(Comput (P2,s2,$1))) & (Comput (P1,s1,$1)) | (dom (DataPart p)) = (Comput (P2,s2,$1)) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),$1)) = DataPart (Comput (P2,s2,$1)) ); A9: p c= s1 +* (DataPart s2) by A2, A3, MEMSTR_0:61; A10: for i being Element of NAT st S1[i] holds S1[i + 1] proof set DPp = DataPart p; let i be Element of NAT ; ::_thesis: ( S1[i] implies S1[i + 1] ) assume that A11: (IC (Comput (P1,s1,i))) + k = IC (Comput (P2,s2,i)) and A12: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = CurInstr (P2,(Comput (P2,s2,i))) and A13: (Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart p)) and A14: DataPart (Comput (P1,(s1 +* (DataPart s2)),i)) = DataPart (Comput (P2,s2,i)) ; ::_thesis: S1[i + 1] set Cs2i1 = Comput (P2,s2,(i + 1)); set Cs3i = Comput (P1,(s1 +* (DataPart s2)),i); set Cs2i = Comput (P2,s2,i); dom (Comput (P2,s2,(i + 1))) = the carrier of SCM by PARTFUN1:def_2; then A15: dom (Comput (P2,s2,(i + 1))) = {(IC )} \/ (Data-Locations ) by STRUCT_0:4; set Cs3i1 = Comput (P1,(s1 +* (DataPart s2)),(i + 1)); A16: dom (DataPart (Comput (P2,s2,i))) = Data-Locations by MEMSTR_0:9; A17: dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) = Data-Locations by MEMSTR_0:9; A18: dom (DataPart (Comput (P2,s2,(i + 1)))) = Data-Locations by MEMSTR_0:9; A19: now__::_thesis:_for_x_being_set_st_x_in_dom_(DataPart_(Comput_(P1,(s1_+*_(DataPart_s2)),(i_+_1))))_&_(Comput_(P1,(s1_+*_(DataPart_s2)),(i_+_1)))_._x_=_(Comput_(P2,s2,(i_+_1)))_._x_holds_ (DataPart_(Comput_(P1,(s1_+*_(DataPart_s2)),(i_+_1))))_._x_=_(DataPart_(Comput_(P2,s2,(i_+_1))))_._x let x be set ; ::_thesis: ( x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) & (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = (Comput (P2,s2,(i + 1))) . x implies (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x ) assume that A20: x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) and A21: (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = (Comput (P2,s2,(i + 1))) . x ; ::_thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x thus (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (Comput (P2,s2,(i + 1))) . x by A20, A21, FUNCT_1:47 .= (DataPart (Comput (P2,s2,(i + 1)))) . x by A17, A18, A20, FUNCT_1:47 ; ::_thesis: verum end; A22: dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),i))) = Data-Locations by MEMSTR_0:9; A23: 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 A24: x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) and A25: ( (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . x = (Comput (P1,(s1 +* (DataPart s2)),i)) . x & (Comput (P2,s2,(i + 1))) . x = (Comput (P2,s2,i)) . x ) ; ::_thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x (DataPart (Comput (P1,(s1 +* (DataPart s2)),i))) . x = (Comput (P1,(s1 +* (DataPart s2)),i)) . x by A22, A17, A24, FUNCT_1:47; hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A14, A16, A17, A19, A24, A25, FUNCT_1:47; ::_thesis: verum end; A26: now__::_thesis:_for_s_being_State_of_SCM for_d_being_Data-Location_holds_d_in_dom_(DataPart_s) let s be State of SCM; ::_thesis: for d being Data-Location holds d in dom (DataPart s) let d be Data-Location; ::_thesis: d in dom (DataPart s) d in Data-Locations by AMI_2:def_16, AMI_3:27; hence d in dom (DataPart s) by MEMSTR_0:9; ::_thesis: verum end; A27: now__::_thesis:_for_d_being_Data-Location_holds_(Comput_(P1,(s1_+*_(DataPart_s2)),i))_._d_=_(Comput_(P2,s2,i))_._d let d be Data-Location; ::_thesis: (Comput (P1,(s1 +* (DataPart s2)),i)) . d = (Comput (P2,s2,i)) . d A28: d in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),i))) by A26; hence (Comput (P1,(s1 +* (DataPart s2)),i)) . d = (DataPart (Comput (P1,(s1 +* (DataPart s2)),i))) . d by FUNCT_1:47 .= (Comput (P2,s2,i)) . d by A14, A28, FUNCT_1:47 ; ::_thesis: verum end; set Cs1i1 = Comput (P1,s1,(i + 1)); set Cs1i = Comput (P1,s1,i); dom (Comput (P1,s1,(i + 1))) = the carrier of SCM by PARTFUN1:def_2; then A29: dom (Comput (P1,s1,(i + 1))) = {(IC )} \/ (Data-Locations ) by STRUCT_0:4; dom (DataPart p) = (dom p) /\ (Data-Locations ) by RELAT_1:61; then A30: dom (DataPart p) c= {(IC )} \/ (Data-Locations ) by XBOOLE_1:10, XBOOLE_1:17; A31: dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) = (dom (Comput (P1,s1,(i + 1)))) /\ (dom (DataPart p)) by RELAT_1:61 .= dom (DataPart p) by A29, A30, XBOOLE_1:28 ; A32: 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 A33: (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) ; ::_thesis: IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) reconsider kk = loc as Element of NAT ; A34: loc in dom q by A8, A5, AMISTD_5:def_4; A35: loc + k in dom (Reloc (q,k)) by A34, COMPOS_1:46; A36: 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 A34, A6, GRFUNC_1:2 .= q . loc ; hence IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = (Reloc (q,k)) . (loc + k) by A34, COMPOS_1:35 .= P2 . (IC (Comput (P2,s2,(i + 1)))) by A33, A35, A7, GRFUNC_1:2 .= CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A36, PARTFUN1:def_6 ; ::_thesis: verum end; set I = CurInstr (P1,(Comput (P1,s1,i))); A37: Comput (P2,s2,(i + 1)) = Following (P2,(Comput (P2,s2,i))) by EXTPRO_1:3 .= Exec ((CurInstr (P2,(Comput (P2,s2,i)))),(Comput (P2,s2,i))) ; dom (Comput (P2,s2,i)) = the carrier of SCM by PARTFUN1:def_2; then A38: dom (Comput (P2,s2,i)) = {(IC )} \/ (Data-Locations ) by STRUCT_0:4; dom (Comput (P1,s1,i)) = the carrier of SCM by PARTFUN1:def_2; then A39: dom (Comput (P1,s1,i)) = {(IC )} \/ (Data-Locations ) by STRUCT_0:4; A40: dom ((Comput (P1,s1,i)) | (dom (DataPart p))) = (dom (Comput (P1,s1,i))) /\ (dom (DataPart p)) by RELAT_1:61 .= dom (DataPart p) by A39, A30, XBOOLE_1:28 ; A41: 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 A2, A9, A6, AMISTD_5:7 ; A42: 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, A30, XBOOLE_1:28 ; A43: now__::_thesis:_for_x_being_set_ for_d_being_Data-Location_st_d_=_x_&_d_in_dom_(DataPart_p)_&_(Comput_(P1,s1,(i_+_1)))_._d_=_(Comput_(P2,s2,(i_+_1)))_._d_holds_ ((Comput_(P1,s1,(i_+_1)))_|_(dom_(DataPart_p)))_._x_=_((Comput_(P2,s2,(i_+_1)))_|_(dom_(DataPart_p)))_._x let x be set ; ::_thesis: for d being Data-Location st d = x & d in dom (DataPart p) & (Comput (P1,s1,(i + 1))) . d = (Comput (P2,s2,(i + 1))) . d holds ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x let d be Data-Location; ::_thesis: ( d = x & d in dom (DataPart p) & (Comput (P1,s1,(i + 1))) . d = (Comput (P2,s2,(i + 1))) . d implies ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x ) assume that A44: ( d = x & d in dom (DataPart p) ) and A45: (Comput (P1,s1,(i + 1))) . d = (Comput (P2,s2,(i + 1))) . d ; ::_thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x thus ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = (Comput (P2,s2,(i + 1))) . d by A31, A44, A45, FUNCT_1:47 .= ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A42, A44, FUNCT_1:47 ; ::_thesis: verum end; A46: dom ((Comput (P2,s2,i)) | (dom (DataPart p))) = (dom (Comput (P2,s2,i))) /\ (dom (DataPart p)) by RELAT_1:61 .= dom (DataPart p) by A38, A30, XBOOLE_1:28 ; A47: now__::_thesis:_for_x_being_set_ for_d_being_Data-Location_st_d_=_x_&_d_in_dom_(DataPart_p)_&_(Comput_(P1,s1,(i_+_1)))_._d_=_(Comput_(P1,s1,i))_._d_&_(Comput_(P2,s2,(i_+_1)))_._d_=_(Comput_(P2,s2,i))_._d_holds_ ((Comput_(P1,s1,(i_+_1)))_|_(dom_(DataPart_p)))_._x_=_((Comput_(P2,s2,(i_+_1)))_|_(dom_(DataPart_p)))_._x let x be set ; ::_thesis: for d being Data-Location st d = x & d in dom (DataPart p) & (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d holds ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x let d be Data-Location; ::_thesis: ( d = x & d in dom (DataPart p) & (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d implies ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x ) assume that A48: d = x and A49: d in dom (DataPart p) and A50: ( (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d ) ; ::_thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x ( ((Comput (P1,s1,i)) | (dom (DataPart p))) . d = (Comput (P1,s1,i)) . d & ((Comput (P2,s2,i)) | (dom (DataPart p))) . d = (Comput (P2,s2,i)) . d ) by A40, A46, A49, FUNCT_1:47; hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = (Comput (P2,s2,(i + 1))) . d by A13, A31, A48, A49, A50, FUNCT_1:47 .= ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A42, A48, A49, FUNCT_1:47 ; ::_thesis: verum end; reconsider j = IC (Comput (P1,s1,i)) as Element of NAT ; A51: 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))) ; A52: succ ((IC (Comput (P1,s1,i))) + k) = (j + k) + 1 by NAT_1:38 .= (j + 1) + k .= (succ j) + 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 ) by AMI_5:5, NAT_1:32; suppose InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 0 ; ::_thesis: S1[i + 1] then A53: CurInstr (P1,(Comput (P1,s1,i))) = halt SCM by AMI_5:7; thus (IC (Comput (P1,s1,(i + 1)))) + k = (IC (Comput (P1,s1,i))) + k by A51, A53, EXTPRO_1:def_3 .= IC (Comput (P2,s2,(i + 1))) by A11, A37, A53, A12, EXTPRO_1:def_3 ; ::_thesis: ( IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) & (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) ) hence IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A32; ::_thesis: ( (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) ) A54: Comput (P2,s2,(i + 1)) = Comput (P2,s2,i) by A37, A53, A12, EXTPRO_1:def_3; hence (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A13, A51, A53, EXTPRO_1:def_3; ::_thesis: DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) thus DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) by A14, A41, A53, A54, EXTPRO_1:def_3; ::_thesis: verum end; suppose InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 1 ; ::_thesis: S1[i + 1] then consider da, db being Data-Location such that A55: CurInstr (P1,(Comput (P1,s1,i))) = da := db by AMI_5:8; A56: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = da := db by A55, COMPOS_0:4; A57: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = succ (IC (Comput (P1,s1,i))) by A55, AMI_3:2; hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A11, A12, A51, A37, A52, A56, AMI_3:2; ::_thesis: ( IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) & (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) ) thus IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A11, A12, A32, A51, A37, A52, A56, A57, AMI_3:2; ::_thesis: ( (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) ) A58: (Comput (P1,(s1 +* (DataPart s2)),i)) . db = (Comput (P2,s2,i)) . db by A27; 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 DataPart p c= p by RELAT_1:59; then A59: dom (DataPart p) c= dom p by GRFUNC_1:2; 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 A60: x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) ; ::_thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1 dom (DataPart p) c= Data-Locations by RELAT_1:58; then x in Data-Locations by A31, A60; then reconsider d = x as Data-Location by AMI_2:def_16, AMI_3:27; percases ( da = d or da <> d ) ; supposeA61: da = d ; ::_thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1 then ( (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . db & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . db ) by A12, A51, A37, A55, A56, AMI_3:2; hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A2, A9, A31, A43, A55, A58, A60, A59, A61, A6, AMI_5:17; ::_thesis: verum end; suppose da <> d ; ::_thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1 then ( (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d ) by A12, A51, A37, A55, A56, AMI_3:2; hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A31, A47, A60; ::_thesis: verum end; end; end; then (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A31, A42, GRFUNC_1:2; hence (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A31, A42, 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 A62: x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) ; ::_thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 then reconsider d = x as Data-Location by A17, AMI_2:def_16, AMI_3:27; percases ( da = d or da <> d ) ; suppose da = d ; ::_thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 then ( (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . db & (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . db ) by A12, A37, A41, A55, A56, AMI_3:2; hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A27, A19, A62; ::_thesis: verum end; suppose da <> d ; ::_thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 then ( (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d ) by A12, A37, A41, A55, A56, AMI_3:2; hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A23, A62; ::_thesis: verum end; end; end; then DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1))) by A17, A18, GRFUNC_1:2; hence DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) by A17, A18, GRFUNC_1:3; ::_thesis: verum end; suppose InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 2 ; ::_thesis: S1[i + 1] then consider da, db being Data-Location such that A63: CurInstr (P1,(Comput (P1,s1,i))) = AddTo (da,db) by AMI_5:9; A64: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = AddTo (da,db) by A63, COMPOS_0:4; A65: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = succ (IC (Comput (P1,s1,i))) by A63, AMI_3:3; hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A11, A12, A51, A37, A52, A64, AMI_3:3; ::_thesis: ( IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) & (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) ) thus IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A11, A12, A32, A51, A37, A52, A64, A65, AMI_3:3; ::_thesis: ( (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) ) A66: ( (Comput (P1,(s1 +* (DataPart s2)),i)) . da = (Comput (P2,s2,i)) . da & (Comput (P1,(s1 +* (DataPart s2)),i)) . db = (Comput (P2,s2,i)) . db ) by A27; now__::_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 DataPart p c= p by RELAT_1:59; then A67: dom (DataPart p) c= dom p by GRFUNC_1:2; 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 A68: x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) ; ::_thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1 dom (DataPart p) c= Data-Locations by RELAT_1:58; then x in Data-Locations by A31, A68; then reconsider d = x as Data-Location by AMI_2:def_16, AMI_3:27; percases ( da = d or da <> d ) ; supposeA69: da = d ; ::_thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1 then ( (Comput (P1,s1,(i + 1))) . d = ((Comput (P1,s1,i)) . da) + ((Comput (P1,s1,i)) . db) & (Comput (P2,s2,(i + 1))) . d = ((Comput (P2,s2,i)) . da) + ((Comput (P2,s2,i)) . db) ) by A12, A51, A37, A63, A64, AMI_3:3; hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A2, A9, A31, A43, A63, A66, A68, A67, A69, A6, AMI_5:18; ::_thesis: verum end; suppose da <> d ; ::_thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1 then ( (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d ) by A12, A51, A37, A63, A64, AMI_3:3; hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A31, A47, A68; ::_thesis: verum end; end; end; then (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A31, A42, GRFUNC_1:2; hence (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A31, A42, 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 A70: x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) ; ::_thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 then reconsider d = x as Data-Location by A17, AMI_2:def_16, AMI_3:27; percases ( da = d or da <> d ) ; suppose da = d ; ::_thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 then ( (Comput (P2,s2,(i + 1))) . d = ((Comput (P2,s2,i)) . da) + ((Comput (P2,s2,i)) . db) & (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = ((Comput (P1,(s1 +* (DataPart s2)),i)) . da) + ((Comput (P1,(s1 +* (DataPart s2)),i)) . db) ) by A12, A37, A41, A63, A64, AMI_3:3; hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A19, A66, A70; ::_thesis: verum end; suppose da <> d ; ::_thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 then ( (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d ) by A12, A37, A41, A63, A64, AMI_3:3; hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A23, A70; ::_thesis: verum end; end; end; then DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1))) by A17, A18, GRFUNC_1:2; hence DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) by A17, A18, GRFUNC_1:3; ::_thesis: verum end; suppose InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 3 ; ::_thesis: S1[i + 1] then consider da, db being Data-Location such that A71: CurInstr (P1,(Comput (P1,s1,i))) = SubFrom (da,db) by AMI_5:10; A72: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = SubFrom (da,db) by A71, COMPOS_0:4; A73: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = succ (IC (Comput (P1,s1,i))) by A71, AMI_3:4; hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A11, A12, A51, A37, A52, A72, AMI_3:4; ::_thesis: ( IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) & (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) ) thus IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A11, A12, A32, A51, A37, A52, A72, A73, AMI_3:4; ::_thesis: ( (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) ) A74: ( (Comput (P1,(s1 +* (DataPart s2)),i)) . da = (Comput (P2,s2,i)) . da & (Comput (P1,(s1 +* (DataPart s2)),i)) . db = (Comput (P2,s2,i)) . db ) by A27; now__::_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 DataPart p c= p by RELAT_1:59; then A75: dom (DataPart p) c= dom p by GRFUNC_1:2; 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 A76: x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) ; ::_thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1 dom (DataPart p) c= Data-Locations by RELAT_1:58; then x in Data-Locations by A31, A76; then reconsider d = x as Data-Location by AMI_2:def_16, AMI_3:27; percases ( da = d or da <> d ) ; supposeA77: da = d ; ::_thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1 then ( (Comput (P1,s1,(i + 1))) . d = ((Comput (P1,s1,i)) . da) - ((Comput (P1,s1,i)) . db) & (Comput (P2,s2,(i + 1))) . d = ((Comput (P2,s2,i)) . da) - ((Comput (P2,s2,i)) . db) ) by A12, A51, A37, A71, A72, AMI_3:4; hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A2, A9, A31, A43, A71, A74, A76, A75, A77, A6, AMI_5:19; ::_thesis: verum end; suppose da <> d ; ::_thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1 then ( (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d ) by A12, A51, A37, A71, A72, AMI_3:4; hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A31, A47, A76; ::_thesis: verum end; end; end; then (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A31, A42, GRFUNC_1:2; hence (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A31, A42, 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 A78: x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) ; ::_thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 then reconsider d = x as Data-Location by A17, AMI_2:def_16, AMI_3:27; percases ( da = d or da <> d ) ; suppose da = d ; ::_thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 then ( (Comput (P2,s2,(i + 1))) . d = ((Comput (P2,s2,i)) . da) - ((Comput (P2,s2,i)) . db) & (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = ((Comput (P1,(s1 +* (DataPart s2)),i)) . da) - ((Comput (P1,(s1 +* (DataPart s2)),i)) . db) ) by A12, A37, A41, A71, A72, AMI_3:4; hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A19, A74, A78; ::_thesis: verum end; suppose da <> d ; ::_thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 then ( (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d ) by A12, A37, A41, A71, A72, AMI_3:4; hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A23, A78; ::_thesis: verum end; end; end; then DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1))) by A17, A18, GRFUNC_1:2; hence DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) by A17, A18, GRFUNC_1:3; ::_thesis: verum end; suppose InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 4 ; ::_thesis: S1[i + 1] then consider da, db being Data-Location such that A79: CurInstr (P1,(Comput (P1,s1,i))) = MultBy (da,db) by AMI_5:11; A80: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = MultBy (da,db) by A79, COMPOS_0:4; A81: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = succ (IC (Comput (P1,s1,i))) by A79, AMI_3:5; hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A11, A12, A51, A37, A52, A80, AMI_3:5; ::_thesis: ( IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) & (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) ) thus IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A11, A12, A32, A51, A37, A52, A80, A81, AMI_3:5; ::_thesis: ( (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) ) A82: ( (Comput (P1,(s1 +* (DataPart s2)),i)) . da = (Comput (P2,s2,i)) . da & (Comput (P1,(s1 +* (DataPart s2)),i)) . db = (Comput (P2,s2,i)) . db ) by A27; now__::_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 DataPart p c= p by RELAT_1:59; then A83: dom (DataPart p) c= dom p by GRFUNC_1:2; 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 A84: x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) ; ::_thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1 dom (DataPart p) c= Data-Locations by RELAT_1:58; then x in Data-Locations by A31, A84; then reconsider d = x as Data-Location by AMI_2:def_16, AMI_3:27; percases ( da = d or da <> d ) ; supposeA85: da = d ; ::_thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1 then ( (Comput (P1,s1,(i + 1))) . d = ((Comput (P1,s1,i)) . da) * ((Comput (P1,s1,i)) . db) & (Comput (P2,s2,(i + 1))) . d = ((Comput (P2,s2,i)) . da) * ((Comput (P2,s2,i)) . db) ) by A12, A51, A37, A79, A80, AMI_3:5; hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A2, A9, A31, A43, A79, A82, A84, A83, A85, A6, AMI_5:20; ::_thesis: verum end; suppose da <> d ; ::_thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1 then ( (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d ) by A12, A51, A37, A79, A80, AMI_3:5; hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A31, A47, A84; ::_thesis: verum end; end; end; then (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A31, A42, GRFUNC_1:2; hence (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A31, A42, 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 A86: x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) ; ::_thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 then reconsider d = x as Data-Location by A17, AMI_2:def_16, AMI_3:27; percases ( da = d or da <> d ) ; suppose da = d ; ::_thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 then ( (Comput (P2,s2,(i + 1))) . d = ((Comput (P2,s2,i)) . da) * ((Comput (P2,s2,i)) . db) & (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = ((Comput (P1,(s1 +* (DataPart s2)),i)) . da) * ((Comput (P1,(s1 +* (DataPart s2)),i)) . db) ) by A12, A37, A41, A79, A80, AMI_3:5; hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A19, A82, A86; ::_thesis: verum end; suppose da <> d ; ::_thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 then ( (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d ) by A12, A37, A41, A79, A80, AMI_3:5; hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A23, A86; ::_thesis: verum end; end; end; then DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1))) by A17, A18, GRFUNC_1:2; hence DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) by A17, A18, GRFUNC_1:3; ::_thesis: verum end; suppose InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 5 ; ::_thesis: S1[i + 1] then consider da, db being Data-Location such that A87: CurInstr (P1,(Comput (P1,s1,i))) = Divide (da,db) by AMI_5:12; A88: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = Divide (da,db) by A87, COMPOS_0:4; A89: ( (Comput (P1,(s1 +* (DataPart s2)),i)) . da = (Comput (P2,s2,i)) . da & (Comput (P1,(s1 +* (DataPart s2)),i)) . db = (Comput (P2,s2,i)) . db ) by A27; percases ( da <> db or da = db ) ; supposeA90: da <> db ; ::_thesis: S1[i + 1] A91: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = succ (IC (Comput (P1,s1,i))) by A87, AMI_3:6; hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A11, A12, A51, A37, A52, A88, AMI_3:6; ::_thesis: ( IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) & (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) ) thus IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A11, A12, A32, A51, A37, A52, A88, A91, AMI_3:6; ::_thesis: ( (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) ) now__::_thesis:_for_x_being_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 DataPart p c= p by RELAT_1:59; then A92: dom (DataPart p) c= dom p by GRFUNC_1:2; 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 A93: x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) ; ::_thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1 dom (DataPart p) c= Data-Locations by RELAT_1:58; then x in Data-Locations by A31, A93; then reconsider d = x as Data-Location by AMI_2:def_16, AMI_3:27; percases ( da = d or db = d or ( da <> d & db <> d ) ) ; supposeA94: da = d ; ::_thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1 then A95: ( (Comput (P1,s1,(i + 1))) . d = ((Comput (P1,s1,i)) . da) div ((Comput (P1,s1,i)) . db) & (Comput (P2,s2,(i + 1))) . d = ((Comput (P2,s2,i)) . da) div ((Comput (P2,s2,i)) . db) ) by A12, A51, A37, A87, A88, A90, AMI_3:6; ((Comput (P1,(s1 +* (DataPart s2)),i)) . da) div ((Comput (P1,(s1 +* (DataPart s2)),i)) . db) = ((Comput (P1,s1,i)) . da) div ((Comput (P1,s1,i)) . db) by A2, A9, A31, A87, A90, A93, A92, A94, A6, AMI_5:21; hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = (Comput (P2,s2,(i + 1))) . d by A89, A93, A95, FUNCT_1:47 .= ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A31, A42, A93, FUNCT_1:47 ; ::_thesis: verum end; supposeA96: db = d ; ::_thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1 then ( (Comput (P1,s1,(i + 1))) . d = ((Comput (P1,s1,i)) . da) mod ((Comput (P1,s1,i)) . db) & (Comput (P2,s2,(i + 1))) . d = ((Comput (P2,s2,i)) . da) mod ((Comput (P2,s2,i)) . db) ) by A12, A51, A37, A87, A88, AMI_3:6; hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A2, A9, A31, A43, A87, A89, A93, A92, A96, A6, AMI_5:22; ::_thesis: verum end; suppose ( da <> d & db <> d ) ; ::_thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1 then ( (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d ) by A12, A51, A37, A87, A88, AMI_3:6; hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A31, A47, A93; ::_thesis: verum end; end; end; then (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A31, A42, GRFUNC_1:2; hence (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A31, A42, 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 A97: x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) ; ::_thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 then reconsider d = x as Data-Location by A17, AMI_2:def_16, AMI_3:27; percases ( da = d or db = d or ( da <> d & db <> d ) ) ; suppose da = d ; ::_thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 then ( (Comput (P2,s2,(i + 1))) . d = ((Comput (P2,s2,i)) . da) div ((Comput (P2,s2,i)) . db) & (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = ((Comput (P1,(s1 +* (DataPart s2)),i)) . da) div ((Comput (P1,(s1 +* (DataPart s2)),i)) . db) ) by A12, A37, A41, A87, A88, A90, AMI_3:6; hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A19, A89, A97; ::_thesis: verum end; suppose db = d ; ::_thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 then ( (Comput (P2,s2,(i + 1))) . d = ((Comput (P2,s2,i)) . da) mod ((Comput (P2,s2,i)) . db) & (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = ((Comput (P1,(s1 +* (DataPart s2)),i)) . da) mod ((Comput (P1,(s1 +* (DataPart s2)),i)) . db) ) by A12, A37, A41, A87, A88, AMI_3:6; hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A19, A89, A97; ::_thesis: verum end; suppose ( da <> d & db <> d ) ; ::_thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 then ( (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d ) by A12, A37, A41, A87, A88, AMI_3:6; hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A23, A97; ::_thesis: verum end; end; end; then DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1))) by A17, A18, GRFUNC_1:2; hence DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) by A17, A18, GRFUNC_1:3; ::_thesis: verum end; supposeA98: da = db ; ::_thesis: S1[i + 1] A99: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = succ (IC (Comput (P1,s1,i))) by A87, AMI_3:6; hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A11, A12, A51, A37, A52, A88, AMI_3:6; ::_thesis: ( IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) & (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) ) thus IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A11, A12, A32, A51, A37, A52, A88, A99, AMI_3:6; ::_thesis: ( (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) ) now__::_thesis:_for_x_being_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 ) assume A100: x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) ; ::_thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1 dom (DataPart p) c= Data-Locations by RELAT_1:58; then x in Data-Locations by A31, A100; then reconsider d = x as Data-Location by AMI_2:def_16, AMI_3:27; percases ( da = d or da <> d ) ; supposeA101: da = d ; ::_thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1 A102: ( ((Comput (P1,s1,i)) | (dom (DataPart p))) . d = (Comput (P1,s1,i)) . d & ((Comput (P2,s2,i)) | (dom (DataPart p))) . d = (Comput (P2,s2,i)) . d ) by A31, A40, A46, A100, FUNCT_1:47; A103: ( ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . d = (Comput (P1,s1,(i + 1))) . d & ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . d = (Comput (P2,s2,(i + 1))) . d ) by A31, A42, A100, FUNCT_1:47; (Comput (P2,s2,(i + 1))) . d = ((Comput (P2,s2,i)) . da) mod ((Comput (P2,s2,i)) . db) by A12, A37, A88, A98, A101, AMI_3:6; hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A13, A51, A87, A98, A101, A102, A103, AMI_3:6; ::_thesis: verum end; suppose da <> d ; ::_thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1 then ( (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d ) by A12, A51, A37, A87, A88, A98, AMI_3:6; hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A31, A47, A100; ::_thesis: verum end; end; end; then (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A31, A42, GRFUNC_1:2; hence (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A31, A42, 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 A104: x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) ; ::_thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 then reconsider d = x as Data-Location by A17, AMI_2:def_16, AMI_3:27; percases ( da = d or da <> d ) ; suppose da = d ; ::_thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 then ( (Comput (P2,s2,(i + 1))) . d = ((Comput (P2,s2,i)) . da) mod ((Comput (P2,s2,i)) . db) & (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = ((Comput (P1,(s1 +* (DataPart s2)),i)) . da) mod ((Comput (P1,(s1 +* (DataPart s2)),i)) . db) ) by A12, A37, A41, A87, A88, A98, AMI_3:6; hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A19, A89, A104; ::_thesis: verum end; suppose da <> d ; ::_thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 then ( (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d ) by A12, A37, A41, A87, A88, A98, AMI_3:6; hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A23, A104; ::_thesis: verum end; end; end; then DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1))) by A17, A18, GRFUNC_1:2; hence DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) by A17, A18, 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 A105: CurInstr (P1,(Comput (P1,s1,i))) = SCM-goto loc by AMI_5:13; A106: CurInstr (P2,(Comput (P2,s2,i))) = SCM-goto (loc + k) by A12, A105, Th1; thus (IC (Comput (P1,s1,(i + 1)))) + k = loc + k by A51, A105, AMI_3:7 .= IC (Comput (P2,s2,(i + 1))) by A37, A106, AMI_3:7 ; ::_thesis: ( IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) & (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) ) hence IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A32; ::_thesis: ( (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) ) now__::_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 A107: x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) ; ::_thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x dom (DataPart p) c= Data-Locations by RELAT_1:58; then x in Data-Locations by A31, A107; then reconsider d = x as Data-Location by AMI_2:def_16, AMI_3:27; ( (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d ) by A51, A37, A105, A106, AMI_3:7; hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A31, A47, A107; ::_thesis: verum end; then (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A31, A42, GRFUNC_1:2; hence (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A31, A42, 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 A108: x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) ; ::_thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x then reconsider d = x as Data-Location by A17, AMI_2:def_16, AMI_3:27; ( (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d ) by A37, A41, A105, A106, AMI_3:7; hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A23, A108; ::_thesis: verum end; then DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1))) by A17, A18, GRFUNC_1:2; hence DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) by A17, A18, 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 Data-Location such that A109: CurInstr (P1,(Comput (P1,s1,i))) = da =0_goto loc by AMI_5:14; A110: 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 A51, A109, AMI_3:8; ::_thesis: verum end; case (Comput (P1,s1,i)) . da <> 0 ; ::_thesis: (IC (Comput (P1,s1,(i + 1)))) + k = succ (IC (Comput (P2,s2,i))) hence (IC (Comput (P1,s1,(i + 1)))) + k = succ (IC (Comput (P2,s2,i))) by A11, A51, A52, A109, AMI_3:8; ::_thesis: verum end; end; end; A111: CurInstr (P2,(Comput (P2,s2,i))) = da =0_goto (loc + k) by A12, A109, Th2; A112: 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 A37, A111, AMI_3:8; ::_thesis: verum end; case (Comput (P2,s2,i)) . da <> 0 ; ::_thesis: IC (Comput (P2,s2,(i + 1))) = succ (IC (Comput (P2,s2,i))) hence IC (Comput (P2,s2,(i + 1))) = succ (IC (Comput (P2,s2,i))) by A37, A111, AMI_3:8; ::_thesis: verum end; end; end; A113: (Comput (P1,(s1 +* (DataPart s2)),i)) . da = (Comput (P2,s2,i)) . da by A27; A114: 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 A2, A9, A109, A113, A110, A112, A6, AMI_5:23; ::_thesis: verum end; suppose loc = succ (IC (Comput (P1,s1,i))) ; ::_thesis: (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A11, A52, A110, A112; ::_thesis: verum end; end; end; hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) ; ::_thesis: ( IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) & (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) ) thus IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A32, A114; ::_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 A115: x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) ; ::_thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x dom (DataPart p) c= Data-Locations by RELAT_1:58; then x in Data-Locations by A31, A115; then reconsider d = x as Data-Location by AMI_2:def_16, AMI_3:27; ( (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d ) by A51, A37, A109, A111, AMI_3:8; hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A31, A47, A115; ::_thesis: verum end; then (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A31, A42, GRFUNC_1:2; hence (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A31, A42, 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 A116: x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) ; ::_thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x then reconsider d = x as Data-Location by A17, AMI_2:def_16, AMI_3:27; ( (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d ) by A37, A41, A109, A111, AMI_3:8; hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A23, A116; ::_thesis: verum end; then DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1))) by A17, A18, GRFUNC_1:2; hence DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) by A17, A18, 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 Data-Location such that A117: CurInstr (P1,(Comput (P1,s1,i))) = da >0_goto loc by AMI_5:15; A118: 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 A51, A117, AMI_3:9; ::_thesis: verum end; case (Comput (P1,s1,i)) . da <= 0 ; ::_thesis: (IC (Comput (P1,s1,(i + 1)))) + k = succ (IC (Comput (P2,s2,i))) hence (IC (Comput (P1,s1,(i + 1)))) + k = succ (IC (Comput (P2,s2,i))) by A11, A51, A52, A117, AMI_3:9; ::_thesis: verum end; end; end; A119: CurInstr (P2,(Comput (P2,s2,i))) = da >0_goto (loc + k) by A12, A117, Th3; A120: 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 A37, A119, AMI_3:9; ::_thesis: verum end; case (Comput (P2,s2,i)) . da <= 0 ; ::_thesis: IC (Comput (P2,s2,(i + 1))) = succ (IC (Comput (P2,s2,i))) hence IC (Comput (P2,s2,(i + 1))) = succ (IC (Comput (P2,s2,i))) by A37, A119, AMI_3:9; ::_thesis: verum end; end; end; A121: (Comput (P1,(s1 +* (DataPart s2)),i)) . da = (Comput (P2,s2,i)) . da by A27; A122: 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 A2, A9, A117, A121, A118, A120, A6, AMI_5:24; ::_thesis: verum end; suppose loc = succ (IC (Comput (P1,s1,i))) ; ::_thesis: (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A11, A52, A118, A120; ::_thesis: verum end; end; end; hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) ; ::_thesis: ( IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) & (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) ) thus IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A32, A122; ::_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 A123: x in dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) ; ::_thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x dom (DataPart p) c= Data-Locations by RELAT_1:58; then x in Data-Locations by A31, A123; then reconsider d = x as Data-Location by AMI_2:def_16, AMI_3:27; ( (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d ) by A51, A37, A117, A119, AMI_3:9; hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A31, A47, A123; ::_thesis: verum end; then (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A31, A42, GRFUNC_1:2; hence (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A31, A42, 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 A124: x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) ; ::_thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x then reconsider d = x as Data-Location by A17, AMI_2:def_16, AMI_3:27; ( (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = (Comput (P1,(s1 +* (DataPart s2)),i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d ) by A37, A41, A117, A119, AMI_3:9; hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A23, A124; ::_thesis: verum end; then DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1))) by A17, A18, GRFUNC_1:2; hence DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) by A17, A18, GRFUNC_1:3; ::_thesis: verum end; end; end; A125: DataPart p c= p by RELAT_1:59; A126: 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 by EXTPRO_1:2 .= (IC p) + k by A2, A4, GRFUNC_1:2 .= (IC p) + k .= IC (IncIC (p,k)) by MEMSTR_0:53 .= IC s2 by A3, A126, GRFUNC_1:2 .= IC (Comput (P2,s2,0)) by EXTPRO_1:2 ; ::_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 ; A127: IC p = IC s1 by A2, A4, GRFUNC_1:2; then IC p = IC (Comput (P1,s1,0)) by EXTPRO_1:2; then A128: loc in dom q by A8, A5, AMISTD_5:def_4; A129: (IC p) + k in dom (Reloc (q,k)) by A128, COMPOS_1:46; A130: IC in dom (IncIC (p,k)) by MEMSTR_0:52; A131: q . (IC p) = P1 . (IC s1) by A127, A128, A6, GRFUNC_1:2; dom P2 = NAT by PARTFUN1:def_2; then A132: CurInstr (P2,(Comput (P2,s2,0))) = P2 . (IC (Comput (P2,s2,0))) by PARTFUN1:def_6 .= P2 . (IC s2) by EXTPRO_1:2 .= P2 . (IC (IncIC (p,k))) by A3, A130, GRFUNC_1:2 .= P2 . ((IC p) + k) by MEMSTR_0:53 .= P2 . ((IC p) + k) .= (Reloc (q,k)) . ((IC p) + k) by A129, A6, GRFUNC_1:2 ; A133: dom P1 = NAT by PARTFUN1:def_2; CurInstr (P1,(Comput (P1,s1,0))) = CurInstr (P1,s1) by EXTPRO_1:2 .= P1 . (IC s1) by A133, PARTFUN1:def_6 ; hence IncAddr ((CurInstr (P1,(Comput (P1,s1,0)))),k) = CurInstr (P2,(Comput (P2,s2,0))) by A128, A131, A132, 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)) ) A134: dom (DataPart s2) = Data-Locations by MEMSTR_0:9; A135: DataPart p c= s1 by A2, A125, XBOOLE_1:1; A136: DataPart (IncIC (p,k)) = DataPart p by MEMSTR_0:51; DataPart p c= IncIC (p,k) by A136, MEMSTR_0:12; then A137: DataPart p c= s2 by A3, XBOOLE_1:1; thus (Comput (P1,s1,0)) | (dom (DataPart p)) = s1 | (dom (DataPart p)) by EXTPRO_1:2 .= DataPart p by A135, GRFUNC_1:23 .= s2 | (dom (DataPart p)) by A137, GRFUNC_1:23 .= (Comput (P2,s2,0)) | (dom (DataPart p)) by EXTPRO_1:2 ; ::_thesis: DataPart (Comput (P1,(s1 +* (DataPart s2)),0)) = DataPart (Comput (P2,s2,0)) thus DataPart (Comput (P1,(s1 +* (DataPart s2)),0)) = DataPart (s1 +* (DataPart s2)) by EXTPRO_1:2 .= DataPart s2 by A134, FUNCT_4:23 .= DataPart (Comput (P2,s2,0)) by EXTPRO_1:2 ; ::_thesis: verum end; then A138: S1[ 0 ] ; thus for i being Element of NAT holds S1[i] from NAT_1:sch_1(A138, A10); ::_thesis: verum end; theorem :: RELOC:6 for k being Element of NAT for q being NAT -defined the InstructionsF of SCM -valued finite non halt-free Function for p being non empty b2 -autonomic FinPartState of SCM for s1, s2 being State of SCM st IC in dom p & p c= s1 & IncIC (p,k) c= s2 holds for P1, P2 being Instruction-Sequence of SCM st q c= P1 & Reloc (q,k) c= P2 holds for i being Element of NAT holds (IC (Comput (P1,s1,i))) + k = IC (Comput (P2,s2,i)) by Lm1; registration cluster SCM -> relocable1 relocable2 ; coherence ( SCM is relocable1 & SCM is relocable2 ) proof thus SCM is relocable1 ::_thesis: SCM is relocable2 proof thus for k being Element of NAT for q being NAT -defined the InstructionsF of SCM -valued finite non halt-free Function for p being non empty b2 -autonomic FinPartState of SCM for s1, s2 being State of SCM st p c= s1 & IncIC (p,k) c= s2 holds for P1, P2 being Instruction-Sequence of SCM st q c= P1 & Reloc (q,k) c= P2 holds for i being Element of NAT holds IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = CurInstr (P2,(Comput (P2,s2,i))) by Lm1; :: according to AMISTD_5:def_5 ::_thesis: verum end; 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)) | (proj1 (DataPart b2)) = (Comput (b6,b4,b7)) | (proj1 (DataPart b2)) ) ) let q be NAT -defined the InstructionsF of SCM -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)) | (proj1 (DataPart b1)) = (Comput (b5,b3,b6)) | (proj1 (DataPart b1)) ) ) let p be non empty q -autonomic FinPartState of SCM; ::_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)) | (proj1 (DataPart p)) = (Comput (b4,b2,b5)) | (proj1 (DataPart p)) ) ) let s1, s2 be State of SCM; ::_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)) | (proj1 (DataPart p)) = (Comput (b2,s2,b3)) | (proj1 (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)) | (proj1 (DataPart p)) = (Comput (b2,s2,b3)) | (proj1 (DataPart p)) ) let P1, P2 be Instruction-Sequence of SCM; ::_thesis: ( not q c= P1 or not Reloc (q,k) c= P2 or for b1 being Element of NAT holds (Comput (P1,s1,b1)) | (proj1 (DataPart p)) = (Comput (P2,s2,b1)) | (proj1 (DataPart p)) ) assume A2: ( q c= P1 & Reloc (q,k) c= P2 ) ; ::_thesis: for b1 being Element of NAT holds (Comput (P1,s1,b1)) | (proj1 (DataPart p)) = (Comput (P2,s2,b1)) | (proj1 (DataPart p)) thus for i being Element of NAT holds (Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart p)) by A1, Lm1, A2; ::_thesis: verum end; end; theorem :: RELOC:7 for k being Element of NAT for q being NAT -defined the InstructionsF of SCM -valued finite non halt-free Function for p being non empty b2 -autonomic FinPartState of SCM for s1, s2, s3 being State of SCM st IC in dom p & p c= s1 & IncIC (p,k) c= s2 & s3 = s1 +* (DataPart s2) holds for P1, P2 being Instruction-Sequence of SCM st q c= P1 & Reloc (q,k) c= P2 holds for i being Element of NAT holds DataPart (Comput (P1,s3,i)) = DataPart (Comput (P2,s2,i)) by Lm1;