Re: [mizar] Concatenation of finite sequences

[trybulec@math.uwb.edu.pl]

Hi:

Cytowanie Freek Wiedijk <freek@cs.ru.nl>:

> Sorry, but I don't understand this.  These operations are
> not the same?  So why remove one of them?

Usual arguments on integrity:

We don't want to duplicate theorems. We will get even more if in a 
theorem the both operation are used.

More important, we do not want to press users to decide which one to use.

> If you only want to apply them in the "interesting" case,
> you should add an "assume" at the start of the definition
> that states that the operation needs the last element of
> the first argument to be equal to the first of the last.

The reason that I wrote about this is that a special kind of finite 
sequences is used (cmp. COMPOS_1) let us call them finite seauences 
with full stop.
I mean the case that there is a special symbol that occurs on the end 
of every finite sequence and only on the end. Then to catenate such 
finite sequences we may use '$^', to remove the full stop from the 
first one.

> In that case the question becomes: what notation is to
> be preferred?

Right!

> Another operation is to do "normal" concatenation if the
> two endpoints don't match.  So only remove the duplicate
> one if it's actually duplicate.  That one has the nice
> property that even without assumptions it distributes over
> sequence reversal.  (Neither of the two that you give have
> that property, right?)

Looks interesting.

Regards,
Andrzej