helm/software/matita/contribs/TPTP/HEQ/ANA031-2.ma

   1 set "baseuri" "cic:/matita/TPTP/ANA031-2".
   2 include "logic/equality.ma".
   3
   4 (* Inclusion of: ANA031-2.p *)
   5
   6 (* ------------------------------------------------------------------------------ *)
   7
   8 (*  File     : ANA031-2 : TPTP v3.2.0. Released v3.2.0. *)
   9
  10 (*  Domain   : Analysis *)
  11
  12 (*  Problem  : Problem about Big-O notation *)
  13
  14 (*  Version  : [Pau06] axioms : Reduced > Especial. *)
  15
  16 (*  English  :  *)
  17
  18 (*  Refs     : [Pau06] Paulson (2006), Email to G. Sutcliffe *)
  19
  20 (*  Source   : [Pau06] *)
  21
  22 (*  Names    :  *)
  23
  24 (*  Status   : Unsatisfiable *)
  25
  26 (*  Rating   : 0.43 v3.2.0 *)
  27
  28 (*  Syntax   : Number of clauses     :   11 (   0 non-Horn;   3 unit;   7 RR) *)
  29
  30 (*             Number of atoms       :   21 (   2 equality) *)
  31
  32 (*             Maximal clause size   :    4 (   2 average) *)
  33
  34 (*             Number of predicates  :    7 (   0 propositional; 1-3 arity) *)
  35
  36 (*             Number of functors    :    9 (   3 constant; 0-3 arity) *)
  37
  38 (*             Number of variables   :   32 (  20 singleton) *)
  39
  40 (*             Maximal term depth    :    6 (   2 average) *)
  41
  42 (*  Comments : The problems in the [Pau06] collection each have very many axioms, *)
  43
  44 (*             of which only a small selection are required for the refutation. *)
  45
  46 (*             The mission is to find those few axioms, after which a refutation *)
  47
  48 (*             can be quite easily found. This version has only the necessary *)
  49
  50 (*             axioms. *)
  51
  52 (* ------------------------------------------------------------------------------ *)
  53 theorem cls_conjecture_1:
  54  ∀Univ:Set.∀V_U:Univ.∀c_HOL_Oabs:∀_:Univ.∀_:Univ.Univ.∀c_lessequals:∀_:Univ.∀_:Univ.∀_:Univ.Prop.∀c_times:∀_:Univ.∀_:Univ.∀_:Univ.Univ.∀t_b:Univ.∀v_b:∀_:Univ.Univ.∀v_c:Univ.∀v_f:∀_:Univ.Univ.∀v_g:∀_:Univ.Univ.∀v_x:∀_:Univ.Univ.∀H0:∀V_U:Univ.c_lessequals (c_HOL_Oabs (v_b V_U) t_b) (c_times v_c (c_HOL_Oabs (v_g V_U) t_b) t_b) t_b.∃V_U:Univ.c_lessequals (c_times (c_HOL_Oabs (v_b (v_x V_U)) t_b) (c_HOL_Oabs (v_f (v_x V_U)) t_b) t_b) (c_times V_U (c_times (c_HOL_Oabs (v_f (v_x V_U)) t_b) (c_HOL_Oabs (v_g (v_x V_U)) t_b) t_b) t_b) t_b
  55 .
  56 intros.
  57 exists[
  58 2:
  59 autobatch depth=5 width=5 size=20 timeout=10;
  60 try assumption.
  61 |
  62 skip]
  63 print proofterm.
  64 qed.
  65
  66 (* ------------------------------------------------------------------------------ *)