{-# LANGUAGE DataKinds #-}
{-# LANGUAGE DerivingStrategies #-}
{-# LANGUAGE Safe #-}
{-# OPTIONS_GHC -Wno-missing-export-lists #-}
{-# OPTIONS_GHC -Wno-missing-exported-signatures #-}
{-# OPTIONS_GHC -Wno-missing-signatures #-}
{-# OPTIONS_HADDOCK hide #-}

module Data.Tree.BST.Extern.Examples where

import Data.Proxy (Proxy (Proxy))
import Data.Tree.BST.Extern
  ( deleteBST,
    emptyBST,
    insertBST,
    lookupBST,
  )
import Prelude
  ( Bool (False, True),
    Float,
    Int,
    Show,
    String,
  )

p0 :: Proxy 0
p0 = Proxy 0
forall {k} (t :: k). Proxy t
Proxy :: Proxy 0

p1 :: Proxy 1
p1 = Proxy 1
forall {k} (t :: k). Proxy t
Proxy :: Proxy 1

p2 :: Proxy 2
p2 = Proxy 2
forall {k} (t :: k). Proxy t
Proxy :: Proxy 2

p3 :: Proxy 3
p3 = Proxy 3
forall {k} (t :: k). Proxy t
Proxy :: Proxy 3

p4 :: Proxy 4
p4 = Proxy 4
forall {k} (t :: k). Proxy t
Proxy :: Proxy 4

p5 :: Proxy 5
p5 = Proxy 5
forall {k} (t :: k). Proxy t
Proxy :: Proxy 5

p6 :: Proxy 6
p6 = Proxy 6
forall {k} (t :: k). Proxy t
Proxy :: Proxy 6

p7 :: Proxy 7
p7 = Proxy 7
forall {k} (t :: k). Proxy t
Proxy :: Proxy 7

bste :: BST 'EmptyTree
bste = BST 'EmptyTree
emptyBST

bst1 :: BST (Insert 4 Char 'EmptyTree)
bst1 = Proxy 4 -> Char -> BST 'EmptyTree -> BST (Insert 4 Char 'EmptyTree)
forall (x :: Nat) a (t :: Tree).
(Insertable x a t, ProofIsBSTInsert x a t) =>
Proxy x -> a -> BST t -> BST (Insert x a t)
insertBST Proxy 4
p4 Char
'f' BST 'EmptyTree
bste

bst2 :: BST (Insert 2 Int ('ForkTree 'EmptyTree (Node 4 Char) 'EmptyTree))
bst2 = Proxy 2
-> Int
-> BST ('ForkTree 'EmptyTree (Node 4 Char) 'EmptyTree)
-> BST
     (Insert 2 Int ('ForkTree 'EmptyTree (Node 4 Char) 'EmptyTree))
forall (x :: Nat) a (t :: Tree).
(Insertable x a t, ProofIsBSTInsert x a t) =>
Proxy x -> a -> BST t -> BST (Insert x a t)
insertBST Proxy 2
p2 (Int
4 :: Int) BST ('ForkTree 'EmptyTree (Node 4 Char) 'EmptyTree)
bst1

bst3 :: BST
  (Insert
     6
     [Char]
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 2 Int) 'EmptyTree)
        (Node 4 Char)
        'EmptyTree))
bst3 = Proxy 6
-> [Char]
-> BST
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 2 Int) 'EmptyTree)
        (Node 4 Char)
        'EmptyTree)
-> BST
     (Insert
        6
        [Char]
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 2 Int) 'EmptyTree)
           (Node 4 Char)
           'EmptyTree))
forall (x :: Nat) a (t :: Tree).
(Insertable x a t, ProofIsBSTInsert x a t) =>
Proxy x -> a -> BST t -> BST (Insert x a t)
insertBST Proxy 6
p6 [Char]
"lala" BST
  ('ForkTree
     ('ForkTree 'EmptyTree (Node 2 Int) 'EmptyTree)
     (Node 4 Char)
     'EmptyTree)
bst2

bst4 :: BST
  (Insert
     3
     Bool
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 2 Int) 'EmptyTree)
        (Node 4 Char)
        ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)))
bst4 = Proxy 3
-> Bool
-> BST
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 2 Int) 'EmptyTree)
        (Node 4 Char)
        ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree))
-> BST
     (Insert
        3
        Bool
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 2 Int) 'EmptyTree)
           (Node 4 Char)
           ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)))
forall (x :: Nat) a (t :: Tree).
(Insertable x a t, ProofIsBSTInsert x a t) =>
Proxy x -> a -> BST t -> BST (Insert x a t)
insertBST Proxy 3
p3 Bool
True BST
  ('ForkTree
     ('ForkTree 'EmptyTree (Node 2 Int) 'EmptyTree)
     (Node 4 Char)
     ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree))
bst3

bst5 :: BST
  (Insert
     5
     [Int]
     ('ForkTree
        ('ForkTree
           'EmptyTree
           (Node 2 Int)
           ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
        (Node 4 Char)
        ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)))
bst5 = Proxy 5
-> [Int]
-> BST
     ('ForkTree
        ('ForkTree
           'EmptyTree
           (Node 2 Int)
           ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
        (Node 4 Char)
        ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree))
-> BST
     (Insert
        5
        [Int]
        ('ForkTree
           ('ForkTree
              'EmptyTree
              (Node 2 Int)
              ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
           (Node 4 Char)
           ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree)))
forall (x :: Nat) a (t :: Tree).
(Insertable x a t, ProofIsBSTInsert x a t) =>
Proxy x -> a -> BST t -> BST (Insert x a t)
insertBST Proxy 5
p5 ([Int
1, Int
2, Int
3] :: [Int]) BST
  ('ForkTree
     ('ForkTree
        'EmptyTree
        (Node 2 Int)
        ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
     (Node 4 Char)
     ('ForkTree 'EmptyTree (Node 6 [Char]) 'EmptyTree))
bst4

bst6 :: BST
  (Insert
     0
     Float
     ('ForkTree
        ('ForkTree
           'EmptyTree
           (Node 2 Int)
           ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
        (Node 4 Char)
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 5 [Int]) 'EmptyTree)
           (Node 6 [Char])
           'EmptyTree)))
bst6 = Proxy 0
-> Float
-> BST
     ('ForkTree
        ('ForkTree
           'EmptyTree
           (Node 2 Int)
           ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
        (Node 4 Char)
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 5 [Int]) 'EmptyTree)
           (Node 6 [Char])
           'EmptyTree))
-> BST
     (Insert
        0
        Float
        ('ForkTree
           ('ForkTree
              'EmptyTree
              (Node 2 Int)
              ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
           (Node 4 Char)
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 5 [Int]) 'EmptyTree)
              (Node 6 [Char])
              'EmptyTree)))
forall (x :: Nat) a (t :: Tree).
(Insertable x a t, ProofIsBSTInsert x a t) =>
Proxy x -> a -> BST t -> BST (Insert x a t)
insertBST Proxy 0
p0 (Float
1.8 :: Float) BST
  ('ForkTree
     ('ForkTree
        'EmptyTree
        (Node 2 Int)
        ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
     (Node 4 Char)
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 5 [Int]) 'EmptyTree)
        (Node 6 [Char])
        'EmptyTree))
bst5

bst7 :: BST
  (Insert
     7
     [Bool]
     ('ForkTree
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
           (Node 2 Int)
           ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
        (Node 4 Char)
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 5 [Int]) 'EmptyTree)
           (Node 6 [Char])
           'EmptyTree)))
bst7 = Proxy 7
-> [Bool]
-> BST
     ('ForkTree
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
           (Node 2 Int)
           ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
        (Node 4 Char)
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 5 [Int]) 'EmptyTree)
           (Node 6 [Char])
           'EmptyTree))
-> BST
     (Insert
        7
        [Bool]
        ('ForkTree
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
              (Node 2 Int)
              ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
           (Node 4 Char)
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 5 [Int]) 'EmptyTree)
              (Node 6 [Char])
              'EmptyTree)))
forall (x :: Nat) a (t :: Tree).
(Insertable x a t, ProofIsBSTInsert x a t) =>
Proxy x -> a -> BST t -> BST (Insert x a t)
insertBST Proxy 7
p7 [Bool
False] BST
  ('ForkTree
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
        (Node 2 Int)
        ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
     (Node 4 Char)
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 5 [Int]) 'EmptyTree)
        (Node 6 [Char])
        'EmptyTree))
bst6

data SomeData = SD
  deriving stock (Int -> SomeData -> ShowS
[SomeData] -> ShowS
SomeData -> [Char]
(Int -> SomeData -> ShowS)
-> (SomeData -> [Char]) -> ([SomeData] -> ShowS) -> Show SomeData
forall a.
(Int -> a -> ShowS) -> (a -> [Char]) -> ([a] -> ShowS) -> Show a
showList :: [SomeData] -> ShowS
$cshowList :: [SomeData] -> ShowS
show :: SomeData -> [Char]
$cshow :: SomeData -> [Char]
showsPrec :: Int -> SomeData -> ShowS
$cshowsPrec :: Int -> SomeData -> ShowS
Show)

bst8 :: BST
  (Insert
     7
     SomeData
     ('ForkTree
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
           (Node 2 Int)
           ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
        (Node 4 Char)
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 5 [Int]) 'EmptyTree)
           (Node 6 [Char])
           ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree))))
bst8 = Proxy 7
-> SomeData
-> BST
     ('ForkTree
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
           (Node 2 Int)
           ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
        (Node 4 Char)
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 5 [Int]) 'EmptyTree)
           (Node 6 [Char])
           ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree)))
-> BST
     (Insert
        7
        SomeData
        ('ForkTree
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
              (Node 2 Int)
              ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
           (Node 4 Char)
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 5 [Int]) 'EmptyTree)
              (Node 6 [Char])
              ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree))))
forall (x :: Nat) a (t :: Tree).
(Insertable x a t, ProofIsBSTInsert x a t) =>
Proxy x -> a -> BST t -> BST (Insert x a t)
insertBST Proxy 7
p7 SomeData
SD BST
  ('ForkTree
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
        (Node 2 Int)
        ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
     (Node 4 Char)
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 5 [Int]) 'EmptyTree)
        (Node 6 [Char])
        ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree)))
bst7

l1 :: String
l1 :: [Char]
l1 = Proxy 6
-> BST
     ('ForkTree
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
           (Node 2 Int)
           ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
        (Node 4 Char)
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 5 [Int]) 'EmptyTree)
           (Node 6 [Char])
           ('ForkTree 'EmptyTree (Node 7 SomeData) 'EmptyTree)))
-> [Char]
forall (t :: Tree) (l :: Tree) (n :: Nat) a1 (r :: Tree) (x :: Nat)
       a.
(t ~ 'ForkTree l (Node n a1) r, Member x t t ~ 'True,
 Lookupable x a t) =>
Proxy x -> BST t -> a
lookupBST Proxy 6
p6 BST
  ('ForkTree
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
        (Node 2 Int)
        ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
     (Node 4 Char)
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 5 [Int]) 'EmptyTree)
        (Node 6 [Char])
        ('ForkTree 'EmptyTree (Node 7 SomeData) 'EmptyTree)))
bst8

-- | Error: key p1 ('S 'Z) is not in the tree bst8
-- err = lookupBST p1 bst8
bst9 :: BST
  (Delete
     7
     ('ForkTree
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
           (Node 2 Int)
           ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
        (Node 4 Char)
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 5 [Int]) 'EmptyTree)
           (Node 6 [Char])
           ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree))))
bst9 = Proxy 7
-> BST
     ('ForkTree
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
           (Node 2 Int)
           ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
        (Node 4 Char)
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 5 [Int]) 'EmptyTree)
           (Node 6 [Char])
           ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree)))
