module rbt_varif where

open import Level renaming ( suc to succ ; zero to Zero )
open import Relation.Binary
open import Data.Nat hiding (_!$\leq$!_  ; _!$\leq$!?_)
open import Data.List hiding ([_])
open import Data.Product
open import Data.Nat.Properties as NP



mutual
  data  right-List : Set where
    [] : right-List
    [_] : !$\mathbb{N}$! !$\rightarrow$! right-List
    _!$\text{::}$!>_Cond_ : (x : !$\mathbb{N}$!) !$\rightarrow$! (xs : right-List ) !$\rightarrow$! (p : x Data.Nat.> top-r xs) !$\rightarrow$! right-List

  top-r : right-List !$\rightarrow$! !$\mathbb{N}$!
  top-r [] = {!!}
  top-r [ x ] = x
  top-r (x !$\text{::}$!> l Cond x!$\text{1}$!) = x

  insert-r : !$\mathbb{N}$! !$\rightarrow$! right-List !$\rightarrow$! right-List
  insert-r x [] = {!!}
  insert-r x [ y ] with <-cmp x y
  ... | tri< a !$\neg$!b !$\neg$!c = [ y ]
  ... | tri≈ !$\neg$!a b !$\neg$!c = [ y ]
  ... | tri> !$\neg$!a !$\neg$!b c = x !$\text{::}$!>  [ y ] Cond c
  insert-r x (y !$\text{::}$!> ys Cond p) with <-cmp x y
  ... | tri< a !$\neg$!b !$\neg$!c = (y !$\text{::}$!> ys Cond p)
  ... | tri≈ !$\neg$!a b !$\neg$!c = (y !$\text{::}$!> ys Cond p)
  ... | tri> !$\neg$!a !$\neg$!b c = x !$\text{::}$!> (y !$\text{::}$!> ys Cond p) Cond c

  data  left-List : Set where
    [] : left-List
    [_] : !$\mathbb{N}$! -> left-List
    _<!$\text{::}$!_Cond_ : (x : !$\mathbb{N}$!) -> (xs : left-List ) -> (p : x Data.Nat.< top-l xs) -> left-List

  top-l : left-List !$\rightarrow$! !$\mathbb{N}$!
  top-l [] = {!!}
  top-l [ x ] = x
  top-l (x <!$\text{::}$! l Cond x!$\text{1}$!) = x

  insert-l : !$\mathbb{N}$! -> left-List -> left-List
  insert-l x [] = [ x ]
  insert-l x l@([ y ]) with <-cmp x y
  ... | tri< a !$\neg$!b !$\neg$!c = x <!$\text{::}$! l Cond a
  ... | tri≈ !$\neg$!a b !$\neg$!c = l
  ... | tri> !$\neg$!a !$\neg$!b c = l
  insert-l x l@(y <!$\text{::}$! ys Cond p) with <-cmp x y
  ... | tri< a !$\neg$!b !$\neg$!c = x <!$\text{::}$! l Cond a
  ... | tri≈ !$\neg$!a b !$\neg$!c = l

  ... | tri> !$\neg$!a !$\neg$!b c = l