internlm/Lean-Github huggingface dataset:
Theorem: strong_confluent_implies_confluent
Proof state before:
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
Tactic:
. apply h.1
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 x₂ xₙ
Theorem: strong_confluent_implies_confluent
Proof state before:
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 x₂ xₙ
Tactic:
. trivial
Proof state after:
no goals
Theorem: strong_confluent_implies_confluent
Proof state before:
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✝
Tactic:
apply h.1
Proof state after:
no goals
Theorem: strong_confluent_implies_confluent
Proof state before:
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 x₂ xₙ
Tactic:
trivial
Proof state after:
no goals
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.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
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₂
ih : joins R y₂ xₙ
⊢ 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₂
ih : joins R y₂ xₙ
⊢ joins R y xₙ
Tactic:
cases' ih with w _
Proof state after:
case a.step.intro.base.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₂
a✝ : R x₂ y₂
w : A
h✝ : refl_trans_clos R y₂ w ∧ refl_trans_clos R xₙ w
⊢ joins R y xₙ
Theorem: strong_confluent_implies_confluent
Proof state before:
case a.step.intro.base.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₂
a✝ : R x₂ y₂
w : A
h✝ : refl_trans_clos R y₂ w ∧ refl_trans_clos R xₙ w
⊢ joins R y xₙ
Tactic:
exists w
Proof state after:
case a.step.intro.base.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₂
a✝ : R x₂ y₂
w : A
h✝ : refl_trans_clos R y₂ w ∧ refl_trans_clos R xₙ w
⊢ refl_trans_clos R y w ∧ refl_trans_clos R xₙ w
Theorem: strong_confluent_implies_confluent
Proof state before:
case a.step.intro.base.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₂
a✝ : R x₂ y₂
w : A
h✝ : refl_trans_clos R y₂ w ∧ refl_trans_clos R xₙ w
⊢ refl_trans_clos R y w ∧ refl_trans_clos R xₙ w
Tactic:
constructor
Proof state after:
case a.step.intro.base.intro.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
y₂ : A
h : refl_trans_clos R y y₂ ∧ refl_clos R x₂ y₂
a✝ : R x₂ y₂
w : A
h✝ : refl_trans_clos R y₂ w ∧ refl_trans_clos R xₙ w
⊢ refl_trans_clos R y w

case a.step.intro.base.intro.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
y₂ : A
h : refl_trans_clos R y y₂ ∧ refl_clos R x₂ y₂
a✝ : R x₂ y₂
w : A
h✝ : refl_trans_clos R y₂ w ∧ refl_trans_clos R xₙ w
⊢ refl_trans_clos R xₙ w
Theorem: strong_confluent_implies_confluent
Proof state before:
case a.step.intro.base.intro.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
y₂ : A
h : refl_trans_clos R y y₂ ∧ refl_clos R x₂ y₂
a✝ : R x₂ y₂
w : A
h✝ : refl_trans_clos R y₂ w ∧ refl_trans_clos R xₙ w
⊢ refl_trans_clos R y w

case a.step.intro.base.intro.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
y₂ : A
h : refl_trans_clos R y y₂ ∧ refl_clos R x₂ y₂
a✝ : R x₂ y₂
w : A
h✝ : refl_trans_clos R y₂ w ∧ refl_trans_clos R xₙ w
⊢ refl_trans_clos R xₙ w
Tactic:
. apply refl_trans_clos_transitive
  . apply h.1
  . aesop
