English
Characterizes when an element l' belongs to the folded list in terms of possible membership in L or a construction from L's elements.
Русский
Описывает принадлежность элемента l' сложенному списку через принадлежность к L или конструктор из элементов L.
LaTeX
$$$\forall {\alpha}, {t}:{\alpha}, {ts}:{List\alpha}, {r}, {L}:{List\;List\alpha}, {l'}:{List\alpha},\; \; Iff \; (l' \in \\mathrm{foldr} (\\lambda y r. (List.permutationsAux2 t ts r y id).2) r L) l') \\Rightarrow (Or (List.instMembership.mem r l') (Exists l_1 l_2, l_1 ++ l_2 ∈ L ∧ l_2 ≠ [] ∧ l' = l_1 ++ t :: (l_2 ++ ts)))$$$
Lean4
theorem mem_foldr_permutationsAux2 {t : α} {ts : List α} {r L : List (List α)} {l' : List α} :
l' ∈ foldr (fun y r => (permutationsAux2 t ts r y id).2) r L ↔
l' ∈ r ∨ ∃ l₁ l₂, l₁ ++ l₂ ∈ L ∧ l₂ ≠ [] ∧ l' = l₁ ++ t :: l₂ ++ ts :=
by
have :
(∃ a : List α, a ∈ L ∧ ∃ l₁ l₂ : List α, ¬l₂ = nil ∧ a = l₁ ++ l₂ ∧ l' = l₁ ++ t :: (l₂ ++ ts)) ↔
∃ l₁ l₂ : List α, ¬l₂ = nil ∧ l₁ ++ l₂ ∈ L ∧ l' = l₁ ++ t :: (l₂ ++ ts) :=
⟨fun ⟨_, aL, l₁, l₂, l0, e, h⟩ => ⟨l₁, l₂, l0, e ▸ aL, h⟩, fun ⟨l₁, l₂, l0, aL, h⟩ => ⟨_, aL, l₁, l₂, l0, rfl, h⟩⟩
rw [foldr_permutationsAux2]
simp only [mem_permutationsAux2', ← this, or_comm, and_left_comm, mem_append, mem_flatMap, append_assoc, cons_append]
