proposition: Lemma eval_mono c min k (v : Vector.t nat k) (f : recalg k) o : eval c min (erase f) (vec_list v) = Some (inl o) -> forall c', c' >= c -> eval c' min (erase f) (vec_list v) = Some (inl o).
proof: Proof. intros H c' Hl. eapply erase_correct in H. eapply ra_bs_mono in H. 2: eauto. now eapply erase_correct in H. Qed.
imports: Undecidability.H10(H10 dio_single dio_logic) Undecidability.L.Datatypes(LNat LOptions LSum) Undecidability.L(Tactics.LTactics Computability.MuRec Computability.Synthetic Tactics.GenEncode) Undecidability.Shared(DLW.Utils.finite DLW.Vec.vec DLW.Vec.pos) Undecidability.MuRec(MuRec recalg ra_sem_eq) Undecidability.L.Reductions.MuRec.MuRec_extract Undecidability.L.Reductions.MuRec.MuRec_extract Undecidability(MuRec_computable LVector) Undecidability.L.Util(NaryApp ClosedLAdmissible) Undecidability(LOptions) Undecidability.L.Reductions.MuRec.MuRec_extract