diff options
Diffstat (limited to 'theories/Relations')
| -rwxr-xr-x | theories/Relations/Newman.v | 14 | ||||
| -rwxr-xr-x | theories/Relations/Rstar.v | 10 |
2 files changed, 22 insertions, 2 deletions
diff --git a/theories/Relations/Newman.v b/theories/Relations/Newman.v index e7829b00e..2fe408543 100755 --- a/theories/Relations/Newman.v +++ b/theories/Relations/Newman.v @@ -10,6 +10,16 @@ Require Rstar. +Section Newman. + +Variable A: Type. +Variable R: A->A->Prop. + +Local Rstar := (Rstar A R). +Local Rstar_reflexive := (Rstar_reflexive A R). +Local Rstar_transitive := (Rstar_transitive A R). +Local Rstar_Rstar' := (Rstar_Rstar' A R). + Definition coherence := [x:A][y:A] (exT2 ? (Rstar x) (Rstar y)). Theorem coherence_intro : (x:A)(y:A)(z:A)(Rstar x z)->(Rstar y z)->(coherence x y). @@ -99,3 +109,7 @@ Theorem Newman : (x:A)(confluence x). Proof [x:A](Hyp1 x confluence Ind_proof). End Newman_section. + + +End Newman. + diff --git a/theories/Relations/Rstar.v b/theories/Relations/Rstar.v index a0aaed9ad..ff2e02a4b 100755 --- a/theories/Relations/Rstar.v +++ b/theories/Relations/Rstar.v @@ -10,8 +10,10 @@ (* Properties of a binary relation R on type A *) -Parameter A : Type. -Parameter R : A->A->Prop. +Section Rstar. + +Variable A : Type. +Variable R : A->A->Prop. (* Definition of the reflexive-transitive closure R* of R *) (* Smallest reflexive P containing R o P *) @@ -71,3 +73,7 @@ Theorem Rstar_Rstar': (x:A)(y:A)(Rstar x y)->(Rstar' x y). Definition commut := [A:Set][R1,R2:A->A->Prop] (x,y:A)(R1 y x)->(z:A)(R2 z y) ->(EX y':A |(R2 y' x) & (R1 z y')). + + +End Rstar. + |