Let be the common-prefix index from the first-divergence lemma for minimal walks. If , the walk to has followed the entire walk to and must make at least one further step, contradicting the assumed equality of lengths. Hence .
The current nodes agree, so put . Then is an initial segment of . It is proper because . Therefore
In particular, each function is injective: equality of two trace sequences would give equal lengths and then contradict this proper-initial-segment conclusion.

Articles by others on the same topic (0)

There are currently no matching articles.