let S be non empty 1-sorted ; :: thesis: for x being Element of SCM-Instr S holds
( ( x in {[0,{},{}]} & InsCode x = 0 ) or ( x in { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } & ( InsCode x = 1 or InsCode x = 2 or InsCode x = 3 or InsCode x = 4 ) ) or ( x in { [6,<*i*>,{}] where i is Nat : verum } & InsCode x = 6 ) or ( x in { [7,<*i*>,<*a*>] where i is Nat, a is Element of SCM-Data-Loc : verum } & InsCode x = 7 ) or ( x in { [5,{},<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of S : verum } & InsCode x = 5 ) )
let x be Element of SCM-Instr S; :: thesis: ( ( x in {[0,{},{}]} & InsCode x = 0 ) or ( x in { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } & ( InsCode x = 1 or InsCode x = 2 or InsCode x = 3 or InsCode x = 4 ) ) or ( x in { [6,<*i*>,{}] where i is Nat : verum } & InsCode x = 6 ) or ( x in { [7,<*i*>,<*a*>] where i is Nat, a is Element of SCM-Data-Loc : verum } & InsCode x = 7 ) or ( x in { [5,{},<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of S : verum } & InsCode x = 5 ) )
( x in (({[0,{},{}]} \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } ) \/ { [6,<*i*>,{}] where i is Nat : verum } ) \/ { [7,<*i*>,<*a*>] where i is Nat, a is Element of SCM-Data-Loc : verum } or x in { [5,{},<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of S : verum } ) by XBOOLE_0:def 3;
then ( x in ({[0,{},{}]} \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } ) \/ { [6,<*i*>,{}] where i is Nat : verum } or x in { [7,<*i*>,<*a*>] where i is Nat, a is Element of SCM-Data-Loc : verum } or x in { [5,{},<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of S : verum } ) by XBOOLE_0:def 3;
then ( x in {[0,{},{}]} \/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } or x in { [6,<*i*>,{}] where i is Nat : verum } or x in { [7,<*i*>,<*a*>] where i is Nat, a is Element of SCM-Data-Loc : verum } or x in { [5,{},<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of S : verum } ) by XBOOLE_0:def 3;
per cases then ( x in {[0,{},{}]} or x in { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } or x in { [6,<*i*>,{}] where i is Nat : verum } or x in { [7,<*i*>,<*a*>] where i is Nat, a is Element of SCM-Data-Loc : verum } or x in { [5,{},<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of S : verum } ) by XBOOLE_0:def 3;
case x in {[0,{},{}]} ; :: thesis: InsCode x = 0
then x = [0,{},{}] by TARSKI:def 1;
hence InsCode x = 0 ; :: thesis: verum
end;
case x in { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is Element of SCM-Data-Loc : I in {1,2,3,4} } ; :: thesis: ( InsCode x = 1 or InsCode x = 2 or InsCode x = 3 or InsCode x = 4 )
then consider I being Element of Segm 8, a, b being Element of SCM-Data-Loc such that
A1: x = [I,{},<*a,b*>] and
A2: I in {1,2,3,4} ;
InsCode x = I by A1;
hence ( InsCode x = 1 or InsCode x = 2 or InsCode x = 3 or InsCode x = 4 ) by A2, ENUMSET1:def 2; :: thesis: verum
end;
case x in { [6,<*i*>,{}] where i is Nat : verum } ; :: thesis: InsCode x = 6
then ex i being Nat st x = [6,<*i*>,{}] ;
hence InsCode x = 6 ; :: thesis: verum
end;
case x in { [7,<*i*>,<*a*>] where i is Nat, a is Element of SCM-Data-Loc : verum } ; :: thesis: InsCode x = 7
then ex i being Nat ex a being Element of SCM-Data-Loc st x = [7,<*i*>,<*a*>] ;
hence InsCode x = 7 ; :: thesis: verum
end;
case x in { [5,{},<*a,r*>] where a is Element of SCM-Data-Loc , r is Element of S : verum } ; :: thesis: InsCode x = 5
then ex a being Element of SCM-Data-Loc ex r being Element of S st x = [5,{},<*a,r*>] ;
hence InsCode x = 5 ; :: thesis: verum
end;
end;