Proof state after:
case a.step.intro.base.intro.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
y₂ : A
h : refl_trans_clos R y y₂ ∧ refl_clos R x₂ y₂
a✝ : R x₂ y₂
w : A
h✝ : refl_trans_clos R y₂ w ∧ refl_trans_clos R xₙ w
⊢ refl_trans_clos R xₙ w
Theorem: strong_confluent_implies_confluent
Proof state before:
case a.step.intro.base.intro.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
y₂ : A
h : refl_trans_clos R y y₂ ∧ refl_clos R x₂ y₂
a✝ : R x₂ y₂
w : A
h✝ : refl_trans_clos R y₂ w ∧ refl_trans_clos R xₙ w
⊢ refl_trans_clos R xₙ w
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
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:
apply ih
Proof state after:
case red_x_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
y₂ : A
h : refl_trans_clos R y y₂ ∧ refl_clos R x₂ y₂
a✝ : R x₂ y₂
⊢ R x₂ y₂
Theorem: strong_confluent_implies_confluent
Proof state before:
case red_x_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
y₂ : A
h : refl_trans_clos R y y₂ ∧ refl_clos R x₂ y₂
a✝ : R x₂ y₂
⊢ R x₂ y₂
Tactic:
trivial
Proof state after:
no goals
Theorem: strong_confluent_implies_confluent
Proof state before:
case a.step.intro.base.intro.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
y₂ : A
h : refl_trans_clos R y y₂ ∧ refl_clos R x₂ y₂
a✝ : R x₂ y₂
w : A
h✝ : refl_trans_clos R y₂ w ∧ refl_trans_clos R xₙ w
⊢ refl_trans_clos R y w
Tactic:
apply refl_trans_clos_transitive
Proof state after:
case a.step.intro.base.intro.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
y₂ : A
h : refl_trans_clos R y y₂ ∧ refl_clos R x₂ y₂
a✝ : R x₂ y₂
w : A
h✝ : refl_trans_clos R y₂ w ∧ refl_trans_clos R xₙ w
⊢ refl_trans_clos R y ?a.step.intro.base.intro.left.y✝

case a.step.intro.base.intro.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
y₂ : A
h : refl_trans_clos R y y₂ ∧ refl_clos R x₂ y₂
a✝ : R x₂ y₂
w : A
h✝ : refl_trans_clos R y₂ w ∧ refl_trans_clos R xₙ w
⊢ refl_trans_clos R ?a.step.intro.base.intro.left.y✝ w

case a.step.intro.base.intro.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
y₂ : A
h : refl_trans_clos R y y₂ ∧ refl_clos R x₂ y₂
a✝ : R x₂ y₂
w : A
h✝ : refl_trans_clos R y₂ w ∧ refl_trans_clos R xₙ w
⊢ A
Theorem: strong_confluent_implies_confluent
Proof state before:
case a.step.intro.base.intro.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
y₂ : A
h : refl_trans_clos R y y₂ ∧ refl_clos R x₂ y₂
a✝ : R x₂ y₂
w : A
h✝ : refl_trans_clos R y₂ w ∧ refl_trans_clos R xₙ w
⊢ refl_trans_clos R y ?a.step.intro.base.intro.left.y✝

case a.step.intro.base.intro.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
y₂ : A
h : refl_trans_clos R y y₂ ∧ refl_clos R x₂ y₂
a✝ : R x₂ y₂
w : A
h✝ : refl_trans_clos R y₂ w ∧ refl_trans_clos R xₙ w
⊢ refl_trans_clos R ?a.step.intro.base.intro.left.y✝ w

