SEG_CONV : conv
STRUCTURE
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
HOL  Kananaskis-13