- [[]] (forall '': [[]]/)
- [[A]] A(forall '':
[[]]/, [[]]/)
- <, , ...>[[A]]
[[A]]
- |= A forall in St:
[[A]]
- [[Enabled A]] exists
in St: [[A]]
- <, , ...>[[always ]]
forall in Nat: <, , ...>[[]]
- sigma[[ and ]] sigma[[]] and sigma[[]]
- sigma[[not ]] not sigma[[]]
- |= forall sigma
in St^infinity:
sigma[[A]]