new results on multiple relocation

[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..0fd397829a58fea5ce1ccd2eec2b2facbe3930cf 100644 (file)
--- a/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_at.ma
+++ b/matita/matita/contribs/lambdadelta/ground_2/relocation/trace_at.ma
@@ -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.