proposition: Lemma enum_tmap (f : @form Σ_funcs1 Σ_preds1 ops1 ff1 -> @form Σ_funcs2 Σ_preds2 ops2 ff2) (T : @theory Σ_funcs1 Σ_preds1 ops1 ff1) : enumerable T -> enumerable (tmap f T).
proof: Proof. intros (L & HL). exists (fun n => match (L n) with Some k => Some (f k) | None => None end). split. - intros (y & Hy & <-). destruct (HL y) as [HL1 HL2]. destruct (HL1 Hy) as [n Hn]. exists n. rewrite Hn. easy. - intros (n & Hn). destruct (L n) as [f0|] eqn:Heq; try congruence. exists f0. split; try congruence. destruct (HL f0) as [HL1 HL2]. apply HL2. exists n. easy. Qed.
imports: Undecidability.FOL.Syntax(Core Facts) Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability(Shared.ListAutomation) Undecidability(Shared.Libs.PSL.Vectors.Vectors) Coq.Setoids.Setoid Arith Lia List