HI,
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})
PROOF
<n>2. \A x \in SomeSet : x \in var => SomeAction(x)
PROOF
<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