Welcome to Abella 2.0.5-dev.
Abella < Specification "processes_terms".
Reading specification "processes_terms".

Abella < Define red_db_ker : pt -> pt -> pt -> prop,	
red_db : pt -> pt -> prop,	
red_ls_ker : pt -> (pt -> pt) -> (pt -> pt) -> prop,	
red_ls : pt -> pt -> prop by 
red_db_ker (abs U) V (subex U V);
red_db_ker (subex U V) W (subex U1 V) := nabla x, red_db_ker (U x) W (U1 x);
red_db (app U V) W := red_db_ker U V W;
red_ls_ker W x\x x\W;
red_ls_ker W (x\app (U1 x) (V x)) (x\app (U2 x) (V x)) := red_ls_ker W U1 U2;
red_ls_ker W (x\subex (U1 x) (V x)) (x\subex (U2 x) (V x)) := nabla y, red_ls_ker W (x\U1 x y) (x\U2 x y);
red_ls (subex U W) (subex V W) := red_ls_ker W U V.

Abella < Define evc_cl : (pt -> pt -> prop) -> pt -> pt -> prop by 
evc_cl R U V := R U V;
evc_cl R (app U W) (app V W) := evc_cl R U V;
evc_cl R (subex U W) (subex V W) := nabla x, evc_cl R (U x) (V x).

Abella <