let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in SCM-Instr or x in [:NAT,(),:] )
assume A1: x in SCM-Instr ; :: thesis: x in [:NAT,(),:]
per cases ( x in ( \/ { [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 ;
suppose A2: x in ( \/ { [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,(),:]
per cases ( x in \/ { [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 ;
suppose A3: x in \/ { [J,<*a2*>,{}] where J is Element of Segm 9, a2 is Nat : J = 6 } ; :: thesis: x in [:NAT,(),:]
per cases ( x in or x in { [J,<*a2*>,{}] where J is Element of Segm 9, a2 is Nat : J = 6 } ) by ;
suppose x in { [J,<*a2*>,{}] where J is Element of Segm 9, a2 is Nat : J = 6 } ; :: thesis: x in [:NAT,(),:]
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 ;
hence x in [:NAT,(),:] by ; :: 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,(),:]
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 ;
hence x in [:NAT,(),:] by ; :: 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,(),:]
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 ;
hence x in [:NAT,(),:] by ; :: thesis: verum
end;
end;