On 2021-01-08 02:26, John Paul Martin wrote:
> {-# TERMINATING #-}
> BST-alg : ℕ → ℕ → Tree → Set
> BST-alg n m t = (t ≡ leaf)
> ∨ ( ∃[ x ] ∃[ l ] ∃[ r ] (t ≡ (node l x r) × (x ≤ m) × (n ≤ x) × (BST-alg n x l) × (BST-alg x m r)))
> Does this family(BST-alg) actually terminate?
No. Try normalising BST-alg in Agda.
--
/NAD