internlm/Lean-Github huggingface dataset:
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:
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
Tactic:
constructor
Proof state after:
no goals
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 [*]
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) X.c 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) X.c X.a
Tactic:
constructor
Proof state after:
case left.inl.inr.right.a
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
⊢ X.c = X.b ∧ ?left.inl.inr.right.b = X.a ∨
    X.c = X.b ∧ ?left.inl.inr.right.b = X.c ∨
      X.c = X.c ∧ ?left.inl.inr.right.b = X.b ∨ X.c = X.c ∧ ?left.inl.inr.right.b = X.d

case left.inl.inr.right.a
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)
    ?left.inl.inr.right.b X.a

case left.inl.inr.right.b
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
⊢ X
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case left.inl.inr.right.a
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
⊢ X.c = X.b ∧ ?left.inl.inr.right.b = X.a ∨
    X.c = X.b ∧ ?left.inl.inr.right.b = X.c ∨
      X.c = X.c ∧ ?left.inl.inr.right.b = X.b ∨ X.c = X.c ∧ ?left.inl.inr.right.b = X.d

case left.inl.inr.right.a
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)
    ?left.inl.inr.right.b X.a

case left.inl.inr.right.b
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
⊢ X
Tactic:
simp [RX]
Proof state after:
case left.inl.inr.right.a
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
⊢ ?left.inl.inr.right.b = X.b ∨ ?left.inl.inr.right.b = X.d

case left.inl.inr.right.a
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)
    ?left.inl.inr.right.b X.a

case left.inl.inr.right.b
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
⊢ X
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case left.inl.inr.right.a
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
⊢ ?left.inl.inr.right.b = X.b ∨ ?left.inl.inr.right.b = X.d

case left.inl.inr.right.a
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)
    ?left.inl.inr.right.b X.a

case left.inl.inr.right.b
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
⊢ X
Tactic:
. left; trivial
Proof state after:
case left.inl.inr.right.a
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.b X.a
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case left.inl.inr.right.a
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.b X.a
Tactic:
. constructor; simp [RX]; left; trivial; constructor
Proof state after:
no goals
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case left.inl.inr.right.a
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
⊢ ?left.inl.inr.right.b = X.b ∨ ?left.inl.inr.right.b = X.d
Tactic:
left
Proof state after:
case left.inl.inr.right.a.h
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
⊢ ?left.inl.inr.right.b = X.b
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case left.inl.inr.right.a.h
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
⊢ ?left.inl.inr.right.b = X.b
Tactic:
trivial
Proof state after:
no goals
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case left.inl.inr.right.a
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.b X.a
Tactic:
constructor
Proof state after:
case left.inl.inr.right.a.a
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
⊢ X.b = X.b ∧ ?left.inl.inr.right.a.b = X.a ∨
    X.b = X.b ∧ ?left.inl.inr.right.a.b = X.c ∨
      X.b = X.c ∧ ?left.inl.inr.right.a.b = X.b ∨ X.b = X.c ∧ ?left.inl.inr.right.a.b = X.d

case left.inl.inr.right.a.a
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)
    ?left.inl.inr.right.a.b X.a

case left.inl.inr.right.a.b
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
⊢ X
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case left.inl.inr.right.a.a
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
⊢ X.b = X.b ∧ ?left.inl.inr.right.a.b = X.a ∨
    X.b = X.b ∧ ?left.inl.inr.right.a.b = X.c ∨
      X.b = X.c ∧ ?left.inl.inr.right.a.b = X.b ∨ X.b = X.c ∧ ?left.inl.inr.right.a.b = X.d

case left.inl.inr.right.a.a
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)
    ?left.inl.inr.right.a.b X.a

case left.inl.inr.right.a.b
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
⊢ X
Tactic:
simp [RX]
Proof state after:
case left.inl.inr.right.a.a
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
⊢ ?left.inl.inr.right.a.b = X.a ∨ ?left.inl.inr.right.a.b = X.c

case left.inl.inr.right.a.a
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)
    ?left.inl.inr.right.a.b X.a

case left.inl.inr.right.a.b
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
⊢ X
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case left.inl.inr.right.a.a
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
⊢ ?left.inl.inr.right.a.b = X.a ∨ ?left.inl.inr.right.a.b = X.c

