const SNo_pair : set set set const add_SNo : set set set term + = add_SNo infix + 2281 2280 const mul_SNo : set set set term * = mul_SNo infix * 2291 2290 const CSNo_Re : set set const minus_SNo : set set term - = minus_SNo const CSNo_Im : set set term mul_CSNo = \x:set.\y:set.SNo_pair (CSNo_Re x * CSNo_Re y + - CSNo_Im x * CSNo_Im y) (CSNo_Re x * CSNo_Im y + CSNo_Im x * CSNo_Re y) const SNo : set prop axiom SNo_Re: !x:set.SNo x -> CSNo_Re x = x const Empty : set axiom SNo_pair_0: !x:set.SNo_pair x Empty = x const CSNo : set prop axiom SNo_CSNo: !x:set.SNo x -> CSNo x axiom CSNo_ImR: !x:set.CSNo x -> SNo (CSNo_Im x) axiom CSNo_ReR: !x:set.CSNo x -> SNo (CSNo_Re x) axiom SNo_mul_SNo: !x:set.!y:set.SNo x -> SNo y -> SNo (x * y) axiom add_SNo_0R: !x:set.SNo x -> x + Empty = x axiom minus_SNo_0: - Empty = Empty axiom mul_SNo_zeroL: !x:set.SNo x -> Empty * x = Empty axiom SNo_Im: !x:set.SNo x -> CSNo_Im x = Empty axiom SNo_0: SNo Empty axiom mul_SNo_zeroR: !x:set.SNo x -> x * Empty = Empty claim !x:set.!y:set.SNo x -> SNo y -> x * y = mul_CSNo x y