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

-- |
-- Module      : Data.Tree.BST.Extern.InsertProofs
-- Description : Proofs for insertion over externalist AVL trees
-- Copyright   : (c) Nicolás Rodríguez, 2021
-- License     : GPL-3
-- Maintainer  : Nicolás Rodríguez
-- Stability   : experimental
-- Portability : POSIX
--
-- Implementation of the necessary proofs to ensure (at compile time) that the
-- insertion algorithm defined in "Data.Tree.AVL.Extern.Insert" respects the key ordering and height balance restrictions.
module Data.Tree.AVL.Extern.InsertProofs
  ( ProofIsBalancedInsert (proofIsBalancedInsert),
    ProofIsBSTInsert (proofIsBSTInsert),
  )
where

import Data.Kind (Type)
import Data.Proxy (Proxy (Proxy))
import Data.Tree.AVL.Extern.BalanceProofs
  ( ProofGtNBalance (proofGtNBalance),
    ProofIsBSTBalance (proofIsBSTBalance),
    ProofIsBalancedBalance (proofIsBalancedBalance),
    ProofLtNBalance (proofLtNBalance),
  )
import Data.Tree.AVL.Extern.Constructors (IsAlmostBalancedT (ForkIsAlmostBalancedT), IsBalancedT (EmptyIsBalancedT, ForkIsBalancedT))
import Data.Tree.AVL.Extern.Insert
  ( Insert',
    Insertable (Insert),
  )
import Data.Tree.BST.Extern.Constructors (IsBSTT (EmptyIsBSTT, ForkIsBSTT))
import Data.Tree.BST.Invariants (GtN, LtN)
import Data.Tree.ITree (Tree (EmptyTree, ForkTree))
import Data.Tree.Node (Node)
import Data.Type.Equality (gcastWith, (:~:) (Refl))
import GHC.TypeNats (CmpNat, Nat)
import Prelude (Bool (True), Ordering (EQ, GT, LT), ($))

-- | Prove that inserting a node with key @x@ and element value @a@
-- in a `Data.Tree.BST.Extern.Constructors.BST` tree preserves @BST@ condition.
class ProofIsBSTInsert (x :: Nat) (a :: Type) (t :: Tree) where
  proofIsBSTInsert :: Proxy (Node x a) -> IsBSTT t -> IsBSTT (Insert x a t)

instance ProofIsBSTInsert x a 'EmptyTree where
  proofIsBSTInsert :: Proxy (Node x a)
