\form#0:$\phi$
\form#1:$\Gamma$
\form#2:$\Gamma\models\bot$
\form#3:$\{\psi_1,\ldots,\psi_k\}$
\form#4:$D_{x/y}\equiv y\ne 0$
\form#5:$\Gamma\vdash\phi$
\form#6:\[\frac{\Gamma_1\vdash\phi_1\quad\cdots\quad\Gamma_n\vdash\phi_n} {\Gamma_1,\ldots,\Gamma_n\vdash\psi}\]
\form#7:\[\frac{\Gamma_1\vdash\alpha\quad \Gamma_2, \alpha\vdash\phi} {\Gamma_1, \Gamma_2\vdash\phi}\mbox{Cut}\]
\form#8:$\alpha$
\form#9:\[\frac{\Gamma_1\vdash x < y \quad \Gamma_2\vdash y < z} {\Gamma_1, \Gamma_2\vdash x < z}\mbox{project} \]
\form#10:\[\Gamma\models_T \phi\]
\form#11:$T$
\form#12:$\Gamma \models_T \phi$
\form#13:$\Gamma'$
\form#14:$\Gamma'\models_T \phi$
\form#15:$\Delta$
\form#16:$\Gamma \cup \Delta \not\models_T \mathit{false}$
\form#17:$\Gamma \cup \Delta \models_T \lnot \phi$
\form#18:$\mathrm{REAL}$
\form#19:$\mathrm{BITVECTOR}(n)$
\form#20:$n > 0$
\form#21:$\mathrm{BOOLEAN}$
\form#22:$\mathrm{INT}$
\form#23:$\to$
\form#24:\[ \begin{array}{l} \_ \to \_ \\[1ex] (\ \_\ ,\ \_\ ) \to \_ \\[1ex] (\ \_\ ,\ \_\ ,\ \_\ ) \to \_ \\[1ex] \ldots \end{array} \]
\form#25:$(T_1, \ldots, T_n) \to T$
\form#26:$T_1 \times \cdots \times T_n$
\form#27:$\mathrm{INT} \to \mathrm{REAL}$
\form#28:$\mathrm{ARRAY}\ \_\ \mathrm{OF}\ \_$
\form#29:$\mathrm{ARRAY}\ T_1\ \mathrm{OF}\ T_2$
\form#30:$T_1$
\form#31:$T_2$
\form#32:$T_1 \to T_2$
\form#33:\[ \begin{array}{l} [\ \_\ ] \\[1ex] [\ \_\ ,\ \_\ ] \\[1ex] [\ \_\ ,\ \_\ \ ,\ \_\ ] \\[1ex] \ldots \end{array} \]
\form#34:$[T_1, \ldots, T_n]$
\form#35:$[T_1 \times \cdots \times T_n] \to T$
\form#36:\[ [\#\ l_1: \_\ ,\ \ldots\ ,\ l_n: \_\ \#] \]
\form#37:$l_1,\ldots, l_n$
\form#38:\[ \begin{array}{l} \mathrm{DATATYPE} \\ \ \ \mathit{type\_name}_1 = C_{1,1} \mid C_{1,2} \mid \cdots \mid C_{1,m_1}, \\ \ \ \mathit{type\_name}_2 = C_{2,1} \mid C_{2,2} \mid \cdots \mid C_{2,m_2}, \\ \ \ \vdots \\ \ \ \mathit{type\_name}_n = C_{n,1} \mid C_{n,2} \mid \cdots \mid C_{n,m_n} \\ \mathrm{END}; \end{array} \]
\form#39:$C_{ij}$
\form#40:\[ \mathit{cons}(\ \mathit{sel}_1: T_1,\ \ldots,\ \mathit{sel}_k: T_k\ ) \]
\form#41:$T_1, \ldots, T_k$
\form#42:$\mathit{type\_name}_i$
\form#43:$cons$
\form#44:$(T_1, \ldots, T_k) \to \mathit{type\_name}_i$
\form#45:$\mathit{sel}_j$
\form#46:$\mathit{type\_name}_i \to T_j$
\form#47:$\mathit{is\_cons}$
\form#48:$\mathit{type\_name}_i \to \mathrm{BOOLEAN}$
\form#49:$n \geq 1$
\form#50:$T_1, \ldots, T_n$
\form#51:$f$
\form#52:$t_1, \ldots, t_n$
\form#53:$t_i$
\form#54:$T_i$
\form#55:$(\mathit{ARRAY}\ T_1\ \mathit{OF}\ T_2,\; T_1) \to T_2$
\form#56:$T_1, T_2$
\form#57:$f_1, \ldots, f_m: T;$
\form#58:$m > 0$
\form#59:$f_i$
\form#60:$f:T = t;$
\form#61:$\mathit{BOOLEAN}$
\form#62:\[ f:(T_1, \ldots, T_n) \to T = \mathrm{LAMBDA}(x_1:T_1, \ldots, x:T_n): t\;; \]
\form#63:$t$
\form#64:$\{x_1, \ldots, x_n\}$
\form#65:$x_1, \ldots, x_n$
\form#66:$k$
\form#67:$T_i, \ldots, T_{i+k-1}$
\form#68:$\mathrm{LAMBDA}(x_1:T_1, \ldots, x:T_n): t$
\form#69:$\mathrm{LAMBDA}(x_1:T_1, \ldots, x_i,\ldots, x_{i+k-1}:T_i,\ldots, x:T_n): t$
\form#70:\[ \begin{array}{rl} \mathrm{LET} & f_1 = t_1, \\ & \vdots \\ & f_n = t_m \\ \mathrm{IN} & t ; \end{array} \]
\form#71:\[ \begin{array}{rlcl} \mathrm{LET} & f_1 & = &\mathrm{LAMBDA}(x^1_1:T^1_1, \ldots, x^{n_1}_1:T^{n_1}_1):\; t_1, \\ & & \vdots & \\ & f_m & = & \mathrm{LAMBDA}(x^1_m:T^1_m, \ldots, x^{n_m}_m:T^{n_m}_m):\; t_m \\ \mathrm{IN} & t ; \end{array} \]
\form#72:$(\mathrm{BOOLEAN},\mathrm{BOOLEAN}) \to \mathrm{BOOLEAN}$
\form#73:$(T,T) \to \mathrm{BOOLEAN}$
\form#74:$\mathrm{DISTINCT}$
\form#75:$(T,...,T) \to \mathrm{BOOLEAN}$
\form#76:$(T,...,T)$
\form#77:$\psi$
\form#78:\[ Q\:(x_1:T_1, \ldots, x_k:T_k):\; p_1: \ldots\; p_n:\; \varphi \]
\form#79:$n \geq 0$
\form#80:$Q$
\form#81:$\mathrm{FORALL}$
\form#82:$\mathrm{EXISTS}$
\form#83:$\varphi$
\form#84:$p_i$
\form#85:$Q\:(x_1:T_1, \ldots, x_k:T_k)$
\form#86:\[ \mathrm{PATTERN}\; (t_1, \ldots, t_m) \]
\form#87:$t_1, \ldots, t_m$
\form#88:$x_1, \ldots, x_k$
\form#89:\[ \mathrm{IF}\ b\ \mathrm{THEN}\ t\ \mathrm{ELSIF}\ b_1\ \mathrm{THEN}\ t_1\ \ldots\ \mathrm{ELSIF}\ b_n\ \mathrm{THEN}\ t_n\ \mathrm{ELSE}\ t_{n+1}\ \mathrm{ENDIF} \]
\form#90:$b, b_1, \ldots, b_n$
\form#91:$t, t_1, \ldots, t_n, t_{n+1}$
\form#92:$m,n > 0$
\form#93:$m$
\form#94:$n$
\form#95:$2^n$
\form#96:$v_1$
\form#97:$v_2$
\form#98:$(m+n)$
\form#99:$[i:j]$
\form#100:$i, j$
\form#101:$n > i >= j >= 0$
\form#102:$v$
\form#103:$(i-j+1)$
\form#104:$i$
\form#105:$j$
\form#106:$<< k$
\form#107:$k >= 0$
\form#108:$(n+k)$
\form#109:$>> k$
\form#110:$v[n-1:k]$
\form#111:$\mathrm{SX}(\_, k)$
\form#112:$k >= n$
\form#113:$k-n$
\form#114:$\mathrm{BVZEROEXTEND}(\_, k)$
\form#115:$k >= 1$
\form#116:$n+k$
\form#117:$\mathrm{BVREPEAT}(\_, k)$
\form#118:$n*k$
\form#119:$\mathrm{BVROTL}(\_, k)$
\form#120:$(n)$
\form#121:$\mathrm{BVROTR}(\_, k)$
\form#122:$\mathrm{BVCOMP}$
\form#123:$\mathrm{0bin1}$
\form#124:$\mathrm{0bin0}$
\form#125:$k > 0$
\form#126:$\mathrm{BVPLUS}(k,\_, \_, \ldots)$
\form#127:$(k)$
\form#128:$\mathrm{BVMULT}(k,\_, \_)$
\form#129:$\mathrm{BVUMINUS}(\_)$
\form#130:$\mathrm{BVPLUS}(n,\verb|~|v,\mathrm{0bin1})$
\form#131:$\mathrm{BVSUB}(k,\_, \_)$
\form#132:$\mathrm{BVPLUS}(k,v_1,\mathrm{BVUMINUS}(v'))$
\form#133:$v'$
\form#134:$\mathrm{BVSHL}(\_, \_)$
\form#135:$\mathrm{BVASHR}(\_, \_)$
\form#136:$\mathrm{BVLSHR}(\_, \_)$
\form#137:$\mathrm{BVUDIV}(\_, \_)$
\form#138:$\mathrm{BVSDIV}(\_, \_)$
\form#139:$\mathrm{BVUREM}(\_, \_)$
\form#140:$\mathrm{BVSREM}(\_, \_)$
\form#141:$\mathrm{BVSMOD}(\_, \_)$
\form#142:$m, n > 0$
\form#143:$\mathrm{BVLT}(\_, \_)$
\form#144:$\mathrm{TRUE}$
\form#145:$\mathrm{BVLE}(\_, \_)$
\form#146:$\mathrm{BVGT}(\_, \_)$
\form#147:$\mathrm{BVLT}(v_2, v_1)$
\form#148:$\mathrm{BVGE}(\_, \_)$
\form#149:$\mathrm{BVLE}(v_2, v_1)$
\form#150:$\_[\_]$
\form#151:$\_\ \mathrm{WITH}\ [\_]\ := \_$
\form#152:$a$
\form#153:$e$
\form#154:$\_\ \mathrm{WITH}\ [\_]\ := \_, \ldots, [\_]\ := \_$
\form#155:$[\# l_0:T_0, \ldots, l_n:T_n \#]$
\form#156:\[ \begin{array}{l} \mathrm{DATATYPE} \\ \ \ \mathrm{Record} = \mathit{rec}(l_0:T_0, \ldots, l_n:T_n) \\ \mathrm{END}; \end{array} \]
\form#157:$(\#\ l_0 := \_, \ldots, l_n := \_\ \#)$
\form#158:$T_0, \ldots, T_n$
\form#159:$[\ T_0, \ldots, T_n\ ]$
\form#160:$(\ \_, \ldots, \_\ )$
\form#161:$[\#\ l_0:T_0, \ldots, l_n:T_n\ \#]$
\form#162:$i=0, \ldots, n$
\form#163:\[ \_\ \mathrm{WITH}\ .l_i\ := \_ \]
\form#164:$r$
\form#165:$l_i$
\form#166:$[T_0, \ldots, T_n]$
\form#167:\[ \_\ \mathrm{WITH}\ .i\ := \_ \]
\form#168:$F$
\form#169:$\Gamma\models_T F$
\form#170:$\Gamma\cup\{F\} \not\models_T \mathit{false}$
\form#171:$\Gamma \models_T F$
\form#172:$\Gamma \not\models_T F$
\form#173:$\Gamma \cup \{\neg F\}$
\form#174:$\Gamma\cup\Delta$
\form#175:$\Gamma\cup\Delta\models_T \neg F$
\form#176:$\neg f$
\form#177:$\Gamma\cup C$
\form#178:$\neg F$
\form#179:$\mathrm{FORALL}\; (x_1:T_1, \ldots, x_n:T_n)$
\form#180:$x_i$
\form#181:$\mathrm{PATTERN}\; (t_1, \ldots, t_m)$
\form#182:$\sigma$
\form#183:$(t_1, \ldots, t_m)$
\form#184:$i = 1, \ldots, m$
\form#185:$\sigma(t_i)$
\form#186:$s_i$
\form#187:$\Gamma \models_T \sigma(t_i) = s_i$
\form#188:$(x_1:T_1, \ldots, x_n:T_n)$
\form#189:$T_p$
\form#190:$p$
\form#191:$T \to \mathrm{BOOLEAN}$
\form#192:$T_P$
\form#193:\[ \mathit{subtype\_name}: \mathrm{TYPE} = \mathrm{SUBTYPE}(p) \]
\form#194:$\lambda x:T.\; \varphi$
\form#195:$x$
\form#196:$INT$
\form#197:$REAL$
\form#198:$\mathrm{int\_to\_real}:\mathrm{INT} \to \mathrm{REAL}$
\form#199:$\mathrm{real\_to\_int}:\mathrm{REAL} \to \mathrm{INT}$
\form#200:$S$
\form#201:$\exists\, x:T.\; p(x)$
\form#202:\[ \mathit{subtype\_name}: \mathrm{TYPE} = \mathrm{SUBTYPE}(p,t) \]
\form#203:$f(t_1, \ldots, t_n)$
\form#204:$i \geq 0$
\form#205:$(S_1, \ldots, S_n) \to S$
\form#206:$p(f(t_1, \ldots, t_n))$
\form#207:$S_i$
\form#208:$S_1 \to T_2$
\form#209:$S_1$
\form#210:$\mathrm{REAL} \times \mathrm{REAL}$
\form#211:$\mathrm{REAL} \times \{0\}$
\form#212:$0$
\form#213:$\forall\; x:\mathrm{REAL}.\; x/0 = 0$
\form#214:$M$
\form#215:\[ y > 0 \;\Rightarrow\; x/y = z \]
\form#216:$y$
\form#217:$z$
\form#218:$x/y = z$
\form#219:$\lnot \phi_1$
\form#220:$\phi_1$
\form#221:$\phi_1 \lor \phi_2$
\form#222:$\phi_2$
\form#223:$\exists\:x.\; \phi_1$
\form#224:$M'$
\form#225:$y > 0 \;\Rightarrow\; x/y = z$
\form#226:$\lnot(y > 0) \;\lor\; x/y = z$
\form#227:$\lnot(y > 0)$
\form#228:$\phi, \phi'$
\form#229:$\Gamma \models_T \phi \Leftrightarrow \phi'$
\form#230:$\Delta_\phi$
\form#231:$\Gamma \models_T \Delta_\phi$
\form#232:$D_\phi$
\form#233:\[\frac{\Gamma_1\vdash_2 \phi\quad \Gamma_2\vdash_2 D_{\phi}} {\Gamma_1,\,\Gamma_2\vdash_3\phi}\]
\form#234:\[\frac{\Gamma_0,\,\alpha_1\,\ldots,\,\alpha_n\vdash_3\phi\quad (\Gamma_i\vdash D_{\alpha_i})_{i\in[1..n]}} {\Gamma_0,\,\Gamma_1, \ldots, \Gamma_n\vdash_3 (\bigwedge_{i=1}^n\alpha_i)\to\phi}\]
\form#235:$\alpha_1\ldots\alpha_n$
\form#236:$D_{\alpha_1}\ldots D_{\alpha_n}$
\form#237:\[\frac{}{a\vdash a}\]
\form#238:\[\frac{}{a = a}\quad or \quad\frac{}{a \Leftrightarrow a}\]
\form#239:\[\frac{a_1=a_2}{a_2=a_1}\]
\form#240:\[\frac{}{(a_1=a_2)\Leftrightarrow (a_2=a_1)}\]
\form#241:\[\frac{a_1=a_2\quad a_2=a_3}{a_1=a_3}\]
\form#242:\[\frac{(c_1=d_1)\wedge\ldots\wedge(c_n=d_n)} {op(c_1,\ldots,c_n)=op(d_1,\ldots,d_n)}\]
\form#243:$c_i\not=d_i$
\form#244:$op(c_1,\ldots,c_n)$
\form#245:$c_i=d_i$
\form#246:\[\frac{\Gamma_1\vdash e\quad\Gamma_2\vdash \neg e} {\Gamma_1\cup\Gamma_2\vdash \mathrm{FALSE}} \]
\form#247:\[\frac{\Gamma\vdash e}{\Gamma\vdash e\Leftrightarrow\mathrm{TRUE}}\]
\form#248:\[\frac{\Gamma\vdash e}{\Gamma\vdash\neg e\Leftrightarrow\mathrm{FALSE}}\]
\form#249:\[\frac{\Gamma\vdash e\Leftrightarrow\mathrm{TRUE}}{\Gamma\vdash e}\]
\form#250:\[\frac{\Gamma\vdash e\Leftrightarrow\mathrm{FALSE}}{\Gamma\vdash\neg e}\]
\form#251:\[\frac{\Gamma\vdash e_1\Leftrightarrow e_2} {\Gamma\vdash\sim e_1\Leftrightarrow\sim e_2}\]
\form#252:\[\frac{\Gamma\vdash\neg\neg e}{\Gamma\vdash e}\]
\form#253:\[\frac{\Gamma_1\vdash e_1\quad \Gamma_2\vdash(e_1\Leftrightarrow e_2)} {\Gamma_1\cup\Gamma_2\vdash e_2} \]
\form#254:\[\frac{\Gamma_1\vdash e_1\quad \Gamma_2\vdash(e_1\Rightarrow e_2)} {\Gamma_1\cup\Gamma_2\vdash e_2} \]
\form#255:\[\frac{\vdash e_1\wedge\cdots\wedge e_n}{\vdash e_i}\]
\form#256:\[\frac{\Gamma_1\vdash e_1\quad \Gamma_2\vdash e_2} {\Gamma_1\cup\Gamma_2\vdash e_1\wedge e_2} \]
\form#257:\[\frac{\Gamma_1\vdash e_1\quad \cdots \quad\Gamma_n\vdash e_n} {\bigcup_{i=1}^n\Gamma_i\vdash \bigwedge_{i=1}^n e_i} \]
\form#258:\[\frac{\Gamma,\,\alpha_1\,\ldots,\,\alpha_n\vdash\phi} {\Gamma\vdash(\bigwedge_{i=1}^n\alpha_i)\to\phi}\]
\form#259:\[\frac{\Gamma\vdash e_1\Rightarrow e_2} {\Gamma\vdash\sim e_2\Rightarrow\sim e_1}\]
\form#260:\[\frac{\vdash\neg e}{\vdash e\Leftrightarrow\mathrm{FALSE}}\]
\form#261:\[\frac{\vdash e_1 XOR e_2}{\vdash e_1\Leftrightarrow(\neg e_2)}\]
\form#262:$\epsilon$
\form#263:$(q, k) = q + k\epsilon$
\form#264:$(q_1, k_1) + (q_2, k_2) \equiv (q_1 + q_2, k_1 + k_2)$
\form#265:$a \times (q, k) \equiv (a \times q, a \times k)$
\form#266:$(q_1, k_1) \leq (q_2, k_2) \equiv (q_1 < q_2) \vee (q_1 = q_2 \wedge k_1 \leq k_2)$
\form#267:$const term_0 term_1 ... term_n$
\form#268:$term_i$
\form#269:$rat leaf$
\form#270:$term_{i+1}$
\form#271:$x_r$
\form#272:$x_s$
\form#273:$a_{rs} \neq 0$
\form#274:\[x_r = \sum_{x_j \in N}{a_{rj}xj}\]
\form#275:\[x_s = \frac{x_r}{a_{rs}} - \sum_{x_j \in N }{\frac{a_{rj}}{a_rs}x_j}\]
\form#276:$x_j$
\form#277:$\sum a_i x_i = y$
\form#278:$x_i = \sum_{x_j \in \mathcal{N}}{a_ij x_j}$
\form#279:$\mathcal{N}^+ = \left\lbrace x_j \in \mathcal{N} \; | \; a_{ij} > 0 \right\rbrace$
\form#280:$\mathcal{N}^- = \left\lbrace x_j \in \mathcal{N} \; | \; a_{ij} < 0\right\rbrace$
\form#281:\[\Gamma = \left\lbrace x_j \leq u_j \; | \; x_j \in \mathcal{N}^+\right\rbrace \cup \left\lbrace l_j \leq x_j \; | \; x_j \in \mathcal{N}^-\right\rbrace \cup \left\lbrace l_i \leq x_i \right\rbrace\]
\form#282:\[\Gamma = \left\lbrace x_j \leq u_j \; | \; x_j \in \mathcal{N}^-\right\rbrace \cup \left\lbrace l_j \leq x_j \; | \; x_j \in \mathcal{N}^+\right\rbrace \cup \left\lbrace x_i \leq u_i \right\rbrace\]
\form#283:$x = q + k \epsilon$
\form#284:\[ \lfloor \beta(x) \rfloor = \left\{ \begin{tabular}{ll} $\lfloor q \rfloor$ & $\mathrm{if\ } q \notin Z$\\ $q$ & $\mathrm{if\ } q \in Z \mathrm{\ and\ } k \geq 0$\\ $q - 1$ & $\mathrm{if\ } q \in Z \mathrm{\ and\ } k < 0$ \end{tabular}\right. \]
\form#285:\[ \lfloor \beta(x) \rfloor = \begin{cases} \lfloor q \rfloor & \text{ if } q \notin Z\\ q & \text{ if } q \in Z \text{ and } k \geq 0\\ q - 1 & \text{ if } q \in Z \text{ and } k < 0 \end{cases} \]
\form#286:$\exists x. t = x$
\form#287:$\exists x. pred(x))$
\form#288:\[\frac{A_1,\ldots,A_n\vdash B} {\vdash\neg A_1\vee\cdots\vee \neg A_n\vee B}\]
\form#289:$ A_1,\ldots,A_n\vdash B$
\form#290:$A_i$
\form#291:$B$
\form#292:$\mathrm{FALSE}$
\form#293:\[\frac{\Gamma, \neg A \vdash\mathrm{FALSE}}{\Gamma \vdash A}\]
\form#294:$\neg A$
\form#295:$\Gamma, \neg A \vdash\mathrm{FALSE}$
\form#296:\[\frac{\Gamma, A \vdash\mathrm{FALSE}}{\Gamma\vdash\neg A}\]
\form#297:$\Gamma, A \vdash\mathrm{FALSE}$
\form#298:\[\frac{\Gamma_1, A\vdash C \quad \Gamma_2, \neg A\vdash C} {\Gamma_1\cup\Gamma_2\vdash C}\]
\form#299:$\Gamma_1, A\vdash C$
\form#300:$\Gamma_2, \neg A\vdash C$
\form#301:\[\frac{\Gamma,A_1,\ldots,A_n\vdash\mathrm{FALSE}} {\Gamma\vdash\neg A_1\vee\cdots\vee \neg A_n}\]
\form#302:$\Gamma,A_1,\ldots,A_n\vdash\mathrm{FALSE}$
\form#303:\[\frac{\Gamma_1\vdash A_1\quad\cdots\quad\Gamma_n\vdash A_n \quad \Gamma', A_1,\ldots,A_n\vdash B} {\bigcup_{i=1}^n\Gamma_i\cup\Gamma'\vdash B}\]
\form#304:$\Gamma_i\vdash A_i$
\form#305:$\Gamma', A_1,\ldots,A_n\vdash B$
\form#306:\[\frac{\Gamma_j\vdash\neg A_j\mbox{ for }j\in[1\ldots n]-\{i\} \quad \Gamma\vdash A_1\vee\cdots\vee A_n} {\bigcup_{j\in[1\ldots n]-\{i\}}\Gamma_j\cup\Gamma\vdash A_i}\]
\form#307:$ \Gamma\vdash A_1\vee\cdots\vee A_n$
\form#308:$\Gamma_j\vdash\neg A_j$
\form#309:\[\frac{\Gamma_j\vdash\neg A_j\mbox{ for }j\in[1\ldots n] \quad \Gamma\vdash A_1\vee\cdots\vee A_n} {\bigcup_{j\in[1\ldots n]}\Gamma_j\cup\Gamma \vdash\mathrm{FALSE}}\]
\form#310:\[\frac{\mathrm{GRAY\_SHADOW}(ax,c,c1,c2)} {ax = c + i - \mathrm{sign}(i)\cdot j(c,i,a) \lor GRAY\_SHADOW(ax, c, i-\mathrm{sign}(i)\cdot (a+j(c,i,a)))}\]
\form#311:\[\frac{\mathsf{int}(a\cdot x)\quad \mathsf{int}(C+\sum_{i=1}^{n}a_{i}\cdot x_{i})} {a\cdot x=C+\sum_{i=1}^{n}a_{i}\cdot x_{i} \quad\equiv\quad x=t_{2}\wedge 0=t_{3}} \]
\form#312:\[\begin{array}{rcl} t_{2} & = & -(C\ \mathbf{mod}\ m+\sum_{i=1}^{n}(a_{i}\ \mathbf{mod}\ m) \cdot x_{i}-m\cdot\sigma(t))\\ & & \\ t_{3} & = & \mathbf{f}(C,m)+\sum_{i=1}^{n}\mathbf{f}(a_{i},m)\cdot x_{i} -a\cdot\sigma(t)\\ & & \\ t & = & (C\ \mathbf{mod}\ m+\sum_{i=1}^{n}(a_{i}\ \mathbf{mod}\ m) \cdot x_{i}+x)/m\\ & & \\ m & = & a+1\\ & & \\ \mathbf{f}(i,m) & = & \left\lfloor \frac{i}{m} +\frac{1}{2}\right\rfloor +i\ \mathbf{mod}\ m\\ & & \\ i\ \mathbf{mod}\ m & = & i-m\left\lfloor\frac{i}{m} +\frac{1}{2}\right\rfloor \end{array} \]
\form#313:\[a\cdot x = C + \sum_{i=1}^n a_i\cdot x_i.\]
\form#314:\[\frac{\Gamma\models ax=t\quad \Gamma'\models\mathsf{int}(x)\quad \{\Gamma_i\models\mathsf{int}(x_i) | x_i\mbox{ is var in }t\}} {\Gamma,\Gamma',\bigcup_i\Gamma_i\models \exists (y:\mathrm{int}).\ x=t_2(y)\wedge 0=t_3(y)} \]
\form#315:\[\begin{array}{rcl} t & = & C+\sum_{i=1}^na_{i}\cdot x_{i}\\ t_{2}(y) & = & -(C\ \mathbf{mod}\ m+\sum_{i=1}^{n}(a_{i}\ \mathbf{mod}\ m) \cdot x_{i}-m\cdot y)\\ & & \\ t_{3}(y) & = & \mathbf{f}(C,m)+\sum_{i=1}^{n}\mathbf{f}(a_{i},m)\cdot x_{i} -a\cdot y\\ & & \\ m & = & a+1\\ & & \\ \mathbf{f}(i,m) & = & \left\lfloor \frac{i}{m} +\frac{1}{2}\right\rfloor +i\ \mathbf{mod}\ m\\ & & \\ i\ \mathbf{mod}\ m & = & i-m\left\lfloor\frac{i}{m} +\frac{1}{2}\right\rfloor \end{array} \]
\form#316:\[ \frac{}{\mathrm{BOOLEXTRACT(x,i)} \iff \mathrm{TRUE}} \]
\form#317:\[ \frac{}{\mathrm{BOOLEXTRACT(x,i)} \iff \mathrm{FALSE}} \]
\form#318:\[ \frac{}{(t_{[m]}@q_{[n]})[i] \iff (q_{[n]})[i]} \]
\form#319:\[ 0 \geq i \geq n-1 \]
\form#320:\[\frac{}{(t_{[m]}@q_{[n]})[i] \iff (t_{[m]})[i-n]} \]
\form#321:\[ n \geq i \geq m+n-1 \]
\form#322:\[ \frac{}{(t_{[n]}[k:j])[i] \iff (t_{[n]})[i+j]} \]
\form#323:\[ 0 \geq j \geq k < n, 0 \geq i < k-j \]
\form#324:\[ \frac{}{(\mathrm{BVPLUS}(n,t,q))[0] \iff t[0] \oplus q[0]} \]
\form#325:\[ 0 < i \leq n-1 \]
\form#326:\[ \frac{}{(\mathrm{BVPLUS}(n,t,q))[i] \iff t[i] \oplus q[i] \oplus c(t,q,i)} \]
\form#327:\[ \frac{}{(\sim t_{[n]})[i] \iff \neg (t_{[n]}[i])} \]
\form#328:\[ e_{[n]} \ll k \]
\form#329:\[\frac{}{(e_{[n]} \ll k)[i] \iff \mathrm{FALSE}} \]
\form#330:\[\frac{}{(e_{[n]} \ll k)[i] \iff e_{[n]}[i]} \]
\form#331:\[x_1 \vee x_2 \vee \ldots \vee x_n = 0\]
\form#332:\[x_1 = 0 \wedge x_2 = 0 \wedge \ldots \wedge x_n = 0\]
\form#333:\[x_1 \wedge x_2 \wedge \ldots \wedge x_n = 1^n\]
\form#334:\[x_1 = 1^n \wedge x_2 = 1^n \wedge \ldots \wedge x_n = 1^n\]
\form#335:\[\frac{e_1 = e_2}{\bigwedge_{i=1}^n (e_{1}[i] \iff e_{2}[i]) } \]
\form#336:\[ e_{1}[i], e{2}[i] \]
\form#337:\[ e_{1}, e_{2} \]
\form#338:\[\frac{e_1 \not = e_2}{\bigwedge_{i=1}^n ((\neg e_{1}[i]) \iff e_{2}[i]) } \]
\form#339:$t1[0] \wedge t2[0]$
\form#340:\[ (t1[i-1] \wedge t2[i-1]) \vee (t1[i-1] \wedge computeCarry(t1,t2,i-1)) \vee (t2[i-1] \wedge computeCarry(t1,t2,i-1)) \]
\form#341:\[\exists s: s = x/y \wedge (y \neq 0 \implies x = y * s + m \wedge 0 <= m < y)\]
\form#342:$(msb(e1)\ pred\ msb(e2)) \vee (msb(e1)=msb(e2) \wedge e1[n-2:0]\ pred\ e2[n-2:0])$