Theorem: newmans_lemma (Traat/chapter1.lean)

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ normalizing R → weakly_confluent R → confluent R
Tactic:
intros norm_R weak
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
⊢ confluent R

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
⊢ confluent R
Tactic:
intros y z wedge
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
y z : A
wedge : _root_.wedge R y z
⊢ joins R y z

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
y z : A
wedge : _root_.wedge R y z
⊢ joins R y z
Tactic:
cases wedge
State after:
case intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
y z w✝ : A
h✝ : refl_trans_clos R w✝ y ∧ refl_trans_clos R w✝ z
⊢ joins R y z

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
y z x : A
h : refl_trans_clos R x y ∧ refl_trans_clos R x z
⊢ joins R y z
Tactic:
case intro x h =>
revert h z y
have norm_trans := normalizes_trans _ norm_R
have h :=
  normalizes_ind (. ~>+ .)
  (λ x ↦ ∀ y z, x ~>* y ∧ x ~>* z → y ~>*.*<~ z)
intros y z wedge
(apply h <;> try trivial) <;> try apply norm_trans
clear h
intros x ih y z wedge
cases wedge.1
. exists z; aesop
. case a.step y' red_x_y' red_y'_y =>
  cases wedge.2
  . exists y; aesop
  . case step z' red_x_z' red_z'_z =>
    have join1 := weak _ _ _ red_x_y' red_x_z'
    cases' join1 with w h'
    have join2 : y ~>*.*<~ w :=
    by
      apply ih
      . apply trans_clos.base
        apply red_x_y'
      . aesop
    have join3 : z ~>*.*<~ w :=
    by
      apply ih
      . apply trans_clos.base
        apply red_x_z'
      . aesop
    cases' join2 with w1 h1
    cases' join3 with w2 h2
    have red_x_w : x ~>+ w :=
      by
        apply refl_trans_step_is_trans
        . apply red_x_z'
        . apply h'.2
    have join4 : w1 ~>*.*<~ w2 :=
    by
      apply ih
      . apply red_x_w
      . aesop
     
    cases' join4 with omega h3
    exists omega; constructor
    . apply refl_trans_clos_transitive
      . apply h1.1
      . apply h3.1
    . apply refl_trans_clos_transitive
      . apply h2.1
      . apply h3.2
