{-# OPTIONS --without-K --safe #-}
open import Labelled-transition-system
module Similarity.Weak.Up-to {ℓ} (lts : LTS ℓ) where
open import Logical-equivalence using (_⇔_)
open import Prelude
open import Equational-reasoning
open import Expansion lts using (Expansion)
open import Relation
open import Similarity.Weak lts
import Similarity.Weak.Equational-reasoning-instances
import Up-to
open LTS lts
open Up-to StepC public
Up-to-expansion-and-weak-similarity : Trans₂ ℓ Proc
Up-to-expansion-and-weak-similarity R =
Expansion ∞ ⊙ R ⊙ Weak-similarity ∞
up-to-expansion-and-weak-similarity-monotone :
Monotone Up-to-expansion-and-weak-similarity
up-to-expansion-and-weak-similarity-monotone R⊆S =
Σ-map id (Σ-map id (Σ-map id (Σ-map R⊆S id)))
up-to-expansion-and-weak-similarity-size-preserving :
Size-preserving Up-to-expansion-and-weak-similarity
up-to-expansion-and-weak-similarity-size-preserving =
_⇔_.from (monotone→⇔ up-to-expansion-and-weak-similarity-monotone)
(λ where
{x = p , q} (r , p≳r , s , r≼s , s≼q) →
p ∼⟨ p≳r ⟩
r ∼′⟨ r≼s ⟩ ≼:
s ∼⟨ s≼q ⟩■
q)