{'fraction_non_alphanumeric': 0.05127691760099662, 'fraction_numerical': 0.009120840007118705, 'mean_word_length': 3.2090823970037454, 'pattern_counts': {'":': 0, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 82, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Satisfaction, Restriction and Amalgamation of Constraints in the Framework of M-Adhesive Categories

Application conditions for rules and constraints for graphs are well-known in the theory of graph transformation and have been extended already to M-adhesive transformation systems. According to the literature we distinguish between two kinds of satisfaction for constraints, called general and initial satisfaction of constraints, where initial satisfaction is defined for constraints over an initial object of the base category. Unfortunately, the standard definition of general satisfaction is not compatible with negation in contrast to initial satisfaction. Based on the well-known restriction of objects along type morphisms, we study in this paper restriction and amalgamation of application conditions and constraints together with their solutions. In our main result, we show compatibility of initial satisfaction for positive constraints with restriction and amalgamation, while general satisfaction fails in general. Our main result is based on the compatibility of composition via pushouts with restriction, which is ensured by the horizontal van Kampen property in addition to the vertical one that is generally satisfied in M-adhesive categories.


Introduction
The framework of M-adhesive categories has been introduced recently [8,3] as a generalization of different kinds of high level replacement systems based on the double pushout (DPO) approach [6]. Prominent examples that fit into the framework of M-adhesive categories are (typed attributed) graphs [6,19] and (high-level) Petri nets [2,10]. In the context of domain specific languages and model transformations based on graph transformation, graph conditions (constraints) are already used extensively for the specification of model constraints and the specification of application conditions of transformation rules. Graph conditions can be nested, may contain Boolean expressions [13,14] and are expressively equivalent to first-order formulas on graphs [4] as shown in [14,20]. We generally use the term "nested condition" whenever we refer to the most general case.
Restriction is a general concept for the definition of views of domain languages and is used for reducing the complexity of a model and for increasing the focus to relevant model element types. A major research challenge in this field is to provide general results that allow for reasoning on properties of the full model (system) by analyzing restricted properties on the views (restrictions) of the model only. Technically, a restriction of a model is given as a pullback along type morphisms. While this construction can be extended directly to restrictions of nested conditions, the satisfaction of the restricted nested conditions is not generally guaranteed for the restricted models, but-as we show in this paper-can be ensured under some sufficient conditions.
According to the literature [14,6], we distinguish between two kinds of satisfaction for nested conditions, called general and initial satisfaction, where initial satisfaction is defined for nested conditions over an initial object of the base category. Intuitively, general satisfaction requires that a property holds for all occurrences of a premise pattern, while initial satisfaction requires this property for at least one occurrence. Unfortunately, the standard definition of general satisfaction is not compatible with the Boolean operators for negation and disjunction, but initial satisfaction is compatible with all Boolean operators (see App. A in [21]). In order to show, in addition, compatibility of initial satisfaction with restriction, we introduce the concept of amalgamation for typed objects, where objects can be amalgamated along their overlapping according to the given type restrictions.
As the main technical result, we show that solutions for nested conditions can be composed and decomposed along an amalgamation of them (Thm. 4.10), if the nested conditions are positive, i.e., they contain neither a negation nor a "for all" expression (universal quantification). Based on this property, we show in our main result (Thm. 5.1), that initial satisfaction of positive nested conditions is compatible with amalgamation based on restrictions that agree on their overlappings. Note in particular that this result does not hold for general satisfaction which we illustrate by a concrete counterexample.
The structure of the paper is as follows. Section 2 reviews the general framework of M-adhesive categories and main concepts for nested conditions and their satisfaction. Thereafter, Sec. 3 presents the restriction of objects and nested conditions along type object morphisms. Section 4 contains the constructions and results concerning the amalgamation of objects and nested conditions and in Sec. 5, we present our main result showing the compatibility of initial satisfaction with amalgamation and restriction. Related work is discussed in Sec. 6. Section 7 concludes the paper and discusses aspects of future work. Appendix A contains the proofs that are not contained in the main part. Additionally, App. A in [21] provides formal details concerning the transformation between both satisfaction relations and, moreover, their compatibility resp. incompatibility with Boolean operators.

General Framework and Concepts
In this section we recall some basic well-known concepts and notions and introduce some new notions that we are using in our approach. Our considerations are based on the framework of M-adhesive categories. An M-adhesive category [8] consists of a category C together with a class M of monomorphisms as defined in Def. 2.1 below. The concept of M-adhesive categories generalizes that of adhesive [17], adhesive HLR [9], and weak adhesive HLR categories [6].
In Sec. 3, Sec. 4 and Sec. 5 we will also need the horizontal VK property, where the VK property is only required for commutative cubes with all horizontal morphisms in M (see [8]), to show the compatibility of object composition and the corresponding restrictions. Note moreover, that an Madhesive category which also satisfies the horizontal VK property is a weak adhesive HLR category [6].
A set of transformation rules over an M-adhesive category according to the DPO approach constitutes an M-adhesive transformation system [8]. For various examples (graphs, Petri nets, etc.) see [6].
In Sec. 3, Sec. 4 and Sec. 5 we are considering M-adhesive categories with effective pushouts. According to [18], the formal definition is as follows.

Definition 2.3 (Effective Pushout).
Given M-morphisms a : B → X, b : C → X in an M-adhesive category (C, M) and let (A, p 1 , p 2 ) be obtained by the pullback of a and b. Then pushout (1) of p 1 and p 2 is called effective, if the unique morphism u : D → X induced by pushout (1) is an M-morphism.
Nested conditions in this paper are defined as application conditions for rules in [13]. Depending on the context in which a nested condition occurs, we use the terms application condition [13] and constraint [6], respectively. Furthermore, we define positive nested conditions to be used in Sec. 3, Sec. 4, and Sec. 5 for our main results.

Definition 2.4 (Nested Condition).
A nested condition ac P over an object P is inductively defined as follows: • true is a nested condition over P.
• For every morphism a : P → C and nested condition ac C over C, ∃ (a, ac C ) is a nested condition over P.
• A nested condition can also be a Boolean formula over nested conditions. This means that also ¬ac P , i∈I ac P,i , and i∈I ac P,i are nested conditions over P for nested conditions ac P , ac P,i (i ∈ I) over P for some index set I.
Furthermore, we distinguish the following concepts: • A nested condition is called application condition in the context of rules and match morphisms.
• A nested condition is called constraint in the context of properties of objects.
• A positive nested condition is built up only by nested conditions of the form true, ∃ (a, ac), i∈I ac P,i and i∈I ac P,i , where I = / 0.
An example for a nested condition and its meaning is given below.
Example 2.5 (Nested Condition). Given the nested condition ac P from Fig. 2 where all morphisms are inclusions. Condition ac P means that the source of every b-edge has a b-self-loop and must be followed by some c-edge such that subsequently, there is a path in the reverse direction visiting the source and target of the first b-edge with precisely one c-edge and one b-edge in an arbitrary order. We denote this nested condition by ac P = ∃ (a 1 ,true) ∧ ∃ (a 2 , ∃ (a 3 ,true) ∨ ∃ (a 4 ,true)).
We are now defining inductively whether a morphism satisfies a nested condition (see [6]).
Definition 2.6 (Satisfaction of Nested Condition). Given a nested condition ac P over P, a morphism p : P → G satisfies ac P (see Fig. 1(a)), written p ac P , if: • ac P = true, or • ac P = ∃ (a, ac C ) with a : P → C and there exists a morphism q : C → G ∈ M such that q • a = p and q ac C , or • ac P = ¬ac P and p ac P , or • ac P = i∈I ac P,i and for all i ∈ I holds p ac P,i , or • ac P = i∈I ac P,i and for some i ∈ I holds p ac P,i .
In the following we distinguish two kinds of satisfaction relations for constraints: General [6] and initial satisfaction [14]. Initial satisfaction is defined for constraints over an initial object of the base category while general satisfaction is considered for constraints over arbitrary objects. Intuitively, while general satisfaction requires that a constraint ac P is satisfied by every M-morphism p : P → G, intial satisfaction requires just the existence of an M-morphism p : P → G which satisfies ac P .  2.7 (General Satisfaction of Constraints). Given a constraint ac P over P. An object G generally satisfies ac P , written G ac P , if ∀ p : P → G ∈ M. p ac P (see Fig. 1(a)). Definition 2.8 (Initial Satisfaction of Constraints). Given a constraint ac I over an initial object I. An object G initially satisfies ac I , written G I ac I , if i G ac I for the initial morphism i G : I → G. Note, that for ac I = ∃ (i P , ac P ) we have G I ac I ⇔ ∃ p : P → G ∈ M. p ac P (see Fig. 1(b)).
This means that the general satisfaction corresponds more to the universal satisfaction of constraints while the initial satisfaction corresponds more to the existential satisfaction.
For positive nested conditions, we define solutions for the satisfaction problem. A solution Q (a tree of morphisms) determines which morphisms are used to fulfill the satisfaction condition. Definition 2.9 (Solution for Satisfaction of Positive Nested Conditions). Given a positive nested condition ac P over P and a morphism p : P → G. Then Q is a solution for p ac P if: • ac P = true and Q = / 0, or • ac P = ∃ (a, ac C ) with a : P → C and Q = (q, Q C ) with M-morphism q : C → G such that q • a = p and Q C is a solution for q ac C (see Fig. 1(a)), or • ac P = i∈I ac P,i and Q = (Q i ) i∈I such that Q i is a solution for p ac P,i for all i ∈ I, or • ac P = i∈I ac P,i and Q = (Q i ) i∈I such that there is j ∈ I with solution Q j for p ac P, j and for all k ∈ I with k = j it holds that Q k = / 0.
The following example demonstrates the general and initial satisfaction of constraints and gives their corresponding solutions.
Example 2.10 (Satisfaction and Solution of Constraints).

General Satisfaction
Consider the graph G A from Fig. 2 below and the constraint ac P from Ex. 2.5. There are two possible M-morphisms p 1 , p 2 : P → G A , where p 1 is an inclusion and p 2 maps b 1 to b 2 with the corresponding node mapping. For both matches p 1 and p 2 , there is a b-self-loop on the image of node 1, a c-edge outgoing from the image of node 2, as well as the corresponding images for edges b 2 and c 2 in C 3 . Thus, G A generally satisfies ac P . A corresponding solution for p 1 ac P is given by Q gen = (Q i ) i∈{1,2} with Q 1 = (q 1 , / 0) and Q 2 = (q 2 , (Q j ) j∈{3,4} ), where Q 3 = (q 3 , / 0), Q 4 = / 0 and q i : C i → G A for i = 1, 2, 3 are inclusions.

Initial Satisfaction
Let ac I = ∃ (i P , ac P ) with i P as depicted in Fig. 2 and ac P from Ex. 2.5. The graph G A initially satisfies ac I since there is p 1 : P → G A ∈ M satisfying ac P as mentioned before. A corresponding solution for i G ac I is given by Q init = (p 1 , Q gen ) with Q gen from the example for general satisfaction.
Remark 2.11. A nested condition is called typed over a given type object, if all nested conditions in every of its nesting levels are also typed over the same type object. Furthermore, matches and corresponding solutions are required to be compatible with this type of object as well.

Restriction Along Type Morphisms
In this section, we present the restriction of objects, morphisms, positive nested conditions and their solutions along type morphisms which are the basis for the amalgamation of nested conditions in Sec. 4.
General Assumption. In this and the following sections, we consider an M-adhesive category (C, M) satisfying the horizontal VK property (see Rem. 2.2) and has effective pushouts (see Def. 2.3).
Definition 3.1 (Restriction along Type Morphism). Given an object G A typed over T G A by t G A : G A → T G A and t : T G B → T G A ∈ M, then T G B is called restriction of T G A , G B is a restriction of G A , and t G B is a restriction of t G A , if (1) is a pullback. Given a : G A → G A , then b is a restriction of a along type morphism t, written b = Restr t (a), if (2) is a pullback.
For positive nested conditions, we can define the restriction recursively as restriction of their components.
Definition 3.2 (Restriction of Positive Nested Conditions). Given a positive nested condition ac P A typed over T G A and let T G B be a restriction of it with t : T G B → T G A ∈ M. Then we define the restriction ac P B = Restr t (ac P A ) over the restriction P B of P A as follows: • The restriction of true is true, • the restriction of ∃ (a, ac C A ) is given by restriction of a and ac C A , i. e., ac P B = ∃ (Restr t (a), Restr t (ac C A )), and • the restriction of a Boolean formula is given by the restrictions of its components, i. e., Restr t (¬ac P A ) = ¬Restr t (ac P A ), Restr t ( i∈I ac P A ,i ) = i∈I Restr t (ac P A ,i ), and Restr t ( i∈I ac P A ,i ) = i∈I Restr t (ac P A ,i ).
Now we extend the restriction construction to solutions of positive nested conditions and show in Fact 3.4 that a restriction of a solution is also a solution for the corresponding restricted constraint.

Definition 3.3 (Restriction of Solutions for Positive Nested Conditions).
Given a positive nested condition ac P A typed over T G A together with a restriction ac P B along t : T G B → T G A . For a morphism p A : P A → G and a solution Q A for p A ac P A , the restriction Q B of Q A along t, written Q B = Restr t (Q A ), is defined inductively as follows: • If Q A is empty then also Q B is empty, are restrictions of q A respectively Q CA , and • if ac P A = i∈I ac P A ,i or ac P A = i∈I ac P A ,i , and Q A = (Q A,i ) i∈I , then Q B = (Q B,i ) i∈I such that Q B,i is a restriction of Q A,i for all i ∈ I.

Amalgamation
The amalgamation of typed objects allows to combine objects of different types provided that they agree on a common subtype. This concept is already known in the context of different types of Petri net processes, such as open net processes [1] and algebraic high-level processes [7], which can be seen as special kinds of typed objects. In this section, we introduce a general definition for the amalgamation of typed objects. Moreover, we extend the concept to the amalgamation of positive nested conditions and their solutions.
As required for amalgamation, we discuss under which conditions morphisms can be composed via a span of restriction morphisms. Two morphisms g B and g C "agree" in a morphism g D , if g D can be constructed as a common restriction and can be used as a composition interface for g B and g C as in Def. 4.1.
We say g B , g C agree in g D , if g D is a restriction of g B and g C , i.e., Restr tg DB (g B ) = g D = Restr tg DC (g C ).
Given pushout (1) below with all morphisms in M and typed objects g B , g C agreeing in g D . A morphism g A : G A → T G A is called amalgamation of g B and g C over g D , written g A = g B + g D g C , if the outer square is a pushout and g B , g C are restrictions of g A .  Composition. Given g B , g C agreeing in g D , then there exists a unique amalgamation g A = g B + g D g C .
Decomposition. Vice versa, given g A : G A → T G A , there are unique restrictions g B , g C , and g D of g A such that g A = g B + g D g C .
Here and in the following, uniqueness means uniqueness up to isomorphism.
Proof. Given g B , g C agreeing in g D , we have that the upper two trapezoids are pullbacks. Now we construct G A as pushout over G B and G C via G D , such that the outer diamond is a pushout. This leads to a unique induced morphism g A : G A → T G A , such that the diagram commutes and via the horizontal VK property we get that the lower two trapezoids are pullbacks and therefore g A = g B + g D g C . Vice versa, we can construct G B , G C , G D as restrictions such that the trapezoids become pullbacks, where g A : G A → T G A and T G A , T G B , T G C , T G D are given such that (1) is a pushout with M-morphisms only. Then the horizontal VK property implies that the outer diamond is a pushout and g A is unique because of the universal property and g A = g B + g D g C .
The uniqueness (up to isomorphism) of the amalgamated composition and decomposition constructions follows from uniqueness of pushouts and pullpacks up to isomorphism.  Figure 3 shows a pushout of type graphs T G A , T G B , T G C and T G D .
Composition. Consider the typed graphs G B , G C and G D typed over T G B , T G C and T G D , respectively.
Graph G D , containing the same nodes as G B and G C and no edges, is the common restriction of G B and G C . So, the type morphisms g B and g C agree in g D , which by Fact 4.2 means that there is an amalgamation g A = g B + g D g C . It can be obtained by computing the pushout of G B and G C over G D , leading to the graph G A that contains the b-edges of G B as well as the c-edges of G C . The type morphism g A is induced by the universal property of pushouts, mapping all edges in the same way as g B and g C .
Decomposition. Vice versa, consider the graph G A typed over T G A . We can restrict G A to the type graphs T G B and T G C , leading to typed graphs G B and G C , containing only the b-respectively c-edges of G A . Restricting the graphs G B and G C to type graph T G D , we get in both cases the graph G D that contains no edges, and we have that   (1) below with all morphisms in M. Two positive nested conditions ac P B typed over TG B and ac P C typed over TG C agree in ac P D typed over TG D if ac P D is a restriction of ac P B and ac P C .
Given ac P B and ac P C agreeing in ac P D then a positive nested condition ac P A typed over T G A is called amalgamation of ac P B and ac P C over ac P D , written ac P A = ac P B + ac P D ac P C , if ac P B and ac P C are restrictions of ac P A and t PA = t PB + t PD t PC . In particular, we have true A = true B + true D true C , short true = true + true true.
In the following Fact 4.5, we give a construction for the amalgamation of positive nested conditions and in Thm. 4.10 for the corresponding solutions. Composition. If there are positive nested conditions ac P B and ac P C typed over T G B and T G C , respectively, agreeing in ac P D typed over T G D , then there exists a unique positive nested condition ac P A typed over T G A such that ac P A = ac P B + ac P D ac P C .
Decomposition. Vice versa, given a positive nested condition ac P A typed over T G A , there are unique restrictions ac P B , ac P C and ac P D of ac P A such that ac P A = ac P B + ac P D ac P C .
The amalgamated composition and decomposition constructions are unique up to isomorphism.
Remark 4.6. Given an amalgamation ac P A = ac P B + ac P D ac P C of positive nested conditions, we can conclude from the proof of Fact 4.5 (see App. A) that we also have corresponding amalgamations in each level of nesting.    Figure 4 shows a pushout of typed graphs T G A , T G B , T G C and T G D , and four positive nested conditions ac P A , ac P B , ac P C and ac P D typed over T G A , T G B , T G C and T G D , respectively. For simplicity, the figure contains only the type morphisms of the Ps, but there are also corresponding type morphisms for the Cs, mapping all b-edges to b and all c-edges to c. There is ac P A = i∈{1,2} ac C i,A with ac C i,A = ∃ (a i,A ,true) for i = 1, 2, and ac P B , ac P C and ac P D have a similar structure.
Composition. We have that t P D is a common restriction of t P B and t P C , and also that a i,D is a common restriction of a i,B and a i,C for i = 1, 2. Thus, ac P D is a common restriction of ac P B and ac P C which means that ac P B and ac P C agree in ac P D . So by Fact 4.5 there exists an amalgamation ac P A = ac P B + ac P D ac P C , and according to Rem. 4.6 it can be obtained as amalgamation of its components.
This means that we have an amalgamation t P A = t P B + t P D t P C with pushout of the Ps as shown in Fig. 4, as well as amalgamations of the corresponding type morphisms of the Cs, leading to the pushouts depicted in Fig. 4 by dotted arrows for the C 1 s and by dashed arrows for the C 2 s. The morphisms a 1,A and a 2,A are obtained by the universal property of pushouts.
Decomposition. The other way around, considering the condition ac P A , we can construct the restrictions ac P B and ac P C by deleting the c-respectively b-edges. Then, restricting ac P B and ac P C to T G D by deleting all remaining edges, we obtain the same condition ac P D such that ac P A = ac P B + ac P D ac P C . In order to answer the question, under which conditions such amalgamated positive nested conditions are satisfied, we need to define an amalgamation of their solutions. Afterwards, we show in the proof of Thm. 4.10 that a composition of two solutions via an interface leads to a unique amalgamated solution and that a given solution for an amalgamated positive nested condition is the amalgamation of its unique restrictions.  (1) below with all morphisms in M, an amalgamation of typed objects g A = g B + g D g C , and an amalgamation of positive nested conditions ac P A = ac P B + ac P D ac P C with corresponding matches p A = p B + p D p C .
1. Two solutions Q B for p B ac P B and Q C for p C ac P C agree in a solution Q D for p D ac P D , if Q D is a restriction of Q B and Q C .
2. Given solutions Q B for p B ac P B and Q C for p C ac P C agreeing in a solution Q D for p D ac P D , then a solution Q A for p A ac P A is called amalgamation of Q B and Q C over Q D , written Q A = Q B + Q D Q C , if Q B and Q C are restrictions of Q A .
Note that by assumption g A = g B + g D g C in the definition above we already have a pushout over the Gs, and by ac P A = ac P B + ac P D ac P C we also have a pushout over the Ps. Theorem 4.10 (Amalgamation of Solutions for Positive Nested Conditions). Given pushout (1) as in Def. 4.8 with all morphisms in M, an amalgamation of typed objects g A = g B + g D g C , and an amalgamation of positive nested conditions ac P A = ac P B + ac P D ac P C with corresponding matches p A = p B + p D p C .
Composition. Given solutions Q B for p B ac P B and Q C for p C ac P C agreeing in a solution Q D for p D ac P D , then there is a solution Q A for p A ac P A constructed as amalgamation Q A = Q B + Q D Q C .
Decomposition. Given a solution Q A for p A ac P A , then there are solutions Q B , Q C and Q D for p B ac P B , p C ac P C and p D ac P D , respectively, which are constructed as restrictions Q B , Q C and Q D of Q A such that Q A = Q B + Q D Q C . The amalgamated composition and decomposition constructions are unique up to isomorphism. Remark 4.11. From the proof of Thm. 4.10 (see App. A) we can conclude that for a given amalgamation of solutions Q A = Q B + Q D Q C , we also have corresponding amalgamations of its components.

Compatibility of Initial Satisfaction with Restriction and Amalgamation
In this section we present our main result showing compatibility of initial satisfaction with amalgamation (Thm. 5.1) and restriction (Cor. 5.2) which are based on the amalgamation of solutions for positive nested conditions (Thm. 4.10). This main result allows to conclude the satisfaction of a constraint for a composed object from the satisfaction of the corresponding restricted constraints for the component objects. It is valid for initial satisfaction, but not for general satisfaction.

I ac
Decomposition. By Def. 2.8 a solution Q A for G A I ac A is also a solution for i G A ac A , where i G A is the unique morphism i G A : I → G A . Moreover, due to amalgamation g A = g B + g D g C the inner trapezoids in the diagram above are pullbacks. So by closure of M under pullbacks we have that g BA , g CA , g DB , g DC ∈ M which means that they are monomorphisms. Therefore, the outer trapezoids become pullbacks by standard category theory, which means that i G B : I → G B is a restriction of i G A , i G C : I → G C is a restriction of i G A , and i G D : I → G D is a restriction of i G B as well as of i G C . Furthermore, the outer square in the diagram is a pushout, implying that we have an amalgamation i G A = i G B + i G D i G C . Thus, using Thm. 4.10 we obtain solutions Q B for i G B ac B , Q C for i G C ac C and Q D for i G D ac D such that Q A = Q B + Q D Q C , and by Def. Then by Def. 2.8 we have that Q B , Q C and Q D are solutions for i G B ac B , i G C ac C and i G D ac D , respectively. As shown in item 1, there is i G A = i G B + i G D i G C and therefore, since Q B and Q C agree in Q D , by Thm. 4.10 we obtain a solution Q A for i G A ac A such that Q A = Q B + Q D Q C . Finally, Proof. Consider the diagram in Thm. 5.1 with G C = G A , G D = G B , ac C = ac A and ac D = ac B . Then by standard category theory we have that all rectangles in the diagram are pushouts and the trapezoids are pullbacks. Thus, we have g A = g B + g B g A and, analogously, ac A = ac B + ac B ac A with corresponding   Figure 5 shows the amalgamation of typed graphs g A = g B + g D g C from Ex. 4.3 and an amalgamation of positive nested conditions ac A = ac B + ac D ac C . Note that we have ac A = ∃ (i P A , ac P A ) and ac B , ac C and ac D with similar structure, where the amalgamation ac P A = ac P B + ac P D ac P C is presented in Ex. 4.7. First, we explain in detail the amalgamation q 1,A = q 1,B + q 1,D q 1,C . Note that the graphs G A , G B , G C and G D can be considered as type graphs such that e. g. C 1,D is typed over G D by q 1,D . So, since q 1,D is a common restriction of q 1,B and q 1,C , we have that q 1,B and q 1,C agree in q 1,D . This means that there is an amalgamation of typed objects q 1,A = q 1,B + q 1,D q 1,C , where the inclusion q 1,A maps all nodes and edges in the same way as q 1,B and q 1,C . Moreover, for the empty solutions we have an empty solution as amalgamation, and thus, we have amalgamations of solutions Q 1,A = Q 1,B + Q 1,D Q 1,C = (q 1,A , / 0) and Q 2,A = Q 2,B + Q 2,D Q 2,C = / 0. The amalgamation q A = q B + q D q C can be obtained analogously as described for q 1,A , and hence, we ac D as described in the composition case above. From Cor. 5.2, we know that initial satisfaction is compatible with restriction of typed objects and constraints. In contrast, general satisfaction and restriction are not compatible in general. As the following example illustrates, it is possible that a typed object generally satisfies a constraint while the same does not hold for their restrictions.   Figure 6 shows a restriction G B of the typed graph G A and a restriction ac P B of constraint ac P A . There are two possible matches p 1,A , p 2,A : P A → G A ∈ M where p 1,A is an inclusion and p 2,A maps b 1 to b 2 and c 1 to c 2 . Since for each of the matches the graph G A contains the required edges in the inverse direction, both of the matches satisfy ac P A . For p i,A we have q i,A with q i,A • a A = p i,A for i = 1, 2. Thus, we have that G A ac P A .

Def. 2.8 implies that Q A is a solution for G
For the constraint ac P B there is a match p B : P B → G B ∈ M mapping edge b 1 identically and node 3 to node 4. We have that p B ac P B because there is no edge from node 4 to node 2 in G B , which means that G B ac P B . This is due to the fact that there is no match p A : P A → G A ∈ M such that p B is the restriction of p A . Figure 6: Counterexample for restriction of general satisfaction

Related Work
The framework of M-adhesive categories [8] generalizes various kinds of categories for high level replacement systems, e.g. adhesive [17], quasi-adhesive [18], partial VK square adhesive [15], and weak-adhesive categories [6]. Therefore, the results of this paper are applicable to all of them, where the category of typed attributed graphs is a prominent example. The concepts of nested graph conditions [13] and first-order graph formulas [4] are shown to be expressively equivalent in [14] using the translation between first-order logic and predicates on edgelabeled graphs without parallel edges [20].
Multi-view modelling is an important concept in software engineering. Several approaches have been studied and used, e.g. focussing on aspect oriented techniques [12]. In this line, graph transformation (GT) approaches have been extended to support view concepts based on the integration of type graphs. For this purpose, the concept of restriction along type morphisms has been studied and used intensively [11,5] including GT systems using the concept of inheritance and views [5,16]. Instead of restriction of constraints considered in this paper, only more restrictive forward translations of view constraints have been studied in [5] for the case of atomic constraints with general satisfaction leading to a result similar to Thm. 5.1. The notions of initial and general satisfaction for nested conditions can be transformed one into the other [14], but this transformation uses the Boolean operator negation that is not present in positive constraints, for which, however, our main result on the compatibility of restriction and initial satisfaction holds. Moreover, we have shown by counterexample that general satisfaction is not compatible with restriction in general, even if only positive constraints are considered.

Conclusion
Nested application conditions for rules and constraints for graphs and more general models have been studied already in the framework of M-adhesive transformation systems [6,9]. The new contribution of this paper is to study compatibility of satisfaction with restriction and amalgamation. This is important for large typed systems respectively objects, which can be decomposed by restriction and composed by amalgamation. The main result in this paper shows that initial satisfaction of positive constraints is compatible with restriction and amalgamation (Thm. 5.1 and Cor. 5.2). The amalgamation construction is based on the horizontal van Kampen (VK) property, which is required in addition to the vertical VK property of M-adhesive categories. To our best knowledge, this is the most interesting result for Madhesive transformation systems which is based on the horizontal VK property. Note that the main result is not valid for general satisfaction of positive constraints nor for initial satisfaction of general constraints. For future work, it is important to obtain weaker versions of the main result, which are valid for general satisfaction and constraints, respectively.

A Remaining Proofs
In this appendix, we give the proofs for Fact 3.4, Fact 4.5 and Thm. 4.10.

Fact 3.4 (Restriction of Solutions for Positive Nested Conditions).
Given a positive nested condition ac P A and a match p A : P A → G A over T G A with restrictions ac P B = Restr t (ac P A ), p B = Restr t (p A ) along t : T G B → T G A . Then for a solution Q A of p A ac P A there is a solution Q B = Restr t (Q A ) for p B ac P B . Proof.
• For ac P A = true the implication is trivial, because Q A is empty which means that also Q B is empty and thus a solution for p B ac P B is empty, because ac P B is also true.
• For ac P A = ∃ (a, ac C A ) we have that Q A = (q A , Q CA ) such that q A : C A → G A ∈ M with q A • a = p A and Q CA is a solution for q A ac C A . Then by q B = Restr t (q A ) : C B → G B , we have q B ∈ M and we also have t G : G B → G A ∈ M, because t ∈ M (see Fig. 7). So for ac P B = ∃ (b, ac C B ) we have Moreover, the fact that Q CA is a solution for q A ac C A implies that Q CB = Restr t (Q CA ) is a solution for q B ac C B by induction hypothesis and hence the restriction Q B = (q B , Q CB ) of Q A is a solution for p B ac P B .
• Now, for ac P A = i∈I ac P A ,i we have ac P B = i∈I Restr t (ac P A ,i ). By the fact that Q A is a solution for p A ac P A , we have that Q A = (Q A,i ) i∈I such that Q A,i is a solution for p A ac A,i for all i ∈ I. Thus, by induction hypothesis, we have restrictions Q B,i = Restr t (Q A,i ) that are solutions for p B Restr t (ac P A ,i ) for all i ∈ I. Hence, the restriction Q B = (Q B,i ) i∈I of Q A is a solution for p B ac P B .
• Finally, for ac P A = i∈I ac P A ,i we have ac P B = i∈I Restr t (ac P A ,i ). By the fact that Q A is a solution for p A ac P A we have that Q A = (Q A,i ) i∈I such that for one j ∈ I there is a solution Q A, j for p A ac A, j and for all k = j we have that Q A,k = / 0. Thus, by induction hypothesis, the restriction Q B, j of Q A, j is a solution for p B Restr t (ac P A , j ). Hence, we also have that the restriction Q B = (Q B,i ) i∈I is a solution for p B ac P B with Q B,k = / 0 for k = j.  Figure 7: Restriction of solution q A for p A ∃ (a, ac C A ) Composition. If there are positive nested conditions ac P B and ac P C typed over T G B and T G C , respectively, agreeing in ac P D typed over T G D then there exists a unique positive nested condition ac P A typed over T G A such that ac P A = ac P B + ac P D ac P C .
Decomposition. Vice versa, given a positive nested condition ac P A typed over T G A , there are unique restrictions ac P B , ac P C and ac P D of ac P A such that ac P A = ac P B + ac P D ac P C .
The amalgamated composition and decomposition constructions are unique up to isomorphism. Proof.
Composition. We perform an induction over the structure of ac P D : • ac P D = true. Then we also have ac P B = true and ac P C = true, and the amalgamation ac P A is trivially given by ac P A = true.
The assumption that ac P B and ac P C agree in ac P D means that ac P D is a restriction of ac P B and ac P C and thus, by Def. 3.2, we have that ac P B = ∃ (b, ac C B ) with b : P B → C B , ac P C = ∃ (c, ac C C ) with c : P C → C C , d is a restriction of b and c, and ac C D is a restriction of ac C B and ac C C . This in turn means that ac C B and ac C C agree in ac C D according to Def. 4.4. So, by induction hypothesis, we obtain an amalgamation ac C A = ac C B + ac C D ac C C , which implies that t CA = t CB + t CD t CC , i. e., diagrams (2)-(5) below are pullbacks. By closure of M under pullbacks, we obtain from tg BA ,tg CA ∈ M that also c BA , c CA ∈ M. Moreover, the fact that d is a restriction of b and c means that (6)+(2) and (7)+(3) are pullbacks, which by pullback decomposition implies that (6) and (7) are pullbacks. Note that b, c and d can be considered as typed over C B , C C and C D , respectively. So, according to Def. 4.1, we obtain that b and c agree in d with respect to the pushout of the Cs, leading to an amalgamation a = b + d c : P A → C A with pullbacks (8) and (9) by Fact 4.2. Hence, ac P A = ∃ (a, ac C A ) is the required amalgamation.
• ac P D = i∈I ac P D ,i .
Since ac P D is a restriction of ac P B and ac P C , they must be of the form ac P B = i∈I ac P B ,i and ac P C = i∈I ac P C ,i . Moreover, since ac P B and ac P C agree in ac P D , we obtain that also ac P B ,i and ac P C ,i agree in ac P D ,i for all i ∈ I. So, by induction hypothesis, there are amalgamations ac P A ,i = ac P B ,i + ac P D ,i ac P C ,i such that ac P B ,i and ac P C ,i are restrictions of ac P A ,i for all i ∈ I. Hence, ac P A = i∈I ac P A ,i is the required amalgamation.
• The remaining case for disjunction works analogously to the case for conjunction.
The uniqueness of the amalgamation follows from the fact that we have an amalgamation in each level of nesting and the amalgamation of typed objects is unique by Fact 4.2.
Decomposition. We do an induction over the structure of ac P A : • ac P A = true. This case is trivial because true = true + true true.
• ac P A = ∃ (a, ac C A ) with a : P A → C A . Then by induction hypothesis, there exist restrictions ac C B , ac C C and ac C D of ac C A such that ac C A = ac C B + ac C D ac C C . Moreover, by Fact 4.2, there are unique restrictions b, c and d of a such that a = b + d c. Hence, we have restrictions ac P B = ∃ (b, ac C B ), ac P C = ∃ (c, ac C C ) and ac P D = ∃ (d, ac C D ) of ac P A , and, as shown for the case of composition before, the fact that ac C A = ac C B + ac C D ac C C and a = b + d c implies that ac P A = ac P B + ac P D ac P C .
• ac P A = i∈I ac P A ,i . Then by induction hypothesis, there exist restrictions ac P B ,i , ac P C ,i and ac P D ,i of ac P A ,i such that ac P A ,i = ac P B ,i + ac P D ,i ac P C ,i for all i ∈ I. Hence, ac P B = i∈I ac P B ,i , ac P C = i∈I ac P C ,i and ac P D = i∈I ac P D ,i are restrictions of ac P A such that ac P A = ac P B + ac P D ac P C .
• Again, the remaining case for disjunction works analogously to the case for conjunction.
The uniqueness of the decomposition follows from the uniqueness of restrictions by pullback construction.
Theorem 4.10 (Amalgamation of Solutions for Positive Nested Conditions). Given pushout (1) as in Def. 4.8 with all morphisms in M, an amalgamation of typed objects g A = g B + g D g C , and an amalgamation of positive nested conditions ac P A = ac P B + ac P D ac P C with corresponding matches p A = p B + p D p C .
Composition. Given solutions Q B for p B ac P B and Q C for p C ac P C agreeing in a solution Q D for p D ac P D , then there is a solution Q A for p A ac P A constructed as amalgamation Q A = Q B + Q D Q C .
Decomposition. Given a solution Q A for p A ac P A , then there are solutions Q B , Q C and Q D for p B ac P B , p C ac P C and p D ac P D , respectively, which are constructed as restrictions Q B , Q C and Q D of Q A such that Q A = Q B + Q D Q C .
The amalgamated composition and decomposition constructions are unique up to isomorphism.

Proof.
Composition. We perform an induction over the structure of ac P A .
• ac P A = true.
Then also ac P B , ac P C , ac P D are true and we have empty solutions Q A , Q B , Q C and Q D . Since the restriction of an empty solution is empty, we have that Q B and Q C are restrictions of Q A .
• ac P A = ∃ (a, ac C A ) with a : P A → C A . By Fact 4.5 (Composition), we have the following diagram, where all rectangles are pushouts and all trapezoids are pullbacks, and all horizontal and vertical morphisms are in M.
Now, we consider solutions Q B = (q B , Q CB ), Q C = (q C , Q CC ) and Q D = (q D , Q CD ) for p B ac P B , p C ac P C and p D ac P D , respectively, such that Q D is a restriction of Q B and Q C . Then we also have that q D is a restriction of q B and q C , and thus Together with the pushout over the Cs, this implies a unique morphism q A : and analogously q A • a • p CA = p A • p CA . Since p BA and p CA are jointly epimorphic, this implies that q A • a = p A . In order to show that q A ∈ M, we consider the following diagram in the left: We have that (6) is a pushout with all morphisms in M and thus also a pullback. Diagrams (7) and (8) are pullbacks by restriction, and (9) is a pullback because q D ∈ M is a monomorphism. Hence, by composition of pullbacks, we obtain that the complete diagram is a pullback along M-morphisms g BA • q B and g CA • q C , which means that the pushout of the Cs is effective (see Def. 2.3), implying that q A ∈ M. It remains to show that q B and q C are restrictions of q A . In the following diagram, we have that (10) and (11) are pullbacks by restrictions, the Cs and the Gs form pushouts (see Rem. 4.9) and all morphisms in (10)-(13) are in M. So, the horizontal as well as the vertical VK property implies that also (12) and (13) are pullbacks, which means that q B and q C are restrictions of q A .
Finally, Q D being a restriction of Q B and Q C means that Q CD is a restriction of Q CB and Q CC by induction hypothesis, this implies a solution Q CA of q A ac C A such that Q CB and Q CC are restrictions of Q CA . Hence, Q A = (q A , Q CA ) is a solution for p A ac A such that Q B and Q C are restrictions of Q A . • ac P A = i∈I ac P A ,i .
We have ac P B = i∈I ac P B ,i , ac P C = i∈I ac P C ,i and ac P D = i∈I ac P D ,i such that for all i ∈ I there is ac P D ,i a restriction of ac P B ,i and ac P C ,i . Moreover, given solutions Q B , Q C and Q D of p B ac P B , p C ac P C and p D ac P D , respectively, we have Q B = (Q B,i ) i∈I , Q C = (Q C,i ) i∈I and Q D = (Q D,i ) i∈I such that for all i ∈ I we have that Q B,i , Q C,i and Q D,i are solutions for p B ac P B ,i , p C ac P C ,i and p D ac P D ,i , respectively, and Q D,i is a restriction of Q B,i and Q C,i . Then, by induction hypothesis, there are solutions Q A,i for p A ac P A ,i for all i ∈ I such that Q B,i and Q C,i are restrictions of Q A,i . Hence, Q A = (Q A,i ) i∈I is the required solution for p A ac P A . • ac P A = i∈I ac P A ,i .
We have ac P B = i∈I ac P B ,i , ac P C = i∈I ac P C ,i and ac P D = i∈I ac P D ,i such that for all i ∈ I there is ac P D ,i a restriction of ac P B ,i and ac P C ,i . Moreover, given solutions Q B , Q C and Q D of p B ac P B , p C ac P C and p D ac P D , respectively. Then we have Q B = (Q B,i ) i∈I , Q C = (Q C,i ) i∈I and Q D = (Q D,i ) i∈I such that for some j B , j C , j D ∈ I we have that Q B, j B , Q C, j C and Q D, j D are solutions for p B ac P B , j B , p C ac P C , j C and p D ac P D , j D , respectively, and for all k B , k C , k D ∈ I with k B = j B , k C = j C and k D = j D we have that Q B,k B , Q C,k C and Q D,k D are empty. Furthermore, Q D,i is a restriction of Q B,i and Q C,i for all i ∈ I . Case 1. Q D, j D = / 0. Then we have Q D, j = / 0 for all j ∈ I. According to Def. 3.3, only the restriction of an empty solution is empty, implying that we also have Q B, j = Q C, j = / 0 for all j ∈ I. Moreover, since Q D, j D is a solution for p D ac P D , j D , we can conclude that ac P D , j D = true, and by the fact that ac P D , j D is a restriction of ac P A , j D , ac P B , j D and ac P C , j D it follows that also ac P A , j D = true, ac P B , j D = true and ac P C , j D = true. So, as shown above, there is a solution Q A, j D = / 0 for p A ac P A , j D . Hence, Q A = (Q A,i ) i∈I with Q A,i = / 0 for all i ∈ I is a solution for p A ac P A such that Q B and Q C are restrictions of Q A . Case 2. Q D, j D = / 0. Then according to Def. 3.3, there are also Q B, j D = / 0 and Q C, j D = / 0 which means that j B = j C = j D . So, by induction hypothesis, there is a solution Q A, j D for p A ac P A , j D such that Q B, j D and Q C, j D are restrictions of Q A, j D . Hence, Q A = (Q A,i ) i∈I with Q A,k = / 0 for all k ∈ I with k = j D is a solution for p A ac P A , and we have that Q B and Q C are restrictions of Q A .
In the first case (ac P A = true), the uniqueness of the amalgamation follows from the fact that an empty solution can only be the restriction of another empty solution. In the second case (ac P A = ∃ (a, ac C A )), the uniqueness of Q A = (q A , Q CA ) follows from the uniqueness of q A by universal pushout property, and by uniqueness of Q CA by induction hypothesis. Finally, in the cases of conjunction and disjunction, the uniqueness of the solution follows from uniqueness of its components by induction hypothesis.
Decomposition. Again, we perform an induction over the structure of ac P A .
• ac P A = true.
Then we also have that ac P B , ac P C and ac P D are true. Moreover, we have that Q A is empty, leading to empty restrictions Q B , Q C and Q D that are solutions for p B ac P B , p C ac P C and p D ac P D , respectively. • ac P A = ∃ (a, ac C A ) with a : P A → C A .
Then we have ac P B = ∃ (b, ac C B ), ac P C = ∃ (c, ac C C ) and ac P D = ∃ (d, ac C D ). By amalgamation g A = g B + g D g C , we have pullbacks (2)-(5) below. Moreover, by restrictions ac P B , ac P C and ac P D of ac P A , we have restrictions b, c and d of a, implying pullbacks (6)- (9) below. According to Rem. 4.6, we have an amalgamation of positive nested conditions ac C A = ac C B + ac C D ac C C , which implies an amalgamation of typed objects t CA = t CB + t CD t CC by Def. 4.4.