-> IsBSTT 'EmptyTree -> IsBSTT (Insert x a 'EmptyTree)
proofIsBSTInsert Proxy (Node x a)
pNode IsBSTT 'EmptyTree
_ = IsBSTT 'EmptyTree
-> Proxy (Node x a)
-> IsBSTT 'EmptyTree
-> IsBSTT ('ForkTree 'EmptyTree (Node x a) 'EmptyTree)
forall (l :: Tree) (n :: Nat) (a :: Tree) r.
(LtN l n ~ 'True, GtN a n ~ 'True) =>
IsBSTT l
-> Proxy (Node n r)
-> IsBSTT a
-> IsBSTT ('ForkTree l (Node n r) a)
ForkIsBSTT IsBSTT 'EmptyTree
EmptyIsBSTT Proxy (Node x a)
pNode IsBSTT 'EmptyTree
EmptyIsBSTT

instance
  ProofIsBSTInsert' x a ('ForkTree l (Node n a1) r) (CmpNat x n) =>
  ProofIsBSTInsert x a ('ForkTree l (Node n a1) r)
  where
  proofIsBSTInsert :: Proxy (Node x a)
-> IsBSTT ('ForkTree l (Node n a1) r)
-> IsBSTT (Insert x a ('ForkTree l (Node n a1) r))
proofIsBSTInsert Proxy (Node x a)
pNode IsBSTT ('ForkTree l (Node n a1) r)
tIsBST = Proxy (Node x a)
-> IsBSTT ('ForkTree l (Node n a1) r)
-> Proxy (CmpNat x n)
-> IsBSTT (Insert' x a ('ForkTree l (Node n a1) r) (CmpNat x n))
forall (x :: Nat) a (t :: Tree) (o :: Ordering).
ProofIsBSTInsert' x a t o =>
Proxy (Node x a) -> IsBSTT t -> Proxy o -> IsBSTT (Insert' x a t o)
proofIsBSTInsert' Proxy (Node x a)
pNode IsBSTT ('ForkTree l (Node n a1) r)
tIsBST (Proxy (CmpNat x n)
forall {k} (t :: k). Proxy t
Proxy :: Proxy (CmpNat x n))

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

instance ProofIsBSTInsert' x a ('ForkTree l (Node n a1) r) 'EQ where
  proofIsBSTInsert' :: Proxy (Node x a)
-> IsBSTT ('ForkTree l (Node n a1) r)
-> Proxy 'EQ
-> IsBSTT (Insert' x a ('ForkTree l (Node n a1) r) 'EQ)
proofIsBSTInsert' Proxy (Node x a)
_ (ForkIsBSTT IsBSTT l
lIsBST Proxy (Node n a)
_ IsBSTT r
rIsBST) Proxy 'EQ
_ = IsBSTT l
-> Proxy (Node n a)
-> IsBSTT r
-> IsBSTT ('ForkTree l (Node n a) r)
forall (l :: Tree) (n :: Nat) (a :: Tree) r.
(LtN l n ~ 'True, GtN a n ~ 'True) =>
IsBSTT l
-> Proxy (Node n r)
-> IsBSTT a
-> IsBSTT ('ForkTree l (Node n r) a)
ForkIsBSTT IsBSTT l
lIsBST Proxy (Node n a)
pNode IsBSTT r
rIsBST
    where
      pNode :: Proxy (Node n a)
pNode = Proxy (Node n a)
forall {k} (t :: k). Proxy t
Proxy :: Proxy (Node n a)

instance
  ( CmpNat x n ~ 'LT,
    ProofIsBSTBalance ('ForkTree ('ForkTree 'EmptyTree (Node x a) 'EmptyTree) (Node n a1) r)
  ) =>
  ProofIsBSTInsert' x a ('ForkTree 'EmptyTree (Node n a1) r) 'LT
  where
  proofIsBSTInsert' :: Proxy (Node x a)
-> IsBSTT ('ForkTree 'EmptyTree (Node n a1) r)
-> Proxy 'LT
-> IsBSTT (Insert' x a ('ForkTree 'EmptyTree (Node n a1) r) 'LT)
proofIsBSTInsert' Proxy (Node x a)
pNode (ForkIsBSTT IsBSTT l
_ Proxy (Node n a)
pNode' IsBSTT r
rIsBST) Proxy 'LT
_ =
    IsBSTT
  ('ForkTree
     ('ForkTree 'EmptyTree (Node x a) 'EmptyTree) (Node n a) r)
-> IsBSTT
     (Balance
        ('ForkTree
           ('ForkTree 'EmptyTree (Node x a) 'EmptyTree) (Node n a) r))
forall (t :: Tree).
ProofIsBSTBalance t =>
IsBSTT t -> IsBSTT (Balance t)
proofIsBSTBalance (IsBSTT
   ('ForkTree
      ('ForkTree 'EmptyTree (Node x a) 'EmptyTree) (Node n a) r)
 -> IsBSTT
      (Balance
         ('ForkTree
            ('ForkTree 'EmptyTree (Node x a) 'EmptyTree) (Node n a) r)))
-> IsBSTT
     ('ForkTree
        ('ForkTree 'EmptyTree (Node x a) 'EmptyTree) (Node n a) r)
-> IsBSTT
     (Balance
        ('ForkTree
           ('ForkTree 'EmptyTree (Node x a) 'EmptyTree) (Node n a) r))
forall a b. (a -> b) -> a -> b
$ IsBSTT ('ForkTree 'EmptyTree (Node x a) 'EmptyTree)
-> Proxy (Node n a)
-> IsBSTT r
-> IsBSTT
     ('ForkTree
        ('ForkTree 'EmptyTree (Node x a) 'EmptyTree) (Node n a) r)
forall (l :: Tree) (n :: Nat) (a :: Tree) r.
(LtN l n ~ 'True, GtN a n ~ 'True) =>
IsBSTT l
-> Proxy (Node n r)
-> IsBSTT a
-> IsBSTT ('ForkTree l (Node n r) a)
ForkIsBSTT (IsBSTT 'EmptyTree
-> Proxy (Node x a)
-> IsBSTT 'EmptyTree
-> IsBSTT ('ForkTree 'EmptyTree (Node x a) 'EmptyTree)
forall (l :: Tree) (n :: Nat) (a :: Tree) r.
(LtN l n ~ 'True, GtN a n ~ 'True) =>
IsBSTT l
-> Proxy (Node n r)
-> IsBSTT a
-> IsBSTT ('ForkTree l (Node n r) a)
ForkIsBSTT IsBSTT 'EmptyTree
EmptyIsBSTT Proxy (Node x a)
pNode IsBSTT 'EmptyTree
EmptyIsBSTT) Proxy (Node n a)
pNode' IsBSTT r
rIsBST

instance
  ( l ~ 'ForkTree ll (Node ln lna) lr,
    o ~ CmpNat x ln,
    CmpNat x n ~ 'LT,
    ProofIsBSTInsert' x a l o,
    ProofLtNInsert' x a l n o,
    ProofIsBSTBalance ('ForkTree (Insert' x a l o) (Node n a1) r)
  ) =>
  ProofIsBSTInsert' x a ('ForkTree ('ForkTree ll (Node ln lna) lr) (Node n a1) r) 'LT
  where
  proofIsBSTInsert' :: Proxy (Node x a)
-> IsBSTT ('ForkTree ('ForkTree ll (Node ln lna) lr) (Node n a1) r)
-> Proxy 'LT
-> IsBSTT
     (Insert'
        x a ('ForkTree ('ForkTree ll (Node ln lna) lr) (Node n a1) r) 'LT)
proofIsBSTInsert' Proxy (Node x a)
pNode (ForkIsBSTT IsBSTT l
lIsBST Proxy (Node n a)
pNode' IsBSTT r
rIsBST) 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) =>
    IsBSTT
      (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))))
-> IsBSTT
     (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 (Proxy (Node x a)
-> IsBSTT l
-> Proxy n
-> Proxy o
-> LtN (Insert' x a l o) 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) =>
Proxy (Node x a)
-> IsBSTT t
-> Proxy n
-> Proxy o
-> LtN (Insert' x a t o) n :~: 'True
proofLtNInsert' Proxy (Node x a)
pNode IsBSTT l
lIsBST (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n) (Proxy o
forall {k} (t :: k). Proxy t
Proxy :: Proxy o)) (((LtN (Insert' x a ('ForkTree ll (Node ln lna) lr) o) n
   ~ 'True) =>
  IsBSTT
    (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))))
 -> IsBSTT
      (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) =>
    IsBSTT
      (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))))
-> IsBSTT
     (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
$
      IsBSTT
  ('ForkTree
     (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n a) r)
-> IsBSTT
     (Balance
        ('ForkTree
           (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n a) r))
forall (t :: Tree).
ProofIsBSTBalance t =>
IsBSTT t -> IsBSTT (Balance t)
proofIsBSTBalance (IsBSTT
   ('ForkTree
      (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n a) r)
 -> IsBSTT
      (Balance
         ('ForkTree
            (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n a) r)))
-> IsBSTT
     ('ForkTree
        (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n a) r)
-> IsBSTT
     (Balance
        ('ForkTree
           (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n a) r))
forall a b. (a -> b) -> a -> b
$ IsBSTT (Insert' x a ('ForkTree ll (Node ln lna) lr) o)
-> Proxy (Node n a)
-> IsBSTT r
-> IsBSTT
     ('ForkTree
        (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n a) r)
forall (l :: Tree) (n :: Nat) (a :: Tree) r.
(LtN l n ~ 'True, GtN a n ~ 'True) =>
IsBSTT l
-> Proxy (Node n r)
-> IsBSTT a
-> IsBSTT ('ForkTree l (Node n r) a)
ForkIsBSTT (Proxy (Node x a) -> IsBSTT l -> IsBSTT (Insert x a l)
forall (x :: Nat) a (t :: Tree).
ProofIsBSTInsert x a t =>
Proxy (Node x a) -> IsBSTT t -> IsBSTT (Insert x a t)
proofIsBSTInsert Proxy (Node x a)
pNode IsBSTT l
lIsBST) Proxy (Node n a)
pNode' IsBSTT r
rIsBST

instance
  ( CmpNat x n ~ 'GT,
    ProofIsBSTBalance ('ForkTree l (Node n a1) ('ForkTree 'EmptyTree (Node x a) 'EmptyTree))
  ) =>
  ProofIsBSTInsert' x a ('ForkTree l (Node n a1) 'EmptyTree) 'GT
  where
  proofIsBSTInsert' :: Proxy (Node x a)
-> IsBSTT ('ForkTree l (Node n a1) 'EmptyTree)
-> Proxy 'GT
-> IsBSTT (Insert' x a ('ForkTree l (Node n a1) 'EmptyTree) 'GT)
proofIsBSTInsert' Proxy (Node x a)
pNode (ForkIsBSTT IsBSTT l
lIsBST Proxy (Node n a)
pNode' IsBSTT r
_) Proxy 'GT
_ =
    IsBSTT
  ('ForkTree
     l (Node n a) ('ForkTree 'EmptyTree (Node x a) 'EmptyTree))
-> IsBSTT
     (Balance
        ('ForkTree
           l (Node n a) ('ForkTree 'EmptyTree (Node x a) 'EmptyTree)))
forall (t :: Tree).
ProofIsBSTBalance t =>
IsBSTT t -> IsBSTT (Balance t)
proofIsBSTBalance (IsBSTT l
-> Proxy (Node n a)
-> IsBSTT ('ForkTree 'EmptyTree (Node x a) 'EmptyTree)
-> IsBSTT
     ('ForkTree
        l (Node n a) ('ForkTree 'EmptyTree (Node x a) 'EmptyTree))
forall (l :: Tree) (n :: Nat) (a :: Tree) r.
(LtN l n ~ 'True, GtN a n ~ 'True) =>
IsBSTT l
-> Proxy (Node n r)
-> IsBSTT a
-> IsBSTT ('ForkTree l (Node n r) a)
ForkIsBSTT IsBSTT l
lIsBST Proxy (Node n a)
pNode' (IsBSTT 'EmptyTree
-> Proxy (Node x a)
-> IsBSTT 'EmptyTree
-> IsBSTT ('ForkTree 'EmptyTree (Node x a) 'EmptyTree)
forall (l :: Tree) (n :: Nat) (a :: Tree) r.
(LtN l n ~ 'True, GtN a n ~ 'True) =>
IsBSTT l
-> Proxy (Node n r)
-> IsBSTT a
-> IsBSTT ('ForkTree l (Node n r) a)
ForkIsBSTT IsBSTT 'EmptyTree
EmptyIsBSTT Proxy (Node x a)
pNode IsBSTT 'EmptyTree
EmptyIsBSTT))

instance
  ( r ~ 'ForkTree rl (Node rn rna) rr,
    o ~ CmpNat x rn,
    CmpNat x n ~ 'GT,
    ProofGtNInsert' x a r n o,
    ProofIsBSTInsert' x a r o,
    ProofIsBSTBalance ('ForkTree l (Node n a1) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))
  ) =>
  ProofIsBSTInsert' x a ('ForkTree l (Node n a1) ('ForkTree rl (Node rn rna) rr)) 'GT
  where
  proofIsBSTInsert' :: Proxy (Node x a)
-> IsBSTT ('ForkTree l (Node n a1) ('ForkTree rl (Node rn rna) rr))
-> Proxy 'GT
-> IsBSTT
     (Insert'
        x a ('ForkTree l (Node n a1) ('ForkTree rl (Node rn rna) rr)) 'GT)
proofIsBSTInsert' Proxy (Node x a)
pNode (ForkIsBSTT IsBSTT l
lIsBST Proxy (Node n a)
pNode' IsBSTT r
rIsBST) 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) =>
    IsBSTT
      (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)))))
-> IsBSTT
     (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 (Proxy (Node x a)
-> IsBSTT r
-> Proxy n
-> Proxy o
-> GtN (Insert' x a r o) 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) =>
Proxy (Node x a)
-> IsBSTT t
-> Proxy n
-> Proxy o
-> GtN (Insert' x a t o) n :~: 'True
proofGtNInsert' Proxy (Node x a)
pNode IsBSTT r
rIsBST (Proxy n
forall {k} (t :: k). Proxy t
Proxy :: Proxy n) (Proxy o
forall {k} (t :: k). Proxy t
Proxy :: Proxy o)) (((GtN (Insert' x a ('ForkTree rl (Node rn rna) rr) o) n
   ~ 'True) =>
  IsBSTT
    (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)))))
 -> IsBSTT
      (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) =>
    IsBSTT
      (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)))))
-> IsBSTT
     (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
$
      IsBSTT
  ('ForkTree
     l (Node n a) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))
-> IsBSTT
     (Balance
        ('ForkTree
           l (Node n a) (Insert' x a ('ForkTree rl (Node rn rna) rr) o)))
forall (t :: Tree).
ProofIsBSTBalance t =>
IsBSTT t -> IsBSTT (Balance t)
proofIsBSTBalance (IsBSTT
   ('ForkTree
      l (Node n a) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))
 -> IsBSTT
      (Balance
         ('ForkTree
            l (Node n a) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))))
-> IsBSTT
     ('ForkTree
        l (Node n a) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))
-> IsBSTT
     (Balance
        ('ForkTree
           l (Node n a) (Insert' x a ('ForkTree rl (Node rn rna) rr) o)))
forall a b. (a -> b) -> a -> b
$ IsBSTT l
-> Proxy (Node n a)
-> IsBSTT (Insert' x a ('ForkTree rl (Node rn rna) rr) o)
-> IsBSTT
     ('ForkTree
        l (Node n a) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))
forall (l :: Tree) (n :: Nat) (a :: Tree) r.
(LtN l n ~ 'True, GtN a n ~ 'True) =>
IsBSTT l
-> Proxy (Node n r)
-> IsBSTT a
-> IsBSTT ('ForkTree l (Node n r) a)
ForkIsBSTT IsBSTT l
lIsBST Proxy (Node n a)
pNode' (Proxy (Node x a) -> IsBSTT r -> IsBSTT (Insert x a r)
forall (x :: Nat) a (t :: Tree).
ProofIsBSTInsert x a t =>
Proxy (Node x a) -> IsBSTT t -> IsBSTT (Insert x a t)
proofIsBSTInsert Proxy (Node x a)
pNode IsBSTT r
rIsBST)

-- | Prove that inserting a node with key @x@ (lower than @n@) and element value @a@
-- 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 ProofLtNInsert' (x :: Nat) (a :: Type) (t :: Tree) (n :: Nat) (o :: Ordering) where
  proofLtNInsert' ::
    (CmpNat x n ~ 'LT, LtN t n ~ 'True) =>
    Proxy (Node x a) ->
    IsBSTT t ->
    Proxy n ->
    Proxy o ->
    LtN (Insert' x a t o) n :~: 'True

instance 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) =>
Proxy (Node x a)
-> IsBSTT ('ForkTree l (Node n1 a1) r)
-> Proxy n
-> Proxy 'EQ
-> LtN (Insert' x a ('ForkTree l (Node n1 a1) r) 'EQ) n :~: 'True
proofLtNInsert' Proxy (Node x a)
_ IsBSTT ('ForkTree l (Node n1 a1) r)
_ Proxy n
_ Proxy 'EQ
_ = LtN (Insert' x a ('ForkTree l (Node n1 a1) r) 'EQ) 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
  ) =>
  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) =>
Proxy (Node x a)
-> IsBSTT ('ForkTree 'EmptyTree (Node n1 a1) r)
-> Proxy n
-> Proxy 'LT
-> LtN (Insert' x a ('ForkTree 'EmptyTree (Node n1 a1) r) 'LT) n
   :~: 'True
proofLtNInsert' Proxy (Node x a)
pNode (ForkIsBSTT IsBSTT l
_ Proxy (Node n a)
pNode' IsBSTT r
rIsBST) 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 (IsBSTT
  ('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) =>
IsBSTT t -> Proxy n -> LtN (Balance t) n :~: 'True
proofLtNBalance (IsBSTT ('ForkTree 'EmptyTree (Node x a) 'EmptyTree)
-> Proxy (Node n a)
-> IsBSTT r
-> IsBSTT
     ('ForkTree
        ('ForkTree 'EmptyTree (Node x a) 'EmptyTree) (Node n a) r)
forall (l :: Tree) (n :: Nat) (a :: Tree) r.
(LtN l n ~ 'True, GtN a n ~ 'True) =>
IsBSTT l
-> Proxy (Node n r)
-> IsBSTT a
-> IsBSTT ('ForkTree l (Node n r) a)
ForkIsBSTT (IsBSTT 'EmptyTree
-> Proxy (Node x a)
-> IsBSTT 'EmptyTree
-> IsBSTT ('ForkTree 'EmptyTree (Node x a) 'EmptyTree)
forall (l :: Tree) (n :: Nat) (a :: Tree) r.
(LtN l n ~ 'True, GtN a n ~ 'True) =>
IsBSTT l
-> Proxy (Node n r)
-> IsBSTT a
-> IsBSTT ('ForkTree l (Node n r) a)
ForkIsBSTT IsBSTT 'EmptyTree
EmptyIsBSTT Proxy (Node x a)
pNode IsBSTT 'EmptyTree
EmptyIsBSTT) Proxy (Node n a)
pNode' IsBSTT r
rIsBST) 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,
    ProofLtNInsert' x a l n o,
    ProofLtNInsert' x a l n1 o,
    ProofIsBSTInsert x a l,
    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) =>
Proxy (Node x a)
-> IsBSTT
     ('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) 'LT)
     n
   :~: 'True
proofLtNInsert' Proxy (Node x a)
pNode (ForkIsBSTT IsBSTT l
lIsBST Proxy (Node n a)
pNode' IsBSTT r
rIsBST) 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 (Proxy (Node x a)
-> IsBSTT l
-> Proxy n
-> Proxy o
-> LtN (Insert' x a l o) 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) =>
Proxy (Node x a)
-> IsBSTT t
-> Proxy n
-> Proxy o
-> LtN (Insert' x a t o) n :~: 'True
proofLtNInsert' Proxy (Node x a)
pNode IsBSTT l
lIsBST 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 (Proxy (Node x a)
-> IsBSTT l
-> Proxy n1
-> Proxy o
-> LtN (Insert' x a l o) 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) =>
Proxy (Node x a)
-> IsBSTT t
-> Proxy n
-> Proxy o
-> LtN (Insert' x a t o) n :~: 'True
proofLtNInsert' Proxy (Node x a)
pNode IsBSTT l
lIsBST (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 (IsBSTT
  ('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) =>
IsBSTT t -> Proxy n -> LtN (Balance t) n :~: 'True
proofLtNBalance (IsBSTT (Insert' x a ('ForkTree ll (Node ln lna) lr) o)
-> Proxy (Node n a)
-> IsBSTT r
-> IsBSTT
     ('ForkTree
        (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n a) r)
forall (l :: Tree) (n :: Nat) (a :: Tree) r.
(LtN l n ~ 'True, GtN a n ~ 'True) =>
IsBSTT l
-> Proxy (Node n r)
-> IsBSTT a
-> IsBSTT ('ForkTree l (Node n r) a)
ForkIsBSTT IsBSTT (Insert' x a ('ForkTree ll (Node ln lna) lr) o)
IsBSTT (Insert x a l)
lIsBST' Proxy (Node n a)
pNode' IsBSTT r
rIsBST) 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
      lIsBST' :: IsBSTT (Insert x a l)
lIsBST' = Proxy (Node x a) -> IsBSTT l -> IsBSTT (Insert x a l)
forall (x :: Nat) a (t :: Tree).
ProofIsBSTInsert x a t =>
Proxy (Node x a) -> IsBSTT t -> IsBSTT (Insert x a t)
proofIsBSTInsert Proxy (Node x a)
pNode IsBSTT l
lIsBST

instance
  ( CmpNat x n1 ~ 'GT,
    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) =>
Proxy (Node x a)
-> IsBSTT ('ForkTree l (Node n1 a1) 'EmptyTree)
-> Proxy n
-> Proxy 'GT
-> LtN (Insert' x a ('ForkTree l (Node n1 a1) 'EmptyTree) 'GT) n
   :~: 'True
proofLtNInsert' Proxy (Node x a)
pNode (ForkIsBSTT IsBSTT l
lIsBST Proxy (Node n a)
pNode' IsBSTT 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 (IsBSTT
  ('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) =>
IsBSTT t -> Proxy n -> LtN (Balance t) n :~: 'True
proofLtNBalance (IsBSTT l
-> Proxy (Node n a)
-> IsBSTT ('ForkTree 'EmptyTree (Node x a) 'EmptyTree)
-> IsBSTT
     ('ForkTree
        l (Node n a) ('ForkTree 'EmptyTree (Node x a) 'EmptyTree))
forall (l :: Tree) (n :: Nat) (a :: Tree) r.
(LtN l n ~ 'True, GtN a n ~ 'True) =>
IsBSTT l
-> Proxy (Node n r)
-> IsBSTT a
-> IsBSTT ('ForkTree l (Node n r) a)
ForkIsBSTT IsBSTT l
lIsBST Proxy (Node n a)
pNode' (IsBSTT 'EmptyTree
-> Proxy (Node x a)
-> IsBSTT 'EmptyTree
-> IsBSTT ('ForkTree 'EmptyTree (Node x a) 'EmptyTree)
forall (l :: Tree) (n :: Nat) (a :: Tree) r.
(LtN l n ~ 'True, GtN a n ~ 'True) =>
IsBSTT l
-> Proxy (Node n r)
-> IsBSTT a
-> IsBSTT ('ForkTree l (Node n r) a)
ForkIsBSTT IsBSTT 'EmptyTree
EmptyIsBSTT Proxy (Node x a)
pNode IsBSTT 'EmptyTree
EmptyIsBSTT)) 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 n1 n ~ 'LT,
    CmpNat x n1 ~ 'GT,
    LtN r n ~ 'True,
    ProofLtNInsert' x a r n o,
    ProofGtNInsert' x a r n1 o,
    ProofIsBSTInsert x a r,
    ProofLtNBalance ('ForkTree l (Node n1 a1) (Insert' x a r o)) n
  ) =>
  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) =>
Proxy (Node x a)
-> IsBSTT
     ('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)) 'GT)
     n
   :~: 'True
proofLtNInsert' Proxy (Node x a)
pNode (ForkIsBSTT IsBSTT l
lIsBST Proxy (Node n a)
pNode' IsBSTT r
rIsBST) 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 (Proxy (Node x a)
-> IsBSTT r
-> Proxy n
-> Proxy o
-> LtN (Insert' x a r o) 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) =>
Proxy (Node x a)
-> IsBSTT t
-> Proxy n
-> Proxy o
-> LtN (Insert' x a t o) n :~: 'True
proofLtNInsert' Proxy (Node x a)
pNode IsBSTT r
rIsBST 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 (Proxy (Node x a)
-> IsBSTT r
-> Proxy n1
-> Proxy o
-> GtN (Insert' x a r o) 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) =>
Proxy (Node x a)
-> IsBSTT t
-> Proxy n
-> Proxy o
-> GtN (Insert' x a t o) n :~: 'True
proofGtNInsert' Proxy (Node x a)
pNode IsBSTT r
rIsBST (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 (IsBSTT
  ('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) =>
IsBSTT t -> Proxy n -> LtN (Balance t) n :~: 'True
proofLtNBalance (IsBSTT l
-> Proxy (Node n a)
-> IsBSTT (Insert' x a ('ForkTree rl (Node rn rna) rr) o)
-> IsBSTT
     ('ForkTree
        l (Node n a) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))
forall (l :: Tree) (n :: Nat) (a :: Tree) r.
(LtN l n ~ 'True, GtN a n ~ 'True) =>
IsBSTT l
-> Proxy (Node n r)
-> IsBSTT a
-> IsBSTT ('ForkTree l (Node n r) a)
ForkIsBSTT IsBSTT l
lIsBST Proxy (Node n a)
pNode' IsBSTT (Insert' x a ('ForkTree rl (Node rn rna) rr) o)
IsBSTT (Insert x a r)
rIsBST') 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
      rIsBST' :: IsBSTT (Insert x a r)
rIsBST' = Proxy (Node x a) -> IsBSTT r -> IsBSTT (Insert x a r)
forall (x :: Nat) a (t :: Tree).
ProofIsBSTInsert x a t =>
Proxy (Node x a) -> IsBSTT t -> IsBSTT (Insert x a t)
proofIsBSTInsert Proxy (Node x a)
pNode IsBSTT r
rIsBST

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

instance 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) =>
Proxy (Node x a)
-> IsBSTT ('ForkTree l (Node n1 a1) r)
-> Proxy n
-> Proxy 'EQ
-> GtN (Insert' x a ('ForkTree l (Node n1 a1) r) 'EQ) n :~: 'True
proofGtNInsert' Proxy (Node x a)
_ IsBSTT ('ForkTree l (Node n1 a1) r)
_ Proxy n
_ Proxy 'EQ
_ = GtN (Insert' x a ('ForkTree l (Node n1 a1) r) 'EQ) n :~: 'True
forall {k} (a :: k). a :~: a
Refl

instance
  ( CmpNat x n1 ~ 'LT,
    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) =>
Proxy (Node x a)
-> IsBSTT ('ForkTree 'EmptyTree (Node n1 a1) r)
-> Proxy n
-> Proxy 'LT
-> GtN (Insert' x a ('ForkTree 'EmptyTree (Node n1 a1) r) 'LT) n
   :~: 'True
proofGtNInsert' Proxy (Node x a)
pNode (ForkIsBSTT IsBSTT l
_ Proxy (Node n a)
pNode' IsBSTT r
rIsBST) 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 (IsBSTT
  ('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) =>
IsBSTT t -> Proxy n -> GtN (Balance t) n :~: 'True
proofGtNBalance (IsBSTT ('ForkTree 'EmptyTree (Node x a) 'EmptyTree)
-> Proxy (Node n a)
-> IsBSTT r
-> IsBSTT
     ('ForkTree
        ('ForkTree 'EmptyTree (Node x a) 'EmptyTree) (Node n a) r)
forall (l :: Tree) (n :: Nat) (a :: Tree) r.
(LtN l n ~ 'True, GtN a n ~ 'True) =>
IsBSTT l
-> Proxy (Node n r)
-> IsBSTT a
-> IsBSTT ('ForkTree l (Node n r) a)
ForkIsBSTT (IsBSTT 'EmptyTree
-> Proxy (Node x a)
-> IsBSTT 'EmptyTree
-> IsBSTT ('ForkTree 'EmptyTree (Node x a) 'EmptyTree)
forall (l :: Tree) (n :: Nat) (a :: Tree) r.
(LtN l n ~ 'True, GtN a n ~ 'True) =>
IsBSTT l
-> Proxy (Node n r)
-> IsBSTT a
-> IsBSTT ('ForkTree l (Node n r) a)
ForkIsBSTT IsBSTT 'EmptyTree
EmptyIsBSTT Proxy (Node x a)
pNode IsBSTT 'EmptyTree
EmptyIsBSTT) Proxy (Node n a)
pNode' IsBSTT r
rIsBST) 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,
    ProofGtNInsert' x a l n o,
    ProofLtNInsert' x a l n1 o,
    ProofIsBSTInsert x a l,
    ProofGtNBalance ('ForkTree (Insert' x a l o) (Node n1 a1) r) n
  ) =>
  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) =>
Proxy (Node x a)
-> IsBSTT
     ('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) 'LT)
     n
   :~: 'True
proofGtNInsert' Proxy (Node x a)
pNode (ForkIsBSTT IsBSTT l
lIsBST Proxy (Node n a)
pNode' IsBSTT r
rIsBST) 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 (Proxy (Node x a)
-> IsBSTT l
-> Proxy n
-> Proxy o
-> GtN (Insert' x a l o) 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) =>
Proxy (Node x a)
-> IsBSTT t
-> Proxy n
-> Proxy o
-> GtN (Insert' x a t o) n :~: 'True
proofGtNInsert' Proxy (Node x a)
pNode IsBSTT l
lIsBST 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 (Proxy (Node x a)
-> IsBSTT l
-> Proxy n1
-> Proxy o
-> LtN (Insert' x a l o) 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) =>
Proxy (Node x a)
-> IsBSTT t
-> Proxy n
-> Proxy o
-> LtN (Insert' x a t o) n :~: 'True
proofLtNInsert' Proxy (Node x a)
pNode IsBSTT l
lIsBST (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 (IsBSTT
  ('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) =>
IsBSTT t -> Proxy n -> GtN (Balance t) n :~: 'True
proofGtNBalance (IsBSTT (Insert' x a ('ForkTree ll (Node ln lna) lr) o)
-> Proxy (Node n a)
-> IsBSTT r
-> IsBSTT
     ('ForkTree
        (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n a) r)
forall (l :: Tree) (n :: Nat) (a :: Tree) r.
(LtN l n ~ 'True, GtN a n ~ 'True) =>
IsBSTT l
-> Proxy (Node n r)
-> IsBSTT a
-> IsBSTT ('ForkTree l (Node n r) a)
ForkIsBSTT IsBSTT (Insert' x a ('ForkTree ll (Node ln lna) lr) o)
IsBSTT (Insert x a l)
lIsBST' Proxy (Node n a)
pNode' IsBSTT r
rIsBST) 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
      lIsBST' :: IsBSTT (Insert x a l)
lIsBST' = Proxy (Node x a) -> IsBSTT l -> IsBSTT (Insert x a l)
forall (x :: Nat) a (t :: Tree).
ProofIsBSTInsert x a t =>
Proxy (Node x a) -> IsBSTT t -> IsBSTT (Insert x a t)
proofIsBSTInsert Proxy (Node x a)
pNode IsBSTT l
lIsBST

instance
  ( CmpNat x n1 ~ 'GT,
    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) =>
Proxy (Node x a)
-> IsBSTT ('ForkTree l (Node n1 a1) 'EmptyTree)
-> Proxy n
-> Proxy 'GT
-> GtN (Insert' x a ('ForkTree l (Node n1 a1) 'EmptyTree) 'GT) n
   :~: 'True
proofGtNInsert' Proxy (Node x a)
pNode (ForkIsBSTT IsBSTT l
lIsBST Proxy (Node n a)
pNode' IsBSTT 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 (IsBSTT
  ('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) =>
IsBSTT t -> Proxy n -> GtN (Balance t) n :~: 'True
proofGtNBalance (IsBSTT l
-> Proxy (Node n a)
-> IsBSTT ('ForkTree 'EmptyTree (Node x a) 'EmptyTree)
-> IsBSTT
     ('ForkTree
        l (Node n a) ('ForkTree 'EmptyTree (Node x a) 'EmptyTree))
forall (l :: Tree) (n :: Nat) (a :: Tree) r.
(LtN l n ~ 'True, GtN a n ~ 'True) =>
IsBSTT l
-> Proxy (Node n r)
-> IsBSTT a
-> IsBSTT ('ForkTree l (Node n r) a)
ForkIsBSTT IsBSTT l
lIsBST Proxy (Node n a)
pNode' (IsBSTT 'EmptyTree
-> Proxy (Node x a)
-> IsBSTT 'EmptyTree
-> IsBSTT ('ForkTree 'EmptyTree (Node x a) 'EmptyTree)
forall (l :: Tree) (n :: Nat) (a :: Tree) r.
(LtN l n ~ 'True, GtN a n ~ 'True) =>
IsBSTT l
-> Proxy (Node n r)
-> IsBSTT a
-> IsBSTT ('ForkTree l (Node n r) a)
ForkIsBSTT IsBSTT 'EmptyTree
EmptyIsBSTT Proxy (Node x a)
pNode IsBSTT 'EmptyTree
EmptyIsBSTT)) 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,
    ProofGtNInsert' x a r n o,
    ProofGtNInsert' x a r n1 o,
    ProofIsBSTInsert x a r,
    ProofGtNBalance ('ForkTree l (Node n1 a1) (Insert' x a r o)) n
  ) =>
  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) =>
Proxy (Node x a)
-> IsBSTT
     ('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)) 'GT)
     n
   :~: 'True
proofGtNInsert' Proxy (Node x a)
pNode (ForkIsBSTT IsBSTT l
lIsBST Proxy (Node n a)
pNode' IsBSTT r
rIsBST) 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 (Proxy (Node x a)
-> IsBSTT r
-> Proxy n
-> Proxy o
-> GtN (Insert' x a r o) 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) =>
Proxy (Node x a)
-> IsBSTT t
-> Proxy n
-> Proxy o
-> GtN (Insert' x a t o) n :~: 'True
proofGtNInsert' Proxy (Node x a)
pNode IsBSTT r
rIsBST 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 (Proxy (Node x a)
-> IsBSTT r
-> Proxy n1
-> Proxy o
-> GtN (Insert' x a r o) 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) =>
Proxy (Node x a)
-> IsBSTT t
-> Proxy n
-> Proxy o
-> GtN (Insert' x a t o) n :~: 'True
proofGtNInsert' Proxy (Node x a)
pNode IsBSTT r
rIsBST (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 (IsBSTT
  ('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) =>
IsBSTT t -> Proxy n -> GtN (Balance t) n :~: 'True
proofGtNBalance (IsBSTT l
-> Proxy (Node n a)
-> IsBSTT (Insert' x a ('ForkTree rl (Node rn rna) rr) o)
-> IsBSTT
     ('ForkTree
        l (Node n a) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))
forall (l :: Tree) (n :: Nat) (a :: Tree) r.
(LtN l n ~ 'True, GtN a n ~ 'True) =>
IsBSTT l
-> Proxy (Node n r)
-> IsBSTT a
-> IsBSTT ('ForkTree l (Node n r) a)
ForkIsBSTT IsBSTT l
lIsBST Proxy (Node n a)
pNode' IsBSTT (Insert' x a ('ForkTree rl (Node rn rna) rr) o)
IsBSTT (Insert x a r)
rIsBST') 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
      rIsBST' :: IsBSTT (Insert x a r)
rIsBST' = Proxy (Node x a) -> IsBSTT r -> IsBSTT (Insert x a r)
forall (x :: Nat) a (t :: Tree).
ProofIsBSTInsert x a t =>
Proxy (Node x a) -> IsBSTT t -> IsBSTT (Insert x a t)
proofIsBSTInsert Proxy (Node x a)
pNode IsBSTT r
rIsBST

-- | Prove that inserting a node with key @x@ and element value @a@
-- in an `Data.Tree.AVL.Extern.Constructors.AVL` tree preserves the @AVL@ condition.
class ProofIsBalancedInsert (x :: Nat) (a :: Type) (t :: Tree) where
  proofIsBalancedInsert :: Proxy (Node x a) -> IsBalancedT t -> IsBalancedT (Insert x a t)

instance ProofIsBalancedInsert x a 'EmptyTree where
  proofIsBalancedInsert :: Proxy (Node x a)
-> IsBalancedT 'EmptyTree -> IsBalancedT (Insert x a 'EmptyTree)
proofIsBalancedInsert Proxy (Node x a)
pNode IsBalancedT 'EmptyTree
_ = IsBalancedT 'EmptyTree
-> Proxy (Node x a)
-> IsBalancedT 'EmptyTree
-> IsBalancedT ('ForkTree 'EmptyTree (Node x a) 'EmptyTree)
forall (l :: Tree) (n :: Tree) (a :: Nat) r.
(BalancedHeights (Height l) (Height n) a ~ 'True) =>
IsBalancedT l
-> Proxy (Node a r)
-> IsBalancedT n
-> IsBalancedT ('ForkTree l (Node a r) n)
ForkIsBalancedT IsBalancedT 'EmptyTree
EmptyIsBalancedT Proxy (Node x a)
pNode IsBalancedT 'EmptyTree
EmptyIsBalancedT

instance
  (o ~ CmpNat x n, ProofIsBalancedInsert' x a ('ForkTree l (Node n a1) r) o) =>
  ProofIsBalancedInsert x a ('ForkTree l (Node n a1) r)
  where
  proofIsBalancedInsert :: Proxy (Node x a)
-> IsBalancedT ('ForkTree l (Node n a1) r)
-> IsBalancedT (Insert x a ('ForkTree l (Node n a1) r))
proofIsBalancedInsert Proxy (Node x a)
pNode IsBalancedT ('ForkTree l (Node n a1) r)
tIsBalanced = Proxy (Node x a)
-> IsBalancedT ('ForkTree l (Node n a1) r)
-> Proxy o
-> IsBalancedT (Insert' x a ('ForkTree l (Node n a1) r) o)
forall (x :: Nat) a (t :: Tree) (o :: Ordering).
ProofIsBalancedInsert' x a t o =>
Proxy (Node x a)
-> IsBalancedT t -> Proxy o -> IsBalancedT (Insert' x a t o)
proofIsBalancedInsert' Proxy (Node x a)
pNode IsBalancedT ('ForkTree l (Node n a1) r)
tIsBalanced (Proxy o
forall {k} (t :: k). Proxy t
Proxy :: Proxy o)

-- | Prove that inserting a node with key @x@ and element value @a@
-- in an `Data.Tree.BST.Extern.Constructors.BST` tree preserves the @AVL@ condition, given that the comparison between
-- @x@ and the root key of the tree equals @o@.
-- The @AVL@ condition was already checked when `proofIsBSTInsert` was called before.
-- The @o@ parameter guides the proof.
class ProofIsBalancedInsert' (x :: Nat) (a :: Type) (t :: Tree) (o :: Ordering) where
  proofIsBalancedInsert' :: Proxy (Node x a) -> IsBalancedT t -> Proxy o -> IsBalancedT (Insert' x a t o)

instance ProofIsBalancedInsert' x a ('ForkTree l (Node n a1) r) 'EQ where
  proofIsBalancedInsert' :: Proxy (Node x a)
-> IsBalancedT ('ForkTree l (Node n a1) r)
-> Proxy 'EQ
-> IsBalancedT (Insert' x a ('ForkTree l (Node n a1) r) 'EQ)
proofIsBalancedInsert' Proxy (Node x a)
_ (ForkIsBalancedT IsBalancedT l
lIsBalanced Proxy (Node n a)
_ IsBalancedT r
rIsBalanced) Proxy 'EQ
_ = IsBalancedT l
-> Proxy (Node n a)
-> IsBalancedT r
-> IsBalancedT ('ForkTree l (Node n a) r)
forall (l :: Tree) (n :: Tree) (a :: Nat) r.
(BalancedHeights (Height l) (Height n) a ~ 'True) =>
IsBalancedT l
-> Proxy (Node a r)
-> IsBalancedT n
-> IsBalancedT ('ForkTree l (Node a r) n)
ForkIsBalancedT IsBalancedT l
lIsBalanced Proxy (Node n a)
pNode IsBalancedT r
rIsBalanced
    where
      pNode :: Proxy (Node n a)
pNode = Proxy (Node n a)
forall {k} (t :: k). Proxy t
Proxy :: Proxy (Node n a)

instance
  (ProofIsBalancedBalance ('ForkTree ('ForkTree 'EmptyTree (Node x a) 'EmptyTree) (Node n a1) r)) =>
  ProofIsBalancedInsert' x a ('ForkTree 'EmptyTree (Node n a1) r) 'LT
  where
  proofIsBalancedInsert' :: Proxy (Node x a)
-> IsBalancedT ('ForkTree 'EmptyTree (Node n a1) r)
-> Proxy 'LT
-> IsBalancedT
     (Insert' x a ('ForkTree 'EmptyTree (Node n a1) r) 'LT)
proofIsBalancedInsert' Proxy (Node x a)
pNode (ForkIsBalancedT IsBalancedT l
_ Proxy (Node n a)
pNode' IsBalancedT r
rIsBalanced) Proxy 'LT
_ =
    IsAlmostBalancedT
  ('ForkTree
     ('ForkTree 'EmptyTree (Node x a) 'EmptyTree) (Node n a) r)
-> IsBalancedT
     (Balance
        ('ForkTree
           ('ForkTree 'EmptyTree (Node x a) 'EmptyTree) (Node n a) r))
forall (t :: Tree).
ProofIsBalancedBalance t =>
IsAlmostBalancedT t -> IsBalancedT (Balance t)
proofIsBalancedBalance (IsBalancedT ('ForkTree 'EmptyTree (Node x a) 'EmptyTree)
-> Proxy (Node n a)
-> IsBalancedT r
-> IsAlmostBalancedT
     ('ForkTree
        ('ForkTree 'EmptyTree (Node x a) 'EmptyTree) (Node n a) r)
forall (l :: Tree) (n :: Nat) a (r :: Tree).
IsBalancedT l
-> Proxy (Node n a)
-> IsBalancedT r
-> IsAlmostBalancedT ('ForkTree l (Node n a) r)
ForkIsAlmostBalancedT (IsBalancedT 'EmptyTree
-> Proxy (Node x a)
-> IsBalancedT 'EmptyTree
-> IsBalancedT ('ForkTree 'EmptyTree (Node x a) 'EmptyTree)
forall (l :: Tree) (n :: Tree) (a :: Nat) r.
(BalancedHeights (Height l) (Height n) a ~ 'True) =>
IsBalancedT l
-> Proxy (Node a r)
-> IsBalancedT n
-> IsBalancedT ('ForkTree l (Node a r) n)
ForkIsBalancedT IsBalancedT 'EmptyTree
EmptyIsBalancedT Proxy (Node x a)
pNode IsBalancedT 'EmptyTree
EmptyIsBalancedT) Proxy (Node n a)
pNode' IsBalancedT r
rIsBalanced)

instance
  ( l ~ 'ForkTree ll (Node ln lna) lr,
    o ~ CmpNat x ln,
    ProofIsBalancedInsert' x a l o,
    ProofIsBalancedBalance ('ForkTree (Insert' x a l o) (Node n a1) r)
  ) =>
  ProofIsBalancedInsert' x a ('ForkTree ('ForkTree ll (Node ln lna) lr) (Node n a1) r) 'LT
  where
  proofIsBalancedInsert' :: Proxy (Node x a)
-> IsBalancedT
     ('ForkTree ('ForkTree ll (Node ln lna) lr) (Node n a1) r)
-> Proxy 'LT
-> IsBalancedT
     (Insert'
        x a ('ForkTree ('ForkTree ll (Node ln lna) lr) (Node n a1) r) 'LT)
proofIsBalancedInsert' Proxy (Node x a)
pNode (ForkIsBalancedT IsBalancedT l
lIsBalanced Proxy (Node n a)
pNode' IsBalancedT r
rIsBalanced) Proxy 'LT
_ =
    IsAlmostBalancedT
  ('ForkTree
     (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n a) r)
-> IsBalancedT
     (Balance
        ('ForkTree
           (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n a) r))
forall (t :: Tree).
ProofIsBalancedBalance t =>
IsAlmostBalancedT t -> IsBalancedT (Balance t)
proofIsBalancedBalance (IsAlmostBalancedT
   ('ForkTree
      (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n a) r)
 -> IsBalancedT
      (Balance
         ('ForkTree
            (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n a) r)))
-> IsAlmostBalancedT
     ('ForkTree
        (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n a) r)
-> IsBalancedT
     (Balance
        ('ForkTree
           (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n a) r))
forall a b. (a -> b) -> a -> b
$ IsBalancedT (Insert' x a ('ForkTree ll (Node ln lna) lr) o)
-> Proxy (Node n a)
-> IsBalancedT r
-> IsAlmostBalancedT
     ('ForkTree
        (Insert' x a ('ForkTree ll (Node ln lna) lr) o) (Node n a) r)
forall (l :: Tree) (n :: Nat) a (r :: Tree).
IsBalancedT l
-> Proxy (Node n a)
-> IsBalancedT r
-> IsAlmostBalancedT ('ForkTree l (Node n a) r)
ForkIsAlmostBalancedT IsBalancedT (Insert' x a ('ForkTree ll (Node ln lna) lr) o)
IsBalancedT (Insert x a l)
lIsBalanced' Proxy (Node n a)
pNode' IsBalancedT r
rIsBalanced
    where
      lIsBalanced' :: IsBalancedT (Insert x a l)
lIsBalanced' = Proxy (Node x a) -> IsBalancedT l -> IsBalancedT (Insert x a l)
forall (x :: Nat) a (t :: Tree).
ProofIsBalancedInsert x a t =>
Proxy (Node x a) -> IsBalancedT t -> IsBalancedT (Insert x a t)
proofIsBalancedInsert Proxy (Node x a)
pNode IsBalancedT l
lIsBalanced

instance
  (ProofIsBalancedBalance ('ForkTree l (Node n a1) ('ForkTree 'EmptyTree (Node x a) 'EmptyTree))) =>
  ProofIsBalancedInsert' x a ('ForkTree l (Node n a1) 'EmptyTree) 'GT
  where
  proofIsBalancedInsert' :: Proxy (Node x a)
-> IsBalancedT ('ForkTree l (Node n a1) 'EmptyTree)
-> Proxy 'GT
-> IsBalancedT
     (Insert' x a ('ForkTree l (Node n a1) 'EmptyTree) 'GT)
proofIsBalancedInsert' Proxy (Node x a)
pNode (ForkIsBalancedT IsBalancedT l
lIsBalanced Proxy (Node n a)
pNode' IsBalancedT r
_) Proxy 'GT
_ =
    IsAlmostBalancedT
  ('ForkTree
     l (Node n a) ('ForkTree 'EmptyTree (Node x a) 'EmptyTree))
-> IsBalancedT
     (Balance
        ('ForkTree
           l (Node n a) ('ForkTree 'EmptyTree (Node x a) 'EmptyTree)))
forall (t :: Tree).
ProofIsBalancedBalance t =>
IsAlmostBalancedT t -> IsBalancedT (Balance t)
proofIsBalancedBalance (IsAlmostBalancedT
   ('ForkTree
      l (Node n a) ('ForkTree 'EmptyTree (Node x a) 'EmptyTree))
 -> IsBalancedT
      (Balance
         ('ForkTree
            l (Node n a) ('ForkTree 'EmptyTree (Node x a) 'EmptyTree))))
-> IsAlmostBalancedT
     ('ForkTree
        l (Node n a) ('ForkTree 'EmptyTree (Node x a) 'EmptyTree))
-> IsBalancedT
     (Balance
        ('ForkTree
           l (Node n a) ('ForkTree 'EmptyTree (Node x a) 'EmptyTree)))
forall a b. (a -> b) -> a -> b
$ IsBalancedT l
-> Proxy (Node n a)
-> IsBalancedT ('ForkTree 'EmptyTree (Node x a) 'EmptyTree)
-> IsAlmostBalancedT
     ('ForkTree
        l (Node n a) ('ForkTree 'EmptyTree (Node x a) 'EmptyTree))
forall (l :: Tree) (n :: Nat) a (r :: Tree).
IsBalancedT l
-> Proxy (Node n a)
-> IsBalancedT r
-> IsAlmostBalancedT ('ForkTree l (Node n a) r)
ForkIsAlmostBalancedT IsBalancedT l
lIsBalanced Proxy (Node n a)
pNode' (IsBalancedT 'EmptyTree
-> Proxy (Node x a)
-> IsBalancedT 'EmptyTree
-> IsBalancedT ('ForkTree 'EmptyTree (Node x a) 'EmptyTree)
forall (l :: Tree) (n :: Tree) (a :: Nat) r.
(BalancedHeights (Height l) (Height n) a ~ 'True) =>
IsBalancedT l
-> Proxy (Node a r)
-> IsBalancedT n
-> IsBalancedT ('ForkTree l (Node a r) n)
ForkIsBalancedT IsBalancedT 'EmptyTree
EmptyIsBalancedT Proxy (Node x a)
pNode IsBalancedT 'EmptyTree
EmptyIsBalancedT)

instance
  ( r ~ 'ForkTree rl (Node rn rna) rr,
    o ~ CmpNat x rn,
    ProofIsBalancedInsert' x a r o,
    ProofIsBalancedBalance ('ForkTree l (Node n a1) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))
  ) =>
  ProofIsBalancedInsert' x a ('ForkTree l (Node n a1) ('ForkTree rl (Node rn rna) rr)) 'GT
  where
  proofIsBalancedInsert' :: Proxy (Node x a)
-> IsBalancedT
     ('ForkTree l (Node n a1) ('ForkTree rl (Node rn rna) rr))
-> Proxy 'GT
-> IsBalancedT
     (Insert'
        x a ('ForkTree l (Node n a1) ('ForkTree rl (Node rn rna) rr)) 'GT)
proofIsBalancedInsert' Proxy (Node x a)
pNode (ForkIsBalancedT IsBalancedT l
lIsBalanced Proxy (Node n a)
pNode' IsBalancedT r
rIsBalanced) Proxy 'GT
_ =
    IsAlmostBalancedT
  ('ForkTree
     l (Node n a) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))
-> IsBalancedT
     (Balance
        ('ForkTree
           l (Node n a) (Insert' x a ('ForkTree rl (Node rn rna) rr) o)))
forall (t :: Tree).
ProofIsBalancedBalance t =>
IsAlmostBalancedT t -> IsBalancedT (Balance t)
proofIsBalancedBalance (IsAlmostBalancedT
   ('ForkTree
      l (Node n a) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))
 -> IsBalancedT
      (Balance
         ('ForkTree
            l (Node n a) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))))
-> IsAlmostBalancedT
     ('ForkTree
        l (Node n a) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))
-> IsBalancedT
     (Balance
        ('ForkTree
           l (Node n a) (Insert' x a ('ForkTree rl (Node rn rna) rr) o)))
forall a b. (a -> b) -> a -> b
$ IsBalancedT l
-> Proxy (Node n a)
-> IsBalancedT (Insert' x a ('ForkTree rl (Node rn rna) rr) o)
-> IsAlmostBalancedT
     ('ForkTree
        l (Node n a) (Insert' x a ('ForkTree rl (Node rn rna) rr) o))
forall (l :: Tree) (n :: Nat) a (r :: Tree).
IsBalancedT l
-> Proxy (Node n a)
-> IsBalancedT r
-> IsAlmostBalancedT ('ForkTree l (Node n a) r)
ForkIsAlmostBalancedT IsBalancedT l
lIsBalanced Proxy (Node n a)
pNode' IsBalancedT (Insert' x a ('ForkTree rl (Node rn rna) rr) o)
IsBalancedT (Insert x a r)
rIsBalanced'
    where
      rIsBalanced' :: IsBalancedT (Insert x a r)
rIsBalanced' = Proxy (Node x a) -> IsBalancedT r -> IsBalancedT (Insert x a r)
forall (x :: Nat) a (t :: Tree).
ProofIsBalancedInsert x a t =>
Proxy (Node x a) -> IsBalancedT t -> IsBalancedT (Insert x a t)
proofIsBalancedInsert Proxy (Node x a)
pNode IsBalancedT r
rIsBalanced