Unbound variable warning when modeling expression evaluation in Tamarin

[Prashant Agrawal]

Hi all,

I am trying to model expression evaluation in Tamarin for a simple expression grammar as follows:

theory TestEvalSimple
begin
functions: v/1, c/1

rule evalConst: [ ] --> [ !Eval(c(e), e) ]
rule evalPair: [ !Eval(e1,m1),!Eval(e2,m2)  ] --> [ !Eval(<e1,e2>, <m1,m2>) ]

rule evalX:     [ ] --> [ !Eval(v('x'), 'm') ]
rule evalExpr:
    [ !Eval(<c('s'),<c('r'), v('x')>>, <'s',<'r','m'>>) ]
    --[ Success() ]->
    [ ]
lemma test: exists-trace
    "Ex #j. Success()@j"

end 

All my expressions are made up of pairing operations over two types of terms: a constant term modelled using the unary function `c', and a variable term modelled using the unary function `v'. The evalX rule gives a particular valuation for variable x. Under this valuation, I want to ascertain that the expression  <c('s'),<c('r'), v('x')>> evaluates to <'s', <'r', 'm'>>.

The lemma "test" passes as expected. My questions are mainly about a warning that says that variable e in rule evalConst is unbounded: 

1. Can I safely ignore this warning if I want this rule to be universally quantified over all expressions e?
2. Do rules with unbound variables incur some performance hit? Is there a way to improve the modelling to avoid this hit?

Thanks for any help.

Prashant