C  
check [Symkat] 
utility for verifications: check two expressions for equivalence
(
`E ), difference (`D ), lefttoright inclusion (`L ), or
righttoleft inclusion (`G ).

compare [Symkat] 
full comparison:
compare ~hyps x y returns `E if x and y are equivalent,, `L w if x is strictly contained in y (then w is a witness for strictness),, `G w if y is strictly contained in x (then w is a witness for strictness),, `D(w1,w2) if x and y are incomparable (then w1 is a witness against x<=y , and w2 is a witness against y<=x ).
Also return the actually compared terms, in symbolic form.
Exploit hypotheses if asked to.

congruence [Symkat] 
do we use upto congruence

construction [Symkat] 
which construction do we use

D  
deriv [Brzozowski] 
derivatives

deriv [Antimirov] 
partial derivatives

dfa [Brzozowski] 
corresponding symbolic DFA

dot [Kat]  
E  
enfa [IlieYu] 
corresponding automaton

epsilon [Kat] 
output of a symbolic expression

equiv [Symkat] 
equivalence check, using the above parameters; returns a
counterexample if any.

expr [Parse] 
parsing a string into a KAT expression

expr' [Kat] 
from explicit expressions to (normalised) symbolic ones

H  
hash [Kat] 
hash of an expression

head [Kat] 
top constructor of a symbolic KAT expression

hk [Symkat] 
do we use Hopcroft and Karp's version?

hyps [Parse] 
parsing a finite set of KAT equations (for hypothesis elimination)

N  
nfa [Antimirov] 
corresponding symbolic NFA

O  
one [Kat]  
P  
pls [Kat] 
smart constructors for symbolic KAT expressions: sums are sorted and associated to the left, consecutive tests are merged,
duplicates and
0 are removed , products are associated to the left are simplified w.r.t. constants 0 and 1 ,
and consecutive tests (on the left) are merged

print_expr [Kat]  
print_expr' [Kat]  
print_gstring [Kat]  
print_test [Kat] 
prettyprinting for tests and expressions

R  
random_expr [Kat]  random_expr as ps n returns a random expression
constructed from atomic tests in as and atomic Kleene elements in ps , with n connectives , with all negations at the leaves, without 0

random_full_expr [Kat]  random_full_expr as ps n returns a saturated random expression:
a random expression as explained above, summed with the universal
expression (\sum ps)*

S  
split [Antimirov] 
split a sum into a set of expressions

ssf [Symkat] 
do we put expressions in strict star form first?

ssf [Kat] 
putting an expression in strict star form: forall subexpression
of the shape
e* , it is guaranted that e does not contain 1
(i.e., epsilon e!=top )

str [Kat]  
subst [Kat] 
term substitution

T  
test_to_formula [Kat] 
Conversion to Boolean BDD

tod [Kat]  
trace [Symkat] 
do we trace unifications in
Format.str_formatter

tst [Kat]  
V  
var [Kat]  
vars [Kat] 
set of variables appearing in an expression

Z  
zer [Kat] 