Выдержка из книги
Чень Ч.N.
Математическая логика и автоматическое доказательство теорем
Мы проверим теперь, удовлетворяет ли этот граф всем условиям из определения программы. Заметим, что есть один стартовый узел и один стоп-узел, и любой узел находится на некотором пути от S к Я. Каждому ребру поставлены в соответствие некоторая формула и некоторое присваивание. Наконец, имеется ровно одно ребро, а именно а, выходящее из S; для всевозможных значений 1 ( х2, yt и у2 формула И всегда истинна. Что касается узла 1, то имеется два ребра, а именно b и с, выходящие из этого узла.