helm/software/matita/tests/paramodulation/BOO075-1.ma

   1 set "baseuri" "cic:/matita/TPTP/BOO075-1".
   2
   3 inductive eq (A:Type) (x:A) : A \to Prop \def refl_eq : eq A x x.
   4
   5 theorem sym_eq : \forall A:Type.\forall x,y:A. eq A x y \to eq A y x.
   6 intros.elim H. apply refl_eq.
   7 qed.
   8
   9 theorem eq_elim_r:
  10  \forall A:Type.\forall x:A. \forall P: A \to Prop.
  11    P x \to \forall y:A. eq A y x \to P y.
  12 intros. elim (sym_eq ? ? ? H1).assumption.
  13 qed.
  14
  15 theorem trans_eq :
  16     \forall A:Type.\forall x,y,z:A. eq A x y \to eq A y z \to eq A x z.
  17 intros.elim H1.assumption.
  18 qed.
  19
  20 default "equality"
  21  cic:/matita/TPTP/BOO075-1/eq.ind
  22  cic:/matita/TPTP/BOO075-1/sym_eq.con
  23  cic:/matita/TPTP/BOO075-1/trans_eq.con
  24  cic:/matita/TPTP/BOO075-1/eq_ind.con
  25  cic:/matita/TPTP/BOO075-1/eq_elim_r.con
  26  cic:/matita/TPTP/BOO075-1/eq_f.con
  27  cic:/matita/TPTP/BOO075-1/eq_f1.con.
  28
  29 theorem eq_f: \forall  A,B:Type.\forall f:A\to B.
  30   \forall x,y:A. eq A x y \to eq B (f x) (f y).
  31 intros.elim H.reflexivity.
  32 qed.
  33
  34 theorem eq_f1: \forall  A,B:Type.\forall f:A\to B.
  35   \forall x,y:A. eq A x y \to eq B (f y) (f x).
  36 intros.elim H.reflexivity.
  37 qed.
  38
  39 inductive ex (A:Type) (P:A \to Prop) : Prop \def
  40     ex_intro: \forall x:A. P x \to ex A P.
  41 interpretation "exists" 'exists \eta.x =
  42   (cic:/matita/TPTP/BOO075-1/ex.ind#xpointer(1/1) _ x).
  43
  44 notation < "hvbox(\exists ident i opt (: ty) break . p)"
  45   right associative with precedence 20
  46 for @{ 'exists ${default
  47   @{\lambda ${ident i} : $ty. $p)}
  48   @{\lambda ${ident i} . $p}}}.
  49
  50
  51 (* Inclusion of: BOO075-1.p *)
  52 (* -------------------------------------------------------------------------- *)
  53 (*  File     : BOO075-1 : TPTP v3.1.1. Released v2.6.0. *)
  54 (*  Domain   : Boolean Algebra *)
  55 (*  Problem  : Sh-1 is a single axiom for Boolean algebra, part 1 *)
  56 (*  Version  : [EF+02] axioms. *)
  57 (*  English  :  *)
  58 (*  Refs     : [EF+02] Ernst et al. (2002), More First-order Test Problems in *)
  59 (*           : [MV+02] McCune et al. (2002), Short Single Axioms for Boolean *)
  60 (*  Source   : [TPTP] *)
  61 (*  Names    :  *)
  62 (*  Status   : Unsatisfiable *)
  63 (*  Rating   : 0.00 v2.6.0 *)
  64 (*  Syntax   : Number of clauses     :    2 (   0 non-Horn;   2 unit;   1 RR) *)
  65 (*             Number of atoms       :    2 (   2 equality) *)
  66 (*             Maximal clause size   :    1 (   1 average) *)
  67 (*             Number of predicates  :    1 (   0 propositional; 2-2 arity) *)
  68 (*             Number of functors    :    3 (   2 constant; 0-2 arity) *)
  69 (*             Number of variables   :    3 (   1 singleton) *)
  70 (*             Maximal term depth    :    5 (   2 average) *)
  71 (*  Comments : A UEQ part of BOO039-1 *)
  72 (* -------------------------------------------------------------------------- *)
  73 theorem prove_meredith_2_basis_1:
  74  \forall Univ:Set.
  75 \forall a:Univ.
  76 \forall b:Univ.
  77 \forall nand:Univ\rarr Univ\rarr Univ.
  78 \forall H0:\forall A:Univ.\forall B:Univ.\forall C:Univ.eq Univ (nand (nand A (nand (nand B A) A)) (nand B (nand C A))) B.eq Univ (nand (nand a a) (nand b a)) a
  79 .
  80 intros.
  81 auto paramodulation timeout=600.
  82 try assumption.
  83 print proofterm.
  84 qed.
  85 (* -------------------------------------------------------------------------- *)