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 term TransSet = \x:set.!y:set.y iIn x -> Subq y x term ordinal = \x:set.TransSet x & !y:set.y iIn x -> TransSet y const In_rec_iii : (set (set set set set) set set set) set set set set const If_iii : prop (set set set) (set set set) set set set const If_ii : prop (set set) (set set) set set const SNoS_ : set set const ordsucc : set set const SNoLev : set set const Descr_ii : ((set set) prop) set set term SNo_rec_ii = \P:set (set set set) set set.\x:set.In_rec_iii (\y:set.\Q:set set set set.If_iii (ordinal y) (\z:set.If_ii (z iIn SNoS_ (ordsucc y)) (P z \w:set.Q (SNoLev w) w) (Descr_ii \f:set set.True)) \z:set.Descr_ii \f:set set.True) (SNoLev x) x term nIn = \x:set.\y:set.~ x iIn y axiom ordinal_ordsucc: !x:set.ordinal x -> ordinal (ordsucc x) axiom If_ii_1: !P:prop.!f:set set.!f2:set set.P -> If_ii P f f2 = f axiom If_ii_0: !P:prop.!f:set set.!f2:set set.~ P -> If_ii P f f2 = f2 axiom xm: !P:prop.P | ~ P axiom func_ext: !g:set set set.!h:set set set.(!x:set.g x = h x) -> g = h axiom If_iii_1: !P:prop.!g:set set set.!h:set set set.P -> If_iii P g h = g axiom If_iii_0: !P:prop.!g:set set set.!h:set set set.~ P -> If_iii P g h = h const SNo : set prop lemma !P:set (set set set) set set.!x:set.(!y:set.SNo y -> !g:set set set.!h:set set set.(!z:set.z iIn SNoS_ (SNoLev y) -> g z = h z) -> P y g = P y h) -> SNo x -> (!y:set.!Q:set set set set.!R:set set set set.(!z:set.z iIn y -> Q z = R z) -> If_iii (ordinal y) (\z:set.If_ii (z iIn SNoS_ (ordsucc y)) (P z \w:set.Q (SNoLev w) w) (Descr_ii \f:set set.True)) (\z:set.Descr_ii \f:set set.True) = If_iii (ordinal y) (\z:set.If_ii (z iIn SNoS_ (ordsucc y)) (P z \w:set.R (SNoLev w) w) (Descr_ii \f:set set.True)) \z:set.Descr_ii \f:set set.True) -> In_rec_iii (\y:set.\Q:set set set set.If_iii (ordinal y) (\z:set.If_ii (z iIn SNoS_ (ordsucc y)) (P z \w:set.Q (SNoLev w) w) (Descr_ii \f:set set.True)) \z:set.Descr_ii \f:set set.True) (SNoLev x) x = P x \y:set.In_rec_iii (\z:set.\Q:set set set set.If_iii (ordinal z) (\w:set.If_ii (w iIn SNoS_ (ordsucc z)) (P w \u:set.Q (SNoLev u) u) (Descr_ii \f:set set.True)) \w:set.Descr_ii \f:set set.True) (SNoLev y) y lemma !P:set (set set set) set set.!x:set.!Q:set set set set.!R:set set set set.!y:set.(!z:set.SNo z -> !g:set set set.!h:set set set.(!w:set.w iIn SNoS_ (SNoLev z) -> g w = h w) -> P z g = P z h) -> (!z:set.z iIn x -> Q z = R z) -> ordinal x -> y iIn SNoS_ (ordsucc x) -> ordinal (ordsucc x) -> P y (\z:set.Q (SNoLev z) z) = P y \z:set.R (SNoLev z) z claim !P:set (set set set) set set.(!x:set.SNo x -> !g:set set set.!h:set set set.(!y:set.y iIn SNoS_ (SNoLev x) -> g y = h y) -> P x g = P x h) -> !x:set.SNo x -> SNo_rec_ii P x = P x (SNo_rec_ii P)