fact: Definition encode_constraint x y z := encode_bound x ++ encode_bound y ++ encode_bound z ++ encode_nat x ++ encode_nat y ++ encode_nat z ++ let x := embed (x, 0, 1) in let yy := embed (y, 1, 1) in let y := embed (y, 0, 1) in let z := embed (z, 0, 1) in [ (•0 ⊍ x ⊍ yy ⊍ yy ⊍ y, mset_term_var z) ].
imports: Arith Lia List Permutation Undecidability.SetConstraints.FMsetC Undecidability.SetConstraints.Util.Facts Undecidability.Synthetic.Definitions ssreflect ssrbool ssrfun