{-# OPTIONS --without-K --safe --guardedness --no-sized-types #-}

open import prelude
open import RTC

-- Sambinic like interaction formula between "⟦ w * ⟧ U" and "ν w⊥"
module InteractionSystems.execution {I : Set} (w : IS I) (U : Pow I) where

  open IS w renaming (Command to A; Response to D; next to n)
  open IS (w *) renaming (Command to A* ; Response to D* ; next to n*)

  private lemma_aux : (i : I) → (as : A* i) → ((ds : D* i as) → U (n* {i} as ds)) → ν (w ⊥) i → U ≬ (ν (w ⊥))
  lemma_aux i Leaf r T = ( i , ( r ⋆ , T ) )
  lemma_aux i (a ◂ f) r T =
    let tmp = νElim T in
    let d = (fst tmp) a in
    let i' : I
        i' = n a d in
    lemma_aux i' (f d) (λ ds → r ( d , ds )) (snd tmp a)

  lemma : (⟦ w * ⟧ U) ≬ (ν (w ⊥)) → U ≬ (ν (w ⊥))
  lemma ( i , ( ( t , r ) , T ) ) = lemma_aux i t r T


{- I had to add "lemma_aux" to get around a problem with termination checking: sometimes, termination
   checking doesn't go inside pairs... For example, the following doesn't pass the termination test:

  test : ((i : I) -> (a : A i) -> D i a) -> (i : I) -> (⟦ w * ⟧ X i) -> One
  test f i ( Leaf , r ) = ⋆
  test f i ( (a ◂ t) , r ) = test f (n a (f i a)) ( t (f i a) , (λ ds → r ( f i a , ds )) )
-}