proposition: Fact mm_nullify_compute i lr v w : v#>zero = 0 -> (forall p, In p lr -> p <> zero) -> (forall p, In p lr -> w#>p = 0) -> (forall p, ~ In p lr -> w#>p = v#>p) -> (i,mm_nullify i lr) // (i,v) ->> (length (mm_nullify i lr)+i,w).
proof: Proof. rewrite mm_nullify_length. revert i v w; induction lr as [ | x lr IH ]; intros i v w H1 H2 H3 H4. mm sss stop; f_equal. apply vec_pos_ext; intros; rewrite H4; auto. rew length. unfold mm_nullify; fold mm_nullify. apply sss_compute_trans with (2+i,v[0/x]). apply subcode_sss_compute with (P := (i,mm_null x zero i)); auto. apply sss_progress_compute, mm_null_progress; auto. apply H2; left; auto. apply subcode_sss_compute with (P := (2+i,mm_nullify (2+i) lr)). subcode_tac; solve list eq. replace (2*S (length lr)+i) with (2*(length lr)+(2+i)) by lia. apply IH. specialize (H2 x (or_introl eq_refl)); rew vec. intros; apply H2; right; auto. intros; apply H3; right; auto. intros p Hp. dest p x. apply H3; left; auto. apply H4; intros [|]; auto. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils list_bool pos vec subcode sss) Undecidability.MinskyMachines.MM(mm_defs)