proposition: Theorem reduction : H10UC_SAT ⪯ FMsetTC_SAT.
proof: Proof. exists (fun h10ucs => flat_map Argument.encode_h10uc h10ucs). move=> h10ucs. constructor. - move=> [φ Hφ]. exists (Argument.construct_valuation φ). elim: h10ucs Hφ; first by constructor. move=> [[x y] z] h10cs IH. move /Forall_forall. rewrite Forall_cons_iff. move=> [Hxyz /Forall_forall /IH]. move=> {}IH. apply /Forall_app. constructor; last done. by apply: Argument.encode_constraint_sat. - move=> [φ] Hφ. pose ψ := (fun x => length (φ (Argument.embed (x, 0, 1)))). exists ψ. rewrite -Forall_forall. elim: h10ucs Hφ; first done. move=> [[x y] z] h10ucs IH. rewrite /flat_map -/(flat_map _) /mset_sat Forall_app /(Argument.encode_h10uc _). move=> [/Argument.encode_constraint_spec Hxyz /IH ?]. by constructor. Qed.
imports: Arith Lia List Permutation Undecidability.SetConstraints.FMsetC Undecidability.SetConstraints.Util.Facts Undecidability.Synthetic.Definitions ssreflect ssrbool ssrfun