proposition: Fact mm_transfert_progress i v st : v#>dst = 0 -> v#>zero = 0 -> st = (3+i,v[0/src][(v#>src)/dst]) -> (i,mm_transfert i) // (i,v) -+> st.
proof: Proof. Proof using Hdz Hsz Hsd. intros H1 H2 ?; subst; apply mm_transfert_spec with (1 := eq_refl) (2 := eq_refl); auto. rewrite H1; apply vec_pos_ext; intros p; dest p dst. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss) Undecidability.MinskyMachines.MM(mm_defs)