All presented properties are showed by automated theorem-prover Prover9.
(There is no special order in the presentation of the theorems.)
ID |
Name |
Lemma |
Duals |
OAT1 |
iteration of tests |
$p^\omega = p\cdot 1^\omega$ |
n/a |
In general, we write
$x,y...$
and
$a,b...$ for
arbitrary semiring elements and
$p,q...$ for tests. If other letters are involved we
adapted the original notation of the authors.