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 omega : set const ordsucc : set set axiom omega_ordsucc: !x:set.x iIn omega -> ordsucc x iIn omega const SNo : set prop const Empty : set axiom SNo_0: SNo Empty const add_SNo : set set set term + = add_SNo infix + 2281 2280 const minus_SNo : set set term - = minus_SNo axiom add_SNo_minus_R2': !x:set.!y:set.SNo x -> SNo y -> (x + - y) + y = x axiom add_SNo_0L: !x:set.SNo x -> Empty + x = x const SNoLt : set set prop term < = SNoLt infix < 2020 2020 axiom add_SNo_Lt1_cancel: !x:set.!y:set.!z:set.SNo x -> SNo y -> SNo z -> (x + y) < z + y -> x < z axiom SNoLt_irref: !x:set.~ x < x axiom FalseE: ~ False axiom xm: !P:prop.P | ~ P const nat_primrec : set (set set set) set set const Eps_i : (set prop) set const SNoS_ : set set const eps_ : set set const SNoLe : set set prop term <= = SNoLe infix <= 2020 2020 lemma !x:set.!y:set.!z:set.!w:set.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 iIn SNoS_ omega -> 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) -> x < z + eps_ (ordsucc y) -> SNo z -> 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 -> 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 -> 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) -> SNo (eps_ (ordsucc y)) -> w iIn omega -> 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 -> ordsucc w iIn 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) const abs_SNo : set set lemma !x:set.!y:set.SNo x -> (!z:set.z iIn SNoS_ omega -> (!w:set.w iIn omega -> abs_SNo (z + - x) < eps_ w) -> z = x) -> nat_primrec (Eps_i \z:set.z iIn SNoS_ omega & z < x & x < z + eps_ Empty) (\z:set.\w:set.Eps_i \u:set.u iIn SNoS_ omega & u < x & x < u + eps_ (ordsucc z) & w < u) y iIn SNoS_ omega -> nat_primrec (Eps_i \z:set.z iIn SNoS_ omega & z < x & x < z + eps_ Empty) (\z:set.\w:set.Eps_i \u:set.u iIn SNoS_ omega & u < x & x < u + eps_ (ordsucc z) & w < u) y < x -> SNo (nat_primrec (Eps_i \z:set.z iIn SNoS_ omega & z < x & x < z + eps_ Empty) (\z:set.\w:set.Eps_i \u:set.u iIn SNoS_ omega & u < x & x < u + eps_ (ordsucc z) & w < u) y) -> SNo (x + - nat_primrec (Eps_i \z:set.z iIn SNoS_ omega & z < x & x < z + eps_ Empty) (\z:set.\w:set.Eps_i \u:set.u iIn SNoS_ omega & u < x & x < u + eps_ (ordsucc z) & w < u) y) -> ~ (?z:set.z iIn omega & eps_ z <= x + - nat_primrec (Eps_i \w:set.w iIn SNoS_ omega & w < x & x < w + eps_ Empty) (\w:set.\u:set.Eps_i \v:set.v iIn SNoS_ omega & v < x & x < v + eps_ (ordsucc w) & u < v) y) -> Empty < x + - nat_primrec (Eps_i \z:set.z iIn SNoS_ omega & z < x & x < z + eps_ Empty) (\z:set.\w:set.Eps_i \u:set.u iIn SNoS_ omega & u < x & x < u + eps_ (ordsucc z) & w < u) y -> x < x const nat_p : set prop var x:set var y:set var z:set hyp SNo x hyp !w:set.w iIn SNoS_ omega -> (!u:set.u iIn omega -> abs_SNo (w + - x) < eps_ u) -> w = x hyp nat_p y hyp nat_primrec (Eps_i \w:set.w iIn SNoS_ omega & w < x & x < w + eps_ Empty) (\w:set.\u:set.Eps_i \v:set.v iIn SNoS_ omega & v < x & x < v + eps_ (ordsucc w) & u < v) y iIn SNoS_ omega hyp nat_primrec (Eps_i \w:set.w iIn SNoS_ omega & w < x & x < w + eps_ Empty) (\w:set.\u:set.Eps_i \v:set.v iIn SNoS_ omega & v < x & x < v + eps_ (ordsucc w) & u < v) y < x hyp SNo (nat_primrec (Eps_i \w:set.w iIn SNoS_ omega & w < x & x < w + eps_ Empty) (\w:set.\u:set.Eps_i \v:set.v iIn SNoS_ omega & v < x & x < v + eps_ (ordsucc w) & u < v) y) hyp x < z + eps_ (ordsucc y) hyp SNo z hyp z <= nat_primrec (Eps_i \w:set.w iIn SNoS_ omega & w < x & x < w + eps_ Empty) (\w:set.\u:set.Eps_i \v:set.v iIn SNoS_ omega & v < x & x < v + eps_ (ordsucc w) & u < v) y hyp SNo - nat_primrec (Eps_i \w:set.w iIn SNoS_ omega & w < x & x < w + eps_ Empty) (\w:set.\u:set.Eps_i \v:set.v iIn SNoS_ omega & v < x & x < v + eps_ (ordsucc w) & u < v) y hyp SNo (x + - nat_primrec (Eps_i \w:set.w iIn SNoS_ omega & w < x & x < w + eps_ Empty) (\w:set.\u:set.Eps_i \v:set.v iIn SNoS_ omega & v < x & x < v + eps_ (ordsucc w) & u < v) y) claim SNo (eps_ (ordsucc y)) -> ?w:set.w iIn SNoS_ omega & w < x & x < 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 < w