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___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
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 2003/11/29 17:28:41 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 inline procedural "cic:/Coq/Relations/Newman/Newman/Rstar.con" "Newman__" as definition.
51 inline procedural "cic:/Coq/Relations/Newman/Newman/Rstar_reflexive.con" "Newman__" as definition.
53 inline procedural "cic:/Coq/Relations/Newman/Newman/Rstar_transitive.con" "Newman__" as definition.
55 inline procedural "cic:/Coq/Relations/Newman/Newman/Rstar_Rstar'.con" "Newman__" as definition.
57 inline procedural "cic:/Coq/Relations/Newman/coherence.con" as definition.
59 inline procedural "cic:/Coq/Relations/Newman/coherence_intro.con" as theorem.
61 (*#* A very simple case of coherence : *)
63 inline procedural "cic:/Coq/Relations/Newman/Rstar_coherence.con" as lemma.
65 (*#* coherence is symmetric *)
67 inline procedural "cic:/Coq/Relations/Newman/coherence_sym.con" as lemma.
69 inline procedural "cic:/Coq/Relations/Newman/confluence.con" as definition.
71 inline procedural "cic:/Coq/Relations/Newman/local_confluence.con" as definition.
73 inline procedural "cic:/Coq/Relations/Newman/noetherian.con" as definition.
76 Section Newman_section
79 (*#* The general hypotheses of the theorem *)
82 cic:/Coq/Relations/Newman/Newman/Newman_section/Hyp1.var
86 cic:/Coq/Relations/Newman/Newman/Newman_section/Hyp2.var
89 (*#* The induction hypothesis *)
96 cic:/Coq/Relations/Newman/Newman/Newman_section/Induct/x.var
100 cic:/Coq/Relations/Newman/Newman/Newman_section/Induct/hyp_ind.var
103 (*#* Confluence in [x] *)
106 cic:/Coq/Relations/Newman/Newman/Newman_section/Induct/y.var
110 cic:/Coq/Relations/Newman/Newman/Newman_section/Induct/z.var
114 cic:/Coq/Relations/Newman/Newman/Newman_section/Induct/h1.var
118 cic:/Coq/Relations/Newman/Newman/Newman_section/Induct/h2.var
121 (*#* particular case [x->u] and [u->*y] *)
128 cic:/Coq/Relations/Newman/Newman/Newman_section/Induct/Newman_/u.var
132 cic:/Coq/Relations/Newman/Newman/Newman_section/Induct/Newman_/t1.var
136 cic:/Coq/Relations/Newman/Newman/Newman_section/Induct/Newman_/t2.var
139 (*#* In the usual diagram, we assume also [x->v] and [v->*z] *)
141 inline procedural "cic:/Coq/Relations/Newman/Diagram.con" as theorem.
143 inline procedural "cic:/Coq/Relations/Newman/caseRxy.con" as theorem.
145 (*i case x->v->*z i*)
151 inline procedural "cic:/Coq/Relations/Newman/Ind_proof.con" as theorem.
153 (*i case x->u->*z i*)
159 inline procedural "cic:/Coq/Relations/Newman/Newman.con" as theorem.