- matita: computed auto traces now include the "width" parameter

[helm.git] / matita / matita / contribs / lambdadelta / ground_2 / relocation / trace_at.ma

diff --git a/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_at.ma b/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_at.ma
index b40b1c87b3be088ea46e2c08fea38a329e561cc9..02d8ac1ebae0cc17fa5cbcb1c6530362bf181d08 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_at.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_at.ma
@@ -139,7 +139,7 @@ lemma at_inv_le: ∀cs,i1,i2. @⦃i1, cs⦄ ≡ i2 → i1 ≤ ∥cs∥ ∧ i2 
 #cs #i1 #i2 #_ * /3 width=1 by le_S_S, conj/ 
 qed-.
 
-lemma at_inv_gt1: ∀cs,i1,i2. @⦃i1, cs⦄ ≡ i2 → ∥cs∥  < i1 → ⊥.
+lemma at_inv_gt1: ∀cs,i1,i2. @⦃i1, cs⦄ ≡ i2 → ∥cs∥ < i1 → ⊥.
 #cs #i1 #i2 #H elim (at_inv_le … H) -H /2 width=4 by lt_le_false/
 qed-.
 
@@ -181,7 +181,7 @@ lemma at_monotonic: ∀cs,i1,i2. @⦃i1, cs⦄ ≡ i2 → ∀j1. j1 < i1 →
 ]
 qed-.
 
-lemma at_at_dec: ∀cs,i1,i2. Decidable (@⦃i1, cs⦄ ≡ i2).
+lemma at_dec: ∀cs,i1,i2. Decidable (@⦃i1, cs⦄ ≡ i2).
 #cs elim cs -cs [ | * #cs #IH ]
 [ * [2: #i1 ] * [2,4: #i2 ]
   [4: /2 width=1 by at_empty, or_introl/
@@ -202,6 +202,27 @@ lemma at_at_dec: ∀cs,i1,i2. Decidable (@⦃i1, cs⦄ ≡ i2).
 ]
 qed-.
 
+lemma is_at_dec: ∀cs,i2. Decidable (∃i1. @⦃i1, cs⦄ ≡ i2).
+#cs elim cs -cs
+[ * /3 width=2 by ex_intro, or_introl/
+  #i2 @or_intror * /2 width=3 by at_inv_empty_succ_dx/
+| * #cs #IH * [2,4: #i2 ]
+  [ elim (IH i2) -IH
+    [ * /4 width=2 by at_succ, ex_intro, or_introl/
+    | #H @or_intror * #x #Hx
+      elim (at_inv_true_succ_dx … Hx) -Hx
+      /3 width=2 by ex_intro/
+    ]
+  | elim (IH i2) -IH
+    [ * /4 width=2 by at_false, ex_intro, or_introl/
+    | #H @or_intror * /4 width=2 by at_inv_false_S, ex_intro/ 
+    ]
+  | /3 width=2 by at_zero, ex_intro, or_introl/
+  | @or_intror * /2 width=3 by at_inv_false_O/
+  ]
+]
+qed-.
+
 (* Basic forward lemmas *****************************************************)
 
 lemma at_increasing: ∀cs,i1,i2. @⦃i1, cs⦄ ≡ i2 → i1 ≤ i2.