Theorem: commuting_confluence_implies_confluence (Traat/chapter1.lean)

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
⊢ commute R S → confluent R → confluent S → confluent ((fun R S x y => R x y ∨ S x y) R S)
Tactic:
intros commut_r_s conf_r conf_s
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
⊢ confluent ((fun R S x y => R x y ∨ S x y) R S)

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

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

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

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

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

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

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

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

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

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

case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
⊢ confluent fun x y => ∃ z, (fun x x_1 => refl_trans_clos R x x_1) x z ∧ (fun x x_1 => refl_trans_clos S x x_1) z y
Tactic:
. simp
  intros x y z red_x_z red_z_y
  apply refl_trans_clos_transitive
  . apply refl_trans_union_left
    trivial
  . apply refl_trans_union_right; trivial
State after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
⊢ confluent fun x y => ∃ z, (fun x x_1 => refl_trans_clos R x x_1) x z ∧ (fun x x_1 => refl_trans_clos S x x_1) z y

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

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

State before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
h :
  (fun R R' => ∀ (x y : A), R x y → R' x y) ((fun R S x y => R x y ∨ S x y) R S)
    ((fun R S x y => ∃ z, R x z ∧ S z y) (fun x x_1 => refl_trans_clos R x x_1) fun x x_1 => refl_trans_clos S x x_1)
⊢ ∀ (x y : A), (fun x x_1 => (fun R S x y => R x y ∨ S x y) R S x x_1) x y → (fun x x_1 => ?S x x_1) x y
Tactic:
apply h
State after:
no goals

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
⊢ (fun R R' => ∀ (x y : A), R x y → R' x y) ((fun R S x y => R x y ∨ S x y) R S)
    ((fun R S x y => ∃ z, R x z ∧ S z y) (fun x x_1 => refl_trans_clos R x x_1) fun x x_1 => refl_trans_clos S x x_1)
Tactic:
simp
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
⊢ ∀ (x y : A), R x y ∨ S x y → ∃ z, refl_trans_clos R x z ∧ refl_trans_clos S z y

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
⊢ ∀ (x y : A), R x y ∨ S x y → ∃ z, refl_trans_clos R x z ∧ refl_trans_clos S z y
Tactic:
intros x y red_or
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y : A
red_or : R x y ∨ S x y
⊢ ∃ z, refl_trans_clos R x z ∧ refl_trans_clos S z y

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y : A
red_or : R x y ∨ S x y
⊢ ∃ z, refl_trans_clos R x z ∧ refl_trans_clos S z y
Tactic:
cases red_or
State after:
case inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y : A
h✝ : R x y
⊢ ∃ z, refl_trans_clos R x z ∧ refl_trans_clos S z y

case inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y : A
h✝ : S x y
⊢ ∃ z, refl_trans_clos R x z ∧ refl_trans_clos S z y

State before:
case inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y : A
h✝ : R x y
⊢ ∃ z, refl_trans_clos R x z ∧ refl_trans_clos S z y

case inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y : A
h✝ : S x y
⊢ ∃ z, refl_trans_clos R x z ∧ refl_trans_clos S z y
Tactic:
. exists y; aesop
State after:
case inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y : A
h✝ : S x y
⊢ ∃ z, refl_trans_clos R x z ∧ refl_trans_clos S z y

State before:
case inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y : A
h✝ : S x y
⊢ ∃ z, refl_trans_clos R x z ∧ refl_trans_clos S z y
Tactic:
. exists x; aesop
State after:
no goals

State before:
case inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y : A
h✝ : R x y
⊢ ∃ z, refl_trans_clos R x z ∧ refl_trans_clos S z y
Tactic:
exists y
State after:
case inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y : A
h✝ : R x y
⊢ refl_trans_clos R x y ∧ refl_trans_clos S y y

State before:
case inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y : A
h✝ : R x y
⊢ refl_trans_clos R x y ∧ refl_trans_clos S y y
Tactic:
aesop
State after:
no goals

State before:
case inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y : A
h✝ : S x y
⊢ ∃ z, refl_trans_clos R x z ∧ refl_trans_clos S z y
Tactic:
exists x
State after:
case inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y : A
h✝ : S x y
⊢ refl_trans_clos R x x ∧ refl_trans_clos S x y

State before:
case inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y : A
h✝ : S x y
⊢ refl_trans_clos R x x ∧ refl_trans_clos S x y
Tactic:
aesop
State after:
no goals

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

State before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
⊢ ∀ (x y x_1 : A), refl_trans_clos R x x_1 → refl_trans_clos S x_1 y → refl_trans_clos (fun x y => R x y ∨ S x y) x y
Tactic:
intros x y z red_x_z red_z_y
State after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y z : A
red_x_z : refl_trans_clos R x z
red_z_y : refl_trans_clos S z y
⊢ refl_trans_clos (fun x y => R x y ∨ S x y) x y

State before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y z : A
red_x_z : refl_trans_clos R x z
red_z_y : refl_trans_clos S z y
⊢ refl_trans_clos (fun x y => R x y ∨ S x y) x y
Tactic:
apply refl_trans_clos_transitive
State after:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y z : A
red_x_z : refl_trans_clos R x z
red_z_y : refl_trans_clos S z y
⊢ refl_trans_clos (fun x y => R x y ∨ S x y) x ?a.y✝

case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y z : A
red_x_z : refl_trans_clos R x z
red_z_y : refl_trans_clos S z y
⊢ refl_trans_clos (fun x y => R x y ∨ S x y) ?a.y✝ y

case a.y
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y z : A
red_x_z : refl_trans_clos R x z
red_z_y : refl_trans_clos S z y
⊢ A

State before:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y z : A
red_x_z : refl_trans_clos R x z
red_z_y : refl_trans_clos S z y
⊢ refl_trans_clos (fun x y => R x y ∨ S x y) x ?a.y✝

case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y z : A
red_x_z : refl_trans_clos R x z
red_z_y : refl_trans_clos S z y
⊢ refl_trans_clos (fun x y => R x y ∨ S x y) ?a.y✝ y

case a.y
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y z : A
red_x_z : refl_trans_clos R x z
red_z_y : refl_trans_clos S z y
⊢ A
Tactic:
. apply refl_trans_union_left
  trivial
State after:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y z : A
red_x_z : refl_trans_clos R x z
red_z_y : refl_trans_clos S z y
⊢ refl_trans_clos (fun x y => R x y ∨ S x y) z y

State before:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y z : A
red_x_z : refl_trans_clos R x z
red_z_y : refl_trans_clos S z y
⊢ refl_trans_clos (fun x y => R x y ∨ S x y) z y
Tactic:
. apply refl_trans_union_right; trivial
State after:
no goals

State before:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y z : A
red_x_z : refl_trans_clos R x z
red_z_y : refl_trans_clos S z y
⊢ refl_trans_clos (fun x y => R x y ∨ S x y) x ?a.y✝
Tactic:
apply refl_trans_union_left
State after:
case a.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y z : A
red_x_z : refl_trans_clos R x z
red_z_y : refl_trans_clos S z y
⊢ refl_trans_clos (fun x y => R x y) x ?a.y✝

State before:
case a.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y z : A
red_x_z : refl_trans_clos R x z
red_z_y : refl_trans_clos S z y
⊢ refl_trans_clos (fun x y => R x y) x ?a.y✝
Tactic:
trivial
State after:
no goals

State before:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y z : A
red_x_z : refl_trans_clos R x z
red_z_y : refl_trans_clos S z y
⊢ refl_trans_clos (fun x y => R x y ∨ S x y) z y
Tactic:
apply refl_trans_union_right
State after:
case a.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y z : A
red_x_z : refl_trans_clos R x z
red_z_y : refl_trans_clos S z y
⊢ refl_trans_clos (fun x y => S x y) z y

State before:
case a.a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y z : A
red_x_z : refl_trans_clos R x z
red_z_y : refl_trans_clos S z y
⊢ refl_trans_clos (fun x y => S x y) z y
Tactic:
trivial
State after:
no goals

State before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
⊢ confluent fun x y => ∃ z, (fun x x_1 => refl_trans_clos R x x_1) x z ∧ (fun x x_1 => refl_trans_clos S x x_1) z y
Tactic:
apply diamond_implies_confluent
State after:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
⊢ diamond fun x y => ∃ z, (fun x x_1 => refl_trans_clos R x x_1) x z ∧ (fun x x_1 => refl_trans_clos S x x_1) z y

State before:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
⊢ diamond fun x y => ∃ z, (fun x x_1 => refl_trans_clos R x x_1) x z ∧ (fun x x_1 => refl_trans_clos S x x_1) z y
Tactic:
simp [diamond]
State after:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
⊢ ∀ (x y z x_1 : A),
    refl_trans_clos R x x_1 →
      refl_trans_clos S x_1 y →
        ∀ (x_2 : A),
          refl_trans_clos R x x_2 →
            refl_trans_clos S x_2 z →
              ∃ w,
                (∃ z, refl_trans_clos R y z ∧ refl_trans_clos S z w) ∧
                  ∃ z_1, refl_trans_clos R z z_1 ∧ refl_trans_clos S z_1 w

State before:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
⊢ ∀ (x y z x_1 : A),
    refl_trans_clos R x x_1 →
      refl_trans_clos S x_1 y →
        ∀ (x_2 : A),
          refl_trans_clos R x x_2 →
            refl_trans_clos S x_2 z →
              ∃ w,
                (∃ z, refl_trans_clos R y z ∧ refl_trans_clos S z w) ∧
                  ∃ z_1, refl_trans_clos R z z_1 ∧ refl_trans_clos S z_1 w
Tactic:
intros x y z y1 red_x_y1 red_y1_y
State after:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y z y1 : A
red_x_y1 : refl_trans_clos R x y1
red_y1_y : refl_trans_clos S y1 y
⊢ ∀ (x_1 : A),
    refl_trans_clos R x x_1 →
      refl_trans_clos S x_1 z →
        ∃ w,
          (∃ z, refl_trans_clos R y z ∧ refl_trans_clos S z w) ∧
            ∃ z_1, refl_trans_clos R z z_1 ∧ refl_trans_clos S z_1 w

State before:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y z y1 : A
red_x_y1 : refl_trans_clos R x y1
red_y1_y : refl_trans_clos S y1 y
⊢ ∀ (x_1 : A),
    refl_trans_clos R x x_1 →
      refl_trans_clos S x_1 z →
        ∃ w,
          (∃ z, refl_trans_clos R y z ∧ refl_trans_clos S z w) ∧
            ∃ z_1, refl_trans_clos R z z_1 ∧ refl_trans_clos S z_1 w
Tactic:
intros z1 red_x_z1 red_z1_z
State after:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y z y1 : A
red_x_y1 : refl_trans_clos R x y1
red_y1_y : refl_trans_clos S y1 y
z1 : A
red_x_z1 : refl_trans_clos R x z1
red_z1_z : refl_trans_clos S z1 z
⊢ ∃ w, (∃ z, refl_trans_clos R y z ∧ refl_trans_clos S z w) ∧ ∃ z_1, refl_trans_clos R z z_1 ∧ refl_trans_clos S z_1 w

State before:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y z y1 : A
red_x_y1 : refl_trans_clos R x y1
red_y1_y : refl_trans_clos S y1 y
z1 : A
red_x_z1 : refl_trans_clos R x z1
red_z1_z : refl_trans_clos S z1 z
⊢ ∃ w, (∃ z, refl_trans_clos R y z ∧ refl_trans_clos S z w) ∧ ∃ z_1, refl_trans_clos R z z_1 ∧ refl_trans_clos S z_1 w
Tactic:
have wedge_y1_z1 : wedge R y1 z1 :=
  by exists x
