internlm/Lean-Github huggingface dataset:
Theorem: newmans_lemma
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
x✝ : A
norm_trans : normalizing fun x x_1 => trans_clos R x x_1
y✝ z✝ : A
wedge✝ : refl_trans_clos R x✝ y✝ ∧ refl_trans_clos R x✝ z✝
x : A
ih : ∀ (y : A), trans_clos R x y → ∀ (y_1 z : A), refl_trans_clos R y y_1 ∧ refl_trans_clos R y z → joins R y_1 z
y z : A
wedge : refl_trans_clos R x y ∧ refl_trans_clos R x z
y' : A
red_x_y' : R x y'
red_y'_y : refl_trans_clos R y' y
z' : A
red_x_z' : R x z'
red_z'_z : refl_trans_clos R z' z
⊢ joins R y z
Tactic:
have join1 := weak _ _ _ red_x_y' red_x_z'
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
x✝ : A
norm_trans : normalizing fun x x_1 => trans_clos R x x_1
y✝ z✝ : A
wedge✝ : refl_trans_clos R x✝ y✝ ∧ refl_trans_clos R x✝ z✝
x : A
ih : ∀ (y : A), trans_clos R x y → ∀ (y_1 z : A), refl_trans_clos R y y_1 ∧ refl_trans_clos R y z → joins R y_1 z
y z : A
wedge : refl_trans_clos R x y ∧ refl_trans_clos R x z
y' : A
red_x_y' : R x y'
red_y'_y : refl_trans_clos R y' y
z' : A
red_x_z' : R x z'
red_z'_z : refl_trans_clos R z' z
join1 : joins R y' z'
⊢ joins R y z
Theorem: newmans_lemma
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
x✝ : A
norm_trans : normalizing fun x x_1 => trans_clos R x x_1
y✝ z✝ : A
wedge✝ : refl_trans_clos R x✝ y✝ ∧ refl_trans_clos R x✝ z✝
x : A
ih : ∀ (y : A), trans_clos R x y → ∀ (y_1 z : A), refl_trans_clos R y y_1 ∧ refl_trans_clos R y z → joins R y_1 z
y z : A
wedge : refl_trans_clos R x y ∧ refl_trans_clos R x z
y' : A
red_x_y' : R x y'
red_y'_y : refl_trans_clos R y' y
z' : A
red_x_z' : R x z'
red_z'_z : refl_trans_clos R z' z
join1 : joins R y' z'
⊢ joins R y z
Tactic:
cases' join1 with w h'
Proof state after:
case intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
x✝ : A
norm_trans : normalizing fun x x_1 => trans_clos R x x_1
y✝ z✝ : A
wedge✝ : refl_trans_clos R x✝ y✝ ∧ refl_trans_clos R x✝ z✝
x : A
ih : ∀ (y : A), trans_clos R x y → ∀ (y_1 z : A), refl_trans_clos R y y_1 ∧ refl_trans_clos R y z → joins R y_1 z
y z : A
wedge : refl_trans_clos R x y ∧ refl_trans_clos R x z
y' : A
red_x_y' : R x y'
red_y'_y : refl_trans_clos R y' y
z' : A
red_x_z' : R x z'
red_z'_z : refl_trans_clos R z' z
w : A
h' : refl_trans_clos R y' w ∧ refl_trans_clos R z' w
⊢ joins R y z
Theorem: newmans_lemma
Proof state before:
case intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
x✝ : A
norm_trans : normalizing fun x x_1 => trans_clos R x x_1
y✝ z✝ : A
wedge✝ : refl_trans_clos R x✝ y✝ ∧ refl_trans_clos R x✝ z✝
x : A
ih : ∀ (y : A), trans_clos R x y → ∀ (y_1 z : A), refl_trans_clos R y y_1 ∧ refl_trans_clos R y z → joins R y_1 z
y z : A
wedge : refl_trans_clos R x y ∧ refl_trans_clos R x z
y' : A
red_x_y' : R x y'
red_y'_y : refl_trans_clos R y' y
z' : A
red_x_z' : R x z'
red_z'_z : refl_trans_clos R z' z
w : A
h' : refl_trans_clos R y' w ∧ refl_trans_clos R z' w
⊢ joins R y z
Tactic:
have join2 : y ~>*.*<~ w :=
by
  apply ih
  . apply trans_clos.base
    apply red_x_y'
  . aesop
