let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in SCM-Instr or x in [:NAT,(NAT *),(proj2 SCM-Instr):] )
assume A1: x in SCM-Instr ; :: thesis: x in [:NAT,(NAT *),(proj2 SCM-Instr):]
per cases ( x in ({[SCM-Halt,{},{}]} \/ { [J,<*a2*>,{}] where J is Element of Segm 9, a2 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 A1, XBOOLE_0:def 3;
suppose A2: x in ({[SCM-Halt,{},{}]} \/ { [J,<*a2*>,{}] where J is Element of Segm 9, a2 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} } ; :: thesis: x in [:NAT,(NAT *),(proj2 SCM-Instr):]
per cases ( x in {[SCM-Halt,{},{}]} \/ { [J,<*a2*>,{}] where J is Element of Segm 9, a2 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} } ) by A2, XBOOLE_0:def 3;
suppose A3: x in {[SCM-Halt,{},{}]} \/ { [J,<*a2*>,{}] where J is Element of Segm 9, a2 is Nat : J = 6 } ; :: thesis: x in [:NAT,(NAT *),(proj2 SCM-Instr):]
per cases ( x in {[SCM-Halt,{},{}]} or x in { [J,<*a2*>,{}] where J is Element of Segm 9, a2 is Nat : J = 6 } ) by A3, XBOOLE_0:def 3;
suppose x in { [J,<*a2*>,{}] where J is Element of Segm 9, a2 is Nat : J = 6 } ; :: thesis: x in [:NAT,(NAT *),(proj2 SCM-Instr):]
then consider J being Element of Segm 9, a being Nat such that
A5: ( x = [J,<*a*>,{}] & J = 6 ) ;
( J in NAT & <*a*> in NAT * & {} in proj2 SCM-Instr ) by A1, A5, FUNCT_7:18, XTUPLE_0:def 13, ORDINAL1:def 12;
hence x in [:NAT,(NAT *),(proj2 SCM-Instr):] by A5, DOMAIN_1:3; :: thesis: verum
end;
end;
end;
suppose 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: x in [:NAT,(NAT *),(proj2 SCM-Instr):]
then consider K being Element of Segm 9, a1 being Nat, b1 being Element of SCM-Data-Loc such that
A6: ( x = [K,<*a1*>,<*b1*>] & K in {7,8} ) ;
( K in NAT & <*a1*> in NAT * & <*b1*> in proj2 SCM-Instr ) by A1, A6, FUNCT_7:18, XTUPLE_0:def 13, ORDINAL1:def 12;
hence x in [:NAT,(NAT *),(proj2 SCM-Instr):] by A6, DOMAIN_1:3; :: thesis: verum
end;
end;
end;
suppose 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: x in [:NAT,(NAT *),(proj2 SCM-Instr):]
then consider I being Element of Segm 9, b, c being Element of SCM-Data-Loc such that
A7: ( x = [I,{},<*b,c*>] & I in {1,2,3,4,5} ) ;
( I in NAT & {} in NAT * & <*b,c*> in proj2 SCM-Instr ) by A1, A7, FINSEQ_1:49, XTUPLE_0:def 13;
hence x in [:NAT,(NAT *),(proj2 SCM-Instr):] by A7, DOMAIN_1:3; :: thesis: verum
end;
end;