module CCS.Fresh where

open import Prelude hiding (P)
open import Data.Nat
open import Data.Nat.Order
open import CCS.Syntax
open import CCS.Act

opaque
  max-var : P ℕ → ℕ
  max-var = fold-P _⊔_ zero

  # : P ℕ → ℕ
  # = suc ∘ max-var

  ∈-≤max : ∀ n p → n ∈ₚ p → n ≤ max-var p
  ∈-≤max n (p ⊕ q) (inl n∈p) = ≤-⊔ˡ n (max-var p) (max-var q) (∈-≤max n p n∈p)
  ∈-≤max n (p ⊕ q) (inr n∈q) = ≤-⊔ʳ n (max-var p) (max-var q) (∈-≤max n q n∈q)
  ∈-≤max n (p ⌊ q) (inl n∈p) = ≤-⊔ˡ n (max-var p) (max-var q) (∈-≤max n p n∈p)
  ∈-≤max n (p ⌊ q) (inr n∈q) = ≤-⊔ʳ n (max-var p) (max-var q) (∈-≤max n q n∈q)
  ∈-≤max n (p ∥ q) (inl n∈p) = ≤-⊔ˡ n (max-var p) (max-var q) (∈-≤max n p n∈p)
  ∈-≤max n (p ∥ q) (inr n∈q) = ≤-⊔ʳ n (max-var p) (max-var q) (∈-≤max n q n∈q)
  ∈-≤max n (inp x · p) (inl n∈a) = ≤-⊔ˡ n x (max-var p) (subst (n ≤_) n∈a (≤-refl n))
  ∈-≤max n (out x · p) (inl n∈a) = ≤-⊔ˡ n x (max-var p) (subst (n ≤_) n∈a (≤-refl n))
  ∈-≤max n (inp x · p) (inr n∈p) = ≤-⊔ʳ n x (max-var p) (∈-≤max n p n∈p)
  ∈-≤max n (out x · p) (inr n∈p) = ≤-⊔ʳ n x (max-var p) (∈-≤max n p n∈p)
  ∈-≤max n (τ · p) (inr n∈p) = ∈-≤max n p n∈p
  ∈-≤max n (ν x - p) (inl n≡x) = ≤-⊔ˡ n x (max-var p) (subst (n ≤_) n≡x (≤-refl n))
  ∈-≤max n (ν x - p) (inr n∈p) = ≤-⊔ʳ n x (max-var p) (∈-≤max n p n∈p)
  ∈-≤max n (! p) n∈p = ∈-≤max n p n∈p

  #-∉ : ∀ p → # p ∉ₚ p
  #-∉ p fp∈p = <-irrefl (max-var p) (∈-≤max (# p) p fp∈p)