proposition: Fact ndmm2_accept_mono Σ Θ a b u : Σ ⊆ Θ -> Σ // a ⊕ b ⊦ u -> Θ // a ⊕ b ⊦ u.
proof: Proof. intros H. induction 1. + constructor; auto. + by constr 2 with H. + by constr 3 with H. + by constr 4 with H. + by constr 5 with H. + by constr 6 with H. + by constr 7 with H. Qed.
imports: List Undecidability.MinskyMachines(ndMM2)