equal
deleted
inserted
replaced
1690 \begin{tabular}{cp{7cm}} |
1690 \begin{tabular}{cp{7cm}} |
1691 %% @{text "\<forall>b. P1 b KStar"}\\ |
1691 %% @{text "\<forall>b. P1 b KStar"}\\ |
1692 %% @{text "\<forall>tk1 tk2 b. \<^raw:\big(>\<forall>c. P1 c tk1 \<and> \<forall>c. P1 c tk2\<^raw:\big)> \<Longrightarrow> P1 b (KFun tk1 tk2)"}\\ |
1692 %% @{text "\<forall>tk1 tk2 b. \<^raw:\big(>\<forall>c. P1 c tk1 \<and> \<forall>c. P1 c tk2\<^raw:\big)> \<Longrightarrow> P1 b (KFun tk1 tk2)"}\\ |
1693 %% @{text "\<dots>"}\\ |
1693 %% @{text "\<dots>"}\\ |
1694 @{text "\<forall>v ty t1 t2 b. \<^raw:\big(>\<forall>c. P3 c ty \<and> \<forall>c. P7 c t1 \<and> \<forall>c. P7 c t2 \<and>"}\\ |
1694 @{text "\<forall>v ty t1 t2 b. \<^raw:\big(>\<forall>c. P3 c ty \<and> \<forall>c. P7 c t1 \<and> \<forall>c. P7 c t2 \<and>"}\\ |
1695 @{text "\<^raw:\hspace{2cm}>\<and> atom var \<sharp> b\<^raw:\big)> \<Longrightarrow> P7 b (Let v ty t1 t2)"}\\ |
1695 @{text "\<^raw:\hfill>\<and> atom var \<sharp> b\<^raw:\big)> \<Longrightarrow> P7 b (Let v ty t1 t2)"}\\ |
1696 @{text "\<forall>p t al b. \<^raw:\big(>\<forall>c. P9 c p \<and> \<forall>c. P7 c t \<and> \<forall>c. P8 c al \<and>"}\\ |
1696 @{text "\<forall>p t al b. \<^raw:\big(>\<forall>c. P9 c p \<and> \<forall>c. P7 c t \<and> \<forall>c. P8 c al \<and>"}\\ |
1697 @{text "\<^raw:\hspace{2cm}>\<and> set (bv p) \<sharp>* b\<^raw:\big)> \<Longrightarrow> P8 b (ACons p t al)"}\\ |
1697 @{text "\<^raw:\hfill>\<and> set (bv p) \<sharp>* b\<^raw:\big)> \<Longrightarrow> P8 b (ACons p t al)"}\\ |
1698 @{text "\<dots>"} |
1698 @{text "\<dots>"} |
1699 \end{tabular} |
1699 \end{tabular} |
1700 } |
1700 } |
1701 \end{equation} |
1701 \end{equation} |
1702 |
1702 |