{-# 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 AVL 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.AVL.Extern.Delete" respects the key ordering and height balance restrictions.
module Data.Tree.AVL.Extern.DeleteProofs
  ( IsBalancedT (..),
    ProofIsBalancedDelete (proofIsBalancedDelete),
    ProofIsBSTDelete (proofIsBSTDelete),
  )
where

import Data.Proxy (Proxy (Proxy))
import Data.Tree.AVL.Extern.BalanceProofs
  ( ProofGtNBalance (proofGtNBalance),
    ProofIsBSTBalance (proofIsBSTBalance),
    ProofIsBalancedBalance (proofIsBalancedBalance),
    ProofLtNBalance (proofLtNBalance),
  )
import Data.Tree.AVL.Extern.Constructors (IsAlmostBalancedT (ForkIsAlmostBalancedT), IsBalancedT (EmptyIsBalancedT, ForkIsBalancedT))
import Data.Tree.AVL.Extern.Delete
  ( Deletable (Delete),
    Deletable' (Delete'),
    MaxKeyDeletable (MaxKeyDelete),
  )
import Data.Tree.BST.Extern.Constructors (IsBSTT (EmptyIsBSTT, ForkIsBSTT))
import Data.Tree.BST.Extern.Delete (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 an `Data.Tree.AVL.Extern.Constructors.AVL` tree preserves the @AVL@ 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 inserting a node with key @x@ and element value @a@
-- in an `Data.Tree.AVL.Extern.Constructors.AVL` tree preserves the @AVL@ restrictions, given that the comparison between
-- @x@ and the root key of the tree equals @o@.
-- The @AVL@ restrictions were already checked when `Data.Tree.AVL.Extern.InsertProofs.proofIsBSTInsert` 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)
_ IsBSTT r
rIsBST) 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,
    ProofIsBSTBalance ('ForkTree (MaxKeyDelete l) (Node (MaxKey l) (MaxValue l)) r)
  ) =>
  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
lIsBST Proxy (Node n a)
_ IsBSTT r
rIsBST) Proxy 'EQ
_ =
    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)
-> IsBSTT
     (Balance
        ('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 (t :: Tree).
ProofIsBSTBalance t =>
IsBSTT t -> IsBSTT (Balance t)
proofIsBSTBalance (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)
 -> IsBSTT
      (Balance
         ('ForkTree
            (MaxKeyDelete ('ForkTree ll (Node ln la) lr))
            (Node
               (MaxKey ('ForkTree ll (Node ln la) lr))
               (MaxValue ('ForkTree ll (Node ln la) lr)))
            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)
-> IsBSTT
     (Balance
        ('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 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) (a :: Tree) r.
(LtN l n ~ 'True, GtN a n ~ 'True) =>
IsBSTT l
-> Proxy (Node n r)
-> IsBSTT a
-> IsBSTT ('ForkTree l (Node n r) a)
ForkIsBSTT (IsBSTT l -> IsBSTT (MaxKeyDelete l)
forall (t :: Tree).
ProofMaxKeyDeleteIsBST t =>
IsBSTT t -> IsBSTT (MaxKeyDelete t)
proofMaxKeyDeleteIsBST IsBSTT l
lIsBST) 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
rIsBST
    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,
    CmpNat x n ~ 'LT,
    ProofIsBSTDelete' x l o,
    ProofLtNDelete' x l n o,
    ProofIsBSTBalance ('ForkTree (Delete' x l o) (Node n a1) r)
  ) =>
  ProofIsBSTDelete' x ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a1) r) 'LT
  where
  proofIsBSTDelete' :: Proxy x
-> IsBSTT ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a1) r)
-> Proxy 'LT
-> IsBSTT
     (Delete'
        x ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a1) r) 'LT)
proofIsBSTDelete' Proxy x
px (ForkIsBSTT IsBSTT l
lIsBST Proxy (Node n a)
node IsBSTT r
rIsBST) 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
      (Balance'
         ('ForkTree
            (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n a1) r)
         (UnbalancedState
            (Height (Delete' x ('ForkTree ll (Node ln la) lr) o)) (Height r))))
-> IsBSTT
     (Balance'
        ('ForkTree
           (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n a1) r)
        (UnbalancedState
           (Height (Delete' x ('ForkTree ll (Node ln la) lr) o)) (Height 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, CmpNat x n ~ 'LT, 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
lIsBST (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n) (Proxy o
forall {k} (t :: k). Proxy t
Proxy :: Proxy o)) (((LtN (Delete' x ('ForkTree ll (Node ln la) lr) o) n ~ 'True) =>
  IsBSTT
    (Balance'
       ('ForkTree
          (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n a1) r)
       (UnbalancedState
          (Height (Delete' x ('ForkTree ll (Node ln la) lr) o)) (Height r))))
 -> IsBSTT
      (Balance'
         ('ForkTree
            (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n a1) r)
         (UnbalancedState
            (Height (Delete' x ('ForkTree ll (Node ln la) lr) o)) (Height r))))
-> ((LtN (Delete' x ('ForkTree ll (Node ln la) lr) o) n ~ 'True) =>
    IsBSTT
      (Balance'
         ('ForkTree
            (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n a1) r)
         (UnbalancedState
            (Height (Delete' x ('ForkTree ll (Node ln la) lr) o)) (Height r))))
-> IsBSTT
     (Balance'
        ('ForkTree
           (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n a1) r)
        (UnbalancedState
           (Height (Delete' x ('ForkTree ll (Node ln la) lr) o)) (Height r)))
forall a b. (a -> b) -> a -> b
$
      IsBSTT
  ('ForkTree
     (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n a) r)
-> IsBSTT
     (Balance
        ('ForkTree
           (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n a) r))
forall (t :: Tree).
ProofIsBSTBalance t =>
IsBSTT t -> IsBSTT (Balance t)
proofIsBSTBalance (IsBSTT
   ('ForkTree
      (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n a) r)
 -> IsBSTT
      (Balance
         ('ForkTree
            (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n a) r)))
-> IsBSTT
     ('ForkTree
        (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n a) r)
-> IsBSTT
     (Balance
        ('ForkTree
           (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n a) 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) (a :: Tree) r.
(LtN l n ~ 'True, GtN a n ~ 'True) =>
IsBSTT l
-> Proxy (Node n r)
-> IsBSTT a
-> IsBSTT ('ForkTree l (Node n r) a)
ForkIsBSTT (Proxy x -> IsBSTT l -> IsBSTT (Delete x l)
forall (x :: Nat) (t :: Tree).
ProofIsBSTDelete x t =>
Proxy x -> IsBSTT t -> IsBSTT (Delete x t)
proofIsBSTDelete Proxy x
px IsBSTT l
lIsBST) Proxy (Node n a)
node IsBSTT r
rIsBST

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,
    CmpNat x n ~ 'GT,
    ProofIsBSTDelete' x r o,
    ProofGtNDelete' x r n o,
    ProofIsBSTBalance ('ForkTree l (Node n a1) (Delete' x r 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
lIsBST Proxy (Node n a)
node IsBSTT r
rIsBST) 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
      (Balance'
         ('ForkTree
            l (Node n a1) (Delete' x ('ForkTree rl (Node rn ra) rr) o))
         (UnbalancedState
            (Height l) (Height (Delete' x ('ForkTree rl (Node rn ra) rr) o)))))
-> IsBSTT
     (Balance'
        ('ForkTree
           l (Node n a1) (Delete' x ('ForkTree rl (Node rn ra) rr) o))
        (UnbalancedState
           (Height l) (Height (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, CmpNat x n ~ 'GT, 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
rIsBST (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n) (Proxy o
forall {k} (t :: k). Proxy t
Proxy :: Proxy o)) (((GtN (Delete' x ('ForkTree rl (Node rn ra) rr) o) n ~ 'True) =>
  IsBSTT
    (Balance'
       ('ForkTree
          l (Node n a1) (Delete' x ('ForkTree rl (Node rn ra) rr) o))
       (UnbalancedState
          (Height l) (Height (Delete' x ('ForkTree rl (Node rn ra) rr) o)))))
 -> IsBSTT
      (Balance'
         ('ForkTree
            l (Node n a1) (Delete' x ('ForkTree rl (Node rn ra) rr) o))
         (UnbalancedState
            (Height l) (Height (Delete' x ('ForkTree rl (Node rn ra) rr) o)))))
-> ((GtN (Delete' x ('ForkTree rl (Node rn ra) rr) o) n ~ 'True) =>
    IsBSTT
      (Balance'
         ('ForkTree
            l (Node n a1) (Delete' x ('ForkTree rl (Node rn ra) rr) o))
         (UnbalancedState
            (Height l) (Height (Delete' x ('ForkTree rl (Node rn ra) rr) o)))))
-> IsBSTT
     (Balance'
        ('ForkTree
           l (Node n a1) (Delete' x ('ForkTree rl (Node rn ra) rr) o))
        (UnbalancedState
           (Height l) (Height (Delete' x ('ForkTree rl (Node rn ra) rr) o))))
forall a b. (a -> b) -> a -> b
$
      IsBSTT
  ('ForkTree
     l (Node n a) (Delete' x ('ForkTree rl (Node rn ra) rr) o))
-> IsBSTT
     (Balance
        ('ForkTree
           l (Node n a) (Delete' x ('ForkTree rl (Node rn ra) rr) o)))
forall (t :: Tree).
ProofIsBSTBalance t =>
IsBSTT t -> IsBSTT (Balance t)
proofIsBSTBalance (IsBSTT
   ('ForkTree
      l (Node n a) (Delete' x ('ForkTree rl (Node rn ra) rr) o))
 -> IsBSTT
      (Balance
         ('ForkTree
            l (Node n a) (Delete' x ('ForkTree rl (Node rn ra) rr) o))))
-> IsBSTT
     ('ForkTree
        l (Node n a) (Delete' x ('ForkTree rl (Node rn ra) rr) o))
