Pattern avoidance in inversion sequences

DefinitionContainment of a length-3 pattern#✓fully proved

A sequence \(e = e_0 e_1 \cdots e_{n-1}\) of natural numbers contains the length-3 pattern \(p = p_0 p_1 p_2\) of natural numbers when there are positions \(i_0 < i_1 < i_2\) in \(\{0, \dots, n - 1\}\) such that, for all \(a, b \in \{0, 1, 2\}\), \(e_{i_a} < e_{i_b}\) if and only if \(p_a < p_b\); that is, the subsequence \(e_{i_0} e_{i_1} e_{i_2}\) is order-isomorphic to \(p\).

def InvSeqContainsPattern {n : ℕ} (e : Fin n → ℕ) (p : Fin 3 → ℕ) : Prop :=
  ∃ f : Fin 3 ↪o Fin n, ∀ a b, e (f a) < e (f b) ↔ p a < p b

Sources

• Toufik Mansour, Inversion Sequences Avoiding a Set of Length-3 Patterns, INTEGERS 24 (2024), Article A76, Introduction.

Used by 4

Used byNumber of inversion sequences avoiding a set of patterns · One inversion sequence of length one · Reducible sets of length-3 patterns for inversion sequences · Short sequences contain no length-3 pattern

TheoremShort sequences contain no length-3 pattern#✓fully proved

If \(n < 3\), then no sequence \(e_0 e_1 \cdots e_{n-1}\) of natural numbers contains a length-3 pattern \(p\).

theorem not_invSeqContainsPattern_of_lt {n : ℕ} (hn : n < 3) (e : Fin n → ℕ)
    (p : Fin 3 → ℕ) : ¬ InvSeqContainsPattern e p

Sources

• Toufik Mansour, Inversion Sequences Avoiding a Set of Length-3 Patterns, INTEGERS 24 (2024), Article A76, Introduction.

Uses 1 · Used by 1

Statement usesContainment of a length-3 pattern

Used byOne inversion sequence of length one

DefinitionNumber of inversion sequences avoiding a set of patterns#✓fully proved

An inversion sequence of length \(n\) is a sequence \(e = e_0 e_1 \cdots e_{n-1}\) of natural numbers with \(e_i \le i\) for every \(i\). It contains a length-3 pattern \(p = p_0 p_1 p_2\) (a triple of natural numbers) when some subsequence \(e_a e_b e_c\) with \(a < b < c\) is order-isomorphic to \(p\). For a set \(B\) of length-3 patterns, \(|I_n(B)|\) is the number of inversion sequences of length \(n\) that contain no pattern of \(B\).

noncomputable def invSeqAvoidCount (B : Set (Fin 3 → ℕ)) (n : ℕ) : ℕ :=
  Nat.card {e : Fin n → ℕ // (∀ i, e i ≤ i) ∧ ∀ p ∈ B, ¬ InvSeqContainsPattern e p}

Sources

• Toufik Mansour, Inversion Sequences Avoiding a Set of Length-3 Patterns, INTEGERS 24 (2024), Article A76, Introduction.

Uses 1 · Used by 16

Statement usesContainment of a length-3 pattern

Used byCoefficients of the generating function of pattern-avoiding inversion sequences · One inversion sequence of length one · Generating function of inversion sequences avoiding a set of patterns · I-Wilf equivalence of \(\{000, 010, 100, 101, 120\}\) and \(\{000, 010, 100, 110, 120\}\) · Three I-Wilf-equivalent sets of five patterns containing \(000\), \(010\) and \(120\) · Five I-Wilf-equivalent sets of six patterns containing \(000\), \(010\) and \(120\) · Two I-Wilf equivalences exchanging \(201\) and \(210\) in five-pattern sets · Three I-Wilf-equivalent sets of five patterns containing \(000\), \(102\) and \(120\) · Exchanging \(201\) and \(210\) in \(\{010, 100, 101, 102, 120, 201\}\) · I-Wilf equivalence of \(\{010, 100, 101, 120, 201\}\) and \(\{010, 100, 101, 120, 210\}\) · I-Wilf equivalences among five-pattern sets containing \(010\), \(102\) and \(120\) · I-Wilf-equivalence of 101 and 110 alongside 010, 120, 201, 210 · Three I-Wilf-equivalent six-pattern sets containing 102 and 110 · I-Wilf-equivalence of 101 and 110 alongside 102, 120, 210 · Number of I-Wilf classes of sets of length-3 patterns · Eight-pattern sets differing in 201 and 210: equivalence and generating function

TheoremOne inversion sequence of length one#✓fully proved

For every set \(B\) of length-3 patterns, the number \(|I_1(B)|\) of inversion sequences of length one that avoid every pattern in \(B\) equals \(1\): the only inversion sequence of length one is \(0\), and it avoids every length-3 pattern.

theorem invSeqAvoidCount_one (B : Set (Fin 3 → ℕ)) : invSeqAvoidCount B 1 = 1

Sources

• Toufik Mansour, Inversion Sequences Avoiding a Set of Length-3 Patterns, INTEGERS 24 (2024), Article A76, Introduction.

Uses 3

Statement usesNumber of inversion sequences avoiding a set of patterns

Proof usesContainment of a length-3 pattern · Short sequences contain no length-3 pattern

DefinitionGenerating function of inversion sequences avoiding a set of patterns#✓fully proved

For a set \(B\) of length-3 patterns, \(F_B(x) = \sum_{n \ge 1} |I_n(B)| x^n\) is the formal power series in \(\mathbb{Q}[[x]]\) with constant coefficient \(0\) whose coefficient of \(x^n\), for \(n \ge 1\), is the number \(|I_n(B)|\) of inversion sequences of length \(n\) that avoid every pattern in \(B\).

noncomputable def invSeqAvoidGF (B : Set (Fin 3 → ℕ)) : ℚ⟦X⟧ :=
  PowerSeries.mk fun n => if n = 0 then 0 else (invSeqAvoidCount B n : ℚ)

Sources

• Toufik Mansour, Inversion Sequences Avoiding a Set of Length-3 Patterns, INTEGERS 24 (2024), Article A76, Section 2.

Uses 1 · Used by 8

Statement usesNumber of inversion sequences avoiding a set of patterns

Used byCoefficients of the generating function of pattern-avoiding inversion sequences · Inversion sequences avoiding \(\{000, 100, 101, 102, 110, 120, 201, 210\}\) · A common generating function for three sets of seven patterns · A Catalan generating function for two sets of five patterns · Inversion sequences avoiding \(\{011, 102, 120\}\) · A common generating function for three sets of eight patterns · Inversion sequences avoiding nine patterns · Eight-pattern sets differing in 201 and 210: equivalence and generating function

TheoremCoefficients of the generating function of pattern-avoiding inversion sequences#✓fully proved

For every set \(B\) of length-3 patterns and every \(n \ge 0\), the generating function \(F_B(x) = \sum_{m \ge 1} |I_m(B)| x^m \in \mathbb{Q}[[x]]\) has constant coefficient \(0\), and its coefficient of \(x^{n+1}\) is \(|I_{n+1}(B)|\), the number of inversion sequences of length \(n + 1\) that avoid every pattern in \(B\).

theorem coeff_invSeqAvoidGF (B : Set (Fin 3 → ℕ)) (n : ℕ) :
    coeff 0 (invSeqAvoidGF B) = 0 ∧
      coeff (n + 1) (invSeqAvoidGF B) = (invSeqAvoidCount B (n + 1) : ℚ)

Sources

• Toufik Mansour, Inversion Sequences Avoiding a Set of Length-3 Patterns, INTEGERS 24 (2024), Article A76, Section 2.

Uses 2

Statement usesNumber of inversion sequences avoiding a set of patterns · Generating function of inversion sequences avoiding a set of patterns

TheoremI-Wilf equivalence of \(\{000, 010, 100, 101, 120\}\) and \(\{000, 010, 100, 110, 120\}\)#●ready to prove

Write length-3 patterns as digit strings (\(101\) is the pattern \((1, 0, 1)\)) and let \(|I_n(B)|\) be the number of inversion sequences of length \(n\) that avoid every pattern in the set \(B\). Then for every \(n \ge 0\), \(|I_n(\{000, 010, 100, 101, 120\})| = |I_n(\{000, 010, 100, 110, 120\})|\).

public theorem_wanted invSeq_wilf_000_010_100_120_101_110 :
    invSeqAvoidCount ({![0, 0, 0], ![0, 1, 0], ![1, 0, 0], ![1, 0, 1], ![1, 2, 0]}
        : Set (Fin 3 → ℕ)) =
      invSeqAvoidCount ({![0, 0, 0], ![0, 1, 0], ![1, 0, 0], ![1, 1, 0], ![1, 2, 0]}
          : Set (Fin 3 → ℕ))

Sources

• Toufik Mansour, Inversion Sequences Avoiding a Set of Length-3 Patterns, INTEGERS 24 (2024), Article A76, Theorem 4.

Uses 1

Statement usesNumber of inversion sequences avoiding a set of patterns

TheoremThree I-Wilf-equivalent sets of five patterns containing \(000\), \(010\) and \(120\)#●ready to prove

Write length-3 patterns as digit strings (\(101\) is the pattern \((1, 0, 1)\)) and let \(|I_n(B)|\) be the number of inversion sequences of length \(n\) that avoid every pattern in the set \(B\). For \(B_1 = \{000, 010, 101, 120, 201\}\), \(B_2 = \{000, 010, 101, 120, 210\}\) and \(B_3 = \{000, 010, 110, 120, 210\}\), and for every \(n \ge 0\), \(|I_n(B_1)| = |I_n(B_2)| = |I_n(B_3)|\).

public theorem_wanted invSeq_wilf_000_010_120_five_class :
    invSeqAvoidCount ({![0, 0, 0], ![0, 1, 0], ![1, 0, 1], ![1, 2, 0], ![2, 0, 1]}
        : Set (Fin 3 → ℕ)) =
      invSeqAvoidCount ({![0, 0, 0], ![0, 1, 0], ![1, 0, 1], ![1, 2, 0], ![2, 1, 0]}
          : Set (Fin 3 → ℕ)) ∧
    invSeqAvoidCount ({![0, 0, 0], ![0, 1, 0], ![1, 0, 1], ![1, 2, 0], ![2, 1, 0]}
        : Set (Fin 3 → ℕ)) =
      invSeqAvoidCount ({![0, 0, 0], ![0, 1, 0], ![1, 1, 0], ![1, 2, 0], ![2, 1, 0]}
          : Set (Fin 3 → ℕ))

Sources

• Toufik Mansour, Inversion Sequences Avoiding a Set of Length-3 Patterns, INTEGERS 24 (2024), Article A76, Theorem 5.

Uses 1

Statement usesNumber of inversion sequences avoiding a set of patterns

TheoremInversion sequences avoiding \(\{011, 102, 120\}\)#●ready to prove

Let \(B = \{011, 102, 120\}\), where a pattern is written as a digit string (\(101\) is the triple \((1, 0, 1)\)), and let \(F_B(x) = \sum_{n \ge 1} |I_n(B)| x^n \in \mathbb{Q}[[x]]\) be the generating function of the inversion sequences avoiding every pattern in \(B\). Then

\[(1 - 2x)^2 F_B(x) = x(1 - x)^2.\]

Since \((1 - 2x)^2\) is a unit in \(\mathbb{Q}[[x]]\), this says \(F_B(x) = x(1 - x)^2/(1 - 2x)^2\).

public theorem_wanted invSeqAvoidGF_011_102_120 :
    (1 - 2 * X) ^ 2 * invSeqAvoidGF ({![0, 1, 1], ![1, 0, 2], ![1, 2, 0]} : Set (Fin 3 → ℕ)) =
      X * (1 - X) ^ 2

Sources

• Toufik Mansour, Inversion Sequences Avoiding a Set of Length-3 Patterns, INTEGERS 24 (2024), Article A76, Theorem 6.

Uses 1

Statement usesGenerating function of inversion sequences avoiding a set of patterns

TheoremThree I-Wilf-equivalent sets of five patterns containing \(000\), \(102\) and \(120\)#●ready to prove

Write length-3 patterns as digit strings (\(101\) is the pattern \((1, 0, 1)\)) and let \(|I_n(B)|\) be the number of inversion sequences of length \(n\) that avoid every pattern in the set \(B\). For \(B_1 = \{000, 101, 102, 120, 201\}\), \(B_2 = \{000, 101, 102, 120, 210\}\) and \(B_3 = \{000, 102, 110, 120, 210\}\), and for every \(n \ge 0\), \(|I_n(B_1)| = |I_n(B_2)| = |I_n(B_3)|\).

public theorem_wanted invSeq_wilf_000_102_120_five_class :
    invSeqAvoidCount ({![0, 0, 0], ![1, 0, 1], ![1, 0, 2], ![1, 2, 0], ![2, 0, 1]}
        : Set (Fin 3 → ℕ)) =
      invSeqAvoidCount ({![0, 0, 0], ![1, 0, 1], ![1, 0, 2], ![1, 2, 0], ![2, 1, 0]}
          : Set (Fin 3 → ℕ)) ∧
    invSeqAvoidCount ({![0, 0, 0], ![1, 0, 1], ![1, 0, 2], ![1, 2, 0], ![2, 1, 0]}
        : Set (Fin 3 → ℕ)) =
      invSeqAvoidCount ({![0, 0, 0], ![1, 0, 2], ![1, 1, 0], ![1, 2, 0], ![2, 1, 0]}
          : Set (Fin 3 → ℕ))

Sources

• Toufik Mansour, Inversion Sequences Avoiding a Set of Length-3 Patterns, INTEGERS 24 (2024), Article A76, Theorem 7.

Uses 1

Statement usesNumber of inversion sequences avoiding a set of patterns

TheoremTwo I-Wilf equivalences exchanging \(201\) and \(210\) in five-pattern sets#●ready to prove

Write length-3 patterns as digit strings (\(101\) is the pattern \((1, 0, 1)\)) and let \(|I_n(B)|\) be the number of inversion sequences of length \(n\) that avoid every pattern in the set \(B\). For a pattern \(\tau\) let \(A_\tau = \{000, 100, 101, 120, \tau\}\) and \(B_\tau = \{000, 100, 110, 120, \tau\}\). Then for every \(n \ge 0\), \(|I_n(A_{201})| = |I_n(A_{210})|\) and \(|I_n(B_{201})| = |I_n(B_{210})|\).

public theorem_wanted invSeq_wilf_000_100_120_201_210 :
    invSeqAvoidCount ({![0, 0, 0], ![1, 0, 0], ![1, 0, 1], ![1, 2, 0], ![2, 0, 1]}
        : Set (Fin 3 → ℕ)) =
      invSeqAvoidCount ({![0, 0, 0], ![1, 0, 0], ![1, 0, 1], ![1, 2, 0], ![2, 1, 0]}
          : Set (Fin 3 → ℕ)) ∧
    invSeqAvoidCount ({![0, 0, 0], ![1, 0, 0], ![1, 1, 0], ![1, 2, 0], ![2, 0, 1]}
        : Set (Fin 3 → ℕ)) =
      invSeqAvoidCount ({![0, 0, 0], ![1, 0, 0], ![1, 1, 0], ![1, 2, 0], ![2, 1, 0]}
          : Set (Fin 3 → ℕ))

Sources

• Toufik Mansour, Inversion Sequences Avoiding a Set of Length-3 Patterns, INTEGERS 24 (2024), Article A76, Theorem 8.

Uses 1

Statement usesNumber of inversion sequences avoiding a set of patterns

TheoremI-Wilf equivalences among five-pattern sets containing \(010\), \(102\) and \(120\)#●ready to prove

Write length-3 patterns as digit strings (\(101\) is the pattern \((1, 0, 1)\)) and let \(|I_n(B)|\) be the number of inversion sequences of length \(n\) that avoid every pattern in the set \(B\). For a pattern \(\tau\) let \(A_\tau = \{010, \tau, 102, 120, 201\}\) and \(A'_\tau = \{010, \tau, 102, 120, 210\}\), and let \(B = \{010, 101, 102, 120, 201\}\). Then for every \(n \ge 0\), \(|I_n(A_{100})| = |I_n(A_{110})|\) and \(|I_n(A'_{100})| = |I_n(A'_{101})| = |I_n(A'_{110})| = |I_n(B)|\).

MetaMathlibExt.invSeq_wilf_010_102_120_five_classes · 17 lines

public theorem_wanted invSeq_wilf_010_102_120_five_classes :
    invSeqAvoidCount ({![0, 1, 0], ![1, 0, 0], ![1, 0, 2], ![1, 2, 0], ![2, 0, 1]}
        : Set (Fin 3 → ℕ)) =
      invSeqAvoidCount ({![0, 1, 0], ![1, 1, 0], ![1, 0, 2], ![1, 2, 0], ![2, 0, 1]}
          : Set (Fin 3 → ℕ)) ∧
    invSeqAvoidCount ({![0, 1, 0], ![1, 0, 0], ![1, 0, 2], ![1, 2, 0], ![2, 1, 0]}
        : Set (Fin 3 → ℕ)) =
      invSeqAvoidCount ({![0, 1, 0], ![1, 0, 1], ![1, 0, 2], ![1, 2, 0], ![2, 1, 0]}
          : Set (Fin 3 → ℕ)) ∧
    invSeqAvoidCount ({![0, 1, 0], ![1, 0, 1], ![1, 0, 2], ![1, 2, 0], ![2, 1, 0]}
        : Set (Fin 3 → ℕ)) =
      invSeqAvoidCount ({![0, 1, 0], ![1, 1, 0], ![1, 0, 2], ![1, 2, 0], ![2, 1, 0]}
          : Set (Fin 3 → ℕ)) ∧
    invSeqAvoidCount ({![0, 1, 0], ![1, 1, 0], ![1, 0, 2], ![1, 2, 0], ![2, 1, 0]}
        : Set (Fin 3 → ℕ)) =
      invSeqAvoidCount ({![0, 1, 0], ![1, 0, 1], ![1, 0, 2], ![1, 2, 0], ![2, 0, 1]}
          : Set (Fin 3 → ℕ))

Sources

• Toufik Mansour, Inversion Sequences Avoiding a Set of Length-3 Patterns, INTEGERS 24 (2024), Article A76, Theorem 9.

Uses 1

Statement usesNumber of inversion sequences avoiding a set of patterns

TheoremI-Wilf equivalence of \(\{010, 100, 101, 120, 201\}\) and \(\{010, 100, 101, 120, 210\}\)#●ready to prove

Write length-3 patterns as digit strings (\(101\) is the pattern \((1, 0, 1)\)) and let \(|I_n(B)|\) be the number of inversion sequences of length \(n\) that avoid every pattern in the set \(B\). Then for every \(n \ge 0\), \(|I_n(\{010, 100, 101, 120, 201\})| = |I_n(\{010, 100, 101, 120, 210\})|\).

public theorem_wanted invSeq_wilf_010_100_101_120_201_210 :
    invSeqAvoidCount ({![0, 1, 0], ![1, 0, 0], ![1, 0, 1], ![1, 2, 0], ![2, 0, 1]}
        : Set (Fin 3 → ℕ)) =
      invSeqAvoidCount ({![0, 1, 0], ![1, 0, 0], ![1, 0, 1], ![1, 2, 0], ![2, 1, 0]}
          : Set (Fin 3 → ℕ))

Sources

• Toufik Mansour, Inversion Sequences Avoiding a Set of Length-3 Patterns, INTEGERS 24 (2024), Article A76, Theorem 11.

Uses 1

Statement usesNumber of inversion sequences avoiding a set of patterns

TheoremFive I-Wilf-equivalent sets of six patterns containing \(000\), \(010\) and \(120\)#●ready to prove

Write length-3 patterns as digit strings (\(101\) is the pattern \((1, 0, 1)\)) and let \(|I_n(B)|\) be the number of inversion sequences of length \(n\) that avoid every pattern in the set \(B\). For a pattern \(\tau\) let \(A_\tau = \{000, 010, 100, 101, 120, \tau\}\) and \(B_\tau = \{000, 010, 100, 110, 120, \tau\}\), and let \(C = \{000, 010, 101, 110, 120, 201\}\). Then for every \(n \ge 0\), \(|I_n(A_{201})| = |I_n(A_{210})| = |I_n(B_{201})| = |I_n(B_{210})| = |I_n(C)|\).

MetaMathlibExt.invSeq_wilf_000_010_120_six_class · 17 lines

