internlm/Lean-Github huggingface dataset:
Theorem: equiv_conf
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
x✝ y✝ : A
⊢ ?R x✝ y✝ → S x✝ y✝

case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
⊢ refl_trans_clos ?R x y

case R
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
⊢ A → A → Prop
Tactic:
apply (equiv _ _).2
Proof state after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
⊢ refl_trans_clos (fun x y => R x y) x y
Theorem: equiv_conf
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
⊢ refl_trans_clos (fun x y => R x y) x y
Tactic:
trivial
Proof state after:
no goals
Theorem: equiv_conf
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1 : refl_trans_clos S x y
⊢ refl_trans_clos S x z
Tactic:
apply refl_trans_clos_monotone
Proof state after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1 : refl_trans_clos S x y
⊢ ∀ (x y : A), ?R x y → S x y

case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1 : refl_trans_clos S x y
⊢ refl_trans_clos ?R x z

case R
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1 : refl_trans_clos S x y
⊢ A → A → Prop
Theorem: equiv_conf
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1 : refl_trans_clos S x y
⊢ ∀ (x y : A), ?R x y → S x y

case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1 : refl_trans_clos S x y
⊢ refl_trans_clos ?R x z

case R
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1 : refl_trans_clos S x y
⊢ A → A → Prop
Tactic:
intros _ _
Proof state after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1 : refl_trans_clos S x y
x✝ y✝ : A
⊢ ?R x✝ y✝ → S x✝ y✝

case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1 : refl_trans_clos S x y
⊢ refl_trans_clos ?R x z

case R
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1 : refl_trans_clos S x y
⊢ A → A → Prop
Theorem: equiv_conf
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1 : refl_trans_clos S x y
x✝ y✝ : A
⊢ ?R x✝ y✝ → S x✝ y✝

case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1 : refl_trans_clos S x y
⊢ refl_trans_clos ?R x z

case R
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1 : refl_trans_clos S x y
⊢ A → A → Prop
Tactic:
apply (equiv _ _).2
Proof state after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1 : refl_trans_clos S x y
⊢ refl_trans_clos (fun x y => R x y) x z
Theorem: equiv_conf
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1 : refl_trans_clos S x y
⊢ refl_trans_clos (fun x y => R x y) x z
Tactic:
trivial
Proof state after:
no goals
Theorem: equiv_conf
Proof state before:
case intro.intro.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1✝ : refl_trans_clos S x y
h2✝ : refl_trans_clos S x z
w : A
h1 : refl_trans_clos S y w
h2 : refl_trans_clos S z w
⊢ ∀ (x y : A), ?intro.intro.left.R x y → R x y
Tactic:
intros x y
Proof state after:
case intro.intro.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y✝ z x✝ : A
red_x_y : refl_trans_clos R x✝ y✝
red_y_z : refl_trans_clos R x✝ z
h1✝ : refl_trans_clos S x✝ y✝
h2✝ : refl_trans_clos S x✝ z
w : A
h1 : refl_trans_clos S y✝ w
h2 : refl_trans_clos S z w
x y : A
⊢ ?intro.intro.left.R x y → R x y
Theorem: equiv_conf
Proof state before:
case intro.intro.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y✝ z x✝ : A
red_x_y : refl_trans_clos R x✝ y✝
red_y_z : refl_trans_clos R x✝ z
h1✝ : refl_trans_clos S x✝ y✝
h2✝ : refl_trans_clos S x✝ z
w : A
h1 : refl_trans_clos S y✝ w
h2 : refl_trans_clos S z w
x y : A
⊢ ?intro.intro.left.R x y → R x y
Tactic:
apply (equiv _ _).1
Proof state after:
no goals
Theorem: equiv_conf
Proof state before:
case intro.intro.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1✝ : refl_trans_clos S x y
h2✝ : refl_trans_clos S x z
w : A
h1 : refl_trans_clos S y w
h2 : refl_trans_clos S z w
⊢ refl_trans_clos (fun x y => S x y) y w
Tactic:
trivial
Proof state after:
no goals
Theorem: equiv_conf
Proof state before:
case intro.intro.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1✝ : refl_trans_clos S x y
h2✝ : refl_trans_clos S x z
w : A
h1 : refl_trans_clos S y w
h2 : refl_trans_clos S z w
⊢ ∀ (x y : A), ?intro.intro.right.R x y → R x y
Tactic:
intros x y
Proof state after:
case intro.intro.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y✝ z x✝ : A
red_x_y : refl_trans_clos R x✝ y✝
red_y_z : refl_trans_clos R x✝ z
h1✝ : refl_trans_clos S x✝ y✝
h2✝ : refl_trans_clos S x✝ z
w : A
h1 : refl_trans_clos S y✝ w
h2 : refl_trans_clos S z w
x y : A
⊢ ?intro.intro.right.R x y → R x y
Theorem: equiv_conf
Proof state before:
case intro.intro.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y✝ z x✝ : A
red_x_y : refl_trans_clos R x✝ y✝
red_y_z : refl_trans_clos R x✝ z
h1✝ : refl_trans_clos S x✝ y✝
h2✝ : refl_trans_clos S x✝ z
w : A
h1 : refl_trans_clos S y✝ w
h2 : refl_trans_clos S z w
x y : A
⊢ ?intro.intro.right.R x y → R x y
Tactic:
apply (equiv _ _).1
Proof state after:
no goals
Theorem: equiv_conf
Proof state before:
case intro.intro.right.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
equiv : ∀ (x y : A), S x y ↔ R x y
h :
  ∀ (y z x : A),
    refl_trans_clos S x y → refl_trans_clos S x z → ∃ z_1, refl_trans_clos S y z_1 ∧ refl_trans_clos S z z_1
