A  
adaptability_cstr [Clock_expression] 
Adaptability constraints:
p_1 on ... <: p_2 on ... and
c_x on p_1' <: c_y on p_2' .

C  
choice_of_number_of_1 [Clock_expression] 
Choice of number of 1s for a set of word variables

clock_type [Clock_type] 
Clock type:
ct ::= 'a  ct on p .

clock_type_variable [Clock_type] 
Clock type varaible:
'a_n .

I  
integer_variable [Clock_expression] 
Variables corresponding to the size (i.e.,
c_n ) and the index of
a 1 (i.e., I_{c_n}(j) ) of a word variable c_n .

iof_and_size_cstrs [Clock_expression] 
Constraints on sizes and indexes of 1s.

L  
linear_cstr [Clock_expression] 
Integer linear constraints.

linear_cstrs [Clock_expression] 
Linear constraint system.

P  
periodic_binary_word [Pbword] 
Ultimately Periodic Binary Words:
p ::= u(v) .

precedence_cstr [Clock_expression] 
Precedence constraint:
c_x on p_x <= c_y on p_y .

precedence_cstrs [Clock_expression] 
Precedence constraint system.

S  
simplified_adaptability_cstr [Clock_expression] 
Simplified adaptability constraint:
c_x on p_x <: c_y on p_y .

simplified_adaptability_cstrs [Clock_expression] 
Simplified adaptability constraint system.

subtype_cstr [Clock_type] 
Subtyping constraint:
'a_x on p_1 on ... <: 'a_y on p_2 on ... .

synchronizability_cstr [Clock_expression] 
Synchronizability constraint:
c_x on p_x >< c_y on p_y .

synchronizability_cstrs [Clock_expression] 
Synchronizability constraint system.

T  
t [Clock_expression.Ordered_integer_var]  
W  
word [Pbword] 
Finite word:
u ::= epsilon  0u  1v .

word_expr [Clock_expression] 
Expression on words:
w ::= c  p  w on w .

word_variable [Clock_expression] 
Unknown word variable:
c_n .
