Re: rewrite rule for expressions inside LAMBDA

[John Rushby <rushby@csl.sri.com>]

Ordinary rewrites don't rewrite under bound variables, but
auto-rewrites do.   So:

them1 :  

  |-------
{1}   FORALL (pi: LTLlib[State].Path):
        (G(LAMBDA (st: State): st`submod_inst`inp)(pi))

Rule? (skosimp)
Skolemizing and flattening,
this simplifies to: 
them1 :  

  |-------
{1}   (G(LAMBDA (st: State): st`submod_inst`inp)(pi!1))

Rule? (auto-rewrite "conninput")
Installing rewrite rule conninput
Installing automatic rewrites from: 
  conninput
this simplifies to: 
them1 :  

  |-------
[1]   (G(LAMBDA (st: State): st`submod_inst`inp)(pi!1))

Rule? (assert)
conninput rewrites st`submod_inst`inp
  to st`mainin
Simplifying, rewriting, and recording with decision procedures,
this simplifies to: 
them1 :  

  |-------
{1}   (G(LAMBDA (st: State): st`mainin)(pi!1))

Rule? 


Note that I had to reverse the direction of conninput:

  conninput : AXIOM (
    FORALL (st: State) :
      st`submod_inst`inp = st`mainin
  )


John Rushby