Rewrite and Introduce New Notations (for vertical and horizontal composition) in Natrans.v