Commit dfb96891 by Ulrich

### minor

parent db0dd28e
 ... ... @@ -303,10 +303,10 @@ $A^{glv} := \dneg A$ {\centering \displaystyle \begin{aligned} & \text{A is a pre-envelope} && \text{iff} &&& \forall Z, \KIbox \oplus Z \vdash \dneg sub_\dneg(A) \rightarrow A^{kol} \\ & \text{A is a post-envelope}&& \text{iff} &&& \forall Z, \KIbox \oplus Z \vdash A^{kol} \rightarrow \dneg sub_\dneg(A) \\ & \text{A is a\dneg$-envelope} && \text{iff} &&& \forall Z, \KIbox \oplus Z \vdash A^{kol} \leftrightarrow \dneg sub_\dneg(A) \\ & \text{Z is a Kuroda-envelope} && \text{iff} &&& \forall A, \KIbox \oplus Z \vdash A^{kol} \leftrightarrow \dneg sub_\dneg(A) & \text{A is a pre-envelope} && \text{iff} &&& \forall Z, \KIbox \oplus Z \vdash \dneg sub_\dneg(A) \rightarrow A^{t} \\ & \text{A is a post-envelope}&& \text{iff} &&& \forall Z, \KIbox \oplus Z \vdash A^{t} \rightarrow \dneg sub_\dneg(A) \\ & \text{A is a$\dneg-envelope} && \text{iff} &&& \forall Z, \KIbox \oplus Z \vdash A^{t} \leftrightarrow \dneg sub_\dneg(A) \\ & \text{Z is a Kuroda-envelope} && \text{iff} &&& \forall A, \KIbox \oplus Z \vdash A^{t} \leftrightarrow \dneg sub_\dneg(A) \end{aligned} \par } \end{definition} ... ...
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment