{-# OPTIONS --without-K --safe #-}
open import Labelled-transition-system
module Labelled-transition-system.Equational-reasoning-instances
{ℓ} (lts : LTS ℓ) where
open import Prelude
open import Equational-reasoning
open LTS lts
private
get : ∀ {μ} → T (silent? μ) → Silent μ
get {μ} _ with silent? μ
get {μ} () | no _
get {μ} _ | yes s = s
instance
convert⟶ : ∀ {μ} → Convertible _[ μ ]⟶_ _[ μ ]⟶_
convert⟶ = is-convertible id
convert⟶⇒ : ∀ {μ} {s : T (silent? μ)} → Convertible _[ μ ]⟶_ _⇒_
convert⟶⇒ {s = s} = is-convertible (⟶→⇒ (get s))
convert⟶[]⇒ : ∀ {μ} → Convertible _[ μ ]⟶_ _[ μ ]⇒_
convert⟶[]⇒ = is-convertible ⟶→[]⇒
convert⟶⇒̂ : ∀ {μ} → Convertible _[ μ ]⟶_ _[ μ ]⇒̂_
convert⟶⇒̂ = is-convertible ⟶→⇒̂
convert⟶⟶̂ : ∀ {μ} → Convertible _[ μ ]⟶_ _[ μ ]⟶̂_
convert⟶⟶̂ = is-convertible ⟶→⟶̂
convert⇒ : Convertible _⇒_ _⇒_
convert⇒ = is-convertible id
convert⇒⇒̂ : ∀ {μ} {s : T (silent? μ)} → Convertible _⇒_ _[ μ ]⇒̂_
convert⇒⇒̂ {s = s} = is-convertible (silent (get s))
convert[]⇒ : ∀ {μ} → Convertible _[ μ ]⇒_ _[ μ ]⇒_
convert[]⇒ = is-convertible id
convert[]⇒⇒ : ∀ {μ} {s : T (silent? μ)} → Convertible _[ μ ]⇒_ _⇒_
convert[]⇒⇒ {s = s} = is-convertible ([]⇒→⇒ (get s))
convert[]⇒⇒̂ : ∀ {μ} → Convertible _[ μ ]⇒_ _[ μ ]⇒̂_
convert[]⇒⇒̂ = is-convertible ⇒→⇒̂
convert⇒̂ : ∀ {μ} → Convertible _[ μ ]⇒̂_ _[ μ ]⇒̂_
convert⇒̂ = is-convertible id
convert⇒̂⇒ : ∀ {μ} {s : T (silent? μ)} → Convertible _[ μ ]⇒̂_ _⇒_
convert⇒̂⇒ {s = s} = is-convertible (⇒̂→⇒ (get s))
convert⇒̂[]⇒ : ∀ {μ} {¬s : if (silent? μ) then ⊥ else ⊤} →
Convertible _[ μ ]⇒̂_ _[ μ ]⇒_
convert⇒̂[]⇒ {μ} with silent? μ
convert⇒̂[]⇒ {¬s = ()} | yes _
convert⇒̂[]⇒ | no ¬s = is-convertible (⇒̂→[]⇒ ¬s)
convert⟶̂ : ∀ {μ} → Convertible _[ μ ]⟶̂_ _[ μ ]⟶̂_
convert⟶̂ = is-convertible id
convert⟶̂⇒ : ∀ {μ} {s : T (silent? μ)} → Convertible _[ μ ]⟶̂_ _⇒_
convert⟶̂⇒ {s = s} = is-convertible (⟶̂→⇒ (get s))
convert⟶̂⇒̂ : ∀ {μ} → Convertible _[ μ ]⟶̂_ _[ μ ]⇒̂_
convert⟶̂⇒̂ = is-convertible ⟶̂→⇒̂
reflexive⇒ : Reflexive _⇒_
reflexive⇒ = is-reflexive done
reflexive⟶̂ : ∀ {μ} {s : T (silent? μ)} → Reflexive _[ μ ]⟶̂_
reflexive⟶̂ {s = s} = is-reflexive (done (get s))
reflexive⇒̂ : ∀ {μ} {s : T (silent? μ)} → Reflexive _[ μ ]⇒̂_
reflexive⇒̂ {s = s} = is-reflexive (silent (get s) done)
trans⇒ : Transitive _⇒_ _⇒_
trans⇒ = is-transitive ⇒-transitive
trans⟶⇒ : ∀ {μ} {s : T (silent? μ)} → Transitive _[ μ ]⟶_ _⇒_
trans⟶⇒ {s = s} = is-transitive (⇒-transitive ∘ ⟶→⇒ (get s))
trans⇒̂⇒ : ∀ {μ} {s : T (silent? μ)} → Transitive _[ μ ]⇒̂_ _⇒_
trans⇒̂⇒ {s = s} = is-transitive (⇒-transitive ∘ ⇒̂→⇒ (get s))
trans⟶̂⇒ : ∀ {μ} {s : T (silent? μ)} → Transitive _[ μ ]⟶̂_ _⇒_
trans⟶̂⇒ {s = s} = is-transitive (⇒-transitive ∘ ⟶̂→⇒ (get s))
trans⇒[]⇒ : ∀ {μ} → Transitive _⇒_ _[ μ ]⇒_
trans⇒[]⇒ = is-transitive ⇒[]⇒-transitive
trans⟶[]⇒ : ∀ {μ μ′} {s : T (silent? μ′)} →
Transitive _[ μ′ ]⟶_ _[ μ ]⇒_
trans⟶[]⇒ {s = s} = is-transitive (⇒[]⇒-transitive ∘ ⟶→⇒ (get s))
trans[]⇒[]⇒ : ∀ {μ μ′} {s : T (silent? μ′)} →
Transitive _[ μ′ ]⇒_ _[ μ ]⇒_
trans[]⇒[]⇒ {s = s} = is-transitive (⇒[]⇒-transitive ∘ []⇒→⇒ (get s))
trans⟶̂[]⇒ : ∀ {μ μ′} {s : T (silent? μ′)} →
Transitive _[ μ′ ]⟶̂_ _[ μ ]⇒_
trans⟶̂[]⇒ {s = s} = is-transitive (⇒[]⇒-transitive ∘ ⟶̂→⇒ (get s))
trans⇒⇒̂ : ∀ {μ} → Transitive _⇒_ _[ μ ]⇒̂_
trans⇒⇒̂ = is-transitive ⇒⇒̂-transitive
trans⟶⇒̂ : ∀ {μ μ′} {s : T (silent? μ′)} →
Transitive _[ μ′ ]⟶_ _[ μ ]⇒̂_
trans⟶⇒̂ {s = s} = is-transitive (⇒⇒̂-transitive ∘ ⟶→⇒ (get s))
trans[]⇒⇒̂ : ∀ {μ μ′} {s : T (silent? μ′)} →
Transitive _[ μ′ ]⇒_ _[ μ ]⇒̂_
trans[]⇒⇒̂ {s = s} = is-transitive (⇒⇒̂-transitive ∘ []⇒→⇒ (get s))
trans[]⇒̂⇒̂ : ∀ {μ μ′} {s : T (silent? μ′)} →
Transitive _[ μ′ ]⇒̂_ _[ μ ]⇒̂_
trans[]⇒̂⇒̂ {s = s} = is-transitive (⇒⇒̂-transitive ∘ ⇒̂→⇒ (get s))
trans⟶̂⇒̂ : ∀ {μ μ′} {s : T (silent? μ′)} →
Transitive _[ μ′ ]⟶̂_ _[ μ ]⇒̂_
trans⟶̂⇒̂ {s = s} = is-transitive (⇒⇒̂-transitive ∘ ⟶̂→⇒ (get s))
trans′⇒⟶ : ∀ {μ} {s : T (silent? μ)} → Transitive′ _⇒_ _[ μ ]⟶_
trans′⇒⟶ {s = s} =
is-transitive (flip (flip ⇒-transitive ∘ ⟶→⇒ (get s)))
trans′⇒[]⇒ : ∀ {μ} {s : T (silent? μ)} → Transitive′ _⇒_ _[ μ ]⇒_
trans′⇒[]⇒ {s = s} =
is-transitive (flip (flip ⇒-transitive ∘ []⇒→⇒ (get s)))
trans′⇒⇒̂ : ∀ {μ} {s : T (silent? μ)} → Transitive′ _⇒_ _[ μ ]⇒̂_
trans′⇒⇒̂ {s = s} =
is-transitive (flip (flip ⇒-transitive ∘ ⇒̂→⇒ (get s)))
trans′⇒⟶̂ : ∀ {μ} {s : T (silent? μ)} → Transitive′ _⇒_ _[ μ ]⟶̂_
trans′⇒⟶̂ {s = s} =
is-transitive (flip (flip ⇒-transitive ∘ ⟶̂→⇒ (get s)))
trans′[]⇒⟶ : ∀ {μ μ′} {s : T (silent? μ′)} →
Transitive′ _[ μ ]⇒_ _[ μ′ ]⟶_
trans′[]⇒⟶ {s = s} =
is-transitive (flip (flip []⇒⇒-transitive ∘ ⟶→⇒ (get s)))
trans′[]⇒⇒ : ∀ {μ} → Transitive′ _[ μ ]⇒_ _⇒_
trans′[]⇒⇒ = is-transitive []⇒⇒-transitive
trans′[]⇒[]⇒ : ∀ {μ μ′} {s : T (silent? μ′)} →
Transitive′ _[ μ ]⇒_ _[ μ′ ]⇒_
trans′[]⇒[]⇒ {s = s} =
is-transitive (flip (flip []⇒⇒-transitive ∘ []⇒→⇒ (get s)))
trans′[]⇒[]⇒̂ : ∀ {μ μ′} {s : T (silent? μ′)} →
Transitive′ _[ μ ]⇒_ _[ μ′ ]⇒̂_
trans′[]⇒[]⇒̂ {s = s} =
is-transitive (flip (flip []⇒⇒-transitive ∘ ⇒̂→⇒ (get s)))
trans′[]⇒⟶̂ : ∀ {μ μ′} {s : T (silent? μ′)} →
Transitive′ _[ μ ]⇒_ _[ μ′ ]⟶̂_
trans′[]⇒⟶̂ {s = s} =
is-transitive (flip (flip []⇒⇒-transitive ∘ ⟶̂→⇒ (get s)))
trans′⇒̂⟶ : ∀ {μ μ′} {s : T (silent? μ′)} →
Transitive′ _[ μ ]⇒̂_ _[ μ′ ]⟶_
trans′⇒̂⟶ {s = s} =
is-transitive (flip (flip ⇒̂⇒-transitive ∘ ⟶→⇒ (get s)))
trans′⇒̂⇒ : ∀ {μ} → Transitive′ _[ μ ]⇒̂_ _⇒_
trans′⇒̂⇒ = is-transitive ⇒̂⇒-transitive
trans′⇒̂[]⇒ : ∀ {μ μ′} {s : T (silent? μ′)} →
Transitive′ _[ μ ]⇒̂_ _[ μ′ ]⇒_
trans′⇒̂[]⇒ {s = s} =
is-transitive (flip (flip ⇒̂⇒-transitive ∘ []⇒→⇒ (get s)))
trans′⇒̂⇒̂ : ∀ {μ μ′} {s : T (silent? μ′)} →
Transitive′ _[ μ ]⇒̂_ _[ μ′ ]⇒̂_
trans′⇒̂⇒̂ {s = s} =
is-transitive (flip (flip ⇒̂⇒-transitive ∘ ⇒̂→⇒ (get s)))
trans′⇒̂⟶̂ : ∀ {μ μ′} {s : T (silent? μ′)} →
Transitive′ _[ μ ]⇒̂_ _[ μ′ ]⟶̂_
trans′⇒̂⟶̂ {s = s} =
is-transitive (flip (flip ⇒̂⇒-transitive ∘ ⟶̂→⇒ (get s)))