Equilibrious words

DefinitionEquilibrious binary words#✓fully proved

A finite word \(u\) over the binary alphabet \(\{0, 1\}\) is equilibrious when the letters \(0\) and \(1\) occur the same number of times in \(u\).

The letters \(a\) and \(b\) of the source alphabet \(\Sigma = \{a, b\}\) are represented by \(0\) and \(1\).

public def IsEquilibriousWord (u : List (Fin 2)) : Prop :=
  u.count 0 = u.count 1

Sources

• https://cs.uwaterloo.ca/journals/JIS/VOL28/Coons/coons6.tex, lines 543–575.

Used by 5

Used byReversal preserves equilibrious words · Prepending an equilibrious word is undone by deletion · Prepending an equilibrious word shifts the position functions · Eventually linear relative position functions with positive slope · Relative positions of the Fibonacci word with an equilibrious word prepended

TheoremReversal preserves equilibrious words#✓fully proved

A finite word \(u\) over the binary alphabet \(\{0, 1\}\) is equilibrious if and only if its reversal is equilibrious.

public theorem isEquilibriousWord_reverse {u : List (Fin 2)} :
    IsEquilibriousWord u.reverse ↔ IsEquilibriousWord u

Uses 1

Statement usesEquilibrious binary words

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.