-> BST
     (Delete
        7
        ('ForkTree
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
              (Node 2 Int)
              ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
           (Node 4 Char)
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 5 [Int]) 'EmptyTree)
              (Node 6 [Char])
              ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree))))
forall (x :: Nat) (t :: Tree).
(Deletable x t, ProofIsBSTDelete x t) =>
Proxy x -> BST t -> BST (Delete x t)
deleteBST Proxy 7
p7 BST
  ('ForkTree
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
        (Node 2 Int)
        ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
     (Node 4 Char)
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 5 [Int]) 'EmptyTree)
        (Node 6 [Char])
        ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree)))
bst7

bst10 :: BST
  (Delete
     4
     ('ForkTree
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
           (Node 2 Int)
           ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
        (Node 4 Char)
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 5 [Int]) 'EmptyTree)
           (Node 6 [Char])
           ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree))))
bst10 = Proxy 4
-> BST
     ('ForkTree
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
           (Node 2 Int)
           ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
        (Node 4 Char)
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 5 [Int]) 'EmptyTree)
           (Node 6 [Char])
           ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree)))
-> BST
     (Delete
        4
        ('ForkTree
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
              (Node 2 Int)
              ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
           (Node 4 Char)
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 5 [Int]) 'EmptyTree)
              (Node 6 [Char])
              ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree))))