public theorem_wanted invSeq_wilf_000_010_120_six_class :
    invSeqAvoidCount ({![0, 0, 0], ![0, 1, 0], ![1, 0, 0], ![1, 0, 1], ![1, 2, 0], ![2, 0, 1]}
        : Set (Fin 3 → ℕ)) =
      invSeqAvoidCount ({![0, 0, 0], ![0, 1, 0], ![1, 0, 0], ![1, 0, 1], ![1, 2, 0], ![2, 1, 0]}
          : Set (Fin 3 → ℕ)) ∧
    invSeqAvoidCount ({![0, 0, 0], ![0, 1, 0], ![1, 0, 0], ![1, 0, 1], ![1, 2, 0], ![2, 1, 0]}
        : Set (Fin 3 → ℕ)) =
      invSeqAvoidCount ({![0, 0, 0], ![0, 1, 0], ![1, 0, 0], ![1, 1, 0], ![1, 2, 0], ![2, 0, 1]}
          : Set (Fin 3 → ℕ)) ∧
    invSeqAvoidCount ({![0, 0, 0], ![0, 1, 0], ![1, 0, 0], ![1, 1, 0], ![1, 2, 0], ![2, 0, 1]}
        : Set (Fin 3 → ℕ)) =
      invSeqAvoidCount ({![0, 0, 0], ![0, 1, 0], ![1, 0, 0], ![1, 1, 0], ![1, 2, 0], ![2, 1, 0]}
          : Set (Fin 3 → ℕ)) ∧
    invSeqAvoidCount ({![0, 0, 0], ![0, 1, 0], ![1, 0, 0], ![1, 1, 0], ![1, 2, 0], ![2, 1, 0]}
        : Set (Fin 3 → ℕ)) =
      invSeqAvoidCount ({![0, 0, 0], ![0, 1, 0], ![1, 0, 1], ![1, 1, 0], ![1, 2, 0], ![2, 0, 1]}
          : Set (Fin 3 → ℕ))

Sources

• Toufik Mansour, Inversion Sequences Avoiding a Set of Length-3 Patterns, INTEGERS 24 (2024), Article A76, Theorem 13.

Uses 1

Statement usesNumber of inversion sequences avoiding a set of patterns

TheoremThree I-Wilf-equivalent six-pattern sets containing 102 and 110#●ready to prove

Write a length-3 pattern as the word of its values, so \(101\) is the pattern \((1, 0, 1)\), and for a set \(B\) of patterns let \(|I_n(B)|\) be the number of inversion sequences of length \(n\) that avoid every pattern in \(B\). Let \(A_\tau = \{011, 101, 102, 110, 120, \tau\}\) and \(C = \{011, 021, 102, 110, 201, 210\}\). Then \(|I_n(A_{201})| = |I_n(A_{210})| = |I_n(C)|\) for every \(n \ge 0\).

public theorem_wanted invSeq_wilf_102_110_six_class :
    invSeqAvoidCount ({![0, 1, 1], ![1, 0, 1], ![1, 0, 2], ![1, 1, 0], ![1, 2, 0], ![2, 0, 1]}
        : Set (Fin 3 → ℕ)) =
      invSeqAvoidCount ({![0, 1, 1], ![1, 0, 1], ![1, 0, 2], ![1, 1, 0], ![1, 2, 0], ![2, 1, 0]}
          : Set (Fin 3 → ℕ)) ∧
    invSeqAvoidCount ({![0, 1, 1], ![1, 0, 1], ![1, 0, 2], ![1, 1, 0], ![1, 2, 0], ![2, 1, 0]}
        : Set (Fin 3 → ℕ)) =
      invSeqAvoidCount ({![0, 1, 1], ![0, 2, 1], ![1, 0, 2], ![1, 1, 0], ![2, 0, 1], ![2, 1, 0]}
          : Set (Fin 3 → ℕ))

Sources

• Toufik Mansour, Inversion Sequences Avoiding a Set of Length-3 Patterns, INTEGERS 24 (2024), Article A76, Theorem 14.

Uses 1

Statement usesNumber of inversion sequences avoiding a set of patterns

TheoremA common generating function for three sets of seven patterns#●ready to prove

Let \(B_1 = \{010, 011, 100, 101, 102, 201, 210\}\), \(B_2 = \{010, 011, 100, 102, 110, 201, 210\}\) and \(B_3 = \{010, 011, 101, 102, 110, 201, 210\}\), where a pattern is written as a digit string (\(101\) is the triple \((1, 0, 1)\)). For a set \(B\) of patterns let \(F_B(x) = \sum_{n \ge 1} |I_n(B)| x^n \in \mathbb{Q}[[x]]\) be the generating function of the inversion sequences avoiding every pattern in \(B\). Then for each \(j \in \{1, 2, 3\}\),

\[(1 - x)(1 - 2x)^2 F_{B_j}(x) = x(1 - 2x)^2 + x^2(1 - x)^2.\]

Since \((1 - x)(1 - 2x)^2\) is a unit in \(\mathbb{Q}[[x]]\), this says \(F_{B_j}(x) = x/(1 - x) + x^2(1 - x)/(1 - 2x)^2\).

public theorem_wanted invSeqAvoidGF_010_011_102_201_210_seven :
    ∀ B : Set (Fin 3 → ℕ),
      (B = {![0, 1, 0], ![0, 1, 1], ![1, 0, 0], ![1, 0, 1], ![1, 0, 2], ![2, 0, 1], ![2, 1, 0]} ∨
        B = {![0, 1, 0], ![0, 1, 1], ![1, 0, 0], ![1, 0, 2], ![1, 1, 0], ![2, 0, 1], ![2, 1, 0]} ∨
        B = {![0, 1, 0], ![0, 1, 1], ![1, 0, 1], ![1, 0, 2], ![1, 1, 0], ![2, 0, 1], ![2, 1, 0]}) →
      (1 - X) * (1 - 2 * X) ^ 2 * invSeqAvoidGF B =
        X * (1 - 2 * X) ^ 2 + X ^ 2 * (1 - X) ^ 2

Sources

• Toufik Mansour, Inversion Sequences Avoiding a Set of Length-3 Patterns, INTEGERS 24 (2024), Article A76, Theorem 16.

Uses 1

Statement usesGenerating function of inversion sequences avoiding a set of patterns

TheoremEight-pattern sets differing in 201 and 210: equivalence and generating function#●ready to prove

Write a length-3 pattern as the word of its values, so \(101\) is the pattern \((1, 0, 1)\). For a set \(B\) of patterns let \(|I_n(B)|\) be the number of inversion sequences of length \(n\) that avoid every pattern in \(B\), and let \(F_B(x) = \sum_{n \ge 1} |I_n(B)| x^n \in \mathbb{Q}[[x]]\). Let \(B_\tau = \{000, 010, 100, 101, 102, 110, 120, \tau\}\). Then \(|I_n(B_{201})| = |I_n(B_{210})|\) for every \(n \ge 0\), and for every power series \(s \in \mathbb{Q}[[x]]\) with constant term \(1\) and \(s^2 = 1 - 2x - 3x^2\),

\[ 2x^3 (1 + x)(x^2 + 2x + 2) F_{B_{201}}(x) = 1 - x^2 - 4x^3 - 7x^4 - 5x^5 - 2x^6 - (1 + x + 2x^2 + 2x^3 + x^4) s. \]

This is the paper's closed form for \(F_{B_{201}}\) with the denominator cleared, where \(s\) plays the role of \(\sqrt{1 - 2x - 3x^2}\).

public theorem_wanted invSeq_wilf_eight_201_210_and_gf :
    invSeqAvoidCount ({![0, 0, 0], ![0, 1, 0], ![1, 0, 0], ![1, 0, 1], ![1, 0, 2], ![1, 1, 0],
        ![1, 2, 0], ![2, 0, 1]} : Set (Fin 3 → ℕ)) =
      invSeqAvoidCount ({![0, 0, 0], ![0, 1, 0], ![1, 0, 0], ![1, 0, 1], ![1, 0, 2], ![1, 1, 0],
        ![1, 2, 0], ![2, 1, 0]} : Set (Fin 3 → ℕ)) ∧
    ∀ s : ℚ⟦X⟧, constantCoeff s = 1 → s ^ 2 = 1 - 2 * X - 3 * X ^ 2 →
      2 * X ^ 3 * (1 + X) * (X ^ 2 + 2 * X + 2) *
          invSeqAvoidGF ({![0, 0, 0], ![0, 1, 0], ![1, 0, 0], ![1, 0, 1], ![1, 0, 2], ![1, 1, 0],
            ![1, 2, 0], ![2, 0, 1]} : Set (Fin 3 → ℕ)) =
        1 - X ^ 2 - 4 * X ^ 3 - 7 * X ^ 4 - 5 * X ^ 5 - 2 * X ^ 6 -
          (1 + X + 2 * X ^ 2 + 2 * X ^ 3 + X ^ 4) * s

Sources

• Toufik Mansour, Inversion Sequences Avoiding a Set of Length-3 Patterns, INTEGERS 24 (2024), Article A76, Theorem 17.

Uses 2

Statement usesNumber of inversion sequences avoiding a set of patterns · Generating function of inversion sequences avoiding a set of patterns

TheoremA common generating function for three sets of eight patterns#●ready to prove

Let \(B_1 = \{000, 010, 100, 101, 102, 120, 201, 210\}\), \(B_2 = \{000, 010, 100, 102, 110, 120, 201, 210\}\) and \(B_3 = \{000, 010, 101, 102, 110, 120, 201, 210\}\), where a pattern is written as a digit string (\(101\) is the triple \((1, 0, 1)\)). For a set \(B\) of patterns let \(F_B(x) = \sum_{n \ge 1} |I_n(B)| x^n \in \mathbb{Q}[[x]]\) be the generating function of the inversion sequences avoiding every pattern in \(B\). For each \(j \in \{1, 2, 3\}\) and every power series \(s \in \mathbb{Q}[[x]]\) with constant term \(1\) and \(s^2 = 1 - 2x - 3x^2\),

\[x^2 F_{B_j}(x) = 1 - 2x - x^2 + x^3 - (1 - x) s.\]

This is the closed form \(F_{B_j}(x) = (1 - 2x - x^2 + x^3 - (1 - x)\sqrt{1 - 2x - 3x^2}) / x^2\) with the denominator cleared, \(s\) standing for \(\sqrt{1 - 2x - 3x^2}\).

public theorem_wanted invSeqAvoidGF_eight_radical_three :
    ∀ B : Set (Fin 3 → ℕ),
      (B = {![0, 0, 0], ![0, 1, 0], ![1, 0, 0], ![1, 0, 1], ![1, 0, 2], ![1, 2, 0], ![2, 0, 1],
          ![2, 1, 0]} ∨
        B = {![0, 0, 0], ![0, 1, 0], ![1, 0, 0], ![1, 0, 2], ![1, 1, 0], ![1, 2, 0], ![2, 0, 1],
          ![2, 1, 0]} ∨
        B = {![0, 0, 0], ![0, 1, 0], ![1, 0, 1], ![1, 0, 2], ![1, 1, 0], ![1, 2, 0], ![2, 0, 1],
          ![2, 1, 0]}) →
      ∀ s : ℚ⟦X⟧, constantCoeff s = 1 → s ^ 2 = 1 - 2 * X - 3 * X ^ 2 →
        X ^ 2 * invSeqAvoidGF B = 1 - 2 * X - X ^ 2 + X ^ 3 - (1 - X) * s

Sources

• Toufik Mansour, Inversion Sequences Avoiding a Set of Length-3 Patterns, INTEGERS 24 (2024), Article A76, Theorem 18.

Uses 1

Statement usesGenerating function of inversion sequences avoiding a set of patterns

TheoremInversion sequences avoiding \(\{000, 100, 101, 102, 110, 120, 201, 210\}\)#●ready to prove

Let \(B = \{000, 100, 101, 102, 110, 120, 201, 210\}\), where a pattern is written as a digit string (\(101\) is the triple \((1, 0, 1)\)), and let \(F_B(x) = \sum_{n \ge 1} |I_n(B)| x^n \in \mathbb{Q}[[x]]\) be the generating function of the inversion sequences avoiding every pattern in \(B\). For every power series \(s \in \mathbb{Q}[[x]]\) with constant term \(1\) and \(s^2 = 1 - 2x - 3x^2\),

\[2x^2(1 + x) F_B(x) = 2 - 2x - 5x^2 - x^3 - (2 - x^2) s.\]

This is the closed form \(F_B(x) = (2 - 2x - 5x^2 - x^3 - (2 - x^2)\sqrt{1 - 2x - 3x^2}) / (2x^2(1 + x))\) with the denominator cleared, \(s\) standing for \(\sqrt{1 - 2x - 3x^2}\).

public theorem_wanted invSeqAvoidGF_000_100_101_102_110_120_201_210 :
    ∀ s : ℚ⟦X⟧, constantCoeff s = 1 → s ^ 2 = 1 - 2 * X - 3 * X ^ 2 →
      2 * X ^ 2 * (1 + X) *
          invSeqAvoidGF ({![0, 0, 0], ![1, 0, 0], ![1, 0, 1], ![1, 0, 2], ![1, 1, 0], ![1, 2, 0],
            ![2, 0, 1], ![2, 1, 0]} : Set (Fin 3 → ℕ)) =
        2 - 2 * X - 5 * X ^ 2 - X ^ 3 - (2 - X ^ 2) * s

Sources

• Toufik Mansour, Inversion Sequences Avoiding a Set of Length-3 Patterns, INTEGERS 24 (2024), Article A76, Theorem 21.

Uses 1

Statement usesGenerating function of inversion sequences avoiding a set of patterns

TheoremInversion sequences avoiding nine patterns#●ready to prove

Let \(B = \{000, 010, 100, 101, 102, 110, 120, 201, 210\}\), where a pattern is written as a digit string (\(101\) is the triple \((1, 0, 1)\)), and let \(F_B(x) = \sum_{n \ge 1} |I_n(B)| x^n \in \mathbb{Q}[[x]]\) be the generating function of the inversion sequences avoiding every pattern in \(B\). For every power series \(s \in \mathbb{Q}[[x]]\) with constant term \(1\) and \(s^2 = 1 - 2x - 3x^2\),

\[2x^2(1 + x) F_B(x) = 2 - 3x - 3x^2 + (x - 2) s.\]

This is the closed form \(F_B(x) = (2 - 3x - 3x^2 + (x - 2)\sqrt{1 - 2x - 3x^2}) / (2x^2(1 + x))\) with the denominator cleared, \(s\) standing for \(\sqrt{1 - 2x - 3x^2}\).

public theorem_wanted invSeqAvoidGF_nine_patterns :
    ∀ s : ℚ⟦X⟧, constantCoeff s = 1 → s ^ 2 = 1 - 2 * X - 3 * X ^ 2 →
      2 * X ^ 2 * (1 + X) *
          invSeqAvoidGF ({![0, 0, 0], ![0, 1, 0], ![1, 0, 0], ![1, 0, 1], ![1, 0, 2], ![1, 1, 0],
            ![1, 2, 0], ![2, 0, 1], ![2, 1, 0]} : Set (Fin 3 → ℕ)) =
        2 - 3 * X - 3 * X ^ 2 + (X - 2) * s

Sources

• Toufik Mansour, Inversion Sequences Avoiding a Set of Length-3 Patterns, INTEGERS 24 (2024), Article A76, Theorem 22.

Uses 1

Statement usesGenerating function of inversion sequences avoiding a set of patterns

TheoremNumber of I-Wilf classes of sets of length-3 patterns#●ready to prove

Let \(P\) be the set of the thirteen length-3 patterns \(000, 001, 010, 011, 012, 021, 100, 101, 102, 110, 120, 201, 210\), each written as the word of its values. For \(B \subseteq P\) let \(|I_n(B)|\) be the number of inversion sequences of length \(n\) that avoid every pattern in \(B\), and let \(w_d\) be the number of distinct sequences \((|I_n(B)|)_{n \ge 0}\) as \(B\) ranges over the \(d\)-element subsets of \(P\) (the number of I-Wilf-equivalence classes of such sets). Then \(w_5 = 219\), \(w_6 = 167\), \(w_7 = 105\), \(w_8 = 61\), \(w_9 = 35\), \(w_{10} = 21\), \(w_{11} = 10\), \(w_{12} = 4\) and \(w_{13} = 1\).

public theorem_wanted invSeq_wilfClassCount :
    let P : Finset (Fin 3 → ℕ) := {![0, 0, 0], ![0, 0, 1], ![0, 1, 0], ![0, 1, 1], ![0, 1, 2],
      ![0, 2, 1], ![1, 0, 0], ![1, 0, 1], ![1, 0, 2], ![1, 1, 0], ![1, 2, 0], ![2, 0, 1],
      ![2, 1, 0]}
    let w : ℕ → ℕ := fun d =>
      Nat.card ↥((fun B : Finset (Fin 3 → ℕ) => invSeqAvoidCount (B : Set (Fin 3 → ℕ))) ''
        (P.powersetCard d : Set (Finset (Fin 3 → ℕ))))
    w 5 = 219 ∧ w 6 = 167 ∧ w 7 = 105 ∧ w 8 = 61 ∧ w 9 = 35 ∧ w 10 = 21 ∧ w 11 = 10 ∧
      w 12 = 4 ∧ w 13 = 1

Sources

• Toufik Mansour, Inversion Sequences Avoiding a Set of Length-3 Patterns, INTEGERS 24 (2024), Article A76, Theorem 1.

Uses 1

Statement usesNumber of inversion sequences avoiding a set of patterns

TheoremReducible sets of length-3 patterns for inversion sequences#●ready to prove

An inversion sequence of length \(n\) is a sequence \(e_0 e_1 \cdots e_{n-1}\) of natural numbers with \(e_i \le i\) for all \(i\); write a length-3 pattern as a digit string (\(101\) is the pattern \((1, 0, 1)\)). For each pair \((C, \tau)\) listed below and every \(n\), every inversion sequence of length \(n\) that avoids every pattern in \(C\) also avoids \(\tau\), so \(C \cup \{\tau\}\) and \(C\) are avoided by the same inversion sequences. The pairs are: \(C = \{001\}\) with \(\tau \in \{101, 102, 201\}\); \(C = \{011\}\) with \(\tau \in \{101, 110\}\); \(C = \{012\}\) with \(\tau \in \{102, 120\}\); \(C = \{021\}\) with \(\tau \in \{201, 210\}\); \(C = \{000, 001\}\) with \(\tau = 100\); \(C = \{000, 011\}\) with \(\tau \in \{100, 201, 210\}\); \(C = \{000, 012\}\) with \(\tau \in \{201, 210\}\); \(C = \{000, 021\}\) with \(\tau = 100\); \(C = \{001, 010\}\) with \(\tau \in \{021, 100, 110, 120, 210\}\); \(C = \{001, 011\}\) with \(\tau = 021\); \(C = \{001, 012\}\) with \(\tau = 021\); \(C = \{001, 110\}\) with \(\tau = 210\); \(C = \{001, 120\}\) with \(\tau = 210\); \(C = \{010, 011\}\) with \(\tau = 100\); \(C = \{010, 012\}\) with \(\tau \in \{101, 201\}\); \(C = \{010, 021\}\) with \(\tau \in \{100, 101, 102, 110, 120\}\); \(C = \{001, 011, 012\}\) with \(\tau = 210\); \(C = \{001, 011, 100\}\) with \(\tau = 210\); and \(C = \{001, 012, 100\}\) with \(\tau = 210\).

MetaMathlibExt.invSeq_reducible_pattern_sets · 40 lines

public theorem_wanted invSeq_reducible_pattern_sets :
    ∀ Cτ ∈ ([(({![0, 0, 1]} : Set (Fin 3 → ℕ)), ![1, 0, 1]),
        (({![0, 0, 1]} : Set (Fin 3 → ℕ)), ![1, 0, 2]),
        (({![0, 0, 1]} : Set (Fin 3 → ℕ)), ![2, 0, 1]),
        (({![0, 1, 1]} : Set (Fin 3 → ℕ)), ![1, 0, 1]),
        (({![0, 1, 1]} : Set (Fin 3 → ℕ)), ![1, 1, 0]),
        (({![0, 1, 2]} : Set (Fin 3 → ℕ)), ![1, 0, 2]),
        (({![0, 1, 2]} : Set (Fin 3 → ℕ)), ![1, 2, 0]),
        (({![0, 2, 1]} : Set (Fin 3 → ℕ)), ![2, 0, 1]),
        (({![0, 2, 1]} : Set (Fin 3 → ℕ)), ![2, 1, 0]),
        (({![0, 0, 0], ![0, 0, 1]} : Set (Fin 3 → ℕ)), ![1, 0, 0]),
        (({![0, 0, 0], ![0, 1, 1]} : Set (Fin 3 → ℕ)), ![1, 0, 0]),
        (({![0, 0, 0], ![0, 1, 1]} : Set (Fin 3 → ℕ)), ![2, 0, 1]),
        (({![0, 0, 0], ![0, 1, 1]} : Set (Fin 3 → ℕ)), ![2, 1, 0]),
        (({![0, 0, 0], ![0, 1, 2]} : Set (Fin 3 → ℕ)), ![2, 0, 1]),
        (({![0, 0, 0], ![0, 1, 2]} : Set (Fin 3 → ℕ)), ![2, 1, 0]),
        (({![0, 0, 0], ![0, 2, 1]} : Set (Fin 3 → ℕ)), ![1, 0, 0]),
        (({![0, 0, 1], ![0, 1, 0]} : Set (Fin 3 → ℕ)), ![0, 2, 1]),
        (({![0, 0, 1], ![0, 1, 0]} : Set (Fin 3 → ℕ)), ![1, 0, 0]),
        (({![0, 0, 1], ![0, 1, 0]} : Set (Fin 3 → ℕ)), ![1, 1, 0]),
        (({![0, 0, 1], ![0, 1, 0]} : Set (Fin 3 → ℕ)), ![1, 2, 0]),
        (({![0, 0, 1], ![0, 1, 0]} : Set (Fin 3 → ℕ)), ![2, 1, 0]),
        (({![0, 0, 1], ![0, 1, 1]} : Set (Fin 3 → ℕ)), ![0, 2, 1]),
        (({![0, 0, 1], ![0, 1, 2]} : Set (Fin 3 → ℕ)), ![0, 2, 1]),
        (({![0, 0, 1], ![1, 1, 0]} : Set (Fin 3 → ℕ)), ![2, 1, 0]),
        (({![0, 0, 1], ![1, 2, 0]} : Set (Fin 3 → ℕ)), ![2, 1, 0]),
        (({![0, 1, 0], ![0, 1, 1]} : Set (Fin 3 → ℕ)), ![1, 0, 0]),
        (({![0, 1, 0], ![0, 1, 2]} : Set (Fin 3 → ℕ)), ![1, 0, 1]),
        (({![0, 1, 0], ![0, 1, 2]} : Set (Fin 3 → ℕ)), ![2, 0, 1]),
        (({![0, 1, 0], ![0, 2, 1]} : Set (Fin 3 → ℕ)), ![1, 0, 0]),
        (({![0, 1, 0], ![0, 2, 1]} : Set (Fin 3 → ℕ)), ![1, 0, 1]),
        (({![0, 1, 0], ![0, 2, 1]} : Set (Fin 3 → ℕ)), ![1, 0, 2]),
        (({![0, 1, 0], ![0, 2, 1]} : Set (Fin 3 → ℕ)), ![1, 1, 0]),
        (({![0, 1, 0], ![0, 2, 1]} : Set (Fin 3 → ℕ)), ![1, 2, 0]),
        (({![0, 0, 1], ![0, 1, 1], ![0, 1, 2]} : Set (Fin 3 → ℕ)), ![2, 1, 0]),
        (({![0, 0, 1], ![0, 1, 1], ![1, 0, 0]} : Set (Fin 3 → ℕ)), ![2, 1, 0]),
        (({![0, 0, 1], ![0, 1, 2], ![1, 0, 0]} : Set (Fin 3 → ℕ)), ![2, 1, 0])]
      : List (Set (Fin 3 → ℕ) × (Fin 3 → ℕ))),
      ∀ (n : ℕ) (e : Fin n → ℕ), (∀ i, e i ≤ i) → (∀ p ∈ Cτ.1, ¬ InvSeqContainsPattern e p) →
        ¬ InvSeqContainsPattern e Cτ.2

Sources

• Toufik Mansour, Inversion Sequences Avoiding a Set of Length-3 Patterns, INTEGERS 24 (2024), Article A76, Theorem 2.

Uses 1

Statement usesContainment of a length-3 pattern

TheoremA Catalan generating function for two sets of five patterns#●ready to prove

Let \(B = \{010, 101, 102, 201, 210\}\) and \(B' = \{011, 101, 110, 201, 210\}\), where a pattern is written as a digit string (\(101\) is the triple \((1, 0, 1)\)). For a set \(A\) of patterns let \(F_A(x) = \sum_{n \ge 1} |I_n(A)| x^n \in \mathbb{Q}[[x]]\) be the generating function of the inversion sequences avoiding every pattern in \(A\), and let \(C(x) = \sum_{n \ge 0} C_n x^n\) be the generating function of the Catalan numbers \(C_n = \binom{2n}{n}/(n + 1)\). Then \(F_B = F_{B'}\) and

\[(1 - x)(2 - C(x)) F_B(x) = x.\]

Since \(C(x) = (1 - \sqrt{1 - 4x})/(2x)\) and \((1 - x)(2 - C(x))\) is a unit in \(\mathbb{Q}[[x]]\), this says \(F_B(x) = F_{B'}(x) = x / ((1 - x)(2 - (1 - \sqrt{1 - 4x})/(2x)))\).

public theorem_wanted invSeqAvoidGF_010_101_102_201_210_catalan :
    invSeqAvoidGF ({![0, 1, 0], ![1, 0, 1], ![1, 0, 2], ![2, 0, 1], ![2, 1, 0]} : Set (Fin 3 → ℕ)) =
        invSeqAvoidGF ({![0, 1, 1], ![1, 0, 1], ![1, 1, 0], ![2, 0, 1], ![2, 1, 0]}
            : Set (Fin 3 → ℕ)) ∧
      (1 - X) * (2 - PowerSeries.mk fun n => (catalan n : ℚ)) *
          invSeqAvoidGF ({![0, 1, 0], ![1, 0, 1], ![1, 0, 2], ![2, 0, 1], ![2, 1, 0]}
              : Set (Fin 3 → ℕ)) = X

Sources

• Toufik Mansour, Inversion Sequences Avoiding a Set of Length-3 Patterns, INTEGERS 24 (2024), Article A76, Theorem 3.

Uses 1

Statement usesGenerating function of inversion sequences avoiding a set of patterns

TheoremI-Wilf-equivalence of 101 and 110 alongside 102, 120, 210#●ready to prove

Write a length-3 pattern as the word of its values, so \(101\) is the pattern \((1, 0, 1)\), and for a set \(S\) of patterns let \(|I_n(S)|\) be the number of inversion sequences of length \(n\) that avoid every pattern in \(S\). Let \(B_\tau = \{100, \tau, 102, 120, 210\}\) and \(C_\tau = \{\tau, 102, 120, 201, 210\}\). Then for every \(n \ge 0\), \(|I_n(B_{101})| = |I_n(B_{110})|\) and \(|I_n(C_{101})| = |I_n(C_{110})|\).

The paper's Theorem 10 also claims \(|I_n(A_{101})| = |I_n(A_{110})|\) for all \(n\), where \(A_\tau = \{100, \tau, 102, 120, 201\}\); that claim is false, since for \(n = 6\) the two counts are \(206\) and \(205\).

public theorem_wanted invSeq_wilf_102_120_101_110_parts_B_C :
    invSeqAvoidCount ({![1, 0, 0], ![1, 0, 1], ![1, 0, 2], ![1, 2, 0], ![2, 1, 0]}
        : Set (Fin 3 → ℕ)) =
      invSeqAvoidCount ({![1, 0, 0], ![1, 1, 0], ![1, 0, 2], ![1, 2, 0], ![2, 1, 0]}
          : Set (Fin 3 → ℕ)) ∧
    invSeqAvoidCount ({![1, 0, 1], ![1, 0, 2], ![1, 2, 0], ![2, 0, 1], ![2, 1, 0]}
        : Set (Fin 3 → ℕ)) =
      invSeqAvoidCount ({![1, 1, 0], ![1, 0, 2], ![1, 2, 0], ![2, 0, 1], ![2, 1, 0]}
          : Set (Fin 3 → ℕ))

Sources

• Toufik Mansour, Inversion Sequences Avoiding a Set of Length-3 Patterns, INTEGERS 24 (2024), Article A76, Theorem 10.

Uses 1

Statement usesNumber of inversion sequences avoiding a set of patterns

TheoremI-Wilf-equivalence of 101 and 110 alongside 010, 120, 201, 210#●ready to prove

Write a length-3 pattern as the word of its values, so \(101\) is the pattern \((1, 0, 1)\), and for a set \(B\) of patterns let \(|I_n(B)|\) be the number of inversion sequences of length \(n\) that avoid every pattern in \(B\). For every \(n \ge 0\),

\[|I_n(\{010, 101, 120, 201, 210\})| = |I_n(\{010, 110, 120, 201, 210\})|.\]

The paper's Theorem 12 also claims this equality for \(\{100, 101, 120, 201, 210\}\) and \(\{100, 110, 120, 201, 210\}\); that claim is false, since for \(n = 5\) the two counts are \(79\) and \(81\).

public theorem_wanted invSeq_wilf_010_120_201_210_101_110 :
    invSeqAvoidCount ({![0, 1, 0], ![1, 0, 1], ![1, 2, 0], ![2, 0, 1], ![2, 1, 0]}
        : Set (Fin 3 → ℕ)) =
      invSeqAvoidCount ({![0, 1, 0], ![1, 1, 0], ![1, 2, 0], ![2, 0, 1], ![2, 1, 0]}
          : Set (Fin 3 → ℕ))

Sources

• Toufik Mansour, Inversion Sequences Avoiding a Set of Length-3 Patterns, INTEGERS 24 (2024), Article A76, Theorem 12.

Uses 1

Statement usesNumber of inversion sequences avoiding a set of patterns

TheoremExchanging \(201\) and \(210\) in \(\{010, 100, 101, 102, 120, 201\}\)#●ready to prove

Write length-3 patterns as digit strings (\(101\) is the pattern \((1, 0, 1)\)) and let \(|I_n(B)|\) be the number of inversion sequences of length \(n\) that avoid every pattern in the set \(B\). For a pattern \(\tau\) let \(A_\tau = \{010, 100, 101, 102, 120, \tau\}\). Then for every \(n \ge 0\), \(|I_n(A_{201})| = |I_n(A_{210})|\).

The source further claims \(|I_n(A_{210})| = |I_n(B)| = |I_n(C)|\) for all \(n\), with \(B = \{010, 100, 110, 102, 120, 201\}\) and \(C = \{010, 101, 110, 102, 120, 210\}\); these claims are false as printed (\(|I_7| = 538, 537, 539\) for \(A_{210}\), \(B\), \(C\)) and are omitted.

public theorem_wanted invSeq_wilf_010_100_101_102_120_201_210 :
    invSeqAvoidCount ({![0, 1, 0], ![1, 0, 0], ![1, 0, 1], ![1, 0, 2], ![1, 2, 0], ![2, 0, 1]}
        : Set (Fin 3 → ℕ)) =
      invSeqAvoidCount ({![0, 1, 0], ![1, 0, 0], ![1, 0, 1], ![1, 0, 2], ![1, 2, 0], ![2, 1, 0]}
          : Set (Fin 3 → ℕ))

Sources

• Toufik Mansour, Inversion Sequences Avoiding a Set of Length-3 Patterns, INTEGERS 24 (2024), Article A76, Theorem 15.

Uses 1

Statement usesNumber of inversion sequences avoiding a set of patterns

StructureLength-2 signed pattern#✓fully proved

A length-2 signed pattern is a word \(\tau_1\tau_2\) whose underlying word \(|\tau_1||\tau_2|\) is \(00\), \(01\) or \(10\) and each of whose letters may be barred, for example \(\bar10\) or \(0\bar1\). It is given by the comparison of \(|\tau_1|\) with \(|\tau_2|\) (equal for \(00\), less for \(01\), greater for \(10\)) together with whether \(\tau_1\) is barred and whether \(\tau_2\) is barred.

structure SignedPattern2 where
  /-- The comparison of `|τ₁|` with `|τ₂|`. -/
  ord : Ordering
  /-- Whether the first letter is barred. -/
  bar₁ : Bool
  /-- Whether the second letter is barred. -/
  bar₂ : Bool
deriving DecidableEq, Fintype

Sources

• Toufik Mansour and Amir Safadi, Signed Inversion Sequences Avoiding a Set of Length-2 Signed Patterns, INTEGERS 26 (2026), Article A74, Introduction.

Used by 51

Used byNumber of length-2 signed patterns · Coefficients of the avoidance generating function · Number of signed inversion sequences avoiding a set of patterns · Eight signed-pattern triples with (n + 1)! avoiders (Lemma 8) · Three six-pattern sets with 2 · n! avoiders (Theorem 17) · Signed inversion sequences of length one · Signed inversion sequences of length zero · Generating function of signed inversion sequences avoiding a set of patterns · Containment of a length-2 signed pattern · Wilf-equivalence and count for {0̄0̄, 0̄0, 01̄} (Lemma 2) · Mansour–Safadi Lemma 3 (signed patterns 0̄1̄, 0̄0̄, 01̄) · Mansour–Safadi Lemma 4 (signed patterns 0̄1̄, 0̄0̄, 0̄1) · Mansour–Safadi Theorem 3, class C2 (signed patterns 0̄0̄, 0̄0, 0̄1, 01) · Mansour–Safadi Lemma 1 (signed patterns 0̄1̄, 0̄0, 01) · Mansour–Safadi Theorem 3, class C16 (signed patterns 0̄1̄, 0̄0, 01̄, 01) · Mansour–Safadi Theorem 3, class C12 (signed patterns 0̄1̄, 0̄0̄, 01̄, 01) · Mansour–Safadi Theorem 3, class C4 (signed patterns 0̄1̄, 0̄0̄, 0̄0, 01̄) · Mansour–Safadi Theorem 3, class C3 (signed patterns 0̄1̄, 0̄0̄, 0̄1, 01̄) · Mansour–Safadi Theorem 3, class C15 (signed patterns 0̄1̄, 0̄0̄, 0̄1, 01) · Signed inversion sequences avoiding \(\{\bar1\bar0, \bar0\bar0, 0\bar1, 01\}\) · Mansour–Safadi Theorem 3, class C41 (signed patterns 1̄0̄, 0̄0̄, 01̄, 00) · Signed inversion sequences avoiding \(\{\bar1\bar0, \bar0\bar0, \bar00, 01\}\) · Signed inversion sequences avoiding \(\{\bar1\bar0, \bar0\bar1, 01\}\) · Signed inversion sequences avoiding \(\{\bar1\bar0, \bar0\bar1, 0\bar1, 01\}\) · Signed inversion sequences avoiding \(\{\bar1\bar0, \bar0\bar1, 0\bar1, 00\}\) · Signed inversion sequences avoiding \(\{\bar1\bar0, \bar0\bar1, \bar00, 01\}\) · Signed inversion sequences avoiding \(\{\bar1\bar0, \bar0\bar1, \bar00, 00\}\) · Signed inversion sequences avoiding \(\{\bar1\bar0, \bar0\bar1, \bar01, 00\}\) · Signed inversion sequences avoiding \(\{\bar1\bar0, \bar0\bar1, \bar01, 0\bar1\}\) · Signed inversion sequences avoiding \(\{\bar1\bar0, \bar0\bar1, \bar0\bar0, 00\}\) · Mansour–Safadi Theorem 3, class C21 · Mansour–Safadi Theorem 4 · Mansour–Safadi Theorem 6 · Mansour–Safadi Theorem 14 · Mansour–Safadi Lemma 7 · Mansour–Safadi Theorem 15 · Mansour–Safadi Lemma 10 · Mansour–Safadi Lemma 6 · Mansour–Safadi Theorem 3, class C45 · Mansour–Safadi Theorem 5 · Mansour–Safadi Theorem 12: four Wilf-equivalences of five-pattern sets · Mansour–Safadi Theorem 13: a Wilf-equivalence of five-pattern sets · Mansour–Safadi Theorem 8: two Wilf-equivalences of four-pattern sets · Mansour–Safadi Theorem 7: four Wilf-equivalent four-pattern sets · Mansour–Safadi Lemma 9: a Wilf-equivalence of three-pattern sets · Mansour–Safadi Theorem 9: a Wilf-equivalence of four-pattern sets · Mansour–Safadi Class 141 Wilf-equivalence · Mansour–Safadi Theorem 16: a Wilf-equivalence of six-pattern sets · Mansour–Safadi Theorem 18: a Wilf-equivalence of seven-pattern sets · Number of signed Wilf classes · The empty pattern set forms one signed Wilf class

TheoremNumber of length-2 signed patterns#✓fully proved

There are exactly twelve length-2 signed patterns.

theorem card_signedPattern2 : Fintype.card SignedPattern2 = 12

Sources

• Toufik Mansour and Amir Safadi, Signed Inversion Sequences Avoiding a Set of Length-2 Signed Patterns, INTEGERS 26 (2026), Article A74, Section 5 (binom 12 k sets of k patterns).

Uses 1

Statement usesLength-2 signed pattern

DefinitionContainment of a length-2 signed pattern#✓fully proved

Let \(e = e_1 \cdots e_n\) be a sequence whose entries are natural numbers \(|e_i|\), each barred or not, and let \(\tau_1\tau_2\) be a length-2 signed pattern. Then \(e\) contains \(\tau_1\tau_2\) if there are positions \(i < j\) such that \(|e_i|\) is equal to, smaller than or larger than \(|e_j|\) exactly as \(|\tau_1|\) is equal to, smaller than or larger than \(|\tau_2|\), and \(e_i\) and \(e_j\) are barred exactly when \(\tau_1\) and \(\tau_2\) are.

def SignedInvSeqContains {n : ℕ} (e : Fin n → ℕ × Bool) (p : SignedPattern2) : Prop :=
  ∃ i j : Fin n, i < j ∧ compare (e i).1 (e j).1 = p.ord ∧ (e i).2 = p.bar₁ ∧ (e j).2 = p.bar₂

Sources

• Toufik Mansour and Amir Safadi, Signed Inversion Sequences Avoiding a Set of Length-2 Signed Patterns, INTEGERS 26 (2026), Article A74, Introduction.

Uses 1 · Used by 3

Statement usesLength-2 signed pattern

Used byNumber of signed inversion sequences avoiding a set of patterns · Signed inversion sequences of length one · Signed inversion sequences of length zero

DefinitionNumber of signed inversion sequences avoiding a set of patterns#✓fully proved

A signed inversion sequence of length \(n\) is a word \(e_1 \cdots e_n\) in which each entry \(e_i\) is a natural number \(|e_i| \le i - 1\), either barred or not; that is, \(e_i \in \lbrace 0, \bar 0, 1, \bar 1, \dots, i - 1, \overline{i - 1} \rbrace\). For a finite set \(B\) of length-2 signed patterns and \(n \ge 0\), \(|\bar I_n(B)|\) is the number of signed inversion sequences of length \(n\) that contain no pattern of \(B\).

noncomputable def signedInvAvoidCount (B : Finset SignedPattern2) (n : ℕ) : ℕ :=
  Nat.card {e : Fin n → ℕ × Bool // (∀ i, (e i).1 ≤ i) ∧ ∀ p ∈ B, ¬ SignedInvSeqContains e p}

Sources

• Toufik Mansour and Amir Safadi, Signed Inversion Sequences Avoiding a Set of Length-2 Signed Patterns, INTEGERS 26 (2026), Article A74, Introduction.

Uses 2 · Used by 48

Statement usesContainment of a length-2 signed pattern · Length-2 signed pattern

Used byCoefficients of the avoidance generating function · Eight signed-pattern triples with (n + 1)! avoiders (Lemma 8) · Three six-pattern sets with 2 · n! avoiders (Theorem 17) · Signed inversion sequences of length one · Signed inversion sequences of length zero · Generating function of signed inversion sequences avoiding a set of patterns · Wilf-equivalence and count for {0̄0̄, 0̄0, 01̄} (Lemma 2) · Mansour–Safadi Lemma 3 (signed patterns 0̄1̄, 0̄0̄, 01̄) · Mansour–Safadi Lemma 4 (signed patterns 0̄1̄, 0̄0̄, 0̄1) · Mansour–Safadi Theorem 3, class C2 (signed patterns 0̄0̄, 0̄0, 0̄1, 01) · Mansour–Safadi Lemma 1 (signed patterns 0̄1̄, 0̄0, 01) · Mansour–Safadi Theorem 3, class C16 (signed patterns 0̄1̄, 0̄0, 01̄, 01) · Mansour–Safadi Theorem 3, class C12 (signed patterns 0̄1̄, 0̄0̄, 01̄, 01) · Mansour–Safadi Theorem 3, class C4 (signed patterns 0̄1̄, 0̄0̄, 0̄0, 01̄) · Mansour–Safadi Theorem 3, class C3 (signed patterns 0̄1̄, 0̄0̄, 0̄1, 01̄) · Mansour–Safadi Theorem 3, class C15 (signed patterns 0̄1̄, 0̄0̄, 0̄1, 01) · Signed inversion sequences avoiding \(\{\bar1\bar0, \bar0\bar0, 0\bar1, 01\}\) · Mansour–Safadi Theorem 3, class C41 (signed patterns 1̄0̄, 0̄0̄, 01̄, 00) · Signed inversion sequences avoiding \(\{\bar1\bar0, \bar0\bar0, \bar00, 01\}\) · Signed inversion sequences avoiding \(\{\bar1\bar0, \bar0\bar1, 01\}\) · Signed inversion sequences avoiding \(\{\bar1\bar0, \bar0\bar1, 0\bar1, 01\}\) · Signed inversion sequences avoiding \(\{\bar1\bar0, \bar0\bar1, 0\bar1, 00\}\) · Signed inversion sequences avoiding \(\{\bar1\bar0, \bar0\bar1, \bar00, 01\}\) · Signed inversion sequences avoiding \(\{\bar1\bar0, \bar0\bar1, \bar00, 00\}\) · Signed inversion sequences avoiding \(\{\bar1\bar0, \bar0\bar1, \bar01, 00\}\) · Signed inversion sequences avoiding \(\{\bar1\bar0, \bar0\bar1, \bar01, 0\bar1\}\) · Signed inversion sequences avoiding \(\{\bar1\bar0, \bar0\bar1, \bar0\bar0, 00\}\) · Mansour–Safadi Theorem 3, class C21 · Mansour–Safadi Theorem 4 · Mansour–Safadi Theorem 6 · Mansour–Safadi Theorem 14 · Mansour–Safadi Lemma 7 · Mansour–Safadi Theorem 15 · Mansour–Safadi Lemma 10 · Mansour–Safadi Lemma 6 · Mansour–Safadi Theorem 3, class C45 · Mansour–Safadi Theorem 5 · Mansour–Safadi Theorem 12: four Wilf-equivalences of five-pattern sets · Mansour–Safadi Theorem 13: a Wilf-equivalence of five-pattern sets · Mansour–Safadi Theorem 8: two Wilf-equivalences of four-pattern sets · Mansour–Safadi Theorem 7: four Wilf-equivalent four-pattern sets · Mansour–Safadi Lemma 9: a Wilf-equivalence of three-pattern sets · Mansour–Safadi Theorem 9: a Wilf-equivalence of four-pattern sets · Mansour–Safadi Class 141 Wilf-equivalence · Mansour–Safadi Theorem 16: a Wilf-equivalence of six-pattern sets · Mansour–Safadi Theorem 18: a Wilf-equivalence of seven-pattern sets · Number of signed Wilf classes · The empty pattern set forms one signed Wilf class

TheoremSigned inversion sequences of length zero#✓fully proved

The empty sequence is the only signed inversion sequence of length \(0\), and it contains no pattern, so for every finite set \(B\) of length-2 signed patterns the number \(|\bar I_0(B)|\) of signed inversion sequences of length \(0\) avoiding every pattern of \(B\) is \(1\).

theorem signedInvAvoidCount_zero (B : Finset SignedPattern2) : signedInvAvoidCount B 0 = 1

Sources

• Toufik Mansour and Amir Safadi, Signed Inversion Sequences Avoiding a Set of Length-2 Signed Patterns, INTEGERS 26 (2026), Article A74, Introduction.

Uses 3

Statement usesLength-2 signed pattern · Number of signed inversion sequences avoiding a set of patterns

Proof usesContainment of a length-2 signed pattern

TheoremSigned inversion sequences of length one#✓fully proved

The signed inversion sequences of length \(1\) are \(0\) and \(\bar 0\), and neither contains a length-2 signed pattern, so for every finite set \(B\) of length-2 signed patterns the number \(|\bar I_1(B)|\) of signed inversion sequences of length \(1\) avoiding every pattern of \(B\) is \(2\).

theorem signedInvAvoidCount_one (B : Finset SignedPattern2) : signedInvAvoidCount B 1 = 2

Sources

• Toufik Mansour and Amir Safadi, Signed Inversion Sequences Avoiding a Set of Length-2 Signed Patterns, INTEGERS 26 (2026), Article A74, Introduction.

Uses 3

Statement usesLength-2 signed pattern · Number of signed inversion sequences avoiding a set of patterns

Proof usesContainment of a length-2 signed pattern

DefinitionGenerating function of signed inversion sequences avoiding a set of patterns#✓fully proved

For a finite set \(B\) of length-2 signed patterns, \(F_B(x) = \sum_{n \ge 0} |\bar I_n(B)| x^n\) is the formal power series with rational coefficients whose coefficient of \(x^n\) is the number \(|\bar I_n(B)|\) of signed inversion sequences of length \(n\) avoiding every pattern of \(B\).

noncomputable def signedInvAvoidGF (B : Finset SignedPattern2) : ℚ⟦X⟧ :=
  PowerSeries.mk fun n => (signedInvAvoidCount B n : ℚ)

Sources

• Toufik Mansour and Amir Safadi, Signed Inversion Sequences Avoiding a Set of Length-2 Signed Patterns, INTEGERS 26 (2026), Article A74, Section 2.

Uses 2 · Used by 17

Statement usesLength-2 signed pattern · Number of signed inversion sequences avoiding a set of patterns

Used byCoefficients of the avoidance generating function · Mansour–Safadi Theorem 3, class C2 (signed patterns 0̄0̄, 0̄0, 0̄1, 01) · Mansour–Safadi Lemma 1 (signed patterns 0̄1̄, 0̄0, 01) · Mansour–Safadi Theorem 3, class C16 (signed patterns 0̄1̄, 0̄0, 01̄, 01) · Mansour–Safadi Theorem 3, class C12 (signed patterns 0̄1̄, 0̄0̄, 01̄, 01) · Mansour–Safadi Theorem 3, class C15 (signed patterns 0̄1̄, 0̄0̄, 0̄1, 01) · Signed inversion sequences avoiding \(\{\bar1\bar0, \bar0\bar0, 0\bar1, 01\}\) · Mansour–Safadi Theorem 3, class C41 (signed patterns 1̄0̄, 0̄0̄, 01̄, 00) · Signed inversion sequences avoiding \(\{\bar1\bar0, \bar0\bar0, \bar00, 01\}\) · Signed inversion sequences avoiding \(\{\bar1\bar0, \bar0\bar1, 01\}\) · Signed inversion sequences avoiding \(\{\bar1\bar0, \bar0\bar1, 0\bar1, 01\}\) · Signed inversion sequences avoiding \(\{\bar1\bar0, \bar0\bar1, 0\bar1, 00\}\) · Signed inversion sequences avoiding \(\{\bar1\bar0, \bar0\bar1, \bar00, 01\}\) · Signed inversion sequences avoiding \(\{\bar1\bar0, \bar0\bar1, \bar00, 00\}\) · Signed inversion sequences avoiding \(\{\bar1\bar0, \bar0\bar1, \bar01, 00\}\) · Signed inversion sequences avoiding \(\{\bar1\bar0, \bar0\bar1, \bar01, 0\bar1\}\) · Signed inversion sequences avoiding \(\{\bar1\bar0, \bar0\bar1, \bar0\bar0, 00\}\)

TheoremCoefficients of the avoidance generating function#✓fully proved

For a finite set \(B\) of length-2 signed patterns and \(m \ge 0\), let \(|\bar I_m(B)|\) be the number of signed inversion sequences of length \(m\) avoiding every pattern of \(B\), and let \(F_B(x) = \sum_{m \ge 0} |\bar I_m(B)| x^m\) be their generating function, a formal power series with rational coefficients. Then for every \(n \ge 0\) the coefficient of \(x^n\) in \(F_B(x)\) is \(|\bar I_n(B)|\), viewed as a rational number.

theorem coeff_signedInvAvoidGF (B : Finset SignedPattern2) (n : ℕ) :
    coeff n (signedInvAvoidGF B) = (signedInvAvoidCount B n : ℚ)

Sources

• Toufik Mansour and Amir Safadi, Signed Inversion Sequences Avoiding a Set of Length-2 Signed Patterns, INTEGERS 26 (2026), Article A74, Section 2.

Uses 3

Statement usesLength-2 signed pattern · Number of signed inversion sequences avoiding a set of patterns · Generating function of signed inversion sequences avoiding a set of patterns

DefinitionNumber of signed Wilf classes#✓fully proved

For \(k \ge 0\), \(\mathrm{sw}_k\) is the number of Wilf-equivalence classes among the sets of \(k\) length-2 signed patterns, that is, the number of distinct counting functions \(n \mapsto |\bar{I}_n(B)|\) (for \(n \ge 0\)) over all sets \(B\) of exactly \(k\) length-2 signed patterns, where \(|\bar{I}_n(B)|\) is the number of signed inversion sequences of length \(n\) avoiding every pattern of \(B\).

noncomputable def signedWilfClassCount (k : ℕ) : ℕ :=
  Set.ncard ((fun B => signedInvAvoidCount B) '' {B : Finset SignedPattern2 | B.card = k})

Sources

• Toufik Mansour and Amir Safadi, Signed Inversion Sequences Avoiding a Set of Length-2 Signed Patterns, INTEGERS 26 (2026), Article A74, Theorem 1.

Uses 2 · Used by 5

Statement usesLength-2 signed pattern · Number of signed inversion sequences avoiding a set of patterns

Used bySigned Wilf classes of sets of five to twelve patterns · Signed Wilf classes of sets of four patterns · Signed Wilf classes of sets of three patterns · Signed Wilf classes of sets of three to twelve patterns · The empty pattern set forms one signed Wilf class

TheoremThe empty pattern set forms one signed Wilf class#✓fully proved

The number \(\mathrm{sw}_0\) of Wilf-equivalence classes among the sets of \(0\) length-2 signed patterns is \(1\): the empty set is the only set of no patterns.

theorem signedWilfClassCount_zero : signedWilfClassCount 0 = 1

Sources

• Toufik Mansour and Amir Safadi, Signed Inversion Sequences Avoiding a Set of Length-2 Signed Patterns, INTEGERS 26 (2026), Article A74, Theorem 1 (definition of sw_k).

Uses 3

Statement usesNumber of signed Wilf classes

Proof usesLength-2 signed pattern · Number of signed inversion sequences avoiding a set of patterns

TheoremMansour–Safadi Lemma 1 (signed patterns 0̄1̄, 0̄0, 01)#●ready to prove

A signed inversion sequence of length \(n\) is a word \(e_1 \cdots e_n\) with \(e_k \in \{0, \bar 0, 1, \bar 1, \dots, k - 1, \overline{k - 1}\}\). It avoids a length-2 signed pattern \(\tau_1\tau_2\) (one of \(00\), \(01\), \(10\), each letter possibly barred) when no \(i < j\) have \(|e_i|\), \(|e_j|\) in the same order as \(|\tau_1|\), \(|\tau_2|\) with \(e_i\), \(e_j\) barred exactly when \(\tau_1\), \(\tau_2\) are. Write \(\bar I_n(B)\) for the set of signed inversion sequences of length \(n\) that avoid every pattern in \(B\), and \(F_B(x) = \sum_{n \ge 0} |\bar I_n(B)|\,x^n\) in \(\mathbb{Q}[[x]]\). Let \(B_1 = \{\bar 0\bar 1, \bar 0 0, 01\}\) and \(B_2 = \{\bar 0\bar 1, \bar 0 1, 01\}\). Then \(|\bar I_n(B_1)| = |\bar I_n(B_2)|\) for every \(n \ge 0\), and \((1 - 3x + x^2)\,F_{B_1}(x) = 1 - x\), that is, \(F_{B_1}(x) = (1 - x)/(1 - 3x + x^2)\).

public theorem_wanted signedInvSeq_wilf_and_gf_b0b1_b00_01 :
    signedInvAvoidCount {⟨.lt, true, true⟩, ⟨.eq, true, false⟩, ⟨.lt, false, false⟩} =
      signedInvAvoidCount {⟨.lt, true, true⟩, ⟨.lt, true, false⟩, ⟨.lt, false, false⟩} ∧
    (1 - 3 * X + X ^ 2) * signedInvAvoidGF {⟨.lt, true, true⟩, ⟨.eq, true, false⟩,
        ⟨.lt, false, false⟩} = 1 - X

Sources

• Toufik Mansour and Amir Safadi, Signed Inversion Sequences Avoiding a Set of Length-2 Signed Patterns, INTEGERS 26 (2026), Article A74, Lemma 1.

Uses 3

Statement usesLength-2 signed pattern · Number of signed inversion sequences avoiding a set of patterns · Generating function of signed inversion sequences avoiding a set of patterns

TheoremWilf-equivalence and count for {0̄0̄, 0̄0, 01̄} (Lemma 2)#●ready to prove

Write a length-2 signed pattern as \(\tau_1\tau_2\), where \(00\), \(01\) and \(10\) record whether \(|\tau_1|\) is equal to, smaller than or larger than \(|\tau_2|\) and a bar marks a barred letter, and write \(|\bar I_n(B)|\) for the number of signed inversion sequences of length \(n\) avoiding every pattern of a set \(B\) of such patterns. Let \(B = \lbrace \bar 0\bar 0, \bar 0 0, 0\bar 1 \rbrace\) and \(C = \lbrace \bar 0 0, \bar 0 1, 0\bar 1 \rbrace\). Then \(B\) and \(C\) are Wilf-equivalent, that is, \(|\bar I_n(B)| = |\bar I_n(C)|\) for every \(n \ge 0\), and for every \(n \ge 0\),

\[ |\bar I_n(B)| = 1 + \sum_{j=0}^{n-1} (2j + 1)\, j!. \]

public theorem_wanted signedInvSeq_wilf_and_count_b0b0_b00_0b1 :
    signedInvAvoidCount {⟨.eq, true, true⟩, ⟨.eq, true, false⟩, ⟨.lt, false, true⟩} =
      signedInvAvoidCount {⟨.eq, true, false⟩, ⟨.lt, true, false⟩, ⟨.lt, false, true⟩} ∧
    ∀ n, signedInvAvoidCount {⟨.eq, true, true⟩, ⟨.eq, true, false⟩, ⟨.lt, false, true⟩} n =
        1 + ∑ j ∈ Finset.range n, (2 * j + 1) * j !

Sources

• Toufik Mansour and Amir Safadi, Signed Inversion Sequences Avoiding a Set of Length-2 Signed Patterns, INTEGERS 26 (2026), Article A74, Lemma 2.

Uses 2

Statement usesLength-2 signed pattern · Number of signed inversion sequences avoiding a set of patterns

TheoremMansour–Safadi Lemma 3 (signed patterns 0̄1̄, 0̄0̄, 01̄)#●ready to prove

A signed inversion sequence of length \(n\) is a word \(e_1 \cdots e_n\) with \(e_k \in \{0, \bar 0, 1, \bar 1, \dots, k - 1, \overline{k - 1}\}\). It avoids a length-2 signed pattern \(\tau_1\tau_2\) (one of \(00\), \(01\), \(10\), each letter possibly barred) when no \(i < j\) have \(|e_i|\), \(|e_j|\) in the same order as \(|\tau_1|\), \(|\tau_2|\) with \(e_i\), \(e_j\) barred exactly when \(\tau_1\), \(\tau_2\) are. Write \(\bar I_n(B)\) for the set of signed inversion sequences of length \(n\) that avoid every pattern in \(B\). Let \(B_1 = \{\bar 0\bar 1, \bar 0\bar 0, 0\bar 1\}\), \(B_2 = \{\bar 0\bar 1, \bar 0 0, 0\bar 1\}\) and \(B_3 = \{\bar 0\bar 1, 0\bar 1, 0\bar 0\}\). For every \(n \ge 0\), \(|\bar I_n(B_1)| = |\bar I_n(B_2)| = |\bar I_n(B_3)| = n!\,(1 + H_n)\), where \(H_n = \sum_{k=1}^{n} 1/k\) is the \(n\)th harmonic number.

public theorem_wanted signedInvSeq_wilf_and_count_b0b1_b0b0_0b1 :
    signedInvAvoidCount {⟨.lt, true, true⟩, ⟨.eq, true, true⟩, ⟨.lt, false, true⟩} =
      signedInvAvoidCount {⟨.lt, true, true⟩, ⟨.eq, true, false⟩, ⟨.lt, false, true⟩} ∧
    signedInvAvoidCount {⟨.lt, true, true⟩, ⟨.eq, true, false⟩, ⟨.lt, false, true⟩} =
      signedInvAvoidCount {⟨.lt, true, true⟩, ⟨.lt, false, true⟩, ⟨.eq, false, true⟩} ∧
    ∀ n, (signedInvAvoidCount {⟨.lt, true, true⟩, ⟨.eq, true, true⟩, ⟨.lt, false, true⟩} n : ℚ) =
        n ! * (1 + harmonic n)

Sources

• Toufik Mansour and Amir Safadi, Signed Inversion Sequences Avoiding a Set of Length-2 Signed Patterns, INTEGERS 26 (2026), Article A74, Lemma 3.

Uses 2

Statement usesLength-2 signed pattern · Number of signed inversion sequences avoiding a set of patterns

TheoremMansour–Safadi Lemma 4 (signed patterns 0̄1̄, 0̄0̄, 0̄1)#●ready to prove

A signed inversion sequence of length \(n\) is a word \(e_1 \cdots e_n\) with \(e_k \in \{0, \bar 0, 1, \bar 1, \dots, k - 1, \overline{k - 1}\}\). It avoids a length-2 signed pattern \(\tau_1\tau_2\) (one of \(00\), \(01\), \(10\), each letter possibly barred) when no \(i < j\) have \(|e_i|\), \(|e_j|\) in the same order as \(|\tau_1|\), \(|\tau_2|\) with \(e_i\), \(e_j\) barred exactly when \(\tau_1\), \(\tau_2\) are. Write \(\bar I_n(B)\) for the set of signed inversion sequences of length \(n\) that avoid every pattern in \(B\). For every \(n \ge 0\), \(|\bar I_n(\{\bar 0\bar 1, \bar 0\bar 0, \bar 0 1\})| = |\bar I_n(\{\bar 0\bar 1, \bar 0 0, \bar 0 1\})| = \sum_{j=0}^{n} j!\,(j + 1)^{n - j}\).

public theorem_wanted signedInvSeq_wilf_and_count_b0b1_b0b0_b01 :
    signedInvAvoidCount {⟨.lt, true, true⟩, ⟨.eq, true, true⟩, ⟨.lt, true, false⟩} =
      signedInvAvoidCount {⟨.lt, true, true⟩, ⟨.eq, true, false⟩, ⟨.lt, true, false⟩} ∧
    ∀ n, signedInvAvoidCount {⟨.lt, true, true⟩, ⟨.eq, true, true⟩, ⟨.lt, true, false⟩} n =
        ∑ j ∈ Finset.range (n + 1), j ! * (j + 1) ^ (n - j)

Sources

• Toufik Mansour and Amir Safadi, Signed Inversion Sequences Avoiding a Set of Length-2 Signed Patterns, INTEGERS 26 (2026), Article A74, Lemma 4.

Uses 2

Statement usesLength-2 signed pattern · Number of signed inversion sequences avoiding a set of patterns

TheoremSigned inversion sequences avoiding \(\{\bar1\bar0, \bar0\bar1, 01\}\)#●ready to prove

For a set \(B\) of length-2 signed patterns (a bar marks a barred letter), let \(|\bar I_n(B)|\) be the number of signed inversion sequences of length \(n\) avoiding every pattern of \(B\), and let \(F_B(x) = \sum_{n \ge 0} |\bar I_n(B)| x^n \in \mathbb{Q}[[x]]\). Let \(B = \{\bar1\bar0, \bar0\bar1, 01\}\) and \(C = \{\bar10, \bar0\bar1, 01\}\). Then \(|\bar I_n(B)| = |\bar I_n(C)|\) for every \(n \ge 0\), and

\[ (1 - 2x)(1 - 3x + x^2)(1 - x)^2 F_B(x) = (1 - 2x)(1 - 3x + x^2)(1 - x)^2 + x(1 - x)^4 + x(1 - x + x^2)(1 - 3x + x^2), \]

that is, \(F_B(x) = 1 + \frac{x(1 - x)^2}{(1 - 2x)(1 - 3x + x^2)} + \frac{x(1 - x + x^2)}{(1 - 2x)(1 - x)^2}\).

public theorem_wanted signedInvSeq_wilf_and_gf_b1b0_b0b1_01 :
    signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.lt, true, true⟩, ⟨.lt, false, false⟩} =
      signedInvAvoidCount {⟨.gt, true, false⟩, ⟨.lt, true, true⟩, ⟨.lt, false, false⟩} ∧
    (1 - 2 * X) * (1 - 3 * X + X ^ 2) * (1 - X) ^ 2 * signedInvAvoidGF {⟨.gt, true, true⟩,
        ⟨.lt, true, true⟩, ⟨.lt, false, false⟩} =
      (1 - 2 * X) * (1 - 3 * X + X ^ 2) * (1 - X) ^ 2 + X * (1 - X) ^ 4 +
        X * (1 - X + X ^ 2) * (1 - 3 * X + X ^ 2)

Sources

• Toufik Mansour and Amir Safadi, Signed Inversion Sequences Avoiding a Set of Length-2 Signed Patterns, INTEGERS 26 (2026), Article A74, Lemma 5.

Uses 3

Statement usesLength-2 signed pattern · Number of signed inversion sequences avoiding a set of patterns · Generating function of signed inversion sequences avoiding a set of patterns

TheoremMansour–Safadi Lemma 6#●ready to prove

Write \(\bar{I}_n(B)\) for the set of signed inversion sequences of length \(n\) that avoid every length-2 signed pattern in \(B\), where a pattern is one of \(00\), \(01\), \(10\) with a bar over each barred letter. Then for every \(n \ge 0\), \(|\bar{I}_n(\{\bar{1}\bar{0}, \bar{0}\bar{0}, \bar{0}1\})| = |\bar{I}_n(\{\bar{1}\bar{0}, \bar{0}0, \bar{0}1\})|\).

public theorem_wanted signedInvSeq_wilf_b1b0_b0b0_b01 :
    signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.eq, true, true⟩, ⟨.lt, true, false⟩} =
      signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.eq, true, false⟩, ⟨.lt, true, false⟩}

