proposition: Lemma encode_nat_spec {φ x} : mset_sat φ (encode_bound x) -> mset_sat φ (encode_nat x) -> length (φ (embed (x, 1, 1))) + length (φ (embed (x, 1, 1))) + length (φ (embed (x, 0, 1))) = length (φ (embed (x, 0, 1))) * length (φ (embed (x, 0, 1))).
proof: Proof. move /encode_bound_spec. rewrite /mset_sat /encode_nat ?Forall_cons_iff Forall_nil_iff /mset_sem. pose X n := φ (embed (x, n, 1)). rewrite -?/(X _). move=> /(@Forall_eq_repeat nat) ->. move: (length (φ _)) => m. move=> [/(Permutation_repeat 0) H1] [/(Permutation_repeat 0) H2]. have -> : map S (X 4) = map [eta Init.Nat.add 1] (X 4) by done. move=> [/seq_spec2 [n]]. rewrite (map_ext (Nat.mul 1) id); [lia|]. rewrite map_id. move=> [->] _ []. have -> : X 0 = repeat 0 (length (X 0)). { elim: (X 0) (m) H1; [done|]. move=> ?? /= IH [|m'] /=; [done|]. move=> [-> /IH] ->. by rewrite repeat_length. } move=> /[dup] H3. rewrite repeat_length. have -> : length (X 0) = n. { move: H3 => /Permutation_length. rewrite !app_length map_length seq_length repeat_length. by lia. } move=> /square_spec <- [/Permutation_length]. rewrite !app_length map_length. by lia. Qed.
imports: Arith Lia List Permutation Undecidability.SetConstraints.FMsetC Undecidability.SetConstraints.Util.Facts Undecidability.Synthetic.Definitions ssreflect ssrbool ssrfun