internlm/Lean-Github huggingface dataset:
Theorem: confluent_implies_church_rosser
Proof state before:
case intro.intro.intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x✝ y✝ x y z : A
red_x_y : refl_trans_sym_clos R x y
red_y_z : refl_trans_sym_clos R y z
w1 : A
h11 : refl_trans_clos R x w1
h12 : refl_trans_clos R y w1
w2 : A
h21 : refl_trans_clos R y w2
h22 : refl_trans_clos R z w2
h' : wedge R w1 w2
⊢ joins R x z
Tactic:
have h := confl w1 w2 h'
Proof state after:
case intro.intro.intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x✝ y✝ x y z : A
red_x_y : refl_trans_sym_clos R x y
red_y_z : refl_trans_sym_clos R y z
w1 : A
h11 : refl_trans_clos R x w1
h12 : refl_trans_clos R y w1
w2 : A
h21 : refl_trans_clos R y w2
h22 : refl_trans_clos R z w2
h' : wedge R w1 w2
h : joins R w1 w2
⊢ joins R x z
Theorem: confluent_implies_church_rosser
Proof state before:
case intro.intro.intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x✝ y✝ x y z : A
red_x_y : refl_trans_sym_clos R x y
red_y_z : refl_trans_sym_clos R y z
w1 : A
h11 : refl_trans_clos R x w1
h12 : refl_trans_clos R y w1
w2 : A
h21 : refl_trans_clos R y w2
h22 : refl_trans_clos R z w2
h' : wedge R w1 w2
h : joins R w1 w2
⊢ joins R x z
Tactic:
cases' h with w h''
Proof state after:
case intro.intro.intro.intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x✝ y✝ x y z : A
red_x_y : refl_trans_sym_clos R x y
red_y_z : refl_trans_sym_clos R y z
w1 : A
h11 : refl_trans_clos R x w1
h12 : refl_trans_clos R y w1
w2 : A
h21 : refl_trans_clos R y w2
h22 : refl_trans_clos R z w2
h' : wedge R w1 w2
w : A
h'' : refl_trans_clos R w1 w ∧ refl_trans_clos R w2 w
⊢ joins R x z
Theorem: confluent_implies_church_rosser
Proof state before:
case intro.intro.intro.intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x✝ y✝ x y z : A
red_x_y : refl_trans_sym_clos R x y
red_y_z : refl_trans_sym_clos R y z
w1 : A
h11 : refl_trans_clos R x w1
h12 : refl_trans_clos R y w1
w2 : A
h21 : refl_trans_clos R y w2
h22 : refl_trans_clos R z w2
h' : wedge R w1 w2
w : A
h'' : refl_trans_clos R w1 w ∧ refl_trans_clos R w2 w
⊢ joins R x z
Tactic:
exists w
Proof state after:
case intro.intro.intro.intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x✝ y✝ x y z : A
red_x_y : refl_trans_sym_clos R x y
red_y_z : refl_trans_sym_clos R y z
w1 : A
h11 : refl_trans_clos R x w1
h12 : refl_trans_clos R y w1
w2 : A
h21 : refl_trans_clos R y w2
h22 : refl_trans_clos R z w2
h' : wedge R w1 w2
w : A
h'' : refl_trans_clos R w1 w ∧ refl_trans_clos R w2 w
⊢ refl_trans_clos R x w ∧ refl_trans_clos R z w
Theorem: confluent_implies_church_rosser
Proof state before:
case intro.intro.intro.intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x✝ y✝ x y z : A
red_x_y : refl_trans_sym_clos R x y
red_y_z : refl_trans_sym_clos R y z
w1 : A
h11 : refl_trans_clos R x w1
h12 : refl_trans_clos R y w1
w2 : A
h21 : refl_trans_clos R y w2
h22 : refl_trans_clos R z w2
h' : wedge R w1 w2
w : A
h'' : refl_trans_clos R w1 w ∧ refl_trans_clos R w2 w
⊢ refl_trans_clos R x w ∧ refl_trans_clos R z w
Tactic:
cases' h'' with h3 h4
Proof state after:
case intro.intro.intro.intro.intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x✝ y✝ x y z : A
red_x_y : refl_trans_sym_clos R x y
red_y_z : refl_trans_sym_clos R y z
w1 : A
h11 : refl_trans_clos R x w1
h12 : refl_trans_clos R y w1
w2 : A
h21 : refl_trans_clos R y w2
h22 : refl_trans_clos R z w2
h' : wedge R w1 w2
w : A
h3 : refl_trans_clos R w1 w
h4 : refl_trans_clos R w2 w
⊢ refl_trans_clos R x w ∧ refl_trans_clos R z w
Theorem: confluent_implies_church_rosser
Proof state before:
case intro.intro.intro.intro.intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x✝ y✝ x y z : A
red_x_y : refl_trans_sym_clos R x y
red_y_z : refl_trans_sym_clos R y z
w1 : A
h11 : refl_trans_clos R x w1
h12 : refl_trans_clos R y w1
w2 : A
h21 : refl_trans_clos R y w2
h22 : refl_trans_clos R z w2
h' : wedge R w1 w2
w : A
h3 : refl_trans_clos R w1 w
h4 : refl_trans_clos R w2 w
⊢ refl_trans_clos R x w ∧ refl_trans_clos R z w
Tactic:
constructor <;> apply refl_trans_clos_transitive <;> trivial
Proof state after:
no goals
Theorem: confluent_implies_church_rosser
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x✝ y✝ x y z : A
red_x_y : refl_trans_sym_clos R x y
red_y_z : refl_trans_sym_clos R y z
w1 : A
h11 : refl_trans_clos R x w1
h12 : refl_trans_clos R y w1
w2 : A
h21 : refl_trans_clos R y w2
h22 : refl_trans_clos R z w2
⊢ wedge R w1 w2
Tactic:
exists y
Proof state after:
no goals
Theorem: confluent_implies_church_rosser
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x y a✝¹ b✝ : A
a✝ : refl_trans_sym_clos R b✝ a✝¹
h : joins R b✝ a✝¹
⊢ joins R a✝¹ b✝
Tactic:
cases' h with w h'
Proof state after:
case intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x y a✝¹ b✝ : A
a✝ : refl_trans_sym_clos R b✝ a✝¹
w : A
h' : refl_trans_clos R b✝ w ∧ refl_trans_clos R a✝¹ w
⊢ joins R a✝¹ b✝
Theorem: confluent_implies_church_rosser
Proof state before:
case intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x y a✝¹ b✝ : A
a✝ : refl_trans_sym_clos R b✝ a✝¹
w : A
h' : refl_trans_clos R b✝ w ∧ refl_trans_clos R a✝¹ w
⊢ joins R a✝¹ b✝
Tactic:
cases' h' with h1 h2
Proof state after:
case intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x y a✝¹ b✝ : A
a✝ : refl_trans_sym_clos R b✝ a✝¹
w : A
h1 : refl_trans_clos R b✝ w
h2 : refl_trans_clos R a✝¹ w
⊢ joins R a✝¹ b✝
Theorem: confluent_implies_church_rosser
Proof state before:
case intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
confl : confluent R
x y a✝¹ b✝ : A
a✝ : refl_trans_sym_clos R b✝ a✝¹
w : A
h1 : refl_trans_clos R b✝ w
h2 : refl_trans_clos R a✝¹ w
⊢ joins R a✝¹ b✝
Tactic:
exists w
Proof state after:
no goals
Theorem: not_joins_a_d
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ ¬joins RX X.a X.d
Tactic:
intros h
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : joins RX X.a X.d
⊢ False
Theorem: not_joins_a_d
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : joins RX X.a X.d
⊢ False
Tactic:
cases' h with w h
Proof state after:
case intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
w : X
h : refl_trans_clos RX X.a w ∧ refl_trans_clos RX X.d w
⊢ False
Theorem: not_joins_a_d
Proof state before:
case intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
w : X
h : refl_trans_clos RX X.a w ∧ refl_trans_clos RX X.d w
⊢ False
Tactic:
cases' h with h1 h2
Proof state after:
case intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
w : X
h1 : refl_trans_clos RX X.a w
h2 : refl_trans_clos RX X.d w
⊢ False
Theorem: not_joins_a_d
Proof state before:
case intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
w : X
h1 : refl_trans_clos RX X.a w
h2 : refl_trans_clos RX X.d w
⊢ False
Tactic:
have eq_a : X.a = w := by
  apply normal_red RX <;> aesop
Proof state after:
case intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
w : X
h1 : refl_trans_clos RX X.a w
h2 : refl_trans_clos RX X.d w
eq_a : X.a = w
⊢ False
Theorem: not_joins_a_d
Proof state before:
case intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
w : X
h1 : refl_trans_clos RX X.a w
h2 : refl_trans_clos RX X.d w
eq_a : X.a = w
⊢ False
Tactic:
have eq_d : X.d = w := by
  apply normal_red RX <;> aesop
Proof state after:
case intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
w : X
h1 : refl_trans_clos RX X.a w
h2 : refl_trans_clos RX X.d w
eq_a : X.a = w
eq_d : X.d = w
⊢ False
Theorem: not_joins_a_d
Proof state before:
case intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
w : X
h1 : refl_trans_clos RX X.a w
h2 : refl_trans_clos RX X.d w
eq_a : X.a = w
eq_d : X.d = w
⊢ False
Tactic:
simp [← eq_a] at eq_d
Proof state after:
no goals
Theorem: not_joins_a_d
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
w : X
h1 : refl_trans_clos RX X.a w
h2 : refl_trans_clos RX X.d w
⊢ X.a = w
Tactic:
apply normal_red RX <;> aesop
Proof state after:
no goals
Theorem: not_joins_a_d
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
w : X
h1 : refl_trans_clos RX X.a w
h2 : refl_trans_clos RX X.d w
eq_a : X.a = w
⊢ X.d = w
Tactic:
apply normal_red RX <;> aesop
Proof state after:
no goals
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ ∃ A R, weakly_confluent R ∧ ¬confluent R
Tactic:
exists X, RX
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ weakly_confluent RX ∧ ¬confluent RX
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ weakly_confluent RX ∧ ¬confluent RX
Tactic:
constructor
Proof state after:
case left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ weakly_confluent RX

