proposition: Fact mm_zeroify_spec v : v#>zero = 0 -> (i,mm_zeroify) // (i,v) -+> (0,vec_zero).
proof: Proof. intros H; unfold mm_zeroify. apply sss_compute_progress_trans with (length (mm_nullify zero i l)+i,vec_zero). + apply subcode_sss_compute with (P := (i,mm_nullify zero i l)); auto. apply mm_nullify_compute; auto; unfold l; intros p; rewrite filter_In; unfold c; destruct (pos_eq_dec p zero); subst; auto. all: try rewrite vec_zero_spec; try rewrite H; auto. * intros []; easy. * intros []; split; auto; apply pos_list_prop. + mm sss DEC zero with zero 0; auto. * now rewrite vec_zero_spec. * mm sss stop. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss) Undecidability.MinskyMachines.MM(mm_defs)