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

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

module CCS.Hyp.Properties.Restrict {r} {Name R : Type r} (mod : Semilattice R) ⦃ discName : IsDiscrete Name ⦄ where

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

open import CCS.Hyp.Definition Name R
open import CCS.Hyp.SemiModel {R = R} mod {Name = Name}

open import CCS.Hyp.Properties.RestrictPar {Name = Name} mod

open Semilattice mod

private instance
  _ : CCSAlg Communicator
  _ = hypAlg

private instance
  _ : CCSSemiModel Communicator
  _ = hypMod


open import Data.List.Properties
open import Data.Fin

ι-ν-comm : ∀ (n : Name) p (q : Communicator) m → n ∉ₚ p → ι ⟦ ν n - p ⟧ q m ≡ ι ⟦ p ⟧ (ν n - q) m
ι-ν-comm n p q m n∉p with n ∈ₘ? m
... | no _ = refl
ι-ν-comm n p q (𝕚 (out m)) n∉p | yes n≡m = sym (ι-𝕚-out→𝟘 p (ν n - q) m)
ι-ν-comm n p q (𝕚 (inp m)) n∉p | yes n≡m = sym (ι-∉-inp→𝟘 p (ν n - q) m (n∉p ∘ subst (_∈ₚ p) (sym n≡m)))

