Theorem: strong_confluent_implies_confluent (Traat/chapter1.lean)

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
⊢ strongly_confluent R → confluent R
Tactic:
intros str_conf
State after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
⊢ confluent R

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
⊢ confluent R
Tactic:
apply semi_confluent_implies_confluent
State after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
⊢ semi_confluent R

State before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
⊢ semi_confluent R
Tactic:
unfold semi_confluent
State after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
⊢ ∀ (x y z : A), R x y → refl_trans_clos R x z → joins R y z

State before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
⊢ ∀ (x y z : A), R x y → refl_trans_clos R x z → joins R y z
Tactic:
intros x y z red_x_y red_x_z
State after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x y z : A
red_x_y : R x y
red_x_z : refl_trans_clos R x z
⊢ joins R y z

State before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x y z : A
red_x_y : R x y
red_x_z : refl_trans_clos R x z
⊢ joins R y z
Tactic:
revert red_x_y y
State after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x z : A
red_x_z : refl_trans_clos R x z
⊢ ∀ (y : A), R x y → joins R y z

State before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x z : A
red_x_z : refl_trans_clos R x z
⊢ ∀ (y : A), R x y → joins R y z
Tactic:
induction' red_x_z with a x x₂ xₙ red_x_x2 red_x2_xn ih
State after:
case a.refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x z a : A
⊢ ∀ (y : A), R a y → joins R y a

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

State before:
case a.refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x z a : A
⊢ ∀ (y : A), R a y → joins R y a

case a.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x✝ z x x₂ xₙ : A
red_x_x2 : R x x₂
red_x2_xn : refl_trans_clos R x₂ xₙ
ih : ∀ (y : A), R x₂ y → joins R y xₙ
⊢ ∀ (y : A), R x y → joins R y xₙ
Tactic:
. intros y _; exists y; aesop
State after:
case a.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x✝ z x x₂ xₙ : A
red_x_x2 : R x x₂
red_x2_xn : refl_trans_clos R x₂ xₙ
ih : ∀ (y : A), R x₂ y → joins R y xₙ
⊢ ∀ (y : A), R x y → joins R y xₙ

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

State before:
case a.refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x z a : A
⊢ ∀ (y : A), R a y → joins R y a
Tactic:
intros y _
State after:
case a.refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x z a y : A
red_x_y✝ : R a y
⊢ joins R y a

State before:
case a.refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x z a y : A
red_x_y✝ : R a y
⊢ joins R y a
Tactic:
exists y
State after:
case a.refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x z a y : A
red_x_y✝ : R a y
⊢ refl_trans_clos R y y ∧ refl_trans_clos R a y

State before:
case a.refl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x z a y : A
red_x_y✝ : R a y
⊢ refl_trans_clos R y y ∧ refl_trans_clos R a y
Tactic:
aesop
State after:
no goals

State before:
case a.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x✝ z x x₂ xₙ : A
red_x_x2 : R x x₂
red_x2_xn : refl_trans_clos R x₂ xₙ
ih : ∀ (y : A), R x₂ y → joins R y xₙ
⊢ ∀ (y : A), R x y → joins R y xₙ
Tactic:
intros y red_x_y
State after:
case a.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x✝ z x x₂ xₙ : A
red_x_x2 : R x x₂
red_x2_xn : refl_trans_clos R x₂ xₙ
ih : ∀ (y : A), R x₂ y → joins R y xₙ
y : A
red_x_y : R x y
⊢ joins R y xₙ

State before:
case a.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x✝ z x x₂ xₙ : A
red_x_x2 : R x x₂
red_x2_xn : refl_trans_clos R x₂ xₙ
ih : ∀ (y : A), R x₂ y → joins R y xₙ
y : A
red_x_y : R x y
⊢ joins R y xₙ
Tactic:
cases' (str_conf _ _ _ red_x_y red_x_x2) with y₂ h
State after:
case a.step.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x✝ z x x₂ xₙ : A
red_x_x2 : R x x₂
red_x2_xn : refl_trans_clos R x₂ xₙ
ih : ∀ (y : A), R x₂ y → joins R y xₙ
y : A
red_x_y : R x y
y₂ : A
h : refl_trans_clos R y y₂ ∧ refl_clos R x₂ y₂
⊢ joins R y xₙ

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

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

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