Proof state after:
case intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
x✝ : A
norm_trans : normalizing fun x x_1 => trans_clos R x x_1
y✝ z✝ : A
wedge✝ : refl_trans_clos R x✝ y✝ ∧ refl_trans_clos R x✝ z✝
x : A
ih : ∀ (y : A), trans_clos R x y → ∀ (y_1 z : A), refl_trans_clos R y y_1 ∧ refl_trans_clos R y z → joins R y_1 z
y z : A
wedge : refl_trans_clos R x y ∧ refl_trans_clos R x z
y' : A
red_x_y' : R x y'
red_y'_y : refl_trans_clos R y' y
z' : A
red_x_z' : R x z'
red_z'_z : refl_trans_clos R z' z
w : A
h' : refl_trans_clos R y' w ∧ refl_trans_clos R z' w
join2 : joins R y w
⊢ joins R y z
Theorem: newmans_lemma
Proof state before:
case intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
x✝ : A
norm_trans : normalizing fun x x_1 => trans_clos R x x_1
y✝ z✝ : A
wedge✝ : refl_trans_clos R x✝ y✝ ∧ refl_trans_clos R x✝ z✝
x : A
ih : ∀ (y : A), trans_clos R x y → ∀ (y_1 z : A), refl_trans_clos R y y_1 ∧ refl_trans_clos R y z → joins R y_1 z
y z : A
wedge : refl_trans_clos R x y ∧ refl_trans_clos R x z
y' : A
red_x_y' : R x y'
red_y'_y : refl_trans_clos R y' y
z' : A
red_x_z' : R x z'
red_z'_z : refl_trans_clos R z' z
w : A
h' : refl_trans_clos R y' w ∧ refl_trans_clos R z' w
join2 : joins R y w
⊢ joins R y z
Tactic:
have join3 : z ~>*.*<~ w :=
by
  apply ih
  . apply trans_clos.base
    apply red_x_z'
  . aesop
