internlm/Lean-Github huggingface dataset:
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
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
Tactic:
simp [RX]
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
⊢ ?inr.inl.right.b = X.a ∨ ?inr.inl.right.b = X.c

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

case inr.inl.right.a.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
h✝ : z = X.b
⊢ X
Tactic:
trivial
Proof state after:
case inr.inl.right.a.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) X.d X.d
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case inr.inl.right.a.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) X.d X.d
Tactic:
constructor
Proof state after:
no goals
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
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
⊢ 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.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
⊢ 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.d X.d
Tactic:
repeat constructor
Proof state after:
no goals
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case inr.inr.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
x y z : X
h✝¹ : y = X.d
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 right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ ¬confluent RX
Tactic:
intros h
Proof state after:
case right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ False
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ False
Tactic:
apply not_joins_a_d
Proof state after:
case right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ joins RX X.a X.d
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ joins RX X.a X.d
Tactic:
apply h
Proof state after:
case right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ wedge RX X.a X.d
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ wedge RX X.a X.d
Tactic:
exists X.b
Proof state after:
case right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ refl_trans_clos RX X.b X.a ∧ refl_trans_clos RX X.b X.d
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ refl_trans_clos RX X.b X.a ∧ refl_trans_clos RX X.b X.d
Tactic:
constructor
Proof state after:
case right.a.left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ refl_trans_clos RX X.b X.a

case right.a.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ refl_trans_clos RX X.b X.d
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case right.a.left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ refl_trans_clos RX X.b X.a

case right.a.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ refl_trans_clos RX X.b X.d
Tactic:
. constructor
  simp [RX]
  left; trivial
  constructor
Proof state after:
case right.a.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ refl_trans_clos RX X.b X.d
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case right.a.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ refl_trans_clos RX 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 right.a.left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ refl_trans_clos RX X.b X.a
Tactic:
constructor
Proof state after:
case right.a.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ RX X.b ?right.a.left.b

case right.a.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ refl_trans_clos RX ?right.a.left.b X.a

case right.a.left.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ X
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case right.a.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ RX X.b ?right.a.left.b

case right.a.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ refl_trans_clos RX ?right.a.left.b X.a

case right.a.left.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ X
Tactic:
simp [RX]
Proof state after:
case right.a.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ ?right.a.left.b = X.a ∨ ?right.a.left.b = X.c

case right.a.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ refl_trans_clos RX ?right.a.left.b X.a

case right.a.left.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ X
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case right.a.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ ?right.a.left.b = X.a ∨ ?right.a.left.b = X.c

case right.a.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ refl_trans_clos RX ?right.a.left.b X.a

case right.a.left.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ X
Tactic:
left
Proof state after:
case right.a.left.a.h
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ ?right.a.left.b = X.a

case right.a.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ refl_trans_clos RX ?right.a.left.b X.a

case right.a.left.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ X
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case right.a.left.a.h
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ ?right.a.left.b = X.a

case right.a.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ refl_trans_clos RX ?right.a.left.b X.a

case right.a.left.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ X
Tactic:
trivial
Proof state after:
case right.a.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ refl_trans_clos RX X.a X.a
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case right.a.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ refl_trans_clos RX X.a X.a
Tactic:
constructor
Proof state after:
no goals
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case right.a.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ refl_trans_clos RX X.b X.d
Tactic:
constructor
Proof state after:
case right.a.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ RX X.b ?right.a.right.b

case right.a.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ refl_trans_clos RX ?right.a.right.b X.d

case right.a.right.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ X
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case right.a.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ RX X.b ?right.a.right.b

case right.a.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ refl_trans_clos RX ?right.a.right.b X.d

case right.a.right.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ X
Tactic:
simp [RX]
Proof state after:
case right.a.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ ?right.a.right.b = X.a ∨ ?right.a.right.b = X.c

case right.a.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ refl_trans_clos RX ?right.a.right.b X.d

case right.a.right.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ X
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case right.a.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ ?right.a.right.b = X.a ∨ ?right.a.right.b = X.c

case right.a.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ refl_trans_clos RX ?right.a.right.b X.d

