The program reads the tree, copies the word of its root into an array, reads the code of the formula into a second array, and lists the nodes of the tree in breadth-first order. It fills a table with a row for every position of the code and a column for every node, from the last position to the first. At a position where a subformula starts, the entry of a node is the value of the subformula at the node: an atom is looked up among the atom codes of the node, a negation or a conjunction is read off the rows of its subformulas, and $∃ y (dist(xᵢ, y) ≤ s ∧ ψ)$ holds if some extension of the node with guard $i$ has a child where $ψ$ holds, read off the row of $ψ$. A second table records where every subformula ends, which locates the second conjunct of a conjunction. This is the recursion of the proof of the evaluation lemma over pairs of a subformula and a node. The answer is the entry of the first position at the root, which is the semantic core $evalNode$, whose correctness is $evalNode_node$. A cell takes time linear in the length of the input, so the time is a polynomial of degree three. Every value is at most a constant times the square of the input length, so word-length exponent $2$ suffices.

The proof is carried out for the notion $Lax185574.Computing.Computes$, and transferred to $Lax185574.Algorithms.Algorithm.Computes$ through $Lax185574Proofs.Interface$.