------------------------------------------------------------------------
-- An alternative (non-standard) classical definition of weak
-- bisimilarity
------------------------------------------------------------------------

-- This definition is based on the function "wb" in Section 6.5.1 of
-- Pous and Sangiorgi's "Enhancements of the bisimulation proof
-- method".

{-# OPTIONS --without-K --safe #-}

open import Labelled-transition-system

module Bisimilarity.Weak.Alternative.Classical {} (lts : LTS ) where

open import Prelude

import Bisimilarity.Classical

open LTS lts

-- We get weak bisimilarity by instantiating strong bisimilarity with
-- a different LTS.

private
  module WB = Bisimilarity.Classical (weak lts)

open WB public
  using (⟪_,_⟫)
  renaming ( Bisimulation  to Weak-bisimulation
           ; Bisimilarity′ to Weak-bisimilarity′
           ; Bisimilarity  to Weak-bisimilarity
           ; _∼_           to _≈_
           )