{-# LANGUAGE DataKinds #-}
{-# 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.AVL.Intern.Examples where

import Data.Proxy (Proxy (Proxy))
import Data.Tree.AVL.Intern
  ( deleteAVL,
    emptyAVL,
    insertAVL,
    lookupAVL,
  )
import Prelude (Bool (False, True), Float, Int, String)

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

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

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

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

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

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

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

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

-- | Test Balanced Binary Tree
avle :: AVL 'EmptyTree
avle = AVL 'EmptyTree
emptyAVL

avlt1 :: AVL (Insert 20 Char 'EmptyTree)
avlt1 = Proxy 20
-> Char -> AVL 'EmptyTree -> AVL (Insert 20 Char 'EmptyTree)
forall (x :: Nat) a (t :: Tree).
Insertable x a t =>
Proxy x -> a -> AVL t -> AVL (Insert x a t)
insertAVL (Proxy 20
forall {k} (t :: k). Proxy t
Proxy :: Proxy 20) Char
'f' AVL 'EmptyTree
avle

avlt2 :: AVL
  (Insert 60 Int ('ForkTree 'EmptyTree (Node 20 Char) 'EmptyTree))
avlt2 = Proxy 60
-> Int
-> AVL ('ForkTree 'EmptyTree (Node 20 Char) 'EmptyTree)
-> AVL
     (Insert 60 Int ('ForkTree 'EmptyTree (Node 20 Char) 'EmptyTree))
forall (x :: Nat) a (t :: Tree).
Insertable x a t =>
Proxy x -> a -> AVL t -> AVL (Insert x a t)
insertAVL (Proxy 60
forall {k} (t :: k). Proxy t
Proxy :: Proxy 60) (Int
4 :: Int) AVL ('ForkTree 'EmptyTree (Node 20 Char) 'EmptyTree)
avlt1

avlt3 :: AVL
  (Insert
     30
     [Char]
     ('ForkTree
        'EmptyTree
        (Node 20 Char)
        ('ForkTree 'EmptyTree (Node 60 Int) 'EmptyTree)))
avlt3 = Proxy 30
-> [Char]
-> AVL
     ('ForkTree
        'EmptyTree
        (Node 20 Char)
        ('ForkTree 'EmptyTree (Node 60 Int) 'EmptyTree))
-> AVL
     (Insert
        30
        [Char]
        ('ForkTree
           'EmptyTree
           (Node 20 Char)
           ('ForkTree 'EmptyTree (Node 60 Int) 'EmptyTree)))
forall (x :: Nat) a (t :: Tree).
Insertable x a t =>
Proxy x -> a -> AVL t -> AVL (Insert x a t)
insertAVL (Proxy 30
forall {k} (t :: k). Proxy t
Proxy :: Proxy 30) [Char]
"lala" AVL
  ('ForkTree
     'EmptyTree
     (Node 20 Char)
     ('ForkTree 'EmptyTree (Node 60 Int) 'EmptyTree))
avlt2

avlt4 :: AVL
  (Insert
     50
     Bool
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 20 Char) 'EmptyTree)
        (Node 30 [Char])
        ('ForkTree 'EmptyTree (Node 60 Int) 'EmptyTree)))
avlt4 = Proxy 50
-> Bool
-> AVL
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 20 Char) 'EmptyTree)
        (Node 30 [Char])
        ('ForkTree 'EmptyTree (Node 60 Int) 'EmptyTree))
-> AVL
     (Insert
        50
        Bool
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 20 Char) 'EmptyTree)
           (Node 30 [Char])
           ('ForkTree 'EmptyTree (Node 60 Int) 'EmptyTree)))
forall (x :: Nat) a (t :: Tree).
Insertable x a t =>
Proxy x -> a -> AVL t -> AVL (Insert x a t)
insertAVL (Proxy 50
forall {k} (t :: k). Proxy t
Proxy :: Proxy 50) Bool
True AVL
  ('ForkTree
     ('ForkTree 'EmptyTree (Node 20 Char) 'EmptyTree)
     (Node 30 [Char])
     ('ForkTree 'EmptyTree (Node 60 Int) 'EmptyTree))
avlt3

avlt5 :: AVL
  (Insert
     0
     [Int]
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 20 Char) 'EmptyTree)
        (Node 30 [Char])
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 50 Bool) 'EmptyTree)
           (Node 60 Int)
           'EmptyTree)))
avlt5 = Proxy 0
-> [Int]
-> AVL
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 20 Char) 'EmptyTree)
        (Node 30 [Char])
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 50 Bool) 'EmptyTree)
           (Node 60 Int)
           'EmptyTree))
-> AVL
     (Insert
        0
        [Int]
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 20 Char) 'EmptyTree)
           (Node 30 [Char])
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 50 Bool) 'EmptyTree)
              (Node 60 Int)
              'EmptyTree)))
forall (x :: Nat) a (t :: Tree).
Insertable x a t =>
Proxy x -> a -> AVL t -> AVL (Insert x a t)
insertAVL (Proxy 0
forall {k} (t :: k). Proxy t
Proxy :: Proxy 0) ([Int
1, Int
2, Int
3] :: [Int]) AVL
  ('ForkTree
     ('ForkTree 'EmptyTree (Node 20 Char) 'EmptyTree)
     (Node 30 [Char])
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 50 Bool) 'EmptyTree)
        (Node 60 Int)
        'EmptyTree))
avlt4

avlt6 :: AVL
  (Insert
     70
     Float
     ('ForkTree
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 [Int]) 'EmptyTree)
           (Node 20 Char)
           'EmptyTree)
        (Node 30 [Char])
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 50 Bool) 'EmptyTree)
           (Node 60 Int)
           'EmptyTree)))
avlt6 = Proxy 70
-> Float
-> AVL
     ('ForkTree
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 [Int]) 'EmptyTree)
           (Node 20 Char)
           'EmptyTree)
        (Node 30 [Char])
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 50 Bool) 'EmptyTree)
           (Node 60 Int)
           'EmptyTree))
-> AVL
     (Insert
        70
        Float
        ('ForkTree
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 0 [Int]) 'EmptyTree)
              (Node 20 Char)
              'EmptyTree)
           (Node 30 [Char])
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 50 Bool) 'EmptyTree)
              (Node 60 Int)
              'EmptyTree)))
forall (x :: Nat) a (t :: Tree).
Insertable x a t =>
Proxy x -> a -> AVL t -> AVL (Insert x a t)
insertAVL (Proxy 70
forall {k} (t :: k). Proxy t
Proxy :: Proxy 70) (Float
1.8 :: Float) AVL
  ('ForkTree
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 0 [Int]) 'EmptyTree)
        (Node 20 Char)
        'EmptyTree)
     (Node 30 [Char])
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 50 Bool) 'EmptyTree)
        (Node 60 Int)
        'EmptyTree))
avlt5

avlt7 :: AVL
  (Insert
     70
     [Bool]
     ('ForkTree
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 [Int]) 'EmptyTree)
           (Node 20 Char)
           'EmptyTree)
        (Node 30 [Char])
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 50 Bool) 'EmptyTree)
           (Node 60 Int)
           ('ForkTree 'EmptyTree (Node 70 Float) 'EmptyTree))))
avlt7 = Proxy 70
-> [Bool]
-> AVL
     ('ForkTree
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 [Int]) 'EmptyTree)
           (Node 20 Char)
           'EmptyTree)
        (Node 30 [Char])
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 50 Bool) 'EmptyTree)
           (Node 60 Int)
           ('ForkTree 'EmptyTree (Node 70 Float) 'EmptyTree)))
-> AVL
     (Insert
        70
        [Bool]
        ('ForkTree
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 0 [Int]) 'EmptyTree)
              (Node 20 Char)
              'EmptyTree)
           (Node 30 [Char])
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 50 Bool) 'EmptyTree)
              (Node 60 Int)
              ('ForkTree 'EmptyTree (Node 70 Float) 'EmptyTree))))
forall (x :: Nat) a (t :: Tree).
Insertable x a t =>
Proxy x -> a -> AVL t -> AVL (Insert x a t)
insertAVL (Proxy 70
forall {k} (t :: k). Proxy t
Proxy :: Proxy 70) [Bool
False] AVL
  ('ForkTree
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 0 [Int]) 'EmptyTree)
        (Node 20 Char)
        'EmptyTree)
     (Node 30 [Char])
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 50 Bool) 'EmptyTree)
        (Node 60 Int)
        ('ForkTree 'EmptyTree (Node 70 Float) 'EmptyTree)))
avlt6

avlt8 :: AVL
  (Insert
     75
     Char
     ('ForkTree
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 [Int]) 'EmptyTree)
           (Node 20 Char)
           'EmptyTree)
        (Node 30 [Char])
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 50 Bool) 'EmptyTree)
           (Node 60 Int)
           ('ForkTree 'EmptyTree (Node 70 [Bool]) 'EmptyTree))))
avlt8 = Proxy 75
-> Char
-> AVL
     ('ForkTree
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 [Int]) 'EmptyTree)
           (Node 20 Char)
           'EmptyTree)
        (Node 30 [Char])
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 50 Bool) 'EmptyTree)
           (Node 60 Int)
           ('ForkTree 'EmptyTree (Node 70 [Bool]) 'EmptyTree)))
-> AVL
     (Insert
        75
        Char
        ('ForkTree
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 0 [Int]) 'EmptyTree)
              (Node 20 Char)
              'EmptyTree)
           (Node 30 [Char])
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 50 Bool) 'EmptyTree)
              (Node 60 Int)
              ('ForkTree 'EmptyTree (Node 70 [Bool]) 'EmptyTree))))
forall (x :: Nat) a (t :: Tree).
Insertable x a t =>
Proxy x -> a -> AVL t -> AVL (Insert x a t)
insertAVL (Proxy 75
forall {k} (t :: k). Proxy t
Proxy :: Proxy 75) Char
'a' AVL
  ('ForkTree
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 0 [Int]) 'EmptyTree)
        (Node 20 Char)
        'EmptyTree)
     (Node 30 [Char])
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 50 Bool) 'EmptyTree)
        (Node 60 Int)
        ('ForkTree 'EmptyTree (Node 70 [Bool]) 'EmptyTree)))
avlt7

avlt9 :: AVL
  (Insert
     80
     Char
     ('ForkTree
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 [Int]) 'EmptyTree)
           (Node 20 Char)
           'EmptyTree)
        (Node 30 [Char])
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 50 Bool) 'EmptyTree)
           (Node 60 Int)
           ('ForkTree
              'EmptyTree
              (Node 70 [Bool])
              ('ForkTree 'EmptyTree (Node 75 Char) 'EmptyTree)))))
avlt9 = Proxy 80
-> Char
-> AVL
     ('ForkTree
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 [Int]) 'EmptyTree)
           (Node 20 Char)
           'EmptyTree)
        (Node 30 [Char])
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 50 Bool) 'EmptyTree)
           (Node 60 Int)
           ('ForkTree
              'EmptyTree
              (Node 70 [Bool])
              ('ForkTree 'EmptyTree (Node 75 Char) 'EmptyTree))))
-> AVL
     (Insert
        80
        Char
        ('ForkTree
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 0 [Int]) 'EmptyTree)
              (Node 20 Char)
              'EmptyTree)
           (Node 30 [Char])
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 50 Bool) 'EmptyTree)
              (Node 60 Int)
              ('ForkTree
                 'EmptyTree
                 (Node 70 [Bool])
                 ('ForkTree 'EmptyTree (Node 75 Char) 'EmptyTree)))))
forall (x :: Nat) a (t :: Tree).
Insertable x a t =>
Proxy x -> a -> AVL t -> AVL (Insert x a t)
insertAVL (Proxy 80
forall {k} (t :: k). Proxy t
Proxy :: Proxy 80) Char
'a' AVL
  ('ForkTree
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 0 [Int]) 'EmptyTree)
        (Node 20 Char)
        'EmptyTree)
     (Node 30 [Char])
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 50 Bool) 'EmptyTree)
        (Node 60 Int)
        ('ForkTree
           'EmptyTree
           (Node 70 [Bool])
           ('ForkTree 'EmptyTree (Node 75 Char) 'EmptyTree))))
avlt8

avlt10 :: AVL
  (Insert
     90
     Char
     ('ForkTree
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 [Int]) 'EmptyTree)
           (Node 20 Char)
           'EmptyTree)
        (Node 30 [Char])
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 50 Bool) 'EmptyTree)
           (Node 60 Int)
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 70 [Bool]) 'EmptyTree)
              (Node 75 Char)
              ('ForkTree 'EmptyTree (Node 80 Char) 'EmptyTree)))))
avlt10 = Proxy 90
-> Char
-> AVL
     ('ForkTree
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 [Int]) 'EmptyTree)
           (Node 20 Char)
           'EmptyTree)
        (Node 30 [Char])
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 50 Bool) 'EmptyTree)
           (Node 60 Int)
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 70 [Bool]) 'EmptyTree)
              (Node 75 Char)
              ('ForkTree 'EmptyTree (Node 80 Char) 'EmptyTree))))
-> AVL
     (Insert
        90
        Char
        ('ForkTree
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 0 [Int]) 'EmptyTree)
              (Node 20 Char)
              'EmptyTree)
           (Node 30 [Char])
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 50 Bool) 'EmptyTree)
              (Node 60 Int)
              ('ForkTree
                 ('ForkTree 'EmptyTree (Node 70 [Bool]) 'EmptyTree)
                 (Node 75 Char)
                 ('ForkTree 'EmptyTree (Node 80 Char) 'EmptyTree)))))
forall (x :: Nat) a (t :: Tree).
Insertable x a t =>
Proxy x -> a -> AVL t -> AVL (Insert x a t)
insertAVL (Proxy 90
forall {k} (t :: k). Proxy t
Proxy :: Proxy 90) Char
'a' AVL
  ('ForkTree
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 0 [Int]) 'EmptyTree)
        (Node 20 Char)
        'EmptyTree)
     (Node 30 [Char])
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 50 Bool) 'EmptyTree)
        (Node 60 Int)
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 70 [Bool]) 'EmptyTree)
           (Node 75 Char)
           ('ForkTree 'EmptyTree (Node 80 Char) 'EmptyTree))))
avlt9

l1' :: String
l1' :: [Char]
l1' = Proxy 30
-> AVL
     ('ForkTree
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 [Int]) 'EmptyTree)
           (Node 20 Char)
           'EmptyTree)
        (Node 30 [Char])
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 50 Bool) 'EmptyTree)
           (Node 60 Int)
           ('ForkTree
              'EmptyTree
              (Node 70 [Bool])
              ('ForkTree 'EmptyTree (Node 75 Char) '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 -> AVL t -> a
lookupAVL (Proxy 30
forall {k} (t :: k). Proxy t
Proxy :: Proxy 30) AVL
  ('ForkTree
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 0 [Int]) 'EmptyTree)
        (Node 20 Char)
        'EmptyTree)
     (Node 30 [Char])
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 50 Bool) 'EmptyTree)
        (Node 60 Int)
        ('ForkTree
           'EmptyTree
           (Node 70 [Bool])
           ('ForkTree 'EmptyTree (Node 75 Char) 'EmptyTree))))
avlt8

-- | Error: key 10 is not in the tree avlt8
-- err = lookupAVL (Proxy::Proxy 10) avlt8
avlt11 :: AVL
  (Delete
     20
     ('ForkTree
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 [Int]) 'EmptyTree)
           (Node 20 Char)
           'EmptyTree)
        (Node 30 [Char])
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 50 Bool) 'EmptyTree)
           (Node 60 Int)
           ('ForkTree
              'EmptyTree
              (Node 70 [Bool])
              ('ForkTree 'EmptyTree (Node 75 Char) 'EmptyTree)))))
avlt11 = Proxy 20
-> AVL
     ('ForkTree
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 [Int]) 'EmptyTree)
           (Node 20 Char)
           'EmptyTree)
        (Node 30 [Char])
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 50 Bool) 'EmptyTree)
           (Node 60 Int)
           ('ForkTree
              'EmptyTree
              (Node 70 [Bool])
              ('ForkTree 'EmptyTree (Node 75 Char) 'EmptyTree))))
-> AVL
     (Delete
        20
        ('ForkTree
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 0 [Int]) 'EmptyTree)
              (Node 20 Char)
              'EmptyTree)
           (Node 30 [Char])
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 50 Bool) 'EmptyTree)
              (Node 60 Int)
              ('ForkTree
                 'EmptyTree
                 (Node 70 [Bool])
                 ('ForkTree 'EmptyTree (Node 75 Char) 'EmptyTree)))))
forall (x :: Nat) (t :: Tree).
Deletable x t =>
Proxy x -> AVL t -> AVL (Delete x t)
deleteAVL (Proxy 20
forall {k} (t :: k). Proxy t
Proxy :: Proxy 20) AVL
  ('ForkTree
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 0 [Int]) 'EmptyTree)
        (Node 20 Char)
        'EmptyTree)
     (Node 30 [Char])
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 50 Bool) 'EmptyTree)
        (Node 60 Int)
        ('ForkTree
           'EmptyTree
           (Node 70 [Bool])
           ('ForkTree 'EmptyTree (Node 75 Char) 'EmptyTree))))
avlt8

avlt12 :: AVL
  (Delete
     60
     ('ForkTree
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 [Int]) 'EmptyTree)
           (Node 20 Char)
           'EmptyTree)
        (Node 30 [Char])
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 50 Bool) 'EmptyTree)
           (Node 60 Int)
           ('ForkTree
              'EmptyTree
              (Node 70 [Bool])
              ('ForkTree 'EmptyTree (Node 75 Char) 'EmptyTree)))))
avlt12 = Proxy 60
-> AVL
     ('ForkTree
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 [Int]) 'EmptyTree)
           (Node 20 Char)
           'EmptyTree)
        (Node 30 [Char])
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 50 Bool) 'EmptyTree)
           (Node 60 Int)
           ('ForkTree
              'EmptyTree
              (Node 70 [Bool])
              ('ForkTree 'EmptyTree (Node 75 Char) 'EmptyTree))))
-> AVL
     (Delete
        60
        ('ForkTree
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 0 [Int]) 'EmptyTree)
              (Node 20 Char)
              'EmptyTree)
           (Node 30 [Char])
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 50 Bool) 'EmptyTree)
              (Node 60 Int)
              ('ForkTree
                 'EmptyTree
                 (Node 70 [Bool])
                 ('ForkTree 'EmptyTree (Node 75 Char) 'EmptyTree)))))
forall (x :: Nat) (t :: Tree).
Deletable x t =>
Proxy x -> AVL t -> AVL (Delete x t)
deleteAVL (Proxy 60
forall {k} (t :: k). Proxy t
Proxy :: Proxy 60) AVL
  ('ForkTree
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 0 [Int]) 'EmptyTree)
        (Node 20 Char)
        'EmptyTree)
     (Node 30 [Char])
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 50 Bool) 'EmptyTree)
        (Node 60 Int)
        ('ForkTree
           'EmptyTree
           (Node 70 [Bool])
           ('ForkTree 'EmptyTree (Node 75 Char) 'EmptyTree))))
avlt8

avlt13 :: AVL
  (Delete
     30
     ('ForkTree
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 [Int]) 'EmptyTree)
           (Node 20 Char)
           'EmptyTree)
        (Node 30 [Char])
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 50 Bool) 'EmptyTree)
           (Node 60 Int)
           ('ForkTree
              'EmptyTree
              (Node 70 [Bool])
              ('ForkTree 'EmptyTree (Node 75 Char) 'EmptyTree)))))
avlt13 = Proxy 30
-> AVL
     ('ForkTree
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 [Int]) 'EmptyTree)
           (Node 20 Char)
           'EmptyTree)
        (Node 30 [Char])
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 50 Bool) 'EmptyTree)
           (Node 60 Int)
           ('ForkTree
              'EmptyTree
              (Node 70 [Bool])
              ('ForkTree 'EmptyTree (Node 75 Char) 'EmptyTree))))
-> AVL
     (Delete
        30
        ('ForkTree
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 0 [Int]) 'EmptyTree)
              (Node 20 Char)
              'EmptyTree)
           (Node 30 [Char])
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 50 Bool) 'EmptyTree)
              (Node 60 Int)
              ('ForkTree
                 'EmptyTree
                 (Node 70 [Bool])
                 ('ForkTree 'EmptyTree (Node 75 Char) 'EmptyTree)))))
forall (x :: Nat) (t :: Tree).
Deletable x t =>
Proxy x -> AVL t -> AVL (Delete x t)
deleteAVL (Proxy 30
forall {k} (t :: k). Proxy t
Proxy :: Proxy 30) AVL
  ('ForkTree
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 0 [Int]) 'EmptyTree)
        (Node 20 Char)
        'EmptyTree)
     (Node 30 [Char])
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 50 Bool) 'EmptyTree)
        (Node 60 Int)
        ('ForkTree
           'EmptyTree
           (Node 70 [Bool])
           ('ForkTree 'EmptyTree (Node 75 Char) 'EmptyTree))))
avlt8

avlt14 :: AVL
  (Delete
     50
     ('ForkTree
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 [Int]) 'EmptyTree)
           (Node 20 Char)
           'EmptyTree)
        (Node 30 [Char])
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 50 Bool) 'EmptyTree)
           (Node 60 Int)
           ('ForkTree
              'EmptyTree
              (Node 70 [Bool])
              ('ForkTree 'EmptyTree (Node 75 Char) 'EmptyTree)))))
avlt14 = Proxy 50
-> AVL
     ('ForkTree
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 [Int]) 'EmptyTree)
           (Node 20 Char)
           'EmptyTree)
        (Node 30 [Char])
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 50 Bool) 'EmptyTree)
           (Node 60 Int)
           ('ForkTree
              'EmptyTree
              (Node 70 [Bool])
              ('ForkTree 'EmptyTree (Node 75 Char) 'EmptyTree))))
-> AVL
     (Delete
        50
        ('ForkTree
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 0 [Int]) 'EmptyTree)
              (Node 20 Char)
              'EmptyTree)
           (Node 30 [Char])
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 50 Bool) 'EmptyTree)
              (Node 60 Int)
              ('ForkTree
                 'EmptyTree
                 (Node 70 [Bool])
                 ('ForkTree 'EmptyTree (Node 75 Char) 'EmptyTree)))))
forall (x :: Nat) (t :: Tree).
Deletable x t =>
Proxy x -> AVL t -> AVL (Delete x t)
deleteAVL (Proxy 50
forall {k} (t :: k). Proxy t
Proxy :: Proxy 50) AVL
  ('ForkTree
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 0 [Int]) 'EmptyTree)
        (Node 20 Char)
        'EmptyTree)
     (Node 30 [Char])
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 50 Bool) 'EmptyTree)
        (Node 60 Int)
        ('ForkTree
           'EmptyTree
           (Node 70 [Bool])
           ('ForkTree 'EmptyTree (Node 75 Char) 'EmptyTree))))
avlt8

avlt15 :: AVL
  (Delete
     0
     ('ForkTree
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 [Int]) 'EmptyTree)
           (Node 20 Char)
           'EmptyTree)
        (Node 30 [Char])
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 50 Bool) 'EmptyTree)
           (Node 60 Int)
           ('ForkTree
              'EmptyTree
              (Node 70 [Bool])
              ('ForkTree 'EmptyTree (Node 75 Char) 'EmptyTree)))))
avlt15 = Proxy 0
-> AVL
     ('ForkTree
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 [Int]) 'EmptyTree)
           (Node 20 Char)
           'EmptyTree)
        (Node 30 [Char])
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 50 Bool) 'EmptyTree)
           (Node 60 Int)
           ('ForkTree
              'EmptyTree
              (Node 70 [Bool])
              ('ForkTree 'EmptyTree (Node 75 Char) 'EmptyTree))))
-> AVL
     (Delete
        0
        ('ForkTree
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 0 [Int]) 'EmptyTree)
              (Node 20 Char)
              'EmptyTree)
           (Node 30 [Char])
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 50 Bool) 'EmptyTree)
              (Node 60 Int)
              ('ForkTree
                 'EmptyTree
                 (Node 70 [Bool])
                 ('ForkTree 'EmptyTree (Node 75 Char) 'EmptyTree)))))
forall (x :: Nat) (t :: Tree).
Deletable x t =>
Proxy x -> AVL t -> AVL (Delete x t)
deleteAVL (Proxy 0
forall {k} (t :: k). Proxy t
Proxy :: Proxy 0) AVL
  ('ForkTree
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 0 [Int]) 'EmptyTree)
        (Node 20 Char)
        'EmptyTree)
     (Node 30 [Char])
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 50 Bool) 'EmptyTree)
        (Node 60 Int)
        ('ForkTree
           'EmptyTree
           (Node 70 [Bool])
           ('ForkTree 'EmptyTree (Node 75 Char) 'EmptyTree))))
avlt8

avlt16 :: AVL
  (Delete
     70
     ('ForkTree
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 [Int]) 'EmptyTree)
           (Node 20 Char)
           'EmptyTree)
        (Node 30 [Char])
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 50 Bool) 'EmptyTree)
           (Node 60 Int)
           ('ForkTree
              'EmptyTree
              (Node 70 [Bool])
              ('ForkTree 'EmptyTree (Node 75 Char) 'EmptyTree)))))
avlt16 = Proxy 70
-> AVL
     ('ForkTree
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 [Int]) 'EmptyTree)
           (Node 20 Char)
           'EmptyTree)
        (Node 30 [Char])
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 50 Bool) 'EmptyTree)
           (Node 60 Int)
           ('ForkTree
              'EmptyTree
              (Node 70 [Bool])
              ('ForkTree 'EmptyTree (Node 75 Char) 'EmptyTree))))
-> AVL
     (Delete
        70
        ('ForkTree
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 0 [Int]) 'EmptyTree)
              (Node 20 Char)
              'EmptyTree)
           (Node 30 [Char])
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 50 Bool) 'EmptyTree)
              (Node 60 Int)
              ('ForkTree
                 'EmptyTree
                 (Node 70 [Bool])
                 ('ForkTree 'EmptyTree (Node 75 Char) 'EmptyTree)))))
forall (x :: Nat) (t :: Tree).
Deletable x t =>
Proxy x -> AVL t -> AVL (Delete x t)
deleteAVL (Proxy 70
forall {k} (t :: k). Proxy t
Proxy :: Proxy 70) AVL
  ('ForkTree
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 0 [Int]) 'EmptyTree)
        (Node 20 Char)
        'EmptyTree)
     (Node 30 [Char])
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 50 Bool) 'EmptyTree)
        (Node 60 Int)
        ('ForkTree
           'EmptyTree
           (Node 70 [Bool])
           ('ForkTree 'EmptyTree (Node 75 Char) 'EmptyTree))))
avlt8

avlt17 :: AVL
  (Delete
     70
     ('ForkTree
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 [Int]) 'EmptyTree)
           (Node 20 Char)
           'EmptyTree)
        (Node 30 [Char])
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 50 Bool) 'EmptyTree)
           (Node 60 Int)
           ('ForkTree
              'EmptyTree
              (Node 70 [Bool])
              ('ForkTree 'EmptyTree (Node 75 Char) 'EmptyTree)))))
avlt17 = Proxy 70
-> AVL
     ('ForkTree
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 [Int]) 'EmptyTree)
           (Node 20 Char)
           'EmptyTree)
        (Node 30 [Char])
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 50 Bool) 'EmptyTree)
           (Node 60 Int)
           ('ForkTree
              'EmptyTree
              (Node 70 [Bool])
              ('ForkTree 'EmptyTree (Node 75 Char) 'EmptyTree))))
-> AVL
     (Delete
        70
        ('ForkTree
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 0 [Int]) 'EmptyTree)
              (Node 20 Char)
              'EmptyTree)
           (Node 30 [Char])
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 50 Bool) 'EmptyTree)
              (Node 60 Int)
              ('ForkTree
                 'EmptyTree
                 (Node 70 [Bool])
                 ('ForkTree 'EmptyTree (Node 75 Char) 'EmptyTree)))))
forall (x :: Nat) (t :: Tree).
Deletable x t =>
Proxy x -> AVL t -> AVL (Delete x t)
deleteAVL (Proxy 70
forall {k} (t :: k). Proxy t
Proxy :: Proxy 70) AVL
  ('ForkTree
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 0 [Int]) 'EmptyTree)
        (Node 20 Char)
        'EmptyTree)
     (Node 30 [Char])
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 50 Bool) 'EmptyTree)
        (Node 60 Int)
        ('ForkTree
           'EmptyTree
           (Node 70 [Bool])
           ('ForkTree 'EmptyTree (Node 75 Char) 'EmptyTree))))
avlt8

avlt18 :: AVL
  (Delete
     75
     ('ForkTree
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 [Int]) 'EmptyTree)
           (Node 20 Char)
           'EmptyTree)
        (Node 30 [Char])
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 50 Bool) 'EmptyTree)
           (Node 60 Int)
           ('ForkTree
              'EmptyTree
              (Node 70 [Bool])
              ('ForkTree 'EmptyTree (Node 75 Char) 'EmptyTree)))))
avlt18 = Proxy 75
-> AVL
     ('ForkTree
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 [Int]) 'EmptyTree)
           (Node 20 Char)
           'EmptyTree)
        (Node 30 [Char])
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 50 Bool) 'EmptyTree)
           (Node 60 Int)
           ('ForkTree
              'EmptyTree
              (Node 70 [Bool])
              ('ForkTree 'EmptyTree (Node 75 Char) 'EmptyTree))))
-> AVL
     (Delete
        75
        ('ForkTree
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 0 [Int]) 'EmptyTree)
              (Node 20 Char)
              'EmptyTree)
           (Node 30 [Char])
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 50 Bool) 'EmptyTree)
              (Node 60 Int)
              ('ForkTree
                 'EmptyTree
                 (Node 70 [Bool])
                 ('ForkTree 'EmptyTree (Node 75 Char) 'EmptyTree)))))
forall (x :: Nat) (t :: Tree).
Deletable x t =>
Proxy x -> AVL t -> AVL (Delete x t)
deleteAVL (Proxy 75
forall {k} (t :: k). Proxy t
Proxy :: Proxy 75) AVL
  ('ForkTree
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 0 [Int]) 'EmptyTree)
        (Node 20 Char)
        'EmptyTree)
     (Node 30 [Char])
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 50 Bool) 'EmptyTree)
        (Node 60 Int)
        ('ForkTree
           'EmptyTree
           (Node 70 [Bool])
           ('ForkTree 'EmptyTree (Node 75 Char) 'EmptyTree))))
avlt8

avlt19 :: AVL
  (Delete
     21
     ('ForkTree
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 [Int]) 'EmptyTree)
           (Node 20 Char)
           'EmptyTree)
        (Node 30 [Char])
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 50 Bool) 'EmptyTree)
           (Node 60 Int)
           ('ForkTree
              'EmptyTree
              (Node 70 [Bool])
              ('ForkTree 'EmptyTree (Node 75 Char) 'EmptyTree)))))
avlt19 = Proxy 21
-> AVL
     ('ForkTree
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 0 [Int]) 'EmptyTree)
           (Node 20 Char)
           'EmptyTree)
        (Node 30 [Char])
        ('ForkTree
           ('ForkTree 'EmptyTree (Node 50 Bool) 'EmptyTree)
           (Node 60 Int)
           ('ForkTree
              'EmptyTree
              (Node 70 [Bool])
              ('ForkTree 'EmptyTree (Node 75 Char) 'EmptyTree))))
-> AVL
     (Delete
        21
        ('ForkTree
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 0 [Int]) 'EmptyTree)
              (Node 20 Char)
              'EmptyTree)
           (Node 30 [Char])
           ('ForkTree
              ('ForkTree 'EmptyTree (Node 50 Bool) 'EmptyTree)
              (Node 60 Int)
              ('ForkTree
                 'EmptyTree
                 (Node 70 [Bool])
                 ('ForkTree 'EmptyTree (Node 75 Char) 'EmptyTree)))))
forall (x :: Nat) (t :: Tree).
Deletable x t =>
Proxy x -> AVL t -> AVL (Delete x t)
deleteAVL (Proxy 21
forall {k} (t :: k). Proxy t
Proxy :: Proxy 21) AVL
  ('ForkTree
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 0 [Int]) 'EmptyTree)
        (Node 20 Char)
        'EmptyTree)
     (Node 30 [Char])
     ('ForkTree
        ('ForkTree 'EmptyTree (Node 50 Bool) 'EmptyTree)
        (Node 60 Int)
        ('ForkTree
           'EmptyTree
           (Node 70 [Bool])
           ('ForkTree 'EmptyTree (Node 75 Char) 'EmptyTree))))
avlt8

avlt20 :: AVL (Delete 21 'EmptyTree)
avlt20 = Proxy 21 -> AVL 'EmptyTree -> AVL (Delete 21 'EmptyTree)
forall (x :: Nat) (t :: Tree).
Deletable x t =>
Proxy x -> AVL t -> AVL (Delete x t)
deleteAVL (Proxy 21
forall {k} (t :: k). Proxy t
Proxy :: Proxy 21) AVL 'EmptyTree
avle