A propositional formula is finite mathematical data: an atom has a natural number as its name, a negation has one subformula, and a conjunction has two. The example below represents this syntax directly, without evaluating the formula or attaching information about its truth or satisfiability.

The single $derive_certified_encoding$ command generates $formulaRaw$, its complete constructor equations $formulaRaw.Laws$, and their checked witness $formulaRaw.certified$. Atoms retain their natural indices; negation and conjunction retain their constructor names and recursively encoded children.

For the sample formula $p_0 \land \neg p_1$, the structural description is $conj(atom(0), neg(atom(1)))$, expressed using the fixed $Raw.constructor$ vocabulary. $sampleInput$ then gives its distinguished word-arena input: the root address followed by the three-word blocks for the structural nodes. The same two-stage construction applies to other supported finite datatypes.