Relations_3_facts.v

Built with Alectryon, running Coq+SerAPI v8.10.0+0.7.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.
(************************************************************************)
(*         *   The Coq Proof Assistant / The Coq Development Team       *)
(*  v      *   INRIA, CNRS and contributors - Copyright 1999-2018       *)
(* <O___,, *       (see CREDITS file for the list of authors)           *)
(*   \VV/  **************************************************************)
(*    //   *    This file is distributed under the terms of the         *)
(*         *     GNU Lesser General Public License Version 2.1          *)
(*         *     (see LICENSE file for the text of the license)         *)
(************************************************************************)
(****************************************************************************)
(*                                                                          *)
(*                         Naive Set Theory in Coq                          *)
(*                                                                          *)
(*                     INRIA                        INRIA                   *)
(*              Rocquencourt                        Sophia-Antipolis        *)
(*                                                                          *)
(*                                 Coq V6.1                                 *)
(*									    *)
(*			         Gilles Kahn 				    *)
(*				 Gerard Huet				    *)
(*									    *)
(*									    *)
(*                                                                          *)
(* Acknowledgments: This work was started in July 1993 by F. Prost. Thanks  *)
(* to the Newton Institute for providing an exceptional work environment    *)
(* in Summer 1995. Several developments by E. Ledinot were an inspiration.  *)
(****************************************************************************)

Require Export Relations_1.
Require Export Relations_1_facts.
Require Export Relations_2.
Require Export Relations_2_facts.
Require Export Relations_3.

Theorem Rstar_imp_coherent :
 forall (U:Type) (R:Relation U) (x y:U), Rstar U R x y -> coherent U R x y.forall (U : Type) (R : Relation U) (x y : U),
Rstar U R x y -> coherent U R x y
Proof.forall (U : Type) (R : Relation U) (x y : U),
Rstar U R x y -> coherent U R x y
intros U R x y H'; red.U:Type
R:Relation U
x, y:U
H':Rstar U R x y
exists z : U, Rstar U R x z /\ Rstar U R y z
exists y; auto with sets.
Qed.
Hint Resolve Rstar_imp_coherent : core.

Theorem coherent_symmetric :
 forall (U:Type) (R:Relation U), Symmetric U (coherent U R).forall (U : Type) (R : Relation U),
Symmetric U (coherent U R)
Proof.forall (U : Type) (R : Relation U),
Symmetric U (coherent U R)
unfold coherent at 1.forall (U : Type) (R : Relation U),
Symmetric U
  (fun x y : U =>
   exists z : U, Rstar U R x z /\ Rstar U R y z)
intros U R; red.U:Type
R:Relation U
forall x y : U,
(exists z : U, Rstar U R x z /\ Rstar U R y z) ->
exists z : U, Rstar U R y z /\ Rstar U R x z
intros x y H'; elim H'.U:Type
R:Relation U
x, y:U
H':exists z : U, Rstar U R x z /\ Rstar U R y z
forall x0 : U,
Rstar U R x x0 /\ Rstar U R y x0 ->
exists z : U, Rstar U R y z /\ Rstar U R x z
intros z H'0; exists z; tauto.
Qed.

Theorem Strong_confluence :
 forall (U:Type) (R:Relation U), Strongly_confluent U R -> Confluent U R.forall (U : Type) (R : Relation U),
Strongly_confluent U R -> Confluent U R
Proof.forall (U : Type) (R : Relation U),
Strongly_confluent U R -> Confluent U R
intros U R H'; red.U:Type
R:Relation U
H':Strongly_confluent U R
forall x : U, confluent U R x
intro x; red; intros a b H'0.U:Type
R:Relation U
H':Strongly_confluent U R
x, a, b:U
H'0:Rstar U R x a
Rstar U R x b -> coherent U R a b
unfold coherent at 1.U:Type
R:Relation U
H':Strongly_confluent U R
x, a, b:U
H'0:Rstar U R x a
Rstar U R x b ->
exists z : U, Rstar U R a z /\ Rstar U R b z
generalize b; clear b.U:Type
R:Relation U
H':Strongly_confluent U R
x, a:U
H'0:Rstar U R x a
forall b : U,
Rstar U R x b ->
exists z : U, Rstar U R a z /\ Rstar U R b z
elim H'0; clear H'0.U:Type
R:Relation U
H':Strongly_confluent U R
x, a:U
forall x0 b : U,
Rstar U R x0 b ->
exists z : U, Rstar U R x0 z /\ Rstar U R b z
U:Type
R:Relation U
H':Strongly_confluent U R
x, a:U
forall x0 y z : U,
R x0 y ->
Rstar U R y z ->
(forall b : U,
 Rstar U R y b ->
 exists z0 : U, Rstar U R z z0 /\ Rstar U R b z0) ->
forall b : U,
Rstar U R x0 b ->
exists z0 : U, Rstar U R z z0 /\ Rstar U R b z0
-U:Type
R:Relation U
H':Strongly_confluent U R
x, a:U
forall x0 b : U,
Rstar U R x0 b ->
exists z : U, Rstar U R x0 z /\ Rstar U R b z intros x0 b H'1; exists b; auto with sets.
-U:Type
R:Relation U
H':Strongly_confluent U R
x, a:U
forall x0 y z : U,
R x0 y ->
Rstar U R y z ->
(forall b : U,
 Rstar U R y b ->
 exists z0 : U, Rstar U R z z0 /\ Rstar U R b z0) ->
forall b : U,
Rstar U R x0 b ->
exists z0 : U, Rstar U R z z0 /\ Rstar U R b z0 intros x0 y z H'1 H'2 H'3 b H'4.U:Type
R:Relation U
H':Strongly_confluent U R
x, a, x0, y, z:U
H'1:R x0 y
H'2:Rstar U R y z
H'3:forall b0 : U,
Rstar U R y b0 -> exists z0 : U, Rstar U R z z0 /\ Rstar U R b0 z0
b:U
H'4:Rstar U R x0 b
exists z0 : U, Rstar U R z z0 /\ Rstar U R b z0
  generalize (Lemma1 U R); intro h; lapply h;
    [ intro H'0; generalize (H'0 x0 b); intro h0; lapply h0;
      [ intro H'5; generalize (H'5 y); intro h1; lapply h1;
        [ intro h2; elim h2; intros z0 h3; elim h3; intros H'6 H'7;
          clear h h0 h1 h2 h3
        | clear h h0 h1 ]
      | clear h h0 ]
    | clear h ]; auto with sets.U:Type
