| pbc_redex: ∀b. pbc b → pbc (𝗔◗b◖𝗟)
| pbc_after: ∀b1,b2. pbc b1 → pbc b2 → pbc (b1●b2)
.
interpretation
"balance condition (path)"
| pbc_redex: ∀b. pbc b → pbc (𝗔◗b◖𝗟)
| pbc_after: ∀b1,b2. pbc b1 → pbc b2 → pbc (b1●b2)
.
interpretation
"balance condition (path)"