-> IsBSTT
     (Balance
        ('ForkTree
           l (Node n a) (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) (a :: Tree) r.
(LtN l n ~ 'True, GtN a n ~ 'True) =>
IsBSTT l
-> Proxy (Node n r)
-> IsBSTT a
-> IsBSTT ('ForkTree l (Node n r) a)
ForkIsBSTT IsBSTT l
lIsBST Proxy (Node n a)
node (Proxy x -> IsBSTT r -> IsBSTT (Delete x r)
forall (x :: Nat) (t :: Tree).
ProofIsBSTDelete x t =>
Proxy x -> IsBSTT t -> IsBSTT (Delete x t)
proofIsBSTDelete Proxy x
px IsBSTT r
rIsBST)

-- | Prove that deleting a node with key @x@ (lower than @n@)
-- 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' ::
    (CmpNat x n ~ 'LT, 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' :: (CmpNat x n ~ 'LT,
 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' :: (CmpNat x n ~ 'LT,
 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' :: (CmpNat x n ~ 'LT,
 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,
    GtN r (MaxKey l) ~ 'True,
    LtN (MaxKeyDelete l) (MaxKey l) ~ 'True,
    ProofLTMaxKey l n,
    ProofLtNMaxKeyDelete l n,
    ProofMaxKeyDeleteIsBST l,
    ProofLtNBalance ('ForkTree (MaxKeyDelete l) (Node (MaxKey l) (MaxValue l)) r) n
  ) =>
  ProofLtNDelete' x ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a1) ('ForkTree rl (Node rn ra) rr)) n 'EQ
  where
  proofLtNDelete' :: (CmpNat x n ~ 'LT,
 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
lIsBST Proxy (Node n a)
_ IsBSTT r
rIsBST) Proxy n
pn Proxy 'EQ
_ =
    (LtN (MaxKeyDelete ('ForkTree ll (Node ln la) lr)) n :~: 'True)
-> ((LtN (MaxKeyDelete ('ForkTree ll (Node ln la) lr)) n
     ~ 'True) =>
    LtN
      (Balance'
         ('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))
         (UnbalancedState
            (Height (MaxKeyDelete ('ForkTree ll (Node ln la) lr)))
            (1 + If (Height rl <=? Height rr) (Height rr) (Height rl))))
      n
    :~: 'True)
-> LtN
     (Balance'
        ('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))
        (UnbalancedState
           (Height (MaxKeyDelete ('ForkTree ll (Node ln la) lr)))
           (1 + If (Height rl <=? Height rr) (Height rr) (Height rl))))
     n
   :~: '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
lIsBST Proxy n
pn) (((LtN (MaxKeyDelete ('ForkTree ll (Node ln la) lr)) n ~ 'True) =>
  LtN
    (Balance'
       ('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))
       (UnbalancedState
          (Height (MaxKeyDelete ('ForkTree ll (Node ln la) lr)))
          (1 + If (Height rl <=? Height rr) (Height rr) (Height rl))))
    n
  :~: 'True)
 -> LtN
      (Balance'
         ('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))
         (UnbalancedState
            (Height (MaxKeyDelete ('ForkTree ll (Node ln la) lr)))
            (1 + If (Height rl <=? Height rr) (Height rr) (Height rl))))
      n
    :~: 'True)
-> ((LtN (MaxKeyDelete ('ForkTree ll (Node ln la) lr)) n
     ~ 'True) =>
    LtN
      (Balance'
         ('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))
         (UnbalancedState
            (Height (MaxKeyDelete ('ForkTree ll (Node ln la) lr)))
            (1 + If (Height rl <=? Height rr) (Height rr) (Height rl))))
      n
    :~: 'True)
-> LtN
     (Balance'
        ('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))
        (UnbalancedState
           (Height (MaxKeyDelete ('ForkTree ll (Node ln la) lr)))
           (1 + If (Height rl <=? Height rr) (Height rr) (Height rl))))
     n
   :~: 'True
forall a b. (a -> b) -> a -> b
$
      (CmpNat (MaxKey ('ForkTree ll (Node ln la) lr)) n :~: 'LT)
-> ((CmpNat (MaxKey ('ForkTree ll (Node ln la) lr)) n ~ 'LT) =>
    LtN
      (Balance'
         ('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))
         (UnbalancedState
            (Height (MaxKeyDelete ('ForkTree ll (Node ln la) lr)))
            (1 + If (Height rl <=? Height rr) (Height rr) (Height rl))))
      n
    :~: 'True)
-> LtN
     (Balance'
        ('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))
        (UnbalancedState
           (Height (MaxKeyDelete ('ForkTree ll (Node ln la) lr)))
           (1 + If (Height rl <=? Height rr) (Height rr) (Height rl))))
     n
   :~: '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
lIsBST Proxy n
pn) (((CmpNat (MaxKey ('ForkTree ll (Node ln la) lr)) n ~ 'LT) =>
  LtN
    (Balance'
       ('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))
       (UnbalancedState
          (Height (MaxKeyDelete ('ForkTree ll (Node ln la) lr)))
          (1 + If (Height rl <=? Height rr) (Height rr) (Height rl))))
    n
  :~: 'True)
 -> LtN
      (Balance'
         ('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))
         (UnbalancedState
            (Height (MaxKeyDelete ('ForkTree ll (Node ln la) lr)))
            (1 + If (Height rl <=? Height rr) (Height rr) (Height rl))))
      n
    :~: 'True)
-> ((CmpNat (MaxKey ('ForkTree ll (Node ln la) lr)) n ~ 'LT) =>
    LtN
      (Balance'
         ('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))
         (UnbalancedState
            (Height (MaxKeyDelete ('ForkTree ll (Node ln la) lr)))
            (1 + If (Height rl <=? Height rr) (Height rr) (Height rl))))
      n
    :~: 'True)
-> LtN
     (Balance'
        ('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))
        (UnbalancedState
           (Height (MaxKeyDelete ('ForkTree ll (Node ln la) lr)))
           (1 + If (Height rl <=? Height rr) (Height rr) (Height rl))))
     n
   :~: 'True
forall a b. (a -> b) -> a -> b
$
        (LtN
   (Balance'
      ('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))
      (UnbalancedState
         (Height (MaxKeyDelete ('ForkTree ll (Node ln la) lr)))
         (1 + If (Height rl <=? Height rr) (Height rr) (Height rl))))
   n
 :~: 'True)
-> ((LtN
       (Balance'
          ('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))
          (UnbalancedState
             (Height (MaxKeyDelete ('ForkTree ll (Node ln la) lr)))
             (1 + If (Height rl <=? Height rr) (Height rr) (Height rl))))
       n
     ~ 'True) =>
    LtN
      (Balance'
         ('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))
         (UnbalancedState
            (Height (MaxKeyDelete ('ForkTree ll (Node ln la) lr)))
            (1 + If (Height rl <=? Height rr) (Height rr) (Height rl))))
      n
    :~: 'True)
-> LtN
     (Balance'
        ('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))
        (UnbalancedState
           (Height (MaxKeyDelete ('ForkTree ll (Node ln la) lr)))
           (1 + If (Height rl <=? Height rr) (Height rr) (Height rl))))
     n
   :~: 'True
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (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)
-> Proxy n
-> LtN
     (Balance
        ('ForkTree
           (MaxKeyDelete ('ForkTree ll (Node ln la) lr))
           (Node
              (MaxKey ('ForkTree ll (Node ln la) lr))
              (MaxValue ('ForkTree ll (Node ln la) lr)))
           r))
     n
   :~: 'True
forall (t :: Tree) (n :: Nat).
(ProofLtNBalance t n, LtN t n ~ 'True) =>
IsBSTT t -> Proxy n -> LtN (Balance t) n :~: 'True
proofLtNBalance (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) (a :: Tree) r.
(LtN l n ~ 'True, GtN a n ~ 'True) =>
IsBSTT l
-> Proxy (Node n r)
-> IsBSTT a
-> IsBSTT ('ForkTree l (Node n r) a)
ForkIsBSTT IsBSTT (MaxKeyDelete l)
IsBSTT (MaxKeyDelete ('ForkTree ll (Node ln la) lr))
lIsBST' 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
rIsBST) Proxy n
pn) (LtN
   (Balance'
      ('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))
      (UnbalancedState
         (Height (MaxKeyDelete ('ForkTree ll (Node ln la) lr)))
         (1 + If (Height rl <=? Height rr) (Height rr) (Height rl))))
   n
 ~ 'True) =>
LtN
  (Balance'
     ('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))
     (UnbalancedState
        (Height (MaxKeyDelete ('ForkTree ll (Node ln la) lr)))
        (1 + If (Height rl <=? Height rr) (Height rr) (Height rl))))
  n
:~: 'True
forall {k} (a :: k). a :~: a
Refl
    where
      lIsBST' :: IsBSTT (MaxKeyDelete l)
lIsBST' = IsBSTT l -> IsBSTT (MaxKeyDelete l)
forall (t :: Tree).
ProofMaxKeyDeleteIsBST t =>
IsBSTT t -> IsBSTT (MaxKeyDelete t)
proofMaxKeyDeleteIsBST IsBSTT l
lIsBST
      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 ProofLtNDelete' x ('ForkTree 'EmptyTree (Node n1 a1) r) n 'LT where
  proofLtNDelete' :: (CmpNat x n ~ 'LT,
 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,
    LtN r n ~ 'True,
    CmpNat x n1 ~ 'LT,
    ProofLtNDelete' x l n o,
    ProofIsBSTDelete x l,
    ProofLtNDelete' x l n1 o,
    ProofLtNBalance ('ForkTree (Delete' x l o) (Node n1 a1) r) n
  ) =>
  ProofLtNDelete' x ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a1) r) n 'LT
  where
  proofLtNDelete' :: (CmpNat x n ~ 'LT,
 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
lIsBST Proxy (Node n a)
node IsBSTT r
rIsBST) 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) =>
    LtN
      (Balance'
         ('ForkTree
            (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n1 a1) r)
         (UnbalancedState
            (Height (Delete' x ('ForkTree ll (Node ln la) lr) o)) (Height r)))
      n
    :~: 'True)
-> LtN
     (Balance'
        ('ForkTree
           (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n1 a1) r)
        (UnbalancedState
           (Height (Delete' x ('ForkTree ll (Node ln la) lr) o)) (Height r)))
     n
   :~: '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, CmpNat x n ~ 'LT, 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
lIsBST Proxy n
pn Proxy o
po) (((LtN (Delete' x ('ForkTree ll (Node ln la) lr) o) n ~ 'True) =>
  LtN
    (Balance'
       ('ForkTree
          (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n1 a1) r)
       (UnbalancedState
          (Height (Delete' x ('ForkTree ll (Node ln la) lr) o)) (Height r)))
    n
  :~: 'True)
 -> LtN
      (Balance'
         ('ForkTree
            (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n1 a1) r)
         (UnbalancedState
            (Height (Delete' x ('ForkTree ll (Node ln la) lr) o)) (Height r)))
      n
    :~: 'True)
-> ((LtN (Delete' x ('ForkTree ll (Node ln la) lr) o) n ~ 'True) =>
    LtN
      (Balance'
         ('ForkTree
            (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n1 a1) r)
         (UnbalancedState
            (Height (Delete' x ('ForkTree ll (Node ln la) lr) o)) (Height r)))
      n
    :~: 'True)
-> LtN
     (Balance'
        ('ForkTree
           (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n1 a1) r)
        (UnbalancedState
           (Height (Delete' x ('ForkTree ll (Node ln la) lr) o)) (Height r)))
     n
   :~: 'True
forall a b. (a -> b) -> a -> b
$
      (LtN (Delete' x ('ForkTree ll (Node ln la) lr) o) n1 :~: 'True)
-> ((LtN (Delete' x ('ForkTree ll (Node ln la) lr) o) n1
     ~ 'True) =>
    LtN
      (Balance'
         ('ForkTree
            (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n1 a1) r)
         (UnbalancedState
            (Height (Delete' x ('ForkTree ll (Node ln la) lr) o)) (Height r)))
      n
    :~: 'True)
-> LtN
     (Balance'
        ('ForkTree
           (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n1 a1) r)
        (UnbalancedState
           (Height (Delete' x ('ForkTree ll (Node ln la) lr) o)) (Height r)))
     n
   :~: 'True
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (Proxy x
-> IsBSTT l
-> Proxy n1
-> Proxy o
-> LtN (Delete' x l o) n1 :~: 'True
forall (x :: Nat) (t :: Tree) (n :: Nat) (o :: Ordering).
(ProofLtNDelete' x t n o, CmpNat x n ~ 'LT, 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
lIsBST (Proxy n1
forall {k} (t :: k). Proxy t
Proxy :: Proxy n1) Proxy o
po) (((LtN (Delete' x ('ForkTree ll (Node ln la) lr) o) n1 ~ 'True) =>
  LtN
    (Balance'
       ('ForkTree
          (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n1 a1) r)
       (UnbalancedState
          (Height (Delete' x ('ForkTree ll (Node ln la) lr) o)) (Height r)))
    n
  :~: 'True)
 -> LtN
      (Balance'
         ('ForkTree
            (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n1 a1) r)
         (UnbalancedState
            (Height (Delete' x ('ForkTree ll (Node ln la) lr) o)) (Height r)))
      n
    :~: 'True)
-> ((LtN (Delete' x ('ForkTree ll (Node ln la) lr) o) n1
     ~ 'True) =>
    LtN
      (Balance'
         ('ForkTree
            (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n1 a1) r)
         (UnbalancedState
            (Height (Delete' x ('ForkTree ll (Node ln la) lr) o)) (Height r)))
      n
    :~: 'True)
-> LtN
     (Balance'
        ('ForkTree
           (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n1 a1) r)
        (UnbalancedState
           (Height (Delete' x ('ForkTree ll (Node ln la) lr) o)) (Height r)))
     n
   :~: 'True
forall a b. (a -> b) -> a -> b
$
        (LtN
   (Balance'
      ('ForkTree
         (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n1 a1) r)
      (UnbalancedState
         (Height (Delete' x ('ForkTree ll (Node ln la) lr) o)) (Height r)))
   n
 :~: 'True)
-> ((LtN
       (Balance'
          ('ForkTree
             (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n1 a1) r)
          (UnbalancedState
             (Height (Delete' x ('ForkTree ll (Node ln la) lr) o)) (Height r)))
       n
     ~ 'True) =>
    LtN
      (Balance'
         ('ForkTree
            (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n1 a1) r)
         (UnbalancedState
            (Height (Delete' x ('ForkTree ll (Node ln la) lr) o)) (Height r)))
      n
    :~: 'True)
-> LtN
     (Balance'
        ('ForkTree
           (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n1 a1) r)
        (UnbalancedState
           (Height (Delete' x ('ForkTree ll (Node ln la) lr) o)) (Height r)))
     n
   :~: 'True
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (IsBSTT
  ('ForkTree
     (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n a) r)
-> Proxy n
-> LtN
     (Balance
        ('ForkTree
           (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n a) r))
     n
   :~: 'True
forall (t :: Tree) (n :: Nat).
(ProofLtNBalance t n, LtN t n ~ 'True) =>
IsBSTT t -> Proxy n -> LtN (Balance t) n :~: 'True
proofLtNBalance (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) (a :: Tree) r.
(LtN l n ~ 'True, GtN a n ~ 'True) =>
IsBSTT l
-> Proxy (Node n r)
-> IsBSTT a
-> IsBSTT ('ForkTree l (Node n r) a)
ForkIsBSTT IsBSTT (Delete' x ('ForkTree ll (Node ln la) lr) o)
IsBSTT (Delete x l)
lIsBST' Proxy (Node n a)
node IsBSTT r
rIsBST) Proxy n
pn) (LtN
   (Balance'
      ('ForkTree
         (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n1 a1) r)
      (UnbalancedState
         (Height (Delete' x ('ForkTree ll (Node ln la) lr) o)) (Height r)))
   n
 ~ 'True) =>
LtN
  (Balance'
     ('ForkTree
        (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n1 a1) r)
     (UnbalancedState
        (Height (Delete' x ('ForkTree ll (Node ln la) lr) o)) (Height r)))
  n
:~: 'True
forall {k} (a :: k). a :~: a
Refl
    where
      po :: Proxy o
po = Proxy o
forall {k} (t :: k). Proxy t
Proxy :: Proxy o
      lIsBST' :: IsBSTT (Delete x l)
lIsBST' = Proxy x -> IsBSTT l -> IsBSTT (Delete x l)
forall (x :: Nat) (t :: Tree).
ProofIsBSTDelete x t =>
Proxy x -> IsBSTT t -> IsBSTT (Delete x t)
proofIsBSTDelete Proxy x
px IsBSTT l
lIsBST

instance ProofLtNDelete' x ('ForkTree l (Node n1 a1) 'EmptyTree) n 'GT where
  proofLtNDelete' :: (CmpNat x n ~ 'LT,
 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,
    CmpNat x n1 ~ 'GT,
    LtN r n ~ 'True,
    ProofLtNDelete' x r n o,
    ProofGtNDelete' x r n1 o,
    ProofIsBSTDelete x r,
    ProofLtNBalance ('ForkTree l (Node n1 a1) (Delete' x r o)) n
  ) =>
  ProofLtNDelete' x ('ForkTree l (Node n1 a1) ('ForkTree rl (Node rn ra) rr)) n 'GT
  where
  proofLtNDelete' :: (CmpNat x n ~ 'LT,
 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
lIsBST Proxy (Node n a)
node IsBSTT r
rIsBST) 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) =>
    LtN
      (Balance'
         ('ForkTree
            l (Node n1 a1) (Delete' x ('ForkTree rl (Node rn ra) rr) o))
         (UnbalancedState
            (Height l) (Height (Delete' x ('ForkTree rl (Node rn ra) rr) o))))
      n
    :~: 'True)
-> LtN
     (Balance'
        ('ForkTree
           l (Node n1 a1) (Delete' x ('ForkTree rl (Node rn ra) rr) o))
        (UnbalancedState
           (Height l) (Height (Delete' x ('ForkTree rl (Node rn ra) rr) o))))
     n
   :~: '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, CmpNat x n ~ 'LT, 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
rIsBST Proxy n
pn Proxy o
po) (((LtN (Delete' x ('ForkTree rl (Node rn ra) rr) o) n ~ 'True) =>
  LtN
    (Balance'
       ('ForkTree
          l (Node n1 a1) (Delete' x ('ForkTree rl (Node rn ra) rr) o))
       (UnbalancedState
          (Height l) (Height (Delete' x ('ForkTree rl (Node rn ra) rr) o))))
    n
  :~: 'True)
 -> LtN
      (Balance'
         ('ForkTree
            l (Node n1 a1) (Delete' x ('ForkTree rl (Node rn ra) rr) o))
         (UnbalancedState
            (Height l) (Height (Delete' x ('ForkTree rl (Node rn ra) rr) o))))
      n
    :~: 'True)
-> ((LtN (Delete' x ('ForkTree rl (Node rn ra) rr) o) n ~ 'True) =>
    LtN
      (Balance'
         ('ForkTree
            l (Node n1 a1) (Delete' x ('ForkTree rl (Node rn ra) rr) o))
         (UnbalancedState
            (Height l) (Height (Delete' x ('ForkTree rl (Node rn ra) rr) o))))
      n
    :~: 'True)
-> LtN
     (Balance'
        ('ForkTree
           l (Node n1 a1) (Delete' x ('ForkTree rl (Node rn ra) rr) o))
        (UnbalancedState
           (Height l) (Height (Delete' x ('ForkTree rl (Node rn ra) rr) o))))
     n
   :~: 'True
forall a b. (a -> b) -> a -> b
$
      (GtN (Delete' x ('ForkTree rl (Node rn ra) rr) o) n1 :~: 'True)
-> ((GtN (Delete' x ('ForkTree rl (Node rn ra) rr) o) n1
     ~ 'True) =>
    LtN
      (Balance'
         ('ForkTree
            l (Node n1 a1) (Delete' x ('ForkTree rl (Node rn ra) rr) o))
         (UnbalancedState
            (Height l) (Height (Delete' x ('ForkTree rl (Node rn ra) rr) o))))
      n
    :~: 'True)
-> LtN
     (Balance'
        ('ForkTree
           l (Node n1 a1) (Delete' x ('ForkTree rl (Node rn ra) rr) o))
        (UnbalancedState
           (Height l) (Height (Delete' x ('ForkTree rl (Node rn ra) rr) o))))
     n
   :~: 'True
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (Proxy x
-> IsBSTT r
-> Proxy n1
-> Proxy o
-> GtN (Delete' x r o) n1 :~: 'True
forall (x :: Nat) (t :: Tree) (n :: Nat) (o :: Ordering).
(ProofGtNDelete' x t n o, CmpNat x n ~ 'GT, 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
rIsBST (Proxy n1
forall {k} (t :: k). Proxy t
Proxy :: Proxy n1) Proxy o
po) (((GtN (Delete' x ('ForkTree rl (Node rn ra) rr) o) n1 ~ 'True) =>
  LtN
    (Balance'
       ('ForkTree
          l (Node n1 a1) (Delete' x ('ForkTree rl (Node rn ra) rr) o))
       (UnbalancedState
          (Height l) (Height (Delete' x ('ForkTree rl (Node rn ra) rr) o))))
    n
  :~: 'True)
 -> LtN
      (Balance'
         ('ForkTree
            l (Node n1 a1) (Delete' x ('ForkTree rl (Node rn ra) rr) o))
         (UnbalancedState
            (Height l) (Height (Delete' x ('ForkTree rl (Node rn ra) rr) o))))
      n
    :~: 'True)
-> ((GtN (Delete' x ('ForkTree rl (Node rn ra) rr) o) n1
     ~ 'True) =>
    LtN
      (Balance'
         ('ForkTree
            l (Node n1 a1) (Delete' x ('ForkTree rl (Node rn ra) rr) o))
         (UnbalancedState
            (Height l) (Height (Delete' x ('ForkTree rl (Node rn ra) rr) o))))
      n
    :~: 'True)
-> LtN
     (Balance'
        ('ForkTree
           l (Node n1 a1) (Delete' x ('ForkTree rl (Node rn ra) rr) o))
        (UnbalancedState
           (Height l) (Height (Delete' x ('ForkTree rl (Node rn ra) rr) o))))
     n
   :~: 'True
forall a b. (a -> b) -> a -> b
$
        (LtN
   (Balance'
      ('ForkTree
         l (Node n1 a1) (Delete' x ('ForkTree rl (Node rn ra) rr) o))
      (UnbalancedState
         (Height l) (Height (Delete' x ('ForkTree rl (Node rn ra) rr) o))))
   n
 :~: 'True)
-> ((LtN
       (Balance'
          ('ForkTree
             l (Node n1 a1) (Delete' x ('ForkTree rl (Node rn ra) rr) o))
          (UnbalancedState
             (Height l) (Height (Delete' x ('ForkTree rl (Node rn ra) rr) o))))
       n
     ~ 'True) =>
    LtN
      (Balance'
         ('ForkTree
            l (Node n1 a1) (Delete' x ('ForkTree rl (Node rn ra) rr) o))
         (UnbalancedState
            (Height l) (Height (Delete' x ('ForkTree rl (Node rn ra) rr) o))))
      n
    :~: 'True)
-> LtN
     (Balance'
        ('ForkTree
           l (Node n1 a1) (Delete' x ('ForkTree rl (Node rn ra) rr) o))
        (UnbalancedState
           (Height l) (Height (Delete' x ('ForkTree rl (Node rn ra) rr) o))))
     n
   :~: 'True
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (IsBSTT
  ('ForkTree
     l (Node n a) (Delete' x ('ForkTree rl (Node rn ra) rr) o))
-> Proxy n
-> LtN
     (Balance
        ('ForkTree
           l (Node n a) (Delete' x ('ForkTree rl (Node rn ra) rr) o)))
     n
   :~: 'True
forall (t :: Tree) (n :: Nat).
(ProofLtNBalance t n, LtN t n ~ 'True) =>
IsBSTT t -> Proxy n -> LtN (Balance t) n :~: 'True
proofLtNBalance (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) (a :: Tree) r.
(LtN l n ~ 'True, GtN a n ~ 'True) =>
IsBSTT l
-> Proxy (Node n r)
-> IsBSTT a
-> IsBSTT ('ForkTree l (Node n r) a)
ForkIsBSTT IsBSTT l
lIsBST Proxy (Node n a)
node IsBSTT (Delete' x ('ForkTree rl (Node rn ra) rr) o)
IsBSTT (Delete x r)
rIsBST') Proxy n
pn) (LtN
   (Balance'
      ('ForkTree
         l (Node n1 a1) (Delete' x ('ForkTree rl (Node rn ra) rr) o))
      (UnbalancedState
         (Height l) (Height (Delete' x ('ForkTree rl (Node rn ra) rr) o))))
   n
 ~ 'True) =>
LtN
  (Balance'
     ('ForkTree
        l (Node n1 a1) (Delete' x ('ForkTree rl (Node rn ra) rr) o))
     (UnbalancedState
        (Height l) (Height (Delete' x ('ForkTree rl (Node rn ra) rr) o))))
  n
:~: 'True
forall {k} (a :: k). a :~: a
Refl
    where
      po :: Proxy o
po = Proxy o
forall {k} (t :: k). Proxy t
Proxy :: Proxy o
      rIsBST' :: IsBSTT (Delete x r)
rIsBST' = Proxy x -> IsBSTT r -> IsBSTT (Delete x r)
forall (x :: Nat) (t :: Tree).
ProofIsBSTDelete x t =>
Proxy x -> IsBSTT t -> IsBSTT (Delete x t)
proofIsBSTDelete Proxy x
px IsBSTT r
rIsBST

-- | Prove that deleting a node with key @x@ (greater than @n@)
-- 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' ::
    (CmpNat x n ~ 'GT, 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' :: (CmpNat x n ~ 'GT,
 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' :: (CmpNat x n ~ 'GT,
 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' :: (CmpNat x n ~ 'GT,
 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,
    MaxKeyDeletable l,
    GtN l n ~ 'True,
    GtN r n ~ 'True,
    GtN r (MaxKey l) ~ 'True,
    LtN (MaxKeyDelete l) (MaxKey l) ~ 'True,
    ProofGTMaxKey l n,
    ProofGtNMaxKeyDelete l n,
    ProofMaxKeyDeleteIsBST l,
    ProofGtNBalance ('ForkTree (MaxKeyDelete l) (Node (MaxKey l) (MaxValue l)) r) n
  ) =>
  ProofGtNDelete' x ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a1) ('ForkTree rl (Node rn ra) rr)) n 'EQ
  where
  proofGtNDelete' :: (CmpNat x n ~ 'GT,
 GtN
   ('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
-> GtN
     (Delete'
        x
        ('ForkTree
           ('ForkTree ll (Node ln la) lr)
           (Node n1 a1)
           ('ForkTree rl (Node rn ra) rr))
        'EQ)
     n
   :~: 'True
proofGtNDelete' Proxy x
_ (ForkIsBSTT IsBSTT l
lIsBST Proxy (Node n a)
_ IsBSTT r
rIsBST) 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) =>
    GtN
      (Balance'
         ('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))
         (UnbalancedState
            (Height (MaxKeyDelete ('ForkTree ll (Node ln la) lr)))
            (1 + If (Height rl <=? Height rr) (Height rr) (Height rl))))
      n
    :~: 'True)
-> GtN
     (Balance'
        ('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))
        (UnbalancedState
           (Height (MaxKeyDelete ('ForkTree ll (Node ln la) lr)))
           (1 + If (Height rl <=? Height rr) (Height rr) (Height rl))))
     n
   :~: '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, MaxKeyDeletable t, GtN t n ~ 'True) =>
IsBSTT t -> Proxy n -> GtN (MaxKeyDelete t) n :~: 'True
proofGtNMaxKeyDelete IsBSTT l
lIsBST Proxy n
pn) (((GtN (MaxKeyDelete ('ForkTree ll (Node ln la) lr)) n ~ 'True) =>
  GtN
    (Balance'
       ('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))
       (UnbalancedState
          (Height (MaxKeyDelete ('ForkTree ll (Node ln la) lr)))
          (1 + If (Height rl <=? Height rr) (Height rr) (Height rl))))
    n
  :~: 'True)
 -> GtN
      (Balance'
         ('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))
         (UnbalancedState
            (Height (MaxKeyDelete ('ForkTree ll (Node ln la) lr)))
            (1 + If (Height rl <=? Height rr) (Height rr) (Height rl))))
      n
    :~: 'True)
-> ((GtN (MaxKeyDelete ('ForkTree ll (Node ln la) lr)) n
     ~ 'True) =>
    GtN
      (Balance'
         ('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))
         (UnbalancedState
            (Height (MaxKeyDelete ('ForkTree ll (Node ln la) lr)))
            (1 + If (Height rl <=? Height rr) (Height rr) (Height rl))))
      n
    :~: 'True)
-> GtN
     (Balance'
        ('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))
        (UnbalancedState
           (Height (MaxKeyDelete ('ForkTree ll (Node ln la) lr)))
           (1 + If (Height rl <=? Height rr) (Height rr) (Height rl))))
     n
   :~: '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) =>
    GtN
      (Balance'
         ('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))
         (UnbalancedState
            (Height (MaxKeyDelete ('ForkTree ll (Node ln la) lr)))
            (1 + If (Height rl <=? Height rr) (Height rr) (Height rl))))
      n
    :~: 'True)
-> GtN
     (Balance'
        ('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))
        (UnbalancedState
           (Height (MaxKeyDelete ('ForkTree ll (Node ln la) lr)))
           (1 + If (Height rl <=? Height rr) (Height rr) (Height rl))))
     n
   :~: '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
lIsBST Proxy n
pn) (((CmpNat (MaxKey ('ForkTree ll (Node ln la) lr)) n ~ 'GT) =>
  GtN
    (Balance'
       ('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))
       (UnbalancedState
          (Height (MaxKeyDelete ('ForkTree ll (Node ln la) lr)))
          (1 + If (Height rl <=? Height rr) (Height rr) (Height rl))))
    n
  :~: 'True)
 -> GtN
      (Balance'
         ('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))
         (UnbalancedState
            (Height (MaxKeyDelete ('ForkTree ll (Node ln la) lr)))
            (1 + If (Height rl <=? Height rr) (Height rr) (Height rl))))
      n
    :~: 'True)
-> ((CmpNat (MaxKey ('ForkTree ll (Node ln la) lr)) n ~ 'GT) =>
    GtN
      (Balance'
         ('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))
         (UnbalancedState
            (Height (MaxKeyDelete ('ForkTree ll (Node ln la) lr)))
            (1 + If (Height rl <=? Height rr) (Height rr) (Height rl))))
      n
    :~: 'True)
-> GtN
     (Balance'
        ('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))
        (UnbalancedState
           (Height (MaxKeyDelete ('ForkTree ll (Node ln la) lr)))
           (1 + If (Height rl <=? Height rr) (Height rr) (Height rl))))
     n
   :~: 'True
forall a b. (a -> b) -> a -> b
$
        (GtN
   (Balance'
      ('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))
      (UnbalancedState
         (Height (MaxKeyDelete ('ForkTree ll (Node ln la) lr)))
         (1 + If (Height rl <=? Height rr) (Height rr) (Height rl))))
   n
 :~: 'True)
-> ((GtN
       (Balance'
          ('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))
          (UnbalancedState
             (Height (MaxKeyDelete ('ForkTree ll (Node ln la) lr)))
             (1 + If (Height rl <=? Height rr) (Height rr) (Height rl))))
       n
     ~ 'True) =>
    GtN
      (Balance'
         ('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))
         (UnbalancedState
            (Height (MaxKeyDelete ('ForkTree ll (Node ln la) lr)))
            (1 + If (Height rl <=? Height rr) (Height rr) (Height rl))))
      n
    :~: 'True)
-> GtN
     (Balance'
        ('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))
        (UnbalancedState
           (Height (MaxKeyDelete ('ForkTree ll (Node ln la) lr)))
           (1 + If (Height rl <=? Height rr) (Height rr) (Height rl))))
     n
   :~: 'True
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (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)
-> Proxy n
-> GtN
     (Balance
        ('ForkTree
           (MaxKeyDelete ('ForkTree ll (Node ln la) lr))
           (Node
              (MaxKey ('ForkTree ll (Node ln la) lr))
              (MaxValue ('ForkTree ll (Node ln la) lr)))
           r))
     n
   :~: 'True
forall (t :: Tree) (n :: Nat).
(ProofGtNBalance t n, GtN t n ~ 'True) =>
IsBSTT t -> Proxy n -> GtN (Balance t) n :~: 'True
proofGtNBalance (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) (a :: Tree) r.
(LtN l n ~ 'True, GtN a n ~ 'True) =>
IsBSTT l
-> Proxy (Node n r)
-> IsBSTT a
-> IsBSTT ('ForkTree l (Node n r) a)
ForkIsBSTT IsBSTT (MaxKeyDelete l)
IsBSTT (MaxKeyDelete ('ForkTree ll (Node ln la) lr))
lIsBST' 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
rIsBST) Proxy n
pn) (GtN
   (Balance'
      ('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))
      (UnbalancedState
         (Height (MaxKeyDelete ('ForkTree ll (Node ln la) lr)))
         (1 + If (Height rl <=? Height rr) (Height rr) (Height rl))))
   n
 ~ 'True) =>
GtN
  (Balance'
     ('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))
     (UnbalancedState
        (Height (MaxKeyDelete ('ForkTree ll (Node ln la) lr)))
        (1 + If (Height rl <=? Height rr) (Height rr) (Height rl))))
  n
:~: 'True
forall {k} (a :: k). a :~: a
Refl
    where
      lIsBST' :: IsBSTT (MaxKeyDelete l)
lIsBST' = IsBSTT l -> IsBSTT (MaxKeyDelete l)
forall (t :: Tree).
ProofMaxKeyDeleteIsBST t =>
IsBSTT t -> IsBSTT (MaxKeyDelete t)
proofMaxKeyDeleteIsBST IsBSTT l
lIsBST
      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 ProofGtNDelete' x ('ForkTree 'EmptyTree (Node n1 a1) r) n 'LT where
  proofGtNDelete' :: (CmpNat x n ~ 'GT,
 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,
    CmpNat x n1 ~ 'LT,
    GtN l n ~ 'True,
    GtN r n ~ 'True,
    ProofLtNDelete' x l n1 o,
    ProofGtNDelete' x l n o,
    ProofIsBSTDelete x l,
    ProofGtNBalance ('ForkTree (Delete' x l o) (Node n1 a1) r) n
  ) =>
  ProofGtNDelete' x ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a1) r) n 'LT
  where
  proofGtNDelete' :: (CmpNat x n ~ 'GT,
 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
lIsBST Proxy (Node n a)
node IsBSTT r
rIsBST) 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) =>
    GtN
      (Balance'
         ('ForkTree
            (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n1 a1) r)
         (UnbalancedState
            (Height (Delete' x ('ForkTree ll (Node ln la) lr) o)) (Height r)))
      n
    :~: 'True)
-> GtN
     (Balance'
        ('ForkTree
           (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n1 a1) r)
        (UnbalancedState
           (Height (Delete' x ('ForkTree ll (Node ln la) lr) o)) (Height r)))
     n
   :~: '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, CmpNat x n ~ 'GT, 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
lIsBST Proxy n
pn Proxy o
po) (((GtN (Delete' x ('ForkTree ll (Node ln la) lr) o) n ~ 'True) =>
  GtN
    (Balance'
       ('ForkTree
          (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n1 a1) r)
       (UnbalancedState
          (Height (Delete' x ('ForkTree ll (Node ln la) lr) o)) (Height r)))
    n
  :~: 'True)
 -> GtN
      (Balance'
         ('ForkTree
            (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n1 a1) r)
         (UnbalancedState
            (Height (Delete' x ('ForkTree ll (Node ln la) lr) o)) (Height r)))
      n
    :~: 'True)
-> ((GtN (Delete' x ('ForkTree ll (Node ln la) lr) o) n ~ 'True) =>
    GtN
      (Balance'
         ('ForkTree
            (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n1 a1) r)
         (UnbalancedState
            (Height (Delete' x ('ForkTree ll (Node ln la) lr) o)) (Height r)))
      n
    :~: 'True)
-> GtN
     (Balance'
        ('ForkTree
           (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n1 a1) r)
        (UnbalancedState
           (Height (Delete' x ('ForkTree ll (Node ln la) lr) o)) (Height r)))
     n
   :~: 'True
forall a b. (a -> b) -> a -> b
$
      (LtN (Delete' x ('ForkTree ll (Node ln la) lr) o) n1 :~: 'True)
-> ((LtN (Delete' x ('ForkTree ll (Node ln la) lr) o) n1
     ~ 'True) =>
    GtN
      (Balance'
         ('ForkTree
            (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n1 a1) r)
         (UnbalancedState
            (Height (Delete' x ('ForkTree ll (Node ln la) lr) o)) (Height r)))
      n
    :~: 'True)
-> GtN
     (Balance'
        ('ForkTree
           (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n1 a1) r)
        (UnbalancedState
           (Height (Delete' x ('ForkTree ll (Node ln la) lr) o)) (Height r)))
     n
   :~: 'True
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (Proxy x
-> IsBSTT l
-> Proxy n1
-> Proxy o
-> LtN (Delete' x l o) n1 :~: 'True
forall (x :: Nat) (t :: Tree) (n :: Nat) (o :: Ordering).
(ProofLtNDelete' x t n o, CmpNat x n ~ 'LT, 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
lIsBST (Proxy n1
forall {k} (t :: k). Proxy t
Proxy :: Proxy n1) Proxy o
po) (((LtN (Delete' x ('ForkTree ll (Node ln la) lr) o) n1 ~ 'True) =>
  GtN
    (Balance'
       ('ForkTree
          (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n1 a1) r)
       (UnbalancedState
          (Height (Delete' x ('ForkTree ll (Node ln la) lr) o)) (Height r)))
    n
  :~: 'True)
 -> GtN
      (Balance'
         ('ForkTree
            (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n1 a1) r)
         (UnbalancedState
            (Height (Delete' x ('ForkTree ll (Node ln la) lr) o)) (Height r)))
      n
    :~: 'True)
-> ((LtN (Delete' x ('ForkTree ll (Node ln la) lr) o) n1
     ~ 'True) =>
    GtN
      (Balance'
         ('ForkTree
            (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n1 a1) r)
         (UnbalancedState
            (Height (Delete' x ('ForkTree ll (Node ln la) lr) o)) (Height r)))
      n
    :~: 'True)
-> GtN
     (Balance'
        ('ForkTree
           (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n1 a1) r)
        (UnbalancedState
           (Height (Delete' x ('ForkTree ll (Node ln la) lr) o)) (Height r)))
     n
   :~: 'True
forall a b. (a -> b) -> a -> b
$
        (GtN
   (Balance'
      ('ForkTree
         (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n1 a1) r)
      (UnbalancedState
         (Height (Delete' x ('ForkTree ll (Node ln la) lr) o)) (Height r)))
   n
 :~: 'True)
-> ((GtN
       (Balance'
          ('ForkTree
             (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n1 a1) r)
          (UnbalancedState
             (Height (Delete' x ('ForkTree ll (Node ln la) lr) o)) (Height r)))
       n
     ~ 'True) =>
    GtN
      (Balance'
         ('ForkTree
            (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n1 a1) r)
         (UnbalancedState
            (Height (Delete' x ('ForkTree ll (Node ln la) lr) o)) (Height r)))
      n
    :~: 'True)
-> GtN
     (Balance'
        ('ForkTree
           (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n1 a1) r)
        (UnbalancedState
           (Height (Delete' x ('ForkTree ll (Node ln la) lr) o)) (Height r)))
     n
   :~: 'True
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (IsBSTT
  ('ForkTree
     (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n a) r)
-> Proxy n
-> GtN
     (Balance
        ('ForkTree
           (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n a) r))
     n
   :~: 'True
forall (t :: Tree) (n :: Nat).
(ProofGtNBalance t n, GtN t n ~ 'True) =>
IsBSTT t -> Proxy n -> GtN (Balance t) n :~: 'True
proofGtNBalance (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) (a :: Tree) r.
(LtN l n ~ 'True, GtN a n ~ 'True) =>
IsBSTT l
-> Proxy (Node n r)
-> IsBSTT a
-> IsBSTT ('ForkTree l (Node n r) a)
ForkIsBSTT IsBSTT (Delete' x ('ForkTree ll (Node ln la) lr) o)
IsBSTT (Delete x l)
lIsBST' Proxy (Node n a)
node IsBSTT r
rIsBST) Proxy n
pn) (GtN
   (Balance'
      ('ForkTree
         (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n1 a1) r)
      (UnbalancedState
         (Height (Delete' x ('ForkTree ll (Node ln la) lr) o)) (Height r)))
   n
 ~ 'True) =>
GtN
  (Balance'
     ('ForkTree
        (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n1 a1) r)
     (UnbalancedState
        (Height (Delete' x ('ForkTree ll (Node ln la) lr) o)) (Height r)))
  n
:~: 'True
forall {k} (a :: k). a :~: a
Refl
    where
      po :: Proxy o
po = Proxy o
forall {k} (t :: k). Proxy t
Proxy :: Proxy o
      lIsBST' :: IsBSTT (Delete x l)
lIsBST' = Proxy x -> IsBSTT l -> IsBSTT (Delete x l)
forall (x :: Nat) (t :: Tree).
ProofIsBSTDelete x t =>
Proxy x -> IsBSTT t -> IsBSTT (Delete x t)
proofIsBSTDelete Proxy x
px IsBSTT l
lIsBST

instance ProofGtNDelete' x ('ForkTree l (Node n1 a1) 'EmptyTree) n 'GT where
  proofGtNDelete' :: (CmpNat x n ~ 'GT,
 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,
    CmpNat x n1 ~ 'GT,
    GtN r n ~ 'True,
    ProofGtNDelete' x r n o,
    ProofGtNDelete' x r n1 o,
    ProofIsBSTDelete x r,
    ProofGtNBalance ('ForkTree l (Node n1 a1) (Delete' x r o)) n
  ) =>
  ProofGtNDelete' x ('ForkTree l (Node n1 a1) ('ForkTree rl (Node rn ra) rr)) n 'GT
  where
  proofGtNDelete' :: (CmpNat x n ~ 'GT,
 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
lIsBST Proxy (Node n a)
node IsBSTT r
rIsBST) 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) =>
    GtN
      (Balance'
         ('ForkTree
            l (Node n1 a1) (Delete' x ('ForkTree rl (Node rn ra) rr) o))
         (UnbalancedState
            (Height l) (Height (Delete' x ('ForkTree rl (Node rn ra) rr) o))))
      n
    :~: 'True)
-> GtN
     (Balance'
        ('ForkTree
           l (Node n1 a1) (Delete' x ('ForkTree rl (Node rn ra) rr) o))
        (UnbalancedState
           (Height l) (Height (Delete' x ('ForkTree rl (Node rn ra) rr) o))))
     n
   :~: '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, CmpNat x n ~ 'GT, 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
rIsBST Proxy n
pn Proxy o
po) (((GtN (Delete' x ('ForkTree rl (Node rn ra) rr) o) n ~ 'True) =>
  GtN
    (Balance'
       ('ForkTree
          l (Node n1 a1) (Delete' x ('ForkTree rl (Node rn ra) rr) o))
       (UnbalancedState
          (Height l) (Height (Delete' x ('ForkTree rl (Node rn ra) rr) o))))
    n
  :~: 'True)
 -> GtN
      (Balance'
         ('ForkTree
            l (Node n1 a1) (Delete' x ('ForkTree rl (Node rn ra) rr) o))
         (UnbalancedState
            (Height l) (Height (Delete' x ('ForkTree rl (Node rn ra) rr) o))))
      n
    :~: 'True)
-> ((GtN (Delete' x ('ForkTree rl (Node rn ra) rr) o) n ~ 'True) =>
    GtN
      (Balance'
         ('ForkTree
            l (Node n1 a1) (Delete' x ('ForkTree rl (Node rn ra) rr) o))
         (UnbalancedState
            (Height l) (Height (Delete' x ('ForkTree rl (Node rn ra) rr) o))))
      n
    :~: 'True)
-> GtN
     (Balance'
        ('ForkTree
           l (Node n1 a1) (Delete' x ('ForkTree rl (Node rn ra) rr) o))
        (UnbalancedState
           (Height l) (Height (Delete' x ('ForkTree rl (Node rn ra) rr) o))))
     n
   :~: 'True
forall a b. (a -> b) -> a -> b
$
      (GtN (Delete' x ('ForkTree rl (Node rn ra) rr) o) n1 :~: 'True)
-> ((GtN (Delete' x ('ForkTree rl (Node rn ra) rr) o) n1
     ~ 'True) =>
    GtN
      (Balance'
         ('ForkTree
            l (Node n1 a1) (Delete' x ('ForkTree rl (Node rn ra) rr) o))
         (UnbalancedState
            (Height l) (Height (Delete' x ('ForkTree rl (Node rn ra) rr) o))))
      n
    :~: 'True)
-> GtN
     (Balance'
        ('ForkTree
           l (Node n1 a1) (Delete' x ('ForkTree rl (Node rn ra) rr) o))
        (UnbalancedState
           (Height l) (Height (Delete' x ('ForkTree rl (Node rn ra) rr) o))))
     n
   :~: 'True
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (Proxy x
-> IsBSTT r
-> Proxy n1
-> Proxy o
-> GtN (Delete' x r o) n1 :~: 'True
forall (x :: Nat) (t :: Tree) (n :: Nat) (o :: Ordering).
(ProofGtNDelete' x t n o, CmpNat x n ~ 'GT, 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
rIsBST (Proxy n1
forall {k} (t :: k). Proxy t
Proxy :: Proxy n1) Proxy o
po) (((GtN (Delete' x ('ForkTree rl (Node rn ra) rr) o) n1 ~ 'True) =>
  GtN
    (Balance'
       ('ForkTree
          l (Node n1 a1) (Delete' x ('ForkTree rl (Node rn ra) rr) o))
       (UnbalancedState
          (Height l) (Height (Delete' x ('ForkTree rl (Node rn ra) rr) o))))
    n
  :~: 'True)
 -> GtN
      (Balance'
         ('ForkTree
            l (Node n1 a1) (Delete' x ('ForkTree rl (Node rn ra) rr) o))
         (UnbalancedState
            (Height l) (Height (Delete' x ('ForkTree rl (Node rn ra) rr) o))))
      n
    :~: 'True)
-> ((GtN (Delete' x ('ForkTree rl (Node rn ra) rr) o) n1
     ~ 'True) =>
    GtN
      (Balance'
         ('ForkTree
            l (Node n1 a1) (Delete' x ('ForkTree rl (Node rn ra) rr) o))
         (UnbalancedState
            (Height l) (Height (Delete' x ('ForkTree rl (Node rn ra) rr) o))))
      n
    :~: 'True)
-> GtN
     (Balance'
        ('ForkTree
           l (Node n1 a1) (Delete' x ('ForkTree rl (Node rn ra) rr) o))
        (UnbalancedState
           (Height l) (Height (Delete' x ('ForkTree rl (Node rn ra) rr) o))))
     n
   :~: 'True
forall a b. (a -> b) -> a -> b
$
        (GtN
   (Balance'
      ('ForkTree
         l (Node n1 a1) (Delete' x ('ForkTree rl (Node rn ra) rr) o))
      (UnbalancedState
         (Height l) (Height (Delete' x ('ForkTree rl (Node rn ra) rr) o))))
   n
 :~: 'True)
-> ((GtN
       (Balance'
          ('ForkTree
             l (Node n1 a1) (Delete' x ('ForkTree rl (Node rn ra) rr) o))
          (UnbalancedState
             (Height l) (Height (Delete' x ('ForkTree rl (Node rn ra) rr) o))))
       n
     ~ 'True) =>
    GtN
      (Balance'
         ('ForkTree
            l (Node n1 a1) (Delete' x ('ForkTree rl (Node rn ra) rr) o))
         (UnbalancedState
            (Height l) (Height (Delete' x ('ForkTree rl (Node rn ra) rr) o))))
      n
    :~: 'True)
-> GtN
     (Balance'
        ('ForkTree
           l (Node n1 a1) (Delete' x ('ForkTree rl (Node rn ra) rr) o))
        (UnbalancedState
           (Height l) (Height (Delete' x ('ForkTree rl (Node rn ra) rr) o))))
     n
   :~: 'True
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (IsBSTT
  ('ForkTree
     l (Node n a) (Delete' x ('ForkTree rl (Node rn ra) rr) o))
-> Proxy n
-> GtN
     (Balance
        ('ForkTree
           l (Node n a) (Delete' x ('ForkTree rl (Node rn ra) rr) o)))
     n
   :~: 'True
forall (t :: Tree) (n :: Nat).
(ProofGtNBalance t n, GtN t n ~ 'True) =>
IsBSTT t -> Proxy n -> GtN (Balance t) n :~: 'True
proofGtNBalance (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) (a :: Tree) r.
(LtN l n ~ 'True, GtN a n ~ 'True) =>
IsBSTT l
-> Proxy (Node n r)
-> IsBSTT a
-> IsBSTT ('ForkTree l (Node n r) a)
ForkIsBSTT IsBSTT l
lIsBST Proxy (Node n a)
node IsBSTT (Delete' x ('ForkTree rl (Node rn ra) rr) o)
IsBSTT (Delete x r)
rIsBST') Proxy n
pn) (GtN
   (Balance'
      ('ForkTree
         l (Node n1 a1) (Delete' x ('ForkTree rl (Node rn ra) rr) o))
      (UnbalancedState
         (Height l) (Height (Delete' x ('ForkTree rl (Node rn ra) rr) o))))
   n
 ~ 'True) =>
GtN
  (Balance'
     ('ForkTree
        l (Node n1 a1) (Delete' x ('ForkTree rl (Node rn ra) rr) o))
     (UnbalancedState
        (Height l) (Height (Delete' x ('ForkTree rl (Node rn ra) rr) o))))
  n
:~: 'True
forall {k} (a :: k). a :~: a
Refl
    where
      po :: Proxy o
po = Proxy o
forall {k} (t :: k). Proxy t
Proxy :: Proxy o
      rIsBST' :: IsBSTT (Delete x r)
rIsBST' = Proxy x -> IsBSTT r -> IsBSTT (Delete x r)
forall (x :: Nat) (t :: Tree).
ProofIsBSTDelete x t =>
Proxy x -> IsBSTT t -> IsBSTT (Delete x t)
proofIsBSTDelete Proxy x
px IsBSTT r
rIsBST

-- | 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 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,
    MaxKeyDeletable r,
    ProofGtNMaxKeyDelete r n,
    ProofMaxKeyDeleteIsBST r,
    ProofIsBSTBalance ('ForkTree l (Node n a) (MaxKeyDelete r))
  ) =>
  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
lIsBST Proxy (Node n a)
node IsBSTT r
rIsBST) =
    (GtN (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)) n :~: 'True)
-> ((GtN (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)) n
     ~ 'True) =>
    IsBSTT
      (Balance'
         ('ForkTree
            ('ForkTree ll (Node ln la) lr)
            (Node n a)
            (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
         (UnbalancedState
            (1 + If (Height ll <=? Height lr) (Height lr) (Height ll))
            (Height (MaxKeyDelete ('ForkTree rl (Node rn ra) rr))))))
-> IsBSTT
     (Balance'
        ('ForkTree
           ('ForkTree ll (Node ln la) lr)
           (Node n a)
           (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
        (UnbalancedState
           (1 + If (Height ll <=? Height lr) (Height lr) (Height ll))
           (Height (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, MaxKeyDeletable t, GtN t n ~ 'True) =>
IsBSTT t -> Proxy n -> GtN (MaxKeyDelete t) n :~: 'True
proofGtNMaxKeyDelete IsBSTT r
rIsBST (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)) (((GtN (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)) n ~ 'True) =>
  IsBSTT
    (Balance'
       ('ForkTree
          ('ForkTree ll (Node ln la) lr)
          (Node n a)
          (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
       (UnbalancedState
          (1 + If (Height ll <=? Height lr) (Height lr) (Height ll))
          (Height (MaxKeyDelete ('ForkTree rl (Node rn ra) rr))))))
 -> IsBSTT
      (Balance'
         ('ForkTree
            ('ForkTree ll (Node ln la) lr)
            (Node n a)
            (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
         (UnbalancedState
            (1 + If (Height ll <=? Height lr) (Height lr) (Height ll))
            (Height (MaxKeyDelete ('ForkTree rl (Node rn ra) rr))))))
-> ((GtN (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)) n
     ~ 'True) =>
    IsBSTT
      (Balance'
         ('ForkTree
            ('ForkTree ll (Node ln la) lr)
            (Node n a)
            (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
         (UnbalancedState
            (1 + If (Height ll <=? Height lr) (Height lr) (Height ll))
            (Height (MaxKeyDelete ('ForkTree rl (Node rn ra) rr))))))
-> IsBSTT
     (Balance'
        ('ForkTree
           ('ForkTree ll (Node ln la) lr)
           (Node n a)
           (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
        (UnbalancedState
           (1 + If (Height ll <=? Height lr) (Height lr) (Height ll))
           (Height (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))))
forall a b. (a -> b) -> a -> b
$
      IsBSTT
  ('ForkTree
     l (Node n a) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
-> IsBSTT
     (Balance
        ('ForkTree
           l (Node n a) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr))))
forall (t :: Tree).
ProofIsBSTBalance t =>
IsBSTT t -> IsBSTT (Balance t)
proofIsBSTBalance (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) (a :: Tree) r.
(LtN l n ~ 'True, GtN a n ~ 'True) =>
IsBSTT l
-> Proxy (Node n r)
-> IsBSTT a
-> IsBSTT ('ForkTree l (Node n r) a)
ForkIsBSTT IsBSTT l
lIsBST Proxy (Node n a)
node IsBSTT (MaxKeyDelete r)
IsBSTT (MaxKeyDelete ('ForkTree rl (Node rn ra) rr))
rIsBST')
    where
      rIsBST' :: IsBSTT (MaxKeyDelete r)
rIsBST' = IsBSTT r -> IsBSTT (MaxKeyDelete r)
forall (t :: Tree).
ProofMaxKeyDeleteIsBST t =>
IsBSTT t -> IsBSTT (MaxKeyDelete t)
proofMaxKeyDeleteIsBST IsBSTT r
rIsBST

-- | 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.AVL.Extern.Delete.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
rIsBST) 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
rIsBST 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.AVL.Extern.Delete.delete` operation.
class ProofGtNMaxKeyDelete (t :: Tree) (n :: Nat) where
  proofGtNMaxKeyDelete ::
    (MaxKeyDeletable t, 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 :: (MaxKeyDeletable ('ForkTree l (Node n1 a) 'EmptyTree),
 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 l n ~ 'True,
    GtN r n ~ 'True,
    MaxKeyDeletable r,
    ProofGtNMaxKeyDelete r n,
    ProofGtNMaxKeyDelete r n1,
    ProofMaxKeyDeleteIsBST r,
    ProofGtNBalance ('ForkTree l (Node n1 a) (MaxKeyDelete r)) n
  ) =>
  ProofGtNMaxKeyDelete ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr)) n
  where
  proofGtNMaxKeyDelete :: (MaxKeyDeletable
   ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr)),
 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
lIsBST Proxy (Node n a)
node IsBSTT r
rIsBST) Proxy n
pn =
    (GtN (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)) n :~: 'True)
-> ((GtN (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)) n
     ~ 'True) =>
    GtN
      (Balance'
         ('ForkTree
            l (Node n1 a) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
         (UnbalancedState
            (Height l) (Height (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))))
      n
    :~: 'True)
-> GtN
     (Balance'
        ('ForkTree
           l (Node n1 a) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
        (UnbalancedState
           (Height l) (Height (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))))
     n
   :~: '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, MaxKeyDeletable t, GtN t n ~ 'True) =>
IsBSTT t -> Proxy n -> GtN (MaxKeyDelete t) n :~: 'True
proofGtNMaxKeyDelete IsBSTT r
rIsBST Proxy n
pn) (((GtN (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)) n ~ 'True) =>
  GtN
    (Balance'
       ('ForkTree
          l (Node n1 a) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
       (UnbalancedState
          (Height l) (Height (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))))
    n
  :~: 'True)
 -> GtN
      (Balance'
         ('ForkTree
            l (Node n1 a) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
         (UnbalancedState
            (Height l) (Height (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))))
      n
    :~: 'True)
-> ((GtN (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)) n
     ~ 'True) =>
    GtN
      (Balance'
         ('ForkTree
            l (Node n1 a) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
         (UnbalancedState
            (Height l) (Height (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))))
      n
    :~: 'True)
-> GtN
     (Balance'
        ('ForkTree
           l (Node n1 a) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
        (UnbalancedState
           (Height l) (Height (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))))
     n
   :~: 'True
forall a b. (a -> b) -> a -> b
$
      (GtN (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)) n1 :~: 'True)
-> ((GtN (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)) n1
     ~ 'True) =>
    GtN
      (Balance'
         ('ForkTree
            l (Node n1 a) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
         (UnbalancedState
            (Height l) (Height (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))))
      n
    :~: 'True)
-> GtN
     (Balance'
        ('ForkTree
           l (Node n1 a) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
        (UnbalancedState
           (Height l) (Height (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))))
     n
   :~: 'True
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (IsBSTT r -> Proxy n1 -> GtN (MaxKeyDelete r) n1 :~: 'True
forall (t :: Tree) (n :: Nat).
(ProofGtNMaxKeyDelete t n, MaxKeyDeletable t, GtN t n ~ 'True) =>
IsBSTT t -> Proxy n -> GtN (MaxKeyDelete t) n :~: 'True
proofGtNMaxKeyDelete IsBSTT r
rIsBST (Proxy n1
forall {k} (t :: k). Proxy t
Proxy :: Proxy n1)) (((GtN (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)) n1 ~ 'True) =>
  GtN
    (Balance'
       ('ForkTree
          l (Node n1 a) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
       (UnbalancedState
          (Height l) (Height (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))))
    n
  :~: 'True)
 -> GtN
      (Balance'
         ('ForkTree
            l (Node n1 a) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
         (UnbalancedState
            (Height l) (Height (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))))
      n
    :~: 'True)
-> ((GtN (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)) n1
     ~ 'True) =>
    GtN
      (Balance'
         ('ForkTree
            l (Node n1 a) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
         (UnbalancedState
            (Height l) (Height (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))))
      n
    :~: 'True)
-> GtN
     (Balance'
        ('ForkTree
           l (Node n1 a) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
        (UnbalancedState
           (Height l) (Height (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))))
     n
   :~: 'True
forall a b. (a -> b) -> a -> b
$
        (GtN
   (Balance'
      ('ForkTree
         l (Node n1 a) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
      (UnbalancedState
         (Height l) (Height (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))))
   n
 :~: 'True)
-> ((GtN
       (Balance'
          ('ForkTree
             l (Node n1 a) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
          (UnbalancedState
             (Height l) (Height (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))))
       n
     ~ 'True) =>
    GtN
      (Balance'
         ('ForkTree
            l (Node n1 a) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
         (UnbalancedState
            (Height l) (Height (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))))
      n
    :~: 'True)
-> GtN
     (Balance'
        ('ForkTree
           l (Node n1 a) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
        (UnbalancedState
           (Height l) (Height (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))))
     n
   :~: 'True
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (IsBSTT
  ('ForkTree
     l (Node n a) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
-> Proxy n
-> GtN
     (Balance
        ('ForkTree
           l (Node n a) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr))))
     n
   :~: 'True
forall (t :: Tree) (n :: Nat).
(ProofGtNBalance t n, GtN t n ~ 'True) =>
IsBSTT t -> Proxy n -> GtN (Balance t) n :~: 'True
proofGtNBalance (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) (a :: Tree) r.
(LtN l n ~ 'True, GtN a n ~ 'True) =>
IsBSTT l
-> Proxy (Node n r)
-> IsBSTT a
-> IsBSTT ('ForkTree l (Node n r) a)
ForkIsBSTT IsBSTT l
lIsBST Proxy (Node n a)
node IsBSTT (MaxKeyDelete r)
IsBSTT (MaxKeyDelete ('ForkTree rl (Node rn ra) rr))
rIsBST') Proxy n
pn) (GtN
   (Balance'
      ('ForkTree
         l (Node n1 a) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
      (UnbalancedState
         (Height l) (Height (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))))
   n
 ~ 'True) =>
GtN
  (Balance'
     ('ForkTree
        l (Node n1 a) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
     (UnbalancedState
        (Height l) (Height (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))))
  n
:~: 'True
forall {k} (a :: k). a :~: a
Refl
    where
      rIsBST' :: IsBSTT (MaxKeyDelete r)
rIsBST' = IsBSTT r -> IsBSTT (MaxKeyDelete r)
forall (t :: Tree).
ProofMaxKeyDeleteIsBST t =>
IsBSTT t -> IsBSTT (MaxKeyDelete t)
proofMaxKeyDeleteIsBST IsBSTT r
rIsBST

-- | 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.AVL.Extern.Delete.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
rIsBST) 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
rIsBST 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.AVL.Extern.Delete.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,
    MaxKeyDeletable r,
    ProofGtNMaxKeyDelete r n1,
    ProofMaxKeyDeleteIsBST r,
    ProofLtNMaxKeyDelete r n,
    ProofLtNBalance ('ForkTree l (Node n1 a) (MaxKeyDelete 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
lIsBST Proxy (Node n a)
node IsBSTT r
rIsBST) Proxy n
pn =
    (LtN (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)) n :~: 'True)
-> ((LtN (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)) n
     ~ 'True) =>
    LtN
      (Balance'
         ('ForkTree
            l (Node n1 a) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
         (UnbalancedState
            (Height l) (Height (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))))
      n
    :~: 'True)
-> LtN
     (Balance'
        ('ForkTree
           l (Node n1 a) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
        (UnbalancedState
           (Height l) (Height (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))))
     n
   :~: '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
rIsBST Proxy n
pn) (((LtN (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)) n ~ 'True) =>
  LtN
    (Balance'
       ('ForkTree
          l (Node n1 a) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
       (UnbalancedState
          (Height l) (Height (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))))
    n
  :~: 'True)
 -> LtN
      (Balance'
         ('ForkTree
            l (Node n1 a) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
         (UnbalancedState
            (Height l) (Height (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))))
      n
    :~: 'True)
-> ((LtN (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)) n
     ~ 'True) =>
    LtN
      (Balance'
         ('ForkTree
            l (Node n1 a) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
         (UnbalancedState
            (Height l) (Height (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))))
      n
    :~: 'True)
-> LtN
     (Balance'
        ('ForkTree
           l (Node n1 a) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
        (UnbalancedState
           (Height l) (Height (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))))
     n
   :~: 'True
forall a b. (a -> b) -> a -> b
$
      (GtN (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)) n1 :~: 'True)
-> ((GtN (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)) n1
     ~ 'True) =>
    LtN
      (Balance'
         ('ForkTree
            l (Node n1 a) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
         (UnbalancedState
            (Height l) (Height (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))))
      n
    :~: 'True)
-> LtN
     (Balance'
        ('ForkTree
           l (Node n1 a) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
        (UnbalancedState
           (Height l) (Height (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))))
     n
   :~: 'True
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (IsBSTT r -> Proxy n1 -> GtN (MaxKeyDelete r) n1 :~: 'True
forall (t :: Tree) (n :: Nat).
(ProofGtNMaxKeyDelete t n, MaxKeyDeletable t, GtN t n ~ 'True) =>
IsBSTT t -> Proxy n -> GtN (MaxKeyDelete t) n :~: 'True
proofGtNMaxKeyDelete IsBSTT r
rIsBST (Proxy n1
forall {k} (t :: k). Proxy t
Proxy :: Proxy n1)) (((GtN (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)) n1 ~ 'True) =>
  LtN
    (Balance'
       ('ForkTree
          l (Node n1 a) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
       (UnbalancedState
          (Height l) (Height (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))))
    n
  :~: 'True)
 -> LtN
      (Balance'
         ('ForkTree
            l (Node n1 a) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
         (UnbalancedState
            (Height l) (Height (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))))
      n
    :~: 'True)
-> ((GtN (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)) n1
     ~ 'True) =>
    LtN
      (Balance'
         ('ForkTree
            l (Node n1 a) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
         (UnbalancedState
            (Height l) (Height (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))))
      n
    :~: 'True)
-> LtN
     (Balance'
        ('ForkTree
           l (Node n1 a) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
        (UnbalancedState
           (Height l) (Height (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))))
     n
   :~: 'True
forall a b. (a -> b) -> a -> b
$
        (LtN
   (Balance'
      ('ForkTree
         l (Node n1 a) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
      (UnbalancedState
         (Height l) (Height (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))))
   n
 :~: 'True)
-> ((LtN
       (Balance'
          ('ForkTree
             l (Node n1 a) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
          (UnbalancedState
             (Height l) (Height (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))))
       n
     ~ 'True) =>
    LtN
      (Balance'
         ('ForkTree
            l (Node n1 a) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
         (UnbalancedState
            (Height l) (Height (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))))
      n
    :~: 'True)
-> LtN
     (Balance'
        ('ForkTree
           l (Node n1 a) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
        (UnbalancedState
           (Height l) (Height (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))))
     n
   :~: 'True
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (IsBSTT
  ('ForkTree
     l (Node n a) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
-> Proxy n
-> LtN
     (Balance
        ('ForkTree
           l (Node n a) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr))))
     n
   :~: 'True
forall (t :: Tree) (n :: Nat).
(ProofLtNBalance t n, LtN t n ~ 'True) =>
IsBSTT t -> Proxy n -> LtN (Balance t) n :~: 'True
proofLtNBalance (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) (a :: Tree) r.
(LtN l n ~ 'True, GtN a n ~ 'True) =>
IsBSTT l
-> Proxy (Node n r)
-> IsBSTT a
-> IsBSTT ('ForkTree l (Node n r) a)
ForkIsBSTT IsBSTT l
lIsBST Proxy (Node n a)
node IsBSTT (MaxKeyDelete r)
IsBSTT (MaxKeyDelete ('ForkTree rl (Node rn ra) rr))
rIsBST') Proxy n
pn) (LtN
   (Balance'
      ('ForkTree
         l (Node n1 a) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
      (UnbalancedState
         (Height l) (Height (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))))
   n
 ~ 'True) =>
LtN
  (Balance'
     ('ForkTree
        l (Node n1 a) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
     (UnbalancedState
        (Height l) (Height (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))))
  n
:~: 'True
forall {k} (a :: k). a :~: a
Refl
    where
      rIsBST' :: IsBSTT (MaxKeyDelete r)
rIsBST' = IsBSTT r -> IsBSTT (MaxKeyDelete r)
forall (t :: Tree).
ProofMaxKeyDeleteIsBST t =>
IsBSTT t -> IsBSTT (MaxKeyDelete t)
proofMaxKeyDeleteIsBST IsBSTT r
rIsBST

-- | Prove that deleting the node with maximum key value
-- in an `Data.Tree.AVL.Extern.Constructors.AVL` @t@ preserves the @AVL@ restrictions.
-- This proof is needed for the `Data.Tree.AVL.Extern.Delete.delete` operation.
class ProofMaxKeyDeleteIsBalanced (t :: Tree) where
  proofMaxKeyDeleteIsBalanced :: IsBalancedT t -> IsBalancedT (MaxKeyDelete t)

instance ProofMaxKeyDeleteIsBalanced 'EmptyTree where
  proofMaxKeyDeleteIsBalanced :: IsBalancedT 'EmptyTree -> IsBalancedT (MaxKeyDelete 'EmptyTree)
proofMaxKeyDeleteIsBalanced IsBalancedT 'EmptyTree
_ = IsBalancedT 'EmptyTree
IsBalancedT (MaxKeyDelete 'EmptyTree)
EmptyIsBalancedT

instance ProofMaxKeyDeleteIsBalanced ('ForkTree 'EmptyTree (Node n a) 'EmptyTree) where
  proofMaxKeyDeleteIsBalanced :: IsBalancedT ('ForkTree 'EmptyTree (Node n a) 'EmptyTree)
-> IsBalancedT
     (MaxKeyDelete ('ForkTree 'EmptyTree (Node n a) 'EmptyTree))
proofMaxKeyDeleteIsBalanced IsBalancedT ('ForkTree 'EmptyTree (Node n a) 'EmptyTree)
_ = IsBalancedT 'EmptyTree
IsBalancedT
  (MaxKeyDelete ('ForkTree 'EmptyTree (Node n a) 'EmptyTree))
EmptyIsBalancedT

instance ProofMaxKeyDeleteIsBalanced ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a) 'EmptyTree) where
  proofMaxKeyDeleteIsBalanced :: IsBalancedT
  ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a) 'EmptyTree)
-> IsBalancedT
     (MaxKeyDelete
        ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a) 'EmptyTree))
proofMaxKeyDeleteIsBalanced (ForkIsBalancedT IsBalancedT l
lIsBalanced Proxy (Node n a)
_ IsBalancedT r
_) = IsBalancedT l
IsBalancedT
  (MaxKeyDelete
     ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a) 'EmptyTree))
lIsBalanced

instance
  ( l ~ 'ForkTree ll (Node ln la) lr,
    r ~ 'ForkTree rl (Node rn ra) rr,
    ProofMaxKeyDeleteIsBalanced r,
    ProofIsBalancedBalance ('ForkTree l (Node n a) (MaxKeyDelete r))
  ) =>
  ProofMaxKeyDeleteIsBalanced ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a) ('ForkTree rl (Node rn ra) rr))
  where
  proofMaxKeyDeleteIsBalanced :: IsBalancedT
  ('ForkTree
     ('ForkTree ll (Node ln la) lr)
     (Node n a)
     ('ForkTree rl (Node rn ra) rr))
-> IsBalancedT
     (MaxKeyDelete
        ('ForkTree
           ('ForkTree ll (Node ln la) lr)
           (Node n a)
           ('ForkTree rl (Node rn ra) rr)))
proofMaxKeyDeleteIsBalanced (ForkIsBalancedT IsBalancedT l
lIsBalanced Proxy (Node n a)
node IsBalancedT r
rIsBalanced) =
    IsAlmostBalancedT
  ('ForkTree
     l (Node n a) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
-> IsBalancedT
     (Balance
        ('ForkTree
           l (Node n a) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr))))
forall (t :: Tree).
ProofIsBalancedBalance t =>
IsAlmostBalancedT t -> IsBalancedT (Balance t)
proofIsBalancedBalance (IsAlmostBalancedT
   ('ForkTree
      l (Node n a) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
 -> IsBalancedT
      (Balance
         ('ForkTree
            l (Node n a) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))))
-> IsAlmostBalancedT
     ('ForkTree
        l (Node n a) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
-> IsBalancedT
     (Balance
        ('ForkTree
           l (Node n a) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr))))
forall a b. (a -> b) -> a -> b
$ IsBalancedT l
-> Proxy (Node n a)
-> IsBalancedT (MaxKeyDelete ('ForkTree rl (Node rn ra) rr))
-> IsAlmostBalancedT
     ('ForkTree
        l (Node n a) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
forall (l :: Tree) (n :: Nat) a (r :: Tree).
IsBalancedT l
-> Proxy (Node n a)
-> IsBalancedT r
-> IsAlmostBalancedT ('ForkTree l (Node n a) r)
ForkIsAlmostBalancedT IsBalancedT l
lIsBalanced Proxy (Node n a)
node (IsBalancedT r -> IsBalancedT (MaxKeyDelete r)
forall (t :: Tree).
ProofMaxKeyDeleteIsBalanced t =>
IsBalancedT t -> IsBalancedT (MaxKeyDelete t)
proofMaxKeyDeleteIsBalanced IsBalancedT r
rIsBalanced)

-- | Prove that deleting a node with key @x@
-- in an `Data.Tree.AVL.Extern.Constructors.AVL` tree preserves the @AVL@ condition.
class ProofIsBalancedDelete (x :: Nat) (t :: Tree) where
  proofIsBalancedDelete :: Proxy x -> IsBalancedT t -> IsBalancedT (Delete x t)

instance ProofIsBalancedDelete x 'EmptyTree where
  proofIsBalancedDelete :: Proxy x
-> IsBalancedT 'EmptyTree -> IsBalancedT (Delete x 'EmptyTree)
proofIsBalancedDelete Proxy x
_ IsBalancedT 'EmptyTree
_ = IsBalancedT 'EmptyTree
IsBalancedT (Delete x 'EmptyTree)
EmptyIsBalancedT

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

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

instance ProofIsBalancedDelete' x ('ForkTree 'EmptyTree (Node n a1) 'EmptyTree) 'EQ where
  proofIsBalancedDelete' :: Proxy x
-> IsBalancedT ('ForkTree 'EmptyTree (Node n a1) 'EmptyTree)
-> Proxy 'EQ
-> IsBalancedT
     (Delete' x ('ForkTree 'EmptyTree (Node n a1) 'EmptyTree) 'EQ)
proofIsBalancedDelete' Proxy x
_ IsBalancedT ('ForkTree 'EmptyTree (Node n a1) 'EmptyTree)
_ Proxy 'EQ
_ = IsBalancedT 'EmptyTree
IsBalancedT
  (Delete' x ('ForkTree 'EmptyTree (Node n a1) 'EmptyTree) 'EQ)
EmptyIsBalancedT

instance ProofIsBalancedDelete' x ('ForkTree 'EmptyTree (Node n a1) ('ForkTree rl (Node rn ra) rr)) 'EQ where
  proofIsBalancedDelete' :: Proxy x
-> IsBalancedT
     ('ForkTree 'EmptyTree (Node n a1) ('ForkTree rl (Node rn ra) rr))
-> Proxy 'EQ
-> IsBalancedT
     (Delete'
        x
        ('ForkTree 'EmptyTree (Node n a1) ('ForkTree rl (Node rn ra) rr))
        'EQ)
proofIsBalancedDelete' Proxy x
_ (ForkIsBalancedT IsBalancedT l
_ Proxy (Node n a)
_ IsBalancedT r
rIsBalanced) Proxy 'EQ
_ = IsBalancedT r
IsBalancedT
  (Delete'
     x
     ('ForkTree 'EmptyTree (Node n a1) ('ForkTree rl (Node rn ra) rr))
     'EQ)
rIsBalanced

instance ProofIsBalancedDelete' x ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a1) 'EmptyTree) 'EQ where
  proofIsBalancedDelete' :: Proxy x
-> IsBalancedT
     ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a1) 'EmptyTree)
-> Proxy 'EQ
-> IsBalancedT
     (Delete'
        x
        ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a1) 'EmptyTree)
        'EQ)
proofIsBalancedDelete' Proxy x
_ (ForkIsBalancedT IsBalancedT l
lIsBalanced Proxy (Node n a)
_ IsBalancedT r
_) Proxy 'EQ
_ = IsBalancedT l
IsBalancedT
  (Delete'
     x
     ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a1) 'EmptyTree)
     'EQ)
lIsBalanced

instance
  ( l ~ 'ForkTree ll (Node ln la) lr,
    r ~ 'ForkTree rl (Node rn ra) rr,
    ProofMaxKeyDeleteIsBalanced l,
    ProofIsBalancedBalance ('ForkTree (MaxKeyDelete l) (Node (MaxKey l) (MaxValue l)) r)
  ) =>
  ProofIsBalancedDelete' x ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a1) ('ForkTree rl (Node rn ra) rr)) 'EQ
  where
  proofIsBalancedDelete' :: Proxy x
-> IsBalancedT
     ('ForkTree
        ('ForkTree ll (Node ln la) lr)
        (Node n a1)
        ('ForkTree rl (Node rn ra) rr))
-> Proxy 'EQ
-> IsBalancedT
     (Delete'
        x
        ('ForkTree
           ('ForkTree ll (Node ln la) lr)
           (Node n a1)
           ('ForkTree rl (Node rn ra) rr))
        'EQ)
proofIsBalancedDelete' Proxy x
_ (ForkIsBalancedT IsBalancedT l
lIsBalanced Proxy (Node n a)
_ IsBalancedT r
rIsBalanced) Proxy 'EQ
_ =
    IsAlmostBalancedT
  ('ForkTree
     (MaxKeyDelete ('ForkTree ll (Node ln la) lr))
     (Node
        (MaxKey ('ForkTree ll (Node ln la) lr))
        (MaxValue ('ForkTree ll (Node ln la) lr)))
     r)
-> IsBalancedT
     (Balance
        ('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 (t :: Tree).
ProofIsBalancedBalance t =>
IsAlmostBalancedT t -> IsBalancedT (Balance t)
proofIsBalancedBalance (IsBalancedT (MaxKeyDelete ('ForkTree ll (Node ln la) lr))
-> Proxy
     (Node
        (MaxKey ('ForkTree ll (Node ln la) lr))
        (MaxValue ('ForkTree ll (Node ln la) lr)))
-> IsBalancedT r
-> IsAlmostBalancedT
     ('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) a (r :: Tree).
IsBalancedT l
-> Proxy (Node n a)
-> IsBalancedT r
-> IsAlmostBalancedT ('ForkTree l (Node n a) r)
ForkIsAlmostBalancedT IsBalancedT (MaxKeyDelete l)
IsBalancedT (MaxKeyDelete ('ForkTree ll (Node ln la) lr))
lIsBalanced' Proxy (Node (MaxKey l) (MaxValue l))
Proxy
  (Node
     (MaxKey ('ForkTree ll (Node ln la) lr))
     (MaxValue ('ForkTree ll (Node ln la) lr)))
pNode IsBalancedT r
rIsBalanced)
    where
      lIsBalanced' :: IsBalancedT (MaxKeyDelete l)
lIsBalanced' = IsBalancedT l -> IsBalancedT (MaxKeyDelete l)
forall (t :: Tree).
ProofMaxKeyDeleteIsBalanced t =>
IsBalancedT t -> IsBalancedT (MaxKeyDelete t)
proofMaxKeyDeleteIsBalanced IsBalancedT l
lIsBalanced
      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 ProofIsBalancedDelete' x ('ForkTree 'EmptyTree (Node n a1) r) 'LT where
  proofIsBalancedDelete' :: Proxy x
-> IsBalancedT ('ForkTree 'EmptyTree (Node n a1) r)
-> Proxy 'LT
-> IsBalancedT (Delete' x ('ForkTree 'EmptyTree (Node n a1) r) 'LT)
proofIsBalancedDelete' Proxy x
_ IsBalancedT ('ForkTree 'EmptyTree (Node n a1) r)
tIsBalanced Proxy 'LT
_ = IsBalancedT ('ForkTree 'EmptyTree (Node n a1) r)
IsBalancedT (Delete' x ('ForkTree 'EmptyTree (Node n a1) r) 'LT)
tIsBalanced

instance
  ( l ~ 'ForkTree ll (Node ln la) lr,
    ProofIsBalancedDelete x l,
    ProofIsBalancedBalance ('ForkTree (Delete' x l (CmpNat x ln)) (Node n a1) r)
  ) =>
  ProofIsBalancedDelete' x ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a1) r) 'LT
  where
  proofIsBalancedDelete' :: Proxy x
-> IsBalancedT
     ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a1) r)
-> Proxy 'LT
-> IsBalancedT
     (Delete'
        x ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a1) r) 'LT)
proofIsBalancedDelete' Proxy x
px (ForkIsBalancedT IsBalancedT l
lIsBalanced Proxy (Node n a)
node IsBalancedT r
rIsBalanced) Proxy 'LT
_ =
    IsAlmostBalancedT
  ('ForkTree
     (Delete' x ('ForkTree ll (Node ln la) lr) (CmpNat x ln))
     (Node n a)
     r)
-> IsBalancedT
     (Balance
        ('ForkTree
           (Delete' x ('ForkTree ll (Node ln la) lr) (CmpNat x ln))
           (Node n a)
           r))
forall (t :: Tree).
ProofIsBalancedBalance t =>
IsAlmostBalancedT t -> IsBalancedT (Balance t)
proofIsBalancedBalance (IsBalancedT
  (Delete' x ('ForkTree ll (Node ln la) lr) (CmpNat x ln))
-> Proxy (Node n a)
-> IsBalancedT r
-> IsAlmostBalancedT
     ('ForkTree
        (Delete' x ('ForkTree ll (Node ln la) lr) (CmpNat x ln))
        (Node n a)
        r)
forall (l :: Tree) (n :: Nat) a (r :: Tree).
IsBalancedT l
-> Proxy (Node n a)
-> IsBalancedT r
-> IsAlmostBalancedT ('ForkTree l (Node n a) r)
ForkIsAlmostBalancedT IsBalancedT
  (Delete' x ('ForkTree ll (Node ln la) lr) (CmpNat x ln))
IsBalancedT (Delete x l)
lIsBalanced' Proxy (Node n a)
node IsBalancedT r
rIsBalanced)
    where
      lIsBalanced' :: IsBalancedT (Delete x l)
lIsBalanced' = Proxy x -> IsBalancedT l -> IsBalancedT (Delete x l)
forall (x :: Nat) (t :: Tree).
ProofIsBalancedDelete x t =>
Proxy x -> IsBalancedT t -> IsBalancedT (Delete x t)
proofIsBalancedDelete Proxy x
px IsBalancedT l
lIsBalanced

instance ProofIsBalancedDelete' x ('ForkTree l (Node n a1) 'EmptyTree) 'GT where
  proofIsBalancedDelete' :: Proxy x
-> IsBalancedT ('ForkTree l (Node n a1) 'EmptyTree)
-> Proxy 'GT
-> IsBalancedT (Delete' x ('ForkTree l (Node n a1) 'EmptyTree) 'GT)
proofIsBalancedDelete' Proxy x
_ IsBalancedT ('ForkTree l (Node n a1) 'EmptyTree)
tIsBalanced Proxy 'GT
_ = IsBalancedT ('ForkTree l (Node n a1) 'EmptyTree)
IsBalancedT (Delete' x ('ForkTree l (Node n a1) 'EmptyTree) 'GT)
tIsBalanced

instance
  ( r ~ 'ForkTree rl (Node rn ra) rr,
    ProofIsBalancedDelete x r,
    ProofIsBalancedBalance ('ForkTree l (Node n a1) (Delete' x r (CmpNat x rn)))
  ) =>
  ProofIsBalancedDelete' x ('ForkTree l (Node n a1) ('ForkTree rl (Node rn ra) rr)) 'GT
  where
  proofIsBalancedDelete' :: Proxy x
-> IsBalancedT
     ('ForkTree l (Node n a1) ('ForkTree rl (Node rn ra) rr))
-> Proxy 'GT
-> IsBalancedT
     (Delete'
        x ('ForkTree l (Node n a1) ('ForkTree rl (Node rn ra) rr)) 'GT)
proofIsBalancedDelete' Proxy x
px (ForkIsBalancedT IsBalancedT l
lIsBalanced Proxy (Node n a)
node IsBalancedT r
rIsBalanced) Proxy 'GT
_ =
    IsAlmostBalancedT
  ('ForkTree
     l
     (Node n a)
     (Delete' x ('ForkTree rl (Node rn ra) rr) (CmpNat x rn)))
-> IsBalancedT
     (Balance
        ('ForkTree
           l
           (Node n a)
           (Delete' x ('ForkTree rl (Node rn ra) rr) (CmpNat x rn))))
forall (t :: Tree).
ProofIsBalancedBalance t =>
IsAlmostBalancedT t -> IsBalancedT (Balance t)
proofIsBalancedBalance (IsBalancedT l
-> Proxy (Node n a)
-> IsBalancedT
     (Delete' x ('ForkTree rl (Node rn ra) rr) (CmpNat x rn))
-> IsAlmostBalancedT
     ('ForkTree
        l
        (Node n a)
        (Delete' x ('ForkTree rl (Node rn ra) rr) (CmpNat x rn)))
forall (l :: Tree) (n :: Nat) a (r :: Tree).
IsBalancedT l
-> Proxy (Node n a)
-> IsBalancedT r
-> IsAlmostBalancedT ('ForkTree l (Node n a) r)
ForkIsAlmostBalancedT IsBalancedT l
lIsBalanced Proxy (Node n a)
node IsBalancedT
  (Delete' x ('ForkTree rl (Node rn ra) rr) (CmpNat x rn))
IsBalancedT (Delete x r)
rIsBalanced')
    where
      rIsBalanced' :: IsBalancedT (Delete x r)
rIsBalanced' = Proxy x -> IsBalancedT r -> IsBalancedT (Delete x r)
forall (x :: Nat) (t :: Tree).
ProofIsBalancedDelete x t =>
Proxy x -> IsBalancedT t -> IsBalancedT (Delete x t)
proofIsBalancedDelete Proxy x
px IsBalancedT r
rIsBalanced