const SNo : set prop const Empty : set axiom SNo_0: SNo Empty const minus_SNo : set set term - = minus_SNo axiom SNo_minus_SNo: !x:set.SNo x -> SNo - x const In : set set prop term iIn = In infix iIn 2000 2000 const SNoL : set set const SNoLev : set set const SNoLt : set set prop term < = SNoLt infix < 2020 2020 axiom SNoL_E: !x:set.SNo x -> !y:set.y iIn SNoL x -> !P:prop.(SNo y -> SNoLev y iIn SNoLev x -> y < x -> P) -> P const Repl : set (set set) set axiom ReplE_impred: !x:set.!f:set set.!y:set.y iIn Repl x f -> !P:prop.(!z:set.z iIn x -> y = f z -> P) -> P const binunion : set set set axiom binunionE: !x:set.!y:set.!z:set.z iIn binunion x y -> z iIn x | z iIn y const SNoR : set set axiom SNoR_E: !x:set.SNo x -> !y:set.y iIn SNoR x -> !P:prop.(SNo y -> SNoLev y iIn SNoLev x -> x < y -> P) -> P const SNoCutP : set set prop const Subq : set set prop const SNoCut : set set set const SNoEq_ : set set set prop axiom SNoCutP_SNoCut_fst: !x:set.!y:set.SNoCutP x y -> !z:set.SNo z -> (!w:set.w iIn x -> w < z) -> (!w:set.w iIn y -> z < w) -> Subq (SNoLev (SNoCut x y)) (SNoLev z) & SNoEq_ (SNoLev (SNoCut x y)) (SNoCut x y) z const SNoS_ : set set const add_SNo : set set set term + = add_SNo infix + 2281 2280 lemma !x:set.SNo x -> (!y:set.y iIn SNoS_ (SNoLev x) -> - y + y = Empty) -> SNo - x -> SNoCutP (binunion (Repl (SNoL - x) \y:set.y + x) (Repl (SNoL x) (add_SNo - x))) (binunion (Repl (SNoR - x) \y:set.y + x) (Repl (SNoR x) (add_SNo - x))) -> SNo (SNoCut (binunion (Repl (SNoL - x) \y:set.y + x) (Repl (SNoL x) (add_SNo - x))) (binunion (Repl (SNoR - x) \y:set.y + x) (Repl (SNoR x) (add_SNo - x)))) -> Subq (SNoLev (SNoCut (binunion (Repl (SNoL - x) \y:set.y + x) (Repl (SNoL x) (add_SNo - x))) (binunion (Repl (SNoR - x) \y:set.y + x) (Repl (SNoR x) (add_SNo - x))))) (SNoLev Empty) & SNoEq_ (SNoLev (SNoCut (binunion (Repl (SNoL - x) \y:set.y + x) (Repl (SNoL x) (add_SNo - x))) (binunion (Repl (SNoR - x) \y:set.y + x) (Repl (SNoR x) (add_SNo - x))))) (SNoCut (binunion (Repl (SNoL - x) \y:set.y + x) (Repl (SNoL x) (add_SNo - x))) (binunion (Repl (SNoR - x) \y:set.y + x) (Repl (SNoR x) (add_SNo - x)))) Empty -> SNoCut (binunion (Repl (SNoL - x) \y:set.y + x) (Repl (SNoL x) (add_SNo - x))) (binunion (Repl (SNoR - x) \y:set.y + x) (Repl (SNoR x) (add_SNo - x))) = Empty lemma !x:set.!y:set.!z:set.SNo x -> (!w:set.w iIn SNoS_ (SNoLev x) -> - w + w = Empty) -> SNo - x -> y = z + x -> SNo z -> SNoLev z iIn SNoLev - x -> z < - x -> SNo - z -> y < Empty lemma !x:set.!y:set.!z:set.SNo x -> (!w:set.w iIn SNoS_ (SNoLev x) -> - w + w = Empty) -> SNo - x -> y = - x + z -> SNo z -> SNoLev z iIn SNoLev x -> z < x -> SNo - z -> y < Empty lemma !x:set.!y:set.!z:set.SNo x -> (!w:set.w iIn SNoS_ (SNoLev x) -> - w + w = Empty) -> SNo - x -> y = z + x -> SNo z -> SNoLev z iIn SNoLev - x -> - x < z -> SNo - z -> Empty < y lemma !x:set.!y:set.!z:set.SNo x -> (!w:set.w iIn SNoS_ (SNoLev x) -> - w + w = Empty) -> SNo - x -> y = - x + z -> SNo z -> SNoLev z iIn SNoLev x -> x < z -> SNo - z -> Empty < y var x:set hyp SNo x hyp !y:set.y iIn SNoS_ (SNoLev x) -> - y + y = Empty hyp SNo - x hyp SNoCutP (binunion (Repl (SNoL - x) \y:set.y + x) (Repl (SNoL x) (add_SNo - x))) (binunion (Repl (SNoR - x) \y:set.y + x) (Repl (SNoR x) (add_SNo - x))) claim SNo (SNoCut (binunion (Repl (SNoL - x) \y:set.y + x) (Repl (SNoL x) (add_SNo - x))) (binunion (Repl (SNoR - x) \y:set.y + x) (Repl (SNoR x) (add_SNo - x)))) -> SNoCut (binunion (Repl (SNoL - x) \y:set.y + x) (Repl (SNoL x) (add_SNo - x))) (binunion (Repl (SNoR - x) \y:set.y + x) (Repl (SNoR x) (add_SNo - x))) = Empty