V_______________________________________________________________ *)
include "basics/logic.ma".
+include "basics/core_notation/compose_2.ma".
+include "basics/core_notation/subseteq_2.ma".
(********** predicates *********)
definition singlevalued: ∀A,B. predicate (relation2 A B) ≝ λA,B,R.
∀a,b1. R a b1 → ∀b2. R a b2 → b1 = b2.
-definition confluent1: ∀A. relation A → predicate A ≝ λA,R,a0.
- ∀a1. R a0 a1 → ∀a2. R a0 a2 →
- ∃∃a. R a1 a & R a2 a.
+definition pw_confluent: ∀A. relation A → predicate A ≝ λA,R,a0.
+ ∀a1. R a0 a1 → ∀a2. R a0 a2 →
+ ∃∃a. R a1 a & R a2 a.
definition confluent: ∀A. predicate (relation A) ≝ λA,R.
- ∀a0. confluent1 … R a0.
+ ∀a0. pw_confluent … R a0.
(* triangular confluence of two relations *)
definition Conf3: ∀A,B. relation2 A B → relation A → Prop ≝ λA,B,S,R.