Stream: Beginner Questions

Topic: How to write this set notation


view this post on Zulip 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.

view this post on Zulip 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}?

view this post on Zulip waynee95 (Jun 27 2022 at 22:23):

@Maximilian Schaeffeler Yes, that works! Thank you.


Last updated: Aug 15 2022 at 04:16 UTC