What is the complexity of the equivalence problem for read-once decision trees? A read-once decision tree is defined as follows:

$True$ and $False$ are read-once decision trees.
If $A$ and $B$ are read-once decision trees and
$x$ is a variable not occurring in $A$ and $B$,
then $(x \land A) \lor (\bar x \land B)$ is also a read-once decision tree.

What is the complexity of the equivalence problem for read-once decision trees?

Input: Two read-once decision trees $A$ and $B$.
Output: Is $A \equiv B$?


Motivation:
This problem came up while I was looking at
the proof equivalence problem (permutation of rules) of
a fragment of Linear Logic.
I found a partial solution. The problem is in L.

The negation of $A \leftrightarrow B$ is equivalent to $(\bar A \land B) \lor (A \land \bar{B})$ which is equivalent to $False$ iff both $(\bar A \land B)$ and $(A \land \bar{B})$ are.

The read-once decision tree for $\bar{A}$ can be obtained from the read-once decision tree for $A$ by switching $True$ and $False$ in $A$.
This can be done in log space.

To check if $\bar A \land B$ is equivlent to $False$ 
(and similarly for ${A} \land \bar{B}$)
we run through all the pairs of $True$ leaves, one from each tree, 
and check if they are compatible (that is there is no $x$ on one of the paths and $\bar x$ on the other). It is equivalent to $False$ iff we find no compatible pair.
This can be done in log space.

So the problem is at least in L. 



EDIT: I have some ideas to prove this to be L-complete, under $AC_0$ reduction probably. But I'd need to check the details and it won't fit in here. I'll post a link to the article I am writing if it all works out!



EDIT2: there it is, http://iml.univ-mrs.fr/~bagnol/drafts/mall_bdd.pdf

So the problem is indeed Logspace-complete.