Selected Objects

def	finite	Finite(T) == n:. n ~ T
COM	turing_1_contents	Definition of Turing Machine
COM	proto_machine_def	=========================================
def	proto_machine	PM{i} == q:Type proto_sigma:Type proto_pi:Type(Void+proto_pi)(q(proto_sigma+proto_pi)q(proto_sigma+proto_pi))qqq
def	tm_q	(p) == 1of(p)
THM	tm_q_wf	p:PM{i}. (p) Type
def	tm_proto_sigma	P(p) == 1of(2of(p))
THM	tm_proto_sigma_wf	p:PM{i}. P(p) Type
def	tm_sigma	(tm) == P(tm)+Void
def	tm_proto_pi	P(p) == 1of(2of(2of(p)))
THM	tm_proto_pi_wf	p:PM{i}. P(p) Type
def	tm_pi	(p) == Void+P(p)
def	tm_gamma	G(p) == P(p)+P(p)
def	tm_blank	_(p) == 1of(2of(2of(2of(p))))
THM	blank_proto_pi	p:PM{i}. _(p) Void+P(p)
THM	blank_pi	p:PM{i}. _(p) (p)
THM	tm_blank_wf	p:PM{i}. _(p) G(p)
def	tm_delta	(p) == 1of(2of(2of(2of(2of(p)))))
THM	tm_delta_proto	p:PM{i}. (p) (p)(P(p)+P(p))(p)(P(p)+P(p))
THM	tm_delta_wf	p:PM{i}. (p) (p)G(p)(p)G(p)
def	tm_s	p.s == 1of(2of(2of(2of(2of(2of(p))))))
THM	tm_s_wf	p:PM{i}. p.s (p)
def	tm_t	p.t == 1of(2of(2of(2of(2of(2of(2of(p)))))))
THM	tm_t_wf	p:PM{i}. p.t (p)
def	tm_r	p.r == 2of(2of(2of(2of(2of(2of(2of(p)))))))
THM	tm_r_wf	p:PM{i}. p.r (p)
COM	tm_config_def	===========================================
def	tm_config	Config(M) == (M)(G(M))
def	conf_st	t.st == 1of(t)
THM	conf_st_wf	M:PM{i}, t:Config(M). t.st (M)
def	conf_tape	t.tape == 1of(2of(t))
THM	conf_tape_wf	M:PM{i}, t:Config(M). t.tape G(M)
def	conf_hd	t.hd == 2of(2of(t))
THM	conf_hd_wf	M:PM{i}, t:Config(M). t.hd
def	next_config	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	next_config_wf	M:PM{i}, C:Config(M). M(C) Config(M)
def	nth_config	(rec) M(C)[n] == if n=0 C else M(M(C)[n-1]) fi
THM	nth_config_wf	M:PM{i}, C:Config(M), n:. M(C)[n] Config(M)
def	accept_config	M(C) == n:. M(C)[n].st = M.t & (k:n. M(C)[n].st = M.r)
def	turing_machine	TM(M) == Finite((M)) & Finite((M)) & Finite((M)) & M.t = M.r