Re: [mizar] Concatenation of finite sequences

[trybulec@math.uwb.edu.pl]

Cytowanie Piotr Rudnicki <piotr@cs.ualberta.ca>:

> I am in favour of ^' becasue
>
>   - it was introduced first (by me in a work with Y. Nakamura ;-),
>   - is defined through -cut which is independently useful.

Hi:

The second argument is not very strong, p$^q might be defined as
      p|(len p -' 1)^q
(well, it will be difference in the case of q = {}, but who cares?)
and p ^'q should be defined as
    p^(q/^1)
not by -cut. Still, the definiens of p^'q looks a bit simpler.

If we define the similar opreations for XFinSequences then quite 
natural is to generalize them to T-sequences. But in the case of 
transfinite sequence there is
stronger argument for (the counterpart of) your definition because a 
transfinite sequence have always the first memeber but not necessarily 
the last one. So, the second operation cannot be defined in uniform 
way. We have to do something when the the length of the first argument 
is a limit ordinal.

Regards,
Andrzej