proposition: Lemma fractran_mma_sound x y : fractran_compute Q x y -> Q /F/ y ⊁ * -> (1,fractran_mma) //ₐ (1,x##0##ø) ->> (length fractran_mma+1,y##0##ø).
proof: Proof. Proof using HQ. intros (u & H2) H3. revert x y H2 H3. induction u as [ | u IHu ]; simpl; intros x y H2 H3. + rewrite H2; apply mma_fractran_step_failure_compute; auto. + destruct H2 as (z & H2 & H4). apply mma_fractran_step_success_progress with (1 := HQ) (j := 1) (i := 1) in H2; auto. apply IHu with (x := z) in H3; auto; rew vec. apply sss_compute_trans with (2 := H3). apply sss_progress_compute; 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)