:: SCMPDS_I semantic presentation begin theorem Th1: :: SCMPDS_I:1 for k being Integer holds k in SCM-Data-Loc \/ INT proof let k be Integer; ::_thesis: k in SCM-Data-Loc \/ INT ( k in INT & INT c= SCM-Data-Loc \/ INT ) by INT_1:def_2, XBOOLE_1:7; hence k in SCM-Data-Loc \/ INT ; ::_thesis: verum end; begin definition func SCMPDS-Instr -> set equals :: SCMPDS_I:def 1 (((({[0,{},{}]} \/ { [14,{},<*l*>] where l is Element of INT : verum } ) \/ { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } ) \/ { [I,{},<*v,c*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } ) \/ { [I,{},<*v,c1,c2*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {4,5,6,7,8} } ) \/ { [I,{},<*v1,v2,c1,c2*>] where I is Element of Segm 15, v1, v2 is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {9,10,11,12,13} } ; coherence (((({[0,{},{}]} \/ { [14,{},<*l*>] where l is Element of INT : verum } ) \/ { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } ) \/ { [I,{},<*v,c*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } ) \/ { [I,{},<*v,c1,c2*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {4,5,6,7,8} } ) \/ { [I,{},<*v1,v2,c1,c2*>] where I is Element of Segm 15, v1, v2 is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {9,10,11,12,13} } is set ; end; :: deftheorem defines SCMPDS-Instr SCMPDS_I:def_1_:_ SCMPDS-Instr = (((({[0,{},{}]} \/ { [14,{},<*l*>] where l is Element of INT : verum } ) \/ { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } ) \/ { [I,{},<*v,c*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } ) \/ { [I,{},<*v,c1,c2*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {4,5,6,7,8} } ) \/ { [I,{},<*v1,v2,c1,c2*>] where I is Element of Segm 15, v1, v2 is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {9,10,11,12,13} } ; Lm1: [0,{},{}] in SCMPDS-Instr proof set S1 = { [14,{},<*k1*>] where k1 is Element of INT : verum } ; set S2 = { [1,{},<*d1*>] where d1 is Element of SCM-Data-Loc : verum } ; set S3 = { [I2,{},<*d2,k2*>] where I2 is Element of Segm 15, d2 is Element of SCM-Data-Loc , k2 is Element of INT : I2 in {2,3} } ; [0,{},{}] in {[0,{},{}]} by TARSKI:def_1; then [0,{},{}] in {[0,{},{}]} \/ { [14,{},<*k1*>] where k1 is Element of INT : verum } by XBOOLE_0:def_3; then [0,{},{}] in ({[0,{},{}]} \/ { [14,{},<*k1*>] where k1 is Element of INT : verum } ) \/ { [1,{},<*d1*>] where d1 is Element of SCM-Data-Loc : verum } by XBOOLE_0:def_3; then [0,{},{}] in (({[0,{},{}]} \/ { [14,{},<*k1*>] where k1 is Element of INT : verum } ) \/ { [1,{},<*d1*>] where d1 is Element of SCM-Data-Loc : verum } ) \/ { [I2,{},<*d2,k2*>] where I2 is Element of Segm 15, d2 is Element of SCM-Data-Loc , k2 is Element of INT : I2 in {2,3} } by XBOOLE_0:def_3; then [0,{},{}] in ((({[0,{},{}]} \/ { [14,{},<*k1*>] where k1 is Element of INT : verum } ) \/ { [1,{},<*d1*>] where d1 is Element of SCM-Data-Loc : verum } ) \/ { [I2,{},<*d2,k2*>] where I2 is Element of Segm 15, d2 is Element of SCM-Data-Loc , k2 is Element of INT : I2 in {2,3} } ) \/ { [I3,{},<*d3,k3,k4*>] where I3 is Element of Segm 15, d3 is Element of SCM-Data-Loc , k3, k4 is Element of INT : I3 in {4,5,6,7,8} } by XBOOLE_0:def_3; hence [0,{},{}] in SCMPDS-Instr by XBOOLE_0:def_3; ::_thesis: verum end; theorem :: SCMPDS_I:2 [14,{},<*0*>] in SCMPDS-Instr proof set S1 = { [14,{},<*k1*>] where k1 is Element of INT : verum } ; set S2 = { [1,{},<*d1*>] where d1 is Element of SCM-Data-Loc : verum } ; set S3 = { [I2,{},<*d2,k2*>] where I2 is Element of Segm 15, d2 is Element of SCM-Data-Loc , k2 is Element of INT : I2 in {2,3} } ; 0 is Element of INT by INT_1:def_2; then [14,{},<*0*>] in { [14,{},<*k1*>] where k1 is Element of INT : verum } ; then [14,{},<*0*>] in {[0,{},{}]} \/ { [14,{},<*k1*>] where k1 is Element of INT : verum } by XBOOLE_0:def_3; then [14,{},<*0*>] in ({[0,{},{}]} \/ { [14,{},<*k1*>] where k1 is Element of INT : verum } ) \/ { [1,{},<*d1*>] where d1 is Element of SCM-Data-Loc : verum } by XBOOLE_0:def_3; then [14,{},<*0*>] in (({[0,{},{}]} \/ { [14,{},<*k1*>] where k1 is Element of INT : verum } ) \/ { [1,{},<*d1*>] where d1 is Element of SCM-Data-Loc : verum } ) \/ { [I2,{},<*d2,k2*>] where I2 is Element of Segm 15, d2 is Element of SCM-Data-Loc , k2 is Element of INT : I2 in {2,3} } by XBOOLE_0:def_3; then [14,{},<*0*>] in ((({[0,{},{}]} \/ { [14,{},<*k1*>] where k1 is Element of INT : verum } ) \/ { [1,{},<*d1*>] where d1 is Element of SCM-Data-Loc : verum } ) \/ { [I2,{},<*d2,k2*>] where I2 is Element of Segm 15, d2 is Element of SCM-Data-Loc , k2 is Element of INT : I2 in {2,3} } ) \/ { [I3,{},<*d3,k3,k4*>] where I3 is Element of Segm 15, d3 is Element of SCM-Data-Loc , k3, k4 is Element of INT : I3 in {4,5,6,7,8} } by XBOOLE_0:def_3; hence [14,{},<*0*>] in SCMPDS-Instr by XBOOLE_0:def_3; ::_thesis: verum end; registration cluster SCMPDS-Instr -> non empty ; coherence not SCMPDS-Instr is empty ; end; definition let d be Element of SCM-Data-Loc ; let s be Integer; :: original: <* redefine func<*d,s*> -> FinSequence of SCM-Data-Loc \/ INT; coherence <*d,s*> is FinSequence of SCM-Data-Loc \/ INT proof let y be set ; :: according to TARSKI:def_3,FINSEQ_1:def_4 ::_thesis: ( not y in proj2 <*d,s*> or y in SCM-Data-Loc \/ INT ) A1: dom <*d,s*> = {1,2} by FINSEQ_1:2, FINSEQ_1:89; assume y in rng <*d,s*> ; ::_thesis: y in SCM-Data-Loc \/ INT then consider x being set such that A2: x in dom <*d,s*> and A3: <*d,s*> . x = y by FUNCT_1:def_3; percases ( x = 1 or x = 2 ) by A2, A1, TARSKI:def_2; suppose x = 1 ; ::_thesis: y in SCM-Data-Loc \/ INT then y = d by A3, FINSEQ_1:44; hence y in SCM-Data-Loc \/ INT by XBOOLE_0:def_3; ::_thesis: verum end; supposeA4: x = 2 ; ::_thesis: y in SCM-Data-Loc \/ INT A5: s in INT by INT_1:def_2; y = s by A3, A4, FINSEQ_1:44; hence y in SCM-Data-Loc \/ INT by A5, XBOOLE_0:def_3; ::_thesis: verum end; end; end; end; definition let x be Element of SCMPDS-Instr ; given mk being Element of SCM-Data-Loc , I being Element of Segm 15 such that A1: x = [I,{},<*mk*>] ; funcx address_1 -> Element of SCM-Data-Loc means :Def2: :: SCMPDS_I:def 2 ex f being FinSequence of SCM-Data-Loc st ( f = x `3_3 & it = f /. 1 ); existence ex b1 being Element of SCM-Data-Loc ex f being FinSequence of SCM-Data-Loc st ( f = x `3_3 & b1 = f /. 1 ) proof take mk ; ::_thesis: ex f being FinSequence of SCM-Data-Loc st ( f = x `3_3 & mk = f /. 1 ) take <*mk*> ; ::_thesis: ( <*mk*> = x `3_3 & mk = <*mk*> /. 1 ) thus ( <*mk*> = x `3_3 & mk = <*mk*> /. 1 ) by A1, FINSEQ_4:16, RECDEF_2:def_3; ::_thesis: verum end; uniqueness for b1, b2 being Element of SCM-Data-Loc st ex f being FinSequence of SCM-Data-Loc st ( f = x `3_3 & b1 = f /. 1 ) & ex f being FinSequence of SCM-Data-Loc st ( f = x `3_3 & b2 = f /. 1 ) holds b1 = b2 ; end; :: deftheorem Def2 defines address_1 SCMPDS_I:def_2_:_ for x being Element of SCMPDS-Instr st ex mk being Element of SCM-Data-Loc ex I being Element of Segm 15 st x = [I,{},<*mk*>] holds for b2 being Element of SCM-Data-Loc holds ( b2 = x address_1 iff ex f being FinSequence of SCM-Data-Loc st ( f = x `3_3 & b2 = f /. 1 ) ); theorem :: SCMPDS_I:3 for I being Element of Segm 15 for x being Element of SCMPDS-Instr for mk being Element of SCM-Data-Loc st x = [I,{},<*mk*>] holds x address_1 = mk proof let I be Element of Segm 15; ::_thesis: for x being Element of SCMPDS-Instr for mk being Element of SCM-Data-Loc st x = [I,{},<*mk*>] holds x address_1 = mk let x be Element of SCMPDS-Instr ; ::_thesis: for mk being Element of SCM-Data-Loc st x = [I,{},<*mk*>] holds x address_1 = mk let mk be Element of SCM-Data-Loc ; ::_thesis: ( x = [I,{},<*mk*>] implies x address_1 = mk ) assume A1: x = [I,{},<*mk*>] ; ::_thesis: x address_1 = mk then consider f being FinSequence of SCM-Data-Loc such that A2: f = x `3_3 and A3: x address_1 = f /. 1 by Def2; f = <*mk*> by A1, A2, RECDEF_2:def_3; hence x address_1 = mk by A3, FINSEQ_4:16; ::_thesis: verum end; definition let x be Element of SCMPDS-Instr ; given r being Integer, I being Element of Segm 15 such that A1: x = [I,{},<*r*>] ; funcx const_INT -> Integer means :Def3: :: SCMPDS_I:def 3 ex f being FinSequence of INT st ( f = x `3_3 & it = f /. 1 ); existence ex b1 being Integer ex f being FinSequence of INT st ( f = x `3_3 & b1 = f /. 1 ) proof reconsider mm = r as Element of INT by INT_1:def_2; take r ; ::_thesis: ex f being FinSequence of INT st ( f = x `3_3 & r = f /. 1 ) take <*mm*> ; ::_thesis: ( <*mm*> = x `3_3 & r = <*mm*> /. 1 ) thus ( <*mm*> = x `3_3 & r = <*mm*> /. 1 ) by A1, FINSEQ_4:16, RECDEF_2:def_3; ::_thesis: verum end; uniqueness for b1, b2 being Integer st ex f being FinSequence of INT st ( f = x `3_3 & b1 = f /. 1 ) & ex f being FinSequence of INT st ( f = x `3_3 & b2 = f /. 1 ) holds b1 = b2 ; end; :: deftheorem Def3 defines const_INT SCMPDS_I:def_3_:_ for x being Element of SCMPDS-Instr st ex r being Integer ex I being Element of Segm 15 st x = [I,{},<*r*>] holds for b2 being Integer holds ( b2 = x const_INT iff ex f being FinSequence of INT st ( f = x `3_3 & b2 = f /. 1 ) ); theorem :: SCMPDS_I:4 for I being Element of Segm 15 for x being Element of SCMPDS-Instr for k being Integer st x = [I,{},<*k*>] holds x const_INT = k proof let I be Element of Segm 15; ::_thesis: for x being Element of SCMPDS-Instr for k being Integer st x = [I,{},<*k*>] holds x const_INT = k let x be Element of SCMPDS-Instr ; ::_thesis: for k being Integer st x = [I,{},<*k*>] holds x const_INT = k let k be Integer; ::_thesis: ( x = [I,{},<*k*>] implies x const_INT = k ) assume A1: x = [I,{},<*k*>] ; ::_thesis: x const_INT = k then consider f being FinSequence of INT such that A2: f = x `3_3 and A3: x const_INT = f /. 1 by Def3; ( k is Element of INT & f = <*k*> ) by A1, A2, INT_1:def_2, RECDEF_2:def_3; hence x const_INT = k by A3, FINSEQ_4:16; ::_thesis: verum end; definition let x be Element of SCMPDS-Instr ; given mk being Element of SCM-Data-Loc , r being Integer, I being Element of Segm 15 such that A1: x = [I,{},<*mk,r*>] ; funcx P21address -> Element of SCM-Data-Loc means :Def4: :: SCMPDS_I:def 4 ex f being FinSequence of SCM-Data-Loc \/ INT st ( f = x `3_3 & it = f /. 1 ); existence ex b1 being Element of SCM-Data-Loc ex f being FinSequence of SCM-Data-Loc \/ INT st ( f = x `3_3 & b1 = f /. 1 ) proof take mk ; ::_thesis: ex f being FinSequence of SCM-Data-Loc \/ INT st ( f = x `3_3 & mk = f /. 1 ) take <*mk,r*> ; ::_thesis: ( <*mk,r*> = x `3_3 & mk = <*mk,r*> /. 1 ) r in INT by INT_1:def_2; then ( mk is Element of SCM-Data-Loc \/ INT & r is Element of SCM-Data-Loc \/ INT ) by XBOOLE_0:def_3; hence ( <*mk,r*> = x `3_3 & mk = <*mk,r*> /. 1 ) by A1, FINSEQ_4:17, RECDEF_2:def_3; ::_thesis: verum end; uniqueness for b1, b2 being Element of SCM-Data-Loc st ex f being FinSequence of SCM-Data-Loc \/ INT st ( f = x `3_3 & b1 = f /. 1 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st ( f = x `3_3 & b2 = f /. 1 ) holds b1 = b2 ; funcx P22const -> Integer means :Def5: :: SCMPDS_I:def 5 ex f being FinSequence of SCM-Data-Loc \/ INT st ( f = x `3_3 & it = f /. 2 ); existence ex b1 being Integer ex f being FinSequence of SCM-Data-Loc \/ INT st ( f = x `3_3 & b1 = f /. 2 ) proof take r ; ::_thesis: ex f being FinSequence of SCM-Data-Loc \/ INT st ( f = x `3_3 & r = f /. 2 ) take <*mk,r*> ; ::_thesis: ( <*mk,r*> = x `3_3 & r = <*mk,r*> /. 2 ) r in INT by INT_1:def_2; then ( mk is Element of SCM-Data-Loc \/ INT & r is Element of SCM-Data-Loc \/ INT ) by XBOOLE_0:def_3; hence ( <*mk,r*> = x `3_3 & r = <*mk,r*> /. 2 ) by A1, FINSEQ_4:17, RECDEF_2:def_3; ::_thesis: verum end; uniqueness for b1, b2 being Integer st ex f being FinSequence of SCM-Data-Loc \/ INT st ( f = x `3_3 & b1 = f /. 2 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st ( f = x `3_3 & b2 = f /. 2 ) holds b1 = b2 ; end; :: deftheorem Def4 defines P21address SCMPDS_I:def_4_:_ for x being Element of SCMPDS-Instr st ex mk being Element of SCM-Data-Loc ex r being Integer ex I being Element of Segm 15 st x = [I,{},<*mk,r*>] holds for b2 being Element of SCM-Data-Loc holds ( b2 = x P21address iff ex f being FinSequence of SCM-Data-Loc \/ INT st ( f = x `3_3 & b2 = f /. 1 ) ); :: deftheorem Def5 defines P22const SCMPDS_I:def_5_:_ for x being Element of SCMPDS-Instr st ex mk being Element of SCM-Data-Loc ex r being Integer ex I being Element of Segm 15 st x = [I,{},<*mk,r*>] holds for b2 being Integer holds ( b2 = x P22const iff ex f being FinSequence of SCM-Data-Loc \/ INT st ( f = x `3_3 & b2 = f /. 2 ) ); theorem :: SCMPDS_I:5 for I being Element of Segm 15 for x being Element of SCMPDS-Instr for mk being Element of SCM-Data-Loc for r being Integer st x = [I,{},<*mk,r*>] holds ( x P21address = mk & x P22const = r ) proof let I be Element of Segm 15; ::_thesis: for x being Element of SCMPDS-Instr for mk being Element of SCM-Data-Loc for r being Integer st x = [I,{},<*mk,r*>] holds ( x P21address = mk & x P22const = r ) let x be Element of SCMPDS-Instr ; ::_thesis: for mk being Element of SCM-Data-Loc for r being Integer st x = [I,{},<*mk,r*>] holds ( x P21address = mk & x P22const = r ) let mk be Element of SCM-Data-Loc ; ::_thesis: for r being Integer st x = [I,{},<*mk,r*>] holds ( x P21address = mk & x P22const = r ) let r be Integer; ::_thesis: ( x = [I,{},<*mk,r*>] implies ( x P21address = mk & x P22const = r ) ) r in INT by INT_1:def_2; then A1: ( mk is Element of SCM-Data-Loc \/ INT & r is Element of SCM-Data-Loc \/ INT ) by XBOOLE_0:def_3; assume A2: x = [I,{},<*mk,r*>] ; ::_thesis: ( x P21address = mk & x P22const = r ) then consider f being FinSequence of SCM-Data-Loc \/ INT such that A3: f = x `3_3 and A4: x P21address = f /. 1 by Def4; f = <*mk,r*> by A2, A3, RECDEF_2:def_3; hence x P21address = mk by A4, A1, FINSEQ_4:17; ::_thesis: x P22const = r consider f being FinSequence of SCM-Data-Loc \/ INT such that A5: f = x `3_3 and A6: x P22const = f /. 2 by A2, Def5; f = <*mk,r*> by A2, A5, RECDEF_2:def_3; hence x P22const = r by A1, A6, FINSEQ_4:17; ::_thesis: verum end; definition let x be Element of SCMPDS-Instr ; given m1 being Element of SCM-Data-Loc , k1, k2 being Integer, I being Element of Segm 15 such that A1: x = [I,{},<*m1,k1,k2*>] ; funcx P31address -> Element of SCM-Data-Loc means :Def6: :: SCMPDS_I:def 6 ex f being FinSequence of SCM-Data-Loc \/ INT st ( f = x `3_3 & it = f /. 1 ); existence ex b1 being Element of SCM-Data-Loc ex f being FinSequence of SCM-Data-Loc \/ INT st ( f = x `3_3 & b1 = f /. 1 ) proof reconsider mm = m1, k1 = k1, k2 = k2 as Element of SCM-Data-Loc \/ INT by Th1, XBOOLE_0:def_3; take m1 ; ::_thesis: ex f being FinSequence of SCM-Data-Loc \/ INT st ( f = x `3_3 & m1 = f /. 1 ) take f = <*mm,k1,k2*>; ::_thesis: ( f = x `3_3 & m1 = f /. 1 ) thus f = x `3_3 by A1, RECDEF_2:def_3; ::_thesis: m1 = f /. 1 thus m1 = f /. 1 by FINSEQ_4:18; ::_thesis: verum end; uniqueness for b1, b2 being Element of SCM-Data-Loc st ex f being FinSequence of SCM-Data-Loc \/ INT st ( f = x `3_3 & b1 = f /. 1 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st ( f = x `3_3 & b2 = f /. 1 ) holds b1 = b2 ; funcx P32const -> Integer means :Def7: :: SCMPDS_I:def 7 ex f being FinSequence of SCM-Data-Loc \/ INT st ( f = x `3_3 & it = f /. 2 ); existence ex b1 being Integer ex f being FinSequence of SCM-Data-Loc \/ INT st ( f = x `3_3 & b1 = f /. 2 ) proof reconsider m1 = m1, mm = k1, k2 = k2 as Element of SCM-Data-Loc \/ INT by Th1, XBOOLE_0:def_3; take k1 ; ::_thesis: ex f being FinSequence of SCM-Data-Loc \/ INT st ( f = x `3_3 & k1 = f /. 2 ) take f = <*m1,mm,k2*>; ::_thesis: ( f = x `3_3 & k1 = f /. 2 ) thus f = x `3_3 by A1, RECDEF_2:def_3; ::_thesis: k1 = f /. 2 thus k1 = f /. 2 by FINSEQ_4:18; ::_thesis: verum end; uniqueness for b1, b2 being Integer st ex f being FinSequence of SCM-Data-Loc \/ INT st ( f = x `3_3 & b1 = f /. 2 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st ( f = x `3_3 & b2 = f /. 2 ) holds b1 = b2 ; funcx P33const -> Integer means :Def8: :: SCMPDS_I:def 8 ex f being FinSequence of SCM-Data-Loc \/ INT st ( f = x `3_3 & it = f /. 3 ); existence ex b1 being Integer ex f being FinSequence of SCM-Data-Loc \/ INT st ( f = x `3_3 & b1 = f /. 3 ) proof reconsider m1 = m1, k1 = k1, mm = k2 as Element of SCM-Data-Loc \/ INT by Th1, XBOOLE_0:def_3; take k2 ; ::_thesis: ex f being FinSequence of SCM-Data-Loc \/ INT st ( f = x `3_3 & k2 = f /. 3 ) take f = <*m1,k1,mm*>; ::_thesis: ( f = x `3_3 & k2 = f /. 3 ) thus f = x `3_3 by A1, RECDEF_2:def_3; ::_thesis: k2 = f /. 3 thus k2 = f /. 3 by FINSEQ_4:18; ::_thesis: verum end; uniqueness for b1, b2 being Integer st ex f being FinSequence of SCM-Data-Loc \/ INT st ( f = x `3_3 & b1 = f /. 3 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st ( f = x `3_3 & b2 = f /. 3 ) holds b1 = b2 ; end; :: deftheorem Def6 defines P31address SCMPDS_I:def_6_:_ for x being Element of SCMPDS-Instr st ex m1 being Element of SCM-Data-Loc ex k1, k2 being Integer ex I being Element of Segm 15 st x = [I,{},<*m1,k1,k2*>] holds for b2 being Element of SCM-Data-Loc holds ( b2 = x P31address iff ex f being FinSequence of SCM-Data-Loc \/ INT st ( f = x `3_3 & b2 = f /. 1 ) ); :: deftheorem Def7 defines P32const SCMPDS_I:def_7_:_ for x being Element of SCMPDS-Instr st ex m1 being Element of SCM-Data-Loc ex k1, k2 being Integer ex I being Element of Segm 15 st x = [I,{},<*m1,k1,k2*>] holds for b2 being Integer holds ( b2 = x P32const iff ex f being FinSequence of SCM-Data-Loc \/ INT st ( f = x `3_3 & b2 = f /. 2 ) ); :: deftheorem Def8 defines P33const SCMPDS_I:def_8_:_ for x being Element of SCMPDS-Instr st ex m1 being Element of SCM-Data-Loc ex k1, k2 being Integer ex I being Element of Segm 15 st x = [I,{},<*m1,k1,k2*>] holds for b2 being Integer holds ( b2 = x P33const iff ex f being FinSequence of SCM-Data-Loc \/ INT st ( f = x `3_3 & b2 = f /. 3 ) ); theorem :: SCMPDS_I:6 for I being Element of Segm 15 for x being Element of SCMPDS-Instr for d1 being Element of SCM-Data-Loc for k1, k2 being Integer st x = [I,{},<*d1,k1,k2*>] holds ( x P31address = d1 & x P32const = k1 & x P33const = k2 ) proof let I be Element of Segm 15; ::_thesis: for x being Element of SCMPDS-Instr for d1 being Element of SCM-Data-Loc for k1, k2 being Integer st x = [I,{},<*d1,k1,k2*>] holds ( x P31address = d1 & x P32const = k1 & x P33const = k2 ) let x be Element of SCMPDS-Instr ; ::_thesis: for d1 being Element of SCM-Data-Loc for k1, k2 being Integer st x = [I,{},<*d1,k1,k2*>] holds ( x P31address = d1 & x P32const = k1 & x P33const = k2 ) let d1 be Element of SCM-Data-Loc ; ::_thesis: for k1, k2 being Integer st x = [I,{},<*d1,k1,k2*>] holds ( x P31address = d1 & x P32const = k1 & x P33const = k2 ) let k1, k2 be Integer; ::_thesis: ( x = [I,{},<*d1,k1,k2*>] implies ( x P31address = d1 & x P32const = k1 & x P33const = k2 ) ) k1 in INT by INT_1:def_2; then A1: ( d1 is Element of SCM-Data-Loc \/ INT & k1 is Element of SCM-Data-Loc \/ INT ) by XBOOLE_0:def_3; k2 in INT by INT_1:def_2; then A2: k2 is Element of SCM-Data-Loc \/ INT by XBOOLE_0:def_3; assume A3: x = [I,{},<*d1,k1,k2*>] ; ::_thesis: ( x P31address = d1 & x P32const = k1 & x P33const = k2 ) then consider f being FinSequence of SCM-Data-Loc \/ INT such that A4: f = x `3_3 and A5: x P31address = f /. 1 by Def6; f = <*d1,k1,k2*> by A3, A4, RECDEF_2:def_3; hence x P31address = d1 by A1, A2, A5, FINSEQ_4:18; ::_thesis: ( x P32const = k1 & x P33const = k2 ) consider f being FinSequence of SCM-Data-Loc \/ INT such that A6: f = x `3_3 and A7: x P32const = f /. 2 by A3, Def7; f = <*d1,k1,k2*> by A3, A6, RECDEF_2:def_3; hence x P32const = k1 by A1, A2, A7, FINSEQ_4:18; ::_thesis: x P33const = k2 consider f being FinSequence of SCM-Data-Loc \/ INT such that A8: f = x `3_3 and A9: x P33const = f /. 3 by A3, Def8; f = <*d1,k1,k2*> by A3, A8, RECDEF_2:def_3; hence x P33const = k2 by A1, A2, A9, FINSEQ_4:18; ::_thesis: verum end; definition let x be Element of SCMPDS-Instr ; given m1, m2 being Element of SCM-Data-Loc , k1, k2 being Integer, I being Element of Segm 15 such that A1: x = [I,{},<*m1,m2,k1,k2*>] ; funcx P41address -> Element of SCM-Data-Loc means :Def9: :: SCMPDS_I:def 9 ex f being FinSequence of SCM-Data-Loc \/ INT st ( f = x `3_3 & it = f /. 1 ); existence ex b1 being Element of SCM-Data-Loc ex f being FinSequence of SCM-Data-Loc \/ INT st ( f = x `3_3 & b1 = f /. 1 ) proof reconsider mm = m1, m2 = m2, k1 = k1, k2 = k2 as Element of SCM-Data-Loc \/ INT by Th1, XBOOLE_0:def_3; take m1 ; ::_thesis: ex f being FinSequence of SCM-Data-Loc \/ INT st ( f = x `3_3 & m1 = f /. 1 ) take f = <*mm,m2,k1,k2*>; ::_thesis: ( f = x `3_3 & m1 = f /. 1 ) thus f = x `3_3 by A1, RECDEF_2:def_3; ::_thesis: m1 = f /. 1 thus m1 = f /. 1 by FINSEQ_4:80; ::_thesis: verum end; uniqueness for b1, b2 being Element of SCM-Data-Loc st ex f being FinSequence of SCM-Data-Loc \/ INT st ( f = x `3_3 & b1 = f /. 1 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st ( f = x `3_3 & b2 = f /. 1 ) holds b1 = b2 ; funcx P42address -> Element of SCM-Data-Loc means :Def10: :: SCMPDS_I:def 10 ex f being FinSequence of SCM-Data-Loc \/ INT st ( f = x `3_3 & it = f /. 2 ); existence ex b1 being Element of SCM-Data-Loc ex f being FinSequence of SCM-Data-Loc \/ INT st ( f = x `3_3 & b1 = f /. 2 ) proof reconsider m1 = m1, mm = m2, k1 = k1, k2 = k2 as Element of SCM-Data-Loc \/ INT by Th1, XBOOLE_0:def_3; take m2 ; ::_thesis: ex f being FinSequence of SCM-Data-Loc \/ INT st ( f = x `3_3 & m2 = f /. 2 ) take f = <*m1,mm,k1,k2*>; ::_thesis: ( f = x `3_3 & m2 = f /. 2 ) thus f = x `3_3 by A1, RECDEF_2:def_3; ::_thesis: m2 = f /. 2 thus m2 = f /. 2 by FINSEQ_4:80; ::_thesis: verum end; uniqueness for b1, b2 being Element of SCM-Data-Loc st ex f being FinSequence of SCM-Data-Loc \/ INT st ( f = x `3_3 & b1 = f /. 2 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st ( f = x `3_3 & b2 = f /. 2 ) holds b1 = b2 ; funcx P43const -> Integer means :Def11: :: SCMPDS_I:def 11 ex f being FinSequence of SCM-Data-Loc \/ INT st ( f = x `3_3 & it = f /. 3 ); existence ex b1 being Integer ex f being FinSequence of SCM-Data-Loc \/ INT st ( f = x `3_3 & b1 = f /. 3 ) proof reconsider m1 = m1, m2 = m2, mm = k1, k2 = k2 as Element of SCM-Data-Loc \/ INT by Th1, XBOOLE_0:def_3; take k1 ; ::_thesis: ex f being FinSequence of SCM-Data-Loc \/ INT st ( f = x `3_3 & k1 = f /. 3 ) take f = <*m1,m2,mm,k2*>; ::_thesis: ( f = x `3_3 & k1 = f /. 3 ) thus f = x `3_3 by A1, RECDEF_2:def_3; ::_thesis: k1 = f /. 3 thus k1 = f /. 3 by FINSEQ_4:80; ::_thesis: verum end; uniqueness for b1, b2 being Integer st ex f being FinSequence of SCM-Data-Loc \/ INT st ( f = x `3_3 & b1 = f /. 3 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st ( f = x `3_3 & b2 = f /. 3 ) holds b1 = b2 ; funcx P44const -> Integer means :Def12: :: SCMPDS_I:def 12 ex f being FinSequence of SCM-Data-Loc \/ INT st ( f = x `3_3 & it = f /. 4 ); existence ex b1 being Integer ex f being FinSequence of SCM-Data-Loc \/ INT st ( f = x `3_3 & b1 = f /. 4 ) proof reconsider m1 = m1, m2 = m2, k1 = k1, mm = k2 as Element of SCM-Data-Loc \/ INT by Th1, XBOOLE_0:def_3; take k2 ; ::_thesis: ex f being FinSequence of SCM-Data-Loc \/ INT st ( f = x `3_3 & k2 = f /. 4 ) take f = <*m1,m2,k1,mm*>; ::_thesis: ( f = x `3_3 & k2 = f /. 4 ) thus f = x `3_3 by A1, RECDEF_2:def_3; ::_thesis: k2 = f /. 4 thus k2 = f /. 4 by FINSEQ_4:80; ::_thesis: verum end; uniqueness for b1, b2 being Integer st ex f being FinSequence of SCM-Data-Loc \/ INT st ( f = x `3_3 & b1 = f /. 4 ) & ex f being FinSequence of SCM-Data-Loc \/ INT st ( f = x `3_3 & b2 = f /. 4 ) holds b1 = b2 ; end; :: deftheorem Def9 defines P41address SCMPDS_I:def_9_:_ for x being Element of SCMPDS-Instr st ex m1, m2 being Element of SCM-Data-Loc ex k1, k2 being Integer ex I being Element of Segm 15 st x = [I,{},<*m1,m2,k1,k2*>] holds for b2 being Element of SCM-Data-Loc holds ( b2 = x P41address iff ex f being FinSequence of SCM-Data-Loc \/ INT st ( f = x `3_3 & b2 = f /. 1 ) ); :: deftheorem Def10 defines P42address SCMPDS_I:def_10_:_ for x being Element of SCMPDS-Instr st ex m1, m2 being Element of SCM-Data-Loc ex k1, k2 being Integer ex I being Element of Segm 15 st x = [I,{},<*m1,m2,k1,k2*>] holds for b2 being Element of SCM-Data-Loc holds ( b2 = x P42address iff ex f being FinSequence of SCM-Data-Loc \/ INT st ( f = x `3_3 & b2 = f /. 2 ) ); :: deftheorem Def11 defines P43const SCMPDS_I:def_11_:_ for x being Element of SCMPDS-Instr st ex m1, m2 being Element of SCM-Data-Loc ex k1, k2 being Integer ex I being Element of Segm 15 st x = [I,{},<*m1,m2,k1,k2*>] holds for b2 being Integer holds ( b2 = x P43const iff ex f being FinSequence of SCM-Data-Loc \/ INT st ( f = x `3_3 & b2 = f /. 3 ) ); :: deftheorem Def12 defines P44const SCMPDS_I:def_12_:_ for x being Element of SCMPDS-Instr st ex m1, m2 being Element of SCM-Data-Loc ex k1, k2 being Integer ex I being Element of Segm 15 st x = [I,{},<*m1,m2,k1,k2*>] holds for b2 being Integer holds ( b2 = x P44const iff ex f being FinSequence of SCM-Data-Loc \/ INT st ( f = x `3_3 & b2 = f /. 4 ) ); theorem :: SCMPDS_I:7 for I being Element of Segm 15 for x being Element of SCMPDS-Instr for d1, d2 being Element of SCM-Data-Loc for k1, k2 being Integer st x = [I,{},<*d1,d2,k1,k2*>] holds ( x P41address = d1 & x P42address = d2 & x P43const = k1 & x P44const = k2 ) proof let I be Element of Segm 15; ::_thesis: for x being Element of SCMPDS-Instr for d1, d2 being Element of SCM-Data-Loc for k1, k2 being Integer st x = [I,{},<*d1,d2,k1,k2*>] holds ( x P41address = d1 & x P42address = d2 & x P43const = k1 & x P44const = k2 ) let x be Element of SCMPDS-Instr ; ::_thesis: for d1, d2 being Element of SCM-Data-Loc for k1, k2 being Integer st x = [I,{},<*d1,d2,k1,k2*>] holds ( x P41address = d1 & x P42address = d2 & x P43const = k1 & x P44const = k2 ) let d1, d2 be Element of SCM-Data-Loc ; ::_thesis: for k1, k2 being Integer st x = [I,{},<*d1,d2,k1,k2*>] holds ( x P41address = d1 & x P42address = d2 & x P43const = k1 & x P44const = k2 ) let k1, k2 be Integer; ::_thesis: ( x = [I,{},<*d1,d2,k1,k2*>] implies ( x P41address = d1 & x P42address = d2 & x P43const = k1 & x P44const = k2 ) ) A1: ( d1 is Element of SCM-Data-Loc \/ INT & d2 is Element of SCM-Data-Loc \/ INT ) by XBOOLE_0:def_3; k1 in INT by INT_1:def_2; then A2: k1 is Element of SCM-Data-Loc \/ INT by XBOOLE_0:def_3; k2 in INT by INT_1:def_2; then A3: k2 is Element of SCM-Data-Loc \/ INT by XBOOLE_0:def_3; assume A4: x = [I,{},<*d1,d2,k1,k2*>] ; ::_thesis: ( x P41address = d1 & x P42address = d2 & x P43const = k1 & x P44const = k2 ) then consider f being FinSequence of SCM-Data-Loc \/ INT such that A5: f = x `3_3 and A6: x P41address = f /. 1 by Def9; f = <*d1,d2,k1,k2*> by A4, A5, RECDEF_2:def_3; hence x P41address = d1 by A1, A2, A3, A6, FINSEQ_4:80; ::_thesis: ( x P42address = d2 & x P43const = k1 & x P44const = k2 ) consider f being FinSequence of SCM-Data-Loc \/ INT such that A7: f = x `3_3 and A8: x P42address = f /. 2 by A4, Def10; f = <*d1,d2,k1,k2*> by A4, A7, RECDEF_2:def_3; hence x P42address = d2 by A1, A2, A3, A8, FINSEQ_4:80; ::_thesis: ( x P43const = k1 & x P44const = k2 ) consider f being FinSequence of SCM-Data-Loc \/ INT such that A9: f = x `3_3 and A10: x P43const = f /. 3 by A4, Def11; f = <*d1,d2,k1,k2*> by A4, A9, RECDEF_2:def_3; hence x P43const = k1 by A1, A2, A3, A10, FINSEQ_4:80; ::_thesis: x P44const = k2 consider f being FinSequence of SCM-Data-Loc \/ INT such that A11: f = x `3_3 and A12: x P44const = f /. 4 by A4, Def12; f = <*d1,d2,k1,k2*> by A4, A11, RECDEF_2:def_3; hence x P44const = k2 by A1, A2, A3, A12, FINSEQ_4:80; ::_thesis: verum end; definition func RetSP -> Element of NAT equals :: SCMPDS_I:def 13 0 ; coherence 0 is Element of NAT ; func RetIC -> Element of NAT equals :: SCMPDS_I:def 14 1; coherence 1 is Element of NAT ; end; :: deftheorem defines RetSP SCMPDS_I:def_13_:_ RetSP = 0 ; :: deftheorem defines RetIC SCMPDS_I:def_14_:_ RetIC = 1; theorem Th8: :: SCMPDS_I:8 for x being Element of SCMPDS-Instr holds ( ( x in {[0,{},{}]} & InsCode x = 0 ) or ( x in { [14,{},<*l*>] where l is Element of INT : verum } & InsCode x = 14 ) or ( x in { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } & InsCode x = 1 ) or ( x in { [I,{},<*v,c*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } & ( InsCode x = 2 or InsCode x = 3 ) ) or ( x in { [I,{},<*v,c1,c2*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {4,5,6,7,8} } & ( InsCode x = 4 or InsCode x = 5 or InsCode x = 6 or InsCode x = 7 or InsCode x = 8 ) ) or ( x in { [I,{},<*v1,v2,c1,c2*>] where I is Element of Segm 15, v1, v2 is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {9,10,11,12,13} } & ( InsCode x = 9 or InsCode x = 10 or InsCode x = 11 or InsCode x = 12 or InsCode x = 13 ) ) ) proof let x be Element of SCMPDS-Instr ; ::_thesis: ( ( x in {[0,{},{}]} & InsCode x = 0 ) or ( x in { [14,{},<*l*>] where l is Element of INT : verum } & InsCode x = 14 ) or ( x in { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } & InsCode x = 1 ) or ( x in { [I,{},<*v,c*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } & ( InsCode x = 2 or InsCode x = 3 ) ) or ( x in { [I,{},<*v,c1,c2*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {4,5,6,7,8} } & ( InsCode x = 4 or InsCode x = 5 or InsCode x = 6 or InsCode x = 7 or InsCode x = 8 ) ) or ( x in { [I,{},<*v1,v2,c1,c2*>] where I is Element of Segm 15, v1, v2 is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {9,10,11,12,13} } & ( InsCode x = 9 or InsCode x = 10 or InsCode x = 11 or InsCode x = 12 or InsCode x = 13 ) ) ) ( x in ((({[0,{},{}]} \/ { [14,{},<*l*>] where l is Element of INT : verum } ) \/ { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } ) \/ { [I,{},<*v,c*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } ) \/ { [I,{},<*v,c1,c2*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {4,5,6,7,8} } or x in { [I,{},<*v1,v2,c1,c2*>] where I is Element of Segm 15, v1, v2 is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {9,10,11,12,13} } ) by XBOOLE_0:def_3; then ( x in (({[0,{},{}]} \/ { [14,{},<*l*>] where l is Element of INT : verum } ) \/ { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } ) \/ { [I,{},<*v,c*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } or x in { [I,{},<*v,c1,c2*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {4,5,6,7,8} } or x in { [I,{},<*v1,v2,c1,c2*>] where I is Element of Segm 15, v1, v2 is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {9,10,11,12,13} } ) by XBOOLE_0:def_3; then ( x in ({[0,{},{}]} \/ { [14,{},<*l*>] where l is Element of INT : verum } ) \/ { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } or x in { [I,{},<*v,c*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } or x in { [I,{},<*v,c1,c2*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {4,5,6,7,8} } or x in { [I,{},<*v1,v2,c1,c2*>] where I is Element of Segm 15, v1, v2 is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {9,10,11,12,13} } ) by XBOOLE_0:def_3; then ( x in {[0,{},{}]} \/ { [14,{},<*l*>] where l is Element of INT : verum } or x in { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } or x in { [I,{},<*v,c*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } or x in { [I,{},<*v,c1,c2*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {4,5,6,7,8} } or x in { [I,{},<*v1,v2,c1,c2*>] where I is Element of Segm 15, v1, v2 is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {9,10,11,12,13} } ) by XBOOLE_0:def_3; percasesthen ( x in {[0,{},{}]} or x in { [14,{},<*l*>] where l is Element of INT : verum } or x in { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } or x in { [I,{},<*v,c*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } or x in { [I,{},<*v,c1,c2*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {4,5,6,7,8} } or x in { [I,{},<*v1,v2,c1,c2*>] where I is Element of Segm 15, v1, v2 is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {9,10,11,12,13} } ) by XBOOLE_0:def_3; case x in {[0,{},{}]} ; ::_thesis: InsCode x = 0 then x = [0,{},{}] by TARSKI:def_1; hence InsCode x = 0 by RECDEF_2:def_1; ::_thesis: verum end; case x in { [14,{},<*l*>] where l is Element of INT : verum } ; ::_thesis: InsCode x = 14 then ex l being Element of INT st x = [14,{},<*l*>] ; hence InsCode x = 14 by RECDEF_2:def_1; ::_thesis: verum end; case x in { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } ; ::_thesis: InsCode x = 1 then ex sp being Element of SCM-Data-Loc st x = [1,{},<*sp*>] ; hence InsCode x = 1 by RECDEF_2:def_1; ::_thesis: verum end; case x in { [I,{},<*v,c*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } ; ::_thesis: ( InsCode x = 2 or InsCode x = 3 ) then consider I being Element of Segm 15, v being Element of SCM-Data-Loc , c being Element of INT such that A1: x = [I,{},<*v,c*>] and A2: I in {2,3} ; InsCode x = I by A1, RECDEF_2:def_1; hence ( InsCode x = 2 or InsCode x = 3 ) by A2, TARSKI:def_2; ::_thesis: verum end; case x in { [I,{},<*v,c1,c2*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {4,5,6,7,8} } ; ::_thesis: ( InsCode x = 4 or InsCode x = 5 or InsCode x = 6 or InsCode x = 7 or InsCode x = 8 ) then consider I being Element of Segm 15, v being Element of SCM-Data-Loc , c1, c2 being Element of INT such that A3: x = [I,{},<*v,c1,c2*>] and A4: I in {4,5,6,7,8} ; InsCode x = I by A3, RECDEF_2:def_1; hence ( InsCode x = 4 or InsCode x = 5 or InsCode x = 6 or InsCode x = 7 or InsCode x = 8 ) by A4, ENUMSET1:def_3; ::_thesis: verum end; case x in { [I,{},<*v1,v2,c1,c2*>] where I is Element of Segm 15, v1, v2 is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {9,10,11,12,13} } ; ::_thesis: ( InsCode x = 9 or InsCode x = 10 or InsCode x = 11 or InsCode x = 12 or InsCode x = 13 ) then consider I being Element of Segm 15, v1, v2 being Element of SCM-Data-Loc , c1, c2 being Element of INT such that A5: x = [I,{},<*v1,v2,c1,c2*>] and A6: I in {9,10,11,12,13} ; InsCode x = I by A5, RECDEF_2:def_1; hence ( InsCode x = 9 or InsCode x = 10 or InsCode x = 11 or InsCode x = 12 or InsCode x = 13 ) by A6, ENUMSET1:def_3; ::_thesis: verum end; end; end; begin registration cluster proj2 SCMPDS-Instr -> FinSequence-membered ; coherence proj2 SCMPDS-Instr is FinSequence-membered proof let f be set ; :: according to FINSEQ_1:def_18 ::_thesis: ( not f in proj2 SCMPDS-Instr or f is set ) assume f in proj2 SCMPDS-Instr ; ::_thesis: f is set then consider y being set such that A1: [y,f] in SCMPDS-Instr by XTUPLE_0:def_13; set x = [y,f]; percases ( [y,f] in ((({[0,{},{}]} \/ { [14,{},<*l*>] where l is Element of INT : verum } ) \/ { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } ) \/ { [I,{},<*v,c*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } ) \/ { [I,{},<*v,c1,c2*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {4,5,6,7,8} } or [y,f] in { [I,{},<*v1,v2,c1,c2*>] where I is Element of Segm 15, v1, v2 is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {9,10,11,12,13} } ) by A1, XBOOLE_0:def_3; supposeA2: [y,f] in ((({[0,{},{}]} \/ { [14,{},<*l*>] where l is Element of INT : verum } ) \/ { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } ) \/ { [I,{},<*v,c*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } ) \/ { [I,{},<*v,c1,c2*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {4,5,6,7,8} } ; ::_thesis: f is set percases ( [y,f] in (({[0,{},{}]} \/ { [14,{},<*l*>] where l is Element of INT : verum } ) \/ { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } ) \/ { [I,{},<*v,c*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } or [y,f] in { [I,{},<*v,c1,c2*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {4,5,6,7,8} } ) by A2, XBOOLE_0:def_3; suppose [y,f] in (({[0,{},{}]} \/ { [14,{},<*l*>] where l is Element of INT : verum } ) \/ { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } ) \/ { [I,{},<*v,c*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } ; ::_thesis: f is set then [y,f] in ({[0,{},{}]} \/ ( { [14,{},<*l*>] where l is Element of INT : verum } \/ { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } )) \/ { [I,{},<*v,c*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } by XBOOLE_1:4; then ( [y,f] in {[0,{},{}]} \/ ( { [14,{},<*l*>] where l is Element of INT : verum } \/ { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } ) or [y,f] in { [I,{},<*v,c*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } ) by XBOOLE_0:def_3; percasesthen ( [y,f] in {[0,{},{}]} or [y,f] in { [14,{},<*l*>] where l is Element of INT : verum } \/ { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } or [y,f] in { [I,{},<*v,c*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } ) by XBOOLE_0:def_3; suppose [y,f] in {[0,{},{}]} ; ::_thesis: f is set then [y,f] = [0,{},{}] by TARSKI:def_1; hence f is FinSequence by XTUPLE_0:1; ::_thesis: verum end; supposeA3: [y,f] in { [14,{},<*l*>] where l is Element of INT : verum } \/ { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } ; ::_thesis: f is set percases ( [y,f] in { [14,{},<*l*>] where l is Element of INT : verum } or [y,f] in { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } ) by A3, XBOOLE_0:def_3; suppose [y,f] in { [14,{},<*l*>] where l is Element of INT : verum } ; ::_thesis: f is set then ex l being Element of INT st [y,f] = [14,{},<*l*>] ; hence f is FinSequence by XTUPLE_0:1; ::_thesis: verum end; suppose [y,f] in { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } ; ::_thesis: f is set then ex sp being Element of SCM-Data-Loc st [y,f] = [1,{},<*sp*>] ; hence f is FinSequence by XTUPLE_0:1; ::_thesis: verum end; end; end; suppose [y,f] in { [I,{},<*v,c*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } ; ::_thesis: f is set then ex I being Element of Segm 15 ex v being Element of SCM-Data-Loc ex c being Element of INT st ( [y,f] = [I,{},<*v,c*>] & I in {2,3} ) ; hence f is FinSequence by XTUPLE_0:1; ::_thesis: verum end; end; end; suppose [y,f] in { [I,{},<*v,c1,c2*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {4,5,6,7,8} } ; ::_thesis: f is set then ex I being Element of Segm 15 ex v being Element of SCM-Data-Loc ex c1, c2 being Element of INT st ( [y,f] = [I,{},<*v,c1,c2*>] & I in {4,5,6,7,8} ) ; hence f is FinSequence by XTUPLE_0:1; ::_thesis: verum end; end; end; suppose [y,f] in { [I,{},<*v1,v2,c1,c2*>] where I is Element of Segm 15, v1, v2 is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {9,10,11,12,13} } ; ::_thesis: f is set then ex I being Element of Segm 15 ex v1, v2 being Element of SCM-Data-Loc ex c1, c2 being Element of INT st ( [y,f] = [I,{},<*v1,v2,c1,c2*>] & I in {9,10,11,12,13} ) ; hence f is FinSequence by XTUPLE_0:1; ::_thesis: verum end; end; end; end; registration cluster SCMPDS-Instr -> standard-ins ; coherence SCMPDS-Instr is standard-ins proof consider X being non empty set such that A1: proj2 SCMPDS-Instr c= X * by FINSEQ_1:85; take X ; :: according to COMPOS_0:def_1 ::_thesis: SCMPDS-Instr c= [:NAT,(NAT *),(X *):] let x be set ; :: according to TARSKI:def_3 ::_thesis: ( not x in SCMPDS-Instr or x in [:NAT,(NAT *),(X *):] ) assume A2: x in SCMPDS-Instr ; ::_thesis: x in [:NAT,(NAT *),(X *):] A3: {} in NAT * by FINSEQ_1:49; percases ( x in ((({[0,{},{}]} \/ { [14,{},<*l*>] where l is Element of INT : verum } ) \/ { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } ) \/ { [I,{},<*v,c*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } ) \/ { [I,{},<*v,c1,c2*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {4,5,6,7,8} } or x in { [I,{},<*v1,v2,c1,c2*>] where I is Element of Segm 15, v1, v2 is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {9,10,11,12,13} } ) by A2, XBOOLE_0:def_3; suppose x in ((({[0,{},{}]} \/ { [14,{},<*l*>] where l is Element of INT : verum } ) \/ { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } ) \/ { [I,{},<*v,c*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } ) \/ { [I,{},<*v,c1,c2*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {4,5,6,7,8} } ; ::_thesis: x in [:NAT,(NAT *),(X *):] percasesthen ( x in (({[0,{},{}]} \/ { [14,{},<*l*>] where l is Element of INT : verum } ) \/ { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } ) \/ { [I,{},<*v,c*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } or x in { [I,{},<*v,c1,c2*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {4,5,6,7,8} } ) by XBOOLE_0:def_3; supposeA4: x in (({[0,{},{}]} \/ { [14,{},<*l*>] where l is Element of INT : verum } ) \/ { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } ) \/ { [I,{},<*v,c*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } ; ::_thesis: x in [:NAT,(NAT *),(X *):] percases ( x in ({[0,{},{}]} \/ { [14,{},<*l*>] where l is Element of INT : verum } ) \/ { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } or x in { [I,{},<*v,c*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } ) by A4, XBOOLE_0:def_3; supposeA5: x in ({[0,{},{}]} \/ { [14,{},<*l*>] where l is Element of INT : verum } ) \/ { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } ; ::_thesis: x in [:NAT,(NAT *),(X *):] percases ( x in {[0,{},{}]} \/ { [14,{},<*l*>] where l is Element of INT : verum } or x in { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } ) by A5, XBOOLE_0:def_3; suppose x in {[0,{},{}]} \/ { [14,{},<*l*>] where l is Element of INT : verum } ; ::_thesis: x in [:NAT,(NAT *),(X *):] percasesthen ( x in {[0,{},{}]} or x in { [14,{},<*l*>] where l is Element of INT : verum } ) by XBOOLE_0:def_3; suppose x in {[0,{},{}]} ; ::_thesis: x in [:NAT,(NAT *),(X *):] then A6: x = [0,{},{}] by TARSKI:def_1; {} in X * by FINSEQ_1:49; hence x in [:NAT,(NAT *),(X *):] by A6, A3, MCART_1:69; ::_thesis: verum end; suppose x in { [14,{},<*l*>] where l is Element of INT : verum } ; ::_thesis: x in [:NAT,(NAT *),(X *):] then consider l being Element of INT such that A7: x = [14,{},<*l*>] ; <*l*> in proj2 SCMPDS-Instr by A2, A7, XTUPLE_0:def_13; hence x in [:NAT,(NAT *),(X *):] by A1, A7, A3, MCART_1:69; ::_thesis: verum end; end; end; suppose x in { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } ; ::_thesis: x in [:NAT,(NAT *),(X *):] then consider sp being Element of SCM-Data-Loc such that A8: x = [1,{},<*sp*>] ; <*sp*> in proj2 SCMPDS-Instr by A2, A8, XTUPLE_0:def_13; hence x in [:NAT,(NAT *),(X *):] by A1, A8, A3, MCART_1:69; ::_thesis: verum end; end; end; suppose x in { [I,{},<*v,c*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } ; ::_thesis: x in [:NAT,(NAT *),(X *):] then consider I being Element of Segm 15, v being Element of SCM-Data-Loc , c being Element of INT such that A9: ( x = [I,{},<*v,c*>] & I in {2,3} ) ; <*v,c*> in proj2 SCMPDS-Instr by A2, A9, XTUPLE_0:def_13; hence x in [:NAT,(NAT *),(X *):] by A1, A9, A3, MCART_1:69; ::_thesis: verum end; end; end; suppose x in { [I,{},<*v,c1,c2*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {4,5,6,7,8} } ; ::_thesis: x in [:NAT,(NAT *),(X *):] then consider I being Element of Segm 15, v being Element of SCM-Data-Loc , c1, c2 being Element of INT such that A10: ( x = [I,{},<*v,c1,c2*>] & I in {4,5,6,7,8} ) ; <*v,c1,c2*> in proj2 SCMPDS-Instr by A2, A10, XTUPLE_0:def_13; hence x in [:NAT,(NAT *),(X *):] by A1, A10, A3, MCART_1:69; ::_thesis: verum end; end; end; suppose x in { [I,{},<*v1,v2,c1,c2*>] where I is Element of Segm 15, v1, v2 is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {9,10,11,12,13} } ; ::_thesis: x in [:NAT,(NAT *),(X *):] then consider I being Element of Segm 15, v1, v2 being Element of SCM-Data-Loc , c1, c2 being Element of INT such that A11: ( x = [I,{},<*v1,v2,c1,c2*>] & I in {9,10,11,12,13} ) ; <*v1,v2,c1,c2*> in proj2 SCMPDS-Instr by A2, A11, XTUPLE_0:def_13; hence x in [:NAT,(NAT *),(X *):] by A1, A11, A3, MCART_1:69; ::_thesis: verum end; end; end; end; Lm2: for l being Element of SCMPDS-Instr holds InsCode l <= 14 proof let l be Element of SCMPDS-Instr ; ::_thesis: InsCode l <= 14 ( InsCode l = 0 or InsCode l = 1 or InsCode l = 2 or InsCode l = 3 or InsCode l = 4 or InsCode l = 5 or InsCode l = 6 or InsCode l = 7 or InsCode l = 8 or InsCode l = 9 or InsCode l = 10 or InsCode l = 11 or InsCode l = 12 or InsCode l = 13 or InsCode l = 14 ) by Th8; hence InsCode l <= 14 ; ::_thesis: verum end; Lm3: for i being Element of SCMPDS-Instr st InsCode i = 0 holds JumpPart i = {} proof let i be Element of SCMPDS-Instr ; ::_thesis: ( InsCode i = 0 implies JumpPart i = {} ) assume InsCode i = 0 ; ::_thesis: JumpPart i = {} then i in {[0,{},{}]} by Th8; then i = [0,{},{}] by TARSKI:def_1; hence JumpPart i = {} by RECDEF_2:def_2; ::_thesis: verum end; Lm4: for i being Element of SCMPDS-Instr st InsCode i = 14 holds JumpPart i = {} proof let i be Element of SCMPDS-Instr ; ::_thesis: ( InsCode i = 14 implies JumpPart i = {} ) assume InsCode i = 14 ; ::_thesis: JumpPart i = {} then i in { [14,{},<*l*>] where l is Element of INT : verum } by Th8; then ex l being Element of INT st i = [14,{},<*l*>] ; hence JumpPart i = {} by RECDEF_2:def_2; ::_thesis: verum end; Lm5: for i being Element of SCMPDS-Instr st InsCode i = 1 holds JumpPart i = {} proof let i be Element of SCMPDS-Instr ; ::_thesis: ( InsCode i = 1 implies JumpPart i = {} ) assume InsCode i = 1 ; ::_thesis: JumpPart i = {} then i in { [1,{},<*sp*>] where sp is Element of SCM-Data-Loc : verum } by Th8; then ex sp being Element of SCM-Data-Loc st i = [1,{},<*sp*>] ; hence JumpPart i = {} by RECDEF_2:def_2; ::_thesis: verum end; Lm6: for i being Element of SCMPDS-Instr st ( InsCode i = 2 or InsCode i = 3 ) holds JumpPart i = {} proof let i be Element of SCMPDS-Instr ; ::_thesis: ( ( InsCode i = 2 or InsCode i = 3 ) implies JumpPart i = {} ) assume ( InsCode i = 2 or InsCode i = 3 ) ; ::_thesis: JumpPart i = {} then i in { [I,{},<*v,c*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c is Element of INT : I in {2,3} } by Th8; then ex I being Element of Segm 15 ex v being Element of SCM-Data-Loc ex c being Element of INT st ( i = [I,{},<*v,c*>] & I in {2,3} ) ; hence JumpPart i = {} by RECDEF_2:def_2; ::_thesis: verum end; Lm7: for i being Element of SCMPDS-Instr st ( InsCode i = 4 or InsCode i = 5 or InsCode i = 6 or InsCode i = 7 or InsCode i = 8 ) holds JumpPart i = {} proof let i be Element of SCMPDS-Instr ; ::_thesis: ( ( InsCode i = 4 or InsCode i = 5 or InsCode i = 6 or InsCode i = 7 or InsCode i = 8 ) implies JumpPart i = {} ) assume ( InsCode i = 4 or InsCode i = 5 or InsCode i = 6 or InsCode i = 7 or InsCode i = 8 ) ; ::_thesis: JumpPart i = {} then i in { [I,{},<*v,c1,c2*>] where I is Element of Segm 15, v is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {4,5,6,7,8} } by Th8; then ex I being Element of Segm 15 ex v being Element of SCM-Data-Loc ex c1, c2 being Element of INT st ( i = [I,{},<*v,c1,c2*>] & I in {4,5,6,7,8} ) ; hence JumpPart i = {} by RECDEF_2:def_2; ::_thesis: verum end; Lm8: for i being Element of SCMPDS-Instr st ( InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 or InsCode i = 13 ) holds JumpPart i = {} proof let i be Element of SCMPDS-Instr ; ::_thesis: ( ( InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 or InsCode i = 13 ) implies JumpPart i = {} ) assume ( InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 or InsCode i = 13 ) ; ::_thesis: JumpPart i = {} then i in { [I,{},<*v1,v2,c1,c2*>] where I is Element of Segm 15, v1, v2 is Element of SCM-Data-Loc , c1, c2 is Element of INT : I in {9,10,11,12,13} } by Th8; then ex I being Element of Segm 15 ex v1, v2 being Element of SCM-Data-Loc ex c1, c2 being Element of INT st ( i = [I,{},<*v1,v2,c1,c2*>] & I in {9,10,11,12,13} ) ; hence JumpPart i = {} by RECDEF_2:def_2; ::_thesis: verum end; registration cluster SCMPDS-Instr -> homogeneous ; coherence SCMPDS-Instr is homogeneous proof let i, j be Element of SCMPDS-Instr ; :: according to COMPOS_0:def_5 ::_thesis: ( not InsCode i = InsCode j or dom (i `2_3) = dom (j `2_3) ) assume A1: InsCode i = InsCode j ; ::_thesis: dom (i `2_3) = dom (j `2_3) percases ( InsCode i = 0 or InsCode i = 14 or InsCode i = 1 or InsCode i = 2 or InsCode i = 3 or InsCode i = 4 or InsCode i = 5 or InsCode i = 6 or InsCode i = 7 or InsCode i = 8 or InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 or InsCode i = 13 ) by Lm2, NAT_1:60; suppose InsCode i = 0 ; ::_thesis: dom (i `2_3) = dom (j `2_3) then ( JumpPart i = {} & JumpPart j = {} ) by A1, Lm3; hence dom (i `2_3) = dom (j `2_3) ; ::_thesis: verum end; suppose InsCode i = 14 ; ::_thesis: dom (i `2_3) = dom (j `2_3) then ( JumpPart i = {} & JumpPart j = {} ) by A1, Lm4; hence dom (i `2_3) = dom (j `2_3) ; ::_thesis: verum end; suppose InsCode i = 1 ; ::_thesis: dom (i `2_3) = dom (j `2_3) then ( JumpPart i = {} & JumpPart j = {} ) by A1, Lm5; hence dom (i `2_3) = dom (j `2_3) ; ::_thesis: verum end; suppose ( InsCode i = 2 or InsCode i = 3 ) ; ::_thesis: dom (i `2_3) = dom (j `2_3) then ( JumpPart i = {} & JumpPart j = {} ) by A1, Lm6; hence dom (i `2_3) = dom (j `2_3) ; ::_thesis: verum end; suppose ( InsCode i = 4 or InsCode i = 5 or InsCode i = 6 or InsCode i = 7 or InsCode i = 8 ) ; ::_thesis: dom (i `2_3) = dom (j `2_3) then ( JumpPart i = {} & JumpPart j = {} ) by A1, Lm7; hence dom (i `2_3) = dom (j `2_3) ; ::_thesis: verum end; suppose ( InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 or InsCode i = 13 ) ; ::_thesis: dom (i `2_3) = dom (j `2_3) then ( JumpPart i = {} & JumpPart j = {} ) by A1, Lm8; hence dom (i `2_3) = dom (j `2_3) ; ::_thesis: verum end; end; end; end; registration cluster SCMPDS-Instr -> J/A-independent ; coherence SCMPDS-Instr is J/A-independent proof let T be InsType of SCMPDS-Instr; :: according to COMPOS_0:def_7 ::_thesis: for b1, b2 being set holds ( not b1 in JumpParts T or not proj1 b1 = proj1 b2 or for b3 being set holds ( not [T,b1,b3] in SCMPDS-Instr or [T,b2,b3] in SCMPDS-Instr ) ) let f1, f2 be natural-valued Function; ::_thesis: ( not f1 in JumpParts T or not proj1 f1 = proj1 f2 or for b1 being set holds ( not [T,f1,b1] in SCMPDS-Instr or [T,f2,b1] in SCMPDS-Instr ) ) assume that A1: f1 in JumpParts T and A2: dom f1 = dom f2 ; ::_thesis: for b1 being set holds ( not [T,f1,b1] in SCMPDS-Instr or [T,f2,b1] in SCMPDS-Instr ) let p be set ; ::_thesis: ( not [T,f1,p] in SCMPDS-Instr or [T,f2,p] in SCMPDS-Instr ) assume A3: [T,f1,p] in SCMPDS-Instr ; ::_thesis: [T,f2,p] in SCMPDS-Instr reconsider i = [T,f1,p] as Element of SCMPDS-Instr by A3; ( InsCode i = 0 or InsCode i = 1 or InsCode i = 2 or InsCode i = 3 or InsCode i = 4 or InsCode i = 5 or InsCode i = 6 or InsCode i = 7 or InsCode i = 8 or InsCode i = 9 or InsCode i = 10 or InsCode i = 11 or InsCode i = 12 or InsCode i = 13 or InsCode i = 14 ) by Lm2, NAT_1:60; then A4: JumpPart i = {} by Lm4, Lm5, Lm6, Lm7, Lm8, Lm3; T = InsCode i by RECDEF_2:def_1; then A5: JumpParts T = {0} by A4, COMPOS_0:11; f1 = 0 by A5, A1, TARSKI:def_1; then f1 = f2 by A2; hence [T,f2,p] in SCMPDS-Instr by A3; ::_thesis: verum end; end; registration cluster SCMPDS-Instr -> with_halt ; coherence SCMPDS-Instr is with_halt proof thus [0,{},{}] in SCMPDS-Instr by Lm1; :: according to COMPOS_0:def_10 ::_thesis: verum end; end;