let x be Element of SCM-Instr ; :: thesis: ( ( x in {[SCM-Halt,{},{}]} & InsCode x = 0 ) or ( x in { [J,<*a*>,{}] where J is Element of Segm 9, a is Nat : J = 6 } & InsCode x = 6 ) or ( x in { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Nat, b1 is Element of SCM-Data-Loc : K in {7,8} } & ( InsCode x = 7 or InsCode x = 8 ) ) or ( x in { [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of SCM-Data-Loc : I in {1,2,3,4,5} } & ( InsCode x = 1 or InsCode x = 2 or InsCode x = 3 or InsCode x = 4 or InsCode x = 5 ) ) )

( x in ({[SCM-Halt,{},{}]} \/ { [J,<*a*>,{}] where J is Element of Segm 9, a is Nat : J = 6 } ) \/ { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Nat, b1 is Element of SCM-Data-Loc : K in {7,8} } or x in { [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of SCM-Data-Loc : I in {1,2,3,4,5} } ) by XBOOLE_0:def 3;

then ( x in {[SCM-Halt,{},{}]} \/ { [J,<*a*>,{}] where J is Element of Segm 9, a is Nat : J = 6 } or x in { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Nat, b1 is Element of SCM-Data-Loc : K in {7,8} } or x in { [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of SCM-Data-Loc : I in {1,2,3,4,5} } ) by XBOOLE_0:def 3;

( x in ({[SCM-Halt,{},{}]} \/ { [J,<*a*>,{}] where J is Element of Segm 9, a is Nat : J = 6 } ) \/ { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Nat, b1 is Element of SCM-Data-Loc : K in {7,8} } or x in { [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of SCM-Data-Loc : I in {1,2,3,4,5} } ) by XBOOLE_0:def 3;

then ( x in {[SCM-Halt,{},{}]} \/ { [J,<*a*>,{}] where J is Element of Segm 9, a is Nat : J = 6 } or x in { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Nat, b1 is Element of SCM-Data-Loc : K in {7,8} } or x in { [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of SCM-Data-Loc : I in {1,2,3,4,5} } ) by XBOOLE_0:def 3;

per cases then
( x in {[SCM-Halt,{},{}]} or x in { [J,<*a*>,{}] where J is Element of Segm 9, a is Nat : J = 6 } or x in { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Nat, b1 is Element of SCM-Data-Loc : K in {7,8} } or x in { [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of SCM-Data-Loc : I in {1,2,3,4,5} } )
by XBOOLE_0:def 3;

end;

case
x in { [J,<*a*>,{}] where J is Element of Segm 9, a is Nat : J = 6 }
; :: thesis: InsCode x = 6

then
ex J being Element of Segm 9 ex a being Nat st

( x = [J,<*a*>,{}] & J = 6 ) ;

hence InsCode x = 6 ; :: thesis: verum

end;( x = [J,<*a*>,{}] & J = 6 ) ;

hence InsCode x = 6 ; :: thesis: verum

case
x in { [K,<*a1*>,<*b1*>] where K is Element of Segm 9, a1 is Nat, b1 is Element of SCM-Data-Loc : K in {7,8} }
; :: thesis: ( InsCode x = 7 or InsCode x = 8 )

then consider K being Element of Segm 9, a1 being Nat, b1 being Element of SCM-Data-Loc such that

A1: x = [K,<*a1*>,<*b1*>] and

A2: K in {7,8} ;

InsCode x = K by A1;

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

end;A1: x = [K,<*a1*>,<*b1*>] and

A2: K in {7,8} ;

InsCode x = K by A1;

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

case
x in { [I,{},<*b,c*>] where I is Element of Segm 9, b, c is Element of SCM-Data-Loc : I in {1,2,3,4,5} }
; :: thesis: ( InsCode x = 1 or InsCode x = 2 or InsCode x = 3 or InsCode x = 4 or InsCode x = 5 )

then consider I being Element of Segm 9, b, c being Element of SCM-Data-Loc such that

A3: x = [I,{},<*b,c*>] and

A4: I in {1,2,3,4,5} ;

InsCode x = I by A3;

hence ( InsCode x = 1 or InsCode x = 2 or InsCode x = 3 or InsCode x = 4 or InsCode x = 5 ) by A4, ENUMSET1:def 3; :: thesis: verum

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

A4: I in {1,2,3,4,5} ;

InsCode x = I by A3;

hence ( InsCode x = 1 or InsCode x = 2 or InsCode x = 3 or InsCode x = 4 or InsCode x = 5 ) by A4, ENUMSET1:def 3; :: thesis: verum