Recursive function on finite sets – how to prove termination
I am (still) struggling with a recursive function on finite sets. I would like to define a special Cartesian product on a finite set of (finite) sets. A simplified example of what I am trying to achieve is the pcart
function below: