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-13