Title: Proving termination of normalization functions for conditional expressions
First published: 1985