Isabelle Logic простой тест на естественный вычет

Question

http://pastebin.com/1ZEt9r32

Что не так с линией 30? Изабель говорит, что это "Не удалось завершить proof⌂: цель (2 подзадачи): 1. ¬ P ⟹ Q 2. Q ⟹ ¬ P"

Это теория естественного класса вычетов

Answer 1

порядок помещений находится в неправильном порядке. Если вы переупорядочиваете их следующим образом, то подтверждение принимается.

from pq and npq and qq show "Q" by (rule disjE) 

Вы можете проверить ожидаемый заказ

thm disjE 

Надеется, что это помогает, Рене