case a.step.intro.base.intro.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
y₂ : A
h : refl_trans_clos R y y₂ ∧ refl_clos R x₂ y₂
a✝ : R x₂ y₂
w : A
h✝ : refl_trans_clos R y₂ w ∧ refl_trans_clos R xₙ w
⊢ A
Tactic:
. apply h.1
Proof state after:
case a.step.intro.base.intro.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
y₂ : A
h : refl_trans_clos R y y₂ ∧ refl_clos R x₂ y₂
a✝ : R x₂ y₂
w : A
h✝ : refl_trans_clos R y₂ w ∧ refl_trans_clos R xₙ w
⊢ refl_trans_clos R y₂ w
Theorem: strong_confluent_implies_confluent
Proof state before:
case a.step.intro.base.intro.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
y₂ : A
h : refl_trans_clos R y y₂ ∧ refl_clos R x₂ y₂
a✝ : R x₂ y₂
w : A
h✝ : refl_trans_clos R y₂ w ∧ refl_trans_clos R xₙ w
⊢ refl_trans_clos R y₂ w
Tactic:
. aesop
Proof state after:
no goals
Theorem: strong_confluent_implies_confluent
Proof state before:
case a.step.intro.base.intro.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
y₂ : A
h : refl_trans_clos R y y₂ ∧ refl_clos R x₂ y₂
a✝ : R x₂ y₂
w : A
h✝ : refl_trans_clos R y₂ w ∧ refl_trans_clos R xₙ w
⊢ refl_trans_clos R y ?a.step.intro.base.intro.left.y✝
Tactic:
apply h.1
Proof state after:
no goals
Theorem: strong_confluent_implies_confluent
Proof state before:
case a.step.intro.base.intro.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
y₂ : A
h : refl_trans_clos R y y₂ ∧ refl_clos R x₂ y₂
a✝ : R x₂ y₂
w : A
h✝ : refl_trans_clos R y₂ w ∧ refl_trans_clos R xₙ w
⊢ refl_trans_clos R y₂ w
Tactic:
aesop
Proof state after:
no goals
Theorem: strong_confluent_implies_confluent
Proof state before:
case a.step.intro.base.intro.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
y₂ : A
h : refl_trans_clos R y y₂ ∧ refl_clos R x₂ y₂
a✝ : R x₂ y₂
w : A
h✝ : refl_trans_clos R y₂ w ∧ refl_trans_clos R xₙ w
⊢ refl_trans_clos R xₙ w
Tactic:
aesop
Proof state after:
no goals
Theorem: refl_trans_union_left
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 => refl_trans_clos R x x_1)
    (refl_trans_clos ((fun R S x y => R x y ∨ S x y) R S))
Tactic:
simp
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
⊢ ∀ (x y : A), refl_trans_clos R x y → refl_trans_clos (fun x y => R x y ∨ S x y) x y
Theorem: refl_trans_union_left
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
⊢ ∀ (x y : A), refl_trans_clos R x y → refl_trans_clos (fun x y => R x y ∨ S x y) x y
Tactic:
intros x y red_x_y
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
x y : A
red_x_y : refl_trans_clos R x y
⊢ refl_trans_clos (fun x y => R x y ∨ S x y) x y
Theorem: refl_trans_union_left
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
x y : A
red_x_y : refl_trans_clos R x y
⊢ refl_trans_clos (fun x y => R x y ∨ S x y) x y
Tactic:
induction red_x_y <;> aesop
Proof state after:
no goals
Theorem: refl_trans_union_right
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 => refl_trans_clos S x x_1)
    (refl_trans_clos ((fun R S x y => R x y ∨ S x y) R S))
Tactic:
simp
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
⊢ ∀ (x y : A), refl_trans_clos S x y → refl_trans_clos (fun x y => R x y ∨ S x y) x y
Theorem: refl_trans_union_right
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
⊢ ∀ (x y : A), refl_trans_clos S x y → refl_trans_clos (fun x y => R x y ∨ S x y) x y
Tactic:
intros x y red_x_y
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
x y : A
red_x_y : refl_trans_clos S x y
⊢ refl_trans_clos (fun x y => R x y ∨ S x y) x y
Theorem: refl_trans_union_right
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
x y : A
red_x_y : refl_trans_clos S x y
⊢ refl_trans_clos (fun x y => R x y ∨ S x y) x y
Tactic:
induction red_x_y <;> aesop
Proof state after:
no goals
Theorem: commuting_confluence_implies_confluence
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
⊢ commute R S → confluent R → confluent S → confluent ((fun R S x y => R x y ∨ S x y) R S)
Tactic:
intros commut_r_s conf_r conf_s
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
⊢ confluent ((fun R S x y => R x y ∨ S x y) R S)
Theorem: commuting_confluence_implies_confluence
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
⊢ confluent ((fun R S x y => R x y ∨ S x y) R S)
Tactic:
apply inc_refl_trans_confl
Proof state after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
⊢ ∀ (x y : A), (fun x x_1 => (fun R S x y => R x y ∨ S x y) R S x x_1) x y → (fun x x_1 => ?S x x_1) x y

