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

-- |
-- Module      : Data.Tree.AVL.Intern.Delete
-- Description : Deletion algorithm (with proofs) over internalist AVL trees
-- Copyright   : (c) Nicolás Rodríguez, 2021
-- License     : GPL-3
-- Maintainer  : Nicolás Rodríguez
-- Stability   : experimental
-- Portability : POSIX
--
-- Implementation of the deletion algorithm over internalist AVL trees,
-- along with the necessary proofs to ensure (at compile time) that the
-- key ordering and height balancing still holds.
module Data.Tree.AVL.Intern.Delete
  ( Deletable (Delete, delete),
  )
where

import Data.Kind (Type)
import Data.Proxy (Proxy (Proxy))
import Data.Tree.AVL.Intern.Balance
  ( Balanceable (Balance, balance),
    ProofGtNBalance (proofGtNBalance),
    ProofLtNBalance (proofLtNBalance),
  )
import Data.Tree.AVL.Intern.Constructors
  ( AVL (EmptyAVL, ForkAVL),
    AlmostAVL (AlmostAVL),
  )
import Data.Tree.BST.Invariants (GtN, LtN)
import Data.Tree.ITree (Tree (EmptyTree, ForkTree))
import Data.Tree.Node (Node, getValue, mkNode)
import Data.Type.Equality (gcastWith, (:~:) (Refl))
import GHC.TypeLits (CmpNat, Nat)
import Prelude
  ( Bool (True),
    Ordering (EQ, GT, LT),
    Show,
    ($),
  )

-- | 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 ->
    AVL 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