y z x : A
red_x_y : refl_trans_clos R x y
red_y_z : refl_trans_clos R x z
h1✝ : refl_trans_clos S x y
h2✝ : refl_trans_clos S x z
w : A
h1 : refl_trans_clos S y w
h2 : refl_trans_clos S z w
⊢ refl_trans_clos (fun x y => S x y) z w
Tactic:
trivial
Proof state after:
no goals
Theorem: trans_clos_idempotent
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
⊢ ∀ (R : A → A → Prop),
    (fun R R' => ∀ (x y : A), R x y ↔ R' x y) (refl_trans_clos (refl_trans_clos R)) (refl_trans_clos R)
Tactic:
simp
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
⊢ ∀ (R : A → A → Prop) (x y : A), refl_trans_clos (refl_trans_clos R) x y ↔ refl_trans_clos R x y
Theorem: trans_clos_idempotent
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
⊢ ∀ (R : A → A → Prop) (x y : A), refl_trans_clos (refl_trans_clos R) x y ↔ refl_trans_clos R x y
Tactic:
intros R x y
Proof state after:
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y : A
⊢ refl_trans_clos (refl_trans_clos R) x y ↔ refl_trans_clos R x y
Theorem: trans_clos_idempotent
Proof state before:
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y : A
⊢ refl_trans_clos (refl_trans_clos R) x y ↔ refl_trans_clos R x y
Tactic:
constructor <;> intros steps <;> induction' steps with z a b c red_a_c _red_b_c ih
Proof state after:
case mp.refl
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y z : A
⊢ refl_trans_clos R z z

case mp.step
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y a b c : A
red_a_c : refl_trans_clos R a b
_red_b_c : refl_trans_clos (refl_trans_clos R) b c
ih : refl_trans_clos R b c
⊢ refl_trans_clos R a c

case mpr.refl
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y z : A
⊢ refl_trans_clos (refl_trans_clos R) z z

case mpr.step
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y a b c : A
red_a_c : R a b
_red_b_c : refl_trans_clos R b c
ih : refl_trans_clos (refl_trans_clos R) b c
⊢ refl_trans_clos (refl_trans_clos R) a c
Theorem: trans_clos_idempotent
Proof state before:
case mp.refl
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y z : A
⊢ refl_trans_clos R z z

case mp.step
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y a b c : A
red_a_c : refl_trans_clos R a b
_red_b_c : refl_trans_clos (refl_trans_clos R) b c
ih : refl_trans_clos R b c
⊢ refl_trans_clos R a c

case mpr.refl
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y z : A
⊢ refl_trans_clos (refl_trans_clos R) z z

case mpr.step
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y a b c : A
red_a_c : R a b
_red_b_c : refl_trans_clos R b c
ih : refl_trans_clos (refl_trans_clos R) b c
⊢ refl_trans_clos (refl_trans_clos R) a c
Tactic:
. constructor
Proof state after:
case mp.step
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y a b c : A
red_a_c : refl_trans_clos R a b
_red_b_c : refl_trans_clos (refl_trans_clos R) b c
ih : refl_trans_clos R b c
⊢ refl_trans_clos R a c

case mpr.refl
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y z : A
⊢ refl_trans_clos (refl_trans_clos R) z z

