The literal deterministic rank table has width 6, initial state 0, and 99 rows

Abstract

The literal deterministic rank table has width 6, initial state 0, and 99 rows

Definition 1.1 (rankA).

$$rankA:ChunkRank$$

Formalization. D5/S1/Words/Palindromes/FridPrefix/RankA.rankA (✓ std3).

Source. Repository-derived.

Commentary.

The literal deterministic rank table has width 6, initial state 0, and 99 rows. State 98 is its dead state. transitions and weights are the two arrays printed in Lean; a numeric six-bit chunk labels each column.

References

• Truth anchor: D5/S1/Words/Palindromes/FridPrefix/RankA.rankA
• Dependency: D5/S1/Words/Palindromes/FridPrefix/RankAutomata