internlm/Lean-Github huggingface dataset:
Theorem: inc_refl_trans_confl
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
⊢ ((fun R R' => ∀ (x y : A), R x y → R' x y) (fun x x_1 => R x x_1) fun x x_1 => S x x_1) →
    ((fun R R' => ∀ (x y : A), R x y → R' x y) (fun x x_1 => S x x_1) fun x x_1 => refl_trans_clos R x x_1) →
      confluent S → confluent R
Tactic:
simp
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
⊢ (∀ (x y : A), R x y → S x y) → (∀ (x y : A), S x y → refl_trans_clos R x y) → confluent S → confluent R
Theorem: inc_refl_trans_confl
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
⊢ (∀ (x y : A), R x y → S x y) → (∀ (x y : A), S x y → refl_trans_clos R x y) → confluent S → confluent R
Tactic:
intros
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ confluent R
Theorem: inc_refl_trans_confl
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ confluent R
Tactic:
apply (conf_trans_clos _).1
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ confluent (refl_trans_clos R)
Theorem: inc_refl_trans_confl
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ confluent (refl_trans_clos R)
Tactic:
apply equiv_conf
Proof state after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ ∀ (x y : A), ?S x y ↔ refl_trans_clos R x y

case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ confluent ?S

case S
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ A → A → Prop
Theorem: inc_refl_trans_confl
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ ∀ (x y : A), ?S x y ↔ refl_trans_clos R x y

case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ confluent ?S

case S
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ A → A → Prop
Tactic:
. apply inc_refl_trans_eq; simp
  . trivial
  . simp; trivial
Proof state after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ confluent fun x y => (fun x x_1 => refl_trans_clos (fun x y => S x y) x x_1) x y
Theorem: inc_refl_trans_confl
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ confluent fun x y => (fun x x_1 => refl_trans_clos (fun x y => S x y) x x_1) x y
Tactic:
. aesop
Proof state after:
no goals
Theorem: inc_refl_trans_confl
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ ∀ (x y : A), ?S x y ↔ refl_trans_clos R x y
Tactic:
apply inc_refl_trans_eq
Proof state after:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ ∀ (x y : A), (fun x x_1 => R x x_1) x y → (fun x x_1 => ?a.S✝ x x_1) x y

case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ ∀ (x y : A), (fun x x_1 => ?a.S✝ x x_1) x y → (fun x x_1 => refl_trans_clos R x x_1) x y

case a.S
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ A → A → Prop
Theorem: inc_refl_trans_confl
Proof state before:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ ∀ (x y : A), (fun x x_1 => R x x_1) x y → (fun x x_1 => ?a.S✝ x x_1) x y

case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ ∀ (x y : A), (fun x x_1 => ?a.S✝ x x_1) x y → (fun x x_1 => refl_trans_clos R x x_1) x y

case a.S
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ A → A → Prop
Tactic:
simp
Proof state after:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ ∀ (x y : A), R x y → ?a.S✝ x y

case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ ∀ (x y : A), (fun x x_1 => ?a.S✝ x x_1) x y → (fun x x_1 => refl_trans_clos R x x_1) x y

case a.S
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ A → A → Prop
Theorem: inc_refl_trans_confl
Proof state before:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ ∀ (x y : A), R x y → ?a.S✝ x y

case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ ∀ (x y : A), (fun x x_1 => ?a.S✝ x x_1) x y → (fun x x_1 => refl_trans_clos R x x_1) x y

