Proof of normalization of traced terms

Proposition (Normalization). For any term f there is a normal form g such that f = g.

Proof. An induction on f. The only difficult case is composition. By induction we have (drawing the one-cycle case for simplicity: the multiple-cycle case is dealt with the same way):

We can find permutations p and q such that:
=
and:
: X Y,Z (Y a vector of traceable sorts)
Again, we shall only prove the case where Y is a singleton vector, the more general case follows in the same way.
= = = = = =
So we have normalized the composition. The other cases are simpler.

Back