{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE Safe #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_HADDOCK ignore-exports #-}

-- |
-- Module      : Data.Tree.BST.Extern.DeleteProofs
-- Description : Proofs for deletion over externalist BST trees
-- Copyright   : (c) Nicolás Rodríguez, 2021
-- License     : GPL-3
-- Maintainer  : Nicolás Rodríguez
-- Stability   : experimental
-- Portability : POSIX
--
-- Implementation of the necessary proofs to ensure (at compile time) that the
-- deletion algorithm defined in "Data.Tree.BST.Extern.Delete" respects the key ordering.
module Data.Tree.BST.Extern.DeleteProofs
  ( ProofIsBSTDelete (proofIsBSTDelete),
  )
where

import Data.Proxy (Proxy (Proxy))
import Data.Tree.BST.Extern.Constructors (IsBSTT (EmptyIsBSTT, ForkIsBSTT))
import Data.Tree.BST.Extern.Delete
  ( Deletable (Delete),
    Deletable' (Delete'),
    MaxKeyDeletable (MaxKeyDelete),
    Maxable (MaxKey, MaxValue),
  )
import Data.Tree.BST.Invariants (GtN, LtN)
import Data.Tree.ITree (Tree (EmptyTree, ForkTree))
import Data.Tree.Node (Node)
import Data.Type.Equality (gcastWith, (:~:) (Refl))
import GHC.TypeNats (CmpNat, Nat)
import Prelude (Bool (True), Ordering (EQ, GT, LT), ($))

-- | Prove that deleting a node with key @x@ in a `Data.Tree.BST.Extern.Constructors.BST` tree preserves @BST@ restrictions.
class ProofIsBSTDelete (x :: Nat) (t :: Tree) where
  proofIsBSTDelete :: Proxy x -> IsBSTT t -> IsBSTT (Delete x t)

instance ProofIsBSTDelete x 'EmptyTree where
  proofIsBSTDelete :: Proxy x -> IsBSTT 'EmptyTree -> IsBSTT (Delete x 'EmptyTree)
