(* ITERATED EXTENSION ON REFERRED ENTRIES OF A CONTEXT-SENSITIVE REALTION ***)
definition tc_f_dedropable_sn: predicate (relation3 lenv term term) ≝
- λR. â\88\80b,f,L1,K1. â¬\87*[b,f] L1 ≘ K1 →
- â\88\80K2,T. K1 ⪤*[R,T] K2 â\86\92 â\88\80U. â¬\86*[f] T ≘ U →
- â\88\83â\88\83L2. L1 ⪤*[R,U] L2 & â¬\87*[b,f] L2 ≘ K2 & L1 ≡[f] L2.
+ λR. â\88\80b,f,L1,K1. â\87©*[b,f] L1 ≘ K1 →
+ â\88\80K2,T. K1 ⪤*[R,T] K2 â\86\92 â\88\80U. â\87§*[f] T ≘ U →
+ â\88\83â\88\83L2. L1 ⪤*[R,U] L2 & â\87©*[b,f] L2 ≘ K2 & L1 ≡[f] L2.
definition tc_f_dropable_sn: predicate (relation3 lenv term term) ≝
- λR. â\88\80b,f,L1,K1. â¬\87*[b,f] L1 â\89\98 K1 â\86\92 ð\9d\90\94â¦\83fâ¦\84 →
- â\88\80L2,U. L1 ⪤*[R,U] L2 â\86\92 â\88\80T. â¬\86*[f] T ≘ U →
- â\88\83â\88\83K2. K1 ⪤*[R,T] K2 & â¬\87*[b,f] L2 ≘ K2.
+ λR. â\88\80b,f,L1,K1. â\87©*[b,f] L1 â\89\98 K1 â\86\92 ð\9d\90\94â\9d¨fâ\9d© →
+ â\88\80L2,U. L1 ⪤*[R,U] L2 â\86\92 â\88\80T. â\87§*[f] T ≘ U →
+ â\88\83â\88\83K2. K1 ⪤*[R,T] K2 & â\87©*[b,f] L2 ≘ K2.
definition tc_f_dropable_dx: predicate (relation3 lenv term term) ≝
λR. ∀L1,L2,U. L1 ⪤*[R,U] L2 →
- â\88\80b,f,K2. â¬\87*[b,f] L2 â\89\98 K2 â\86\92 ð\9d\90\94â¦\83fâ¦\84 â\86\92 â\88\80T. â¬\86*[f] T ≘ U →
- â\88\83â\88\83K1. â¬\87*[b,f] L1 ≘ K1 & K1 ⪤*[R,T] K2.
+ â\88\80b,f,K2. â\87©*[b,f] L2 â\89\98 K2 â\86\92 ð\9d\90\94â\9d¨fâ\9d© â\86\92 â\88\80T. â\87§*[f] T ≘ U →
+ â\88\83â\88\83K1. â\87©*[b,f] L1 ≘ K1 & K1 ⪤*[R,T] K2.
(* Properties with generic slicing for local environments *******************)