Proof state after:
case intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
x✝ : A
norm_trans : normalizing fun x x_1 => trans_clos R x x_1
y✝ z✝ : A
wedge✝ : refl_trans_clos R x✝ y✝ ∧ refl_trans_clos R x✝ z✝
x : A
ih : ∀ (y : A), trans_clos R x y → ∀ (y_1 z : A), refl_trans_clos R y y_1 ∧ refl_trans_clos R y z → joins R y_1 z
y z : A
wedge : refl_trans_clos R x y ∧ refl_trans_clos R x z
y' : A
red_x_y' : R x y'
red_y'_y : refl_trans_clos R y' y
z' : A
red_x_z' : R x z'
red_z'_z : refl_trans_clos R z' z
w : A
h' : refl_trans_clos R y' w ∧ refl_trans_clos R z' w
join2 : joins R y w
join3 : joins R z w
⊢ joins R y z
Theorem: newmans_lemma
Proof state before:
case intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
x✝ : A
norm_trans : normalizing fun x x_1 => trans_clos R x x_1
y✝ z✝ : A
wedge✝ : refl_trans_clos R x✝ y✝ ∧ refl_trans_clos R x✝ z✝
x : A
ih : ∀ (y : A), trans_clos R x y → ∀ (y_1 z : A), refl_trans_clos R y y_1 ∧ refl_trans_clos R y z → joins R y_1 z
y z : A
wedge : refl_trans_clos R x y ∧ refl_trans_clos R x z
y' : A
red_x_y' : R x y'
red_y'_y : refl_trans_clos R y' y
z' : A
red_x_z' : R x z'
red_z'_z : refl_trans_clos R z' z
w : A
h' : refl_trans_clos R y' w ∧ refl_trans_clos R z' w
join2 : joins R y w
join3 : joins R z w
⊢ joins R y z
Tactic:
cases' join2 with w1 h1
Proof state after:
case intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
x✝ : A
norm_trans : normalizing fun x x_1 => trans_clos R x x_1
y✝ z✝ : A
wedge✝ : refl_trans_clos R x✝ y✝ ∧ refl_trans_clos R x✝ z✝
x : A
ih : ∀ (y : A), trans_clos R x y → ∀ (y_1 z : A), refl_trans_clos R y y_1 ∧ refl_trans_clos R y z → joins R y_1 z
y z : A
wedge : refl_trans_clos R x y ∧ refl_trans_clos R x z
y' : A
red_x_y' : R x y'
red_y'_y : refl_trans_clos R y' y
z' : A
red_x_z' : R x z'
red_z'_z : refl_trans_clos R z' z
w : A
h' : refl_trans_clos R y' w ∧ refl_trans_clos R z' w
join3 : joins R z w
w1 : A
h1 : refl_trans_clos R y w1 ∧ refl_trans_clos R w w1
⊢ joins R y z
Theorem: newmans_lemma
Proof state before:
case intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
x✝ : A
norm_trans : normalizing fun x x_1 => trans_clos R x x_1
y✝ z✝ : A
wedge✝ : refl_trans_clos R x✝ y✝ ∧ refl_trans_clos R x✝ z✝
x : A
ih : ∀ (y : A), trans_clos R x y → ∀ (y_1 z : A), refl_trans_clos R y y_1 ∧ refl_trans_clos R y z → joins R y_1 z
y z : A
wedge : refl_trans_clos R x y ∧ refl_trans_clos R x z
y' : A
red_x_y' : R x y'
red_y'_y : refl_trans_clos R y' y
z' : A
red_x_z' : R x z'
red_z'_z : refl_trans_clos R z' z
w : A
h' : refl_trans_clos R y' w ∧ refl_trans_clos R z' w
join3 : joins R z w
w1 : A
h1 : refl_trans_clos R y w1 ∧ refl_trans_clos R w w1
⊢ joins R y z
Tactic:
cases' join3 with w2 h2
Proof state after:
case intro.intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
x✝ : A
norm_trans : normalizing fun x x_1 => trans_clos R x x_1
y✝ z✝ : A
wedge✝ : refl_trans_clos R x✝ y✝ ∧ refl_trans_clos R x✝ z✝
x : A
ih : ∀ (y : A), trans_clos R x y → ∀ (y_1 z : A), refl_trans_clos R y y_1 ∧ refl_trans_clos R y z → joins R y_1 z
y z : A
wedge : refl_trans_clos R x y ∧ refl_trans_clos R x z
y' : A
red_x_y' : R x y'
red_y'_y : refl_trans_clos R y' y
z' : A
red_x_z' : R x z'
red_z'_z : refl_trans_clos R z' z
w : A
h' : refl_trans_clos R y' w ∧ refl_trans_clos R z' w
w1 : A
h1 : refl_trans_clos R y w1 ∧ refl_trans_clos R w w1
w2 : A
h2 : refl_trans_clos R z w2 ∧ refl_trans_clos R w w2
⊢ joins R y z
Theorem: newmans_lemma
Proof state before:
case intro.intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
x✝ : A
norm_trans : normalizing fun x x_1 => trans_clos R x x_1
y✝ z✝ : A
wedge✝ : refl_trans_clos R x✝ y✝ ∧ refl_trans_clos R x✝ z✝
x : A
ih : ∀ (y : A), trans_clos R x y → ∀ (y_1 z : A), refl_trans_clos R y y_1 ∧ refl_trans_clos R y z → joins R y_1 z
y z : A
wedge : refl_trans_clos R x y ∧ refl_trans_clos R x z
y' : A
red_x_y' : R x y'
red_y'_y : refl_trans_clos R y' y
z' : A
red_x_z' : R x z'
red_z'_z : refl_trans_clos R z' z
w : A
h' : refl_trans_clos R y' w ∧ refl_trans_clos R z' w
w1 : A
h1 : refl_trans_clos R y w1 ∧ refl_trans_clos R w w1
w2 : A
h2 : refl_trans_clos R z w2 ∧ refl_trans_clos R w w2
⊢ joins R y z
Tactic:
have red_x_w : x ~>+ w :=
  by
    apply refl_trans_step_is_trans
    . apply red_x_z'
    . apply h'.2
