What the drawn circuit computes

The intended value of each gate of DescriptiveComplexity.Problems.Cvp.Hardness.Interp, and the two halves of the statement that the circuit computes it.

The building half (this file's first section) walks the chains: each gate's value follows from its inputs', by induction along the order for the two chains and by strong induction on the rank of the stage for the propagation, whose gates at stage s read the propagation gates one stage below. The inverting half is the converse, and it is one induction on the derivation DescriptiveComplexity.GateVal: whatever the circuit derives, it derives for the intended reason, because the wiring lemmas leave a gate no other input to have derived it from.

Only the true rail carries information; the false rail is where the constant 0 and the unfired chains sit, and nothing downstream reads it, so the inverting half states nothing about it.

The intended values

def DescriptiveComplexity.CvpVal.GlVal {A : Type} [FirstOrder.Language.sat.Structure A] [LinearOrder A] (c : A) : Prop

The value of a goal-chain gate: the instance is not Horn, or some clause up to c is a goal clause whose negative literals are all forced.

Equations

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

Reading the values off the stages

Building a derivation

Each gate evaluates to 1 as soon as its intended value holds.

Inverting a derivation

Whatever the circuit derives on the true rail, it derives for the intended reason: the wiring leaves a gate no other input to have derived it from.