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

open import dtt
open import equality
open import RTC
open import Simulations


-------------------------------------------
-- _* is indeed reflexive and transitive --
-------------------------------------------

module RTC.free-monad {I : Set} (w : IS 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*)


reflexive : (X : Pow I) → X ⊂ ⟦ w * ⟧ X
reflexive X {i} x = Leaf , λ _ → x

transitive : (X : Pow I) → ⟦ w ⟧ (⟦ w * ⟧ X) ⊂ ⟦ w * ⟧ X
transitive X {i} (a , f) = (a ◂ (λ d → fst (f d))) , λ ds → snd (f (fst ds)) (snd ds)




module _ (X Y : Pow I) (incl : X ⊂ Y) (trans : ⟦ w ⟧ Y ⊂ Y) where
  {-# TERMINATING #-}
  least : ⟦ w * ⟧ X ⊂ Y
  least {i} (Leaf , f) = incl (f ⋆)
  least {i} (a ◂ as , f) =
    -- recursive call, we remove the root "a" from the well-founded tree
    let rec-call d = least ((as d) , (λ ds → f (d , ds))) in
    trans (a , (λ d → rec-call d))


-- the same, but with an auxiliary function to make the termination checker happy...
module _ (X Y : Pow I) (incl : X ⊂ Y) (trans : ⟦ w ⟧ Y ⊂ Y) where

  private lemma : (i : I) (as : A* i) (f : (ds : D* i as) → X (n* as ds)) → Y i
  lemma i Leaf f = incl (f ⋆)
  lemma i (a ◂ as) f = trans (a , (λ d → lemma (n a d) (as d) (λ ds → f (d , ds))))

  least-bis : ⟦ w * ⟧ X ⊂ Y
  least-bis {i} (as , f) = lemma i as f