SEG_CONV : conv
STRUCTURE
listLib
SYNOPSIS
Computes by inference the result of taking a segment of a list.
DESCRIPTION
For any object language list of the form --`[x0;...x(n-1)]`-- , the result of evaluating 
   SEG_CONV (--`SEG m k [x0;...;x(n-1)]`--)
is the theorem 
   |- SEG m k [x0;...;x(n-1)] = [xk;...;x(m+k-1)]

FAILURE
SEG_CONV tm fails if tm is not in the form described above or the indexes m and k are not in the correct range, i.e., m + k <= n.
EXAMPLE
Evaluating the expression 
   SEG_CONV (--`SEG 2 3[0;1;2;3;4;5]`--);
returns the following theorem 
   |- SEG 2 3[0;1;2;3;4;5] = [3;4]
SEEALSO
FIRSTN_CONV, LASTN_CONV, BUTFIRSTN_CONV, BUTLASTN_CONV, LAST_CONV, BUTLAST_CONV
HOL  Kananaskis-10