const SNo_rec2 : (set set (set set set) set) set set set const SNoCut : set set set const binunion : set set set const Repl : set (set set) set const setprod : set set set const SNoL : set set const add_SNo : set set set term + = add_SNo infix + 2281 2280 const ap : set set set const Empty : set const ordsucc : set set const minus_SNo : set set term - = minus_SNo const SNoR : set set term mul_SNo = SNo_rec2 \x:set.\y:set.\g:set set set.SNoCut (binunion (Repl (setprod (SNoL x) (SNoL y)) \z:set.g (ap z Empty) y + g x (ap z (ordsucc Empty)) + - g (ap z Empty) (ap z (ordsucc Empty))) (Repl (setprod (SNoR x) (SNoR y)) \z:set.g (ap z Empty) y + g x (ap z (ordsucc Empty)) + - g (ap z Empty) (ap z (ordsucc Empty)))) (binunion (Repl (setprod (SNoL x) (SNoR y)) \z:set.g (ap z Empty) y + g x (ap z (ordsucc Empty)) + - g (ap z Empty) (ap z (ordsucc Empty))) (Repl (setprod (SNoR x) (SNoL y)) \z:set.g (ap z Empty) y + g x (ap z (ordsucc Empty)) + - g (ap z Empty) (ap z (ordsucc Empty)))) term * = mul_SNo infix * 2291 2290 const SNo : set prop const In : set set prop term iIn = In infix iIn 2000 2000 const SNoS_ : set set const SNoLev : set set axiom SNo_rec2_eq: !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 -> !y:set.SNo y -> SNo_rec2 P x y = P x y (SNo_rec2 P) claim (!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) -> SNoCut (binunion (Repl (setprod (SNoL x) (SNoL y)) \z:set.g (ap z Empty) y + g x (ap z (ordsucc Empty)) + - g (ap z Empty) (ap z (ordsucc Empty))) (Repl (setprod (SNoR x) (SNoR y)) \z:set.g (ap z Empty) y + g x (ap z (ordsucc Empty)) + - g (ap z Empty) (ap z (ordsucc Empty)))) (binunion (Repl (setprod (SNoL x) (SNoR y)) \z:set.g (ap z Empty) y + g x (ap z (ordsucc Empty)) + - g (ap z Empty) (ap z (ordsucc Empty))) (Repl (setprod (SNoR x) (SNoL y)) \z:set.g (ap z Empty) y + g x (ap z (ordsucc Empty)) + - g (ap z Empty) (ap z (ordsucc Empty)))) = SNoCut (binunion (Repl (setprod (SNoL x) (SNoL y)) \z:set.h (ap z Empty) y + h x (ap z (ordsucc Empty)) + - h (ap z Empty) (ap z (ordsucc Empty))) (Repl (setprod (SNoR x) (SNoR y)) \z:set.h (ap z Empty) y + h x (ap z (ordsucc Empty)) + - h (ap z Empty) (ap z (ordsucc Empty)))) (binunion (Repl (setprod (SNoL x) (SNoR y)) \z:set.h (ap z Empty) y + h x (ap z (ordsucc Empty)) + - h (ap z Empty) (ap z (ordsucc Empty))) (Repl (setprod (SNoR x) (SNoL y)) \z:set.h (ap z Empty) y + h x (ap z (ordsucc Empty)) + - h (ap z Empty) (ap z (ordsucc Empty))))) -> !x:set.SNo x -> !y:set.SNo y -> SNo_rec2 (\z:set.\w:set.\g:set set set.SNoCut (binunion (Repl (setprod (SNoL z) (SNoL w)) \u:set.g (ap u Empty) w + g z (ap u (ordsucc Empty)) + - g (ap u Empty) (ap u (ordsucc Empty))) (Repl (setprod (SNoR z) (SNoR w)) \u:set.g (ap u Empty) w + g z (ap u (ordsucc Empty)) + - g (ap u Empty) (ap u (ordsucc Empty)))) (binunion (Repl (setprod (SNoL z) (SNoR w)) \u:set.g (ap u Empty) w + g z (ap u (ordsucc Empty)) + - g (ap u Empty) (ap u (ordsucc Empty))) (Repl (setprod (SNoR z) (SNoL w)) \u:set.g (ap u Empty) w + g z (ap u (ordsucc Empty)) + - g (ap u Empty) (ap u (ordsucc Empty))))) x y = SNoCut (binunion (Repl (setprod (SNoL x) (SNoL y)) \z:set.SNo_rec2 (\w:set.\u:set.\g:set set set.SNoCut (binunion (Repl (setprod (SNoL w) (SNoL u)) \v:set.g (ap v Empty) u + g w (ap v (ordsucc Empty)) + - g (ap v Empty) (ap v (ordsucc Empty))) (Repl (setprod (SNoR w) (SNoR u)) \v:set.g (ap v Empty) u + g w (ap v (ordsucc Empty)) + - g (ap v Empty) (ap v (ordsucc Empty)))) (binunion (Repl (setprod (SNoL w) (SNoR u)) \v:set.g (ap v Empty) u + g w (ap v (ordsucc Empty)) + - g (ap v Empty) (ap v (ordsucc Empty))) (Repl (setprod (SNoR w) (SNoL u)) \v:set.g (ap v Empty) u + g w (ap v (ordsucc Empty)) + - g (ap v Empty) (ap v (ordsucc Empty))))) (ap z Empty) y + SNo_rec2 (\w:set.\u:set.\g:set set set.SNoCut (binunion (Repl (setprod (SNoL w) (SNoL u)) \v:set.g (ap v Empty) u + g w (ap v (ordsucc Empty)) + - g (ap v Empty) (ap v (ordsucc Empty))) (Repl (setprod (SNoR w) (SNoR u)) \v:set.g (ap v Empty) u + g w (ap v (ordsucc Empty)) + - g (ap v Empty) (ap v (ordsucc Empty)))) (binunion (Repl (setprod (SNoL w) (SNoR u)) \v:set.g (ap v Empty) u + g w (ap v (ordsucc Empty)) + - g (ap v Empty) (ap v (ordsucc Empty))) (Repl (setprod (SNoR w) (SNoL u)) \v:set.g (ap v Empty) u + g w (ap v (ordsucc Empty)) + - g (ap v Empty) (ap v (ordsucc Empty))))) x (ap z (ordsucc Empty)) + - SNo_rec2 (\w:set.\u:set.\g:set set set.SNoCut (binunion (Repl (setprod (SNoL w) (SNoL u)) \v:set.g (ap v Empty) u + g w (ap v (ordsucc Empty)) + - g (ap v Empty) (ap v (ordsucc Empty))) (Repl (setprod (SNoR w) (SNoR u)) \v:set.g (ap v Empty) u + g w (ap v (ordsucc Empty)) + - g (ap v Empty) (ap v (ordsucc Empty)))) (binunion (Repl (setprod (SNoL w) (SNoR u)) \v:set.g (ap v Empty) u + g w (ap v (ordsucc Empty)) + - g (ap v Empty) (ap v (ordsucc Empty))) (Repl (setprod (SNoR w) (SNoL u)) \v:set.g (ap v Empty) u + g w (ap v (ordsucc Empty)) + - g (ap v Empty) (ap v (ordsucc Empty))))) (ap z Empty) (ap z (ordsucc Empty))) (Repl (setprod (SNoR x) (SNoR y)) \z:set.SNo_rec2 (\w:set.\u:set.\g:set set set.SNoCut (binunion (Repl (setprod (SNoL w) (SNoL u)) \v:set.g (ap v Empty) u + g w (ap v (ordsucc Empty)) + - g (ap v Empty) (ap v (ordsucc Empty))) (Repl (setprod (SNoR w) (SNoR u)) \v:set.g (ap v Empty) u + g w (ap v (ordsucc Empty)) + - g (ap v Empty) (ap v (ordsucc Empty)))) (binunion (Repl (setprod (SNoL w) (SNoR u)) \v:set.g (ap v Empty) u + g w (ap v (ordsucc Empty)) + - g (ap v Empty) (ap v (ordsucc Empty))) (Repl (setprod (SNoR w) (SNoL u)) \v:set.g (ap v Empty) u + g w (ap v (ordsucc Empty)) + - g (ap v Empty) (ap v (ordsucc Empty))))) (ap z Empty) y + SNo_rec2 (\w:set.\u:set.\g:set set set.SNoCut (binunion (Repl (setprod (SNoL w) (SNoL u)) \v:set.g (ap v Empty) u + g w (ap v (ordsucc Empty)) + - g (ap v Empty) (ap v (ordsucc Empty))) (Repl (setprod (SNoR w) (SNoR u)) \v:set.g (ap v Empty) u + g w (ap v (ordsucc Empty)) + - g (ap v Empty) (ap v (ordsucc Empty)))) (binunion (Repl (setprod (SNoL w) (SNoR u)) \v:set.g (ap v Empty) u + g w (ap v (ordsucc Empty)) + - g (ap v Empty) (ap v (ordsucc Empty))) (Repl (setprod (SNoR w) (SNoL u)) \v:set.g (ap v Empty) u + g w (ap v (ordsucc Empty)) + - g (ap v Empty) (ap v (ordsucc Empty))))) x (ap z (ordsucc Empty)) + - SNo_rec2 (\w:set.\u:set.\g:set set set.SNoCut (binunion (Repl (setprod (SNoL w) (SNoL u)) \v:set.g (ap v Empty) u + g w (ap v (ordsucc Empty)) + - g (ap v Empty) (ap v (ordsucc Empty))) (Repl (setprod (SNoR w) (SNoR u)) \v:set.g (ap v Empty) u + g w (ap v (ordsucc Empty)) + - g (ap v Empty) (ap v (ordsucc Empty)))) (binunion (Repl (setprod (SNoL w) (SNoR u)) \v:set.g (ap v Empty) u + g w (ap v (ordsucc Empty)) + - g (ap v Empty) (ap v (ordsucc Empty))) (Repl (setprod (SNoR w) (SNoL u)) \v:set.g (ap v Empty) u + g w (ap v (ordsucc Empty)) + - g (ap v Empty) (ap v (ordsucc Empty))))) (ap z Empty) (ap z (ordsucc Empty)))) (binunion (Repl (setprod (SNoL x) (SNoR y)) \z:set.SNo_rec2 (\w:set.\u:set.\g:set set set.SNoCut (binunion (Repl (setprod (SNoL w) (SNoL u)) \v:set.g (ap v Empty) u + g w (ap v (ordsucc Empty)) + - g (ap v Empty) (ap v (ordsucc Empty))) (Repl (setprod (SNoR w) (SNoR u)) \v:set.g (ap v Empty) u + g w (ap v (ordsucc Empty)) + - g (ap v Empty) (ap v (ordsucc Empty)))) (binunion (Repl (setprod (SNoL w) (SNoR u)) \v:set.g (ap v Empty) u + g w (ap v (ordsucc Empty)) + - g (ap v Empty) (ap v (ordsucc Empty))) (Repl (setprod (SNoR w) (SNoL u)) \v:set.g (ap v Empty) u + g w (ap v (ordsucc Empty)) + - g (ap v Empty) (ap v (ordsucc Empty))))) (ap z Empty) y + SNo_rec2 (\w:set.\u:set.\g:set set set.SNoCut (binunion (Repl (setprod (SNoL w) (SNoL u)) \v:set.g (ap v Empty) u + g w (ap v (ordsucc Empty)) + - g (ap v Empty) (ap v (ordsucc Empty))) (Repl (setprod (SNoR w) (SNoR u)) \v:set.g (ap v Empty) u + g w (ap v (ordsucc Empty)) + - g (ap v Empty) (ap v (ordsucc Empty)))) (binunion (Repl (setprod (SNoL w) (SNoR u)) \v:set.g (ap v Empty) u + g w (ap v (ordsucc Empty)) + - g (ap v Empty) (ap v (ordsucc Empty))) (Repl (setprod (SNoR w) (SNoL u)) \v:set.g (ap v Empty) u + g w (ap v (ordsucc Empty)) + - g (ap v Empty) (ap v (ordsucc Empty))))) x (ap z (ordsucc Empty)) + - SNo_rec2 (\w:set.\u:set.\g:set set set.SNoCut (binunion (Repl (setprod (SNoL w) (SNoL u)) \v:set.g (ap v Empty) u + g w (ap v (ordsucc Empty)) + - g (ap v Empty) (ap v (ordsucc Empty))) (Repl (setprod (SNoR w) (SNoR u)) \v:set.g (ap v Empty) u + g w (ap v (ordsucc Empty)) + - g (ap v Empty) (ap v (ordsucc Empty)))) (binunion (Repl (setprod (SNoL w) (SNoR u)) \v:set.g (ap v Empty) u + g w (ap v (ordsucc Empty)) + - g (ap v Empty) (ap v (ordsucc Empty))) (Repl (setprod (SNoR w) (SNoL u)) \v:set.g (ap v Empty) u + g w (ap v (ordsucc Empty)) + - g (ap v Empty) (ap v (ordsucc Empty))))) (ap z Empty) (ap z (ordsucc Empty))) (Repl (setprod (SNoR x) (SNoL y)) \z:set.SNo_rec2 (\w:set.\u:set.\g:set set set.SNoCut (binunion (Repl (setprod (SNoL w) (SNoL u)) \v:set.g (ap v Empty) u + g w (ap v (ordsucc Empty)) + - g (ap v Empty) (ap v (ordsucc Empty))) (Repl (setprod (SNoR w) (SNoR u)) \v:set.g (ap v Empty) u + g w (ap v (ordsucc Empty)) + - g (ap v Empty) (ap v (ordsucc Empty)))) (binunion (Repl (setprod (SNoL w) (SNoR u)) \v:set.g (ap v Empty) u + g w (ap v (ordsucc Empty)) + - g (ap v Empty) (ap v (ordsucc Empty))) (Repl (setprod (SNoR w) (SNoL u)) \v:set.g (ap v Empty) u + g w (ap v (ordsucc Empty)) + - g (ap v Empty) (ap v (ordsucc Empty))))) (ap z Empty) y + SNo_rec2 (\w:set.\u:set.\g:set set set.SNoCut (binunion (Repl (setprod (SNoL w) (SNoL u)) \v:set.g (ap v Empty) u + g w (ap v (ordsucc Empty)) + - g (ap v Empty) (ap v (ordsucc Empty))) (Repl (setprod (SNoR w) (SNoR u)) \v:set.g (ap v Empty) u + g w (ap v (ordsucc Empty)) + - g (ap v Empty) (ap v (ordsucc Empty)))) (binunion (Repl (setprod (SNoL w) (SNoR u)) \v:set.g (ap v Empty) u + g w (ap v (ordsucc Empty)) + - g (ap v Empty) (ap v (ordsucc Empty))) (Repl (setprod (SNoR w) (SNoL u)) \v:set.g (ap v Empty) u + g w (ap v (ordsucc Empty)) + - g (ap v Empty) (ap v (ordsucc Empty))))) x (ap z (ordsucc Empty)) + - SNo_rec2 (\w:set.\u:set.\g:set set set.SNoCut (binunion (Repl (setprod (SNoL w) (SNoL u)) \v:set.g (ap v Empty) u + g w (ap v (ordsucc Empty)) + - g (ap v Empty) (ap v (ordsucc Empty))) (Repl (setprod (SNoR w) (SNoR u)) \v:set.g (ap v Empty) u + g w (ap v (ordsucc Empty)) + - g (ap v Empty) (ap v (ordsucc Empty)))) (binunion (Repl (setprod (SNoL w) (SNoR u)) \v:set.g (ap v Empty) u + g w (ap v (ordsucc Empty)) + - g (ap v Empty) (ap v (ordsucc Empty))) (Repl (setprod (SNoR w) (SNoL u)) \v:set.g (ap v Empty) u + g w (ap v (ordsucc Empty)) + - g (ap v Empty) (ap v (ordsucc Empty))))) (ap z Empty) (ap z (ordsucc Empty))))