String constraints and word equations

• String constraints: syntax and semantics
• Bounded string constraints: finite-search specification
• SAT and bounded string constraints: reduction correctness
• PCP characterization of a string-constraint family
• The closed straight-line fragment is decidable
• Ordinary word equations
• Bit-blasting word equations to the verified DPLL solver

TheoremLength-directed Levi's lemma#✓fully proved

Length-directed Levi's lemma: if u is no longer than x, then x splits as u ++ w and the remainders satisfy v = w ++ y. The general form is Mathlib's List.append_eq_append_iff, used directly.

theorem levi_of_le {u v x y : List α} (h : u ++ v = x ++ y)
    (hle : u.length ≤ x.length) : ∃ w, x = u ++ w ∧ v = w ++ y

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.