--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground_2/relocation/rtmap_tl.ma".
+
+(* RELOCATION MAP ***********************************************************)
+
+inductive le (f1): predicate rtmap ≝
+| le_eq: ∀f2. f1 ≗ f2 → le f1 f2
+| le_tl: ∀f2,g2. le f1 f2 → ↓g2 = f2 → le f1 g2
+.
+
+interpretation "less or equal to (rtmap)" 'leq x y = (le x y).
+
+(* Basic properties *********************************************************)
+
+lemma le_refl: reflexive … le.
+/2 width=1 by eq_refl, le_eq/ qed.
+
+lemma le_eq_repl_back_dx: ∀f1. eq_repl_back (λf2. f1 ≤ f2).
+#f #f1 #Hf1 elim Hf1 -f1
+/4 width=3 by le_tl, le_eq, tl_eq_repl, eq_trans/
+qed-.
+
+lemma le_eq_repl_fwd_dx: ∀f1. eq_repl_fwd (λf2. f1 ≤ f2).
+#f1 @eq_repl_sym /2 width=3 by le_eq_repl_back_dx/
+qed-.
+
+lemma le_eq_repl_back_sn: ∀f2. eq_repl_back (λf1. f1 ≤ f2).
+#f #f1 #Hf1 elim Hf1 -f
+/4 width=3 by le_tl, le_eq, tl_eq_repl, eq_canc_sn/
+qed-.
+
+lemma le_eq_repl_fwd_sn: ∀f2. eq_repl_fwd (λf1. f1 ≤ f2).
+#f2 @eq_repl_sym /2 width=3 by le_eq_repl_back_sn/
+qed-.
+
+lemma le_tl_comp: ∀f1,f2. f1 ≤ f2 → ∀g1,g2. ↓f1 = g1 → ↓f2 = g2 → g1 ≤ g2.
+#f1 #f2 #H elim H -f2
+/3 width=3 by le_tl, le_eq, tl_eq_repl/
+qed.
+
+(* Main properties **********************************************************)
+
+theorem le_trans: Transitive … le.
+#f1 #f #H elim H -f
+/4 width=5 by le_tl_comp, le_eq_repl_fwd_sn, le_tl/
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground_2/notation/functions/norm_1.ma".
+include "ground_2/lib/bool.ma".
+include "ground_2/lib/list.ma".
+
+(* RELOCATION TRACE *********************************************************)
+
+definition trace: Type[0] ≝ list bool.
+
+let rec colength (cs:trace) on cs ≝ match cs with
+[ nil ⇒ 0
+| cons b tl ⇒ match b with [ true ⇒ ⫯(colength tl) | false ⇒ colength tl ]
+].
+
+interpretation "colength (trace)"
+ 'Norm cs = (colength cs).
+
+(* basic properties *********************************************************)
+
+lemma colength_empty: ∥◊∥ = 0.
+// qed.
+
+lemma colength_true: ∀cs. ∥Ⓣ@cs∥ = ⫯∥cs∥.
+// qed.
+
+lemma colength_false: ∀cs. ∥Ⓕ@cs∥ = ∥cs∥.
+// qed.
+
+lemma colength_cons: ∀cs1,cs2. ∥cs1∥ = ∥cs2∥ →
+ ∀b. ∥b@cs1∥ = ∥b@cs2∥.
+#cs1 #cs2 #H * /2 width=1 by/
+qed.
+
+lemma colength_le: ∀cs. ∥cs∥ ≤ |cs|.
+#cs elim cs -cs //
+* /2 width=1 by le_S_S, le_S/
+qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground_2/notation/relations/rafter_3.ma".
+include "ground_2/relocation/trace_at.ma".
+
+(* RELOCATION TRACE *********************************************************)
+
+inductive after: relation3 trace trace trace ≝
+ | after_empty: after (◊) (◊) (◊)
+ | after_true : ∀cs1,cs2,cs. after cs1 cs2 cs →
+ ∀b. after (Ⓣ @ cs1) (b @ cs2) (b @ cs)
+ | after_false: ∀cs1,cs2,cs. after cs1 cs2 cs →
+ after (Ⓕ @ cs1) cs2 (Ⓕ @ cs).
+
+interpretation "composition (trace)"
+ 'RAfter cs1 cs2 cs = (after cs1 cs2 cs).
+
+(* Basic properties *********************************************************)
+
+lemma after_length: ∀cs1,cs2. ∥cs1∥ = |cs2| →
+ ∃∃cs. cs1 ⊚ cs2 ≡ cs & |cs| = |cs1| & ∥cs∥ = ∥cs2∥.
+#cs1 elim cs1 -cs1
+[ #cs2 #H >(length_inv_zero_sn … H) -cs2 /2 width=4 by after_empty, ex3_intro/
+| * #cs1 #IH #cs2 #Hcs
+ [ elim (length_inv_succ_sn … Hcs) -Hcs
+ #tl #b #Hcs #H destruct
+ ]
+ elim (IH … Hcs) -IH -Hcs
+ #cs #Hcs #H1 #H2 [ @(ex3_intro … (b@cs)) | @(ex3_intro … (Ⓕ@cs)) ] /2 width=1 by after_true, after_false, colength_cons/
+]
+qed-.
+
+(* Basic inversion lemmas ***************************************************)
+
+fact after_inv_empty1_aux: ∀cs1,cs2,cs. cs1 ⊚ cs2 ≡ cs → cs1 = ◊ →
+ cs2 = ◊ ∧ cs = ◊.
+#cs1 #cs2 #cs * -cs1 -cs2 -cs
+[ /2 width=1 by conj/
+| #cs1 #cs2 #cs #_ #b #H destruct
+| #cs1 #cs2 #cs #_ #H destruct
+]
+qed-.
+
+lemma after_inv_empty1: ∀cs2,cs. ◊ ⊚ cs2 ≡ cs → cs2 = ◊ ∧ cs = ◊.
+/2 width=3 by after_inv_empty1_aux/ qed-.
+
+fact after_inv_true1_aux: ∀cs1,cs2,cs. cs1 ⊚ cs2 ≡ cs → ∀tl1. cs1 = Ⓣ @ tl1 →
+ ∃∃tl2,tl,b. cs2 = b @ tl2 & cs = b @ tl & tl1 ⊚ tl2 ≡ tl.
+#cs1 #cs2 #cs * -cs1 -cs2 -cs
+[ #tl1 #H destruct
+| #cs1 #cs2 #cs #H12 #b #tl1 #H destruct
+ /2 width=6 by ex3_3_intro/
+| #cs1 #cs2 #cs #_ #tl1 #H destruct
+]
+qed-.
+
+lemma after_inv_true1: ∀tl1,cs2,cs. (Ⓣ @ tl1) ⊚ cs2 ≡ cs →
+ ∃∃tl2,tl,b. cs2 = b @ tl2 & cs = b @ tl & tl1 ⊚ tl2 ≡ tl.
+/2 width=3 by after_inv_true1_aux/ qed-.
+
+fact after_inv_false1_aux: ∀cs1,cs2,cs. cs1 ⊚ cs2 ≡ cs → ∀tl1. cs1 = Ⓕ @ tl1 →
+ ∃∃tl. cs = Ⓕ @ tl & tl1 ⊚ cs2 ≡ tl.
+#cs1 #cs2 #cs * -cs1 -cs2 -cs
+[ #tl1 #H destruct
+| #cs1 #cs2 #cs #_ #b #tl1 #H destruct
+| #cs1 #cs2 #cs #H12 #tl1 #H destruct
+ /2 width=3 by ex2_intro/
+]
+qed-.
+
+lemma after_inv_false1: ∀tl1,cs2,cs. (Ⓕ @ tl1) ⊚ cs2 ≡ cs →
+ ∃∃tl. cs = Ⓕ @ tl & tl1 ⊚ cs2 ≡ tl.
+/2 width=3 by after_inv_false1_aux/ qed-.
+
+fact after_inv_empty3_aux: ∀cs1,cs2,cs. cs1 ⊚ cs2 ≡ cs → cs = ◊ →
+ cs1 = ◊ ∧ cs2 = ◊.
+#cs1 #cs2 #cs * -cs1 -cs2 -cs
+[ /2 width=1 by conj/
+| #cs1 #cs2 #cs #_ #b #H destruct
+| #cs1 #cs2 #cs #_ #H destruct
+]
+qed-.
+
+lemma after_inv_empty3: ∀cs1,cs2. cs1 ⊚ cs2 ≡ ◊ → cs1 = ◊ ∧ cs2 = ◊.
+/2 width=3 by after_inv_empty3_aux/ qed-.
+
+fact after_inv_inh3_aux: ∀cs1,cs2,cs. cs1 ⊚ cs2 ≡ cs → ∀tl,b. cs = b @ tl →
+ (∃∃tl1,tl2. cs1 = Ⓣ @ tl1 & cs2 = b @ tl2 & tl1 ⊚ tl2 ≡ tl) ∨
+ ∃∃tl1. cs1 = Ⓕ @ tl1 & b = Ⓕ & tl1 ⊚ cs2 ≡ tl.
+#cs1 #cs2 #cs * -cs1 -cs2 -cs
+[ #tl #b #H destruct
+| #cs1 #cs2 #cs #H12 #b0 #tl #b #H destruct
+ /3 width=5 by ex3_2_intro, or_introl/
+| #cs1 #cs2 #cs #H12 #tl #b #H destruct
+ /3 width=3 by ex3_intro, or_intror/
+]
+qed-.
+
+lemma after_inv_inh3: ∀cs1,cs2,tl,b. cs1 ⊚ cs2 ≡ b @ tl →
+ (∃∃tl1,tl2. cs1 = Ⓣ @ tl1 & cs2 = b @ tl2 & tl1 ⊚ tl2 ≡ tl) ∨
+ ∃∃tl1. cs1 = Ⓕ @ tl1 & b = Ⓕ & tl1 ⊚ cs2 ≡ tl.
+/2 width=3 by after_inv_inh3_aux/ qed-.
+
+lemma after_inv_true3: ∀cs1,cs2,tl. cs1 ⊚ cs2 ≡ Ⓣ @ tl →
+ ∃∃tl1,tl2. cs1 = Ⓣ @ tl1 & cs2 = Ⓣ @ tl2 & tl1 ⊚ tl2 ≡ tl.
+#cs1 #cs2 #tl #H elim (after_inv_inh3 … H) -H // *
+#tl1 #_ #H destruct
+qed-.
+
+lemma after_inv_false3: ∀cs1,cs2,tl. cs1 ⊚ cs2 ≡ Ⓕ @ tl →
+ (∃∃tl1,tl2. cs1 = Ⓣ @ tl1 & cs2 = Ⓕ @ tl2 & tl1 ⊚ tl2 ≡ tl) ∨
+ ∃∃tl1. cs1 = Ⓕ @ tl1 & tl1 ⊚ cs2 ≡ tl.
+#cs1 #cs2 #tl #H elim (after_inv_inh3 … H) -H /2 width=1 by or_introl/ * /3 width=3 by ex2_intro, or_intror/
+qed-.
+
+lemma after_inv_length: ∀cs1,cs2,cs. cs1 ⊚ cs2 ≡ cs →
+ ∧∧ ∥cs1∥ = |cs2| & |cs| = |cs1| & ∥cs∥ = ∥cs2∥.
+#cs1 #cs2 #cs #H elim H -cs1 -cs2 -cs /2 width=1 by and3_intro/
+#cs1 #cs2 #cs #_ [ * ] * /2 width=1 by and3_intro/
+qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma after_at_fwd: ∀cs1,cs2,cs. cs2 ⊚ cs1 ≡ cs → ∀i1,i. @⦃i1, cs⦄ ≡ i →
+ ∃∃i2. @⦃i1, cs1⦄ ≡ i2 & @⦃i2, cs2⦄ ≡ i.
+#cs1 #cs2 #cs #H elim H -cs1 -cs2 -cs
+[ #i1 #i #H elim (at_inv_empty … H) -H
+ #H1 #H2 destruct /2 width=3 by at_empty, ex2_intro/
+| #cs1 #cs2 #cs #_ * #IH #i1 #i #H
+ [ elim (at_inv_true … H) -H *
+ [ -IH #H1 #H2 destruct /2 width=3 by at_zero, ex2_intro/
+ | #j1 #j #H1 #H2 #Hj1 destruct
+ elim (IH … Hj1) -IH -Hj1 /3 width=3 by at_succ, ex2_intro/
+ ]
+ | elim (at_inv_false … H) -H
+ #j #H #Hj destruct
+ elim (IH … Hj) -IH -Hj /3 width=3 by at_succ, at_false, ex2_intro/
+ ]
+| #cs1 #cs2 #cs #_ #IH #i1 #i #H elim (at_inv_false … H) -H
+ #j #H #Hj destruct
+ elim (IH … Hj) -IH -Hj /3 width=3 by at_false, ex2_intro/
+]
+qed-.
+
+lemma after_at1_fwd: ∀cs1,cs2,cs. cs2 ⊚ cs1 ≡ cs → ∀i1,i2. @⦃i1, cs1⦄ ≡ i2 →
+ ∃∃i. @⦃i2, cs2⦄ ≡ i & @⦃i1, cs⦄ ≡ i.
+#cs1 #cs2 #cs #H elim H -cs1 -cs2 -cs
+[ #i1 #i2 #H elim (at_inv_empty … H) -H
+ #H1 #H2 destruct /2 width=3 by at_empty, ex2_intro/
+| #cs1 #cs2 #cs #_ * #IH #i1 #i2 #H
+ [ elim (at_inv_true … H) -H *
+ [ -IH #H1 #H2 destruct /2 width=3 by at_zero, ex2_intro/
+ | #j1 #j2 #H1 #H2 #Hj12 destruct
+ elim (IH … Hj12) -IH -Hj12 /3 width=3 by at_succ, ex2_intro/
+ ]
+ | elim (at_inv_false … H) -H
+ #j2 #H #Hj2 destruct
+ elim (IH … Hj2) -IH -Hj2 /3 width=3 by at_succ, at_false, ex2_intro/
+ ]
+| #cs1 #cs2 #cs #_ #IH #i1 #i2 #H elim (IH … H) -IH -H
+ /3 width=3 by at_false, ex2_intro/
+]
+qed-.
+
+lemma after_fwd_at: ∀cs1,cs2,cs. cs2 ⊚ cs1 ≡ cs →
+ ∀i1,i2,i. @⦃i1, cs1⦄ ≡ i2 → @⦃i2, cs2⦄ ≡ i → @⦃i1, cs⦄ ≡ i.
+#cs1 #cs2 #cs #Hcs #i1 #i2 #i #Hi1 #Hi2 elim (after_at1_fwd … Hcs … Hi1) -cs1
+#j #H #Hj >(at_mono … Hi2 … H) -i2 //
+qed-.
+
+lemma after_fwd_at1: ∀cs1,cs2,cs. cs2 ⊚ cs1 ≡ cs →
+ ∀i1,i2,i. @⦃i1, cs⦄ ≡ i → @⦃i2, cs2⦄ ≡ i → @⦃i1, cs1⦄ ≡ i2.
+#cs1 #cs2 #cs #Hcs #i1 #i2 #i #Hi1 #Hi2 elim (after_at_fwd … Hcs … Hi1) -cs
+#j1 #Hij1 #H >(at_inj … Hi2 … H) -i //
+qed-.
+
+lemma after_fwd_at2: ∀cs1,cs2,cs. cs2 ⊚ cs1 ≡ cs →
+ ∀i1,i2,i. @⦃i1, cs⦄ ≡ i → @⦃i1, cs1⦄ ≡ i2 → @⦃i2, cs2⦄ ≡ i.
+#cs1 #cs2 #cs #H elim H -cs1 -cs2 -cs
+[ #i1 #i2 #i #Hi #Hi1 elim (at_inv_empty … Hi1) -Hi1 //
+| #cs1 #cs2 #cs #_ * #IH #i1 #i2 #i #Hi #Hi1
+ [ elim (at_inv_true … Hi1) -Hi1 *
+ [ -IH #H1 #H2 destruct >(at_inv_true_zero_sn … Hi) -i //
+ | #j1 #j2 #H1 #H2 #Hj12 destruct elim (at_inv_true_succ_sn … Hi) -Hi
+ #j #H #Hj1 destruct /3 width=3 by at_succ/
+ ]
+ | elim (at_inv_false … Hi1) -Hi1
+ #j2 #H #Hj2 destruct elim (at_inv_false … Hi) -Hi
+ #j #H #Hj destruct /3 width=3 by at_succ/
+ ]
+| #cs1 #cs2 #cs #_ #IH #i1 #i2 #i #Hi #Hi2 elim (at_inv_false … Hi) -Hi
+ #j #H #Hj destruct /3 width=3 by at_false/
+]
+qed-.
+
+(* Main properties **********************************************************)
+
+theorem after_trans1: ∀cs1,cs2,cs0. cs1 ⊚ cs2 ≡ cs0 →
+ ∀cs3, cs4. cs0 ⊚ cs3 ≡ cs4 →
+ ∃∃cs. cs2 ⊚ cs3 ≡ cs & cs1 ⊚ cs ≡ cs4.
+#cs1 #cs2 #cs0 #H elim H -cs1 -cs2 -cs0
+[ #cs3 #cs4 #H elim (after_inv_empty1 … H) -H
+ #H1 #H2 destruct /2 width=3 by ex2_intro, after_empty/
+| #cs1 #cs2 #cs0 #_ * #IH #cs3 #cs4 #H
+ [ elim (after_inv_true1 … H) -H
+ #tl3 #tl4 #b #H1 #H2 #Htl destruct
+ elim (IH … Htl) -cs0
+ /3 width=3 by ex2_intro, after_true/
+ | elim (after_inv_false1 … H) -H
+ #tl4 #H #Htl destruct
+ elim (IH … Htl) -cs0
+ /3 width=3 by ex2_intro, after_true, after_false/
+ ]
+| #cs1 #cs2 #cs0 #_ #IH #cs3 #cs4 #H
+ elim (after_inv_false1 … H) -H
+ #tl4 #H #Htl destruct
+ elim (IH … Htl) -cs0
+ /3 width=3 by ex2_intro, after_false/
+]
+qed-.
+
+theorem after_trans2: ∀cs1,cs0,cs4. cs1 ⊚ cs0 ≡ cs4 →
+ ∀cs2, cs3. cs2 ⊚ cs3 ≡ cs0 →
+ ∃∃cs. cs1 ⊚ cs2 ≡ cs & cs ⊚ cs3 ≡ cs4.
+#cs1 #cs0 #cs4 #H elim H -cs1 -cs0 -cs4
+[ #cs2 #cs3 #H elim (after_inv_empty3 … H) -H
+ #H1 #H2 destruct /2 width=3 by ex2_intro, after_empty/
+| #cs1 #cs0 #cs4 #_ #b #IH #cs2 #cs3 #H elim (after_inv_inh3 … H) -H *
+ [ #tl2 #tl3 #H1 #H2 #Htl destruct
+ elim (IH … Htl) -cs0
+ /3 width=3 by ex2_intro, after_true/
+ | #tl2 #H1 #H2 #Htl destruct
+ elim (IH … Htl) -cs0
+ /3 width=3 by ex2_intro, after_true, after_false/
+ ]
+| #cs1 #cs0 #cs4 #_ #IH #cs2 #cs3 #H elim (IH … H) -cs0
+ /3 width=3 by ex2_intro, after_false/
+]
+qed-.
+
+theorem after_mono: ∀cs1,cs2,x. cs1 ⊚ cs2 ≡ x → ∀y. cs1 ⊚ cs2 ≡ y → x = y.
+#cs1 #cs2 #x #H elim H -cs1 -cs2 -x
+[ #y #H elim (after_inv_empty1 … H) -H //
+| #cs1 #cs #x #_ #b #IH #y #H elim (after_inv_true1 … H) -H
+ #tl #tly #b0 #H1 #H2 #Htl destruct >(IH … Htl) -tl -cs1 -x //
+| #cs1 #cs2 #x #_ #IH #y #H elim (after_inv_false1 … H) -H
+ #tly #H #Htl destruct >(IH … Htl) -cs1 -cs2 -x //
+]
+qed-.
+
+theorem after_inj: ∀cs1,x,cs. cs1 ⊚ x ≡ cs → ∀y. cs1 ⊚ y ≡ cs → x = y.
+#cs1 #x #cs #H elim H -cs1 -x -cs
+[ #y #H elim (after_inv_empty1 … H) -H //
+| #cs1 #x #cs #_ #b #IH #y #H elim (after_inv_true1 … H) -H
+ #tly #tl #b0 #H1 #H2 #Htl destruct >(IH … Htl) -tl -cs1 -x //
+| #cs1 #x #cs #_ #IH #y #H elim (after_inv_false1 … H) -H
+ #tl #H #Htl destruct >(IH … Htl) -tl -cs1 -x //
+]
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground_2/notation/relations/rat_3.ma".
+include "ground_2/relocation/trace.ma".
+
+(* RELOCATION TRACE *********************************************************)
+
+inductive at: trace → relation nat ≝
+ | at_empty: at (◊) 0 0
+ | at_zero : ∀cs. at (Ⓣ @ cs) 0 0
+ | at_succ : ∀cs,i1,i2. at cs i1 i2 → at (Ⓣ @ cs) (⫯i1) (⫯i2)
+ | at_false: ∀cs,i1,i2. at cs i1 i2 → at (Ⓕ @ cs) i1 (⫯i2).
+
+interpretation "relocation (trace)"
+ 'RAt i1 cs i2 = (at cs i1 i2).
+
+(* Basic inversion lemmas ***************************************************)
+
+fact at_inv_empty_aux: ∀cs,i1,i2. @⦃i1, cs⦄ ≡ i2 → cs = ◊ → i1 = 0 ∧ i2 = 0.
+#cs #i1 #i2 * -cs -i1 -i2 /2 width=1 by conj/
+#cs #i1 #i2 #_ #H destruct
+qed-.
+
+lemma at_inv_empty: ∀i1,i2. @⦃i1, ◊⦄ ≡ i2 → i1 = 0 ∧ i2 = 0.
+/2 width=5 by at_inv_empty_aux/ qed-.
+
+lemma at_inv_empty_zero_sn: ∀i. @⦃0, ◊⦄ ≡ i → i = 0.
+#i #H elim (at_inv_empty … H) -H //
+qed-.
+
+lemma at_inv_empty_zero_dx: ∀i. @⦃i, ◊⦄ ≡ 0 → i = 0.
+#i #H elim (at_inv_empty … H) -H //
+qed-.
+
+lemma at_inv_empty_succ_sn: ∀i1,i2. @⦃⫯i1, ◊⦄ ≡ i2 → ⊥.
+#i1 #i2 #H elim (at_inv_empty … H) -H #H1 #H2 destruct
+qed-.
+
+lemma at_inv_empty_succ_dx: ∀i1,i2. @⦃i1, ◊⦄ ≡ ⫯i2 → ⊥.
+#i1 #i2 #H elim (at_inv_empty … H) -H #H1 #H2 destruct
+qed-.
+
+fact at_inv_true_aux: ∀cs,i1,i2. @⦃i1, cs⦄ ≡ i2 → ∀tl. cs = Ⓣ @ tl →
+ (i1 = 0 ∧ i2 = 0) ∨
+ ∃∃j1,j2. i1 = ⫯j1 & i2 = ⫯j2 & @⦃j1, tl⦄ ≡ j2.
+#cs #i1 #i2 * -cs -i1 -i2
+[2,3,4: #cs [2,3: #i1 #i2 #Hij ] ] #tl #H destruct
+/3 width=5 by ex3_2_intro, or_introl, or_intror, conj/
+qed-.
+
+lemma at_inv_true: ∀cs,i1,i2. @⦃i1, Ⓣ @ cs⦄ ≡ i2 →
+ (i1 = 0 ∧ i2 = 0) ∨
+ ∃∃j1,j2. i1 = ⫯j1 & i2 = ⫯j2 & @⦃j1, cs⦄ ≡ j2.
+/2 width=3 by at_inv_true_aux/ qed-.
+
+lemma at_inv_true_zero_sn: ∀cs,i. @⦃0, Ⓣ @ cs⦄ ≡ i → i = 0.
+#cs #i #H elim (at_inv_true … H) -H * //
+#j1 #j2 #H destruct
+qed-.
+
+lemma at_inv_true_zero_dx: ∀cs,i. @⦃i, Ⓣ @ cs⦄ ≡ 0 → i = 0.
+#cs #i #H elim (at_inv_true … H) -H * //
+#j1 #j2 #_ #H destruct
+qed-.
+
+lemma at_inv_true_succ_sn: ∀cs,i1,i2. @⦃⫯i1, Ⓣ @ cs⦄ ≡ i2 →
+ ∃∃j2. i2 = ⫯j2 & @⦃i1, cs⦄ ≡ j2.
+#cs #i1 #i2 #H elim (at_inv_true … H) -H *
+[ #H destruct
+| #j1 #j2 #H1 #H2 destruct /2 width=3 by ex2_intro/
+]
+qed-.
+
+lemma at_inv_true_succ_dx: ∀cs,i1,i2. @⦃i1, Ⓣ @ cs⦄ ≡ ⫯i2 →
+ ∃∃j1. i1 = ⫯j1 & @⦃j1, cs⦄ ≡ i2.
+#cs #i1 #i2 #H elim (at_inv_true … H) -H *
+[ #_ #H destruct
+| #j1 #j2 #H1 #H2 destruct /2 width=3 by ex2_intro/
+]
+qed-.
+
+lemma at_inv_true_succ: ∀cs,i1,i2. @⦃⫯i1, Ⓣ @ cs⦄ ≡ ⫯i2 →
+ @⦃i1, cs⦄ ≡ i2.
+#cs #i1 #i2 #H elim (at_inv_true … H) -H *
+[ #H destruct
+| #j1 #j2 #H1 #H2 destruct //
+]
+qed-.
+
+lemma at_inv_true_O_S: ∀cs,i. @⦃0, Ⓣ @ cs⦄ ≡ ⫯i → ⊥.
+#cs #i #H elim (at_inv_true … H) -H *
+[ #_ #H destruct
+| #j1 #j2 #H destruct
+]
+qed-.
+
+lemma at_inv_true_S_O: ∀cs,i. @⦃⫯i, Ⓣ @ cs⦄ ≡ 0 → ⊥.
+#cs #i #H elim (at_inv_true … H) -H *
+[ #H destruct
+| #j1 #j2 #_ #H destruct
+]
+qed-.
+
+fact at_inv_false_aux: ∀cs,i1,i2. @⦃i1, cs⦄ ≡ i2 → ∀tl. cs = Ⓕ @ tl →
+ ∃∃j2. i2 = ⫯j2 & @⦃i1, tl⦄ ≡ j2.
+#cs #i1 #i2 * -cs -i1 -i2
+[2,3,4: #cs [2,3: #i1 #i2 #Hij ] ] #tl #H destruct
+/2 width=3 by ex2_intro/
+qed-.
+
+lemma at_inv_false: ∀cs,i1,i2. @⦃i1, Ⓕ @ cs⦄ ≡ i2 →
+ ∃∃j2. i2 = ⫯j2 & @⦃i1, cs⦄ ≡ j2.
+/2 width=3 by at_inv_false_aux/ qed-.
+
+lemma at_inv_false_S: ∀cs,i1,i2. @⦃i1, Ⓕ @ cs⦄ ≡ ⫯i2 → @⦃i1, cs⦄ ≡ i2.
+#cs #i1 #i2 #H elim (at_inv_false … H) -H
+#j2 #H destruct //
+qed-.
+
+lemma at_inv_false_O: ∀cs,i. @⦃i, Ⓕ @ cs⦄ ≡ 0 → ⊥.
+#cs #i #H elim (at_inv_false … H) -H
+#j2 #H destruct
+qed-.
+
+lemma at_inv_le: ∀cs,i1,i2. @⦃i1, cs⦄ ≡ i2 → i1 ≤ ∥cs∥ ∧ i2 ≤ |cs|.
+#cs #i1 #i2 #H elim H -cs -i1 -i2 /2 width=1 by conj/
+#cs #i1 #i2 #_ * /3 width=1 by le_S_S, conj/
+qed-.
+
+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-.
+
+lemma at_inv_gt2: ∀cs,i1,i2. @⦃i1, cs⦄ ≡ i2 → |cs| < i2 → ⊥.
+#cs #i1 #i2 #H elim (at_inv_le … H) -H /2 width=4 by lt_le_false/
+qed-.
+
+(* Basic properties *********************************************************)
+
+(* Note: lemma 250 *)
+lemma at_le: ∀cs,i1. i1 ≤ ∥cs∥ →
+ ∃∃i2. @⦃i1, cs⦄ ≡ i2 & i2 ≤ |cs|.
+#cs elim cs -cs
+[ #i1 #H <(le_n_O_to_eq … H) -i1 /2 width=3 by at_empty, ex2_intro/
+| * #cs #IH
+ [ * /2 width=3 by at_zero, ex2_intro/
+ #i1 #H lapply (le_S_S_to_le … H) -H
+ #H elim (IH … H) -IH -H /3 width=3 by at_succ, le_S_S, ex2_intro/
+ | #i1 #H elim (IH … H) -IH -H /3 width=3 by at_false, le_S_S, ex2_intro/
+ ]
+]
+qed-.
+
+lemma at_top: ∀cs. @⦃∥cs∥, cs⦄ ≡ |cs|.
+#cs elim cs -cs // * /2 width=1 by at_succ, at_false/
+qed.
+
+lemma at_monotonic: ∀cs,i1,i2. @⦃i1, cs⦄ ≡ i2 → ∀j1. j1 < i1 →
+ ∃∃j2. @⦃j1, cs⦄ ≡ j2 & j2 < i2.
+#cs #i1 #i2 #H elim H -cs -i1 -i2
+[ #j1 #H elim (lt_zero_false … H)
+| #cs #j1 #H elim (lt_zero_false … H)
+| #cs #i1 #i2 #Hij #IH * /2 width=3 by ex2_intro, at_zero/
+ #j1 #H lapply (lt_S_S_to_lt … H) -H
+ #H elim (IH … H) -i1
+ #j2 #Hj12 #H /3 width=3 by le_S_S, ex2_intro, at_succ/
+| #cs #i1 #i2 #_ #IH #j1 #H elim (IH … H) -i1
+ /3 width=3 by le_S_S, ex2_intro, at_false/
+]
+qed-.
+
+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/
+ |*: @or_intror #H elim (at_inv_empty … H) #H1 #H2 destruct
+ ]
+| * [2: #i1 ] * [2,4: #i2 ]
+ [ elim (IH i1 i2) -IH
+ /4 width=1 by at_inv_true_succ, at_succ, or_introl, or_intror/
+ | -IH /3 width=3 by at_inv_true_O_S, or_intror/
+ | -IH /3 width=3 by at_inv_true_S_O, or_intror/
+ | -IH /2 width=1 by or_introl, at_zero/
+ ]
+| #i1 * [2: #i2 ]
+ [ elim (IH i1 i2) -IH
+ /4 width=1 by at_inv_false_S, at_false, or_introl, or_intror/
+ | -IH /3 width=3 by at_inv_false_O, or_intror/
+ ]
+]
+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.
+#cs #i1 elim i1 -i1 //
+#j1 #IHi #i2 #H elim (at_monotonic … H j1) -H
+/3 width=3 by le_to_lt_to_lt/
+qed-.
+
+lemma at_increasing_strict: ∀cs,i1,i2. @⦃i1, Ⓕ @ cs⦄ ≡ i2 →
+ i1 < i2 ∧ @⦃i1, cs⦄ ≡ ⫰i2.
+#cs #i1 #i2 #H elim (at_inv_false … H) -H
+#j2 #H #Hj2 destruct /4 width=2 by conj, at_increasing, le_S_S/
+qed-.
+
+(* Main properties **********************************************************)
+
+theorem at_mono: ∀cs,i,i1. @⦃i, cs⦄ ≡ i1 → ∀i2. @⦃i, cs⦄ ≡ i2 → i1 = i2.
+#cs #i #i1 #H elim H -cs -i -i1
+[2,3,4: #cs [2,3: #i #i1 #_ #IH ] ] #i2 #H
+[ elim (at_inv_true_succ_sn … H) -H
+ #j2 #H destruct #H >(IH … H) -cs -i -i1 //
+| elim (at_inv_false … H) -H
+ #j2 #H destruct #H >(IH … H) -cs -i -i1 //
+| /2 width=2 by at_inv_true_zero_sn/
+| /2 width=1 by at_inv_empty_zero_sn/
+]
+qed-.
+
+theorem at_inj: ∀cs,i1,i. @⦃i1, cs⦄ ≡ i → ∀i2. @⦃i2, cs⦄ ≡ i → i1 = i2.
+#cs #i1 #i #H elim H -cs -i1 -i
+[2,3,4: #cs [ |2,3: #i1 #i #_ #IH ] ] #i2 #H
+[ /2 width=2 by at_inv_true_zero_dx/
+| elim (at_inv_true_succ_dx … H) -H
+ #j2 #H destruct #H >(IH … H) -cs -i1 -i //
+| elim (at_inv_false … H) -H
+ #j #H destruct #H >(IH … H) -cs -i1 -j //
+| /2 width=1 by at_inv_empty_zero_dx/
+]
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground_2/notation/relations/isidentity_1.ma".
+include "ground_2/relocation/trace_after.ma".
+include "ground_2/relocation/trace_sle.ma".
+
+(* RELOCATION TRACE *********************************************************)
+
+definition isid: predicate trace ≝ λcs. ∥cs∥ = |cs|.
+
+interpretation "test for identity (trace)"
+ 'IsIdentity cs = (isid cs).
+
+definition t_reflexive: ∀S:Type[0]. predicate (trace → relation S) ≝
+ λS,R. ∀a. ∃∃t. 𝐈⦃t⦄ & R t a a.
+
+(* Basic properties *********************************************************)
+
+lemma isid_empty: 𝐈⦃◊⦄.
+// qed.
+
+lemma isid_true: ∀cs. 𝐈⦃cs⦄ → 𝐈⦃Ⓣ @ cs⦄.
+// qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma isid_inv_true: ∀cs. 𝐈⦃Ⓣ @ cs⦄ → 𝐈⦃cs⦄.
+/2 width=1 by injective_S/ qed-.
+
+lemma isid_inv_false: ∀cs. 𝐈⦃Ⓕ @ cs⦄ → ⊥.
+/3 width=4 by colength_le, lt_le_false/ qed-.
+
+lemma isid_inv_cons: ∀cs,b. 𝐈⦃b @ cs⦄ → 𝐈⦃cs⦄ ∧ b = Ⓣ.
+#cs * #H /3 width=1 by isid_inv_true, conj/
+elim (isid_inv_false … H)
+qed-.
+
+(* Properties on application ************************************************)
+
+lemma isid_at: ∀cs. (∀i1,i2. @⦃i1, cs⦄ ≡ i2 → i1 = i2) → 𝐈⦃cs⦄.
+#cs elim cs -cs // * /2 width=1 by/
+qed.
+
+(* Inversion lemmas on application ******************************************)
+
+lemma isid_inv_at: ∀cs,i1,i2. @⦃i1, cs⦄ ≡ i2 → 𝐈⦃cs⦄ → i1 = i2.
+#cs #i1 #i2 #H elim H -cs -i1 -i2 /4 width=1 by isid_inv_true, eq_f/
+#cs #i1 #i2 #_ #IH #H elim (isid_inv_false … H)
+qed-.
+
+(* Properties on composition ************************************************)
+
+lemma isid_after_sn: ∀cs2. ∃∃cs1. 𝐈⦃cs1⦄ & cs1 ⊚ cs2 ≡ cs2.
+#cs2 elim cs2 -cs2 /2 width=3 by after_empty, ex2_intro/
+#b #cs2 * /3 width=3 by isid_true, after_true, ex2_intro/
+qed-.
+
+lemma isid_after_dx: ∀cs1. ∃∃cs2. 𝐈⦃cs2⦄ & cs1 ⊚ cs2 ≡ cs1.
+#cs1 elim cs1 -cs1 /2 width=3 by after_empty, ex2_intro/
+* #cs1 * /3 width=3 by isid_true, after_true, after_false, ex2_intro/
+qed-.
+
+lemma after_isid_sn: ∀cs1,cs2. cs1 ⊚ cs2 ≡ cs2 → 𝐈⦃cs1⦄ .
+#cs1 #cs2 #H elim (after_inv_length … H) -H //
+qed.
+
+lemma after_isid_dx: ∀cs1,cs2. cs1 ⊚ cs2 ≡ cs1 → 𝐈⦃cs2⦄ .
+#cs1 #cs2 #H elim (after_inv_length … H) -H //
+qed.
+
+(* Inversion lemmas on composition ******************************************)
+
+lemma after_isid_inv_sn: ∀cs1,cs2,cs. cs1 ⊚ cs2 ≡ cs → 𝐈⦃cs1⦄ → cs = cs2.
+#cs1 #cs2 #cs #H elim H -cs1 -cs2 -cs //
+#cs1 #cs2 #cs #_ [ #b ] #IH #H
+[ >IH -IH // | elim (isid_inv_false … H) ]
+qed-.
+
+lemma after_isid_inv_dx: ∀cs1,cs2,cs. cs1 ⊚ cs2 ≡ cs → 𝐈⦃cs2⦄ → cs = cs1.
+#cs1 #cs2 #cs #H elim H -cs1 -cs2 -cs //
+#cs1 #cs2 #cs #_ [ #b ] #IH #H
+[ elim (isid_inv_cons … H) -H #H >IH -IH // | >IH -IH // ]
+qed-.
+
+lemma after_inv_isid3: ∀t1,t2,t. t1 ⊚ t2 ≡ t → 𝐈⦃t⦄ → 𝐈⦃t1⦄ ∧ 𝐈⦃t2⦄.
+#t1 #t2 #t #H elim H -t1 -t2 -t
+[ /2 width=1 by conj/
+| #t1 #t2 #t #_ #b #IHt #H elim (isid_inv_cons … H) -H
+ #Ht #H elim (IHt Ht) -t /2 width=1 by isid_true, conj/
+| #t1 #t2 #t #_ #_ #H elim (isid_inv_false … H)
+]
+qed-.
+
+(* Forward on inclusion *****************************************************)
+
+lemma sle_isid1_fwd: ∀t1,t2. t1 ⊆ t2 → 𝐈⦃t1⦄ → t1 = t2.
+#t1 #t2 #H elim H -t1 -t2 //
+[ #t1 #t2 #_ #IH #H lapply (isid_inv_true … H) -H
+ #HT1 @eq_f2 // @IH @HT1 (**) (* full auto fails *)
+| #t1 #t2 #b #_ #_ #H elim (isid_inv_false … H)
+]
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground_2/notation/relations/isuniform_1.ma".
+include "ground_2/relocation/trace_isid.ma".
+
+(* RELOCATION TRACE *********************************************************)
+
+inductive isun: predicate trace ≝
+| isun_id : ∀t. 𝐈⦃t⦄ → isun t
+| isun_false: ∀t. isun t → isun (Ⓕ@t)
+.
+
+interpretation "test for uniformity (trace)"
+ 'IsUniform t = (isun t).
+
+(* Basic inversion lennas ***************************************************)
+
+fact isun_inv_true_aux: ∀t. 𝐔⦃t⦄ → ∀u. t = Ⓣ@u → 𝐈⦃u⦄.
+#t * -t
+[ #t #Ht #u #H destruct /2 width=1 by isid_inv_true/
+| #t #_ #u #H destruct
+]
+qed-.
+
+lemma isun_inv_true: ∀t. 𝐔⦃Ⓣ@t⦄ → 𝐈⦃t⦄.
+/2 width=3 by isun_inv_true_aux/ qed-.
+
+fact isun_inv_false_aux: ∀t. 𝐔⦃t⦄ → ∀u. t = Ⓕ@u → 𝐔⦃u⦄.
+#t * -t
+[ #t #Ht #u #H destruct elim (isid_inv_false … Ht)
+| #t #Ht #u #H destruct //
+]
+qed-.
+
+lemma isun_inv_false: ∀t. 𝐔⦃Ⓕ@t⦄ → 𝐔⦃t⦄.
+/2 width=3 by isun_inv_false_aux/ qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground_2/relocation/trace_at.ma".
+
+(* RELOCATION TRACE *********************************************************)
+
+inductive sle: relation trace ≝
+| sle_empty: sle (◊) (◊)
+| sle_true : ∀t1,t2. sle t1 t2 → sle (Ⓣ @ t1) (Ⓣ @ t2)
+| sle_false: ∀t1,t2,b. sle t1 t2 → sle (Ⓕ @ t1) (b @ t2)
+.
+
+interpretation
+ "inclusion (trace)"
+ 'subseteq t1 t2 = (sle t1 t2).
+
+(* Basic properties *********************************************************)
+
+(* Basic forward lemmas *****************************************************)
+
+lemma sle_fwd_length: ∀t1,t2. t1 ⊆ t2 → |t1| = |t2|.
+#t1 #t2 #H elim H -t1 -t2 //
+qed-.
+
+lemma sle_fwd_colength: ∀t1,t2. t1 ⊆ t2 → ∥t1∥ ≤ ∥t2∥.
+#t1 #t2 #H elim H -t1 -t2 /2 width=1 by le_S_S/
+#t1 #t2 * /2 width=1 by le_S/
+qed-.
+
+(* Inversion lemmas on application ******************************************)
+
+lemma sle_inv_at: ∀t1,t2. t1 ⊆ t2 →
+ ∀i,i1,i2. @⦃i, t1⦄ ≡ i1 → @⦃i, t2⦄ ≡ i2 → i2 ≤ i1.
+#t1 #t2 #H elim H -t1 -t2
+[ #i #i1 #i2 #_ #H2 elim (at_inv_empty … H2) -H2 //
+| #t1 #t2 #_ #IH #i #i1 #i2 #H0 #H2 elim (at_inv_true … H2) -H2 * //
+ #j1 #j2 #H1 #H2 #Hj destruct elim (at_inv_true_succ_sn … H0) -H0
+ /3 width=3 by le_S_S/
+| #t1 #t2 * #_ #IH #i #i1 #i2 #H0 #H2
+ [ elim (at_inv_true … H2) -H2 * //
+ #j #j2 #H1 #H2 #Hj2 destruct elim (at_inv_false … H0) -H0
+ #j1 #H #Hj1 destruct elim (at_monotonic … Hj1 j) -Hj1 //
+ #x #H1x #H2x @le_S_S /4 width=3 by lt_to_le, le_to_lt_to_lt/ (**) (* full auto too slow *)
+ | elim (at_inv_false … H2) elim (at_inv_false … H0) -H0 -H2
+ /3 width=3 by le_S_S/
+ ]
+]
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground_2/notation/functions/complement_1.ma".
+include "ground_2/relocation/trace.ma".
+
+(* RELOCATION TRACE *********************************************************)
+
+let rec snot (t:trace) on t ≝ match t with
+[ nil ⇒ ◊
+| cons b t ⇒ (¬ b) @ snot t
+].
+
+interpretation
+ "complement (trace)"
+ 'Complement t = (snot t).
+
+(* Basic properties *********************************************************)
+
+lemma snot_empty: ∁ (◊) = ◊.
+// qed.
+
+lemma snot_inh: ∀t,b. ∁ (b@t) = (¬ b) @ ∁ t.
+// qed.
+
+lemma snot_true: ∀t. ∁ (Ⓣ @ t) = Ⓕ @ ∁ t.
+// qed.
+
+lemma snot_false: ∀t. ∁ (Ⓕ @ t) = Ⓣ @ ∁ t.
+// qed.
+
+lemma snot_length: ∀t. |∁ t| = |t|.
+#t elim t -t normalize //
+qed.
+
+lemma snot_colength: ∀t. ∥∁ t∥ = |t| - ∥t∥.
+#t elim t -t //
+* /2 width=1 by minus_Sn_m/
+qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground_2/notation/relations/runion_3.ma".
+include "ground_2/relocation/trace_isid.ma".
+
+(* RELOCATION TRACE *********************************************************)
+
+inductive sor: relation3 trace trace trace ≝
+ | sor_empty: sor (◊) (◊) (◊)
+ | sor_inh : ∀cs1,cs2,cs. sor cs1 cs2 cs →
+ ∀b1,b2. sor (b1 @ cs1) (b2 @ cs2) ((b1 ∨ b2) @ cs).
+
+interpretation
+ "union (trace)"
+ 'RUnion L1 L2 L = (sor L2 L1 L).
+
+(* Basic properties *********************************************************)
+
+lemma sor_length: ∀cs1,cs2. |cs1| = |cs2| →
+ ∃∃cs. cs2 ⋓ cs1 ≡ cs & |cs| = |cs1| & |cs| = |cs2|.
+#cs1 elim cs1 -cs1
+[ #cs2 #H >(length_inv_zero_sn … H) -H /2 width=4 by sor_empty, ex3_intro/
+| #b1 #cs1 #IH #x #H elim (length_inv_succ_sn … H) -H
+ #cs2 #b2 #H12 #H destruct elim (IH … H12) -IH -H12
+ #cs #H12 #H1 #H2 @(ex3_intro … ((b1 ∨ b2) @ cs)) /2 width=1 by sor_inh/ (**) (* explicit constructor *)
+]
+qed-.
+
+lemma sor_sym: ∀cs1,cs2,cs. cs1 ⋓ cs2 ≡ cs → cs2 ⋓ cs1 ≡ cs.
+#cs1 #cs2 #cs #H elim H -cs1 -cs2 -cs /2 width=1 by sor_inh/
+qed-.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma sor_inv_length: ∀cs1,cs2,cs. cs2 ⋓ cs1 ≡ cs →
+ ∧∧ |cs1| = |cs2| & |cs| = |cs1| & |cs| = |cs2|.
+#cs1 #cs2 #cs #H elim H -cs1 -cs2 -cs /2 width=1 by and3_intro/
+#cs1 #cs2 #cs #_ #b1 #b2 * /2 width=1 by and3_intro/
+qed-.
+
+(* Basic forward lemmas *****************************************************)
+
+lemma sor_fwd_isid_sn: ∀cs1,cs2,cs. cs1 ⋓ cs2 ≡ cs → 𝐈⦃cs1⦄ → 𝐈⦃cs⦄.
+#cs1 #cs2 #cs #H elim H -cs1 -cs2 -cs //
+#cs1 #cs2 #cs #_ #b1 #b2 #IH #H elim (isid_inv_cons … H) -H
+/3 width=1 by isid_true/
+qed-.
+
+lemma sor_fwd_isid_dx: ∀cs1,cs2,cs. cs1 ⋓ cs2 ≡ cs → 𝐈⦃cs2⦄ → 𝐈⦃cs⦄.
+/3 width=4 by sor_fwd_isid_sn, sor_sym/ qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+(* GENERAL NOTATION USED BY THE FORMAL SYSTEM λδ ****************************)
+
+notation "hvbox( ↓ term 46 T )"
+ non associative with precedence 46
+ for @{ 'Drop $T }.
(* *)
(**************************************************************************)
+include "ground_2/notation/functions/lift_1.ma".
include "ground_2/lib/arith.ma".
include "ground_2/lib/streams.ma".
(* RELOCATION N-STREAM ******************************************************)
definition rtmap: Type[0] ≝ stream nat.
+
+definition push: rtmap → rtmap ≝ λf. 0@f.
+
+interpretation "push (nstream)" 'Lift f = (push f).
+
+definition next: rtmap → rtmap.
+* #n #f @(⫯n@f)
+qed.
+
+interpretation "next (nstream)" 'Successor f = (next f).
+
+(* Basic properties *********************************************************)
+
+lemma push_rew: ∀f. 0@f = ↑f.
+// qed.
+
+lemma next_rew: ∀f,n. (⫯n)@f = ⫯(n@f).
+// qed.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma injective_push: injective ? ? push.
+#f1 #f2 normalize #H destruct //
+qed-.
+
+lemma discr_push_next: ∀f1,f2. ↑f1 = ⫯f2 → ⊥.
+#f1 * #n2 #f2 normalize #H destruct
+qed-.
+
+lemma discr_next_push: ∀f1,f2. ⫯f1 = ↑f2 → ⊥.
+* #n1 #f1 #f2 normalize #H destruct
+qed-.
+
+lemma injective_next: injective ? ? next.
+* #n1 #f1 * #n2 #f2 normalize #H destruct //
+qed-.
+
+lemma push_inv_seq_sn: ∀f,g,n. n@g = ↑f → 0 = n ∧ g = f.
+#f #g #n <push_rew #H destruct /2 width=1 by conj/
+qed-.
+
+lemma push_inv_seq_dx: ∀f,g,n. ↑f = n@g → 0 = n ∧ g = f.
+#f #g #n <push_rew #H destruct /2 width=1 by conj/
+qed-.
+
+lemma next_inv_seq_sn: ∀f,g,n. n@g = ⫯f → ∃∃m. m@g = f & ⫯m = n.
+* #m #f #g #n <next_rew #H destruct /2 width=3 by ex2_intro/
+qed-.
+
+lemma next_inv_seq_dx: ∀f,g,n. ⫯f = n@g → ∃∃m. m@g = f & ⫯m = n.
+* #m #f #g #n <next_rew #H destruct /2 width=3 by ex2_intro/
+qed-.
+
+lemma case_prop: ∀R:predicate rtmap.
+ (∀f. R (↑f)) → (∀f. R (⫯f)) → ∀f. R f.
+#R #H1 #H2 * * //
+qed-.
+
+lemma case_type0: ∀R:rtmap→Type[0].
+ (∀f. R (↑f)) → (∀f. R (⫯f)) → ∀f. R f.
+#R #H1 #H2 * * //
+qed-.
+
+lemma iota_push: ∀R,a,b,f. a f = case_type0 R a b (↑f).
+// qed.
+
+lemma iota_next: ∀R,a,b,f. b f = case_type0 R a b (⫯f).
+#R #a #b * //
+qed.
qed.
(* Main inversion lemmas ****************************************************)
-
+(*
lemma apply_inj_aux: ∀f1,f2,j1,j2,i1,i2. f1@❴i1❵ = j1 → f2@❴i2❵ = j2 →
j1 = j2 → f1 ≗ f2 → i1 = i2.
/2 width=6 by at_inj/ qed-.
+*)
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "ground_2/notation/functions/lift_1.ma".
-include "ground_2/relocation/nstream.ma".
-
-(* RELOCATION N-STREAM ******************************************************)
-
-definition push: rtmap → rtmap ≝ λf. 0@f.
-
-interpretation "push (nstream)" 'Lift f = (push f).
-
-definition next: rtmap → rtmap.
-* #n #f @(⫯n@f)
-qed.
-
-interpretation "next (nstream)" 'Successor f = (next f).
-
-(* Basic properties *********************************************************)
-
-lemma push_rew: ∀f. 0@f = ↑f.
-// qed.
-
-lemma next_rew: ∀f,n. (⫯n)@f = ⫯(n@f).
-// qed.
-(*
-lemma next_rew_sn: ∀f,n1,n2. n1 = ⫯n2 → n1@f = ⫯(n2@f).
-// qed.
-*)
-(* Basic inversion lemmas ***************************************************)
-
-lemma injective_push: injective ? ? push.
-#f1 #f2 normalize #H destruct //
-qed-.
-
-lemma discr_push_next: ∀f1,f2. ↑f1 = ⫯f2 → ⊥.
-#f1 * #n2 #f2 normalize #H destruct
-qed-.
-
-lemma discr_next_push: ∀f1,f2. ⫯f1 = ↑f2 → ⊥.
-* #n1 #f1 #f2 normalize #H destruct
-qed-.
-
-lemma injective_next: injective ? ? next.
-* #n1 #f1 * #n2 #f2 normalize #H destruct //
-qed-.
-
-lemma push_inv_seq_sn: ∀f,g,n. n@g = ↑f → 0 = n ∧ g = f.
-#f #g #n <push_rew #H destruct /2 width=1 by conj/
-qed-.
-
-lemma push_inv_seq_dx: ∀f,g,n. ↑f = n@g → 0 = n ∧ g = f.
-#f #g #n <push_rew #H destruct /2 width=1 by conj/
-qed-.
-
-lemma next_inv_seq_sn: ∀f,g,n. n@g = ⫯f → ∃∃m. m@g = f & ⫯m = n.
-* #m #f #g #n <next_rew #H destruct /2 width=3 by ex2_intro/
-qed-.
-
-lemma next_inv_seq_dx: ∀f,g,n. ⫯f = n@g → ∃∃m. m@g = f & ⫯m = n.
-* #m #f #g #n <next_rew #H destruct /2 width=3 by ex2_intro/
-qed-.
-
-lemma pn_split: ∀f. (∃g. ↑g = f) ∨ (∃g. ⫯g = f).
-* * /3 width=2 by or_introl, or_intror, ex_intro/
-qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground_2/relocation/nstream.ma".
+
+(* RELOCATION MAP ***********************************************************)
+
+lemma pn_split: ∀f. (∃g. ↑g = f) ∨ (∃g. ⫯g = f).
+@case_prop /3 width=2 by or_introl, or_intror, ex_intro/
+qed-.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground_2/notation/relations/rafter_3.ma".
+include "ground_2/relocation/rtmap_istot.ma".
+
+(* RELOCATION MAP ***********************************************************)
+
+coinductive after: relation3 rtmap rtmap rtmap ≝
+| after_refl: ∀f1,f2,f,g1,g2,g.
+ after f1 f2 f → ↑f1 = g1 → ↑f2 = g2 → ↑f = g → after g1 g2 g
+| after_push: ∀f1,f2,f,g1,g2,g.
+ after f1 f2 f → ↑f1 = g1 → ⫯f2 = g2 → ⫯f = g → after g1 g2 g
+| after_next: ∀f1,f2,f,g1,g.
+ after f1 f2 f → ⫯f1 = g1 → ⫯f = g → after g1 f2 g
+.
+
+interpretation "relational composition (rtmap)"
+ 'RAfter f1 f2 f = (after f1 f2 f).
+
+definition H_after_inj: predicate rtmap ≝
+ λf1. 𝐓⦃f1⦄ →
+ ∀f,f21,f22. f1 ⊚ f21 ≡ f → f1 ⊚ f22 ≡ f → f21 ≗ f22.
+
+(* Basic inversion lemmas ***************************************************)
+
+lemma after_inv_ppx: ∀g1,g2,g. g1 ⊚ g2 ≡ g → ∀f1,f2. ↑f1 = g1 → ↑f2 = g2 →
+ ∃∃f. f1 ⊚ f2 ≡ f & ↑f = g.
+#g1 #g2 #g * -g1 -g2 -g #f1 #f2 #f #g1
+[ #g2 #g #Hf #H1 #H2 #H #x1 #x2 #Hx1 #Hx2 destruct
+ >(injective_push … Hx1) >(injective_push … Hx2) -x2 -x1
+ /2 width=3 by ex2_intro/
+| #g2 #g #_ #_ #H2 #_ #x1 #x2 #_ #Hx2 destruct
+ elim (discr_push_next … Hx2)
+| #g #_ #H1 #_ #x1 #x2 #Hx1 #_ destruct
+ elim (discr_push_next … Hx1)
+]
+qed-.
+
+lemma after_inv_pnx: ∀g1,g2,g. g1 ⊚ g2 ≡ g → ∀f1,f2. ↑f1 = g1 → ⫯f2 = g2 →
+ ∃∃f. f1 ⊚ f2 ≡ f & ⫯f = g.
+#g1 #g2 #g * -g1 -g2 -g #f1 #f2 #f #g1
+[ #g2 #g #_ #_ #H2 #_ #x1 #x2 #_ #Hx2 destruct
+ elim (discr_next_push … Hx2)
+| #g2 #g #Hf #H1 #H2 #H3 #x1 #x2 #Hx1 #Hx2 destruct
+ >(injective_push … Hx1) >(injective_next … Hx2) -x2 -x1
+ /2 width=3 by ex2_intro/
+| #g #_ #H1 #_ #x1 #x2 #Hx1 #_ destruct
+ elim (discr_push_next … Hx1)
+]
+qed-.
+
+lemma after_inv_nxx: ∀g1,f2,g. g1 ⊚ f2 ≡ g → ∀f1. ⫯f1 = g1 →
+ ∃∃f. f1 ⊚ f2 ≡ f & ⫯f = g.
+#g1 #f2 #g * -g1 -f2 -g #f1 #f2 #f #g1
+[ #g2 #g #_ #H1 #_ #_ #x1 #Hx1 destruct
+ elim (discr_next_push … Hx1)
+| #g2 #g #_ #H1 #_ #_ #x1 #Hx1 destruct
+ elim (discr_next_push … Hx1)
+| #g #Hf #H1 #H #x1 #Hx1 destruct
+ >(injective_next … Hx1) -x1
+ /2 width=3 by ex2_intro/
+]
+qed-.
+
+(* Advanced inversion lemmas ************************************************)
+
+lemma after_inv_ppp: ∀g1,g2,g. g1 ⊚ g2 ≡ g →
+ ∀f1,f2,f. ↑f1 = g1 → ↑f2 = g2 → ↑f = g → f1 ⊚ f2 ≡ f.
+#g1 #g2 #g #Hg #f1 #f2 #f #H1 #H2 #H elim (after_inv_ppx … Hg … H1 H2) -g1 -g2
+#x #Hf #Hx destruct <(injective_push … Hx) -f //
+qed-.
+
+lemma after_inv_ppn: ∀g1,g2,g. g1 ⊚ g2 ≡ g →
+ ∀f1,f2,f. ↑f1 = g1 → ↑f2 = g2 → ⫯f = g → ⊥.
+#g1 #g2 #g #Hg #f1 #f2 #f #H1 #H2 #H elim (after_inv_ppx … Hg … H1 H2) -g1 -g2
+#x #Hf #Hx destruct elim (discr_push_next … Hx)
+qed-.
+
+lemma after_inv_pnn: ∀g1,g2,g. g1 ⊚ g2 ≡ g →
+ ∀f1,f2,f. ↑f1 = g1 → ⫯f2 = g2 → ⫯f = g → f1 ⊚ f2 ≡ f.
+#g1 #g2 #g #Hg #f1 #f2 #f #H1 #H2 #H elim (after_inv_pnx … Hg … H1 H2) -g1 -g2
+#x #Hf #Hx destruct <(injective_next … Hx) -f //
+qed-.
+
+lemma after_inv_pnp: ∀g1,g2,g. g1 ⊚ g2 ≡ g →
+ ∀f1,f2,f. ↑f1 = g1 → ⫯f2 = g2 → ↑f = g → ⊥.
+#g1 #g2 #g #Hg #f1 #f2 #f #H1 #H2 #H elim (after_inv_pnx … Hg … H1 H2) -g1 -g2
+#x #Hf #Hx destruct elim (discr_next_push … Hx)
+qed-.
+
+lemma after_inv_nxn: ∀g1,f2,g. g1 ⊚ f2 ≡ g →
+ ∀f1,f. ⫯f1 = g1 → ⫯f = g → f1 ⊚ f2 ≡ f.
+#g1 #f2 #g #Hg #f1 #f #H1 #H elim (after_inv_nxx … Hg … H1) -g1
+#x #Hf #Hx destruct <(injective_next … Hx) -f //
+qed-.
+
+lemma after_inv_nxp: ∀g1,f2,g. g1 ⊚ f2 ≡ g →
+ ∀f1,f. ⫯f1 = g1 → ↑f = g → ⊥.
+#g1 #f2 #g #Hg #f1 #f #H1 #H elim (after_inv_nxx … Hg … H1) -g1
+#x #Hf #Hx destruct elim (discr_next_push … Hx)
+qed-.
+
+lemma after_inv_pxp: ∀g1,g2,g. g1 ⊚ g2 ≡ g →
+ ∀f1,f. ↑f1 = g1 → ↑f = g →
+ ∃∃f2. f1 ⊚ f2 ≡ f & ↑f2 = g2.
+#g1 * * [2: #m2] #g2 #g #Hg #f1 #f #H1 #H
+[ elim (after_inv_pnp … Hg … H1 … H) -g1 -g -f1 -f //
+| lapply (after_inv_ppp … Hg … H1 … H) -g1 -g /2 width=3 by ex2_intro/
+]
+qed-.
+
+lemma after_inv_pxn: ∀g1,g2,g. g1 ⊚ g2 ≡ g →
+ ∀f1,f. ↑f1 = g1 → ⫯f = g →
+ ∃∃f2. f1 ⊚ f2 ≡ f & ⫯f2 = g2.
+#g1 * * [2: #m2] #g2 #g #Hg #f1 #f #H1 #H
+[ lapply (after_inv_pnn … Hg … H1 … H) -g1 -g /2 width=3 by ex2_intro/
+| elim (after_inv_ppn … Hg … H1 … H) -g1 -g -f1 -f //
+]
+qed-.
+
+lemma after_inv_xxp: ∀g1,g2,g. g1 ⊚ g2 ≡ g → ∀f. ↑f = g →
+ ∃∃f1,f2. f1 ⊚ f2 ≡ f & ↑f1 = g1 & ↑f2 = g2.
+* * [2: #m1 ] #g1 #g2 #g #Hg #f #H
+[ elim (after_inv_nxp … Hg … H) -g2 -g -f //
+| elim (after_inv_pxp … Hg … H) -g /2 width=5 by ex3_2_intro/
+]
+qed-.
+
+lemma after_inv_xxn: ∀g1,g2,g. g1 ⊚ g2 ≡ g → ∀f. ⫯f = g →
+ (∃∃f1,f2. f1 ⊚ f2 ≡ f & ↑f1 = g1 & ⫯f2 = g2) ∨
+ ∃∃f1. f1 ⊚ g2 ≡ f & ⫯f1 = g1.
+* * [2: #m1 ] #g1 #g2 #g #Hg #f #H
+[ /4 width=5 by after_inv_nxn, or_intror, ex2_intro/
+| elim (after_inv_pxn … Hg … H) -g
+ /3 width=5 by or_introl, ex3_2_intro/
+]
+qed-.
+
+lemma after_inv_pxx: ∀g1,g2,g. g1 ⊚ g2 ≡ g → ∀f1. ↑f1 = g1 →
+ (∃∃f2,f. f1 ⊚ f2 ≡ f & ↑f2 = g2 & ↑f = g) ∨
+ (∃∃f2,f. f1 ⊚ f2 ≡ f & ⫯f2 = g2 & ⫯f = g).
+#g1 * * [2: #m2 ] #g2 #g #Hg #f1 #H
+[ elim (after_inv_pnx … Hg … H) -g1
+ /3 width=5 by or_intror, ex3_2_intro/
+| elim (after_inv_ppx … Hg … H) -g1
+ /3 width=5 by or_introl, ex3_2_intro/
+]
+qed-.
+
+(* Main properties **********************************************************)
+
+let corec after_trans1: ∀f0,f3,f4. f0 ⊚ f3 ≡ f4 →
+ ∀f1,f2. f1 ⊚ f2 ≡ f0 →
+ ∀f. f2 ⊚ f3 ≡ f → f1 ⊚ f ≡ f4 ≝ ?.
+#f0 #f3 #f4 * -f0 -f3 -f4 #f0 #f3 #f4 #g0 [1,2: #g3 ] #g4
+[ #Hf4 #H0 #H3 #H4 #g1 #g2 #Hg0 #g #Hg
+ cases (after_inv_xxp … Hg0 … H0) -g0
+ #f1 #f2 #Hf0 #H1 #H2
+ cases (after_inv_ppx … Hg … H2 H3) -g2 -g3
+ #f #Hf #H /3 width=7 by after_refl/
+| #Hf4 #H0 #H3 #H4 #g1 #g2 #Hg0 #g #Hg
+ cases (after_inv_xxp … Hg0 … H0) -g0
+ #f1 #f2 #Hf0 #H1 #H2
+ cases (after_inv_pnx … Hg … H2 H3) -g2 -g3
+ #f #Hf #H /3 width=7 by after_push/
+| #Hf4 #H0 #H4 #g1 #g2 #Hg0 #g #Hg
+ cases (after_inv_xxn … Hg0 … H0) -g0 *
+ [ #f1 #f2 #Hf0 #H1 #H2
+ cases (after_inv_nxx … Hg … H2) -g2
+ #f #Hf #H /3 width=7 by after_push/
+ | #f1 #Hf0 #H1 /3 width=6 by after_next/
+ ]
+]
+qed-.
+
+let corec after_trans2: ∀f1,f0,f4. f1 ⊚ f0 ≡ f4 →
+ ∀f2, f3. f2 ⊚ f3 ≡ f0 →
+ ∀f. f1 ⊚ f2 ≡ f → f ⊚ f3 ≡ f4 ≝ ?.
+#f1 #f0 #f4 * -f1 -f0 -f4 #f1 #f0 #f4 #g1 [1,2: #g0 ] #g4
+[ #Hf4 #H1 #H0 #H4 #g2 #g3 #Hg0 #g #Hg
+ cases (after_inv_xxp … Hg0 … H0) -g0
+ #f2 #f3 #Hf0 #H2 #H3
+ cases (after_inv_ppx … Hg … H1 H2) -g1 -g2
+ #f #Hf #H /3 width=7 by after_refl/
+| #Hf4 #H1 #H0 #H4 #g2 #g3 #Hg0 #g #Hg
+ cases (after_inv_xxn … Hg0 … H0) -g0 *
+ [ #f2 #f3 #Hf0 #H2 #H3
+ cases (after_inv_ppx … Hg … H1 H2) -g1 -g2
+ #f #Hf #H /3 width=7 by after_push/
+ | #f2 #Hf0 #H2
+ cases (after_inv_pnx … Hg … H1 H2) -g1 -g2
+ #f #Hf #H /3 width=6 by after_next/
+ ]
+| #Hf4 #H1 #H4 #f2 #f3 #Hf0 #g #Hg
+ cases (after_inv_nxx … Hg … H1) -g1
+ #f #Hg #H /3 width=6 by after_next/
+]
+qed-.
+
+(* Main inversion lemmas on after *******************************************)
+
+let corec after_mono: ∀f1,f2,x,y. f1 ⊚ f2 ≡ x → f1 ⊚ f2 ≡ y → x ≗ y ≝ ?.
+#f1 #f2 #x #y * -f1 -f2 -x
+#f1 #f2 #x #g1 [1,2: #g2 ] #g #Hx #H1 [1,2: #H2 ] #H0x #Hy
+[ cases (after_inv_ppx … Hy … H1 H2) -g1 -g2 /3 width=8 by eq_push/
+| cases (after_inv_pnx … Hy … H1 H2) -g1 -g2 /3 width=8 by eq_next/
+| cases (after_inv_nxx … Hy … H1) -g1 /3 width=8 by eq_next/
+]
+qed-.
+
+(* Properties on minus ******************************************************)
+
+lemma after_minus: ∀n,f1,f2,f. @⦃0, f1⦄ ≡ n →
+ f1 ⊚ f2 ≡ f → f1-n ⊚ f2 ≡ f-n.
+#n elim n -n //
+#n #IH #f1 #f2 #f #Hf1 #Hf cases (at_inv_pxn … Hf1) -Hf1 [ |*: // ]
+#g1 #Hg1 #H1 cases (after_inv_nxx … Hf … H1) -Hf /2 width=1 by/
+qed.
+
+(* Inversion lemmas on isid *************************************************)
+
+let corec isid_after_sn: ∀f1. 𝐈⦃f1⦄ → ∀f2. f1 ⊚ f2 ≡ f2 ≝ ?.
+#f1 * -f1 #f1 #g1 #Hf1 #H1 #f2 cases (pn_split f2) * #g2 #H2
+/3 width=7 by after_push, after_refl/
+qed-.
+
+let corec isid_after_dx: ∀f2. 𝐈⦃f2⦄ → ∀f1. f1 ⊚ f2 ≡ f1 ≝ ?.
+#f2 * -f2 #f2 #g2 #Hf2 #H2 #f1 cases (pn_split f1) * #g1 #H1
+[ /3 width=7 by after_refl/
+| @(after_next … H1 H1) /3 width=3 by isid_push/
+]
+qed-.
+
+lemma after_isid_inv_sn: ∀f1,f2,f. f1 ⊚ f2 ≡ f → 𝐈⦃f1⦄ → f2 ≗ f.
+/3 width=6 by isid_after_sn, after_mono/
+qed-.
+
+lemma after_isid_inv_dx: ∀f1,f2,f. f1 ⊚ f2 ≡ f → 𝐈⦃f2⦄ → f1 ≗ f.
+/3 width=6 by isid_after_dx, after_mono/
+qed-.
+
+let corec after_fwd_isid1: ∀f1,f2,f. f1 ⊚ f2 ≡ f → 𝐈⦃f⦄ → 𝐈⦃f1⦄ ≝ ?.
+#f1 #f2 #f * -f1 -f2 -f
+#f1 #f2 #f #g1 [1,2: #g2 ] #g #Hf #H1 [1,2: #H2 ] #H0 #H
+[ /4 width=6 by isid_inv_push, isid_push/ ]
+cases (isid_inv_next … H … H0)
+qed-.
+
+let corec after_fwd_isid2: ∀f1,f2,f. f1 ⊚ f2 ≡ f → 𝐈⦃f⦄ → 𝐈⦃f2⦄ ≝ ?.
+#f1 #f2 #f * -f1 -f2 -f
+#f1 #f2 #f #g1 [1,2: #g2 ] #g #Hf #H1 [1,2: #H2 ] #H0 #H
+[ /4 width=6 by isid_inv_push, isid_push/ ]
+cases (isid_inv_next … H … H0)
+qed-.
+
+lemma after_inv_isid3: ∀f1,f2,f. f1 ⊚ f2 ≡ f → 𝐈⦃f⦄ → 𝐈⦃f1⦄ ∧ 𝐈⦃f2⦄.
+/3 width=4 by after_fwd_isid2, after_fwd_isid1, conj/ qed-.
+
+(* Forward lemmas on at *****************************************************)
+
+lemma after_at_fwd: ∀i,i1,f. @⦃i1, f⦄ ≡ i → ∀f2,f1. f2 ⊚ f1 ≡ f →
+ ∃∃i2. @⦃i1, f1⦄ ≡ i2 & @⦃i2, f2⦄ ≡ i.
+#i elim i -i [2: #i #IH ] #i1 #f #Hf #f2 #f1 #Hf21
+[ elim (at_inv_xxn … Hf) -Hf [1,3:* |*: // ]
+ [1: #g #j1 #Hg #H0 #H |2,4: #g #Hg #H ]
+| elim (at_inv_xxp … Hf) -Hf //
+ #g #H1 #H
+]
+[2: elim (after_inv_xxn … Hf21 … H) -f *
+ [ #g2 #g1 #Hg21 #H2 #H1 | #g2 #Hg21 #H2 ]
+|*: elim (after_inv_xxp … Hf21 … H) -f
+ #g2 #g1 #Hg21 #H2 #H1
+]
+[4: -Hg21 |*: elim (IH … Hg … Hg21) -g -IH ]
+/3 width=9 by at_refl, at_push, at_next, ex2_intro/
+qed-.
+
+lemma after_fwd_at: ∀i,i2,i1,f1,f2. @⦃i1, f1⦄ ≡ i2 → @⦃i2, f2⦄ ≡ i →
+ ∀f. f2 ⊚ f1 ≡ f → @⦃i1, f⦄ ≡ i.
+#i elim i -i [2: #i #IH ] #i2 #i1 #f1 #f2 #Hf1 #Hf2 #f #Hf
+[ elim (at_inv_xxn … Hf2) -Hf2 [1,3: * |*: // ]
+ #g2 [ #j2 ] #Hg2 [ #H22 ] #H20
+ [ elim (at_inv_xxn … Hf1 … H22) -i2 *
+ #g1 [ #j1 ] #Hg1 [ #H11 ] #H10
+ [ elim (after_inv_ppx … Hf … H20 H10) -f1 -f2 /3 width=7 by at_push/
+ | elim (after_inv_pnx … Hf … H20 H10) -f1 -f2 /3 width=6 by at_next/
+ ]
+ | elim (after_inv_nxx … Hf … H20) -f2 /3 width=7 by at_next/
+ ]
+| elim (at_inv_xxp … Hf2) -Hf2 // #g2 #H22 #H20
+ elim (at_inv_xxp … Hf1 … H22) -i2 #g1 #H11 #H10
+ elim (after_inv_ppx … Hf … H20 H10) -f1 -f2 /2 width=2 by at_refl/
+]
+qed-.
+
+lemma after_fwd_at2: ∀f,i1,i. @⦃i1, f⦄ ≡ i → ∀f1,i2. @⦃i1, f1⦄ ≡ i2 →
+ ∀f2. f2 ⊚ f1 ≡ f → @⦃i2, f2⦄ ≡ i.
+#f #i1 #i #Hf #f1 #i2 #Hf1 #f2 #H elim (after_at_fwd … Hf … H) -f
+#j1 #H #Hf2 <(at_mono … Hf1 … H) -i1 -i2 //
+qed-.
+
+lemma after_fwd_at1: ∀i,i2,i1,f,f2. @⦃i1, f⦄ ≡ i → @⦃i2, f2⦄ ≡ i →
+ ∀f1. f2 ⊚ f1 ≡ f → @⦃i1, f1⦄ ≡ i2.
+#i elim i -i [2: #i #IH ] #i2 #i1 #f #f2 #Hf #Hf2 #f1 #Hf1
+[ elim (at_inv_xxn … Hf) -Hf [1,3: * |*: // ]
+ #g [ #j1 ] #Hg [ #H01 ] #H00
+ elim (at_inv_xxn … Hf2) -Hf2 [1,3,5,7: * |*: // ]
+ #g2 [1,3: #j2 ] #Hg2 [1,2: #H22 ] #H20
+ [ elim (after_inv_pxp … Hf1 … H20 H00) -f2 -f /3 width=7 by at_push/
+ | elim (after_inv_pxn … Hf1 … H20 H00) -f2 -f /3 width=5 by at_next/
+ | elim (after_inv_nxp … Hf1 … H20 H00)
+ | /4 width=9 by after_inv_nxn, at_next/
+ ]
+| elim (at_inv_xxp … Hf) -Hf // #g #H01 #H00
+ elim (at_inv_xxp … Hf2) -Hf2 // #g2 #H21 #H20
+ elim (after_inv_pxp … Hf1 … H20 H00) -f2 -f /3 width=2 by at_refl/
+]
+qed-.
+
+(* Forward lemmas on istot **************************************************)
+
+lemma after_istot_fwd: ∀f2,f1,f. f2 ⊚ f1 ≡ f → 𝐓⦃f2⦄ → 𝐓⦃f1⦄ → 𝐓⦃f⦄.
+#f2 #f1 #f #Hf #Hf2 #Hf1 #i1 elim (Hf1 i1) -Hf1
+#i2 #Hf1 elim (Hf2 i2) -Hf2
+/3 width=7 by after_fwd_at, ex_intro/
+qed-.
+
+lemma after_fwd_istot_dx: ∀f2,f1,f. f2 ⊚ f1 ≡ f → 𝐓⦃f⦄ → 𝐓⦃f1⦄.
+#f2 #f1 #f #H #Hf #i1 elim (Hf i1) -Hf
+#i2 #Hf elim (after_at_fwd … Hf … H) -f /2 width=2 by ex_intro/
+qed-.
+
+lemma after_fwd_istot_sn: ∀f2,f1,f. f2 ⊚ f1 ≡ f → 𝐓⦃f⦄ → 𝐓⦃f2⦄.
+#f2 #f1 #f #H #Hf #i1 elim (Hf i1) -Hf
+#i #Hf elim (after_at_fwd … Hf … H) -f
+#i2 #Hf1 #Hf2 lapply (at_increasing … Hf1) -f1
+#Hi12 elim (at_le_ex … Hf2 … Hi12) -i2 /2 width=2 by ex_intro/
+qed-.
+
+lemma after_inv_istot: ∀f2,f1,f. f2 ⊚ f1 ≡ f → 𝐓⦃f⦄ → 𝐓⦃f2⦄ ∧ 𝐓⦃f1⦄.
+/3 width=4 by after_fwd_istot_sn, after_fwd_istot_dx, conj/ qed-.
+
+lemma after_at1_fwd: ∀f1,i1,i2. @⦃i1, f1⦄ ≡ i2 → ∀f2. 𝐓⦃f2⦄ → ∀f. f2 ⊚ f1 ≡ f →
+ ∃∃i. @⦃i2, f2⦄ ≡ i & @⦃i1, f⦄ ≡ i.
+#f1 #i1 #i2 #Hf1 #f2 #Hf2 #f #Hf elim (Hf2 i2) -Hf2
+/3 width=8 by after_fwd_at, ex2_intro/
+qed-.
+
+lemma after_fwd_isid_sn: ∀f2,f1,f. 𝐓⦃f⦄ → f2 ⊚ f1 ≡ f → f1 ≗ f → 𝐈⦃f2⦄.
+#f2 #f1 #f #H #Hf elim (after_inv_istot … Hf H) -H
+#Hf2 #Hf1 #H @isid_at_total // -Hf2
+#i2 #i #Hf2 elim (Hf1 i2) -Hf1
+#i0 #Hf1 lapply (at_increasing … Hf1)
+#Hi20 lapply (after_fwd_at2 … i0 … Hf1 … Hf) -Hf
+/3 width=7 by at_eq_repl_back, at_mono, at_id_le/
+qed-.
+
+lemma after_fwd_isid_dx: ∀f2,f1,f. 𝐓⦃f⦄ → f2 ⊚ f1 ≡ f → f2 ≗ f → 𝐈⦃f1⦄.
+#f2 #f1 #f #H #Hf elim (after_inv_istot … Hf H) -H
+#Hf2 #Hf1 #H2 @isid_at_total // -Hf1
+#i1 #i2 #Hi12 elim (after_at1_fwd … Hi12 … Hf) -f1
+/3 width=8 by at_inj, at_eq_repl_back/
+qed-.
+
+let corec after_inj_O_aux: ∀f1. @⦃0, f1⦄ ≡ 0 → H_after_inj f1 ≝ ?.
+#f1 #H1f1 #H2f1 #f #f21 #f22 #H1f #H2f
+cases (at_inv_pxp … H1f1) -H1f1 [ |*: // ] #g1 #H1
+lapply (istot_inv_push … H2f1 … H1) -H2f1 #H2g1
+cases (H2g1 0) #n #Hn
+cases (after_inv_pxx … H1f … H1) -H1f * #g21 #g #H1g #H21 #H
+[ cases (after_inv_pxp … H2f … H1 H) -f1 -f #g22 #H2g #H22
+ @(eq_push … H21 H22) -f21 -f22
+| cases (after_inv_pxn … H2f … H1 H) -f1 -f #g22 #H2g #H22
+ @(eq_next … H21 H22) -f21 -f22
+]
+@(after_inj_O_aux (g1-n) … (g-n)) -after_inj_O_aux
+/2 width=1 by after_minus, istot_minus, at_pxx_minus/
+qed-.
+
+fact after_inj_aux: (∀f1. @⦃0, f1⦄ ≡ 0 → H_after_inj f1) →
+ ∀i2,f1. @⦃0, f1⦄ ≡ i2 → H_after_inj f1.
+#H0 #i2 elim i2 -i2 /2 width=1 by/ -H0
+#i2 #IH #f1 #H1f1 #H2f1 #f #f21 #f22 #H1f #H2f
+elim (at_inv_pxn … H1f1) -H1f1 [ |*: // ] #g1 #H1g1 #H1
+elim (after_inv_nxx … H1f … H1) -H1f #g #H1g #H
+lapply (after_inv_nxn … H2f … H1 H) -f #H2g
+/3 width=6 by istot_inv_next/
+qed-.
+
+theorem after_inj: ∀f1. H_after_inj f1.
+#f1 #H cases (H 0) /3 width=7 by after_inj_aux, after_inj_O_aux/
+qed-.
#H destruct
qed-.
+lemma at_inv_npp: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 →
+ ∀g,j1. ⫯j1 = i1 → ↑g = f → 0 = i2 → ⊥.
+#f #i1 #i2 #Hf #g #j1 #H1 #H elim (at_inv_npx … Hf … H1 H) -f -i1
+#x2 #Hg * -i2 #H destruct
+qed-.
+
lemma at_inv_npn: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 →
∀g,j1,j2. ⫯j1 = i1 → ↑g = f → ⫯j2 = i2 → @⦃j1, g⦄ ≡ j2.
#f #i1 #i2 #Hf #g #j1 #j2 #H1 #H elim (at_inv_npx … Hf … H1 H) -f -i1
#x2 #Hg * -i2 #H destruct //
qed-.
-lemma at_inv_npp: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 →
- ∀g,j1. ⫯j1 = i1 → ↑g = f → 0 = i2 → ⊥.
-#f #i1 #i2 #Hf #g #j1 #H1 #H elim (at_inv_npx … Hf … H1 H) -f -i1
+lemma at_inv_xnp: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 →
+ ∀g. ⫯g = f → 0 = i2 → ⊥.
+#f #i1 #i2 #Hf #g #H elim (at_inv_xnx … Hf … H) -f
#x2 #Hg * -i2 #H destruct
qed-.
#x2 #Hg * -i2 #H destruct //
qed-.
+(* --------------------------------------------------------------------------*)
+
+lemma at_inv_pxp: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → 0 = i1 → 0 = i2 → ∃g. ↑g = f.
+#f elim (pn_split … f) * /2 width=2 by ex_intro/
+#g #H #i1 #i2 #Hf #H1 #H2 cases (at_inv_xnp … Hf … H H2)
+qed-.
+
lemma at_inv_pxn: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → ∀j2. 0 = i1 → ⫯j2 = i2 →
∃∃g. @⦃i1, g⦄ ≡ j2 & ⫯g = f.
#f elim (pn_split … f) *
]
qed-.
-lemma at_inv_xnp: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 →
- ∀g. ⫯g = f → 0 = i2 → ⊥.
-#f #i1 #i2 #Hf #g #H elim (at_inv_xnx … Hf … H) -f
-#x2 #Hg * -i2 #H destruct
-qed-.
-
lemma at_inv_nxp: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 →
∀j1. ⫯j1 = i1 → 0 = i2 → ⊥.
#f elim (pn_split f) *
/4 width=7 by at_inv_xnn, at_inv_npn, ex2_intro, or_intror, or_introl/
qed-.
+(* --------------------------------------------------------------------------*)
+
lemma at_inv_xpx: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → ∀g. ↑g = f →
(0 = i1 ∧ 0 = i2) ∨
∃∃j1,j2. @⦃j1, g⦄ ≡ j2 & ⫯j1 = i1 & ⫯j2 = i2.
]
qed-.
+lemma at_inv_xxn: ∀f,i1,i2. @⦃i1, f⦄ ≡ i2 → ∀j2. ⫯j2 = i2 →
+ (∃∃g,j1. @⦃j1, g⦄ ≡ j2 & ⫯j1 = i1 & ↑g = f) ∨
+ ∃∃g. @⦃i1, g⦄ ≡ j2 & ⫯g = f.
+#f elim (pn_split f) *
+#g #H #i1 #i2 #Hf #j2 #H2
+[ elim (at_inv_xpn … Hf … H H2) -i2 /3 width=5 by or_introl, ex3_2_intro/
+| lapply (at_inv_xnn … Hf … H H2) -i2 /3 width=3 by or_intror, ex2_intro/
+]
+qed-.
+
(* Basic forward lemmas *****************************************************)
lemma at_increasing: ∀i2,i1,f. @⦃i1, f⦄ ≡ i2 → i1 ≤ i2.
#i1 #i2 @eq_repl_sym /2 width=3 by at_eq_repl_back/
qed-.
+lemma at_le_ex: ∀j2,i2,f. @⦃i2, f⦄ ≡ j2 → ∀i1. i1 ≤ i2 →
+ ∃∃j1. @⦃i1, f⦄ ≡ j1 & j1 ≤ j2.
+#j2 elim j2 -j2 [2: #j2 #IH ] #i2 #f #Hf
+[ elim (at_inv_xxn … Hf) -Hf [1,3: * |*: // ]
+ #g [ #x2 ] #Hg [ #H2 ] #H0
+ [ * /3 width=3 by at_refl, ex2_intro/
+ #i1 #Hi12 destruct lapply (le_S_S_to_le … Hi12) -Hi12
+ #Hi12 elim (IH … Hg … Hi12) -x2 -IH
+ /3 width=7 by at_push, ex2_intro, le_S_S/
+ | #i1 #Hi12 elim (IH … Hg … Hi12) -IH -i2
+ /3 width=5 by at_next, ex2_intro, le_S_S/
+ ]
+| elim (at_inv_xxp … Hf) -Hf //
+ #g * -i2 #H2 #i1 #Hi12 <(le_n_O_to_eq … Hi12)
+ /3 width=3 by at_refl, ex2_intro/
+]
+qed-.
+
lemma at_id_le: ∀i1,i2. i1 ≤ i2 → ∀f. @⦃i2, f⦄ ≡ i2 → @⦃i1, f⦄ ≡ i1.
#i1 #i2 #H @(le_elim … H) -i1 -i2 [ #i2 | #i1 #i2 #IH ]
#f #Hf elim (at_fwd_id_ex … Hf) /4 width=7 by at_inv_npn, at_push, at_refl/
(* Main properties **********************************************************)
-theorem at_monotonic: ∀j2,i2,f2. @⦃i2, f2⦄ ≡ j2 → ∀j1,i1,f1. @⦃i1, f1⦄ ≡ j1 →
- f1 ≗ f2 → i1 < i2 → j1 < j2.
+theorem at_monotonic: ∀j2,i2,f. @⦃i2, f⦄ ≡ j2 → ∀j1,i1. @⦃i1, f⦄ ≡ j1 →
+ i1 < i2 → j1 < j2.
#j2 elim j2 -j2
-[ #i2 #f2 #Hf2 elim (at_inv_xxp … Hf2) -Hf2 //
- #g #H21 #_ #j1 #i1 #f1 #_ #_ #Hi elim (lt_le_false … Hi) -Hi //
-| #j2 #IH #i2 #f2 #Hf2 * //
- #j1 #i1 #f1 #Hf1 #Hf #Hi elim (lt_inv_gen … Hi)
- #x2 #_ #H21 elim (at_inv_nxn … Hf2 … H21) -Hf2 [1,3: * |*: // ]
- #g2 #Hg2 #H2
- [ elim (eq_inv_xp … Hf … H2) -f2
- #g1 #Hg #H1 elim (at_inv_xpn … Hf1 … H1) -f1
+[ #i2 #f #H2f elim (at_inv_xxp … H2f) -H2f //
+ #g #H21 #_ #j1 #i1 #_ #Hi elim (lt_le_false … Hi) -Hi //
+| #j2 #IH #i2 #f #H2f * //
+ #j1 #i1 #H1f #Hi elim (lt_inv_gen … Hi)
+ #x2 #_ #H21 elim (at_inv_nxn … H2f … H21) -H2f [1,3: * |*: // ]
+ #g #H2g #H
+ [ elim (at_inv_xpn … H1f … H) -f
/4 width=8 by lt_S_S_to_lt, lt_S_S/
- | elim (eq_inv_xn … Hf … H2) -f2
- /4 width=8 by at_inv_xnn, lt_S_S/
+ | /4 width=8 by at_inv_xnn, lt_S_S/
]
]
qed-.
-theorem at_inv_monotonic: ∀j1,i1,f1. @⦃i1, f1⦄ ≡ j1 → ∀j2,i2,f2. @⦃i2, f2⦄ ≡ j2 →
- f1 ≗ f2 → j1 < j2 → i1 < i2.
+theorem at_inv_monotonic: ∀j1,i1,f. @⦃i1, f⦄ ≡ j1 → ∀j2,i2. @⦃i2, f⦄ ≡ j2 →
+ j1 < j2 → i1 < i2.
#j1 elim j1 -j1
-[ #i1 #f1 #Hf1 elim (at_inv_xxp … Hf1) -Hf1 //
- #g1 * -i1 #H1 #j2 #i2 #f2 #Hf2 #Hf #Hj elim (lt_inv_O1 … Hj) -Hj
- #x2 #H22 elim (eq_inv_px … Hf … H1) -f1
- #g2 #Hg #H2 elim (at_inv_xpn … Hf2 … H2 H22) -f2 //
+[ #i1 #f #H1f elim (at_inv_xxp … H1f) -H1f //
+ #g * -i1 #H #j2 #i2 #H2f #Hj elim (lt_inv_O1 … Hj) -Hj
+ #x2 #H22 elim (at_inv_xpn … H2f … H H22) -f //
| #j1 #IH *
- [ #f1 #Hf1 elim (at_inv_pxn … Hf1) -Hf1 [ |*: // ]
- #g1 #Hg1 #H1 #j2 #i2 #f2 #Hf2 #Hf #Hj elim (lt_inv_S1 … Hj) -Hj
- elim (eq_inv_nx … Hf … H1) -f1 /3 width=7 by at_inv_xnn/
- | #i1 #f1 #Hf1 #j2 #i2 #f2 #Hf2 #Hf #Hj elim (lt_inv_S1 … Hj) -Hj
- #y2 #Hj #H22 elim (at_inv_nxn … Hf1) -Hf1 [1,4: * |*: // ]
- #g1 #Hg1 #H1
- [ elim (eq_inv_px … Hf … H1) -f1
- #g2 #Hg #H2 elim (at_inv_xpn … Hf2 … H2 H22) -f2 -H22
+ [ #f #H1f elim (at_inv_pxn … H1f) -H1f [ |*: // ]
+ #g #H1g #H #j2 #i2 #H2f #Hj elim (lt_inv_S1 … Hj) -Hj
+ /3 width=7 by at_inv_xnn/
+ | #i1 #f #H1f #j2 #i2 #H2f #Hj elim (lt_inv_S1 … Hj) -Hj
+ #y2 #Hj #H22 elim (at_inv_nxn … H1f) -H1f [1,4: * |*: // ]
+ #g #Hg #H
+ [ elim (at_inv_xpn … H2f … H H22) -f -H22
/3 width=7 by lt_S_S/
- | elim (eq_inv_nx … Hf … H1) -f1 /3 width=7 by at_inv_xnn/
+ | /3 width=7 by at_inv_xnn/
]
]
]
qed-.
-theorem at_mono: ∀f1,f2. f1 ≗ f2 → ∀i,i1. @⦃i, f1⦄ ≡ i1 → ∀i2. @⦃i, f2⦄ ≡ i2 → i2 = i1.
-#f1 #f2 #Ht #i #i1 #H1 #i2 #H2 elim (lt_or_eq_or_gt i2 i1) //
-#Hi elim (lt_le_false i i) /3 width=8 by at_inv_monotonic, eq_sym/
+theorem at_mono: ∀f,i,i1. @⦃i, f⦄ ≡ i1 → ∀i2. @⦃i, f⦄ ≡ i2 → i2 = i1.
+#f #i #i1 #H1 #i2 #H2 elim (lt_or_eq_or_gt i2 i1) //
+#Hi elim (lt_le_false i i) /3 width=6 by at_inv_monotonic, eq_sym/
qed-.
-theorem at_inj: ∀f1,f2. f1 ≗ f2 → ∀i1,i. @⦃i1, f1⦄ ≡ i → ∀i2. @⦃i2, f2⦄ ≡ i → i1 = i2.
-#f1 #f2 #Ht #i1 #i #H1 #i2 #H2 elim (lt_or_eq_or_gt i2 i1) //
-#Hi elim (lt_le_false i i) /3 width=8 by at_monotonic, eq_sym/
+theorem at_inj: ∀f,i1,i. @⦃i1, f⦄ ≡ i → ∀i2. @⦃i2, f⦄ ≡ i → i1 = i2.
+#f #i1 #i #H1 #i2 #H2 elim (lt_or_eq_or_gt i2 i1) //
+#Hi elim (lt_le_false i i) /3 width=6 by at_monotonic, eq_sym/
qed-.
+(* Properties on minus ******************************************************)
+
+lemma at_pxx_minus: ∀n,f. @⦃0, f⦄ ≡ n → @⦃0, f-n⦄ ≡ 0.
+#n elim n -n //
+#n #IH #f #Hf cases (at_inv_pxn … Hf) -Hf /2 width=3 by/
+qed.
+
(* Advanced inversion lemmas on isid ****************************************)
lemma isid_inv_at: ∀i,f. 𝐈⦃f⦄ → @⦃i, f⦄ ≡ i.
(**************************************************************************)
include "ground_2/notation/relations/funexteq_2.ma".
-include "ground_2/relocation/nstream_lift.ma".
+include "ground_2/relocation/rtmap.ma".
(* RELOCATION MAP ***********************************************************)
/3 width=5 by eq_push, eq_next/
qed-.
-theorem eq_canc_sn: ∀f,f1,f2. f ≗ f1 → f ≗ f2 → f1 ≗ f2.
+theorem eq_canc_sn: ∀f2. eq_repl_back (λf. f ≗ f2).
/3 width=3 by eq_trans, eq_sym/ qed-.
-theorem eq_canc_dx: ∀f,f1,f2. f1 ≗ f → f2 ≗ f → f1 ≗ f2.
+theorem eq_canc_dx: ∀f1. eq_repl_fwd (λf. f1 ≗ f).
/3 width=3 by eq_trans, eq_sym/ qed-.
(**************************************************************************)
include "ground_2/notation/relations/isidentity_1.ma".
-include "ground_2/relocation/rtmap_eq.ma".
+include "ground_2/relocation/rtmap_minus.ma".
(* RELOCATION MAP ***********************************************************)
#j #Hg elim (at_inv_xnx … Hg … H) -Hg -H /2 width=2 by ex_intro/
qed-.
+(* Properties on tl *********************************************************)
+
+lemma istot_tl: ∀f. 𝐓⦃f⦄ → 𝐓⦃↓f⦄.
+#f cases (pn_split f) *
+#g * -f /2 width=3 by istot_inv_next, istot_inv_push/
+qed.
+
+(* Properties on minus ******************************************************)
+
+lemma istot_minus: ∀n,f. 𝐓⦃f⦄ → 𝐓⦃f-n⦄.
+#n elim n -n /3 width=1 by istot_tl/
+qed.
+
(* Advanced forward lemmas on at ********************************************)
let corec at_ext: ∀f1,f2. 𝐓⦃f1⦄ → 𝐓⦃f2⦄ →
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground_2/relocation/rtmap_tl.ma".
+
+(* RELOCATION MAP ***********************************************************)
+
+let rec minus (f:rtmap) (n:nat) on n: rtmap ≝ match n with
+[ O ⇒ f | S m ⇒ ↓(minus f m) ].
+
+interpretation "minus (rtmap)" 'minus f n = (minus f n).
+
+(* Basic properties *********************************************************)
+
+lemma minus_rew_O: ∀f. f = f - 0.
+// qed.
+
+lemma minus_rew_S: ∀f,n. ↓(f - n) = f - ⫯n.
+// qed.
+
+lemma minus_eq_repl: ∀n. eq_repl (λf1,f2. f1 - n ≗ f2 - n).
+#n elim n -n /3 width=1 by tl_eq_repl/
+qed.
+
+(* Advancedd properties *****************************************************)
+
+lemma minus_xn: ∀n,f. (↓f) - n = f - ⫯n.
+#n elim n -n //
+qed.
--- /dev/null
+(**************************************************************************)
+(* ___ *)
+(* ||M|| *)
+(* ||A|| A project by Andrea Asperti *)
+(* ||T|| *)
+(* ||I|| Developers: *)
+(* ||T|| The HELM team. *)
+(* ||A|| http://helm.cs.unibo.it *)
+(* \ / *)
+(* \ / This file is distributed under the terms of the *)
+(* v GNU General Public License Version 2 *)
+(* *)
+(**************************************************************************)
+
+include "ground_2/notation/functions/drop_1.ma".
+include "ground_2/relocation/rtmap_eq.ma".
+
+(* RELOCATION MAP ***********************************************************)
+
+definition tl: rtmap → rtmap.
+@case_type0 #f @f
+defined.
+
+interpretation "tail (rtmap)" 'Drop f = (tl f).
+
+(* Basic properties *********************************************************)
+
+lemma tl_rew: ∀f. case_type0 (λ_:rtmap.rtmap) (λf:rtmap.f) (λf:rtmap.f) f = ↓f.
+// qed.
+
+lemma tl_push_rew: ∀f. f = ↓↑f.
+#f <tl_rew <iota_push //
+qed.
+
+lemma tl_next_rew: ∀f. f = ↓⫯f.
+#f <tl_rew <iota_next //
+qed.
+
+lemma tl_eq_repl: eq_repl … (λf1,f2. ↓f1 ≗ ↓f2).
+#f1 #f2 * -f1 -f2 //
+qed.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "ground_2/notation/functions/norm_1.ma".
-include "ground_2/lib/bool.ma".
-include "ground_2/lib/list.ma".
-
-(* RELOCATION TRACE *********************************************************)
-
-definition trace: Type[0] ≝ list bool.
-
-let rec colength (cs:trace) on cs ≝ match cs with
-[ nil ⇒ 0
-| cons b tl ⇒ match b with [ true ⇒ ⫯(colength tl) | false ⇒ colength tl ]
-].
-
-interpretation "colength (trace)"
- 'Norm cs = (colength cs).
-
-(* basic properties *********************************************************)
-
-lemma colength_empty: ∥◊∥ = 0.
-// qed.
-
-lemma colength_true: ∀cs. ∥Ⓣ@cs∥ = ⫯∥cs∥.
-// qed.
-
-lemma colength_false: ∀cs. ∥Ⓕ@cs∥ = ∥cs∥.
-// qed.
-
-lemma colength_cons: ∀cs1,cs2. ∥cs1∥ = ∥cs2∥ →
- ∀b. ∥b@cs1∥ = ∥b@cs2∥.
-#cs1 #cs2 #H * /2 width=1 by/
-qed.
-
-lemma colength_le: ∀cs. ∥cs∥ ≤ |cs|.
-#cs elim cs -cs //
-* /2 width=1 by le_S_S, le_S/
-qed.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "ground_2/notation/relations/rafter_3.ma".
-include "ground_2/relocation/trace_at.ma".
-
-(* RELOCATION TRACE *********************************************************)
-
-inductive after: relation3 trace trace trace ≝
- | after_empty: after (◊) (◊) (◊)
- | after_true : ∀cs1,cs2,cs. after cs1 cs2 cs →
- ∀b. after (Ⓣ @ cs1) (b @ cs2) (b @ cs)
- | after_false: ∀cs1,cs2,cs. after cs1 cs2 cs →
- after (Ⓕ @ cs1) cs2 (Ⓕ @ cs).
-
-interpretation "composition (trace)"
- 'RAfter cs1 cs2 cs = (after cs1 cs2 cs).
-
-(* Basic properties *********************************************************)
-
-lemma after_length: ∀cs1,cs2. ∥cs1∥ = |cs2| →
- ∃∃cs. cs1 ⊚ cs2 ≡ cs & |cs| = |cs1| & ∥cs∥ = ∥cs2∥.
-#cs1 elim cs1 -cs1
-[ #cs2 #H >(length_inv_zero_sn … H) -cs2 /2 width=4 by after_empty, ex3_intro/
-| * #cs1 #IH #cs2 #Hcs
- [ elim (length_inv_succ_sn … Hcs) -Hcs
- #tl #b #Hcs #H destruct
- ]
- elim (IH … Hcs) -IH -Hcs
- #cs #Hcs #H1 #H2 [ @(ex3_intro … (b@cs)) | @(ex3_intro … (Ⓕ@cs)) ] /2 width=1 by after_true, after_false, colength_cons/
-]
-qed-.
-
-(* Basic inversion lemmas ***************************************************)
-
-fact after_inv_empty1_aux: ∀cs1,cs2,cs. cs1 ⊚ cs2 ≡ cs → cs1 = ◊ →
- cs2 = ◊ ∧ cs = ◊.
-#cs1 #cs2 #cs * -cs1 -cs2 -cs
-[ /2 width=1 by conj/
-| #cs1 #cs2 #cs #_ #b #H destruct
-| #cs1 #cs2 #cs #_ #H destruct
-]
-qed-.
-
-lemma after_inv_empty1: ∀cs2,cs. ◊ ⊚ cs2 ≡ cs → cs2 = ◊ ∧ cs = ◊.
-/2 width=3 by after_inv_empty1_aux/ qed-.
-
-fact after_inv_true1_aux: ∀cs1,cs2,cs. cs1 ⊚ cs2 ≡ cs → ∀tl1. cs1 = Ⓣ @ tl1 →
- ∃∃tl2,tl,b. cs2 = b @ tl2 & cs = b @ tl & tl1 ⊚ tl2 ≡ tl.
-#cs1 #cs2 #cs * -cs1 -cs2 -cs
-[ #tl1 #H destruct
-| #cs1 #cs2 #cs #H12 #b #tl1 #H destruct
- /2 width=6 by ex3_3_intro/
-| #cs1 #cs2 #cs #_ #tl1 #H destruct
-]
-qed-.
-
-lemma after_inv_true1: ∀tl1,cs2,cs. (Ⓣ @ tl1) ⊚ cs2 ≡ cs →
- ∃∃tl2,tl,b. cs2 = b @ tl2 & cs = b @ tl & tl1 ⊚ tl2 ≡ tl.
-/2 width=3 by after_inv_true1_aux/ qed-.
-
-fact after_inv_false1_aux: ∀cs1,cs2,cs. cs1 ⊚ cs2 ≡ cs → ∀tl1. cs1 = Ⓕ @ tl1 →
- ∃∃tl. cs = Ⓕ @ tl & tl1 ⊚ cs2 ≡ tl.
-#cs1 #cs2 #cs * -cs1 -cs2 -cs
-[ #tl1 #H destruct
-| #cs1 #cs2 #cs #_ #b #tl1 #H destruct
-| #cs1 #cs2 #cs #H12 #tl1 #H destruct
- /2 width=3 by ex2_intro/
-]
-qed-.
-
-lemma after_inv_false1: ∀tl1,cs2,cs. (Ⓕ @ tl1) ⊚ cs2 ≡ cs →
- ∃∃tl. cs = Ⓕ @ tl & tl1 ⊚ cs2 ≡ tl.
-/2 width=3 by after_inv_false1_aux/ qed-.
-
-fact after_inv_empty3_aux: ∀cs1,cs2,cs. cs1 ⊚ cs2 ≡ cs → cs = ◊ →
- cs1 = ◊ ∧ cs2 = ◊.
-#cs1 #cs2 #cs * -cs1 -cs2 -cs
-[ /2 width=1 by conj/
-| #cs1 #cs2 #cs #_ #b #H destruct
-| #cs1 #cs2 #cs #_ #H destruct
-]
-qed-.
-
-lemma after_inv_empty3: ∀cs1,cs2. cs1 ⊚ cs2 ≡ ◊ → cs1 = ◊ ∧ cs2 = ◊.
-/2 width=3 by after_inv_empty3_aux/ qed-.
-
-fact after_inv_inh3_aux: ∀cs1,cs2,cs. cs1 ⊚ cs2 ≡ cs → ∀tl,b. cs = b @ tl →
- (∃∃tl1,tl2. cs1 = Ⓣ @ tl1 & cs2 = b @ tl2 & tl1 ⊚ tl2 ≡ tl) ∨
- ∃∃tl1. cs1 = Ⓕ @ tl1 & b = Ⓕ & tl1 ⊚ cs2 ≡ tl.
-#cs1 #cs2 #cs * -cs1 -cs2 -cs
-[ #tl #b #H destruct
-| #cs1 #cs2 #cs #H12 #b0 #tl #b #H destruct
- /3 width=5 by ex3_2_intro, or_introl/
-| #cs1 #cs2 #cs #H12 #tl #b #H destruct
- /3 width=3 by ex3_intro, or_intror/
-]
-qed-.
-
-lemma after_inv_inh3: ∀cs1,cs2,tl,b. cs1 ⊚ cs2 ≡ b @ tl →
- (∃∃tl1,tl2. cs1 = Ⓣ @ tl1 & cs2 = b @ tl2 & tl1 ⊚ tl2 ≡ tl) ∨
- ∃∃tl1. cs1 = Ⓕ @ tl1 & b = Ⓕ & tl1 ⊚ cs2 ≡ tl.
-/2 width=3 by after_inv_inh3_aux/ qed-.
-
-lemma after_inv_true3: ∀cs1,cs2,tl. cs1 ⊚ cs2 ≡ Ⓣ @ tl →
- ∃∃tl1,tl2. cs1 = Ⓣ @ tl1 & cs2 = Ⓣ @ tl2 & tl1 ⊚ tl2 ≡ tl.
-#cs1 #cs2 #tl #H elim (after_inv_inh3 … H) -H // *
-#tl1 #_ #H destruct
-qed-.
-
-lemma after_inv_false3: ∀cs1,cs2,tl. cs1 ⊚ cs2 ≡ Ⓕ @ tl →
- (∃∃tl1,tl2. cs1 = Ⓣ @ tl1 & cs2 = Ⓕ @ tl2 & tl1 ⊚ tl2 ≡ tl) ∨
- ∃∃tl1. cs1 = Ⓕ @ tl1 & tl1 ⊚ cs2 ≡ tl.
-#cs1 #cs2 #tl #H elim (after_inv_inh3 … H) -H /2 width=1 by or_introl/ * /3 width=3 by ex2_intro, or_intror/
-qed-.
-
-lemma after_inv_length: ∀cs1,cs2,cs. cs1 ⊚ cs2 ≡ cs →
- ∧∧ ∥cs1∥ = |cs2| & |cs| = |cs1| & ∥cs∥ = ∥cs2∥.
-#cs1 #cs2 #cs #H elim H -cs1 -cs2 -cs /2 width=1 by and3_intro/
-#cs1 #cs2 #cs #_ [ * ] * /2 width=1 by and3_intro/
-qed-.
-
-(* Basic forward lemmas *****************************************************)
-
-lemma after_at_fwd: ∀cs1,cs2,cs. cs2 ⊚ cs1 ≡ cs → ∀i1,i. @⦃i1, cs⦄ ≡ i →
- ∃∃i2. @⦃i1, cs1⦄ ≡ i2 & @⦃i2, cs2⦄ ≡ i.
-#cs1 #cs2 #cs #H elim H -cs1 -cs2 -cs
-[ #i1 #i #H elim (at_inv_empty … H) -H
- #H1 #H2 destruct /2 width=3 by at_empty, ex2_intro/
-| #cs1 #cs2 #cs #_ * #IH #i1 #i #H
- [ elim (at_inv_true … H) -H *
- [ -IH #H1 #H2 destruct /2 width=3 by at_zero, ex2_intro/
- | #j1 #j #H1 #H2 #Hj1 destruct
- elim (IH … Hj1) -IH -Hj1 /3 width=3 by at_succ, ex2_intro/
- ]
- | elim (at_inv_false … H) -H
- #j #H #Hj destruct
- elim (IH … Hj) -IH -Hj /3 width=3 by at_succ, at_false, ex2_intro/
- ]
-| #cs1 #cs2 #cs #_ #IH #i1 #i #H elim (at_inv_false … H) -H
- #j #H #Hj destruct
- elim (IH … Hj) -IH -Hj /3 width=3 by at_false, ex2_intro/
-]
-qed-.
-
-lemma after_at1_fwd: ∀cs1,cs2,cs. cs2 ⊚ cs1 ≡ cs → ∀i1,i2. @⦃i1, cs1⦄ ≡ i2 →
- ∃∃i. @⦃i2, cs2⦄ ≡ i & @⦃i1, cs⦄ ≡ i.
-#cs1 #cs2 #cs #H elim H -cs1 -cs2 -cs
-[ #i1 #i2 #H elim (at_inv_empty … H) -H
- #H1 #H2 destruct /2 width=3 by at_empty, ex2_intro/
-| #cs1 #cs2 #cs #_ * #IH #i1 #i2 #H
- [ elim (at_inv_true … H) -H *
- [ -IH #H1 #H2 destruct /2 width=3 by at_zero, ex2_intro/
- | #j1 #j2 #H1 #H2 #Hj12 destruct
- elim (IH … Hj12) -IH -Hj12 /3 width=3 by at_succ, ex2_intro/
- ]
- | elim (at_inv_false … H) -H
- #j2 #H #Hj2 destruct
- elim (IH … Hj2) -IH -Hj2 /3 width=3 by at_succ, at_false, ex2_intro/
- ]
-| #cs1 #cs2 #cs #_ #IH #i1 #i2 #H elim (IH … H) -IH -H
- /3 width=3 by at_false, ex2_intro/
-]
-qed-.
-
-lemma after_fwd_at: ∀cs1,cs2,cs. cs2 ⊚ cs1 ≡ cs →
- ∀i1,i2,i. @⦃i1, cs1⦄ ≡ i2 → @⦃i2, cs2⦄ ≡ i → @⦃i1, cs⦄ ≡ i.
-#cs1 #cs2 #cs #Hcs #i1 #i2 #i #Hi1 #Hi2 elim (after_at1_fwd … Hcs … Hi1) -cs1
-#j #H #Hj >(at_mono … Hi2 … H) -i2 //
-qed-.
-
-lemma after_fwd_at1: ∀cs1,cs2,cs. cs2 ⊚ cs1 ≡ cs →
- ∀i1,i2,i. @⦃i1, cs⦄ ≡ i → @⦃i2, cs2⦄ ≡ i → @⦃i1, cs1⦄ ≡ i2.
-#cs1 #cs2 #cs #Hcs #i1 #i2 #i #Hi1 #Hi2 elim (after_at_fwd … Hcs … Hi1) -cs
-#j1 #Hij1 #H >(at_inj … Hi2 … H) -i //
-qed-.
-
-lemma after_fwd_at2: ∀cs1,cs2,cs. cs2 ⊚ cs1 ≡ cs →
- ∀i1,i2,i. @⦃i1, cs⦄ ≡ i → @⦃i1, cs1⦄ ≡ i2 → @⦃i2, cs2⦄ ≡ i.
-#cs1 #cs2 #cs #H elim H -cs1 -cs2 -cs
-[ #i1 #i2 #i #Hi #Hi1 elim (at_inv_empty … Hi1) -Hi1 //
-| #cs1 #cs2 #cs #_ * #IH #i1 #i2 #i #Hi #Hi1
- [ elim (at_inv_true … Hi1) -Hi1 *
- [ -IH #H1 #H2 destruct >(at_inv_true_zero_sn … Hi) -i //
- | #j1 #j2 #H1 #H2 #Hj12 destruct elim (at_inv_true_succ_sn … Hi) -Hi
- #j #H #Hj1 destruct /3 width=3 by at_succ/
- ]
- | elim (at_inv_false … Hi1) -Hi1
- #j2 #H #Hj2 destruct elim (at_inv_false … Hi) -Hi
- #j #H #Hj destruct /3 width=3 by at_succ/
- ]
-| #cs1 #cs2 #cs #_ #IH #i1 #i2 #i #Hi #Hi2 elim (at_inv_false … Hi) -Hi
- #j #H #Hj destruct /3 width=3 by at_false/
-]
-qed-.
-
-(* Main properties **********************************************************)
-
-theorem after_trans1: ∀cs1,cs2,cs0. cs1 ⊚ cs2 ≡ cs0 →
- ∀cs3, cs4. cs0 ⊚ cs3 ≡ cs4 →
- ∃∃cs. cs2 ⊚ cs3 ≡ cs & cs1 ⊚ cs ≡ cs4.
-#cs1 #cs2 #cs0 #H elim H -cs1 -cs2 -cs0
-[ #cs3 #cs4 #H elim (after_inv_empty1 … H) -H
- #H1 #H2 destruct /2 width=3 by ex2_intro, after_empty/
-| #cs1 #cs2 #cs0 #_ * #IH #cs3 #cs4 #H
- [ elim (after_inv_true1 … H) -H
- #tl3 #tl4 #b #H1 #H2 #Htl destruct
- elim (IH … Htl) -cs0
- /3 width=3 by ex2_intro, after_true/
- | elim (after_inv_false1 … H) -H
- #tl4 #H #Htl destruct
- elim (IH … Htl) -cs0
- /3 width=3 by ex2_intro, after_true, after_false/
- ]
-| #cs1 #cs2 #cs0 #_ #IH #cs3 #cs4 #H
- elim (after_inv_false1 … H) -H
- #tl4 #H #Htl destruct
- elim (IH … Htl) -cs0
- /3 width=3 by ex2_intro, after_false/
-]
-qed-.
-
-theorem after_trans2: ∀cs1,cs0,cs4. cs1 ⊚ cs0 ≡ cs4 →
- ∀cs2, cs3. cs2 ⊚ cs3 ≡ cs0 →
- ∃∃cs. cs1 ⊚ cs2 ≡ cs & cs ⊚ cs3 ≡ cs4.
-#cs1 #cs0 #cs4 #H elim H -cs1 -cs0 -cs4
-[ #cs2 #cs3 #H elim (after_inv_empty3 … H) -H
- #H1 #H2 destruct /2 width=3 by ex2_intro, after_empty/
-| #cs1 #cs0 #cs4 #_ #b #IH #cs2 #cs3 #H elim (after_inv_inh3 … H) -H *
- [ #tl2 #tl3 #H1 #H2 #Htl destruct
- elim (IH … Htl) -cs0
- /3 width=3 by ex2_intro, after_true/
- | #tl2 #H1 #H2 #Htl destruct
- elim (IH … Htl) -cs0
- /3 width=3 by ex2_intro, after_true, after_false/
- ]
-| #cs1 #cs0 #cs4 #_ #IH #cs2 #cs3 #H elim (IH … H) -cs0
- /3 width=3 by ex2_intro, after_false/
-]
-qed-.
-
-theorem after_mono: ∀cs1,cs2,x. cs1 ⊚ cs2 ≡ x → ∀y. cs1 ⊚ cs2 ≡ y → x = y.
-#cs1 #cs2 #x #H elim H -cs1 -cs2 -x
-[ #y #H elim (after_inv_empty1 … H) -H //
-| #cs1 #cs #x #_ #b #IH #y #H elim (after_inv_true1 … H) -H
- #tl #tly #b0 #H1 #H2 #Htl destruct >(IH … Htl) -tl -cs1 -x //
-| #cs1 #cs2 #x #_ #IH #y #H elim (after_inv_false1 … H) -H
- #tly #H #Htl destruct >(IH … Htl) -cs1 -cs2 -x //
-]
-qed-.
-
-theorem after_inj: ∀cs1,x,cs. cs1 ⊚ x ≡ cs → ∀y. cs1 ⊚ y ≡ cs → x = y.
-#cs1 #x #cs #H elim H -cs1 -x -cs
-[ #y #H elim (after_inv_empty1 … H) -H //
-| #cs1 #x #cs #_ #b #IH #y #H elim (after_inv_true1 … H) -H
- #tly #tl #b0 #H1 #H2 #Htl destruct >(IH … Htl) -tl -cs1 -x //
-| #cs1 #x #cs #_ #IH #y #H elim (after_inv_false1 … H) -H
- #tl #H #Htl destruct >(IH … Htl) -tl -cs1 -x //
-]
-qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "ground_2/notation/relations/rat_3.ma".
-include "ground_2/relocation/trace.ma".
-
-(* RELOCATION TRACE *********************************************************)
-
-inductive at: trace → relation nat ≝
- | at_empty: at (◊) 0 0
- | at_zero : ∀cs. at (Ⓣ @ cs) 0 0
- | at_succ : ∀cs,i1,i2. at cs i1 i2 → at (Ⓣ @ cs) (⫯i1) (⫯i2)
- | at_false: ∀cs,i1,i2. at cs i1 i2 → at (Ⓕ @ cs) i1 (⫯i2).
-
-interpretation "relocation (trace)"
- 'RAt i1 cs i2 = (at cs i1 i2).
-
-(* Basic inversion lemmas ***************************************************)
-
-fact at_inv_empty_aux: ∀cs,i1,i2. @⦃i1, cs⦄ ≡ i2 → cs = ◊ → i1 = 0 ∧ i2 = 0.
-#cs #i1 #i2 * -cs -i1 -i2 /2 width=1 by conj/
-#cs #i1 #i2 #_ #H destruct
-qed-.
-
-lemma at_inv_empty: ∀i1,i2. @⦃i1, ◊⦄ ≡ i2 → i1 = 0 ∧ i2 = 0.
-/2 width=5 by at_inv_empty_aux/ qed-.
-
-lemma at_inv_empty_zero_sn: ∀i. @⦃0, ◊⦄ ≡ i → i = 0.
-#i #H elim (at_inv_empty … H) -H //
-qed-.
-
-lemma at_inv_empty_zero_dx: ∀i. @⦃i, ◊⦄ ≡ 0 → i = 0.
-#i #H elim (at_inv_empty … H) -H //
-qed-.
-
-lemma at_inv_empty_succ_sn: ∀i1,i2. @⦃⫯i1, ◊⦄ ≡ i2 → ⊥.
-#i1 #i2 #H elim (at_inv_empty … H) -H #H1 #H2 destruct
-qed-.
-
-lemma at_inv_empty_succ_dx: ∀i1,i2. @⦃i1, ◊⦄ ≡ ⫯i2 → ⊥.
-#i1 #i2 #H elim (at_inv_empty … H) -H #H1 #H2 destruct
-qed-.
-
-fact at_inv_true_aux: ∀cs,i1,i2. @⦃i1, cs⦄ ≡ i2 → ∀tl. cs = Ⓣ @ tl →
- (i1 = 0 ∧ i2 = 0) ∨
- ∃∃j1,j2. i1 = ⫯j1 & i2 = ⫯j2 & @⦃j1, tl⦄ ≡ j2.
-#cs #i1 #i2 * -cs -i1 -i2
-[2,3,4: #cs [2,3: #i1 #i2 #Hij ] ] #tl #H destruct
-/3 width=5 by ex3_2_intro, or_introl, or_intror, conj/
-qed-.
-
-lemma at_inv_true: ∀cs,i1,i2. @⦃i1, Ⓣ @ cs⦄ ≡ i2 →
- (i1 = 0 ∧ i2 = 0) ∨
- ∃∃j1,j2. i1 = ⫯j1 & i2 = ⫯j2 & @⦃j1, cs⦄ ≡ j2.
-/2 width=3 by at_inv_true_aux/ qed-.
-
-lemma at_inv_true_zero_sn: ∀cs,i. @⦃0, Ⓣ @ cs⦄ ≡ i → i = 0.
-#cs #i #H elim (at_inv_true … H) -H * //
-#j1 #j2 #H destruct
-qed-.
-
-lemma at_inv_true_zero_dx: ∀cs,i. @⦃i, Ⓣ @ cs⦄ ≡ 0 → i = 0.
-#cs #i #H elim (at_inv_true … H) -H * //
-#j1 #j2 #_ #H destruct
-qed-.
-
-lemma at_inv_true_succ_sn: ∀cs,i1,i2. @⦃⫯i1, Ⓣ @ cs⦄ ≡ i2 →
- ∃∃j2. i2 = ⫯j2 & @⦃i1, cs⦄ ≡ j2.
-#cs #i1 #i2 #H elim (at_inv_true … H) -H *
-[ #H destruct
-| #j1 #j2 #H1 #H2 destruct /2 width=3 by ex2_intro/
-]
-qed-.
-
-lemma at_inv_true_succ_dx: ∀cs,i1,i2. @⦃i1, Ⓣ @ cs⦄ ≡ ⫯i2 →
- ∃∃j1. i1 = ⫯j1 & @⦃j1, cs⦄ ≡ i2.
-#cs #i1 #i2 #H elim (at_inv_true … H) -H *
-[ #_ #H destruct
-| #j1 #j2 #H1 #H2 destruct /2 width=3 by ex2_intro/
-]
-qed-.
-
-lemma at_inv_true_succ: ∀cs,i1,i2. @⦃⫯i1, Ⓣ @ cs⦄ ≡ ⫯i2 →
- @⦃i1, cs⦄ ≡ i2.
-#cs #i1 #i2 #H elim (at_inv_true … H) -H *
-[ #H destruct
-| #j1 #j2 #H1 #H2 destruct //
-]
-qed-.
-
-lemma at_inv_true_O_S: ∀cs,i. @⦃0, Ⓣ @ cs⦄ ≡ ⫯i → ⊥.
-#cs #i #H elim (at_inv_true … H) -H *
-[ #_ #H destruct
-| #j1 #j2 #H destruct
-]
-qed-.
-
-lemma at_inv_true_S_O: ∀cs,i. @⦃⫯i, Ⓣ @ cs⦄ ≡ 0 → ⊥.
-#cs #i #H elim (at_inv_true … H) -H *
-[ #H destruct
-| #j1 #j2 #_ #H destruct
-]
-qed-.
-
-fact at_inv_false_aux: ∀cs,i1,i2. @⦃i1, cs⦄ ≡ i2 → ∀tl. cs = Ⓕ @ tl →
- ∃∃j2. i2 = ⫯j2 & @⦃i1, tl⦄ ≡ j2.
-#cs #i1 #i2 * -cs -i1 -i2
-[2,3,4: #cs [2,3: #i1 #i2 #Hij ] ] #tl #H destruct
-/2 width=3 by ex2_intro/
-qed-.
-
-lemma at_inv_false: ∀cs,i1,i2. @⦃i1, Ⓕ @ cs⦄ ≡ i2 →
- ∃∃j2. i2 = ⫯j2 & @⦃i1, cs⦄ ≡ j2.
-/2 width=3 by at_inv_false_aux/ qed-.
-
-lemma at_inv_false_S: ∀cs,i1,i2. @⦃i1, Ⓕ @ cs⦄ ≡ ⫯i2 → @⦃i1, cs⦄ ≡ i2.
-#cs #i1 #i2 #H elim (at_inv_false … H) -H
-#j2 #H destruct //
-qed-.
-
-lemma at_inv_false_O: ∀cs,i. @⦃i, Ⓕ @ cs⦄ ≡ 0 → ⊥.
-#cs #i #H elim (at_inv_false … H) -H
-#j2 #H destruct
-qed-.
-
-lemma at_inv_le: ∀cs,i1,i2. @⦃i1, cs⦄ ≡ i2 → i1 ≤ ∥cs∥ ∧ i2 ≤ |cs|.
-#cs #i1 #i2 #H elim H -cs -i1 -i2 /2 width=1 by conj/
-#cs #i1 #i2 #_ * /3 width=1 by le_S_S, conj/
-qed-.
-
-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-.
-
-lemma at_inv_gt2: ∀cs,i1,i2. @⦃i1, cs⦄ ≡ i2 → |cs| < i2 → ⊥.
-#cs #i1 #i2 #H elim (at_inv_le … H) -H /2 width=4 by lt_le_false/
-qed-.
-
-(* Basic properties *********************************************************)
-
-(* Note: lemma 250 *)
-lemma at_le: ∀cs,i1. i1 ≤ ∥cs∥ →
- ∃∃i2. @⦃i1, cs⦄ ≡ i2 & i2 ≤ |cs|.
-#cs elim cs -cs
-[ #i1 #H <(le_n_O_to_eq … H) -i1 /2 width=3 by at_empty, ex2_intro/
-| * #cs #IH
- [ * /2 width=3 by at_zero, ex2_intro/
- #i1 #H lapply (le_S_S_to_le … H) -H
- #H elim (IH … H) -IH -H /3 width=3 by at_succ, le_S_S, ex2_intro/
- | #i1 #H elim (IH … H) -IH -H /3 width=3 by at_false, le_S_S, ex2_intro/
- ]
-]
-qed-.
-
-lemma at_top: ∀cs. @⦃∥cs∥, cs⦄ ≡ |cs|.
-#cs elim cs -cs // * /2 width=1 by at_succ, at_false/
-qed.
-
-lemma at_monotonic: ∀cs,i1,i2. @⦃i1, cs⦄ ≡ i2 → ∀j1. j1 < i1 →
- ∃∃j2. @⦃j1, cs⦄ ≡ j2 & j2 < i2.
-#cs #i1 #i2 #H elim H -cs -i1 -i2
-[ #j1 #H elim (lt_zero_false … H)
-| #cs #j1 #H elim (lt_zero_false … H)
-| #cs #i1 #i2 #Hij #IH * /2 width=3 by ex2_intro, at_zero/
- #j1 #H lapply (lt_S_S_to_lt … H) -H
- #H elim (IH … H) -i1
- #j2 #Hj12 #H /3 width=3 by le_S_S, ex2_intro, at_succ/
-| #cs #i1 #i2 #_ #IH #j1 #H elim (IH … H) -i1
- /3 width=3 by le_S_S, ex2_intro, at_false/
-]
-qed-.
-
-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/
- |*: @or_intror #H elim (at_inv_empty … H) #H1 #H2 destruct
- ]
-| * [2: #i1 ] * [2,4: #i2 ]
- [ elim (IH i1 i2) -IH
- /4 width=1 by at_inv_true_succ, at_succ, or_introl, or_intror/
- | -IH /3 width=3 by at_inv_true_O_S, or_intror/
- | -IH /3 width=3 by at_inv_true_S_O, or_intror/
- | -IH /2 width=1 by or_introl, at_zero/
- ]
-| #i1 * [2: #i2 ]
- [ elim (IH i1 i2) -IH
- /4 width=1 by at_inv_false_S, at_false, or_introl, or_intror/
- | -IH /3 width=3 by at_inv_false_O, or_intror/
- ]
-]
-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.
-#cs #i1 elim i1 -i1 //
-#j1 #IHi #i2 #H elim (at_monotonic … H j1) -H
-/3 width=3 by le_to_lt_to_lt/
-qed-.
-
-lemma at_increasing_strict: ∀cs,i1,i2. @⦃i1, Ⓕ @ cs⦄ ≡ i2 →
- i1 < i2 ∧ @⦃i1, cs⦄ ≡ ⫰i2.
-#cs #i1 #i2 #H elim (at_inv_false … H) -H
-#j2 #H #Hj2 destruct /4 width=2 by conj, at_increasing, le_S_S/
-qed-.
-
-(* Main properties **********************************************************)
-
-theorem at_mono: ∀cs,i,i1. @⦃i, cs⦄ ≡ i1 → ∀i2. @⦃i, cs⦄ ≡ i2 → i1 = i2.
-#cs #i #i1 #H elim H -cs -i -i1
-[2,3,4: #cs [2,3: #i #i1 #_ #IH ] ] #i2 #H
-[ elim (at_inv_true_succ_sn … H) -H
- #j2 #H destruct #H >(IH … H) -cs -i -i1 //
-| elim (at_inv_false … H) -H
- #j2 #H destruct #H >(IH … H) -cs -i -i1 //
-| /2 width=2 by at_inv_true_zero_sn/
-| /2 width=1 by at_inv_empty_zero_sn/
-]
-qed-.
-
-theorem at_inj: ∀cs,i1,i. @⦃i1, cs⦄ ≡ i → ∀i2. @⦃i2, cs⦄ ≡ i → i1 = i2.
-#cs #i1 #i #H elim H -cs -i1 -i
-[2,3,4: #cs [ |2,3: #i1 #i #_ #IH ] ] #i2 #H
-[ /2 width=2 by at_inv_true_zero_dx/
-| elim (at_inv_true_succ_dx … H) -H
- #j2 #H destruct #H >(IH … H) -cs -i1 -i //
-| elim (at_inv_false … H) -H
- #j #H destruct #H >(IH … H) -cs -i1 -j //
-| /2 width=1 by at_inv_empty_zero_dx/
-]
-qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "ground_2/notation/relations/isidentity_1.ma".
-include "ground_2/relocation/trace_after.ma".
-include "ground_2/relocation/trace_sle.ma".
-
-(* RELOCATION TRACE *********************************************************)
-
-definition isid: predicate trace ≝ λcs. ∥cs∥ = |cs|.
-
-interpretation "test for identity (trace)"
- 'IsIdentity cs = (isid cs).
-
-definition t_reflexive: ∀S:Type[0]. predicate (trace → relation S) ≝
- λS,R. ∀a. ∃∃t. 𝐈⦃t⦄ & R t a a.
-
-(* Basic properties *********************************************************)
-
-lemma isid_empty: 𝐈⦃◊⦄.
-// qed.
-
-lemma isid_true: ∀cs. 𝐈⦃cs⦄ → 𝐈⦃Ⓣ @ cs⦄.
-// qed.
-
-(* Basic inversion lemmas ***************************************************)
-
-lemma isid_inv_true: ∀cs. 𝐈⦃Ⓣ @ cs⦄ → 𝐈⦃cs⦄.
-/2 width=1 by injective_S/ qed-.
-
-lemma isid_inv_false: ∀cs. 𝐈⦃Ⓕ @ cs⦄ → ⊥.
-/3 width=4 by colength_le, lt_le_false/ qed-.
-
-lemma isid_inv_cons: ∀cs,b. 𝐈⦃b @ cs⦄ → 𝐈⦃cs⦄ ∧ b = Ⓣ.
-#cs * #H /3 width=1 by isid_inv_true, conj/
-elim (isid_inv_false … H)
-qed-.
-
-(* Properties on application ************************************************)
-
-lemma isid_at: ∀cs. (∀i1,i2. @⦃i1, cs⦄ ≡ i2 → i1 = i2) → 𝐈⦃cs⦄.
-#cs elim cs -cs // * /2 width=1 by/
-qed.
-
-(* Inversion lemmas on application ******************************************)
-
-lemma isid_inv_at: ∀cs,i1,i2. @⦃i1, cs⦄ ≡ i2 → 𝐈⦃cs⦄ → i1 = i2.
-#cs #i1 #i2 #H elim H -cs -i1 -i2 /4 width=1 by isid_inv_true, eq_f/
-#cs #i1 #i2 #_ #IH #H elim (isid_inv_false … H)
-qed-.
-
-(* Properties on composition ************************************************)
-
-lemma isid_after_sn: ∀cs2. ∃∃cs1. 𝐈⦃cs1⦄ & cs1 ⊚ cs2 ≡ cs2.
-#cs2 elim cs2 -cs2 /2 width=3 by after_empty, ex2_intro/
-#b #cs2 * /3 width=3 by isid_true, after_true, ex2_intro/
-qed-.
-
-lemma isid_after_dx: ∀cs1. ∃∃cs2. 𝐈⦃cs2⦄ & cs1 ⊚ cs2 ≡ cs1.
-#cs1 elim cs1 -cs1 /2 width=3 by after_empty, ex2_intro/
-* #cs1 * /3 width=3 by isid_true, after_true, after_false, ex2_intro/
-qed-.
-
-lemma after_isid_sn: ∀cs1,cs2. cs1 ⊚ cs2 ≡ cs2 → 𝐈⦃cs1⦄ .
-#cs1 #cs2 #H elim (after_inv_length … H) -H //
-qed.
-
-lemma after_isid_dx: ∀cs1,cs2. cs1 ⊚ cs2 ≡ cs1 → 𝐈⦃cs2⦄ .
-#cs1 #cs2 #H elim (after_inv_length … H) -H //
-qed.
-
-(* Inversion lemmas on composition ******************************************)
-
-lemma after_isid_inv_sn: ∀cs1,cs2,cs. cs1 ⊚ cs2 ≡ cs → 𝐈⦃cs1⦄ → cs = cs2.
-#cs1 #cs2 #cs #H elim H -cs1 -cs2 -cs //
-#cs1 #cs2 #cs #_ [ #b ] #IH #H
-[ >IH -IH // | elim (isid_inv_false … H) ]
-qed-.
-
-lemma after_isid_inv_dx: ∀cs1,cs2,cs. cs1 ⊚ cs2 ≡ cs → 𝐈⦃cs2⦄ → cs = cs1.
-#cs1 #cs2 #cs #H elim H -cs1 -cs2 -cs //
-#cs1 #cs2 #cs #_ [ #b ] #IH #H
-[ elim (isid_inv_cons … H) -H #H >IH -IH // | >IH -IH // ]
-qed-.
-
-lemma after_inv_isid3: ∀t1,t2,t. t1 ⊚ t2 ≡ t → 𝐈⦃t⦄ → 𝐈⦃t1⦄ ∧ 𝐈⦃t2⦄.
-#t1 #t2 #t #H elim H -t1 -t2 -t
-[ /2 width=1 by conj/
-| #t1 #t2 #t #_ #b #IHt #H elim (isid_inv_cons … H) -H
- #Ht #H elim (IHt Ht) -t /2 width=1 by isid_true, conj/
-| #t1 #t2 #t #_ #_ #H elim (isid_inv_false … H)
-]
-qed-.
-
-(* Forward on inclusion *****************************************************)
-
-lemma sle_isid1_fwd: ∀t1,t2. t1 ⊆ t2 → 𝐈⦃t1⦄ → t1 = t2.
-#t1 #t2 #H elim H -t1 -t2 //
-[ #t1 #t2 #_ #IH #H lapply (isid_inv_true … H) -H
- #HT1 @eq_f2 // @IH @HT1 (**) (* full auto fails *)
-| #t1 #t2 #b #_ #_ #H elim (isid_inv_false … H)
-]
-qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "ground_2/notation/relations/isuniform_1.ma".
-include "ground_2/relocation/trace_isid.ma".
-
-(* RELOCATION TRACE *********************************************************)
-
-inductive isun: predicate trace ≝
-| isun_id : ∀t. 𝐈⦃t⦄ → isun t
-| isun_false: ∀t. isun t → isun (Ⓕ@t)
-.
-
-interpretation "test for uniformity (trace)"
- 'IsUniform t = (isun t).
-
-(* Basic inversion lennas ***************************************************)
-
-fact isun_inv_true_aux: ∀t. 𝐔⦃t⦄ → ∀u. t = Ⓣ@u → 𝐈⦃u⦄.
-#t * -t
-[ #t #Ht #u #H destruct /2 width=1 by isid_inv_true/
-| #t #_ #u #H destruct
-]
-qed-.
-
-lemma isun_inv_true: ∀t. 𝐔⦃Ⓣ@t⦄ → 𝐈⦃t⦄.
-/2 width=3 by isun_inv_true_aux/ qed-.
-
-fact isun_inv_false_aux: ∀t. 𝐔⦃t⦄ → ∀u. t = Ⓕ@u → 𝐔⦃u⦄.
-#t * -t
-[ #t #Ht #u #H destruct elim (isid_inv_false … Ht)
-| #t #Ht #u #H destruct //
-]
-qed-.
-
-lemma isun_inv_false: ∀t. 𝐔⦃Ⓕ@t⦄ → 𝐔⦃t⦄.
-/2 width=3 by isun_inv_false_aux/ qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "ground_2/relocation/trace_at.ma".
-
-(* RELOCATION TRACE *********************************************************)
-
-inductive sle: relation trace ≝
-| sle_empty: sle (◊) (◊)
-| sle_true : ∀t1,t2. sle t1 t2 → sle (Ⓣ @ t1) (Ⓣ @ t2)
-| sle_false: ∀t1,t2,b. sle t1 t2 → sle (Ⓕ @ t1) (b @ t2)
-.
-
-interpretation
- "inclusion (trace)"
- 'subseteq t1 t2 = (sle t1 t2).
-
-(* Basic properties *********************************************************)
-
-(* Basic forward lemmas *****************************************************)
-
-lemma sle_fwd_length: ∀t1,t2. t1 ⊆ t2 → |t1| = |t2|.
-#t1 #t2 #H elim H -t1 -t2 //
-qed-.
-
-lemma sle_fwd_colength: ∀t1,t2. t1 ⊆ t2 → ∥t1∥ ≤ ∥t2∥.
-#t1 #t2 #H elim H -t1 -t2 /2 width=1 by le_S_S/
-#t1 #t2 * /2 width=1 by le_S/
-qed-.
-
-(* Inversion lemmas on application ******************************************)
-
-lemma sle_inv_at: ∀t1,t2. t1 ⊆ t2 →
- ∀i,i1,i2. @⦃i, t1⦄ ≡ i1 → @⦃i, t2⦄ ≡ i2 → i2 ≤ i1.
-#t1 #t2 #H elim H -t1 -t2
-[ #i #i1 #i2 #_ #H2 elim (at_inv_empty … H2) -H2 //
-| #t1 #t2 #_ #IH #i #i1 #i2 #H0 #H2 elim (at_inv_true … H2) -H2 * //
- #j1 #j2 #H1 #H2 #Hj destruct elim (at_inv_true_succ_sn … H0) -H0
- /3 width=3 by le_S_S/
-| #t1 #t2 * #_ #IH #i #i1 #i2 #H0 #H2
- [ elim (at_inv_true … H2) -H2 * //
- #j #j2 #H1 #H2 #Hj2 destruct elim (at_inv_false … H0) -H0
- #j1 #H #Hj1 destruct elim (at_monotonic … Hj1 j) -Hj1 //
- #x #H1x #H2x @le_S_S /4 width=3 by lt_to_le, le_to_lt_to_lt/ (**) (* full auto too slow *)
- | elim (at_inv_false … H2) elim (at_inv_false … H0) -H0 -H2
- /3 width=3 by le_S_S/
- ]
-]
-qed-.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "ground_2/notation/functions/complement_1.ma".
-include "ground_2/relocation/trace.ma".
-
-(* RELOCATION TRACE *********************************************************)
-
-let rec snot (t:trace) on t ≝ match t with
-[ nil ⇒ ◊
-| cons b t ⇒ (¬ b) @ snot t
-].
-
-interpretation
- "complement (trace)"
- 'Complement t = (snot t).
-
-(* Basic properties *********************************************************)
-
-lemma snot_empty: ∁ (◊) = ◊.
-// qed.
-
-lemma snot_inh: ∀t,b. ∁ (b@t) = (¬ b) @ ∁ t.
-// qed.
-
-lemma snot_true: ∀t. ∁ (Ⓣ @ t) = Ⓕ @ ∁ t.
-// qed.
-
-lemma snot_false: ∀t. ∁ (Ⓕ @ t) = Ⓣ @ ∁ t.
-// qed.
-
-lemma snot_length: ∀t. |∁ t| = |t|.
-#t elim t -t normalize //
-qed.
-
-lemma snot_colength: ∀t. ∥∁ t∥ = |t| - ∥t∥.
-#t elim t -t //
-* /2 width=1 by minus_Sn_m/
-qed.
+++ /dev/null
-(**************************************************************************)
-(* ___ *)
-(* ||M|| *)
-(* ||A|| A project by Andrea Asperti *)
-(* ||T|| *)
-(* ||I|| Developers: *)
-(* ||T|| The HELM team. *)
-(* ||A|| http://helm.cs.unibo.it *)
-(* \ / *)
-(* \ / This file is distributed under the terms of the *)
-(* v GNU General Public License Version 2 *)
-(* *)
-(**************************************************************************)
-
-include "ground_2/notation/relations/runion_3.ma".
-include "ground_2/relocation/trace_isid.ma".
-
-(* RELOCATION TRACE *********************************************************)
-
-inductive sor: relation3 trace trace trace ≝
- | sor_empty: sor (◊) (◊) (◊)
- | sor_inh : ∀cs1,cs2,cs. sor cs1 cs2 cs →
- ∀b1,b2. sor (b1 @ cs1) (b2 @ cs2) ((b1 ∨ b2) @ cs).
-
-interpretation
- "union (trace)"
- 'RUnion L1 L2 L = (sor L2 L1 L).
-
-(* Basic properties *********************************************************)
-
-lemma sor_length: ∀cs1,cs2. |cs1| = |cs2| →
- ∃∃cs. cs2 ⋓ cs1 ≡ cs & |cs| = |cs1| & |cs| = |cs2|.
-#cs1 elim cs1 -cs1
-[ #cs2 #H >(length_inv_zero_sn … H) -H /2 width=4 by sor_empty, ex3_intro/
-| #b1 #cs1 #IH #x #H elim (length_inv_succ_sn … H) -H
- #cs2 #b2 #H12 #H destruct elim (IH … H12) -IH -H12
- #cs #H12 #H1 #H2 @(ex3_intro … ((b1 ∨ b2) @ cs)) /2 width=1 by sor_inh/ (**) (* explicit constructor *)
-]
-qed-.
-
-lemma sor_sym: ∀cs1,cs2,cs. cs1 ⋓ cs2 ≡ cs → cs2 ⋓ cs1 ≡ cs.
-#cs1 #cs2 #cs #H elim H -cs1 -cs2 -cs /2 width=1 by sor_inh/
-qed-.
-
-(* Basic inversion lemmas ***************************************************)
-
-lemma sor_inv_length: ∀cs1,cs2,cs. cs2 ⋓ cs1 ≡ cs →
- ∧∧ |cs1| = |cs2| & |cs| = |cs1| & |cs| = |cs2|.
-#cs1 #cs2 #cs #H elim H -cs1 -cs2 -cs /2 width=1 by and3_intro/
-#cs1 #cs2 #cs #_ #b1 #b2 * /2 width=1 by and3_intro/
-qed-.
-
-(* Basic forward lemmas *****************************************************)
-
-lemma sor_fwd_isid_sn: ∀cs1,cs2,cs. cs1 ⋓ cs2 ≡ cs → 𝐈⦃cs1⦄ → 𝐈⦃cs⦄.
-#cs1 #cs2 #cs #H elim H -cs1 -cs2 -cs //
-#cs1 #cs2 #cs #_ #b1 #b2 #IH #H elim (isid_inv_cons … H) -H
-/3 width=1 by isid_true/
-qed-.
-
-lemma sor_fwd_isid_dx: ∀cs1,cs2,cs. cs1 ⋓ cs2 ≡ cs → 𝐈⦃cs2⦄ → 𝐈⦃cs⦄.
-/3 width=4 by sor_fwd_isid_sn, sor_sym/ qed-.
class "grass"
[ { "multiple relocation" * } {
[ { "" * } {
- [ "rtmap_eq ( ? ≗ ? )" "rtmap_isid ( 𝐈⦃?⦄ )" "rtmap_id" "rtmap_at ( @⦃?,?⦄ ≡ ? )" "rtmap_istot ( 𝐓⦃?⦄ )" "rtmap_sle ( ? ⊆ ? )" * ]
- [ "nstream" "nstream_lift ( ↑? ) ( ⫯? )" "nstream_eq" "nstream_isid" "nstream_id ( 𝐈𝐝 )" "nstream_istot ( ?@❴?❵ )" "nstream_after ( ? ∘ ? ) ( ? ⊚ ? ≡ ? )" * ]
+ [ "rtmap" "rtmap_eq ( ? ≗ ? )" "rtmap_tl ( ↓? )" "rtmap_minus ( ? - ? )" "rtmap_isid ( 𝐈⦃?⦄ )" "rtmap_id" "rtmap_sle ( ? ⊆ ? )" "rtmap_at ( @⦃?,?⦄ ≡ ? )" "rtmap_istot ( 𝐓⦃?⦄ )" "rtmap_after ( ? ⊚ ? ≡ ? )" * ]
+ [ "nstream ( ↑? ) ( ⫯? )" "nstream_eq" "nstream_isid" "nstream_id ( 𝐈𝐝 )" "nstream_istot ( ?@❴?❵ )" "nstream_after ( ? ∘ ? )" * ]
[ "trace ( ∥?∥ )" "trace_at ( @⦃?,?⦄ ≡ ? )" "trace_after ( ? ⊚ ? ≡ ? )" "trace_isid ( 𝐈⦃?⦄ )" "trace_isun ( 𝐔⦃?⦄ )"
"trace_sle ( ? ⊆ ? )" "trace_sor ( ? ⋓ ? ≡ ? )" "trace_snot ( ∁ ? )" * ]
[ "mr2" "mr2_at ( @⦃?,?⦄ ≡ ? )" "mr2_plus ( ? + ? )" "mr2_minus ( ? ▭ ? ≡ ? )" * ]
projects / helm.git / commitdiff