proposition: Lemma fractran_mma_complete x : (1,fractran_mma) //ₐ (1,x##0##ø) ↓ -> Q /F/ x ↓.
proof: Proof. Proof using HQ. intros ((j,w) & (k & H2) & H3); simpl fst in H3. revert x H2; induction on k as IHu with measure k; intros x H2. destruct (fractran_step_dec Q x) as [ (y & Hy) | H4 ]. 2: { exists x; split; auto; exists 0; simpl; auto. } generalize Hy; intros H4. apply mma_fractran_step_success_progress with (1 := HQ) (j := 1) (i := 1) in H4; auto. fold fractran_mma in H4. destruct subcode_sss_progress_inv with (4 := H4) (5 := H2) as (r & H5 & H6); auto. 1: apply mma_sss_fun. apply IHu in H6; auto; rew vec. destruct H6 as (z & (u & Hk) & Hz2). exists z; split; auto; exists (S u), y; split; 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)