Proof state after:
case intro.intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
x✝ : A
norm_trans : normalizing fun x x_1 => trans_clos R x x_1
y✝ z✝ : A
wedge✝ : refl_trans_clos R x✝ y✝ ∧ refl_trans_clos R x✝ z✝
x : A
ih : ∀ (y : A), trans_clos R x y → ∀ (y_1 z : A), refl_trans_clos R y y_1 ∧ refl_trans_clos R y z → joins R y_1 z
y z : A
wedge : refl_trans_clos R x y ∧ refl_trans_clos R x z
y' : A
red_x_y' : R x y'
red_y'_y : refl_trans_clos R y' y
z' : A
red_x_z' : R x z'
red_z'_z : refl_trans_clos R z' z
w : A
h' : refl_trans_clos R y' w ∧ refl_trans_clos R z' w
w1 : A
h1 : refl_trans_clos R y w1 ∧ refl_trans_clos R w w1
w2 : A
h2 : refl_trans_clos R z w2 ∧ refl_trans_clos R w w2
red_x_w : trans_clos R x w
⊢ joins R y z
Theorem: newmans_lemma
Proof state before:
case intro.intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
x✝ : A
norm_trans : normalizing fun x x_1 => trans_clos R x x_1
y✝ z✝ : A
wedge✝ : refl_trans_clos R x✝ y✝ ∧ refl_trans_clos R x✝ z✝
x : A
ih : ∀ (y : A), trans_clos R x y → ∀ (y_1 z : A), refl_trans_clos R y y_1 ∧ refl_trans_clos R y z → joins R y_1 z
y z : A
wedge : refl_trans_clos R x y ∧ refl_trans_clos R x z
y' : A
red_x_y' : R x y'
red_y'_y : refl_trans_clos R y' y
z' : A
red_x_z' : R x z'
red_z'_z : refl_trans_clos R z' z
w : A
h' : refl_trans_clos R y' w ∧ refl_trans_clos R z' w
w1 : A
h1 : refl_trans_clos R y w1 ∧ refl_trans_clos R w w1
w2 : A
h2 : refl_trans_clos R z w2 ∧ refl_trans_clos R w w2
red_x_w : trans_clos R x w
⊢ joins R y z
Tactic:
have join4 : w1 ~>*.*<~ w2 :=
by
  apply ih
  . apply red_x_w
  . aesop