forall (x :: Nat) (t :: Tree).
(Deletable x t, ProofIsBSTDelete x t) =>
Proxy x -> BST t -> BST (Delete x t)
deleteBST Proxy 4
p4 BST
  ('ForkTree
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
        (Node 2 Int)
        ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
     (Node 4 Char)
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 5 [Int]) 'EmptyTree)
        (Node 6 [Char])
        ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree)))
bst7

bst11 :: BST
  (Delete
     1
     ('ForkTree
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
           (Node 2 Int)
           ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
        (Node 4 Char)
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 5 [Int]) 'EmptyTree)
           (Node 6 [Char])
           ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree))))
bst11 = Proxy 1
-> BST
     ('ForkTree
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
           (Node 2 Int)
           ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
        (Node 4 Char)
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 5 [Int]) 'EmptyTree)
           (Node 6 [Char])
           ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree)))
-> BST
     (Delete
        1
        ('ForkTree
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
              (Node 2 Int)
              ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
           (Node 4 Char)
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 5 [Int]) 'EmptyTree)
              (Node 6 [Char])
              ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree))))
forall (x :: Nat) (t :: Tree).
(Deletable x t, ProofIsBSTDelete x t) =>
Proxy x -> BST t -> BST (Delete x t)
deleteBST Proxy 1
p1 BST
  ('ForkTree
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
        (Node 2 Int)
        ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
     (Node 4 Char)
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 5 [Int]) 'EmptyTree)
        (Node 6 [Char])
        ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree)))
