A short proof that adding some permutation rules to beta preserves SN

TL;DR

This paper proves that adding certain permutation rules to the beta reduction in lambda calculus does not affect the strong normalization property of terms that are already strongly normalizing under beta.

Contribution

It provides a short proof demonstrating that specific permutation rules preserve strong normalization in lambda calculus.

Findings

Permutation rules do not break strong normalization.

The proof is concise and applicable to certain lambda calculus extensions.

Strong normalization is maintained with added permutation rules.

Abstract

I show that, if a term is $SN$ for $\beta$, it remains $SN$ when some permutation rules are added.