case a.step.intro.base
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x✝ z x x₂ xₙ : A
red_x_x2 : R x x₂
red_x2_xn : refl_trans_clos R x₂ xₙ
ih : ∀ (y : A), R x₂ y → joins R y xₙ
y : A
red_x_y : R x y
y₂ : A
h : refl_trans_clos R y y₂ ∧ refl_clos R x₂ y₂
a✝ : R x₂ y₂
⊢ joins R y xₙ
Tactic:
. exists xₙ; constructor
  . apply refl_trans_clos_transitive
    . apply h.1
    . trivial
  . constructor
State after:
case a.step.intro.base
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x✝ z x x₂ xₙ : A
red_x_x2 : R x x₂
red_x2_xn : refl_trans_clos R x₂ xₙ
ih : ∀ (y : A), R x₂ y → joins R y xₙ
y : A
red_x_y : R x y
y₂ : A
h : refl_trans_clos R y y₂ ∧ refl_clos R x₂ y₂
a✝ : R x₂ y₂
⊢ joins R y xₙ

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

State before:
case a.step.intro.base
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x✝ z x x₂ xₙ : A
red_x_x2 : R x x₂
red_x2_xn : refl_trans_clos R x₂ xₙ
ih : ∀ (y : A), R x₂ y → joins R y xₙ
y : A
red_x_y : R x y
y₂ : A
h : refl_trans_clos R y y₂ ∧ refl_clos R x₂ y₂
a✝ : R x₂ y₂
⊢ joins R y xₙ
Tactic:
have ih : y₂ ~>*.*<~ xₙ :=
  by apply ih; trivial
State after:
case a.step.intro.base
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x✝ z x x₂ xₙ : A
red_x_x2 : R x x₂
red_x2_xn : refl_trans_clos R x₂ xₙ
ih✝ : ∀ (y : A), R x₂ y → joins R y xₙ
y : A
red_x_y : R x y
y₂ : A
h : refl_trans_clos R y y₂ ∧ refl_clos R x₂ y₂
a✝ : R x₂ y₂
ih : joins R y₂ xₙ
⊢ joins R y xₙ

State before:
case a.step.intro.base
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x✝ z x x₂ xₙ : A
red_x_x2 : R x x₂
red_x2_xn : refl_trans_clos R x₂ xₙ
ih✝ : ∀ (y : A), R x₂ y → joins R y xₙ
y : A
red_x_y : R x y
y₂ : A
h : refl_trans_clos R y y₂ ∧ refl_clos R x₂ y₂
a✝ : R x₂ y₂
ih : joins R y₂ xₙ
⊢ joins R y xₙ
Tactic:
cases' ih with w _
State after:
case a.step.intro.base.intro
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x✝ z x x₂ xₙ : A
red_x_x2 : R x x₂
red_x2_xn : refl_trans_clos R x₂ xₙ
ih : ∀ (y : A), R x₂ y → joins R y xₙ
y : A
red_x_y : R x y
y₂ : A
h : refl_trans_clos R y y₂ ∧ refl_clos R x₂ y₂
a✝ : R x₂ y₂
w : A
h✝ : refl_trans_clos R y₂ w ∧ refl_trans_clos R xₙ w
⊢ joins R y xₙ

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

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

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

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

case a.step.intro.base.intro.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x✝ z x x₂ xₙ : A
red_x_x2 : R x x₂
red_x2_xn : refl_trans_clos R x₂ xₙ
ih : ∀ (y : A), R x₂ y → joins R y xₙ
y : A
red_x_y : R x y
y₂ : A
h : refl_trans_clos R y y₂ ∧ refl_clos R x₂ y₂
a✝ : R x₂ y₂
w : A
h✝ : refl_trans_clos R y₂ w ∧ refl_trans_clos R xₙ w
⊢ refl_trans_clos R xₙ w
Tactic:
. apply refl_trans_clos_transitive
  . apply h.1
  . aesop
State after:
case a.step.intro.base.intro.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x✝ z x x₂ xₙ : A
red_x_x2 : R x x₂
red_x2_xn : refl_trans_clos R x₂ xₙ
ih : ∀ (y : A), R x₂ y → joins R y xₙ
y : A
red_x_y : R x y
y₂ : A
h : refl_trans_clos R y y₂ ∧ refl_clos R x₂ y₂
a✝ : R x₂ y₂
w : A
h✝ : refl_trans_clos R y₂ w ∧ refl_trans_clos R xₙ w
⊢ refl_trans_clos R xₙ w

