Syntax for expressions and equations

Equations should be entered like this:
<expr1> <cmp> <expr2>
.
An expression can use strings as variables/letters, and the
operations:

0
: the empty set;

1
: the empty process;

<expr1> + <expr2>
: the set
union;

<expr1>  <expr2>
: the parallel
product;

<expr1> . <expr2>
: the sequential
product;

<expr1>^+
: the transitive closure;

<expr1>^*
: the reflexive transitive
closure;

<expr1>{int}
: the iteration. For
instance, (a.b){3}
is a shorthand
for (a.b).(a.b).(a.b)
.
You can also use brackets (...)
. The valid
comparaisons <cmp>
are:

<=
: loose inclusion

>=
: converse of the loose inclusion

<
: strict inclusion

>
: converse of the strict inclusion

=
: equality

=/=
: negation of the equality

<>
: means that the two expressions are
incomparable,
i.e. neither one of them is included in the
other.
For instance,
(ab)^+.C + d < d + a.b.C + (da)
is an acceptable equation.