State after:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y z y1 : A
red_x_y1 : refl_trans_clos R x y1
red_y1_y : refl_trans_clos S y1 y
z1 : A
red_x_z1 : refl_trans_clos R x z1
red_z1_z : refl_trans_clos S z1 z
wedge_y1_z1 : wedge R y1 z1
⊢ ∃ w, (∃ z, refl_trans_clos R y z ∧ refl_trans_clos S z w) ∧ ∃ z_1, refl_trans_clos R z z_1 ∧ refl_trans_clos S z_1 w

State before:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y z y1 : A
red_x_y1 : refl_trans_clos R x y1
red_y1_y : refl_trans_clos S y1 y
z1 : A
red_x_z1 : refl_trans_clos R x z1
red_z1_z : refl_trans_clos S z1 z
wedge_y1_z1 : wedge R y1 z1
⊢ ∃ w, (∃ z, refl_trans_clos R y z ∧ refl_trans_clos S z w) ∧ ∃ z_1, refl_trans_clos R z z_1 ∧ refl_trans_clos S z_1 w
Tactic:
have join_y1_z1 := conf_r _ _ wedge_y1_z1
State after:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y z y1 : A
red_x_y1 : refl_trans_clos R x y1
red_y1_y : refl_trans_clos S y1 y
z1 : A
red_x_z1 : refl_trans_clos R x z1
red_z1_z : refl_trans_clos S z1 z
wedge_y1_z1 : wedge R y1 z1
join_y1_z1 : joins R y1 z1
⊢ ∃ w, (∃ z, refl_trans_clos R y z ∧ refl_trans_clos S z w) ∧ ∃ z_1, refl_trans_clos R z z_1 ∧ refl_trans_clos S z_1 w

State before:
case a.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y z y1 : A
red_x_y1 : refl_trans_clos R x y1
red_y1_y : refl_trans_clos S y1 y
z1 : A
red_x_z1 : refl_trans_clos R x z1
red_z1_z : refl_trans_clos S z1 z
wedge_y1_z1 : wedge R y1 z1
join_y1_z1 : joins R y1 z1
⊢ ∃ w, (∃ z, refl_trans_clos R y z ∧ refl_trans_clos S z w) ∧ ∃ z_1, refl_trans_clos R z z_1 ∧ refl_trans_clos S z_1 w
Tactic:
cases' join_y1_z1 with w h
State after:
case a.a.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y z y1 : A
red_x_y1 : refl_trans_clos R x y1
red_y1_y : refl_trans_clos S y1 y
z1 : A
red_x_z1 : refl_trans_clos R x z1
red_z1_z : refl_trans_clos S z1 z
wedge_y1_z1 : wedge R y1 z1
w : A
h : refl_trans_clos R y1 w ∧ refl_trans_clos R z1 w
⊢ ∃ w, (∃ z, refl_trans_clos R y z ∧ refl_trans_clos S z w) ∧ ∃ z_1, refl_trans_clos R z z_1 ∧ refl_trans_clos S z_1 w

State before:
case a.a.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y z y1 : A
red_x_y1 : refl_trans_clos R x y1
red_y1_y : refl_trans_clos S y1 y
z1 : A
red_x_z1 : refl_trans_clos R x z1
red_z1_z : refl_trans_clos S z1 z
wedge_y1_z1 : wedge R y1 z1
w : A
h : refl_trans_clos R y1 w ∧ refl_trans_clos R z1 w
⊢ ∃ w, (∃ z, refl_trans_clos R y z ∧ refl_trans_clos S z w) ∧ ∃ z_1, refl_trans_clos R z z_1 ∧ refl_trans_clos S z_1 w
Tactic:
clear wedge_y1_z1
State after:
case a.a.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y z y1 : A
red_x_y1 : refl_trans_clos R x y1
red_y1_y : refl_trans_clos S y1 y
z1 : A
red_x_z1 : refl_trans_clos R x z1
red_z1_z : refl_trans_clos S z1 z
w : A
h : refl_trans_clos R y1 w ∧ refl_trans_clos R z1 w
⊢ ∃ w, (∃ z, refl_trans_clos R y z ∧ refl_trans_clos S z w) ∧ ∃ z_1, refl_trans_clos R z z_1 ∧ refl_trans_clos S z_1 w

State before:
case a.a.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y z y1 : A
red_x_y1 : refl_trans_clos R x y1
red_y1_y : refl_trans_clos S y1 y
z1 : A
red_x_z1 : refl_trans_clos R x z1
red_z1_z : refl_trans_clos S z1 z
w : A
h : refl_trans_clos R y1 w ∧ refl_trans_clos R z1 w
⊢ ∃ w, (∃ z, refl_trans_clos R y z ∧ refl_trans_clos S z w) ∧ ∃ z_1, refl_trans_clos R z z_1 ∧ refl_trans_clos S z_1 w
Tactic:
have h1 := commut_r_s _ _ _ h.1 red_y1_y
State after:
case a.a.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y z y1 : A
red_x_y1 : refl_trans_clos R x y1
red_y1_y : refl_trans_clos S y1 y
z1 : A
red_x_z1 : refl_trans_clos R x z1
red_z1_z : refl_trans_clos S z1 z
w : A
h : refl_trans_clos R y1 w ∧ refl_trans_clos R z1 w
h1 : ∃ w_1, refl_trans_clos S w w_1 ∧ refl_trans_clos R y w_1
⊢ ∃ w, (∃ z, refl_trans_clos R y z ∧ refl_trans_clos S z w) ∧ ∃ z_1, refl_trans_clos R z z_1 ∧ refl_trans_clos S z_1 w