bst7

bst12 :: BST
  (Delete
     0
     ('ForkTree
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
           (Node 2 Int)
           ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
        (Node 4 Char)
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 5 [Int]) 'EmptyTree)
           (Node 6 [Char])
           ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree))))
bst12 = Proxy 0
-> BST
     ('ForkTree
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
           (Node 2 Int)
           ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
        (Node 4 Char)
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 5 [Int]) 'EmptyTree)
           (Node 6 [Char])
           ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree)))
-> BST
     (Delete
        0
        ('ForkTree
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
              (Node 2 Int)
              ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
           (Node 4 Char)
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 5 [Int]) 'EmptyTree)
              (Node 6 [Char])
              ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree))))
forall (x :: Nat) (t :: Tree).
(Deletable x t, ProofIsBSTDelete x t) =>
Proxy x -> BST t -> BST (Delete x t)
deleteBST Proxy 0
p0 BST
  ('ForkTree
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
        (Node 2 Int)
        ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
     (Node 4 Char)
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 5 [Int]) 'EmptyTree)
        (Node 6 [Char])
        ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree)))
bst7

bst13 :: BST
  (Delete
     2
     ('ForkTree
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
           (Node 2 Int)
           ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
        (Node 4 Char)
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 5 [Int]) 'EmptyTree)
           (Node 6 [Char])
           ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree))))
bst13 = Proxy 2
-> BST
     ('ForkTree
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
           (Node 2 Int)
           ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
        (Node 4 Char)
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 5 [Int]) 'EmptyTree)
           (Node 6 [Char])
           ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree)))
