Axiomatizing Binding Bigraphs (revised)

Extending Milners work on pure bigraphs, we axiomatize static congruence for binding bigraphs and prove that the theory generated is complete. In doing so, we also define a normal form for binding bigraphs, and prove that the four forms are unique up to certain isomorphisms. Compared with the axioms stated by Milner for pure bigraphs, we have extended the set with 5 axioms concerned with binding; and as our ions have names on both faces, we have two axioms -- handling inner and outer renaming. The remaining axioms are transfered straightforwardly.