State before:
case a.a.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y z y1 : A
red_x_y1 : refl_trans_clos R x y1
red_y1_y : refl_trans_clos S y1 y
z1 : A
red_x_z1 : refl_trans_clos R x z1
red_z1_z : refl_trans_clos S z1 z
w : A
h : refl_trans_clos R y1 w ∧ refl_trans_clos R z1 w
h1 : ∃ w_1, refl_trans_clos S w w_1 ∧ refl_trans_clos R y w_1
⊢ ∃ w, (∃ z, refl_trans_clos R y z ∧ refl_trans_clos S z w) ∧ ∃ z_1, refl_trans_clos R z z_1 ∧ refl_trans_clos S z_1 w
Tactic:
have h2 := commut_r_s _ _ _ h.2 red_z1_z
State after:
case a.a.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y z y1 : A
red_x_y1 : refl_trans_clos R x y1
red_y1_y : refl_trans_clos S y1 y
z1 : A
red_x_z1 : refl_trans_clos R x z1
red_z1_z : refl_trans_clos S z1 z
w : A
h : refl_trans_clos R y1 w ∧ refl_trans_clos R z1 w
h1 : ∃ w_1, refl_trans_clos S w w_1 ∧ refl_trans_clos R y w_1
h2 : ∃ w_1, refl_trans_clos S w w_1 ∧ refl_trans_clos R z w_1
⊢ ∃ w, (∃ z, refl_trans_clos R y z ∧ refl_trans_clos S z w) ∧ ∃ z_1, refl_trans_clos R z z_1 ∧ refl_trans_clos S z_1 w

State before:
case a.a.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y z y1 : A
red_x_y1 : refl_trans_clos R x y1
red_y1_y : refl_trans_clos S y1 y
z1 : A
red_x_z1 : refl_trans_clos R x z1
red_z1_z : refl_trans_clos S z1 z
w : A
h : refl_trans_clos R y1 w ∧ refl_trans_clos R z1 w
h1 : ∃ w_1, refl_trans_clos S w w_1 ∧ refl_trans_clos R y w_1
h2 : ∃ w_1, refl_trans_clos S w w_1 ∧ refl_trans_clos R z w_1
⊢ ∃ w, (∃ z, refl_trans_clos R y z ∧ refl_trans_clos S z w) ∧ ∃ z_1, refl_trans_clos R z z_1 ∧ refl_trans_clos S z_1 w
Tactic:
cases' h1 with w1 h1
State after:
case a.a.intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y z y1 : A
red_x_y1 : refl_trans_clos R x y1
red_y1_y : refl_trans_clos S y1 y
z1 : A
red_x_z1 : refl_trans_clos R x z1
red_z1_z : refl_trans_clos S z1 z
w : A
h : refl_trans_clos R y1 w ∧ refl_trans_clos R z1 w
h2 : ∃ w_1, refl_trans_clos S w w_1 ∧ refl_trans_clos R z w_1
w1 : A
h1 : refl_trans_clos S w w1 ∧ refl_trans_clos R y w1
⊢ ∃ w, (∃ z, refl_trans_clos R y z ∧ refl_trans_clos S z w) ∧ ∃ z_1, refl_trans_clos R z z_1 ∧ refl_trans_clos S z_1 w

State before:
case a.a.intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y z y1 : A
red_x_y1 : refl_trans_clos R x y1
red_y1_y : refl_trans_clos S y1 y
z1 : A
red_x_z1 : refl_trans_clos R x z1
red_z1_z : refl_trans_clos S z1 z
w : A
h : refl_trans_clos R y1 w ∧ refl_trans_clos R z1 w
h2 : ∃ w_1, refl_trans_clos S w w_1 ∧ refl_trans_clos R z w_1
w1 : A
h1 : refl_trans_clos S w w1 ∧ refl_trans_clos R y w1
⊢ ∃ w, (∃ z, refl_trans_clos R y z ∧ refl_trans_clos S z w) ∧ ∃ z_1, refl_trans_clos R z z_1 ∧ refl_trans_clos S z_1 w
Tactic:
cases' h2 with w2 h2
State after:
case a.a.intro.intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y z y1 : A
red_x_y1 : refl_trans_clos R x y1
red_y1_y : refl_trans_clos S y1 y
z1 : A
red_x_z1 : refl_trans_clos R x z1
red_z1_z : refl_trans_clos S z1 z
w : A
h : refl_trans_clos R y1 w ∧ refl_trans_clos R z1 w
w1 : A
h1 : refl_trans_clos S w w1 ∧ refl_trans_clos R y w1
w2 : A
h2 : refl_trans_clos S w w2 ∧ refl_trans_clos R z w2
⊢ ∃ w, (∃ z, refl_trans_clos R y z ∧ refl_trans_clos S z w) ∧ ∃ z_1, refl_trans_clos R z z_1 ∧ refl_trans_clos S z_1 w

State before:
case a.a.intro.intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y z y1 : A
red_x_y1 : refl_trans_clos R x y1
red_y1_y : refl_trans_clos S y1 y
z1 : A
red_x_z1 : refl_trans_clos R x z1
red_z1_z : refl_trans_clos S z1 z
w : A
h : refl_trans_clos R y1 w ∧ refl_trans_clos R z1 w
w1 : A
h1 : refl_trans_clos S w w1 ∧ refl_trans_clos R y w1
w2 : A
h2 : refl_trans_clos S w w2 ∧ refl_trans_clos R z w2
⊢ ∃ w, (∃ z, refl_trans_clos R y z ∧ refl_trans_clos S z w) ∧ ∃ z_1, refl_trans_clos R z z_1 ∧ refl_trans_clos S z_1 w
Tactic:
have wedge_w1_w2 : wedge S w1 w2 :=
  by exists w; aesop
