I am trying to express this in Isabelle

image.png

but

```
"eval_fm M v (Mu X a) = ⋂{S ⊆ (states M). eval_fm M (v(X := S)) a ⊆ S}
```

yields a syntax error. It seems that the subset operator is not allowed on the lefthand side of dot in the set notation.

Does this work for you: `⋂{S. S ⊆ (states M) ∧ eval_fm M (v(X := S)) a ⊆ S}`

?

@Maximilian Schaeffeler Yes, that works! Thank you.

Last updated: Jun 20 2024 at 08:21 UTC