module CCS.Fresh.Proc where

open import Prelude hiding (A)
open import CCS.Fresh
open import CCS.Proc

open import CCS.Alg
open import CCS.SemiModel

private
  A : Type
  A = ℕ

open CCSAlg ⦃ ... ⦄
open CCSSemiModel ⦃ ... ⦄

instance
  _ : CCSAlg (Proc A)
  _ = procAlg

instance
  _ : CCSSemiModel (Proc A)
  _ = procMod


open import CCS.Proc.RestrictPar
open import Swaps {A = A}

ν-⌊-rewrite : ∀ (ns : List A) (n : A) p q
            → νₛ ns - (⟦ ν n - p ⌊ q ⟧ ⦂ Proc A) ≡
              νₛ (# (p ⌊ q) ∷ ns) - ⟦ `ρ (n /→ # (p ⌊ q)) p ⌊ q ⟧
ν-⌊-rewrite ns n p q =
  let m = # (p ⌊ q)
      m∉ = #-∉ (p ⌊ q)
  in

  νₛ ns - ⟦ ν n - p ⌊ q ⟧

    ≡⟨⟩

  νₛ ns - ((ν n - ⟦ p ⟧) ⌊ ⟦ q ⟧)

    ≡⟨ cong (λ e → νₛ ns - (e ⌊ ⟦ q ⟧)) (ν-ρ-∉ᵖ n m ⟦ p ⟧ (∉ᵖ⇒∉ₚ m p (m∉ ∘ inl))) ⟩

  νₛ ns - ((ν m - ρ (n /↔ m) ⟦ p ⟧) ⌊ ⟦ q ⟧)

    ≡˘⟨ cong (λ e → νₛ ns - ((ν m - ρ (n /↔ m) ⟦ p ⟧) ⌊ e)) (ν-∉ᵖ m ⟦ q ⟧ (∉ᵖ⇒∉ₚ m q (m∉ ∘ inr))) ⟩

  νₛ ns - ((ν m - ρ (n /↔ m) ⟦ p ⟧) ⌊ ν m - ⟦ q ⟧)

    ≡⟨ cong (νₛ ns -_) (ν-ν-ν-⌊ m (ρ (n /↔ m) ⟦ p ⟧) ⟦ q ⟧) ⟩

  νₛ ns - ν m - ((ν m - ρ (n /↔ m) ⟦ p ⟧) ⌊ ν m - ⟦ q ⟧)

    ≡˘⟨ cong (νₛ ns -_) (ν-⌊-ν m (ρ (n /↔ m) ⟦ p ⟧) ⟦ q ⟧) ⟩

  νₛ ns - ν m - ((ρ (n /↔ m) ⟦ p ⟧) ⌊ ν m - ⟦ q ⟧)

    ≡⟨ cong (λ e → νₛ ns - ν m - ((ρ (n /↔ m) ⟦ p ⟧) ⌊ e)) (ν-∉ᵖ m ⟦ q ⟧ (∉ᵖ⇒∉ₚ m q (m∉ ∘ inr))) ⟩

  νₛ ns - ν m - ((ρ (n /↔ m) ⟦ p ⟧) ⌊ ⟦ q ⟧)

    ≡⟨ cong (λ e → νₛ ns - ν m - (e ⌊ ⟦ q ⟧)) (ρ-hom ((n /↔ m) , iso-is-inj (n /⇔ m)) p) ⟩

  νₛ ns - ν m - (⟦ `ρ (n /↔ m) p ⟧ ⌊ ⟦ q ⟧)

    ≡˘⟨ cong (λ e → νₛ ns - ν m - (⟦ e ⟧ ⌊ ⟦ q ⟧)) (ρ-∉-↔ n m p (m∉ ∘ inl)) ⟩

  νₛ ns - ν m - (⟦ `ρ (n /→ m) p ⟧ ⌊ ⟦ q ⟧)

    ∎

ν-sync-rewrite : ∀ (n : A) (a : Act A) p q
            → syncᵢₒ ⟦ a · p ⟧ (ν n - ⟦ q ⟧) ≡
              ν (# ((a · p) ⌊ q)) - syncᵢₒ ⟦ a · p ⟧ ⟦ `ρ (n /→ # ((a · p) ⌊ q)) q ⟧
ν-sync-rewrite n a p q =
  let m  = # ((a · p) ⌊ q)
      m∉ = #-∉ ((a · p) ⌊ q)
  in

  syncᵢₒ ⟦ a · p ⟧ (ν n - ⟦ q ⟧)

    ≡⟨ cong₂ syncᵢₒ (sym (ν-∉ᵖ m ⟦ a · p ⟧ (∉ᵖ⇒∉ₚ m (a · p) (m∉ ∘ inl)))) (ν-ρ-∉ᵖ n m ⟦ q ⟧ (∉ᵖ⇒∉ₚ m q (m∉ ∘ inr))) ⟩

  syncᵢₒ (ν m - ⟦ a · p ⟧) (ν m - ρ (n /↔ m) ⟦ q ⟧)

    ≡⟨ ν-ν-ν-syncᵢₒ m ⟦ a · p ⟧ (ρ (n /↔ m) ⟦ q ⟧) ⟩

  ν m - syncᵢₒ (ν m - ⟦ a · p ⟧) (ν m - ρ (n /↔ m) ⟦ q ⟧)

    ≡˘⟨ ν-ν-syncᵢₒ m ⟦ a · p ⟧ (ρ (n /↔ m) ⟦ q ⟧) ⟩

  ν m - syncᵢₒ (ν m - ⟦ a · p ⟧) (ρ (n /↔ m) ⟦ q ⟧)

    ≡⟨ cong (ν m -_) (cong₂ syncᵢₒ (ν-∉ᵖ m ⟦ a · p ⟧ (∉ᵖ⇒∉ₚ m (a · p) (m∉ ∘ inl))) ((ρ-hom ((n /↔ m) , iso-is-inj (n /⇔ m)) q))) ⟩

  ν m - syncᵢₒ ⟦ a · p ⟧ ⟦ `ρ (n /↔ m) q ⟧

    ≡˘⟨ cong (λ e → ν m - syncᵢₒ ⟦ a · p ⟧ ⟦ e ⟧) (ρ-∉-↔ n m q (m∉ ∘ inr)) ⟩

  ν m - syncᵢₒ ⟦ a · p ⟧ ⟦ `ρ (n /→ m) q ⟧

    ∎