case right.a.right.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ X
Tactic:
right
Proof state after:
case right.a.right.a.h
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ ?right.a.right.b = X.c

case right.a.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ refl_trans_clos RX ?right.a.right.b X.d

case right.a.right.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ X
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case right.a.right.a.h
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ ?right.a.right.b = X.c

case right.a.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ refl_trans_clos RX ?right.a.right.b X.d

case right.a.right.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ X
Tactic:
trivial
Proof state after:
case right.a.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ refl_trans_clos RX X.c X.d
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case right.a.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ refl_trans_clos RX X.c X.d
Tactic:
constructor
Proof state after:
case right.a.right.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ RX X.c ?right.a.right.a.b

case right.a.right.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ refl_trans_clos RX ?right.a.right.a.b X.d

case right.a.right.a.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ X
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case right.a.right.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ RX X.c ?right.a.right.a.b

case right.a.right.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ refl_trans_clos RX ?right.a.right.a.b X.d

case right.a.right.a.b
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ X
Tactic:
. simp [RX]; right; trivial
Proof state after:
case right.a.right.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ refl_trans_clos RX X.d X.d
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case right.a.right.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ refl_trans_clos RX X.d X.d
Tactic:
. constructor
Proof state after:
no goals
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case right.a.right.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ RX X.c ?right.a.right.a.b
Tactic:
simp [RX]
Proof state after:
case right.a.right.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ ?right.a.right.a.b = X.b ∨ ?right.a.right.a.b = X.d
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case right.a.right.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ ?right.a.right.a.b = X.b ∨ ?right.a.right.a.b = X.d
Tactic:
right
Proof state after:
case right.a.right.a.a.h
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ ?right.a.right.a.b = X.d
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case right.a.right.a.a.h
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ ?right.a.right.a.b = X.d
Tactic:
trivial
Proof state after:
no goals
Theorem: weakly_confluent_does_not_imply_confluent
Proof state before:
case right.a.right.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
h : confluent RX
⊢ refl_trans_clos RX X.d X.d
Tactic:
constructor
Proof state after:
no goals
Theorem: normalizes_trans
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ normalizing R → normalizing fun x x_1 => trans_clos R x x_1
Tactic:
intros norm
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
⊢ normalizing fun x x_1 => trans_clos R x x_1
Theorem: normalizes_trans
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
⊢ normalizing fun x x_1 => trans_clos R x x_1
Tactic:
apply ind_normalizing
Proof state after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
⊢ ∀ (P : A → Prop), (∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x) → ∀ (x : A), P x
Theorem: normalizes_trans
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
⊢ ∀ (P : A → Prop), (∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x) → ∀ (x : A), P x
Tactic:
intros P ih
Proof state after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
⊢ ∀ (x : A), P x
Theorem: normalizes_trans
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
⊢ ∀ (x : A), P x
Tactic:
let Q := λ x ↦ P x ∧ ∀ y, x ~>+ y → P y
Proof state after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
⊢ ∀ (x : A), P x
Theorem: normalizes_trans
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
⊢ ∀ (x : A), P x
Tactic:
have h : ∀ x, Q x :=
by
  intros x
  apply normalizing_ind R
  . intros x ih'
    constructor
    . apply ih
      intros y red_x_y
      cases red_x_y
      . apply (ih' _ _).1; trivial
      . apply (ih' _ _).2 <;> trivial
    . intros y red_x_y
      cases red_x_y
      . apply (ih' _ _).1; trivial
      . apply (ih' _ _).2 <;> trivial
  . trivial
Proof state after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
h : ∀ (x : A), Q x
⊢ ∀ (x : A), P x
Theorem: normalizes_trans
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
h : ∀ (x : A), Q x
⊢ ∀ (x : A), P x
Tactic:
intros x
Proof state after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
h : ∀ (x : A), Q x
x : A
⊢ P x
Theorem: normalizes_trans
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
h : ∀ (x : A), Q x
x : A
⊢ P x
Tactic:
apply (h x).1
Proof state after:
no goals
Theorem: normalizes_trans
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
⊢ ∀ (x : A), Q x
Tactic:
intros x
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x : A
⊢ Q x