Go backward to Quantification over Flexible Variables Go up to Top Go forward to Quantification in TLA

Quantification over Flexible Variables

• "Obvious" definition:
  • sigma[[exists x: F]] <=> exists tau in St^infinity: (sigma =_x tau) and tau[[F]]
  • Not correct since not necessarily invaraint under stuttering!
• Remove stuttering steps:
  • #<s₀, s₁, ...><=>
       if forall n in Nat: s_n = s₀
          then <s₀, s₀, ...>
          else if s₁ = s₀ then #<s₁, s₂, ...>
             else <s₀> o #<s₁, ...>
• TLA = STLA + quantification.
  • Existential quantifier over flexible and rigid variables.
  • All TLA formulas are invariant under stuttering:
    #sigma = #tau => sigma[[F]] = tau[[F]]