From a023ee84b0efd8febff8bdd3cf7d92aa0317f12a Mon Sep 17 00:00:00 2001 From: Andrea Asperti Date: Fri, 26 Jun 2009 11:00:20 +0000 Subject: [PATCH] test for deep subsumption added --- helm/software/matita/tests/subsumption.ma | 54 +++++++++++++++++++++++ 1 file changed, 54 insertions(+) create mode 100644 helm/software/matita/tests/subsumption.ma diff --git a/helm/software/matita/tests/subsumption.ma b/helm/software/matita/tests/subsumption.ma new file mode 100644 index 000000000..333afdc5c --- /dev/null +++ b/helm/software/matita/tests/subsumption.ma @@ -0,0 +1,54 @@ +(**************************************************************************) +(* ___ *) +(* ||M|| *) +(* ||A|| A project by Andrea Asperti *) +(* ||T|| *) +(* ||I|| Developers: *) +(* ||T|| The HELM team. *) +(* ||A|| http://helm.cs.unibo.it *) +(* \ / *) +(* \ / This file is distributed under the terms of the *) +(* v GNU General Public License Version 2 *) +(* *) +(**************************************************************************) +include "logic/equality.ma". + +ntheorem foo : + ∀U : Type. + ∀a : U. + ∀b : U. + ∀f : U → U → U. + ∀g : U → U → U. + ∀H : ∀x.g x a = g a x. + ∃y,z. f (g y b) y = f (g z a) a. +#U. #a. #b. #f. #g. #H. +napply (ex_intro ????); +##[ ##2: napply (ex_intro ????); + ##[ ##2: nauto by H. ##| ##skip ##] ##| ##skip ##] nqed. + +ntheorem foo1 : + ∀U : Type. + ∀a : U. + ∀b : U. + ∀f : U → U → U. + ∀g : U → U → U. + ∀H : ∀x.g x a = g a x. + ∃y,z. f y (g y b) = f a (g z a). +#U. #a. #b. #f. #g. #H. +napply (ex_intro ????); +##[ ##2: napply (ex_intro ????); + ##[ ##2: nauto by H. ##| ##skip ##] ##| ##skip ##] nqed. + +ntheorem foo2 : + ∀U : Type. + ∀a : U. + ∀b : U. + ∀f : U → U → U. + ∀g : U → U → U. + ∀H : ∀x.g x a = g a x. + ∃y,z. f (g z a) (g y b) = f (g y b) (g z a). +#U. #a. #b. #f. #g. #H. +napply (ex_intro ????); +##[ ##2: napply (ex_intro ????); + ##[ ##2: nauto by H. ##| ##skip ##] ##| ##skip ##] nqed. + \ No newline at end of file -- 2.39.2