Regular cuts in models of bounded arithmetic