From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Sun, 20 Aug 2006 19:44:22 +0000 (+0000)
Subject: new definitions
X-Git-Tag: 0.4.95@7852~1131
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=65a362a7d62079640b6d1a759d3e33b8b3d1cd0a;p=helm.git

new definitions
---

diff --git a/matita/contribs/RELATIONAL-ARITHMETICS/BEq.ma b/matita/contribs/RELATIONAL-ARITHMETICS/BEq.ma
new file mode 100644
index 000000000..cf837aee7
--- /dev/null
+++ b/matita/contribs/RELATIONAL-ARITHMETICS/BEq.ma
@@ -0,0 +1,23 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/RELATIONAL-ARITHMETICS/BEq".
+
+include "logic/equality.ma".
+
+include "BNot.ma".
+
+inductive BEq (b1:Bool): Bool \to Bool \to Prop \def
+   | BEq_false: \forall b2. BNot b1 b2 \to BEq b1 false b2
+   | BEq_true : BEq b1 true b1.
diff --git a/matita/contribs/RELATIONAL-ARITHMETICS/BNot.ma b/matita/contribs/RELATIONAL-ARITHMETICS/BNot.ma
new file mode 100644
index 000000000..8d6405407
--- /dev/null
+++ b/matita/contribs/RELATIONAL-ARITHMETICS/BNot.ma
@@ -0,0 +1,21 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/RELATIONAL-ARITHMETICS/BNot".
+
+include "Bool.ma".
+
+inductive BNot: Bool \to Bool \to Prop \def
+   | BNot_false: BNot false true
+   | BNot_true : BNot true false.
diff --git a/matita/contribs/RELATIONAL-ARITHMETICS/Bool.ma b/matita/contribs/RELATIONAL-ARITHMETICS/Bool.ma
new file mode 100644
index 000000000..1d7b343fc
--- /dev/null
+++ b/matita/contribs/RELATIONAL-ARITHMETICS/Bool.ma
@@ -0,0 +1,19 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/RELATIONAL-ARITHMETICS/Bool".
+
+inductive Bool: Set \def
+   | false: Bool
+   | true: Bool.
diff --git a/matita/contribs/RELATIONAL-ARITHMETICS/NLE.ma b/matita/contribs/RELATIONAL-ARITHMETICS/NLE.ma
new file mode 100644
index 000000000..8e9c492c8
--- /dev/null
+++ b/matita/contribs/RELATIONAL-ARITHMETICS/NLE.ma
@@ -0,0 +1,21 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||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/RELATIONAL-ARITHMETICS/NLE".
+
+include "Nat.ma".
+
+inductive NLE: Nat \to Nat \to Prop \def
+   | NLE_zero: \forall q. NLE zero q
+   | NLE_succ: \forall p,q. NLE p q \to NLE (succ p) (succ q).
diff --git a/matita/contribs/RELATIONAL-ARITHMETICS/Nat.ma b/matita/contribs/RELATIONAL-ARITHMETICS/Nat.ma
index bc0624140..e3721fcd4 100644
--- a/matita/contribs/RELATIONAL-ARITHMETICS/Nat.ma
+++ b/matita/contribs/RELATIONAL-ARITHMETICS/Nat.ma
@@ -14,8 +14,6 @@
 
 set "baseuri" "cic:/matita/RELATIONAL-ARITHMETICS/Nat".
 
-include "logic/equality.ma".
-
 inductive Nat: Set \def
    | zero: Nat
    | succ: Nat \to Nat.
diff --git a/matita/contribs/RELATIONAL-ARITHMETICS/Nat_fwd.ma b/matita/contribs/RELATIONAL-ARITHMETICS/Nat_fwd.ma
index ede85286a..adfdcace4 100644
--- a/matita/contribs/RELATIONAL-ARITHMETICS/Nat_fwd.ma
+++ b/matita/contribs/RELATIONAL-ARITHMETICS/Nat_fwd.ma
@@ -14,6 +14,8 @@
 
 set "baseuri" "cic:/matita/RELATIONAL-ARITHMETICS/Nat_fwd".
 
+include "logic/equality.ma".
+
 include "Nat.ma".
 
 theorem eq_gen_zero_succ: \forall (P:Prop). \forall m2. zero = succ m2 \to P.
diff --git a/matita/contribs/RELATIONAL-ARITHMETICS/Plus.ma b/matita/contribs/RELATIONAL-ARITHMETICS/Plus.ma
index 5d8f4f3ec..5b86bf749 100644
--- a/matita/contribs/RELATIONAL-ARITHMETICS/Plus.ma
+++ b/matita/contribs/RELATIONAL-ARITHMETICS/Plus.ma
@@ -14,6 +14,8 @@
 
 set "baseuri" "cic:/matita/RELATIONAL-ARITHMETICS/Plus".
 
+include "logic/equality.ma".
+
 include "Nat.ma".
 
 inductive Plus (p:Nat): Nat \to Nat \to Prop \def