expected

totality013a.idr:5:3-49:
  |
5 |   foo order x xs y ys _ = mtot order (x :: xs) ys
  |   ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Main.foo is possibly not total due to recursive path Main.foo --> Main.mtot --> Main.mtot --> Main.mtot

totality013a.idr:9:3-36:
  |
9 |   mtot order []      right   = right
  |   ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Main.mtot is possibly not total due to: Main.foo