From: Ferruccio Guidi <ferruccio.guidi@unibo.it>
Date: Fri, 25 Nov 2011 23:08:44 +0000 (+0000)
Subject: Ground_2 ported to new syntax ...
X-Git-Tag: make_still_working~2060
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=eac748dd6d912e84b3c78e682f9e40d90fb10acb;p=helm.git

Ground_2 ported to new syntax ...
---

diff --git a/matita/matita/contribs/lambda_delta/Ground_2/arith.ma b/matita/matita/contribs/lambda_delta/Ground_2/arith.ma
index 5d043c140..a6ac73c12 100644
--- a/matita/matita/contribs/lambda_delta/Ground_2/arith.ma
+++ b/matita/matita/contribs/lambda_delta/Ground_2/arith.ma
@@ -18,7 +18,7 @@ include "Ground_2/star.ma".
 (* ARITHMETICAL PROPERTIES **************************************************)
 
 lemma false_lt_to_le: ∀x,y. (x < y → False) → y ≤ x.
-#x #y #H elim (decidable_lt x y) [2: /2 width=1/ ]
+#x #y #H elim (decidable_lt x y) /2 width=1/
 #Hxy elim (H Hxy)
 qed-.
 
@@ -35,50 +35,50 @@ lemma plus_S_le_to_pos: ∀n,m,p. n + S m ≤ p → 0 < p.
 qed.
 
 lemma minus_le: ∀m,n. m - n ≤ m.
-/2/ qed.
+/2 width=1/ qed.
 
 lemma le_O_to_eq_O: ∀n. n ≤ 0 → n = 0.
-/2/ qed.
+/2 width=1/ qed.
 
 lemma lt_to_le: ∀a,b. a < b → a ≤ b.
-/2/ qed.
+/2 width=2/ qed.
 
 lemma lt_refl_false: ∀n. n < n → False.
-#n #H elim (lt_to_not_eq … H) -H /2/
+#n #H elim (lt_to_not_eq … H) -H /2 width=1/
 qed-.
 
 lemma lt_zero_false: ∀n. n < 0 → False.
-#n #H elim (lt_to_not_le … H) -H /2/
+#n #H elim (lt_to_not_le … H) -H /2 width=1/
 qed-.
 
 lemma lt_or_ge: ∀m,n. m < n ∨ n ≤ m.
-#m #n elim (decidable_lt m n) /3/
+#m #n elim (decidable_lt m n) /2 width=1/ /3 width=1/
 qed.
 
 lemma lt_or_eq_or_gt: ∀m,n. ∨∨ m < n | n = m | n < m.
 #m elim m -m
