Thm* M:PM{i}, C:Config(M), n:. M(C)[n] Config(M) nth_config_wf

Thm* M:PM{i}, C:Config(M). M(C) Config(M) next_config_wf

Thm* M:PM{i}, t:Config(M). t.hd conf_hd_wf

Thm* M:PM{i}, t:Config(M). t.tape G(M) conf_tape_wf

Thm* M:PM{i}, t:Config(M). t.st (M) conf_st_wf

Thm* p:PM{i}. p.r (p) tm_r_wf

Thm* p:PM{i}. p.t (p) tm_t_wf

Thm* p:PM{i}. p.s (p) tm_s_wf

Thm* p:PM{i}. (p) (p)G(p)(p)G(p) tm_delta_wf

Thm* p:PM{i}. (p) (p)(P(p)+P(p))(p)(P(p)+P(p)) tm_delta_proto

Thm* p:PM{i}. _(p) G(p) tm_blank_wf

Thm* p:PM{i}. _(p) (p) blank_pi

Thm* p:PM{i}. _(p) Void+P(p) blank_proto_pi

Thm* p:PM{i}. P(p) Type tm_proto_pi_wf

Thm* p:PM{i}. P(p) Type tm_proto_sigma_wf

Thm* p:PM{i}. (p) Type tm_q_wf