const SNo_rec_ii : (set (set set set) set set) set set set const If_i : prop set set set const SNo : set prop const SNo_rec_i : (set (set set) set) set set const Empty : set term SNo_rec2 = \P:set set (set set set) set.SNo_rec_ii \x:set.\g:set set set.\y:set.If_i (SNo y) (SNo_rec_i (\z:set.\f:set set.P x z \w:set.\u:set.If_i (w = x) (f u) (g w u)) y) Empty const In : set set prop term iIn = In infix iIn 2000 2000 const SNoS_ : set set const SNoLev : set set axiom SNoS_In_neq: !x:set.SNo x -> !y:set.y iIn SNoS_ (SNoLev x) -> y != x axiom SNo_rec2_eq_1: !P:set set (set set set) set.(!x:set.SNo x -> !y:set.SNo y -> !g:set set set.!h:set set set.(!z:set.z iIn SNoS_ (SNoLev x) -> !w:set.SNo w -> g z w = h z w) -> (!z:set.z iIn SNoS_ (SNoLev y) -> g x z = h x z) -> P x y g = P x y h) -> !x:set.SNo x -> !g:set set set.!y:set.SNo y -> SNo_rec_i (\z:set.\f:set set.P x z \w:set.\u:set.If_i (w = x) (f u) (g w u)) y = P x y \z:set.\w:set.If_i (z = x) (SNo_rec_i (\u:set.\f:set set.P x u \v:set.\x2:set.If_i (v = x) (f x2) (g v x2)) w) (g z w) axiom If_i_1: !P:prop.!x:set.!y:set.P -> If_i P x y = x lemma !P:set set (set set set) set.!x:set.!y:set.(!z:set.SNo z -> !w:set.SNo w -> !g:set set set.!h:set set set.(!u:set.u iIn SNoS_ (SNoLev z) -> !v:set.SNo v -> g u v = h u v) -> (!u:set.u iIn SNoS_ (SNoLev w) -> g z u = h z u) -> P z w g = P z w h) -> SNo x -> SNo y -> (!z:set.SNo z -> !g:set set set.!h:set set set.(!w:set.w iIn SNoS_ (SNoLev z) -> g w = h w) -> (\w:set.If_i (SNo w) (SNo_rec_i (\u:set.\f:set set.P z u \v:set.\x2:set.If_i (v = z) (f x2) (g v x2)) w) Empty) = \w:set.If_i (SNo w) (SNo_rec_i (\u:set.\f:set set.P z u \v:set.\x2:set.If_i (v = z) (f x2) (h v x2)) w) Empty) -> If_i (SNo y) (SNo_rec_i (\z:set.\f:set set.P x z \w:set.\u:set.If_i (w = x) (f u) (SNo_rec_ii (\v:set.\g:set set set.\x2:set.If_i (SNo x2) (SNo_rec_i (\y2:set.\f2:set set.P v y2 \z2:set.\w2:set.If_i (z2 = v) (f2 w2) (g z2 w2)) x2) Empty) w u)) y) Empty = P x y (SNo_rec2 P) -> SNo_rec_ii (\z:set.\g:set set set.\w:set.If_i (SNo w) (SNo_rec_i (\u:set.\f:set set.P z u \v:set.\x2:set.If_i (v = z) (f x2) (g v x2)) w) Empty) x y = P x y (SNo_rec2 P) lemma !P:set set (set set set) set.!x:set.!y:set.(!z:set.SNo z -> !w:set.SNo w -> !g:set set set.!h:set set set.(!u:set.u iIn SNoS_ (SNoLev z) -> !v:set.SNo v -> g u v = h u v) -> (!u:set.u iIn SNoS_ (SNoLev w) -> g z u = h z u) -> P z w g = P z w h) -> SNo x -> SNo y -> (!z:set.SNo z -> !g:set set set.!h:set set set.(!w:set.w iIn SNoS_ (SNoLev z) -> g w = h w) -> (\w:set.If_i (SNo w) (SNo_rec_i (\u:set.\f:set set.P z u \v:set.\x2:set.If_i (v = z) (f x2) (g v x2)) w) Empty) = \w:set.If_i (SNo w) (SNo_rec_i (\u:set.\f:set set.P z u \v:set.\x2:set.If_i (v = z) (f x2) (h v x2)) w) Empty) -> (!z:set.z iIn SNoS_ (SNoLev x) -> !w:set.SNo w -> If_i (z = x) (SNo_rec_i (\u:set.\f:set set.P x u \v:set.\x2:set.If_i (v = x) (f x2) (SNo_rec_ii (\y2:set.\g:set set set.\z2:set.If_i (SNo z2) (SNo_rec_i (\w2:set.\f2:set set.P y2 w2 \u2:set.\v2:set.If_i (u2 = y2) (f2 v2) (g u2 v2)) z2) Empty) v x2)) w) (SNo_rec_ii (\u:set.\g:set set set.\v:set.If_i (SNo v) (SNo_rec_i (\x2:set.\f:set set.P u x2 \y2:set.\z2:set.If_i (y2 = u) (f z2) (g y2 z2)) v) Empty) z w) = SNo_rec_ii (\u:set.\g:set set set.\v:set.If_i (SNo v) (SNo_rec_i (\x2:set.\f:set set.P u x2 \y2:set.\z2:set.If_i (y2 = u) (f z2) (g y2 z2)) v) Empty) z w) -> P x y (\z:set.\w:set.If_i (z = x) (SNo_rec_i (\u:set.\f:set set.P x u \v:set.\x2:set.If_i (v = x) (f x2) (SNo_rec_ii (\y2:set.\g:set set set.\z2:set.If_i (SNo z2) (SNo_rec_i (\w2:set.\f2:set set.P y2 w2 \u2:set.\v2:set.If_i (u2 = y2) (f2 v2) (g u2 v2)) z2) Empty) v x2)) w) (SNo_rec_ii (\u:set.\g:set set set.\v:set.If_i (SNo v) (SNo_rec_i (\x2:set.\f:set set.P u x2 \y2:set.\z2:set.If_i (y2 = u) (f z2) (g y2 z2)) v) Empty) z w)) = P x y (SNo_rec_ii \z:set.\g:set set set.\w:set.If_i (SNo w) (SNo_rec_i (\u:set.\f:set set.P z u \v:set.\x2:set.If_i (v = z) (f x2) (g v x2)) w) Empty) lemma !P:set set (set set set) set.!x:set.!y:set.!z:set.SNo x -> y iIn SNoS_ (SNoLev x) -> y != x -> If_i (y = x) (SNo_rec_i (\w:set.\f:set set.P x w \u:set.\v:set.If_i (u = x) (f v) (SNo_rec_ii (\x2:set.\g:set set set.\y2:set.If_i (SNo y2) (SNo_rec_i (\z2:set.\f2:set set.P x2 z2 \w2:set.\u2:set.If_i (w2 = x2) (f2 u2) (g w2 u2)) y2) Empty) u v)) z) (SNo_rec_ii (\w:set.\g:set set set.\u:set.If_i (SNo u) (SNo_rec_i (\v:set.\f:set set.P w v \x2:set.\y2:set.If_i (x2 = w) (f y2) (g x2 y2)) u) Empty) y z) = SNo_rec_ii (\w:set.\g:set set set.\u:set.If_i (SNo u) (SNo_rec_i (\v:set.\f:set set.P w v \x2:set.\y2:set.If_i (x2 = w) (f y2) (g x2 y2)) u) Empty) y z var P:set set (set set set) set var x:set var y:set hyp !z:set.SNo z -> !w:set.SNo w -> !g:set set set.!h:set set set.(!u:set.u iIn SNoS_ (SNoLev z) -> !v:set.SNo v -> g u v = h u v) -> (!u:set.u iIn SNoS_ (SNoLev w) -> g z u = h z u) -> P z w g = P z w h hyp SNo x hyp SNo y claim (!z:set.SNo z -> !g:set set set.!h:set set set.(!w:set.w iIn SNoS_ (SNoLev z) -> g w = h w) -> (\w:set.If_i (SNo w) (SNo_rec_i (\u:set.\f:set set.P z u \v:set.\x2:set.If_i (v = z) (f x2) (g v x2)) w) Empty) = \w:set.If_i (SNo w) (SNo_rec_i (\u:set.\f:set set.P z u \v:set.\x2:set.If_i (v = z) (f x2) (h v x2)) w) Empty) -> SNo_rec_ii (\z:set.\g:set set set.\w:set.If_i (SNo w) (SNo_rec_i (\u:set.\f:set set.P z u \v:set.\x2:set.If_i (v = z) (f x2) (g v x2)) w) Empty) x y = P x y (SNo_rec2 P)