case mpr.step
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y a b c : A
red_a_c : R a b
_red_b_c : refl_trans_clos R b c
ih : refl_trans_clos (refl_trans_clos R) b c
⊢ refl_trans_clos (refl_trans_clos R) a c
Theorem: trans_clos_idempotent
Proof state before:
case mp.step
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y a b c : A
red_a_c : refl_trans_clos R a b
_red_b_c : refl_trans_clos (refl_trans_clos R) b c
ih : refl_trans_clos R b c
⊢ refl_trans_clos R a c

case mpr.refl
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y z : A
⊢ refl_trans_clos (refl_trans_clos R) z z

case mpr.step
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y a b c : A
red_a_c : R a b
_red_b_c : refl_trans_clos R b c
ih : refl_trans_clos (refl_trans_clos R) b c
⊢ refl_trans_clos (refl_trans_clos R) a c
Tactic:
. apply refl_trans_clos_transitive <;> trivial
Proof state after:
case mpr.refl
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y z : A
⊢ refl_trans_clos (refl_trans_clos R) z z

case mpr.step
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y a b c : A
red_a_c : R a b
_red_b_c : refl_trans_clos R b c
ih : refl_trans_clos (refl_trans_clos R) b c
⊢ refl_trans_clos (refl_trans_clos R) a c
Theorem: trans_clos_idempotent
Proof state before:
case mpr.refl
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y z : A
⊢ refl_trans_clos (refl_trans_clos R) z z

case mpr.step
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y a b c : A
red_a_c : R a b
_red_b_c : refl_trans_clos R b c
ih : refl_trans_clos (refl_trans_clos R) b c
⊢ refl_trans_clos (refl_trans_clos R) a c
Tactic:
. constructor
Proof state after:
case mpr.step
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y a b c : A
red_a_c : R a b
_red_b_c : refl_trans_clos R b c
ih : refl_trans_clos (refl_trans_clos R) b c
⊢ refl_trans_clos (refl_trans_clos R) a c
Theorem: trans_clos_idempotent
Proof state before:
case mpr.step
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y a b c : A
red_a_c : R a b
_red_b_c : refl_trans_clos R b c
ih : refl_trans_clos (refl_trans_clos R) b c
⊢ refl_trans_clos (refl_trans_clos R) a c
Tactic:
. apply refl_trans_clos.step
  . apply refl_trans_clos.step; trivial
    constructor
  . trivial
Proof state after:
no goals
Theorem: trans_clos_idempotent
Proof state before:
case mp.refl
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y z : A
⊢ refl_trans_clos R z z
Tactic:
constructor
Proof state after:
no goals
Theorem: trans_clos_idempotent
Proof state before:
case mp.step
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y a b c : A
red_a_c : refl_trans_clos R a b
_red_b_c : refl_trans_clos (refl_trans_clos R) b c
ih : refl_trans_clos R b c
⊢ refl_trans_clos R a c
Tactic:
apply refl_trans_clos_transitive <;> trivial
Proof state after:
no goals
Theorem: trans_clos_idempotent
Proof state before:
case mpr.refl
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y z : A
⊢ refl_trans_clos (refl_trans_clos R) z z
Tactic:
constructor
Proof state after:
no goals
Theorem: trans_clos_idempotent
Proof state before:
case mpr.step
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y a b c : A
red_a_c : R a b
_red_b_c : refl_trans_clos R b c
ih : refl_trans_clos (refl_trans_clos R) b c
⊢ refl_trans_clos (refl_trans_clos R) a c
Tactic:
apply refl_trans_clos.step
Proof state after:
case mpr.step.a
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y a b c : A
red_a_c : R a b
_red_b_c : refl_trans_clos R b c
ih : refl_trans_clos (refl_trans_clos R) b c
⊢ refl_trans_clos R a ?mpr.step.b

case mpr.step.a
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y a b c : A
red_a_c : R a b
_red_b_c : refl_trans_clos R b c
ih : refl_trans_clos (refl_trans_clos R) b c
⊢ refl_trans_clos (refl_trans_clos R) ?mpr.step.b c

case mpr.step.b
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y a b c : A
red_a_c : R a b
_red_b_c : refl_trans_clos R b c
ih : refl_trans_clos (refl_trans_clos R) b c
⊢ A
Theorem: trans_clos_idempotent
Proof state before:
case mpr.step.a
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y a b c : A
red_a_c : R a b
_red_b_c : refl_trans_clos R b c
ih : refl_trans_clos (refl_trans_clos R) b c
⊢ refl_trans_clos R a ?mpr.step.b

case mpr.step.a
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y a b c : A
red_a_c : R a b
_red_b_c : refl_trans_clos R b c
ih : refl_trans_clos (refl_trans_clos R) b c
⊢ refl_trans_clos (refl_trans_clos R) ?mpr.step.b c

