Cheap compare for cyclic terms [injective collation keys]

General
1

Here is a relatively cheap compare for cyclic terms that satisfies the
laws, except lexical order. It is based on the idea to define:

S @<' T :<=> rep(S) @< rep(T)

The only requirement to the function rep is that it is injective,
then the laws, except for lexical order, are automatically satisfied.
The proof are not that difficult in our modern times, where there

are automated proof assistants. Here is an example proof, showing
connectedness of @<' based on connectedness of @<:

/* I am using r for the function rep,
   R for the relation @<' and L for the relation @< */
/* Injectivity */
∀x∀y(r(x)=r(y) → x=y), 

/* Bootstrapping */
∀x∀y(Rxy ↔ Lr(x)r(y)), 

/* Connectedness */
∀x∀y(¬x=y → (Lyx ∨ Lxy))

/* Connectedness */
entails ∀x∀y(¬x=y → Ryx ∨ Rxy)

https://www.umsu.de/trees/#~6x~6y(r(x)=r(y)~5x=y),~6x~6y(Rxy~4Lr(x)r(y)),~6x~6y(~3x=y~5Lyx~2Lxy)

Here is a suggestion:

rep(X, Y-Z) :-
   term_factorized(X, Y, Z),
   numberassoc(Z, 0).

numberassoc([], _).
numberassoc(['$VAR'(N)=_|L], N) :-
   M is N+1, 
   numberassoc(L, M).

And then the comparator:

rep_compare(C, X, Y) :- 
   rep(X, A), rep(Y, B), 
   compare(C, A, B).

Any bugs? It requires that term_factorized/3 is stable and it works
only for terms that don’t have already ‘$VAR’/1 in it. Might need to
use something else, but with ‘$VAR’/1 rep/2 can be easily inspected.