Диссертация (1150902), страница 20

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 20)

20.↑0 @1↑(App−T ree)−→↑0 @1 @2↑0 @1 @2 λs1 1 @7↑(App−T ree)(App−T ree)−→↑↑−→↑0 @1 @2 λs1↑(Lam−Elim−App−T ree)−→↑0 @1 @2 λs1 1 @7 λs2cleanup(Lam−Elim−App−T ree)↑↑−→↑↓0 @1 @2 λs1 1 @7 λs2 2 S −→ 0 @1 @2 λs1 1 @7 λs2 2 S 2(F REE−I)−→↑↑↑↓0 @1 @2 λs1 1 @7 λs2 2 S 2 λz2(Lam−N on−Elim−T ree)−→121↑↑↑↓0 @1 @2 λs1 1 @7 λs2 2 S 2 λz2 @5↑↑↑↓↑↑↑↓(App−T ree)−→(BV ar)0 @1 @2 λs1 1 @7 λs2 2 S 2 λz2 @5 s2 −→0 @1 @2 λs1 1 @7 λs2 2 S 2 λz2 @5 s2 S↑↑↑(F REE−II)−→↓0 @1 @2 λs1 1 @7 λs2 2 S 2 λz2 @5 s2 S @6↑↑↑↓↑↑↑↓(App−T ree)−→(BV ar)0 @1 @2 λs1 1 @7 λs2 2 S 2 λz2 @5 s2 S @6 s2 −→0 @1 @2 λs1 1 @7 λs2 2 S 2 λz2 @5 s2 S @6 s2 S↑↑↑↓(F REE−II)−→cleanup0 @1 @2 λs1 1 @7 λs2 2 S 2 λz2 @5 s2 S @6 s2 S z2 −→122↑↑↓0 @1 @2 λs1 1 λz2 @5 S @6 S z2 1↑↑(F REE−I)−→↓0 @1 @2 λs1 1 λz2 @5 S @6 S z2 1 λz1(Lam−Elim−App−T ree)−→↑↑↓↑↑↑↓↑cleanup0 @1 @2 λs1 1 λz2 @5 S @6 S z2 1 λz1 1 Z −→↓0 @1 @2 λs1 1 λz2 @5 S @6 S z2 1 λz1 1 Z 1↑↑↓↑(F REE−I)−→↓0 @1 @2 λs1 1 λz2 @5 S @6 S z2 1 λz1 1 Z 1 @3↑↑↓↑↓↑↑↓↑↓(App−T ree)−→(BV ar)0 @1 @2 λs1 1 λz2 @5 S @6 S z2 1 λz1 1 Z 1 @3 s1 −→0 @1 @2 λs1 1 λz2 @5 S @6 S z2 1 λz1 1 Z 1 @3 s1 λz2(Lam−Elim−App−T ree)−→↑↓↑↓↑↑↑↓↑↓↑↑↓↑↑↓↑↓↑−→↑(BV ar)0 @1 @2 λs1 1 λz2 @5 S @6 S z2 1 λz1 1 Z 1 @3 s1 λz2 1 @4 s1 λz2 2 z1 −→↑0 @1 @2 λs1 1 λz2 @5 S @6 S z2 1 λz1 1 Z 1 @3 s1 λz2 1 @4 s1 λz2↓(Lam−Elim−App−T ree)(BV ar)−→(App−T ree)0 @1 @2 λs1 1 λz2 @5 S @6 S z2 1 λz1 1 Z 1 @3 s1 λz2 1 @4 s1 −→↑↑0 @1 @2 λs1 1 λz2 @5 S @6 S z2 1 λz1 1 Z 1 @3 s1 λz2 1 @4↑123↑↓↑↓↑↑↑↓↑↓↑↑↓↑↓↑↓↑↑↓0 @1 @2 λs1 1 λz2 @5 S @6 S z2 1 λz1 1 Z 1 @3 s1 λz2 1 @4 s1 λz2 2 Z 2 @5 S↑−→(F REE−V )−→(App−Argument)−→(F REE−IV )0 @1 @2 λs1 1 λz2 @5 S @6 S z2 1 λz1 1 Z 1 @3 s1 λz2 1 @4 s1 λz2 2 Z 2 @5↑0 @1 @2 λs1 1 λz2 @5 S @6 S z2 1 λz1 1 Z 1 @3 s1 λz2 1 @4 s1 λz2 2 z1 Z↑124↑↓↑↓↑↑↓↑↓↑↓↑↑↓↑↓↑↓↑↑↓(BV ar)0 @1 @2 λs1 1 λz2 @5 S @6 S z2 1 λz1 1 Z 1 @3 s1 λz2 1 @4 s1 λz2 2 Z 2 @5 S @6 S z2 −→↑−→(F REE−V )−→(App−Argument)0 @1 @2 λs1 1 λz2 @5 S @6 S z2 1 λz1 1 Z 1 @3 s1 λz2 1 @4 s1 λz2 2 Z 2 @5 S @6 S↑0 @1 @2 λs1 1 λz2 @5 S @6 S z2 1 λz1 1 Z 1 @3 s1 λz2 1 @4 s1 λz2 2 Z 2 @5 S @6↑125↑↓↑↓↑↑↓↑↓↑↓↑↓↑↓↑↓↑↓−→(F REE−V )−→(App−Argument)0 @1 @2 λs1 1 λz2 @5 S @6 S z2 1 λz1 1 Z 1 @3 s1 λz2 1 @5 S @6 S Z 1 @5 S↑0 @1 @2 λs1 1 λz2 @5 S @6 S z2 1 λz1 1 Z 1 @3 s1 λz2 1 @5 S @6 S Z 1 @5↑−→(F REE−IV );cleanup0 @1 @2 λs1 1 λz2 @5 S @6 S z2 1 λz1 1 Z 1 @3 s1 λz2 1 @4 s1 λz2 2 Z 2 @5 S @6 S z2 Z↑126↑↓↑↓↑↓↑↓↑↓↑↓↑↓↑↓↑↓(BV ar)0 @1 @2 λs1 1 λz2 @5 S @6 S z2 1 λz1 1 Z 1 @3 s1 λz2 1 @5 S @6 S Z 1 @5 S @6 S z2 −→↑−→(F REE−V )−→(App−Argument)0 @1 @2 λs1 1 λz2 @5 S @6 S z2 1 λz1 1 Z 1 @3 s1 λz2 1 @5 S @6 S Z 1 @5 S @6 S↑0 @1 @2 λs1 1 λz2 @5 S @6 S z2 1 λz1 1 Z 1 @3 s1 λz2 1 @5 S @6 S Z 1 @5 S @6↑127↑↓↑↓↑↓↑↓↑↓↑↓↑↓↑↓↑↓−→(App−Argument)0 @1 @2 λs1 1 λz2 @5 S @6 S z2 1 λz1 1 Z 1 @3 s1 λz2 1 @5 S @6 S Z 1 @5 S @6 S z2 @5 S @6↑−→(F REE−V )0 @1 @2 λs1 1 λz2 @5 S @6 S z2 1 λz1 1 Z 1 @3 s1 λz2 1 @5 S @6 S Z 1 @5 S @6 S z2 @5 S↑−→(App−Argument)0 @1 @2 λs1 1 λz2 @5 S @6 S z2 1 λz1 1 Z 1 @3 s1 λz2 1 @5 S @6 S Z 1 @5 S @6 S z2 @5↑128↑↓↑↓↑↓↑↓↑↓↑↓0 @1 @2 λs1 1 λz2 @5 S @6 S z2 1 λz1 1 Z 1 @3 s1 λz2 1 @5 S @6 S Z 1 @5 S @6 S z2 @5 S @6 S Z↑−→(F REE−V )0 @1 @2 λs1 1 λz2 @5 S @6 S z2 1 λz1 1 Z 1 @3 s1 λz2 1 @5 S @6 S Z 1 @5 S @6 S z2 @5 S @6 S↑129130конец; окончательный вызов cleanup−→↓↑0 @5 S @6 S @5 S @6 S Z 0Результат восстановления нормальной формы терма из итогового обхода приведён на рисунке Б.1.@5@6S@5S@6SSZРисунок Б.1.

Результат восстановления нормальной формы терма из итоговогообхода.

Характеристики

Список файлов диссертации