| nth_config |
Def (rec) M(C)[n] == if n= 0 C else M(M(C)[n-1]) fi
Thm*  M:PM{i}, C:Config(M), n: . M(C)[n]  Config(M)
|
| next_config |
Def M(Conf)
== let delta =  (M)( < Conf.st,Conf.tape(Conf.hd) > ) in
< 1of(delta)
,( z.if z=Conf.hd 1of(2of(delta)) else Conf.tape(z) fi)
,if 2of(2of(delta)) Conf.hd+1 else Conf.hd-1 fi >
Thm* M:PM{i}, C:Config(M). M(C) Config(M)
|
| eq_int |
Def i=j == if i=jtrue; false fi
Thm* i,j: . i=j 
|
| conf_hd |
Def t.hd == 2of(2of(t))
Thm* M:PM{i}, t:Config(M). t.hd
|
| conf_tape |
Def t.tape == 1of(2of(t))
Thm* M:PM{i}, t:Config(M). t.tape   G(M)
|
| tm_delta |
Def (p) == 1of(2of(2of(2of(2of(p)))))
Thm* p:PM{i}. (p)  (p) G(p)(p)G(p)
|
| pi2 |
Def 2of(t) == t.2
Thm* B:(AType), p:a:AB(a). 2of(p) B(1of(p))
|
| conf_st |
Def t.st == 1of(t)
Thm* M:PM{i}, t:Config(M). t.st (M)
|
| pi1 |
Def 1of(t) == t.1
Thm* B:(AType), p:a:AB(a). 1of(p) A
|
| let |
Def let x = a in b(x) == (x.b(x))(a)
Thm* a:A, b:(AB). let x = a in b(x) B
|