Fixed bug in Mona_syntax.nnf in <=> case; Simplified Myconstruction, and the counterexample handling; Fixed bug in Nfa_from_dot initial state assignment; Added .tex files of algorithms' pseudocode.