Davide's bang rules


P -{alpha}-> P'
--------------------- bn(alpha) cap fn(P) = nil (trans.bang)
!P -{alpha}-> P' | !P

P -{x-y}-> P'  P-{xy}-> P''
--------------------------- (trans.bang.comm)
!P -{tau}-> (P'|P'')|!P

P -{x-(y)}-> P'  P-{xy}-> P''
-------------------------------- y notin fn(P)  (trans.bang.close)
!P -{tau}-> new y.(P'|P'') | !P



Claim !!P ~ !P


Suppose !!P -{alpha}-> P0.

Case alpha = tau:

  Case (trans.bang.comm):