State after:
case a.a.intro.intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y z y1 : A
red_x_y1 : refl_trans_clos R x y1
red_y1_y : refl_trans_clos S y1 y
z1 : A
red_x_z1 : refl_trans_clos R x z1
red_z1_z : refl_trans_clos S z1 z
w : A
h : refl_trans_clos R y1 w ∧ refl_trans_clos R z1 w
w1 : A
h1 : refl_trans_clos S w w1 ∧ refl_trans_clos R y w1
w2 : A
h2 : refl_trans_clos S w w2 ∧ refl_trans_clos R z w2
wedge_w1_w2 : wedge S w1 w2
⊢ ∃ w, (∃ z, refl_trans_clos R y z ∧ refl_trans_clos S z w) ∧ ∃ z_1, refl_trans_clos R z z_1 ∧ refl_trans_clos S z_1 w

State before:
case a.a.intro.intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y z y1 : A
red_x_y1 : refl_trans_clos R x y1
red_y1_y : refl_trans_clos S y1 y
z1 : A
red_x_z1 : refl_trans_clos R x z1
red_z1_z : refl_trans_clos S z1 z
w : A
h : refl_trans_clos R y1 w ∧ refl_trans_clos R z1 w
w1 : A
h1 : refl_trans_clos S w w1 ∧ refl_trans_clos R y w1
w2 : A
h2 : refl_trans_clos S w w2 ∧ refl_trans_clos R z w2
wedge_w1_w2 : wedge S w1 w2
⊢ ∃ w, (∃ z, refl_trans_clos R y z ∧ refl_trans_clos S z w) ∧ ∃ z_1, refl_trans_clos R z z_1 ∧ refl_trans_clos S z_1 w
Tactic:
have join_w1_w2 : joins S w1 w2 := by apply conf_s; trivial
State after:
case a.a.intro.intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y z y1 : A
red_x_y1 : refl_trans_clos R x y1
red_y1_y : refl_trans_clos S y1 y
z1 : A
red_x_z1 : refl_trans_clos R x z1
red_z1_z : refl_trans_clos S z1 z
w : A
h : refl_trans_clos R y1 w ∧ refl_trans_clos R z1 w
w1 : A
h1 : refl_trans_clos S w w1 ∧ refl_trans_clos R y w1
w2 : A
h2 : refl_trans_clos S w w2 ∧ refl_trans_clos R z w2
wedge_w1_w2 : wedge S w1 w2
join_w1_w2 : joins S w1 w2
⊢ ∃ w, (∃ z, refl_trans_clos R y z ∧ refl_trans_clos S z w) ∧ ∃ z_1, refl_trans_clos R z z_1 ∧ refl_trans_clos S z_1 w

State before:
case a.a.intro.intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y z y1 : A
red_x_y1 : refl_trans_clos R x y1
red_y1_y : refl_trans_clos S y1 y
z1 : A
red_x_z1 : refl_trans_clos R x z1
red_z1_z : refl_trans_clos S z1 z
w : A
h : refl_trans_clos R y1 w ∧ refl_trans_clos R z1 w
w1 : A
h1 : refl_trans_clos S w w1 ∧ refl_trans_clos R y w1
w2 : A
h2 : refl_trans_clos S w w2 ∧ refl_trans_clos R z w2
wedge_w1_w2 : wedge S w1 w2
join_w1_w2 : joins S w1 w2
⊢ ∃ w, (∃ z, refl_trans_clos R y z ∧ refl_trans_clos S z w) ∧ ∃ z_1, refl_trans_clos R z z_1 ∧ refl_trans_clos S z_1 w
Tactic:
cases' join_w1_w2 with omega h3
State after:
case a.a.intro.intro.intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y z y1 : A
red_x_y1 : refl_trans_clos R x y1
red_y1_y : refl_trans_clos S y1 y
z1 : A
red_x_z1 : refl_trans_clos R x z1
red_z1_z : refl_trans_clos S z1 z
w : A
h : refl_trans_clos R y1 w ∧ refl_trans_clos R z1 w
w1 : A
h1 : refl_trans_clos S w w1 ∧ refl_trans_clos R y w1
w2 : A
h2 : refl_trans_clos S w w2 ∧ refl_trans_clos R z w2
wedge_w1_w2 : wedge S w1 w2
omega : A
h3 : refl_trans_clos S w1 omega ∧ refl_trans_clos S w2 omega
⊢ ∃ w, (∃ z, refl_trans_clos R y z ∧ refl_trans_clos S z w) ∧ ∃ z_1, refl_trans_clos R z z_1 ∧ refl_trans_clos S z_1 w

State before:
case a.a.intro.intro.intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y z y1 : A
red_x_y1 : refl_trans_clos R x y1
red_y1_y : refl_trans_clos S y1 y
z1 : A
red_x_z1 : refl_trans_clos R x z1
red_z1_z : refl_trans_clos S z1 z
w : A
h : refl_trans_clos R y1 w ∧ refl_trans_clos R z1 w
w1 : A
h1 : refl_trans_clos S w w1 ∧ refl_trans_clos R y w1
w2 : A
h2 : refl_trans_clos S w w2 ∧ refl_trans_clos R z w2
wedge_w1_w2 : wedge S w1 w2
omega : A
h3 : refl_trans_clos S w1 omega ∧ refl_trans_clos S w2 omega
⊢ ∃ w, (∃ z, refl_trans_clos R y z ∧ refl_trans_clos S z w) ∧ ∃ z_1, refl_trans_clos R z z_1 ∧ refl_trans_clos S z_1 w
Tactic:
clear wedge_w1_w2
State after:
case a.a.intro.intro.intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y z y1 : A
red_x_y1 : refl_trans_clos R x y1
red_y1_y : refl_trans_clos S y1 y
z1 : A
red_x_z1 : refl_trans_clos R x z1
red_z1_z : refl_trans_clos S z1 z
w : A
h : refl_trans_clos R y1 w ∧ refl_trans_clos R z1 w
w1 : A
h1 : refl_trans_clos S w w1 ∧ refl_trans_clos R y w1
w2 : A
h2 : refl_trans_clos S w w2 ∧ refl_trans_clos R z w2
omega : A
h3 : refl_trans_clos S w1 omega ∧ refl_trans_clos S w2 omega
⊢ ∃ w, (∃ z, refl_trans_clos R y z ∧ refl_trans_clos S z w) ∧ ∃ z_1, refl_trans_clos R z z_1 ∧ refl_trans_clos S z_1 w