Proof state after:
case intro.intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
x✝ : A
norm_trans : normalizing fun x x_1 => trans_clos R x x_1
y✝ z✝ : A
wedge✝ : refl_trans_clos R x✝ y✝ ∧ refl_trans_clos R x✝ z✝
x : A
ih : ∀ (y : A), trans_clos R x y → ∀ (y_1 z : A), refl_trans_clos R y y_1 ∧ refl_trans_clos R y z → joins R y_1 z
y z : A
wedge : refl_trans_clos R x y ∧ refl_trans_clos R x z
y' : A
red_x_y' : R x y'
red_y'_y : refl_trans_clos R y' y
z' : A
red_x_z' : R x z'
red_z'_z : refl_trans_clos R z' z
w : A
h' : refl_trans_clos R y' w ∧ refl_trans_clos R z' w
w1 : A
h1 : refl_trans_clos R y w1 ∧ refl_trans_clos R w w1
w2 : A
h2 : refl_trans_clos R z w2 ∧ refl_trans_clos R w w2
red_x_w : trans_clos R x w
join4 : joins R w1 w2
⊢ joins R y z
Theorem: newmans_lemma
Proof state before:
case intro.intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
x✝ : A
norm_trans : normalizing fun x x_1 => trans_clos R x x_1
y✝ z✝ : A
wedge✝ : refl_trans_clos R x✝ y✝ ∧ refl_trans_clos R x✝ z✝
x : A
ih : ∀ (y : A), trans_clos R x y → ∀ (y_1 z : A), refl_trans_clos R y y_1 ∧ refl_trans_clos R y z → joins R y_1 z
y z : A
wedge : refl_trans_clos R x y ∧ refl_trans_clos R x z
y' : A
red_x_y' : R x y'
red_y'_y : refl_trans_clos R y' y
z' : A
red_x_z' : R x z'
red_z'_z : refl_trans_clos R z' z
w : A
h' : refl_trans_clos R y' w ∧ refl_trans_clos R z' w
w1 : A
h1 : refl_trans_clos R y w1 ∧ refl_trans_clos R w w1
w2 : A
h2 : refl_trans_clos R z w2 ∧ refl_trans_clos R w w2
red_x_w : trans_clos R x w
join4 : joins R w1 w2
⊢ joins R y z
Tactic:
cases' join4 with omega h3
Proof state after:
case intro.intro.intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
x✝ : A
norm_trans : normalizing fun x x_1 => trans_clos R x x_1
y✝ z✝ : A
wedge✝ : refl_trans_clos R x✝ y✝ ∧ refl_trans_clos R x✝ z✝
x : A
ih : ∀ (y : A), trans_clos R x y → ∀ (y_1 z : A), refl_trans_clos R y y_1 ∧ refl_trans_clos R y z → joins R y_1 z
y z : A
wedge : refl_trans_clos R x y ∧ refl_trans_clos R x z
y' : A
red_x_y' : R x y'
red_y'_y : refl_trans_clos R y' y
z' : A
red_x_z' : R x z'
red_z'_z : refl_trans_clos R z' z
w : A
h' : refl_trans_clos R y' w ∧ refl_trans_clos R z' w
w1 : A
h1 : refl_trans_clos R y w1 ∧ refl_trans_clos R w w1
w2 : A
h2 : refl_trans_clos R z w2 ∧ refl_trans_clos R w w2
red_x_w : trans_clos R x w
omega : A
h3 : refl_trans_clos R w1 omega ∧ refl_trans_clos R w2 omega
⊢ joins R y z
Theorem: newmans_lemma
Proof state before:
case intro.intro.intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
x✝ : A
norm_trans : normalizing fun x x_1 => trans_clos R x x_1
y✝ z✝ : A
wedge✝ : refl_trans_clos R x✝ y✝ ∧ refl_trans_clos R x✝ z✝
x : A
ih : ∀ (y : A), trans_clos R x y → ∀ (y_1 z : A), refl_trans_clos R y y_1 ∧ refl_trans_clos R y z → joins R y_1 z
y z : A
wedge : refl_trans_clos R x y ∧ refl_trans_clos R x z
y' : A
red_x_y' : R x y'
red_y'_y : refl_trans_clos R y' y
z' : A
red_x_z' : R x z'
red_z'_z : refl_trans_clos R z' z
w : A
h' : refl_trans_clos R y' w ∧ refl_trans_clos R z' w
w1 : A
h1 : refl_trans_clos R y w1 ∧ refl_trans_clos R w w1
w2 : A
h2 : refl_trans_clos R z w2 ∧ refl_trans_clos R w w2
red_x_w : trans_clos R x w
omega : A
h3 : refl_trans_clos R w1 omega ∧ refl_trans_clos R w2 omega
⊢ joins R y z
Tactic:
exists omega
Proof state after:
case intro.intro.intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
x✝ : A
norm_trans : normalizing fun x x_1 => trans_clos R x x_1
y✝ z✝ : A
wedge✝ : refl_trans_clos R x✝ y✝ ∧ refl_trans_clos R x✝ z✝
x : A
ih : ∀ (y : A), trans_clos R x y → ∀ (y_1 z : A), refl_trans_clos R y y_1 ∧ refl_trans_clos R y z → joins R y_1 z
y z : A
wedge : refl_trans_clos R x y ∧ refl_trans_clos R x z
y' : A
red_x_y' : R x y'
red_y'_y : refl_trans_clos R y' y
z' : A
red_x_z' : R x z'
red_z'_z : refl_trans_clos R z' z
w : A
h' : refl_trans_clos R y' w ∧ refl_trans_clos R z' w
w1 : A
h1 : refl_trans_clos R y w1 ∧ refl_trans_clos R w w1
w2 : A
h2 : refl_trans_clos R z w2 ∧ refl_trans_clos R w w2
red_x_w : trans_clos R x w
omega : A
h3 : refl_trans_clos R w1 omega ∧ refl_trans_clos R w2 omega
⊢ refl_trans_clos R y omega ∧ refl_trans_clos R z omega
Theorem: newmans_lemma
Proof state before:
case intro.intro.intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
x✝ : A
norm_trans : normalizing fun x x_1 => trans_clos R x x_1
y✝ z✝ : A
wedge✝ : refl_trans_clos R x✝ y✝ ∧ refl_trans_clos R x✝ z✝
x : A
ih : ∀ (y : A), trans_clos R x y → ∀ (y_1 z : A), refl_trans_clos R y y_1 ∧ refl_trans_clos R y z → joins R y_1 z
y z : A
wedge : refl_trans_clos R x y ∧ refl_trans_clos R x z
y' : A
red_x_y' : R x y'
red_y'_y : refl_trans_clos R y' y
z' : A
red_x_z' : R x z'
red_z'_z : refl_trans_clos R z' z
w : A
h' : refl_trans_clos R y' w ∧ refl_trans_clos R z' w
w1 : A
h1 : refl_trans_clos R y w1 ∧ refl_trans_clos R w w1
w2 : A
h2 : refl_trans_clos R z w2 ∧ refl_trans_clos R w w2
red_x_w : trans_clos R x w
omega : A
h3 : refl_trans_clos R w1 omega ∧ refl_trans_clos R w2 omega
⊢ refl_trans_clos R y omega ∧ refl_trans_clos R z omega
Tactic:
constructor
Proof state after:
case intro.intro.intro.intro.left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
x✝ : A
norm_trans : normalizing fun x x_1 => trans_clos R x x_1
y✝ z✝ : A
wedge✝ : refl_trans_clos R x✝ y✝ ∧ refl_trans_clos R x✝ z✝
x : A
ih : ∀ (y : A), trans_clos R x y → ∀ (y_1 z : A), refl_trans_clos R y y_1 ∧ refl_trans_clos R y z → joins R y_1 z
y z : A
wedge : refl_trans_clos R x y ∧ refl_trans_clos R x z
y' : A
red_x_y' : R x y'
red_y'_y : refl_trans_clos R y' y
z' : A
red_x_z' : R x z'
red_z'_z : refl_trans_clos R z' z
w : A
h' : refl_trans_clos R y' w ∧ refl_trans_clos R z' w
w1 : A
h1 : refl_trans_clos R y w1 ∧ refl_trans_clos R w w1
w2 : A
h2 : refl_trans_clos R z w2 ∧ refl_trans_clos R w w2
red_x_w : trans_clos R x w
omega : A
h3 : refl_trans_clos R w1 omega ∧ refl_trans_clos R w2 omega
⊢ refl_trans_clos R y omega