case left.inl.inr.right.a.a
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)
    ?left.inl.inr.right.a.b X.a

case left.inl.inr.right.a.b
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
⊢ X
Tactic:
left
Proof state after:
case left.inl.inr.right.a.a.h
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
⊢ ?left.inl.inr.right.a.b = X.a

case left.inl.inr.right.a.a
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)
    ?left.inl.inr.right.a.b X.a

case left.inl.inr.right.a.b
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
⊢ X
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case left.inl.inr.right.a.a.h
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
⊢ ?left.inl.inr.right.a.b = X.a

case left.inl.inr.right.a.a
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)
    ?left.inl.inr.right.a.b X.a

case left.inl.inr.right.a.b
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
⊢ X
Tactic:
trivial
Proof state after:
case left.inl.inr.right.a.a
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
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case left.inl.inr.right.a.a
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
Tactic:
constructor
Proof state after:
no goals
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
Tactic:
exists X.a
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
⊢ 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) y 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.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
⊢ 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) y 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:
simp [*]
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
⊢ 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.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.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
⊢ 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.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:
case left.inr.inl.left
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
⊢ 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.a

case left.inr.inl.right
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
⊢ 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.inr.inl.left
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
⊢ 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.a

case left.inr.inl.right
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
⊢ 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; simp [RX]; left; trivial)
  constructor
Proof state after:
case left.inr.inl.right
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
⊢ 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.inr.inl.right
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
⊢ 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.inr.inl.left
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
⊢ 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.a
Tactic:
repeat (constructor; simp [RX]; left; trivial)
Proof state after:
case left.inr.inl.left.a.a
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
⊢ 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.inr.inl.left.a.a
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
⊢ 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.inr.inl.left.a.a
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
⊢ 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; simp [RX]; left; trivial)
Proof state after:
no goals
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case left.inr.inl.left.a.a
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
⊢ X.b = X.b ∧ ?left.inr.inl.left.a.b = X.a ∨
    X.b = X.b ∧ ?left.inr.inl.left.a.b = X.c ∨
      X.b = X.c ∧ ?left.inr.inl.left.a.b = X.b ∨ X.b = X.c ∧ ?left.inr.inl.left.a.b = X.d

case left.inr.inl.left.a.a
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
⊢ 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)
    ?left.inr.inl.left.a.b X.a

case left.inr.inl.left.a.b
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
⊢ X
Tactic:
simp [RX]
Proof state after:
case left.inr.inl.left.a.a
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
⊢ ?left.inr.inl.left.a.b = X.a ∨ ?left.inr.inl.left.a.b = X.c

case left.inr.inl.left.a.a
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
⊢ 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)
    ?left.inr.inl.left.a.b X.a

case left.inr.inl.left.a.b
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
⊢ X
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case left.inr.inl.left.a.a
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
⊢ ?left.inr.inl.left.a.b = X.a ∨ ?left.inr.inl.left.a.b = X.c

case left.inr.inl.left.a.a
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
⊢ 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)
    ?left.inr.inl.left.a.b X.a

case left.inr.inl.left.a.b
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
⊢ X
Tactic:
left
Proof state after:
case left.inr.inl.left.a.a.h
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
⊢ ?left.inr.inl.left.a.b = X.a

case left.inr.inl.left.a.a
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
⊢ 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)
    ?left.inr.inl.left.a.b X.a

case left.inr.inl.left.a.b
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
⊢ X
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case left.inr.inl.left.a.a.h
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
⊢ ?left.inr.inl.left.a.b = X.a

case left.inr.inl.left.a.a
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
⊢ 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)
    ?left.inr.inl.left.a.b X.a

case left.inr.inl.left.a.b
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
⊢ X
Tactic:
trivial
Proof state after:
case left.inr.inl.left.a.a
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
⊢ 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.inr.inl.right
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
⊢ 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:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h1 : x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d
h2 : 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:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h1 : x = X.b ∧ y = X.c ∨ x = X.c ∧ y = X.b ∨ x = X.c ∧ y = X.d
h2 : 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:
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.c
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.c X.c

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

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