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?