Elementary interfaces used by the priority reflection proof #
theorem
Undecidability.Thue.Matiyasevich1993.Compression.source_binary_iff
{n r : ℕ}
(F E : Fin r → List (Fin n))
(X Y : List (Fin n))
:
ThueEq (finiteSystem F E) X Y ↔ ThueEq (binarySystem F E) ((Precompression.embedding F E).encode X) ((Precompression.embedding F E).encode Y)
The contextual form of equation (25) needed by the reflection induction.
The hypotheses say that all e letters are in the left context of the
displayed long side.
Equations
- One or more equations did not get rendered due to their size.
Instances For
theorem
Undecidability.Thue.Matiyasevich1993.Compression.decode_reachable_of_contextual
{n r : ℕ}
(hselect : ContextualReplacement)
(F E : Fin r → List (Fin n))
(X : List (Fin n))
{W : List Priority.A₂}
(h : ThueEq (stage₂System (leftLong F E) (rightLong F E)) (priorityEncode F E X) W)
:
∃ (B : List (Fin 2)),
ThueEq (binarySystem F E) ((Precompression.embedding F E).encode X) B ∧ Priority.firstNormal W = Priority.encode (u n r) B
Equation (25), packaged as the invariant needed in the remainder of the construction: every reachable word has the normal form of a reachable binary word.
theorem
Undecidability.Thue.Matiyasevich1993.Compression.reachableNoAAA_of_contextual
{n r : ℕ}
(hselect : ContextualReplacement)
(F E : Fin r → List (Fin n))
(X : List (Fin n))
:
Priority.ReachableNoAAA (leftLong F E) (rightLong F E) (priorityEncode F E X)
theorem
Undecidability.Thue.Matiyasevich1993.Compression.priority_thueEq_iff_of_contextual
{n r : ℕ}
(hselect : ContextualReplacement)
(F E : Fin r → List (Fin n))
(X Y : List (Fin n))
:
ThueEq (finiteSystem F E) X Y ↔ ThueEq (stage₂System (leftLong F E) (rightLong F E)) (priorityEncode F E X) (priorityEncode F E Y)
theorem
Undecidability.Thue.Matiyasevich1993.Compression.priorityBridge_of_contextual
{n r : ℕ}
(hselect : ContextualReplacement)
(F E : Fin r → List (Fin n))
:
PriorityBridge F E
Matiyasevich's complete finite-system compression theorem.