const SNo : set prop
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 SNoCutP : set set prop
const binunion : set set set
const Repl : set (set set) set
const SNoL : set set
const add_SNo : set set set
term + = add_SNo
infix + 2281 2280
const SNoR : set set
axiom add_SNo_SNoCutP: !x:set.!y:set.SNo x -> SNo y -> SNoCutP (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)))
const In : set set prop
term iIn = In
infix iIn 2000 2000
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
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 SNoLe : set set prop
term <= = SNoLe
infix <= 2020 2020
axiom mul_SNo_SNoL_interpolate_impred: !x:set.!y:set.SNo x -> SNo y -> !z:set.z iIn SNoL (x * y) -> !P:prop.(!w:set.w iIn SNoL x -> !u:set.u iIn SNoL y -> (z + w * u) <= w * y + x * u -> P) -> (!w:set.w iIn SNoR x -> !u:set.u iIn SNoR y -> (z + w * u) <= w * y + x * u -> P) -> P
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
axiom add_SNo_com: !x:set.!y:set.SNo x -> SNo y -> x + y = y + x
axiom binunionE: !x:set.!y:set.!z:set.z iIn binunion x y -> z iIn x | z iIn y
axiom mul_SNo_SNoR_interpolate_impred: !x:set.!y:set.SNo x -> SNo y -> !z:set.z iIn SNoR (x * y) -> !P:prop.(!w:set.w iIn SNoL x -> !u:set.u iIn SNoR y -> (w * y + x * u) <= z + w * u -> P) -> (!w:set.w iIn SNoR x -> !u:set.u iIn SNoL y -> (w * y + x * u) <= z + w * u -> P) -> P
const SNoCut : set set set
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
const SNoS_ : set set
const minus_SNo : set set
term - = minus_SNo
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 * z + y * z) -> (!v:set.v iIn SNoS_ (SNoLev y) -> (x + v) * z = x * z + v * z) -> (!v:set.v iIn SNoS_ (SNoLev z) -> (x + y) * v = x * v + y * v) -> (!v:set.v iIn SNoS_ (SNoLev x) -> !x2:set.x2 iIn SNoS_ (SNoLev z) -> (v + y) * x2 = v * x2 + y * x2) -> (!v:set.v iIn SNoS_ (SNoLev y) -> !x2:set.x2 iIn SNoS_ (SNoLev z) -> (x + v) * x2 = x * x2 + v * x2) -> SNo (x + y) -> SNo (x * z) -> SNo (y * z) -> SNo (x * z + y * z) -> w iIn SNoL (x + y) -> u iIn SNoL z -> SNo w -> SNo u -> u < z -> SNo (x * u) -> (w * z + (x + y) * u + - w * u) < x * z + 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 * z + y * z) -> (!v:set.v iIn SNoS_ (SNoLev y) -> (x + v) * z = x * z + v * z) -> (!v:set.v iIn SNoS_ (SNoLev z) -> (x + y) * v = x * v + y * v) -> (!v:set.v iIn SNoS_ (SNoLev x) -> !x2:set.x2 iIn SNoS_ (SNoLev z) -> (v + y) * x2 = v * x2 + y * x2) -> (!v:set.v iIn SNoS_ (SNoLev y) -> !x2:set.x2 iIn SNoS_ (SNoLev z) -> (x + v) * x2 = x * x2 + v * x2) -> SNo (x + y) -> SNo (x * z) -> SNo (y * z) -> SNo (x * z + y * z) -> w iIn SNoR (x + y) -> u iIn SNoR z -> SNo w -> SNo u -> z SNo (x * u) -> (w * z + (x + y) * u + - w * u) < x * z + 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 * z + y * z) -> (!v:set.v iIn SNoS_ (SNoLev y) -> (x + v) * z = x * z + v * z) -> (!v:set.v iIn SNoS_ (SNoLev z) -> (x + y) * v = x * v + y * v) -> (!v:set.v iIn SNoS_ (SNoLev x) -> !x2:set.x2 iIn SNoS_ (SNoLev z) -> (v + y) * x2 = v * x2 + y * x2) -> (!v:set.v iIn SNoS_ (SNoLev y) -> !x2:set.x2 iIn SNoS_ (SNoLev z) -> (x + v) * x2 = x * x2 + v * x2) -> SNo (x + y) -> SNo (x * z) -> SNo (y * z) -> SNo (x * z + y * z) -> w iIn SNoL (x + y) -> u iIn SNoR z -> SNo w -> SNo u -> z SNo (x * u) -> (x * z + y * z) < w * z + (x + y) * u + - w * u
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 * z + y * z) -> (!v:set.v iIn SNoS_ (SNoLev y) -> (x + v) * z = x * z + v * z) -> (!v:set.v iIn SNoS_ (SNoLev z) -> (x + y) * v = x * v + y * v) -> (!v:set.v iIn SNoS_ (SNoLev x) -> !x2:set.x2 iIn SNoS_ (SNoLev z) -> (v + y) * x2 = v * x2 + y * x2) -> (!v:set.v iIn SNoS_ (SNoLev y) -> !x2:set.x2 iIn SNoS_ (SNoLev z) -> (x + v) * x2 = x * x2 + v * x2) -> SNo (x + y) -> SNo (x * z) -> SNo (y * z) -> SNo (x * z + y * z) -> w iIn SNoR (x + y) -> u iIn SNoL z -> SNo w -> SNo u -> u < z -> SNo (x * u) -> (x * z + y * z) < w * z + (x + y) * u + - w * u
lemma !x:set.!y:set.!z:set.!w:set.!u:set.!v:set.SNo x -> SNo y -> SNo z -> (!x2:set.x2 iIn SNoS_ (SNoLev x) -> (x2 + y) * z = x2 * z + y * z) -> (!x2:set.x2 iIn SNoS_ (SNoLev z) -> (x + y) * x2 = x * x2 + y * x2) -> (!x2:set.x2 iIn SNoS_ (SNoLev x) -> !y2:set.y2 iIn SNoS_ (SNoLev z) -> (x2 + y) * y2 = x2 * y2 + y * y2) -> SNo (x + y) -> SNo ((x + y) * z) -> SNo (y * z) -> SNo w -> u iIn SNoL x -> v iIn SNoL z -> (w + u * v) <= u * z + x * v -> SNo u -> u < x -> SNo v -> v < z -> SNo (u * v) -> (w + y * z) < (x + y) * z
lemma !x:set.!y:set.!z:set.!w:set.!u:set.!v:set.SNo x -> SNo y -> SNo z -> (!x2:set.x2 iIn SNoS_ (SNoLev x) -> (x2 + y) * z = x2 * z + y * z) -> (!x2:set.x2 iIn SNoS_ (SNoLev z) -> (x + y) * x2 = x * x2 + y * x2) -> (!x2:set.x2 iIn SNoS_ (SNoLev x) -> !y2:set.y2 iIn SNoS_ (SNoLev z) -> (x2 + y) * y2 = x2 * y2 + y * y2) -> SNo (x + y) -> SNo ((x + y) * z) -> SNo (y * z) -> SNo w -> u iIn SNoR x -> v iIn SNoR z -> (w + u * v) <= u * z + x * v -> SNo u -> x SNo v -> z < v -> SNo (u * v) -> (w + y * z) < (x + y) * z
lemma !x:set.!y:set.!z:set.!w:set.!u:set.!v:set.SNo x -> SNo y -> SNo z -> (!x2:set.x2 iIn SNoS_ (SNoLev y) -> (x + x2) * z = x * z + x2 * z) -> (!x2:set.x2 iIn SNoS_ (SNoLev z) -> (x + y) * x2 = x * x2 + y * x2) -> (!x2:set.x2 iIn SNoS_ (SNoLev y) -> !y2:set.y2 iIn SNoS_ (SNoLev z) -> (x + x2) * y2 = x * y2 + x2 * y2) -> SNo (x + y) -> SNo ((x + y) * z) -> SNo (x * z) -> SNo w -> u iIn SNoL y -> v iIn SNoL z -> (w + u * v) <= u * z + y * v -> SNo u -> u < y -> SNo v -> v < z -> SNo (u * v) -> (w + x * z) < (x + y) * z
lemma !x:set.!y:set.!z:set.!w:set.!u:set.!v:set.SNo x -> SNo y -> SNo z -> (!x2:set.x2 iIn SNoS_ (SNoLev y) -> (x + x2) * z = x * z + x2 * z) -> (!x2:set.x2 iIn SNoS_ (SNoLev z) -> (x + y) * x2 = x * x2 + y * x2) -> (!x2:set.x2 iIn SNoS_ (SNoLev y) -> !y2:set.y2 iIn SNoS_ (SNoLev z) -> (x + x2) * y2 = x * y2 + x2 * y2) -> SNo (x + y) -> SNo ((x + y) * z) -> SNo (x * z) -> SNo w -> u iIn SNoR y -> v iIn SNoR z -> (w + u * v) <= u * z + y * v -> SNo u -> y SNo v -> z < v -> SNo (u * v) -> (w + x * z) < (x + y) * z
lemma !x:set.!y:set.!z:set.!w:set.!u:set.!v:set.SNo x -> SNo y -> SNo z -> (!x2:set.x2 iIn SNoS_ (SNoLev x) -> (x2 + y) * z = x2 * z + y * z) -> (!x2:set.x2 iIn SNoS_ (SNoLev z) -> (x + y) * x2 = x * x2 + y * x2) -> (!x2:set.x2 iIn SNoS_ (SNoLev x) -> !y2:set.y2 iIn SNoS_ (SNoLev z) -> (x2 + y) * y2 = x2 * y2 + y * y2) -> SNo (x + y) -> SNo ((x + y) * z) -> SNo (y * z) -> SNo w -> u iIn SNoL x -> v iIn SNoR z -> (u * z + x * v) <= w + u * v -> SNo u -> u < x -> SNo v -> z < v -> SNo (u * v) -> (x + y) * z < w + y * z
lemma !x:set.!y:set.!z:set.!w:set.!u:set.!v:set.SNo x -> SNo y -> SNo z -> (!x2:set.x2 iIn SNoS_ (SNoLev x) -> (x2 + y) * z = x2 * z + y * z) -> (!x2:set.x2 iIn SNoS_ (SNoLev z) -> (x + y) * x2 = x * x2 + y * x2) -> (!x2:set.x2 iIn SNoS_ (SNoLev x) -> !y2:set.y2 iIn SNoS_ (SNoLev z) -> (x2 + y) * y2 = x2 * y2 + y * y2) -> SNo (x + y) -> SNo ((x + y) * z) -> SNo (y * z) -> SNo w -> u iIn SNoR x -> v iIn SNoL z -> (u * z + x * v) <= w + u * v -> SNo u -> x SNo v -> v < z -> SNo (u * v) -> (x + y) * z < w + y * z
lemma !x:set.!y:set.!z:set.!w:set.!u:set.!v:set.SNo x -> SNo y -> SNo z -> (!x2:set.x2 iIn SNoS_ (SNoLev y) -> (x + x2) * z = x * z + x2 * z) -> (!x2:set.x2 iIn SNoS_ (SNoLev z) -> (x + y) * x2 = x * x2 + y * x2) -> (!x2:set.x2 iIn SNoS_ (SNoLev y) -> !y2:set.y2 iIn SNoS_ (SNoLev z) -> (x + x2) * y2 = x * y2 + x2 * y2) -> SNo (x + y) -> SNo ((x + y) * z) -> SNo (x * z) -> SNo w -> u iIn SNoL y -> v iIn SNoR z -> (u * z + y * v) <= w + u * v -> SNo u -> u < y -> SNo v -> z < v -> SNo (u * v) -> (x + y) * z < w + x * z
lemma !x:set.!y:set.!z:set.!w:set.!u:set.!v:set.SNo x -> SNo y -> SNo z -> (!x2:set.x2 iIn SNoS_ (SNoLev y) -> (x + x2) * z = x * z + x2 * z) -> (!x2:set.x2 iIn SNoS_ (SNoLev z) -> (x + y) * x2 = x * x2 + y * x2) -> (!x2:set.x2 iIn SNoS_ (SNoLev y) -> !y2:set.y2 iIn SNoS_ (SNoLev z) -> (x + x2) * y2 = x * y2 + x2 * y2) -> SNo (x + y) -> SNo ((x + y) * z) -> SNo (x * z) -> SNo w -> u iIn SNoR y -> v iIn SNoL z -> (u * z + y * v) <= w + u * v -> SNo u -> y SNo v -> v < z -> SNo (u * v) -> (x + y) * z < w + x * z
var x:set
var y:set
var z:set
var w:set
var u:set
hyp SNo x
hyp SNo y
hyp SNo z
hyp !v:set.v iIn SNoS_ (SNoLev x) -> (v + y) * z = v * z + y * z
hyp !v:set.v iIn SNoS_ (SNoLev y) -> (x + v) * z = x * z + v * z
hyp !v:set.v iIn SNoS_ (SNoLev z) -> (x + y) * v = x * v + y * v
hyp !v:set.v iIn SNoS_ (SNoLev x) -> !x2:set.x2 iIn SNoS_ (SNoLev z) -> (v + y) * x2 = v * x2 + y * x2
hyp !v:set.v iIn SNoS_ (SNoLev y) -> !x2:set.x2 iIn SNoS_ (SNoLev z) -> (x + v) * x2 = x * x2 + v * x2
hyp SNoCutP w u
hyp !v:set.v iIn w -> !P:prop.(!x2:set.x2 iIn SNoL (x + y) -> !y2:set.y2 iIn SNoL z -> v = x2 * z + (x + y) * y2 + - x2 * y2 -> P) -> (!x2:set.x2 iIn SNoR (x + y) -> !y2:set.y2 iIn SNoR z -> v = x2 * z + (x + y) * y2 + - x2 * y2 -> P) -> P
hyp !v:set.v iIn u -> !P:prop.(!x2:set.x2 iIn SNoL (x + y) -> !y2:set.y2 iIn SNoR z -> v = x2 * z + (x + y) * y2 + - x2 * y2 -> P) -> (!x2:set.x2 iIn SNoR (x + y) -> !y2:set.y2 iIn SNoL z -> v = x2 * z + (x + y) * y2 + - x2 * y2 -> P) -> P
hyp (x + y) * z = SNoCut w u
hyp SNo (x + y)
hyp SNo ((x + y) * z)
hyp SNo (x * z)
hyp SNo (y * z)
hyp SNo (x * z + y * z)
claim x * z + y * z = SNoCut (binunion (Repl (SNoL (x * z)) \v:set.v + y * z) (Repl (SNoL (y * z)) (add_SNo (x * z)))) (binunion (Repl (SNoR (x * z)) \v:set.v + y * z) (Repl (SNoR (y * z)) (add_SNo (x * z)))) -> (x + y) * z = x * z + y * z