# Index of values

 C check [Symkat] utility for verifications: check two expressions for equivalence (E), difference (D), left-to-right inclusion (L), or right-to-left 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 up-to 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 counter-example 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] pretty-printing 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 sub-expression 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]