The INCLUDES clause allows to regroup in an abstract machine the variables, constants and sets -along with their properties- coming from other abstract machines. Thus, the INCLUDES clause is useful for decomposing a complex abstract machine into several simpler abstract machines, simplifying in this way the proving tasks. Indeed, the proof of a component and its “included” machines is globally simpler than the proof of a not decomposed counterpart. The interpretation of “including” is simple: the variables and constants of the included machine become entities in the including machine, and the included operations become usable “specification chunks”. It is possible to include several different instances of a same abstract machine: in this case, the created instances are abstract instances, not accessible by SEES (see later). When a component M includes an abstract machine N, several possibilities could be considered when writing implementation M_imp, which implements the specification of M. The implementation M_imp can import the abstract machine N: in this way, the variables, sets and constants of the included abstract machine in the implementation will be implemented by the variables, sets and constants of the imported instance. The implementation M_imp could as well not import the abstract machine N. In this case, the concrete sets, variables and constants defined in the abstract machine N would have to be defined in the implementation M_imp, either locally, either creating an instance of another component. The choice of this decomposition is taken by the user; the INCLUDES / IMPORTS link combinations is further developed in this chapter.