* В определении <tex>TAUT</tex> стоит написать, что эта <tex>\phi</tex> — это булева формула, потому что навскидку это не понять.
* Косметическая правка: «тогда по лемме 1 <tex>TAUT</tex>…» единица с <tex>TAUT</tex> сливаются, попробуй написать «по лемме (1)…».
* Второй абзац после второго псевдокода: странная оценка, там (1) может быть неверно максимум 1 раз.
* Последний абзац написан неподробно.