ID | Name | Lemma | Duals |
LIS1 | join splitting | $x+y \leq z \Leftrightarrow x \leq z \wedge y\leq z$ | n/a |
LIS2 | weak form of right distributivity | $y+z \leq w \Rightarrow x\cdot y + x\cdot z \leq x\cdot w$ | n/a |
LIS3 | non-termination is equivalent to absence of terminating elements | $(\forall y (x\cdot y = x)) \Leftrightarrow x\cdot 0 = x$ | n/a |
LIS4 | equivalence between |N| = 1 and multiplication is right-strict | $(\forall y (y\cdot 0 = 0)) \Leftrightarrow (\forall x ((\forall y (x\cdot y = x)) \Rightarrow x = 0))$ | n/a |
LIS5 | equivalence between |N| = 1 and $\top \cdot 0 = 0$ | $(\forall x ((\forall y (x\cdot y = x)) \Rightarrow x= 0)) \Leftrightarrow \top\cdot 0 = 0$ | n/a |
LIS6 | equivalence of $\top;0 = 0$ and multiplication is right-strict | $\top\cdot 0 = 0 \Leftrightarrow \forall x (x\cdot0 \leq 0)$ | n/a |
LIS7 | towards upward closedness of the set N | $(\forall y (x\cdot y = x) \wedge x \leq z) \Rightarrow x\cdot 0 \leq z\cdot 0$ | n/a |
LIS8 | finite computations are closed unter choice (set theoretic) | $(x\cdot 0 = 0 \wedge y\cdot 0 = 0) \Rightarrow (x + y)\cdot 0 = 0$ | n/a |
LIS9 | terminating computations are closed under choice | $x\cdot 0=0 \wedge x\neq 0 \wedge y\cdot 0=0 \wedge y\neq 0 -> (x+y)\cdot 0 = 0 \wedge x+y\neq 0$ | n/a |
LIS10 | finite computations areclosed under composition | $x\cdot 0 = 0 \wedge y\cdot 0 = 0 \Rightarrow (x\cdot y)\cdot 0 = 0$ | n/a |
LIS11 | zero the only finite and infinite element | $(\forall y (x\cdot y = x)) \wedge (x\cdot 0 = 0) \Rightarrow x = 0$ | n/a |
LIS12 | splitting I | $x\cdot y = \inf(x) + \fin(x)\cdot y$ | n/a |
LIS13 | lazy-additivity of multiplication | $\inf(x\cdot y) = \inf(x) + \fin(x)\cdot \inf(y)$ | n/a |
LIS14 | fin-splitting w.r.t. multiplication | $\fin(x\cdot y) = \fin(\fin(x)\cdot y)$ | n/a |
LIS15 | semi-additivity of multiplication | $\fin(x) \cdot \fin(y) \leq \fin(x \cdot y)$ $\fin(x) \cdot \fin(y) \leq \fin(\fin(x) \cdot y)$ |
n/a |
LIS16 | if f,g weakly partition K then f is a kernel operation | $f(x)\leq x$ $f(x)=f(f(x))$ |
n/a |
LIS17 | TBD | $x = f(x) \Leftrightarrow g(x) = 0$ | n/a |
LIS18 | if f,g strongly partition thsn g-parts of elements are ignored by f | $f(g(x)+y) = f(y)$ | n/a |
LIS19 | if f,g strongly partition K then f is uniquely defined by g | $y=g(y) + x \wedge x = f(x) \Rightarrow x = f(y)$ | n/a |
LIS20 | If there is a least element and f is kernel function then f is strict | $0 \leq x \Rightarrow f(0) = 0$ | n/a |
LIS21 | Kernel functions are closed under addition | $f(f(x) + f(y)) = f(x) + f(y)$ | n/a |
LIS22 | fin and inf are disjoint | $y\leq \fin(x) \wedge y\leq \inf(x) \Rightarrow y=0$ | n/a |
LIS23 | properties of F and N | $1\leq \F$ $\F+\N=\top$ $\F\cdot \F =\F$ $\N = \top\cdot 0$ |
n/a |
LIS24 | if residuals exist then F=0/0 | $\F=0/0$ | n/a |
LIS25 | TBD | $y\leq x \wedge y \leq 0/0 \Leftrightarrow y\leq \fin(x)$ | n/a |
©2007. Peter Höfner |