const bij : set set (set set) prop term equip = \x:set.\y:set.?f:set set.bij x y f const In : set set prop term iIn = In infix iIn 2000 2000 term PNoEq_ = \x:set.\p:set prop.\q:set prop.!y:set.y iIn x -> (p y <-> q y) term nIn = \x:set.\y:set.~ x iIn y term SNoEq_ = \x:set.\y:set.\z:set.PNoEq_ x (\w:set.w iIn y) \w:set.w iIn z const nat_p : set prop const omega : set axiom nat_p_omega: !x:set.nat_p x -> x iIn omega const ordinal : set prop axiom omega_ordinal: ordinal omega const SNo : set prop const SNo_extend1 : set set axiom SNo_extend1_SNo: !x:set.SNo x -> SNo (SNo_extend1 x) 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 Sep : set (set prop) set axiom SepE: !x:set.!p:set prop.!y:set.y iIn Sep x p -> y iIn x & p y const SNo_extend0 : set set axiom SNo_extend0_SNo: !x:set.SNo x -> SNo (SNo_extend0 x) const add_SNo : set set set term + = add_SNo infix + 2281 2280 const minus_SNo : set set term - = minus_SNo axiom add_SNo_omega_In_cases: !x:set.!y:set.y iIn omega -> !z:set.nat_p z -> x iIn y + z -> x iIn y | x + - y iIn z const binintersect : set set set const SNoElts_ : set set const ordsucc : set set lemma !x:set.!f:set set.!f2:set set.!y:set.!z:set.nat_p x -> (!w:set.x iIn w -> f2 w = f (binintersect w (SNoElts_ x))) -> f z = y -> SNoLev z = x -> SNo z -> SNo (SNo_extend1 z) -> ?w:set.w iIn Sep (SNoS_ omega) (\u:set.SNoLev u = ordsucc x) & f2 w = y const exp_SNo_nat : set set set const Empty : set lemma !x:set.!f:set set.!f2:set set.!y:set.!z:set.nat_p x -> SNo (exp_SNo_nat (ordsucc (ordsucc Empty)) x) -> (!w:set.nIn x w -> f2 w = exp_SNo_nat (ordsucc (ordsucc Empty)) x + f (binintersect w (SNoElts_ x))) -> SNo y -> f z = y + - exp_SNo_nat (ordsucc (ordsucc Empty)) x -> SNoLev z = x -> SNo z -> SNo (SNo_extend0 z) -> ?w:set.w iIn Sep (SNoS_ omega) (\u:set.SNoLev u = ordsucc x) & f2 w = y var x:set var f:set set var f2:set set var y:set hyp nat_p x hyp nat_p (exp_SNo_nat (ordsucc (ordsucc Empty)) x) hyp SNo (exp_SNo_nat (ordsucc (ordsucc Empty)) x) hyp !z:set.z iIn exp_SNo_nat (ordsucc (ordsucc Empty)) x -> ?w:set.w iIn Sep (SNoS_ omega) (\u:set.SNoLev u = x) & f w = z hyp !z:set.x iIn z -> f2 z = f (binintersect z (SNoElts_ x)) hyp !z:set.nIn x z -> f2 z = exp_SNo_nat (ordsucc (ordsucc Empty)) x + f (binintersect z (SNoElts_ x)) hyp y iIn exp_SNo_nat (ordsucc (ordsucc Empty)) x + exp_SNo_nat (ordsucc (ordsucc Empty)) x hyp nat_p y claim SNo y -> ?z:set.z iIn Sep (SNoS_ omega) (\w:set.SNoLev w = ordsucc x) & f2 z = y