diff options
Diffstat (limited to 'theories/Sets/Relations_2.v')
| -rwxr-xr-x | theories/Sets/Relations_2.v | 34 |
1 files changed, 17 insertions, 17 deletions
diff --git a/theories/Sets/Relations_2.v b/theories/Sets/Relations_2.v index 65363d816..d7ee68b66 100755 --- a/theories/Sets/Relations_2.v +++ b/theories/Sets/Relations_2.v @@ -29,28 +29,28 @@ Require Export Relations_1. Section Relations_2. -Variable U: Type. -Variable R: (Relation U). +Variable U : Type. +Variable R : Relation U. -Inductive Rstar : (Relation U) := - Rstar_0: (x: U) (Rstar x x) - | Rstar_n: (x, y, z: U) (R x y) -> (Rstar y z) -> (Rstar x z). +Inductive Rstar : Relation U := + | Rstar_0 : forall x:U, Rstar x x + | Rstar_n : forall x y z:U, R x y -> Rstar y z -> Rstar x z. -Inductive Rstar1 : (Relation U) := - Rstar1_0: (x: U) (Rstar1 x x) - | Rstar1_1: (x: U) (y: U) (R x y) -> (Rstar1 x y) - | Rstar1_n: (x, y, z: U) (Rstar1 x y) -> (Rstar1 y z) -> (Rstar1 x z). +Inductive Rstar1 : Relation U := + | Rstar1_0 : forall x:U, Rstar1 x x + | Rstar1_1 : forall x y:U, R x y -> Rstar1 x y + | Rstar1_n : forall x y z:U, Rstar1 x y -> Rstar1 y z -> Rstar1 x z. -Inductive Rplus : (Relation U) := - Rplus_0: (x, y: U) (R x y) -> (Rplus x y) - | Rplus_n: (x, y, z: U) (R x y) -> (Rplus y z) -> (Rplus x z). +Inductive Rplus : Relation U := + | Rplus_0 : forall x y:U, R x y -> Rplus x y + | Rplus_n : forall x y z:U, R x y -> Rplus y z -> Rplus x z. Definition Strongly_confluent : Prop := - (x, a, b: U) (R x a) -> (R x b) -> (exT U [z: U] (R a z) /\ (R b z)). + forall x a b:U, R x a -> R x b -> ex (fun z:U => R a z /\ R b z). End Relations_2. -Hints Resolve Rstar_0 : sets v62. -Hints Resolve Rstar1_0 : sets v62. -Hints Resolve Rstar1_1 : sets v62. -Hints Resolve Rplus_0 : sets v62. +Hint Resolve Rstar_0: sets v62. +Hint Resolve Rstar1_0: sets v62. +Hint Resolve Rstar1_1: sets v62. +Hint Resolve Rplus_0: sets v62.
\ No newline at end of file |