internlm/Lean-Github huggingface dataset:
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case inl.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.c
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.c 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.c X.c
Tactic:
repeat constructor
Proof state after:
no goals
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case inl.inl.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.c
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.c X.c
Tactic:
constructor
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
x y z : X
h1 : x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d
h2 : 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.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:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h1 : x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d
h2 : 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:
cases h1 <;> cases h2 <;> simp [*] at *
Proof state after:
case inl.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.b
⊢ 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.b X.b

case inl.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : 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) X.b X.d

case inr.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ 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.d X.b

case inr.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : 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) X.d X.d
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case inl.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.b
⊢ 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.b X.b

case inl.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : 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) X.b X.d

case inr.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ 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.d X.b

case inr.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : 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) X.d X.d
Tactic:
. exists X.b; repeat constructor
Proof state after:
case inl.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : 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) X.b X.d

case inr.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ 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.d X.b

case inr.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : 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) X.d X.d
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case inl.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : 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) X.b X.d

case inr.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ 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.d X.b

case inr.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : 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) X.d X.d
Tactic:
. exists X.d; constructor
  . constructor; simp [RX]; right; trivial
    constructor; simp [RX]; right; trivial
    constructor
  . constructor
Proof state after:
case inr.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ 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.d X.b

case inr.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : 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) X.d X.d
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case inr.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ 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.d X.b

case inr.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : 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) X.d X.d
Tactic:
. exists X.d; constructor
  . constructor
  . constructor; simp [RX]; right; trivial
    constructor; simp [RX]; right; trivial
    constructor
Proof state after:
case inr.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : 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) X.d X.d
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case inr.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : 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) X.d X.d
Tactic:
. exists X.d; repeat constructor
Proof state after:
no goals
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case inl.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.b
⊢ 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.b X.b
Tactic:
exists X.b
Proof state after:
case inl.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.b
⊢ 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.b X.b ∧
    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.b X.b
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case inl.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.b
⊢ 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.b X.b ∧
    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.b X.b
Tactic:
repeat constructor
Proof state after:
no goals
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case inl.inl.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.b
⊢ 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.b X.b
Tactic:
constructor
Proof state after:
no goals
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case inl.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : 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) X.b X.d
Tactic:
exists X.d
Proof state after:
case inl.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ 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.b X.d ∧
    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.d X.d
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case inl.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ 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.b X.d ∧
    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.d X.d
Tactic:
constructor
Proof state after:
case inl.inr.left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ 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.b X.d

case inl.inr.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ 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.d X.d
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case inl.inr.left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ 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.b X.d

case inl.inr.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ 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.d X.d
Tactic:
. constructor; simp [RX]; right; trivial
  constructor; simp [RX]; right; trivial
  constructor
Proof state after:
case inl.inr.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ 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.d X.d
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case inl.inr.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ 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.d X.d
Tactic:
. constructor
Proof state after:
no goals
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case inl.inr.left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ 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.b X.d
Tactic:
constructor
Proof state after:
case inl.inr.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ X.b = X.b ∧ ?inl.inr.left.b = X.a ∨
    X.b = X.b ∧ ?inl.inr.left.b = X.c ∨ X.b = X.c ∧ ?inl.inr.left.b = X.b ∨ X.b = X.c ∧ ?inl.inr.left.b = X.d

case inl.inr.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ 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)
    ?inl.inr.left.b X.d

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

case inl.inr.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ 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)
    ?inl.inr.left.b X.d

case inl.inr.left.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ X
Tactic:
simp [RX]
Proof state after:
case inl.inr.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ ?inl.inr.left.b = X.a ∨ ?inl.inr.left.b = X.c

case inl.inr.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ 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)
    ?inl.inr.left.b X.d

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

case inl.inr.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ 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)
    ?inl.inr.left.b X.d

case inl.inr.left.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ X
Tactic:
right
Proof state after:
case inl.inr.left.a.h
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ ?inl.inr.left.b = X.c

case inl.inr.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ 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)
    ?inl.inr.left.b X.d

case inl.inr.left.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ X
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case inl.inr.left.a.h
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ ?inl.inr.left.b = X.c

case inl.inr.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ 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)
    ?inl.inr.left.b X.d

case inl.inr.left.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ X
Tactic:
trivial
Proof state after:
case inl.inr.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ 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.c X.d
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case inl.inr.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ 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.c X.d
Tactic:
constructor
Proof state after:
case inl.inr.left.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ X.c = X.b ∧ ?inl.inr.left.a.b = X.a ∨
    X.c = X.b ∧ ?inl.inr.left.a.b = X.c ∨ X.c = X.c ∧ ?inl.inr.left.a.b = X.b ∨ X.c = X.c ∧ ?inl.inr.left.a.b = X.d

case inl.inr.left.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ 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)
    ?inl.inr.left.a.b X.d

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

case inl.inr.left.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ 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)
    ?inl.inr.left.a.b X.d

case inl.inr.left.a.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ X
Tactic:
simp [RX]
Proof state after:
case inl.inr.left.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ ?inl.inr.left.a.b = X.b ∨ ?inl.inr.left.a.b = X.d

case inl.inr.left.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ 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)
    ?inl.inr.left.a.b X.d

case inl.inr.left.a.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ X
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case inl.inr.left.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ ?inl.inr.left.a.b = X.b ∨ ?inl.inr.left.a.b = X.d

case inl.inr.left.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ 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)
    ?inl.inr.left.a.b X.d

case inl.inr.left.a.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ X
Tactic:
right
Proof state after:
case inl.inr.left.a.a.h
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ ?inl.inr.left.a.b = X.d

case inl.inr.left.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ 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)
    ?inl.inr.left.a.b X.d

case inl.inr.left.a.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ X
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case inl.inr.left.a.a.h
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ ?inl.inr.left.a.b = X.d

case inl.inr.left.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ 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)
    ?inl.inr.left.a.b X.d

case inl.inr.left.a.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ X
Tactic:
trivial
Proof state after:
case inl.inr.left.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ 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.d X.d
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case inl.inr.left.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ 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.d X.d
Tactic:
constructor
Proof state after:
no goals
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case inl.inr.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.b
h✝ : z = X.d
⊢ 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.d X.d
Tactic:
constructor
Proof state after:
no goals
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case inr.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ 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.d X.b
Tactic:
exists X.d
Proof state after:
case inr.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ 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.d X.d ∧
    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.b X.d
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case inr.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ 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.d X.d ∧
    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.b X.d
Tactic:
constructor
Proof state after:
case inr.inl.left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ 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.d X.d

case inr.inl.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ 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.b X.d
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case inr.inl.left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ 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.d X.d

case inr.inl.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ 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.b X.d
Tactic:
. constructor
Proof state after:
case inr.inl.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ 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.b X.d
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case inr.inl.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ 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.b X.d
Tactic:
. 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 inr.inl.left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ 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.d X.d
Tactic:
constructor
Proof state after:
no goals
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case inr.inl.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ 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.b X.d
Tactic:
constructor
Proof state after:
case inr.inl.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ X.b = X.b ∧ ?inr.inl.right.b = X.a ∨
    X.b = X.b ∧ ?inr.inl.right.b = X.c ∨ X.b = X.c ∧ ?inr.inl.right.b = X.b ∨ X.b = X.c ∧ ?inr.inl.right.b = X.d

case inr.inl.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ 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)
    ?inr.inl.right.b X.d

case inr.inl.right.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ X