es39
 
 
 
 
 
 
                                                       Z'(N(Z))=< p1,rho>          Z(p2)=< p3,rho'>        
                                                         x in dom(rho)              y in dom(rho')
   c = <(lambda(x)x),p1>                                 rho(x) not= ?              rho'(x) not= ?
------------------------------                       ---------------------       --------------------
Z,p1 |- (lambda (x) x) -> c,Z    Z,p1 |- + -> op+,Z   Z',N(Z) |- x -> op+           Z,p2 |- y -> 5,Z
----------------------------------------------------------------------------     --------------------
                       Z,p1 |- ((lambda (x) x) +) -> op+,Z                         Z,p1 |- y -> 5,Z        Z,p1 |- 3 -> 3,Z       |-op op+(5,3) -> 8
                  -------------------------------------------------------------------------------------------------------------------------------------
                                                           Z,p1 |-  ( ((lambda (x) x) +) y 3 ) -> 8,Z
Dove
Z' = Z [N(Z), < p1, rho>]

rho = empty[x,op+]

rho' = empty[y,5][pippo, true]