-[ * /2/
-| #m #IHm * [ /2/ ]
+[ * /2 width=1/
+| #m #IHm * /2 width=1/
   #n elim (IHm n) -IHm #H 
-  [ @or3_intro0 | @or3_intro1 destruct | @or3_intro2 ] /2/ (**) (* /3/ is slow *)
+  [ @or3_intro0 | @or3_intro1 destruct | @or3_intro2 ] // /2 width=1/ (**) (* /3 width=1/ is slow *)
 qed.
 
 lemma le_to_lt_or_eq: ∀m,n. m ≤ n → m < n ∨ m = n.
-/2/ qed. (**) (* REMOVE: this is le_to_or_lt_eq *)
+/2 width=1/ qed. (**) (* REMOVE: this is le_to_or_lt_eq *)
 
 lemma plus_le_weak: ∀m,n,p. m + n ≤ p → n ≤ p.
-/2/ qed.
+/2 width=2/ qed.
 
 lemma plus_lt_false: ∀m,n. m + n < m → False.
 #m #n #H1 lapply (le_plus_n_r n m) #H2
-lapply (le_to_lt_to_lt … H2 H1) -H2 H1 #H
+lapply (le_to_lt_to_lt … H2 H1) -H2 -H1 #H
 elim (lt_refl_false … H)
 qed-.
 
 lemma le_fwd_plus_plus_ge: ∀m1,m2. m2 ≤ m1 → ∀n1,n2. m1 + n1 ≤ m2 + n2 → n1 ≤ n2.
-#m1 #m2 #H elim H -H m1
-[ /2/
-| #m1 #_ #IHm1 #n1 #n2 #H @IHm1 /2/
+#m1 #m2 #H elim H -m1
+[ /2 width=2/
+| #m1 #_ #IHm1 #n1 #n2 #H @IHm1 /2 width=1/
 ]
 qed.
 
@@ -88,10 +88,10 @@ lemma monotonic_lt_minus_l: ∀p,q,n. n ≤ q → q < p → q - n < p - n.
 qed.
 
 lemma plus_le_minus: ∀a,b,c. a + b ≤ c → a ≤ c - b.
-/2/ qed.
+/2 width=1/ qed.
 
 lemma lt_plus_minus: ∀i,u,d. u ≤ i → i < d + u → i - u < d.
-/2/ qed.
+/2 width=1/ qed.
 
 lemma plus_plus_comm_23: ∀m,n,p. m + n + p = m + p + n.
 // qed.
@@ -107,7 +107,7 @@ lemma minus_le_minus_minus_comm: ∀b,c,a. c ≤ b → a - (b - c) = a + c - b.
 | #b #IHb #c elim c -c //
   #c #_ #a #Hcb
   lapply (le_S_S_to_le … Hcb) -Hcb #Hcb
-  <plus_n_Sm normalize /2/
+  <plus_n_Sm normalize /2 width=1/
 ]
 qed.
 
@@ -115,26 +115,26 @@ lemma minus_plus_comm: ∀a,b,c. a - b - c = a - (c + b).
 // qed.
 
 lemma minus_minus_comm: ∀a,b,c. a - b - c = a - c - b.
-/3/ qed.
+/3 width=1/ qed.
 
 lemma le_plus_minus: ∀a,b,c. c ≤ b → a + b - c = a + (b - c).
-/2/ qed.
+/2 width=1/ qed.
 
 lemma plus_minus_m_m_comm: ∀n,m. m ≤ n → n = m + (n - m).
-/2/ qed.
+/2 width=1/ qed.
 
 lemma minus_plus_m_m_comm: ∀n,m. n = (m + n) - m.
-/2/ qed.
+/2 width=1/ qed.
 
 lemma arith_a2: ∀a,c1,c2. c1 + c2 ≤ a → a - c1 - c2 + (c1 + c2) = a.
-/2/ qed.
+/2 width=1/ qed.
 
 lemma arith_b1: ∀a,b,c1. c1 ≤ b → a - c1 - (b - c1) = a - b.
-#a #b #c1 #H >minus_plus @eq_f2 /2/
+#a #b #c1 #H >minus_plus @eq_f2 /2 width=1/
 qed.
 
 lemma arith_b2: ∀a,b,c1,c2. c1 + c2 ≤ b → a - c1 - c2 - (b - c1 - c2) = a - b.
-#a #b #c1 #c2 #H >minus_plus >minus_plus >minus_plus /2/
+#a #b #c1 #c2 #H >minus_plus >minus_plus >minus_plus /2 width=1/
 qed.
 
 lemma arith_c1: ∀a,b,c1. a + c1 - (b + c1) = a - b.
@@ -145,25 +145,25 @@ lemma arith_c1x: ∀x,a,b,c1. x + c1 + a - (b + c1) = x + a - b.
 qed.
 
 lemma arith_d1: ∀a,b,c1. c1 ≤ b → a + c1 + (b - c1) = a + b.
-/2/ qed.
+/2 width=1/ qed.
 
 lemma arith_e2: ∀a,c1,c2. a ≤ c1 → c1 + c2 - (c1 - a + c2) = a.
-/3/ qed.
+/3 width=1/ qed.
 
 lemma arith_f1: ∀a,b,c1. a + b ≤ c1 → c1 - (c1 - a - b) = a + b.
 #a #b #c1 #H >minus_plus <minus_minus //
 qed.
 
 lemma arith_g1: ∀a,b,c1. c1 ≤ b → a - (b - c1) - c1 = a - b.
-/2/ qed.
+/2 width=1/ qed.
 
 lemma arith_h1: ∀a1,a2,b,c1. c1 ≤ a1 → c1 ≤ b →
                 a1 - c1 + a2 - (b - c1) = a1 + a2 - b.
-#a1 #a2 #b #c1 #H1 #H2 <le_plus_minus_comm /2/
+#a1 #a2 #b #c1 #H1 #H2 <le_plus_minus_comm /2 width=1/
 qed.
 
 lemma arith_i2: ∀a,c1,c2. c1 + c2 ≤ a → c1 + c2 + (a - c1 - c2) = a.
-/2/ qed.
+/2 width=1/ qed.
 
 lemma arith_z1: ∀a,b,c1. a + c1 - b - c1 = a - b.
 // qed.
@@ -171,17 +171,17 @@ lemma arith_z1: ∀a,b,c1. a + c1 - b - c1 = a - b.
 (* unstable *****************************************************************)
 
 lemma arith1: ∀n,h,m,p. n + h + m ≤ p + h → n + m ≤ p.
-/2/ qed.
+/2 width=2/ qed.
 
 lemma arith2: ∀j,i,e,d. d + e ≤ i → d ≤ i - e + j.
-#j #i #e #d #H lapply (plus_le_minus … H) -H /2/
+#j #i #e #d #H lapply (plus_le_minus … H) -H /2 width=3/
 qed.
 
 lemma arith3: ∀a1,a2,b,c1. a1 + a2 ≤ b → a1 + c1 + a2 ≤ b + c1.
-/2/ qed.
+/2 width=1/ qed.
 
 lemma arith4: ∀h,d,e1,e2. d ≤ e1 + e2 → d + h ≤ e1 + h + e2.
-/2/ qed.
+/2 width=1/ qed.
 
 lemma arith5: ∀a,b1,b2,c1. c1 ≤ b1 → c1 ≤ a → a < b1 + b2 → a - c1 < b1 - c1 + b2.
 #a #b1 #b2 #c1 #H1 #H2 #H3
diff --git a/matita/matita/contribs/lambda_delta/Ground_2/star.ma b/matita/matita/contribs/lambda_delta/Ground_2/star.ma
index 097151367..ee6a901e8 100644
--- a/matita/matita/contribs/lambda_delta/Ground_2/star.ma
+++ b/matita/matita/contribs/lambda_delta/Ground_2/star.ma
@@ -33,63 +33,63 @@ definition transitive: ∀A. ∀R1,R2: relation A. Prop ≝ λA,R1,R2.
 lemma TC_strip1: ∀A,R1,R2. confluent A R1 R2 →
                  ∀a0,a1. TC … R1 a0 a1 → ∀a2. R2 a0 a2 →
                  ∃∃a. R2 a1 a & TC … R1 a2 a.
-#A #R1 #R2 #HR12 #a0 #a1 #H elim H -H a1
+#A #R1 #R2 #HR12 #a0 #a1 #H elim H -a1
 [ #a1 #Ha01 #a2 #Ha02
-  elim (HR12 … Ha01 … Ha02) -HR12 a0 /3/
+  elim (HR12 … Ha01 … Ha02) -HR12 -a0 /3 width=3/
 | #a #a1 #_ #Ha1 #IHa0 #a2 #Ha02
-  elim (IHa0 … Ha02) -IHa0 Ha02 a0 #a0 #Ha0 #Ha20
-  elim (HR12 … Ha1 … Ha0) -HR12 a /4/
+  elim (IHa0 … Ha02) -a0 #a0 #Ha0 #Ha20
+  elim (HR12 … Ha1 … Ha0) -HR12 -a /4 width=3/
 ]
 qed.
 
 lemma TC_strip2: ∀A,R1,R2. confluent A R1 R2 →
                  ∀a0,a2. TC … R2 a0 a2 → ∀a1. R1 a0 a1 →
                  ∃∃a. TC … R2 a1 a & R1 a2 a.
-#A #R1 #R2 #HR12 #a0 #a2 #H elim H -H a2
+#A #R1 #R2 #HR12 #a0 #a2 #H elim H -a2
 [ #a2 #Ha02 #a1 #Ha01
-  elim (HR12 … Ha01 … Ha02) -HR12 a0 /3/
+  elim (HR12 … Ha01 … Ha02) -HR12 -a0 /3 width=3/
 | #a #a2 #_ #Ha2 #IHa0 #a1 #Ha01
-  elim (IHa0 … Ha01) -IHa0 Ha01 a0 #a0 #Ha10 #Ha0
-  elim (HR12 … Ha0 … Ha2) -HR12 a /4/
+  elim (IHa0 … Ha01) -a0 #a0 #Ha10 #Ha0
+  elim (HR12 … Ha0 … Ha2) -HR12 -a /4 width=3/
 ]
 qed.
 
 lemma TC_confluent: ∀A,R1,R2.
                     confluent A R1 R2 → confluent A (TC … R1) (TC … R2).
-#A #R1 #R2 #HR12 #a0 #a1 #H elim H -H a1
+#A #R1 #R2 #HR12 #a0 #a1 #H elim H -a1
 [ #a1 #Ha01 #a2 #Ha02
-  elim (TC_strip2 … HR12 … Ha02 … Ha01) -HR12 a0 /3/
+  elim (TC_strip2 … HR12 … Ha02 … Ha01) -HR12 -a0 /3 width=3/
 | #a #a1 #_ #Ha1 #IHa0 #a2 #Ha02
-  elim (IHa0 … Ha02) -IHa0 Ha02 a0 #a0 #Ha0 #Ha20
-  elim (TC_strip2 … HR12 … Ha0 … Ha1) -HR12 a /4/
+  elim (IHa0 … Ha02) -a0 #a0 #Ha0 #Ha20
+  elim (TC_strip2 … HR12 … Ha0 … Ha1) -HR12 -a /4 width=3/
 ]
 qed.
 
 lemma TC_strap: ∀A. ∀R:relation A. ∀a1,a,a2.
                 R a1 a → TC … R a a2 → TC … R a1 a2.
-/3/ qed.
+/3 width=3/ qed.
 
 lemma TC_strap1: ∀A,R1,R2. transitive A R1 R2 →
                  ∀a1,a0. TC … R1 a1 a0 → ∀a2. R2 a0 a2 →
                  ∃∃a. R2 a1 a & TC … R1 a a2.
-#A #R1 #R2 #HR12 #a1 #a0 #H elim H -H a0
+#A #R1 #R2 #HR12 #a1 #a0 #H elim H -a0
 [ #a0 #Ha10 #a2 #Ha02
-  elim (HR12 … Ha10 … Ha02) -HR12 a0 /3/
+  elim (HR12 … Ha10 … Ha02) -HR12 -a0 /3 width=3/
 | #a #a0 #_ #Ha0 #IHa #a2 #Ha02
-  elim (HR12 … Ha0 … Ha02) -HR12 a0 #a0 #Ha0 #Ha02
-  elim (IHa … Ha0) -a /4/
+  elim (HR12 … Ha0 … Ha02) -HR12 -a0 #a0 #Ha0 #Ha02
+  elim (IHa … Ha0) -a /4 width=3/
 ]
 qed.
 
 lemma TC_strap2: ∀A,R1,R2. transitive A R1 R2 →
                  ∀a0,a2. TC … R2 a0 a2 → ∀a1. R1 a1 a0 →
                  ∃∃a. TC … R2 a1 a & R1 a a2.
-#A #R1 #R2 #HR12 #a0 #a2 #H elim H -H a2
+#A #R1 #R2 #HR12 #a0 #a2 #H elim H -a2
 [ #a2 #Ha02 #a1 #Ha10
-  elim (HR12 … Ha10 … Ha02) -HR12 a0 /3/
+  elim (HR12 … Ha10 … Ha02) -HR12 -a0 /3 width=3/
 | #a #a2 #_ #Ha02 #IHa #a1 #Ha10
   elim (IHa … Ha10) -a0 #a0 #Ha10 #Ha0
-  elim (HR12 … Ha0 … Ha02) -HR12 a /4/
+  elim (HR12 … Ha0 … Ha02) -HR12 -a /4 width=3/
 ]
 qed.
 
@@ -97,20 +97,20 @@ lemma TC_transitive: ∀A,R1,R2.
                      transitive A R1 R2 → transitive A (TC … R1) (TC … R2).
 #A #R1 #R2 #HR12 #a1 #a0 #H elim H -a0
 [ #a0 #Ha10 #a2 #Ha02
-  elim (TC_strap2 … HR12 … Ha02 … Ha10) -HR12 a0 /3/
+  elim (TC_strap2 … HR12 … Ha02 … Ha10) -HR12 -a0 /3 width=3/
 | #a #a0 #_ #Ha0 #IHa #a2 #Ha02
-  elim (TC_strap2 … HR12 … Ha02 … Ha0) -HR12 a0 #a0 #Ha0 #Ha02
-  elim (IHa … Ha0) -a /4/
+  elim (TC_strap2 … HR12 … Ha02 … Ha0) -HR12 -a0 #a0 #Ha0 #Ha02
+  elim (IHa … Ha0) -a /4 width=3/
 ]
 qed.
 
 lemma TC_reflexive: ∀A,R. reflexive A R → reflexive A (TC … R).
-/2/ qed.
+/2 width=1/ qed.
 
 lemma TC_star_ind: ∀A,R. reflexive A R → ∀a1. ∀P:predicate A.
                    P a1 → (∀a,a2. TC … R a1 a → R a a2 → P a → P a2) →
                    ∀a2. TC … R a1 a2 → P a2.
-#A #R #H #a1 #P #Ha1 #IHa1 #a2 #Ha12 elim Ha12 -Ha12 a2 /3/
+#A #R #H #a1 #P #Ha1 #IHa1 #a2 #Ha12 elim Ha12 -a2 /3 width=4/
 qed.
 
 definition NF: ∀A. relation A → relation A → predicate A ≝
@@ -123,5 +123,5 @@ inductive SN (A) (R,S:relation A): predicate A ≝
 lemma NF_to_SN: ∀A,R,S,a. NF A R S a → SN A R S a.
 #A #R #S #a1 #Ha1
 @SN_intro #a2 #HRa12 #HSa12
-elim (HSa12 ?) -HSa12 /2/
+elim (HSa12 ?) -HSa12 /2 width=1/
 qed.
diff --git a/matita/matita/contribs/lambda_delta/Ground_2/xoa_props.ma b/matita/matita/contribs/lambda_delta/Ground_2/xoa_props.ma
index c2d7e2f41..121eb7e74 100644
--- a/matita/matita/contribs/lambda_delta/Ground_2/xoa_props.ma
+++ b/matita/matita/contribs/lambda_delta/Ground_2/xoa_props.ma
@@ -16,5 +16,5 @@ include "Ground_2/xoa_notation.ma".
 include "Ground_2/xoa.ma".
 
 lemma ex2_1_comm: ∀A0. ∀P0,P1:A0→Prop. (∃∃x0. P0 x0 & P1 x0) → ∃∃x0. P1 x0 & P0 x0.
-#A0 #P0 #P1 * /2/
+#A0 #P0 #P1 * /2 width=3/
 qed.