| accept_config |
Def M(C) ==  n: . M(C)[n].st = M.t & ( k:n.  M(C)[n].st = M.r)
Thm* M:PM{i}, C:Config(M). M(C)  Prop
|
| tm_r |
Def p.r == 2of(2of(2of(2of(2of(2of(2of(p)))))))
Thm* p:PM{i}. p.r  (p)
|
| 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)
|
| conf_st |
Def t.st == 1of(t)
Thm* M:PM{i}, t:Config(M). t.st (M)
|
| tm_q |
Def (p) == 1of(p)
Thm* p:PM{i}. (p) Type
|
| int_seg |
Def {i..j } == {k: | i  k < j}
Thm* m,n:. {m..n} Type
|
| nat |
Def == {i:| 0i}
Thm* Type
|
| lelt |
Def i j < k == ij & j < k
|
| le |
Def AB == B < A
Thm* i,j:. ij Prop
|
| not |
Def A == A   False
Thm* (A) Prop
|
| tm_t |
Def p.t == 1of(2of(2of(2of(2of(2of(2of(p)))))))
Thm* p:PM{i}. p.t (p)
|
| 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))
|
| eq_int |
Def i=j == if i=jtrue; false fi
Thm* i,j:. i=j
|
| 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
|