maxl(p(v,0))=0,
maxl(p(v,s(0)))=s(0),
maxl(p(p(v,s(0)),0))=s(0),
maxl(p(p(v,s(0)),s(s(0))))=s(s(0)),
maxl(p(p(v,0),s(s(0))))=s(s(0)),
maxl(p(p(v,0),s(0)))=s(0),
maxl(p(p(v,s(s(s(0)))),s(s(0))))=s(s(s(0)))