{-# OPTIONS --no-termination-check  #-} 

open import Prelude hiding (P)
open import CCS.Alg
open import CCS.SemiModel
open import Algebra
open import CCS.Proc

module CCS.Proc.RestrictPar {a} {A : Type a} ⦃ disc : IsDiscrete A ⦄ where

open CCSAlg ⦃ ... ⦄ hiding (Name)
open CCSSemiModel ⦃ ... ⦄

open import Data.Set renaming (⟦_⟧ to 𝒦⟦_⟧)

private instance
  _ : CCSAlg (Proc A)
  _ = procAlg

private instance
  _ : CCSSemiModel (Proc A)
  _ = procMod

syncₒ-ν : ∀ (a : A) p q → syncₒ a p (ν a - q) ≡ ∅
syncₒ-ν a p q = 𝒦⟦ alg a p ⟧ (↯ q)
  where
  alg : ∀ (a : A) p → Ψ[ q ⦂ 𝒦 (Act A × Proc A) ] ↦ syncₒ a p (ν a - ⟪ q ⟫) ≡ ∅
  alg a p .snd = prop-coh λ q → trunc _ _
  alg a p .fst ∅ = refl
  alg a p .fst ⟅ τ , q ⟆ = refl
  alg a p .fst (xs ⟨ P⟨xs⟩ ⟩∪ ys ⟨ P⟨ys⟩ ⟩) = cong₂ _∪_ P⟨xs⟩ P⟨ys⟩ ⨾ ident ∅
  alg a p .fst ⟅ emit s b , q ⟆ with a ≟ b
  alg a p .fst ⟅ emit s b , q ⟆ | yes a≡b = refl
  alg a p .fst ⟅ inp b , q ⟆ | no a≢b = refl
  alg a p .fst ⟅ out b , q ⟆ | no a≢b = cong (bool _ _) (it-doesn't (a ≟ b) a≢b)

ν-⌊-ν   : ∀ (n : A) (p q : Proc A) → ν n - (p ⌊ ν n - q) ≡ ν n - (ν n - p ⌊ ν n - q)
ν-ν-⌊   : ∀ (n : A) (p q : Proc A) → ν n - (ν n - p ⌊ q) ≡ ν n - (ν n - p ⌊ ν n - q)
ν-ν-∥   : ∀ (n : A) (p q : Proc A) → ν n - (ν n - p ∥ q) ≡ ν n - (ν n - p ∥ ν n - q)
ν-ν-ν-⌊ : ∀ (n : A) (p q : Proc A) → ν n - p ⌊ ν n - q ≡ ν n - (ν n - p ⌊ ν n - q)
ν-∥-ν   : ∀ (n : A) (p q : Proc A) → ν n - (p ∥ ν n - q) ≡ ν n - (ν n - p ∥ ν n - q)
ν-ν-ν-∥ : ∀ (n : A) (p q : Proc A) → ν n - p ∥ ν n - q ≡ ν n - (ν n - p ∥ ν n - q)

sync-νʳ : ∀ a p (n : A) q → syncₐₒ a p (ν n - q) >>= ⟅?⟆ ∘ ν′ n ≡ syncₐₒ a (ν n - p) (ν n - q) >>= ⟅?⟆ ∘ ν′ n
sync-νˡ : ∀ a p (n : A) q → n ∉ₐ a → syncₐₒ a (ν n - p) q >>= ⟅?⟆ ∘ ν′ n ≡ syncₐₒ a (ν n - p) (ν n - q) >>= ⟅?⟆ ∘ ν′ n
sync-ν  : ∀ a p (n : A) q → syncₐₒ a (ν n - p) (ν n - q) ≡ syncₐₒ a (ν n - p) (ν n - q) >>= ⟅?⟆ ∘ ν′ n


ν-ν-ν-∥ n p q =

  ν n - p ∥ ν n - q

    ≡⟨ ⌊-∥ (ν n - p) (ν n - q) ⟩

  ν n - p ⌊ ν n - q ⊕ ν n - q ⌊ ν n - p

    ≡⟨ cong₂ _⊕_ (ν-ν-ν-⌊ n p q) (ν-ν-ν-⌊ n q p) ⟩

  ν n - (ν n - p ⌊ ν n - q) ⊕ ν n - (ν n - q ⌊ ν n - p)

    ≡˘⟨ ν-⊕ n (ν n - p ⌊ ν n - q) (ν n - q ⌊ ν n - p) ⟩

  ν n - (ν n - p ⌊ ν n - q ⊕ ν n - q ⌊ ν n - p)

    ≡˘⟨ cong (ν n -_) (⌊-∥ (ν n - p) (ν n - q)) ⟩

  ν n - (ν n - p ∥ ν n - q)

    ∎

ν-∥-ν n p q =

  ν n - (p ∥ ν n - q)

    ≡⟨ cong (ν n -_) (⌊-∥ p (ν n - q)) ⟩

  ν n - (p ⌊ ν n - q ⊕ ν n - q ⌊ p)

    ≡⟨ ν-⊕ n (p ⌊ ν n - q) (ν n - q ⌊ p) ⟩

  ν n - (p ⌊ ν n - q) ⊕ ν n - (ν n - q ⌊ p)

    ≡⟨ cong₂ _⊕_ (ν-⌊-ν n p q) (ν-ν-⌊ n q p) ⟩

  ν n - (ν n - p ⌊ ν n - q) ⊕ ν n - (ν n - q ⌊ ν n - p)

    ≡˘⟨ ν-⊕ n (ν n - p ⌊ ν n - q) (ν n - q ⌊ ν n - p) ⟩

  ν n - (ν n - p ⌊ ν n - q ⊕ ν n - q ⌊ ν n - p)

    ≡˘⟨ cong (ν n -_) (⌊-∥ _ _) ⟩

  ν n - (ν n - p ∥ ν n - q)

    ∎

ν-ν-ν-⌊ n p q =

  ν n - p ⌊ ν n - q

    ≡⟨ cong-proc refl ⟩

  ⟪ (↯ p >>= ⟅?⟆ ∘ ν′ n) >>= (_⌊ₖ (ν n - q)) ⟫

    ≡⟨ cong-proc (>>=-assoc (↯ p) _ _) ⟩

  ⟪ ↯ p >>= (λ p′ → ⟅?⟆ (ν′ n p′) >>= (_⌊ₖ (ν n - q))) ⟫

    ≡⟨ cong-proc (cong (↯ p >>=_) (funExt lemma₁)) ⟩

  ⟪ ↯ p >>= (λ p″ → ⟅?⟆ (ν′ n p″) >>= (λ p′ → (p′ ⌊ₖ (ν n - q)) >>= (⟅?⟆ ∘ ν′ n))) ⟫

    ≡˘⟨ cong-proc (>>=-assoc (↯ p >>= ⟅?⟆ ∘ ν′ n) _ _ ⨾ >>=-assoc (↯ p) _ _) ⟩

  ⟪ ((↯ p >>= ⟅?⟆ ∘ ν′ n) >>= (_⌊ₖ (ν n - q))) >>= (⟅?⟆ ∘ ν′ n) ⟫

    ≡⟨ cong-proc refl ⟩

  ν n - (ν n - p ⌊ ν n - q)

    ∎

  where
  lemma₁ : ∀ p →
    (⟅?⟆ (ν′ n p) >>= (_⌊ₖ (ν n - q))) ≡
         ⟅?⟆ (ν′ n p) >>= (λ p′ → (p′ ⌊ₖ (ν n - q)) >>= (⟅?⟆ ∘ ν′ n))
  lemma₁ (a , p) with n ∈ₐ? a
  ... | yes _ = refl
  ... | no n∉a =

    (a , ν n - p) ⌊ₖ (ν n - q)

      ≡⟨⟩

    syncₐₒ a (ν n - p) (ν n - q) ∪ ⟅ a , ν n - p ∥ ν n - q ⟆

      ≡⟨ cong₂ _∪_ (sync-ν a p n q ) (cong (⟅_⟆ ∘ (_,_ a)) (ν-ν-ν-∥ n p q)) ⟩

    (syncₐₒ a (ν n - p) (ν n - q) >>= ⟅?⟆ ∘ ν′ n) ∪ ⟅ a , ν n - (ν n - p ∥ ν n - q) ⟆

      ≡˘⟨ cong ((syncₐₒ a (ν n - p) (ν n - q) >>= ⟅?⟆ ∘ ν′ n) ∪_) (cong (⟅?⟆ ∘ bool _ _) (it-doesn't (n ∈ₐ? a) n∉a))  ⟩

    (syncₐₒ a (ν n - p) (ν n - q) >>= ⟅?⟆ ∘ ν′ n) ∪ ⟅?⟆ (ν′ n (a , ν n - p ∥ ν n - q) )

      ≡⟨⟩

    (syncₐₒ a (ν n - p) (ν n - q) ∪ ⟅ a , ν n - p ∥ ν n - q ⟆) >>= ⟅?⟆ ∘ ν′ n

      ≡⟨⟩

    ((a , ν n - p) ⌊ₖ (ν n - q)) >>= (⟅?⟆ ∘ ν′ n)

      ∎

ν-ν-∥ n p q = cong (ν n -_) (∥-comm  (ν n - p) q) ⨾ ν-∥-ν n q p ⨾ cong (ν n -_) (∥-comm (ν n - q) (ν n - p))

sync-ν τ p n q = refl
sync-ν (out a) p n q = refl
sync-ν (inp a) p n q = 𝒦⟦ alg a p n ⟧ (↯ q)
  where
  alg : ∀ a p (n : A) → Ψ[ q ⦂ 𝒦 (Act A × Proc A) ] ↦ (syncₒ a (ν n - p) (ν n - ⟪ q ⟫) ≡ syncₒ a (ν n - p) (ν n - ⟪ q ⟫) >>= ⟅?⟆ ∘ ν′ n)
  alg a p n .snd = prop-coh λ q → trunc _ _
  alg a p n .fst ∅ = refl
  alg a p n .fst (xs ⟨ P⟨xs⟩ ⟩∪ ys ⟨ P⟨ys⟩ ⟩) = cong₂ _∪_ P⟨xs⟩ P⟨ys⟩
  alg a p n .fst ⟅ τ , q ⟆ = refl
  alg a p n .fst ⟅ emit s b , q ⟆ with n ≟ b
  alg a p n .fst ⟅ emit s b , q ⟆ | yes _ = refl
  alg a p n .fst ⟅ inp b , q ⟆ | no _ = refl
  alg a p n .fst ⟅ out b , q ⟆ | no _ with a ≟ b
  alg a p n .fst ⟅ out b , q ⟆ | no _ | no _ = refl
  alg a p n .fst ⟅ out b , q ⟆ | no _ | yes _ = cong (⟅_⟆ ∘ (τ ,_)) (ν-ν-ν-∥ n p q)

sync-νʳ τ p n q = refl
sync-νʳ (out a) p n q = refl
sync-νʳ (inp a) p n q = 𝒦⟦ alg a p n ⟧ (↯ q)
  where
  alg : ∀ a p (n : A) → Ψ[ q ⦂ 𝒦 (Act A × Proc A) ] ↦ (syncₒ a p (ν n - ⟪ q ⟫) >>= ⟅?⟆ ∘ ν′ n ≡ syncₒ a (ν n - p) (ν n - ⟪ q ⟫) >>= ⟅?⟆ ∘ ν′ n)
  alg a p n .snd = prop-coh λ q → trunc _ _
  alg a p n .fst ∅ = refl
  alg a p n .fst (xs ⟨ P⟨xs⟩ ⟩∪ ys ⟨ P⟨ys⟩ ⟩) = cong₂ _∪_ P⟨xs⟩ P⟨ys⟩
  alg a p n .fst ⟅ τ , q ⟆ = refl
  alg a p n .fst ⟅ emit s b , q ⟆ with n ≟ b
  alg a p n .fst ⟅ emit s b , q ⟆ | yes _ = refl
  alg a p n .fst ⟅ inp b , q ⟆ | no _ = refl
  alg a p n .fst ⟅ out b , q ⟆ | no _ with a ≟ b
  alg a p n .fst ⟅ out b , q ⟆ | no _ | no _ = refl
  alg a p n .fst ⟅ out b , q ⟆ | no _ | yes _ = cong (⟅_⟆ ∘ (_,_ τ)) (ν-∥-ν n p q)

sync-νˡ (out _) p n q n∉a = refl
sync-νˡ τ p n q n∉a = refl
sync-νˡ (inp a) p n q n∉a = 𝒦⟦ alg a p n n∉a ⟧ (↯ q)
  where
  alg : ∀ a p (n : A) → n ≢ a → Ψ[ q ⦂ 𝒦 (Act A × Proc A) ] ↦ (syncₒ a (ν n - p) ⟪ q ⟫ >>= ⟅?⟆ ∘ ν′ n ≡ syncₒ a (ν n - p) (ν n - ⟪ q ⟫) >>= ⟅?⟆ ∘ ν′ n)
  alg a p n a∉n .snd = prop-coh λ q → trunc _ _
  alg a p n a∉n .fst ∅ = refl
  alg a p n a∉n .fst (xs ⟨ P⟨xs⟩ ⟩∪ ys ⟨ P⟨ys⟩ ⟩) = cong₂ _∪_ P⟨xs⟩ P⟨ys⟩
  alg a p n a∉n .fst ⟅ τ , q ⟆ = refl
  alg a p n a∉n .fst ⟅ emit s b , q ⟆ with n ≟ b
  alg a p n a∉n .fst ⟅ inp b , q ⟆ | yes _ = refl
  alg a p n a∉n .fst ⟅ out b , q ⟆ | yes _ with a ≟ b
  alg a p n a∉n .fst ⟅ out b , q ⟆ | yes n≡b | yes a≡b = absurd (a∉n (n≡b ⨾ sym a≡b))
  alg a p n a∉n .fst ⟅ out b , q ⟆ | yes _ | no a≢b = refl
  alg a p n a∉n .fst ⟅ inp b , q ⟆ | no _ = refl
  alg a p n a∉n .fst ⟅ out b , q ⟆ | no _ with a ≟ b
  alg a p n a∉n .fst ⟅ out b , q ⟆ | no _ | no _ = refl
  alg a p n a∉n .fst ⟅ out b , q ⟆ | no _ | yes _ = cong (⟅_⟆ ∘ (_,_ τ)) (ν-ν-∥ n p q)

ν-ν-⌊ n p q =

  ν n - (ν n - p ⌊ q)

    ≡⟨ cong-proc refl ⟩

  ⟪ ((↯ p >>= ⟅?⟆ ∘ ν′ n) >>= (_⌊ₖ q)) >>= ⟅?⟆ ∘ ν′ n ⟫

    ≡⟨ cong-proc (>>=-assoc (↯ p >>= ⟅?⟆ ∘ ν′ n) _ _ ⨾ >>=-assoc (↯ p) _ _ ) ⟩

  ⟪ ↯ p >>= (λ p″ → ⟅?⟆ (ν′ n p″) >>= (λ p′ → (p′ ⌊ₖ q) >>= ⟅?⟆ ∘ ν′ n)) ⟫

    ≡⟨ cong-proc (cong (↯ p >>=_) (funExt lemma₁)) ⟩

  ⟪ ↯ p >>= (λ p″ → ⟅?⟆ (ν′ n p″) >>= (λ p′ → (p′ ⌊ₖ (ν n - q)) >>= ⟅?⟆ ∘ ν′ n)) ⟫

    ≡˘⟨ cong-proc (>>=-assoc (↯ p >>= ⟅?⟆ ∘ ν′ n) _ _ ⨾ >>=-assoc (↯ p) _ _) ⟩

  ⟪ ((↯ p >>= ⟅?⟆ ∘ ν′ n) >>= (_⌊ₖ (ν n - q))) >>= ⟅?⟆ ∘ ν′ n ⟫

    ≡⟨ cong-proc refl ⟩

  ν n - (ν n - p ⌊ ν n - q)

    ∎
  where

  lemma₁ : ∀ p →
         ⟅?⟆ (ν′ n p) >>= (λ p′ → (p′ ⌊ₖ q) >>=  ⟅?⟆ ∘ ν′ n)
      ≡
         ⟅?⟆ (ν′ n p) >>= (λ p′ → (p′ ⌊ₖ (ν n - q)) >>= ⟅?⟆ ∘ ν′ n)
  lemma₁ (a , p) with n ∈ₐ? a
  ... | yes n∈a = refl
  ... | no n∉a =

      (syncₐₒ a (ν n - p) q ∪ ⟅ a , (ν n - p) ∥ q ⟆) >>= ⟅?⟆ ∘ ν′ n

        ≡⟨⟩

      (syncₐₒ a (ν n - p) q >>= ⟅?⟆ ∘ ν′ n) ∪ (⟅ a , (ν n - p) ∥ q ⟆ >>= ⟅?⟆ ∘ ν′ n)

        ≡⟨ cong₂ _∪_ (sync-νˡ a p n q n∉a) (cong (⟅?⟆ ∘ bool _ _) (it-doesn't (n ∈ₐ? a) n∉a)  ⨾ cong (⟅_⟆ ∘ (a ,_)) (ν-ν-∥ n p q) ⨾ sym (cong (⟅?⟆ ∘ bool _ _) (it-doesn't (n ∈ₐ? a) n∉a))) ⟩

      (syncₐₒ a (ν n - p) (ν n - q) >>= ⟅?⟆ ∘ ν′ n) ∪ (⟅ a , (ν n - p) ∥ (ν n - q) ⟆ >>= ⟅?⟆ ∘ ν′ n)

        ≡⟨⟩

      (syncₐₒ a (ν n - p) (ν n - q) ∪ ⟅ a , (ν n - p) ∥ (ν n - q) ⟆) >>= ⟅?⟆ ∘ ν′ n

        ∎

ν-⌊-ν n p q = 

  ν n - (p ⌊ ν n - q)

    ≡⟨ cong-proc refl ⟩

  ⟪ (↯ p >>= (_⌊ₖ (ν n - q))) >>= ⟅?⟆ ∘ ν′ n ⟫

    ≡⟨ cong-proc (>>=-assoc (↯ p) _ _) ⟩

  ⟪ ↯ p >>= (λ p′ → (p′ ⌊ₖ (ν n - q)) >>= ⟅?⟆ ∘ ν′ n) ⟫

    ≡⟨ cong-proc (cong (↯ p >>=_) (funExt lemma₁)) ⟩

  ⟪ ↯ p >>= (λ p″ → ⟅?⟆ (ν′ n p″) >>= (λ p′ → (p′ ⌊ₖ (ν n - q)) >>= ⟅?⟆ ∘ ν′ n)) ⟫

    ≡˘⟨ cong-proc (>>=-assoc (↯ p >>= ⟅?⟆ ∘ ν′ n) _ _ ⨾ >>=-assoc (↯ p) _ _)  ⟩

  ⟪ ((↯ p >>= ⟅?⟆ ∘ ν′ n) >>= (_⌊ₖ (ν n - q))) >>= ⟅?⟆ ∘ ν′ n ⟫

    ≡⟨ cong-proc refl ⟩

  ν n - (ν n - p ⌊ ν n - q)

    ∎
  where


  lemma₁ : ∀ p → ((p ⌊ₖ (ν n - q)) >>= (⟅?⟆ ∘ ν′ n)) ≡ ⟅?⟆ (ν′ n p) >>= (λ p′ → (p′ ⌊ₖ (ν n - q)) >>= (λ x → ⟅?⟆ (ν′ n x)))
  lemma₁ (a , p) with n ∈ₐ? a
  ... | no n≢a =

    (syncₐₒ a p (ν n - q) >>= ⟅?⟆ ∘ ν′ n) ∪ ⟅ a , ν n - (p ∥ ν n - q) ⟆

      ≡⟨ cong₂ _∪_ (sync-νʳ a p n q) (cong (⟅_⟆ ∘ (_,_ a)) (ν-∥-ν n p q)) ⟩

    (syncₐₒ a (ν n - p) (ν n - q) >>= ⟅?⟆ ∘ ν′ n) ∪ ⟅ a , ν n - ((ν n - p) ∥ (ν n - q)) ⟆

      ≡˘⟨ cong ((syncₐₒ a (ν n - p) (ν n - q) >>= ⟅?⟆ ∘ ν′ n) ∪_) (cong (⟅?⟆ ∘ bool _ _) (it-doesn't (n ∈ₐ? a) n≢a)) ⟩

    (syncₐₒ a (ν n - p) (ν n - q) >>= ⟅?⟆ ∘ ν′ n) ∪ (⟅ a , (ν n - p) ∥ (ν n - q) ⟆ >>= ⟅?⟆ ∘ ν′ n)

      ≡⟨⟩

    (syncₐₒ a (ν n - p) (ν n - q) ∪ ⟅ a , (ν n - p) ∥ (ν n - q) ⟆) >>= ⟅?⟆ ∘ ν′ n

      ≡⟨⟩

    ((a , ν n - p) ⌊ₖ (ν n - q)) >>= ⟅?⟆ ∘ ν′ n

      ∎

  lemma₁ (τ , p) | yes _ = ident _
  lemma₁ (out _ , p) | yes _ = ident _
  lemma₁ (inp a , p) | yes n≡a  =

   (syncₒ a p (ν n - q) >>= (⟅?⟆ ∘ ν′ n)) ∪ ∅

      ≡⟨ comm _ ∅ ⨾ ident _ ⟩

   (syncₒ a p (ν n - q) >>= (⟅?⟆ ∘ ν′ n))

      ≡⟨ cong (λ e → (syncₒ a p (ν e - q) >>= (⟅?⟆ ∘ ν′ n))) n≡a ⟩

   (syncₒ a p (ν a - q) >>= (⟅?⟆ ∘ ν′ n))

      ≡⟨ cong (_>>= ⟅?⟆ ∘ ν′ n) (syncₒ-ν a p q) ⟩

    ∅ ∎



ν-syncᵢₒ-ν   : ∀ (n : A) (p q : Proc A) → ν n - syncᵢₒ p (ν n - q) ≡ ν n - syncᵢₒ (ν n - p) (ν n - q)
ν-ν-syncᵢₒ   : ∀ (n : A) (p q : Proc A) → ν n - syncᵢₒ (ν n - p) q ≡ ν n - syncᵢₒ (ν n - p) (ν n - q)
ν-ν-ν-syncᵢₒ : ∀ (n : A) (p q : Proc A) → syncᵢₒ (ν n - p) (ν n - q) ≡ ν n - syncᵢₒ (ν n - p) (ν n - q)

ν-syncᵢₒ-ν n p q =
    cong-proc ( >>=-assoc (↯ p) _ _
              ⨾ cong (↯ p >>=_) (funExt lemma)
              ⨾ sym (>>=-assoc (↯ p >>= ⟅?⟆ ∘ ν′ n) _ _
              ⨾ >>=-assoc (↯ p) _ _))
  where
  lemma : ∀ ap → uncurry syncₐₒ ap (ν n - q) >>= ⟅?⟆ ∘ ν′ n
           ≡ ⟅?⟆ (ν′ n ap) >>= (λ ap′ → uncurry syncₐₒ ap′ (ν n - q) >>= ⟅?⟆ ∘ ν′ n)
  lemma (τ , p) = refl
  lemma (emit s a , p) with n ≟ a
  lemma (emit s a , p) | no n≢a = sync-νʳ (emit s a) p n q
  lemma (out a , p) | yes n≡a = sync-νʳ (out a) p n q
  lemma (inp a , p) | yes n≡a = 
      cong (_>>= ⟅?⟆ ∘ ν′ n)
           (cong (λ e → syncₒ a p (ν e - q)) n≡a ⨾ syncₒ-ν a p q)

ν-ν-syncᵢₒ n p q =
  cong-proc ( >>=-assoc (↯ p >>= ⟅?⟆ ∘ ν′ n) _ _
            ⨾ >>=-assoc (↯ p) _ _
            ⨾ cong (↯ p >>=_) (funExt lemma)
            ⨾ sym (>>=-assoc (↯ p >>= ⟅?⟆ ∘ ν′ n) _ _
            ⨾ >>=-assoc (↯ p) _ _))
  where
  lemma : ∀ ap → ⟅?⟆ (ν′ n ap) >>= (λ ap′ → uncurry syncₐₒ ap′ q >>= ⟅?⟆ ∘ ν′ n)
            ≡ ⟅?⟆ (ν′ n ap) >>= (λ ap′ → uncurry syncₐₒ ap′ (ν n - q) >>= ⟅?⟆ ∘ ν′ n)
  lemma (a , p) with n ∈ₐ? a
  ... | yes _ = refl
  ... | no n∉a = sync-νˡ a p n q n∉a

ν-ν-ν-syncᵢₒ n p q =
  cong-proc
    ( (>>=-assoc (↯ p) _ _)
    ⨾ cong (↯ p >>=_) (funExt lemma)
    ⨾ sym (>>=-assoc (↯ p >>= ⟅?⟆ ∘ ν′ n) _ _ ⨾ >>=-assoc (↯ p) _ _))
  where
  lemma : ∀ ap → (⟅?⟆ (ν′ n ap) >>= flip (uncurry syncₐₒ) (ν n - q))
            ≡ ⟅?⟆ (ν′ n ap) >>= (λ ap′ → uncurry syncₐₒ ap′ (ν n - q) >>= ⟅?⟆ ∘ ν′ n)
  lemma (a , p) with n ∈ₐ? a
  ... | yes _ = refl
  ... | no _ = sync-ν a p n q