case intro.intro.intro.intro.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
x✝ : A
norm_trans : normalizing fun x x_1 => trans_clos R x x_1
y✝ z✝ : A
wedge✝ : refl_trans_clos R x✝ y✝ ∧ refl_trans_clos R x✝ z✝
x : A
ih : ∀ (y : A), trans_clos R x y → ∀ (y_1 z : A), refl_trans_clos R y y_1 ∧ refl_trans_clos R y z → joins R y_1 z
y z : A
wedge : refl_trans_clos R x y ∧ refl_trans_clos R x z
y' : A
red_x_y' : R x y'
red_y'_y : refl_trans_clos R y' y
z' : A
red_x_z' : R x z'
red_z'_z : refl_trans_clos R z' z
w : A
h' : refl_trans_clos R y' w ∧ refl_trans_clos R z' w
w1 : A
h1 : refl_trans_clos R y w1 ∧ refl_trans_clos R w w1
w2 : A
h2 : refl_trans_clos R z w2 ∧ refl_trans_clos R w w2
red_x_w : trans_clos R x w
omega : A
h3 : refl_trans_clos R w1 omega ∧ refl_trans_clos R w2 omega
⊢ refl_trans_clos R z omega
Theorem: newmans_lemma
Proof state before:
case intro.intro.intro.intro.left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
x✝ : A
norm_trans : normalizing fun x x_1 => trans_clos R x x_1
y✝ z✝ : A
wedge✝ : refl_trans_clos R x✝ y✝ ∧ refl_trans_clos R x✝ z✝
x : A
ih : ∀ (y : A), trans_clos R x y → ∀ (y_1 z : A), refl_trans_clos R y y_1 ∧ refl_trans_clos R y z → joins R y_1 z
y z : A
wedge : refl_trans_clos R x y ∧ refl_trans_clos R x z
y' : A
red_x_y' : R x y'
red_y'_y : refl_trans_clos R y' y
z' : A
red_x_z' : R x z'
red_z'_z : refl_trans_clos R z' z
w : A
h' : refl_trans_clos R y' w ∧ refl_trans_clos R z' w
w1 : A
h1 : refl_trans_clos R y w1 ∧ refl_trans_clos R w w1
w2 : A
h2 : refl_trans_clos R z w2 ∧ refl_trans_clos R w w2
red_x_w : trans_clos R x w
omega : A
h3 : refl_trans_clos R w1 omega ∧ refl_trans_clos R w2 omega
⊢ refl_trans_clos R y omega