Sources

• Toufik Mansour and Amir Safadi, Signed Inversion Sequences Avoiding a Set of Length-2 Signed Patterns, INTEGERS 26 (2026), Article A74, Lemma 6.

Uses 2

Statement usesLength-2 signed pattern · Number of signed inversion sequences avoiding a set of patterns

TheoremMansour–Safadi Lemma 7#●ready to prove

Write \(\bar{I}_n(B)\) for the set of signed inversion sequences of length \(n\) that avoid every length-2 signed pattern in \(B\), where a pattern is one of \(00\), \(01\), \(10\) with a bar over each barred letter. Then for every \(n \ge 0\), \(|\bar{I}_n(\{\bar{1}0, \bar{0}\bar{1}, \bar{0}\bar{0}\})| = |\bar{I}_n(\{\bar{1}0, \bar{0}\bar{1}, \bar{0}0\})|\).

public theorem_wanted signedInvSeq_wilf_b10_b0b1_b0b0 :
    signedInvAvoidCount {⟨.gt, true, false⟩, ⟨.lt, true, true⟩, ⟨.eq, true, true⟩} =
      signedInvAvoidCount {⟨.gt, true, false⟩, ⟨.lt, true, true⟩, ⟨.eq, true, false⟩}

Sources

• Toufik Mansour and Amir Safadi, Signed Inversion Sequences Avoiding a Set of Length-2 Signed Patterns, INTEGERS 26 (2026), Article A74, Lemma 7.

