[STATEMENT]
lemma NMPDA[rule_format]: "DenyAll \<in> set p \<longrightarrow> not_MT C  p"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. DenyAll \<in> set p \<longrightarrow> not_MT C p
[PROOF STEP]
by (induct p, simp_all add: DAnMT)