proposition: Lemma completeness {l} : FMsetTC_SAT l -> FMsetC_SAT (encode_problem l).
proof: Proof. move=> [φ] Hφ. pose ψ x := if x is 0 then [] else mset_sem φ (nat_to_term x). have H'ψ (A) : ψ (term_to_nat A) = mset_sem φ A. { by rewrite /ψ nat_term_cancel term_to_nat_pos. } have Hψ (A) : Forall (msetc_sem ψ) (term_to_msetcs A). { elim: A. - by constructor. - by rewrite /term_to_msetcs. - move=> A IHA B IHB /=. constructor; last by apply /Forall_app. by rewrite /msetc_sem !H'ψ. - move=> A IH /=. constructor; last done. by rewrite /msetc_sem !H'ψ. } exists ψ. rewrite -Forall_forall /encode_problem Forall_flat_map. apply: Forall_impl; last eassumption. move=> [A B] HφAB. apply /Forall_app. split; last by apply /Forall_app. constructor; [done|constructor;[|done]]. rewrite /msetc_sem !H'ψ. by apply /Permutation_count_occ. Qed.
imports: Arith Lia List Permutation Undecidability.SetConstraints.FMsetC Undecidability.SetConstraints.Util.Facts Undecidability.Synthetic.Definitions ssreflect ssrbool ssrfun