-> AVL ('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
_ AVL ('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
-> AVL
     ('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
_ AVL
  ('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
-> AVL
     ('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
_ AVL
  ('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,
    Show (MaxValue l),
    Maxable l,
    MaxKeyDeletable l,
    ProofLTMaxKey l n,
    ProofLtNMaxKeyDelete l n,
    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
-> AVL
     ('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
_ (ForkAVL AVL l
l Node n a
_ AVL r
r) 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 (AVL l -> Proxy n -> LtN (MaxKeyDelete l) n :~: 'True
forall (t :: Tree) (n :: Nat).
(ProofLtNMaxKeyDelete t n, LtN t n ~ 'True) =>
AVL t -> Proxy n -> LtN (MaxKeyDelete t) n :~: 'True
proofLtNMaxKeyDelete AVL l
l 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 (AVL l -> Proxy n -> CmpNat (MaxKey l) n :~: 'LT
forall (t :: Tree) (n :: Nat).
(ProofLTMaxKey t n, LtN t n ~ 'True) =>
AVL t -> Proxy n -> CmpNat (MaxKey t) n :~: 'LT
proofLTMaxKey AVL l
l 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 (AlmostAVL
  ('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) =>
AlmostAVL t -> Proxy n -> LtN (Balance t) n :~: 'True
proofLtNBalance (AVL (MaxKeyDelete ('ForkTree ll (Node ln la) lr))
-> Node
     (MaxKey ('ForkTree ll (Node ln la) lr))
     (MaxValue ('ForkTree ll (Node ln la) lr))
-> AVL r
-> AlmostAVL
     ('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 (l :: Tree) (n :: Nat) (r :: Tree).
(Show a, LtN l n ~ 'True, GtN r n ~ 'True) =>
AVL l -> Node n a -> AVL r -> AlmostAVL ('ForkTree l (Node n a) r)
AlmostAVL AVL (MaxKeyDelete l)
AVL (MaxKeyDelete ('ForkTree ll (Node ln la) lr))
l' Node
  (MaxKey ('ForkTree ll (Node ln la) lr))
  (MaxValue ('ForkTree ll (Node ln la) lr))
node' AVL r
r) 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
      l' :: AVL (MaxKeyDelete l)
l' = AVL l -> AVL (MaxKeyDelete l)
forall (t :: Tree) (l :: Tree) (n :: Nat) a1 (r :: Tree).
(MaxKeyDeletable t, t ~ 'ForkTree l (Node n a1) r) =>
AVL t -> AVL (MaxKeyDelete t)
maxKeyDelete AVL l
l
      node' :: Node
  (MaxKey ('ForkTree ll (Node ln la) lr))
  (MaxValue ('ForkTree ll (Node ln la) lr))
node' = Proxy (MaxKey ('ForkTree ll (Node ln la) lr))
-> MaxValue ('ForkTree ll (Node ln la) lr)
-> Node
     (MaxKey ('ForkTree ll (Node ln la) lr))
     (MaxValue ('ForkTree ll (Node ln la) lr))
forall (k :: Nat) a. Proxy k -> a -> Node k a
mkNode (Proxy (MaxKey l)
forall {k} (t :: k). Proxy t
Proxy :: Proxy (MaxKey l)) (AVL l -> MaxValue l
forall (t :: Tree) (l :: Tree) (n :: Nat) a1 (r :: Tree).
(Maxable t, t ~ 'ForkTree l (Node n a1) r) =>
AVL t -> MaxValue t
maxValue AVL l
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
-> AVL ('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
_ AVL ('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,
    CmpNat x n1 ~ 'LT,
    LtN l n ~ 'True,
    Deletable x l,
    ProofLtNDelete' x l n o,
    ProofLtNBalance ('ForkTree (Delete' x l o) (Node n1 a1) r) n,
    ProofLtNDelete' x l n1 o
  ) =>
  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
-> AVL ('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 (ForkAVL AVL l
l Node n a
node AVL r
r) Proxy n
pn Proxy 'LT
_ =
    (LtN (Delete' x ('ForkTree ll (Node ln la) lr) o) n :~: 'True)
-> ((LtN (Delete' x ('ForkTree ll (Node ln la) lr) o) n ~ 'True) =>
    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
-> AVL 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
-> AVL t -> Proxy n -> Proxy o -> LtN (Delete' x t o) n :~: 'True
proofLtNDelete' Proxy x
px AVL l
l 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
-> AVL 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
-> AVL t -> Proxy n -> Proxy o -> LtN (Delete' x t o) n :~: 'True
proofLtNDelete' Proxy x
px AVL l
l (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 (AlmostAVL
  ('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) =>
AlmostAVL t -> Proxy n -> LtN (Balance t) n :~: 'True
proofLtNBalance (AVL (Delete' x ('ForkTree ll (Node ln la) lr) o)
-> Node n a
-> AVL r
-> AlmostAVL
     ('ForkTree
        (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n a) r)
forall a (l :: Tree) (n :: Nat) (r :: Tree).
(Show a, LtN l n ~ 'True, GtN r n ~ 'True) =>
AVL l -> Node n a -> AVL r -> AlmostAVL ('ForkTree l (Node n a) r)
AlmostAVL AVL (Delete' x ('ForkTree ll (Node ln la) lr) o)
AVL (Delete x l)
l' Node n a
node AVL r
r) 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
      l' :: AVL (Delete x l)
l' = Proxy x -> AVL l -> AVL (Delete x l)
forall (x :: Nat) (t :: Tree).
Deletable x t =>
Proxy x -> AVL t -> AVL (Delete x t)
delete Proxy x
px AVL l
l

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
-> AVL ('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
_ AVL ('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,
    Deletable x r,
    ProofLtNDelete' x r n o,
    ProofLtNBalance ('ForkTree l (Node n1 a1) (Delete' x r o)) n,
    ProofGtNDelete' x r n1 o
  ) =>
  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
-> AVL ('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 (ForkAVL AVL l
l Node n a
node AVL r
r) Proxy n
pn Proxy 'GT
_ =
    (LtN (Delete' x ('ForkTree rl (Node rn ra) rr) o) n :~: 'True)
-> ((LtN (Delete' x ('ForkTree rl (Node rn ra) rr) o) n ~ 'True) =>
    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
-> AVL 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
-> AVL t -> Proxy n -> Proxy o -> LtN (Delete' x t o) n :~: 'True
proofLtNDelete' Proxy x
px AVL r
r 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
-> AVL 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
-> AVL t -> Proxy n -> Proxy o -> GtN (Delete' x t o) n :~: 'True
proofGtNDelete' Proxy x
px AVL r
r (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 (AlmostAVL
  ('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) =>
AlmostAVL t -> Proxy n -> LtN (Balance t) n :~: 'True
proofLtNBalance (AVL l
-> Node n a
-> AVL (Delete' x ('ForkTree rl (Node rn ra) rr) o)
-> AlmostAVL
     ('ForkTree
        l (Node n a) (Delete' x ('ForkTree rl (Node rn ra) rr) o))
forall a (l :: Tree) (n :: Nat) (r :: Tree).
(Show a, LtN l n ~ 'True, GtN r n ~ 'True) =>
AVL l -> Node n a -> AVL r -> AlmostAVL ('ForkTree l (Node n a) r)
AlmostAVL AVL l
l Node n a
node AVL (Delete' x ('ForkTree rl (Node rn ra) rr) o)
AVL (Delete x r)
r') 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
      r' :: AVL (Delete x r)
r' = Proxy x -> AVL r -> AVL (Delete x r)
forall (x :: Nat) (t :: Tree).
Deletable x t =>
Proxy x -> AVL t -> AVL (Delete x t)
delete Proxy x
px AVL r
r

-- | 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 ->
    AVL 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
-> AVL ('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
_ AVL ('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
-> AVL
     ('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
_ AVL
  ('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
-> AVL
     ('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
_ AVL
  ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a1) 'EmptyTree)
_ Proxy n
_ Proxy 'EQ
_ = GtN
  (Delete'
     x
     ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n1 a1) 'EmptyTree)
     'EQ)
  n
:~: 'True
forall {k} (a :: k). a :~: a
Refl

instance
  ( l ~ 'ForkTree ll (Node ln la) lr,
    r ~ 'ForkTree rl (Node rn ra) rr,
    GtN l n ~ 'True,
    GtN r n ~ 'True,
    GtN r (MaxKey l) ~ 'True,
    LtN (MaxKeyDelete l) (MaxKey l) ~ 'True,
    Show (MaxValue l),
    Maxable l,
    MaxKeyDeletable l,
    ProofGTMaxKey l n,
    ProofGtNMaxKeyDelete l n,
    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
-> AVL
     ('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
_ (ForkAVL AVL l
l Node n a
_ AVL r
r) Proxy n
pn Proxy 'EQ
_ =
    (GtN (MaxKeyDelete ('ForkTree ll (Node ln la) lr)) n :~: 'True)
-> ((GtN (MaxKeyDelete ('ForkTree ll (Node ln la) lr)) n
     ~ 'True) =>
    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 (AVL l -> Proxy n -> GtN (MaxKeyDelete l) n :~: 'True
forall (t :: Tree) (n :: Nat).
(ProofGtNMaxKeyDelete t n, GtN t n ~ 'True) =>
AVL t -> Proxy n -> GtN (MaxKeyDelete t) n :~: 'True
proofGtNMaxKeyDelete AVL l
l 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 (AVL l -> Proxy n -> CmpNat (MaxKey l) n :~: 'GT
forall (t :: Tree) (n :: Nat).
(ProofGTMaxKey t n, GtN t n ~ 'True) =>
AVL t -> Proxy n -> CmpNat (MaxKey t) n :~: 'GT
proofGTMaxKey AVL l
l 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 (AlmostAVL
  ('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) =>
AlmostAVL t -> Proxy n -> GtN (Balance t) n :~: 'True
proofGtNBalance (AVL (MaxKeyDelete ('ForkTree ll (Node ln la) lr))
-> Node
     (MaxKey ('ForkTree ll (Node ln la) lr))
     (MaxValue ('ForkTree ll (Node ln la) lr))
-> AVL r
-> AlmostAVL
     ('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 (l :: Tree) (n :: Nat) (r :: Tree).
(Show a, LtN l n ~ 'True, GtN r n ~ 'True) =>
AVL l -> Node n a -> AVL r -> AlmostAVL ('ForkTree l (Node n a) r)
AlmostAVL AVL (MaxKeyDelete l)
AVL (MaxKeyDelete ('ForkTree ll (Node ln la) lr))
l' Node
  (MaxKey ('ForkTree ll (Node ln la) lr))
  (MaxValue ('ForkTree ll (Node ln la) lr))
node' AVL r
r) 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
      l' :: AVL (MaxKeyDelete l)
l' = AVL l -> AVL (MaxKeyDelete l)
forall (t :: Tree) (l :: Tree) (n :: Nat) a1 (r :: Tree).
(MaxKeyDeletable t, t ~ 'ForkTree l (Node n a1) r) =>
AVL t -> AVL (MaxKeyDelete t)
maxKeyDelete AVL l
l
      node' :: Node
  (MaxKey ('ForkTree ll (Node ln la) lr))
  (MaxValue ('ForkTree ll (Node ln la) lr))
node' = Proxy (MaxKey ('ForkTree ll (Node ln la) lr))
-> MaxValue ('ForkTree ll (Node ln la) lr)
-> Node
     (MaxKey ('ForkTree ll (Node ln la) lr))
     (MaxValue ('ForkTree ll (Node ln la) lr))
forall (k :: Nat) a. Proxy k -> a -> Node k a
mkNode (Proxy (MaxKey l)
forall {k} (t :: k). Proxy t
Proxy :: Proxy (MaxKey l)) (AVL l -> MaxValue l
forall (t :: Tree) (l :: Tree) (n :: Nat) a1 (r :: Tree).
(Maxable t, t ~ 'ForkTree l (Node n a1) r) =>
AVL t -> MaxValue t
maxValue AVL l
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
-> AVL ('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
_ AVL ('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,
    Deletable x l,
    ProofGtNDelete' x l n o,
    ProofGtNBalance ('ForkTree (Delete' x l o) (Node n1 a1) r) n,
    ProofLtNDelete' x l n1 o
  ) =>
  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
-> AVL ('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 (ForkAVL AVL l
l Node n a
node AVL r
r) Proxy n
pn Proxy 'LT
_ =
    (GtN (Delete' x ('ForkTree ll (Node ln la) lr) o) n :~: 'True)
-> ((GtN (Delete' x ('ForkTree ll (Node ln la) lr) o) n ~ 'True) =>
    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
-> AVL 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
-> AVL t -> Proxy n -> Proxy o -> GtN (Delete' x t o) n :~: 'True
proofGtNDelete' Proxy x
px AVL l
l 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
-> AVL 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
-> AVL t -> Proxy n -> Proxy o -> LtN (Delete' x t o) n :~: 'True
proofLtNDelete' Proxy x
px AVL l
l (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 (AlmostAVL
  ('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) =>
AlmostAVL t -> Proxy n -> GtN (Balance t) n :~: 'True
proofGtNBalance (AVL (Delete' x ('ForkTree ll (Node ln la) lr) o)
-> Node n a
-> AVL r
-> AlmostAVL
     ('ForkTree
        (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n a) r)
forall a (l :: Tree) (n :: Nat) (r :: Tree).
(Show a, LtN l n ~ 'True, GtN r n ~ 'True) =>
AVL l -> Node n a -> AVL r -> AlmostAVL ('ForkTree l (Node n a) r)
AlmostAVL AVL (Delete' x ('ForkTree ll (Node ln la) lr) o)
AVL (Delete x l)
l' Node n a
node AVL r
r) 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
      l' :: AVL (Delete x l)
l' = Proxy x -> AVL l -> AVL (Delete x l)
forall (x :: Nat) (t :: Tree).
Deletable x t =>
Proxy x -> AVL t -> AVL (Delete x t)
delete Proxy x
px AVL l
l

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
-> AVL ('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
_ AVL ('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,
    Deletable x r,
    ProofGtNDelete' x r n o,
    ProofGtNBalance ('ForkTree l (Node n1 a1) (Delete' x r o)) n,
    ProofGtNDelete' x r n1 o
  ) =>
  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
-> AVL ('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 (ForkAVL AVL l
l Node n a
node AVL r
r) Proxy n
pn Proxy 'GT
_ =
    (GtN (Delete' x ('ForkTree rl (Node rn ra) rr) o) n :~: 'True)
-> ((GtN (Delete' x ('ForkTree rl (Node rn ra) rr) o) n ~ 'True) =>
    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
-> AVL 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
-> AVL t -> Proxy n -> Proxy o -> GtN (Delete' x t o) n :~: 'True
proofGtNDelete' Proxy x
px AVL r
r 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
-> AVL 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
-> AVL t -> Proxy n -> Proxy o -> GtN (Delete' x t o) n :~: 'True
proofGtNDelete' Proxy x
px AVL r
r (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 (AlmostAVL
  ('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) =>
AlmostAVL t -> Proxy n -> GtN (Balance t) n :~: 'True
proofGtNBalance (AVL l
-> Node n a
-> AVL (Delete' x ('ForkTree rl (Node rn ra) rr) o)
-> AlmostAVL
     ('ForkTree
        l (Node n a) (Delete' x ('ForkTree rl (Node rn ra) rr) o))
forall a (l :: Tree) (n :: Nat) (r :: Tree).
(Show a, LtN l n ~ 'True, GtN r n ~ 'True) =>
AVL l -> Node n a -> AVL r -> AlmostAVL ('ForkTree l (Node n a) r)
AlmostAVL AVL l
l Node n a
node AVL (Delete' x ('ForkTree rl (Node rn ra) rr) o)
AVL (Delete x r)
r') 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
      r' :: AVL (Delete x r)
r' = Proxy x -> AVL r -> AVL (Delete x r)
forall (x :: Nat) (t :: Tree).
Deletable x t =>
Proxy x -> AVL t -> AVL (Delete x t)
delete Proxy x
px AVL r
r

-- | Prove that in a tree @t@ which verifies that @GtN t n ~ 'True@,
-- the maximum key of @t@ is also greater than @n@.
-- This proof is needed for the delete operation.
class ProofGTMaxKey (t :: Tree) (n :: Nat) where
  proofGTMaxKey ::
    (GtN t n ~ 'True) =>
    AVL 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) =>
AVL ('ForkTree l (Node n1 a) 'EmptyTree)
-> Proxy n
-> CmpNat (MaxKey ('ForkTree l (Node n1 a) 'EmptyTree)) n :~: 'GT
proofGTMaxKey AVL ('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) =>
AVL ('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 (ForkAVL AVL l
_ Node n a
_ AVL r
r) Proxy n
pn =
    (CmpNat (MaxKey ('ForkTree rl (Node rn ra) rr)) n :~: 'GT)
-> ((CmpNat (MaxKey ('ForkTree rl (Node rn ra) rr)) n ~ 'GT) =>
    CmpNat (MaxKey ('ForkTree rl (Node rn ra) rr)) n :~: 'GT)
-> CmpNat (MaxKey ('ForkTree rl (Node rn ra) rr)) n :~: 'GT
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (AVL r -> Proxy n -> CmpNat (MaxKey r) n :~: 'GT
forall (t :: Tree) (n :: Nat).
(ProofGTMaxKey t n, GtN t n ~ 'True) =>
AVL t -> Proxy n -> CmpNat (MaxKey t) n :~: 'GT
proofGTMaxKey AVL r
r Proxy n
pn) (CmpNat (MaxKey ('ForkTree rl (Node rn ra) rr)) n ~ 'GT) =>
CmpNat (MaxKey ('ForkTree rl (Node rn ra) rr)) n :~: 'GT
forall {k} (a :: k). a :~: a
Refl

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

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

instance
  ( r ~ 'ForkTree rl (Node rn ra) rr,
    GtN r n ~ 'True,
    MaxKeyDeletable r,
    ProofGtNMaxKeyDelete r n,
    ProofGtNBalance ('ForkTree l (Node n1 a) (MaxKeyDelete r)) n,
    ProofGtNMaxKeyDelete r n1
  ) =>
  ProofGtNMaxKeyDelete ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr)) n
  where
  proofGtNMaxKeyDelete :: (GtN ('ForkTree l (Node n1 a) ('ForkTree rl (Node rn ra) rr)) n
 ~ 'True) =>
AVL ('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 (ForkAVL AVL l
l Node n a
node AVL r
r) Proxy n
pn =
    (GtN (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)) n :~: 'True)
-> ((GtN (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)) n
     ~ 'True) =>
    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 (AVL r -> Proxy n -> GtN (MaxKeyDelete r) n :~: 'True
forall (t :: Tree) (n :: Nat).
(ProofGtNMaxKeyDelete t n, GtN t n ~ 'True) =>
AVL t -> Proxy n -> GtN (MaxKeyDelete t) n :~: 'True
proofGtNMaxKeyDelete AVL r
r 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 (AVL r -> Proxy n1 -> GtN (MaxKeyDelete r) n1 :~: 'True
forall (t :: Tree) (n :: Nat).
(ProofGtNMaxKeyDelete t n, GtN t n ~ 'True) =>
AVL t -> Proxy n -> GtN (MaxKeyDelete t) n :~: 'True
proofGtNMaxKeyDelete AVL r
r (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 (AlmostAVL
  ('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) =>
AlmostAVL t -> Proxy n -> GtN (Balance t) n :~: 'True
proofGtNBalance (AVL l
-> Node n a
-> AVL (MaxKeyDelete ('ForkTree rl (Node rn ra) rr))
-> AlmostAVL
     ('ForkTree
        l (Node n a) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
forall a (l :: Tree) (n :: Nat) (r :: Tree).
(Show a, LtN l n ~ 'True, GtN r n ~ 'True) =>
AVL l -> Node n a -> AVL r -> AlmostAVL ('ForkTree l (Node n a) r)
AlmostAVL AVL l
l Node n a
node AVL (MaxKeyDelete r)
AVL (MaxKeyDelete ('ForkTree rl (Node rn ra) rr))
r') 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
      r' :: AVL (MaxKeyDelete r)
r' = AVL r -> AVL (MaxKeyDelete r)
forall (t :: Tree) (l :: Tree) (n :: Nat) a1 (r :: Tree).
(MaxKeyDeletable t, t ~ 'ForkTree l (Node n a1) r) =>
AVL t -> AVL (MaxKeyDelete t)
maxKeyDelete AVL r
r

-- | 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 `delete` operation.
class ProofLTMaxKey (t :: Tree) (n :: Nat) where
  proofLTMaxKey ::
    (LtN t n ~ 'True) =>
    AVL 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) =>
AVL ('ForkTree l (Node n1 a) 'EmptyTree)
-> Proxy n
-> CmpNat (MaxKey ('ForkTree l (Node n1 a) 'EmptyTree)) n :~: 'LT
proofLTMaxKey AVL ('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) =>
AVL ('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 (ForkAVL AVL l
_ Node n a
_ AVL r
r) Proxy n
pn =
    (CmpNat (MaxKey ('ForkTree rl (Node rn ra) rr)) n :~: 'LT)
-> ((CmpNat (MaxKey ('ForkTree rl (Node rn ra) rr)) n ~ 'LT) =>
    CmpNat (MaxKey ('ForkTree rl (Node rn ra) rr)) n :~: 'LT)
-> CmpNat (MaxKey ('ForkTree rl (Node rn ra) rr)) n :~: 'LT
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (AVL r -> Proxy n -> CmpNat (MaxKey r) n :~: 'LT
forall (t :: Tree) (n :: Nat).
(ProofLTMaxKey t n, LtN t n ~ 'True) =>
AVL t -> Proxy n -> CmpNat (MaxKey t) n :~: 'LT
proofLTMaxKey AVL r
r Proxy n
pn) (CmpNat (MaxKey ('ForkTree rl (Node rn ra) rr)) n ~ 'LT) =>
CmpNat (MaxKey ('ForkTree rl (Node rn ra) rr)) n :~: 'LT
forall {k} (a :: k). a :~: a
Refl

-- | Prove that in a tree @t@ which verifies that @LtN t n ~ 'True@,
-- the tree resulting from the removal of the maximum key of @t@ preserves the `LtN` invariant.
-- This proof is needed for the `delete` operation.
class ProofLtNMaxKeyDelete (t :: Tree) (n :: Nat) where
  proofLtNMaxKeyDelete ::
    (LtN t n ~ 'True) =>
    AVL 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) =>
AVL ('ForkTree l (Node n1 a) 'EmptyTree)
-> Proxy n
-> LtN (MaxKeyDelete ('ForkTree l (Node n1 a) 'EmptyTree)) n
   :~: 'True
proofLtNMaxKeyDelete AVL ('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,
    LtN r n1 ~ 'True,
    MaxKeyDeletable r,
    ProofLtNMaxKeyDelete r n,
    ProofGtNMaxKeyDelete r n1,
    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) =>
AVL ('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 (ForkAVL AVL l
l Node n a
node AVL r
r) Proxy n
pn =
    (LtN (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)) n :~: 'True)
-> ((LtN (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)) n
     ~ 'True) =>
    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 (AVL r -> Proxy n -> LtN (MaxKeyDelete r) n :~: 'True
forall (t :: Tree) (n :: Nat).
(ProofLtNMaxKeyDelete t n, LtN t n ~ 'True) =>
AVL t -> Proxy n -> LtN (MaxKeyDelete t) n :~: 'True
proofLtNMaxKeyDelete AVL r
r 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 (AVL r -> Proxy n1 -> GtN (MaxKeyDelete r) n1 :~: 'True
forall (t :: Tree) (n :: Nat).
(ProofGtNMaxKeyDelete t n, GtN t n ~ 'True) =>
AVL t -> Proxy n -> GtN (MaxKeyDelete t) n :~: 'True
proofGtNMaxKeyDelete AVL r
r (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 (AlmostAVL
  ('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) =>
AlmostAVL t -> Proxy n -> LtN (Balance t) n :~: 'True
proofLtNBalance (AVL l
-> Node n a
-> AVL (MaxKeyDelete ('ForkTree rl (Node rn ra) rr))
-> AlmostAVL
     ('ForkTree
        l (Node n a) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
forall a (l :: Tree) (n :: Nat) (r :: Tree).
(Show a, LtN l n ~ 'True, GtN r n ~ 'True) =>
AVL l -> Node n a -> AVL r -> AlmostAVL ('ForkTree l (Node n a) r)
AlmostAVL AVL l
l Node n a
node AVL (MaxKeyDelete r)
AVL (MaxKeyDelete ('ForkTree rl (Node rn ra) rr))
r') 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
      r' :: AVL (MaxKeyDelete r)
r' = AVL r -> AVL (MaxKeyDelete r)
forall (t :: Tree) (l :: Tree) (n :: Nat) a1 (r :: Tree).
(MaxKeyDeletable t, t ~ 'ForkTree l (Node n a1) r) =>
AVL t -> AVL (MaxKeyDelete t)
maxKeyDelete AVL r
r

-- | This type class provides the functionality to delete the node with maximum key value
-- in an `AVL` @t@.
-- The deletion is defined at the value level and the type level.
class MaxKeyDeletable (t :: Tree) where
  type MaxKeyDelete (t :: Tree) :: Tree
  maxKeyDelete ::
    (t ~ 'ForkTree l (Node n a1) r) =>
    AVL t ->
    AVL (MaxKeyDelete t)

instance MaxKeyDeletable ('ForkTree l (Node n a1) 'EmptyTree) where
  type MaxKeyDelete ('ForkTree l (Node n a1) 'EmptyTree) = l
  maxKeyDelete :: forall (l :: Tree) (n :: Nat) a1 (r :: Tree).
('ForkTree l (Node n a1) 'EmptyTree ~ 'ForkTree l (Node n a1) r) =>
AVL ('ForkTree l (Node n a1) 'EmptyTree)
-> AVL (MaxKeyDelete ('ForkTree l (Node n a1) 'EmptyTree))
maxKeyDelete (ForkAVL AVL l
l Node n a
_ AVL r
_) = AVL l
AVL (MaxKeyDelete ('ForkTree l (Node n a1) 'EmptyTree))
l

instance
  ( r ~ 'ForkTree rl (Node rn ra) rr,
    MaxKeyDeletable r,
    Balanceable ('ForkTree l (Node n a1) (MaxKeyDelete r)),
    ProofGtNMaxKeyDelete r n
  ) =>
  MaxKeyDeletable ('ForkTree l (Node n a1) ('ForkTree rl (Node rn ra) rr))
  where
  type
    MaxKeyDelete ('ForkTree l (Node n a1) ('ForkTree rl (Node rn ra) rr)) =
      Balance ('ForkTree l (Node n a1) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
  maxKeyDelete :: forall (l :: Tree) (n :: Nat) a1 (r :: Tree).
('ForkTree l (Node n a1) ('ForkTree rl (Node rn ra) rr)
 ~ 'ForkTree l (Node n a1) r) =>
AVL ('ForkTree l (Node n a1) ('ForkTree rl (Node rn ra) rr))
-> AVL
     (MaxKeyDelete
        ('ForkTree l (Node n a1) ('ForkTree rl (Node rn ra) rr)))
maxKeyDelete (ForkAVL AVL l
l Node n a
node AVL r
r) =
    (GtN (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)) n :~: 'True)
-> ((GtN (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)) n
     ~ 'True) =>
    AVL
      (Balance'
         ('ForkTree
            l (Node n a1) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
         (UnbalancedState
            (Height l)
            (Height (MaxKeyDelete ('ForkTree rl (Node rn ra) rr))))))
-> AVL
     (Balance'
        ('ForkTree
           l (Node n a1) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
        (UnbalancedState
           (Height l) (Height (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))))
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (AVL r -> Proxy n -> GtN (MaxKeyDelete r) n :~: 'True
forall (t :: Tree) (n :: Nat).
(ProofGtNMaxKeyDelete t n, GtN t n ~ 'True) =>
AVL t -> Proxy n -> GtN (MaxKeyDelete t) n :~: 'True
proofGtNMaxKeyDelete AVL r
r (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n)) (((GtN (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)) n ~ 'True) =>
  AVL
    (Balance'
       ('ForkTree
          l (Node n a1) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
       (UnbalancedState
          (Height l)
          (Height (MaxKeyDelete ('ForkTree rl (Node rn ra) rr))))))
 -> AVL
      (Balance'
         ('ForkTree
            l (Node n a1) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
         (UnbalancedState
            (Height l)
            (Height (MaxKeyDelete ('ForkTree rl (Node rn ra) rr))))))
-> ((GtN (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)) n
     ~ 'True) =>
    AVL
      (Balance'
         ('ForkTree
            l (Node n a1) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
         (UnbalancedState
            (Height l)
            (Height (MaxKeyDelete ('ForkTree rl (Node rn ra) rr))))))
-> AVL
     (Balance'
        ('ForkTree
           l (Node n a1) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
        (UnbalancedState
           (Height l) (Height (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))))
forall a b. (a -> b) -> a -> b
$
      AlmostAVL
  ('ForkTree
     l (Node n a) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
-> AVL
     (Balance
        ('ForkTree
           l (Node n a) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr))))
forall (t :: Tree). Balanceable t => AlmostAVL t -> AVL (Balance t)
balance (AlmostAVL
   ('ForkTree
      l (Node n a) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
 -> AVL
      (Balance
         ('ForkTree
            l (Node n a) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))))
-> AlmostAVL
     ('ForkTree
        l (Node n a) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
-> AVL
     (Balance
        ('ForkTree
           l (Node n a) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr))))
forall a b. (a -> b) -> a -> b
$ AVL l
-> Node n a
-> AVL (MaxKeyDelete ('ForkTree rl (Node rn ra) rr))
-> AlmostAVL
     ('ForkTree
        l (Node n a) (MaxKeyDelete ('ForkTree rl (Node rn ra) rr)))
forall a (l :: Tree) (n :: Nat) (r :: Tree).
(Show a, LtN l n ~ 'True, GtN r n ~ 'True) =>
AVL l -> Node n a -> AVL r -> AlmostAVL ('ForkTree l (Node n a) r)
AlmostAVL AVL l
l Node n a
node (AVL r -> AVL (MaxKeyDelete r)
forall (t :: Tree) (l :: Tree) (n :: Nat) a1 (r :: Tree).
(MaxKeyDeletable t, t ~ 'ForkTree l (Node n a1) r) =>
AVL t -> AVL (MaxKeyDelete t)
maxKeyDelete AVL r
r)

-- | This type class provides the functionality to get the key, type and value of the node with maximum key value
-- in an `AVL` @t@.
-- The lookup is defined at the value level and the type level.
-- Since the keys are only kept at the type level, there's no value level getter of the maximum key.
class Maxable (t :: Tree) where
  type MaxKey (t :: Tree) :: Nat
  type MaxValue (t :: Tree) :: Type
  maxValue ::
    (t ~ 'ForkTree l (Node n a1) r) =>
    AVL t ->
    MaxValue t

instance Maxable ('ForkTree l (Node n a1) 'EmptyTree) where
  type MaxKey ('ForkTree l (Node n a1) 'EmptyTree) = n
  type MaxValue ('ForkTree l (Node n a1) 'EmptyTree) = a1
  maxValue :: forall (l :: Tree) (n :: Nat) a1 (r :: Tree).
('ForkTree l (Node n a1) 'EmptyTree ~ 'ForkTree l (Node n a1) r) =>
AVL ('ForkTree l (Node n a1) 'EmptyTree)
-> MaxValue ('ForkTree l (Node n a1) 'EmptyTree)
maxValue (ForkAVL AVL l
_ Node n a
node AVL r
_) = Node n a -> a
forall (k :: Nat) a. Node k a -> a
getValue Node n a
node

instance
  (Maxable ('ForkTree rl (Node rn ra) rr)) =>
  Maxable ('ForkTree l (Node n a1) ('ForkTree rl (Node rn ra) rr))
  where
  type MaxKey ('ForkTree l (Node n a1) ('ForkTree rl (Node rn ra) rr)) = MaxKey ('ForkTree rl (Node rn ra) rr)
  type MaxValue ('ForkTree l (Node n a1) ('ForkTree rl (Node rn ra) rr)) = MaxValue ('ForkTree rl (Node rn ra) rr)
  maxValue :: forall (l :: Tree) (n :: Nat) a1 (r :: Tree).
('ForkTree l (Node n a1) ('ForkTree rl (Node rn ra) rr)
 ~ 'ForkTree l (Node n a1) r) =>
AVL ('ForkTree l (Node n a1) ('ForkTree rl (Node rn ra) rr))
-> MaxValue
     ('ForkTree l (Node n a1) ('ForkTree rl (Node rn ra) rr))
maxValue (ForkAVL AVL l
_ Node n a
_ AVL r
r) = AVL r -> MaxValue r
forall (t :: Tree) (l :: Tree) (n :: Nat) a1 (r :: Tree).
(Maxable t, t ~ 'ForkTree l (Node n a1) r) =>
AVL t -> MaxValue t
maxValue AVL r
r

-- | This type class provides the functionality to delete the node with key @x@
-- in an `AVL` @t@.
-- The deletion is defined at the value level and the type level,
-- and both return `AVL` trees.
class Deletable (x :: Nat) (t :: Tree) where
  type Delete (x :: Nat) (t :: Tree) :: Tree
  delete :: Proxy x -> AVL t -> AVL (Delete x t)

instance Deletable x 'EmptyTree where
  type Delete x 'EmptyTree = 'EmptyTree
  delete :: Proxy x -> AVL 'EmptyTree -> AVL (Delete x 'EmptyTree)
delete Proxy x
_ AVL 'EmptyTree
_ = AVL 'EmptyTree
AVL (Delete x 'EmptyTree)
EmptyAVL

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

-- | This type class provides the functionality to delete a node with key @x@
-- in a non empty `AVL` @t@.
-- It's only used by the 'Deletable' class and it has one extra parameter @o@,
-- which is the type level comparison of @x@ with the key value of the root node.
-- The @o@ parameter guides the insertion.
class Deletable' (x :: Nat) (t :: Tree) (o :: Ordering) where
  type Delete' (x :: Nat) (t :: Tree) (o :: Ordering) :: Tree
  delete' :: Proxy x -> AVL t -> Proxy o -> AVL (Delete' x t o)

instance Deletable' x ('ForkTree 'EmptyTree (Node n a1) 'EmptyTree) 'EQ where
  type Delete' x ('ForkTree 'EmptyTree (Node n a1) 'EmptyTree) 'EQ = 'EmptyTree
  delete' :: Proxy x
-> AVL ('ForkTree 'EmptyTree (Node n a1) 'EmptyTree)
-> Proxy 'EQ
-> AVL
     (Delete' x ('ForkTree 'EmptyTree (Node n a1) 'EmptyTree) 'EQ)
delete' Proxy x
_ AVL ('ForkTree 'EmptyTree (Node n a1) 'EmptyTree)
_ Proxy 'EQ
_ = AVL 'EmptyTree
AVL (Delete' x ('ForkTree 'EmptyTree (Node n a1) 'EmptyTree) 'EQ)
EmptyAVL

instance Deletable' x ('ForkTree 'EmptyTree (Node n a1) ('ForkTree rl (Node rn ra) rr)) 'EQ where
  type Delete' x ('ForkTree 'EmptyTree (Node n a1) ('ForkTree rl (Node rn ra) rr)) 'EQ = ('ForkTree rl (Node rn ra) rr)
  delete' :: Proxy x
-> AVL
     ('ForkTree 'EmptyTree (Node n a1) ('ForkTree rl (Node rn ra) rr))
-> Proxy 'EQ
-> AVL
     (Delete'
        x
        ('ForkTree 'EmptyTree (Node n a1) ('ForkTree rl (Node rn ra) rr))
        'EQ)
delete' Proxy x
_ (ForkAVL AVL l
_ Node n a
_ AVL r
r) Proxy 'EQ
_ = AVL r
AVL
  (Delete'
     x
     ('ForkTree 'EmptyTree (Node n a1) ('ForkTree rl (Node rn ra) rr))
     'EQ)
r

instance Deletable' x ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a1) 'EmptyTree) 'EQ where
  type Delete' x ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a1) 'EmptyTree) 'EQ = ('ForkTree ll (Node ln la) lr)
  delete' :: Proxy x
-> AVL
     ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a1) 'EmptyTree)
-> Proxy 'EQ
-> AVL
     (Delete'
        x
        ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a1) 'EmptyTree)
        'EQ)
delete' Proxy x
_ (ForkAVL AVL l
l Node n a
_ AVL r
_) Proxy 'EQ
_ = AVL l
AVL
  (Delete'
     x
     ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a1) 'EmptyTree)
     'EQ)
l

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,
    Show (MaxValue l),
    MaxKeyDeletable l,
    Maxable l,
    Balanceable ('ForkTree (MaxKeyDelete l) (Node (MaxKey l) (MaxValue l)) r)
  ) =>
  Deletable' x ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a1) ('ForkTree rl (Node rn ra) rr)) 'EQ
  where
  type
    Delete' x ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a1) ('ForkTree rl (Node rn ra) rr)) 'EQ =
      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))
  delete' :: Proxy x
-> AVL
     ('ForkTree
        ('ForkTree ll (Node ln la) lr)
        (Node n a1)
        ('ForkTree rl (Node rn ra) rr))
-> Proxy 'EQ
-> AVL
     (Delete'
        x
        ('ForkTree
           ('ForkTree ll (Node ln la) lr)
           (Node n a1)
           ('ForkTree rl (Node rn ra) rr))
        'EQ)
delete' Proxy x
_ (ForkAVL AVL l
l Node n a
_ AVL r
r) Proxy 'EQ
_ =
    AlmostAVL
  ('ForkTree
     (MaxKeyDelete ('ForkTree ll (Node ln la) lr))
     (Node
        (MaxKey ('ForkTree ll (Node ln la) lr))
        (MaxValue ('ForkTree ll (Node ln la) lr)))
     r)
-> AVL
     (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). Balanceable t => AlmostAVL t -> AVL (Balance t)
balance (AlmostAVL
   ('ForkTree
      (MaxKeyDelete ('ForkTree ll (Node ln la) lr))
      (Node
         (MaxKey ('ForkTree ll (Node ln la) lr))
         (MaxValue ('ForkTree ll (Node ln la) lr)))
      r)
 -> AVL
      (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)))
-> AlmostAVL
     ('ForkTree
        (MaxKeyDelete ('ForkTree ll (Node ln la) lr))
        (Node
           (MaxKey ('ForkTree ll (Node ln la) lr))
           (MaxValue ('ForkTree ll (Node ln la) lr)))
        r)
-> AVL
     (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
$ AVL (MaxKeyDelete ('ForkTree ll (Node ln la) lr))
-> Node
     (MaxKey ('ForkTree ll (Node ln la) lr))
     (MaxValue ('ForkTree ll (Node ln la) lr))
-> AVL r
-> AlmostAVL
     ('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 (l :: Tree) (n :: Nat) (r :: Tree).
(Show a, LtN l n ~ 'True, GtN r n ~ 'True) =>
AVL l -> Node n a -> AVL r -> AlmostAVL ('ForkTree l (Node n a) r)
AlmostAVL (AVL l -> AVL (MaxKeyDelete l)
forall (t :: Tree) (l :: Tree) (n :: Nat) a1 (r :: Tree).
(MaxKeyDeletable t, t ~ 'ForkTree l (Node n a1) r) =>
AVL t -> AVL (MaxKeyDelete t)
maxKeyDelete AVL l
l) Node
  (MaxKey ('ForkTree ll (Node ln la) lr))
  (MaxValue ('ForkTree ll (Node ln la) lr))
node AVL r
r
    where
      node :: Node
  (MaxKey ('ForkTree ll (Node ln la) lr))
  (MaxValue ('ForkTree ll (Node ln la) lr))
node = Proxy (MaxKey ('ForkTree ll (Node ln la) lr))
-> MaxValue ('ForkTree ll (Node ln la) lr)
-> Node
     (MaxKey ('ForkTree ll (Node ln la) lr))
     (MaxValue ('ForkTree ll (Node ln la) lr))
forall (k :: Nat) a. Proxy k -> a -> Node k a
mkNode (Proxy (MaxKey l)
forall {k} (t :: k). Proxy t
Proxy :: Proxy (MaxKey l)) (AVL l -> MaxValue l
forall (t :: Tree) (l :: Tree) (n :: Nat) a1 (r :: Tree).
(Maxable t, t ~ 'ForkTree l (Node n a1) r) =>
AVL t -> MaxValue t
maxValue AVL l
l)

instance Deletable' x ('ForkTree 'EmptyTree (Node n a1) r) 'LT where
  type Delete' x ('ForkTree 'EmptyTree (Node n a1) r) 'LT = ('ForkTree 'EmptyTree (Node n a1) r)
  delete' :: Proxy x
-> AVL ('ForkTree 'EmptyTree (Node n a1) r)
-> Proxy 'LT
-> AVL (Delete' x ('ForkTree 'EmptyTree (Node n a1) r) 'LT)
delete' Proxy x
_ AVL ('ForkTree 'EmptyTree (Node n a1) r)
t Proxy 'LT
_ = AVL ('ForkTree 'EmptyTree (Node n a1) r)
AVL (Delete' x ('ForkTree 'EmptyTree (Node n a1) r) 'LT)
t

instance
  ( l ~ 'ForkTree ll (Node ln la) lr,
    o ~ CmpNat x ln,
    CmpNat x n ~ 'LT,
    Deletable' x l o,
    Balanceable ('ForkTree (Delete' x l o) (Node n a1) r),
    ProofLtNDelete' x l n o
  ) =>
  Deletable' x ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a1) r) 'LT
  where
  type
    Delete' x ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a1) r) 'LT =
      Balance ('ForkTree (Delete' x ('ForkTree ll (Node ln la) lr) (CmpNat x ln)) (Node n a1) r)
  delete' :: Proxy x
-> AVL ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a1) r)
-> Proxy 'LT
-> AVL
     (Delete'
        x ('ForkTree ('ForkTree ll (Node ln la) lr) (Node n a1) r) 'LT)
delete' Proxy x
px (ForkAVL AVL l
l Node n a
node AVL r
r) Proxy 'LT
_ =
    (LtN (Delete' x ('ForkTree ll (Node ln la) lr) o) n :~: 'True)
-> ((LtN (Delete' x ('ForkTree ll (Node ln la) lr) o) n ~ 'True) =>
    AVL
      (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))))
-> AVL
     (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
-> AVL 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
-> AVL t -> Proxy n -> Proxy o -> LtN (Delete' x t o) n :~: 'True
proofLtNDelete' Proxy x
px AVL l
l (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n) Proxy o
po) (((LtN (Delete' x ('ForkTree ll (Node ln la) lr) o) n ~ 'True) =>
  AVL
    (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))))
 -> AVL
      (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) =>
    AVL
      (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))))
-> AVL
     (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
$
      AlmostAVL
  ('ForkTree
     (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n a) r)
-> AVL
     (Balance
        ('ForkTree
           (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n a) r))
forall (t :: Tree). Balanceable t => AlmostAVL t -> AVL (Balance t)
balance (AlmostAVL
   ('ForkTree
      (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n a) r)
 -> AVL
      (Balance
         ('ForkTree
            (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n a) r)))
-> AlmostAVL
     ('ForkTree
        (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n a) r)
-> AVL
     (Balance
        ('ForkTree
           (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n a) r))
forall a b. (a -> b) -> a -> b
$ AVL (Delete' x ('ForkTree ll (Node ln la) lr) o)
-> Node n a
-> AVL r
-> AlmostAVL
     ('ForkTree
        (Delete' x ('ForkTree ll (Node ln la) lr) o) (Node n a) r)
forall a (l :: Tree) (n :: Nat) (r :: Tree).
(Show a, LtN l n ~ 'True, GtN r n ~ 'True) =>
AVL l -> Node n a -> AVL r -> AlmostAVL ('ForkTree l (Node n a) r)
AlmostAVL (Proxy x -> AVL l -> Proxy o -> AVL (Delete' x l o)
forall (x :: Nat) (t :: Tree) (o :: Ordering).
Deletable' x t o =>
Proxy x -> AVL t -> Proxy o -> AVL (Delete' x t o)
delete' Proxy x
px AVL l
l Proxy o
po) Node n a
node AVL r
r
    where
      po :: Proxy o
po = Proxy o
forall {k} (t :: k). Proxy t
Proxy :: Proxy o

instance Deletable' x ('ForkTree l (Node n a1) 'EmptyTree) 'GT where
  type Delete' x ('ForkTree l (Node n a1) 'EmptyTree) 'GT = ('ForkTree l (Node n a1) 'EmptyTree)
  delete' :: Proxy x
-> AVL ('ForkTree l (Node n a1) 'EmptyTree)
-> Proxy 'GT
-> AVL (Delete' x ('ForkTree l (Node n a1) 'EmptyTree) 'GT)
delete' Proxy x
_ AVL ('ForkTree l (Node n a1) 'EmptyTree)
t Proxy 'GT
_ = AVL ('ForkTree l (Node n a1) 'EmptyTree)
AVL (Delete' x ('ForkTree l (Node n a1) 'EmptyTree) 'GT)
t

instance
  ( r ~ 'ForkTree rl (Node rn ra) rr,
    o ~ CmpNat x rn,
    CmpNat x n ~ 'GT,
    Deletable' x r o,
    Balanceable ('ForkTree l (Node n a1) (Delete' x r o)),
    ProofGtNDelete' x r n o
  ) =>
  Deletable' x ('ForkTree l (Node n a1) ('ForkTree rl (Node rn ra) rr)) 'GT
  where
  type
    Delete' x ('ForkTree l (Node n a1) ('ForkTree rl (Node rn ra) rr)) 'GT =
      Balance ('ForkTree l (Node n a1) (Delete' x ('ForkTree rl (Node rn ra) rr) (CmpNat x rn)))
  delete' :: Proxy x
-> AVL ('ForkTree l (Node n a1) ('ForkTree rl (Node rn ra) rr))
-> Proxy 'GT
-> AVL
     (Delete'
        x ('ForkTree l (Node n a1) ('ForkTree rl (Node rn ra) rr)) 'GT)
delete' Proxy x
px (ForkAVL AVL l
l Node n a
node AVL r
r) Proxy 'GT
_ =
    (GtN (Delete' x ('ForkTree rl (Node rn ra) rr) o) n :~: 'True)
-> ((GtN (Delete' x ('ForkTree rl (Node rn ra) rr) o) n ~ 'True) =>
    AVL
      (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)))))
-> AVL
     (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
-> AVL 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
-> AVL t -> Proxy n -> Proxy o -> GtN (Delete' x t o) n :~: 'True
proofGtNDelete' Proxy x
px AVL r
r (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n) Proxy o
po) (((GtN (Delete' x ('ForkTree rl (Node rn ra) rr) o) n ~ 'True) =>
  AVL
    (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)))))
 -> AVL
      (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) =>
    AVL
      (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)))))
-> AVL
     (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
$
      AlmostAVL
  ('ForkTree
     l (Node n a) (Delete' x ('ForkTree rl (Node rn ra) rr) o))
-> AVL
     (Balance
        ('ForkTree
           l (Node n a) (Delete' x ('ForkTree rl (Node rn ra) rr) o)))
forall (t :: Tree). Balanceable t => AlmostAVL t -> AVL (Balance t)
balance (AlmostAVL
   ('ForkTree
      l (Node n a) (Delete' x ('ForkTree rl (Node rn ra) rr) o))
 -> AVL
      (Balance
         ('ForkTree
            l (Node n a) (Delete' x ('ForkTree rl (Node rn ra) rr) o))))
-> AlmostAVL
     ('ForkTree
        l (Node n a) (Delete' x ('ForkTree rl (Node rn ra) rr) o))
-> AVL
     (Balance
        ('ForkTree
           l (Node n a) (Delete' x ('ForkTree rl (Node rn ra) rr) o)))
forall a b. (a -> b) -> a -> b
$ AVL l
-> Node n a
-> AVL (Delete' x ('ForkTree rl (Node rn ra) rr) o)
-> AlmostAVL
     ('ForkTree
        l (Node n a) (Delete' x ('ForkTree rl (Node rn ra) rr) o))
forall a (l :: Tree) (n :: Nat) (r :: Tree).
(Show a, LtN l n ~ 'True, GtN r n ~ 'True) =>
AVL l -> Node n a -> AVL r -> AlmostAVL ('ForkTree l (Node n a) r)
AlmostAVL AVL l
l Node n a
node (Proxy x -> AVL r -> Proxy o -> AVL (Delete' x r o)
forall (x :: Nat) (t :: Tree) (o :: Ordering).
Deletable' x t o =>
Proxy x -> AVL t -> Proxy o -> AVL (Delete' x t o)
delete' Proxy x
px AVL r
r Proxy o
po)
    where
      po :: Proxy o
po = Proxy o
forall {k} (t :: k). Proxy t
Proxy :: Proxy o