Tutorial/Abstractions_and_quantifiers.ml

   1 MESON[]
   2  `((?x. !y. P(x) <=> P(y)) <=> ((?x. Q(x)) <=> (!y. Q(y)))) <=>
   3   ((?x. !y. Q(x) <=> Q(y)) <=> ((?x. P(x)) <=> (!y. P(y))))`;;
   4
   5 MESON[]
   6 `(!x y z. P x y /\ P y z ==> P x z) /\
   7  (!x y z. Q x y /\ Q y z ==> Q x z) /\
   8  (!x y. P x y ==> P y x) /\
   9  (!x y. P x y \/ Q x y)
  10  ==> (!x y. P x y) \/ (!x y. Q x y)`;;
  11
  12 let ewd1062 = MESON[]
  13  `(!x. x <= x) /\
  14   (!x y z. x <= y /\ y <= z ==> x <= z) /\
  15   (!x y. f(x) <= y <=> x <= g(y))
  16   ==> (!x y. x <= y ==> f(x) <= f(y)) /\
  17       (!x y. x <= y ==> g(x) <= g(y))`;;
  18
  19 let ewd1062 = MESON[]
  20  `(!x. R x x) /\
  21   (!x y z. R x y /\ R y z ==> R x z) /\
  22   (!x y. R (f x) y <=> R x (g y))
  23   ==> (!x y. R x y ==> R (f x) (f y)) /\
  24       (!x y. R x y ==> R (g x) (g y))`;;
  25
  26 MESON[] `(?!x. g(f x) = x) <=> (?!y. f(g y) = y)`;;
  27
  28 MESON [ADD_ASSOC; ADD_SYM] `m + (n + p) = n + (m + p)`;;