matita/tests/TPTP/Veloci/LDA001-1.p.ma

   1
   2 include "logic/equality.ma".
   3 (* Inclusion of: LDA001-1.p *)
   4 (* -------------------------------------------------------------------------- *)
   5 (*  File     : LDA001-1 : TPTP v3.1.1. Released v1.0.0. *)
   6 (*  Domain   : LD-Algebras *)
   7 (*  Problem  : Verify 3*2*U = UUU, where U = 2*2 *)
   8 (*  Version  : [Jec93] (equality) axioms. *)
   9 (*  English  :  *)
  10 (*  Refs     : [Jec93] Jech (1993), LD-Algebras *)
  11 (*  Source   : [Jec93] *)
  12 (*  Names    : Problem 1 [Jec93] *)
  13 (*  Status   : Unsatisfiable *)
  14 (*  Rating   : 0.00 v2.2.1, 0.22 v2.2.0, 0.29 v2.1.0, 0.25 v2.0.0 *)
  15 (*  Syntax   : Number of clauses     :    5 (   0 non-Horn;   5 unit;   4 RR) *)
  16 (*             Number of atoms       :    5 (   5 equality) *)
  17 (*             Maximal clause size   :    1 (   1 average) *)
  18 (*             Number of predicates  :    1 (   0 propositional; 2-2 arity) *)
  19 (*             Number of functors    :    5 (   4 constant; 0-2 arity) *)
  20 (*             Number of variables   :    3 (   0 singleton) *)
  21 (*             Maximal term depth    :    3 (   2 average) *)
  22 (*  Comments :  *)
  23 (* -------------------------------------------------------------------------- *)
  24 (* ----A1: x(yz)=xy(xz)  *)
  25 (* ----3*2*U = U*U*U  *)
  26 theorem prove_equation:
  27  \forall Univ:Set.
  28 \forall f:\forall _:Univ.\forall _:Univ.Univ.
  29 \forall n1:Univ.
  30 \forall n2:Univ.
  31 \forall n3:Univ.
  32 \forall u:Univ.
  33 \forall H0:eq Univ u (f n2 n2).
  34 \forall H1:eq Univ n3 (f n2 n1).
  35 \forall H2:eq Univ n2 (f n1 n1).
  36 \forall H3:\forall X:Univ.\forall Y:Univ.\forall Z:Univ.eq Univ (f X (f Y Z)) (f (f X Y) (f X Z)).eq Univ (f (f n3 n2) u) (f (f u u) u)
  37 .
  38 intros.
  39 autobatch paramodulation timeout=100;
  40 try assumption.
  41 print proofterm.
  42 qed.
  43 (* -------------------------------------------------------------------------- *)