]> matita.cs.unibo.it Git - helm.git/blob - matita/matita/contribs/TPTP/HEQ/ANA003-1.ma
commit of the "substitution" component and of some auxiliary files ...
[helm.git] / matita / matita / contribs / TPTP / HEQ / ANA003-1.ma
1 set "baseuri" "cic:/matita/TPTP/ANA003-1".
2 include "logic/equality.ma".
3
4 (* Inclusion of: ANA003-1.p *)
5
6 (* -------------------------------------------------------------------------- *)
7
8 (*  File     : ANA003-1 : TPTP v3.2.0. Released v1.0.0. *)
9
10 (*  Domain   : Analysis *)
11
12 (*  Problem  : Lemma 1 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   : [ANL] *)
23
24 (*  Names    : prob1.ver2.in [ANL] *)
25
26 (*  Status   : Unsatisfiable *)
27
28 (*  Rating   : 0.71 v3.2.0, 0.86 v3.1.0, 0.67 v2.6.0, 0.71 v2.5.0, 0.60 v2.4.0, 0.83 v2.3.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 (* ----Theorem clauses  *)
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 (add (absolute (add (f (fp33 X)) (minus l1))) (absolute (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 (* -------------------------------------------------------------------------- *)