State before:
case a.a.intro.intro.intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y z y1 : A
red_x_y1 : refl_trans_clos R x y1
red_y1_y : refl_trans_clos S y1 y
z1 : A
red_x_z1 : refl_trans_clos R x z1
red_z1_z : refl_trans_clos S z1 z
w : A
h : refl_trans_clos R y1 w ∧ refl_trans_clos R z1 w
w1 : A
h1 : refl_trans_clos S w w1 ∧ refl_trans_clos R y w1
w2 : A
h2 : refl_trans_clos S w w2 ∧ refl_trans_clos R z w2
omega : A
h3 : refl_trans_clos S w1 omega ∧ refl_trans_clos S w2 omega
⊢ ∃ w, (∃ z, refl_trans_clos R y z ∧ refl_trans_clos S z w) ∧ ∃ z_1, refl_trans_clos R z z_1 ∧ refl_trans_clos S z_1 w
Tactic:
exists omega
State after:
case a.a.intro.intro.intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y z y1 : A
red_x_y1 : refl_trans_clos R x y1
red_y1_y : refl_trans_clos S y1 y
z1 : A
red_x_z1 : refl_trans_clos R x z1
red_z1_z : refl_trans_clos S z1 z
w : A
h : refl_trans_clos R y1 w ∧ refl_trans_clos R z1 w
w1 : A
h1 : refl_trans_clos S w w1 ∧ refl_trans_clos R y w1
w2 : A
h2 : refl_trans_clos S w w2 ∧ refl_trans_clos R z w2
omega : A
h3 : refl_trans_clos S w1 omega ∧ refl_trans_clos S w2 omega
⊢ (∃ z, refl_trans_clos R y z ∧ refl_trans_clos S z omega) ∧
    ∃ z_1, refl_trans_clos R z z_1 ∧ refl_trans_clos S z_1 omega

State before:
case a.a.intro.intro.intro.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y z y1 : A
red_x_y1 : refl_trans_clos R x y1
red_y1_y : refl_trans_clos S y1 y
z1 : A
red_x_z1 : refl_trans_clos R x z1
red_z1_z : refl_trans_clos S z1 z
w : A
h : refl_trans_clos R y1 w ∧ refl_trans_clos R z1 w
w1 : A
h1 : refl_trans_clos S w w1 ∧ refl_trans_clos R y w1
w2 : A
h2 : refl_trans_clos S w w2 ∧ refl_trans_clos R z w2
omega : A
h3 : refl_trans_clos S w1 omega ∧ refl_trans_clos S w2 omega
⊢ (∃ z, refl_trans_clos R y z ∧ refl_trans_clos S z omega) ∧
    ∃ z_1, refl_trans_clos R z z_1 ∧ refl_trans_clos S z_1 omega
Tactic:
constructor
State after:
case a.a.intro.intro.intro.intro.left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y z y1 : A
red_x_y1 : refl_trans_clos R x y1
red_y1_y : refl_trans_clos S y1 y
z1 : A
red_x_z1 : refl_trans_clos R x z1
red_z1_z : refl_trans_clos S z1 z
w : A
h : refl_trans_clos R y1 w ∧ refl_trans_clos R z1 w
w1 : A
h1 : refl_trans_clos S w w1 ∧ refl_trans_clos R y w1
w2 : A
h2 : refl_trans_clos S w w2 ∧ refl_trans_clos R z w2
omega : A
h3 : refl_trans_clos S w1 omega ∧ refl_trans_clos S w2 omega
⊢ ∃ z, refl_trans_clos R y z ∧ refl_trans_clos S z omega

case a.a.intro.intro.intro.intro.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y z y1 : A
red_x_y1 : refl_trans_clos R x y1
red_y1_y : refl_trans_clos S y1 y
z1 : A
red_x_z1 : refl_trans_clos R x z1
red_z1_z : refl_trans_clos S z1 z
w : A
h : refl_trans_clos R y1 w ∧ refl_trans_clos R z1 w
w1 : A
h1 : refl_trans_clos S w w1 ∧ refl_trans_clos R y w1
w2 : A
h2 : refl_trans_clos S w w2 ∧ refl_trans_clos R z w2
omega : A
h3 : refl_trans_clos S w1 omega ∧ refl_trans_clos S w2 omega
⊢ ∃ z_1, refl_trans_clos R z z_1 ∧ refl_trans_clos S z_1 omega

State before:
case a.a.intro.intro.intro.intro.left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y z y1 : A
red_x_y1 : refl_trans_clos R x y1
red_y1_y : refl_trans_clos S y1 y
z1 : A
red_x_z1 : refl_trans_clos R x z1
red_z1_z : refl_trans_clos S z1 z
w : A
h : refl_trans_clos R y1 w ∧ refl_trans_clos R z1 w
w1 : A
h1 : refl_trans_clos S w w1 ∧ refl_trans_clos R y w1
w2 : A
h2 : refl_trans_clos S w w2 ∧ refl_trans_clos R z w2
omega : A
h3 : refl_trans_clos S w1 omega ∧ refl_trans_clos S w2 omega
⊢ ∃ z, refl_trans_clos R y z ∧ refl_trans_clos S z omega

