X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fground_2%2Fynat%2Fynat_plus.ma;h=8f1dacf6c3a7b570db1d8a38f272afeb6c4383eb;hb=397413c4196f84c81d61ba7dd79b54ab1c428ebb;hp=16a933acf7472d41f4d6269153c6333f919a48ef;hpb=24ba1bb3f67505d3e384747ff90d26d3996bd3f5;p=helm.git

diff --git a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_plus.ma b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_plus.ma
index 16a933acf..8f1dacf6c 100644
--- a/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_plus.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/ynat/ynat_plus.ma
@@ -27,7 +27,7 @@ interpretation "ynat plus" 'plus x y = (yplus x y).
 lemma yplus_O2: ∀m:ynat. m + 0 = m.
 // qed.
 
-lemma yplus_S2: ∀m:ynat. ∀n. m + S n = ⫯(m + n).
+lemma yplus_S2: ∀m:ynat. ∀n. m + S n = ↑(m + n).
 // qed.
 
 lemma yplus_Y2: ∀m:ynat. m + (∞) = ∞.
@@ -35,18 +35,18 @@ lemma yplus_Y2: ∀m:ynat. m + (∞) = ∞.
 
 (* Properties on successor **************************************************)
 
-lemma yplus_succ2: ∀m,n. m + ⫯n = ⫯(m + n).
+lemma yplus_succ2: ∀m,n. m + ↑n = ↑(m + n).
 #m * //
 qed.
 
-lemma yplus_succ1: ∀m,n. ⫯m + n = ⫯(m + n).
+lemma yplus_succ1: ∀m,n. ↑m + n = ↑(m + n).
 #m * // #n elim n -n //
 qed.
 
-lemma yplus_succ_swap: ∀m,n. m + ⫯n = ⫯m + n.
+lemma yplus_succ_swap: ∀m,n. m + ↑n = ↑m + n.
 // qed.
 
-lemma yplus_SO2: ∀m. m + 1 = ⫯m.
+lemma yplus_SO2: ∀m. m + 1 = ↑m.
 * //
 qed.
 
@@ -93,12 +93,12 @@ qed.
 
 (* Inversion lemmas on successor *********************************************)
 
-lemma yplus_inv_succ_lt_dx: ∀x,y,z:ynat. 0 < y → x + y = ⫯z → x + ⫰y = z.
+lemma yplus_inv_succ_lt_dx: ∀x,y,z:ynat. 0 < y → x + y = ↑z → x + ↓y = z.
 #x #y #z #H <(ylt_inv_O1 y) // >yplus_succ2
 /2 width=1 by ysucc_inv_inj/
 qed-.
 
-lemma yplus_inv_succ_lt_sn: ∀x,y,z:ynat. 0 < x → x + y = ⫯z → ⫰x + y = z.
+lemma yplus_inv_succ_lt_sn: ∀x,y,z:ynat. 0 < x → x + y = ↑z → ↓x + y = z.
 #x #y #z #H <(ylt_inv_O1 x) // >yplus_succ1
 /2 width=1 by ysucc_inv_inj/
 
@@ -168,13 +168,13 @@ lemma ylt_inv_plus_Y: ∀x,y. x + y < ∞ → x < ∞ ∧ y < ∞.
 #z #H elim (yplus_inv_inj … H) -H /2 width=1 by conj/
 qed-.
 
-lemma ylt_inv_plus_sn: ∀x,y. x < y → ∃∃z. ⫯z + x = y & x < ∞.
+lemma ylt_inv_plus_sn: ∀x,y. x < y → ∃∃z. ↑z + x = y & x < ∞.
 #x #y #H elim (ylt_inv_le … H) -H
 #Hx #H elim (yle_inv_plus_sn … H) -H
 /2 width=2 by ex2_intro/
 qed-.
 
-lemma ylt_inv_plus_dx: ∀x,y. x < y → ∃∃z. x + ⫯z = y & x < ∞.
+lemma ylt_inv_plus_dx: ∀x,y. x < y → ∃∃z. x + ↑z = y & x < ∞.
 #x #y #H elim (ylt_inv_plus_sn … H) -H
 #z >yplus_comm /2 width=2 by ex2_intro/
 qed-.
@@ -302,11 +302,11 @@ qed-.
 
 (* Properties on predeccessor ***********************************************)
 
-lemma yplus_pred1: ∀x,y:ynat. 0 < x → ⫰x + y = ⫰(x+y).
+lemma yplus_pred1: ∀x,y:ynat. 0 < x → ↓x + y = ↓(x+y).
 #x * // #y elim y -y // #y #IH #Hx
 >yplus_S2 >yplus_S2 >IH -IH // >ylt_inv_O1
 /2 width=1 by ylt_plus_dx1_trans/
 qed-.
 
-lemma yplus_pred2: ∀x,y:ynat. 0 < y → x + ⫰y = ⫰(x+y).
+lemma yplus_pred2: ∀x,y:ynat. 0 < y → x + ↓y = ↓(x+y).
 /2 width=1 by yplus_pred1/ qed-.