proposition: Fact mma_transfert_progress v st : st = (3+i,v[0/src][((v#>src)+(v#>dst))/dst]) -> (i,mma_transfert) // (i,v) -+> st.
proof: Proof. Proof using Hsd. intros ?; subst. apply sss_progress_trans with (2+i, v[0/src][(1+(v#>src)+(v#>dst))/dst]). + apply mma_transfert_spec with (1 := eq_refl) (2 := eq_refl); auto. + unfold mma_transfert. mma sss DEC S with dst (3+i) ((v#>src)+(v#>dst)); rew vec. mma sss stop. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils list_bool gcd pos vec subcode sss) Undecidability.MinskyMachines.MMA(mma_defs)