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