[mizar] Concatenation of finite sequences

[trybulec@math.uwb.edu.pl]

Quite often we need to concatenate finite sequences f and g under the 
assumption that the last element of f equals the first element of g and 
we do not want it to be repeated. Let f = (x_1, .. x_m), g = (x_m,..., 
x_n) then the result should be
      (x_1, ..., x_n)

In MML two such functors had been introduced:

 let p,q be FinSequence;
 func p$^q -> FinSequence means
:: REWRITE1:def 1
 it = p^q if p = {} or q = {} otherwise
 ex i being Element of NAT, r being FinSequence st len p = i+1 & r = p|Seg i &
 it = r^q;

and

 let p, q be FinSequence;
 func p ^' q -> FinSequence equals
:: GRAPH_2:def 2
 p^(2, len q)-cut q;

If we neglect the problem of empty sequence (the operation is 
meaningless in such a case anyway) the big difference is that in p $^ q 
the last element of the first sequence is removed and in p ^' q the 
first element of the second one is removed.
In the interesting case (when they coincide) the result is the same. 
So, to keep the integrity of MML we should remove one of the 
definitions. The problem is which one?

What do you think?

Regards,
Andrzej