1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
19 (*#***********************************************************************)
21 (* v * The Coq Proof Assistant / The Coq Development Team *)
23 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
25 (* \VV/ **************************************************************)
27 (* // * This file is distributed under the terms of the *)
29 (* * GNU Lesser General Public License Version 2.1 *)
31 (*#***********************************************************************)
33 (*i $Id: Newman.v,v 1.7.2.1 2004/07/16 19:31:16 herbelin Exp $ i*)
35 include "Relations/Rstar.ma".
42 cic:/Coq/Relations/Newman/Newman/A.var
46 cic:/Coq/Relations/Newman/Newman/R.var
49 (* UNAVAILABLE OBJECT: cic:/Coq/Relations/Newman/Newman/Rstar.con *********)
51 inline procedural "cic:/Coq/Relations/Newman/Newman/Rstar.con" "Newman__" as definition.
53 (* UNAVAILABLE OBJECT: cic:/Coq/Relations/Newman/Newman/Rstar_reflexive.con *)
55 inline procedural "cic:/Coq/Relations/Newman/Newman/Rstar_reflexive.con" "Newman__" as definition.
57 (* UNAVAILABLE OBJECT: cic:/Coq/Relations/Newman/Newman/Rstar_transitive.con *)
59 inline procedural "cic:/Coq/Relations/Newman/Newman/Rstar_transitive.con" "Newman__" as definition.
61 (* UNAVAILABLE OBJECT: cic:/Coq/Relations/Newman/Newman/Rstar_Rstar'.con **)
63 inline procedural "cic:/Coq/Relations/Newman/Newman/Rstar_Rstar'.con" "Newman__" as definition.
65 inline procedural "cic:/Coq/Relations/Newman/coherence.con" as definition.
67 inline procedural "cic:/Coq/Relations/Newman/coherence_intro.con" as theorem.
69 (*#* A very simple case of coherence : *)
71 inline procedural "cic:/Coq/Relations/Newman/Rstar_coherence.con" as lemma.
73 (*#* coherence is symmetric *)
75 inline procedural "cic:/Coq/Relations/Newman/coherence_sym.con" as lemma.
77 inline procedural "cic:/Coq/Relations/Newman/confluence.con" as definition.
79 inline procedural "cic:/Coq/Relations/Newman/local_confluence.con" as definition.
81 inline procedural "cic:/Coq/Relations/Newman/noetherian.con" as definition.
84 Section Newman_section
87 (*#* The general hypotheses of the theorem *)
90 cic:/Coq/Relations/Newman/Newman/Newman_section/Hyp1.var
94 cic:/Coq/Relations/Newman/Newman/Newman_section/Hyp2.var
97 (*#* The induction hypothesis *)
104 cic:/Coq/Relations/Newman/Newman/Newman_section/Induct/x.var
108 cic:/Coq/Relations/Newman/Newman/Newman_section/Induct/hyp_ind.var
111 (*#* Confluence in [x] *)
114 cic:/Coq/Relations/Newman/Newman/Newman_section/Induct/y.var
118 cic:/Coq/Relations/Newman/Newman/Newman_section/Induct/z.var
122 cic:/Coq/Relations/Newman/Newman/Newman_section/Induct/h1.var
126 cic:/Coq/Relations/Newman/Newman/Newman_section/Induct/h2.var
129 (*#* particular case [x->u] and [u->*y] *)
136 cic:/Coq/Relations/Newman/Newman/Newman_section/Induct/Newman_/u.var
140 cic:/Coq/Relations/Newman/Newman/Newman_section/Induct/Newman_/t1.var
144 cic:/Coq/Relations/Newman/Newman/Newman_section/Induct/Newman_/t2.var
147 (*#* In the usual diagram, we assume also [x->v] and [v->*z] *)
149 inline procedural "cic:/Coq/Relations/Newman/Diagram.con" as theorem.
151 inline procedural "cic:/Coq/Relations/Newman/caseRxy.con" as theorem.
153 (*i case x->v->*z i*)
159 inline procedural "cic:/Coq/Relations/Newman/Ind_proof.con" as theorem.
161 (*i case x->u->*z i*)
167 inline procedural "cic:/Coq/Relations/Newman/Newman.con" as theorem.