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 const SNoL : set set const SNoS_ : set set const SNoLev : set set axiom SNoL_SNoS_: !x:set.Subq (SNoL x) (SNoS_ (SNoLev x)) const SNo : set prop 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 add_SNo : set set set term + = add_SNo infix + 2281 2280 const SNoLe : set set prop term <= = SNoLe infix <= 2020 2020 axiom add_SNo_SNoL_interpolate: !x:set.!y:set.SNo x -> SNo y -> !z:set.z iIn SNoL (x + y) -> (?w:set.w iIn SNoL x & z <= w + y) | ?w:set.w iIn SNoL y & z <= x + w 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 SNoCut : set set set const SNoR : set set axiom add_SNo_eq: !x:set.SNo x -> !y:set.SNo y -> x + y = SNoCut (binunion (Repl (SNoL x) \z:set.z + y) (Repl (SNoL y) (add_SNo x))) (binunion (Repl (SNoR x) \z:set.z + y) (Repl (SNoR y) (add_SNo x))) axiom SNoR_SNoS_: !x:set.Subq (SNoR x) (SNoS_ (SNoLev x)) 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 axiom add_SNo_SNoR_interpolate: !x:set.!y:set.SNo x -> SNo y -> !z:set.z iIn SNoR (x + y) -> (?w:set.w iIn SNoR x & (w + y) <= z) | ?w:set.w iIn SNoR y & (x + w) <= z const SNoCutP : set set prop axiom SNoCut_ext: !x:set.!y:set.!z:set.!w:set.SNoCutP x y -> SNoCutP z w -> (!u:set.u iIn x -> u < SNoCut z w) -> (!u:set.u iIn y -> SNoCut z w < u) -> (!u:set.u iIn z -> u < SNoCut x y) -> (!u:set.u iIn w -> SNoCut x y < u) -> SNoCut x y = SNoCut z w lemma !x:set.!y:set.!z:set.!w:set.SNo x -> SNo y -> SNo z -> (!u:set.u iIn SNoS_ (SNoLev x) -> u + y + z = (u + y) + z) -> SNo (x + y) -> w iIn SNoL x -> SNo w -> w < x -> w + y + z = (w + y) + z -> (w + y + z) < (x + y) + z lemma !x:set.!y:set.!z:set.!w:set.!u:set.SNo x -> SNo y -> SNo z -> (!v:set.v iIn SNoS_ (SNoLev y) -> x + v + z = (x + v) + z) -> SNo (x + y) -> SNo w -> u iIn SNoL y -> w <= u + z -> SNo u -> u < y -> x + u + z = (x + u) + z -> (x + w) < (x + y) + z lemma !x:set.!y:set.!z:set.!w:set.!u:set.SNo x -> SNo y -> SNo z -> (!v:set.v iIn SNoS_ (SNoLev z) -> x + y + v = (x + y) + v) -> SNo (x + y) -> SNo w -> u iIn SNoL z -> w <= y + u -> SNo u -> u < z -> x + y + u = (x + y) + u -> (x + w) < (x + y) + z lemma !x:set.!y:set.!z:set.!w:set.SNo x -> SNo y -> SNo z -> (!u:set.u iIn SNoS_ (SNoLev x) -> u + y + z = (u + y) + z) -> SNo (x + y) -> w iIn SNoR x -> SNo w -> x < w -> w + y + z = (w + y) + z -> ((x + y) + z) < w + y + z lemma !x:set.!y:set.!z:set.!w:set.!u:set.SNo x -> SNo y -> SNo z -> (!v:set.v iIn SNoS_ (SNoLev y) -> x + v + z = (x + v) + z) -> SNo (x + y) -> SNo w -> u iIn SNoR y -> (u + z) <= w -> SNo u -> y < u -> x + u + z = (x + u) + z -> ((x + y) + z) < x + w lemma !x:set.!y:set.!z:set.!w:set.!u:set.SNo x -> SNo y -> SNo z -> (!v:set.v iIn SNoS_ (SNoLev z) -> x + y + v = (x + y) + v) -> SNo (x + y) -> SNo w -> u iIn SNoR z -> (y + u) <= w -> SNo u -> z < u -> x + y + u = (x + y) + u -> ((x + y) + z) < x + w lemma !x:set.!y:set.!z:set.!w:set.!u:set.SNo x -> SNo y -> SNo z -> (!v:set.v iIn SNoS_ (SNoLev x) -> v + y + z = (v + y) + z) -> SNo (y + z) -> SNo w -> u iIn SNoL x -> w <= u + y -> SNo u -> u < x -> u + y + z = (u + y) + z -> (w + z) < x + y + z lemma !x:set.!y:set.!z:set.!w:set.!u:set.SNo x -> SNo y -> SNo z -> (!v:set.v iIn SNoS_ (SNoLev y) -> x + v + z = (x + v) + z) -> SNo (y + z) -> SNo w -> u iIn SNoL y -> w <= x + u -> SNo u -> u < y -> x + u + z = (x + u) + z -> (w + z) < x + y + z lemma !x:set.!y:set.!z:set.!w:set.SNo x -> SNo y -> SNo z -> (!u:set.u iIn SNoS_ (SNoLev z) -> x + y + u = (x + y) + u) -> SNo (y + z) -> w iIn SNoL z -> SNo w -> w < z -> x + y + w = (x + y) + w -> ((x + y) + w) < x + y + z lemma !x:set.!y:set.!z:set.!w:set.!u:set.SNo x -> SNo y -> SNo z -> (!v:set.v iIn SNoS_ (SNoLev x) -> v + y + z = (v + y) + z) -> SNo (y + z) -> SNo w -> u iIn SNoR x -> (u + y) <= w -> SNo u -> x < u -> u + y + z = (u + y) + z -> (x + y + z) < w + z lemma !x:set.!y:set.!z:set.!w:set.!u:set.SNo x -> SNo y -> SNo z -> (!v:set.v iIn SNoS_ (SNoLev y) -> x + v + z = (x + v) + z) -> SNo (y + z) -> SNo w -> u iIn SNoR y -> (x + u) <= w -> SNo u -> y < u -> x + u + z = (x + u) + z -> (x + y + z) < w + z lemma !x:set.!y:set.!z:set.!w:set.SNo x -> SNo y -> SNo z -> (!u:set.u iIn SNoS_ (SNoLev z) -> x + y + u = (x + y) + u) -> SNo (y + z) -> w iIn SNoR z -> SNo w -> z < w -> x + y + w = (x + y) + w -> (x + y + z) < (x + y) + w var x:set var y:set var z:set hyp SNo x hyp SNo y hyp SNo z hyp !w:set.w iIn SNoS_ (SNoLev x) -> w + y + z = (w + y) + z hyp !w:set.w iIn SNoS_ (SNoLev y) -> x + w + z = (x + w) + z hyp !w:set.w iIn SNoS_ (SNoLev z) -> x + y + w = (x + y) + w hyp SNo (x + y) hyp SNo (y + z) hyp SNoCutP (binunion (Repl (SNoL x) \w:set.w + y + z) (Repl (SNoL (y + z)) (add_SNo x))) (binunion (Repl (SNoR x) \w:set.w + y + z) (Repl (SNoR (y + z)) (add_SNo x))) claim SNoCutP (binunion (Repl (SNoL (x + y)) \w:set.w + z) (Repl (SNoL z) (add_SNo (x + y)))) (binunion (Repl (SNoR (x + y)) \w:set.w + z) (Repl (SNoR z) (add_SNo (x + y)))) -> SNoCut (binunion (Repl (SNoL x) \w:set.w + y + z) (Repl (SNoL (y + z)) (add_SNo x))) (binunion (Repl (SNoR x) \w:set.w + y + z) (Repl (SNoR (y + z)) (add_SNo x))) = SNoCut (binunion (Repl (SNoL (x + y)) \w:set.w + z) (Repl (SNoL z) (add_SNo (x + y)))) (binunion (Repl (SNoR (x + y)) \w:set.w + z) (Repl (SNoR z) (add_SNo (x + y))))