4.1.3　Structured Operational Semantics of BATC with Static Localities