case a.S
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ A → A → Prop
Tactic:
. trivial
Proof state after:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ ∀ (x y : A), (fun x x_1 => S x x_1) x y → (fun x x_1 => refl_trans_clos R x x_1) x y
Theorem: inc_refl_trans_confl
Proof state before:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ ∀ (x y : A), (fun x x_1 => S x x_1) x y → (fun x x_1 => refl_trans_clos R x x_1) x y
Tactic:
. simp; trivial
Proof state after:
no goals
Theorem: inc_refl_trans_confl
Proof state before:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ ∀ (x y : A), R x y → ?a.S✝ x y
Tactic:
trivial
Proof state after:
no goals
Theorem: inc_refl_trans_confl
Proof state before:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ ∀ (x y : A), (fun x x_1 => S x x_1) x y → (fun x x_1 => refl_trans_clos R x x_1) x y
Tactic:
simp
Proof state after:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ ∀ (x y : A), S x y → refl_trans_clos R x y
Theorem: inc_refl_trans_confl
Proof state before:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ ∀ (x y : A), S x y → refl_trans_clos R x y
Tactic:
trivial
Proof state after:
no goals
Theorem: inc_refl_trans_confl
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
a✝² : ∀ (x y : A), R x y → S x y
a✝¹ : ∀ (x y : A), S x y → refl_trans_clos R x y
a✝ : confluent S
⊢ confluent fun x y => (fun x x_1 => refl_trans_clos (fun x y => S x y) x x_1) x y
Tactic:
aesop
Proof state after:
no goals
Theorem: refl_is_refl_trans
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
x y : A
⊢ refl_clos R x y → refl_trans_clos R x y
Tactic:
aesop
Proof state after:
no goals
Theorem: strong_confluent_implies_confluent
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
⊢ strongly_confluent R → confluent R
Tactic:
intros str_conf
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
⊢ confluent R
Theorem: strong_confluent_implies_confluent
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
⊢ confluent R
Tactic:
apply semi_confluent_implies_confluent
Proof state after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
⊢ semi_confluent R
Theorem: strong_confluent_implies_confluent
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
⊢ semi_confluent R
Tactic:
unfold semi_confluent
Proof state after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
⊢ ∀ (x y z : A), R x y → refl_trans_clos R x z → joins R y z
Theorem: strong_confluent_implies_confluent
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
⊢ ∀ (x y z : A), R x y → refl_trans_clos R x z → joins R y z
Tactic:
intros x y z red_x_y red_x_z
Proof state after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x y z : A
red_x_y : R x y
red_x_z : refl_trans_clos R x z
⊢ joins R y z
Theorem: strong_confluent_implies_confluent
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x y z : A
red_x_y : R x y
red_x_z : refl_trans_clos R x z
⊢ joins R y z
Tactic:
revert red_x_y y
Proof state after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x z : A
red_x_z : refl_trans_clos R x z
⊢ ∀ (y : A), R x y → joins R y z
Theorem: strong_confluent_implies_confluent
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x z : A
red_x_z : refl_trans_clos R x z
⊢ ∀ (y : A), R x y → joins R y z
Tactic:
induction' red_x_z with a x x₂ xₙ red_x_x2 red_x2_xn ih
Proof state after:
case a.refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x z a : A
⊢ ∀ (y : A), R a y → joins R y a

case a.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x✝ z x x₂ xₙ : A
red_x_x2 : R x x₂
red_x2_xn : refl_trans_clos R x₂ xₙ
ih : ∀ (y : A), R x₂ y → joins R y xₙ
⊢ ∀ (y : A), R x y → joins R y xₙ
Theorem: strong_confluent_implies_confluent
Proof state before:
case a.refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x z a : A
⊢ ∀ (y : A), R a y → joins R y a

case a.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x✝ z x x₂ xₙ : A
red_x_x2 : R x x₂
red_x2_xn : refl_trans_clos R x₂ xₙ
ih : ∀ (y : A), R x₂ y → joins R y xₙ
⊢ ∀ (y : A), R x y → joins R y xₙ
Tactic:
. intros y _; exists y; aesop
Proof state after:
case a.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x✝ z x x₂ xₙ : A
red_x_x2 : R x x₂
red_x2_xn : refl_trans_clos R x₂ xₙ
ih : ∀ (y : A), R x₂ y → joins R y xₙ
⊢ ∀ (y : A), R x y → joins R y xₙ
Theorem: strong_confluent_implies_confluent
Proof state before:
case a.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x✝ z x x₂ xₙ : A
red_x_x2 : R x x₂
red_x2_xn : refl_trans_clos R x₂ xₙ
ih : ∀ (y : A), R x₂ y → joins R y xₙ
⊢ ∀ (y : A), R x y → joins R y xₙ
Tactic:
. intros y red_x_y
  cases' (str_conf _ _ _ red_x_y red_x_x2) with y₂ h
  cases h.2
  . exists xₙ; constructor
    . apply refl_trans_clos_transitive
      . apply h.1
      . trivial
    . constructor
  . have ih : y₂ ~>*.*<~ xₙ :=
      by apply ih; trivial
    cases' ih with w _
    exists w; constructor
    . apply refl_trans_clos_transitive
      . apply h.1
      . aesop
    . aesop
