section ‹Vardi Systems› (*<*) theory Vardi imports Probabilistic_Hierarchy begin (*>*) context notes [[bnf_internals]] begin