definition f_transitive_next:
relation3 … ≝ λR1,R2,R3.
∀f,L,T. L ⊢ 𝐅+❪T❫ ≘ f →
- â\88\80g,I,K,i. â\87©[i] L â\89\98 K.â\93\98[I] â\86\92 â\86\91g = ⫱*[i] f →
+ â\88\80g,I,K,i. â\87©[i] L â\89\98 K.â\93\98[I] â\86\92 â\86\91g = â«°*[i] f →
R_pw_transitive_sex (cext2 R1) (cext2 R2) (cext2 R3) (cext2 R1) cfull g K I.
definition f_confluent1_next: relation2 … ≝ λR1,R2.
∀f,L,T. L ⊢ 𝐅+❪T❫ ≘ f →
- â\88\80g,I,K,i. â\87©[i] L â\89\98 K.â\93\98[I] â\86\92 â\86\91g = ⫱*[i] f →
+ â\88\80g,I,K,i. â\87©[i] L â\89\98 K.â\93\98[I] â\86\92 â\86\91g = â«°*[i] f →
R_pw_confluent1_sex (cext2 R1) (cext2 R1) (cext2 R2) cfull g K I.
(* Properties with generic slicing for local environments *******************)