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

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

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