proofIsBSTDelete Proxy x
_ IsBSTT 'EmptyTree
_ = IsBSTT 'EmptyTree
IsBSTT (Delete x 'EmptyTree)
EmptyIsBSTT

instance
  ( o ~ CmpNat x n,
    ProofIsBSTDelete' x ('ForkTree l (Node n a1) r) o
  ) =>
  ProofIsBSTDelete x ('ForkTree l (Node n a1) r)
  where
  proofIsBSTDelete :: Proxy x
-> IsBSTT ('ForkTree l (Node n a1) r)
-> IsBSTT (Delete x ('ForkTree l (Node n a1) r))
proofIsBSTDelete Proxy x
px IsBSTT ('ForkTree l (Node n a1) r)
tIsBST = Proxy x
-> IsBSTT ('ForkTree l (Node n a1) r)
-> Proxy o
-> IsBSTT (Delete' x ('ForkTree l (Node n a1) r) o)
forall (x :: Nat) (t :: Tree) (o :: Ordering).
ProofIsBSTDelete' x t o =>
Proxy x -> IsBSTT t -> Proxy o -> IsBSTT (Delete' x t o)
proofIsBSTDelete' Proxy x
px IsBSTT ('ForkTree l (Node n a1) r)
tIsBST (Proxy o
forall {k} (t :: k). Proxy t
Proxy :: Proxy o)

-- | Prove that deleting a node with key @x@
-- in a `Data.Tree.BST.Extern.Constructors.BST` tree preserves @BST@ restrictions, given that the comparison between
-- @x@ and the root key of the tree equals @o@.
-- The @BST@ restrictions were already checked when `proofIsBSTDelete` was called before.
-- The @o@ parameter guides the proof.
class ProofIsBSTDelete' (x :: Nat) (t :: Tree) (o :: Ordering) where
  proofIsBSTDelete' :: Proxy x -> IsBSTT t -> Proxy o -> IsBSTT (Delete' x t o)

instance ProofIsBSTDelete' x ('ForkTree 'EmptyTree (Node n a1) 'EmptyTree) 'EQ where
  proofIsBSTDelete' :: Proxy x
-> IsBSTT ('ForkTree 'EmptyTree (Node n a1) 'EmptyTree)
-> Proxy 'EQ
-> IsBSTT
     (Delete' x ('ForkTree 'EmptyTree (Node n a1) 'EmptyTree) 'EQ)
proofIsBSTDelete' Proxy x
_ IsBSTT ('ForkTree 'EmptyTree (Node n a1) 'EmptyTree)
_ Proxy 'EQ
_ = IsBSTT 'EmptyTree
IsBSTT
  (Delete' x ('ForkTree 'EmptyTree (Node n a1) 'EmptyTree) 'EQ)
EmptyIsBSTT

instance ProofIsBSTDelete' x ('ForkTree 'EmptyTree (Node n a1) ('ForkTree rl (Node rn ra) rr)) 'EQ where
  proofIsBSTDelete' :: Proxy x
-> IsBSTT
     ('ForkTree 'EmptyTree (Node n a1) ('ForkTree rl (Node rn ra) rr))
-> Proxy 'EQ
-> IsBSTT
     (Delete'
        x
        ('ForkTree 'EmptyTree (Node n a1) ('ForkTree rl (Node rn ra) rr))
        'EQ)
proofIsBSTDelete' Proxy x
_ (ForkIsBSTT IsBSTT l
_ Proxy (Node n a)
_ rIsBST :: IsBSTT r
rIsBST@ForkIsBSTT {}) Proxy 'EQ
_ = IsBSTT r
IsBSTT
  (Delete'
     x
     ('ForkTree 'EmptyTree (Node n a1) ('ForkTree rl (Node rn ra) rr))
     'EQ)
rIsBST

instance ProofIsBSTDelete' x ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a1) 'EmptyTree) 'EQ where
  proofIsBSTDelete' :: Proxy x
-> IsBSTT
     ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a1) 'EmptyTree)
-> Proxy 'EQ
-> IsBSTT
     (Delete'
        x
        ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a1) 'EmptyTree)
        'EQ)
proofIsBSTDelete' Proxy x
_ (ForkIsBSTT IsBSTT l
lIsBST Proxy (Node n a)
_ IsBSTT r
_) Proxy 'EQ
_ = IsBSTT l
IsBSTT
  (Delete'
     x
     ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a1) 'EmptyTree)
     'EQ)
lIsBST

instance
  ( l ~ 'ForkTree ll (Node ln la) lr,
    r ~ 'ForkTree rl (Node rn ra) rr,
    LtN (MaxKeyDelete l) (MaxKey l) ~ 'True,
    GtN r (MaxKey l) ~ 'True,
    ProofMaxKeyDeleteIsBST l,
    ProofLtNMaxKeyDelete l n
  ) =>
  ProofIsBSTDelete' x ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a1) ('ForkTree rl (Node rn ra) rr)) 'EQ
  where
  proofIsBSTDelete' :: Proxy x
-> IsBSTT
     ('ForkTree
        ('ForkTree ll (Node ln la) lr)
        (Node n a1)
        ('ForkTree rl (Node rn ra) rr))
-> Proxy 'EQ
-> IsBSTT
     (Delete'
        x
        ('ForkTree
           ('ForkTree ll (Node ln la) lr)
           (Node n a1)
           ('ForkTree rl (Node rn ra) rr))
        'EQ)
proofIsBSTDelete' Proxy x
_ (ForkIsBSTT IsBSTT l
l Proxy (Node n a)
_ IsBSTT r
r) Proxy 'EQ
_ =
    (LtN (MaxKeyDelete ('ForkTree ll (Node ln la) lr)) n :~: 'True)
-> ((LtN (MaxKeyDelete ('ForkTree ll (Node ln la) lr)) n
     ~ 'True) =>
    IsBSTT
      ('ForkTree
         (MaxKeyDelete ('ForkTree ll (Node ln la) lr))
         (Node
            (MaxKey ('ForkTree ll (Node ln la) lr))
            (MaxValue ('ForkTree ll (Node ln la) lr)))
         ('ForkTree rl (Node rn ra) rr)))
-> IsBSTT
     ('ForkTree
        (MaxKeyDelete ('ForkTree ll (Node ln la) lr))
        (Node
           (MaxKey ('ForkTree ll (Node ln la) lr))
           (MaxValue ('ForkTree ll (Node ln la) lr)))
        ('ForkTree rl (Node rn ra) rr))
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (IsBSTT l -> Proxy n -> LtN (MaxKeyDelete l) n :~: 'True
forall (t :: Tree) (n :: Nat).
(ProofLtNMaxKeyDelete t n, LtN t n ~ 'True) =>
IsBSTT t -> Proxy n -> LtN (MaxKeyDelete t) n :~: 'True
proofLtNMaxKeyDelete IsBSTT l
l (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)) (((LtN (MaxKeyDelete ('ForkTree ll (Node ln la) lr)) n ~ 'True) =>
  IsBSTT
    ('ForkTree
       (MaxKeyDelete ('ForkTree ll (Node ln la) lr))
       (Node
          (MaxKey ('ForkTree ll (Node ln la) lr))
          (MaxValue ('ForkTree ll (Node ln la) lr)))
       ('ForkTree rl (Node rn ra) rr)))
 -> IsBSTT
      ('ForkTree
         (MaxKeyDelete ('ForkTree ll (Node ln la) lr))
         (Node
            (MaxKey ('ForkTree ll (Node ln la) lr))
            (MaxValue ('ForkTree ll (Node ln la) lr)))
         ('ForkTree rl (Node rn ra) rr)))
-> ((LtN (MaxKeyDelete ('ForkTree ll (Node ln la) lr)) n
     ~ 'True) =>
    IsBSTT
      ('ForkTree
         (MaxKeyDelete ('ForkTree ll (Node ln la) lr))
         (Node
            (MaxKey ('ForkTree ll (Node ln la) lr))
            (MaxValue ('ForkTree ll (Node ln la) lr)))
         ('ForkTree rl (Node rn ra) rr)))
-> IsBSTT
     ('ForkTree
        (MaxKeyDelete ('ForkTree ll (Node ln la) lr))
        (Node
           (MaxKey ('ForkTree ll (Node ln la) lr))
           (MaxValue ('ForkTree ll (Node ln la) lr)))
        ('ForkTree rl (Node rn ra) rr))
forall a b. (a -> b) -> a -> b
$
      IsBSTT (MaxKeyDelete ('ForkTree ll (Node ln la) lr))
-> Proxy
     (Node
        (MaxKey ('ForkTree ll (Node ln la) lr))
        (MaxValue ('ForkTree ll (Node ln la) lr)))
-> IsBSTT r
-> IsBSTT
     ('ForkTree
        (MaxKeyDelete ('ForkTree ll (Node ln la) lr))
        (Node
           (MaxKey ('ForkTree ll (Node ln la) lr))
           (MaxValue ('ForkTree ll (Node ln la) lr)))
        r)
forall (l :: Tree) (n :: Nat) (r :: Tree) a.
(LtN l n ~ 'True, GtN r n ~ 'True) =>
IsBSTT l
-> Proxy (Node n a)
-> IsBSTT r
-> IsBSTT ('ForkTree l (Node n a) r)
ForkIsBSTT (IsBSTT l -> IsBSTT (MaxKeyDelete l)
forall (t :: Tree).
ProofMaxKeyDeleteIsBST t =>
IsBSTT t -> IsBSTT (MaxKeyDelete t)
proofMaxKeyDeleteIsBST IsBSTT l
l) Proxy (Node (MaxKey l) (MaxValue l))
Proxy
  (Node
     (MaxKey ('ForkTree ll (Node ln la) lr))
     (MaxValue ('ForkTree ll (Node ln la) lr)))
pNode IsBSTT r
r
    where
      pNode :: Proxy (Node (MaxKey l) (MaxValue l))
pNode = Proxy (Node (MaxKey l) (MaxValue l))
forall {k} (t :: k). Proxy t
Proxy :: Proxy (Node (MaxKey l) (MaxValue l))

instance ProofIsBSTDelete' x ('ForkTree 'EmptyTree (Node n a1) r) 'LT where
  proofIsBSTDelete' :: Proxy x
-> IsBSTT ('ForkTree 'EmptyTree (Node n a1) r)
-> Proxy 'LT
-> IsBSTT (Delete' x ('ForkTree 'EmptyTree (Node n a1) r) 'LT)
proofIsBSTDelete' Proxy x
_ IsBSTT ('ForkTree 'EmptyTree (Node n a1) r)
tIsBST Proxy 'LT
_ = IsBSTT ('ForkTree 'EmptyTree (Node n a1) r)
IsBSTT (Delete' x ('ForkTree 'EmptyTree (Node n a1) r) 'LT)
tIsBST

instance
  ( l ~ 'ForkTree ll (Node ln la) lr,
    o ~ CmpNat x ln,
    ProofIsBSTDelete' x l o,
    ProofLtNDelete' x l n o
  ) =>
  ProofIsBSTDelete' x ('ForkTree l (Node n a1) r) 'LT
  where
  proofIsBSTDelete' :: Proxy x
-> IsBSTT ('ForkTree l (Node n a1) r)
-> Proxy 'LT
-> IsBSTT (Delete' x ('ForkTree l (Node n a1) r) 'LT)
proofIsBSTDelete' Proxy x
px (ForkIsBSTT IsBSTT l
l Proxy (Node n a)
node IsBSTT r
r) Proxy 'LT
_ =
    (LtN (Delete' x ('ForkTree ll (Node ln la) lr) o) n :~: 'True)
-> ((LtN (Delete' x ('ForkTree ll (Node ln la) lr) o) n ~ 'True) =>
    IsBSTT
      ('ForkTree
         (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n a1) r))
-> IsBSTT
     ('ForkTree
        (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n a1) r)
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (Proxy x
-> IsBSTT l
-> Proxy n
-> Proxy o
-> LtN (Delete' x l o) n :~: 'True
forall (x :: Nat) (t :: Tree) (n :: Nat) (o :: Ordering).
(ProofLtNDelete' x t n o, LtN t n ~ 'True) =>
Proxy x
-> IsBSTT t
-> Proxy n
-> Proxy o
-> LtN (Delete' x t o) n :~: 'True
proofLtNDelete' Proxy x
px IsBSTT l
l (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n) Proxy o
po) (((LtN (Delete' x ('ForkTree ll (Node ln la) lr) o) n ~ 'True) =>
  IsBSTT
    ('ForkTree
       (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n a1) r))
 -> IsBSTT
      ('ForkTree
         (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n a1) r))
-> ((LtN (Delete' x ('ForkTree ll (Node ln la) lr) o) n ~ 'True) =>
    IsBSTT
      ('ForkTree
         (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n a1) r))
-> IsBSTT
     ('ForkTree
        (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n a1) r)
forall a b. (a -> b) -> a -> b
$
      IsBSTT (Delete' x ('ForkTree ll (Node ln la) lr) o)
-> Proxy (Node n a)
-> IsBSTT r
-> IsBSTT
     ('ForkTree
        (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n a) r)
forall (l :: Tree) (n :: Nat) (r :: Tree) a.
(LtN l n ~ 'True, GtN r n ~ 'True) =>
IsBSTT l
-> Proxy (Node n a)
-> IsBSTT r
-> IsBSTT ('ForkTree l (Node n a) r)
ForkIsBSTT (Proxy x -> IsBSTT l -> Proxy o -> IsBSTT (Delete' x l o)
forall (x :: Nat) (t :: Tree) (o :: Ordering).
ProofIsBSTDelete' x t o =>
Proxy x -> IsBSTT t -> Proxy o -> IsBSTT (Delete' x t o)
proofIsBSTDelete' Proxy x
px IsBSTT l
l Proxy o
po) Proxy (Node n a)
node IsBSTT r
r
    where
      po :: Proxy o
po = Proxy o
forall {k} (t :: k). Proxy t
Proxy :: Proxy o

instance ProofIsBSTDelete' x ('ForkTree l (Node n a1) 'EmptyTree) 'GT where
  proofIsBSTDelete' :: Proxy x
-> IsBSTT ('ForkTree l (Node n a1) 'EmptyTree)
-> Proxy 'GT
-> IsBSTT (Delete' x ('ForkTree l (Node n a1) 'EmptyTree) 'GT)
proofIsBSTDelete' Proxy x
_ IsBSTT ('ForkTree l (Node n a1) 'EmptyTree)
tIsBST Proxy 'GT
_ = IsBSTT ('ForkTree l (Node n a1) 'EmptyTree)
IsBSTT (Delete' x ('ForkTree l (Node n a1) 'EmptyTree) 'GT)
tIsBST

instance
  ( r ~ 'ForkTree rl (Node rn ra) rr,
    o ~ CmpNat x rn,
    ProofIsBSTDelete' x r o,
    ProofGtNDelete' x r n o
  ) =>
  ProofIsBSTDelete' x ('ForkTree l (Node n a1) ('ForkTree rl (Node rn ra) rr)) 'GT
  where
  proofIsBSTDelete' :: Proxy x
-> IsBSTT ('ForkTree l (Node n a1) ('ForkTree rl (Node rn ra) rr))
-> Proxy 'GT
-> IsBSTT
     (Delete'
        x ('ForkTree l (Node n a1) ('ForkTree rl (Node rn ra) rr)) 'GT)
proofIsBSTDelete' Proxy x
px (ForkIsBSTT IsBSTT l
l Proxy (Node n a)
node IsBSTT r
r) Proxy 'GT
_ =
    (GtN (Delete' x ('ForkTree rl (Node rn ra) rr) o) n :~: 'True)
-> ((GtN (Delete' x ('ForkTree rl (Node rn ra) rr) o) n ~ 'True) =>
    IsBSTT
      ('ForkTree
         l (Node n a1) (Delete' x ('ForkTree rl (Node rn ra) rr) o)))
-> IsBSTT
     ('ForkTree
        l (Node n a1) (Delete' x ('ForkTree rl (Node rn ra) rr) o))
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (Proxy x
-> IsBSTT r
-> Proxy n
-> Proxy o
-> GtN (Delete' x r o) n :~: 'True
forall (x :: Nat) (t :: Tree) (n :: Nat) (o :: Ordering).
(ProofGtNDelete' x t n o, GtN t n ~ 'True) =>
Proxy x
-> IsBSTT t
-> Proxy n
-> Proxy o
-> GtN (Delete' x t o) n :~: 'True
proofGtNDelete' Proxy x
px IsBSTT r
r (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n) Proxy o
po) (((GtN (Delete' x ('ForkTree rl (Node rn ra) rr) o) n ~ 'True) =>
  IsBSTT
    ('ForkTree
       l (Node n a1) (Delete' x ('ForkTree rl (Node rn ra) rr) o)))
 -> IsBSTT
      ('ForkTree
         l (Node n a1) (Delete' x ('ForkTree rl (Node rn ra) rr) o)))
-> ((GtN (Delete' x ('ForkTree rl (Node rn ra) rr) o) n ~ 'True) =>
    IsBSTT
      ('ForkTree
         l (Node n a1) (Delete' x ('ForkTree rl (Node rn ra) rr) o)))
-> IsBSTT
     ('ForkTree
        l (Node n a1) (Delete' x ('ForkTree rl (Node rn ra) rr) o))
forall a b. (a -> b) -> a -> b
$
      IsBSTT l
-> Proxy (Node n a)
-> IsBSTT (Delete' x ('ForkTree rl (Node rn ra) rr) o)
-> IsBSTT
     ('ForkTree
        l (Node n a) (Delete' x ('ForkTree rl (Node rn ra) rr) o))
forall (l :: Tree) (n :: Nat) (r :: Tree) a.
(LtN l n ~ 'True, GtN r n ~ 'True) =>
IsBSTT l
-> Proxy (Node n a)
-> IsBSTT r
-> IsBSTT ('ForkTree l (Node n a) r)
ForkIsBSTT IsBSTT l
l Proxy (Node n a)
node (Proxy x -> IsBSTT r -> Proxy o -> IsBSTT (Delete' x r o)
forall (x :: Nat) (t :: Tree) (o :: Ordering).
ProofIsBSTDelete' x t o =>
Proxy x -> IsBSTT t -> Proxy o -> IsBSTT (Delete' x t o)
proofIsBSTDelete' Proxy x
px IsBSTT r
r Proxy o
po)
    where
      po :: Proxy o
po = Proxy o
forall {k} (t :: k). Proxy t
Proxy :: Proxy o

-- | Prove that deleting a node with key @x@
-- in a tree @t@ which verifies @LtN t n ~ 'True@ preserves the `LtN` invariant,
-- given that the comparison between @x@ and the root key of the tree equals @o@.
-- The @o@ parameter guides the proof.
class ProofLtNDelete' (x :: Nat) (t :: Tree) (n :: Nat) (o :: Ordering) where
  proofLtNDelete' ::
    (LtN t n ~ 'True) =>
    Proxy x ->
    IsBSTT t ->
    Proxy n ->
    Proxy o ->
    LtN (Delete' x t o) n :~: 'True

instance ProofLtNDelete' x ('ForkTree 'EmptyTree (Node n1 a1) 'EmptyTree) n 'EQ where
  proofLtNDelete' :: (LtN ('ForkTree 'EmptyTree (Node n1 a1) 'EmptyTree) n ~ 'True) =>
Proxy x
-> IsBSTT ('ForkTree 'EmptyTree (Node n1 a1) 'EmptyTree)
-> Proxy n
-> Proxy 'EQ
-> LtN
     (Delete' x ('ForkTree 'EmptyTree (Node n1 a1) 'EmptyTree) 'EQ) n
   :~: 'True
proofLtNDelete' Proxy x
_ IsBSTT ('ForkTree 'EmptyTree (Node n1 a1) 'EmptyTree)
_ Proxy n
_ Proxy 'EQ
_ = LtN
  (Delete' x ('ForkTree 'EmptyTree (Node n1 a1) 'EmptyTree) 'EQ) n
:~: 'True
forall {k} (a :: k). a :~: a
Refl

instance
  (LtN ('ForkTree rl (Node rn ra) rr) n ~ 'True) =>
  ProofLtNDelete' x ('ForkTree 'EmptyTree (Node n1 a1) ('ForkTree rl (Node rn ra) rr)) n 'EQ
  where
  proofLtNDelete' :: (LtN
   ('ForkTree 'EmptyTree (Node n1 a1) ('ForkTree rl (Node rn ra) rr))
   n
 ~ 'True) =>
Proxy x
-> IsBSTT
     ('ForkTree 'EmptyTree (Node n1 a1) ('ForkTree rl (Node rn ra) rr))
-> Proxy n
-> Proxy 'EQ
-> LtN
     (Delete'
        x
        ('ForkTree 'EmptyTree (Node n1 a1) ('ForkTree rl (Node rn ra) rr))
        'EQ)
     n
   :~: 'True
proofLtNDelete' Proxy x
_ IsBSTT
  ('ForkTree 'EmptyTree (Node n1 a1) ('ForkTree rl (Node rn ra) rr))
_ Proxy n
_ Proxy 'EQ
_ = LtN
  (Delete'
     x
     ('ForkTree 'EmptyTree (Node n1 a1) ('ForkTree rl (Node rn ra) rr))
     'EQ)
  n
:~: 'True
forall {k} (a :: k). a :~: a
Refl

instance
  (LtN ('ForkTree ll (Node ln la) lr) n ~ 'True) =>
  ProofLtNDelete' x ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a1) 'EmptyTree) n 'EQ
  where
  proofLtNDelete' :: (LtN
   ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a1) 'EmptyTree)
   n
 ~ 'True) =>
Proxy x
-> IsBSTT
     ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a1) 'EmptyTree)
-> Proxy n
-> Proxy 'EQ
-> LtN
     (Delete'
        x
        ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a1) 'EmptyTree)
        'EQ)
     n
   :~: 'True
proofLtNDelete' Proxy x
_ IsBSTT
  ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a1) 'EmptyTree)
_ Proxy n
_ Proxy 'EQ
_ = LtN
  (Delete'
     x
     ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a1) 'EmptyTree)
     'EQ)
  n
:~: 'True
forall {k} (a :: k). a :~: a
Refl

instance
  ( l ~ 'ForkTree ll (Node ln la) lr,
    r ~ 'ForkTree rl (Node rn ra) rr,
    LtN l n ~ 'True,
    LtN r n ~ 'True,
    ProofLTMaxKey l n,
    ProofLtNMaxKeyDelete l n
  ) =>
  ProofLtNDelete' x ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a1) ('ForkTree rl (Node rn ra) rr)) n 'EQ
  where
  proofLtNDelete' :: (LtN
   ('ForkTree
      ('ForkTree ll (Node ln la) lr)
      (Node n1 a1)
      ('ForkTree rl (Node rn ra) rr))
   n
 ~ 'True) =>
Proxy x
-> IsBSTT
     ('ForkTree
        ('ForkTree ll (Node ln la) lr)
        (Node n1 a1)
        ('ForkTree rl (Node rn ra) rr))
-> Proxy n
-> Proxy 'EQ
-> LtN
     (Delete'
        x
        ('ForkTree
           ('ForkTree ll (Node ln la) lr)
           (Node n1 a1)
           ('ForkTree rl (Node rn ra) rr))
        'EQ)
     n
   :~: 'True
proofLtNDelete' Proxy x
_ (ForkIsBSTT IsBSTT l
l Proxy (Node n a)
_ IsBSTT r
_) Proxy n
pn Proxy 'EQ
_ =
    (CmpNat (MaxKey ('ForkTree ll (Node ln la) lr)) n :~: 'LT)
-> ((CmpNat (MaxKey ('ForkTree ll (Node ln la) lr)) n ~ 'LT) =>
    If
      (CmpNat (MaxKey ('ForkTree ll (Node ln la) lr)) n == 'LT)
      (If
         (LtN (MaxKeyDelete ('ForkTree ll (Node ln la) lr)) n)
         'True
         (TypeError ...))
      (TypeError ...)
    :~: 'True)
-> If
     (CmpNat (MaxKey ('ForkTree ll (Node ln la) lr)) n == 'LT)
     (If
        (LtN (MaxKeyDelete ('ForkTree ll (Node ln la) lr)) n)
        'True
        (TypeError ...))
     (TypeError ...)
   :~: 'True
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (IsBSTT l -> Proxy n -> CmpNat (MaxKey l) n :~: 'LT
forall (t :: Tree) (n :: Nat).
(ProofLTMaxKey t n, LtN t n ~ 'True) =>
IsBSTT t -> Proxy n -> CmpNat (MaxKey t) n :~: 'LT
proofLTMaxKey IsBSTT l
l Proxy n
pn) (((CmpNat (MaxKey ('ForkTree ll (Node ln la) lr)) n ~ 'LT) =>
  If
    (CmpNat (MaxKey ('ForkTree ll (Node ln la) lr)) n == 'LT)
    (If
       (LtN (MaxKeyDelete ('ForkTree ll (Node ln la) lr)) n)
       'True
       (TypeError ...))
    (TypeError ...)
  :~: 'True)
 -> If
      (CmpNat (MaxKey ('ForkTree ll (Node ln la) lr)) n == 'LT)
      (If
         (LtN (MaxKeyDelete ('ForkTree ll (Node ln la) lr)) n)
         'True
         (TypeError ...))
      (TypeError ...)
    :~: 'True)
-> ((CmpNat (MaxKey ('ForkTree ll (Node ln la) lr)) n ~ 'LT) =>
    If
      (CmpNat (MaxKey ('ForkTree ll (Node ln la) lr)) n == 'LT)
      (If
         (LtN (MaxKeyDelete ('ForkTree ll (Node ln la) lr)) n)
         'True
         (TypeError ...))
      (TypeError ...)
    :~: 'True)
-> If
     (CmpNat (MaxKey ('ForkTree ll (Node ln la) lr)) n == 'LT)
     (If
        (LtN (MaxKeyDelete ('ForkTree ll (Node ln la) lr)) n)
        'True
        (TypeError ...))
     (TypeError ...)
   :~: 'True
forall a b. (a -> b) -> a -> b
$
      (LtN (MaxKeyDelete ('ForkTree ll (Node ln la) lr)) n :~: 'True)
-> ((LtN (MaxKeyDelete ('ForkTree ll (Node ln la) lr)) n
     ~ 'True) =>
    If
      (CmpNat (MaxKey ('ForkTree ll (Node ln la) lr)) n == 'LT)
      (If
         (LtN (MaxKeyDelete ('ForkTree ll (Node ln la) lr)) n)
         'True
         (TypeError ...))
      (TypeError ...)
    :~: 'True)
-> If
     (CmpNat (MaxKey ('ForkTree ll (Node ln la) lr)) n == 'LT)
     (If
        (LtN (MaxKeyDelete ('ForkTree ll (Node ln la) lr)) n)
        'True
        (TypeError ...))
     (TypeError ...)
   :~: 'True
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (IsBSTT l -> Proxy n -> LtN (MaxKeyDelete l) n :~: 'True
forall (t :: Tree) (n :: Nat).
(ProofLtNMaxKeyDelete t n, LtN t n ~ 'True) =>
IsBSTT t -> Proxy n -> LtN (MaxKeyDelete t) n :~: 'True
proofLtNMaxKeyDelete IsBSTT l
l Proxy n
pn) (LtN (MaxKeyDelete ('ForkTree ll (Node ln la) lr)) n ~ 'True) =>
If
  (CmpNat (MaxKey ('ForkTree ll (Node ln la) lr)) n == 'LT)
  (If
     (LtN (MaxKeyDelete ('ForkTree ll (Node ln la) lr)) n)
     'True
     (TypeError ...))
  (TypeError ...)
:~: 'True
forall {k} (a :: k). a :~: a
Refl

instance ProofLtNDelete' x ('ForkTree 'EmptyTree (Node n1 a1) r) n 'LT where
  proofLtNDelete' :: (LtN ('ForkTree 'EmptyTree (Node n1 a1) r) n ~ 'True) =>
Proxy x
-> IsBSTT ('ForkTree 'EmptyTree (Node n1 a1) r)
-> Proxy n
-> Proxy 'LT
-> LtN (Delete' x ('ForkTree 'EmptyTree (Node n1 a1) r) 'LT) n
   :~: 'True
proofLtNDelete' Proxy x
_ IsBSTT ('ForkTree 'EmptyTree (Node n1 a1) r)
_ Proxy n
_ Proxy 'LT
_ = LtN (Delete' x ('ForkTree 'EmptyTree (Node n1 a1) r) 'LT) n
:~: 'True
forall {k} (a :: k). a :~: a
Refl

instance
  ( l ~ 'ForkTree ll (Node ln la) lr,
    o ~ CmpNat x ln,
    LtN l n ~ 'True,
    ProofLtNDelete' x l n o
  ) =>
  ProofLtNDelete' x ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a1) r) n 'LT
  where
  proofLtNDelete' :: (LtN ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a1) r) n
 ~ 'True) =>
Proxy x
-> IsBSTT ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a1) r)
-> Proxy n
-> Proxy 'LT
-> LtN
     (Delete'
        x ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a1) r) 'LT)
     n
   :~: 'True
proofLtNDelete' Proxy x
px (ForkIsBSTT IsBSTT l
l Proxy (Node n a)
_ IsBSTT r
_) Proxy n
pn Proxy 'LT
_ =
    (LtN (Delete' x ('ForkTree ll (Node ln la) lr) o) n :~: 'True)
-> ((LtN (Delete' x ('ForkTree ll (Node ln la) lr) o) n ~ 'True) =>
    If
      (CmpNat n1 n == 'LT)
      (If
         (LtN (Delete' x ('ForkTree ll (Node ln la) lr) o) n)
         (If (LtN r n) 'True (TypeError ...))
         (TypeError ...))
      (TypeError ...)
    :~: 'True)
-> If
     (CmpNat n1 n == 'LT)
     (If
        (LtN (Delete' x ('ForkTree ll (Node ln la) lr) o) n)
        (If (LtN r n) 'True (TypeError ...))
        (TypeError ...))
     (TypeError ...)
   :~: 'True
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (Proxy x
-> IsBSTT l
-> Proxy n
-> Proxy o
-> LtN (Delete' x l o) n :~: 'True
forall (x :: Nat) (t :: Tree) (n :: Nat) (o :: Ordering).
(ProofLtNDelete' x t n o, LtN t n ~ 'True) =>
Proxy x
-> IsBSTT t
-> Proxy n
-> Proxy o
-> LtN (Delete' x t o) n :~: 'True
proofLtNDelete' Proxy x
px IsBSTT l
l Proxy n
pn (Proxy o
forall {k} (t :: k). Proxy t
Proxy :: Proxy o)) (LtN (Delete' x ('ForkTree ll (Node ln la) lr) o) n ~ 'True) =>
If
  (CmpNat n1 n == 'LT)
  (If
     (LtN (Delete' x ('ForkTree ll (Node ln la) lr) o) n)
     (If (LtN r n) 'True (TypeError ...))
     (TypeError ...))
  (TypeError ...)
:~: 'True
forall {k} (a :: k). a :~: a
Refl

instance ProofLtNDelete' x ('ForkTree l (Node n1 a1) 'EmptyTree) n 'GT where
  proofLtNDelete' :: (LtN ('ForkTree l (Node n1 a1) 'EmptyTree) n ~ 'True) =>
Proxy x
-> IsBSTT ('ForkTree l (Node n1 a1) 'EmptyTree)
-> Proxy n
-> Proxy 'GT
-> LtN (Delete' x ('ForkTree l (Node n1 a1) 'EmptyTree) 'GT) n
   :~: 'True
proofLtNDelete' Proxy x
_ IsBSTT ('ForkTree l (Node n1 a1) 'EmptyTree)
_ Proxy n
_ Proxy 'GT
_ = LtN (Delete' x ('ForkTree l (Node n1 a1) 'EmptyTree) 'GT) n
:~: 'True
forall {k} (a :: k). a :~: a
Refl

instance
  ( r ~ 'ForkTree rl (Node rn ra) rr,
    o ~ CmpNat x rn,
    LtN r n ~ 'True,
    ProofLtNDelete' x r n o
  ) =>
  ProofLtNDelete' x ('ForkTree l (Node n1 a1) ('ForkTree rl (Node rn ra) rr)) n 'GT
  where
  proofLtNDelete' :: (LtN ('ForkTree l (Node n1 a1) ('ForkTree rl (Node rn ra) rr)) n
 ~ 'True) =>
Proxy x
-> IsBSTT ('ForkTree l (Node n1 a1) ('ForkTree rl (Node rn ra) rr))
-> Proxy n
-> Proxy 'GT
-> LtN
     (Delete'
        x ('ForkTree l (Node n1 a1) ('ForkTree rl (Node rn ra) rr)) 'GT)
     n
   :~: 'True
proofLtNDelete' Proxy x
px (ForkIsBSTT IsBSTT l
_ Proxy (Node n a)
_ IsBSTT r
r) Proxy n
pn Proxy 'GT
_ =
    (LtN (Delete' x ('ForkTree rl (Node rn ra) rr) o) n :~: 'True)
-> ((LtN (Delete' x ('ForkTree rl (Node rn ra) rr) o) n ~ 'True) =>
    If
      (CmpNat n1 n == 'LT)
      (If
         (LtN l n)
         (If
            (LtN (Delete' x ('ForkTree rl (Node rn ra) rr) o) n)
            'True
            (TypeError ...))
         (TypeError ...))
      (TypeError ...)
    :~: 'True)
-> If
     (CmpNat n1 n == 'LT)
     (If
        (LtN l n)
        (If
           (LtN (Delete' x ('ForkTree rl (Node rn ra) rr) o) n)
           'True
           (TypeError ...))
        (TypeError ...))
     (TypeError ...)
   :~: 'True
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (Proxy x
-> IsBSTT r
-> Proxy n
-> Proxy o
-> LtN (Delete' x r o) n :~: 'True
forall (x :: Nat) (t :: Tree) (n :: Nat) (o :: Ordering).
(ProofLtNDelete' x t n o, LtN t n ~ 'True) =>
Proxy x
-> IsBSTT t
-> Proxy n
-> Proxy o
-> LtN (Delete' x t o) n :~: 'True
proofLtNDelete' Proxy x
px IsBSTT r
r Proxy n
pn (Proxy o
forall {k} (t :: k). Proxy t
Proxy :: Proxy o)) (LtN (Delete' x ('ForkTree rl (Node rn ra) rr) o) n ~ 'True) =>
If
  (CmpNat n1 n == 'LT)
  (If
     (LtN l n)
     (If
        (LtN (Delete' x ('ForkTree rl (Node rn ra) rr) o) n)
        'True
        (TypeError ...))
     (TypeError ...))
  (TypeError ...)
:~: 'True
forall {k} (a :: k). a :~: a
Refl

-- | Prove that deleting a node with key @x@
-- in a tree @t@ which verifies @GtN t n ~ 'True@ preserves the `GtN` invariant,
-- given that the comparison between @x@ and the root key of the tree equals @o@.
-- The @o@ parameter guides the proof.
class ProofGtNDelete' (x :: Nat) (t :: Tree) (n :: Nat) (o :: Ordering) where
  proofGtNDelete' ::
    (GtN t n ~ 'True) =>
    Proxy x ->
    IsBSTT t ->
    Proxy n ->
    Proxy o ->
    GtN (Delete' x t o) n :~: 'True

instance ProofGtNDelete' x ('ForkTree 'EmptyTree (Node n1 a1) 'EmptyTree) n 'EQ where
  proofGtNDelete' :: (GtN ('ForkTree 'EmptyTree (Node n1 a1) 'EmptyTree) n ~ 'True) =>
Proxy x
-> IsBSTT ('ForkTree 'EmptyTree (Node n1 a1) 'EmptyTree)
-> Proxy n
-> Proxy 'EQ
-> GtN
     (Delete' x ('ForkTree 'EmptyTree (Node n1 a1) 'EmptyTree) 'EQ) n
   :~: 'True
proofGtNDelete' Proxy x
_ IsBSTT ('ForkTree 'EmptyTree (Node n1 a1) 'EmptyTree)
_ Proxy n
_ Proxy 'EQ
_ = GtN
  (Delete' x ('ForkTree 'EmptyTree (Node n1 a1) 'EmptyTree) 'EQ) n
:~: 'True
forall {k} (a :: k). a :~: a
Refl

instance
  (GtN ('ForkTree rl (Node rn ra) rr) n ~ 'True) =>
  ProofGtNDelete' x ('ForkTree 'EmptyTree (Node n1 a1) ('ForkTree rl (Node rn ra) rr)) n 'EQ
  where
  proofGtNDelete' :: (GtN
   ('ForkTree 'EmptyTree (Node n1 a1) ('ForkTree rl (Node rn ra) rr))
   n
 ~ 'True) =>
Proxy x
-> IsBSTT
     ('ForkTree 'EmptyTree (Node n1 a1) ('ForkTree rl (Node rn ra) rr))
-> Proxy n
-> Proxy 'EQ
-> GtN
     (Delete'
        x
        ('ForkTree 'EmptyTree (Node n1 a1) ('ForkTree rl (Node rn ra) rr))
        'EQ)
     n
   :~: 'True
proofGtNDelete' Proxy x
_ IsBSTT
  ('ForkTree 'EmptyTree (Node n1 a1) ('ForkTree rl (Node rn ra) rr))
_ Proxy n
_ Proxy 'EQ
_ = GtN
  (Delete'
     x
     ('ForkTree 'EmptyTree (Node n1 a1) ('ForkTree rl (Node rn ra) rr))
     'EQ)
  n
:~: 'True
forall {k} (a :: k). a :~: a
Refl

instance
  (GtN ('ForkTree ll (Node ln la) lr) n ~ 'True) =>
  ProofGtNDelete' x ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a1) 'EmptyTree) n 'EQ
  where
  proofGtNDelete' :: (GtN
   ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a1) 'EmptyTree)
   n
 ~ 'True) =>
Proxy x
-> IsBSTT
     ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a1) 'EmptyTree)
-> Proxy n
-> Proxy 'EQ
-> GtN
     (Delete'
        x
        ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a1) 'EmptyTree)
        'EQ)
     n
   :~: 'True
proofGtNDelete' Proxy x
_ IsBSTT
  ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a1) 'EmptyTree)
_ Proxy n
_ Proxy 'EQ
_ = GtN
  (Delete'
     x
     ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a1) 'EmptyTree)
     'EQ)
  n
:~: 'True
forall {k} (a :: k). a :~: a
Refl

instance
  ( l ~ 'ForkTree ll (Node ln la) lr,
    r ~ 'ForkTree rl (Node rn ra) rr,
    GtN l n ~ 'True,
    GtN r n ~ 'True,
    ProofGTMaxKey l n,
    ProofGtNMaxKeyDelete l n
  ) =>
  ProofGtNDelete' x ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a1) r) n 'EQ
  where
  proofGtNDelete' :: (GtN ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a1) r) n
 ~ 'True) =>
Proxy x
-> IsBSTT ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a1) r)
-> Proxy n
-> Proxy 'EQ
-> GtN
     (Delete'
        x ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a1) r) 'EQ)
     n
   :~: 'True
proofGtNDelete' Proxy x
_ (ForkIsBSTT IsBSTT l
l Proxy (Node n a)
_ IsBSTT r
_) Proxy n
pn Proxy 'EQ
_ =
    (GtN (MaxKeyDelete ('ForkTree ll (Node ln la) lr)) n :~: 'True)
-> ((GtN (MaxKeyDelete ('ForkTree ll (Node ln la) lr)) n
     ~ 'True) =>
    If
      (CmpNat (MaxKey ('ForkTree ll (Node ln la) lr)) n == 'GT)
      (If
         (GtN (MaxKeyDelete ('ForkTree ll (Node ln la) lr)) n)
         'True
         (TypeError ...))
      (TypeError ...)
    :~: 'True)
-> If
     (CmpNat (MaxKey ('ForkTree ll (Node ln la) lr)) n == 'GT)
     (If
        (GtN (MaxKeyDelete ('ForkTree ll (Node ln la) lr)) n)
        'True
        (TypeError ...))
     (TypeError ...)
   :~: 'True
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (IsBSTT l -> Proxy n -> GtN (MaxKeyDelete l) n :~: 'True
forall (t :: Tree) (n :: Nat).
(ProofGtNMaxKeyDelete t n, GtN t n ~ 'True) =>
IsBSTT t -> Proxy n -> GtN (MaxKeyDelete t) n :~: 'True
proofGtNMaxKeyDelete IsBSTT l
l Proxy n
pn) (((GtN (MaxKeyDelete ('ForkTree ll (Node ln la) lr)) n ~ 'True) =>
  If
    (CmpNat (MaxKey ('ForkTree ll (Node ln la) lr)) n == 'GT)
    (If
       (GtN (MaxKeyDelete ('ForkTree ll (Node ln la) lr)) n)
       'True
       (TypeError ...))
    (TypeError ...)
  :~: 'True)
 -> If
      (CmpNat (MaxKey ('ForkTree ll (Node ln la) lr)) n == 'GT)
      (If
         (GtN (MaxKeyDelete ('ForkTree ll (Node ln la) lr)) n)
         'True
         (TypeError ...))
      (TypeError ...)
    :~: 'True)
-> ((GtN (MaxKeyDelete ('ForkTree ll (Node ln la) lr)) n
     ~ 'True) =>
    If
      (CmpNat (MaxKey ('ForkTree ll (Node ln la) lr)) n == 'GT)
      (If
         (GtN (MaxKeyDelete ('ForkTree ll (Node ln la) lr)) n)
         'True
         (TypeError ...))
      (TypeError ...)
    :~: 'True)
-> If
     (CmpNat (MaxKey ('ForkTree ll (Node ln la) lr)) n == 'GT)
     (If
        (GtN (MaxKeyDelete ('ForkTree ll (Node ln la) lr)) n)
        'True
        (TypeError ...))
     (TypeError ...)
   :~: 'True
forall a b. (a -> b) -> a -> b
$
      (CmpNat (MaxKey ('ForkTree ll (Node ln la) lr)) n :~: 'GT)
-> ((CmpNat (MaxKey ('ForkTree ll (Node ln la) lr)) n ~ 'GT) =>
    If
      (CmpNat (MaxKey ('ForkTree ll (Node ln la) lr)) n == 'GT)
      (If
         (GtN (MaxKeyDelete ('ForkTree ll (Node ln la) lr)) n)
         'True
         (TypeError ...))
      (TypeError ...)
    :~: 'True)
-> If
     (CmpNat (MaxKey ('ForkTree ll (Node ln la) lr)) n == 'GT)
     (If
        (GtN (MaxKeyDelete ('ForkTree ll (Node ln la) lr)) n)
        'True
        (TypeError ...))
     (TypeError ...)
   :~: 'True
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (IsBSTT l -> Proxy n -> CmpNat (MaxKey l) n :~: 'GT
forall (t :: Tree) (n :: Nat).
(ProofGTMaxKey t n, GtN t n ~ 'True) =>
IsBSTT t -> Proxy n -> CmpNat (MaxKey t) n :~: 'GT
proofGTMaxKey IsBSTT l
l Proxy n
pn) (CmpNat (MaxKey ('ForkTree ll (Node ln la) lr)) n ~ 'GT) =>
If
  (CmpNat (MaxKey ('ForkTree ll (Node ln la) lr)) n == 'GT)
  (If
     (GtN (MaxKeyDelete ('ForkTree ll (Node ln la) lr)) n)
     'True
     (TypeError ...))
  (TypeError ...)
:~: 'True
forall {k} (a :: k). a :~: a
Refl

instance ProofGtNDelete' x ('ForkTree 'EmptyTree (Node n1 a1) r) n 'LT where
  proofGtNDelete' :: (GtN ('ForkTree 'EmptyTree (Node n1 a1) r) n ~ 'True) =>
Proxy x
-> IsBSTT ('ForkTree 'EmptyTree (Node n1 a1) r)
-> Proxy n
-> Proxy 'LT
-> GtN (Delete' x ('ForkTree 'EmptyTree (Node n1 a1) r) 'LT) n
   :~: 'True
proofGtNDelete' Proxy x
_ IsBSTT ('ForkTree 'EmptyTree (Node n1 a1) r)
_ Proxy n
_ Proxy 'LT
_ = GtN (Delete' x ('ForkTree 'EmptyTree (Node n1 a1) r) 'LT) n
:~: 'True
forall {k} (a :: k). a :~: a
Refl

instance
  ( l ~ 'ForkTree ll (Node ln la) lr,
    o ~ CmpNat x ln,
    GtN l n ~ 'True,
    ProofGtNDelete' x l n o
  ) =>
  ProofGtNDelete' x ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a1) r) n 'LT
  where
  proofGtNDelete' :: (GtN ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a1) r) n
 ~ 'True) =>
Proxy x
-> IsBSTT ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a1) r)
-> Proxy n
-> Proxy 'LT
-> GtN
     (Delete'
        x ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a1) r) 'LT)
     n
   :~: 'True
proofGtNDelete' Proxy x
px (ForkIsBSTT IsBSTT l
l Proxy (Node n a)
_ IsBSTT r
_) Proxy n
pn Proxy 'LT
_ =
    (GtN (Delete' x ('ForkTree ll (Node ln la) lr) o) n :~: 'True)
-> ((GtN (Delete' x ('ForkTree ll (Node ln la) lr) o) n ~ 'True) =>
    If
      (CmpNat n1 n == 'GT)
      (If
         (GtN (Delete' x ('ForkTree ll (Node ln la) lr) o) n)
         (If (GtN r n) 'True (TypeError ...))
         (TypeError ...))
      (TypeError ...)
    :~: 'True)
-> If
     (CmpNat n1 n == 'GT)
     (If
        (GtN (Delete' x ('ForkTree ll (Node ln la) lr) o) n)
        (If (GtN r n) 'True (TypeError ...))
        (TypeError ...))
     (TypeError ...)
   :~: 'True
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (Proxy x
-> IsBSTT l
-> Proxy n
-> Proxy o
-> GtN (Delete' x l o) n :~: 'True
forall (x :: Nat) (t :: Tree) (n :: Nat) (o :: Ordering).
(ProofGtNDelete' x t n o, GtN t n ~ 'True) =>
Proxy x
-> IsBSTT t
-> Proxy n
-> Proxy o
-> GtN (Delete' x t o) n :~: 'True
proofGtNDelete' Proxy x
px IsBSTT l
l Proxy n
pn (Proxy o
forall {k} (t :: k). Proxy t
Proxy :: Proxy o)) (GtN (Delete' x ('ForkTree ll (Node ln la) lr) o) n ~ 'True) =>
If
  (CmpNat n1 n == 'GT)
  (If
     (GtN (Delete' x ('ForkTree ll (Node ln la) lr) o) n)
     (If (GtN r n) 'True (TypeError ...))
     (TypeError ...))
  (TypeError ...)
:~: 'True
forall {k} (a :: k). a :~: a
Refl

instance ProofGtNDelete' x ('ForkTree l (Node n1 a1) 'EmptyTree) n 'GT where
  proofGtNDelete' :: (GtN ('ForkTree l (Node n1 a1) 'EmptyTree) n ~ 'True) =>
Proxy x
-> IsBSTT ('ForkTree l (Node n1 a1) 'EmptyTree)
-> Proxy n
-> Proxy 'GT
-> GtN (Delete' x ('ForkTree l (Node n1 a1) 'EmptyTree) 'GT) n
   :~: 'True
proofGtNDelete' Proxy x
_ IsBSTT ('ForkTree l (Node n1 a1) 'EmptyTree)
_ Proxy n
_ Proxy 'GT
_ = GtN (Delete' x ('ForkTree l (Node n1 a1) 'EmptyTree) 'GT) n
:~: 'True
forall {k} (a :: k). a :~: a
Refl

instance
  ( r ~ 'ForkTree rl (Node rn ra) rr,
    o ~ CmpNat x rn,
    GtN r n ~ 'True,
    ProofGtNDelete' x r n o
  ) =>
  ProofGtNDelete' x ('ForkTree l (Node n1 a1) ('ForkTree rl (Node rn ra) rr)) n 'GT
  where
  proofGtNDelete' :: (GtN ('ForkTree l (Node n1 a1) ('ForkTree rl (Node rn ra) rr)) n
 ~ 'True) =>
Proxy x
-> IsBSTT ('ForkTree l (Node n1 a1) ('ForkTree rl (Node rn ra) rr))
-> Proxy n
-> Proxy 'GT
-> GtN
     (Delete'
        x ('ForkTree l (Node n1 a1) ('ForkTree rl (Node rn ra) rr)) 'GT)
     n
   :~: 'True
proofGtNDelete' Proxy x
px (ForkIsBSTT IsBSTT l
_ Proxy (Node n a)
_ IsBSTT r
r) Proxy n
pn Proxy 'GT
_ =
    (GtN (Delete' x ('ForkTree rl (Node rn ra) rr) o) n :~: 'True)
-> ((GtN (Delete' x ('ForkTree rl (Node rn ra) rr) o) n ~ 'True) =>
    If
      (CmpNat n1 n == 'GT)
      (If
         (GtN l n)
         (If
            (GtN (Delete' x ('ForkTree rl (Node rn ra) rr) o) n)
            'True
            (TypeError ...))
         (TypeError ...))
      (TypeError ...)
    :~: 'True)
-> If
     (CmpNat n1 n == 'GT)
     (If
        (GtN l n)
        (If
           (GtN (Delete' x ('ForkTree rl (Node rn ra) rr) o) n)
           'True
           (TypeError ...))
        (TypeError ...))
     (TypeError ...)
   :~: 'True
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (Proxy x
-> IsBSTT r
-> Proxy n
-> Proxy o
-> GtN (Delete' x r o) n :~: 'True
forall (x :: Nat) (t :: Tree) (n :: Nat) (o :: Ordering).
(ProofGtNDelete' x t n o, GtN t n ~ 'True) =>
Proxy x
-> IsBSTT t
-> Proxy n
-> Proxy o
-> GtN (Delete' x t o) n :~: 'True
proofGtNDelete' Proxy x
px IsBSTT r
r Proxy n
pn (Proxy o
forall {k} (t :: k). Proxy t
Proxy :: Proxy o)) (GtN (Delete' x ('ForkTree rl (Node rn ra) rr) o) n ~ 'True) =>
If
  (CmpNat n1 n == 'GT)
  (If
     (GtN l n)
     (If
        (GtN (Delete' x ('ForkTree rl (Node rn ra) rr) o) n)
        'True
        (TypeError ...))
     (TypeError ...))
  (TypeError ...)
:~: 'True
forall {k} (a :: k). a :~: a
Refl

-- | Prove that deleting the node with maximum key value
-- in a `Data.Tree.BST.Extern.Constructors.BST` @t@ preserves the @BST@ restrictions.
-- This proof is needed for the `Data.Tree.Extern.delete` operation.
class ProofMaxKeyDeleteIsBST (t :: Tree) where
  proofMaxKeyDeleteIsBST :: IsBSTT t -> IsBSTT (MaxKeyDelete t)

instance ProofMaxKeyDeleteIsBST 'EmptyTree where
  proofMaxKeyDeleteIsBST :: IsBSTT 'EmptyTree -> IsBSTT (MaxKeyDelete 'EmptyTree)
proofMaxKeyDeleteIsBST IsBSTT 'EmptyTree
_ = IsBSTT 'EmptyTree
IsBSTT (MaxKeyDelete 'EmptyTree)
EmptyIsBSTT

instance ProofMaxKeyDeleteIsBST ('ForkTree 'EmptyTree (Node n a) 'EmptyTree) where
  proofMaxKeyDeleteIsBST :: IsBSTT ('ForkTree 'EmptyTree (Node n a) 'EmptyTree)
-> IsBSTT
     (MaxKeyDelete ('ForkTree 'EmptyTree (Node n a) 'EmptyTree))
proofMaxKeyDeleteIsBST IsBSTT ('ForkTree 'EmptyTree (Node n a) 'EmptyTree)
_ = IsBSTT 'EmptyTree
IsBSTT (MaxKeyDelete ('ForkTree 'EmptyTree (Node n a) 'EmptyTree))
EmptyIsBSTT

instance ProofMaxKeyDeleteIsBST ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a) 'EmptyTree) where
  proofMaxKeyDeleteIsBST :: IsBSTT
  ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a) 'EmptyTree)
-> IsBSTT
     (MaxKeyDelete
        ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a) 'EmptyTree))
proofMaxKeyDeleteIsBST (ForkIsBSTT IsBSTT l
lIsBST Proxy (Node n a)
_ IsBSTT r
_) = IsBSTT l
IsBSTT
  (MaxKeyDelete
     ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a) 'EmptyTree))
lIsBST

instance
  ( l ~ 'ForkTree ll (Node ln la) lr,
    r ~ 'ForkTree rl (Node rn ra) rr,
    ProofMaxKeyDeleteIsBST r,
    ProofGtNMaxKeyDelete r n
  ) =>
  ProofMaxKeyDeleteIsBST ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a) ('ForkTree rl (Node rn ra) rr))
  where
  proofMaxKeyDeleteIsBST :: IsBSTT
  ('ForkTree
     ('ForkTree ll (Node ln la) lr)
     (Node n a)
     ('ForkTree rl (Node rn ra) rr))
-> IsBSTT
     (MaxKeyDelete
        ('ForkTree
           ('ForkTree ll (Node ln la) lr)
           (Node n a)
           ('ForkTree rl (Node rn ra) rr)))
proofMaxKeyDeleteIsBST (ForkIsBSTT IsBSTT l
l Proxy (Node n a)
node IsBSTT r
r) =
    (GtN (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)) n :~: 'True)
-> ((GtN (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)) n
     ~ 'True) =>
    IsBSTT
      ('ForkTree
         ('ForkTree ll (Node ln la) lr)
         (Node n a)
         (MaxKeyDelete ('ForkTree rl (Node rn ra) rr))))
-> IsBSTT
     ('ForkTree
        ('ForkTree ll (Node ln la) lr)
        (Node n a)
        (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (IsBSTT r -> Proxy n -> GtN (MaxKeyDelete r) n :~: 'True
forall (t :: Tree) (n :: Nat).
(ProofGtNMaxKeyDelete t n, GtN t n ~ 'True) =>
IsBSTT t -> Proxy n -> GtN (MaxKeyDelete t) n :~: 'True
proofGtNMaxKeyDelete IsBSTT r
r (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)) (((GtN (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)) n ~ 'True) =>
  IsBSTT
    ('ForkTree
       ('ForkTree ll (Node ln la) lr)
       (Node n a)
       (MaxKeyDelete ('ForkTree rl (Node rn ra) rr))))
 -> IsBSTT
      ('ForkTree
         ('ForkTree ll (Node ln la) lr)
         (Node n a)
         (MaxKeyDelete ('ForkTree rl (Node rn ra) rr))))
-> ((GtN (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)) n
     ~ 'True) =>
    IsBSTT
      ('ForkTree
         ('ForkTree ll (Node ln la) lr)
         (Node n a)
         (MaxKeyDelete ('ForkTree rl (Node rn ra) rr))))
-> IsBSTT
     ('ForkTree
        ('ForkTree ll (Node ln la) lr)
        (Node n a)
        (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
forall a b. (a -> b) -> a -> b
$
      IsBSTT l
-> Proxy (Node n a)
-> IsBSTT (MaxKeyDelete ('ForkTree rl (Node rn ra) rr))
-> IsBSTT
     ('ForkTree
        l (Node n a) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
forall (l :: Tree) (n :: Nat) (r :: Tree) a.
(LtN l n ~ 'True, GtN r n ~ 'True) =>
IsBSTT l
-> Proxy (Node n a)
-> IsBSTT r
-> IsBSTT ('ForkTree l (Node n a) r)
ForkIsBSTT IsBSTT l
l Proxy (Node n a)
node (IsBSTT r -> IsBSTT (MaxKeyDelete r)
forall (t :: Tree).
ProofMaxKeyDeleteIsBST t =>
IsBSTT t -> IsBSTT (MaxKeyDelete t)
proofMaxKeyDeleteIsBST IsBSTT r
r)

-- | Prove that in a tree @t@ which verifies that @GtN t n ~ 'True@,
-- the maximum key of @t@ is also greater than @n@.
-- This proof is needed for the `Data.Tree.BST.Extern.delete` operation.
class ProofGTMaxKey (t :: Tree) (n :: Nat) where
  proofGTMaxKey ::
    (GtN t n ~ 'True) =>
    IsBSTT t ->
    Proxy n ->
    CmpNat (MaxKey t) n :~: 'GT

instance
  (CmpNat n1 n ~ 'GT) =>
  ProofGTMaxKey ('ForkTree l (Node n1 a) 'EmptyTree) n
  where
  proofGTMaxKey :: (GtN ('ForkTree l (Node n1 a) 'EmptyTree) n ~ 'True) =>
IsBSTT ('ForkTree l (Node n1 a) 'EmptyTree)
-> Proxy n
-> CmpNat (MaxKey ('ForkTree l (Node n1 a) 'EmptyTree)) n :~: 'GT
proofGTMaxKey IsBSTT ('ForkTree l (Node n1 a) 'EmptyTree)
_ Proxy n
_ = CmpNat (MaxKey ('ForkTree l (Node n1 a) 'EmptyTree)) n :~: 'GT
forall {k} (a :: k). a :~: a
Refl

instance
  ( r ~ 'ForkTree rl (Node rn ra) rr,
    GtN r n ~ 'True,
    ProofGTMaxKey r n
  ) =>
  ProofGTMaxKey ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr)) n
  where
  proofGTMaxKey :: (GtN ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr)) n
 ~ 'True) =>
IsBSTT ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr))
-> Proxy n
-> CmpNat
     (MaxKey ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr))) n
   :~: 'GT
proofGTMaxKey (ForkIsBSTT IsBSTT l
_ Proxy (Node n a)
_ IsBSTT r
r) Proxy n
pn =
    (CmpNat (MaxKey ('ForkTree rl (Node rn ra) rr)) n :~: 'GT)
-> ((CmpNat (MaxKey ('ForkTree rl (Node rn ra) rr)) n ~ 'GT) =>
    CmpNat (MaxKey ('ForkTree rl (Node rn ra) rr)) n :~: 'GT)
-> CmpNat (MaxKey ('ForkTree rl (Node rn ra) rr)) n :~: 'GT
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (IsBSTT r -> Proxy n -> CmpNat (MaxKey r) n :~: 'GT
forall (t :: Tree) (n :: Nat).
(ProofGTMaxKey t n, GtN t n ~ 'True) =>
IsBSTT t -> Proxy n -> CmpNat (MaxKey t) n :~: 'GT
proofGTMaxKey IsBSTT r
r Proxy n
pn) (CmpNat (MaxKey ('ForkTree rl (Node rn ra) rr)) n ~ 'GT) =>
CmpNat (MaxKey ('ForkTree rl (Node rn ra) rr)) n :~: 'GT
forall {k} (a :: k). a :~: a
Refl

-- | Prove that in a tree @t@ which verifies that @GtN t n ~ 'True@,
-- the tree resulting from the removal of the maximum key of @t@ preserves the `GtN` invariant.
-- This proof is needed for the `Data.Tree.Extern.delete` operation.
class ProofGtNMaxKeyDelete (t :: Tree) (n :: Nat) where
  proofGtNMaxKeyDelete ::
    (GtN t n ~ 'True) =>
    IsBSTT t ->
    Proxy n ->
    GtN (MaxKeyDelete t) n :~: 'True

instance
  (GtN l n ~ 'True) =>
  ProofGtNMaxKeyDelete ('ForkTree l (Node n1 a) 'EmptyTree) n
  where
  proofGtNMaxKeyDelete :: (GtN ('ForkTree l (Node n1 a) 'EmptyTree) n ~ 'True) =>
IsBSTT ('ForkTree l (Node n1 a) 'EmptyTree)
-> Proxy n
-> GtN (MaxKeyDelete ('ForkTree l (Node n1 a) 'EmptyTree)) n
   :~: 'True
proofGtNMaxKeyDelete IsBSTT ('ForkTree l (Node n1 a) 'EmptyTree)
_ Proxy n
_ = GtN (MaxKeyDelete ('ForkTree l (Node n1 a) 'EmptyTree)) n :~: 'True
forall {k} (a :: k). a :~: a
Refl

instance
  ( r ~ 'ForkTree rl (Node rn ra) rr,
    GtN r n ~ 'True,
    ProofGtNMaxKeyDelete r n
  ) =>
  ProofGtNMaxKeyDelete ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr)) n
  where
  proofGtNMaxKeyDelete :: (GtN ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr)) n
 ~ 'True) =>
IsBSTT ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr))
-> Proxy n
-> GtN
     (MaxKeyDelete
        ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr)))
     n
   :~: 'True
proofGtNMaxKeyDelete (ForkIsBSTT IsBSTT l
_ Proxy (Node n a)
_ IsBSTT r
r) Proxy n
pn =
    (GtN (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)) n :~: 'True)
-> ((GtN (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)) n
     ~ 'True) =>
    If
      (CmpNat n1 n == 'GT)
      (If
         (GtN l n)
         (If
            (GtN (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)) n)
            'True
            (TypeError ...))
         (TypeError ...))
      (TypeError ...)
    :~: 'True)
-> If
     (CmpNat n1 n == 'GT)
     (If
        (GtN l n)
        (If
           (GtN (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)) n)
           'True
           (TypeError ...))
        (TypeError ...))
     (TypeError ...)
   :~: 'True
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (IsBSTT r -> Proxy n -> GtN (MaxKeyDelete r) n :~: 'True
forall (t :: Tree) (n :: Nat).
(ProofGtNMaxKeyDelete t n, GtN t n ~ 'True) =>
IsBSTT t -> Proxy n -> GtN (MaxKeyDelete t) n :~: 'True
proofGtNMaxKeyDelete IsBSTT r
r Proxy n
pn) (GtN (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)) n ~ 'True) =>
If
  (CmpNat n1 n == 'GT)
  (If
     (GtN l n)
     (If
        (GtN (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)) n)
        'True
        (TypeError ...))
     (TypeError ...))
  (TypeError ...)
:~: 'True
forall {k} (a :: k). a :~: a
Refl

-- | Prove that in a tree @t@ which verifies that @LtN t n ~ 'True@,
-- the maximum key of @t@ is also less than @n@.
-- This proof is needed for the `Data.Tree.Extern.delete` operation.
class ProofLTMaxKey (t :: Tree) (n :: Nat) where
  proofLTMaxKey ::
    (LtN t n ~ 'True) =>
    IsBSTT t ->
    Proxy n ->
    CmpNat (MaxKey t) n :~: 'LT

instance
  (CmpNat n1 n ~ 'LT) =>
  ProofLTMaxKey ('ForkTree l (Node n1 a) 'EmptyTree) n
  where
  proofLTMaxKey :: (LtN ('ForkTree l (Node n1 a) 'EmptyTree) n ~ 'True) =>
IsBSTT ('ForkTree l (Node n1 a) 'EmptyTree)
-> Proxy n
-> CmpNat (MaxKey ('ForkTree l (Node n1 a) 'EmptyTree)) n :~: 'LT
proofLTMaxKey IsBSTT ('ForkTree l (Node n1 a) 'EmptyTree)
_ Proxy n
_ = CmpNat (MaxKey ('ForkTree l (Node n1 a) 'EmptyTree)) n :~: 'LT
forall {k} (a :: k). a :~: a
Refl

instance
  ( r ~ 'ForkTree rl (Node rn ra) rr,
    LtN r n ~ 'True,
    ProofLTMaxKey r n
  ) =>
  ProofLTMaxKey ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr)) n
  where
  proofLTMaxKey :: (LtN ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr)) n
 ~ 'True) =>
IsBSTT ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr))
-> Proxy n
-> CmpNat
     (MaxKey ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr))) n
   :~: 'LT
proofLTMaxKey (ForkIsBSTT IsBSTT l
_ Proxy (Node n a)
_ IsBSTT r
r) Proxy n
pn =
    (CmpNat (MaxKey ('ForkTree rl (Node rn ra) rr)) n :~: 'LT)
-> ((CmpNat (MaxKey ('ForkTree rl (Node rn ra) rr)) n ~ 'LT) =>
    CmpNat (MaxKey ('ForkTree rl (Node rn ra) rr)) n :~: 'LT)
-> CmpNat (MaxKey ('ForkTree rl (Node rn ra) rr)) n :~: 'LT
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (IsBSTT r -> Proxy n -> CmpNat (MaxKey r) n :~: 'LT
forall (t :: Tree) (n :: Nat).
(ProofLTMaxKey t n, LtN t n ~ 'True) =>
IsBSTT t -> Proxy n -> CmpNat (MaxKey t) n :~: 'LT
proofLTMaxKey IsBSTT r
r Proxy n
pn) (CmpNat (MaxKey ('ForkTree rl (Node rn ra) rr)) n ~ 'LT) =>
CmpNat (MaxKey ('ForkTree rl (Node rn ra) rr)) n :~: 'LT
forall {k} (a :: k). a :~: a
Refl

-- | Prove that in a tree @t@ which verifies that @LtN t n ~ 'True@,
-- the tree resulting from the removal of the maximum key of @t@ preserves the `LtN` invariant.
-- This proof is needed for the `Data.Tree.Extern.delete` operation.
class ProofLtNMaxKeyDelete (t :: Tree) (n :: Nat) where
  proofLtNMaxKeyDelete ::
    (LtN t n ~ 'True) =>
    IsBSTT t ->
    Proxy n ->
    LtN (MaxKeyDelete t) n :~: 'True

instance
  (LtN l n ~ 'True) =>
  ProofLtNMaxKeyDelete ('ForkTree l (Node n1 a) 'EmptyTree) n
  where
  proofLtNMaxKeyDelete :: (LtN ('ForkTree l (Node n1 a) 'EmptyTree) n ~ 'True) =>
IsBSTT ('ForkTree l (Node n1 a) 'EmptyTree)
-> Proxy n
-> LtN (MaxKeyDelete ('ForkTree l (Node n1 a) 'EmptyTree)) n
   :~: 'True
proofLtNMaxKeyDelete IsBSTT ('ForkTree l (Node n1 a) 'EmptyTree)
_ Proxy n
_ = LtN (MaxKeyDelete ('ForkTree l (Node n1 a) 'EmptyTree)) n :~: 'True
forall {k} (a :: k). a :~: a
Refl

instance
  ( r ~ 'ForkTree rl (Node rn ra) rr,
    LtN r n ~ 'True,
    ProofLtNMaxKeyDelete r n
  ) =>
  ProofLtNMaxKeyDelete ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr)) n
  where
  proofLtNMaxKeyDelete :: (LtN ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr)) n
 ~ 'True) =>
IsBSTT ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr))
-> Proxy n
-> LtN
     (MaxKeyDelete
        ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr)))
     n
   :~: 'True
proofLtNMaxKeyDelete (ForkIsBSTT IsBSTT l
_ Proxy (Node n a)
_ IsBSTT r
r) Proxy n
pn =
    (LtN (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)) n :~: 'True)
-> ((LtN (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)) n
     ~ 'True) =>
    If
      (CmpNat n1 n == 'LT)
      (If
         (LtN l n)
         (If
            (LtN (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)) n)
            'True
            (TypeError ...))
         (TypeError ...))
      (TypeError ...)
    :~: 'True)
-> If
     (CmpNat n1 n == 'LT)
     (If
        (LtN l n)
        (If
           (LtN (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)) n)
           'True
           (TypeError ...))
        (TypeError ...))
     (TypeError ...)
   :~: 'True
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (IsBSTT r -> Proxy n -> LtN (MaxKeyDelete r) n :~: 'True
forall (t :: Tree) (n :: Nat).
(ProofLtNMaxKeyDelete t n, LtN t n ~ 'True) =>
IsBSTT t -> Proxy n -> LtN (MaxKeyDelete t) n :~: 'True
proofLtNMaxKeyDelete IsBSTT r
r Proxy n
pn) (LtN (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)) n ~ 'True) =>
If
  (CmpNat n1 n == 'LT)
  (If
     (LtN l n)
     (If
        (LtN (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)) n)
        'True
        (TypeError ...))
     (TypeError ...))
  (TypeError ...)
:~: 'True
forall {k} (a :: k). a :~: a
Refl