proposition: Lemma fractran_mma0_sound x y : fractran_compute Q x y -> fractran_stop Q y -> (1,FRAC_MMAₐ) //ₐ (1,x##0##ø) ->> (0,0##0##ø).
proof: Proof. Proof using HQ. intros H2 H3. unfold fractran_mma0. apply sss_compute_trans with (length P+1,y##0##ø). + apply subcode_sss_compute with (P := (1,P)); auto. apply fractran_mma_sound with (2 := H2); auto. + apply sss_progress_compute, fmma0_1; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils gcd pos vec subcode sss) Undecidability.MinskyMachines.MMA(mma_defs mma_utils) Undecidability.FRACTRAN(FRACTRAN fractran_utils)