I have constructed a functor from a monad that appears (based on computer experiments to test the monad laws) to also have monad properties but I am having trouble proving it.

Here is the idea: M[A] is a monad, and Either[A.B] is the usual "or" bifunctor.

Let N[A] = M[Either[A, N[A]]] It's a recursive definition so these M-trees could be finite or infinite. I specify that they are finite only.

Now we can define map, unit and join transformations of the correct type signature

N(f) = M( bimap(f, N(f))) and so on.

I have managed to prove, with brute force techniques, that N is a functor and unit is a natural transformation in the appropriate way. However, I am having difficulty with the laws dealing with the join, because the definitions of map and join are recursive, and so my proofs go around in circles.

Is there a particular mathematical technique for proving a functor is a monad when it is defined recursively?