Uses 2

Statement usesLength-2 signed pattern · Number of signed inversion sequences avoiding a set of patterns

TheoremEight signed-pattern triples with (n + 1)! avoiders (Lemma 8)#●ready to prove

Write a length-2 signed pattern as \(\tau_1\tau_2\), where \(00\), \(01\) and \(10\) record whether \(|\tau_1|\) is equal to, smaller than or larger than \(|\tau_2|\) and a bar marks a barred letter, and write \(|\bar I_n(B)|\) for the number of signed inversion sequences of length \(n\) avoiding every pattern of a set \(B\) of such patterns. For every \(n \ge 0\) and each of the eight sets \(B = \lbrace \bar 1\bar 0, \bar 0\bar 1, \bar 0\bar 0 \rbrace\), \(\lbrace \bar 1\bar 0, \bar 0\bar 1, \bar 0 0 \rbrace\), \(\lbrace \bar 1\bar 0, \bar 0\bar 1, 0\bar 1 \rbrace\), \(\lbrace \bar 1 0, \bar 0\bar 1, 0\bar 1 \rbrace\), \(\lbrace \bar 1 0, \bar 0 0, \bar 0 1 \rbrace\), \(\lbrace \bar 1\bar 0, \bar 0\bar 1, 0\bar 0 \rbrace\), \(\lbrace \bar 1 0, \bar 0 0, 0\bar 1 \rbrace\) and \(\lbrace \bar 1 0, 0\bar 0, 0\bar 1 \rbrace\), we have \(|\bar I_n(B)| = (n+1)!\).

The source prints an unbarred \(I_n\) in parts (iii) and (iv); it is read as \(\bar I_n\).

public theorem_wanted signedInvAvoidCount_eq_factorial_succ :
    ∀ n,
    signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.lt, true, true⟩, ⟨.eq, true, true⟩} n = (n + 1)! ∧
    signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.lt, true, true⟩, ⟨.eq, true, false⟩} n = (n + 1)! ∧
    signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.lt, true, true⟩, ⟨.lt, false, true⟩} n = (n + 1)! ∧
    signedInvAvoidCount {⟨.gt, true, false⟩, ⟨.lt, true, true⟩, ⟨.lt, false, true⟩} n = (n + 1)! ∧
    signedInvAvoidCount {⟨.gt, true, false⟩, ⟨.eq, true, false⟩, ⟨.lt, true, false⟩} n = (n + 1)! ∧
    signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.lt, true, true⟩, ⟨.eq, false, true⟩} n = (n + 1)! ∧
    signedInvAvoidCount {⟨.gt, true, false⟩, ⟨.eq, true, false⟩, ⟨.lt, false, true⟩} n = (n + 1)! ∧
    signedInvAvoidCount {⟨.gt, true, false⟩, ⟨.eq, false, true⟩, ⟨.lt, false, true⟩} n = (n + 1)!

Sources

• Toufik Mansour and Amir Safadi, Signed Inversion Sequences Avoiding a Set of Length-2 Signed Patterns, INTEGERS 26 (2026), Article A74, Lemma 8.

Uses 2

Statement usesLength-2 signed pattern · Number of signed inversion sequences avoiding a set of patterns

TheoremMansour–Safadi Lemma 9: a Wilf-equivalence of three-pattern sets#●ready to prove

Length-2 signed patterns are written as in the paper, a bar marking a barred letter, and \(B \sim C\) means that for every \(n \ge 0\) the number \(|\bar I_n(B)|\) of signed inversion sequences of length \(n\) avoiding every pattern of \(B\) equals \(|\bar I_n(C)|\). Then \(\{\bar1\bar0, \bar10, \bar0\bar0\} \sim \{\bar1\bar0, \bar10, \bar00\}\).

public theorem_wanted signedInvSeq_wilf_b1b0_b10_b0b0 :
    signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.gt, true, false⟩, ⟨.eq, true, true⟩} =
      signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.gt, true, false⟩, ⟨.eq, true, false⟩}

Sources

• Toufik Mansour and Amir Safadi, Signed Inversion Sequences Avoiding a Set of Length-2 Signed Patterns, INTEGERS 26 (2026), Article A74, Lemma 9.

Uses 2

Statement usesLength-2 signed pattern · Number of signed inversion sequences avoiding a set of patterns

TheoremMansour–Safadi Lemma 10#●ready to prove

Write \(\bar{I}_n(B)\) for the set of signed inversion sequences of length \(n\) that avoid every length-2 signed pattern in \(B\), where a pattern is one of \(00\), \(01\), \(10\) with a bar over each barred letter. Then for every \(n \ge 0\), \(|\bar{I}_n(\{\bar{1}\bar{0}, \bar{0}\bar{0}, 1\bar{0}\})| = |\bar{I}_n(\{\bar{1}\bar{0}, 0\bar{0}, 1\bar{0}\})|\).

public theorem_wanted signedInvSeq_wilf_b1b0_b0b0_1b0 :
    signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.eq, true, true⟩, ⟨.gt, false, true⟩} =
      signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.eq, false, true⟩, ⟨.gt, false, true⟩}

Sources

• Toufik Mansour and Amir Safadi, Signed Inversion Sequences Avoiding a Set of Length-2 Signed Patterns, INTEGERS 26 (2026), Article A74, Lemma 10.

Uses 2

Statement usesLength-2 signed pattern · Number of signed inversion sequences avoiding a set of patterns

TheoremSigned Wilf classes of sets of three to twelve patterns#●ready to prove

Let \(\mathrm{sw}_k\) be the number of Wilf-equivalence classes among the sets of \(k\) length-2 signed patterns. Then \(\mathrm{sw}_3 = 93\), \(\mathrm{sw}_4 = 195\), \(239 \le \mathrm{sw}_5 \le 240\), \(\mathrm{sw}_6 = 190\), \(\mathrm{sw}_7 = 107\), \(\mathrm{sw}_8 = 49\), \(\mathrm{sw}_9 = 22\), \(\mathrm{sw}_{10} = 8\), \(\mathrm{sw}_{11} = 3\) and \(\mathrm{sw}_{12} = 1\).

public theorem_wanted signedWilfClassCount_three_to_twelve :
    signedWilfClassCount 3 = 93 ∧ signedWilfClassCount 4 = 195 ∧
    239 ≤ signedWilfClassCount 5 ∧ signedWilfClassCount 5 ≤ 240 ∧
    signedWilfClassCount 6 = 190 ∧ signedWilfClassCount 7 = 107 ∧ signedWilfClassCount 8 = 49 ∧
    signedWilfClassCount 9 = 22 ∧ signedWilfClassCount 10 = 8 ∧ signedWilfClassCount 11 = 3 ∧
    signedWilfClassCount 12 = 1

Sources

• Toufik Mansour and Amir Safadi, Signed Inversion Sequences Avoiding a Set of Length-2 Signed Patterns, INTEGERS 26 (2026), Article A74, Theorem 1.

Uses 1

Statement usesNumber of signed Wilf classes

TheoremMansour–Safadi Class 141 Wilf-equivalence#●ready to prove

Length-2 signed patterns are written as in the paper, a bar marking a barred letter, and \(B \sim C\) means that for every \(n \ge 0\) the number \(|\bar I_n(B)|\) of signed inversion sequences of length \(n\) avoiding every pattern of \(B\) equals \(|\bar I_n(C)|\). Then \(\{\bar1\bar0, \bar10, \bar0\bar0, \bar00, 00\} \sim \{\bar1\bar0, \bar10, \bar0\bar1, 0\bar1, 00\}\).

The paper leaves this equivalence (Class 141 of its Table 6) open; it is what remains to be shown for the number of Wilf classes of five-pattern sets to be exactly \(239\).

public theorem_wanted signedInvSeq_wilf_b1b0_b10_b0b0_b00_00 :
    signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.gt, true, false⟩, ⟨.eq, true, true⟩,
        ⟨.eq, true, false⟩, ⟨.eq, false, false⟩} =
      signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.gt, true, false⟩, ⟨.lt, true, true⟩,
          ⟨.lt, false, true⟩, ⟨.eq, false, false⟩}

Sources

• Toufik Mansour and Amir Safadi, Signed Inversion Sequences Avoiding a Set of Length-2 Signed Patterns, INTEGERS 26 (2026), Article A74, Theorem 1, closing remark.

Uses 2

Statement usesLength-2 signed pattern · Number of signed inversion sequences avoiding a set of patterns

TheoremSigned Wilf classes of sets of three patterns#●ready to prove

The number \(\mathrm{sw}_3\) of Wilf-equivalence classes among the sets of \(3\) length-2 signed patterns is \(93\).

public theorem_wanted signedWilfClassCount_three :
    signedWilfClassCount 3 = 93

Sources

• Toufik Mansour and Amir Safadi, Signed Inversion Sequences Avoiding a Set of Length-2 Signed Patterns, INTEGERS 26 (2026), Article A74, Theorem 2.

Uses 1

Statement usesNumber of signed Wilf classes

TheoremSigned Wilf classes of sets of four patterns#●ready to prove

The number \(\mathrm{sw}_4\) of Wilf-equivalence classes among the sets of \(4\) length-2 signed patterns is \(195\).

public theorem_wanted signedWilfClassCount_four :
    signedWilfClassCount 4 = 195

Sources

• Toufik Mansour and Amir Safadi, Signed Inversion Sequences Avoiding a Set of Length-2 Signed Patterns, INTEGERS 26 (2026), Article A74, Theorem 10.

Uses 1

Statement usesNumber of signed Wilf classes

TheoremSigned Wilf classes of sets of five to twelve patterns#●ready to prove

Let \(\mathrm{sw}_k\) be the number of Wilf-equivalence classes among the sets of \(k\) length-2 signed patterns. Then \(239 \le \mathrm{sw}_5 \le 240\), \(\mathrm{sw}_6 = 190\), \(\mathrm{sw}_7 = 107\), \(\mathrm{sw}_8 = 49\), \(\mathrm{sw}_9 = 22\), \(\mathrm{sw}_{10} = 8\), \(\mathrm{sw}_{11} = 3\) and \(\mathrm{sw}_{12} = 1\).

public theorem_wanted signedWilfClassCount_five_to_twelve :
    239 ≤ signedWilfClassCount 5 ∧ signedWilfClassCount 5 ≤ 240 ∧
    signedWilfClassCount 6 = 190 ∧ signedWilfClassCount 7 = 107 ∧ signedWilfClassCount 8 = 49 ∧
    signedWilfClassCount 9 = 22 ∧ signedWilfClassCount 10 = 8 ∧ signedWilfClassCount 11 = 3 ∧
    signedWilfClassCount 12 = 1

Sources

• Toufik Mansour and Amir Safadi, Signed Inversion Sequences Avoiding a Set of Length-2 Signed Patterns, INTEGERS 26 (2026), Article A74, Theorem 11.

Uses 1

Statement usesNumber of signed Wilf classes

TheoremMansour–Safadi Theorem 3, class C2 (signed patterns 0̄0̄, 0̄0, 0̄1, 01)#●ready to prove

A signed inversion sequence of length \(n\) is a word \(e_1 \cdots e_n\) with \(e_k \in \{0, \bar 0, 1, \bar 1, \dots, k - 1, \overline{k - 1}\}\). It avoids a length-2 signed pattern \(\tau_1\tau_2\) (one of \(00\), \(01\), \(10\), each letter possibly barred) when no \(i < j\) have \(|e_i|\), \(|e_j|\) in the same order as \(|\tau_1|\), \(|\tau_2|\) with \(e_i\), \(e_j\) barred exactly when \(\tau_1\), \(\tau_2\) are. Write \(\bar I_n(B)\) for the set of signed inversion sequences of length \(n\) that avoid every pattern in \(B\), and \(F_B(x) = \sum_{n \ge 0} |\bar I_n(B)|\,x^n\) in \(\mathbb{Q}[[x]]\). Let \(B_1 = \{\bar 0\bar 0, \bar 0 0, \bar 0 1, 01\}\) and \(B_2 = \{\bar 0\bar 0, \bar 0 1, 0\bar 0, 01\}\). For every \(n \ge 0\), \(|\bar I_n(B_1)| = |\bar I_n(B_2)|\), and the coefficient of \(x^n\) in \(F_{B_1}(x)\) equals the coefficient of \(x^n\) in \(1 + 2\sum_{k=1}^{n} x^k \prod_{i=1}^{k} (1 - ix)^{-1}\).

Since the terms with \(k > n\) contribute nothing to \(x^n\), this says \(F_{B_1}(x) = 1 + 2\sum_{k \ge 1} x^k / \prod_{i=1}^{k} (1 - ix)\).

public theorem_wanted signedInvSeq_wilf_and_gf_b0b0_b00_b01_01 :
    signedInvAvoidCount {⟨.eq, true, true⟩, ⟨.eq, true, false⟩, ⟨.lt, true, false⟩,
        ⟨.lt, false, false⟩} =
      signedInvAvoidCount {⟨.eq, true, true⟩, ⟨.lt, true, false⟩, ⟨.eq, false, true⟩,
          ⟨.lt, false, false⟩} ∧
    ∀ n, coeff n (signedInvAvoidGF {⟨.eq, true, true⟩, ⟨.eq, true, false⟩, ⟨.lt, true, false⟩,
        ⟨.lt, false, false⟩}) =
      coeff n (1 + 2 * ∑ k ∈ Finset.Icc 1 n, X ^ k * ∏ i ∈ Finset.Icc 1 k, (1 - (i : ℚ⟦X⟧) * X)⁻¹)

Sources

• Toufik Mansour and Amir Safadi, Signed Inversion Sequences Avoiding a Set of Length-2 Signed Patterns, INTEGERS 26 (2026), Article A74, Theorem 3 (C2).

Uses 3

Statement usesLength-2 signed pattern · Number of signed inversion sequences avoiding a set of patterns · Generating function of signed inversion sequences avoiding a set of patterns

TheoremMansour–Safadi Theorem 3, class C3 (signed patterns 0̄1̄, 0̄0̄, 0̄1, 01̄)#●ready to prove

A signed inversion sequence of length \(n\) is a word \(e_1 \cdots e_n\) with \(e_k \in \{0, \bar 0, 1, \bar 1, \dots, k - 1, \overline{k - 1}\}\). It avoids a length-2 signed pattern \(\tau_1\tau_2\) (one of \(00\), \(01\), \(10\), each letter possibly barred) when no \(i < j\) have \(|e_i|\), \(|e_j|\) in the same order as \(|\tau_1|\), \(|\tau_2|\) with \(e_i\), \(e_j\) barred exactly when \(\tau_1\), \(\tau_2\) are. Write \(\bar I_n(B)\) for the set of signed inversion sequences of length \(n\) that avoid every pattern in \(B\). Let \(B_1 = \{\bar 0\bar 1, \bar 0\bar 0, \bar 0 1, 0\bar 1\}\), \(B_2 = \{\bar 0\bar 1, \bar 0 0, \bar 0 1, 0\bar 1\}\) and \(B_3 = \{\bar 0\bar 0, \bar 0 0, 0\bar 1, 0\bar 0\}\). For every \(n \ge 0\), \(|\bar I_n(B_1)| = |\bar I_n(B_2)| = |\bar I_n(B_3)| = \sum_{i=0}^{n} i!\).

public theorem_wanted signedInvSeq_wilf_and_gf_b0b1_b0b0_b01_0b1 :
    signedInvAvoidCount {⟨.lt, true, true⟩, ⟨.eq, true, true⟩, ⟨.lt, true, false⟩,
        ⟨.lt, false, true⟩} =
      signedInvAvoidCount {⟨.lt, true, true⟩, ⟨.eq, true, false⟩, ⟨.lt, true, false⟩,
          ⟨.lt, false, true⟩} ∧
    signedInvAvoidCount {⟨.lt, true, true⟩, ⟨.eq, true, false⟩, ⟨.lt, true, false⟩,
        ⟨.lt, false, true⟩} =
      signedInvAvoidCount {⟨.eq, true, true⟩, ⟨.eq, true, false⟩, ⟨.lt, false, true⟩,
          ⟨.eq, false, true⟩} ∧
    ∀ n, signedInvAvoidCount {⟨.lt, true, true⟩, ⟨.eq, true, true⟩, ⟨.lt, true, false⟩,
        ⟨.lt, false, true⟩} n =
      ∑ i ∈ Finset.range (n + 1), i !

Sources

• Toufik Mansour and Amir Safadi, Signed Inversion Sequences Avoiding a Set of Length-2 Signed Patterns, INTEGERS 26 (2026), Article A74, Theorem 3 (C3).

Uses 2

Statement usesLength-2 signed pattern · Number of signed inversion sequences avoiding a set of patterns

TheoremMansour–Safadi Theorem 3, class C4 (signed patterns 0̄1̄, 0̄0̄, 0̄0, 01̄)#●ready to prove

A signed inversion sequence of length \(n\) is a word \(e_1 \cdots e_n\) with \(e_k \in \{0, \bar 0, 1, \bar 1, \dots, k - 1, \overline{k - 1}\}\). It avoids a length-2 signed pattern \(\tau_1\tau_2\) (one of \(00\), \(01\), \(10\), each letter possibly barred) when no \(i < j\) have \(|e_i|\), \(|e_j|\) in the same order as \(|\tau_1|\), \(|\tau_2|\) with \(e_i\), \(e_j\) barred exactly when \(\tau_1\), \(\tau_2\) are. Write \(\bar I_n(B)\) for the set of signed inversion sequences of length \(n\) that avoid every pattern in \(B\). Let \(B_1 = \{\bar 0\bar 1, \bar 0\bar 0, \bar 0 0, 0\bar 1\}\), \(B_2 = \{\bar 0\bar 1, \bar 0\bar 0, 0\bar 1, 0\bar 0\}\), \(B_3 = \{\bar 0\bar 1, \bar 0 0, 0\bar 1, 0\bar 0\}\) and \(B_4 = \{\bar 0 0, \bar 0 1, 0\bar 1, 0\bar 0\}\). Then \(|\bar I_n(B_1)| = |\bar I_n(B_2)| = |\bar I_n(B_3)| = |\bar I_n(B_4)|\) for every \(n \ge 0\), and \(|\bar I_n(B_1)| = 2\,n!\) for every \(n \ge 1\).

Together with \(|\bar I_0(B)| = 1\), which holds for every \(B\), this says that \(\sum_{n \ge 0} |\bar I_n(B_1)|\,x^n = 1 + 2\sum_{k \ge 1} k!\,x^k\).

MetaMathlibExt.signedInvSeq_wilf_and_gf_b0b1_b0b0_b00_0b1 · 15 lines

public theorem_wanted signedInvSeq_wilf_and_gf_b0b1_b0b0_b00_0b1 :
    signedInvAvoidCount {⟨.lt, true, true⟩, ⟨.eq, true, true⟩, ⟨.eq, true, false⟩,
        ⟨.lt, false, true⟩} =
      signedInvAvoidCount {⟨.lt, true, true⟩, ⟨.eq, true, true⟩, ⟨.lt, false, true⟩,
          ⟨.eq, false, true⟩} ∧
    signedInvAvoidCount {⟨.lt, true, true⟩, ⟨.eq, true, true⟩, ⟨.lt, false, true⟩,
        ⟨.eq, false, true⟩} =
      signedInvAvoidCount {⟨.lt, true, true⟩, ⟨.eq, true, false⟩, ⟨.lt, false, true⟩,
          ⟨.eq, false, true⟩} ∧
    signedInvAvoidCount {⟨.lt, true, true⟩, ⟨.eq, true, false⟩, ⟨.lt, false, true⟩,
        ⟨.eq, false, true⟩} =
      signedInvAvoidCount {⟨.eq, true, false⟩, ⟨.lt, true, false⟩, ⟨.lt, false, true⟩,
          ⟨.eq, false, true⟩} ∧
    ∀ n, signedInvAvoidCount {⟨.lt, true, true⟩, ⟨.eq, true, true⟩, ⟨.eq, true, false⟩,
        ⟨.lt, false, true⟩} (n + 1) = 2 * (n + 1)!

Sources

• Toufik Mansour and Amir Safadi, Signed Inversion Sequences Avoiding a Set of Length-2 Signed Patterns, INTEGERS 26 (2026), Article A74, Theorem 3 (C4).

Uses 2

Statement usesLength-2 signed pattern · Number of signed inversion sequences avoiding a set of patterns

TheoremMansour–Safadi Theorem 3, class C12 (signed patterns 0̄1̄, 0̄0̄, 01̄, 01)#●ready to prove

A signed inversion sequence of length \(n\) is a word \(e_1 \cdots e_n\) with \(e_k \in \{0, \bar 0, 1, \bar 1, \dots, k - 1, \overline{k - 1}\}\). It avoids a length-2 signed pattern \(\tau_1\tau_2\) (one of \(00\), \(01\), \(10\), each letter possibly barred) when no \(i < j\) have \(|e_i|\), \(|e_j|\) in the same order as \(|\tau_1|\), \(|\tau_2|\) with \(e_i\), \(e_j\) barred exactly when \(\tau_1\), \(\tau_2\) are. Write \(\bar I_n(B)\) for the set of signed inversion sequences of length \(n\) that avoid every pattern in \(B\), and \(F_B(x) = \sum_{n \ge 0} |\bar I_n(B)|\,x^n\) in \(\mathbb{Q}[[x]]\). Let \(B_1 = \{\bar 0\bar 1, \bar 0\bar 0, 0\bar 1, 01\}\), \(B_2 = \{\bar 0\bar 1, \bar 0 1, 0\bar 1, 00\}\) and \(B_3 = \{\bar 0\bar 1, \bar 0 1, 0\bar 0, 00\}\). Then \(|\bar I_n(B_1)| = |\bar I_n(B_2)| = |\bar I_n(B_3)|\) for every \(n \ge 0\), and \((1 - x)^2\,F_{B_1}(x) = 1 + x^2\).

public theorem_wanted signedInvSeq_wilf_and_gf_b0b1_b0b0_0b1_01 :
    signedInvAvoidCount {⟨.lt, true, true⟩, ⟨.eq, true, true⟩, ⟨.lt, false, true⟩,
        ⟨.lt, false, false⟩} =
      signedInvAvoidCount {⟨.lt, true, true⟩, ⟨.lt, true, false⟩, ⟨.lt, false, true⟩,
          ⟨.eq, false, false⟩} ∧
    signedInvAvoidCount {⟨.lt, true, true⟩, ⟨.lt, true, false⟩, ⟨.lt, false, true⟩,
        ⟨.eq, false, false⟩} =
      signedInvAvoidCount {⟨.lt, true, true⟩, ⟨.lt, true, false⟩, ⟨.eq, false, true⟩,
          ⟨.eq, false, false⟩} ∧
    ((1 - X) ^ 2) * signedInvAvoidGF {⟨.lt, true, true⟩, ⟨.eq, true, true⟩, ⟨.lt, false, true⟩,
        ⟨.lt, false, false⟩} =
      1 + X ^ 2

Sources

• Toufik Mansour and Amir Safadi, Signed Inversion Sequences Avoiding a Set of Length-2 Signed Patterns, INTEGERS 26 (2026), Article A74, Theorem 3 (C12).

Uses 3

Statement usesLength-2 signed pattern · Number of signed inversion sequences avoiding a set of patterns · Generating function of signed inversion sequences avoiding a set of patterns

TheoremMansour–Safadi Theorem 3, class C15 (signed patterns 0̄1̄, 0̄0̄, 0̄1, 01)#●ready to prove

A signed inversion sequence of length \(n\) is a word \(e_1 \cdots e_n\) with \(e_k \in \{0, \bar 0, 1, \bar 1, \dots, k - 1, \overline{k - 1}\}\). It avoids a length-2 signed pattern \(\tau_1\tau_2\) (one of \(00\), \(01\), \(10\), each letter possibly barred) when no \(i < j\) have \(|e_i|\), \(|e_j|\) in the same order as \(|\tau_1|\), \(|\tau_2|\) with \(e_i\), \(e_j\) barred exactly when \(\tau_1\), \(\tau_2\) are. Write \(\bar I_n(B)\) for the set of signed inversion sequences of length \(n\) that avoid every pattern in \(B\), and \(F_B(x) = \sum_{n \ge 0} |\bar I_n(B)|\,x^n\) in \(\mathbb{Q}[[x]]\). Let \(B_1 = \{\bar 0\bar 1, \bar 0\bar 0, \bar 0 1, 01\}\), \(B_2 = \{\bar 0\bar 1, \bar 0 0, \bar 0 1, 00\}\), \(B_3 = \{\bar 0\bar 1, \bar 0\bar 0, 0\bar 1, 00\}\), \(B_4 = \{\bar 0\bar 1, \bar 0\bar 0, 0\bar 0, 00\}\), \(B_5 = \{\bar 0\bar 1, \bar 0 1, 0\bar 1, 01\}\), \(B_6 = \{\bar 0\bar 0, \bar 0 0, 0\bar 1, 00\}\) and \(B_7 = \{\bar 0\bar 0, \bar 0 0, 0\bar 0, 00\}\). Then \(|\bar I_n(B_1)| = |\bar I_n(B_2)| = \cdots = |\bar I_n(B_7)|\) for every \(n \ge 0\), and \((1 - 2x)\,F_{B_1}(x) = 1\), that is, \(F_{B_1}(x) = 1/(1 - 2x)\).

MetaMathlibExt.signedInvSeq_wilf_and_gf_b0b1_b0b0_b01_01 · 28 lines

public theorem_wanted signedInvSeq_wilf_and_gf_b0b1_b0b0_b01_01 :
    signedInvAvoidCount {⟨.lt, true, true⟩, ⟨.eq, true, true⟩, ⟨.lt, true, false⟩,
        ⟨.lt, false, false⟩} =
      signedInvAvoidCount {⟨.lt, true, true⟩, ⟨.eq, true, false⟩, ⟨.lt, true, false⟩,
          ⟨.eq, false, false⟩} ∧
    signedInvAvoidCount {⟨.lt, true, true⟩, ⟨.eq, true, false⟩, ⟨.lt, true, false⟩,
        ⟨.eq, false, false⟩} =
      signedInvAvoidCount {⟨.lt, true, true⟩, ⟨.eq, true, true⟩, ⟨.lt, false, true⟩,
          ⟨.eq, false, false⟩} ∧
    signedInvAvoidCount {⟨.lt, true, true⟩, ⟨.eq, true, true⟩, ⟨.lt, false, true⟩,
        ⟨.eq, false, false⟩} =
      signedInvAvoidCount {⟨.lt, true, true⟩, ⟨.eq, true, true⟩, ⟨.eq, false, true⟩,
          ⟨.eq, false, false⟩} ∧
    signedInvAvoidCount {⟨.lt, true, true⟩, ⟨.eq, true, true⟩, ⟨.eq, false, true⟩,
        ⟨.eq, false, false⟩} =
      signedInvAvoidCount {⟨.lt, true, true⟩, ⟨.lt, true, false⟩, ⟨.lt, false, true⟩,
          ⟨.lt, false, false⟩} ∧
    signedInvAvoidCount {⟨.lt, true, true⟩, ⟨.lt, true, false⟩, ⟨.lt, false, true⟩,
        ⟨.lt, false, false⟩} =
      signedInvAvoidCount {⟨.eq, true, true⟩, ⟨.eq, true, false⟩, ⟨.lt, false, true⟩,
          ⟨.eq, false, false⟩} ∧
    signedInvAvoidCount {⟨.eq, true, true⟩, ⟨.eq, true, false⟩, ⟨.lt, false, true⟩,
        ⟨.eq, false, false⟩} =
      signedInvAvoidCount {⟨.eq, true, true⟩, ⟨.eq, true, false⟩, ⟨.eq, false, true⟩,
          ⟨.eq, false, false⟩} ∧
    (1 - 2 * X) * signedInvAvoidGF {⟨.lt, true, true⟩, ⟨.eq, true, true⟩, ⟨.lt, true, false⟩,
        ⟨.lt, false, false⟩} =
      1

Sources

• Toufik Mansour and Amir Safadi, Signed Inversion Sequences Avoiding a Set of Length-2 Signed Patterns, INTEGERS 26 (2026), Article A74, Theorem 3 (C15).

Uses 3

Statement usesLength-2 signed pattern · Number of signed inversion sequences avoiding a set of patterns · Generating function of signed inversion sequences avoiding a set of patterns

TheoremMansour–Safadi Theorem 3, class C16 (signed patterns 0̄1̄, 0̄0, 01̄, 01)#●ready to prove

A signed inversion sequence of length \(n\) is a word \(e_1 \cdots e_n\) with \(e_k \in \{0, \bar 0, 1, \bar 1, \dots, k - 1, \overline{k - 1}\}\). It avoids a length-2 signed pattern \(\tau_1\tau_2\) (one of \(00\), \(01\), \(10\), each letter possibly barred) when no \(i < j\) have \(|e_i|\), \(|e_j|\) in the same order as \(|\tau_1|\), \(|\tau_2|\) with \(e_i\), \(e_j\) barred exactly when \(\tau_1\), \(\tau_2\) are. Write \(\bar I_n(B)\) for the set of signed inversion sequences of length \(n\) that avoid every pattern in \(B\), and \(F_B(x) = \sum_{n \ge 0} |\bar I_n(B)|\,x^n\) in \(\mathbb{Q}[[x]]\). Let \(B_1 = \{\bar 0\bar 1, \bar 0 0, 0\bar 1, 01\}\) and \(B_2 = \{\bar 0\bar 1, \bar 0 1, 0\bar 0, 01\}\). Then \(|\bar I_n(B_1)| = |\bar I_n(B_2)|\) for every \(n \ge 0\), and \((1 - x)^2 (1 - 3x + x^2)\,F_{B_1}(x) = 1 - 3x + 2x^2 - x^3\).

public theorem_wanted signedInvSeq_wilf_and_gf_b0b1_b00_0b1_01 :
    signedInvAvoidCount {⟨.lt, true, true⟩, ⟨.eq, true, false⟩, ⟨.lt, false, true⟩,
        ⟨.lt, false, false⟩} =
      signedInvAvoidCount {⟨.lt, true, true⟩, ⟨.lt, true, false⟩, ⟨.eq, false, true⟩,
          ⟨.lt, false, false⟩} ∧
    ((1 - X) ^ 2 * (1 - 3 * X + X ^ 2)) * signedInvAvoidGF {⟨.lt, true, true⟩, ⟨.eq, true, false⟩,
        ⟨.lt, false, true⟩, ⟨.lt, false, false⟩} =
      1 - 3 * X + 2 * X ^ 2 - X ^ 3

Sources

• Toufik Mansour and Amir Safadi, Signed Inversion Sequences Avoiding a Set of Length-2 Signed Patterns, INTEGERS 26 (2026), Article A74, Theorem 3 (C16).

Uses 3

Statement usesLength-2 signed pattern · Number of signed inversion sequences avoiding a set of patterns · Generating function of signed inversion sequences avoiding a set of patterns

TheoremMansour–Safadi Theorem 3, class C21#●ready to prove

Write \(\bar{I}_n(B)\) for the set of signed inversion sequences of length \(n\) that avoid every length-2 signed pattern in \(B\), where a pattern is one of \(00\), \(01\), \(10\) with a bar over each barred letter. Then for every \(n \ge 0\), \(|\bar{I}_n(\{\bar{0}\bar{1}, \bar{0}1, 0\bar{1}, 0\bar{0}\})| = |\bar{I}_n(\{\bar{0}\bar{0}, \bar{0}1, 0\bar{1}, 0\bar{0}\})|\).

The generating function printed in the paper, \(1/(1 - x)^2 + \sum_{j \ge 0} j!\, x^j\), is false (its constant term is \(2\), while \(|\bar{I}_0(B)| = 1\)) and is omitted.

public theorem_wanted signedInvSeq_wilf_b0b1_b01_0b1_0b0 :
    signedInvAvoidCount {⟨.lt, true, true⟩, ⟨.lt, true, false⟩, ⟨.lt, false, true⟩,
        ⟨.eq, false, true⟩} =
      signedInvAvoidCount {⟨.eq, true, true⟩, ⟨.lt, true, false⟩, ⟨.lt, false, true⟩,
          ⟨.eq, false, true⟩}

Sources

• Toufik Mansour and Amir Safadi, Signed Inversion Sequences Avoiding a Set of Length-2 Signed Patterns, INTEGERS 26 (2026), Article A74, Theorem 3 (C21).

Uses 2

Statement usesLength-2 signed pattern · Number of signed inversion sequences avoiding a set of patterns

TheoremSigned inversion sequences avoiding \(\{\bar1\bar0, \bar0\bar1, \bar01, 00\}\)#●ready to prove

For a set \(B\) of length-2 signed patterns (a bar marks a barred letter), let \(|\bar I_n(B)|\) be the number of signed inversion sequences of length \(n\) avoiding every pattern of \(B\), and let \(F_B(x) = \sum_{n \ge 0} |\bar I_n(B)| x^n \in \mathbb{Q}[[x]]\). Let \(B = \{\bar1\bar0, \bar0\bar1, \bar01, 00\}\) and \(C = \{\bar10, \bar0\bar0, 0\bar1, 01\}\). Then \(|\bar I_n(B)| = |\bar I_n(C)|\) for every \(n \ge 0\), and \((1 - x)^3 F_B(x) = 1 - x + 2x^2\), that is, \(F_B(x) = (1 - x + 2x^2)/(1 - x)^3\).

public theorem_wanted signedInvSeq_wilf_and_gf_b1b0_b0b1_b01_00 :
    signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.lt, true, true⟩, ⟨.lt, true, false⟩,
        ⟨.eq, false, false⟩} =
      signedInvAvoidCount {⟨.gt, true, false⟩, ⟨.eq, true, true⟩, ⟨.lt, false, true⟩,
          ⟨.lt, false, false⟩} ∧
    ((1 - X) ^ 3) * signedInvAvoidGF {⟨.gt, true, true⟩, ⟨.lt, true, true⟩, ⟨.lt, true, false⟩,
        ⟨.eq, false, false⟩} =
      1 - X + 2 * X ^ 2

Sources

• Toufik Mansour and Amir Safadi, Signed Inversion Sequences Avoiding a Set of Length-2 Signed Patterns, INTEGERS 26 (2026), Article A74, Theorem 3 (C23).

Uses 3

Statement usesLength-2 signed pattern · Number of signed inversion sequences avoiding a set of patterns · Generating function of signed inversion sequences avoiding a set of patterns

TheoremSigned inversion sequences avoiding \(\{\bar1\bar0, \bar0\bar0, 0\bar1, 01\}\)#●ready to prove

For a set \(B\) of length-2 signed patterns (a bar marks a barred letter), let \(|\bar I_n(B)|\) be the number of signed inversion sequences of length \(n\) avoiding every pattern of \(B\), and let \(F_B(x) = \sum_{n \ge 0} |\bar I_n(B)| x^n \in \mathbb{Q}[[x]]\). Let \(B = \{\bar1\bar0, \bar0\bar0, 0\bar1, 01\}\) and \(C = \{\bar10, \bar0\bar1, \bar01, 00\}\). Then \(|\bar I_n(B)| = |\bar I_n(C)|\) for every \(n \ge 0\), and \((1 - x)(1 - 2x) F_B(x) = 1 - x + x^2\), that is, \(F_B(x) = (1 - x + x^2)/((1 - x)(1 - 2x))\).

public theorem_wanted signedInvSeq_wilf_and_gf_b1b0_b0b0_0b1_01 :
    signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.eq, true, true⟩, ⟨.lt, false, true⟩,
        ⟨.lt, false, false⟩} =
      signedInvAvoidCount {⟨.gt, true, false⟩, ⟨.lt, true, true⟩, ⟨.lt, true, false⟩,
          ⟨.eq, false, false⟩} ∧
    ((1 - X) * (1 - 2 * X)) * signedInvAvoidGF {⟨.gt, true, true⟩, ⟨.eq, true, true⟩,
        ⟨.lt, false, true⟩, ⟨.lt, false, false⟩} =
      1 - X + X ^ 2

Sources

• Toufik Mansour and Amir Safadi, Signed Inversion Sequences Avoiding a Set of Length-2 Signed Patterns, INTEGERS 26 (2026), Article A74, Theorem 3 (C25).

Uses 3

Statement usesLength-2 signed pattern · Number of signed inversion sequences avoiding a set of patterns · Generating function of signed inversion sequences avoiding a set of patterns

TheoremSigned inversion sequences avoiding \(\{\bar1\bar0, \bar0\bar1, \bar0\bar0, 00\}\)#●ready to prove

For a set \(B\) of length-2 signed patterns (a bar marks a barred letter), let \(|\bar I_n(B)|\) be the number of signed inversion sequences of length \(n\) avoiding every pattern of \(B\), and let \(F_B(x) = \sum_{n \ge 0} |\bar I_n(B)| x^n \in \mathbb{Q}[[x]]\). Let \(B_1 = \{\bar1\bar0, \bar0\bar1, \bar0\bar0, 00\}\), \(B_2 = \{\bar1\bar0, \bar0\bar1, \bar01, 01\}\), \(B_3 = \{\bar10, \bar0\bar1, \bar01, 01\}\), \(B_4 = \{\bar10, \bar0\bar0, 0\bar1, 00\}\) and \(B_5 = \{\bar0\bar0, \bar01, 00, 1\bar0\}\). Then \(|\bar I_n(B_1)| = |\bar I_n(B_2)| = |\bar I_n(B_3)| = |\bar I_n(B_4)| = |\bar I_n(B_5)|\) for every \(n \ge 0\), and \((1 - x)^2(1 - 2x) F_{B_1}(x) = 1 - 2x + 2x^2\), that is, \(F_{B_1}(x) = (1 - 2x + 2x^2)/((1 - x)^2(1 - 2x))\).

MetaMathlibExt.signedInvSeq_wilf_and_gf_b1b0_b0b1_b0b0_00 · 20 lines

public theorem_wanted signedInvSeq_wilf_and_gf_b1b0_b0b1_b0b0_00 :
    signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.lt, true, true⟩, ⟨.eq, true, true⟩,
        ⟨.eq, false, false⟩} =
      signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.lt, true, true⟩, ⟨.lt, true, false⟩,
          ⟨.lt, false, false⟩} ∧
    signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.lt, true, true⟩, ⟨.lt, true, false⟩,
        ⟨.lt, false, false⟩} =
      signedInvAvoidCount {⟨.gt, true, false⟩, ⟨.lt, true, true⟩, ⟨.lt, true, false⟩,
          ⟨.lt, false, false⟩} ∧
    signedInvAvoidCount {⟨.gt, true, false⟩, ⟨.lt, true, true⟩, ⟨.lt, true, false⟩,
        ⟨.lt, false, false⟩} =
      signedInvAvoidCount {⟨.gt, true, false⟩, ⟨.eq, true, true⟩, ⟨.lt, false, true⟩,
          ⟨.eq, false, false⟩} ∧
    signedInvAvoidCount {⟨.gt, true, false⟩, ⟨.eq, true, true⟩, ⟨.lt, false, true⟩,
        ⟨.eq, false, false⟩} =
      signedInvAvoidCount {⟨.eq, true, true⟩, ⟨.lt, true, false⟩, ⟨.eq, false, false⟩,
          ⟨.gt, false, true⟩} ∧
    ((1 - X) ^ 2 * (1 - 2 * X)) * signedInvAvoidGF {⟨.gt, true, true⟩, ⟨.lt, true, true⟩,
        ⟨.eq, true, true⟩, ⟨.eq, false, false⟩} =
      1 - 2 * X + 2 * X ^ 2

Sources

• Toufik Mansour and Amir Safadi, Signed Inversion Sequences Avoiding a Set of Length-2 Signed Patterns, INTEGERS 26 (2026), Article A74, Theorem 3 (C30).

Uses 3

Statement usesLength-2 signed pattern · Number of signed inversion sequences avoiding a set of patterns · Generating function of signed inversion sequences avoiding a set of patterns

TheoremSigned inversion sequences avoiding \(\{\bar1\bar0, \bar0\bar1, \bar00, 01\}\)#●ready to prove

For a set \(B\) of length-2 signed patterns (a bar marks a barred letter), let \(|\bar I_n(B)|\) be the number of signed inversion sequences of length \(n\) avoiding every pattern of \(B\), and let \(F_B(x) = \sum_{n \ge 0} |\bar I_n(B)| x^n \in \mathbb{Q}[[x]]\). Let \(B = \{\bar1\bar0, \bar0\bar1, \bar00, 01\}\) and \(C = \{\bar10, \bar0\bar1, \bar00, 01\}\). Then \(|\bar I_n(B)| = |\bar I_n(C)|\) for every \(n \ge 0\), and \((1 - x)(1 - 2x)(1 - 3x + x^2) F_B(x) = 1 - 4x + 5x^2 - 3x^3\), that is, \(F_B(x) = (1 - 4x + 5x^2 - 3x^3)/((1 - x)(1 - 2x)(1 - 3x + x^2))\).

public theorem_wanted signedInvSeq_wilf_and_gf_b1b0_b0b1_b00_01 :
    signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.lt, true, true⟩, ⟨.eq, true, false⟩,
        ⟨.lt, false, false⟩} =
      signedInvAvoidCount {⟨.gt, true, false⟩, ⟨.lt, true, true⟩, ⟨.eq, true, false⟩,
          ⟨.lt, false, false⟩} ∧
    ((1 - X) * (1 - 2 * X) * (1 - 3 * X + X ^ 2)) * signedInvAvoidGF {⟨.gt, true, true⟩,
        ⟨.lt, true, true⟩, ⟨.eq, true, false⟩, ⟨.lt, false, false⟩} =
      1 - 4 * X + 5 * X ^ 2 - 3 * X ^ 3

