proposition: Lemma signature_is_decidable n R : (forall p : syms_pred, decidable (fun v : Vector.t (obstring n) (ar_preds p) => @i_atom _ _ (obstring n) (@FIB R n) p v)).
proof: Proof. intros [| |]; cbn. - exists (fun X => if cdrv_decider R (Vector.hd X) (Vector.hd (Vector.tl X)) then true else false). intros X. destruct (cdrv_decider R (Vector.hd X) (Vector.hd (Vector.tl X))) as [Ht|Hf]; now split. - exists (fun X => if sub_decider (Vector.hd X) (Vector.hd (Vector.tl X)) then true else false). intros X. destruct (sub_decider (Vector.hd X) (Vector.hd (Vector.tl X))) as [Ht|Hf]; now split. - exists (fun X => if obstring_eqdec (Vector.hd X) (Vector.hd (Vector.tl X)) then true else false). intros X. destruct (obstring_eqdec (Vector.hd X) (Vector.hd (Vector.tl X))) as [Ht|Hf]; now split. Qed.
imports: Lia Arith Undecidability.PCP.PCP Undecidability.PCP.Util.PCP_facts Undecidability.Synthetic.DecidabilityFacts Undecidability(FOL.Utils.FullSyntax) Undecidability(FOL.FSAT) Undecidability.Shared.ListAutomation