/*

specification of lower bound lists

*/

use(to).
use(lists).

% projections

element(lb(E1,E2))=E1.
l_bound(lb(E1,E2))=E2.


% remove

remove(E,nil)=nil.
remove(E1,cons(L,lb(E1,E2)))=L.
remove(E1,cons(L,lb(E2,E3)))=cons(remove(E1,L),lb(E2,E3)),E1=E2.

% adjust

adjust(E,nil)=nil.
E3<E1 ->
 adjust(E1,cons(L,lb(E2,E3)))=cons(lb(E2,E1),adjust(E1,L)).
E1=<E3 ->
 adjust(E1,cons(L,lb(E2,E3)))=cons(L,lb(E2,E3)).


/*

lower_bound function is the functin that returns the lower bound of the element E.
If there are more elements E, lower_bound function returns the value of the first element

*/

lower_bound(E1,nil)=undef.
lower_bound(E1,cons(L,lb(E1,E2)))=E2.
lower_bound(E1,cons(L,lb(E2,E3)))=lower_bound(E1,L),E1=E2.

precedence([adjust,remove,lower_bound,element,l_bound,lb,prefix,cons,nil,inf,undef,=<,<]).