proposition: Fact mma_fractran_step_success_progress Q i x y : fractran_regular Q -> Q /F/ x ≻ y -> (i,mma_fractran_step Q i) //ₐ (i,x##0##ø) -+> (j,y##0##ø).
proof: Proof. unfold fractran_regular. intros H1 H2; revert H2 i H1. induction 1 as [ p q ll x y H1 | p q ll x y H1 H2 IH2 ]; intros i H3; rewrite Forall_cons_inv in H3; destruct H3 as (H3 & H4); simpl in H3, H4; unfold mma_fractran_step; fold mma_fractran_step. + apply subcode_sss_progress with (P := (i,mma_fractran_one p q j i)); auto. apply mma_fractran_one_ok_progress with (v := _##_##ø); auto. simpl; rewrite <- H1; ring. + apply sss_progress_trans with (length (mma_fractran_one p q j i)+i,x##0##ø). { apply subcode_sss_progress with (P := (i,mma_fractran_one p q j i)); auto. apply mma_fractran_one_nok_progress; auto. } { apply subcode_sss_progress with (P := (length (mma_fractran_one p q j i)+i, mma_fractran_step ll (length (mma_fractran_one p q j i)+i))); 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)