{-# 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.RestrictPar {r} {Name R : Type r} (lat : Semilattice R) ⦃ disc : IsDiscrete Name ⦄ where

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

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

private instance
  _ : CCSAlg Communicator
  _ = hypAlg

private instance
  _ : CCSSemiModel Communicator
  _ = hypMod

ν-⌊-ν : ∀ (n : Name) (p q : Communicator) → ν n - (p ⌊ ν n - q) ≡ ν n - (ν n - p ⌊ ν n - q)
ν-ν-⌊ : ∀ (n : Name) (p q : Communicator) → ν n - (ν n - p ⌊ q) ≡ ν n - (ν n - p ⌊ ν n - q)
ν-∥-ν : ∀ (n : Name) (p q : Communicator) → ν n - (p ∥ ν n - q) ≡ ν n - (ν n - p ∥ ν n - q)
ν-ν-∥ : ∀ (n : Name) (p q : Communicator) → ν n - (ν n - p ∥ q) ≡ ν n - (ν n - p ∥ ν n - q)
ν-ν-ν-∥ : ∀ (n : Name) (p q : Communicator) → ν n - p ∥ ν n - q ≡ ν n - (ν n - p ∥ ν n - q)
ν-ν-ν-⌊ : ∀ (n : Name) (p q : Communicator) → ν n - p ⌊ ν n - q ≡ ν n - (ν n - p ⌊ ν n - q)

ν-ν-ν-∥ n p 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 - (ν n - p ⌊ ν n - q ⊕ ν n - q ⌊ ν n - p) ≡˘⟨ cong (ν n -_) (⌊-∥ _ _) ⟩
  ν n - (ν n - p ∥ ν n - q) ∎

ν-ν-ν-⌊ n p q = cong-ι (funExt ∘′ lemma n p q)
  where
  lemma : ∀ n p q r m →
    ι (ν n - p ⌊ ν n - q) r m ≡ ι (ν n - (ν n - p ⌊ ν n - q)) r m
  lemma n p q r m with n ∈ₘ? m
  ... | yes n∈m = cong (bool′ _ _) (it-does (n ∈ₘ? m) n∈m) ⨾ sym (cong (bool′ _ _) (it-does (n ∈ₘ? m) n∈m))
  ... | no n∉m =
    ι (ν n - p ⌊ ν n - q) r m ≡⟨⟩
    ι (ν n - p) (ν n - q ∥ r) m ≡⟨ cong (bool′ _ _) (it-doesn't (n ∈ₘ? m) n∉m) ⟩
    ι p (ν n - (ν n - q ∥ r)) m ≡⟨ cong (flip (ι p) m) (ν-ν-∥ n q r) ⟩
    ι p (ν n - (ν n - q ∥ ν n - r)) m ≡˘⟨ cong (bool′ _ _) (it-doesn't (n ∈ₘ? m) n∉m) ⟩
    ι (ν n - p) (ν n - q ∥ ν n - r) m ≡˘⟨ cong (bool′ _ _) (it-doesn't (n ∈ₘ? m) n∉m) ⟩
    ι (ν n - (ν n - p ⌊ ν n - q)) r m ∎

ν-∥-ν n p q =
  ν n - (p ∥ ν n - q) ≡⟨ cong (ν n -_) (⌊-∥ _ _) ⟩
  ν n - (p ⌊ ν n - q ⊕ ν n - q ⌊ p) ≡⟨ ν-⊕ n _ _ ⟩
  ν 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 - (ν n - p ⌊ ν n - q ⊕ ν n - q ⌊ ν n - p) ≡˘⟨ cong (ν n -_) (⌊-∥ _ _) ⟩
  ν n - (ν n - p ∥ ν n - q) ∎

ν-ν-∥ n p q =
  ν n - (ν n - p ∥ q) ≡⟨ cong (ν n -_) (⌊-∥ _ _) ⟩
  ν n - (ν n - p ⌊ q ⊕ q ⌊ ν n - p) ≡⟨ ν-⊕ n _ _ ⟩
  ν n - (ν n - p ⌊ q) ⊕ ν n - (q ⌊ ν n - p) ≡⟨ cong₂ _⊕_ (ν-ν-⌊ n p q) (ν-⌊-ν n q p) ⟩
  ν n - (ν n - p ⌊ ν n - q) ⊕ ν n - (ν n - q ⌊ ν n - p) ≡˘⟨ ν-⊕ n _ _ ⟩
  ν n - (ν n - p ⌊ ν n - q ⊕ ν n - q ⌊ ν n - p) ≡˘⟨ cong (ν n -_) (⌊-∥ _ _) ⟩
  ν n - (ν n - p ∥ ν n - q) ∎

ν-⌊-ν n p q = cong-ι (funExt ∘′ lemma n p q)
  where
  lemma : ∀ n p q r m →
    ι (ν n - (p ⌊ ν n - q)) r m ≡ ι (ν n - (ν n - p ⌊ ν n - q)) r m
  lemma n p q r m with n ∈ₘ? m
  ... | yes n∈a = cong (bool′ _ _) (it-does (n ∈ₘ? m) n∈a) ⨾ sym (cong (bool′ _ _) (it-does (n ∈ₘ? m) n∈a))
  ... | no n∉m =
    ι (ν n - (p ⌊ ν n - q)) r m ≡⟨ cong (bool′ _ _) (it-doesn't (n ∈ₘ? m) n∉m) ⟩
    ι (p ⌊ ν n - q) (ν n - r) m ≡⟨⟩
    ι p (ν n - q ∥ ν n - r) m ≡⟨ cong (flip (ι p) m) (ν-ν-ν-∥ n q r) ⟩
    ι p (ν n - (ν n - q ∥ ν n - r)) m ≡˘⟨ cong (bool′ _ _) (it-doesn't (n ∈ₘ? m) n∉m) ⟩
    ι (ν n - p) (ν n - q ∥ ν n - r) m ≡⟨⟩
    ι (ν n - p ⌊ ν n - q) (ν n - r) m ≡˘⟨ cong (bool′ _ _) (it-doesn't (n ∈ₘ? m) n∉m) ⟩
    ι (ν n - (ν n - p ⌊ ν n - q)) r m ∎

ν-ν-⌊ n p q = cong-ι (funExt ∘′ lemma n p q)
  where
  lemma : ∀ n p q r m →
    ι (ν n - (ν n - p ⌊ q)) r m ≡ ι (ν n - (ν n - p ⌊ ν n - q)) r m
  lemma n p q r m with n ∈ₘ? m
  ... | yes n∈a = cong (bool′ _ _) (it-does (n ∈ₘ? m) n∈a) ⨾ sym (cong (bool′ _ _) (it-does (n ∈ₘ? m) n∈a))
  ... | no n∉m = 
    ι (ν n - (ν n - p ⌊ q)) r m ≡⟨ cong (bool′ _ _) (it-doesn't (n ∈ₘ? m) n∉m) ⟩
    ι (ν n - p ⌊ q) (ν n - r) m ≡⟨⟩
    ι (ν n - p) (q ∥ ν n - r) m ≡⟨ cong (bool′ _ _) (it-doesn't (n ∈ₘ? m) n∉m) ⟩
    ι p (ν n - (q ∥ ν n - r)) m ≡⟨ cong (flip (ι p) m) (ν-∥-ν n q r) ⟩
    ι p (ν n - (ν n - q ∥ ν n - r)) m ≡˘⟨ cong (bool′ _ _) (it-doesn't (n ∈ₘ? m) n∉m) ⟩
    ι (ν n - p) (ν n - q ∥ ν n - r) m ≡⟨⟩
    ι (ν n - p ⌊ ν n - q) (ν n - r) m ≡˘⟨ cong (bool′ _ _) (it-doesn't (n ∈ₘ? m) n∉m) ⟩
    ι (ν n - (ν n - p ⌊ ν n - q)) r m ∎