{-# 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.Insert
-- Description : Insertion 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 insertion 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.Insert
  ( Insertable (Insert, insert),
  )
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 inserting a node with key @x@ (lower than @n@) and element value @a@
-- in an `AVL` @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 ProofLtNInsert' (x :: Nat) (a :: Type) (t :: Tree) (n :: Nat) (o :: Ordering) where
  proofLtNInsert' ::
    (CmpNat x n ~ 'LT, LtN t n ~ 'True) =>
    Node x a ->
    AVL t ->
    Proxy n ->
    Proxy o ->
    LtN (Insert x a t) n :~: 'True

instance
  (CmpNat x n1 ~ 'EQ) =>
  ProofLtNInsert' x a ('ForkTree l (Node n1 a1) r) n 'EQ
  where
  proofLtNInsert' :: (CmpNat x n ~ 'LT, LtN ('ForkTree l (Node n1 a1) r) n ~ 'True) =>
Node x a
-> AVL ('ForkTree l (Node n1 a1) r)
-> Proxy n
-> Proxy 'EQ
-> LtN (Insert x a ('ForkTree l (Node n1 a1) r)) n :~: 'True
proofLtNInsert' Node x a
_ AVL ('ForkTree l (Node n1 a1) r)
_ Proxy n
_ Proxy 'EQ
_ = LtN (Insert x a ('ForkTree l (Node n1 a1) r)) n :~: 'True
forall {k} (a :: k). a :~: a
Refl

instance
  ( CmpNat x n1 ~ 'LT,
    ProofLtNBalance ('ForkTree ('ForkTree 'EmptyTree (Node x a) 'EmptyTree) (Node n1 a1) r) n,
    Show a
  ) =>
  ProofLtNInsert' x a ('ForkTree 'EmptyTree (Node n1 a1) r) n 'LT
  where
  proofLtNInsert' :: (CmpNat x n ~ 'LT,
 LtN ('ForkTree 'EmptyTree (Node n1 a1) r) n ~ 'True) =>
Node x a
-> AVL ('ForkTree 'EmptyTree (Node n1 a1) r)
-> Proxy n
-> Proxy 'LT
-> LtN (Insert x a ('ForkTree 'EmptyTree (Node n1 a1) r)) n
   :~: 'True
proofLtNInsert' Node x a
node (ForkAVL AVL l
_ Node n a
node' AVL r
r) Proxy n
pn Proxy 'LT
_ =
    (LtN
   (Balance'
      ('ForkTree
         ('ForkTree 'EmptyTree (Node x a) 'EmptyTree) (Node n1 a1) r)
      (UnbalancedState 1 (Height r)))
   n
 :~: 'True)
-> ((LtN
       (Balance'
          ('ForkTree
             ('ForkTree 'EmptyTree (Node x a) 'EmptyTree) (Node n1 a1) r)
          (UnbalancedState 1 (Height r)))
       n
     ~ 'True) =>
    LtN
      (Balance'
         ('ForkTree
            ('ForkTree 'EmptyTree (Node x a) 'EmptyTree) (Node n1 a1) r)
         (UnbalancedState 1 (Height r)))
      n
    :~: 'True)
-> LtN
     (Balance'
        ('ForkTree
           ('ForkTree 'EmptyTree (Node x a) 'EmptyTree) (Node n1 a1) r)
        (UnbalancedState 1 (Height r)))
     n
   :~: 'True
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (AlmostAVL
  ('ForkTree
     ('ForkTree 'EmptyTree (Node x a) 'EmptyTree) (Node n a) r)
-> Proxy n
-> LtN
     (Balance
        ('ForkTree
           ('ForkTree 'EmptyTree (Node x a) 'EmptyTree) (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 ('ForkTree 'EmptyTree (Node x a) 'EmptyTree)
-> Node n a
-> AVL r
-> AlmostAVL
     ('ForkTree
        ('ForkTree 'EmptyTree (Node x a) 'EmptyTree) (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 'EmptyTree
-> Node x a
-> AVL 'EmptyTree
-> AVL ('ForkTree 'EmptyTree (Node x a) 'EmptyTree)
forall a (l :: Tree) (n :: Nat) (r :: Tree).
(Show a, LtN l n ~ 'True, GtN r n ~ 'True,
 BalancedHeights (Height l) (Height r) n ~ 'True) =>
AVL l -> Node n a -> AVL r -> AVL ('ForkTree l (Node n a) r)
ForkAVL AVL 'EmptyTree
EmptyAVL Node x a
node AVL 'EmptyTree
EmptyAVL) Node n a
node' AVL r
r) Proxy n
pn) (LtN
   (Balance'
      ('ForkTree
         ('ForkTree 'EmptyTree (Node x a) 'EmptyTree) (Node n1 a1) r)
      (UnbalancedState 1 (Height r)))
   n
 ~ 'True) =>
LtN
  (Balance'
     ('ForkTree
        ('ForkTree 'EmptyTree (Node x a) 'EmptyTree) (Node n1 a1) r)
     (UnbalancedState 1 (Height r)))
  n
:~: 'True
forall {k} (a :: k). a :~: a
Refl

instance
  ( l ~ 'ForkTree ll (Node ln lna) lr,
    o ~ CmpNat x ln,
    CmpNat x n1 ~ 'LT,
    LtN l n ~ 'True,
    Insertable x a l,
    ProofLtNInsert' x a l n1 o,
    ProofLtNInsert' x a l n o,
    ProofLtNBalance ('ForkTree (Insert' x a l o) (Node n1 a1) r) n
  ) =>
  ProofLtNInsert' x a ('ForkTree ('ForkTree ll (Node ln lna) lr) (Node n1 a1) r) n 'LT
  where
  proofLtNInsert' :: (CmpNat x n ~ 'LT,
 LtN ('ForkTree ('ForkTree ll (Node ln lna) lr) (Node n1 a1) r) n
 ~ 'True) =>
Node x a
-> AVL ('ForkTree ('ForkTree ll (Node ln lna) lr) (Node n1 a1) r)
-> Proxy n
-> Proxy 'LT
-> LtN
     (Insert
        x a ('ForkTree ('ForkTree ll (Node ln lna) lr) (Node n1 a1) r))
     n
   :~: 'True
proofLtNInsert' Node x a
node (ForkAVL AVL l
l Node n a
node' AVL r
r) Proxy n
pn Proxy 'LT
_ =
    (LtN (Insert' x a ('ForkTree ll (Node ln lna) lr) o) n :~: 'True)
-> ((LtN (Insert' x a ('ForkTree ll (Node ln lna) lr) o) n
     ~ 'True) =>
    LtN
      (Balance'
         ('ForkTree
            (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n1 a1) r)
         (UnbalancedState
            (Height (Insert' x a ('ForkTree ll (Node ln lna) lr) o))
            (Height r)))
      n
    :~: 'True)
-> LtN
     (Balance'
        ('ForkTree
           (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n1 a1) r)
        (UnbalancedState
           (Height (Insert' x a ('ForkTree ll (Node ln lna) lr) o))
           (Height r)))
     n
   :~: 'True
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (Node x a
-> AVL l -> Proxy n -> Proxy o -> LtN (Insert x a l) n :~: 'True
forall (x :: Nat) a (t :: Tree) (n :: Nat) (o :: Ordering).
(ProofLtNInsert' x a t n o, CmpNat x n ~ 'LT, LtN t n ~ 'True) =>
Node x a
-> AVL t -> Proxy n -> Proxy o -> LtN (Insert x a t) n :~: 'True
proofLtNInsert' Node x a
node AVL l
l Proxy n
pn Proxy o
po) (((LtN (Insert' x a ('ForkTree ll (Node ln lna) lr) o) n
   ~ 'True) =>
  LtN
    (Balance'
       ('ForkTree
          (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n1 a1) r)
       (UnbalancedState
          (Height (Insert' x a ('ForkTree ll (Node ln lna) lr) o))
          (Height r)))
    n
  :~: 'True)
 -> LtN
      (Balance'
         ('ForkTree
            (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n1 a1) r)
         (UnbalancedState
            (Height (Insert' x a ('ForkTree ll (Node ln lna) lr) o))
            (Height r)))
      n
    :~: 'True)
-> ((LtN (Insert' x a ('ForkTree ll (Node ln lna) lr) o) n
     ~ 'True) =>
    LtN
      (Balance'
         ('ForkTree
            (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n1 a1) r)
         (UnbalancedState
            (Height (Insert' x a ('ForkTree ll (Node ln lna) lr) o))
            (Height r)))
      n
    :~: 'True)
-> LtN
     (Balance'
        ('ForkTree
           (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n1 a1) r)
        (UnbalancedState
           (Height (Insert' x a ('ForkTree ll (Node ln lna) lr) o))
           (Height r)))
     n
   :~: 'True
forall a b. (a -> b) -> a -> b
$
      (LtN (Insert' x a ('ForkTree ll (Node ln lna) lr) o) n1 :~: 'True)
-> ((LtN (Insert' x a ('ForkTree ll (Node ln lna) lr) o) n1
     ~ 'True) =>
    LtN
      (Balance'
         ('ForkTree
            (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n1 a1) r)
         (UnbalancedState
            (Height (Insert' x a ('ForkTree ll (Node ln lna) lr) o))
            (Height r)))
      n
    :~: 'True)
-> LtN
     (Balance'
        ('ForkTree
           (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n1 a1) r)
        (UnbalancedState
           (Height (Insert' x a ('ForkTree ll (Node ln lna) lr) o))
           (Height r)))
     n
   :~: 'True
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (Node x a
-> AVL l -> Proxy n1 -> Proxy o -> LtN (Insert x a l) n1 :~: 'True
forall (x :: Nat) a (t :: Tree) (n :: Nat) (o :: Ordering).
(ProofLtNInsert' x a t n o, CmpNat x n ~ 'LT, LtN t n ~ 'True) =>
Node x a
-> AVL t -> Proxy n -> Proxy o -> LtN (Insert x a t) n :~: 'True
proofLtNInsert' Node x a
node AVL l
l (Proxy n1
forall {k} (t :: k). Proxy t
Proxy :: Proxy n1) Proxy o
po) (((LtN (Insert' x a ('ForkTree ll (Node ln lna) lr) o) n1
   ~ 'True) =>
  LtN
    (Balance'
       ('ForkTree
          (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n1 a1) r)
       (UnbalancedState
          (Height (Insert' x a ('ForkTree ll (Node ln lna) lr) o))
          (Height r)))
    n
  :~: 'True)
 -> LtN
      (Balance'
         ('ForkTree
            (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n1 a1) r)
         (UnbalancedState
            (Height (Insert' x a ('ForkTree ll (Node ln lna) lr) o))
            (Height r)))
      n
    :~: 'True)
-> ((LtN (Insert' x a ('ForkTree ll (Node ln lna) lr) o) n1
     ~ 'True) =>
    LtN
      (Balance'
         ('ForkTree
            (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n1 a1) r)
         (UnbalancedState
            (Height (Insert' x a ('ForkTree ll (Node ln lna) lr) o))
            (Height r)))
      n
    :~: 'True)
-> LtN
     (Balance'
        ('ForkTree
           (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n1 a1) r)
        (UnbalancedState
           (Height (Insert' x a ('ForkTree ll (Node ln lna) lr) o))
           (Height r)))
     n
   :~: 'True
forall a b. (a -> b) -> a -> b
$
        (LtN
   (Balance'
      ('ForkTree
         (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n1 a1) r)
      (UnbalancedState
         (Height (Insert' x a ('ForkTree ll (Node ln lna) lr) o))
         (Height r)))
   n
 :~: 'True)
-> ((LtN
       (Balance'
          ('ForkTree
             (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n1 a1) r)
          (UnbalancedState
             (Height (Insert' x a ('ForkTree ll (Node ln lna) lr) o))
             (Height r)))
       n
     ~ 'True) =>
    LtN
      (Balance'
         ('ForkTree
            (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n1 a1) r)
         (UnbalancedState
            (Height (Insert' x a ('ForkTree ll (Node ln lna) lr) o))
            (Height r)))
      n
    :~: 'True)
-> LtN
     (Balance'
        ('ForkTree
           (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n1 a1) r)
        (UnbalancedState
           (Height (Insert' x a ('ForkTree ll (Node ln lna) lr) o))
           (Height r)))
     n
   :~: 'True
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (AlmostAVL
  ('ForkTree
     (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n a) r)
-> Proxy n
-> LtN
     (Balance
        ('ForkTree
           (Insert' x a ('ForkTree ll (Node ln lna) 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 (Insert' x a ('ForkTree ll (Node ln lna) lr) o)
-> Node n a
-> AVL r
-> AlmostAVL
     ('ForkTree
        (Insert' x a ('ForkTree ll (Node ln lna) 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 (Insert' x a ('ForkTree ll (Node ln lna) lr) o)
AVL (Insert x a l)
l' Node n a
node' AVL r
r) Proxy n
pn) (LtN
   (Balance'
      ('ForkTree
         (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n1 a1) r)
      (UnbalancedState
         (Height (Insert' x a ('ForkTree ll (Node ln lna) lr) o))
         (Height r)))
   n
 ~ 'True) =>
LtN
  (Balance'
     ('ForkTree
        (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n1 a1) r)
     (UnbalancedState
        (Height (Insert' x a ('ForkTree ll (Node ln lna) 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 (Insert x a l)
l' = Node x a -> AVL l -> AVL (Insert x a l)
forall (x :: Nat) a (t :: Tree).
Insertable x a t =>
Node x a -> AVL t -> AVL (Insert x a t)
insert Node x a
node AVL l
l

instance
  ( CmpNat x n1 ~ 'GT,
    Show a,
    ProofLtNBalance ('ForkTree l (Node n1 a1) ('ForkTree 'EmptyTree (Node x a) 'EmptyTree)) n
  ) =>
  ProofLtNInsert' x a ('ForkTree l (Node n1 a1) 'EmptyTree) n 'GT
  where
  proofLtNInsert' :: (CmpNat x n ~ 'LT,
 LtN ('ForkTree l (Node n1 a1) 'EmptyTree) n ~ 'True) =>
Node x a
-> AVL ('ForkTree l (Node n1 a1) 'EmptyTree)
-> Proxy n
-> Proxy 'GT
-> LtN (Insert x a ('ForkTree l (Node n1 a1) 'EmptyTree)) n
   :~: 'True
proofLtNInsert' Node x a
node (ForkAVL AVL l
l Node n a
node' AVL r
_) Proxy n
pn Proxy 'GT
_ =
    (LtN
   (Balance'
      ('ForkTree
         l (Node n1 a1) ('ForkTree 'EmptyTree (Node x a) 'EmptyTree))
      (UnbalancedState (Height l) 1))
   n
 :~: 'True)
-> ((LtN
       (Balance'
          ('ForkTree
             l (Node n1 a1) ('ForkTree 'EmptyTree (Node x a) 'EmptyTree))
          (UnbalancedState (Height l) 1))
       n
     ~ 'True) =>
    LtN
      (Balance'
         ('ForkTree
            l (Node n1 a1) ('ForkTree 'EmptyTree (Node x a) 'EmptyTree))
         (UnbalancedState (Height l) 1))
      n
    :~: 'True)
-> LtN
     (Balance'
        ('ForkTree
           l (Node n1 a1) ('ForkTree 'EmptyTree (Node x a) 'EmptyTree))
        (UnbalancedState (Height l) 1))
     n
   :~: 'True
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (AlmostAVL
  ('ForkTree
     l (Node n a) ('ForkTree 'EmptyTree (Node x a) 'EmptyTree))
-> Proxy n
-> LtN
     (Balance
        ('ForkTree
           l (Node n a) ('ForkTree 'EmptyTree (Node x a) 'EmptyTree)))
     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 ('ForkTree 'EmptyTree (Node x a) 'EmptyTree)
-> AlmostAVL
     ('ForkTree
        l (Node n a) ('ForkTree 'EmptyTree (Node x a) 'EmptyTree))
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 'EmptyTree
-> Node x a
-> AVL 'EmptyTree
-> AVL ('ForkTree 'EmptyTree (Node x a) 'EmptyTree)
forall a (l :: Tree) (n :: Nat) (r :: Tree).
(Show a, LtN l n ~ 'True, GtN r n ~ 'True,
 BalancedHeights (Height l) (Height r) n ~ 'True) =>
AVL l -> Node n a -> AVL r -> AVL ('ForkTree l (Node n a) r)
ForkAVL AVL 'EmptyTree
EmptyAVL Node x a
node AVL 'EmptyTree
EmptyAVL)) Proxy n
pn) (LtN
   (Balance'
      ('ForkTree
         l (Node n1 a1) ('ForkTree 'EmptyTree (Node x a) 'EmptyTree))
      (UnbalancedState (Height l) 1))
   n
 ~ 'True) =>
LtN
  (Balance'
     ('ForkTree
        l (Node n1 a1) ('ForkTree 'EmptyTree (Node x a) 'EmptyTree))
     (UnbalancedState (Height l) 1))
  n
:~: 'True
forall {k} (a :: k). a :~: a
Refl

instance
  ( r ~ 'ForkTree rl (Node rn rna) rr,
    o ~ CmpNat x rn,
    CmpNat x n1 ~ 'GT,
    LtN r n ~ 'True,
    Insertable x a r,
    ProofLtNInsert' x a r n o,
    ProofLtNBalance ('ForkTree l (Node n1 a1) (Insert' x a r o)) n,
    ProofGtNInsert' x a r n1 o
  ) =>
  ProofLtNInsert' x a ('ForkTree l (Node n1 a1) ('ForkTree rl (Node rn rna) rr)) n 'GT
  where
  proofLtNInsert' :: (CmpNat x n ~ 'LT,
 LtN ('ForkTree l (Node n1 a1) ('ForkTree rl (Node rn rna) rr)) n
 ~ 'True) =>
Node x a
-> AVL ('ForkTree l (Node n1 a1) ('ForkTree rl (Node rn rna) rr))
-> Proxy n
-> Proxy 'GT
-> LtN
     (Insert
        x a ('ForkTree l (Node n1 a1) ('ForkTree rl (Node rn rna) rr)))
     n
   :~: 'True
proofLtNInsert' Node x a
node (ForkAVL AVL l
l Node n a
node' AVL r
r) Proxy n
pn Proxy 'GT
_ =
    (LtN (Insert' x a ('ForkTree rl (Node rn rna) rr) o) n :~: 'True)
-> ((LtN (Insert' x a ('ForkTree rl (Node rn rna) rr) o) n
     ~ 'True) =>
    LtN
      (Balance'
         ('ForkTree
            l (Node n1 a1) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))
         (UnbalancedState
            (Height l)
            (Height (Insert' x a ('ForkTree rl (Node rn rna) rr) o))))
      n
    :~: 'True)
-> LtN
     (Balance'
        ('ForkTree
           l (Node n1 a1) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))
        (UnbalancedState
           (Height l)
           (Height (Insert' x a ('ForkTree rl (Node rn rna) rr) o))))
     n
   :~: 'True
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (Node x a
-> AVL r -> Proxy n -> Proxy o -> LtN (Insert x a r) n :~: 'True
forall (x :: Nat) a (t :: Tree) (n :: Nat) (o :: Ordering).
(ProofLtNInsert' x a t n o, CmpNat x n ~ 'LT, LtN t n ~ 'True) =>
Node x a
-> AVL t -> Proxy n -> Proxy o -> LtN (Insert x a t) n :~: 'True
proofLtNInsert' Node x a
node AVL r
r Proxy n
pn Proxy o
po) (((LtN (Insert' x a ('ForkTree rl (Node rn rna) rr) o) n
   ~ 'True) =>
  LtN
    (Balance'
       ('ForkTree
          l (Node n1 a1) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))
       (UnbalancedState
          (Height l)
          (Height (Insert' x a ('ForkTree rl (Node rn rna) rr) o))))
    n
  :~: 'True)
 -> LtN
      (Balance'
         ('ForkTree
            l (Node n1 a1) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))
         (UnbalancedState
            (Height l)
            (Height (Insert' x a ('ForkTree rl (Node rn rna) rr) o))))
      n
    :~: 'True)
-> ((LtN (Insert' x a ('ForkTree rl (Node rn rna) rr) o) n
     ~ 'True) =>
    LtN
      (Balance'
         ('ForkTree
            l (Node n1 a1) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))
         (UnbalancedState
            (Height l)
            (Height (Insert' x a ('ForkTree rl (Node rn rna) rr) o))))
      n
    :~: 'True)
-> LtN
     (Balance'
        ('ForkTree
           l (Node n1 a1) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))
        (UnbalancedState
           (Height l)
           (Height (Insert' x a ('ForkTree rl (Node rn rna) rr) o))))
     n
   :~: 'True
forall a b. (a -> b) -> a -> b
$
      (GtN (Insert' x a ('ForkTree rl (Node rn rna) rr) o) n1 :~: 'True)
-> ((GtN (Insert' x a ('ForkTree rl (Node rn rna) rr) o) n1
     ~ 'True) =>
    LtN
      (Balance'
         ('ForkTree
            l (Node n1 a1) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))
         (UnbalancedState
            (Height l)
            (Height (Insert' x a ('ForkTree rl (Node rn rna) rr) o))))
      n
    :~: 'True)
-> LtN
     (Balance'
        ('ForkTree
           l (Node n1 a1) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))
        (UnbalancedState
           (Height l)
           (Height (Insert' x a ('ForkTree rl (Node rn rna) rr) o))))
     n
   :~: 'True
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (Node x a
-> AVL r -> Proxy n1 -> Proxy o -> GtN (Insert x a r) n1 :~: 'True
forall (x :: Nat) a (t :: Tree) (n :: Nat) (o :: Ordering).
(ProofGtNInsert' x a t n o, CmpNat x n ~ 'GT, GtN t n ~ 'True) =>
Node x a
-> AVL t -> Proxy n -> Proxy o -> GtN (Insert x a t) n :~: 'True
proofGtNInsert' Node x a
node AVL r
r (Proxy n1
forall {k} (t :: k). Proxy t
Proxy :: Proxy n1) Proxy o
po) (((GtN (Insert' x a ('ForkTree rl (Node rn rna) rr) o) n1
   ~ 'True) =>
  LtN
    (Balance'
       ('ForkTree
          l (Node n1 a1) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))
       (UnbalancedState
          (Height l)
          (Height (Insert' x a ('ForkTree rl (Node rn rna) rr) o))))
    n
  :~: 'True)
 -> LtN
      (Balance'
         ('ForkTree
            l (Node n1 a1) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))
         (UnbalancedState
            (Height l)
            (Height (Insert' x a ('ForkTree rl (Node rn rna) rr) o))))
      n
    :~: 'True)
-> ((GtN (Insert' x a ('ForkTree rl (Node rn rna) rr) o) n1
     ~ 'True) =>
    LtN
      (Balance'
         ('ForkTree
            l (Node n1 a1) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))
         (UnbalancedState
            (Height l)
            (Height (Insert' x a ('ForkTree rl (Node rn rna) rr) o))))
      n
    :~: 'True)
-> LtN
     (Balance'
        ('ForkTree
           l (Node n1 a1) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))
        (UnbalancedState
           (Height l)
           (Height (Insert' x a ('ForkTree rl (Node rn rna) rr) o))))
     n
   :~: 'True
forall a b. (a -> b) -> a -> b
$
        (LtN
   (Balance'
      ('ForkTree
         l (Node n1 a1) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))
      (UnbalancedState
         (Height l)
         (Height (Insert' x a ('ForkTree rl (Node rn rna) rr) o))))
   n
 :~: 'True)
-> ((LtN
       (Balance'
          ('ForkTree
             l (Node n1 a1) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))
          (UnbalancedState
             (Height l)
             (Height (Insert' x a ('ForkTree rl (Node rn rna) rr) o))))
       n
     ~ 'True) =>
    LtN
      (Balance'
         ('ForkTree
            l (Node n1 a1) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))
         (UnbalancedState
            (Height l)
            (Height (Insert' x a ('ForkTree rl (Node rn rna) rr) o))))
      n
    :~: 'True)
-> LtN
     (Balance'
        ('ForkTree
           l (Node n1 a1) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))
        (UnbalancedState
           (Height l)
           (Height (Insert' x a ('ForkTree rl (Node rn rna) rr) o))))
     n
   :~: 'True
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (AlmostAVL
  ('ForkTree
     l (Node n a) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))
-> Proxy n
-> LtN
     (Balance
        ('ForkTree
           l (Node n a) (Insert' x a ('ForkTree rl (Node rn rna) 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 (Insert' x a ('ForkTree rl (Node rn rna) rr) o)
-> AlmostAVL
     ('ForkTree
        l (Node n a) (Insert' x a ('ForkTree rl (Node rn rna) 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 (Insert' x a ('ForkTree rl (Node rn rna) rr) o)
AVL (Insert x a r)
r') Proxy n
pn) (LtN
   (Balance'
      ('ForkTree
         l (Node n1 a1) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))
      (UnbalancedState
         (Height l)
         (Height (Insert' x a ('ForkTree rl (Node rn rna) rr) o))))
   n
 ~ 'True) =>
LtN
  (Balance'
     ('ForkTree
        l (Node n1 a1) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))
     (UnbalancedState
        (Height l)
        (Height (Insert' x a ('ForkTree rl (Node rn rna) 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 (Insert x a r)
r' = Node x a -> AVL r -> AVL (Insert x a r)
forall (x :: Nat) a (t :: Tree).
Insertable x a t =>
Node x a -> AVL t -> AVL (Insert x a t)
insert Node x a
node AVL r
r

-- | Prove that inserting a node with key @x@ (greater than @n@) and element value @a@
-- in an `AVL` @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 ProofGtNInsert' (x :: Nat) (a :: Type) (t :: Tree) (n :: Nat) (o :: Ordering) where
  proofGtNInsert' ::
    (CmpNat x n ~ 'GT, GtN t n ~ 'True) =>
    Node x a ->
    AVL t ->
    Proxy n ->
    Proxy o ->
    GtN (Insert x a t) n :~: 'True

instance
  (CmpNat x n1 ~ 'EQ) =>
  ProofGtNInsert' x a ('ForkTree l (Node n1 a1) r) n 'EQ
  where
  proofGtNInsert' :: (CmpNat x n ~ 'GT, GtN ('ForkTree l (Node n1 a1) r) n ~ 'True) =>
Node x a
-> AVL ('ForkTree l (Node n1 a1) r)
-> Proxy n
-> Proxy 'EQ
-> GtN (Insert x a ('ForkTree l (Node n1 a1) r)) n :~: 'True
proofGtNInsert' Node x a
_ AVL ('ForkTree l (Node n1 a1) r)
_ Proxy n
_ Proxy 'EQ
_ = GtN (Insert x a ('ForkTree l (Node n1 a1) r)) n :~: 'True
forall {k} (a :: k). a :~: a
Refl

instance
  ( CmpNat x n1 ~ 'LT,
    Show a,
    ProofGtNBalance ('ForkTree ('ForkTree 'EmptyTree (Node x a) 'EmptyTree) (Node n1 a1) r) n
  ) =>
  ProofGtNInsert' x a ('ForkTree 'EmptyTree (Node n1 a1) r) n 'LT
  where
  proofGtNInsert' :: (CmpNat x n ~ 'GT,
 GtN ('ForkTree 'EmptyTree (Node n1 a1) r) n ~ 'True) =>
Node x a
-> AVL ('ForkTree 'EmptyTree (Node n1 a1) r)
-> Proxy n
-> Proxy 'LT
-> GtN (Insert x a ('ForkTree 'EmptyTree (Node n1 a1) r)) n
   :~: 'True
proofGtNInsert' Node x a
node (ForkAVL AVL l
_ Node n a
node' AVL r
r) Proxy n
pn Proxy 'LT
_ =
    (GtN
   (Balance'
      ('ForkTree
         ('ForkTree 'EmptyTree (Node x a) 'EmptyTree) (Node n1 a1) r)
      (UnbalancedState 1 (Height r)))
   n
 :~: 'True)
-> ((GtN
       (Balance'
          ('ForkTree
             ('ForkTree 'EmptyTree (Node x a) 'EmptyTree) (Node n1 a1) r)
          (UnbalancedState 1 (Height r)))
       n
     ~ 'True) =>
    GtN
      (Balance'
         ('ForkTree
            ('ForkTree 'EmptyTree (Node x a) 'EmptyTree) (Node n1 a1) r)
         (UnbalancedState 1 (Height r)))
      n
    :~: 'True)
-> GtN
     (Balance'
        ('ForkTree
           ('ForkTree 'EmptyTree (Node x a) 'EmptyTree) (Node n1 a1) r)
        (UnbalancedState 1 (Height r)))
     n
   :~: 'True
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (AlmostAVL
  ('ForkTree
     ('ForkTree 'EmptyTree (Node x a) 'EmptyTree) (Node n a) r)
-> Proxy n
-> GtN
     (Balance
        ('ForkTree
           ('ForkTree 'EmptyTree (Node x a) 'EmptyTree) (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 ('ForkTree 'EmptyTree (Node x a) 'EmptyTree)
-> Node n a
-> AVL r
-> AlmostAVL
     ('ForkTree
        ('ForkTree 'EmptyTree (Node x a) 'EmptyTree) (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 'EmptyTree
-> Node x a
-> AVL 'EmptyTree
-> AVL ('ForkTree 'EmptyTree (Node x a) 'EmptyTree)
forall a (l :: Tree) (n :: Nat) (r :: Tree).
(Show a, LtN l n ~ 'True, GtN r n ~ 'True,
 BalancedHeights (Height l) (Height r) n ~ 'True) =>
AVL l -> Node n a -> AVL r -> AVL ('ForkTree l (Node n a) r)
ForkAVL AVL 'EmptyTree
EmptyAVL Node x a
node AVL 'EmptyTree
EmptyAVL) Node n a
node' AVL r
r) Proxy n
pn) (GtN
   (Balance'
      ('ForkTree
         ('ForkTree 'EmptyTree (Node x a) 'EmptyTree) (Node n1 a1) r)
      (UnbalancedState 1 (Height r)))
   n
 ~ 'True) =>
GtN
  (Balance'
     ('ForkTree
        ('ForkTree 'EmptyTree (Node x a) 'EmptyTree) (Node n1 a1) r)
     (UnbalancedState 1 (Height r)))
  n
:~: 'True
forall {k} (a :: k). a :~: a
Refl

instance
  ( l ~ 'ForkTree ll (Node ln lna) lr,
    o ~ CmpNat x ln,
    CmpNat x n1 ~ 'LT,
    GtN l n ~ 'True,
    Insertable x a l,
    ProofGtNInsert' x a l n o,
    ProofGtNBalance ('ForkTree (Insert' x a l o) (Node n1 a1) r) n,
    ProofLtNInsert' x a l n1 o
  ) =>
  ProofGtNInsert' x a ('ForkTree ('ForkTree ll (Node ln lna) lr) (Node n1 a1) r) n 'LT
  where
  proofGtNInsert' :: (CmpNat x n ~ 'GT,
 GtN ('ForkTree ('ForkTree ll (Node ln lna) lr) (Node n1 a1) r) n
 ~ 'True) =>
Node x a
-> AVL ('ForkTree ('ForkTree ll (Node ln lna) lr) (Node n1 a1) r)
-> Proxy n
-> Proxy 'LT
-> GtN
     (Insert
        x a ('ForkTree ('ForkTree ll (Node ln lna) lr) (Node n1 a1) r))
     n
   :~: 'True
proofGtNInsert' Node x a
node (ForkAVL AVL l
l Node n a
node' AVL r
r) Proxy n
pn Proxy 'LT
_ =
    (GtN (Insert' x a ('ForkTree ll (Node ln lna) lr) o) n :~: 'True)
-> ((GtN (Insert' x a ('ForkTree ll (Node ln lna) lr) o) n
     ~ 'True) =>
    GtN
      (Balance'
         ('ForkTree
            (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n1 a1) r)
         (UnbalancedState
            (Height (Insert' x a ('ForkTree ll (Node ln lna) lr) o))
            (Height r)))
      n
    :~: 'True)
-> GtN
     (Balance'
        ('ForkTree
           (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n1 a1) r)
        (UnbalancedState
           (Height (Insert' x a ('ForkTree ll (Node ln lna) lr) o))
           (Height r)))
     n
   :~: 'True
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (Node x a
-> AVL l -> Proxy n -> Proxy o -> GtN (Insert x a l) n :~: 'True
forall (x :: Nat) a (t :: Tree) (n :: Nat) (o :: Ordering).
(ProofGtNInsert' x a t n o, CmpNat x n ~ 'GT, GtN t n ~ 'True) =>
Node x a
-> AVL t -> Proxy n -> Proxy o -> GtN (Insert x a t) n :~: 'True
proofGtNInsert' Node x a
node AVL l
l Proxy n
pn Proxy o
po) (((GtN (Insert' x a ('ForkTree ll (Node ln lna) lr) o) n
   ~ 'True) =>
  GtN
    (Balance'
       ('ForkTree
          (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n1 a1) r)
       (UnbalancedState
          (Height (Insert' x a ('ForkTree ll (Node ln lna) lr) o))
          (Height r)))
    n
  :~: 'True)
 -> GtN
      (Balance'
         ('ForkTree
            (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n1 a1) r)
         (UnbalancedState
            (Height (Insert' x a ('ForkTree ll (Node ln lna) lr) o))
            (Height r)))
      n
    :~: 'True)
-> ((GtN (Insert' x a ('ForkTree ll (Node ln lna) lr) o) n
     ~ 'True) =>
    GtN
      (Balance'
         ('ForkTree
            (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n1 a1) r)
         (UnbalancedState
            (Height (Insert' x a ('ForkTree ll (Node ln lna) lr) o))
            (Height r)))
      n
    :~: 'True)
-> GtN
     (Balance'
        ('ForkTree
           (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n1 a1) r)
        (UnbalancedState
           (Height (Insert' x a ('ForkTree ll (Node ln lna) lr) o))
           (Height r)))
     n
   :~: 'True
forall a b. (a -> b) -> a -> b
$
      (LtN (Insert' x a ('ForkTree ll (Node ln lna) lr) o) n1 :~: 'True)
-> ((LtN (Insert' x a ('ForkTree ll (Node ln lna) lr) o) n1
     ~ 'True) =>
    GtN
      (Balance'
         ('ForkTree
            (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n1 a1) r)
         (UnbalancedState
            (Height (Insert' x a ('ForkTree ll (Node ln lna) lr) o))
            (Height r)))
      n
    :~: 'True)
-> GtN
     (Balance'
        ('ForkTree
           (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n1 a1) r)
        (UnbalancedState
           (Height (Insert' x a ('ForkTree ll (Node ln lna) lr) o))
           (Height r)))
     n
   :~: 'True
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (Node x a
-> AVL l -> Proxy n1 -> Proxy o -> LtN (Insert x a l) n1 :~: 'True
forall (x :: Nat) a (t :: Tree) (n :: Nat) (o :: Ordering).
(ProofLtNInsert' x a t n o, CmpNat x n ~ 'LT, LtN t n ~ 'True) =>
Node x a
-> AVL t -> Proxy n -> Proxy o -> LtN (Insert x a t) n :~: 'True
proofLtNInsert' Node x a
node AVL l
l (Proxy n1
forall {k} (t :: k). Proxy t
Proxy :: Proxy n1) Proxy o
po) (((LtN (Insert' x a ('ForkTree ll (Node ln lna) lr) o) n1
   ~ 'True) =>
  GtN
    (Balance'
       ('ForkTree
          (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n1 a1) r)
       (UnbalancedState
          (Height (Insert' x a ('ForkTree ll (Node ln lna) lr) o))
          (Height r)))
    n
  :~: 'True)
 -> GtN
      (Balance'
         ('ForkTree
            (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n1 a1) r)
         (UnbalancedState
            (Height (Insert' x a ('ForkTree ll (Node ln lna) lr) o))
            (Height r)))
      n
    :~: 'True)
-> ((LtN (Insert' x a ('ForkTree ll (Node ln lna) lr) o) n1
     ~ 'True) =>
    GtN
      (Balance'
         ('ForkTree
            (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n1 a1) r)
         (UnbalancedState
            (Height (Insert' x a ('ForkTree ll (Node ln lna) lr) o))
            (Height r)))
      n
    :~: 'True)
-> GtN
     (Balance'
        ('ForkTree
           (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n1 a1) r)
        (UnbalancedState
           (Height (Insert' x a ('ForkTree ll (Node ln lna) lr) o))
           (Height r)))
     n
   :~: 'True
forall a b. (a -> b) -> a -> b
$
        (GtN
   (Balance'
      ('ForkTree
         (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n1 a1) r)
      (UnbalancedState
         (Height (Insert' x a ('ForkTree ll (Node ln lna) lr) o))
         (Height r)))
   n
 :~: 'True)
-> ((GtN
       (Balance'
          ('ForkTree
             (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n1 a1) r)
          (UnbalancedState
             (Height (Insert' x a ('ForkTree ll (Node ln lna) lr) o))
             (Height r)))
       n
     ~ 'True) =>
    GtN
      (Balance'
         ('ForkTree
            (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n1 a1) r)
         (UnbalancedState
            (Height (Insert' x a ('ForkTree ll (Node ln lna) lr) o))
            (Height r)))
      n
    :~: 'True)
-> GtN
     (Balance'
        ('ForkTree
           (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n1 a1) r)
        (UnbalancedState
           (Height (Insert' x a ('ForkTree ll (Node ln lna) lr) o))
           (Height r)))
     n
   :~: 'True
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (AlmostAVL
  ('ForkTree
     (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n a) r)
-> Proxy n
-> GtN
     (Balance
        ('ForkTree
           (Insert' x a ('ForkTree ll (Node ln lna) 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 (Insert' x a ('ForkTree ll (Node ln lna) lr) o)
-> Node n a
-> AVL r
-> AlmostAVL
     ('ForkTree
        (Insert' x a ('ForkTree ll (Node ln lna) 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 (Insert' x a ('ForkTree ll (Node ln lna) lr) o)
AVL (Insert x a l)
l' Node n a
node' AVL r
r) Proxy n
pn) (GtN
   (Balance'
      ('ForkTree
         (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n1 a1) r)
      (UnbalancedState
         (Height (Insert' x a ('ForkTree ll (Node ln lna) lr) o))
         (Height r)))
   n
 ~ 'True) =>
GtN
  (Balance'
     ('ForkTree
        (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n1 a1) r)
     (UnbalancedState
        (Height (Insert' x a ('ForkTree ll (Node ln lna) 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 (Insert x a l)
l' = Node x a -> AVL l -> AVL (Insert x a l)
forall (x :: Nat) a (t :: Tree).
Insertable x a t =>
Node x a -> AVL t -> AVL (Insert x a t)
insert Node x a
node AVL l
l

instance
  ( CmpNat x n1 ~ 'GT,
    Show a,
    ProofGtNBalance ('ForkTree l (Node n1 a1) ('ForkTree 'EmptyTree (Node x a) 'EmptyTree)) n
  ) =>
  ProofGtNInsert' x a ('ForkTree l (Node n1 a1) 'EmptyTree) n 'GT
  where
  proofGtNInsert' :: (CmpNat x n ~ 'GT,
 GtN ('ForkTree l (Node n1 a1) 'EmptyTree) n ~ 'True) =>
Node x a
-> AVL ('ForkTree l (Node n1 a1) 'EmptyTree)
-> Proxy n
-> Proxy 'GT
-> GtN (Insert x a ('ForkTree l (Node n1 a1) 'EmptyTree)) n
   :~: 'True
proofGtNInsert' Node x a
node (ForkAVL AVL l
l Node n a
node' AVL r
_) Proxy n
pn Proxy 'GT
_ =
    (GtN
   (Balance'
      ('ForkTree
         l (Node n1 a1) ('ForkTree 'EmptyTree (Node x a) 'EmptyTree))
      (UnbalancedState (Height l) 1))
   n
 :~: 'True)
-> ((GtN
       (Balance'
          ('ForkTree
             l (Node n1 a1) ('ForkTree 'EmptyTree (Node x a) 'EmptyTree))
          (UnbalancedState (Height l) 1))
       n
     ~ 'True) =>
    GtN
      (Balance'
         ('ForkTree
            l (Node n1 a1) ('ForkTree 'EmptyTree (Node x a) 'EmptyTree))
         (UnbalancedState (Height l) 1))
      n
    :~: 'True)
-> GtN
     (Balance'
        ('ForkTree
           l (Node n1 a1) ('ForkTree 'EmptyTree (Node x a) 'EmptyTree))
        (UnbalancedState (Height l) 1))
     n
   :~: 'True
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (AlmostAVL
  ('ForkTree
     l (Node n a) ('ForkTree 'EmptyTree (Node x a) 'EmptyTree))
-> Proxy n
-> GtN
     (Balance
        ('ForkTree
           l (Node n a) ('ForkTree 'EmptyTree (Node x a) 'EmptyTree)))
     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 ('ForkTree 'EmptyTree (Node x a) 'EmptyTree)
-> AlmostAVL
     ('ForkTree
        l (Node n a) ('ForkTree 'EmptyTree (Node x a) 'EmptyTree))
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 'EmptyTree
-> Node x a
-> AVL 'EmptyTree
-> AVL ('ForkTree 'EmptyTree (Node x a) 'EmptyTree)
forall a (l :: Tree) (n :: Nat) (r :: Tree).
(Show a, LtN l n ~ 'True, GtN r n ~ 'True,
 BalancedHeights (Height l) (Height r) n ~ 'True) =>
AVL l -> Node n a -> AVL r -> AVL ('ForkTree l (Node n a) r)
ForkAVL AVL 'EmptyTree
EmptyAVL Node x a
node AVL 'EmptyTree
EmptyAVL)) Proxy n
pn) (GtN
   (Balance'
      ('ForkTree
         l (Node n1 a1) ('ForkTree 'EmptyTree (Node x a) 'EmptyTree))
      (UnbalancedState (Height l) 1))
   n
 ~ 'True) =>
GtN
  (Balance'
     ('ForkTree
        l (Node n1 a1) ('ForkTree 'EmptyTree (Node x a) 'EmptyTree))
     (UnbalancedState (Height l) 1))
  n
:~: 'True
forall {k} (a :: k). a :~: a
Refl

instance
  ( r ~ 'ForkTree rl (Node rn rna) rr,
    o ~ CmpNat x rn,
    CmpNat x n1 ~ 'GT,
    GtN r n ~ 'True,
    Insertable x a r,
    ProofGtNInsert' x a r n o,
    ProofGtNBalance ('ForkTree l (Node n1 a1) (Insert' x a r o)) n,
    ProofGtNInsert' x a r n1 o
  ) =>
  ProofGtNInsert' x a ('ForkTree l (Node n1 a1) ('ForkTree rl (Node rn rna) rr)) n 'GT
  where
  proofGtNInsert' :: (CmpNat x n ~ 'GT,
 GtN ('ForkTree l (Node n1 a1) ('ForkTree rl (Node rn rna) rr)) n
 ~ 'True) =>
Node x a
-> AVL ('ForkTree l (Node n1 a1) ('ForkTree rl (Node rn rna) rr))
-> Proxy n
-> Proxy 'GT
-> GtN
     (Insert
        x a ('ForkTree l (Node n1 a1) ('ForkTree rl (Node rn rna) rr)))
     n
   :~: 'True
proofGtNInsert' Node x a
node (ForkAVL AVL l
l Node n a
node' AVL r
r) Proxy n
pn Proxy 'GT
_ =
    (GtN (Insert' x a ('ForkTree rl (Node rn rna) rr) o) n :~: 'True)
-> ((GtN (Insert' x a ('ForkTree rl (Node rn rna) rr) o) n
     ~ 'True) =>
    GtN
      (Balance'
         ('ForkTree
            l (Node n1 a1) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))
         (UnbalancedState
            (Height l)
            (Height (Insert' x a ('ForkTree rl (Node rn rna) rr) o))))
      n
    :~: 'True)
-> GtN
     (Balance'
        ('ForkTree
           l (Node n1 a1) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))
        (UnbalancedState
           (Height l)
           (Height (Insert' x a ('ForkTree rl (Node rn rna) rr) o))))
     n
   :~: 'True
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (Node x a
-> AVL r -> Proxy n -> Proxy o -> GtN (Insert x a r) n :~: 'True
forall (x :: Nat) a (t :: Tree) (n :: Nat) (o :: Ordering).
(ProofGtNInsert' x a t n o, CmpNat x n ~ 'GT, GtN t n ~ 'True) =>
Node x a
-> AVL t -> Proxy n -> Proxy o -> GtN (Insert x a t) n :~: 'True
proofGtNInsert' Node x a
node AVL r
r Proxy n
pn Proxy o
po) (((GtN (Insert' x a ('ForkTree rl (Node rn rna) rr) o) n
   ~ 'True) =>
  GtN
    (Balance'
       ('ForkTree
          l (Node n1 a1) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))
       (UnbalancedState
          (Height l)
          (Height (Insert' x a ('ForkTree rl (Node rn rna) rr) o))))
    n
  :~: 'True)
 -> GtN
      (Balance'
         ('ForkTree
            l (Node n1 a1) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))
         (UnbalancedState
            (Height l)
            (Height (Insert' x a ('ForkTree rl (Node rn rna) rr) o))))
      n
    :~: 'True)
-> ((GtN (Insert' x a ('ForkTree rl (Node rn rna) rr) o) n
     ~ 'True) =>
    GtN
      (Balance'
         ('ForkTree
            l (Node n1 a1) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))
         (UnbalancedState
            (Height l)
            (Height (Insert' x a ('ForkTree rl (Node rn rna) rr) o))))
      n
    :~: 'True)
-> GtN
     (Balance'
        ('ForkTree
           l (Node n1 a1) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))
        (UnbalancedState
           (Height l)
           (Height (Insert' x a ('ForkTree rl (Node rn rna) rr) o))))
     n
   :~: 'True
forall a b. (a -> b) -> a -> b
$
      (GtN (Insert' x a ('ForkTree rl (Node rn rna) rr) o) n1 :~: 'True)
-> ((GtN (Insert' x a ('ForkTree rl (Node rn rna) rr) o) n1
     ~ 'True) =>
    GtN
      (Balance'
         ('ForkTree
            l (Node n1 a1) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))
         (UnbalancedState
            (Height l)
            (Height (Insert' x a ('ForkTree rl (Node rn rna) rr) o))))
      n
    :~: 'True)
-> GtN
     (Balance'
        ('ForkTree
           l (Node n1 a1) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))
        (UnbalancedState
           (Height l)
           (Height (Insert' x a ('ForkTree rl (Node rn rna) rr) o))))
     n
   :~: 'True
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (Node x a
-> AVL r -> Proxy n1 -> Proxy o -> GtN (Insert x a r) n1 :~: 'True
forall (x :: Nat) a (t :: Tree) (n :: Nat) (o :: Ordering).
(ProofGtNInsert' x a t n o, CmpNat x n ~ 'GT, GtN t n ~ 'True) =>
Node x a
-> AVL t -> Proxy n -> Proxy o -> GtN (Insert x a t) n :~: 'True
proofGtNInsert' Node x a
node AVL r
r (Proxy n1
forall {k} (t :: k). Proxy t
Proxy :: Proxy n1) Proxy o
po) (((GtN (Insert' x a ('ForkTree rl (Node rn rna) rr) o) n1
   ~ 'True) =>
  GtN
    (Balance'
       ('ForkTree
          l (Node n1 a1) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))
       (UnbalancedState
          (Height l)
          (Height (Insert' x a ('ForkTree rl (Node rn rna) rr) o))))
    n
  :~: 'True)
 -> GtN
      (Balance'
         ('ForkTree
            l (Node n1 a1) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))
         (UnbalancedState
            (Height l)
            (Height (Insert' x a ('ForkTree rl (Node rn rna) rr) o))))
      n
    :~: 'True)
-> ((GtN (Insert' x a ('ForkTree rl (Node rn rna) rr) o) n1
     ~ 'True) =>
    GtN
      (Balance'
         ('ForkTree
            l (Node n1 a1) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))
         (UnbalancedState
            (Height l)
            (Height (Insert' x a ('ForkTree rl (Node rn rna) rr) o))))
      n
    :~: 'True)
-> GtN
     (Balance'
        ('ForkTree
           l (Node n1 a1) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))
        (UnbalancedState
           (Height l)
           (Height (Insert' x a ('ForkTree rl (Node rn rna) rr) o))))
     n
   :~: 'True
forall a b. (a -> b) -> a -> b
$
        (GtN
   (Balance'
      ('ForkTree
         l (Node n1 a1) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))
      (UnbalancedState
         (Height l)
         (Height (Insert' x a ('ForkTree rl (Node rn rna) rr) o))))
   n
 :~: 'True)
-> ((GtN
       (Balance'
          ('ForkTree
             l (Node n1 a1) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))
          (UnbalancedState
             (Height l)
             (Height (Insert' x a ('ForkTree rl (Node rn rna) rr) o))))
       n
     ~ 'True) =>
    GtN
      (Balance'
         ('ForkTree
            l (Node n1 a1) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))
         (UnbalancedState
            (Height l)
            (Height (Insert' x a ('ForkTree rl (Node rn rna) rr) o))))
      n
    :~: 'True)
-> GtN
     (Balance'
        ('ForkTree
           l (Node n1 a1) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))
        (UnbalancedState
           (Height l)
           (Height (Insert' x a ('ForkTree rl (Node rn rna) rr) o))))
     n
   :~: 'True
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (AlmostAVL
  ('ForkTree
     l (Node n a) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))
-> Proxy n
-> GtN
     (Balance
        ('ForkTree
           l (Node n a) (Insert' x a ('ForkTree rl (Node rn rna) 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 (Insert' x a ('ForkTree rl (Node rn rna) rr) o)
-> AlmostAVL
     ('ForkTree
        l (Node n a) (Insert' x a ('ForkTree rl (Node rn rna) 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 (Insert' x a ('ForkTree rl (Node rn rna) rr) o)
AVL (Insert x a r)
r') Proxy n
pn) (GtN
   (Balance'
      ('ForkTree
         l (Node n1 a1) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))
      (UnbalancedState
         (Height l)
         (Height (Insert' x a ('ForkTree rl (Node rn rna) rr) o))))
   n
 ~ 'True) =>
GtN
  (Balance'
     ('ForkTree
        l (Node n1 a1) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))
     (UnbalancedState
        (Height l)
        (Height (Insert' x a ('ForkTree rl (Node rn rna) 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 (Insert x a r)
r' = Node x a -> AVL r -> AVL (Insert x a r)
forall (x :: Nat) a (t :: Tree).
Insertable x a t =>
Node x a -> AVL t -> AVL (Insert x a t)
insert Node x a
node AVL r
r

-- | This type class provides the functionality to insert a node with key @x@ and value type @a@
-- in an `AVL` @t@.
-- The insertion is defined at the value level and the type level.
-- The returned tree verifies the @BST@/@AVL@ restrictions.
class Insertable (x :: Nat) (a :: Type) (t :: Tree) where
  type Insert (x :: Nat) (a :: Type) (t :: Tree) :: Tree
  insert :: Node x a -> AVL t -> AVL (Insert x a t)

instance
  (Show a) =>
  Insertable x a 'EmptyTree
  where
  type Insert x a 'EmptyTree = 'ForkTree 'EmptyTree (Node x a) 'EmptyTree
  insert :: Node x a -> AVL 'EmptyTree -> AVL (Insert x a 'EmptyTree)
insert Node x a
node AVL 'EmptyTree
_ = AVL 'EmptyTree
-> Node x a
-> AVL 'EmptyTree
-> AVL ('ForkTree 'EmptyTree (Node x a) 'EmptyTree)
forall a (l :: Tree) (n :: Nat) (r :: Tree).
(Show a, LtN l n ~ 'True, GtN r n ~ 'True,
 BalancedHeights (Height l) (Height r) n ~ 'True) =>
AVL l -> Node n a -> AVL r -> AVL ('ForkTree l (Node n a) r)
ForkAVL AVL 'EmptyTree
EmptyAVL Node x a
node' AVL 'EmptyTree
EmptyAVL
    where
      node' :: Node x a
node' = Proxy x -> a -> Node x a
forall (k :: Nat) a. Proxy k -> a -> Node k a
mkNode (Proxy x
forall {k} (t :: k). Proxy t
Proxy :: Proxy x) (Node x a -> a
forall (k :: Nat) a. Node k a -> a
getValue Node x a
node)

instance
  ( o ~ CmpNat x n,
    Insertable' x a ('ForkTree l (Node n a1) r) o
  ) =>
  Insertable x a ('ForkTree l (Node n a1) r)
  where
  type Insert x a ('ForkTree l (Node n a1) r) = Insert' x a ('ForkTree l (Node n a1) r) (CmpNat x n)
  insert :: Node x a
-> AVL ('ForkTree l (Node n a1) r)
-> AVL (Insert x a ('ForkTree l (Node n a1) r))
insert Node x a
node AVL ('ForkTree l (Node n a1) r)
t = Node x a
-> AVL ('ForkTree l (Node n a1) r)
-> Proxy o
-> AVL (Insert' x a ('ForkTree l (Node n a1) r) o)
forall (x :: Nat) a (t :: Tree) (o :: Ordering).
Insertable' x a t o =>
Node x a -> AVL t -> Proxy o -> AVL (Insert' x a t o)
insert' Node x a
node 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 insert a node with key @x@ and value type @a@
-- in a non empty `AVL` @t@.
-- It's only used by the 'Insertable' 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 Insertable' (x :: Nat) (a :: Type) (t :: Tree) (o :: Ordering) where
  type Insert' (x :: Nat) (a :: Type) (t :: Tree) (o :: Ordering) :: Tree
  insert' :: Node x a -> AVL t -> Proxy o -> AVL (Insert' x a t o)

instance
  (Show a) =>
  Insertable' x a ('ForkTree l (Node n a1) r) 'EQ
  where
  type Insert' x a ('ForkTree l (Node n a1) r) 'EQ = 'ForkTree l (Node n a) r
  insert' :: Node x a
-> AVL ('ForkTree l (Node n a1) r)
-> Proxy 'EQ
-> AVL (Insert' x a ('ForkTree l (Node n a1) r) 'EQ)
insert' Node x a
node (ForkAVL AVL l
l Node n a
_ AVL r
r) Proxy 'EQ
_ = AVL l -> Node n a -> AVL r -> AVL ('ForkTree l (Node n a) r)
forall a (l :: Tree) (n :: Nat) (r :: Tree).
(Show a, LtN l n ~ 'True, GtN r n ~ 'True,
 BalancedHeights (Height l) (Height r) n ~ 'True) =>
AVL l -> Node n a -> AVL r -> AVL ('ForkTree l (Node n a) r)
ForkAVL AVL l
l Node n a
node' AVL r
r
    where
      node' :: Node n a
node' = Proxy n -> a -> Node n a
forall (k :: Nat) a. Proxy k -> a -> Node k a
mkNode (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n) (Node x a -> a
forall (k :: Nat) a. Node k a -> a
getValue Node x a
node)

instance
  ( CmpNat x n ~ 'LT,
    Show a,
    Balanceable ('ForkTree ('ForkTree 'EmptyTree (Node x a) 'EmptyTree) (Node n a1) r)
  ) =>
  Insertable' x a ('ForkTree 'EmptyTree (Node n a1) r) 'LT
  where
  type Insert' x a ('ForkTree 'EmptyTree (Node n a1) r) 'LT = Balance ('ForkTree ('ForkTree 'EmptyTree (Node x a) 'EmptyTree) (Node n a1) r)
  insert' :: Node x a
-> AVL ('ForkTree 'EmptyTree (Node n a1) r)
-> Proxy 'LT
-> AVL (Insert' x a ('ForkTree 'EmptyTree (Node n a1) r) 'LT)
insert' Node x a
node (ForkAVL AVL l
_ Node n a
node' AVL r
r) Proxy 'LT
_ = AlmostAVL
  ('ForkTree
     ('ForkTree 'EmptyTree (Node x a) 'EmptyTree) (Node n a) r)
-> AVL
     (Balance
        ('ForkTree
           ('ForkTree 'EmptyTree (Node x a) 'EmptyTree) (Node n a) r))
forall (t :: Tree). Balanceable t => AlmostAVL t -> AVL (Balance t)
balance (AVL ('ForkTree 'EmptyTree (Node x a) 'EmptyTree)
-> Node n a
-> AVL r
-> AlmostAVL
     ('ForkTree
        ('ForkTree 'EmptyTree (Node x a) 'EmptyTree) (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 'EmptyTree
-> Node x a
-> AVL 'EmptyTree
-> AVL ('ForkTree 'EmptyTree (Node x a) 'EmptyTree)
forall a (l :: Tree) (n :: Nat) (r :: Tree).
(Show a, LtN l n ~ 'True, GtN r n ~ 'True,
 BalancedHeights (Height l) (Height r) n ~ 'True) =>
AVL l -> Node n a -> AVL r -> AVL ('ForkTree l (Node n a) r)
ForkAVL AVL 'EmptyTree
EmptyAVL Node x a
node AVL 'EmptyTree
EmptyAVL) Node n a
node' AVL r
r)

instance
  ( l ~ 'ForkTree ll (Node ln lna) lr,
    o ~ CmpNat x ln,
    CmpNat x n ~ 'LT,
    Insertable' x a l o,
    Balanceable ('ForkTree (Insert' x a l o) (Node n a1) r),
    ProofLtNInsert' x a l n o
  ) =>
  Insertable' x a ('ForkTree ('ForkTree ll (Node ln lna) lr) (Node n a1) r) 'LT
  where
  type
    Insert' x a ('ForkTree ('ForkTree ll (Node ln lna) lr) (Node n a1) r) 'LT =
      Balance ('ForkTree (Insert' x a ('ForkTree ll (Node ln lna) lr) (CmpNat x ln)) (Node n a1) r)
  insert' :: Node x a
-> AVL ('ForkTree ('ForkTree ll (Node ln lna) lr) (Node n a1) r)
-> Proxy 'LT
-> AVL
     (Insert'
        x a ('ForkTree ('ForkTree ll (Node ln lna) lr) (Node n a1) r) 'LT)
insert' Node x a
node (ForkAVL AVL l
l Node n a
node' AVL r
r) Proxy 'LT
_ =
    (LtN (Insert' x a ('ForkTree ll (Node ln lna) lr) o) n :~: 'True)
-> ((LtN (Insert' x a ('ForkTree ll (Node ln lna) lr) o) n
     ~ 'True) =>
    AVL
      (Balance'
         ('ForkTree
            (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n a1) r)
         (UnbalancedState
            (Height (Insert' x a ('ForkTree ll (Node ln lna) lr) o))
            (Height r))))
-> AVL
     (Balance'
        ('ForkTree
           (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n a1) r)
        (UnbalancedState
           (Height (Insert' x a ('ForkTree ll (Node ln lna) lr) o))
           (Height r)))
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (Node x a
-> AVL l -> Proxy n -> Proxy o -> LtN (Insert x a l) n :~: 'True
forall (x :: Nat) a (t :: Tree) (n :: Nat) (o :: Ordering).
(ProofLtNInsert' x a t n o, CmpNat x n ~ 'LT, LtN t n ~ 'True) =>
Node x a
-> AVL t -> Proxy n -> Proxy o -> LtN (Insert x a t) n :~: 'True
proofLtNInsert' Node x a
node AVL l
l (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n) Proxy o
po) (((LtN (Insert' x a ('ForkTree ll (Node ln lna) lr) o) n
   ~ 'True) =>
  AVL
    (Balance'
       ('ForkTree
          (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n a1) r)
       (UnbalancedState
          (Height (Insert' x a ('ForkTree ll (Node ln lna) lr) o))
          (Height r))))
 -> AVL
      (Balance'
         ('ForkTree
            (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n a1) r)
         (UnbalancedState
            (Height (Insert' x a ('ForkTree ll (Node ln lna) lr) o))
            (Height r))))
-> ((LtN (Insert' x a ('ForkTree ll (Node ln lna) lr) o) n
     ~ 'True) =>
    AVL
      (Balance'
         ('ForkTree
            (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n a1) r)
         (UnbalancedState
            (Height (Insert' x a ('ForkTree ll (Node ln lna) lr) o))
            (Height r))))
-> AVL
     (Balance'
        ('ForkTree
           (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n a1) r)
        (UnbalancedState
           (Height (Insert' x a ('ForkTree ll (Node ln lna) lr) o))
           (Height r)))
forall a b. (a -> b) -> a -> b
$
      AlmostAVL
  ('ForkTree
     (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n a) r)
-> AVL
     (Balance
        ('ForkTree
           (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n a) r))
forall (t :: Tree). Balanceable t => AlmostAVL t -> AVL (Balance t)
balance (AlmostAVL
   ('ForkTree
      (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n a) r)
 -> AVL
      (Balance
         ('ForkTree
            (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n a) r)))
-> AlmostAVL
     ('ForkTree
        (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n a) r)
-> AVL
     (Balance
        ('ForkTree
           (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n a) r))
forall a b. (a -> b) -> a -> b
$ AVL (Insert' x a ('ForkTree ll (Node ln lna) lr) o)
-> Node n a
-> AVL r
-> AlmostAVL
     ('ForkTree
        (Insert' x a ('ForkTree ll (Node ln lna) 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 (Node x a -> AVL l -> Proxy o -> AVL (Insert' x a l o)
forall (x :: Nat) a (t :: Tree) (o :: Ordering).
Insertable' x a t o =>
Node x a -> AVL t -> Proxy o -> AVL (Insert' x a t o)
insert' Node x a
node 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
  ( CmpNat x n ~ 'GT,
    Show a,
    Balanceable ('ForkTree l (Node n a1) ('ForkTree 'EmptyTree (Node x a) 'EmptyTree))
  ) =>
  Insertable' x a ('ForkTree l (Node n a1) 'EmptyTree) 'GT
  where
  type Insert' x a ('ForkTree l (Node n a1) 'EmptyTree) 'GT = Balance ('ForkTree l (Node n a1) ('ForkTree 'EmptyTree (Node x a) 'EmptyTree))
  insert' :: Node x a
-> AVL ('ForkTree l (Node n a1) 'EmptyTree)
-> Proxy 'GT
-> AVL (Insert' x a ('ForkTree l (Node n a1) 'EmptyTree) 'GT)
insert' Node x a
node (ForkAVL AVL l
l Node n a
node' AVL r
_) Proxy 'GT
_ = AlmostAVL
  ('ForkTree
     l (Node n a) ('ForkTree 'EmptyTree (Node x a) 'EmptyTree))
-> AVL
     (Balance
        ('ForkTree
           l (Node n a) ('ForkTree 'EmptyTree (Node x a) 'EmptyTree)))
forall (t :: Tree). Balanceable t => AlmostAVL t -> AVL (Balance t)
balance (AVL l
-> Node n a
-> AVL ('ForkTree 'EmptyTree (Node x a) 'EmptyTree)
-> AlmostAVL
     ('ForkTree
        l (Node n a) ('ForkTree 'EmptyTree (Node x a) 'EmptyTree))
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 'EmptyTree
-> Node x a
-> AVL 'EmptyTree
-> AVL ('ForkTree 'EmptyTree (Node x a) 'EmptyTree)
forall a (l :: Tree) (n :: Nat) (r :: Tree).
(Show a, LtN l n ~ 'True, GtN r n ~ 'True,
 BalancedHeights (Height l) (Height r) n ~ 'True) =>
AVL l -> Node n a -> AVL r -> AVL ('ForkTree l (Node n a) r)
ForkAVL AVL 'EmptyTree
EmptyAVL Node x a
node AVL 'EmptyTree
EmptyAVL))

instance
  ( r ~ 'ForkTree rl (Node rn rna) rr,
    o ~ CmpNat x rn,
    CmpNat x n ~ 'GT,
    Insertable' x a r o,
    Balanceable ('ForkTree l (Node n a1) (Insert' x a r o)),
    ProofGtNInsert' x a r n o
  ) =>
  Insertable' x a ('ForkTree l (Node n a1) ('ForkTree rl (Node rn rna) rr)) 'GT
  where
  type
    Insert' x a ('ForkTree l (Node n a1) ('ForkTree rl (Node rn rna) rr)) 'GT =
      Balance ('ForkTree l (Node n a1) (Insert' x a ('ForkTree rl (Node rn rna) rr) (CmpNat x rn)))
  insert' :: Node x a
-> AVL ('ForkTree l (Node n a1) ('ForkTree rl (Node rn rna) rr))
-> Proxy 'GT
-> AVL
     (Insert'
        x a ('ForkTree l (Node n a1) ('ForkTree rl (Node rn rna) rr)) 'GT)
insert' Node x a
node (ForkAVL AVL l
l Node n a
node' AVL r
r) Proxy 'GT
_ =
    (GtN (Insert' x a ('ForkTree rl (Node rn rna) rr) o) n :~: 'True)
-> ((GtN (Insert' x a ('ForkTree rl (Node rn rna) rr) o) n
     ~ 'True) =>
    AVL
      (Balance'
         ('ForkTree
            l (Node n a1) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))
         (UnbalancedState
            (Height l)
            (Height (Insert' x a ('ForkTree rl (Node rn rna) rr) o)))))
-> AVL
     (Balance'
        ('ForkTree
           l (Node n a1) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))
        (UnbalancedState
           (Height l)
           (Height (Insert' x a ('ForkTree rl (Node rn rna) rr) o))))
forall {k} (a :: k) (b :: k) r. (a :~: b) -> ((a ~ b) => r) -> r
gcastWith (Node x a
-> AVL r -> Proxy n -> Proxy o -> GtN (Insert x a r) n :~: 'True
forall (x :: Nat) a (t :: Tree) (n :: Nat) (o :: Ordering).
(ProofGtNInsert' x a t n o, CmpNat x n ~ 'GT, GtN t n ~ 'True) =>
Node x a
-> AVL t -> Proxy n -> Proxy o -> GtN (Insert x a t) n :~: 'True
proofGtNInsert' Node x a
node AVL r
r (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n) Proxy o
po) (((GtN (Insert' x a ('ForkTree rl (Node rn rna) rr) o) n
   ~ 'True) =>
  AVL
    (Balance'
       ('ForkTree
          l (Node n a1) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))
       (UnbalancedState
          (Height l)
          (Height (Insert' x a ('ForkTree rl (Node rn rna) rr) o)))))
 -> AVL
      (Balance'
         ('ForkTree
            l (Node n a1) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))
         (UnbalancedState
            (Height l)
            (Height (Insert' x a ('ForkTree rl (Node rn rna) rr) o)))))
-> ((GtN (Insert' x a ('ForkTree rl (Node rn rna) rr) o) n
     ~ 'True) =>
    AVL
      (Balance'
         ('ForkTree
            l (Node n a1) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))
         (UnbalancedState
            (Height l)
            (Height (Insert' x a ('ForkTree rl (Node rn rna) rr) o)))))
-> AVL
     (Balance'
        ('ForkTree
           l (Node n a1) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))
        (UnbalancedState
           (Height l)
           (Height (Insert' x a ('ForkTree rl (Node rn rna) rr) o))))
forall a b. (a -> b) -> a -> b
$
      AlmostAVL
  ('ForkTree
     l (Node n a) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))
-> AVL
     (Balance
        ('ForkTree
           l (Node n a) (Insert' x a ('ForkTree rl (Node rn rna) rr) o)))
forall (t :: Tree). Balanceable t => AlmostAVL t -> AVL (Balance t)
balance (AlmostAVL
   ('ForkTree
      l (Node n a) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))
 -> AVL
      (Balance
         ('ForkTree
            l (Node n a) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))))
-> AlmostAVL
     ('ForkTree
        l (Node n a) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))
-> AVL
     (Balance
        ('ForkTree
           l (Node n a) (Insert' x a ('ForkTree rl (Node rn rna) rr) o)))
forall a b. (a -> b) -> a -> b
$ AVL l
-> Node n a
-> AVL (Insert' x a ('ForkTree rl (Node rn rna) rr) o)
-> AlmostAVL
     ('ForkTree
        l (Node n a) (Insert' x a ('ForkTree rl (Node rn rna) 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' (Node x a -> AVL r -> Proxy o -> AVL (Insert' x a r o)
forall (x :: Nat) a (t :: Tree) (o :: Ordering).
Insertable' x a t o =>
Node x a -> AVL t -> Proxy o -> AVL (Insert' x a t o)
insert' Node x a
node AVL r
r Proxy o
po)
    where
      po :: Proxy o
po = Proxy o
forall {k} (t :: k). Proxy t
Proxy :: Proxy o