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 term TransSet = \x:set.!y:set.y iIn x -> Subq y x 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 axiom SNo_mul_SNo: !x:set.!y:set.SNo x -> SNo y -> SNo (x * y) const SNoLt : set set prop term < = SNoLt infix < 2020 2020 const add_SNo : set set set term + = add_SNo infix + 2281 2280 const minus_SNo : set set term - = minus_SNo axiom add_SNo_minus_Lt1b3: !x:set.!y:set.!z:set.!w:set.SNo x -> SNo y -> SNo z -> SNo w -> (x + y) < w + z -> (x + y + - z) < w const SNoLev : set set 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 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 SNoCut : set set set axiom SNo_eta: !x:set.SNo x -> x = SNoCut (SNoL x) (SNoR x) const SNoS_ : set set axiom SNoS_I2: !x:set.!y:set.SNo x -> SNo y -> SNoLev x iIn SNoLev y -> x iIn SNoS_ (SNoLev y) const ordinal : set prop axiom SNoLev_ordinal: !x:set.SNo x -> ordinal (SNoLev x) axiom ordinal_TransSet: !x:set.ordinal x -> TransSet x axiom In_no2cycle: !x:set.!y:set.x iIn y -> ~ y iIn x axiom SNoLt_trichotomy_or_impred: !x:set.!y:set.SNo x -> SNo y -> !P:prop.(x < y -> P) -> (x = y -> P) -> (y < x -> P) -> P const SNoLe : set set prop term <= = SNoLe infix <= 2020 2020 axiom SNoCut_Le: !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 w -> SNoCut x y < u) -> SNoCut x y <= SNoCut z w axiom mul_SNo_eq_3: !x:set.!y:set.SNo x -> SNo y -> !P:prop.(!z:set.!w:set.SNoCutP z w -> (!u:set.u iIn z -> !Q:prop.(!v:set.v iIn SNoL x -> !x2:set.x2 iIn SNoL y -> u = v * y + x * x2 + - v * x2 -> Q) -> (!v:set.v iIn SNoR x -> !x2:set.x2 iIn SNoR y -> u = v * y + x * x2 + - v * x2 -> Q) -> Q) -> (!u:set.u iIn SNoL x -> !v:set.v iIn SNoL y -> u * y + x * v + - u * v iIn z) -> (!u:set.u iIn SNoR x -> !v:set.v iIn SNoR y -> u * y + x * v + - u * v iIn z) -> (!u:set.u iIn w -> !Q:prop.(!v:set.v iIn SNoL x -> !x2:set.x2 iIn SNoR y -> u = v * y + x * x2 + - v * x2 -> Q) -> (!v:set.v iIn SNoR x -> !x2:set.x2 iIn SNoL y -> u = v * y + x * x2 + - v * x2 -> Q) -> Q) -> (!u:set.u iIn SNoL x -> !v:set.v iIn SNoR y -> u * y + x * v + - u * v iIn w) -> (!u:set.u iIn SNoR x -> !v:set.v iIn SNoL y -> u * y + x * v + - u * v iIn w) -> x * y = SNoCut z w -> P) -> P axiom SNoLtLe_tra: !x:set.!y:set.!z:set.SNo x -> SNo y -> SNo z -> x < y -> y <= z -> x < z axiom SNoLt_irref: !x:set.~ x < x lemma !x:set.!y:set.!z:set.!w:set.SNo x -> SNo y -> SNo (x * y) -> SNo z -> (!u:set.u iIn SNoS_ (SNoLev z) -> SNoLev u iIn SNoLev (x * y) -> u < x * y -> (?v:set.v iIn SNoL x & ?x2:set.x2 iIn SNoL y & (u + v * x2) <= v * y + x * x2) | ?v:set.v iIn SNoR x & ?x2:set.x2 iIn SNoR y & (u + v * x2) <= v * y + x * x2) -> SNoLev z iIn SNoLev (x * y) -> (!u:set.u iIn SNoL x -> !v:set.v iIn SNoL y -> (u * y + x * v) < z + u * v) -> (!u:set.u iIn SNoR x -> !v:set.v iIn SNoR y -> (u * y + x * v) < z + u * v) -> SNo w -> SNoLev w iIn SNoLev z -> z < w -> w < x * y -> (?u:set.u iIn SNoL x & ?v:set.v iIn SNoL y & (w + u * v) <= u * y + x * v) | (?u:set.u iIn SNoR x & ?v:set.v iIn SNoR y & (w + u * v) <= u * y + x * v) -> x * y < w var x:set var y:set var z:set hyp SNo x hyp SNo y hyp SNo (x * y) hyp SNo z hyp !w:set.w iIn SNoS_ (SNoLev z) -> SNoLev w iIn SNoLev (x * y) -> w < x * y -> (?u:set.u iIn SNoL x & ?v:set.v iIn SNoL y & (w + u * v) <= u * y + x * v) | ?u:set.u iIn SNoR x & ?v:set.v iIn SNoR y & (w + u * v) <= u * y + x * v hyp SNoLev z iIn SNoLev (x * y) hyp z < x * y hyp ~ ((?w:set.w iIn SNoL x & ?u:set.u iIn SNoL y & (z + w * u) <= w * y + x * u) | ?w:set.w iIn SNoR x & ?u:set.u iIn SNoR y & (z + w * u) <= w * y + x * u) hyp !w:set.w iIn SNoL x -> !u:set.u iIn SNoL y -> (w * y + x * u) < z + w * u claim ~ !w:set.w iIn SNoR x -> !u:set.u iIn SNoR y -> (w * y + x * u) < z + w * u