case intro.intro.intro.intro.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
x✝ : A
norm_trans : normalizing fun x x_1 => trans_clos R x x_1
y✝ z✝ : A
wedge✝ : refl_trans_clos R x✝ y✝ ∧ refl_trans_clos R x✝ z✝
x : A
ih : ∀ (y : A), trans_clos R x y → ∀ (y_1 z : A), refl_trans_clos R y y_1 ∧ refl_trans_clos R y z → joins R y_1 z
y z : A
wedge : refl_trans_clos R x y ∧ refl_trans_clos R x z
y' : A
red_x_y' : R x y'
red_y'_y : refl_trans_clos R y' y
z' : A
red_x_z' : R x z'
red_z'_z : refl_trans_clos R z' z
w : A
h' : refl_trans_clos R y' w ∧ refl_trans_clos R z' w
w1 : A
h1 : refl_trans_clos R y w1 ∧ refl_trans_clos R w w1
w2 : A
h2 : refl_trans_clos R z w2 ∧ refl_trans_clos R w w2
red_x_w : trans_clos R x w
omega : A
h3 : refl_trans_clos R w1 omega ∧ refl_trans_clos R w2 omega
⊢ refl_trans_clos R z omega
Tactic:
. apply refl_trans_clos_transitive
  . apply h1.1
  . apply h3.1
Proof state after:
case intro.intro.intro.intro.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
x✝ : A
norm_trans : normalizing fun x x_1 => trans_clos R x x_1
y✝ z✝ : A
wedge✝ : refl_trans_clos R x✝ y✝ ∧ refl_trans_clos R x✝ z✝
x : A
ih : ∀ (y : A), trans_clos R x y → ∀ (y_1 z : A), refl_trans_clos R y y_1 ∧ refl_trans_clos R y z → joins R y_1 z
y z : A
wedge : refl_trans_clos R x y ∧ refl_trans_clos R x z
y' : A
red_x_y' : R x y'
red_y'_y : refl_trans_clos R y' y
z' : A
red_x_z' : R x z'
red_z'_z : refl_trans_clos R z' z
w : A
h' : refl_trans_clos R y' w ∧ refl_trans_clos R z' w
w1 : A
h1 : refl_trans_clos R y w1 ∧ refl_trans_clos R w w1
w2 : A
h2 : refl_trans_clos R z w2 ∧ refl_trans_clos R w w2
red_x_w : trans_clos R x w
omega : A
h3 : refl_trans_clos R w1 omega ∧ refl_trans_clos R w2 omega
⊢ refl_trans_clos R z omega
Theorem: newmans_lemma
Proof state before:
case intro.intro.intro.intro.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
x✝ : A
norm_trans : normalizing fun x x_1 => trans_clos R x x_1
y✝ z✝ : A
wedge✝ : refl_trans_clos R x✝ y✝ ∧ refl_trans_clos R x✝ z✝
x : A
ih : ∀ (y : A), trans_clos R x y → ∀ (y_1 z : A), refl_trans_clos R y y_1 ∧ refl_trans_clos R y z → joins R y_1 z
y z : A
wedge : refl_trans_clos R x y ∧ refl_trans_clos R x z
y' : A
red_x_y' : R x y'
red_y'_y : refl_trans_clos R y' y
z' : A
red_x_z' : R x z'
red_z'_z : refl_trans_clos R z' z
w : A
h' : refl_trans_clos R y' w ∧ refl_trans_clos R z' w
w1 : A
h1 : refl_trans_clos R y w1 ∧ refl_trans_clos R w w1
w2 : A
h2 : refl_trans_clos R z w2 ∧ refl_trans_clos R w w2
red_x_w : trans_clos R x w
omega : A
h3 : refl_trans_clos R w1 omega ∧ refl_trans_clos R w2 omega
⊢ refl_trans_clos R z omega
Tactic:
. apply refl_trans_clos_transitive
  . apply h2.1
  . apply h3.2
