Axiomatizing Binding Bigraphs

Extending the result for pure bigraphs given in [Mil04], we axiomatize static congruence for binding bigraphs as described in [Chapter 11, HM04], 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.