fun pEF(inner: Formula, dir: DirFormula = DirFormula.True): Formula
Create an exists future formula over past paths with optional dir direction restriction.