new definitions

diff --git a/matita/contribs/RELATIONAL-ARITHMETICS/BEq.ma b/matita/contribs/RELATIONAL-ARITHMETICS/BEq.ma
new file mode 100644 (file)
index 0000000..cf837ae
--- /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 (file)
index 0000000..8d64054
--- /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 (file)
index 0000000..1d7b343
--- /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 (file)
index 0000000..8e9c492
--- /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 bc0624140bb5bfb3d474629227a8c6a7065a8ae7..e3721fcd49aa5441d75a007bf58b7835129befe9 100644 (file)
--- 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 ede85286a5484bb044d3ccf45f90461ecce6e9d0..adfdcace434422f8434439fb1bbe9770f41aee2e 100644 (file)
--- 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 5d8f4f3ec66e0ed2fd876208f40dcbb590a1ac24..5b86bf749ce5dc0e4ce0c4d703f670a6399d3212 100644 (file)
--- 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