const SNo : set prop const add_SNo : set set set term + = add_SNo infix + 2281 2280 axiom SNo_add_SNo: !x:set.!y:set.SNo x -> SNo y -> SNo (x + y) const SNoLt : set set prop term < = SNoLt infix < 2020 2020 lemma !g:set set set.!x:set.!y:set.!z:set.!w:set.!u:set.!v:set.(!x2:set.!y2:set.SNo x2 -> SNo y2 -> SNo (g x2 y2)) -> (!x2:set.!y2:set.!z2:set.!w2:set.SNo x2 -> SNo y2 -> SNo z2 -> SNo w2 -> z2 < x2 -> w2 < y2 -> (g z2 y2 + g x2 w2) < g x2 y2 + g z2 w2) -> SNo x -> SNo y -> SNo z -> SNo (g x y) -> SNo w -> w < x -> SNo u -> y < u -> SNo v -> z < v -> SNo (g w y) -> SNo (g w u) -> SNo (g x u) -> SNo (g w y + g x u) -> SNo (g x y + g w u) -> (g (g w y + g x u) z + g (g x y + g w u) v) < g (g x y + g w u) z + g (g w y + g x u) v var g:set set set var x:set var y:set var z:set var w:set var u:set var v:set hyp !x2:set.!y2:set.SNo x2 -> SNo y2 -> SNo (g x2 y2) hyp !x2:set.!y2:set.!z2:set.!w2:set.SNo x2 -> SNo y2 -> SNo z2 -> SNo w2 -> z2 < x2 -> w2 < y2 -> (g z2 y2 + g x2 w2) < g x2 y2 + g z2 w2 hyp SNo x hyp SNo y hyp SNo z hyp SNo (g x y) hyp SNo w hyp w < x hyp SNo u hyp y < u hyp SNo v hyp z < v hyp SNo (g w y) hyp SNo (g w u) hyp SNo (g x u) claim SNo (g w y + g x u) -> (g (g w y + g x u) z + g (g x y + g w u) v) < g (g x y + g w u) z + g (g w y + g x u) v