]> matita.cs.unibo.it Git - helm.git/blob - matitaB/matita/tests/letrecand.ma
update in basic_2
[helm.git] / matitaB / matita / tests / letrecand.ma
1 (**************************************************************************)
2 (*       ___                                                              *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||         The HELM team.                                      *)
8 (*      ||A||         http://helm.cs.unibo.it                             *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU General Public License Version 2                  *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15
16
17 include "nat/nat.ma".
18
19 let rec pari n : Prop :=
20  match n with
21   [ O ⇒ True
22   | S n ⇒ dispari n
23   ]
24 and dispari n : Prop :=
25  match n with
26   [ O => False
27   | S n => pari n
28   ].
29   
30 definition pari2 ≝
31 let rec pari n : Prop :=
32  match n with
33   [ O ⇒ True
34   | S n ⇒ dispari n
35   ]
36 and dispari n : Prop :=
37  match n with
38   [ O => False
39   | S n => pari n
40   ]
41 in pari.
42
43 definition dispari2 ≝
44 let rec pari n : Prop :=
45  match n with
46   [ O ⇒ True
47   | S n ⇒ dispari n
48   ]
49 and dispari n : Prop :=
50  match n with
51   [ O => False
52   | S n => pari n
53   ]
54 in dispari.
55
56 lemma test_pari: pari (S (S O)).
57 simplify.
58 constructor 1.
59 qed.
60
61 lemma test_pari2: pari2 (S (S O)).
62 simplify.
63 constructor 1.
64 qed.
65
66 lemma test_dispari: dispari (S O).
67 simplify.
68 constructor 1.
69 qed.
70
71 lemma test_dispari2: dispari2 (S O).
72 simplify.
73 constructor 1.
74 qed.