Are these BDDs the same?

This is exercise 7.1.4-12 in TAoCP. It is easy, but somehow I liked the solution.

A BDD (binary decision diagram) is a data structure that encodes boolean functions. Each node has a variable and two children, low and high. To make it concrete, let's pick a C-language structure.

struct dd_node {
  int V; // variable, at least 1 and at most N
  int L, H; // indexes in nodes
};
struct dd_node nodes[nodes_size];

A valid BDD representation obeys a few constraints.

1. nodes[k].L!=nodes[k].H for k≥2
2. nodes[k].L==nodes[k].H==k for k<2
3. nodes[nodes[k].X].V>nodes[k].V for k≥2 and X either L or R
4. nodes[k]==nodes[kk] implies k==kk
5. For all 2≤k<nodes_size there is a kk such that nodes[kk].L==k || nodes[kk].R==k.

Each such node basically encodes a (!v?l:h) expression. For example, if value[V] is the value of variable V then the represented boolean function is evaluated by eval(value, nodes_size-1).

int eval(int* value, int k) {
  if (k < 2) return k;
  return !value[nodes[k].V]? eval(value, nodes[k].L) : eval(value, nodes[k].H);
}

Here comes the problem. Suppose you are given two BDDs, nodes1 of size s1 and nodes2 of size s2. Design an algorithm to decide if they represent the same boolean function. And, by the way, do not use a stack, not even the call stack.