:: SCMRING4 semantic presentation begin theorem Th1: :: SCMRING4:1 for n being Element of NAT for R being non trivial Ring holds dl. (R,n) = [1,n] proof let n be Element of NAT ; ::_thesis: for R being non trivial Ring holds dl. (R,n) = [1,n] let R be non trivial Ring; ::_thesis: dl. (R,n) = [1,n] thus dl. (R,n) = dl. n by SCMRING3:def_1 .= [1,n] ; ::_thesis: verum end; theorem :: SCMRING4:2 for R being non trivial Ring for dl being Data-Location of R ex i being Element of NAT st dl = dl. (R,i) proof let R be non trivial Ring; ::_thesis: for dl being Data-Location of R ex i being Element of NAT st dl = dl. (R,i) let dl be Data-Location of R; ::_thesis: ex i being Element of NAT st dl = dl. (R,i) dl in Data-Locations by SCMRING2:1; then consider i being Element of NAT such that A1: dl = [1,i] by AMI_2:23, AMI_3:27; take i ; ::_thesis: dl = dl. (R,i) thus dl = dl. (R,i) by A1, Th1; ::_thesis: verum end; theorem :: SCMRING4:3 for R being non trivial Ring for i, j being Element of NAT st i <> j holds dl. (R,i) <> dl. (R,j) proof let R be non trivial Ring; ::_thesis: for i, j being Element of NAT st i <> j holds dl. (R,i) <> dl. (R,j) let i, j be Element of NAT ; ::_thesis: ( i <> j implies dl. (R,i) <> dl. (R,j) ) assume A1: i <> j ; ::_thesis: dl. (R,i) <> dl. (R,j) ( dl. (R,j) = [1,j] & dl. (R,i) = [1,i] ) by Th1; hence dl. (R,i) <> dl. (R,j) by A1, XTUPLE_0:1; ::_thesis: verum end; theorem :: SCMRING4:4 for R being non trivial Ring for s being State of (SCM R) holds Data-Locations c= dom s proof let R be non trivial Ring; ::_thesis: for s being State of (SCM R) holds Data-Locations c= dom s let s be State of (SCM R); ::_thesis: Data-Locations c= dom s Data-Locations = Data-Locations by SCMRING2:22; hence Data-Locations c= dom s by MEMSTR_0:8; ::_thesis: verum end; theorem Th5: :: SCMRING4:5 for R being non trivial Ring for a being Data-Location of R for loc being Element of NAT for s being State of (SCM R) holds s . a = (s +* (Start-At (loc,(SCM R)))) . a proof let R be non trivial Ring; ::_thesis: for a being Data-Location of R for loc being Element of NAT for s being State of (SCM R) holds s . a = (s +* (Start-At (loc,(SCM R)))) . a let a be Data-Location of R; ::_thesis: for loc being Element of NAT for s being State of (SCM R) holds s . a = (s +* (Start-At (loc,(SCM R)))) . a let loc be Element of NAT ; ::_thesis: for s being State of (SCM R) holds s . a = (s +* (Start-At (loc,(SCM R)))) . a let s be State of (SCM R); ::_thesis: s . a = (s +* (Start-At (loc,(SCM R)))) . a a in the carrier of (SCM R) ; then a in dom s by PARTFUN1:def_2; then A1: ( dom (Start-At (loc,(SCM R))) = {(IC )} & a in (dom s) \/ (dom (Start-At (loc,(SCM R)))) ) by FUNCOP_1:13, XBOOLE_0:def_3; a <> IC by SCMRING3:2; then not a in {(IC )} by TARSKI:def_1; hence s . a = (s +* (Start-At (loc,(SCM R)))) . a by A1, FUNCT_4:def_1; ::_thesis: verum end; theorem Th6: :: SCMRING4:6 for R being non trivial Ring for s1, s2 being State of (SCM R) st IC s1 = IC s2 & ( for a being Data-Location of R holds s1 . a = s2 . a ) holds s1 = s2 proof let R be non trivial Ring; ::_thesis: for s1, s2 being State of (SCM R) st IC s1 = IC s2 & ( for a being Data-Location of R holds s1 . a = s2 . a ) holds s1 = s2 let s1, s2 be State of (SCM R); ::_thesis: ( IC s1 = IC s2 & ( for a being Data-Location of R holds s1 . a = s2 . a ) implies s1 = s2 ) assume A1: IC s1 = IC s2 ; ::_thesis: ( ex a being Data-Location of R st not s1 . a = s2 . a or s1 = s2 ) ( IC in dom s1 & IC in dom s2 ) by MEMSTR_0:2; then A2: ( s1 = (DataPart s1) +* (Start-At ((IC s1),(SCM R))) & s2 = (DataPart s2) +* (Start-At ((IC s2),(SCM R))) ) by MEMSTR_0:26; assume A3: for a being Data-Location of R holds s1 . a = s2 . a ; ::_thesis: s1 = s2 DataPart s1 = DataPart s2 proof A4: dom (DataPart s1) = Data-Locations by MEMSTR_0:9; hence dom (DataPart s1) = dom (DataPart s2) by MEMSTR_0:9; :: according to FUNCT_1:def_11 ::_thesis: for b1 being set holds ( not b1 in dom (DataPart s1) or (DataPart s1) . b1 = (DataPart s2) . b1 ) let x be set ; ::_thesis: ( not x in dom (DataPart s1) or (DataPart s1) . x = (DataPart s2) . x ) assume A5: x in dom (DataPart s1) ; ::_thesis: (DataPart s1) . x = (DataPart s2) . x then A6: x is Data-Location of R by A4, SCMRING2:23; thus (DataPart s1) . x = s1 . x by A5, A4, FUNCT_1:49 .= s2 . x by A6, A3 .= (DataPart s2) . x by A5, A4, FUNCT_1:49 ; ::_thesis: verum end; hence s1 = s2 by A1, A2; ::_thesis: verum end; registration let R be non trivial Ring; cluster SCM R -> relocable ; coherence SCM R is relocable proof let INS be Instruction of (SCM R); :: 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 R); ::_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 ) by NAT_1:31, SCMRING3:39; 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 R) by SCMRING3:12; Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))) = 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 of R such that A3: INS = da := db by SCMRING3:13; now__::_thesis:_for_d_being_Data-Location_of_R_holds_(Exec_((IncAddr_(INS,(j_+_k))),(IncIC_(s,k))))_._d_=_(IncIC_((Exec_((IncAddr_(INS,j)),s)),k))_._d let d be Data-Location of R; ::_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, SCMRING2:11 .= s . db by Th5 .= (Exec (INS,s)) . d by A3, A4, SCMRING2:11 .= (Exec ((IncAddr (INS,j)),s)) . d by A3, COMPOS_0:4 .= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by Th5 ; ::_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, SCMRING2:11 .= s . d by Th5 .= (Exec (INS,s)) . d by A3, A5, SCMRING2:11 .= (Exec ((IncAddr (INS,j)),s)) . d by A3, COMPOS_0:4 .= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by Th5 ; ::_thesis: verum end; end; end; hence Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))) = IncIC ((Exec ((IncAddr (INS,j)),s)),k) by Th6, A1; ::_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 of R such that A6: INS = AddTo (da,db) by SCMRING3:14; now__::_thesis:_for_d_being_Data-Location_of_R_holds_(Exec_((IncAddr_(INS,(j_+_k))),(IncIC_(s,k))))_._d_=_(IncIC_((Exec_((IncAddr_(INS,j)),s)),k))_._d let d be Data-Location of R; ::_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, SCMRING2:12 .= (s . da) + ((IncIC (s,k)) . db) by Th5 .= (s . da) + (s . db) by Th5 .= (Exec (INS,s)) . d by A6, A7, SCMRING2:12 .= (Exec ((IncAddr (INS,j)),s)) . d by A6, COMPOS_0:4 .= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by Th5 ; ::_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, SCMRING2:12 .= s . d by Th5 .= (Exec (INS,s)) . d by A6, A8, SCMRING2:12 .= (Exec ((IncAddr (INS,j)),s)) . d by A6, COMPOS_0:4 .= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by Th5 ; ::_thesis: verum end; end; end; hence Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))) = IncIC ((Exec ((IncAddr (INS,j)),s)),k) by Th6, A1; ::_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 of R such that A9: INS = SubFrom (da,db) by SCMRING3:15; now__::_thesis:_for_d_being_Data-Location_of_R_holds_(Exec_((IncAddr_(INS,(j_+_k))),(IncIC_(s,k))))_._d_=_(IncIC_((Exec_((IncAddr_(INS,j)),s)),k))_._d let d be Data-Location of R; ::_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, SCMRING2:13 .= (s . da) - ((IncIC (s,k)) . db) by Th5 .= (s . da) - (s . db) by Th5 .= (Exec (INS,s)) . d by A9, A10, SCMRING2:13 .= (Exec ((IncAddr (INS,j)),s)) . d by A9, COMPOS_0:4 .= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by Th5 ; ::_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, SCMRING2:13 .= s . d by Th5 .= (Exec (INS,s)) . d by A9, A11, SCMRING2:13 .= (Exec ((IncAddr (INS,j)),s)) . d by A9, COMPOS_0:4 .= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by Th5 ; ::_thesis: verum end; end; end; hence Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))) = IncIC ((Exec ((IncAddr (INS,j)),s)),k) by Th6, A1; ::_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 of R such that A12: INS = MultBy (da,db) by SCMRING3:16; now__::_thesis:_for_d_being_Data-Location_of_R_holds_(Exec_((IncAddr_(INS,(j_+_k))),(IncIC_(s,k))))_._d_=_(IncIC_((Exec_((IncAddr_(INS,j)),s)),k))_._d let d be Data-Location of R; ::_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, SCMRING2:14 .= (s . da) * ((IncIC (s,k)) . db) by Th5 .= (s . da) * (s . db) by Th5 .= (Exec (INS,s)) . d by A12, A13, SCMRING2:14 .= (Exec ((IncAddr (INS,j)),s)) . d by A12, COMPOS_0:4 .= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by Th5 ; ::_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, SCMRING2:14 .= s . d by Th5 .= (Exec (INS,s)) . d by A12, A14, SCMRING2:14 .= (Exec ((IncAddr (INS,j)),s)) . d by A12, COMPOS_0:4 .= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by Th5 ; ::_thesis: verum end; end; end; hence Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))) = IncIC ((Exec ((IncAddr (INS,j)),s)),k) by Th6, A1; ::_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 being Data-Location of R, r being Element of R such that A15: INS = da := r by SCMRING3:17; now__::_thesis:_for_d_being_Data-Location_of_R_holds_(Exec_((IncAddr_(INS,(j_+_k))),(IncIC_(s,k))))_._d_=_(IncIC_((Exec_((IncAddr_(INS,j)),s)),k))_._d let d be Data-Location of R; ::_thesis: (Exec ((IncAddr (INS,(j + k))),(IncIC (s,k)))) . b1 = (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . b1 percases ( da = d or da <> d ) ; supposeA16: 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 .= r by A16, A15, SCMRING2:17 .= (Exec (INS,s)) . d by A15, A16, SCMRING2:17 .= (Exec ((IncAddr (INS,j)),s)) . d by A15, COMPOS_0:4 .= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by Th5 ; ::_thesis: verum end; supposeA17: 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, A17, SCMRING2:17 .= s . d by Th5 .= (Exec (INS,s)) . d by A15, A17, SCMRING2:17 .= (Exec ((IncAddr (INS,j)),s)) . d by A15, COMPOS_0:4 .= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by Th5 ; ::_thesis: verum end; end; end; hence Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))) = IncIC ((Exec ((IncAddr (INS,j)),s)),k) by Th6, A1; ::_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 A18: INS = goto (loc,R) by SCMRING3:18; A19: IncAddr (INS,(j + k)) = goto ((loc + (j + k)),R) by A18, SCMRING3:37; A20: IncAddr (INS,j) = goto ((loc + j),R) by A18, SCMRING3:37; now__::_thesis:_for_d_being_Data-Location_of_R_holds_(Exec_((IncAddr_(INS,(j_+_k))),(IncIC_(s,k))))_._d_=_(IncIC_((Exec_((IncAddr_(INS,j)),s)),k))_._d let d be Data-Location of R; ::_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 A19, SCMRING2:15 .= s . d by Th5 .= (Exec ((IncAddr (INS,j)),s)) . d by A20, SCMRING2:15 .= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by Th5 ; ::_thesis: verum end; hence Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))) = IncIC ((Exec ((IncAddr (INS,j)),s)),k) by Th6, A1; ::_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 da being Data-Location of R, loc being Element of NAT such that A21: INS = da =0_goto loc by SCMRING3:19; A22: IncAddr (INS,(j + k)) = da =0_goto (loc + (j + k)) by A21, SCMRING3:38; A23: IncAddr (INS,j) = da =0_goto (loc + j) by A21, SCMRING3:38; now__::_thesis:_for_d_being_Data-Location_of_R_holds_(Exec_((IncAddr_(INS,(j_+_k))),(IncIC_(s,k))))_._d_=_(IncIC_((Exec_((IncAddr_(INS,j)),s)),k))_._d let d be Data-Location of R; ::_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 A22, SCMRING2:16 .= s . d by Th5 .= (Exec ((IncAddr (INS,j)),s)) . d by A23, SCMRING2:16 .= (IncIC ((Exec ((IncAddr (INS,j)),s)),k)) . d by Th5 ; ::_thesis: verum end; hence Exec ((IncAddr (INS,(j + k))),(IncIC (s,k))) = IncIC ((Exec ((IncAddr (INS,j)),s)),k) by A1, Th6; ::_thesis: verum end; end; end; end; definition let R be non trivial Ring; let a be Data-Location of R; let r be Element of R; :: original: .--> redefine funca .--> r -> FinPartState of (SCM R); coherence a .--> r is FinPartState of (SCM R) proof set k = a .--> r; set f = the_Values_of (SCM R); reconsider b = a as Element of SCM-Memory by SCMRING2:def_1; A1: dom (a .--> r) = {a} by FUNCOP_1:13; for x being set st x in dom (a .--> r) holds (a .--> r) . x in (the_Values_of (SCM R)) . x proof let x be set ; ::_thesis: ( x in dom (a .--> r) implies (a .--> r) . x in (the_Values_of (SCM R)) . x ) assume A2: x in dom (a .--> r) ; ::_thesis: (a .--> r) . x in (the_Values_of (SCM R)) . x then x = a by A1, TARSKI:def_1; then A3: (a .--> r) . x = r by FUNCOP_1:72; a in Data-Locations by SCMRING2:1; then A4: a in SCM-Data-Loc by AMI_3:27; (the_Values_of (SCM R)) . x = Values a by A1, A2, TARSKI:def_1 .= (the_Values_of (SCM R)) . a .= ((SCM-VAL R) * SCM-OK) . a by SCMRING2:24 .= the carrier of R by A4, SCMRING1:3 ; hence (a .--> r) . x in (the_Values_of (SCM R)) . x by A3; ::_thesis: verum end; hence a .--> r is FinPartState of (SCM R) by FUNCT_1:def_14; ::_thesis: verum end; end; registration let R be non trivial Ring; cluster SCM R -> IC-recognized ; coherence SCM R is IC-recognized proof for q being NAT -defined the InstructionsF of (SCM R) -valued finite non halt-free Function for p being b1 -autonomic FinPartState of (SCM R) st DataPart p <> {} holds IC in dom p proof let q be NAT -defined the InstructionsF of (SCM R) -valued finite non halt-free Function; ::_thesis: for p being q -autonomic FinPartState of (SCM R) st DataPart p <> {} holds IC in dom p let p be q -autonomic FinPartState of (SCM R); ::_thesis: ( DataPart p <> {} implies IC in dom p ) assume DataPart p <> {} ; ::_thesis: IC in dom p then A1: dom (DataPart p) <> {} ; assume A2: not IC in dom p ; ::_thesis: contradiction not p is q -autonomic proof set il = the Element of NAT \ (dom q); set d2 = the Element of (Data-Locations ) \ (dom p); set d1 = the Element of dom (DataPart p); A3: the Element of dom (DataPart p) in dom (DataPart p) by A1; DataPart p c= p by MEMSTR_0:12; then A4: dom (DataPart p) c= dom p by RELAT_1:11; dom (DataPart p) c= the carrier of (SCM R) by RELAT_1:def_18; then reconsider d1 = the Element of dom (DataPart p) as Element of (SCM R) by A3; not Data-Locations c= dom p ; then A5: (Data-Locations ) \ (dom p) <> {} by XBOOLE_1:37; then the Element of (Data-Locations ) \ (dom p) in Data-Locations by XBOOLE_0:def_5; then reconsider d2 = the Element of (Data-Locations ) \ (dom p) as Data-Location of R by SCMRING2:1; not d2 in dom p by A5, XBOOLE_0:def_5; then A6: dom p misses {d2} by ZFMISC_1:50; not NAT c= dom q ; then A7: NAT \ (dom q) <> {} by XBOOLE_1:37; then reconsider il = the Element of NAT \ (dom q) as Element of NAT by XBOOLE_0:def_5; A8: not il in dom q by A7, XBOOLE_0:def_5; Data-Locations = Data-Locations by SCMRING2:22; then dom (DataPart p) c= Data-Locations by RELAT_1:58; then reconsider d1 = d1 as Data-Location of R by A3, SCMRING2:1; A9: dom ((d2 .--> (0. R)) +* (Start-At (il,(SCM R)))) = (dom (d2 .--> (0. R))) \/ (dom (Start-At (il,(SCM R)))) by FUNCT_4:def_1; set p1 = p +* ((d2 .--> (0. R)) +* (Start-At (il,(SCM R)))); set q1 = q +* (il .--> (d1 := d2)); consider s1 being State of (SCM R) such that A10: p +* ((d2 .--> (0. R)) +* (Start-At (il,(SCM R)))) c= s1 by PBOOLE:141; consider S1 being Instruction-Sequence of (SCM R) such that A11: q +* (il .--> (d1 := d2)) c= S1 by PBOOLE:145; A12: dom (p +* ((d2 .--> (0. R)) +* (Start-At (il,(SCM R))))) = (dom p) \/ (dom ((d2 .--> (0. R)) +* (Start-At (il,(SCM R))))) by FUNCT_4:def_1; A13: dom (Start-At (il,(SCM R))) = {(IC )} by FUNCOP_1:13; then A14: IC in dom (Start-At (il,(SCM R))) by TARSKI:def_1; then A15: IC in dom ((d2 .--> (0. R)) +* (Start-At (il,(SCM R)))) by A9, XBOOLE_0:def_3; then IC in dom (p +* ((d2 .--> (0. R)) +* (Start-At (il,(SCM R))))) by A12, XBOOLE_0:def_3; then A16: IC s1 = (p +* ((d2 .--> (0. R)) +* (Start-At (il,(SCM R))))) . (IC ) by A10, GRFUNC_1:2 .= ((d2 .--> (0. R)) +* (Start-At (il,(SCM R)))) . (IC ) by A15, FUNCT_4:13 .= (Start-At (il,(SCM R))) . (IC ) by A14, FUNCT_4:13 .= il by FUNCOP_1:72 ; A17: dom (Start-At (il,(SCM R))) = {(IC )} by FUNCOP_1:13; A18: d2 <> IC by SCMRING3:2; then A19: not d2 in dom (Start-At (il,(SCM R))) by A13, TARSKI:def_1; A20: not d2 in dom (Start-At (il,(SCM R))) by A18, A17, TARSKI:def_1; dom (d2 .--> (0. R)) = {d2} by FUNCOP_1:13; then d2 in dom (d2 .--> (0. R)) by TARSKI:def_1; then A21: d2 in dom ((d2 .--> (0. R)) +* (Start-At (il,(SCM R)))) by A9, XBOOLE_0:def_3; then d2 in dom (p +* ((d2 .--> (0. R)) +* (Start-At (il,(SCM R))))) by A12, XBOOLE_0:def_3; then A22: s1 . d2 = (p +* ((d2 .--> (0. R)) +* (Start-At (il,(SCM R))))) . d2 by A10, GRFUNC_1:2 .= ((d2 .--> (0. R)) +* (Start-At (il,(SCM R)))) . d2 by A21, FUNCT_4:13 .= (d2 .--> (0. R)) . d2 by A19, FUNCT_4:11 .= 0. R by FUNCOP_1:72 ; A23: dom (il .--> (d1 := d2)) = {il} by FUNCOP_1:13; then A24: il in dom (il .--> (d1 := d2)) by TARSKI:def_1; dom (q +* (il .--> (d1 := d2))) = (dom q) \/ (dom (il .--> (d1 := d2))) by FUNCT_4:def_1; then il in dom (q +* (il .--> (d1 := d2))) by A24, XBOOLE_0:def_3; then A25: S1 . il = (q +* (il .--> (d1 := d2))) . il by A11, GRFUNC_1:2 .= (il .--> (d1 := d2)) . il by A24, FUNCT_4:13 .= d1 := d2 by FUNCOP_1:72 ; A26: dom p c= the carrier of (SCM R) by RELAT_1:def_18; dom (Comput (S1,s1,1)) = the carrier of (SCM R) by PARTFUN1:def_2; then A27: dom ((Comput (S1,s1,1)) | (dom p)) = dom p by A26, RELAT_1:62; consider e being Element of R such that A28: e <> 0. R by STRUCT_0:def_18; set p2 = p +* ((d2 .--> e) +* (Start-At (il,(SCM R)))); set q2 = q +* (il .--> (d1 := d2)); consider s2 being State of (SCM R) such that A29: p +* ((d2 .--> e) +* (Start-At (il,(SCM R)))) c= s2 by PBOOLE:141; consider S2 being Instruction-Sequence of (SCM R) such that A30: q +* (il .--> (d1 := d2)) c= S2 by PBOOLE:145; A31: dom (Comput (S2,s2,1)) = the carrier of (SCM R) by PARTFUN1:def_2; A32: dom ((Comput (S2,s2,1)) | (dom p)) = dom p by A26, A31, RELAT_1:62; dom p misses {(IC )} by A2, ZFMISC_1:50; then A33: (dom p) /\ {(IC )} = {} by XBOOLE_0:def_7; take P = S1; :: according to EXTPRO_1:def_10 ::_thesis: ex b1 being set st ( q c= P & q c= b1 & ex b2, b3 being set st ( p c= b2 & p c= b3 & not for b4 being Element of NAT holds (Comput (P,b2,b4)) | (dom p) = (Comput (b1,b3,b4)) | (dom p) ) ) take Q = S2; ::_thesis: ( q c= P & q c= Q & ex b1, b2 being set st ( p c= b1 & p c= b2 & not for b3 being Element of NAT holds (Comput (P,b1,b3)) | (dom p) = (Comput (Q,b2,b3)) | (dom p) ) ) dom ((d2 .--> (0. R)) +* (Start-At (il,(SCM R)))) = (dom (d2 .--> (0. R))) \/ (dom (Start-At (il,(SCM R)))) by FUNCT_4:def_1 .= (dom (d2 .--> (0. R))) \/ {(IC )} by FUNCOP_1:13 .= {d2} \/ {(IC )} by FUNCOP_1:13 ; then (dom p) /\ (dom ((d2 .--> (0. R)) +* (Start-At (il,(SCM R))))) = ((dom p) /\ {d2}) \/ {} by A33, XBOOLE_1:23 .= {} by A6, XBOOLE_0:def_7 ; then dom p misses dom ((d2 .--> (0. R)) +* (Start-At (il,(SCM R)))) by XBOOLE_0:def_7; then p c= p +* ((d2 .--> (0. R)) +* (Start-At (il,(SCM R)))) by FUNCT_4:32; then A34: p c= s1 by A10, XBOOLE_1:1; A35: dom q misses dom (il .--> (d1 := d2)) by A23, A8, ZFMISC_1:50; then q c= q +* (il .--> (d1 := d2)) by FUNCT_4:32; hence q c= P by A11, XBOOLE_1:1; ::_thesis: ( q c= Q & ex b1, b2 being set st ( p c= b1 & p c= b2 & not for b3 being Element of NAT holds (Comput (P,b1,b3)) | (dom p) = (Comput (Q,b2,b3)) | (dom p) ) ) dom ((d2 .--> e) +* (Start-At (il,(SCM R)))) = (dom (d2 .--> e)) \/ (dom (Start-At (il,(SCM R)))) by FUNCT_4:def_1 .= (dom (d2 .--> e)) \/ {(IC )} by FUNCOP_1:13 .= {d2} \/ {(IC )} by FUNCOP_1:13 ; then (dom p) /\ (dom ((d2 .--> e) +* (Start-At (il,(SCM R))))) = ((dom p) /\ {d2}) \/ {} by A33, XBOOLE_1:23 .= {} by A6, XBOOLE_0:def_7 ; then dom p misses dom ((d2 .--> e) +* (Start-At (il,(SCM R)))) by XBOOLE_0:def_7; then p c= p +* ((d2 .--> e) +* (Start-At (il,(SCM R)))) by FUNCT_4:32; then A36: p c= s2 by A29, XBOOLE_1:1; q c= q +* (il .--> (d1 := d2)) by A35, FUNCT_4:32; hence q c= Q by A30, XBOOLE_1:1; ::_thesis: ex b1, b2 being set st ( p c= b1 & p c= b2 & not for b3 being Element of NAT holds (Comput (P,b1,b3)) | (dom p) = (Comput (Q,b2,b3)) | (dom p) ) take s1 ; ::_thesis: ex b1 being set st ( p c= s1 & p c= b1 & not for b2 being Element of NAT holds (Comput (P,s1,b2)) | (dom p) = (Comput (Q,b1,b2)) | (dom p) ) take s2 ; ::_thesis: ( p c= s1 & p c= s2 & not for b1 being Element of NAT holds (Comput (P,s1,b1)) | (dom p) = (Comput (Q,s2,b1)) | (dom p) ) thus p c= s1 by A34; ::_thesis: ( p c= s2 & not for b1 being Element of NAT holds (Comput (P,s1,b1)) | (dom p) = (Comput (Q,s2,b1)) | (dom p) ) thus p c= s2 by A36; ::_thesis: not for b1 being Element of NAT holds (Comput (P,s1,b1)) | (dom p) = (Comput (Q,s2,b1)) | (dom p) take 1 ; ::_thesis: not (Comput (P,s1,1)) | (dom p) = (Comput (Q,s2,1)) | (dom p) A37: dom ((d2 .--> e) +* (Start-At (il,(SCM R)))) = (dom (d2 .--> e)) \/ (dom (Start-At (il,(SCM R)))) by FUNCT_4:def_1; A38: dom (d2 .--> e) = {d2} by FUNCOP_1:13; A39: dom (p +* ((d2 .--> e) +* (Start-At (il,(SCM R))))) = (dom p) \/ (dom ((d2 .--> e) +* (Start-At (il,(SCM R))))) by FUNCT_4:def_1; A40: IC in dom (Start-At (il,(SCM R))) by A17, TARSKI:def_1; then A41: IC in dom ((d2 .--> e) +* (Start-At (il,(SCM R)))) by A37, XBOOLE_0:def_3; then IC in dom (p +* ((d2 .--> e) +* (Start-At (il,(SCM R))))) by A39, XBOOLE_0:def_3; then A42: IC s2 = (p +* ((d2 .--> e) +* (Start-At (il,(SCM R))))) . (IC ) by A29, GRFUNC_1:2 .= ((d2 .--> e) +* (Start-At (il,(SCM R)))) . (IC ) by A41, FUNCT_4:13 .= (Start-At (il,(SCM R))) . (IC ) by A40, FUNCT_4:13 .= il by FUNCOP_1:72 ; dom (il .--> (d1 := d2)) = {il} by FUNCOP_1:13; then A43: il in dom (il .--> (d1 := d2)) by TARSKI:def_1; dom (q +* (il .--> (d1 := d2))) = (dom q) \/ (dom (il .--> (d1 := d2))) by FUNCT_4:def_1; then il in dom (q +* (il .--> (d1 := d2))) by A43, XBOOLE_0:def_3; then A44: S2 . il = (q +* (il .--> (d1 := d2))) . il by A30, GRFUNC_1:2 .= (il .--> (d1 := d2)) . il by A43, FUNCT_4:13 .= d1 := d2 by FUNCOP_1:72 ; d2 in dom (d2 .--> e) by A38, TARSKI:def_1; then A45: d2 in dom ((d2 .--> e) +* (Start-At (il,(SCM R)))) by A37, XBOOLE_0:def_3; then d2 in dom (p +* ((d2 .--> e) +* (Start-At (il,(SCM R))))) by A39, XBOOLE_0:def_3; then A46: s2 . d2 = (p +* ((d2 .--> e) +* (Start-At (il,(SCM R))))) . d2 by A29, GRFUNC_1:2 .= ((d2 .--> e) +* (Start-At (il,(SCM R)))) . d2 by A45, FUNCT_4:13 .= (d2 .--> e) . d2 by A20, FUNCT_4:11 .= e by FUNCOP_1:72 ; A47: S2 /. il = S2 . il by PBOOLE:143; A48: (Comput (S2,s2,(0 + 1))) . d1 = (Following (S2,(Comput (S2,s2,0)))) . d1 by EXTPRO_1:3 .= (Following (S2,s2)) . d1 .= e by A42, A44, A46, A47, SCMRING2:11 ; A49: S1 /. il = S1 . il by PBOOLE:143; (Comput (S1,s1,(0 + 1))) . d1 = (Following (S1,(Comput (S1,s1,0)))) . d1 by EXTPRO_1:3 .= (Following (S1,s1)) . d1 .= 0. R by A16, A25, A22, A49, SCMRING2:11 ; then ((Comput (P,s1,1)) | (dom p)) . d1 = 0. R by A27, A3, A4, FUNCT_1:47; hence (Comput (P,s1,1)) | (dom p) <> (Comput (Q,s2,1)) | (dom p) by A28, A3, A32, A4, A48, FUNCT_1:47; ::_thesis: verum end; hence contradiction ; ::_thesis: verum end; hence SCM R is IC-recognized by AMISTD_5:3; ::_thesis: verum end; end; registration let R be non trivial Ring; cluster SCM R -> CurIns-recognized ; coherence SCM R is CurIns-recognized proof let q be NAT -defined the InstructionsF of (SCM R) -valued finite non halt-free Function; :: according to AMISTD_5:def_4 ::_thesis: for b1 being set for b2 being set holds ( not b1 c= b2 or for b3 being set holds ( not q c= b3 or for b4 being Element of NAT holds IC (Comput (b3,b2,b4)) in dom q ) ) let p be non empty q -autonomic FinPartState of (SCM R); ::_thesis: for b1 being set holds ( not p c= b1 or for b2 being set holds ( not q c= b2 or for b3 being Element of NAT holds IC (Comput (b2,b1,b3)) in dom q ) ) let s be State of (SCM R); ::_thesis: ( not p c= s or for b1 being set holds ( not q c= b1 or for b2 being Element of NAT holds IC (Comput (b1,s,b2)) in dom q ) ) assume A1: p c= s ; ::_thesis: for b1 being set holds ( not q c= b1 or for b2 being Element of NAT holds IC (Comput (b1,s,b2)) in dom q ) let P be Instruction-Sequence of (SCM R); ::_thesis: ( not q c= P or for b1 being Element of NAT holds IC (Comput (P,s,b1)) in dom q ) assume A2: q c= P ; ::_thesis: for b1 being Element of NAT holds IC (Comput (P,s,b1)) in dom q let i be Element of NAT ; ::_thesis: IC (Comput (P,s,i)) in dom q set Csi = Comput (P,s,i); set loc = IC (Comput (P,s,i)); set loc1 = (IC (Comput (P,s,i))) + 1; assume A3: not IC (Comput (P,s,i)) in dom q ; ::_thesis: contradiction set I = (dl. (R,0)) := (dl. (R,0)); set q1 = q +* ((IC (Comput (P,s,i))) .--> ((dl. (R,0)) := (dl. (R,0)))); set q2 = q +* ((IC (Comput (P,s,i))) .--> (halt (SCM R))); reconsider P1 = P +* ((IC (Comput (P,s,i))) .--> ((dl. (R,0)) := (dl. (R,0)))) as Instruction-Sequence of (SCM R) ; reconsider P2 = P +* ((IC (Comput (P,s,i))) .--> (halt (SCM R))) as Instruction-Sequence of (SCM R) ; A4: dom ((IC (Comput (P,s,i))) .--> (halt (SCM R))) = {(IC (Comput (P,s,i)))} by FUNCOP_1:13; then A5: IC (Comput (P,s,i)) in dom ((IC (Comput (P,s,i))) .--> (halt (SCM R))) by TARSKI:def_1; A6: dom ((IC (Comput (P,s,i))) .--> ((dl. (R,0)) := (dl. (R,0)))) = {(IC (Comput (P,s,i)))} by FUNCOP_1:13; then A7: IC (Comput (P,s,i)) in dom ((IC (Comput (P,s,i))) .--> ((dl. (R,0)) := (dl. (R,0)))) by TARSKI:def_1; A8: dom q misses dom ((IC (Comput (P,s,i))) .--> (halt (SCM R))) by A3, A4, ZFMISC_1:50; A9: dom q misses dom ((IC (Comput (P,s,i))) .--> ((dl. (R,0)) := (dl. (R,0)))) by A3, A6, ZFMISC_1:50; A10: q +* ((IC (Comput (P,s,i))) .--> ((dl. (R,0)) := (dl. (R,0)))) c= P1 by A2, FUNCT_4:123; A11: q +* ((IC (Comput (P,s,i))) .--> (halt (SCM R))) c= P2 by A2, FUNCT_4:123; set Cs2i = Comput (P2,s,i); set Cs1i = Comput (P1,s,i); not p is q -autonomic proof ((IC (Comput (P,s,i))) .--> (halt (SCM R))) . (IC (Comput (P,s,i))) = halt (SCM R) by FUNCOP_1:72; then A12: P2 . (IC (Comput (P,s,i))) = halt (SCM R) by A5, FUNCT_4:13; A13: ((IC (Comput (P,s,i))) .--> ((dl. (R,0)) := (dl. (R,0)))) . (IC (Comput (P,s,i))) = (dl. (R,0)) := (dl. (R,0)) by FUNCOP_1:72; take P1 ; :: according to EXTPRO_1:def_10 ::_thesis: ex b1 being set st ( q c= P1 & q c= b1 & ex b2, b3 being set st ( p c= b2 & p c= b3 & not for b4 being Element of NAT holds (Comput (P1,b2,b4)) | (dom p) = (Comput (b1,b3,b4)) | (dom p) ) ) take P2 ; ::_thesis: ( q c= P1 & q c= P2 & ex b1, b2 being set st ( p c= b1 & p c= b2 & not for b3 being Element of NAT holds (Comput (P1,b1,b3)) | (dom p) = (Comput (P2,b2,b3)) | (dom p) ) ) q c= q +* ((IC (Comput (P,s,i))) .--> ((dl. (R,0)) := (dl. (R,0)))) by A9, FUNCT_4:32; hence A14: q c= P1 by A10, XBOOLE_1:1; ::_thesis: ( q c= P2 & ex b1, b2 being set st ( p c= b1 & p c= b2 & not for b3 being Element of NAT holds (Comput (P1,b1,b3)) | (dom p) = (Comput (P2,b2,b3)) | (dom p) ) ) q c= q +* ((IC (Comput (P,s,i))) .--> (halt (SCM R))) by A8, FUNCT_4:32; hence A15: q c= P2 by A11, XBOOLE_1:1; ::_thesis: ex b1, b2 being set st ( p c= b1 & p c= b2 & not for b3 being Element of NAT holds (Comput (P1,b1,b3)) | (dom p) = (Comput (P2,b2,b3)) | (dom p) ) take s ; ::_thesis: ex b1 being set st ( p c= s & p c= b1 & not for b2 being Element of NAT holds (Comput (P1,s,b2)) | (dom p) = (Comput (P2,b1,b2)) | (dom p) ) take s ; ::_thesis: ( p c= s & p c= s & not for b1 being Element of NAT holds (Comput (P1,s,b1)) | (dom p) = (Comput (P2,s,b1)) | (dom p) ) thus p c= s by A1; ::_thesis: ( p c= s & not for b1 being Element of NAT holds (Comput (P1,s,b1)) | (dom p) = (Comput (P2,s,b1)) | (dom p) ) A16: (Comput (P1,s,i)) | (dom p) = (Comput (P,s,i)) | (dom p) by A14, A2, A1, EXTPRO_1:def_10; thus p c= s by A1; ::_thesis: not for b1 being Element of NAT holds (Comput (P1,s,b1)) | (dom p) = (Comput (P2,s,b1)) | (dom p) A17: (Comput (P1,s,i)) | (dom p) = (Comput (P2,s,i)) | (dom p) by A14, A15, A1, EXTPRO_1:def_10; take k = i + 1; ::_thesis: not (Comput (P1,s,k)) | (dom p) = (Comput (P2,s,k)) | (dom p) set Cs1k = Comput (P1,s,k); A18: IC in dom p by AMISTD_5:6; IC (Comput (P,s,i)) = IC ((Comput (P,s,i)) | (dom p)) by A18, FUNCT_1:49; then IC (Comput (P1,s,i)) = IC (Comput (P,s,i)) by A16, A18, FUNCT_1:49; then A19: CurInstr (P1,(Comput (P1,s,i))) = P1 . (IC (Comput (P,s,i))) by PBOOLE:143 .= (dl. (R,0)) := (dl. (R,0)) by A13, A7, FUNCT_4:13 ; A20: Comput (P1,s,k) = Following (P1,(Comput (P1,s,i))) by EXTPRO_1:3 .= Exec (((dl. (R,0)) := (dl. (R,0))),(Comput (P1,s,i))) by A19 ; A21: IC (Exec (((dl. (R,0)) := (dl. (R,0))),(Comput (P1,s,i)))) = succ (IC (Comput (P1,s,i))) by SCMRING2:11; A22: IC in dom p by AMISTD_5:6; A23: IC (Comput (P,s,i)) = IC ((Comput (P,s,i)) | (dom p)) by A22, FUNCT_1:49; then A24: IC (Comput (P1,s,k)) = (IC (Comput (P,s,i))) + 1 by A20, A21, A16, A22, FUNCT_1:49; set Cs2k = Comput (P2,s,k); A25: Comput (P2,s,k) = Following (P2,(Comput (P2,s,i))) by EXTPRO_1:3 .= Exec ((CurInstr (P2,(Comput (P2,s,i)))),(Comput (P2,s,i))) ; A26: P2 /. (IC (Comput (P2,s,i))) = P2 . (IC (Comput (P2,s,i))) by PBOOLE:143; IC (Comput (P2,s,i)) = IC (Comput (P,s,i)) by A16, A23, A17, A22, FUNCT_1:49; then A27: IC (Comput (P2,s,k)) = IC (Comput (P,s,i)) by A25, A12, A26, EXTPRO_1:def_3; ( IC ((Comput (P1,s,k)) | (dom p)) = IC (Comput (P1,s,k)) & IC ((Comput (P2,s,k)) | (dom p)) = IC (Comput (P2,s,k)) ) by A22, FUNCT_1:49; hence not (Comput (P1,s,k)) | (dom p) = (Comput (P2,s,k)) | (dom p) by A24, A27; ::_thesis: verum end; hence contradiction ; ::_thesis: verum end; end; theorem Th7: :: SCMRING4:7 for n being Element of NAT for R being non trivial Ring for a, b being Data-Location of R for s1, s2 being State of (SCM R) for P1, P2 being Instruction-Sequence of (SCM R) for q being NAT -defined the InstructionsF of (SCM b2) -valued finite non halt-free Function for p being non empty b9 -autonomic FinPartState of (SCM R) st p c= s1 & p c= s2 & q c= P1 & q c= P2 & CurInstr (P1,(Comput (P1,s1,n))) = a := b & a in dom p holds (Comput (P1,s1,n)) . b = (Comput (P2,s2,n)) . b proof let n be Element of NAT ; ::_thesis: for R being non trivial Ring for a, b being Data-Location of R for s1, s2 being State of (SCM R) for P1, P2 being Instruction-Sequence of (SCM R) for q being NAT -defined the InstructionsF of (SCM b1) -valued finite non halt-free Function for p being non empty b8 -autonomic FinPartState of (SCM R) st p c= s1 & p c= s2 & q c= P1 & q c= P2 & CurInstr (P1,(Comput (P1,s1,n))) = a := b & a in dom p holds (Comput (P1,s1,n)) . b = (Comput (P2,s2,n)) . b let R be non trivial Ring; ::_thesis: for a, b being Data-Location of R for s1, s2 being State of (SCM R) for P1, P2 being Instruction-Sequence of (SCM R) for q being NAT -defined the InstructionsF of (SCM R) -valued finite non halt-free Function for p being non empty b7 -autonomic FinPartState of (SCM R) st p c= s1 & p c= s2 & q c= P1 & q c= P2 & CurInstr (P1,(Comput (P1,s1,n))) = a := b & a in dom p holds (Comput (P1,s1,n)) . b = (Comput (P2,s2,n)) . b let a, b be Data-Location of R; ::_thesis: for s1, s2 being State of (SCM R) for P1, P2 being Instruction-Sequence of (SCM R) for q being NAT -defined the InstructionsF of (SCM R) -valued finite non halt-free Function for p being non empty b5 -autonomic FinPartState of (SCM R) st p c= s1 & p c= s2 & q c= P1 & q c= P2 & CurInstr (P1,(Comput (P1,s1,n))) = a := b & a in dom p holds (Comput (P1,s1,n)) . b = (Comput (P2,s2,n)) . b let s1, s2 be State of (SCM R); ::_thesis: for P1, P2 being Instruction-Sequence of (SCM R) for q being NAT -defined the InstructionsF of (SCM R) -valued finite non halt-free Function for p being non empty b3 -autonomic FinPartState of (SCM R) st p c= s1 & p c= s2 & q c= P1 & q c= P2 & CurInstr (P1,(Comput (P1,s1,n))) = a := b & a in dom p holds (Comput (P1,s1,n)) . b = (Comput (P2,s2,n)) . b let P1, P2 be Instruction-Sequence of (SCM R); ::_thesis: for q being NAT -defined the InstructionsF of (SCM R) -valued finite non halt-free Function for p being non empty b1 -autonomic FinPartState of (SCM R) st p c= s1 & p c= s2 & q c= P1 & q c= P2 & CurInstr (P1,(Comput (P1,s1,n))) = a := b & a in dom p holds (Comput (P1,s1,n)) . b = (Comput (P2,s2,n)) . b set Cs2i1 = Comput (P2,s2,(n + 1)); set Cs1i1 = Comput (P1,s1,(n + 1)); set Cs2i = Comput (P2,s2,n); set Cs1i = Comput (P1,s1,n); set I = CurInstr (P1,(Comput (P1,s1,n))); let q be NAT -defined the InstructionsF of (SCM R) -valued finite non halt-free Function; ::_thesis: for p being non empty q -autonomic FinPartState of (SCM R) st p c= s1 & p c= s2 & q c= P1 & q c= P2 & CurInstr (P1,(Comput (P1,s1,n))) = a := b & a in dom p holds (Comput (P1,s1,n)) . b = (Comput (P2,s2,n)) . b let p be non empty q -autonomic FinPartState of (SCM R); ::_thesis: ( p c= s1 & p c= s2 & q c= P1 & q c= P2 & CurInstr (P1,(Comput (P1,s1,n))) = a := b & a in dom p implies (Comput (P1,s1,n)) . b = (Comput (P2,s2,n)) . b ) assume that A1: ( p c= s1 & p c= s2 ) and A2: ( q c= P1 & q c= P2 ) ; ::_thesis: ( not CurInstr (P1,(Comput (P1,s1,n))) = a := b or not a in dom p or (Comput (P1,s1,n)) . b = (Comput (P2,s2,n)) . b ) A3: ( a in dom p implies ( ((Comput (P1,s1,(n + 1))) | (dom p)) . a = (Comput (P1,s1,(n + 1))) . a & ((Comput (P2,s2,(n + 1))) | (dom p)) . a = (Comput (P2,s2,(n + 1))) . a ) ) by FUNCT_1:49; A4: Comput (P2,s2,(n + 1)) = Following (P2,(Comput (P2,s2,n))) by EXTPRO_1:3 .= Exec ((CurInstr (P2,(Comput (P2,s2,n)))),(Comput (P2,s2,n))) ; assume that A5: CurInstr (P1,(Comput (P1,s1,n))) = a := b and A6: ( a in dom p & (Comput (P1,s1,n)) . b <> (Comput (P2,s2,n)) . b ) ; ::_thesis: contradiction Comput (P1,s1,(n + 1)) = Following (P1,(Comput (P1,s1,n))) by EXTPRO_1:3 .= Exec ((CurInstr (P1,(Comput (P1,s1,n)))),(Comput (P1,s1,n))) ; then A7: (Comput (P1,s1,(n + 1))) . a = (Comput (P1,s1,n)) . b by A5, SCMRING2:11; CurInstr (P1,(Comput (P1,s1,n))) = CurInstr (P2,(Comput (P2,s2,n))) by A1, A2, AMISTD_5:7; then (Comput (P2,s2,(n + 1))) . a = (Comput (P2,s2,n)) . b by A4, A5, SCMRING2:11; hence contradiction by A1, A3, A6, A7, A2, EXTPRO_1:def_10; ::_thesis: verum end; theorem Th8: :: SCMRING4:8 for n being Element of NAT for R being non trivial Ring for a, b being Data-Location of R for s1, s2 being State of (SCM R) for P1, P2 being Instruction-Sequence of (SCM R) for q being NAT -defined the InstructionsF of (SCM b2) -valued finite non halt-free Function for p being non empty b9 -autonomic FinPartState of (SCM R) st p c= s1 & p c= s2 & q c= P1 & q c= P2 & CurInstr (P1,(Comput (P1,s1,n))) = AddTo (a,b) & a in dom p holds ((Comput (P1,s1,n)) . a) + ((Comput (P1,s1,n)) . b) = ((Comput (P2,s2,n)) . a) + ((Comput (P2,s2,n)) . b) proof let n be Element of NAT ; ::_thesis: for R being non trivial Ring for a, b being Data-Location of R for s1, s2 being State of (SCM R) for P1, P2 being Instruction-Sequence of (SCM R) for q being NAT -defined the InstructionsF of (SCM b1) -valued finite non halt-free Function for p being non empty b8 -autonomic FinPartState of (SCM R) st p c= s1 & p c= s2 & q c= P1 & q c= P2 & CurInstr (P1,(Comput (P1,s1,n))) = AddTo (a,b) & a in dom p holds ((Comput (P1,s1,n)) . a) + ((Comput (P1,s1,n)) . b) = ((Comput (P2,s2,n)) . a) + ((Comput (P2,s2,n)) . b) let R be non trivial Ring; ::_thesis: for a, b being Data-Location of R for s1, s2 being State of (SCM R) for P1, P2 being Instruction-Sequence of (SCM R) for q being NAT -defined the InstructionsF of (SCM R) -valued finite non halt-free Function for p being non empty b7 -autonomic FinPartState of (SCM R) st p c= s1 & p c= s2 & q c= P1 & q c= P2 & CurInstr (P1,(Comput (P1,s1,n))) = AddTo (a,b) & a in dom p holds ((Comput (P1,s1,n)) . a) + ((Comput (P1,s1,n)) . b) = ((Comput (P2,s2,n)) . a) + ((Comput (P2,s2,n)) . b) let a, b be Data-Location of R; ::_thesis: for s1, s2 being State of (SCM R) for P1, P2 being Instruction-Sequence of (SCM R) for q being NAT -defined the InstructionsF of (SCM R) -valued finite non halt-free Function for p being non empty b5 -autonomic FinPartState of (SCM R) st p c= s1 & p c= s2 & q c= P1 & q c= P2 & CurInstr (P1,(Comput (P1,s1,n))) = AddTo (a,b) & a in dom p holds ((Comput (P1,s1,n)) . a) + ((Comput (P1,s1,n)) . b) = ((Comput (P2,s2,n)) . a) + ((Comput (P2,s2,n)) . b) let s1, s2 be State of (SCM R); ::_thesis: for P1, P2 being Instruction-Sequence of (SCM R) for q being NAT -defined the InstructionsF of (SCM R) -valued finite non halt-free Function for p being non empty b3 -autonomic FinPartState of (SCM R) st p c= s1 & p c= s2 & q c= P1 & q c= P2 & CurInstr (P1,(Comput (P1,s1,n))) = AddTo (a,b) & a in dom p holds ((Comput (P1,s1,n)) . a) + ((Comput (P1,s1,n)) . b) = ((Comput (P2,s2,n)) . a) + ((Comput (P2,s2,n)) . b) let P1, P2 be Instruction-Sequence of (SCM R); ::_thesis: for q being NAT -defined the InstructionsF of (SCM R) -valued finite non halt-free Function for p being non empty b1 -autonomic FinPartState of (SCM R) st p c= s1 & p c= s2 & q c= P1 & q c= P2 & CurInstr (P1,(Comput (P1,s1,n))) = AddTo (a,b) & a in dom p holds ((Comput (P1,s1,n)) . a) + ((Comput (P1,s1,n)) . b) = ((Comput (P2,s2,n)) . a) + ((Comput (P2,s2,n)) . b) set Cs2i1 = Comput (P2,s2,(n + 1)); set Cs1i1 = Comput (P1,s1,(n + 1)); set Cs2i = Comput (P2,s2,n); set Cs1i = Comput (P1,s1,n); set I = CurInstr (P1,(Comput (P1,s1,n))); let q be NAT -defined the InstructionsF of (SCM R) -valued finite non halt-free Function; ::_thesis: for p being non empty q -autonomic FinPartState of (SCM R) st p c= s1 & p c= s2 & q c= P1 & q c= P2 & CurInstr (P1,(Comput (P1,s1,n))) = AddTo (a,b) & a in dom p holds ((Comput (P1,s1,n)) . a) + ((Comput (P1,s1,n)) . b) = ((Comput (P2,s2,n)) . a) + ((Comput (P2,s2,n)) . b) let p be non empty q -autonomic FinPartState of (SCM R); ::_thesis: ( p c= s1 & p c= s2 & q c= P1 & q c= P2 & CurInstr (P1,(Comput (P1,s1,n))) = AddTo (a,b) & a in dom p implies ((Comput (P1,s1,n)) . a) + ((Comput (P1,s1,n)) . b) = ((Comput (P2,s2,n)) . a) + ((Comput (P2,s2,n)) . b) ) assume that A1: ( p c= s1 & p c= s2 ) and A2: ( q c= P1 & q c= P2 ) ; ::_thesis: ( not CurInstr (P1,(Comput (P1,s1,n))) = AddTo (a,b) or not a in dom p or ((Comput (P1,s1,n)) . a) + ((Comput (P1,s1,n)) . b) = ((Comput (P2,s2,n)) . a) + ((Comput (P2,s2,n)) . b) ) A3: ( a in dom p implies ( ((Comput (P1,s1,(n + 1))) | (dom p)) . a = (Comput (P1,s1,(n + 1))) . a & ((Comput (P2,s2,(n + 1))) | (dom p)) . a = (Comput (P2,s2,(n + 1))) . a ) ) by FUNCT_1:49; A4: Comput (P2,s2,(n + 1)) = Following (P2,(Comput (P2,s2,n))) by EXTPRO_1:3 .= Exec ((CurInstr (P2,(Comput (P2,s2,n)))),(Comput (P2,s2,n))) ; assume that A5: CurInstr (P1,(Comput (P1,s1,n))) = AddTo (a,b) and A6: ( a in dom p & ((Comput (P1,s1,n)) . a) + ((Comput (P1,s1,n)) . b) <> ((Comput (P2,s2,n)) . a) + ((Comput (P2,s2,n)) . b) ) ; ::_thesis: contradiction Comput (P1,s1,(n + 1)) = Following (P1,(Comput (P1,s1,n))) by EXTPRO_1:3 .= Exec ((CurInstr (P1,(Comput (P1,s1,n)))),(Comput (P1,s1,n))) ; then A7: (Comput (P1,s1,(n + 1))) . a = ((Comput (P1,s1,n)) . a) + ((Comput (P1,s1,n)) . b) by A5, SCMRING2:12; CurInstr (P1,(Comput (P1,s1,n))) = CurInstr (P2,(Comput (P2,s2,n))) by A1, A2, AMISTD_5:7; then (Comput (P2,s2,(n + 1))) . a = ((Comput (P2,s2,n)) . a) + ((Comput (P2,s2,n)) . b) by A4, A5, SCMRING2:12; hence contradiction by A1, A3, A6, A7, A2, EXTPRO_1:def_10; ::_thesis: verum end; theorem Th9: :: SCMRING4:9 for n being Element of NAT for R being non trivial Ring for a, b being Data-Location of R for s1, s2 being State of (SCM R) for P1, P2 being Instruction-Sequence of (SCM R) for q being NAT -defined the InstructionsF of (SCM b2) -valued finite non halt-free Function for p being non empty b9 -autonomic FinPartState of (SCM R) st p c= s1 & p c= s2 & q c= P1 & q c= P2 & CurInstr (P1,(Comput (P1,s1,n))) = SubFrom (a,b) & a in dom p holds ((Comput (P1,s1,n)) . a) - ((Comput (P1,s1,n)) . b) = ((Comput (P2,s2,n)) . a) - ((Comput (P2,s2,n)) . b) proof let n be Element of NAT ; ::_thesis: for R being non trivial Ring for a, b being Data-Location of R for s1, s2 being State of (SCM R) for P1, P2 being Instruction-Sequence of (SCM R) for q being NAT -defined the InstructionsF of (SCM b1) -valued finite non halt-free Function for p being non empty b8 -autonomic FinPartState of (SCM R) st p c= s1 & p c= s2 & q c= P1 & q c= P2 & CurInstr (P1,(Comput (P1,s1,n))) = SubFrom (a,b) & a in dom p holds ((Comput (P1,s1,n)) . a) - ((Comput (P1,s1,n)) . b) = ((Comput (P2,s2,n)) . a) - ((Comput (P2,s2,n)) . b) let R be non trivial Ring; ::_thesis: for a, b being Data-Location of R for s1, s2 being State of (SCM R) for P1, P2 being Instruction-Sequence of (SCM R) for q being NAT -defined the InstructionsF of (SCM R) -valued finite non halt-free Function for p being non empty b7 -autonomic FinPartState of (SCM R) st p c= s1 & p c= s2 & q c= P1 & q c= P2 & CurInstr (P1,(Comput (P1,s1,n))) = SubFrom (a,b) & a in dom p holds ((Comput (P1,s1,n)) . a) - ((Comput (P1,s1,n)) . b) = ((Comput (P2,s2,n)) . a) - ((Comput (P2,s2,n)) . b) let a, b be Data-Location of R; ::_thesis: for s1, s2 being State of (SCM R) for P1, P2 being Instruction-Sequence of (SCM R) for q being NAT -defined the InstructionsF of (SCM R) -valued finite non halt-free Function for p being non empty b5 -autonomic FinPartState of (SCM R) st p c= s1 & p c= s2 & q c= P1 & q c= P2 & CurInstr (P1,(Comput (P1,s1,n))) = SubFrom (a,b) & a in dom p holds ((Comput (P1,s1,n)) . a) - ((Comput (P1,s1,n)) . b) = ((Comput (P2,s2,n)) . a) - ((Comput (P2,s2,n)) . b) let s1, s2 be State of (SCM R); ::_thesis: for P1, P2 being Instruction-Sequence of (SCM R) for q being NAT -defined the InstructionsF of (SCM R) -valued finite non halt-free Function for p being non empty b3 -autonomic FinPartState of (SCM R) st p c= s1 & p c= s2 & q c= P1 & q c= P2 & CurInstr (P1,(Comput (P1,s1,n))) = SubFrom (a,b) & a in dom p holds ((Comput (P1,s1,n)) . a) - ((Comput (P1,s1,n)) . b) = ((Comput (P2,s2,n)) . a) - ((Comput (P2,s2,n)) . b) let P1, P2 be Instruction-Sequence of (SCM R); ::_thesis: for q being NAT -defined the InstructionsF of (SCM R) -valued finite non halt-free Function for p being non empty b1 -autonomic FinPartState of (SCM R) st p c= s1 & p c= s2 & q c= P1 & q c= P2 & CurInstr (P1,(Comput (P1,s1,n))) = SubFrom (a,b) & a in dom p holds ((Comput (P1,s1,n)) . a) - ((Comput (P1,s1,n)) . b) = ((Comput (P2,s2,n)) . a) - ((Comput (P2,s2,n)) . b) set Cs2i1 = Comput (P2,s2,(n + 1)); set Cs1i1 = Comput (P1,s1,(n + 1)); set Cs2i = Comput (P2,s2,n); set Cs1i = Comput (P1,s1,n); set I = CurInstr (P1,(Comput (P1,s1,n))); let q be NAT -defined the InstructionsF of (SCM R) -valued finite non halt-free Function; ::_thesis: for p being non empty q -autonomic FinPartState of (SCM R) st p c= s1 & p c= s2 & q c= P1 & q c= P2 & CurInstr (P1,(Comput (P1,s1,n))) = SubFrom (a,b) & a in dom p holds ((Comput (P1,s1,n)) . a) - ((Comput (P1,s1,n)) . b) = ((Comput (P2,s2,n)) . a) - ((Comput (P2,s2,n)) . b) let p be non empty q -autonomic FinPartState of (SCM R); ::_thesis: ( p c= s1 & p c= s2 & q c= P1 & q c= P2 & CurInstr (P1,(Comput (P1,s1,n))) = SubFrom (a,b) & a in dom p implies ((Comput (P1,s1,n)) . a) - ((Comput (P1,s1,n)) . b) = ((Comput (P2,s2,n)) . a) - ((Comput (P2,s2,n)) . b) ) assume that A1: ( p c= s1 & p c= s2 ) and A2: ( q c= P1 & q c= P2 ) ; ::_thesis: ( not CurInstr (P1,(Comput (P1,s1,n))) = SubFrom (a,b) or not a in dom p or ((Comput (P1,s1,n)) . a) - ((Comput (P1,s1,n)) . b) = ((Comput (P2,s2,n)) . a) - ((Comput (P2,s2,n)) . b) ) A3: ( a in dom p implies ( ((Comput (P1,s1,(n + 1))) | (dom p)) . a = (Comput (P1,s1,(n + 1))) . a & ((Comput (P2,s2,(n + 1))) | (dom p)) . a = (Comput (P2,s2,(n + 1))) . a ) ) by FUNCT_1:49; A4: Comput (P2,s2,(n + 1)) = Following (P2,(Comput (P2,s2,n))) by EXTPRO_1:3 .= Exec ((CurInstr (P2,(Comput (P2,s2,n)))),(Comput (P2,s2,n))) ; assume that A5: CurInstr (P1,(Comput (P1,s1,n))) = SubFrom (a,b) and A6: ( a in dom p & ((Comput (P1,s1,n)) . a) - ((Comput (P1,s1,n)) . b) <> ((Comput (P2,s2,n)) . a) - ((Comput (P2,s2,n)) . b) ) ; ::_thesis: contradiction Comput (P1,s1,(n + 1)) = Following (P1,(Comput (P1,s1,n))) by EXTPRO_1:3 .= Exec ((CurInstr (P1,(Comput (P1,s1,n)))),(Comput (P1,s1,n))) ; then A7: (Comput (P1,s1,(n + 1))) . a = ((Comput (P1,s1,n)) . a) - ((Comput (P1,s1,n)) . b) by A5, SCMRING2:13; CurInstr (P1,(Comput (P1,s1,n))) = CurInstr (P2,(Comput (P2,s2,n))) by A1, A2, AMISTD_5:7; then (Comput (P2,s2,(n + 1))) . a = ((Comput (P2,s2,n)) . a) - ((Comput (P2,s2,n)) . b) by A4, A5, SCMRING2:13; hence contradiction by A1, A3, A6, A7, A2, EXTPRO_1:def_10; ::_thesis: verum end; theorem Th10: :: SCMRING4:10 for n being Element of NAT for R being non trivial Ring for a, b being Data-Location of R for s1, s2 being State of (SCM R) for P1, P2 being Instruction-Sequence of (SCM R) for q being NAT -defined the InstructionsF of (SCM b2) -valued finite non halt-free Function for p being non empty b9 -autonomic FinPartState of (SCM R) st p c= s1 & p c= s2 & q c= P1 & q c= P2 & CurInstr (P1,(Comput (P1,s1,n))) = MultBy (a,b) & a in dom p holds ((Comput (P1,s1,n)) . a) * ((Comput (P1,s1,n)) . b) = ((Comput (P2,s2,n)) . a) * ((Comput (P2,s2,n)) . b) proof let n be Element of NAT ; ::_thesis: for R being non trivial Ring for a, b being Data-Location of R for s1, s2 being State of (SCM R) for P1, P2 being Instruction-Sequence of (SCM R) for q being NAT -defined the InstructionsF of (SCM b1) -valued finite non halt-free Function for p being non empty b8 -autonomic FinPartState of (SCM R) st p c= s1 & p c= s2 & q c= P1 & q c= P2 & CurInstr (P1,(Comput (P1,s1,n))) = MultBy (a,b) & a in dom p holds ((Comput (P1,s1,n)) . a) * ((Comput (P1,s1,n)) . b) = ((Comput (P2,s2,n)) . a) * ((Comput (P2,s2,n)) . b) let R be non trivial Ring; ::_thesis: for a, b being Data-Location of R for s1, s2 being State of (SCM R) for P1, P2 being Instruction-Sequence of (SCM R) for q being NAT -defined the InstructionsF of (SCM R) -valued finite non halt-free Function for p being non empty b7 -autonomic FinPartState of (SCM R) st p c= s1 & p c= s2 & q c= P1 & q c= P2 & CurInstr (P1,(Comput (P1,s1,n))) = MultBy (a,b) & a in dom p holds ((Comput (P1,s1,n)) . a) * ((Comput (P1,s1,n)) . b) = ((Comput (P2,s2,n)) . a) * ((Comput (P2,s2,n)) . b) let a, b be Data-Location of R; ::_thesis: for s1, s2 being State of (SCM R) for P1, P2 being Instruction-Sequence of (SCM R) for q being NAT -defined the InstructionsF of (SCM R) -valued finite non halt-free Function for p being non empty b5 -autonomic FinPartState of (SCM R) st p c= s1 & p c= s2 & q c= P1 & q c= P2 & CurInstr (P1,(Comput (P1,s1,n))) = MultBy (a,b) & a in dom p holds ((Comput (P1,s1,n)) . a) * ((Comput (P1,s1,n)) . b) = ((Comput (P2,s2,n)) . a) * ((Comput (P2,s2,n)) . b) let s1, s2 be State of (SCM R); ::_thesis: for P1, P2 being Instruction-Sequence of (SCM R) for q being NAT -defined the InstructionsF of (SCM R) -valued finite non halt-free Function for p being non empty b3 -autonomic FinPartState of (SCM R) st p c= s1 & p c= s2 & q c= P1 & q c= P2 & CurInstr (P1,(Comput (P1,s1,n))) = MultBy (a,b) & a in dom p holds ((Comput (P1,s1,n)) . a) * ((Comput (P1,s1,n)) . b) = ((Comput (P2,s2,n)) . a) * ((Comput (P2,s2,n)) . b) let P1, P2 be Instruction-Sequence of (SCM R); ::_thesis: for q being NAT -defined the InstructionsF of (SCM R) -valued finite non halt-free Function for p being non empty b1 -autonomic FinPartState of (SCM R) st p c= s1 & p c= s2 & q c= P1 & q c= P2 & CurInstr (P1,(Comput (P1,s1,n))) = MultBy (a,b) & a in dom p holds ((Comput (P1,s1,n)) . a) * ((Comput (P1,s1,n)) . b) = ((Comput (P2,s2,n)) . a) * ((Comput (P2,s2,n)) . b) set Cs2i1 = Comput (P2,s2,(n + 1)); set Cs1i1 = Comput (P1,s1,(n + 1)); set Cs2i = Comput (P2,s2,n); set Cs1i = Comput (P1,s1,n); set I = CurInstr (P1,(Comput (P1,s1,n))); let q be NAT -defined the InstructionsF of (SCM R) -valued finite non halt-free Function; ::_thesis: for p being non empty q -autonomic FinPartState of (SCM R) st p c= s1 & p c= s2 & q c= P1 & q c= P2 & CurInstr (P1,(Comput (P1,s1,n))) = MultBy (a,b) & a in dom p holds ((Comput (P1,s1,n)) . a) * ((Comput (P1,s1,n)) . b) = ((Comput (P2,s2,n)) . a) * ((Comput (P2,s2,n)) . b) let p be non empty q -autonomic FinPartState of (SCM R); ::_thesis: ( p c= s1 & p c= s2 & q c= P1 & q c= P2 & CurInstr (P1,(Comput (P1,s1,n))) = MultBy (a,b) & a in dom p implies ((Comput (P1,s1,n)) . a) * ((Comput (P1,s1,n)) . b) = ((Comput (P2,s2,n)) . a) * ((Comput (P2,s2,n)) . b) ) assume that A1: ( p c= s1 & p c= s2 ) and A2: ( q c= P1 & q c= P2 ) ; ::_thesis: ( not CurInstr (P1,(Comput (P1,s1,n))) = MultBy (a,b) or not a in dom p or ((Comput (P1,s1,n)) . a) * ((Comput (P1,s1,n)) . b) = ((Comput (P2,s2,n)) . a) * ((Comput (P2,s2,n)) . b) ) A3: ( a in dom p implies ( ((Comput (P1,s1,(n + 1))) | (dom p)) . a = (Comput (P1,s1,(n + 1))) . a & ((Comput (P2,s2,(n + 1))) | (dom p)) . a = (Comput (P2,s2,(n + 1))) . a ) ) by FUNCT_1:49; A4: Comput (P2,s2,(n + 1)) = Following (P2,(Comput (P2,s2,n))) by EXTPRO_1:3 .= Exec ((CurInstr (P2,(Comput (P2,s2,n)))),(Comput (P2,s2,n))) ; assume that A5: CurInstr (P1,(Comput (P1,s1,n))) = MultBy (a,b) and A6: ( a in dom p & ((Comput (P1,s1,n)) . a) * ((Comput (P1,s1,n)) . b) <> ((Comput (P2,s2,n)) . a) * ((Comput (P2,s2,n)) . b) ) ; ::_thesis: contradiction Comput (P1,s1,(n + 1)) = Following (P1,(Comput (P1,s1,n))) by EXTPRO_1:3 .= Exec ((CurInstr (P1,(Comput (P1,s1,n)))),(Comput (P1,s1,n))) ; then A7: (Comput (P1,s1,(n + 1))) . a = ((Comput (P1,s1,n)) . a) * ((Comput (P1,s1,n)) . b) by A5, SCMRING2:14; CurInstr (P1,(Comput (P1,s1,n))) = CurInstr (P2,(Comput (P2,s2,n))) by A1, A2, AMISTD_5:7; then (Comput (P2,s2,(n + 1))) . a = ((Comput (P2,s2,n)) . a) * ((Comput (P2,s2,n)) . b) by A4, A5, SCMRING2:14; hence contradiction by A1, A3, A6, A7, A2, EXTPRO_1:def_10; ::_thesis: verum end; theorem Th11: :: SCMRING4:11 for n being Element of NAT for R being non trivial Ring for a being Data-Location of R for loc being Element of NAT for s1, s2 being State of (SCM R) for P1, P2 being Instruction-Sequence of (SCM R) for q being NAT -defined the InstructionsF of (SCM b2) -valued finite non halt-free Function for p being non empty b9 -autonomic FinPartState of (SCM R) st p c= s1 & p c= s2 & q c= P1 & q c= P2 & CurInstr (P1,(Comput (P1,s1,n))) = a =0_goto loc & loc <> succ (IC (Comput (P1,s1,n))) holds ( (Comput (P1,s1,n)) . a = 0. R iff (Comput (P2,s2,n)) . a = 0. R ) proof let n be Element of NAT ; ::_thesis: for R being non trivial Ring for a being Data-Location of R for loc being Element of NAT for s1, s2 being State of (SCM R) for P1, P2 being Instruction-Sequence of (SCM R) for q being NAT -defined the InstructionsF of (SCM b1) -valued finite non halt-free Function for p being non empty b8 -autonomic FinPartState of (SCM R) st p c= s1 & p c= s2 & q c= P1 & q c= P2 & CurInstr (P1,(Comput (P1,s1,n))) = a =0_goto loc & loc <> succ (IC (Comput (P1,s1,n))) holds ( (Comput (P1,s1,n)) . a = 0. R iff (Comput (P2,s2,n)) . a = 0. R ) let R be non trivial Ring; ::_thesis: for a being Data-Location of R for loc being Element of NAT for s1, s2 being State of (SCM R) for P1, P2 being Instruction-Sequence of (SCM R) for q being NAT -defined the InstructionsF of (SCM R) -valued finite non halt-free Function for p being non empty b7 -autonomic FinPartState of (SCM R) st p c= s1 & p c= s2 & q c= P1 & q c= P2 & CurInstr (P1,(Comput (P1,s1,n))) = a =0_goto loc & loc <> succ (IC (Comput (P1,s1,n))) holds ( (Comput (P1,s1,n)) . a = 0. R iff (Comput (P2,s2,n)) . a = 0. R ) let a be Data-Location of R; ::_thesis: for loc being Element of NAT for s1, s2 being State of (SCM R) for P1, P2 being Instruction-Sequence of (SCM R) for q being NAT -defined the InstructionsF of (SCM R) -valued finite non halt-free Function for p being non empty b6 -autonomic FinPartState of (SCM R) st p c= s1 & p c= s2 & q c= P1 & q c= P2 & CurInstr (P1,(Comput (P1,s1,n))) = a =0_goto loc & loc <> succ (IC (Comput (P1,s1,n))) holds ( (Comput (P1,s1,n)) . a = 0. R iff (Comput (P2,s2,n)) . a = 0. R ) let loc be Element of NAT ; ::_thesis: for s1, s2 being State of (SCM R) for P1, P2 being Instruction-Sequence of (SCM R) for q being NAT -defined the InstructionsF of (SCM R) -valued finite non halt-free Function for p being non empty b5 -autonomic FinPartState of (SCM R) st p c= s1 & p c= s2 & q c= P1 & q c= P2 & CurInstr (P1,(Comput (P1,s1,n))) = a =0_goto loc & loc <> succ (IC (Comput (P1,s1,n))) holds ( (Comput (P1,s1,n)) . a = 0. R iff (Comput (P2,s2,n)) . a = 0. R ) let s1, s2 be State of (SCM R); ::_thesis: for P1, P2 being Instruction-Sequence of (SCM R) for q being NAT -defined the InstructionsF of (SCM R) -valued finite non halt-free Function for p being non empty b3 -autonomic FinPartState of (SCM R) st p c= s1 & p c= s2 & q c= P1 & q c= P2 & CurInstr (P1,(Comput (P1,s1,n))) = a =0_goto loc & loc <> succ (IC (Comput (P1,s1,n))) holds ( (Comput (P1,s1,n)) . a = 0. R iff (Comput (P2,s2,n)) . a = 0. R ) let P1, P2 be Instruction-Sequence of (SCM R); ::_thesis: for q being NAT -defined the InstructionsF of (SCM R) -valued finite non halt-free Function for p being non empty b1 -autonomic FinPartState of (SCM R) st p c= s1 & p c= s2 & q c= P1 & q c= P2 & CurInstr (P1,(Comput (P1,s1,n))) = a =0_goto loc & loc <> succ (IC (Comput (P1,s1,n))) holds ( (Comput (P1,s1,n)) . a = 0. R iff (Comput (P2,s2,n)) . a = 0. R ) set Cs2i1 = Comput (P2,s2,(n + 1)); set Cs1i1 = Comput (P1,s1,(n + 1)); set I = CurInstr (P1,(Comput (P1,s1,n))); let q be NAT -defined the InstructionsF of (SCM R) -valued finite non halt-free Function; ::_thesis: for p being non empty q -autonomic FinPartState of (SCM R) st p c= s1 & p c= s2 & q c= P1 & q c= P2 & CurInstr (P1,(Comput (P1,s1,n))) = a =0_goto loc & loc <> succ (IC (Comput (P1,s1,n))) holds ( (Comput (P1,s1,n)) . a = 0. R iff (Comput (P2,s2,n)) . a = 0. R ) let p be non empty q -autonomic FinPartState of (SCM R); ::_thesis: ( p c= s1 & p c= s2 & q c= P1 & q c= P2 & CurInstr (P1,(Comput (P1,s1,n))) = a =0_goto loc & loc <> succ (IC (Comput (P1,s1,n))) implies ( (Comput (P1,s1,n)) . a = 0. R iff (Comput (P2,s2,n)) . a = 0. R ) ) assume that A1: ( p c= s1 & p c= s2 ) and A2: ( q c= P1 & q c= P2 ) ; ::_thesis: ( not CurInstr (P1,(Comput (P1,s1,n))) = a =0_goto loc or not loc <> succ (IC (Comput (P1,s1,n))) or ( (Comput (P1,s1,n)) . a = 0. R iff (Comput (P2,s2,n)) . a = 0. R ) ) A3: CurInstr (P1,(Comput (P1,s1,n))) = CurInstr (P2,(Comput (P2,s2,n))) by A1, A2, AMISTD_5:7; set Cs2i = Comput (P2,s2,n); set Cs1i = Comput (P1,s1,n); A4: Comput (P1,s1,(n + 1)) = Following (P1,(Comput (P1,s1,n))) by EXTPRO_1:3 .= Exec ((CurInstr (P1,(Comput (P1,s1,n)))),(Comput (P1,s1,n))) ; A5: Comput (P2,s2,(n + 1)) = Following (P2,(Comput (P2,s2,n))) by EXTPRO_1:3 .= Exec ((CurInstr (P2,(Comput (P2,s2,n)))),(Comput (P2,s2,n))) ; IC in dom p by AMISTD_5:6; then A6: ( ((Comput (P1,s1,(n + 1))) | (dom p)) . (IC ) = (Comput (P1,s1,(n + 1))) . (IC ) & ((Comput (P2,s2,(n + 1))) | (dom p)) . (IC ) = (Comput (P2,s2,(n + 1))) . (IC ) ) by FUNCT_1:49; assume that A7: CurInstr (P1,(Comput (P1,s1,n))) = a =0_goto loc and A8: loc <> succ (IC (Comput (P1,s1,n))) ; ::_thesis: ( (Comput (P1,s1,n)) . a = 0. R iff (Comput (P2,s2,n)) . a = 0. R ) A9: IC (Comput (P1,s1,n)) = IC (Comput (P2,s2,n)) by A1, A2, AMISTD_5:7; hereby ::_thesis: ( (Comput (P2,s2,n)) . a = 0. R implies (Comput (P1,s1,n)) . a = 0. R ) assume ( (Comput (P1,s1,n)) . a = 0. R & (Comput (P2,s2,n)) . a <> 0. R ) ; ::_thesis: contradiction then ( (Comput (P1,s1,(n + 1))) . (IC ) = loc & (Comput (P2,s2,(n + 1))) . (IC ) = succ (IC (Comput (P2,s2,n))) ) by A3, A4, A5, A7, SCMRING2:16; hence contradiction by A1, A9, A6, A8, A2, EXTPRO_1:def_10; ::_thesis: verum end; assume that A10: (Comput (P2,s2,n)) . a = 0. R and A11: (Comput (P1,s1,n)) . a <> 0. R ; ::_thesis: contradiction A12: (Comput (P1,s1,(n + 1))) . (IC ) = succ (IC (Comput (P1,s1,n))) by A4, A7, A11, SCMRING2:16; (Comput (P2,s2,(n + 1))) . (IC ) = loc by A3, A5, A7, A10, SCMRING2:16; hence contradiction by A1, A6, A8, A12, A2, EXTPRO_1:def_10; ::_thesis: verum end; begin theorem Th12: :: SCMRING4:12 for k being Element of NAT for R being non trivial Ring for s1, s2 being State of (SCM R) for q being NAT -defined the InstructionsF of (SCM b2) -valued finite non halt-free Function for p being non empty b5 -autonomic FinPartState of (SCM R) st p c= s1 & IncIC (p,k) c= s2 holds for P1, P2 being Instruction-Sequence of (SCM R) 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 R being non trivial Ring for s1, s2 being State of (SCM R) for q being NAT -defined the InstructionsF of (SCM b1) -valued finite non halt-free Function for p being non empty b4 -autonomic FinPartState of (SCM R) st p c= s1 & IncIC (p,k) c= s2 holds for P1, P2 being Instruction-Sequence of (SCM R) 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 R be non trivial Ring; ::_thesis: for s1, s2 being State of (SCM R) for q being NAT -defined the InstructionsF of (SCM R) -valued finite non halt-free Function for p being non empty b3 -autonomic FinPartState of (SCM R) st p c= s1 & IncIC (p,k) c= s2 holds for P1, P2 being Instruction-Sequence of (SCM R) 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 R); ::_thesis: for q being NAT -defined the InstructionsF of (SCM R) -valued finite non halt-free Function for p being non empty b1 -autonomic FinPartState of (SCM R) st p c= s1 & IncIC (p,k) c= s2 holds for P1, P2 being Instruction-Sequence of (SCM R) 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 R) -valued finite non halt-free Function; ::_thesis: for p being non empty q -autonomic FinPartState of (SCM R) st p c= s1 & IncIC (p,k) c= s2 holds for P1, P2 being Instruction-Sequence of (SCM R) 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 R); ::_thesis: ( p c= s1 & IncIC (p,k) c= s2 implies for P1, P2 being Instruction-Sequence of (SCM R) 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 R) 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)) ) A1: IC in dom p by AMISTD_5:6; let P1, P2 be Instruction-Sequence of (SCM R); ::_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 A5: ( 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)) ) set s = 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)) ); A7: IC p = IC s1 by A2, A1, GRFUNC_1:2; then IC p = IC (Comput (P1,s1,0)) ; then A8: IC p in dom q by A2, A5, AMISTD_5:def_4; 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); A15: 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))) ; A16: now__::_thesis:_for_s_being_State_of_(SCM_R) for_d_being_Data-Location_of_R_holds_d_in_dom_(DataPart_s) let s be State of (SCM R); ::_thesis: for d being Data-Location of R holds d in dom (DataPart s) let d be Data-Location of R; ::_thesis: d in dom (DataPart s) d in Data-Locations by SCMRING2:23; hence d in dom (DataPart s) by MEMSTR_0:9; ::_thesis: verum end; A17: now__::_thesis:_for_d_being_Data-Location_of_R_holds_(Comput_(P1,(s1_+*_(DataPart_s2)),i))_._d_=_(Comput_(P2,s2,i))_._d let d be Data-Location of R; ::_thesis: (Comput (P1,(s1 +* (DataPart s2)),i)) . d = (Comput (P2,s2,i)) . d A18: d in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),i))) by A16; 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, A18, 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 R) by PARTFUN1:def_2; then A19: dom (Comput (P1,s1,(i + 1))) = {(IC )} \/ (Data-Locations ) by XBOOLE_1:45; A20: succ ((IC (Comput (P1,s1,i))) + k) = (succ (IC (Comput (P1,s1,i)))) + k ; A21: 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 A22: (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)))) A23: loc in dom q by A2, A5, AMISTD_5:def_4; loc + k in dom (Reloc (q,k)) by A23, COMPOS_1:46; then A24: (Reloc (q,k)) . (loc + k) = P2 . (loc + k) by A5, GRFUNC_1:2; A25: P2 /. (IC (Comput (P2,s2,(i + 1)))) = P2 . (IC (Comput (P2,s2,(i + 1)))) by PBOOLE:143; CurInstr (P1,(Comput (P1,s1,(i + 1)))) = P1 . loc by PBOOLE:143 .= q . loc by A23, A5, GRFUNC_1:2 ; hence IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A22, A23, A24, A25, COMPOS_1:35; ::_thesis: verum end; dom (Comput (P2,s2,i)) = the carrier of (SCM R) by PARTFUN1:def_2; then A26: dom (Comput (P2,s2,i)) = {(IC )} \/ (Data-Locations ) by XBOOLE_1:45; dom (DataPart p) = (dom p) /\ (Data-Locations ) by RELAT_1:61; then A27: dom (DataPart p) c= {(IC )} \/ (Data-Locations ) by XBOOLE_1:10, XBOOLE_1:17; set Cs3i1 = Comput (P1,(s1 +* (DataPart s2)),(i + 1)); A28: dom (DataPart (Comput (P2,s2,i))) = Data-Locations by MEMSTR_0:9; A29: dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) = Data-Locations by MEMSTR_0:9; then A30: dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) c= dom (DataPart (Comput (P2,s2,(i + 1)))) by MEMSTR_0:9; A31: dom (DataPart (Comput (P2,s2,(i + 1)))) = Data-Locations by MEMSTR_0:9; A32: 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 A33: x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) and A34: (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 A33, A34, FUNCT_1:47 .= (DataPart (Comput (P2,s2,(i + 1)))) . x by A29, A31, A33, FUNCT_1:47 ; ::_thesis: verum end; A35: dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),i))) = Data-Locations by MEMSTR_0:9; A36: 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 A37: x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) and A38: ( (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 A35, A29, A37, FUNCT_1:47; hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A14, A28, A29, A32, A37, A38, FUNCT_1:47; ::_thesis: verum end; dom (Comput (P1,s1,i)) = the carrier of (SCM R) by PARTFUN1:def_2; then A39: dom (Comput (P1,s1,i)) = {(IC )} \/ (Data-Locations ) by XBOOLE_1:45; dom (Comput (P2,s2,(i + 1))) = the carrier of (SCM R) by PARTFUN1:def_2; then A40: dom (Comput (P2,s2,(i + 1))) = {(IC )} \/ (Data-Locations ) by XBOOLE_1:45; set I = CurInstr (P1,(Comput (P1,s1,i))); A41: 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))) ; A42: 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, A27, XBOOLE_1:28 ; A43: 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 A19, A27, XBOOLE_1:28 ; A44: dom ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) = (dom (Comput (P2,s2,(i + 1)))) /\ (dom (DataPart p)) by RELAT_1:61 .= dom (DataPart p) by A40, A27, XBOOLE_1:28 ; then A45: dom ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) c= dom ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) by A43; 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 A26, A27, XBOOLE_1:28 ; A47: now__::_thesis:_for_x_being_set_ for_d_being_Data-Location_of_R_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 of R 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 of R; ::_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 A51: ( ((Comput (P1,s1,i)) | (dom (DataPart p))) . d = (Comput (P1,s1,i)) . d & ((Comput (P2,s2,i)) | (dom (DataPart p))) . d = (Comput (P2,s2,i)) . d ) by A42, A46, A49, FUNCT_1:47; thus ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = (Comput (P1,s1,(i + 1))) . d by A43, A48, A49, FUNCT_1:47 .= ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A13, A44, A48, A49, A50, A51, FUNCT_1:47 ; ::_thesis: verum end; A52: now__::_thesis:_for_x_being_set_ for_d_being_Data-Location_of_R_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 of R 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 of R; ::_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 A53: ( d = x & d in dom (DataPart p) ) and A54: (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 A43, A53, A54, FUNCT_1:47 .= ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A44, A53, FUNCT_1:47 ; ::_thesis: verum end; A55: 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, A5, AMISTD_5:7 ; 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 ) by NAT_1:31, SCMRING3:39; suppose InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 0 ; ::_thesis: S1[i + 1] then A56: CurInstr (P1,(Comput (P1,s1,i))) = halt (SCM R) by SCMRING3:12; hence (IC (Comput (P1,s1,(i + 1)))) + k = (IC (Comput (P1,s1,i))) + k by A41, EXTPRO_1:def_3 .= IC (Comput (P2,s2,(i + 1))) by A11, A12, A15, A56, 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 A21; ::_thesis: ( (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) ) A57: Comput (P2,s2,(i + 1)) = Comput (P2,s2,i) by A12, A15, A56, EXTPRO_1:def_3; hence (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A13, A41, A56, 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, A55, A56, A57, 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 of R such that A58: CurInstr (P1,(Comput (P1,s1,i))) = da := db by SCMRING3:13; A59: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = da := db by A58, COMPOS_0:4; A60: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = succ (IC (Comput (P1,s1,i))) by A58, SCMRING2:11; hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A11, A12, A41, A15, A20, A59, SCMRING2:11; ::_thesis: ( IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) & (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) ) thus IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A11, A12, A21, A41, A15, A20, A59, A60, SCMRING2:11; ::_thesis: ( (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) ) A61: (Comput (P1,(s1 +* (DataPart s2)),i)) . db = (Comput (P2,s2,i)) . db by A17; 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 A62: 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 A63: 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 reconsider d = x as Data-Location of R by A43, A63, SCMRING2:23; percases ( da = d or da <> d ) ; supposeA64: 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, A41, A15, A58, A59, SCMRING2:11; hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A2, A9, A43, A52, A58, A61, A63, A62, A64, Th7, A5; ::_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, A41, A15, A58, A59, SCMRING2:11; hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A43, A47, A63; ::_thesis: verum end; end; end; then (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A45, GRFUNC_1:2; hence (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A43, A44, GRFUNC_1:3; ::_thesis: DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) now__::_thesis:_for_x_being_set_st_x_in_dom_(DataPart_(Comput_(P1,(s1_+*_(DataPart_s2)),(i_+_1))))_holds_ (DataPart_(Comput_(P1,(s1_+*_(DataPart_s2)),(i_+_1))))_._x_=_(DataPart_(Comput_(P2,s2,(i_+_1))))_._x let x be set ; ::_thesis: ( x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) implies (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 ) assume A65: 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 of R by A29, SCMRING2:23; 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, A15, A55, A58, A59, SCMRING2:11; hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A17, A32, A65; ::_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, A15, A55, A58, A59, SCMRING2:11; hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A36, A65; ::_thesis: verum end; end; end; then DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1))) by A30, GRFUNC_1:2; hence DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) by A29, A31, 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 of R such that A66: CurInstr (P1,(Comput (P1,s1,i))) = AddTo (da,db) by SCMRING3:14; A67: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = AddTo (da,db) by A66, COMPOS_0:4; A68: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = succ (IC (Comput (P1,s1,i))) by A66, SCMRING2:12; hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A11, A12, A41, A15, A20, A67, SCMRING2:12; ::_thesis: ( IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) & (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) ) thus IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A11, A12, A21, A41, A15, A20, A67, A68, SCMRING2:12; ::_thesis: ( (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) ) A69: ( (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 A17; 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 A70: 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 A71: 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 reconsider d = x as Data-Location of R by A43, A71, SCMRING2:23; percases ( da = d or da <> d ) ; supposeA72: 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, A41, A15, A66, A67, SCMRING2:12; hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A2, A9, A43, A52, A66, A69, A71, A70, A72, Th8, A5; ::_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, A41, A15, A66, A67, SCMRING2:12; hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A43, A47, A71; ::_thesis: verum end; end; end; then (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A45, GRFUNC_1:2; hence (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A43, A44, GRFUNC_1:3; ::_thesis: DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) now__::_thesis:_for_x_being_set_st_x_in_dom_(DataPart_(Comput_(P1,(s1_+*_(DataPart_s2)),(i_+_1))))_holds_ (DataPart_(Comput_(P1,(s1_+*_(DataPart_s2)),(i_+_1))))_._x_=_(DataPart_(Comput_(P2,s2,(i_+_1))))_._x let x be set ; ::_thesis: ( x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) implies (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 ) assume A73: x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) ; ::_thesis: (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 then reconsider d = x as Data-Location of R by A29, SCMRING2:23; 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, A15, A55, A66, A67, SCMRING2:12; hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A32, A69, A73; ::_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, A15, A55, A66, A67, SCMRING2:12; hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A36, A73; ::_thesis: verum end; end; end; then DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1))) by A30, GRFUNC_1:2; hence DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) by A29, A31, 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 of R such that A74: CurInstr (P1,(Comput (P1,s1,i))) = SubFrom (da,db) by SCMRING3:15; A75: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = SubFrom (da,db) by A74, COMPOS_0:4; A76: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = succ (IC (Comput (P1,s1,i))) by A74, SCMRING2:13; hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A11, A12, A41, A15, A20, A75, SCMRING2:13; ::_thesis: ( IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) & (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) ) thus IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) by A11, A12, A21, A41, A15, A20, A75, A76, SCMRING2:13; ::_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))) ) A77: ( (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 A17; 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 A78: 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 A79: 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 reconsider d = x as Data-Location of R by A43, A79, SCMRING2:23; percases ( da = d or da <> d ) ; supposeA80: 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, A41, A15, A74, A75, SCMRING2:13; hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A2, A9, A43, A52, A74, A77, A79, A78, A80, Th9, A5; ::_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, A41, A15, A74, A75, SCMRING2:13; hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A43, A47, A79; ::_thesis: verum end; end; end; then (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A45, GRFUNC_1:2; hence (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A43, A44, GRFUNC_1:3; ::_thesis: DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) now__::_thesis:_for_x_being_set_st_x_in_dom_(DataPart_(Comput_(P1,(s1_+*_(DataPart_s2)),(i_+_1))))_holds_ (DataPart_(Comput_(P1,(s1_+*_(DataPart_s2)),(i_+_1))))_._x_=_(DataPart_(Comput_(P2,s2,(i_+_1))))_._x let x be set ; ::_thesis: ( x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) implies (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 ) assume A81: 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 of R by A29, SCMRING2:23; 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, A15, A55, A74, A75, SCMRING2:13; hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A32, A77, A81; ::_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, A15, A55, A74, A75, SCMRING2:13; hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A36, A81; ::_thesis: verum end; end; end; then DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1))) by A30, GRFUNC_1:2; hence DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) by A29, A31, 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 of R such that A82: CurInstr (P1,(Comput (P1,s1,i))) = MultBy (da,db) by SCMRING3:16; A83: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = MultBy (da,db) by A82, COMPOS_0:4; A84: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = succ (IC (Comput (P1,s1,i))) by A82, SCMRING2:14; hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A11, A12, A41, A15, A20, A83, SCMRING2:14; ::_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, A21, A41, A15, A20, A83, A84, SCMRING2:14; ::_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))) ) A85: ( (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 A17; 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 A86: 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 A87: 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 reconsider d = x as Data-Location of R by A43, A87, SCMRING2:23; percases ( da = d or da <> d ) ; supposeA88: 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, A41, A15, A82, A83, SCMRING2:14; hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A2, A9, A43, A52, A82, A85, A87, A86, A88, Th10, A5; ::_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, A41, A15, A82, A83, SCMRING2:14; hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A43, A47, A87; ::_thesis: verum end; end; end; then (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A45, GRFUNC_1:2; hence (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A43, A44, GRFUNC_1:3; ::_thesis: DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) now__::_thesis:_for_x_being_set_st_x_in_dom_(DataPart_(Comput_(P1,(s1_+*_(DataPart_s2)),(i_+_1))))_holds_ (DataPart_(Comput_(P1,(s1_+*_(DataPart_s2)),(i_+_1))))_._x_=_(DataPart_(Comput_(P2,s2,(i_+_1))))_._x let x be set ; ::_thesis: ( x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) implies (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 ) assume A89: 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 of R by A29, SCMRING2:23; 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, A15, A55, A82, A83, SCMRING2:14; hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A32, A85, A89; ::_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, A15, A55, A82, A83, SCMRING2:14; hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A36, A89; ::_thesis: verum end; end; end; then DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1))) by A30, GRFUNC_1:2; hence DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) by A29, A31, GRFUNC_1:3; ::_thesis: verum end; suppose InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 5 ; ::_thesis: S1[i + 1] then consider da being Data-Location of R, r being Element of R such that A90: CurInstr (P1,(Comput (P1,s1,i))) = da := r by SCMRING3:17; A91: IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = da := r by A90, COMPOS_0:4; A92: (Exec ((CurInstr (P1,(Comput (P1,s1,i)))),(Comput (P1,s1,i)))) . (IC ) = succ (IC (Comput (P1,s1,i))) by A90, SCMRING2:17; hence (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) by A11, A12, A41, A15, A20, A91, SCMRING2:17; ::_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, A21, A41, A15, A20, A91, A92, SCMRING2:17; ::_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 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 reconsider d = x as Data-Location of R by A43, A93, SCMRING2:23; percases ( da = d or da <> d ) ; supposeA94: da = d ; ::_thesis: ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . b1 = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . b1 thus ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = (Comput (P1,s1,(i + 1))) . d by A43, A93, FUNCT_1:49 .= r by A41, A90, A94, SCMRING2:17 .= (Comput (P2,s2,(i + 1))) . d by A12, A15, A91, A94, SCMRING2:17 .= ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A43, A93, FUNCT_1:49 ; ::_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, A41, A15, A90, A91, SCMRING2:17; hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A43, 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 A45, GRFUNC_1:2; hence (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A43, A44, GRFUNC_1:3; ::_thesis: DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) now__::_thesis:_for_x_being_set_st_x_in_dom_(DataPart_(Comput_(P1,(s1_+*_(DataPart_s2)),(i_+_1))))_holds_ (DataPart_(Comput_(P1,(s1_+*_(DataPart_s2)),(i_+_1))))_._x_=_(DataPart_(Comput_(P2,s2,(i_+_1))))_._x let x be set ; ::_thesis: ( x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) implies (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . b1 = (DataPart (Comput (P2,s2,(i + 1)))) . b1 ) assume A95: 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 of R by A29, SCMRING2:23; 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 = r & (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) . d = r ) by A12, A15, A55, A90, A91, SCMRING2:17; hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A32, A95; ::_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, A15, A55, A90, A91, SCMRING2:17; hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A36, A95; ::_thesis: verum end; end; end; then DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1))) by A30, GRFUNC_1:2; hence DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) by A29, A31, GRFUNC_1:3; ::_thesis: verum end; suppose InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 6 ; ::_thesis: S1[i + 1] then consider loc being Element of NAT such that A96: CurInstr (P1,(Comput (P1,s1,i))) = goto (loc,R) by SCMRING3:18; A97: CurInstr (P2,(Comput (P2,s2,i))) = goto ((loc + k),R) by A12, A96, SCMRING3:37; thus (IC (Comput (P1,s1,(i + 1)))) + k = loc + k by A41, A96, SCMRING2:15 .= IC (Comput (P2,s2,(i + 1))) by A15, A97, SCMRING2:15 ; ::_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 A21; ::_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 A98: 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 reconsider d = x as Data-Location of R by A43, A98, SCMRING2:23; ( (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d ) by A41, A15, A96, A97, SCMRING2:15; hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A43, A47, A98; ::_thesis: verum end; then (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A45, GRFUNC_1:2; hence (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A43, A44, GRFUNC_1:3; ::_thesis: DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) now__::_thesis:_for_x_being_set_st_x_in_dom_(DataPart_(Comput_(P1,(s1_+*_(DataPart_s2)),(i_+_1))))_holds_ (DataPart_(Comput_(P1,(s1_+*_(DataPart_s2)),(i_+_1))))_._x_=_(DataPart_(Comput_(P2,s2,(i_+_1))))_._x let x be set ; ::_thesis: ( x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) implies (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x ) assume A99: 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 of R by A29, SCMRING2:23; ( (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 A15, A55, A96, A97, SCMRING2:15; hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A36, A99; ::_thesis: verum end; then DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1))) by A30, GRFUNC_1:2; hence DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) by A29, A31, GRFUNC_1:3; ::_thesis: verum end; suppose InsCode (CurInstr (P1,(Comput (P1,s1,i)))) = 7 ; ::_thesis: S1[i + 1] then consider da being Data-Location of R, loc being Element of NAT such that A100: CurInstr (P1,(Comput (P1,s1,i))) = da =0_goto loc by SCMRING3:19; A101: now__::_thesis:_(_(_(Comput_(P1,s1,i))_._da_=_0._R_&_(IC_(Comput_(P1,s1,(i_+_1))))_+_k_=_loc_+_k_)_or_(_(Comput_(P1,s1,i))_._da_<>_0._R_&_(IC_(Comput_(P1,s1,(i_+_1))))_+_k_=_succ_(IC_(Comput_(P2,s2,i)))_)_) percases ( (Comput (P1,s1,i)) . da = 0. R or (Comput (P1,s1,i)) . da <> 0. R ) ; case (Comput (P1,s1,i)) . da = 0. R ; ::_thesis: (IC (Comput (P1,s1,(i + 1)))) + k = loc + k hence (IC (Comput (P1,s1,(i + 1)))) + k = loc + k by A41, A100, SCMRING2:16; ::_thesis: verum end; case (Comput (P1,s1,i)) . da <> 0. R ; ::_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, A41, A20, A100, SCMRING2:16; ::_thesis: verum end; end; end; A102: CurInstr (P2,(Comput (P2,s2,i))) = da =0_goto (loc + k) by A12, A100, SCMRING3:38; A103: now__::_thesis:_(_(_(Comput_(P2,s2,i))_._da_=_0._R_&_IC_(Comput_(P2,s2,(i_+_1)))_=_loc_+_k_)_or_(_(Comput_(P2,s2,i))_._da_<>_0._R_&_IC_(Comput_(P2,s2,(i_+_1)))_=_succ_(IC_(Comput_(P2,s2,i)))_)_) percases ( (Comput (P2,s2,i)) . da = 0. R or (Comput (P2,s2,i)) . da <> 0. R ) ; case (Comput (P2,s2,i)) . da = 0. R ; ::_thesis: IC (Comput (P2,s2,(i + 1))) = loc + k hence IC (Comput (P2,s2,(i + 1))) = loc + k by A15, A102, SCMRING2:16; ::_thesis: verum end; case (Comput (P2,s2,i)) . da <> 0. R ; ::_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 A15, A102, SCMRING2:16; ::_thesis: verum end; end; end; A104: (Comput (P1,(s1 +* (DataPart s2)),i)) . da = (Comput (P2,s2,i)) . da by A17; 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, A100, A104, A101, A103, Th11, A5; ::_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, A101, A103; ::_thesis: verum end; end; end; hence ( (IC (Comput (P1,s1,(i + 1)))) + k = IC (Comput (P2,s2,(i + 1))) & IncAddr ((CurInstr (P1,(Comput (P1,s1,(i + 1))))),k) = CurInstr (P2,(Comput (P2,s2,(i + 1)))) ) by A21; ::_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 A105: 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 reconsider d = x as Data-Location of R by A43, A105, SCMRING2:23; ( (Comput (P1,s1,(i + 1))) . d = (Comput (P1,s1,i)) . d & (Comput (P2,s2,(i + 1))) . d = (Comput (P2,s2,i)) . d ) by A41, A15, A100, A102, SCMRING2:16; hence ((Comput (P1,s1,(i + 1))) | (dom (DataPart p))) . x = ((Comput (P2,s2,(i + 1))) | (dom (DataPart p))) . x by A43, A47, A105; ::_thesis: verum end; then (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) c= (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A45, GRFUNC_1:2; hence (Comput (P1,s1,(i + 1))) | (dom (DataPart p)) = (Comput (P2,s2,(i + 1))) | (dom (DataPart p)) by A43, A44, GRFUNC_1:3; ::_thesis: DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) now__::_thesis:_for_x_being_set_st_x_in_dom_(DataPart_(Comput_(P1,(s1_+*_(DataPart_s2)),(i_+_1))))_holds_ (DataPart_(Comput_(P1,(s1_+*_(DataPart_s2)),(i_+_1))))_._x_=_(DataPart_(Comput_(P2,s2,(i_+_1))))_._x let x be set ; ::_thesis: ( x in dom (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) implies (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x ) assume A106: 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 of R by A29, SCMRING2:23; ( (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 A15, A55, A100, A102, SCMRING2:16; hence (DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1)))) . x = (DataPart (Comput (P2,s2,(i + 1)))) . x by A36, A106; ::_thesis: verum end; then DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) c= DataPart (Comput (P2,s2,(i + 1))) by A30, GRFUNC_1:2; hence DataPart (Comput (P1,(s1 +* (DataPart s2)),(i + 1))) = DataPart (Comput (P2,s2,(i + 1))) by A29, A31, GRFUNC_1:3; ::_thesis: verum end; end; end; A107: DataPart p c= p by RELAT_1:59; A108: DataPart (IncIC (p,k)) = DataPart p by MEMSTR_0:51; A109: DataPart p c= IncIC (p,k) by A108, MEMSTR_0:12; A110: (Comput (P1,s1,0)) | (dom (DataPart p)) = s1 | (dom (DataPart p)) .= DataPart p by A2, A107, GRFUNC_1:23, XBOOLE_1:1 .= s2 | (dom (DataPart p)) by A109, A3, GRFUNC_1:23, XBOOLE_1:1 .= (Comput (P2,s2,0)) | (dom (DataPart p)) ; A111: DataPart (Comput (P1,(s1 +* (DataPart s2)),0)) = DataPart (s1 +* (DataPart s2)) .= DataPart s2 by PBOOLE:142 .= DataPart (Comput (P2,s2,0)) ; A112: IC in dom (IncIC (p,k)) by MEMSTR_0:52; A113: (IC (Comput (P1,s1,0))) + k = (IC s1) + k .= (IC p) + k by A2, A1, GRFUNC_1:2 .= (IC p) + k .= IC (IncIC (p,k)) by MEMSTR_0:53 .= IC s2 by A3, A112, GRFUNC_1:2 .= IC (Comput (P2,s2,0)) ; A114: IC in dom (IncIC (p,k)) by MEMSTR_0:52; A115: (IC p) + k in dom (Reloc (q,k)) by A8, COMPOS_1:46; A116: P2 /. (IC s2) = P2 . (IC s2) by PBOOLE:143; A117: CurInstr (P2,(Comput (P2,s2,0))) = P2 . (IC s2) by A116 .= P2 . (IC (IncIC (p,k))) by A3, A114, GRFUNC_1:2 .= P2 . ((IC p) + k) by MEMSTR_0:53 .= P2 . ((IC p) + k) .= (Reloc (q,k)) . ((IC p) + k) by A115, A5, GRFUNC_1:2 ; A118: q . (IC p) = P1 . (IC s1) by A7, A8, A5, GRFUNC_1:2; A119: CurInstr (P1,s1) = q . (IC p) by A118, PBOOLE:143; A120: IncAddr ((CurInstr (P1,(Comput (P1,s1,0)))),k) = IncAddr ((CurInstr (P1,s1)),k) .= CurInstr (P2,(Comput (P2,s2,0))) by A117, A8, A119, COMPOS_1:35 ; A121: S1[ 0 ] by A113, A120, A110, A111; for n being Element of NAT holds S1[n] from NAT_1:sch_1(A121, A10); hence 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)) ) ; ::_thesis: verum end; registration let R be non trivial Ring; cluster SCM R -> relocable1 relocable2 ; coherence ( SCM R is relocable1 & SCM R is relocable2 ) proof thus SCM R is relocable1 ::_thesis: SCM R is relocable2 proof thus for k being Element of NAT for q being NAT -defined the InstructionsF of (SCM R) -valued finite non halt-free Function for p being non empty b2 -autonomic FinPartState of (SCM R) for s1, s2 being State of (SCM R) st p c= s1 & IncIC (p,k) c= s2 holds for P1, P2 being Instruction-Sequence of (SCM R) 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 Th12; :: 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)) | (dom (DataPart b2)) = (Comput (b6,b4,b7)) | (dom (DataPart b2)) ) ) let q be NAT -defined the InstructionsF of (SCM R) -valued finite non halt-free Function; ::_thesis: for b1 being set for b2, b3 being set holds ( not b1 c= b2 or not IncIC (b1,k) c= b3 or for b4, b5 being set holds ( not q c= b4 or not Reloc (q,k) c= b5 or for b6 being Element of NAT holds (Comput (b4,b2,b6)) | (dom (DataPart b1)) = (Comput (b5,b3,b6)) | (dom (DataPart b1)) ) ) let p be non empty q -autonomic FinPartState of (SCM R); ::_thesis: for b1, b2 being set holds ( not p c= b1 or not IncIC (p,k) c= b2 or for b3, b4 being set holds ( not q c= b3 or not Reloc (q,k) c= b4 or for b5 being Element of NAT holds (Comput (b3,b1,b5)) | (dom (DataPart p)) = (Comput (b4,b2,b5)) | (dom (DataPart p)) ) ) let s1, s2 be State of (SCM R); ::_thesis: ( not p c= s1 or not IncIC (p,k) c= s2 or for b1, b2 being set holds ( not q c= b1 or not Reloc (q,k) c= b2 or for b3 being Element of NAT holds (Comput (b1,s1,b3)) | (dom (DataPart p)) = (Comput (b2,s2,b3)) | (dom (DataPart p)) ) ) assume A1: ( p c= s1 & IncIC (p,k) c= s2 ) ; ::_thesis: for b1, b2 being set holds ( not q c= b1 or not Reloc (q,k) c= b2 or for b3 being Element of NAT holds (Comput (b1,s1,b3)) | (dom (DataPart p)) = (Comput (b2,s2,b3)) | (dom (DataPart p)) ) let P1, P2 be Instruction-Sequence of (SCM R); ::_thesis: ( not q c= P1 or not Reloc (q,k) c= P2 or for b1 being Element of NAT holds (Comput (P1,s1,b1)) | (dom (DataPart p)) = (Comput (P2,s2,b1)) | (dom (DataPart p)) ) assume ( q c= P1 & Reloc (q,k) c= P2 ) ; ::_thesis: for b1 being Element of NAT holds (Comput (P1,s1,b1)) | (dom (DataPart p)) = (Comput (P2,s2,b1)) | (dom (DataPart p)) hence for i being Element of NAT holds (Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart p)) by A1, Th12; ::_thesis: verum end; end;