internlm/Lean-Github huggingface dataset:
Theorem: commuting_confluence_implies_confluence
Proof 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
Proof 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
Theorem: commuting_confluence_implies_confluence
Proof 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
Proof 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
Theorem: commuting_confluence_implies_confluence
Proof 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
Proof 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
Theorem: commuting_confluence_implies_confluence
Proof 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
Proof 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
Theorem: commuting_confluence_implies_confluence
Proof 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
Proof 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
Theorem: commuting_confluence_implies_confluence
Proof 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
Proof 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
Theorem: commuting_confluence_implies_confluence
Proof 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
Proof 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
Theorem: commuting_confluence_implies_confluence
Proof 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
Proof 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
Theorem: commuting_confluence_implies_confluence
Proof 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
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
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
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
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
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 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
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 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
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
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
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 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
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 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
Proof state after:
no goals
Theorem: commuting_confluence_implies_confluence
Proof 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
Proof 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
Theorem: commuting_confluence_implies_confluence
Proof 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
Proof state after:
no goals
Theorem: commuting_confluence_implies_confluence
Proof 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
Proof 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
Theorem: commuting_confluence_implies_confluence
Proof 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
Proof state after:
no goals
Theorem: SetTheory.left_mem_pair
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ x ∈ pair x y
Tactic:
simp
Proof state after:
no goals
Theorem: SetTheory.right_mem_pair
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ y ∈ pair x y
Tactic:
simp
Proof state after:
no goals
Theorem: SetTheory.mem_sInter_iff
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ y ∈ ⋂ x ↔ NonemptySet x ∧ ∀ (t : V), t ∈ x → y ∈ t
Tactic:
unfold sInter NonemptySet
Proof state after:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ y ∈
      sep
        (BoundedFormula.all
          (BoundedFormula.imp (BoundedFormula.mem (Sum.inr 1) (Sum.inl ()))
            (BoundedFormula.mem (Sum.inr 0) (Sum.inr 1))))
        (fun x_1 => x) (⋃ x) ↔
    (∃ y, y ∈ x) ∧ ∀ (t : V), t ∈ x → y ∈ t
Theorem: SetTheory.mem_sInter_iff
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ y ∈
      sep
        (BoundedFormula.all
          (BoundedFormula.imp (BoundedFormula.mem (Sum.inr 1) (Sum.inl ()))
            (BoundedFormula.mem (Sum.inr 0) (Sum.inr 1))))
        (fun x_1 => x) (⋃ x) ↔
    (∃ y, y ∈ x) ∧ ∀ (t : V), t ∈ x → y ∈ t
Tactic:
aesop
Proof state after:
no goals
Theorem: SetTheory.subset_sInter
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ NonemptySet x → y ∈ x → ⋂ x ⊆ y
Tactic:
intro hx h z hz
Proof state after:
V : Type u_1
inst✝ : Zermelo V
x y z✝ : V
hx : NonemptySet x
h : y ∈ x
z : V
hz : z ∈ ⋂ x
⊢ z ∈ y
Theorem: SetTheory.subset_sInter
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x y z✝ : V
hx : NonemptySet x
h : y ∈ x
z : V
hz : z ∈ ⋂ x
⊢ z ∈ y
Tactic:
aesop
Proof state after:
no goals
Theorem: SetTheory.mem_inter_iff
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ z ∈ x ∩ y ↔ z ∈ x ∧ z ∈ y
Tactic:
show z ∈ ⋂ pair x y ↔ z ∈ x ∧ z ∈ y
Proof state after:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ z ∈ ⋂ pair x y ↔ z ∈ x ∧ z ∈ y
Theorem: SetTheory.mem_inter_iff
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ z ∈ ⋂ pair x y ↔ z ∈ x ∧ z ∈ y
Tactic:
simp
Proof state after:
no goals
Theorem: SetTheory.union_self
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ x ∪ x = x
Tactic:
ext
Proof state after:
case h
V : Type u_1
inst✝ : Zermelo V
x y z z✝ : V
⊢ z✝ ∈ x ∪ x ↔ z✝ ∈ x
Theorem: SetTheory.union_self
Proof state before:
case h
V : Type u_1
inst✝ : Zermelo V
x y z z✝ : V
⊢ z✝ ∈ x ∪ x ↔ z✝ ∈ x
Tactic:
simp
Proof state after:
no goals
Theorem: SetTheory.inter_self
Proof state before:
V : Type u_1
inst✝ : Zermelo V
x y z : V
⊢ x ∩ x = x
Tactic:
ext
Proof state after:
case h
V : Type u_1
inst✝ : Zermelo V
x y z z✝ : V
⊢ z✝ ∈ x ∩ x ↔ z✝ ∈ x