- new legature == for \equiv used in the notation for NPlus

[helm.git] / helm / software / matita / contribs / RELATIONAL / NPlus / fwd.ma

diff --git a/helm/software/matita/contribs/RELATIONAL/NPlus/fwd.ma b/helm/software/matita/contribs/RELATIONAL/NPlus/fwd.ma
index bae48d4051d774dccb0812918489f53243247139..9b23cb2fb3c3248d6904ac841a3da2424b0c6f17 100644 (file)
--- a/helm/software/matita/contribs/RELATIONAL/NPlus/fwd.ma
+++ b/helm/software/matita/contribs/RELATIONAL/NPlus/fwd.ma
@@ -19,15 +19,15 @@ include "NPlus/defs.ma".
 
 (* primitive generation lemmas proved by elimination and inversion *)
 
-theorem nplus_gen_zero_1: \forall q,r. NPlus zero q r \to q = r.
+theorem nplus_gen_zero_1: \forall q,r. (zero + q == r) \to q = r.
  intros. elim H; clear H q r; intros;
  [ reflexivity
  | clear H1. auto
  ].
 qed.
 
-theorem nplus_gen_succ_1: \forall p,q,r. NPlus (succ p) q r \to 
-                          \exists s. r = (succ s) \land NPlus p q s.
+theorem nplus_gen_succ_1: \forall p,q,r. ((succ p) + q == r) \to 
+                           \exists s. r = (succ s) \land (p + q == s).
  intros. elim H; clear H q r; intros;
  [
  | clear H1.
@@ -36,7 +36,7 @@ theorem nplus_gen_succ_1: \forall p,q,r. NPlus (succ p) q r \to
  ]; apply ex_intro; [| auto || auto ]. (**)
 qed.
 
-theorem nplus_gen_zero_2: \forall p,r. NPlus p zero r \to p = r.
+theorem nplus_gen_zero_2: \forall p,r. (p + zero == r) \to p = r.
  intros. inversion H; clear H; intros;
  [ auto
  | clear H H1.
@@ -44,8 +44,8 @@ theorem nplus_gen_zero_2: \forall p,r. NPlus p zero r \to p = r.
  ].
 qed.
 
-theorem nplus_gen_succ_2: \forall p,q,r. NPlus p (succ q) r \to 
-                          \exists s. r = (succ s) \land NPlus p q s.
+theorem nplus_gen_succ_2: \forall p,q,r. (p + (succ q) == r) \to 
+                           \exists s. r = (succ s) \land (p + q == s).
  intros. inversion H; clear H; intros;
  [ lapply eq_gen_succ_zero to H as H0. apply H0
  | clear H1 H3 r.
@@ -55,7 +55,8 @@ theorem nplus_gen_succ_2: \forall p,q,r. NPlus p (succ q) r \to
  ].
 qed.
 
-theorem nplus_gen_zero_3: \forall p,q. NPlus p q zero \to p = zero \land q = zero.
+theorem nplus_gen_zero_3: \forall p,q. (p + q == zero) \to 
+                           p = zero \land q = zero.
  intros. inversion H; clear H; intros;
  [ rewrite < H1. clear H1 p.
    auto
@@ -64,9 +65,9 @@ theorem nplus_gen_zero_3: \forall p,q. NPlus p q zero \to p = zero \land q = zer
  ].
 qed.
 
-theorem nplus_gen_succ_3: \forall p,q,r. NPlus p q (succ r) \to
-                          \exists s. p = succ s \land NPlus s q r \lor
-                                     q = succ s \land NPlus p s r.
+theorem nplus_gen_succ_3: \forall p,q,r. (p + q == (succ r)) \to
+                           \exists s. p = succ s \land (s + q == r) \lor
+                                      q = succ s \land (p + s == r).
  intros. inversion H; clear H; intros;
  [ rewrite < H1. clear H1 p
  | clear H1.
@@ -77,7 +78,8 @@ qed.
 (*
 (* alternative proofs invoking nplus_gen_2 *)
 
-variant nplus_gen_zero_3_alt: \forall p,q. NPlus p q zero \to p = zero \land q = zero.
+variant nplus_gen_zero_3_alt: \forall p,q. (p + q == zero) \to 
+                               p = zero \land q = zero.
  intros 2. elim q; clear q; intros;
  [ lapply linear nplus_gen_zero_2 to H as H0.
    rewrite > H0. clear H0 p.
@@ -89,9 +91,9 @@ variant nplus_gen_zero_3_alt: \forall p,q. NPlus p q zero \to p = zero \land q =
  ].
 qed.
 
-variant nplus_gen_succ_3_alt: \forall p,q,r. NPlus p q (succ r) \to
-                              \exists s. p = succ s \land NPlus s q r \lor
-                                         q = succ s \land NPlus p s r.
+variant nplus_gen_succ_3_alt: \forall p,q,r. (p + q == (succ r)) \to
+                               \exists s. p = succ s \land (s + q == r) \lor
+                                          q = succ s \land (p + s == r).
  intros 2. elim q; clear q; intros;
  [ lapply linear nplus_gen_zero_2 to H as H0.
    rewrite > H0. clear H0 p
@@ -105,7 +107,7 @@ qed.
 *)
 (* other simplification lemmas *)
 
-theorem nplus_gen_eq_2_3: \forall p,q. NPlus p q q \to p = zero.
+theorem nplus_gen_eq_2_3: \forall p,q. (p + q == q) \to p = zero.
  intros 2. elim q; clear q; intros;
  [ lapply linear nplus_gen_zero_2 to H as H0.
    rewrite > H0. clear H0 p
@@ -116,7 +118,7 @@ theorem nplus_gen_eq_2_3: \forall p,q. NPlus p q q \to p = zero.
  ]; auto.
 qed.
 
-theorem nplus_gen_eq_1_3: \forall p,q. NPlus p q p \to q = zero.
+theorem nplus_gen_eq_1_3: \forall p,q. (p + q == p) \to q = zero.
  intros 1. elim p; clear p; intros;
  [ lapply linear nplus_gen_zero_1 to H as H0.
    rewrite > H0. clear H0 q