From 25192a6604f3cb008a7c921a45d5399b8af5f889 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Thu, 21 Jul 2005 15:15:18 +0000 Subject: [PATCH] ... --- helm/matita/tests/paramodulation.ma | 31 +++++++++++++++++++++++++++++ 1 file changed, 31 insertions(+) create mode 100644 helm/matita/tests/paramodulation.ma diff --git a/helm/matita/tests/paramodulation.ma b/helm/matita/tests/paramodulation.ma new file mode 100644 index 000000000..af8d59be6 --- /dev/null +++ b/helm/matita/tests/paramodulation.ma @@ -0,0 +1,31 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/tests/paramodulation". +alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". +alias symbol "eq" (instance 0) = "leibnitz's equality". +alias symbol "plus" (instance 0) = "natural plus". +alias num (instance 0) = "natural number". +alias symbol "times" (instance 0) = "natural times". + +theorem para1: + \forall n,m,n1,m1:nat. + n=m \to n1 = m1 \to (n + n1) = (m + m1). +intros. auto. +qed. + +theorem para2: + \forall n:nat. n + n = 2 * n. +intros. auto. +qed. \ No newline at end of file -- 2.39.2