const In : set set prop term iIn = In infix iIn 2000 2000 const SNo : set prop const SNoLt : set set prop term < = SNoLt infix < 2020 2020 term SNoCutP = \x:set.\y:set.(!z:set.z iIn x -> SNo z) & (!z:set.z iIn y -> SNo z) & !z:set.z iIn x -> !w:set.w iIn y -> z < w 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 SNoS_ : set set const SNoLev : set set const mul_SNo : set set set term * = mul_SNo infix * 2291 2290 const SNoL : set set const add_SNo : set set set term + = add_SNo infix + 2281 2280 const SNoR : set set const minus_SNo : set set term - = minus_SNo const SNoCut : set set set lemma !x:set.!y:set.!z:set.!w:set.SNo x -> (!u:set.u iIn SNoS_ (SNoLev x) -> !v:set.SNo v -> !P:prop.(SNo (u * v) -> (!x2:set.x2 iIn SNoL u -> !y2:set.y2 iIn SNoL v -> (x2 * v + u * y2) < u * v + x2 * y2) -> (!x2:set.x2 iIn SNoR u -> !y2:set.y2 iIn SNoR v -> (x2 * v + u * y2) < u * v + x2 * y2) -> (!x2:set.x2 iIn SNoL u -> !y2:set.y2 iIn SNoR v -> (u * v + x2 * y2) < x2 * v + u * y2) -> (!x2:set.x2 iIn SNoR u -> !y2:set.y2 iIn SNoL v -> (u * v + x2 * y2) < x2 * v + u * y2) -> P) -> P) -> SNo y -> (!u:set.u iIn SNoS_ (SNoLev y) -> !P:prop.(SNo (x * u) -> (!v:set.v iIn SNoL x -> !x2:set.x2 iIn SNoL u -> (v * u + x * x2) < x * u + v * x2) -> (!v:set.v iIn SNoR x -> !x2:set.x2 iIn SNoR u -> (v * u + x * x2) < x * u + v * x2) -> (!v:set.v iIn SNoL x -> !x2:set.x2 iIn SNoR u -> (x * u + v * x2) < v * u + x * x2) -> (!v:set.v iIn SNoR x -> !x2:set.x2 iIn SNoL u -> (x * u + v * x2) < v * u + x * x2) -> P) -> P) -> (!u:set.u iIn z -> !P:prop.(!v:set.v iIn SNoL x -> !x2:set.x2 iIn SNoL y -> u = v * y + x * x2 + - v * x2 -> P) -> (!v:set.v iIn SNoR x -> !x2:set.x2 iIn SNoR y -> u = v * y + x * x2 + - v * x2 -> P) -> P) -> (!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 -> !P:prop.(!v:set.v iIn SNoL x -> !x2:set.x2 iIn SNoR y -> u = v * y + x * x2 + - v * x2 -> P) -> (!v:set.v iIn SNoR x -> !x2:set.x2 iIn SNoL y -> u = v * y + x * x2 + - v * x2 -> P) -> P) -> (!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 -> (!u:set.u iIn SNoL x -> !v:set.SNo v -> SNo (u * v)) -> (!u:set.u iIn SNoR x -> !v:set.SNo v -> SNo (u * v)) -> (!u:set.u iIn SNoL x -> SNo (u * y)) -> !P:prop.(SNo (x * y) -> (!u:set.u iIn SNoL x -> !v:set.v iIn SNoL y -> (u * y + x * v) < x * y + u * v) -> (!u:set.u iIn SNoR x -> !v:set.v iIn SNoR y -> (u * y + x * v) < x * y + u * v) -> (!u:set.u iIn SNoL x -> !v:set.v iIn SNoR y -> (x * y + u * v) < u * y + x * v) -> (!u:set.u iIn SNoR x -> !v:set.v iIn SNoL y -> (x * y + u * v) < u * y + x * v) -> P) -> P var x:set var y:set var z:set var w:set hyp SNo x hyp !u:set.u iIn SNoS_ (SNoLev x) -> !v:set.SNo v -> !P:prop.(SNo (u * v) -> (!x2:set.x2 iIn SNoL u -> !y2:set.y2 iIn SNoL v -> (x2 * v + u * y2) < u * v + x2 * y2) -> (!x2:set.x2 iIn SNoR u -> !y2:set.y2 iIn SNoR v -> (x2 * v + u * y2) < u * v + x2 * y2) -> (!x2:set.x2 iIn SNoL u -> !y2:set.y2 iIn SNoR v -> (u * v + x2 * y2) < x2 * v + u * y2) -> (!x2:set.x2 iIn SNoR u -> !y2:set.y2 iIn SNoL v -> (u * v + x2 * y2) < x2 * v + u * y2) -> P) -> P hyp SNo y hyp !u:set.u iIn SNoS_ (SNoLev y) -> !P:prop.(SNo (x * u) -> (!v:set.v iIn SNoL x -> !x2:set.x2 iIn SNoL u -> (v * u + x * x2) < x * u + v * x2) -> (!v:set.v iIn SNoR x -> !x2:set.x2 iIn SNoR u -> (v * u + x * x2) < x * u + v * x2) -> (!v:set.v iIn SNoL x -> !x2:set.x2 iIn SNoR u -> (x * u + v * x2) < v * u + x * x2) -> (!v:set.v iIn SNoR x -> !x2:set.x2 iIn SNoL u -> (x * u + v * x2) < v * u + x * x2) -> P) -> P hyp !u:set.u iIn z -> !P:prop.(!v:set.v iIn SNoL x -> !x2:set.x2 iIn SNoL y -> u = v * y + x * x2 + - v * x2 -> P) -> (!v:set.v iIn SNoR x -> !x2:set.x2 iIn SNoR y -> u = v * y + x * x2 + - v * x2 -> P) -> P hyp !u:set.u iIn SNoL x -> !v:set.v iIn SNoL y -> u * y + x * v + - u * v iIn z hyp !u:set.u iIn SNoR x -> !v:set.v iIn SNoR y -> u * y + x * v + - u * v iIn z hyp !u:set.u iIn w -> !P:prop.(!v:set.v iIn SNoL x -> !x2:set.x2 iIn SNoR y -> u = v * y + x * x2 + - v * x2 -> P) -> (!v:set.v iIn SNoR x -> !x2:set.x2 iIn SNoL y -> u = v * y + x * x2 + - v * x2 -> P) -> P hyp !u:set.u iIn SNoL x -> !v:set.v iIn SNoR y -> u * y + x * v + - u * v iIn w hyp !u:set.u iIn SNoR x -> !v:set.v iIn SNoL y -> u * y + x * v + - u * v iIn w hyp x * y = SNoCut z w hyp !u:set.u iIn SNoL x -> !v:set.SNo v -> SNo (u * v) claim (!u:set.u iIn SNoR x -> !v:set.SNo v -> SNo (u * v)) -> !P:prop.(SNo (x * y) -> (!u:set.u iIn SNoL x -> !v:set.v iIn SNoL y -> (u * y + x * v) < x * y + u * v) -> (!u:set.u iIn SNoR x -> !v:set.v iIn SNoR y -> (u * y + x * v) < x * y + u * v) -> (!u:set.u iIn SNoL x -> !v:set.v iIn SNoR y -> (x * y + u * v) < u * y + x * v) -> (!u:set.u iIn SNoR x -> !v:set.v iIn SNoL y -> (x * y + u * v) < u * y + x * v) -> P) -> P