Proof state after:
no goals
Theorem: strong_confluent_implies_confluent
Proof state before:
case a.refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x z a : A
⊢ ∀ (y : A), R a y → joins R y a
Tactic:
intros y _
Proof state after:
case a.refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x z a y : A
red_x_y✝ : R a y
⊢ joins R y a
Theorem: strong_confluent_implies_confluent
Proof state before:
case a.refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x z a y : A
red_x_y✝ : R a y
⊢ joins R y a
Tactic:
exists y
Proof state after:
case a.refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x z a y : A
red_x_y✝ : R a y
⊢ refl_trans_clos R y y ∧ refl_trans_clos R a y
Theorem: strong_confluent_implies_confluent
Proof state before:
case a.refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x z a y : A
red_x_y✝ : R a y
⊢ refl_trans_clos R y y ∧ refl_trans_clos R a y
Tactic:
aesop
Proof state after:
no goals
Theorem: strong_confluent_implies_confluent
Proof state before:
case a.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x✝ z x x₂ xₙ : A
red_x_x2 : R x x₂
red_x2_xn : refl_trans_clos R x₂ xₙ
ih : ∀ (y : A), R x₂ y → joins R y xₙ
⊢ ∀ (y : A), R x y → joins R y xₙ
Tactic:
intros y red_x_y
Proof state after:
case a.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x✝ z x x₂ xₙ : A
red_x_x2 : R x x₂
red_x2_xn : refl_trans_clos R x₂ xₙ
ih : ∀ (y : A), R x₂ y → joins R y xₙ
y : A
red_x_y : R x y
⊢ joins R y xₙ
Theorem: strong_confluent_implies_confluent
Proof state before:
case a.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x✝ z x x₂ xₙ : A
red_x_x2 : R x x₂
red_x2_xn : refl_trans_clos R x₂ xₙ
ih : ∀ (y : A), R x₂ y → joins R y xₙ
y : A
red_x_y : R x y
⊢ joins R y xₙ
Tactic:
cases' (str_conf _ _ _ red_x_y red_x_x2) with y₂ h
Proof state after:
case a.step.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x✝ z x x₂ xₙ : A
red_x_x2 : R x x₂
red_x2_xn : refl_trans_clos R x₂ xₙ
ih : ∀ (y : A), R x₂ y → joins R y xₙ
y : A
red_x_y : R x y
y₂ : A
h : refl_trans_clos R y y₂ ∧ refl_clos R x₂ y₂
⊢ joins R y xₙ
Theorem: strong_confluent_implies_confluent
Proof state before:
case a.step.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x✝ z x x₂ xₙ : A
red_x_x2 : R x x₂
red_x2_xn : refl_trans_clos R x₂ xₙ
ih : ∀ (y : A), R x₂ y → joins R y xₙ
y : A
red_x_y : R x y
y₂ : A
h : refl_trans_clos R y y₂ ∧ refl_clos R x₂ y₂
⊢ joins R y xₙ
Tactic:
cases h.2
Proof state after:
case a.step.intro.refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x✝ z x x₂ xₙ : A
red_x_x2 : R x x₂
red_x2_xn : refl_trans_clos R x₂ xₙ
ih : ∀ (y : A), R x₂ y → joins R y xₙ
y : A
red_x_y : R x y
h : refl_trans_clos R y x₂ ∧ refl_clos R x₂ x₂
⊢ joins R y xₙ

case a.step.intro.base
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x✝ z x x₂ xₙ : A
red_x_x2 : R x x₂
red_x2_xn : refl_trans_clos R x₂ xₙ
ih : ∀ (y : A), R x₂ y → joins R y xₙ
y : A
red_x_y : R x y
y₂ : A
h : refl_trans_clos R y y₂ ∧ refl_clos R x₂ y₂
a✝ : R x₂ y₂
⊢ joins R y xₙ
Theorem: strong_confluent_implies_confluent
Proof state before:
case a.step.intro.refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x✝ z x x₂ xₙ : A
red_x_x2 : R x x₂
red_x2_xn : refl_trans_clos R x₂ xₙ
ih : ∀ (y : A), R x₂ y → joins R y xₙ
y : A
red_x_y : R x y
h : refl_trans_clos R y x₂ ∧ refl_clos R x₂ x₂
⊢ joins R y xₙ

