In Maude, a module can be imported as a submodule of another in three different modes: protecting, extending, including. This is done with the syntax declarations protecting ⟨ModuleExpression⟩ .
extending ⟨ModuleExpression⟩ .
including ⟨ModuleExpression⟩ . which can be abbreviated, respectively, to pr ⟨ModuleExpression⟩ .
ex ⟨ModuleExpression⟩ .
inc ⟨ModuleExpression⟩ . The different modes of importation can be understood as promises by the user, which would need to be proved by him/herself. Before explaining each difference, I clarify no junk and no confusion. No junk is that extra values should not be added. No confusion is that different values should not be made equal.