From d16ded65610c520937da64721fa34879f167a943 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Tue, 10 Jul 2007 08:15:09 +0000 Subject: [PATCH] ... --- helm/software/matita/tests/bad_induction.ma | 27 +++++++++++++++++++++ 1 file changed, 27 insertions(+) create mode 100644 helm/software/matita/tests/bad_induction.ma diff --git a/helm/software/matita/tests/bad_induction.ma b/helm/software/matita/tests/bad_induction.ma new file mode 100644 index 000000000..b009e18d1 --- /dev/null +++ b/helm/software/matita/tests/bad_induction.ma @@ -0,0 +1,27 @@ +(**************************************************************************) +(* ___ *) +(* ||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/nat/bad_induction". + +include "nat/nat.ma". + +include "logic/equality.ma". + +axiom bad_ind : ∀P : nat -> Prop. ∀n.(n = O -> P n) -> (∀n.P n -> P (S n)) -> P n. + +theorem absurd: ∀n. n = O. + intros. + letin P ≝ (λx:nat. n = O). + apply (bad_ind P n); simplify; intros; autobatch. +qed. \ No newline at end of file -- 2.39.2