-definition R_frees_confluent: predicate (relation3 …) ≝
- λRN.
- ∀f1,L,T1. L ⊢ 𝐅*⦃T1⦄ ≡ f1 → ∀T2. RN L T1 T2 →
- ∃∃f2. L ⊢ 𝐅*⦃T2⦄ ≡ f2 & f2 ⊆ f1.
-
-definition lexs_frees_confluent: relation (relation3 …) ≝
- λRN,RP.
- ∀f1,L1,T. L1 ⊢ 𝐅*⦃T⦄ ≡ f1 →
- ∀L2. L1 ⪤*[RN, RP, f1] L2 →
- ∃∃f2. L2 ⊢ 𝐅*⦃T⦄ ≡ f2 & f2 ⊆ f1.
-