Terms are expressions built from variables and fundamental operations. Assuming that for each sort we are given a set of variables , we can define recursively the notion of a term of type s:
we are given a set of variables 
, we can define recursively the notion of a
term of type s:
