Definition [efr-001V]

Let \alpha : TS \leftrightarrows A be a system with interface A, and let P be another arena. A P-valued predicate on \alpha is a lift