const SNo_pair : set set set const add_SNo : set set set term + = add_SNo infix + 2281 2280 const CSNo_Re : set set const CSNo_Im : set set term add_CSNo = \x:set.\y:set.SNo_pair (CSNo_Re x + CSNo_Re y) (CSNo_Im x + CSNo_Im y) const minus_SNo : set set term - = minus_SNo term minus_CSNo = \x:set.SNo_pair (- CSNo_Re x) - CSNo_Im x const CSNo : set prop const SNo : set prop axiom CSNo_ReR: !x:set.CSNo x -> SNo (CSNo_Re x) axiom CSNo_ImR: !x:set.CSNo x -> SNo (CSNo_Im x) const Empty : set axiom SNo_pair_0: !x:set.SNo_pair x Empty = x axiom add_SNo_minus_SNo_linv: !x:set.SNo x -> - x + x = Empty axiom CSNo_Im2: !x:set.!y:set.SNo x -> SNo y -> CSNo_Im (SNo_pair x y) = y axiom CSNo_Re2: !x:set.!y:set.SNo x -> SNo y -> CSNo_Re (SNo_pair x y) = x var x:set hyp CSNo x hyp SNo - CSNo_Re x claim SNo - CSNo_Im x -> SNo_pair (CSNo_Re (SNo_pair (- CSNo_Re x) - CSNo_Im x) + CSNo_Re x) (CSNo_Im (SNo_pair (- CSNo_Re x) - CSNo_Im x) + CSNo_Im x) = Empty