Sources

• Toufik Mansour and Amir Safadi, Signed Inversion Sequences Avoiding a Set of Length-2 Signed Patterns, INTEGERS 26 (2026), Article A74, Theorem 3 (C32).

Uses 3

Statement usesLength-2 signed pattern · Number of signed inversion sequences avoiding a set of patterns · Generating function of signed inversion sequences avoiding a set of patterns

TheoremSigned inversion sequences avoiding \(\{\bar1\bar0, \bar0\bar1, 0\bar1, 01\}\)#●ready to prove

For a set \(B\) of length-2 signed patterns (a bar marks a barred letter), let \(|\bar I_n(B)|\) be the number of signed inversion sequences of length \(n\) avoiding every pattern of \(B\), and let \(F_B(x) = \sum_{n \ge 0} |\bar I_n(B)| x^n \in \mathbb{Q}[[x]]\). Let \(B = \{\bar1\bar0, \bar0\bar1, 0\bar1, 01\}\) and \(C = \{\bar10, \bar0\bar1, 0\bar1, 01\}\). Then \(|\bar I_n(B)| = |\bar I_n(C)|\) for every \(n \ge 0\), and \((1 - 3x + x^2) F_B(x) = 1 - x\), that is, \(F_B(x) = (1 - x)/(1 - 3x + x^2)\).

public theorem_wanted signedInvSeq_wilf_and_gf_b1b0_b0b1_0b1_01 :
    signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.lt, true, true⟩, ⟨.lt, false, true⟩,
        ⟨.lt, false, false⟩} =
      signedInvAvoidCount {⟨.gt, true, false⟩, ⟨.lt, true, true⟩, ⟨.lt, false, true⟩,
          ⟨.lt, false, false⟩} ∧
    (1 - 3 * X + X ^ 2) * signedInvAvoidGF {⟨.gt, true, true⟩, ⟨.lt, true, true⟩,
        ⟨.lt, false, true⟩, ⟨.lt, false, false⟩} =
      1 - X

Sources

• Toufik Mansour and Amir Safadi, Signed Inversion Sequences Avoiding a Set of Length-2 Signed Patterns, INTEGERS 26 (2026), Article A74, Theorem 3 (C38).

Uses 3

Statement usesLength-2 signed pattern · Number of signed inversion sequences avoiding a set of patterns · Generating function of signed inversion sequences avoiding a set of patterns

TheoremSigned inversion sequences avoiding \(\{\bar1\bar0, \bar0\bar0, \bar00, 01\}\)#●ready to prove

For a set \(B\) of length-2 signed patterns (a bar marks a barred letter), let \(|\bar I_n(B)|\) be the number of signed inversion sequences of length \(n\) avoiding every pattern of \(B\), and let \(F_B(x) = \sum_{n \ge 0} |\bar I_n(B)| x^n \in \mathbb{Q}[[x]]\). Let \(B = \{\bar1\bar0, \bar0\bar0, \bar00, 01\}\) and \(C = \{\bar1\bar0, \bar01, 0\bar1, 01\}\). Then \(|\bar I_n(B)| = |\bar I_n(C)|\) for every \(n \ge 0\), and for every power series \(S \in \mathbb{Q}[[x]]\) with constant term \(1\) and \(S^2 = 1 - 4x\),

\[ 2x(1 - x)^2(1 - 2x) F_B(x) = 1 - 3x + 2x^2 + 2x^3 - (1 - 3x + 2x^2) S. \]

This is the formula \(F_B(x) = \bigl(1 - 3x + 2x^2 + 2x^3 - (1 - 3x + 2x^2)\sqrt{1 - 4x}\bigr)/(2x(1 - x)^2(1 - 2x))\) multiplied by its denominator, with \(S = \sqrt{1 - 4x}\).

public theorem_wanted signedInvSeq_wilf_and_gf_b1b0_b0b0_b00_01 :
    signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.eq, true, true⟩, ⟨.eq, true, false⟩,
        ⟨.lt, false, false⟩} =
      signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.lt, true, false⟩, ⟨.lt, false, true⟩,
          ⟨.lt, false, false⟩} ∧
    ∀ S : ℚ⟦X⟧, constantCoeff S = 1 → S ^ 2 = 1 - 4 * X →
      2 * X * (1 - X) ^ 2 * (1 - 2 * X) * signedInvAvoidGF {⟨.gt, true, true⟩, ⟨.eq, true, true⟩,
          ⟨.eq, true, false⟩, ⟨.lt, false, false⟩} =
        1 - 3 * X + 2 * X ^ 2 + 2 * X ^ 3 - (1 - 3 * X + 2 * X ^ 2) * S

Sources

• Toufik Mansour and Amir Safadi, Signed Inversion Sequences Avoiding a Set of Length-2 Signed Patterns, INTEGERS 26 (2026), Article A74, Theorem 3 (C39).

Uses 3

Statement usesLength-2 signed pattern · Number of signed inversion sequences avoiding a set of patterns · Generating function of signed inversion sequences avoiding a set of patterns

TheoremMansour–Safadi Theorem 3, class C41 (signed patterns 1̄0̄, 0̄0̄, 01̄, 00)#●ready to prove

A signed inversion sequence of length \(n\) is a word \(e_1 \cdots e_n\) with \(e_k \in \{0, \bar 0, 1, \bar 1, \dots, k - 1, \overline{k - 1}\}\). It avoids a length-2 signed pattern \(\tau_1\tau_2\) (one of \(00\), \(01\), \(10\), each letter possibly barred) when no \(i < j\) have \(|e_i|\), \(|e_j|\) in the same order as \(|\tau_1|\), \(|\tau_2|\) with \(e_i\), \(e_j\) barred exactly when \(\tau_1\), \(\tau_2\) are. Write \(\bar I_n(B)\) for the set of signed inversion sequences of length \(n\) that avoid every pattern in \(B\), and \(F_B(x) = \sum_{n \ge 0} |\bar I_n(B)|\,x^n\) in \(\mathbb{Q}[[x]]\). Let \(B_1 = \{\bar 1\bar 0, \bar 0\bar 0, 0\bar 1, 00\}\) and \(B_2 = \{\bar 1 0, \bar 0\bar 0, \bar 0 0, 01\}\). For every \(n \ge 0\), \(|\bar I_n(B_1)| = |\bar I_n(B_2)|\), and the coefficient of \(x^n\) in \(F_{B_1}(x)\) equals the coefficient of \(x^n\) in \((1 - x)^{-1} + (1 - x)^{-1} \sum_{j=1}^{n} x^j (1 - (j + 1)x)^{-1}\).

Since the terms with \(j > n\) contribute nothing to \(x^n\), this says \(F_{B_1}(x) = \frac{1}{1 - x}\bigl(1 + \sum_{j \ge 1} x^j / (1 - (j + 1)x)\bigr)\).

public theorem_wanted signedInvSeq_wilf_and_gf_b1b0_b0b0_0b1_00 :
    signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.eq, true, true⟩, ⟨.lt, false, true⟩,
        ⟨.eq, false, false⟩} =
      signedInvAvoidCount {⟨.gt, true, false⟩, ⟨.eq, true, true⟩, ⟨.eq, true, false⟩,
          ⟨.lt, false, false⟩} ∧
    ∀ n, coeff n (signedInvAvoidGF {⟨.gt, true, true⟩, ⟨.eq, true, true⟩, ⟨.lt, false, true⟩,
        ⟨.eq, false, false⟩}) =
      coeff n ((1 - X)⁻¹ + (1 - X)⁻¹ * ∑ j ∈ Finset.Icc 1 n, X ^ j * (1 - ((j + 1 : ℕ) : ℚ⟦X⟧) *
            X)⁻¹)

Sources

• Toufik Mansour and Amir Safadi, Signed Inversion Sequences Avoiding a Set of Length-2 Signed Patterns, INTEGERS 26 (2026), Article A74, Theorem 3 (C41).

Uses 3

Statement usesLength-2 signed pattern · Number of signed inversion sequences avoiding a set of patterns · Generating function of signed inversion sequences avoiding a set of patterns

TheoremMansour–Safadi Theorem 3, class C45#●ready to prove

Write \(\bar{I}_n(B)\) for the set of signed inversion sequences of length \(n\) that avoid every length-2 signed pattern in \(B\), where a pattern is one of \(00\), \(01\), \(10\) with a bar over each barred letter. Then for every \(n \ge 0\), \(|\bar{I}_n(\{\bar{1}\bar{0}, \bar{0}\bar{0}, \bar{0}1, 01\})| = |\bar{I}_n(\{\bar{1}\bar{0}, \bar{0}0, \bar{0}1, 00\})|\).

The generating function \(C(x)\) printed in the paper is not defined there and is omitted.

public theorem_wanted signedInvSeq_wilf_b1b0_b0b0_b01_01 :
    signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.eq, true, true⟩, ⟨.lt, true, false⟩,
        ⟨.lt, false, false⟩} =
      signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.eq, true, false⟩, ⟨.lt, true, false⟩,
          ⟨.eq, false, false⟩}

Sources

• Toufik Mansour and Amir Safadi, Signed Inversion Sequences Avoiding a Set of Length-2 Signed Patterns, INTEGERS 26 (2026), Article A74, Theorem 3 (C45).

Uses 2

Statement usesLength-2 signed pattern · Number of signed inversion sequences avoiding a set of patterns

TheoremSigned inversion sequences avoiding \(\{\bar1\bar0, \bar0\bar1, \bar00, 00\}\)#●ready to prove

For a set \(B\) of length-2 signed patterns (a bar marks a barred letter), let \(|\bar I_n(B)|\) be the number of signed inversion sequences of length \(n\) avoiding every pattern of \(B\), and let \(F_B(x) = \sum_{n \ge 0} |\bar I_n(B)| x^n \in \mathbb{Q}[[x]]\). Let \(B_1 = \{\bar1\bar0, \bar0\bar1, \bar00, 00\}\), \(B_2 = \{\bar1\bar0, \bar0\bar1, 0\bar0, 00\}\) and \(B_3 = \{\bar10, \bar0\bar1, 0\bar0, 00\}\). Then \(|\bar I_n(B_1)| = |\bar I_n(B_2)| = |\bar I_n(B_3)|\) for every \(n \ge 0\), and for every \(n \ge 0\) the coefficient of \(x^n\) in \(F_{B_1}(x)\) equals the coefficient of \(x^n\) in

\[ \frac{1}{1 - x} + \frac{1}{1 - x} \sum_{j=1}^{n} \frac{x^j (1 - jx)}{\prod_{i=1}^{j+1} (1 - ix)}. \]

The terms with \(j > n\) are divisible by \(x^{n+1}\), so this says \(F_{B_1}(x) = \frac{1}{1 - x}\Bigl(1 + \sum_{j \ge 1} x^j (1 - jx) / \prod_{i=1}^{j+1} (1 - ix)\Bigr)\).

public theorem_wanted signedInvSeq_wilf_and_gf_b1b0_b0b1_b00_00 :
    signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.lt, true, true⟩, ⟨.eq, true, false⟩,
        ⟨.eq, false, false⟩} =
      signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.lt, true, true⟩, ⟨.eq, false, true⟩,
          ⟨.eq, false, false⟩} ∧
    signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.lt, true, true⟩, ⟨.eq, false, true⟩,
        ⟨.eq, false, false⟩} =
      signedInvAvoidCount {⟨.gt, true, false⟩, ⟨.lt, true, true⟩, ⟨.eq, false, true⟩,
          ⟨.eq, false, false⟩} ∧
    ∀ n, coeff n (signedInvAvoidGF {⟨.gt, true, true⟩, ⟨.lt, true, true⟩, ⟨.eq, true, false⟩,
        ⟨.eq, false, false⟩}) =
      coeff n ((1 - X)⁻¹ + (1 - X)⁻¹ * ∑ j ∈ Finset.Icc 1 n, X ^ j * (1 - (j : ℚ⟦X⟧) * X) * ∏ i ∈
            Finset.Icc 1 (j + 1), (1 - (i : ℚ⟦X⟧) * X)⁻¹)

Sources

• Toufik Mansour and Amir Safadi, Signed Inversion Sequences Avoiding a Set of Length-2 Signed Patterns, INTEGERS 26 (2026), Article A74, Theorem 3 (C46).

Uses 3

Statement usesLength-2 signed pattern · Number of signed inversion sequences avoiding a set of patterns · Generating function of signed inversion sequences avoiding a set of patterns

TheoremSigned inversion sequences avoiding \(\{\bar1\bar0, \bar0\bar1, \bar01, 0\bar1\}\)#●ready to prove

For a set \(B\) of length-2 signed patterns (a bar marks a barred letter), let \(|\bar I_n(B)|\) be the number of signed inversion sequences of length \(n\) avoiding every pattern of \(B\), and let \(F_B(x) = \sum_{n \ge 0} |\bar I_n(B)| x^n \in \mathbb{Q}[[x]]\). Let \(B = \{\bar1\bar0, \bar0\bar1, \bar01, 0\bar1\}\) and \(C = \{\bar10, \bar0\bar1, \bar01, 0\bar1\}\). Then \(|\bar I_n(B)| = |\bar I_n(C)|\) for every \(n \ge 0\), and \((1 - 2x) F_B(x) = (1 - x) \sum_{j \ge 0} j!\, x^j\), that is, \(F_B(x) = \frac{1 - x}{1 - 2x} \sum_{j \ge 0} j!\, x^j\).

public theorem_wanted signedInvSeq_wilf_and_gf_b1b0_b0b1_b01_0b1 :
    signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.lt, true, true⟩, ⟨.lt, true, false⟩,
        ⟨.lt, false, true⟩} =
      signedInvAvoidCount {⟨.gt, true, false⟩, ⟨.lt, true, true⟩, ⟨.lt, true, false⟩,
          ⟨.lt, false, true⟩} ∧
    (1 - 2 * X) * signedInvAvoidGF {⟨.gt, true, true⟩, ⟨.lt, true, true⟩, ⟨.lt, true, false⟩,
        ⟨.lt, false, true⟩} =
      (1 - X) * PowerSeries.mk fun j => (j ! : ℚ)

Sources

• Toufik Mansour and Amir Safadi, Signed Inversion Sequences Avoiding a Set of Length-2 Signed Patterns, INTEGERS 26 (2026), Article A74, Theorem 3 (C50).

Uses 3

Statement usesLength-2 signed pattern · Number of signed inversion sequences avoiding a set of patterns · Generating function of signed inversion sequences avoiding a set of patterns

TheoremSigned inversion sequences avoiding \(\{\bar1\bar0, \bar0\bar1, 0\bar1, 00\}\)#●ready to prove

For a set \(B\) of length-2 signed patterns (a bar marks a barred letter), let \(|\bar I_n(B)|\) be the number of signed inversion sequences of length \(n\) avoiding every pattern of \(B\), and let \(F_B(x) = \sum_{n \ge 0} |\bar I_n(B)| x^n \in \mathbb{Q}[[x]]\). Let \(B = \{\bar1\bar0, \bar0\bar1, 0\bar1, 00\}\) and \(C = \{\bar10, \bar0\bar1, 0\bar1, 00\}\). Then \(|\bar I_n(B)| = |\bar I_n(C)|\) for every \(n \ge 0\), and for every \(n \ge 0\) the coefficient of \(x^n\) in \(F_B(x)\) equals the coefficient of \(x^n\) in \(\sum_{j=0}^{n} x^j \prod_{i=1}^{j+1} (1 - ix)^{-1}\).

The terms with \(j > n\) are divisible by \(x^{n+1}\), so this says \(F_B(x) = \sum_{j \ge 0} x^j / \prod_{i=1}^{j+1} (1 - ix)\).

public theorem_wanted signedInvSeq_wilf_and_gf_b1b0_b0b1_0b1_00 :
    signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.lt, true, true⟩, ⟨.lt, false, true⟩,
        ⟨.eq, false, false⟩} =
      signedInvAvoidCount {⟨.gt, true, false⟩, ⟨.lt, true, true⟩, ⟨.lt, false, true⟩,
          ⟨.eq, false, false⟩} ∧
    ∀ n, coeff n (signedInvAvoidGF {⟨.gt, true, true⟩, ⟨.lt, true, true⟩, ⟨.lt, false, true⟩,
        ⟨.eq, false, false⟩}) =
      coeff n (∑ j ∈ Finset.range (n + 1), X ^ j * ∏ i ∈ Finset.Icc 1 (j + 1), (1 - (i : ℚ⟦X⟧) *
            X)⁻¹)

Sources

• Toufik Mansour and Amir Safadi, Signed Inversion Sequences Avoiding a Set of Length-2 Signed Patterns, INTEGERS 26 (2026), Article A74, Theorem 3 (C60).

Uses 3

Statement usesLength-2 signed pattern · Number of signed inversion sequences avoiding a set of patterns · Generating function of signed inversion sequences avoiding a set of patterns

TheoremMansour–Safadi Theorem 4#●ready to prove

Write \(\bar{I}_n(B)\) for the set of signed inversion sequences of length \(n\) that avoid every length-2 signed pattern in \(B\), where a pattern is one of \(00\), \(01\), \(10\) with a bar over each barred letter. Then for every \(n \ge 0\), \(|\bar{I}_n(\{\bar{0}\bar{1}, \bar{0}\bar{0}, \bar{0}1, 0\bar{0}\})| = |\bar{I}_n(\{\bar{0}\bar{1}, \bar{0}0, \bar{0}1, 0\bar{0}\})|\).

public theorem_wanted signedInvSeq_wilf_b0b1_b0b0_b01_0b0 :
    signedInvAvoidCount {⟨.lt, true, true⟩, ⟨.eq, true, true⟩, ⟨.lt, true, false⟩,
        ⟨.eq, false, true⟩} =
      signedInvAvoidCount {⟨.lt, true, true⟩, ⟨.eq, true, false⟩, ⟨.lt, true, false⟩,
          ⟨.eq, false, true⟩}

Sources

• Toufik Mansour and Amir Safadi, Signed Inversion Sequences Avoiding a Set of Length-2 Signed Patterns, INTEGERS 26 (2026), Article A74, Theorem 4.

Uses 2

Statement usesLength-2 signed pattern · Number of signed inversion sequences avoiding a set of patterns

TheoremMansour–Safadi Theorem 5#●ready to prove

Write \(\bar{I}_n(B)\) for the set of signed inversion sequences of length \(n\) that avoid every length-2 signed pattern in \(B\), where a pattern is one of \(00\), \(01\), \(10\) with a bar over each barred letter. Then for every \(n \ge 0\), \(|\bar{I}_n(\{\bar{1}\bar{0}, \bar{0}\bar{0}, \bar{0}1, 0\bar{0}\})| = |\bar{I}_n(\{\bar{1}\bar{0}, \bar{0}0, \bar{0}1, 0\bar{0}\})|\), \(|\bar{I}_n(\{\bar{1}0, \bar{0}\bar{1}, \bar{0}\bar{0}, 0\bar{0}\})| = |\bar{I}_n(\{\bar{1}0, \bar{0}\bar{1}, \bar{0}0, 0\bar{0}\})|\), and \(|\bar{I}_n(\{\bar{1}\bar{0}, \bar{0}\bar{0}, \bar{0}1, 1\bar{0}\})| = |\bar{I}_n(\{\bar{1}\bar{0}, \bar{0}0, \bar{0}1, 1\bar{0}\})|\).

public theorem_wanted signedInvSeq_wilf_b1b0_b0b0_b01_0b0 :
    signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.eq, true, true⟩, ⟨.lt, true, false⟩,
        ⟨.eq, false, true⟩} =
      signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.eq, true, false⟩, ⟨.lt, true, false⟩,
          ⟨.eq, false, true⟩} ∧
    signedInvAvoidCount {⟨.gt, true, false⟩, ⟨.lt, true, true⟩, ⟨.eq, true, true⟩,
        ⟨.eq, false, true⟩} =
      signedInvAvoidCount {⟨.gt, true, false⟩, ⟨.lt, true, true⟩, ⟨.eq, true, false⟩,
          ⟨.eq, false, true⟩} ∧
    signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.eq, true, true⟩, ⟨.lt, true, false⟩,
        ⟨.gt, false, true⟩} =
      signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.eq, true, false⟩, ⟨.lt, true, false⟩,
          ⟨.gt, false, true⟩}

Sources

• Toufik Mansour and Amir Safadi, Signed Inversion Sequences Avoiding a Set of Length-2 Signed Patterns, INTEGERS 26 (2026), Article A74, Theorem 5.

Uses 2

Statement usesLength-2 signed pattern · Number of signed inversion sequences avoiding a set of patterns

TheoremMansour–Safadi Theorem 6#●ready to prove

Write \(\bar{I}_n(B)\) for the set of signed inversion sequences of length \(n\) that avoid every length-2 signed pattern in \(B\), where a pattern is one of \(00\), \(01\), \(10\) with a bar over each barred letter. Then for every \(n \ge 0\), \(|\bar{I}_n(\{\bar{1}0, \bar{0}0, 0\bar{1}, 00\})| = |\bar{I}_n(\{\bar{1}0, 0\bar{1}, 0\bar{0}, 00\})|\).