Proof state after:
no goals
Theorem: newmans_lemma
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
x✝ : A
norm_trans : normalizing fun x x_1 => trans_clos R x x_1
y✝ z✝ : A
wedge✝ : refl_trans_clos R x✝ y✝ ∧ refl_trans_clos R x✝ z✝
x : A
ih : ∀ (y : A), trans_clos R x y → ∀ (y_1 z : A), refl_trans_clos R y y_1 ∧ refl_trans_clos R y z → joins R y_1 z
y z : A
wedge : refl_trans_clos R x y ∧ refl_trans_clos R x z
y' : A
red_x_y' : R x y'
red_y'_y : refl_trans_clos R y' y
z' : A
red_x_z' : R x z'
red_z'_z : refl_trans_clos R z' z
w : A
h' : refl_trans_clos R y' w ∧ refl_trans_clos R z' w
⊢ joins R y w
Tactic:
apply ih
Proof state after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
x✝ : A
norm_trans : normalizing fun x x_1 => trans_clos R x x_1
y✝ z✝ : A
wedge✝ : refl_trans_clos R x✝ y✝ ∧ refl_trans_clos R x✝ z✝
x : A
ih : ∀ (y : A), trans_clos R x y → ∀ (y_1 z : A), refl_trans_clos R y y_1 ∧ refl_trans_clos R y z → joins R y_1 z
y z : A
wedge : refl_trans_clos R x y ∧ refl_trans_clos R x z
y' : A
red_x_y' : R x y'
red_y'_y : refl_trans_clos R y' y
z' : A
red_x_z' : R x z'
red_z'_z : refl_trans_clos R z' z
w : A
h' : refl_trans_clos R y' w ∧ refl_trans_clos R z' w
⊢ trans_clos R x ?y

case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
x✝ : A
norm_trans : normalizing fun x x_1 => trans_clos R x x_1
y✝ z✝ : A
wedge✝ : refl_trans_clos R x✝ y✝ ∧ refl_trans_clos R x✝ z✝
x : A
ih : ∀ (y : A), trans_clos R x y → ∀ (y_1 z : A), refl_trans_clos R y y_1 ∧ refl_trans_clos R y z → joins R y_1 z
y z : A
wedge : refl_trans_clos R x y ∧ refl_trans_clos R x z
y' : A
red_x_y' : R x y'
red_y'_y : refl_trans_clos R y' y
z' : A
red_x_z' : R x z'
red_z'_z : refl_trans_clos R z' z
w : A
h' : refl_trans_clos R y' w ∧ refl_trans_clos R z' w
⊢ refl_trans_clos R ?y y ∧ refl_trans_clos R ?y w

case y
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
x✝ : A
norm_trans : normalizing fun x x_1 => trans_clos R x x_1
y✝ z✝ : A
wedge✝ : refl_trans_clos R x✝ y✝ ∧ refl_trans_clos R x✝ z✝
x : A
ih : ∀ (y : A), trans_clos R x y → ∀ (y_1 z : A), refl_trans_clos R y y_1 ∧ refl_trans_clos R y z → joins R y_1 z
y z : A
wedge : refl_trans_clos R x y ∧ refl_trans_clos R x z
y' : A
red_x_y' : R x y'
red_y'_y : refl_trans_clos R y' y
z' : A
red_x_z' : R x z'
red_z'_z : refl_trans_clos R z' z
w : A
h' : refl_trans_clos R y' w ∧ refl_trans_clos R z' w
⊢ A