English
Let t be a fixed element and ts a list of elements from α. For any r and L, where r is a list of lists and L is a list of lists, the length of the result of folding a transformation that extends each inner list in L using permutationsAux2 and then appending to r equals the sum of the lengths of all lists in L plus the length of r. Formally, length (foldr (λ y r, (permutationsAux2 t ts r y id).2) r L) = (map length L).sum + length r.
Русский
Пусть дан элемент t и список ts. Для любых r и L, где r — список списков и L — список списков, длина результата свёртки, который каждый элемент в L дополняет выбранной операцией permutationsAux2 и затем присоединяет к r, равна сумме длин всех списков в L плюс длина r. Формально: length (foldr (λ y r, (permutationsAux2 t ts r y id).2) r L) = (map length L).sum + length r.
LaTeX
$$$$\operatorname{length}\left(\mathrm{foldr}\left(\lambda y\, r,\; (\mathrm{permutationsAux2}\ t\ ts\ r\ y\ id).2\right)\ r\ L\right) = \left(\sum_{S \in L} \operatorname{length}(S)\right) + \operatorname{length}(r).$$$$
Lean4
theorem length_foldr_permutationsAux2 (t : α) (ts : List α) (r L : List (List α)) :
length (foldr (fun y r => (permutationsAux2 t ts r y id).2) r L) = (map length L).sum + length r := by
simp [foldr_permutationsAux2, length_permutationsAux2, length_flatMap]
