const In : set set prop term iIn = In infix iIn 2000 2000 term nIn = \x:set.\y:set.~ x iIn y const Pi : set (set set) set term setexp = \x:set.\y:set.Pi y \z:set.x const ordinal : set prop const omega : set axiom omega_ordinal: ordinal omega const SNo : set prop const eps_ : set set axiom SNo_eps_: !x:set.x iIn omega -> SNo (eps_ x) const add_SNo : set set set term + = add_SNo infix + 2281 2280 axiom SNo_add_SNo: !x:set.!y:set.SNo x -> SNo y -> SNo (x + y) const ordsucc : set set axiom ordsuccI2: !x:set.x iIn ordsucc x const SNoLt : set set prop term < = SNoLt infix < 2020 2020 axiom SNo_eps_decr: !x:set.x iIn omega -> !y:set.y iIn x -> eps_ x < eps_ y axiom add_SNo_Lt2: !x:set.!y:set.!z:set.SNo x -> SNo y -> SNo z -> y < z -> (x + y) < x + z const SNoLe : set set prop term <= = SNoLe infix <= 2020 2020 axiom add_SNo_Le2: !x:set.!y:set.!z:set.SNo x -> SNo y -> SNo z -> y <= z -> (x + y) <= x + z axiom add_SNo_com: !x:set.!y:set.SNo x -> SNo y -> x + y = y + x const minus_SNo : set set term - = minus_SNo axiom add_SNo_minus_L2': !x:set.!y:set.SNo x -> SNo y -> x + - x + y = y axiom SNoLtLe_tra: !x:set.!y:set.!z:set.SNo x -> SNo y -> SNo z -> x < y -> y <= z -> x < z axiom add_SNo_Le1: !x:set.!y:set.!z:set.SNo x -> SNo y -> SNo z -> x <= z -> (x + y) <= z + y axiom add_SNo_eps_Lt': !x:set.!y:set.SNo x -> SNo y -> !z:set.z iIn omega -> x < y -> x < y + eps_ z axiom add_SNo_com_3b_1_2: !x:set.!y:set.!z:set.SNo x -> SNo y -> SNo z -> (x + y) + z = (x + z) + y axiom omega_ordsucc: !x:set.x iIn omega -> ordsucc x iIn omega axiom add_SNo_eps_Lt: !x:set.SNo x -> !y:set.y iIn omega -> x < x + eps_ y const SNoS_ : set set const SNoLev : set set const SNo_ : set set prop axiom SNoS_E2: !x:set.ordinal x -> !y:set.y iIn SNoS_ x -> !P:prop.(SNoLev y iIn x -> ordinal (SNoLev y) -> SNo y -> SNo_ (SNoLev y) y -> P) -> P const nat_primrec : set (set set set) set set const Eps_i : (set prop) set const Empty : set var x:set var y:set var z:set var w:set hyp SNo x hyp nat_primrec (Eps_i \u:set.u iIn SNoS_ omega & u < x & x < u + eps_ Empty) (\u:set.\v:set.Eps_i \x2:set.x2 iIn SNoS_ omega & x2 < x & x < x2 + eps_ (ordsucc u) & v < x2) y iIn SNoS_ omega hyp SNo (nat_primrec (Eps_i \u:set.u iIn SNoS_ omega & u < x & x < u + eps_ Empty) (\u:set.\v:set.Eps_i \x2:set.x2 iIn SNoS_ omega & x2 < x & x < x2 + eps_ (ordsucc u) & v < x2) y) hyp x < z + eps_ (ordsucc y) hyp SNo z hyp z <= nat_primrec (Eps_i \u:set.u iIn SNoS_ omega & u < x & x < u + eps_ Empty) (\u:set.\v:set.Eps_i \x2:set.x2 iIn SNoS_ omega & x2 < x & x < x2 + eps_ (ordsucc u) & v < x2) y hyp SNo - nat_primrec (Eps_i \u:set.u iIn SNoS_ omega & u < x & x < u + eps_ Empty) (\u:set.\v:set.Eps_i \x2:set.x2 iIn SNoS_ omega & x2 < x & x < x2 + eps_ (ordsucc u) & v < x2) y hyp SNo (x + - nat_primrec (Eps_i \u:set.u iIn SNoS_ omega & u < x & x < u + eps_ Empty) (\u:set.\v:set.Eps_i \x2:set.x2 iIn SNoS_ omega & x2 < x & x < x2 + eps_ (ordsucc u) & v < x2) y) hyp SNo (eps_ (ordsucc y)) hyp w iIn omega hyp eps_ w <= x + - nat_primrec (Eps_i \u:set.u iIn SNoS_ omega & u < x & x < u + eps_ Empty) (\u:set.\v:set.Eps_i \x2:set.x2 iIn SNoS_ omega & x2 < x & x < x2 + eps_ (ordsucc u) & v < x2) y hyp ordsucc w iIn omega hyp SNo (eps_ (ordsucc w)) claim nat_primrec (Eps_i \u:set.u iIn SNoS_ omega & u < x & x < u + eps_ Empty) (\u:set.\v:set.Eps_i \x2:set.x2 iIn SNoS_ omega & x2 < x & x < x2 + eps_ (ordsucc u) & v < x2) y + eps_ (ordsucc w) iIn SNoS_ omega -> nat_primrec (Eps_i \u:set.u iIn SNoS_ omega & u < x & x < u + eps_ Empty) (\u:set.\v:set.Eps_i \x2:set.x2 iIn SNoS_ omega & x2 < x & x < x2 + eps_ (ordsucc u) & v < x2) y + eps_ (ordsucc w) iIn SNoS_ omega & (nat_primrec (Eps_i \u:set.u iIn SNoS_ omega & u < x & x < u + eps_ Empty) (\u:set.\v:set.Eps_i \x2:set.x2 iIn SNoS_ omega & x2 < x & x < x2 + eps_ (ordsucc u) & v < x2) y + eps_ (ordsucc w)) < x & x < (nat_primrec (Eps_i \u:set.u iIn SNoS_ omega & u < x & x < u + eps_ Empty) (\u:set.\v:set.Eps_i \x2:set.x2 iIn SNoS_ omega & x2 < x & x < x2 + eps_ (ordsucc u) & v < x2) y + eps_ (ordsucc w)) + eps_ (ordsucc y) & nat_primrec (Eps_i \u:set.u iIn SNoS_ omega & u < x & x < u + eps_ Empty) (\u:set.\v:set.Eps_i \x2:set.x2 iIn SNoS_ omega & x2 < x & x < x2 + eps_ (ordsucc u) & v < x2) y < nat_primrec (Eps_i \u:set.u iIn SNoS_ omega & u < x & x < u + eps_ Empty) (\u:set.\v:set.Eps_i \x2:set.x2 iIn SNoS_ omega & x2 < x & x < x2 + eps_ (ordsucc u) & v < x2) y + eps_ (ordsucc w)