English
If (x,b) :: L1 reduces to L2, then Red L1 [(x, not b)] and Red ((x,b) :: L1) L2 relate by a standard left-cancellation step.
Русский
Если (x,b) :: L1 редуцируется до L2, то L1 и (x, not b) образуют совместную редукцию с L2 через левую отмену.
LaTeX
$$$Red((x,b) :: L_1, L_2) \iff Red(L_1, (x, \text{not } b) :: L_2)$$$
Lean4
/-- If `x` is a letter and `w` is a word such that `xw` reduces to the empty word, then `w` reduces
to `x⁻¹` -/
@[to_additive /-- If `x` is a letter and `w` is a word such that `x + w` reduces to the empty word, then `w`
reduces to `-x`. -/
]
theorem cons_nil_iff_singleton {x b} : Red ((x, b) :: L) [] ↔ Red L [(x, not b)] :=
Iff.intro
(fun h => by
have h₁ : Red ((x, not b) :: (x, b) :: L) [(x, not b)] := cons_cons h
have h₂ : Red ((x, not b) :: (x, b) :: L) L := ReflTransGen.single Step.cons_not_rev
let ⟨L', h₁, h₂⟩ := church_rosser h₁ h₂
rw [singleton_iff] at h₁
subst L'
assumption)
fun h => (cons_cons h).tail Step.cons_not