case a.step.intro.base
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x✝ z x x₂ xₙ : A
red_x_x2 : R x x₂
red_x2_xn : refl_trans_clos R x₂ xₙ
ih : ∀ (y : A), R x₂ y → joins R y xₙ
y : A
red_x_y : R x y
y₂ : A
h : refl_trans_clos R y y₂ ∧ refl_clos R x₂ y₂
a✝ : R x₂ y₂
⊢ joins R y xₙ
Tactic:
. exists xₙ; constructor
  . apply refl_trans_clos_transitive
    . apply h.1
    . trivial
  . constructor
Proof state after:
case a.step.intro.base
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x✝ z x x₂ xₙ : A
red_x_x2 : R x x₂
red_x2_xn : refl_trans_clos R x₂ xₙ
ih : ∀ (y : A), R x₂ y → joins R y xₙ
y : A
red_x_y : R x y
y₂ : A
h : refl_trans_clos R y y₂ ∧ refl_clos R x₂ y₂
a✝ : R x₂ y₂
⊢ joins R y xₙ
Theorem: strong_confluent_implies_confluent
Proof state before:
case a.step.intro.base
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x✝ z x x₂ xₙ : A
red_x_x2 : R x x₂
red_x2_xn : refl_trans_clos R x₂ xₙ
ih : ∀ (y : A), R x₂ y → joins R y xₙ
y : A
red_x_y : R x y
y₂ : A
h : refl_trans_clos R y y₂ ∧ refl_clos R x₂ y₂
a✝ : R x₂ y₂
⊢ joins R y xₙ
Tactic:
. have ih : y₂ ~>*.*<~ xₙ :=
    by apply ih; trivial
  cases' ih with w _
  exists w; constructor
  . apply refl_trans_clos_transitive
    . apply h.1
    . aesop
  . aesop
Proof state after:
no goals
Theorem: strong_confluent_implies_confluent
Proof state before:
case a.step.intro.refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x✝ z x x₂ xₙ : A
red_x_x2 : R x x₂
red_x2_xn : refl_trans_clos R x₂ xₙ
ih : ∀ (y : A), R x₂ y → joins R y xₙ
y : A
red_x_y : R x y
h : refl_trans_clos R y x₂ ∧ refl_clos R x₂ x₂
⊢ joins R y xₙ
Tactic:
exists xₙ
Proof state after:
case a.step.intro.refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x✝ z x x₂ xₙ : A
red_x_x2 : R x x₂
red_x2_xn : refl_trans_clos R x₂ xₙ
ih : ∀ (y : A), R x₂ y → joins R y xₙ
y : A
red_x_y : R x y
h : refl_trans_clos R y x₂ ∧ refl_clos R x₂ x₂
⊢ refl_trans_clos R y xₙ ∧ refl_trans_clos R xₙ xₙ
Theorem: strong_confluent_implies_confluent
Proof state before:
case a.step.intro.refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x✝ z x x₂ xₙ : A
red_x_x2 : R x x₂
red_x2_xn : refl_trans_clos R x₂ xₙ
ih : ∀ (y : A), R x₂ y → joins R y xₙ
y : A
red_x_y : R x y
h : refl_trans_clos R y x₂ ∧ refl_clos R x₂ x₂
⊢ refl_trans_clos R y xₙ ∧ refl_trans_clos R xₙ xₙ
Tactic:
constructor
Proof state after:
case a.step.intro.refl.left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x✝ z x x₂ xₙ : A
red_x_x2 : R x x₂
red_x2_xn : refl_trans_clos R x₂ xₙ
ih : ∀ (y : A), R x₂ y → joins R y xₙ
y : A
red_x_y : R x y
h : refl_trans_clos R y x₂ ∧ refl_clos R x₂ x₂
⊢ refl_trans_clos R y xₙ

