helm/software/matita/contribs/TPTP/HEQ/ANA004-1.ma

   1 set "baseuri" "cic:/matita/TPTP/ANA004-1".
   2 include "logic/equality.ma".
   3
   4 (* Inclusion of: ANA004-1.p *)
   5
   6 (* -------------------------------------------------------------------------- *)
   7
   8 (*  File     : ANA004-1 : TPTP v3.2.0. Released v1.0.0. *)
   9
  10 (*  Domain   : Analysis *)
  11
  12 (*  Problem  : Lemma 2 for the sum of two continuous functions is continuous *)
  13
  14 (*  Version  : [MOW76] axioms : Incomplete > Augmented > Complete. *)
  15
  16 (*  English  : A lemma formed by adding in some resolvants and taking out  *)
  17
  18 (*             the corresponding clauses. *)
  19
  20 (*  Refs     : [MOW76] McCharen et al. (1976), Problems and Experiments for a *)
  21
  22 (*  Source   : [TPTP] *)
  23
  24 (*  Names    :  *)
  25
  26 (*  Status   : Unsatisfiable *)
  27
  28 (*  Rating   : 0.71 v3.2.0, 0.86 v3.1.0, 0.78 v2.7.0, 0.67 v2.6.0, 0.71 v2.5.0, 0.60 v2.4.0, 1.00 v2.0.0 *)
  29
  30 (*  Syntax   : Number of clauses     :   21 (   0 non-Horn;   7 unit;  16 RR) *)
  31
  32 (*             Number of atoms       :   42 (   5 equality) *)
  33
  34 (*             Maximal clause size   :    3 (   2 average) *)
  35
  36 (*             Number of predicates  :    2 (   0 propositional; 2-2 arity) *)
  37
  38 (*             Number of functors    :   15 (   5 constant; 0-2 arity) *)
  39
  40 (*             Number of variables   :   35 (   0 singleton) *)
  41
  42 (*             Maximal term depth    :    6 (   2 average) *)
  43
  44 (*  Comments : No natural language descriptions are available. *)
  45
  46 (*           : Contributed to the ANL library by Woody Bledsoe. *)
  47
  48 (* -------------------------------------------------------------------------- *)
  49
  50 (* ----Include limits axioms  *)
  51
  52 (* Inclusion of: Axioms/ANA001-0.ax *)
  53
  54 (* -------------------------------------------------------------------------- *)
  55
  56 (*  File     : ANA001-0 : TPTP v3.2.0. Released v1.0.0. *)
  57
  58 (*  Domain   : Analysis (Limits) *)
  59
  60 (*  Axioms   : Analysis (limits) axioms for continuous functions *)
  61
  62 (*  Version  : [MOW76] axioms. *)
  63
  64 (*  English  :  *)
  65
  66 (*  Refs     : [MOW76] McCharen et al. (1976), Problems and Experiments for a *)
  67
  68 (*  Source   : [ANL] *)
  69
  70 (*  Names    :  *)
  71
  72 (*  Status   :  *)
  73
  74 (*  Syntax   : Number of clauses    :   14 (   0 non-Horn;   6 unit;   9 RR) *)
  75
  76 (*             Number of literals   :   27 (   5 equality) *)
  77
  78 (*             Maximal clause size  :    3 (   2 average) *)
  79
  80 (*             Number of predicates :    2 (   0 propositional; 2-2 arity) *)
  81
  82 (*             Number of functors   :    6 (   1 constant; 0-2 arity) *)
  83
  84 (*             Number of variables  :   27 (   0 singleton) *)
  85
  86 (*             Maximal term depth   :    3 (   1 average) *)
  87
  88 (*  Comments : No natural language descriptions are available. *)
  89
  90 (*           : "Contributed by W.W. Bledsoe in a private correspondence",  *)
  91
  92 (*             [MOW76]. *)
  93
  94 (* -------------------------------------------------------------------------- *)
  95
  96 (* ----Axiom 1  *)
  97
  98 (* ----Less than transitivity  *)
  99
 100 (* ----Axiom 2  *)
 101
 102 (* ----Axiom 3  *)
 103
 104 (* ----Axiom 4  *)
 105
 106 (* ----Axiom 5  *)
 107
 108 (* ----Axiom 6  *)
 109
 110 (* ----Axiom 7  *)
 111
 112 (* ----Axiom 8  *)
 113
 114 (* -------------------------------------------------------------------------- *)
 115
 116 (* -------------------------------------------------------------------------- *)
 117
 118 (* ----Clauses from the theorem  *)
 119 theorem c_16:
 120  ∀Univ:Set.∀X:Univ.∀Xa:Univ.∀Y:Univ.∀Z:Univ.∀a:Univ.∀absolute:∀_:Univ.Univ.∀add:∀_:Univ.∀_:Univ.Univ.∀b:Univ.∀f:∀_:Univ.Univ.∀fp31:∀_:Univ.Univ.∀fp32:∀_:Univ.Univ.∀fp33:∀_:Univ.Univ.∀g:∀_:Univ.Univ.∀half:∀_:Univ.Univ.∀l1:Univ.∀l2:Univ.∀less_than:∀_:Univ.∀_:Univ.Prop.∀minimum:∀_:Univ.∀_:Univ.Univ.∀minus:∀_:Univ.Univ.∀n0:Univ.∀H0:∀X:Univ.∀_:less_than n0 X.less_than (absolute (add (fp33 X) (minus a))) X.∀H1:less_than n0 b.∀H2:∀X:Univ.∀Y:Univ.∀_:less_than (absolute (add Y (minus a))) (fp32 X).∀_:less_than n0 X.less_than (absolute (add (g Y) (minus l2))) X.∀H3:∀X:Univ.∀_:less_than n0 X.less_than n0 (fp32 X).∀H4:∀X:Univ.∀Y:Univ.∀_:less_than (absolute (add Y (minus a))) (fp31 X).∀_:less_than n0 X.less_than (absolute (add (f Y) (minus l1))) X.∀H5:∀X:Univ.∀_:less_than n0 X.less_than n0 (fp31 X).∀H6:∀X:Univ.∀Y:Univ.eq Univ (minus (add X Y)) (add (minus X) (minus Y)).∀H7:∀Xa:Univ.∀_:less_than n0 Xa.less_than n0 (half Xa).∀H8:∀Xa:Univ.∀_:less_than n0 Xa.less_than n0 (half Xa).∀H9:∀X:Univ.∀Y:Univ.eq Univ (add X Y) (add Y X).∀H10:∀X:Univ.∀Y:Univ.∀Z:Univ.eq Univ (add (add X Y) Z) (add X (add Y Z)).∀H11:∀X:Univ.∀Xa:Univ.∀Y:Univ.∀_:less_than (add (absolute X) (absolute Y)) Xa.less_than (absolute (add X Y)) Xa.∀H12:∀X:Univ.∀Xa:Univ.∀Y:Univ.∀_:less_than Y (half Xa).∀_:less_than X (half Xa).less_than (add X Y) Xa.∀H13:∀X:Univ.∀Y:Univ.∀_:less_than n0 Y.∀_:less_than n0 X.less_than (minimum X Y) Y.∀H14:∀X:Univ.∀Y:Univ.∀_:less_than n0 Y.∀_:less_than n0 X.less_than (minimum X Y) X.∀H15:∀X:Univ.∀Y:Univ.∀_:less_than n0 Y.∀_:less_than n0 X.less_than n0 (minimum X Y).∀H16:∀X:Univ.∀Y:Univ.∀Z:Univ.∀_:less_than Y Z.∀_:less_than X Y.less_than X Z.∀H17:∀X:Univ.less_than X X.∀H18:∀X:Univ.eq Univ (add n0 X) X.∀H19:∀X:Univ.eq Univ (add X n0) X.∃X:Univ.And (less_than (absolute (add (add (f (fp33 X)) (minus l1)) (add (g (fp33 X)) (minus l2)))) b) (less_than n0 X)
 121 .
 122 intros.
 123 exists[
 124 2:
 125 autobatch depth=5 width=5 size=20 timeout=10;
 126 try assumption.
 127 |
 128 skip]
 129 print proofterm.
 130 qed.
 131
 132 (* -------------------------------------------------------------------------- *)