Hi Stephan.
I'm not sure I follow:
On Friday, February 12, 2016 at 11:30:50 AM UTC+2, Stephan Merz wrote:
the soundness of adding auxiliary variables is ensured by the corresponding introduction rules. For example, a simple history variable may be added using a rule such as
Init /\ [][Next]_v => \EE h : Init /\ h = h0 /\ [][Next /\ h' = f(h,v) /\ v' # v]_<<v,h>>
and the validity of this formula (for arbitrary h0 and f) is proved once and for all.
When you say "arbitrary h0 and f", do you mean for *some* h0 and f (i.e., given h0 and f, this should be proven), or that given a specification, this can be proven for *all* h0 and f (I guess not)? In any event, I can't check this with TLC, right?
In other words, the soundness of auxiliary variables is not checked by TLC but ensured by following syntactic patterns when introducing these variables. There should be a chapter about this in a future version of the Hyperbook.
Do you mean that you have a proof that any mapping is sound if some syntactic patterns are followed? Can we get a sneak-peek at those rules?