@ThomasKlimpel I think I’m getting you, if a term is of the form $$f t_1 t_2 \cdots t_n$$ then it can be considered a stack and popping the items from starting (that is from $f$) would lead to a unique parsing. Did I get you the way you wanted me ?

@ConGovDeIn Maybe you got me, but that is not important. The important part is that it should be obvious for you yourself. I tried to clarify that it is extremely simple, and initially overlooked that it is only "extremely" simple when parsing backwards. Then the terms $$t_1 t_2 \cdots t_n$$ are on the stack (as "correctly grouped terms") when $f$ is encountered, so $f$ can just pop of the expected number of items (=terms) from the stack.

Then it pushed itself onto the stack as a new term. Similar each variable of constant just pushes itself onto the stack as a (new) term.

@ThomasKlimpel Okay. I'm getting it, quite.

Yes, I have got it. "$f$ can just pop off the expected number of items from the stack" it will pop off according to its arity.

@ThomasKlimpel Having known this, how do we proceed on proving? I mean what would be the idea of proving? By contradiction?

Yes, in the sense that you assume that you are given two terms, and that you show their are identical iff they generate the same stream of symbols.

Then you start at their back and conclude that each subterm must have been identical, if the stream of symbols was the same.

@ThomasKlimpel I'm quite confused here, first we assume that the stream of symbols are different, then we move on proving that each symbol matches the other symbol of two streams because two streams are same.

No, the stream of symbols are identical. What may be different are the terms.

Or better say string of symbols instead of stream of symbols, because we want to start parsing the string from the end, i.e. backwards.

oh! you mean when collection of $f'$ and $t'_i$ are taken (in the order we both assume to know) the collection is same as the collection of $f$ and $t_i$, they are just different individually?

@ThomasKlimpel

Yes, you assume that they are different individually, and derive a contradiction (i.e. that they are actually identical). The string of symbols on the other hand is just assumed to be given.

(or assume that the $f$ and $t_i$ generated the string of symbols, and then show that $f'$ and $t'_i$ must be identical to $f$ and $t_i$, if they generate the same string of symbols.)

Yes, this is rigorous. However, we want to start at the end, so we would say instead that their final symbols must be same.

Did you mean $t_n$ and $t'_n$?

yes

On the other hand, if I start at the end, I just can conclude that the last (sub)term is identical, but I have no idea how deep inside $t_n$ and $t'_n$ this subterm is burried.

But parsing from the end still seems easier to me, because we can conclude inductively that the stack of subterms are identical.

Okay, we can go like that. But how do we say that $t_n$ and $t'_n$ are same?

"The end terms of same strings must be the same" ?

We say it that when $f$ is encountered, then both stacks (of subterms) are the same, and hence all the terms $t_1 t_2 \cdots t_n$ that get popped from the stack are the same.

So the induction hypothesis is that before encountering $f$ both stacks were the same, and then we encounter $f$, pop the n subterms from the stack, and then push the new subterm on the stack, and hence both stacks are the same again after the induction step.

@ThomasKlimpel Well, I cannot help saying that it is awesome and very digestible.

But it doesn’t feel like the induction I have used before :-)

Yes, I am thinking at the moment about this, i.e. how your initial induction can be made rigorous.

Yours was really something for which the word “awesome” and “brilliant” are made for.

(actually, the two lists have length $n$, i.e. I made a minor mistake)

But we want to look at the substrings $t_1$ and $t'_1$, and it is allowed that they have different length. So the induction hypothesis should only be with respect to the length of the (potentially) shorter string. And it has to be for lists of terms (lists of same length). In the end it probably works, but I find it somewhat hard to follow.

Okay, so hypothesis would be that $t_i$ and $t’_i$ have same lengths?

Can the hypothesis be “t1 and t’1 are uniquely defined” ?

But it won’t help in proof, I reckon.

Well, the hypothesis would be much more complicated than that. It would be that for lists (of same length) of terms such that the shorter resulting string of symbol is shorter than our induction length N (and an initial segment of the other resulting string of symbols), then the two lists of terms will be identical.

What is meant by induction length N?

N is the length of the string of symbols, or more precisely the length of the shorter string of symbols.

I’m trying to understand your last reasoning.

Sorry, if I’m quite slow.

Oh, I cannot clearly follow that reasoning myself too. The induction hypothesis just comes from what is there, and what we "decrease" in the induction step. But it raises a bit the question about the induction start. Should we start with strings of length $\leq n$, where $n$ is the length of the list of terms? What is clear that we need a separate start of induction for each required $n$ (i.e. the $n$s occuring in the signature). Starting at $N\leq n$ at least works. But it feels complicated.