let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in SCM-Instr or x in [:NAT ,(NAT * ),(proj2 SCM-Instr ):] )
assume Z: 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 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 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 Z, XBOOLE_0:def 3;
suppose S: x in ({[SCM-Halt ,{} ,{} ]} \/ { [J,<*a2*>,{} ] where J is Element of Segm 9, a2 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} } ; :: 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 Element of NAT : J = 6 } or x 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} } ) by S, XBOOLE_0:def 3;
suppose S: x in {[SCM-Halt ,{} ,{} ]} \/ { [J,<*a2*>,{} ] where J is Element of Segm 9, a2 is Element of 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 Element of NAT : J = 6 } ) by S, XBOOLE_0:def 3;
suppose x in { [J,<*a2*>,{} ] where J is Element of Segm 9, a2 is Element of NAT : J = 6 } ; :: thesis: x in [:NAT ,(NAT * ),(proj2 SCM-Instr ):]
then consider J being Element of Segm 9, a being Element of NAT such that
W: ( x = [J,<*a*>,{} ] & J = 6 ) ;
( J in NAT & <*a*> in NAT * & {} in proj2 SCM-Instr ) by Z, W, RELAT_1:def 5, FUNCT_7:20;
hence x in [:NAT ,(NAT * ),(proj2 SCM-Instr ):] by W, DOMAIN_1:15; :: thesis: verum
end;
end;
end;
suppose x 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} } ; :: thesis: x in [:NAT ,(NAT * ),(proj2 SCM-Instr ):]
then consider K being Element of Segm 9, a1 being Element of NAT , b1 being Element of SCM-Data-Loc such that
W: ( x = [K,<*a1*>,<*b1*>] & K in {7,8} ) ;
( K in NAT & <*a1*> in NAT * & <*b1*> in proj2 SCM-Instr ) by Z, W, RELAT_1:def 5, FUNCT_7:20;
hence x in [:NAT ,(NAT * ),(proj2 SCM-Instr ):] by W, DOMAIN_1:15; :: 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
W: ( x = [I,{} ,<*b,c*>] & I in {1,2,3,4,5} ) ;
( I in NAT & {} in NAT * & <*b,c*> in proj2 SCM-Instr ) by Z, W, RELAT_1:def 5, FINSEQ_1:66;
hence x in [:NAT ,(NAT * ),(proj2 SCM-Instr ):] by W, DOMAIN_1:15; :: thesis: verum
end;
end;