case a.a.intro.intro.intro.intro.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y z y1 : A
red_x_y1 : refl_trans_clos R x y1
red_y1_y : refl_trans_clos S y1 y
z1 : A
red_x_z1 : refl_trans_clos R x z1
red_z1_z : refl_trans_clos S z1 z
w : A
h : refl_trans_clos R y1 w ∧ refl_trans_clos R z1 w
w1 : A
h1 : refl_trans_clos S w w1 ∧ refl_trans_clos R y w1
w2 : A
h2 : refl_trans_clos S w w2 ∧ refl_trans_clos R z w2
omega : A
h3 : refl_trans_clos S w1 omega ∧ refl_trans_clos S w2 omega
⊢ ∃ z_1, refl_trans_clos R z z_1 ∧ refl_trans_clos S z_1 omega
Tactic:
. exists w1; aesop
State after:
case a.a.intro.intro.intro.intro.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y z y1 : A
red_x_y1 : refl_trans_clos R x y1
red_y1_y : refl_trans_clos S y1 y
z1 : A
red_x_z1 : refl_trans_clos R x z1
red_z1_z : refl_trans_clos S z1 z
w : A
h : refl_trans_clos R y1 w ∧ refl_trans_clos R z1 w
w1 : A
h1 : refl_trans_clos S w w1 ∧ refl_trans_clos R y w1
w2 : A
h2 : refl_trans_clos S w w2 ∧ refl_trans_clos R z w2
omega : A
h3 : refl_trans_clos S w1 omega ∧ refl_trans_clos S w2 omega
⊢ ∃ z_1, refl_trans_clos R z z_1 ∧ refl_trans_clos S z_1 omega

State before:
case a.a.intro.intro.intro.intro.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y z y1 : A
red_x_y1 : refl_trans_clos R x y1
red_y1_y : refl_trans_clos S y1 y
z1 : A
red_x_z1 : refl_trans_clos R x z1
red_z1_z : refl_trans_clos S z1 z
w : A
h : refl_trans_clos R y1 w ∧ refl_trans_clos R z1 w
w1 : A
h1 : refl_trans_clos S w w1 ∧ refl_trans_clos R y w1
w2 : A
h2 : refl_trans_clos S w w2 ∧ refl_trans_clos R z w2
omega : A
h3 : refl_trans_clos S w1 omega ∧ refl_trans_clos S w2 omega
⊢ ∃ z_1, refl_trans_clos R z z_1 ∧ refl_trans_clos S z_1 omega
Tactic:
. exists w2; aesop
State after:
no goals

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y z y1 : A
red_x_y1 : refl_trans_clos R x y1
red_y1_y : refl_trans_clos S y1 y
z1 : A
red_x_z1 : refl_trans_clos R x z1
red_z1_z : refl_trans_clos S z1 z
⊢ wedge R y1 z1
Tactic:
exists x
State after:
no goals

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y z y1 : A
red_x_y1 : refl_trans_clos R x y1
red_y1_y : refl_trans_clos S y1 y
z1 : A
red_x_z1 : refl_trans_clos R x z1
red_z1_z : refl_trans_clos S z1 z
w : A
h : refl_trans_clos R y1 w ∧ refl_trans_clos R z1 w
w1 : A
h1 : refl_trans_clos S w w1 ∧ refl_trans_clos R y w1
w2 : A
h2 : refl_trans_clos S w w2 ∧ refl_trans_clos R z w2
⊢ wedge S w1 w2
Tactic:
exists w
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y z y1 : A
red_x_y1 : refl_trans_clos R x y1
red_y1_y : refl_trans_clos S y1 y
z1 : A
red_x_z1 : refl_trans_clos R x z1
red_z1_z : refl_trans_clos S z1 z
w : A
h : refl_trans_clos R y1 w ∧ refl_trans_clos R z1 w
w1 : A
h1 : refl_trans_clos S w w1 ∧ refl_trans_clos R y w1
w2 : A
h2 : refl_trans_clos S w w2 ∧ refl_trans_clos R z w2
⊢ refl_trans_clos S w w1 ∧ refl_trans_clos S w w2

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y z y1 : A
red_x_y1 : refl_trans_clos R x y1
red_y1_y : refl_trans_clos S y1 y
z1 : A
red_x_z1 : refl_trans_clos R x z1
red_z1_z : refl_trans_clos S z1 z
w : A
h : refl_trans_clos R y1 w ∧ refl_trans_clos R z1 w
w1 : A
h1 : refl_trans_clos S w w1 ∧ refl_trans_clos R y w1
w2 : A
h2 : refl_trans_clos S w w2 ∧ refl_trans_clos R z w2
⊢ refl_trans_clos S w w1 ∧ refl_trans_clos S w w2
Tactic:
aesop
State after:
no goals

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y z y1 : A
red_x_y1 : refl_trans_clos R x y1
red_y1_y : refl_trans_clos S y1 y
z1 : A
red_x_z1 : refl_trans_clos R x z1
red_z1_z : refl_trans_clos S z1 z
w : A
h : refl_trans_clos R y1 w ∧ refl_trans_clos R z1 w
w1 : A
h1 : refl_trans_clos S w w1 ∧ refl_trans_clos R y w1
w2 : A
h2 : refl_trans_clos S w w2 ∧ refl_trans_clos R z w2
wedge_w1_w2 : wedge S w1 w2
⊢ joins S w1 w2
Tactic:
apply conf_s
State after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y z y1 : A
red_x_y1 : refl_trans_clos R x y1
red_y1_y : refl_trans_clos S y1 y
z1 : A
red_x_z1 : refl_trans_clos R x z1
red_z1_z : refl_trans_clos S z1 z
w : A
h : refl_trans_clos R y1 w ∧ refl_trans_clos R z1 w
w1 : A
h1 : refl_trans_clos S w w1 ∧ refl_trans_clos R y w1
w2 : A
h2 : refl_trans_clos S w w2 ∧ refl_trans_clos R z w2
wedge_w1_w2 : wedge S w1 w2
⊢ wedge S w1 w2

