-interpretation "generic entrywise extension (local environment)"
- 'Relation RN RP f L1 L2 = (sex RN RP f L1 L2).
-
-definition sex_transitive: relation3 lenv bind bind → relation3 lenv bind bind →
- relation3 lenv bind bind →
- relation3 lenv bind bind → relation3 lenv bind bind →
- relation3 rtmap lenv bind ≝
- λR1,R2,R3,RN,RP,f,L1,I1.
- ∀I. R1 L1 I1 I → ∀L2. L1 ⪤[RN,RP,f] L2 →
- ∀I2. R2 L2 I I2 → R3 L1 I1 I2.
-
-definition R_pw_confluent2_sex: relation3 lenv bind bind → relation3 lenv bind bind →
- relation3 lenv bind bind → relation3 lenv bind bind →
- relation3 lenv bind bind → relation3 lenv bind bind →
- relation3 rtmap lenv bind ≝
- λR1,R2,RN1,RP1,RN2,RP2,f,L0,I0.
- ∀I1. R1 L0 I0 I1 → ∀I2. R2 L0 I0 I2 →
- ∀L1. L0 ⪤[RN1,RP1,f] L1 → ∀L2. L0 ⪤[RN2,RP2,f] L2 →
- ∃∃I. R2 L1 I1 I & R1 L2 I2 I.
-
-definition R_pw_replace3_sex: relation3 lenv bind bind → relation3 lenv bind bind →
- relation3 lenv bind bind → relation3 lenv bind bind →
- relation3 lenv bind bind → relation3 lenv bind bind →
- relation3 rtmap lenv bind ≝
- λR1,R2,RN1,RP1,RN2,RP2,f,L0,I0.
- ∀I1. R1 L0 I0 I1 → ∀I2. R2 L0 I0 I2 →
- ∀L1. L0 ⪤[RN1,RP1,f] L1 → ∀L2. L0 ⪤[RN2,RP2,f] L2 →
- ∀I. R2 L1 I1 I → R1 L2 I2 I.
+interpretation
+ "generic entrywise extension (local environment)"
+ 'Relation RN RP f L1 L2 = (sex RN RP f L1 L2).
+
+definition R_pw_transitive_sex:
+ relation3 lenv bind bind → relation3 lenv bind bind →
+ relation3 lenv bind bind →
+ relation3 lenv bind bind → relation3 lenv bind bind →
+ relation3 rtmap lenv bind ≝
+ λR1,R2,R3,RN,RP,f,L1,I1.
+ ∀I. R1 L1 I1 I → ∀L2. L1 ⪤[RN,RP,f] L2 →
+ ∀I2. R2 L2 I I2 → R3 L1 I1 I2.
+
+definition R_pw_confluent1_sex:
+ relation3 lenv bind bind → relation3 lenv bind bind →
+ relation3 lenv bind bind → relation3 lenv bind bind →
+ relation3 rtmap lenv bind ≝
+ λR1,R2,RN,RP,f,L1,I1.
+ ∀I2. R1 L1 I1 I2 → ∀L2. L1 ⪤[RN,RP,f] L2 → R2 L2 I1 I2.
+
+definition R_pw_confluent2_sex:
+ relation3 lenv bind bind → relation3 lenv bind bind →
+ relation3 lenv bind bind → relation3 lenv bind bind →
+ relation3 lenv bind bind → relation3 lenv bind bind →
+ relation3 rtmap lenv bind ≝
+ λR1,R2,RN1,RP1,RN2,RP2,f,L0,I0.
+ ∀I1. R1 L0 I0 I1 → ∀I2. R2 L0 I0 I2 →
+ ∀L1. L0 ⪤[RN1,RP1,f] L1 → ∀L2. L0 ⪤[RN2,RP2,f] L2 →
+ ∃∃I. R2 L1 I1 I & R1 L2 I2 I.
+
+definition R_pw_replace3_sex:
+ relation3 lenv bind bind → relation3 lenv bind bind →
+ relation3 lenv bind bind → relation3 lenv bind bind →
+ relation3 lenv bind bind → relation3 lenv bind bind →
+ relation3 rtmap lenv bind ≝
+ λR1,R2,RN1,RP1,RN2,RP2,f,L0,I0.
+ ∀I1. R1 L0 I0 I1 → ∀I2. R2 L0 I0 I2 →
+ ∀L1. L0 ⪤[RN1,RP1,f] L1 → ∀L2. L0 ⪤[RN2,RP2,f] L2 →
+ ∀I. R2 L1 I1 I → R1 L2 I2 I.