```------------------------------------------------------------------------
-- The various approaches are equivalent
------------------------------------------------------------------------

module NonDeterministic.Equivalence where

open import Coinduction
open import Data.Colist

open import NonDeterministic.Expr
open import NonDeterministic.EasyToWorkWith
renaming (_HasTrace_ to _HasTraceW_)
open import NonDeterministic.LongestPrefix
renaming (_HasTrace_ to _HasTraceL_)

------------------------------------------------------------------------
-- EasyToWorkWith to LongestPrefix

WtoL[] : ∀ {e} → e HasTraceW [] → []⊑Trace[ e ]
WtoL[] (nop s) = nop (♯ WtoL[] (♭ s))

WtoL : ∀ {e ms} → e HasTraceW ms → e HasTraceL ms
WtoL s        ⊥                  = ⊥
WtoL s        []                 = []   (WtoL[] s)
WtoL (nop  s) (m ∷ p⊑ms)         = nop  (WtoL s (m ∷ p⊑ms))
WtoL (tick s) (.(user _) ∷ p⊑ms) = tick (WtoL (♭ s) p⊑ms)
WtoL (tock s) (.(ext  _) ∷ p⊑ms) = tock (WtoL (♭ s) p⊑ms)

------------------------------------------------------------------------
-- LongestPrefix to EasyToWorkWith

nop-lemmaL : ∀ {e ms} → nop e HasTraceL ms → ♭ e HasTraceL ms
nop-lemmaL s x = drop-nop (s x)
where
drop-nop : ∀ {ms e} → ms ⊑Trace[ nop e ] → ms ⊑Trace[ ♭ e ]
drop-nop ⊥             = ⊥
drop-nop ([] (nop x′)) = [] (♭ x′)
drop-nop (nop  x′)     = x′
drop-nop (tock x′)     = tock (drop-nop x′)

tick-lemmaL : ∀ {m e ms} →
tick m e HasTraceL user m ∷ ms → ♭ e HasTraceL ♭ ms
tick-lemmaL {m} s x with s (user m ∷ x)
... | tick x′ = x′

tock-lemmaL : ∀ {m e ms} → e HasTraceL ext m ∷ ms → e HasTraceL ♭ ms
tock-lemmaL {m} s x = drop-tock (s (ext m ∷ x))
where
drop-tock : ∀ {ms e} → ext m ∷ ms ⊑Trace[ e ] → ms ⊑Trace[ e ]
drop-tock (nop  x′) = nop (drop-tock x′)
drop-tock (tock x′) = x′

mutual

LtoW : ∀ e ms → e HasTraceL ms → e HasTraceW ms
LtoW (nop e)    []             s = nop (♯ LtoW (♭ e) [] (nop-lemmaL s))
LtoW (nop e)    (m ∷ ms)       s = LtoW′ s (s (m ∷ ⊥))
LtoW (tick m e) []             s with s []
LtoW (tick m e) []             s | [] ()
LtoW (tick m e) (m′      ∷ ms) s with s (m′ ∷ ⊥)
LtoW (tick m e) (user .m ∷ ms) s | tick x = tick (♯ LtoW (♭ e) (♭ ms) (tick-lemmaL s))
LtoW (tick m e) (ext  m′ ∷ ms) s | tock x = tock (♯ LtoW (tick m e) (♭ ms) (tock-lemmaL s))

LtoW′ : ∀ {e m ms} →
e HasTraceL m ∷ ms → m ∷ ⊥ ⊑Trace[ e ] → e HasTraceW m ∷ ms
LtoW′ s (nop  x) = nop (LtoW′ (nop-lemmaL s) x)
LtoW′ s (tick x) = tick (♯ LtoW _ _ (tick-lemmaL s))
LtoW′ s (tock x) = tock (♯ LtoW _ _ (tock-lemmaL s))
```