ν-∉ : ∀ (n : Name) (p : P Name) → n ∉ₚ p → ν n - ⟦ p ⟧ᶜ ≡ ⟦ p ⟧ᶜ
ν-∉ n p n∉p = cong-ι (λ q → funExt λ m → ι-ν-comm n p q m n∉p ⨾ ι-ν-∉ n p q m n∉p)
  where
  
  ι-ν-∉ : ∀ (n : Name) (p : P Name) q (m : Maybe (Act Name)) → n ∉ₚ p →

    ι ⟦ p ⟧ (ν n - q) m ≡ ι ⟦ p ⟧ q m

  ι-ν-∉ n `𝟘       q m n∉p = refl
  ι-ν-∉ n (p `⊕ q) r m n∉p = cong₂ _∙_ (ι-ν-∉ n p r m (n∉p ∘ inl)) (ι-ν-∉ n q r m (n∉p ∘ inr))

  ι-ν-∉ n (p `∥ q) r m n∉p =
    ι ⟦ p ∥ q ⟧ (ν n - r) m                           ≡⟨ cong (λ e → ι e (ν n - r) m) (⌊-∥ ⟦ p ⟧ ⟦ q ⟧) ⟩
    ι ⟦ p ⌊ q ⊕ q ⌊ p ⟧ (ν n - r) m                   ≡⟨⟩
    ι ⟦ p ⌊ q ⟧ (ν n - r) m ∙ ι ⟦ q ⌊ p ⟧ (ν n - r) m ≡⟨ cong₂ _∙_ (ι-ν-∉ n (p ⌊ q) r m n∉p) (ι-ν-∉ n (q ⌊ p) r m (n∉p ∘ (inr ▿ inl))) ⟩
    ι ⟦ p ⌊ q ⟧ r m ∙ ι ⟦ q ⌊ p ⟧ r m                 ≡˘⟨ cong (λ e → ι e r m) (⌊-∥ ⟦ p ⟧ ⟦ q ⟧) ⟩
    ι ⟦ p ∥ q ⟧ r m ∎

  ι-ν-∉ n (`! p) q m n∉p =
    ι ⟦ ! p ⟧ (ν n - q) m                 ≡⟨ cong (λ e → ι e (ν n - q) m) (!-⌊ ⟦ p ⟧) ⟩
    ι ⟦ p ⌊ ! p ⟧ (ν n - q) m             ≡⟨⟩
    ι ⟦ p ⟧ (⟦ ! p ⟧ ∥ ν n - q) m         ≡˘⟨ ι-ν-∉ n p _ m n∉p ⟩
    ι ⟦ p ⟧ (ν n - (⟦ ! p ⟧ ∥ ν n - q)) m ≡⟨ cong (flip (ι ⟦ p ⟧) m) (ν-∥-ν n ⟦ ! p ⟧ q ⨾ sym (ν-ν-∥ n ⟦ ! p ⟧ q)) ⟩
    ι ⟦ p ⟧ (ν n - (ν n - ⟦ ! p ⟧ ∥ q)) m ≡⟨ cong (λ e → ι ⟦ p ⟧ (ν n - (e ∥ q)) m) (ν-∉ n (! p) n∉p) ⟩
    ι ⟦ p ⟧ (ν n - (⟦ ! p ⟧ ∥ q)) m       ≡⟨ ι-ν-∉ n p _ m n∉p ⟩
    ι ⟦ p ⌊ ! p ⟧ q m                     ≡˘⟨ cong (λ e → ι e q m) (!-⌊ ⟦ p ⟧) ⟩
    ι ⟦ ! p ⟧ q m ∎
  
  ι-ν-∉ n (p `⌊ q) r m n∉p =
    ι ⟦ p ⌊ q ⟧ (ν n - r) m                   ≡⟨⟩
    ι ⟦ p ⟧ (⟦ q ⟧ ∥ ν n - r) m               ≡˘⟨ cong (λ e → ι ⟦ p ⟧ (e ∥ ν n - r) m) (ν-∉ n q (n∉p ∘ inr)) ⟩
    ι ⟦ p ⟧ (ν n - ⟦ q ⟧ ∥ ν n - r) m         ≡⟨ cong (flip (ι ⟦ p ⟧) m) (ν-ν-ν-∥ n ⟦ q ⟧ r) ⟩
    ι ⟦ p ⟧ (ν n - (ν n - ⟦ q ⟧ ∥ ν n - r)) m ≡˘⟨ cong (flip (ι ⟦ p ⟧) m) (ν-ν-∥ n ⟦ q ⟧ r) ⟩
    ι ⟦ p ⟧ (ν n - (ν n - ⟦ q ⟧ ∥ r)) m       ≡⟨ cong (λ e → ι ⟦ p ⟧ (ν n - (e ∥ r)) m) (ν-∉ n q (n∉p ∘ inr)) ⟩
    ι ⟦ p ⟧ (ν n - (⟦ q ⟧ ∥ r)) m             ≡⟨ ι-ν-∉ n p (⟦ q ⟧ ∥ r) m (n∉p ∘ inl) ⟩
    ι ⟦ p ⟧ (⟦ q ⟧ ∥ r) m                     ≡⟨⟩
    ι ⟦ p ⌊ q ⟧ r m ∎
  
  ι-ν-∉ n (`ν o - p) q m n∉p = cong (λ e → bool′ e ε _) $
    ι ⟦ p ⟧ (ν o - ν n - q) m ≡⟨ cong (flip (ι ⟦ p ⟧) m) (ν-comm o n q) ⟩
    ι ⟦ p ⟧ (ν n - ν o - q) m ≡⟨ ι-ν-∉ n p (ν o - q) m (n∉p ∘ inr) ⟩
    ι ⟦ p ⟧ (ν o - q) m ∎

  ι-ν-∉ n (a `· p) q 𝕥 n∉p =
    ι ⟦ a · p ⟧ (ν n - q) 𝕥 ≡⟨⟩
    ι (ν n - q) ⟦ p ⟧ (𝕚 a)    ≡⟨ cong (bool _ _) (it-doesn't (n ∈ₐ? a) (n∉p ∘ inl)) ⟩
    ι q (ν n - ⟦ p ⟧) (𝕚 a)    ≡⟨ cong (flip (ι q) (𝕚 a)) (ν-∉ n p (n∉p ∘ inr)) ⟩
    ι ⟦ a · p ⟧ q 𝕥 ∎
  ι-ν-∉ n (inp _ `· p) q (𝕚 _)       n∉p = refl
  ι-ν-∉ n (τ     `· p) q (𝕚 _)       n∉p = refl
  ι-ν-∉ n (out b `· p) q (𝕚 (out x)) n∉p = refl
  ι-ν-∉ n (out b `· p) q (𝕚 τ)       n∉p = refl
  ι-ν-∉ n (out b `· p) q (𝕚 (inp a)) n∉p with a ≟ b
  ... | no a≢b = refl
  ... | yes a≡b =
    ι (ν n - q) ⟦ p ⟧ (𝕚 τ) ≡⟨⟩
    ι q (ν n - ⟦ p ⟧) (𝕚 τ) ≡⟨ cong (flip (ι q) (𝕚 τ)) (ν-∉ n p (n∉p ∘ inr)) ⟩
    ι q ⟦ p ⟧ (𝕚 τ) ∎