State before:
case a.step.intro.base.intro.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x✝ z x x₂ xₙ : A
red_x_x2 : R x x₂
red_x2_xn : refl_trans_clos R x₂ xₙ
ih : ∀ (y : A), R x₂ y → joins R y xₙ
y : A
red_x_y : R x y
y₂ : A
h : refl_trans_clos R y y₂ ∧ refl_clos R x₂ y₂
a✝ : R x₂ y₂
w : A
h✝ : refl_trans_clos R y₂ w ∧ refl_trans_clos R xₙ w
⊢ refl_trans_clos R xₙ w
Tactic:
. aesop
State after:
no goals

State before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x✝ z x x₂ xₙ : A
red_x_x2 : R x x₂
red_x2_xn : refl_trans_clos R x₂ xₙ
ih : ∀ (y : A), R x₂ y → joins R y xₙ
y : A
red_x_y : R x y
y₂ : A
h : refl_trans_clos R y y₂ ∧ refl_clos R x₂ y₂
a✝ : R x₂ y₂
⊢ joins R y₂ xₙ
Tactic:
apply ih
State after:
case red_x_y
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x✝ z x x₂ xₙ : A
red_x_x2 : R x x₂
red_x2_xn : refl_trans_clos R x₂ xₙ
ih : ∀ (y : A), R x₂ y → joins R y xₙ
y : A
red_x_y : R x y
y₂ : A
h : refl_trans_clos R y y₂ ∧ refl_clos R x₂ y₂
a✝ : R x₂ y₂
⊢ R x₂ y₂

State before:
case red_x_y
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x✝ z x x₂ xₙ : A
red_x_x2 : R x x₂
red_x2_xn : refl_trans_clos R x₂ xₙ
ih : ∀ (y : A), R x₂ y → joins R y xₙ
y : A
red_x_y : R x y
y₂ : A
h : refl_trans_clos R y y₂ ∧ refl_clos R x₂ y₂
a✝ : R x₂ y₂
⊢ R x₂ y₂
Tactic:
trivial
State after:
no goals

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

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

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

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

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

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

State before:
case a.step.intro.base.intro.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x✝ z x x₂ xₙ : A
red_x_x2 : R x x₂
red_x2_xn : refl_trans_clos R x₂ xₙ
ih : ∀ (y : A), R x₂ y → joins R y xₙ
y : A
red_x_y : R x y
y₂ : A
h : refl_trans_clos R y y₂ ∧ refl_clos R x₂ y₂
a✝ : R x₂ y₂
w : A
h✝ : refl_trans_clos R y₂ w ∧ refl_trans_clos R xₙ w
⊢ refl_trans_clos R y₂ w
Tactic:
. aesop
State after:
no goals

State before:
case a.step.intro.base.intro.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x✝ z x x₂ xₙ : A
red_x_x2 : R x x₂
red_x2_xn : refl_trans_clos R x₂ xₙ
ih : ∀ (y : A), R x₂ y → joins R y xₙ
y : A
red_x_y : R x y
y₂ : A
h : refl_trans_clos R y y₂ ∧ refl_clos R x₂ y₂
a✝ : R x₂ y₂
w : A
h✝ : refl_trans_clos R y₂ w ∧ refl_trans_clos R xₙ w
⊢ refl_trans_clos R y ?a.step.intro.base.intro.left.y✝
Tactic:
apply h.1
State after:
no goals

State before:
case a.step.intro.base.intro.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x✝ z x x₂ xₙ : A
red_x_x2 : R x x₂
red_x2_xn : refl_trans_clos R x₂ xₙ
ih : ∀ (y : A), R x₂ y → joins R y xₙ
y : A
red_x_y : R x y
y₂ : A
h : refl_trans_clos R y y₂ ∧ refl_clos R x₂ y₂
a✝ : R x₂ y₂
w : A
h✝ : refl_trans_clos R y₂ w ∧ refl_trans_clos R xₙ w
⊢ refl_trans_clos R y₂ w
Tactic:
aesop
State after:
no goals

State before:
case a.step.intro.base.intro.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
str_conf : strongly_confluent R
x✝ z x x₂ xₙ : A
red_x_x2 : R x x₂
red_x2_xn : refl_trans_clos R x₂ xₙ
ih : ∀ (y : A), R x₂ y → joins R y xₙ
y : A
red_x_y : R x y
y₂ : A
h : refl_trans_clos R y y₂ ∧ refl_clos R x₂ y₂
a✝ : R x₂ y₂
w : A
h✝ : refl_trans_clos R y₂ w ∧ refl_trans_clos R xₙ w
⊢ refl_trans_clos R xₙ w
Tactic:
aesop
State after:
no goals