internlm/Lean-Github huggingface dataset:
Theorem: normalizes_trans
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x : A
⊢ Q x
Tactic:
apply normalizing_ind R
Proof state after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x : A
⊢ ∀ (x : A), (∀ (y : A), R x y → Q y) → Q x

case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x : A
⊢ normalizing R
Theorem: normalizes_trans
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x : A
⊢ ∀ (x : A), (∀ (y : A), R x y → Q y) → Q x

case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x : A
⊢ normalizing R
Tactic:
. intros x ih'
  constructor
  . apply ih
    intros y red_x_y
    cases red_x_y
    . apply (ih' _ _).1; trivial
    . apply (ih' _ _).2 <;> trivial
  . intros y red_x_y
    cases red_x_y
    . apply (ih' _ _).1; trivial
    . apply (ih' _ _).2 <;> trivial
Proof state after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x : A
⊢ normalizing R
Theorem: normalizes_trans
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x : A
⊢ normalizing R
Tactic:
. trivial
Proof state after:
no goals
Theorem: normalizes_trans
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x : A
⊢ ∀ (x : A), (∀ (y : A), R x y → Q y) → Q x
Tactic:
intros x ih'
Proof state after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
⊢ Q x
Theorem: normalizes_trans
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
⊢ Q x
Tactic:
constructor
Proof state after:
case a.left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
⊢ P x

case a.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
⊢ ∀ (y : A), trans_clos R x y → P y
Theorem: normalizes_trans
Proof state before:
case a.left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
⊢ P x

case a.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
⊢ ∀ (y : A), trans_clos R x y → P y
Tactic:
. apply ih
  intros y red_x_y
  cases red_x_y
  . apply (ih' _ _).1; trivial
  . apply (ih' _ _).2 <;> trivial
Proof state after:
case a.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
⊢ ∀ (y : A), trans_clos R x y → P y
Theorem: normalizes_trans
Proof state before:
case a.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
⊢ ∀ (y : A), trans_clos R x y → P y
Tactic:
. intros y red_x_y
  cases red_x_y
  . apply (ih' _ _).1; trivial
  . apply (ih' _ _).2 <;> trivial
Proof state after:
no goals
Theorem: normalizes_trans
Proof state before:
case a.left
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
⊢ P x
Tactic:
apply ih
Proof state after:
case a.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
⊢ ∀ (y : A), trans_clos R x y → P y
Theorem: normalizes_trans
Proof state before:
case a.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
⊢ ∀ (y : A), trans_clos R x y → P y
Tactic:
intros y red_x_y
Proof state after:
case a.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
y : A
red_x_y : trans_clos R x y
⊢ P y
Theorem: normalizes_trans
Proof state before:
case a.left.a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
y : A
red_x_y : trans_clos R x y
⊢ P y
Tactic:
cases red_x_y
Proof state after:
case a.left.a.base
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
y : A
a✝ : R x y
⊢ P y

case a.left.a.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
y b✝ : A
a✝¹ : R x b✝
a✝ : trans_clos R b✝ y
⊢ P y
Theorem: normalizes_trans
Proof state before:
case a.left.a.base
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
y : A
a✝ : R x y
⊢ P y

case a.left.a.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
y b✝ : A
a✝¹ : R x b✝
a✝ : trans_clos R b✝ y
⊢ P y
Tactic:
. apply (ih' _ _).1; trivial
Proof state after:
case a.left.a.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
y b✝ : A
a✝¹ : R x b✝
a✝ : trans_clos R b✝ y
⊢ P y
Theorem: normalizes_trans
Proof state before:
case a.left.a.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
y b✝ : A
a✝¹ : R x b✝
a✝ : trans_clos R b✝ y
⊢ P y
Tactic:
. apply (ih' _ _).2 <;> trivial
Proof state after:
no goals
Theorem: normalizes_trans
Proof state before:
case a.left.a.base
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
y : A
a✝ : R x y
⊢ P y
Tactic:
apply (ih' _ _).1
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
y : A
a✝ : R x y
⊢ R x y
Theorem: normalizes_trans
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
y : A
a✝ : R x y
⊢ R x y
Tactic:
trivial
Proof state after:
no goals
Theorem: normalizes_trans
Proof state before:
case a.left.a.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
y b✝ : A
a✝¹ : R x b✝
a✝ : trans_clos R b✝ y
⊢ P y
Tactic:
apply (ih' _ _).2 <;> trivial
Proof state after:
no goals
Theorem: normalizes_trans
Proof state before:
case a.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
⊢ ∀ (y : A), trans_clos R x y → P y
Tactic:
intros y red_x_y
Proof state after:
case a.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
y : A
red_x_y : trans_clos R x y
⊢ P y
Theorem: normalizes_trans
Proof state before:
case a.right
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
y : A
red_x_y : trans_clos R x y
⊢ P y
Tactic:
cases red_x_y
Proof state after:
case a.right.base
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
y : A
a✝ : R x y
⊢ P y

case a.right.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
y b✝ : A
a✝¹ : R x b✝
a✝ : trans_clos R b✝ y
⊢ P y
Theorem: normalizes_trans
Proof state before:
case a.right.base
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
y : A
a✝ : R x y
⊢ P y

case a.right.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
y b✝ : A
a✝¹ : R x b✝
a✝ : trans_clos R b✝ y
⊢ P y
Tactic:
. apply (ih' _ _).1; trivial
Proof state after:
case a.right.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
y b✝ : A
a✝¹ : R x b✝
a✝ : trans_clos R b✝ y
⊢ P y
Theorem: normalizes_trans
Proof state before:
case a.right.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
y b✝ : A
a✝¹ : R x b✝
a✝ : trans_clos R b✝ y
⊢ P y
Tactic:
. apply (ih' _ _).2 <;> trivial
Proof state after:
no goals
Theorem: normalizes_trans
Proof state before:
case a.right.base
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
y : A
a✝ : R x y
⊢ P y
Tactic:
apply (ih' _ _).1
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
y : A
a✝ : R x y
⊢ R x y
Theorem: normalizes_trans
Proof state before:
case a.right.step
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x✝ x : A
ih' : ∀ (y : A), R x y → Q y
y b✝ : A
a✝¹ : R x b✝
a✝ : trans_clos R b✝ y
⊢ P y
Tactic:
apply (ih' _ _).2 <;> trivial
Proof state after:
no goals
Theorem: normalizes_trans
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
norm : normalizing R
P : A → Prop
ih : ∀ (x : A), (∀ (y : A), trans_clos R x y → P y) → P x
Q : A → Prop := fun x => P x ∧ ∀ (y : A), trans_clos R x y → P y
x : A
⊢ normalizing R
Tactic:
trivial
Proof state after:
no goals
Theorem: confluent'_implies_confluent
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
⊢ confluent' R → confluent R
Tactic:
intros conf'
Proof state after:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
conf' : confluent' R
⊢ confluent R
Theorem: confluent'_implies_confluent
Proof state before:
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
conf' : confluent' R
⊢ confluent R
Tactic:
apply semi_confluent_implies_confluent
Proof state after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
conf' : confluent' R
⊢ semi_confluent R
Theorem: confluent'_implies_confluent
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
conf' : confluent' R
⊢ semi_confluent R
Tactic:
intros x y z red_x_y red_x_z
Proof state after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
conf' : 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
Theorem: confluent'_implies_confluent
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
conf' : 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:
have h := refl_trans_is_trans_or_eq _ red_x_z
Proof state after:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
conf' : confluent' R
x y z : A
red_x_y : R x y
red_x_z : refl_trans_clos R x z
h : x = z ∨ trans_clos R x z
⊢ joins R y z
Theorem: confluent'_implies_confluent
Proof state before:
case a
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
conf' : confluent' R
x y z : A
red_x_y : R x y
red_x_z : refl_trans_clos R x z
h : x = z ∨ trans_clos R x z
⊢ joins R y z
Tactic:
cases h
Proof state after:
case a.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
conf' : confluent' R
x y z : A
red_x_y : R x y
red_x_z : refl_trans_clos R x z
h✝ : x = z
⊢ joins R y z

case a.inr
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
conf' : confluent' R
x y z : A
red_x_y : R x y
red_x_z : refl_trans_clos R x z
h✝ : trans_clos R x z
⊢ joins R y z
Theorem: confluent'_implies_confluent
Proof state before:
case a.inl
A : Type
R : A → A → Prop
inhabited_A : Nonempty A
conf' : confluent' R
x y z : A
red_x_y : R x y
red_x_z : refl_trans_clos R x z
h✝ : x = z
⊢ joins R y z

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