const In : set set prop term iIn = In infix iIn 2000 2000 term nIn = \x:set.\y:set.~ x iIn y const SNo : set prop const SNoCutP : set set prop const SNoL : set set const SNoR : set set axiom SNoCutP_SNoL_SNoR: !x:set.SNo x -> SNoCutP (SNoL x) (SNoR x) const mul_SNo : set set set term * = mul_SNo infix * 2291 2290 const Empty : set axiom mul_SNo_zeroR: !x:set.SNo x -> x * Empty = Empty const minus_SNo : set set term - = minus_SNo axiom minus_SNo_0: - Empty = Empty axiom SNo_0: SNo Empty axiom SNo_mul_SNo: !x:set.!y:set.SNo x -> SNo y -> SNo (x * y) const add_SNo : set set set term + = add_SNo infix + 2281 2280 axiom add_SNo_0R: !x:set.SNo x -> x + Empty = x const ordsucc : set set axiom SNo_1: SNo (ordsucc Empty) const SNoS_ : set set const SNoLev : set set axiom SNoL_SNoS: !x:set.SNo x -> !y:set.y iIn SNoL x -> y iIn SNoS_ (SNoLev x) 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 axiom cases_1: !x:set.x iIn ordsucc Empty -> !p:set prop.p Empty -> p x axiom SNoL_1: SNoL (ordsucc Empty) = ordsucc Empty axiom EmptyE: !x:set.nIn x Empty axiom FalseE: ~ False axiom SNoR_1: SNoR (ordsucc Empty) = Empty const SNoCut : set set set axiom SNoCutP_SNoCut_L: !x:set.!y:set.SNoCutP x y -> !z:set.z iIn x -> z < SNoCut x y axiom SNoR_SNoS: !x:set.SNo x -> !y:set.y iIn SNoR x -> y iIn 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 SNoCutP_SNoCut_R: !x:set.!y:set.SNoCutP x y -> !z:set.z iIn y -> SNoCut x y < z 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 axiom SNo_eta: !x:set.SNo x -> x = SNoCut (SNoL x) (SNoR x) lemma !x:set.!y:set.!z:set.SNo x -> (!w:set.w iIn SNoS_ (SNoLev x) -> w * ordsucc Empty = w) -> z iIn SNoL x -> y = z * ordsucc Empty + x * Empty + - z * Empty -> SNo z -> y = z -> y iIn SNoL x lemma !x:set.!y:set.!z:set.SNo x -> (!w:set.w iIn SNoS_ (SNoLev x) -> w * ordsucc Empty = w) -> z iIn SNoR x -> y = z * ordsucc Empty + x * Empty + - z * Empty -> SNo z -> y = z -> y iIn SNoR x lemma !x:set.!y:set.SNo x -> (!z:set.z iIn SNoS_ (SNoLev x) -> z * ordsucc Empty = z) -> (!z:set.z iIn SNoL x -> !w:set.w iIn SNoL (ordsucc Empty) -> (z * ordsucc Empty + x * w) < x * ordsucc Empty + z * w) -> Empty iIn SNoL (ordsucc Empty) -> y iIn SNoL x -> SNo y -> y * ordsucc Empty + x * Empty = y -> y < x * ordsucc Empty lemma !x:set.!y:set.SNo x -> (!z:set.z iIn SNoS_ (SNoLev x) -> z * ordsucc Empty = z) -> (!z:set.z iIn SNoR x -> !w:set.w iIn SNoL (ordsucc Empty) -> (x * ordsucc Empty + z * w) < z * ordsucc Empty + x * w) -> Empty iIn SNoL (ordsucc Empty) -> y iIn SNoR x -> SNo y -> x * ordsucc Empty + y * Empty = x * ordsucc Empty -> x * ordsucc Empty < y var x:set var y:set var z:set hyp SNo x hyp !w:set.w iIn SNoS_ (SNoLev x) -> w * ordsucc Empty = w hyp SNoCutP y z hyp !w:set.w iIn y -> !P:prop.(!u:set.u iIn SNoL x -> !v:set.v iIn SNoL (ordsucc Empty) -> w = u * ordsucc Empty + x * v + - u * v -> P) -> (!u:set.u iIn SNoR x -> !v:set.v iIn SNoR (ordsucc Empty) -> w = u * ordsucc Empty + x * v + - u * v -> P) -> P hyp !w:set.w iIn z -> !P:prop.(!u:set.u iIn SNoL x -> !v:set.v iIn SNoR (ordsucc Empty) -> w = u * ordsucc Empty + x * v + - u * v -> P) -> (!u:set.u iIn SNoR x -> !v:set.v iIn SNoL (ordsucc Empty) -> w = u * ordsucc Empty + x * v + - u * v -> P) -> P hyp x * ordsucc Empty = SNoCut y z hyp !w:set.w iIn SNoL x -> !u:set.u iIn SNoL (ordsucc Empty) -> (w * ordsucc Empty + x * u) < x * ordsucc Empty + w * u hyp !w:set.w iIn SNoR x -> !u:set.u iIn SNoL (ordsucc Empty) -> (x * ordsucc Empty + w * u) < w * ordsucc Empty + x * u claim Empty iIn SNoL (ordsucc Empty) -> x * ordsucc Empty = x