Validation of the structure wire format

A string at a specified universe size has the prescribed length and unary header, and every constant block is one-hot. Relation tables are unrestricted. The tests use natural-number addresses, suitable for polynomial-time loops.

def Complexity.DescriptiveComplexity.IsValidEncoding (V : Vocabulary) (card : ℕ) (bits : List Bool) : Prop

The structure wire format at a specified universe size, including all one-hot blocks.

Equations

• One or more equations did not get rendered due to their size.