Abstract
Binary multirelations associate elements of a set with its subsets; hence
they are binary relations from a set to its power set. Applications include
alternating automata, models and logics for games, program semantics with
dual demonic and angelic nondeterministic choices and concurrent dynamic
logics. This proof document supports an arXiv article that formalises the
basic algebra of multirelations and proposes axiom systems for them,
ranging from weak bi-monoids to weak bi-quantales.