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

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