1236 provided @{term "x\<^isub>j"} is a deep recursive binder with the auxiliary binding |
1236 provided @{term "x\<^isub>j"} is a deep recursive binder with the auxiliary binding |
1237 function @{text "bn\<^isub>m"} and permutation @{text "\<pi>"}, @{term "fvs"} is a compound |
1237 function @{text "bn\<^isub>m"} and permutation @{text "\<pi>"}, @{term "fvs"} is a compound |
1238 free variable function returning the union of appropriate @{term "fv_ty\<^isub>x"} and |
1238 free variable function returning the union of appropriate @{term "fv_ty\<^isub>x"} and |
1239 @{term "R"} is the composition of equivalence relations @{text "\<approx>"} and @{text "\<approx>\<^isub>n"}\\ |
1239 @{term "R"} is the composition of equivalence relations @{text "\<approx>"} and @{text "\<approx>\<^isub>n"}\\ |
1240 $\bullet$ & @{text "x\<^isub>j"} has a deep recursive binding\\ |
1240 $\bullet$ & @{text "x\<^isub>j"} has a deep recursive binding\\ |
1241 $\bullet$ & @{term "({x\<^isub>n, x\<^isub>j) \<approx>gen R fv_ty \<pi> (y\<^isub>n, y\<^isub>j)"} provided @{text "x\<^isub>j"} has |
1241 $\bullet$ & @{term "({x\<^isub>n}, x\<^isub>j) \<approx>gen R fv_ty \<pi> ({y\<^isub>n}, y\<^isub>j)"} provided @{text "x\<^isub>j"} has |
1242 a shallow binder @{text "x\<^isub>n"} with permutation @{text "\<pi>"}, @{term "R"} is the |
1242 a shallow binder @{text "x\<^isub>n"} with permutation @{text "\<pi>"}, @{term "R"} is the |
1243 alpha-equivalence for @{term "x\<^isub>j"} |
1243 alpha-equivalence for @{term "x\<^isub>j"} |
1244 and @{term "fv_ty"} is the free variable function for @{term "x\<^isub>j"}\\ |
1244 and @{term "fv_ty"} is the free variable function for @{term "x\<^isub>j"}\\ |
1245 $\bullet$ & @{term "(bn\<^isub>m x\<^isub>n, x\<^isub>j) \<approx>gen R fv_ty \<pi> (bn\<^isub>m y\<^isub>n, y\<^isub>j)"} provided @{text "x\<^isub>j"} |
1245 $\bullet$ & @{term "(bn\<^isub>m x\<^isub>n, x\<^isub>j) \<approx>gen R fv_ty \<pi> (bn\<^isub>m y\<^isub>n, y\<^isub>j)"} provided @{text "x\<^isub>j"} |
1246 has a deep non-recursive binder @{text "bn\<^isub>m x\<^isub>n"} with permutation @{text "\<pi>"}, @{term "R"} is the |
1246 has a deep non-recursive binder @{text "bn\<^isub>m x\<^isub>n"} with permutation @{text "\<pi>"}, @{term "R"} is the |