waynee95 (Jun 27 2022 at 18:25): waynee95 (Jun 27 2022 at 18:25):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.
Maximilian Schaeffeler (Jun 27 2022 at 20:49):Does this work for you: ⋂{S. S ⊆ (states M) ∧ eval_fm M (v(X := S)) a ⊆ S}?
waynee95 (Jun 27 2022 at 22:23):@Maximilian Schaeffeler Yes, that works! Thank you.
Last updated: Apr 19 2024 at 20:15 UTC