Invariante de Representación

⟨⟩ -- Árbol vacío�⟨l, e, r⟩ -- Árbol con al menos un elemento

check_greater :: T -> ⟨T⟩ -> Bool�check_greater e' ⟨⟩ = True�check_greater e' ⟨l, e, r⟩ = e' > e ∧ check_greater e' l

∧ check_greater e' r

check_smaller :: T -> ⟨T⟩ -> Bool�check_smaller e' ⟨⟩ = True

check_smaller e' ⟨l, e, r⟩ = e' < e ∧

check_smaller e' l ∧� check_smaller e' r

​

is_abb :: ⟨T⟩ -> Bool�is_abb ⟨⟩ = True�is_abb ⟨l, e, r⟩ = check_greater e l ∧ � check_smaller e r ∧� is_abb(l) ∧� is_abb(r)

Operaciones de ABBs - exists

exists :: T -> ⟨T⟩ -> Bool�exists e' ⟨⟩ = False�exists e' ⟨l, e, r⟩ | (e'== e) = True� | (e' > e) = exists e' r� | (e' < e) = exists e' l

​

-- Sin usar definición por casos

exists' :: T -> ⟨T⟩ -> Bool

exists' e' ⟨⟩ = False�exists' e' ⟨l, e, r⟩ = (e'== e) ∨ � ((e' > e) ∧ exists' e' r) ∨

((e' < e) ∧ exists' e' l)

Operaciones de ABBs - add

add :: ⟨T⟩ -> T -> ⟨T⟩�add ⟨⟩ eₙ = ⟨⟨⟩, eₙ, ⟨⟩⟩�add ⟨l, e, r⟩ eₙ | eₙ == e = ⟨l, e, r⟩

| eₙ < e = ⟨add l eₙ, e, r⟩

| eₙ > e = ⟨l, e,add r eₙ⟩

​

​

​

Operaciones de ABBs - remove

max_e :: ⟨T⟩ -> T�max_e ⟨l, e, ⟨⟩⟩ = e�max_e ⟨l, e, r⟩ = max_e r�

del_max :: ⟨T⟩ -> ⟨T⟩�del_max ⟨l, e, ⟨⟩⟩ = l�del_max ⟨l, e, r⟩ = ⟨l, e, del_max r⟩

​

del :: ⟨T⟩ -> T -> ⟨T⟩�del ⟨⟩ eₓ = ⟨⟩�del ⟨l, e, r⟩ eₓ | eₓ < e = ⟨del l eₓ,e, r⟩

| e < eₓ = ⟨l, e, del r eₓ⟩

| e == eₓ | is_empty l = r

| otherwise = ⟨del_max l ,max_e l, r⟩