proposition: Fact mma_fractran_step_failure_compute Q i x : fractran_regular Q -> Q /F/ x ⊁ * -> (i,mma_fractran_step Q i) //ₐ (i,x##0##ø) ->> (length (mma_fractran_step Q i)+i,x##0##ø).
proof: Proof. unfold fractran_regular. intros H1 H2; revert H1 i H2. induction 1 as [ | (p,q) ll Hq Hll IH ]; intros i H4. + mma sss stop. + apply fractan_stop_cons_inv in H4 as (H4 & H5). unfold mma_fractran_step; fold mma_fractran_step. set (P := mma_fractran_one p q j i); rew length. apply sss_compute_trans with (length P+i,x##0##ø). * apply subcode_sss_compute with (P := (i,P)); auto. apply sss_progress_compute, mma_fractran_one_nok_progress; auto. * apply subcode_sss_compute with (P := (length P+i,mma_fractran_step ll (length P + i))); auto. replace (length P+length (mma_fractran_step ll (length P + i))+i) with (length (mma_fractran_step ll (length P + i)) + (length P+i)) by lia; 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)