The nice thing is, which is the only missing property here, is that unification is terminating.

We haven't excluded until now that actually applying rules might actually go on forever.

If you think about it, if you look at this elimination rule, normally when we want to do termination,

we have to be very careful that something gets smaller.

If you look at decomposition, it's completely clear. There are F's above and no F's below, so say the term weight.

If you take the equation system and just weigh it, then the weight gets smaller here.

And the weight also gets smaller here. Unfortunately, this here makes the weight bigger.

Why? Think of A being huge, weight a thousand, and you have, I don't know, 20 X's in E.

You are basically replacing every one of the X's in E, 20 of them, with weight a thousand.

That's not going to be very profitable. Something gets hugely bigger here.

Whenever we're copying and substitution copies a lot, then things get bigger.

So it's not at all clear that this will terminate always.

So rather than just weighing or counting symbols or something like this, which we would kind of normally do,

we have to be a little bit more clever.

And we remember that for the last termination proof, we used a simple counting argument.

Remember, we introduced a measure mu on the tableaus, which was essentially the number of connectives in all non-worked-off formulae.

That was the measure. And that was a measure that went into the natural numbers.

And we know that you can only finitely often go down in natural numbers. That is not going to be enough here.

What we need to do instead is something very fancy schmancy.

We're going to look at the multi-set ordering and the lexicographic ordering.

Who knows about the lexicographic ordering? One, two.

OK, then I should probably say something about it. Who knows about a phone book? Good.

So a phone book is a wondrous thing. You can order any string in a phone book if you know the ordering of the letters.

And in German, that's easy. There are only 27 or 29 or something like that.

And you all know A, B, C, D, E, F, G. You know the ordering.

So if you want to compare two strings,

then in general, you have a joint prefix. The strings are the same initially.

That prefix might be of length zero. So it's always the case that we have a joint prefix.

And then we have a first letter where they differ.

Say we have an R here and a C there. And this one is bigger because the first letter where they differ is bigger.

And we don't care what's behind.

There's only one little problem. What if there is no first letter where they differ?

Then the shorter string wins and is shorter. OK, that's the lexicographic ordering, which is used in phone books.

And everybody knows it. The important thing about it is that you can think of this as a lifting of an ordering from characters to strings.

And strings are made up of characters. And the important thing is if you have an ordering that's terminating on the characters,

then you're getting an ordering that's terminating on the strings.

Or in other words, we can actually go to, we can use that to make a measure into strings or tuples.

And still get a nephirian meaning terminating space. That's not going to be enough.

So we have another lifting, ordering lifting that is well behaved, which is the multi-set ordering.

So a multi-set is just like a set, except that everything can appear multiple times.

OK, a set has the form 1, 2, 3, and it's the same as a set 3, 2, 1.

And a multi-set is something that has the form 1, 2, 3, 3, 3. And it's the same 2, 3, 1, 3, 1, 3, 2. OK?

You can reorder everything, that's fine, but you cannot change the multiplicities.

And you can make something a little bit like the lexicographic or phone book ordering by saying, well, a multi-set is smaller than another multi-set.

If I can replace any element of the bigger multi-set with arbitrarily many smaller elements.

OK, that's a lifting operation from an element ordering to a multi-set, to multi-sets.

And it has the nice property that if the element ordering is terminating, the multi-set ordering is also terminating.

A slight bit of math here.

I think the math was actually done here in Erlangen by, what's her name? Nuta.

Emi, yes. Emi Nuta did these things. So I thought I should probably talk about that here in Erlangen.