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