Reverse-permute equivalence of strings

Abbreviation\(k\)-strings#✓fully proved

For a natural number \(k\), a \(k\)-string is a finite sequence (possibly empty) of elements of \(\{0, 1, \ldots, k-1\}\).

public abbrev KString (k : ℕ) := List (Fin k)

Used by 1

Used byThe reverse-permute relation

DefinitionThe reverse-permute relation#✓fully proved

For a natural number \(k\), a \(k\)-string \(s\) is related to a \(k\)-string \(t\) by the reverse-permute (RP) relation when there is a permutation \(\sigma\) of \(\{0, 1, \ldots, k-1\}\) such that \(t\) is obtained, either from \(s\) or from the reversal of \(s\), by replacing each entry \(x\) with \(\sigma(x)\).

public def rpRelation (k : ℕ) (s t : KString k) : Prop :=
  ∃ σ : Equiv.Perm (Fin k), t = s.map (⇑σ) ∨ t = s.reverse.map (⇑σ)

Uses 1

Statement uses\(k\)-strings

2 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.