State before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y z y1 : A
red_x_y1 : refl_trans_clos R x y1
red_y1_y : refl_trans_clos S y1 y
z1 : A
red_x_z1 : refl_trans_clos R x z1
red_z1_z : refl_trans_clos S z1 z
w : A
h : refl_trans_clos R y1 w ∧ refl_trans_clos R z1 w
w1 : A
h1 : refl_trans_clos S w w1 ∧ refl_trans_clos R y w1
w2 : A
h2 : refl_trans_clos S w w2 ∧ refl_trans_clos R z w2
wedge_w1_w2 : wedge S w1 w2
⊢ wedge S w1 w2
Tactic:
trivial
State after:
no goals

State before:
case a.a.intro.intro.intro.intro.left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y z y1 : A
red_x_y1 : refl_trans_clos R x y1
red_y1_y : refl_trans_clos S y1 y
z1 : A
red_x_z1 : refl_trans_clos R x z1
red_z1_z : refl_trans_clos S z1 z
w : A
h : refl_trans_clos R y1 w ∧ refl_trans_clos R z1 w
w1 : A
h1 : refl_trans_clos S w w1 ∧ refl_trans_clos R y w1
w2 : A
h2 : refl_trans_clos S w w2 ∧ refl_trans_clos R z w2
omega : A
h3 : refl_trans_clos S w1 omega ∧ refl_trans_clos S w2 omega
⊢ ∃ z, refl_trans_clos R y z ∧ refl_trans_clos S z omega
Tactic:
exists w1
State after:
case a.a.intro.intro.intro.intro.left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y z y1 : A
red_x_y1 : refl_trans_clos R x y1
red_y1_y : refl_trans_clos S y1 y
z1 : A
red_x_z1 : refl_trans_clos R x z1
red_z1_z : refl_trans_clos S z1 z
w : A
h : refl_trans_clos R y1 w ∧ refl_trans_clos R z1 w
w1 : A
h1 : refl_trans_clos S w w1 ∧ refl_trans_clos R y w1
w2 : A
h2 : refl_trans_clos S w w2 ∧ refl_trans_clos R z w2
omega : A
h3 : refl_trans_clos S w1 omega ∧ refl_trans_clos S w2 omega
⊢ refl_trans_clos R y w1 ∧ refl_trans_clos S w1 omega

State before:
case a.a.intro.intro.intro.intro.left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y z y1 : A
red_x_y1 : refl_trans_clos R x y1
red_y1_y : refl_trans_clos S y1 y
z1 : A
red_x_z1 : refl_trans_clos R x z1
red_z1_z : refl_trans_clos S z1 z
w : A
h : refl_trans_clos R y1 w ∧ refl_trans_clos R z1 w
w1 : A
h1 : refl_trans_clos S w w1 ∧ refl_trans_clos R y w1
w2 : A
h2 : refl_trans_clos S w w2 ∧ refl_trans_clos R z w2
omega : A
h3 : refl_trans_clos S w1 omega ∧ refl_trans_clos S w2 omega
⊢ refl_trans_clos R y w1 ∧ refl_trans_clos S w1 omega
Tactic:
aesop
State after:
no goals

State before:
case a.a.intro.intro.intro.intro.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y z y1 : A
red_x_y1 : refl_trans_clos R x y1
red_y1_y : refl_trans_clos S y1 y
z1 : A
red_x_z1 : refl_trans_clos R x z1
red_z1_z : refl_trans_clos S z1 z
w : A
h : refl_trans_clos R y1 w ∧ refl_trans_clos R z1 w
w1 : A
h1 : refl_trans_clos S w w1 ∧ refl_trans_clos R y w1
w2 : A
h2 : refl_trans_clos S w w2 ∧ refl_trans_clos R z w2
omega : A
h3 : refl_trans_clos S w1 omega ∧ refl_trans_clos S w2 omega
⊢ ∃ z_1, refl_trans_clos R z z_1 ∧ refl_trans_clos S z_1 omega
Tactic:
exists w2
State after:
case a.a.intro.intro.intro.intro.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y z y1 : A
red_x_y1 : refl_trans_clos R x y1
red_y1_y : refl_trans_clos S y1 y
z1 : A
red_x_z1 : refl_trans_clos R x z1
red_z1_z : refl_trans_clos S z1 z
w : A
h : refl_trans_clos R y1 w ∧ refl_trans_clos R z1 w
w1 : A
h1 : refl_trans_clos S w w1 ∧ refl_trans_clos R y w1
w2 : A
h2 : refl_trans_clos S w w2 ∧ refl_trans_clos R z w2
omega : A
h3 : refl_trans_clos S w1 omega ∧ refl_trans_clos S w2 omega
⊢ refl_trans_clos R z w2 ∧ refl_trans_clos S w2 omega

State before:
case a.a.intro.intro.intro.intro.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y z y1 : A
red_x_y1 : refl_trans_clos R x y1
red_y1_y : refl_trans_clos S y1 y
z1 : A
red_x_z1 : refl_trans_clos R x z1
red_z1_z : refl_trans_clos S z1 z
w : A
h : refl_trans_clos R y1 w ∧ refl_trans_clos R z1 w
w1 : A
h1 : refl_trans_clos S w w1 ∧ refl_trans_clos R y w1
w2 : A
h2 : refl_trans_clos S w w2 ∧ refl_trans_clos R z w2
omega : A
h3 : refl_trans_clos S w1 omega ∧ refl_trans_clos S w2 omega
⊢ refl_trans_clos R z w2 ∧ refl_trans_clos S w2 omega
Tactic:
aesop
State after:
no goals