Formal description of TL combinators