proposition: Fact mma_null_list_spec l i v w : (forall p, In p l -> w#>p = 0) -> (forall p, ~ In p l -> w#>p = v#> p) -> (i,mma_null_list l i) // (i,v) ->> (length l+i,w).
proof: Proof. revert i v w; induction l as [ | x l IHl ]; simpl; intros i v w H1 H2. + replace w with v. 1: mma sss stop. apply vec_pos_ext; intro p; rewrite H2; auto. + apply subcode_sss_compute_trans with (P := (i,DECₐ x i::nil)) (st2 := (S i,v[0/x])); auto. * apply sss_progress_compute, mma_null_progress; auto. * apply subcode_sss_compute with (P := (S i, mma_null_list l (S i))); auto. replace (S (length l+i)) with (length l+S i) by lia. apply IHl. - intros; apply H1; auto. - intros p Hp. dest p x. apply H2; firstorder. Qed.
imports: List Arith Lia Undecidability.Shared.Libs.DLW(utils list_bool gcd pos vec subcode sss) Undecidability.MinskyMachines.MMA(mma_defs)