Конечные пробеги по переходной системе

Question

Я хочу написать предикат, который бы утверждал, что переходная система не может иметь бесконечные прогоны из состояния s.Итак, рассмотрим переходную систему, заданную R, и вот определение, которое я придумал:

inductive finite_runs for R where         
"(∀ s'. R s s' ⟶ finite_runs R s') ⟹ finite_runs R s"

Это самый простой способ, которым я могу изложить этот факт в Изабель?В частности, я просмотрел Архив формальных доказательств (теории переписывания и маркировки переходов), но не нашел более простого решения.

Answer 1

В стандартной библиотеке Wellfounded.termip.Я думаю, что он должен делать именно то, что вы хотите.

Это в основном сокращение, использующее Wellfounded.accp, которое делает то же самое, но идет назад.

Answer 2

Если вы имеете в виду, что конечные прогоны означают отсутствие бесконечных прогонов, то вы можете использовать предикат включения сильной нормализации SN_on записи AFP-записи перезаписи.Однако ваше разрешение на определение также работает как

a -> a -> a -> ...

, что не разрешено SN_on.