English
If the heads x1,b1 and x2,b2 are distinct and Red holds for (x1,b1) :: L1 to L2 and (x2,b2) :: L2 to L3, then Red L1 to (x1, not b1) :: (x2,b2) :: L2.
Русский
Если головы x1,b1 и x2,b2 различны, и существует редукция от (x1,b1) :: L1 к (x2,b2) :: L2, то существует редукция от L1 к (x1, not b1) :: (x2,b2) :: L2.
LaTeX
$$$\forall x_1,b_1,x_2,b_2,\; (x_1,b_1) \ne (x_2,b_2) \Rightarrow Red((x_1,b_1) :: L_1, (x_2,b_2) :: L_2) \Rightarrow Red\,L_1\ ((x_1, \neg b_1) :: (x_2,b_2) :: L_2)$$$
Lean4
/-- If `x` and `y` are distinct letters and `w₁ w₂` are words such that `xw₁` reduces to `yw₂`, then
`w₁` reduces to `x⁻¹yw₂`. -/
@[to_additive /-- If `x` and `y` are distinct letters and `w₁ w₂` are words such that `x + w₁`
reduces to `y + w₂`, then `w₁` reduces to `-x + y + w₂`. -/
]
theorem inv_of_red_of_ne {x1 b1 x2 b2} (H1 : (x1, b1) ≠ (x2, b2)) (H2 : Red ((x1, b1) :: L₁) ((x2, b2) :: L₂)) :
Red L₁ ((x1, not b1) :: (x2, b2) :: L₂) :=
by
have : Red ((x1, b1) :: L₁) ([(x2, b2)] ++ L₂) := H2
rcases to_append_iff.1 this with ⟨_ | ⟨p, L₃⟩, L₄, eq, h₁, h₂⟩
· simp [nil_iff] at h₁
· cases eq
change Red (L₃ ++ L₄) ([(x1, not b1), (x2, b2)] ++ L₂)
apply append_append _ h₂
have h₁ : Red ((x1, not b1) :: (x1, b1) :: L₃) [(x1, not b1), (x2, b2)] := cons_cons h₁
have h₂ : Red ((x1, not b1) :: (x1, b1) :: L₃) L₃ := Step.cons_not_rev.to_red
rcases church_rosser h₁ h₂ with ⟨L', h₁, h₂⟩
rw [red_iff_irreducible H1] at h₁
rwa [h₁] at h₂
