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;

( 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;

per cases then
( 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;

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 ; :: thesis: verum

end;hence InsCode x = 1 ; :: thesis: verum

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;

hence ( InsCode x = 2 or InsCode x = 3 ) by A2, TARSKI:def 2; :: thesis: verum

end;A1: x = [I,{},<*v,c*>] and

A2: I in {2,3} ;

InsCode x = I by A1;

hence ( InsCode x = 2 or InsCode x = 3 ) by A2, TARSKI:def 2; :: thesis: verum

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;

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;A3: x = [I,{},<*v,c1,c2*>] and

A4: I in {4,5,6,7,8} ;

InsCode x = I by A3;

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

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;

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;A5: x = [I,{},<*v1,v2,c1,c2*>] and

A6: I in {9,10,11,12,13} ;

InsCode x = I by A5;

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