Infinite Normal Forms for Non-linear Term Rewriting Systems