The expression is input, not something the program computes. Deciding cliquewidth, or approximating it, is a different theorem with a different proof, and folding it in here would silently claim it; the statement is the honest one, "given a graph together with a k-expression for it". This is the same choice a treewidth-based statement makes when it takes a tree decomposition as input.

The order of the quantifiers is the content of the theorem: the sentence and the width bound come first, then the program and the constant, then the graph and the word length. So one program serves all graphs of cliquewidth at most k at every word length, with one constant, but both may depend — and in every known proof do depend, in a way that grows faster than any tower of exponentials in the sentence — on the sentence and the width. Nothing here estimates the constant. This is the opposite ordering from the vertex cover statement of this submission, and it has to be: there the parameter is an entry of the input word, so one program can read it and serve every parameter, while here the sentence is not part of the input at all and a program that has never seen it cannot decide it. Quantifying the program before the word length says the same thing about $w$ as everywhere else in this submission — one program that works at every word length that admits its input, rather than a family of programs, one of which could hide an arbitrary amount of information in its literals.

One constant does both jobs, and the condition it appears in says two things at once. The first is that the running time fits: taking v to be any entry of the word — an instance word is never empty — the condition gives c(|x|+1) ≤ $2 ^ w$, so $2 ^ w$ is at least the number of steps the claim allows, and with it every quantity the program forms out of the length of the word, the number of nodes of the expression and the addresses of the arrays included. The four tables of the dynamic program are also covered, since their sizes depend on the sentence and the width bound alone and are therefore absorbed into c, which is chosen after both.

The second is that the entries themselves fit, and this is why the condition quantifies over them. A machine at word length $w$ sees its input reduced modulo $2 ^ w$, so an entry that is not a word is not the entry it was handed. Most entries of an instance are small: vertex numbers, offsets and node numbers are below the length of the word, and an operation code is below the number of operations at width k, which $c$ covers. But not all of them are, because the format has slots the encoding deliberately leaves free — the parent entry of the root, through which nothing points, and the vertex name at a node whose operation creates no vertex. Those may hold any number whatever, and saying of every entry that it fits is what makes the claim about them honest instead of silently assuming they are small. It is the same bookkeeping the vertex cover statement of this submission does with $c * (|x| + k + 1)$, where the one entry not bounded by the length is the parameter.

The fitting condition is a condition on the admissible inputs and not a hypothesis of the claim, because as a hypothesis it would be empty. A graph with an edge has encodings of every length, since a block may list a neighbour repeatedly, so no word length accommodates all encodings of a fixed graph at once and "if every instance for $G$ and $k$ fits into a word" would never be satisfied. Restricting the inputs instead says what is meant: at every word length, every instance that fits is decided within the bound.

Only encodings of $G$ are admitted as inputs; the program may behave arbitrarily on words that encode nothing, and on words too long for its word length.