now assume
2
in SCM-Instr
;
:: thesis: contradictionthen
( 2
in ({[SCM-Halt ,{} ]} \/ { [J,<*a*>] where J is Element of Segm 9, a is Element of NAT : J = 6 } ) \/ { [K,<*a1,b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of SCM-Data-Loc : K in {7,8} } or 2
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
( 2
in {[SCM-Halt ,{} ]} \/ { [J,<*a*>] where J is Element of Segm 9, a is Element of NAT : J = 6 } or 2
in { [K,<*a1,b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of SCM-Data-Loc : K in {7,8} } or 2
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
( 2
in {[SCM-Halt ,{} ]} or 2
in { [J,<*a*>] where J is Element of Segm 9, a is Element of NAT : J = 6 } or 2
in { [K,<*a1,b1*>] where K is Element of Segm 9, a1 is Element of NAT , b1 is Element of SCM-Data-Loc : K in {7,8} } or 2
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
( 2
= [SCM-Halt ,{} ] or ex
J being
Element of
Segm 9 ex
a being
Element of
NAT st
( 2
= [J,<*a*>] &
J = 6 ) or ex
K being
Element of
Segm 9 ex
a1 being
Element of
NAT ex
b1 being
Element of
SCM-Data-Loc st
( 2
= [K,<*a1,b1*>] &
K in {7,8} ) or ex
I being
Element of
Segm 9 ex
b,
c being
Element of
SCM-Data-Loc st
( 2
= [I,<*b,c*>] &
I in {1,2,3,4,5} ) )
by TARSKI:def 1;
hence
contradiction
;
:: thesis: verum end;
hence
( SCM-Instr <> INT & NAT <> SCM-Instr )
by INT_1:def 2; :: thesis: verum