R:Relation U
H':Strongly_confluent U R
x, a, x0, y, z:U
H'1:R x0 y
H'2:Rstar U R y z
H'3:forall b0 : U,
Rstar U R y b0 -> exists z1 : U, Rstar U R z z1 /\ Rstar U R b0 z1
b:U
H'4:Rstar U R x0 b
H'0:forall x1 b0 : U,
Rstar U R x1 b0 ->
forall a0 : U, R x1 a0 -> exists z1 : U, Rstar U R a0 z1 /\ R b0 z1
H'5:forall a0 : U, R x0 a0 -> exists z1 : U, Rstar U R a0 z1 /\ R b z1
z0:U
H'6:Rstar U R y z0
H'7:R b z0
exists z1 : U, Rstar U R z z1 /\ Rstar U R b z1
  generalize (H'3 z0); intro h; lapply h;
    [ intro h0; elim h0; intros z1 h1; elim h1; intros H'8 H'9; clear h h0 h1
    | clear h ]; auto with sets.U:Type
R:Relation U
H':Strongly_confluent U R
x, a, x0, y, z:U
H'1:R x0 y
H'2:Rstar U R y z
H'3:forall b0 : U,
Rstar U R y b0 -> exists z2 : U, Rstar U R z z2 /\ Rstar U R b0 z2
b:U
H'4:Rstar U R x0 b
H'0:forall x1 b0 : U,
Rstar U R x1 b0 ->
forall a0 : U, R x1 a0 -> exists z2 : U, Rstar U R a0 z2 /\ R b0 z2
H'5:forall a0 : U, R x0 a0 -> exists z2 : U, Rstar U R a0 z2 /\ R b z2
z0:U
H'6:Rstar U R y z0
H'7:R b z0
z1:U
H'8:Rstar U R z z1
H'9:Rstar U R z0 z1
exists z2 : U, Rstar U R z z2 /\ Rstar U R b z2
  exists z1; split; auto with sets.U:Type
R:Relation U
H':Strongly_confluent U R
x, a, x0, y, z:U
H'1:R x0 y
H'2:Rstar U R y z
H'3:forall b0 : U,
Rstar U R y b0 -> exists z2 : U, Rstar U R z z2 /\ Rstar U R b0 z2
b:U
H'4:Rstar U R x0 b
H'0:forall x1 b0 : U,
Rstar U R x1 b0 ->
forall a0 : U, R x1 a0 -> exists z2 : U, Rstar U R a0 z2 /\ R b0 z2
H'5:forall a0 : U, R x0 a0 -> exists z2 : U, Rstar U R a0 z2 /\ R b z2
z0:U
H'6:Rstar U R y z0
H'7:R b z0
z1:U
H'8:Rstar U R z z1
H'9:Rstar U R z0 z1
Rstar U R b z1
  apply Rstar_n with z0; auto with sets.
Qed.

Theorem Strong_confluence_direct :
 forall (U:Type) (R:Relation U), Strongly_confluent U R -> Confluent U R.forall (U : Type) (R : Relation U),
Strongly_confluent U R -> Confluent U R
Proof.forall (U : Type) (R : Relation U),
Strongly_confluent U R -> Confluent U R
intros U R H'; red.U:Type
R:Relation U
H':Strongly_confluent U R
forall x : U, confluent U R x
intro x; red; intros a b H'0.U:Type
R:Relation U
H':Strongly_confluent U R
x, a, b:U
H'0:Rstar U R x a
Rstar U R x b -> coherent U R a b
unfold coherent at 1.U:Type
R:Relation U
H':Strongly_confluent U R
x, a, b:U
H'0:Rstar U R x a
Rstar U R x b ->
exists z : U, Rstar U R a z /\ Rstar U R b z
generalize b; clear b.U:Type
R:Relation U
H':Strongly_confluent U R
x, a:U
H'0:Rstar U R x a
forall b : U,
Rstar U R x b ->
exists z : U, Rstar U R a z /\ Rstar U R b z
elim H'0; clear H'0.U:Type
R:Relation U
H':Strongly_confluent U R
x, a:U
forall x0 b : U,
Rstar U R x0 b ->
exists z : U, Rstar U R x0 z /\ Rstar U R b z
U:Type
R:Relation U
H':Strongly_confluent U R
x, a:U
forall x0 y z : U,
R x0 y ->
Rstar U R y z ->
(forall b : U,
 Rstar U R y b ->
 exists z0 : U, Rstar U R z z0 /\ Rstar U R b z0) ->
forall b : U,
Rstar U R x0 b ->
exists z0 : U, Rstar U R z z0 /\ Rstar U R b z0
-U:Type
R:Relation U
H':Strongly_confluent U R
x, a:U
forall x0 b : U,
Rstar U R x0 b ->
exists z : U, Rstar U R x0 z /\ Rstar U R b z intros x0 b H'1; exists b; auto with sets.
-U:Type
R:Relation U
H':Strongly_confluent U R
x, a:U
forall x0 y z : U,
R x0 y ->
Rstar U R y z ->
(forall b : U,
 Rstar U R y b ->
 exists z0 : U, Rstar U R z z0 /\ Rstar U R b z0) ->
forall b : U,
Rstar U R x0 b ->
exists z0 : U, Rstar U R z z0 /\ Rstar U R b z0 intros x0 y z H'1 H'2 H'3 b H'4.U:Type
R:Relation U
H':Strongly_confluent U R
x, a, x0, y, z:U
H'1:R x0 y
H'2:Rstar U R y z
H'3:forall b0 : U,
Rstar U R y b0 -> exists z0 : U, Rstar U R z z0 /\ Rstar U R b0 z0
b:U
H'4:Rstar U R x0 b
exists z0 : U, Rstar U R z z0 /\ Rstar U R b z0
  cut (ex (fun t:U => Rstar U R y t /\ R b t)).U:Type
R:Relation U
H':Strongly_confluent U R
x, a, x0, y, z:U
H'1:R x0 y
H'2:Rstar U R y z
H'3:forall b0 : U,
Rstar U R y b0 -> exists z0 : U, Rstar U R z z0 /\ Rstar U R b0 z0
b:U
H'4:Rstar U R x0 b
(exists t : U, Rstar U R y t /\ R b t) ->
exists z0 : U, Rstar U R z z0 /\ Rstar U R b z0
U:Type
R:Relation U
H':Strongly_confluent U R
x, a, x0, y, z:U
H'1:R x0 y
H'2:Rstar U R y z
H'3:forall b0 : U,
Rstar U R y b0 -> exists z0 : U, Rstar U R z z0 /\ Rstar U R b0 z0
b:U
H'4:Rstar U R x0 b
exists t : U, Rstar U R y t /\ R b t
  +U:Type
R:Relation U
H':Strongly_confluent U R
x, a, x0, y, z:U
H'1:R x0 y
H'2:Rstar U R y z
H'3:forall b0 : U,
Rstar U R y b0 -> exists z0 : U, Rstar U R z z0 /\ Rstar U R b0 z0
b:U
H'4:Rstar U R x0 b
(exists t : U, Rstar U R y t /\ R b t) ->
exists z0 : U, Rstar U R z z0 /\ Rstar U R b z0 intro h; elim h; intros t h0; elim h0; intros H'0 H'5; clear h h0.U:Type
R:Relation U
H':Strongly_confluent U R
x, a, x0, y, z:U
H'1:R x0 y
H'2:Rstar U R y z
H'3:forall b0 : U,
Rstar U R y b0 -> exists z0 : U, Rstar U R z z0 /\ Rstar U R b0 z0
b:U
H'4:Rstar U R x0 b
t:U
H'0:Rstar U R y t
H'5:R b t
exists z0 : U, Rstar U R z z0 /\ Rstar U R b z0
    generalize (H'3 t); intro h; lapply h;
      [ intro h0; elim h0; intros z0 h1; elim h1; intros H'6 H'7; clear h h0 h1
      | clear h ]; auto with sets.U:Type
R:Relation U
H':Strongly_confluent U R
x, a, x0, y, z:U
H'1:R x0 y
H'2:Rstar U R y z
H'3:forall b0 : U,
Rstar U R y b0 -> exists z1 : U, Rstar U R z z1 /\ Rstar U R b0 z1
b:U
H'4:Rstar U R x0 b
t:U
H'0:Rstar U R y t
H'5:R b t
z0:U
H'6:Rstar U R z z0
H'7:Rstar U R t z0
exists z1 : U, Rstar U R z z1 /\ Rstar U R b z1
    exists z0; split; [ assumption | idtac ].U:Type
R:Relation U
H':Strongly_confluent U R
x, a, x0, y, z:U
H'1:R x0 y
H'2:Rstar U R y z
H'3:forall b0 : U,
Rstar U R y b0 -> exists z1 : U, Rstar U R z z1 /\ Rstar U R b0 z1
b:U
H'4:Rstar U R x0 b
t:U
H'0:Rstar U R y t
H'5:R b t
z0:U
H'6:Rstar U R z z0
H'7:Rstar U R t z0
Rstar U R b z0
    apply Rstar_n with t; auto with sets.
  +U:Type
R:Relation U
H':Strongly_confluent U R
x, a, x0, y, z:U
H'1:R x0 y
H'2:Rstar U R y z
H'3:forall b0 : U,
Rstar U R y b0 -> exists z0 : U, Rstar U R z z0 /\ Rstar U R b0 z0
b:U
H'4:Rstar U R x0 b
exists t : U, Rstar U R y t /\ R b t generalize H'1; generalize y; clear H'1.U:Type
R:Relation U
H':Strongly_confluent U R
x, a, x0, y, z:U
H'2:Rstar U R y z
H'3:forall b0 : U,
Rstar U R y b0 -> exists z0 : U, Rstar U R z z0 /\ Rstar U R b0 z0
b:U
H'4:Rstar U R x0 b
forall y0 : U,
R x0 y0 -> exists t : U, Rstar U R y0 t /\ R b t
    elim H'4.U:Type
R:Relation U
H':Strongly_confluent U R
x, a, x0, y, z:U
H'2:Rstar U R y z
H'3:forall b0 : U,
Rstar U R y b0 -> exists z0 : U, Rstar U R z z0 /\ Rstar U R b0 z0
b:U
H'4:Rstar U R x0 b
forall x1 y0 : U,
R x1 y0 -> exists t : U, Rstar U R y0 t /\ R x1 t
U:Type
R:Relation U
H':Strongly_confluent U R
x, a, x0, y, z:U
H'2:Rstar U R y z
H'3:forall b0 : U,
Rstar U R y b0 -> exists z0 : U, Rstar U R z z0 /\ Rstar U R b0 z0
b:U
H'4:Rstar U R x0 b
forall x1 y0 z0 : U,
R x1 y0 ->
Rstar U R y0 z0 ->
(forall y1 : U,
 R y0 y1 -> exists t : U, Rstar U R y1 t /\ R z0 t) ->
forall y1 : U,
R x1 y1 -> exists t : U, Rstar U R y1 t /\ R z0 t
    *U:Type
R:Relation U
H':Strongly_confluent U R
x, a, x0, y, z:U
H'2:Rstar U R y z
H'3:forall b0 : U,
Rstar U R y b0 -> exists z0 : U, Rstar U R z z0 /\ Rstar U R b0 z0
b:U
H'4:Rstar U R x0 b
forall x1 y0 : U,
R x1 y0 -> exists t : U, Rstar U R y0 t /\ R x1 t intros x1 y0 H'0; exists y0; auto with sets.
    *U:Type
R:Relation U
H':Strongly_confluent U R
x, a, x0, y, z:U
H'2:Rstar U R y z
H'3:forall b0 : U,
Rstar U R y b0 -> exists z0 : U, Rstar U R z z0 /\ Rstar U R b0 z0
b:U
H'4:Rstar U R x0 b
forall x1 y0 z0 : U,
R x1 y0 ->
Rstar U R y0 z0 ->
(forall y1 : U,
 R y0 y1 -> exists t : U, Rstar U R y1 t /\ R z0 t) ->
forall y1 : U,
R x1 y1 -> exists t : U, Rstar U R y1 t /\ R z0 t intros x1 y0 z0 H'0 H'1 H'5 y1 H'6.U:Type
R:Relation U
H':Strongly_confluent U R
x, a, x0, y, z:U
H'2:Rstar U R y z
H'3:forall b0 : U,
Rstar U R y b0 -> exists z1 : U, Rstar U R z z1 /\ Rstar U R b0 z1
b:U
H'4:Rstar U R x0 b
x1, y0, z0:U
H'0:R x1 y0
H'1:Rstar U R y0 z0
H'5:forall y2 : U, R y0 y2 -> exists t : U, Rstar U R y2 t /\ R z0 t
y1:U
H'6:R x1 y1
exists t : U, Rstar U R y1 t /\ R z0 t
      red in H'.U:Type
R:Relation U
H':forall x2 a0 b0 : U,
R x2 a0 ->
R x2 b0 -> exists z1 : U, R a0 z1 /\ R b0 z1
x, a, x0, y, z:U
H'2:Rstar U R y z
H'3:forall b0 : U,
Rstar U R y b0 -> exists z1 : U, Rstar U R z z1 /\ Rstar U R b0 z1
b:U
H'4:Rstar U R x0 b
x1, y0, z0:U
H'0:R x1 y0
H'1:Rstar U R y0 z0
H'5:forall y2 : U, R y0 y2 -> exists t : U, Rstar U R y2 t /\ R z0 t
y1:U
H'6:R x1 y1
exists t : U, Rstar U R y1 t /\ R z0 t
      generalize (H' x1 y0 y1); intro h; lapply h;
        [ intro H'7; lapply H'7;
          [ intro h0; elim h0; intros z1 h1; elim h1; intros H'8 H'9;
            clear h H'7 h0 h1
          | clear h ]
        | clear h ]; auto with sets.U:Type
R:Relation U
H':forall x2 a0 b0 : U,
R x2 a0 ->
R x2 b0 -> exists z2 : U, R a0 z2 /\ R b0 z2
x, a, x0, y, z:U
H'2:Rstar U R y z
H'3:forall b0 : U,
Rstar U R y b0 -> exists z2 : U, Rstar U R z z2 /\ Rstar U R b0 z2
b:U
H'4:Rstar U R x0 b
x1, y0, z0:U
H'0:R x1 y0
H'1:Rstar U R y0 z0
H'5:forall y2 : U, R y0 y2 -> exists t : U, Rstar U R y2 t /\ R z0 t
y1:U
H'6:R x1 y1
z1:U
H'8:R y0 z1
H'9:R y1 z1
exists t : U, Rstar U R y1 t /\ R z0 t
      generalize (H'5 z1); intro h; lapply h;
        [ intro h0; elim h0; intros t h1; elim h1; intros H'7 H'10; clear h h0 h1
        | clear h ]; auto with sets.U:Type
R:Relation U
H':forall x2 a0 b0 : U,
R x2 a0 ->
R x2 b0 -> exists z2 : U, R a0 z2 /\ R b0 z2
x, a, x0, y, z:U
H'2:Rstar U R y z
H'3:forall b0 : U,
Rstar U R y b0 -> exists z2 : U, Rstar U R z z2 /\ Rstar U R b0 z2
b:U
H'4:Rstar U R x0 b
x1, y0, z0:U
H'0:R x1 y0
H'1:Rstar U R y0 z0
H'5:forall y2 : U, R y0 y2 -> exists t0 : U, Rstar U R y2 t0 /\ R z0 t0
y1:U
H'6:R x1 y1
z1:U
H'8:R y0 z1
H'9:R y1 z1
t:U
H'7:Rstar U R z1 t
H'10:R z0 t
exists t0 : U, Rstar U R y1 t0 /\ R z0 t0
      exists t; split; auto with sets.U:Type
R:Relation U
H':forall x2 a0 b0 : U,
R x2 a0 ->
R x2 b0 -> exists z2 : U, R a0 z2 /\ R b0 z2
x, a, x0, y, z:U
H'2:Rstar U R y z
H'3:forall b0 : U,
Rstar U R y b0 ->
exists z2 : U, Rstar U R z z2 /\ Rstar U R b0 z2
b:U
H'4:Rstar U R x0 b
x1, y0, z0:U
H'0:R x1 y0
H'1:Rstar U R y0 z0
H'5:forall y2 : U,
R y0 y2 ->
exists t0 : U, Rstar U R y2 t0 /\ R z0 t0
y1:U
H'6:R x1 y1
z1:U
H'8:R y0 z1
H'9:R y1 z1
t:U
H'7:Rstar U R z1 t
H'10:R z0 t
Rstar U R y1 t
      apply Rstar_n with z1; auto with sets.
Qed.

Theorem Noetherian_contains_Noetherian :
 forall (U:Type) (R R':Relation U),
   Noetherian U R -> contains U R R' -> Noetherian U R'.forall (U : Type) (R R' : Relation U),
Noetherian U R -> contains U R R' -> Noetherian U R'
Proof.forall (U : Type) (R R' : Relation U),
Noetherian U R -> contains U R R' -> Noetherian U R'
unfold Noetherian at 2.forall (U : Type) (R R' : Relation U),
Noetherian U R ->
contains U R R' -> forall x : U, noetherian U R' x
intros U R R' H' H'0 x.U:Type
R, R':Relation U
H':Noetherian U R
H'0:contains U R R'
x:U
noetherian U R' x
elim (H' x); auto with sets.
Qed.

Theorem Newman :
 forall (U:Type) (R:Relation U),
   Noetherian U R -> Locally_confluent U R -> Confluent U R.forall (U : Type) (R : Relation U),
Noetherian U R ->
Locally_confluent U R -> Confluent U R
Proof.forall (U : Type) (R : Relation U),
Noetherian U R ->
Locally_confluent U R -> Confluent U R
intros U R H' H'0; red; intro x.U:Type
R:Relation U
H':Noetherian U R
H'0:Locally_confluent U R
x:U
confluent U R x
elim (H' x); unfold confluent.U:Type
R:Relation U
H':Noetherian U R
H'0:Locally_confluent U R
x:U
forall x0 : U,
(forall y : U, R x0 y -> noetherian U R y) ->
(forall y : U,
 R x0 y ->
 forall y0 z : U,
 Rstar U R y y0 -> Rstar U R y z -> coherent U R y0 z) ->
forall y z : U,
Rstar U R x0 y -> Rstar U R x0 z -> coherent U R y z
intros x0 H'1 H'2 y z H'3 H'4.U:Type
R:Relation U
H':Noetherian U R
H'0:Locally_confluent U R
x, x0:U
H'1:forall y0 : U, R x0 y0 -> noetherian U R y0
H'2:forall y0 : U,
R x0 y0 ->
forall y1 z0 : U, Rstar U R y0 y1 -> Rstar U R y0 z0 -> coherent U R y1 z0
y, z:U
H'3:Rstar U R x0 y
H'4:Rstar U R x0 z
coherent U R y z
generalize (Rstar_cases U R x0 y); intro h; lapply h;
 [ intro h0; elim h0;
    [ clear h h0; intro h1
    | intro h1; elim h1; intros u h2; elim h2; intros H'5 H'6;
       clear h h0 h1 h2 ]
 | clear h ]; auto with sets.U:Type
R:Relation U
H':Noetherian U R
H'0:Locally_confluent U R
x, x0:U
H'1:forall y0 : U, R x0 y0 -> noetherian U R y0
H'2:forall y0 : U,
R x0 y0 ->
forall y1 z0 : U, Rstar U R y0 y1 -> Rstar U R y0 z0 -> coherent U R y1 z0
y, z:U
H'3:Rstar U R x0 y
H'4:Rstar U R x0 z
h1:x0 = y
coherent U R y z
U:Type
R:Relation U
H':Noetherian U R
H'0:Locally_confluent U R
x, x0:U
H'1:forall y0 : U, R x0 y0 -> noetherian U R y0
H'2:forall y0 : U,
R x0 y0 ->
forall y1 z0 : U, Rstar U R y0 y1 -> Rstar U R y0 z0 -> coherent U R y1 z0
y, z:U
H'3:Rstar U R x0 y
H'4:Rstar U R x0 z
u:U
H'5:R x0 u
H'6:Rstar U R u y
coherent U R y z
-U:Type
R:Relation U
H':Noetherian U R
H'0:Locally_confluent U R
x, x0:U
H'1:forall y0 : U, R x0 y0 -> noetherian U R y0
H'2:forall y0 : U,
R x0 y0 ->
forall y1 z0 : U, Rstar U R y0 y1 -> Rstar U R y0 z0 -> coherent U R y1 z0
y, z:U
H'3:Rstar U R x0 y
H'4:Rstar U R x0 z
h1:x0 = y
coherent U R y z elim h1; auto with sets.
-U:Type
R:Relation U
H':Noetherian U R
H'0:Locally_confluent U R
x, x0:U
H'1:forall y0 : U, R x0 y0 -> noetherian U R y0
H'2:forall y0 : U,
R x0 y0 ->
forall y1 z0 : U, Rstar U R y0 y1 -> Rstar U R y0 z0 -> coherent U R y1 z0
y, z:U
H'3:Rstar U R x0 y
H'4:Rstar U R x0 z
u:U
H'5:R x0 u
H'6:Rstar U R u y
coherent U R y z generalize (Rstar_cases U R x0 z); intro h; lapply h;
    [ intro h0; elim h0;
      [ clear h h0; intro h1
      | intro h1; elim h1; intros v h2; elim h2; intros H'7 H'8;
        clear h h0 h1 h2 ]
    | clear h ]; auto with sets.U:Type
R:Relation U
H':Noetherian U R
H'0:Locally_confluent U R
x, x0:U
H'1:forall y0 : U, R x0 y0 -> noetherian U R y0
H'2:forall y0 : U,
R x0 y0 ->
forall y1 z0 : U, Rstar U R y0 y1 -> Rstar U R y0 z0 -> coherent U R y1 z0
y, z:U
H'3:Rstar U R x0 y
H'4:Rstar U R x0 z
u:U
H'5:R x0 u
H'6:Rstar U R u y
h1:x0 = z
coherent U R y z
U:Type
R:Relation U
H':Noetherian U R
H'0:Locally_confluent U R
x, x0:U
H'1:forall y0 : U, R x0 y0 -> noetherian U R y0
H'2:forall y0 : U,
R x0 y0 ->
forall y1 z0 : U, Rstar U R y0 y1 -> Rstar U R y0 z0 -> coherent U R y1 z0
y, z:U
H'3:Rstar U R x0 y
H'4:Rstar U R x0 z
u:U
H'5:R x0 u
H'6:Rstar U R u y
v:U
H'7:R x0 v
H'8:Rstar U R v z
coherent U R y z
  +U:Type
R:Relation U
H':Noetherian U R
H'0:Locally_confluent U R
x, x0:U
H'1:forall y0 : U, R x0 y0 -> noetherian U R y0
H'2:forall y0 : U,
R x0 y0 ->
forall y1 z0 : U, Rstar U R y0 y1 -> Rstar U R y0 z0 -> coherent U R y1 z0
y, z:U
H'3:Rstar U R x0 y
H'4:Rstar U R x0 z
u:U
H'5:R x0 u
H'6:Rstar U R u y
h1:x0 = z
coherent U R y z elim h1; generalize coherent_symmetric; intro t; red in t; auto with sets.
  +U:Type
R:Relation U
H':Noetherian U R
H'0:Locally_confluent U R
x, x0:U
H'1:forall y0 : U, R x0 y0 -> noetherian U R y0
H'2:forall y0 : U,
R x0 y0 ->
forall y1 z0 : U, Rstar U R y0 y1 -> Rstar U R y0 z0 -> coherent U R y1 z0
y, z:U
H'3:Rstar U R x0 y
H'4:Rstar U R x0 z
u:U
H'5:R x0 u
H'6:Rstar U R u y
v:U
H'7:R x0 v
H'8:Rstar U R v z
coherent U R y z unfold Locally_confluent, locally_confluent, coherent in H'0.U:Type
R:Relation U
H':Noetherian U R
H'0:forall x1 y0 z0 : U,
R x1 y0 -> R x1 z0 -> exists z1 : U, Rstar U R y0 z1 /\ Rstar U R z0 z1
x, x0:U
H'1:forall y0 : U, R x0 y0 -> noetherian U R y0
H'2:forall y0 : U,
R x0 y0 ->
forall y1 z0 : U, Rstar U R y0 y1 -> Rstar U R y0 z0 -> coherent U R y1 z0
y, z:U
H'3:Rstar U R x0 y
H'4:Rstar U R x0 z
u:U
H'5:R x0 u
H'6:Rstar U R u y
v:U
H'7:R x0 v
H'8:Rstar U R v z
coherent U R y z
    generalize (H'0 x0 u v); intro h; lapply h;
      [ intro H'9; lapply H'9;
        [ intro h0; elim h0; intros t h1; elim h1; intros H'10 H'11;
          clear h H'9 h0 h1
        | clear h ]
      | clear h ]; auto with sets.U:Type
R:Relation U
H':Noetherian U R
H'0:forall x1 y0 z0 : U,
R x1 y0 -> R x1 z0 -> exists z1 : U, Rstar U R y0 z1 /\ Rstar U R z0 z1
x, x0:U
H'1:forall y0 : U, R x0 y0 -> noetherian U R y0
H'2:forall y0 : U,
R x0 y0 ->
forall y1 z0 : U, Rstar U R y0 y1 -> Rstar U R y0 z0 -> coherent U R y1 z0
y, z:U
H'3:Rstar U R x0 y
H'4:Rstar U R x0 z
u:U
H'5:R x0 u
H'6:Rstar U R u y
v:U
H'7:R x0 v
H'8:Rstar U R v z
t:U
H'10:Rstar U R u t
H'11:Rstar U R v t
coherent U R y z
    clear H'0.U:Type
R:Relation U
H':Noetherian U R
x, x0:U
H'1:forall y0 : U, R x0 y0 -> noetherian U R y0
H'2:forall y0 : U,
R x0 y0 ->
forall y1 z0 : U,
Rstar U R y0 y1 ->
Rstar U R y0 z0 -> coherent U R y1 z0
y, z:U
H'3:Rstar U R x0 y
H'4:Rstar U R x0 z
u:U
H'5:R x0 u
H'6:Rstar U R u y
v:U
H'7:R x0 v
H'8:Rstar U R v z
t:U
H'10:Rstar U R u t
H'11:Rstar U R v t
coherent U R y z
    unfold coherent at 1 in H'2.U:Type
R:Relation U
H':Noetherian U R
x, x0:U
H'1:forall y0 : U, R x0 y0 -> noetherian U R y0
H'2:forall y0 : U,
R x0 y0 ->
forall y1 z0 : U,
Rstar U R y0 y1 ->
Rstar U R y0 z0 ->
exists z1 : U,
  Rstar U R y1 z1 /\ Rstar U R z0 z1
y, z:U
H'3:Rstar U R x0 y
H'4:Rstar U R x0 z
u:U
H'5:R x0 u
H'6:Rstar U R u y
v:U
H'7:R x0 v
H'8:Rstar U R v z
t:U
H'10:Rstar U R u t
H'11:Rstar U R v t
coherent U R y z
    generalize (H'2 u); intro h; lapply h;
      [ intro H'0; generalize (H'0 y t); intro h0; lapply h0;
        [ intro H'9; lapply H'9;
          [ intro h1; elim h1; intros y1 h2; elim h2; intros H'12 H'13;
            clear h h0 H'9 h1 h2
          | clear h h0 ]
        | clear h h0 ]
      | clear h ]; auto with sets.U:Type
R:Relation U
H':Noetherian U R
x, x0:U
H'1:forall y0 : U, R x0 y0 -> noetherian U R y0
H'2:forall y0 : U,
R x0 y0 ->
forall y2 z0 : U,
Rstar U R y0 y2 ->
Rstar U R y0 z0 ->
exists z1 : U,
  Rstar U R y2 z1 /\ Rstar U R z0 z1
y, z:U
H'3:Rstar U R x0 y
H'4:Rstar U R x0 z
u:U
H'5:R x0 u
H'6:Rstar U R u y
v:U
H'7:R x0 v
H'8:Rstar U R v z
t:U
H'10:Rstar U R u t
H'11:Rstar U R v t
H'0:forall y0 z0 : U,
Rstar U R u y0 ->
Rstar U R u z0 ->
exists z1 : U,
  Rstar U R y0 z1 /\ Rstar U R z0 z1
y1:U
H'12:Rstar U R y y1
H'13:Rstar U R t y1
coherent U R y z
    generalize Rstar_transitive; intro T; red in T.U:Type
R:Relation U
H':Noetherian U R
x, x0:U
H'1:forall y0 : U, R x0 y0 -> noetherian U R y0
H'2:forall y0 : U,
R x0 y0 ->
forall y2 z0 : U,
Rstar U R y0 y2 ->
Rstar U R y0 z0 ->
exists z1 : U,
  Rstar U R y2 z1 /\ Rstar U R z0 z1
y, z:U
H'3:Rstar U R x0 y
H'4:Rstar U R x0 z
u:U
H'5:R x0 u
H'6:Rstar U R u y
v:U
H'7:R x0 v
H'8:Rstar U R v z
t:U
H'10:Rstar U R u t
H'11:Rstar U R v t
H'0:forall y0 z0 : U,
Rstar U R u y0 ->
Rstar U R u z0 ->
exists z1 : U,
  Rstar U R y0 z1 /\ Rstar U R z0 z1
y1:U
H'12:Rstar U R y y1
H'13:Rstar U R t y1
T:forall (U0 : Type) (R0 : Relation U0)
  (x1 y0 z0 : U0),
Rstar U0 R0 x1 y0 ->
Rstar U0 R0 y0 z0 -> Rstar U0 R0 x1 z0
coherent U R y z
    generalize (H'2 v); intro h; lapply h;
      [ intro H'9; generalize (H'9 y1 z); intro h0; lapply h0;
        [ intro H'14; lapply H'14;
          [ intro h1; elim h1; intros z1 h2; elim h2; intros H'15 H'16;
            clear h h0 H'14 h1 h2
          | clear h h0 ]
        | clear h h0 ]
      | clear h ]; auto with sets.U:Type
R:Relation U
H':Noetherian U R
x, x0:U
H'1:forall y0 : U, R x0 y0 -> noetherian U R y0
H'2:forall y0 : U,
R x0 y0 ->
forall y2 z0 : U,
Rstar U R y0 y2 ->
Rstar U R y0 z0 ->
exists z2 : U,
  Rstar U R y2 z2 /\ Rstar U R z0 z2
y, z:U
H'3:Rstar U R x0 y
H'4:Rstar U R x0 z
u:U
H'5:R x0 u
H'6:Rstar U R u y
v:U
H'7:R x0 v
H'8:Rstar U R v z
t:U
H'10:Rstar U R u t
H'11:Rstar U R v t
H'0:forall y0 z0 : U,
Rstar U R u y0 ->
Rstar U R u z0 ->
exists z2 : U,
  Rstar U R y0 z2 /\ Rstar U R z0 z2
y1:U
H'12:Rstar U R y y1
H'13:Rstar U R t y1
T:forall (U0 : Type) (R0 : Relation U0)
  (x1 y0 z0 : U0),
Rstar U0 R0 x1 y0 ->
Rstar U0 R0 y0 z0 -> Rstar U0 R0 x1 z0
H'9:forall y0 z0 : U,
Rstar U R v y0 ->
Rstar U R v z0 ->
exists z2 : U,
  Rstar U R y0 z2 /\ Rstar U R z0 z2
z1:U
H'15:Rstar U R y1 z1
H'16:Rstar U R z z1
coherent U R y z
U:Type
R:Relation U
H':Noetherian U R
x, x0:U
H'1:forall y0 : U, R x0 y0 -> noetherian U R y0
H'2:forall y0 : U,
R x0 y0 ->
forall y2 z0 : U,
Rstar U R y0 y2 ->
Rstar U R y0 z0 ->
exists z1 : U,
  Rstar U R y2 z1 /\ Rstar U R z0 z1
y, z:U
H'3:Rstar U R x0 y
H'4:Rstar U R x0 z
u:U
H'5:R x0 u
H'6:Rstar U R u y
v:U
H'7:R x0 v
H'8:Rstar U R v z
t:U
H'10:Rstar U R u t
H'11:Rstar U R v t
H'0:forall y0 z0 : U,
Rstar U R u y0 ->
Rstar U R u z0 ->
exists z1 : U,
  Rstar U R y0 z1 /\ Rstar U R z0 z1
y1:U
H'12:Rstar U R y y1
H'13:Rstar U R t y1
T:forall (U0 : Type) (R0 : Relation U0)
  (x1 y0 z0 : U0),
Rstar U0 R0 x1 y0 ->
Rstar U0 R0 y0 z0 -> Rstar U0 R0 x1 z0
H'9:forall y0 z0 : U,
Rstar U R v y0 ->
Rstar U R v z0 ->
exists z1 : U,
  Rstar U R y0 z1 /\ Rstar U R z0 z1
Rstar U R v y1
    *U:Type
R:Relation U
H':Noetherian U R
x, x0:U
H'1:forall y0 : U, R x0 y0 -> noetherian U R y0
H'2:forall y0 : U,
R x0 y0 ->
forall y2 z0 : U,
Rstar U R y0 y2 ->
Rstar U R y0 z0 ->
exists z2 : U,
  Rstar U R y2 z2 /\ Rstar U R z0 z2
y, z:U
H'3:Rstar U R x0 y
H'4:Rstar U R x0 z
u:U
H'5:R x0 u
H'6:Rstar U R u y
v:U
H'7:R x0 v
H'8:Rstar U R v z
t:U
H'10:Rstar U R u t
H'11:Rstar U R v t
H'0:forall y0 z0 : U,
Rstar U R u y0 ->
Rstar U R u z0 ->
exists z2 : U,
  Rstar U R y0 z2 /\ Rstar U R z0 z2
y1:U
H'12:Rstar U R y y1
H'13:Rstar U R t y1
T:forall (U0 : Type) (R0 : Relation U0)
  (x1 y0 z0 : U0),
Rstar U0 R0 x1 y0 ->
Rstar U0 R0 y0 z0 -> Rstar U0 R0 x1 z0
H'9:forall y0 z0 : U,
Rstar U R v y0 ->
Rstar U R v z0 ->
exists z2 : U,
  Rstar U R y0 z2 /\ Rstar U R z0 z2
z1:U
H'15:Rstar U R y1 z1
H'16:Rstar U R z z1
coherent U R y z red; (exists z1; split); auto with sets.U:Type
R:Relation U
H':Noetherian U R
x, x0:U
H'1:forall y0 : U, R x0 y0 -> noetherian U R y0
H'2:forall y0 : U,
R x0 y0 ->
forall y2 z0 : U,
Rstar U R y0 y2 ->
Rstar U R y0 z0 ->
exists z2 : U,
  Rstar U R y2 z2 /\ Rstar U R z0 z2
y, z:U
H'3:Rstar U R x0 y
H'4:Rstar U R x0 z
u:U
H'5:R x0 u
H'6:Rstar U R u y
v:U
H'7:R x0 v
H'8:Rstar U R v z
t:U
H'10:Rstar U R u t
H'11:Rstar U R v t
H'0:forall y0 z0 : U,
Rstar U R u y0 ->
Rstar U R u z0 ->
exists z2 : U,
  Rstar U R y0 z2 /\ Rstar U R z0 z2
y1:U
H'12:Rstar U R y y1
H'13:Rstar U R t y1
T:forall (U0 : Type) (R0 : Relation U0)
  (x1 y0 z0 : U0),
Rstar U0 R0 x1 y0 ->
Rstar U0 R0 y0 z0 -> Rstar U0 R0 x1 z0
H'9:forall y0 z0 : U,
Rstar U R v y0 ->
Rstar U R v z0 ->
exists z2 : U,
  Rstar U R y0 z2 /\ Rstar U R z0 z2
z1:U
H'15:Rstar U R y1 z1
H'16:Rstar U R z z1
Rstar U R y z1
      apply T with y1; auto with sets.
    *U:Type
R:Relation U
H':Noetherian U R
x, x0:U
H'1:forall y0 : U, R x0 y0 -> noetherian U R y0
H'2:forall y0 : U,
R x0 y0 ->
forall y2 z0 : U,
Rstar U R y0 y2 ->
Rstar U R y0 z0 ->
exists z1 : U,
  Rstar U R y2 z1 /\ Rstar U R z0 z1
y, z:U
H'3:Rstar U R x0 y
H'4:Rstar U R x0 z
u:U
H'5:R x0 u
H'6:Rstar U R u y
v:U
H'7:R x0 v
H'8:Rstar U R v z
t:U
H'10:Rstar U R u t
H'11:Rstar U R v t
H'0:forall y0 z0 : U,
Rstar U R u y0 ->
Rstar U R u z0 ->
exists z1 : U,
  Rstar U R y0 z1 /\ Rstar U R z0 z1
y1:U
H'12:Rstar U R y y1
H'13:Rstar U R t y1
T:forall (U0 : Type) (R0 : Relation U0)
  (x1 y0 z0 : U0),
Rstar U0 R0 x1 y0 ->
Rstar U0 R0 y0 z0 -> Rstar U0 R0 x1 z0
H'9:forall y0 z0 : U,
Rstar U R v y0 ->
Rstar U R v z0 ->
exists z1 : U,
  Rstar U R y0 z1 /\ Rstar U R z0 z1
Rstar U R v y1 apply T with t; auto with sets.
Qed.