const In : set set prop term iIn = In infix iIn 2000 2000 term Subq = \x:set.\y:set.!z:set.z iIn x -> z iIn y const nat_p : set prop const Empty : set axiom nat_0: nat_p Empty const omega : set axiom nat_p_omega: !x:set.nat_p x -> x iIn omega const SNoS_ : set set axiom omega_SNoS_omega: Subq omega (SNoS_ omega) const SNo : set prop const mul_SNo : set set set term * = mul_SNo infix * 2291 2290 axiom mul_SNo_zeroR: !x:set.SNo x -> x * Empty = Empty axiom omega_SNo: !x:set.x iIn omega -> SNo x const ordsucc : set set axiom nat_1: nat_p (ordsucc Empty) const eps_ : set set axiom SNo_eps_SNoS_omega: !x:set.x iIn omega -> eps_ x iIn SNoS_ omega const add_SNo : set set set term + = add_SNo infix + 2281 2280 axiom add_SNo_SNoS_omega: !x:set.x iIn SNoS_ omega -> !y:set.y iIn SNoS_ omega -> x + y iIn SNoS_ omega axiom mul_SNo_oneR: !x:set.SNo x -> x * ordsucc Empty = x axiom mul_SNo_distrL: !x:set.!y:set.!z:set.SNo x -> SNo y -> SNo z -> x * (y + z) = x * y + x * z axiom add_SNo_1_ordsucc: !x:set.x iIn omega -> x + ordsucc Empty = ordsucc x axiom nat_ind: !p:set prop.p Empty -> (!x:set.nat_p x -> p x -> p (ordsucc x)) -> !x:set.nat_p x -> p x var x:set hyp x iIn omega hyp SNo (eps_ x) claim eps_ x iIn SNoS_ omega -> !y:set.nat_p y -> eps_ x * y iIn SNoS_ omega