The expression block is a certificate, and it is required to be a correct one: the encoding says that the arrays describe some valid expression that evaluates to exactly the graph in the first block. Since the two blocks describe the same graph, a statement is not weakened by carrying both — the first block is what makes a sentence $Sat G φ$ refer to a graph, and the second is what makes the input admissible. The arrays determine the expression completely, the vertex names included, so the existential quantifier over expressions ranges over at most one thing: the certificate is data in the word, not a choice made about it.

The vertex-name array is part of the input even though a program evaluating the expression never reads it. Without it the second block would not be a k-expression, only the shape of one, and a reader could not check against the first block what the certificate claims. Its presence costs nothing: it is one number per node, so it only lengthens the input, and a linear bound is linear in that length.

Children are numbered before their parents, so the root is the last node. That is what lets a machine evaluate the expression in a single left-to-right sweep, with no recursion, no stack and no second pass, and it is where a linear bound comes from. It restricts the encoding, not the class of graphs: every rooted tree admits such a numbering — any postorder is one — and one can be produced from an arbitrary numbering by a sort, which this format simply asks the writer of the input to have done. An encoding that accepted arbitrary parent arrays would describe the same graphs at the price of a renumbering pass inside the program.

Cells are read with $List.getD$, which returns $0$ outside the word, exactly as in the compressed sparse row encoding; the length condition pins the expression block down completely, so the default value is never reached at a position the other conditions constrain.