1191 the union of the values, @{text v}, calculated by the rules for empty, shallow and |
1191 the union of the values, @{text v}, calculated by the rules for empty, shallow and |
1192 deep binding clauses: |
1192 deep binding clauses: |
1193 % |
1193 % |
1194 \begin{equation}\label{deepbinder} |
1194 \begin{equation}\label{deepbinder} |
1195 \mbox{% |
1195 \mbox{% |
1196 \begin{tabular}{c@ {\hspace{2mm}}p{7cm}} |
1196 \begin{tabular}{c@ {\hspace{2mm}}p{7.4cm}} |
1197 \multicolumn{2}{@ {}l}{\isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "y"}:}\\ |
1197 \multicolumn{2}{@ {}l}{\isacommand{bind}~@{term "{}"}~\isacommand{in}~@{text "y"}:}\\ |
1198 $\bullet$ & @{term "v = fv_ty y"} provided @{text "y"} is of type @{text "ty"}\smallskip\\ |
1198 $\bullet$ & @{term "v = fv_ty y"} provided @{text "y"} is of type @{text "ty"}\smallskip\\ |
1199 |
1199 |
1200 \multicolumn{2}{@ {}l}{\isacommand{bind}~@{text "x\<^isub>1..x\<^isub>n"}~\isacommand{in}~@{text "y\<^isub>1..y\<^isub>m"}:}\\ |
1200 \multicolumn{2}{@ {}l}{\isacommand{bind}~@{text "x\<^isub>1\<dots>x\<^isub>n"}~\isacommand{in}~@{text "y\<^isub>1\<dots>y\<^isub>m"}:}\\ |
1201 $\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \<union> .. \<union> fv_ty\<^isub>m y\<^isub>m)"}\\ |
1201 $\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \<union> \<dots> \<union> fv_ty\<^isub>m y\<^isub>m)"}\\ |
1202 & \hspace{10mm}@{text "- (fv_aty\<^isub>1 x\<^isub>1 \<union> .. \<union> fv_aty\<^isub>n x\<^isub>n)"}\\ |
1202 & \hspace{15mm}@{text "- (fv_aty\<^isub>1 x\<^isub>1 \<union> \<dots> \<union> fv_aty\<^isub>n x\<^isub>n)"}\\ |
1203 & provided the bodies @{text "y"}$_{1..m}$ are of type @{text "ty"}$_{1..m}$ and the |
1203 & provided the bodies @{text "y"}$_{1..m}$ are of type @{text "ty"}$_{1..m}$ and the |
1204 binders @{text "x"}$_{1..n}$ of atomic types @{text "aty"}$_{1..n}$\smallskip\\ |
1204 binders @{text "x"}$_{1..n}$ of atomic types @{text "aty"}$_{1..n}$\smallskip\\ |
1205 |
1205 |
1206 \multicolumn{2}{@ {}l}{\isacommand{bind}~@{text "bn x"}~\isacommand{in}~@{text "y\<^isub>1..y\<^isub>m"}:}\\ |
1206 \multicolumn{2}{@ {}l}{\isacommand{bind}~@{text "bn x"}~\isacommand{in}~@{text "y\<^isub>1\<dots>y\<^isub>m"}:}\\ |
1207 $\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \<union> .. \<union> fv_ty\<^isub>m y\<^isub>m) - (bn x) \<union> (fv_bn x)"}\\ |
1207 $\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \<union> \<dots> \<union> fv_ty\<^isub>m y\<^isub>m) - set (bn x) \<union> (fv_bn x)"}\\ |
1208 $\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \<union> .. \<union> fv_ty\<^isub>m y\<^isub>m) - (bn x)"}\\ |
1208 $\bullet$ & @{text "v = (fv_ty\<^isub>1 y\<^isub>1 \<union> \<dots> \<union> fv_ty\<^isub>m y\<^isub>m) - set (bn x)"}\\ |
1209 & provided the @{text "y\<^isub>i"} are of type @{text "ty\<^isub>i"}; the first |
1209 & provided the @{text "y"}$_{1..m}$ are of type @{text "ty"}$_{1..m}$; the first |
1210 clause applies for @{text x} being a non-recursive deep binder, the |
1210 clause applies for @{text x} being a non-recursive deep binder, the |
1211 second for a recursive deep binder |
1211 second for a recursive deep binder |
1212 \end{tabular}} |
1212 \end{tabular}} |
1213 \end{equation} |
1213 \end{equation} |
1214 |
1214 |