State after:
no goals

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
y z x : A
h : refl_trans_clos R x y ∧ refl_trans_clos R x z
⊢ joins R y z
Tactic:
revert h z y
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
x : A
⊢ ∀ (y z : A), refl_trans_clos R x y ∧ refl_trans_clos R x z → joins R y z

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm_R : normalizing R
weak : weakly_confluent R
x : A
⊢ ∀ (y z : A), refl_trans_clos R x y ∧ refl_trans_clos R x z → joins R y z
Tactic:
have norm_trans := normalizes_trans _ norm_R
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), refl_trans_clos R x y ∧ refl_trans_clos R x z → joins R y z

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), refl_trans_clos R x y ∧ refl_trans_clos R x z → joins R y z
Tactic:
have h :=
  normalizes_ind (. ~>+ .)
  (λ x ↦ ∀ y z, x ~>* y ∧ x ~>* z → y ~>*.*<~ z)
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
h :
  (∀ (x : A),
      (∀ (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), refl_trans_clos R x y ∧ refl_trans_clos R x z → joins R y z) →
    ∀ (x : A),
      normalizes (fun x x_1 => trans_clos R x x_1) x →
        ∀ (y z : A), refl_trans_clos R x y ∧ refl_trans_clos R x z → joins R y z
⊢ ∀ (y z : A), refl_trans_clos R x y ∧ refl_trans_clos R x z → joins R y z

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
h :
  (∀ (x : A),
      (∀ (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), refl_trans_clos R x y ∧ refl_trans_clos R x z → joins R y z) →
    ∀ (x : A),
      normalizes (fun x x_1 => trans_clos R x x_1) x →
        ∀ (y z : A), refl_trans_clos R x y ∧ refl_trans_clos R x z → joins R y z
⊢ ∀ (y z : A), refl_trans_clos R x y ∧ refl_trans_clos R x z → joins R y z
Tactic:
intros y z wedge
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
h :
  (∀ (x : A),
      (∀ (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), refl_trans_clos R x y ∧ refl_trans_clos R x z → joins R y z) →
    ∀ (x : A),
      normalizes (fun x x_1 => trans_clos R x x_1) x →
        ∀ (y z : A), refl_trans_clos R x y ∧ refl_trans_clos R x z → joins R y z
y z : A
wedge : refl_trans_clos R x y ∧ refl_trans_clos R x z
⊢ joins R y z

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
h :
  (∀ (x : A),
      (∀ (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), refl_trans_clos R x y ∧ refl_trans_clos R x z → joins R y z) →
    ∀ (x : A),
      normalizes (fun x x_1 => trans_clos R x x_1) x →
        ∀ (y z : A), refl_trans_clos R x y ∧ refl_trans_clos R x z → joins R y z
y z : A
wedge : refl_trans_clos R x y ∧ refl_trans_clos R x z
⊢ joins R y z
Tactic:
(apply h <;> try trivial) <;> try apply norm_trans
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
h :
  (∀ (x : A),
      (∀ (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), refl_trans_clos R x y ∧ refl_trans_clos R x z → joins R y z) →
    ∀ (x : A),
      normalizes (fun x x_1 => trans_clos R x x_1) x →
        ∀ (y z : A), refl_trans_clos R x y ∧ refl_trans_clos R x z → joins R y z
y z : A
wedge : refl_trans_clos R x y ∧ refl_trans_clos R x z
⊢ ∀ (x : A),
    (∀ (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), refl_trans_clos R x y ∧ refl_trans_clos R x z → joins R y z

State before:
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
h :
  (∀ (x : A),
      (∀ (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), refl_trans_clos R x y ∧ refl_trans_clos R x z → joins R y z) →
    ∀ (x : A),
      normalizes (fun x x_1 => trans_clos R x x_1) x →
        ∀ (y z : A), refl_trans_clos R x y ∧ refl_trans_clos R x z → joins R y z
y z : A
wedge : refl_trans_clos R x y ∧ refl_trans_clos R x z
⊢ ∀ (x : A),
    (∀ (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), refl_trans_clos R x y ∧ refl_trans_clos R x z → joins R y z
Tactic:
clear h
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),
    (∀ (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), refl_trans_clos R x y ∧ refl_trans_clos R x z → joins R y z

State before:
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),
    (∀ (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), refl_trans_clos R x y ∧ refl_trans_clos R x z → joins R y z
Tactic:
intros x ih y z wedge
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
⊢ joins R y z

State before:
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
⊢ joins R y z
Tactic:
cases wedge.1
State after:
case a.refl
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
z : A
wedge : refl_trans_clos R x x ∧ refl_trans_clos R x z
⊢ joins R x z

case a.step
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
b✝ : A
a✝¹ : R x b✝
a✝ : refl_trans_clos R b✝ y
⊢ joins R y z

State before:
case a.refl
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
z : A
wedge : refl_trans_clos R x x ∧ refl_trans_clos R x z
⊢ joins R x z

case a.step
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
b✝ : A
a✝¹ : R x b✝
a✝ : refl_trans_clos R b✝ y
⊢ joins R y z
Tactic:
. exists z; aesop
State after:
case a.step
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
b✝ : A
a✝¹ : R x b✝
a✝ : refl_trans_clos R b✝ y
⊢ joins R y z

State before:
case a.step
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
b✝ : A
a✝¹ : R x b✝
a✝ : refl_trans_clos R b✝ y
⊢ joins R y z
Tactic:
. case a.step y' red_x_y' red_y'_y =>
  cases wedge.2
  . exists y; aesop
  . case step z' red_x_z' red_z'_z =>
    have join1 := weak _ _ _ red_x_y' red_x_z'
    cases' join1 with w h'
    have join2 : y ~>*.*<~ w :=
    by
      apply ih
      . apply trans_clos.base
        apply red_x_y'
      . aesop
    have join3 : z ~>*.*<~ w :=
    by
      apply ih
      . apply trans_clos.base
        apply red_x_z'
      . aesop
    cases' join2 with w1 h1
    cases' join3 with w2 h2
    have red_x_w : x ~>+ w :=
      by
        apply refl_trans_step_is_trans
        . apply red_x_z'
        . apply h'.2
    have join4 : w1 ~>*.*<~ w2 :=
    by
      apply ih
      . apply red_x_w
      . aesop
     
    cases' join4 with omega h3
    exists omega; constructor
    . apply refl_trans_clos_transitive
      . apply h1.1
      . apply h3.1
    . apply refl_trans_clos_transitive
      . apply h2.1
      . apply h3.2
State after:
no goals

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
h :
  (∀ (x : A),
      (∀ (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), refl_trans_clos R x y ∧ refl_trans_clos R x z → joins R y z) →
    ∀ (x : A),
      normalizes (fun x x_1 => trans_clos R x x_1) x →
        ∀ (y z : A), refl_trans_clos R x y ∧ refl_trans_clos R x z → joins R y z
y z : A
wedge : refl_trans_clos R x y ∧ refl_trans_clos R x z
⊢ joins R y z
Tactic:
apply h <;> try trivial
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
h :
  (∀ (x : A),
      (∀ (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), refl_trans_clos R x y ∧ refl_trans_clos R x z → joins R y z) →
    ∀ (x : A),
      normalizes (fun x x_1 => trans_clos R x x_1) x →
        ∀ (y z : A), refl_trans_clos R x y ∧ refl_trans_clos R x z → joins R y z
y z : A
wedge : refl_trans_clos R x y ∧ refl_trans_clos R x z
⊢ ∀ (x : A),
    (∀ (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), refl_trans_clos R x y ∧ refl_trans_clos R x z → joins R y z

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
h :
  (∀ (x : A),
      (∀ (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), refl_trans_clos R x y ∧ refl_trans_clos R x z → joins R y z) →
    ∀ (x : A),
      normalizes (fun x x_1 => trans_clos R x x_1) x →
        ∀ (y z : A), refl_trans_clos R x y ∧ refl_trans_clos R x z → joins R y z
y z : A
wedge : refl_trans_clos R x y ∧ refl_trans_clos R x z
⊢ normalizes (fun x x_1 => trans_clos R x x_1) x

State before:
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
h :
  (∀ (x : A),
      (∀ (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), refl_trans_clos R x y ∧ refl_trans_clos R x z → joins R y z) →
    ∀ (x : A),
      normalizes (fun x x_1 => trans_clos R x x_1) x →
        ∀ (y z : A), refl_trans_clos R x y ∧ refl_trans_clos R x z → joins R y z
y z : A
wedge : refl_trans_clos R x y ∧ refl_trans_clos R x z
⊢ refl_trans_clos R ?x y ∧ refl_trans_clos R ?x z
Tactic:
trivial
State after:
no goals

State before:
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
h :
  (∀ (x : A),
      (∀ (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), refl_trans_clos R x y ∧ refl_trans_clos R x z → joins R y z) →
    ∀ (x : A),
      normalizes (fun x x_1 => trans_clos R x x_1) x →
        ∀ (y z : A), refl_trans_clos R x y ∧ refl_trans_clos R x z → joins R y z
y z : A
wedge : refl_trans_clos R x y ∧ refl_trans_clos R x z
⊢ normalizes (fun x x_1 => trans_clos R x x_1) x
Tactic:
apply norm_trans
State after:
no goals

State before:
case a.refl
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
z : A
wedge : refl_trans_clos R x x ∧ refl_trans_clos R x z
⊢ joins R x z
Tactic:
exists z
State after:
case a.refl
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
z : A
wedge : refl_trans_clos R x x ∧ refl_trans_clos R x z
⊢ refl_trans_clos R x z ∧ refl_trans_clos R z z

State before:
case a.refl
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
z : A
wedge : refl_trans_clos R x x ∧ refl_trans_clos R x z
⊢ refl_trans_clos R x z ∧ refl_trans_clos R z z
Tactic:
aesop
State after:
no goals

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
⊢ joins R y z
Tactic:
case a.step y' red_x_y' red_y'_y =>
cases wedge.2
. exists y; aesop
. case step z' red_x_z' red_z'_z =>
  have join1 := weak _ _ _ red_x_y' red_x_z'
  cases' join1 with w h'
  have join2 : y ~>*.*<~ w :=
  by
    apply ih
    . apply trans_clos.base
      apply red_x_y'
    . aesop
  have join3 : z ~>*.*<~ w :=
  by
    apply ih
    . apply trans_clos.base
      apply red_x_z'
    . aesop
  cases' join2 with w1 h1
  cases' join3 with w2 h2
  have red_x_w : x ~>+ w :=
    by
      apply refl_trans_step_is_trans
      . apply red_x_z'
      . apply h'.2
  have join4 : w1 ~>*.*<~ w2 :=
  by
    apply ih
    . apply red_x_w
    . aesop
   
  cases' join4 with omega h3
  exists omega; constructor
  . apply refl_trans_clos_transitive
    . apply h1.1
    . apply h3.1
  . apply refl_trans_clos_transitive
    . apply h2.1
    . apply h3.2
State after:
no goals

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
⊢ joins R y z
Tactic:
cases wedge.2
State after:
case refl
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 y' : A
red_x_y' : R x y'
red_y'_y : refl_trans_clos R y' y
wedge : refl_trans_clos R x y ∧ refl_trans_clos R x x
⊢ joins R y x

case step
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
b✝ : A
a✝¹ : R x b✝
a✝ : refl_trans_clos R b✝ z
⊢ joins R y z

State before:
case refl
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 y' : A
red_x_y' : R x y'
red_y'_y : refl_trans_clos R y' y
wedge : refl_trans_clos R x y ∧ refl_trans_clos R x x
⊢ joins R y x

case step
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
b✝ : A
a✝¹ : R x b✝
a✝ : refl_trans_clos R b✝ z
⊢ joins R y z
Tactic:
. exists y; aesop
State after:
case step
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
b✝ : A
a✝¹ : R x b✝
a✝ : refl_trans_clos R b✝ z
⊢ joins R y z

State before:
case step
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
b✝ : A
a✝¹ : R x b✝
a✝ : refl_trans_clos R b✝ z
⊢ joins R y z
Tactic:
. case step z' red_x_z' red_z'_z =>
  have join1 := weak _ _ _ red_x_y' red_x_z'
  cases' join1 with w h'
  have join2 : y ~>*.*<~ w :=
  by
    apply ih
    . apply trans_clos.base
      apply red_x_y'
    . aesop
  have join3 : z ~>*.*<~ w :=
  by
    apply ih
    . apply trans_clos.base
      apply red_x_z'
    . aesop
  cases' join2 with w1 h1
  cases' join3 with w2 h2
  have red_x_w : x ~>+ w :=
    by
      apply refl_trans_step_is_trans
      . apply red_x_z'
      . apply h'.2
  have join4 : w1 ~>*.*<~ w2 :=
  by
    apply ih
    . apply red_x_w
    . aesop
   
  cases' join4 with omega h3
  exists omega; constructor
  . apply refl_trans_clos_transitive
    . apply h1.1
    . apply h3.1
  . apply refl_trans_clos_transitive
    . apply h2.1
    . apply h3.2
State after:
no goals

State before:
case refl
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 y' : A
red_x_y' : R x y'
red_y'_y : refl_trans_clos R y' y
wedge : refl_trans_clos R x y ∧ refl_trans_clos R x x
⊢ joins R y x
Tactic:
exists y
State after:
case refl
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 y' : A
red_x_y' : R x y'
red_y'_y : refl_trans_clos R y' y
wedge : refl_trans_clos R x y ∧ refl_trans_clos R x x
⊢ refl_trans_clos R y y ∧ refl_trans_clos R x y

State before:
case refl
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 y' : A
red_x_y' : R x y'
red_y'_y : refl_trans_clos R y' y
wedge : refl_trans_clos R x y ∧ refl_trans_clos R x x
⊢ refl_trans_clos R y y ∧ refl_trans_clos R x y
Tactic:
aesop
State after:
no goals

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:
case step z' red_x_z' red_z'_z =>
have join1 := weak _ _ _ red_x_y' red_x_z'
cases' join1 with w h'
have join2 : y ~>*.*<~ w :=
by
  apply ih
  . apply trans_clos.base
    apply red_x_y'
  . aesop
have join3 : z ~>*.*<~ w :=
by
  apply ih
  . apply trans_clos.base
    apply red_x_z'
  . aesop
cases' join2 with w1 h1
cases' join3 with w2 h2
have red_x_w : x ~>+ w :=
  by
    apply refl_trans_step_is_trans
    . apply red_x_z'
    . apply h'.2
have join4 : w1 ~>*.*<~ w2 :=
by
  apply ih
  . apply red_x_w
  . aesop
 
cases' join4 with omega h3
exists omega; constructor
. apply refl_trans_clos_transitive
  . apply h1.1
  . apply h3.1
. apply refl_trans_clos_transitive
  . apply h2.1
  . apply h3.2
State after:
no goals

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'
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

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'
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
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

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
State after:
no goals

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
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

State before:
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
Tactic:
. apply trans_clos.base
  apply red_x_y'
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
⊢ refl_trans_clos R y' y ∧ refl_trans_clos R y' w

State before:
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
Tactic:
. aesop
State after:
no goals

State before:
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
Tactic:
apply trans_clos.base
State after:
case a.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
⊢ R x ?y

State before:
case a.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
⊢ R x ?y
Tactic:
apply red_x_y'
State after:
no goals

State before:
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
Tactic:
aesop
State after:
no goals

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
join2 : joins R y w
⊢ joins R z w
Tactic:
apply ih
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
join2 : joins R y 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
join2 : joins R y w
⊢ refl_trans_clos R ?y z ∧ 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
join2 : joins R y w
⊢ A

State before:
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
join2 : joins R y 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
join2 : joins R y w
⊢ refl_trans_clos R ?y z ∧ 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
join2 : joins R y w
⊢ A
Tactic:
. apply trans_clos.base
  apply red_x_z'
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
join2 : joins R y w
⊢ refl_trans_clos R z' z ∧ refl_trans_clos R z' w

State before:
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
join2 : joins R y w
⊢ refl_trans_clos R z' z ∧ refl_trans_clos R z' w
Tactic:
. aesop
State after:
no goals

State before:
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
join2 : joins R y w
⊢ trans_clos R x ?y
Tactic:
apply trans_clos.base
State after:
case a.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
join2 : joins R y w
⊢ R x ?y

State before:
case a.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
join2 : joins R y w
⊢ R x ?y
Tactic:
apply red_x_z'
State after:
no goals

State before:
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
join2 : joins R y w
⊢ refl_trans_clos R z' z ∧ refl_trans_clos R z' w
Tactic:
aesop
State after:
no goals

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
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
⊢ trans_clos R x w
Tactic:
apply refl_trans_step_is_trans
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
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
⊢ R x ?z

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
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
⊢ refl_trans_clos R ?z w

case z
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
⊢ A

State before:
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
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
⊢ R x ?z

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
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
⊢ refl_trans_clos R ?z w

case z
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
⊢ A
Tactic:
. apply red_x_z'
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
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
⊢ refl_trans_clos R z' w

State before:
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
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
⊢ refl_trans_clos R z' w
Tactic:
. apply h'.2
State after:
no goals

State before:
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
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
⊢ R x ?z
Tactic:
apply red_x_z'
State after:
no goals

State before:
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
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
⊢ refl_trans_clos R z' w
Tactic:
apply h'.2
State after:
no goals

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
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 w1 w2
Tactic:
apply ih
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
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
⊢ 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
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
⊢ refl_trans_clos R ?y w1 ∧ refl_trans_clos R ?y w2

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
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
⊢ A

State before:
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
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
⊢ 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
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
⊢ refl_trans_clos R ?y w1 ∧ refl_trans_clos R ?y w2

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
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
⊢ A
Tactic:
. apply red_x_w
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
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
⊢ refl_trans_clos R w w1 ∧ refl_trans_clos R w w2

State before:
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
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
⊢ refl_trans_clos R w w1 ∧ refl_trans_clos R w w2
Tactic:
. aesop
State after:
no goals

State before:
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
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
⊢ trans_clos R x ?y
Tactic:
apply red_x_w
State after:
no goals

State before:
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
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
⊢ refl_trans_clos R w w1 ∧ refl_trans_clos R w w2
Tactic:
aesop
State after:
no goals

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
Tactic:
apply refl_trans_clos_transitive
State after:
case intro.intro.intro.intro.left.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
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 ?intro.intro.intro.intro.left.y

case intro.intro.intro.intro.left.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
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 ?intro.intro.intro.intro.left.y omega

case intro.intro.intro.intro.left.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
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
⊢ A

State before:
case intro.intro.intro.intro.left.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
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 ?intro.intro.intro.intro.left.y

case intro.intro.intro.intro.left.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
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 ?intro.intro.intro.intro.left.y omega

case intro.intro.intro.intro.left.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
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
⊢ A
Tactic:
. apply h1.1
State after:
case intro.intro.intro.intro.left.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
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 w1 omega

State before:
case intro.intro.intro.intro.left.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
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 w1 omega
Tactic:
. apply h3.1
State after:
no goals

State before:
case intro.intro.intro.intro.left.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
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 ?intro.intro.intro.intro.left.y
Tactic:
apply h1.1
State after:
no goals

State before:
case intro.intro.intro.intro.left.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
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 w1 omega
Tactic:
apply h3.1
State after:
no goals

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
State after:
case intro.intro.intro.intro.right.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
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 ?intro.intro.intro.intro.right.y

case intro.intro.intro.intro.right.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
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 ?intro.intro.intro.intro.right.y omega

case intro.intro.intro.intro.right.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
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
⊢ A

State before:
case intro.intro.intro.intro.right.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
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 ?intro.intro.intro.intro.right.y

case intro.intro.intro.intro.right.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
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 ?intro.intro.intro.intro.right.y omega

case intro.intro.intro.intro.right.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
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
⊢ A
Tactic:
. apply h2.1
State after:
case intro.intro.intro.intro.right.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
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 w2 omega

State before:
case intro.intro.intro.intro.right.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
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 w2 omega
Tactic:
. apply h3.2
State after:
no goals

State before:
case intro.intro.intro.intro.right.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
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 ?intro.intro.intro.intro.right.y
Tactic:
apply h2.1
State after:
no goals

State before:
case intro.intro.intro.intro.right.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
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 w2 omega
Tactic:
apply h3.2
State after:
no goals