notational update in ground_2 and basic_2

[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / ynat / ynat_plus.ma

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 16a933acf7472d41f4d6269153c6333f919a48ef..8f1dacf6c3a7b570db1d8a38f272afeb6c4383eb 100644 (file)
--- 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: â\88\80m:ynat. â\88\80n. m + S n = ⫯(m + n).
+lemma yplus_S2: â\88\80m:ynat. â\88\80n. m + S n = â\86\91(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: â\88\80m,n. m + ⫯n = ⫯(m + n).
+lemma yplus_succ2: â\88\80m,n. m + â\86\91n = â\86\91(m + n).
 #m * //
 qed.
 
-lemma yplus_succ1: â\88\80m,n. ⫯m + n = ⫯(m + n).
+lemma yplus_succ1: â\88\80m,n. â\86\91m + n = â\86\91(m + n).
 #m * // #n elim n -n //
 qed.
 
-lemma yplus_succ_swap: â\88\80m,n. m + ⫯n = ⫯m + n.
+lemma yplus_succ_swap: â\88\80m,n. m + â\86\91n = â\86\91m + n.
 // qed.
 
-lemma yplus_SO2: â\88\80m. m + 1 = ⫯m.
+lemma yplus_SO2: â\88\80m. m + 1 = â\86\91m.
 * //
 qed.
 
@@ -93,12 +93,12 @@ qed.
 
 (* Inversion lemmas on successor *********************************************)
 
-lemma yplus_inv_succ_lt_dx: â\88\80x,y,z:ynat. 0 < y â\86\92 x + y = ⫯z â\86\92 x + â«°y = z.
+lemma yplus_inv_succ_lt_dx: â\88\80x,y,z:ynat. 0 < y â\86\92 x + y = â\86\91z â\86\92 x + â\86\93y = 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: â\88\80x,y,z:ynat. 0 < x â\86\92 x + y = ⫯z â\86\92 â«°x + y = z.
+lemma yplus_inv_succ_lt_sn: â\88\80x,y,z:ynat. 0 < x â\86\92 x + y = â\86\91z â\86\92 â\86\93x + 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: â\88\80x,y. x < y â\86\92 â\88\83â\88\83z. ⫯z + x = y & x < ∞.
+lemma ylt_inv_plus_sn: â\88\80x,y. x < y â\86\92 â\88\83â\88\83z. â\86\91z + 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: â\88\80x,y. x < y â\86\92 â\88\83â\88\83z. x + ⫯z = y & x < ∞.
+lemma ylt_inv_plus_dx: â\88\80x,y. x < y â\86\92 â\88\83â\88\83z. x + â\86\91z = 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: â\88\80x,y:ynat. 0 < x â\86\92 â«°x + y = â«°(x+y).
+lemma yplus_pred1: â\88\80x,y:ynat. 0 < x â\86\92 â\86\93x + y = â\86\93(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: â\88\80x,y:ynat. 0 < y â\86\92 x + â«°y = â«°(x+y).
+lemma yplus_pred2: â\88\80x,y:ynat. 0 < y â\86\92 x + â\86\93y = â\86\93(x+y).
 /2 width=1 by yplus_pred1/ qed-.