const CSNo : set prop const ordsucc : set set const Empty : set axiom CSNo_1: CSNo (ordsucc Empty) const CSNo_Re : set set const mul_CSNo : 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 minus_SNo : set set term - = minus_SNo const CSNo_Im : set set axiom mul_CSNo_CRe: !x:set.!y:set.CSNo x -> CSNo y -> CSNo_Re (mul_CSNo x y) = CSNo_Re x * CSNo_Re y + - CSNo_Im x * CSNo_Im y const SNo : set prop axiom SNo_1: SNo (ordsucc Empty) axiom SNo_0: SNo Empty axiom mul_SNo_oneL: !x:set.SNo x -> ordsucc Empty * x = x const SNo_pair : set set set axiom CSNo_Re2: !x:set.!y:set.SNo x -> SNo y -> CSNo_Re (SNo_pair x y) = x axiom SNo_pair_0: !x:set.SNo_pair x Empty = x axiom CSNo_Im2: !x:set.!y:set.SNo x -> SNo y -> CSNo_Im (SNo_pair x y) = y axiom mul_SNo_zeroL: !x:set.SNo x -> Empty * x = Empty axiom minus_SNo_0: - Empty = Empty axiom add_SNo_com: !x:set.!y:set.SNo x -> SNo y -> x + y = y + x axiom add_SNo_0L: !x:set.SNo x -> Empty + x = x axiom mul_CSNo_CIm: !x:set.!y:set.CSNo x -> CSNo y -> CSNo_Im (mul_CSNo x y) = CSNo_Re x * CSNo_Im y + CSNo_Im x * CSNo_Re y axiom CSNo_ReIm_split: !x:set.!y:set.CSNo x -> CSNo y -> CSNo_Re x = CSNo_Re y -> CSNo_Im x = CSNo_Im y -> x = y var x:set hyp CSNo x hyp CSNo (mul_CSNo (ordsucc Empty) x) hyp SNo (CSNo_Re x) claim SNo (CSNo_Im x) -> mul_CSNo (ordsucc Empty) x = x