proposition: Theorem MMA2_ndMM2_equiv a b : (1,P) //ₐ (1,a##b##ø) ~~> (0,0##0##ø) <-> ΣP //ₙ a ⊕ b ⊦ 1.
proof: Proof. split. + intros []; apply mma2_prog_enc_sound; auto. + split. * now apply mma2_prog_enc_complete. * simpl; lia. Qed.
imports: List Arith Lia Relations Undecidability.MinskyMachines(MMA mma_defs ndMM2) Undecidability.Shared.Libs.DLW(utils Vec.pos Vec.vec Code.subcode Code.sss) Undecidability.Synthetic(Definitions ReducibilityFacts)