True, but I believe that this is equivalent to weak tree(3) -- just ignore the trunks! (However, there may be some slight differences between the two once I use the proper inf-embedding algorithm [for determining uniqueness].)
[edit: To clarify, the trunk on the big tree and the subtree essentially cancel out, because every non-trunk branch has a parent branch. So if we removed trunks from all the trees, nothing would change.]
At this point it can still be cheesed, because e.g. the game incorrectly allows N(L,N(L,L)) to predate N(L,N(N(L,L))), where N is an inner node and L is a leaf. I think the correct inf-embedding allows for embeddings with gaps as long as the order of tree nodes is preserved, but now the game only checks for contiguous subtrees, which is strictly stronger.
The correct embedding checking should be easy to implement, but to check embedding of T into S, each branching node in T will create a possibility of permutation, together with all the backtracking, I guess will blow up the complexity?