case mpr.step.b
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y a b c : A
red_a_c : R a b
_red_b_c : refl_trans_clos R b c
ih : refl_trans_clos (refl_trans_clos R) b c
⊢ A
Tactic:
. apply refl_trans_clos.step; trivial
  constructor
Proof state after:
case mpr.step.a
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y a b c : A
red_a_c : R a b
_red_b_c : refl_trans_clos R b c
ih : refl_trans_clos (refl_trans_clos R) b c
⊢ refl_trans_clos (refl_trans_clos R) b c
Theorem: trans_clos_idempotent
Proof state before:
case mpr.step.a
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y a b c : A
red_a_c : R a b
_red_b_c : refl_trans_clos R b c
ih : refl_trans_clos (refl_trans_clos R) b c
⊢ refl_trans_clos (refl_trans_clos R) b c
Tactic:
. trivial
Proof state after:
no goals
Theorem: trans_clos_idempotent
Proof state before:
case mpr.step.a
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y a b c : A
red_a_c : R a b
_red_b_c : refl_trans_clos R b c
ih : refl_trans_clos (refl_trans_clos R) b c
⊢ refl_trans_clos R a ?mpr.step.b
Tactic:
apply refl_trans_clos.step
Proof state after:
case mpr.step.a.a
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y a b c : A
red_a_c : R a b
_red_b_c : refl_trans_clos R b c
ih : refl_trans_clos (refl_trans_clos R) b c
⊢ R a ?mpr.step.a.b

case mpr.step.a.a
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y a b c : A
red_a_c : R a b
_red_b_c : refl_trans_clos R b c
ih : refl_trans_clos (refl_trans_clos R) b c
⊢ refl_trans_clos R ?mpr.step.a.b ?mpr.step.b

case mpr.step.a.b
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y a b c : A
red_a_c : R a b
_red_b_c : refl_trans_clos R b c
ih : refl_trans_clos (refl_trans_clos R) b c
⊢ A
Theorem: trans_clos_idempotent
Proof state before:
case mpr.step.a.a
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y a b c : A
red_a_c : R a b
_red_b_c : refl_trans_clos R b c
ih : refl_trans_clos (refl_trans_clos R) b c
⊢ R a ?mpr.step.a.b

case mpr.step.a.a
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y a b c : A
red_a_c : R a b
_red_b_c : refl_trans_clos R b c
ih : refl_trans_clos (refl_trans_clos R) b c
⊢ refl_trans_clos R ?mpr.step.a.b ?mpr.step.b

case mpr.step.a.b
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y a b c : A
red_a_c : R a b
_red_b_c : refl_trans_clos R b c
ih : refl_trans_clos (refl_trans_clos R) b c
⊢ A
Tactic:
trivial
Proof state after:
case mpr.step.a.a
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y a b c : A
red_a_c : R a b
_red_b_c : refl_trans_clos R b c
ih : refl_trans_clos (refl_trans_clos R) b c
⊢ refl_trans_clos R b ?mpr.step.b
Theorem: trans_clos_idempotent
Proof state before:
case mpr.step.a.a
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y a b c : A
red_a_c : R a b
_red_b_c : refl_trans_clos R b c
ih : refl_trans_clos (refl_trans_clos R) b c
⊢ refl_trans_clos R b ?mpr.step.b
Tactic:
constructor
Proof state after:
no goals
Theorem: trans_clos_idempotent
Proof state before:
case mpr.step.a
A : Type
R✝ : A → A → Prop
inhabited_A : Nonempty A
S R : A → A → Prop
x y a b c : A
red_a_c : R a b
_red_b_c : refl_trans_clos R b c
ih : refl_trans_clos (refl_trans_clos R) b c
⊢ refl_trans_clos (refl_trans_clos R) b c
Tactic:
trivial
Proof state after:
no goals
Theorem: conf_trans_clos
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
⊢ confluent (refl_trans_clos R) ↔ confluent R
Tactic:
simp [confluent, joins, wedge]
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
⊢ (∀ (y z x : A),
      refl_trans_clos (refl_trans_clos R) x y →
        refl_trans_clos (refl_trans_clos R) x z →
          ∃ z_1, refl_trans_clos (refl_trans_clos R) y z_1 ∧ refl_trans_clos (refl_trans_clos R) z z_1) ↔
    ∀ (y z x : A),
      refl_trans_clos R x y → refl_trans_clos R x z → ∃ z_1, refl_trans_clos R y z_1 ∧ refl_trans_clos R z z_1