From 1994fe8e6355243652770f53a02db5fdf26915f0 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Sat, 7 Mar 2015 15:47:23 +0000 Subject: [PATCH] performance data for basic_1 on dev.helm --- .../lambdadelta/basic_1/etc/performance.txt | 20 +++++++++++++------ .../contribs/lambdadelta/legacy_1/coq/fwd.ma | 2 +- 2 files changed, 15 insertions(+), 7 deletions(-) diff --git a/matita/matita/contribs/lambdadelta/basic_1/etc/performance.txt b/matita/matita/contribs/lambdadelta/basic_1/etc/performance.txt index a4972af9c..6c46086ea 100644 --- a/matita/matita/contribs/lambdadelta/basic_1/etc/performance.txt +++ b/matita/matita/contribs/lambdadelta/basic_1/etc/performance.txt @@ -1,9 +1,17 @@ -full validation of lambdadelta_1 on "monica" - -date: ven 6 mar 2015, 20.31.46, CET +full validation of lambdadelta_1 command: time ../../matitac.opt basic_1 -real 4m39.904s -user 3m58.580s -sys 0m11.473s +- machine: "monica" + date : ven 6 mar 2015, 20.31.46, CET + + real 4m39.904s + user 3m58.580s + sys 0m11.473s + +- machine: "dev.helm" + date : Sat Mar 7 16:41:46 CET 2015 + + real 30m36.357s + user 6m35.749s + sys 0m31.518s diff --git a/matita/matita/contribs/lambdadelta/legacy_1/coq/fwd.ma b/matita/matita/contribs/lambdadelta/legacy_1/coq/fwd.ma index 8738e7234..518bb5ff0 100644 --- a/matita/matita/contribs/lambdadelta/legacy_1/coq/fwd.ma +++ b/matita/matita/contribs/lambdadelta/legacy_1/coq/fwd.ma @@ -90,5 +90,5 @@ let rec Acc_ind (A: Type[0]) (R: (A \to (A \to Prop))) (P: (A \to Prop)) (f: (\forall (x: A).(((\forall (y: A).((R y x) \to (Acc A R y)))) \to (((\forall (y: A).((R y x) \to (P y)))) \to (P x))))) (a: A) (a0: Acc A R a) on a0: P a \def match a0 with [(Acc_intro x a1) \Rightarrow (f x a1 (\lambda (y: -A).(\lambda (r: (R y x)).((Acc_ind A R P f) y (a1 y r)))))]. +A).(\lambda (r0: (R y x)).((Acc_ind A R P f) y (a1 y r0)))))]. -- 2.39.2