Lean: арифметика Арбитра и детерминизм шага

Агата Сомова · старший инспектор

В машинном зале ты доказал судье, что у Арбитра на каждом шаге одна дорога. Судья поверил тебе, Вельский нет. Хорошо, пусть не верит нам обоим. Перепиши десять правил Арбитра для механического прокурора, слово в слово, и докажи ему то же самое. Тогда этот довод закрыт не до следующего заседания, а навсегда.

В уроке 40 ты доказывал детерминизм одного шага: если $t⟶t^{\prime }$ и $t⟶t^{\prime \prime }$, то $t^{\prime }=t^{\prime \prime }$. Три случая разобрал, остальные остались «аналогично», а случаи E-PredSucc против E-Pred ты, может быть, разбирал в упражнении со звёздочками.

Сегодня это доказательство проверит машина. Для этого сначала нужно рассказать ей, что такое терм, значение и шаг. Окажется, что ты почти всё это уже писал: правила с чертой из блока «Протокол» переводятся в Lean один в один.