const In : set set prop term iIn = In infix iIn 2000 2000 term nIn = \x:set.\y:set.~ x iIn y term Subq = \x:set.\y:set.!z:set.z iIn x -> z iIn y const nat_p : set prop const omega : set axiom nat_p_omega: !x:set.nat_p x -> x iIn omega const ordsucc : set set axiom omega_ordsucc: !x:set.x iIn omega -> ordsucc x iIn omega const SNoS_ : set set axiom omega_SNoS_omega: Subq omega (SNoS_ omega) const minus_SNo : set set term - = minus_SNo axiom minus_SNo_SNoS_omega: !x:set.x iIn SNoS_ omega -> - x iIn SNoS_ omega const SNo : set prop const Empty : set axiom SNo_1: SNo (ordsucc Empty) const add_SNo : set set set term + = add_SNo infix + 2281 2280 axiom add_SNo_minus_R2': !x:set.!y:set.SNo x -> SNo y -> (x + - y) + y = x axiom minus_add_SNo_distr: !x:set.!y:set.SNo x -> SNo y -> - (x + y) = - x + - y axiom add_SNo_1_ordsucc: !x:set.x iIn omega -> x + ordsucc Empty = ordsucc x axiom FalseE: ~ False const SNoLt : set set prop term < = SNoLt infix < 2020 2020 axiom SNoLt_trichotomy_or_impred: !x:set.!y:set.SNo x -> SNo y -> !P:prop.(x < y -> P) -> (x = y -> P) -> (y < x -> P) -> P var x:set var y:set hyp SNo x hyp nIn x (SNoS_ omega) hyp nat_p y hyp - y < x -> x < y -> ?z:set.z iIn SNoS_ omega & (z < x & x < z + ordsucc Empty) hyp - ordsucc y < x hyp x < ordsucc y hyp SNo y hyp SNo - y claim y iIn SNoS_ omega -> ?z:set.z iIn SNoS_ omega & (z < x & x < z + ordsucc Empty)