case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
⊢ ∀ (x y : A),
    (fun x x_1 => ?S x x_1) x y → (fun x x_1 => refl_trans_clos ((fun R S x y => R x y ∨ S x y) R S) x x_1) x y

case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
⊢ confluent ?S

case S
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
⊢ A → A → Prop
Theorem: commuting_confluence_implies_confluence
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
⊢ ∀ (x y : A), (fun x x_1 => (fun R S x y => R x y ∨ S x y) R S x x_1) x y → (fun x x_1 => ?S x x_1) x y

case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
⊢ ∀ (x y : A),
    (fun x x_1 => ?S x x_1) x y → (fun x x_1 => refl_trans_clos ((fun R S x y => R x y ∨ S x y) R S) x x_1) x y

case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
⊢ confluent ?S

case S
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
⊢ A → A → Prop
Tactic:
. have h : R ∪ S ⊆ (. ~>₁* .) ∘ (. ~>₂* .) :=
    by
      simp; intros x y red_or
      cases red_or
      . exists y; aesop
      . exists x; aesop
  apply h
Proof state after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
⊢ ∀ (x y : A),
    (fun x x_1 => ∃ z, (fun x x_2 => refl_trans_clos R x x_2) x z ∧ (fun x x_2 => refl_trans_clos S x x_2) z x_1) x y →
      (fun x x_1 => refl_trans_clos ((fun R S x y => R x y ∨ S x y) R S) x x_1) x y

case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
⊢ confluent fun x y => ∃ z, (fun x x_1 => refl_trans_clos R x x_1) x z ∧ (fun x x_1 => refl_trans_clos S x x_1) z y
Theorem: commuting_confluence_implies_confluence
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
⊢ ∀ (x y : A),
    (fun x x_1 => ∃ z, (fun x x_2 => refl_trans_clos R x x_2) x z ∧ (fun x x_2 => refl_trans_clos S x x_2) z x_1) x y →
      (fun x x_1 => refl_trans_clos ((fun R S x y => R x y ∨ S x y) R S) x x_1) x y

case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
⊢ confluent fun x y => ∃ z, (fun x x_1 => refl_trans_clos R x x_1) x z ∧ (fun x x_1 => refl_trans_clos S x x_1) z y
Tactic:
. simp
  intros x y z red_x_z red_z_y
  apply refl_trans_clos_transitive
  . apply refl_trans_union_left
    trivial
  . apply refl_trans_union_right; trivial
Proof state after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
⊢ confluent fun x y => ∃ z, (fun x x_1 => refl_trans_clos R x x_1) x z ∧ (fun x x_1 => refl_trans_clos S x x_1) z y
Theorem: commuting_confluence_implies_confluence
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
⊢ confluent fun x y => ∃ z, (fun x x_1 => refl_trans_clos R x x_1) x z ∧ (fun x x_1 => refl_trans_clos S x x_1) z y
Tactic:
. apply diamond_implies_confluent
  simp [diamond]
  intros x y z y1 red_x_y1 red_y1_y
  intros z1 red_x_z1 red_z1_z
  have wedge_y1_z1 : wedge R y1 z1 :=
    by exists x
  have join_y1_z1 := conf_r _ _ wedge_y1_z1
  cases' join_y1_z1 with w h
  clear wedge_y1_z1
  have h1 := commut_r_s _ _ _ h.1 red_y1_y
  have h2 := commut_r_s _ _ _ h.2 red_z1_z
  cases' h1 with w1 h1
  cases' h2 with w2 h2
  have wedge_w1_w2 : wedge S w1 w2 :=
    by exists w; aesop
  have join_w1_w2 : joins S w1 w2 := by apply conf_s; trivial
  cases' join_w1_w2 with omega h3
  clear wedge_w1_w2
  exists omega; constructor
  . exists w1; aesop
  . exists w2; aesop
Proof state after:
no goals