α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
H1 : (x1, b1) ≠ (x2, b2)
H2 : Red ((x1, b1) :: L₁) ((x2, b2) :: L₂)
this : Red ((x1, b1) :: L₁) ([(x2, b2)] ++ L₂)
⊢ Red L₁ ((x1, !b1) :: (x2, b2) :: L₂)
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
H1 : (x1, b1) ≠ (x2, b2)
H2 : Red ((x1, b1) :: L₁) ((x2, b2) :: L₂)
⊢ Red L₁ ((x1, !b1) :: (x2, b2) :: L₂)
have : Red ((x1, b1) :: L₁) ([(x2, b2)] ++ L₂) := H2
case intro.nil.intro.intro.intro
α : Type u
L L₁ L₂ L₃ L₄✝ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
H1 : (x1, b1) ≠ (x2, b2)
H2 : Red ((x1, b1) :: L₁) ((x2, b2) :: L₂)
this : Red ((x1, b1) :: L₁) ([(x2, b2)] ++ L₂)
L₄ : List (α × Bool)
eq : (x1, b1) :: L₁ = [] ++ L₄
h₁ : Red [] [(x2, b2)]
h₂ : Red L₄ L₂
⊢ Red L₁ ((x1, !b1) :: (x2, b2) :: L₂)

case intro.cons.intro.intro.intro
α : Type u
L L₁ L₂ L₃✝ L₄✝ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
H1 : (x1, b1) ≠ (x2, b2)
H2 : Red ((x1, b1) :: L₁) ((x2, b2) :: L₂)
this : Red ((x1, b1) :: L₁) ([(x2, b2)] ++ L₂)
p : α × Bool
L₃ L₄ : List (α × Bool)
eq : (x1, b1) :: L₁ = p :: L₃ ++ L₄
h₁ : Red (p :: L₃) [(x2, b2)]
h₂ : Red L₄ L₂
⊢ Red L₁ ((x1, !b1) :: (x2, b2) :: L₂)
α : Type u
L L₁ L₂ L₃ L₄ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
H1 : (x1, b1) ≠ (x2, b2)
H2 : Red ((x1, b1) :: L₁) ((x2, b2) :: L₂)
this : Red ((x1, b1) :: L₁) ([(x2, b2)] ++ L₂)
⊢ Red L₁ ((x1, !b1) :: (x2, b2) :: L₂)
rcases to_append_iff.1 this with ⟨_ | ⟨p, L₃⟩, L₄, eq, h₁, h₂⟩
no goals
case intro.nil.intro.intro.intro
α : Type u
L L₁ L₂ L₃ L₄✝ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
H1 : (x1, b1) ≠ (x2, b2)
H2 : Red ((x1, b1) :: L₁) ((x2, b2) :: L₂)
this : Red ((x1, b1) :: L₁) ([(x2, b2)] ++ L₂)
L₄ : List (α × Bool)
eq : (x1, b1) :: L₁ = [] ++ L₄
h₁ : Red [] [(x2, b2)]
h₂ : Red L₄ L₂
⊢ Red L₁ ((x1, !b1) :: (x2, b2) :: L₂)
simp [nil_iff] at h₁
case intro.cons.intro.intro.intro.refl
α : Type u
L L₂ L₃✝ L₄✝ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
H1 : (x1, b1) ≠ (x2, b2)
L₃ L₄ : List (α × Bool)
h₂ : Red L₄ L₂
h₁ : Red ((x1, b1) :: L₃) [(x2, b2)]
H2 : Red ((x1, b1) :: List.append L₃ L₄) ((x2, b2) :: L₂)
this : Red ((x1, b1) :: List.append L₃ L₄) ([(x2, b2)] ++ L₂)
⊢ Red (List.append L₃ L₄) ((x1, !b1) :: (x2, b2) :: L₂)
case intro.cons.intro.intro.intro
α : Type u
L L₁ L₂ L₃✝ L₄✝ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
H1 : (x1, b1) ≠ (x2, b2)
H2 : Red ((x1, b1) :: L₁) ((x2, b2) :: L₂)
this : Red ((x1, b1) :: L₁) ([(x2, b2)] ++ L₂)
p : α × Bool
L₃ L₄ : List (α × Bool)
eq : (x1, b1) :: L₁ = p :: L₃ ++ L₄
h₁ : Red (p :: L₃) [(x2, b2)]
h₂ : Red L₄ L₂
⊢ Red L₁ ((x1, !b1) :: (x2, b2) :: L₂)
cases eq
case intro.cons.intro.intro.intro.refl
α : Type u
L L₂ L₃✝ L₄✝ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
H1 : (x1, b1) ≠ (x2, b2)
L₃ L₄ : List (α × Bool)
h₂ : Red L₄ L₂
h₁ : Red ((x1, b1) :: L₃) [(x2, b2)]
H2 : Red ((x1, b1) :: List.append L₃ L₄) ((x2, b2) :: L₂)
this : Red ((x1, b1) :: List.append L₃ L₄) ([(x2, b2)] ++ L₂)
⊢ Red (L₃ ++ L₄) ([(x1, !b1), (x2, b2)] ++ L₂)
case intro.cons.intro.intro.intro.refl
α : Type u
L L₂ L₃✝ L₄✝ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
H1 : (x1, b1) ≠ (x2, b2)
L₃ L₄ : List (α × Bool)
h₂ : Red L₄ L₂
h₁ : Red ((x1, b1) :: L₃) [(x2, b2)]
H2 : Red ((x1, b1) :: List.append L₃ L₄) ((x2, b2) :: L₂)
this : Red ((x1, b1) :: List.append L₃ L₄) ([(x2, b2)] ++ L₂)
⊢ Red (List.append L₃ L₄) ((x1, !b1) :: (x2, b2) :: L₂)
show Red (L₃ ++ L₄) ([(x1, not b1), (x2, b2)] ++ L₂)
α : Type u
L L₂ L₃✝ L₄✝ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
H1 : (x1, b1) ≠ (x2, b2)
L₃ L₄ : List (α × Bool)
h₂ : Red L₄ L₂
h₁ : Red ((x1, b1) :: L₃) [(x2, b2)]
H2 : Red ((x1, b1) :: List.append L₃ L₄) ((x2, b2) :: L₂)
this : Red ((x1, b1) :: List.append L₃ L₄) ([(x2, b2)] ++ L₂)
⊢ Red L₃ [(x1, !b1), (x2, b2)]
case intro.cons.intro.intro.intro.refl
α : Type u
L L₂ L₃✝ L₄✝ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
H1 : (x1, b1) ≠ (x2, b2)
L₃ L₄ : List (α × Bool)
h₂ : Red L₄ L₂
h₁ : Red ((x1, b1) :: L₃) [(x2, b2)]
H2 : Red ((x1, b1) :: List.append L₃ L₄) ((x2, b2) :: L₂)
this : Red ((x1, b1) :: List.append L₃ L₄) ([(x2, b2)] ++ L₂)
⊢ Red (L₃ ++ L₄) ([(x1, !b1), (x2, b2)] ++ L₂)
apply append_append _ h₂
α : Type u
L L₂ L₃✝ L₄✝ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
H1 : (x1, b1) ≠ (x2, b2)
L₃ L₄ : List (α × Bool)
h₂ : Red L₄ L₂
h₁✝ : Red ((x1, b1) :: L₃) [(x2, b2)]
H2 : Red ((x1, b1) :: List.append L₃ L₄) ((x2, b2) :: L₂)
this : Red ((x1, b1) :: List.append L₃ L₄) ([(x2, b2)] ++ L₂)
h₁ : Red ((x1, !b1) :: (x1, b1) :: L₃) [(x1, !b1), (x2, b2)]
⊢ Red L₃ [(x1, !b1), (x2, b2)]
α : Type u
L L₂ L₃✝ L₄✝ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
H1 : (x1, b1) ≠ (x2, b2)
L₃ L₄ : List (α × Bool)
h₂ : Red L₄ L₂
h₁ : Red ((x1, b1) :: L₃) [(x2, b2)]
H2 : Red ((x1, b1) :: List.append L₃ L₄) ((x2, b2) :: L₂)
this : Red ((x1, b1) :: List.append L₃ L₄) ([(x2, b2)] ++ L₂)
⊢ Red L₃ [(x1, !b1), (x2, b2)]
have h₁ : Red ((x1, not b1) :: (x1, b1) :: L₃) [(x1, not b1), (x2, b2)] := cons_cons h₁
α : Type u
L L₂ L₃✝ L₄✝ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
H1 : (x1, b1) ≠ (x2, b2)
L₃ L₄ : List (α × Bool)
h₂✝ : Red L₄ L₂
h₁✝ : Red ((x1, b1) :: L₃) [(x2, b2)]
H2 : Red ((x1, b1) :: List.append L₃ L₄) ((x2, b2) :: L₂)
this : Red ((x1, b1) :: List.append L₃ L₄) ([(x2, b2)] ++ L₂)
h₁ : Red ((x1, !b1) :: (x1, b1) :: L₃) [(x1, !b1), (x2, b2)]
h₂ : Red ((x1, !b1) :: (x1, b1) :: L₃) L₃
⊢ Red L₃ [(x1, !b1), (x2, b2)]
α : Type u
L L₂ L₃✝ L₄✝ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
H1 : (x1, b1) ≠ (x2, b2)
L₃ L₄ : List (α × Bool)
h₂ : Red L₄ L₂
h₁✝ : Red ((x1, b1) :: L₃) [(x2, b2)]
H2 : Red ((x1, b1) :: List.append L₃ L₄) ((x2, b2) :: L₂)
this : Red ((x1, b1) :: List.append L₃ L₄) ([(x2, b2)] ++ L₂)
h₁ : Red ((x1, !b1) :: (x1, b1) :: L₃) [(x1, !b1), (x2, b2)]
⊢ Red L₃ [(x1, !b1), (x2, b2)]
have h₂ : Red ((x1, not b1) :: (x1, b1) :: L₃) L₃ := Step.cons_not_rev.to_red
case intro.intro
α : Type u
L L₂ L₃✝ L₄✝ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
H1 : (x1, b1) ≠ (x2, b2)
L₃ L₄ : List (α × Bool)
h₂✝¹ : Red L₄ L₂
h₁✝¹ : Red ((x1, b1) :: L₃) [(x2, b2)]
H2 : Red ((x1, b1) :: List.append L₃ L₄) ((x2, b2) :: L₂)
this : Red ((x1, b1) :: List.append L₃ L₄) ([(x2, b2)] ++ L₂)
h₁✝ : Red ((x1, !b1) :: (x1, b1) :: L₃) [(x1, !b1), (x2, b2)]
h₂✝ : Red ((x1, !b1) :: (x1, b1) :: L₃) L₃
L' : List (α × Bool)
h₁ : Red [(x1, !b1), (x2, b2)] L'
h₂ : Red L₃ L'
⊢ Red L₃ [(x1, !b1), (x2, b2)]
α : Type u
L L₂ L₃✝ L₄✝ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
H1 : (x1, b1) ≠ (x2, b2)
L₃ L₄ : List (α × Bool)
h₂✝ : Red L₄ L₂
h₁✝ : Red ((x1, b1) :: L₃) [(x2, b2)]
H2 : Red ((x1, b1) :: List.append L₃ L₄) ((x2, b2) :: L₂)
this : Red ((x1, b1) :: List.append L₃ L₄) ([(x2, b2)] ++ L₂)
h₁ : Red ((x1, !b1) :: (x1, b1) :: L₃) [(x1, !b1), (x2, b2)]
h₂ : Red ((x1, !b1) :: (x1, b1) :: L₃) L₃
⊢ Red L₃ [(x1, !b1), (x2, b2)]
rcases church_rosser h₁ h₂ with ⟨L', h₁, h₂⟩
case intro.intro
α : Type u
L L₂ L₃✝ L₄✝ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
H1 : (x1, b1) ≠ (x2, b2)
L₃ L₄ : List (α × Bool)
h₂✝¹ : Red L₄ L₂
h₁✝¹ : Red ((x1, b1) :: L₃) [(x2, b2)]
H2 : Red ((x1, b1) :: List.append L₃ L₄) ((x2, b2) :: L₂)
this : Red ((x1, b1) :: List.append L₃ L₄) ([(x2, b2)] ++ L₂)
h₁✝ : Red ((x1, !b1) :: (x1, b1) :: L₃) [(x1, !b1), (x2, b2)]
h₂✝ : Red ((x1, !b1) :: (x1, b1) :: L₃) L₃
L' : List (α × Bool)
h₁ : L' = [(x1, !b1), (x2, b2)]
h₂ : Red L₃ L'
⊢ Red L₃ [(x1, !b1), (x2, b2)]
case intro.intro
α : Type u
L L₂ L₃✝ L₄✝ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
H1 : (x1, b1) ≠ (x2, b2)
L₃ L₄ : List (α × Bool)
h₂✝¹ : Red L₄ L₂
h₁✝¹ : Red ((x1, b1) :: L₃) [(x2, b2)]
H2 : Red ((x1, b1) :: List.append L₃ L₄) ((x2, b2) :: L₂)
this : Red ((x1, b1) :: List.append L₃ L₄) ([(x2, b2)] ++ L₂)
h₁✝ : Red ((x1, !b1) :: (x1, b1) :: L₃) [(x1, !b1), (x2, b2)]
h₂✝ : Red ((x1, !b1) :: (x1, b1) :: L₃) L₃
L' : List (α × Bool)
h₁ : Red [(x1, !b1), (x2, b2)] L'
h₂ : Red L₃ L'
⊢ Red L₃ [(x1, !b1), (x2, b2)]
rw [red_iff_irreducible H1] at h₁
no goals
case intro.intro
α : Type u
L L₂ L₃✝ L₄✝ : List (α × Bool)
x1 : α
b1 : Bool
x2 : α
b2 : Bool
H1 : (x1, b1) ≠ (x2, b2)
L₃ L₄ : List (α × Bool)
h₂✝¹ : Red L₄ L₂
h₁✝¹ : Red ((x1, b1) :: L₃) [(x2, b2)]
H2 : Red ((x1, b1) :: List.append L₃ L₄) ((x2, b2) :: L₂)
this : Red ((x1, b1) :: List.append L₃ L₄) ([(x2, b2)] ++ L₂)
h₁✝ : Red ((x1, !b1) :: (x1, b1) :: L₃) [(x1, !b1), (x2, b2)]
h₂✝ : Red ((x1, !b1) :: (x1, b1) :: L₃) L₃
L' : List (α × Bool)
h₁ : L' = [(x1, !b1), (x2, b2)]
h₂ : Red L₃ L'
⊢ Red L₃ [(x1, !b1), (x2, b2)]
rwa [h₁] at h₂