Commit f7b45e7c authored by Guillaume Melquiond's avatar Guillaume Melquiond

Remove redundant hypothesis from axioms about set.Fsetint.min/max_elt.

parent 6be732cd
......@@ -249,16 +249,14 @@ theory Fsetint
axiom min_elt_def1:
forall s: set int. not (is_empty s) -> mem (min_elt s) s
axiom min_elt_def2:
forall s: set int. not (is_empty s) ->
forall x: int. mem x s -> min_elt s <= x
forall s: set int. forall x: int. mem x s -> min_elt s <= x
function max_elt (set int) : int
axiom max_elt_def1:
forall s: set int. not (is_empty s) -> mem (max_elt s) s
axiom max_elt_def2:
forall s: set int. not (is_empty s) ->
forall x: int. mem x s -> x <= max_elt s
forall s: set int. forall x: int. mem x s -> x <= max_elt s
function interval int int : set int
......
Markdown is supported
0%
or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment