More formally, a symbolic value expression 
is either
Unknown or an arbitrary arithmetic/conditional expression in terms of
constants,
variables, and loop indices. A symbolic map
binds variables 
to
symbolic descriptions of their values 
.
A symbolic map associated with a
region R may be either relative or absolute. In a
relative map, variables within bound values refer to their values on
entry to R; in an absolute map, no bound value may contain a
variable modified within R.
For convenience below, we define an operation 
on
symbolic map 
and symbolic value 
, which yields
Unknown if 
contains a 
not bound in 
,
and otherwise yields 
with every occurrence of a 
bound by 
replaced by the bound value 
.