[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[tlaplus] Using the primed variables in proofs

   I was wondering if there is a smart way to use the primed variables in the proofs in order to use them for implication chaining.

   For example: 

        Let us assume we have a variable var.
                                                            var = {} initially
   If we have two rules F == \E x \in SomeSet : (var' = var \cup {x}) 
                            and  G == \A x \in SomeSet : x \in var => SomeAction(x)   

   What should be the approach to prove SomeAction(x) using these two rules? 

   <n>1. \E x \in SomeSet : (var' = var \cup {x})

   <n>2. \A x \in SomeSet : x \in var => SomeAction(x)      

    <n>3. \E x \in SomeSet : x \in var 
             ** Is there any inherent property of the primed variables that can be used to prove this from step <n>1? **

     <n>4. \E x \in SomeSet : SomeAction(x)
              BY <n>2, <n>3           

  Basically, the essence of my question is - since var' represents the new state of var, can we use this new state to prove something that depends on the current state? Doesn't the new state implicitly become the current state once it is updated?

Thank you

You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/21faa3af-ecde-490a-b824-246ceea7bc07%40googlegroups.com.