1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
17 include "Legacy-1/preamble.ma".
19 inductive eq (A: Set) (x: A): A \to Prop \def
20 | refl_equal: eq A x x.
22 inductive True: Prop \def
25 inductive land (A: Prop) (B: Prop): Prop \def
26 | conj: A \to (B \to (land A B)).
28 inductive or (A: Prop) (B: Prop): Prop \def
29 | or_introl: A \to (or A B)
30 | or_intror: B \to (or A B).
32 inductive ex (A: Set) (P: A \to Prop): Prop \def
33 | ex_intro: \forall (x: A).((P x) \to (ex A P)).
35 inductive ex2 (A: Set) (P: A \to Prop) (Q: A \to Prop): Prop \def
36 | ex_intro2: \forall (x: A).((P x) \to ((Q x) \to (ex2 A P Q))).
41 \lambda (A: Prop).(A \to False).
43 inductive bool: Set \def
47 inductive nat: Set \def
51 inductive le (n: nat): nat \to Prop \def
53 | le_S: \forall (m: nat).((le n m) \to (le n (S m))).
56 nat \to (nat \to Prop)
58 \lambda (n: nat).(\lambda (m: nat).(le (S n) m)).
63 \lambda (n: nat).(match n with [O \Rightarrow False | (S _) \Rightarrow
69 \lambda (n: nat).(match n with [O \Rightarrow O | (S u) \Rightarrow u]).
74 let rec plus (n: nat) on n: (nat \to nat) \def (\lambda (m: nat).(match n
75 with [O \Rightarrow m | (S p) \Rightarrow (S (plus p m))])) in plus.
80 let rec minus (n: nat) on n: (nat \to nat) \def (\lambda (m: nat).(match n
81 with [O \Rightarrow O | (S k) \Rightarrow (match m with [O \Rightarrow (S k)
82 | (S l) \Rightarrow (minus k l)])])) in minus.
84 inductive Acc (A: Set) (R: A \to (A \to Prop)): A \to Prop \def
85 | Acc_intro: \forall (x: A).(((\forall (y: A).((R y x) \to (Acc A R y)))) \to
88 definition well_founded:
89 \forall (A: Set).(((A \to (A \to Prop))) \to Prop)
91 \lambda (A: Set).(\lambda (R: ((A \to (A \to Prop)))).(\forall (a: A).(Acc A
95 \forall (A: Set).(((A \to nat)) \to (A \to (A \to Prop)))
97 \lambda (A: Set).(\lambda (f: ((A \to nat))).(\lambda (a: A).(\lambda (b:
98 A).(lt (f a) (f b))))).