internlm/Lean-Github huggingface dataset:
Theorem: commuting_confluence_implies_confluence
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
⊢ ∀ (x y : A), (fun x x_1 => (fun R S x y => R x y ∨ S x y) R S x x_1) x y → (fun x x_1 => ?S x x_1) x y
Tactic:
have h : R ∪ S ⊆ (. ~>₁* .) ∘ (. ~>₂* .) :=
  by
    simp; intros x y red_or
    cases red_or
    . exists y; aesop
    . exists x; aesop
Proof state after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
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
Theorem: commuting_confluence_implies_confluence
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
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
Proof state after:
no goals
Theorem: commuting_confluence_implies_confluence
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
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
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
⊢ ∀ (x y : A), R x y ∨ S x y → ∃ z, refl_trans_clos R x z ∧ refl_trans_clos S z y
Theorem: commuting_confluence_implies_confluence
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
⊢ ∀ (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
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y : A
red_or : R x y ∨ S x y
⊢ ∃ z, refl_trans_clos R x z ∧ refl_trans_clos S z y
Theorem: commuting_confluence_implies_confluence
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
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
Proof 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
Theorem: commuting_confluence_implies_confluence
Proof 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
Proof 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
Theorem: commuting_confluence_implies_confluence
Proof 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
Proof state after:
no goals
Theorem: commuting_confluence_implies_confluence
Proof 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
Proof 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
Theorem: commuting_confluence_implies_confluence
Proof 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
Proof state after:
no goals
Theorem: commuting_confluence_implies_confluence
Proof 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
Proof 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
Theorem: commuting_confluence_implies_confluence
Proof 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
Proof state after:
no goals
Theorem: commuting_confluence_implies_confluence
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
⊢ ∀ (x y : A),
    (fun x x_1 => ∃ z, (fun x x_2 => refl_trans_clos R x x_2) x z ∧ (fun x x_2 => refl_trans_clos S x x_2) z x_1) x y →
      (fun x x_1 => refl_trans_clos ((fun R S x y => R x y ∨ S x y) R S) x x_1) x y
Tactic:
simp
Proof state after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
⊢ ∀ (x y 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
Theorem: commuting_confluence_implies_confluence
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
⊢ ∀ (x y 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
Proof state after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y 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
Theorem: commuting_confluence_implies_confluence
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
x y 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
Proof 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
Theorem: commuting_confluence_implies_confluence
Proof 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
Proof 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
Theorem: commuting_confluence_implies_confluence
Proof 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
Proof state after:
no goals
Theorem: commuting_confluence_implies_confluence
Proof 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
Proof 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✝
Theorem: commuting_confluence_implies_confluence
Proof 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
Proof state after:
no goals
Theorem: commuting_confluence_implies_confluence
Proof 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
Proof 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
Theorem: commuting_confluence_implies_confluence
Proof 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
Proof state after:
no goals
Theorem: commuting_confluence_implies_confluence
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
S : A → A → Prop
commut_r_s : commute R S
conf_r : confluent R
conf_s : confluent S
⊢ confluent fun x y => ∃ z, (fun x x_1 => refl_trans_clos R x x_1) x z ∧ (fun x x_1 => refl_trans_clos S x x_1) z y
Tactic:
apply diamond_implies_confluent
Proof 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
Theorem: commuting_confluence_implies_confluence
Proof 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]
Proof 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
Theorem: commuting_confluence_implies_confluence
Proof 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
Proof 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
Theorem: commuting_confluence_implies_confluence
Proof 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
Proof 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
Theorem: commuting_confluence_implies_confluence
Proof 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
Proof 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
Theorem: commuting_confluence_implies_confluence
Proof 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
Proof 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
Theorem: commuting_confluence_implies_confluence
Proof 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
Proof 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
Theorem: commuting_confluence_implies_confluence
Proof 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
Proof 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
Theorem: commuting_confluence_implies_confluence
Proof 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
Proof 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
Theorem: commuting_confluence_implies_confluence
Proof 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
Proof 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
Theorem: commuting_confluence_implies_confluence
Proof 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
Proof 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