I am currently trying to find a proof for strong normalisation of an extention of $\lambda$-calculus. I've tried several approaches and one would be to assign an ordinal number $\operatorname{cs}(t)$ to each term $t$ in the caculus, and then show that this assigned ordinal number does at least not increase under any reduction and is reduced in certaint cases. Then one could conclude that these certaint cases can only occur a finite number of times in each reduction chain.

Is there a proof of strong normalisation for any calculus which uses ordinal numbers in this way?

I am currently trying to find a proof for strong normalisation of an extension of $\lambda$-calculus. I've tried several approaches and one would be to assign an ordinal number $\operatorname{cs}(t)$ to each term $t$ in the calculus, and then show that this assigned ordinal number at least does not increase under any reduction and is reduced in certain cases. Then one could conclude that these certain cases can only occur a finite number of times in each reduction chain.

Is there a proof of strong normalisation for any calculus which uses ordinal numbers in this way?