X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FTPTP%2FHEQ%2FANA003-1.ma;h=3cbce97a2b2cb1bead588db73aab36da11cd2a4c;hb=2af96fc83e36af5270b1181864855791ed38fbb8;hp=2190a005b249f8c9c7cac311f891f13a1ece4074;hpb=f68f477d76866de24ebdb5351912754a7dccbda5;p=helm.git

diff --git a/helm/software/matita/contribs/TPTP/HEQ/ANA003-1.ma b/helm/software/matita/contribs/TPTP/HEQ/ANA003-1.ma
index 2190a005b..3cbce97a2 100644
--- a/helm/software/matita/contribs/TPTP/HEQ/ANA003-1.ma
+++ b/helm/software/matita/contribs/TPTP/HEQ/ANA003-1.ma
@@ -117,7 +117,7 @@ include "logic/equality.ma".
 
 (* ----Theorem clauses  *)
 theorem c_16:
- ∀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 n0 X.∀_:less_than (absolute (add Y (minus a))) (fp32 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 n0 X.∀_:less_than (absolute (add Y (minus a))) (fp31 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 X (half Xa).∀_:less_than Y (half Xa).less_than (add X Y) Xa.∀H13:∀X:Univ.∀Y:Univ.∀_:less_than n0 X.∀_:less_than n0 Y.less_than (minimum X Y) Y.∀H14:∀X:Univ.∀Y:Univ.∀_:less_than n0 X.∀_:less_than n0 Y.less_than (minimum X Y) X.∀H15:∀X:Univ.∀Y:Univ.∀_:less_than n0 X.∀_:less_than n0 Y.less_than n0 (minimum X Y).∀H16:∀X:Univ.∀Y:Univ.∀Z:Univ.∀_:less_than X Y.∀_:less_than Y Z.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 n0 X) (less_than (add (absolute (add (f (fp33 X)) (minus l1))) (absolute (add (g (fp33 X)) (minus l2)))) b)
+ ∀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)
 .
 intros.
 exists[