case right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ ¬confluent RX
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ weakly_confluent RX

case right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ ¬confluent RX
Tactic:
. intros x y z r_x_y r_x_z
  simp [*] at r_x_y
  simp [*] at r_x_z
  cases r_x_y <;> cases r_x_z <;> simp [*] at *
  . exists X.a; repeat constructor
  . exists X.a; try constructor
    . constructor
    . simp [*]; constructor; simp [RX]
      . left; trivial
      . constructor; simp [RX]; left; trivial; constructor
  . exists X.a; simp [*]; constructor
    . repeat (constructor; simp [RX]; left; trivial)
      constructor
    . constructor
  . case inr h1 h2 =>
    cases h1 <;> cases h2 <;> simp [*] at *
    . exists X.c; repeat constructor
    . case inr h1 h2 =>
      cases h1 <;> cases h2 <;> simp [*] at *
      . exists X.b; repeat constructor
      . exists X.d; constructor
        . constructor; simp [RX]; right; trivial
          constructor; simp [RX]; right; trivial
          constructor
        . constructor
      . exists X.d; constructor
        . constructor
        . constructor; simp [RX]; right; trivial
          constructor; simp [RX]; right; trivial
          constructor
      . exists X.d; repeat constructor
Proof state after:
case right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ ¬confluent RX
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ ¬confluent RX
Tactic:
. intros h
  apply not_joins_a_d
  apply h
  exists X.b; constructor
  . constructor
    simp [RX]
    left; trivial
    constructor
  . constructor
    simp [RX]
    right; trivial
    constructor
    . simp [RX]; right; trivial
    . constructor
Proof state after:
no goals
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ weakly_confluent RX
Tactic:
intros x y z r_x_y r_x_z
Proof state after:
case left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
r_x_y : RX x y
r_x_z : RX x z
⊢ joins RX y z
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
r_x_y : RX x y
r_x_z : RX x z
⊢ joins RX y z
Tactic:
simp [*] at r_x_y
Proof state after:
case left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
r_x_y : x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d
r_x_z : RX x z
⊢ joins RX y z
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
r_x_y : x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d
r_x_z : RX x z
⊢ joins RX y z
Tactic:
simp [*] at r_x_z
Proof state after:
case left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
r_x_y : x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d
r_x_z : x = X.b ∧ z = X.a ∨ x = X.b ∧ z = X.c ∨ x = X.c ∧ z = X.b ∨ x = X.c ∧ z = X.d
⊢ joins RX y z
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
r_x_y : x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d
r_x_z : x = X.b ∧ z = X.a ∨ x = X.b ∧ z = X.c ∨ x = X.c ∧ z = X.b ∨ x = X.c ∧ z = X.d
⊢ joins RX y z
Tactic:
cases r_x_y <;> cases r_x_z <;> simp [*] at *
Proof state after:
case left.inl.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.a
h✝ : z = X.a
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.a X.a

case left.inl.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.a z

case left.inr.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ z = X.a
h✝ : y = X.c
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) y X.a

case left.inr.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d
h✝ : x = X.b ∧ z = X.c ∨ x = X.c ∧ z = X.b ∨ x = X.c ∧ z = X.d
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) y z
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case left.inl.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.a
h✝ : z = X.a
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.a X.a

case left.inl.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.a z

case left.inr.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ z = X.a
h✝ : y = X.c
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) y X.a

case left.inr.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d
h✝ : x = X.b ∧ z = X.c ∨ x = X.c ∧ z = X.b ∨ x = X.c ∧ z = X.d
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) y z
Tactic:
. exists X.a; repeat constructor
Proof state after:
case left.inl.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.a z

case left.inr.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ z = X.a
h✝ : y = X.c
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) y X.a

case left.inr.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d
h✝ : x = X.b ∧ z = X.c ∨ x = X.c ∧ z = X.b ∨ x = X.c ∧ z = X.d
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) y z
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case left.inl.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.a z

case left.inr.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ z = X.a
h✝ : y = X.c
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) y X.a

case left.inr.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d
h✝ : x = X.b ∧ z = X.c ∨ x = X.c ∧ z = X.b ∨ x = X.c ∧ z = X.d
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) y z
Tactic:
. exists X.a; try constructor
  . constructor
  . simp [*]; constructor; simp [RX]
    . left; trivial
    . constructor; simp [RX]; left; trivial; constructor
Proof state after:
case left.inr.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ z = X.a
h✝ : y = X.c
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) y X.a

case left.inr.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d
h✝ : x = X.b ∧ z = X.c ∨ x = X.c ∧ z = X.b ∨ x = X.c ∧ z = X.d
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) y z
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case left.inr.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ z = X.a
h✝ : y = X.c
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) y X.a

case left.inr.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d
h✝ : x = X.b ∧ z = X.c ∨ x = X.c ∧ z = X.b ∨ x = X.c ∧ z = X.d
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) y z
Tactic:
. exists X.a; simp [*]; constructor
  . repeat (constructor; simp [RX]; left; trivial)
    constructor
  . constructor
Proof state after:
case left.inr.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d
h✝ : x = X.b ∧ z = X.c ∨ x = X.c ∧ z = X.b ∨ x = X.c ∧ z = X.d
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) y z
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case left.inr.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d
h✝ : x = X.b ∧ z = X.c ∨ x = X.c ∧ z = X.b ∨ x = X.c ∧ z = X.d
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) y z
Tactic:
. case inr h1 h2 =>
  cases h1 <;> cases h2 <;> simp [*] at *
  . exists X.c; repeat constructor
  . case inr h1 h2 =>
    cases h1 <;> cases h2 <;> simp [*] at *
    . exists X.b; repeat constructor
    . exists X.d; constructor
      . constructor; simp [RX]; right; trivial
        constructor; simp [RX]; right; trivial
        constructor
      . constructor
    . exists X.d; constructor
      . constructor
      . constructor; simp [RX]; right; trivial
        constructor; simp [RX]; right; trivial
        constructor
    . exists X.d; repeat constructor
Proof state after:
no goals
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case left.inl.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.a
h✝ : z = X.a
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.a X.a
Tactic:
exists X.a
Proof state after:
case left.inl.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.a
h✝ : z = X.a
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.a X.a ∧
    refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.a X.a
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case left.inl.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.a
h✝ : z = X.a
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.a X.a ∧
    refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.a X.a
Tactic:
repeat constructor
Proof state after:
no goals
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case left.inl.inl.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.a
h✝ : z = X.a
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.a X.a
Tactic:
constructor
Proof state after:
no goals
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case left.inl.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ joins (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.a z
Tactic:
exists X.a
Proof state after:
case left.inl.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.a X.a ∧
    refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) z X.a
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case left.inl.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.a X.a ∧
    refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) z X.a
Tactic:
try constructor
Proof state after:
case left.inl.inr.left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.a X.a

case left.inl.inr.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) z X.a
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case left.inl.inr.left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) X.a X.a

case left.inl.inr.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) z X.a
Tactic:
. constructor
Proof state after:
case left.inl.inr.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) z X.a
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case left.inl.inr.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : x = X.b ∧ y = X.a
h✝ : z = X.c
⊢ refl_trans_clos (fun x y => x = X.b ∧ y = X.a ∨ x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d) z X.a
Tactic:
. simp [*]; constructor; simp [RX]
  . left; trivial
  . constructor; simp [RX]; left; trivial; constructor
Proof state after:
no goals