A complete axiomatisation for the inclusion of series-parallel partial orders

Series-parallel orders are defined as the least class of partial orders containing the one-element order and closed by ordinal sum and disjoint union. From this inductive definition, it is almost immediate that any series-parallel order may be represented by an algebraic expression, which is unique up to the associativity of ordinal sum and to the associativivity and commutativity of disjoint union. In this paper, we introduce a rewrite system acting on these algebraic expressions that axiomatises completely the sub-ordering relation for the class of series-parallel orders.