| 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)
|
| tm_config |
Def Config(M) ==  (M) (   G(M))
Thm* M:PM{i}. Config(M) Type
|
| nat |
Def == {i:| 0 i}
Thm* Type
|
| proto_machine |
Def PM{i}
== q:Type
proto_sigma:Type
proto_pi:Type(Void+proto_pi)(q(proto_sigma+proto_pi)q(proto_sigma+proto_pi) )qqq
Thm* PM{i} Type{i'}
|
| 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
|
| tm_gamma |
Def G(p) == P (p)+P (p)
Thm* M:PM{i}. G(M) Type
|
| tm_q |
Def (p) == 1of(p)
Thm* p:PM{i}. (p) Type
|
| le |
Def AB ==  B < A
Thm* i,j:. ij Prop
|
| 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)
|
| tm_proto_pi |
Def P(p) == 1of(2of(2of(p)))
Thm* p:PM{i}. P(p) Type
|
| tm_proto_sigma |
Def P(p) == 1of(2of(p))
Thm* p:PM{i}. P(p) Type
|
| 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
|
| not |
Def A == A   False
Thm* (A) Prop
|