Set Implicit Arguments.

Require Export transducer.
Section s.
  Context {atom X: Set}{𝐀 : Atom atom} {𝐗 : Alphabet 𝐀 X}.

  Reserved Notation " u ≡' v " (at level 80).
  Inductive αequiv' : word → word → Prop :=
  | αt' u v w : u ≡' v → v ≡' w → u ≡' w
  | αε' : [] ≡' []
  | αr' u v l : u ≡' v → u++[l] ≡' v++[l]
  | αl' u v l : u ≡' v → l::u ≡' l::v
  | αα' a b u : b #α u → a #α u → u ≡' [(a,b)]∙u
  where " u ≡' v " := (αequiv' u v).
  Hint Constructors αequiv'.

  Theorem equiv_alt u v : u ≡ v ↔ u ≡' v.

  Global Instance αequiv'_equivalence : Equivalence αequiv'.

  Lemma αequiv'_app_left u v w : u ≡' v → w++u≡'w++v.

  Lemma αequiv'_app_right (u v w : word) : u ≡' v → u++w≡'v++w.

  Global Instance αequiv'_app :
    Proper (αequiv' ==> αequiv' ==> αequiv') (@app letter).

  Lemma αequiv'_binding u v : u ≡' v → ∀ a, 𝗙 a u = 𝗙 a v.

  Lemma αequiv'_perm u v π : u ≡' v → π ∙ u ≡' π ∙ v.

  Reserved Notation " u =α= v " (at level 80).
  Inductive αequiv2 : word → word → Prop :=
  | αε2 : [] =α= []
  | αm u v l : u =α= v → u++[l] =α= v++[l]
  | αα2 a b u1 u2 v1 v2 :
      a ⋄ u2 → b ⋄ v2 →
      (∀ c, c # a → c # b → c # u1++u2++v1++v2 →
            u1++open c::[(a,c)]∙u2 =α= v1++open c::[(b,c)]∙v2)
      → u1++open a::u2++[close a] =α= v1++open b::v2++[close b]
  where " u =α= v " := (αequiv2 u v).
  Hint Constructors αequiv2.

  Remark αequiv_alternate u1 u2 v1 v2 a b c :
    c #α u2 → c #α v2 → a ⋄ u2 → b ⋄ v2 →
    u1++open c::[(a,c)]∙u2 ≡ v1++open c::[(b,c)]∙v2 →
    u1++open a::u2++[close a] ≡ v1++open b::v2++[close b].

  Lemma αequiv2_to_αequiv u v : u =α= v → u≡v.

  Lemma αequiv_to_αequiv2 u v : u≡v → u =α= v.
End s.