    ------------------------------------------------------------------------
    -- The Agda standard library
    --
    -- Types and functions which are used to keep track of height
    -- invariants in AVL Trees
    ------------------------------------------------------------------------

    {-# OPTIONS --cubical-compatible --safe #-}

    module Data.Tree.AVL.Height where

    open import Data.Nat.Base
    open import Data.Fin.Base using (Fin; zero; suc)

    ℕ₂ = Fin 2
    pattern 0# = zero
    pattern 1# = suc zero
    pattern ## = suc (suc ())

    -- Addition.

    infixl 6 _⊕_

    _⊕_ : ℕ₂ → ℕ → ℕ
    0# ⊕ n = n
    1# ⊕ n = 1 + n

    -- pred[ i ⊕ n ] = pred (i ⊕ n).

    pred[_⊕_] : ℕ₂ → ℕ → ℕ
    pred[ i ⊕ zero  ] = 0
    pred[ i ⊕ suc n ] = i ⊕ n

    infix 4 _∼_⊔_

    -- If i ∼ j ⊔ m, then the difference between i and j is at most 1,
    -- and the maximum of i and j is m. _∼_⊔_ is used to record the
    -- balance factor of the AVL trees, and also to ensure that the
    -- absolute value of the balance factor is never more than 1.

    data _∼_⊔_ : ℕ → ℕ → ℕ → Set where
      ∼+ : ∀ {n} →     n ∼ 1 + n ⊔ 1 + n
      ∼0 : ∀ {n} →     n ∼ n     ⊔ n
      ∼- : ∀ {n} → 1 + n ∼ n     ⊔ 1 + n

    -- Some lemmas.

    max∼ : ∀ {i j m} → i ∼ j ⊔ m → m ∼ i ⊔ m
    max∼ ∼+ = ∼-
    max∼ ∼0 = ∼0
    max∼ ∼- = ∼0

    ∼max : ∀ {i j m} → i ∼ j ⊔ m → j ∼ m ⊔ m
    ∼max ∼+ = ∼0
    ∼max ∼0 = ∼0
    ∼max ∼- = ∼+