const CSNo : set prop const CSNo_Re : set set const add_CSNo : set set set const add_SNo : set set set term + = add_SNo infix + 2281 2280 axiom add_CSNo_CRe: !x:set.!y:set.CSNo x -> CSNo y -> CSNo_Re (add_CSNo x y) = CSNo_Re x + CSNo_Re y axiom f_eq_i: !f:set set.!x:set.!y:set.x = y -> f x = f y const SNo : set prop axiom CSNo_ReR: !x:set.CSNo x -> SNo (CSNo_Re x) axiom add_SNo_assoc: !x:set.!y:set.!z:set.SNo x -> SNo y -> SNo z -> x + y + z = (x + y) + z const CSNo_Im : set set axiom add_CSNo_CIm: !x:set.!y:set.CSNo x -> CSNo y -> CSNo_Im (add_CSNo x y) = CSNo_Im x + CSNo_Im y axiom CSNo_ImR: !x:set.CSNo x -> SNo (CSNo_Im x) 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 var y:set var z:set hyp CSNo x hyp CSNo y hyp CSNo z hyp CSNo (add_CSNo y z) hyp CSNo (add_CSNo x y) hyp CSNo (add_CSNo x (add_CSNo y z)) claim CSNo (add_CSNo (add_CSNo x y) z) -> add_CSNo x (add_CSNo y z) = add_CSNo (add_CSNo x y) z