case a.step.intro.refl.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x✝ z x x₂ xₙ : A
red_x_x2 : R x x₂
red_x2_xn : refl_trans_clos R x₂ xₙ
ih : ∀ (y : A), R x₂ y → joins R y xₙ
y : A
red_x_y : R x y
h : refl_trans_clos R y x₂ ∧ refl_clos R x₂ x₂
⊢ refl_trans_clos R xₙ xₙ
Theorem: strong_confluent_implies_confluent
Proof state before:
case a.step.intro.refl.left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x✝ z x x₂ xₙ : A
red_x_x2 : R x x₂
red_x2_xn : refl_trans_clos R x₂ xₙ
ih : ∀ (y : A), R x₂ y → joins R y xₙ
y : A
red_x_y : R x y
h : refl_trans_clos R y x₂ ∧ refl_clos R x₂ x₂
⊢ refl_trans_clos R y xₙ

case a.step.intro.refl.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x✝ z x x₂ xₙ : A
red_x_x2 : R x x₂
red_x2_xn : refl_trans_clos R x₂ xₙ
ih : ∀ (y : A), R x₂ y → joins R y xₙ
y : A
red_x_y : R x y
h : refl_trans_clos R y x₂ ∧ refl_clos R x₂ x₂
⊢ refl_trans_clos R xₙ xₙ
Tactic:
. apply refl_trans_clos_transitive
  . apply h.1
  . trivial
Proof state after:
case a.step.intro.refl.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x✝ z x x₂ xₙ : A
red_x_x2 : R x x₂
red_x2_xn : refl_trans_clos R x₂ xₙ
ih : ∀ (y : A), R x₂ y → joins R y xₙ
y : A
red_x_y : R x y
h : refl_trans_clos R y x₂ ∧ refl_clos R x₂ x₂
⊢ refl_trans_clos R xₙ xₙ
Theorem: strong_confluent_implies_confluent
Proof state before:
case a.step.intro.refl.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x✝ z x x₂ xₙ : A
red_x_x2 : R x x₂
red_x2_xn : refl_trans_clos R x₂ xₙ
ih : ∀ (y : A), R x₂ y → joins R y xₙ
y : A
red_x_y : R x y
h : refl_trans_clos R y x₂ ∧ refl_clos R x₂ x₂
⊢ refl_trans_clos R xₙ xₙ
Tactic:
. constructor
Proof state after:
no goals
Theorem: strong_confluent_implies_confluent
Proof state before:
case a.step.intro.refl.left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x✝ z x x₂ xₙ : A
red_x_x2 : R x x₂
red_x2_xn : refl_trans_clos R x₂ xₙ
ih : ∀ (y : A), R x₂ y → joins R y xₙ
y : A
red_x_y : R x y
h : refl_trans_clos R y x₂ ∧ refl_clos R x₂ x₂
⊢ refl_trans_clos R y xₙ
Tactic:
apply refl_trans_clos_transitive
Proof state after:
case a.step.intro.refl.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x✝ z x x₂ xₙ : A
red_x_x2 : R x x₂
red_x2_xn : refl_trans_clos R x₂ xₙ
ih : ∀ (y : A), R x₂ y → joins R y xₙ
y : A
red_x_y : R x y
h : refl_trans_clos R y x₂ ∧ refl_clos R x₂ x₂
⊢ refl_trans_clos R y ?a.step.intro.refl.left.y✝

case a.step.intro.refl.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x✝ z x x₂ xₙ : A
red_x_x2 : R x x₂
red_x2_xn : refl_trans_clos R x₂ xₙ
ih : ∀ (y : A), R x₂ y → joins R y xₙ
y : A
red_x_y : R x y
h : refl_trans_clos R y x₂ ∧ refl_clos R x₂ x₂
⊢ refl_trans_clos R ?a.step.intro.refl.left.y✝ xₙ

case a.step.intro.refl.left.y
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x✝ z x x₂ xₙ : A
red_x_x2 : R x x₂
red_x2_xn : refl_trans_clos R x₂ xₙ
ih : ∀ (y : A), R x₂ y → joins R y xₙ
y : A
red_x_y : R x y
h : refl_trans_clos R y x₂ ∧ refl_clos R x₂ x₂
⊢ A