public theorem_wanted signedInvSeq_wilf_b10_b00_0b1_00 :
    signedInvAvoidCount {⟨.gt, true, false⟩, ⟨.eq, true, false⟩, ⟨.lt, false, true⟩,
        ⟨.eq, false, false⟩} =
      signedInvAvoidCount {⟨.gt, true, false⟩, ⟨.lt, false, true⟩, ⟨.eq, false, true⟩,
          ⟨.eq, false, false⟩}

Sources

• Toufik Mansour and Amir Safadi, Signed Inversion Sequences Avoiding a Set of Length-2 Signed Patterns, INTEGERS 26 (2026), Article A74, Theorem 6.

Uses 2

Statement usesLength-2 signed pattern · Number of signed inversion sequences avoiding a set of patterns

TheoremMansour–Safadi Theorem 7: four Wilf-equivalent four-pattern sets#●ready to prove

Length-2 signed patterns are written as in the paper, a bar marking a barred letter, and \(B \sim C\) means that for every \(n \ge 0\) the number \(|\bar I_n(B)|\) of signed inversion sequences of length \(n\) avoiding every pattern of \(B\) equals \(|\bar I_n(C)|\). Then \(\{\bar1\bar0, \bar0\bar1, \bar0\bar0, \bar00\} \sim \{\bar1\bar0, \bar0\bar1, \bar0\bar0, 0\bar0\} \sim \{\bar1\bar0, \bar0\bar1, \bar00, 0\bar0\} \sim \{\bar10, \bar00, 0\bar1, 0\bar0\}\).

public theorem_wanted signedInvSeq_wilf_b1b0_b0b1_b0b0_b00 :
    signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.lt, true, true⟩, ⟨.eq, true, true⟩,
        ⟨.eq, true, false⟩} =
      signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.lt, true, true⟩, ⟨.eq, true, true⟩,
          ⟨.eq, false, true⟩} ∧
    signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.lt, true, true⟩, ⟨.eq, true, true⟩,
        ⟨.eq, false, true⟩} =
      signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.lt, true, true⟩, ⟨.eq, true, false⟩,
          ⟨.eq, false, true⟩} ∧
    signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.lt, true, true⟩, ⟨.eq, true, false⟩,
        ⟨.eq, false, true⟩} =
      signedInvAvoidCount {⟨.gt, true, false⟩, ⟨.eq, true, false⟩, ⟨.lt, false, true⟩,
          ⟨.eq, false, true⟩}

Sources

• Toufik Mansour and Amir Safadi, Signed Inversion Sequences Avoiding a Set of Length-2 Signed Patterns, INTEGERS 26 (2026), Article A74, Theorem 7.

Uses 2

Statement usesLength-2 signed pattern · Number of signed inversion sequences avoiding a set of patterns

TheoremMansour–Safadi Theorem 8: two Wilf-equivalences of four-pattern sets#●ready to prove

Length-2 signed patterns are written as in the paper, a bar marking a barred letter, and \(B \sim C\) means that for every \(n \ge 0\) the number \(|\bar I_n(B)|\) of signed inversion sequences of length \(n\) avoiding every pattern of \(B\) equals \(|\bar I_n(C)|\). Then \(\{\bar1\bar0, \bar0\bar1, \bar0\bar0, 1\bar0\} \sim \{\bar1\bar0, \bar0\bar1, 0\bar0, 1\bar0\}\) and \(\{\bar1\bar0, \bar0\bar0, \bar00, 1\bar0\} \sim \{\bar1\bar0, \bar00, 0\bar0, 1\bar0\}\).

public theorem_wanted signedInvSeq_wilf_b1b0_b0b1_b0b0_1b0 :
    signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.lt, true, true⟩, ⟨.eq, true, true⟩,
        ⟨.gt, false, true⟩} =
      signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.lt, true, true⟩, ⟨.eq, false, true⟩,
          ⟨.gt, false, true⟩} ∧
    signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.eq, true, true⟩, ⟨.eq, true, false⟩,
        ⟨.gt, false, true⟩} =
      signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.eq, true, false⟩, ⟨.eq, false, true⟩,
          ⟨.gt, false, true⟩}

Sources

• Toufik Mansour and Amir Safadi, Signed Inversion Sequences Avoiding a Set of Length-2 Signed Patterns, INTEGERS 26 (2026), Article A74, Theorem 8.

Uses 2

Statement usesLength-2 signed pattern · Number of signed inversion sequences avoiding a set of patterns

TheoremMansour–Safadi Theorem 9: a Wilf-equivalence of four-pattern sets#●ready to prove

Length-2 signed patterns are written as in the paper, a bar marking a barred letter, and \(B \sim C\) means that for every \(n \ge 0\) the number \(|\bar I_n(B)|\) of signed inversion sequences of length \(n\) avoiding every pattern of \(B\) equals \(|\bar I_n(C)|\). Then \(\{\bar1\bar0, \bar10, \bar0\bar0, 0\bar0\} \sim \{\bar1\bar0, \bar10, \bar00, 0\bar0\}\).

public theorem_wanted signedInvSeq_wilf_b1b0_b10_b0b0_0b0 :
    signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.gt, true, false⟩, ⟨.eq, true, true⟩,
        ⟨.eq, false, true⟩} =
      signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.gt, true, false⟩, ⟨.eq, true, false⟩,
          ⟨.eq, false, true⟩}

Sources

• Toufik Mansour and Amir Safadi, Signed Inversion Sequences Avoiding a Set of Length-2 Signed Patterns, INTEGERS 26 (2026), Article A74, Theorem 9.

Uses 2

Statement usesLength-2 signed pattern · Number of signed inversion sequences avoiding a set of patterns

TheoremMansour–Safadi Theorem 12: four Wilf-equivalences of five-pattern sets#●ready to prove

Length-2 signed patterns are written as in the paper, a bar marking a barred letter, and \(B \sim C\) means that for every \(n \ge 0\) the number \(|\bar I_n(B)|\) of signed inversion sequences of length \(n\) avoiding every pattern of \(B\) equals \(|\bar I_n(C)|\). Then \(\{\bar1\bar0, \bar0\bar1, \bar00, \bar01, 0\bar0\} \sim \{\bar1\bar0, \bar0\bar1, \bar0\bar0, \bar01, 0\bar0\}\), \(\{\bar1\bar0, \bar10, \bar0\bar1, \bar00, 0\bar0\} \sim \{\bar1\bar0, \bar10, \bar0\bar1, \bar0\bar0, 0\bar0\}\), \(\{\bar1\bar0, \bar0\bar1, \bar0\bar0, \bar00, 1\bar0\} \sim \{\bar1\bar0, \bar0\bar1, \bar00, 0\bar0, 1\bar0\}\) and \(\{\bar1\bar0, \bar10, \bar0\bar1, \bar00, 00\} \sim \{\bar1\bar0, \bar10, \bar0\bar1, 0\bar0, 00\}\).

The paper prints a third set in the first equivalence, \(\{\bar1\bar0, \bar0\bar1, \bar01, 0\bar0, 1\bar0\}\); it is left out here because it has \(|\bar I_2| = 5\), against \(4\) for the first two sets.

MetaMathlibExt.signedInvSeq_wilf_b1b0_b0b1_b00_b01_0b0 · 17 lines

public theorem_wanted signedInvSeq_wilf_b1b0_b0b1_b00_b01_0b0 :
    signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.lt, true, true⟩, ⟨.eq, true, false⟩,
        ⟨.lt, true, false⟩, ⟨.eq, false, true⟩} =
      signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.lt, true, true⟩, ⟨.eq, true, true⟩,
          ⟨.lt, true, false⟩, ⟨.eq, false, true⟩} ∧
    signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.gt, true, false⟩, ⟨.lt, true, true⟩,
        ⟨.eq, true, false⟩, ⟨.eq, false, true⟩} =
      signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.gt, true, false⟩, ⟨.lt, true, true⟩,
          ⟨.eq, true, true⟩, ⟨.eq, false, true⟩} ∧
    signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.lt, true, true⟩, ⟨.eq, true, true⟩,
        ⟨.eq, true, false⟩, ⟨.gt, false, true⟩} =
      signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.lt, true, true⟩, ⟨.eq, true, false⟩,
          ⟨.eq, false, true⟩, ⟨.gt, false, true⟩} ∧
    signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.gt, true, false⟩, ⟨.lt, true, true⟩,
        ⟨.eq, true, false⟩, ⟨.eq, false, false⟩} =
      signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.gt, true, false⟩, ⟨.lt, true, true⟩,
          ⟨.eq, false, true⟩, ⟨.eq, false, false⟩}

Sources

• Toufik Mansour and Amir Safadi, Signed Inversion Sequences Avoiding a Set of Length-2 Signed Patterns, INTEGERS 26 (2026), Article A74, Theorem 12.

Uses 2

Statement usesLength-2 signed pattern · Number of signed inversion sequences avoiding a set of patterns

TheoremMansour–Safadi Theorem 13: a Wilf-equivalence of five-pattern sets#●ready to prove

Length-2 signed patterns are written as in the paper, a bar marking a barred letter, and \(B \sim C\) means that for every \(n \ge 0\) the number \(|\bar I_n(B)|\) of signed inversion sequences of length \(n\) avoiding every pattern of \(B\) equals \(|\bar I_n(C)|\). Then \(\{\bar1\bar0, \bar0\bar1, \bar00, \bar01, 1\bar0\} \sim \{\bar1\bar0, \bar0\bar1, \bar0\bar0, \bar01, 1\bar0\}\).

public theorem_wanted signedInvSeq_wilf_b1b0_b0b1_b00_b01_1b0 :
    signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.lt, true, true⟩, ⟨.eq, true, false⟩,
        ⟨.lt, true, false⟩, ⟨.gt, false, true⟩} =
      signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.lt, true, true⟩, ⟨.eq, true, true⟩,
          ⟨.lt, true, false⟩, ⟨.gt, false, true⟩}

Sources

• Toufik Mansour and Amir Safadi, Signed Inversion Sequences Avoiding a Set of Length-2 Signed Patterns, INTEGERS 26 (2026), Article A74, Theorem 13.

Uses 2

Statement usesLength-2 signed pattern · Number of signed inversion sequences avoiding a set of patterns

TheoremMansour–Safadi Theorem 14#●ready to prove

Write \(\bar{I}_n(B)\) for the set of signed inversion sequences of length \(n\) that avoid every length-2 signed pattern in \(B\), where a pattern is one of \(00\), \(01\), \(10\) with a bar over each barred letter. Let \(B_1 = \{\bar{1}0, \bar{0}\bar{1}, 0\bar{1}, 0\bar{0}, 1\bar{0}\}\), \(B_2 = \{\bar{1}\bar{0}, \bar{0}\bar{1}, 0\bar{1}, 0\bar{0}, 1\bar{0}\}\), \(B_3 = \{\bar{1}\bar{0}, \bar{1}0, \bar{0}\bar{0}, \bar{0}0, 0\bar{0}\}\), \(B_4 = \{\bar{1}\bar{0}, \bar{0}\bar{0}, 0\bar{1}, 0\bar{0}, 1\bar{0}\}\), \(B_5 = \{\bar{1}\bar{0}, \bar{0}\bar{1}, \bar{0}\bar{0}, 0\bar{1}, 1\bar{0}\}\), \(B_6 = \{\bar{1}0, \bar{0}\bar{1}, \bar{0}\bar{0}, 0\bar{1}, 1\bar{0}\}\), and \(B_7 = \{\bar{1}\bar{0}, \bar{1}0, \bar{0}\bar{0}, \bar{0}0, \bar{0}1\}\). Then for every \(n \ge 0\), \(|\bar{I}_n(B_1)| = |\bar{I}_n(B_2)| = |\bar{I}_n(B_3)| = |\bar{I}_n(B_4)| = |\bar{I}_n(B_5)| = |\bar{I}_n(B_6)| = |\bar{I}_n(B_7)|\).

MetaMathlibExt.signedInvSeq_wilf_b10_b0b1_0b1_0b0_1b0 · 25 lines

public theorem_wanted signedInvSeq_wilf_b10_b0b1_0b1_0b0_1b0 :
    signedInvAvoidCount {⟨.gt, true, false⟩, ⟨.lt, true, true⟩, ⟨.lt, false, true⟩,
        ⟨.eq, false, true⟩, ⟨.gt, false, true⟩} =
      signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.lt, true, true⟩, ⟨.lt, false, true⟩,
          ⟨.eq, false, true⟩, ⟨.gt, false, true⟩} ∧
    signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.lt, true, true⟩, ⟨.lt, false, true⟩,
        ⟨.eq, false, true⟩, ⟨.gt, false, true⟩} =
      signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.gt, true, false⟩, ⟨.eq, true, true⟩,
          ⟨.eq, true, false⟩, ⟨.eq, false, true⟩} ∧
    signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.gt, true, false⟩, ⟨.eq, true, true⟩,
        ⟨.eq, true, false⟩, ⟨.eq, false, true⟩} =
      signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.eq, true, true⟩, ⟨.lt, false, true⟩,
          ⟨.eq, false, true⟩, ⟨.gt, false, true⟩} ∧
    signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.eq, true, true⟩, ⟨.lt, false, true⟩,
        ⟨.eq, false, true⟩, ⟨.gt, false, true⟩} =
      signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.lt, true, true⟩, ⟨.eq, true, true⟩,
          ⟨.lt, false, true⟩, ⟨.gt, false, true⟩} ∧
    signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.lt, true, true⟩, ⟨.eq, true, true⟩,
        ⟨.lt, false, true⟩, ⟨.gt, false, true⟩} =
      signedInvAvoidCount {⟨.gt, true, false⟩, ⟨.lt, true, true⟩, ⟨.eq, true, true⟩,
          ⟨.lt, false, true⟩, ⟨.gt, false, true⟩} ∧
    signedInvAvoidCount {⟨.gt, true, false⟩, ⟨.lt, true, true⟩, ⟨.eq, true, true⟩,
        ⟨.lt, false, true⟩, ⟨.gt, false, true⟩} =
      signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.gt, true, false⟩, ⟨.eq, true, true⟩,
          ⟨.eq, true, false⟩, ⟨.lt, true, false⟩}

Sources

• Toufik Mansour and Amir Safadi, Signed Inversion Sequences Avoiding a Set of Length-2 Signed Patterns, INTEGERS 26 (2026), Article A74, Theorem 14.

Uses 2

Statement usesLength-2 signed pattern · Number of signed inversion sequences avoiding a set of patterns

TheoremMansour–Safadi Theorem 15#●ready to prove

Write \(\bar{I}_n(B)\) for the set of signed inversion sequences of length \(n\) that avoid every length-2 signed pattern in \(B\), where a pattern is one of \(00\), \(01\), \(10\) with a bar over each barred letter. Then for every \(n \ge 0\), \(|\bar{I}_n(\{\bar{1}\bar{0}, \bar{0}0, \bar{0}1, 0\bar{0}, 1\bar{0}\})| = |\bar{I}_n(\{\bar{1}\bar{0}, \bar{0}\bar{0}, \bar{0}1, 0\bar{0}, 1\bar{0}\})|\).

public theorem_wanted signedInvSeq_wilf_b1b0_b00_b01_0b0_1b0 :
    signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.eq, true, false⟩, ⟨.lt, true, false⟩,
        ⟨.eq, false, true⟩, ⟨.gt, false, true⟩} =
      signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.eq, true, true⟩, ⟨.lt, true, false⟩,
          ⟨.eq, false, true⟩, ⟨.gt, false, true⟩}

Sources

• Toufik Mansour and Amir Safadi, Signed Inversion Sequences Avoiding a Set of Length-2 Signed Patterns, INTEGERS 26 (2026), Article A74, Theorem 15.

Uses 2

Statement usesLength-2 signed pattern · Number of signed inversion sequences avoiding a set of patterns

TheoremMansour–Safadi Theorem 16: a Wilf-equivalence of six-pattern sets#●ready to prove

Length-2 signed patterns are written as in the paper, a bar marking a barred letter, and \(B \sim C\) means that for every \(n \ge 0\) the number \(|\bar I_n(B)|\) of signed inversion sequences of length \(n\) avoiding every pattern of \(B\) equals \(|\bar I_n(C)|\). Then \(\{\bar1\bar0, \bar10, \bar0\bar1, \bar00, \bar01, 0\bar0\} \sim \{\bar1\bar0, \bar10, \bar0\bar1, \bar0\bar0, \bar01, 0\bar0\}\).

public theorem_wanted signedInvSeq_wilf_b1b0_b10_b0b1_b00_b01_0b0 :
    signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.gt, true, false⟩, ⟨.lt, true, true⟩,
        ⟨.eq, true, false⟩, ⟨.lt, true, false⟩, ⟨.eq, false, true⟩} =
      signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.gt, true, false⟩, ⟨.lt, true, true⟩,
          ⟨.eq, true, true⟩, ⟨.lt, true, false⟩, ⟨.eq, false, true⟩}

Sources

• Toufik Mansour and Amir Safadi, Signed Inversion Sequences Avoiding a Set of Length-2 Signed Patterns, INTEGERS 26 (2026), Article A74, Theorem 16.

Uses 2

Statement usesLength-2 signed pattern · Number of signed inversion sequences avoiding a set of patterns

TheoremThree six-pattern sets with 2 · n! avoiders (Theorem 17)#●ready to prove

Write a length-2 signed pattern as \(\tau_1\tau_2\), where \(00\), \(01\) and \(10\) record whether \(|\tau_1|\) is equal to, smaller than or larger than \(|\tau_2|\) and a bar marks a barred letter, and write \(|\bar I_n(A)|\) for the number of signed inversion sequences of length \(n\) avoiding every pattern of a set \(A\) of such patterns. For every \(n \ge 1\) and each of the three sets \(A = \lbrace \bar 1\bar 0, \bar 1 0, \bar 0\bar 1, \bar 0\bar 0, \bar 0 0, 0\bar 1 \rbrace\), \(\lbrace \bar 1\bar 0, \bar 1 0, \bar 0\bar 1, \bar 0\bar 0, \bar 0 0, 0\bar 0 \rbrace\) and \(\lbrace \bar 1\bar 0, \bar 0\bar 1, \bar 0\bar 0, \bar 0 0, \bar 0 1, 1\bar 0 \rbrace\), we have \(|\bar I_n(A)| = 2 \cdot n!\).

public theorem_wanted signedInvAvoidCount_eq_two_mul_factorial :
    ∀ n, 1 ≤ n →
    signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.gt, true, false⟩, ⟨.lt, true, true⟩,
        ⟨.eq, true, true⟩, ⟨.eq, true, false⟩, ⟨.lt, false, true⟩} n = 2 * n ! ∧
    signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.gt, true, false⟩, ⟨.lt, true, true⟩,
        ⟨.eq, true, true⟩, ⟨.eq, true, false⟩, ⟨.eq, false, true⟩} n = 2 * n ! ∧
    signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.lt, true, true⟩, ⟨.eq, true, true⟩,
        ⟨.eq, true, false⟩, ⟨.lt, true, false⟩, ⟨.gt, false, true⟩} n = 2 * n !

Sources

• Toufik Mansour and Amir Safadi, Signed Inversion Sequences Avoiding a Set of Length-2 Signed Patterns, INTEGERS 26 (2026), Article A74, Theorem 17.

Uses 2

Statement usesLength-2 signed pattern · Number of signed inversion sequences avoiding a set of patterns

TheoremMansour–Safadi Theorem 18: a Wilf-equivalence of seven-pattern sets#●ready to prove

Length-2 signed patterns are written as in the paper, a bar marking a barred letter, and \(B \sim C\) means that for every \(n \ge 0\) the number \(|\bar I_n(B)|\) of signed inversion sequences of length \(n\) avoiding every pattern of \(B\) equals \(|\bar I_n(C)|\). Then \(\{\bar1\bar0, \bar10, \bar0\bar1, \bar0\bar0, \bar00, \bar01, 1\bar0\} \sim \{\bar1\bar0, \bar10, \bar0\bar0, \bar00, \bar01, 0\bar0, 1\bar0\}\).

public theorem_wanted signedInvSeq_wilf_b1b0_b10_b0b1_b0b0_b00_b01_1b0 :
    signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.gt, true, false⟩, ⟨.lt, true, true⟩,
        ⟨.eq, true, true⟩, ⟨.eq, true, false⟩, ⟨.lt, true, false⟩, ⟨.gt, false, true⟩} =
      signedInvAvoidCount {⟨.gt, true, true⟩, ⟨.gt, true, false⟩, ⟨.eq, true, true⟩,
          ⟨.eq, true, false⟩, ⟨.lt, true, false⟩, ⟨.eq, false, true⟩, ⟨.gt, false, true⟩}

Sources

• Toufik Mansour and Amir Safadi, Signed Inversion Sequences Avoiding a Set of Length-2 Signed Patterns, INTEGERS 26 (2026), Article A74, Theorem 18.

Uses 2

Statement usesLength-2 signed pattern · Number of signed inversion sequences avoiding a set of patterns

16 fully proved66 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.