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 system does not affect the strong normalization property of terms, ensuring their termination behavior remains intact.

Contribution

It introduces 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 straightforward

Strong normalization is maintained with added rules

Abstract

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