From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Fri, 6 Mar 2015 19:37:30 +0000 (+0000)
Subject: with matita 0.99.2 we can validate lambdadelta_1 (as is) in 4 minutes
X-Git-Tag: make_still_working~726
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=78d9265b6261eb24cad483fb57a386e39eae6a3c;p=helm.git

with matita 0.99.2 we can validate lambdadelta_1 (as is) in 4 minutes
---

diff --git a/matita/matita/contribs/lambdadelta/basic_1/etc/performance.txt b/matita/matita/contribs/lambdadelta/basic_1/etc/performance.txt
new file mode 100644
index 000000000..a4972af9c
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_1/etc/performance.txt
@@ -0,0 +1,9 @@
+full validation of lambdadelta_1 on "monica"
+
+date: ven  6 mar 2015, 20.31.46, CET
+
+command: time ../../matitac.opt basic_1
+
+real    4m39.904s
+user    3m58.580s
+sys     0m11.473s
diff --git a/matita/matita/contribs/lambdadelta/basic_1/etc/planes.txt b/matita/matita/contribs/lambdadelta/basic_1/etc/planes.txt
new file mode 100644
index 000000000..d4b66b373
--- /dev/null
+++ b/matita/matita/contribs/lambdadelta/basic_1/etc/planes.txt
@@ -0,0 +1,13 @@
+T s tlist tlt iso
+C r flt app
+lift cnt drop clear getl clen cimp
+lift1 drop1
+subst0 subst1 subst csubst0 csubst1 fsubst0 
+G next_plus
+sty0 sty1
+A asucc aplus leq llt aprem ex0 
+pr0 wcpr0 pr1 pr2 pr3 
+csubv arity csuba
+nf2 sn3 sc3 csubc ex2
+pc1 pc3
+ty3 csubt wf3 ex1
diff --git a/matita/matita/contribs/lambdadelta/basic_1/planes.txt b/matita/matita/contribs/lambdadelta/basic_1/planes.txt
deleted file mode 100644
index d4b66b373..000000000
--- a/matita/matita/contribs/lambdadelta/basic_1/planes.txt
+++ /dev/null
@@ -1,13 +0,0 @@
-T s tlist tlt iso
-C r flt app
-lift cnt drop clear getl clen cimp
-lift1 drop1
-subst0 subst1 subst csubst0 csubst1 fsubst0 
-G next_plus
-sty0 sty1
-A asucc aplus leq llt aprem ex0 
-pr0 wcpr0 pr1 pr2 pr3 
-csubv arity csuba
-nf2 sn3 sc3 csubc ex2
-pc1 pc3
-ty3 csubt wf3 ex1