-> BST
     (Delete
        2
        ('ForkTree
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
              (Node 2 Int)
              ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
           (Node 4 Char)
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 5 [Int]) 'EmptyTree)
              (Node 6 [Char])
              ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree))))
forall (x :: Nat) (t :: Tree).
(Deletable x t, ProofIsBSTDelete x t) =>
Proxy x -> BST t -> BST (Delete x t)
deleteBST Proxy 2
p2 BST
  ('ForkTree
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
        (Node 2 Int)
        ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
     (Node 4 Char)
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 5 [Int]) 'EmptyTree)
        (Node 6 [Char])
        ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree)))
bst7

bst14 :: BST
  (Delete
     6
     ('ForkTree
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
           (Node 2 Int)
           ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
        (Node 4 Char)
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 5 [Int]) 'EmptyTree)
           (Node 6 [Char])
           ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree))))
bst14 = Proxy 6
-> BST
     ('ForkTree
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
           (Node 2 Int)
           ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
        (Node 4 Char)
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 5 [Int]) 'EmptyTree)
           (Node 6 [Char])
           ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree)))
-> BST
     (Delete
        6
        ('ForkTree
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
              (Node 2 Int)
              ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
           (Node 4 Char)
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 5 [Int]) 'EmptyTree)
              (Node 6 [Char])
              ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree))))
forall (x :: Nat) (t :: Tree).
(Deletable x t, ProofIsBSTDelete x t) =>
Proxy x -> BST t -> BST (Delete x t)
deleteBST Proxy 6
p6 BST
  ('ForkTree
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
        (Node 2 Int)
        ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
     (Node 4 Char)
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 5 [Int]) 'EmptyTree)
        (Node 6 [Char])
        ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree)))
bst7

bst15 :: BST
  (Delete
     5
     ('ForkTree
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
           (Node 2 Int)
           ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
        (Node 4 Char)
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 5 [Int]) 'EmptyTree)
           (Node 6 [Char])
           ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree))))
bst15 = Proxy 5
-> BST
     ('ForkTree
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
           (Node 2 Int)
           ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
        (Node 4 Char)
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 5 [Int]) 'EmptyTree)
           (Node 6 [Char])
           ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree)))
-> BST
     (Delete
        5
        ('ForkTree
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
              (Node 2 Int)
              ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
           (Node 4 Char)
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 5 [Int]) 'EmptyTree)
              (Node 6 [Char])
              ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree))))
forall (x :: Nat) (t :: Tree).
(Deletable x t, ProofIsBSTDelete x t) =>
Proxy x -> BST t -> BST (Delete x t)
deleteBST Proxy 5
p5 BST
  ('ForkTree
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
        (Node 2 Int)
        ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
     (Node 4 Char)
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 5 [Int]) 'EmptyTree)
        (Node 6 [Char])
        ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree)))
bst7

bst16 :: BST
  (Delete
     3
     ('ForkTree
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
           (Node 2 Int)
           ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
        (Node 4 Char)
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 5 [Int]) 'EmptyTree)
           (Node 6 [Char])
           ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree))))
bst16 = Proxy 3
-> BST
     ('ForkTree
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
           (Node 2 Int)
           ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
        (Node 4 Char)
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 5 [Int]) 'EmptyTree)
           (Node 6 [Char])
           ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree)))
-> BST
     (Delete
        3
        ('ForkTree
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
              (Node 2 Int)
              ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
           (Node 4 Char)
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 5 [Int]) 'EmptyTree)
              (Node 6 [Char])
              ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree))))
forall (x :: Nat) (t :: Tree).
(Deletable x t, ProofIsBSTDelete x t) =>
Proxy x -> BST t -> BST (Delete x t)
deleteBST Proxy 3
p3 BST
  ('ForkTree
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 0 Float) 'EmptyTree)
        (Node 2 Int)
        ('ForkTree 'EmptyTree (Node 3 Bool) 'EmptyTree))
     (Node 4 Char)
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 5 [Int]) 'EmptyTree)
        (Node 6 [Char])
        ('ForkTree 'EmptyTree (Node 7 [Bool]) 'EmptyTree)))
bst7