Constraints of the Provenance Data Model

1.1 Conventions

The key words "must", "must not", "required", "shall", "shall not", "should", "should not", "recommended", "may", and "optional" in this document are to be interpreted as described in [RFC2119].

In this document, logical formulas contain variables written as lower-case identifiers. Some of these ariables are written beginning with the underscore character _, by convention, to indicate that they (intentionally) appear only once in the formula; thus, the textual variable name is mnemonic only.

1.2 Purpose of this document

The PROV Data Model, PROV-DM, is a conceptual data model for provenance, which is realizable using different serializations such as PROV-N and PROV-O. A PROV instance is a set of PROV statements, possibly including bundles, or named sets of statements. For example, such a PROV instance could be a .provn document, the result of a query, a triple store containing PROV statements in RDF, etc. The PROV-DM specification [PROV-DM] imposes minimal requirements upon PROV instances. A valid PROV instance corresponds to a consistent history of objects and interactions to which logical reasoning can be safely applied. By default, PROV instances need not be valid.

This document specifies inferences over PROV instances that applications may employ, including definitions of some provenance statements in terms of others, and also defines a class of valid PROV instances by specifying constraints that valid PROV instances must satisfy. Applications should produce valid provenance and may reject provenance that is not valid. Applications should also use definitions, inferences and constraints to normalize PROV instances in order to determine whether two such instances convey the same information.

To summarize: compliant applications use definitions, inferences, and uniqueness constraints to normalize PROV instances, and then apply event ordering constraints to determine whether the instance has a consistent event ordering. If so, the instance is valid, and the normal form is considered equivalent to the original instance. Also, any two PROV instances that yield the same normal form are considered equivalent. Further discussion of the semantics of PROV statements, which justifies the inferences and constraints, can be found in the formal semantics [PROV-SEM].

1.3 Structure of this document

Section 2 gives a brief rationale for the definitions, inferences and constraints.

Section 3 summarizes the requirements for compliance with this document, which are specified in detail in the rest of the document.

Section 4 presents inferences and definitions. Definitions allow replacing shorthand notation in [PROV-N] with more explicit and complete statements; inferences allow adding new facts representing implicit knowledge about the structure of provenance.

Section 5 presents three kinds of constraints, uniqueness constraints that prescribe that certain statments must be unique within PROV instances, event ordering constraints that require that the records in a PROV instance are consistent with a sensible ordering of events relating the activities, entities and agents involved, and impossibility constraints that forbid certain patterns of statements in valid PROV instances.

Section 6 defines the notions of validity, equivalence and normalization.

1.4 Audience

The audience for this document is the same as for [PROV-DM]: developers and users who wish to create, process, share or integrate provenance records on the (Semantic) Web. Not all PROV-compliant applications need to perform inferences or check validity when processing provenance. However, applications that create or transform provenance should attempt to produce valid provenance, to make it more useful to other applications by ruling out nonsensical or inconsistent information.

This document assumes familiarity with [PROV-DM] and employs the [PROV-N] notation.

4.1 Optional Identifiers and Attributes

Many PROV relation statements have an identifier, identifying a link between two or more related objects. Identifiers can sometimes be omitted in [PROV-N] notation. For the purpose of inference and validity checking, we generate special identifiers called existential variables denoting the unknown values. Existential variables can be substituted with constant identifiers, literals, the placeholder -, or other existential variables. We note that Definitions 1, 2, and 3 desugar compact PROV-N notation into a normal form.

Likewise, many PROV statements allow for an optional attribute list. If it is omitted, this is the same as specifying an empty attribute list:

Finally, many PROV statements have other optional arguments or short forms that can be used if none of the optional arguments is present. These are handled by specific rules listed below.

Finally, most optional parameters (written -) are, for the purpose of this document, considered to be distinct, fresh existential variables. Thus, before proceeding to apply other definitions or inferences, most occurrences of - must be replaced by fresh existential variables, distinct from any others occurring in the instance. The only exceptions, where - must be left in place, are the activity parameter in wasDerivedFrom and the plan parameter in wasAssociatedWith.

The following table characterizes the expandable parameters of the properties of PROV, needed in the following definition. For emphasis, the two optional parameters that are not expandable are also listed.

4.2 Entities and Activities

Communication between activities is defined as the existence of an underlying entity generated by one activity and used by the other.

The relationship wasInformedBy is not transitive. Indeed, consider the following statements.

wasInformedBy(a2,a1)
wasInformedBy(a3,a2)

We cannot infer wasInformedBy(a3,a1) from these statements. Indeed, from wasInformedBy(a2,a1), we know that there exists e1 such that e1 was generated by a1 and used by a2. Likewise, from wasInformedBy(a3,a2), we know that there exists e2 such that e2 was generated by a2 and used by a3. The following illustration shows a counterexample to transitivity. The horizontal axis represents the event line. We see that e1 was generated after e2 was used. Furthermore, the illustration also shows that a3 completes before a1. So it is impossible for a3 to have used an entity generated by a1. This is illustrated in Figure 1.

Figure 1 ^◊: Counter-example for transitivity of wasInformedBy

From an entity, we can infer that existence of generation and invalidation events.

From an activity statemen,t we can infer that start and end events having times matching the start and end times of the activity.

Start of a by trigger e1 and starter activity a1 implies that e1 was generated by a1.

Likewise, end of a by trigger e1 and ender activity a1 implies that e1 was generated by a1.

4.3 Derivations

Derivations with explicit activity, generation, and usage admit the following inference:

Derivations with an explicit activity and no specified generation and usage admit the following inference:

This inference is justified by the fact that the entity denoted by e2 is generated by at most one activity (see Constraint 27 (unique-generation)). Hence, this activity is also the one referred to by the usage of e1.

A derivation specifying activity, generation and use events is a special case of a derivation that leaves these unspecified. (The converse is not the case).

A revision admits the following inference, stating that the two entities linked by a revision are also alternates.

4.4 Agents

Attribution identifies an agent as responsible for an entity. An agent can only be responsible for an entity if it was associated with an activity that generated the entity. If the activity, generation and association events are not explicit in the instance, they can be inferred.

Delegation relates agents where one agent acts on behalf of another, in the context of some activity. The supervising agent delegates some responsibility for part of the activity to the subordinate agent, while retaining some responsibility for the overall activity. Both agents are associated with this activity.

The wasInfluencedBy relation is implied by other relations, including usage, start, end, generation, invalidation, communication, derivation, attribution, association, and delegation. To capture this explicitly, we allow the following inferences:

4.5 Alternate and Specialized Entities

The relation alternateOf is an equivalence relation: reflexive, transitive and symmetric.

Similarly, specialization is a strict partial order: it is irreflexive and transitive. Irreflexivity is handled later as a constraint.

If one entity specializes another, then they are also alternates:

If one entity specializes another then all attributes of the more general entity are also attributes of the more specific one.

If one entity is a mention of another in a bundle, then the former is also a specialization of the latter:

5.1 Uniqueness Constraints

In the absence of existential variables, uniqueness constraints could be checked directly by checking that no identifier appears more than once for a given statement. However, in the presence of existential variables, we need to be more careful to combine partial information that might be present in multiple compatible statements, due to inferences. Uniqueness constraints are enforced through merging pairs of statements subject to equalities. For example, suppose we have two activity statements activity(a,2011-11-16T16:00:00,t1,[a=1]) and activity(a,t2,2011-11-16T18:00:00,[b=2]). The merge of these two statements (describing the same activity a) is activity(a,2011-11-16T16:00:00,2011-11-16T18:00:00,[a=1,b=2]).

Merging can be applied to a pair of terms, or a pair of attribute lists. The result of merging is either a substitution (mapping existentially quantified variables to terms) or a special symbol undefined indicating that the merge cannot be performed. Merging of pairs of terms, attribute lists, or statements is defined as follows.

• If t and t' are concrete identifiers or values (including the placeholder -), then their merge exists only if they are equal, otherwise merging is undefined.
• If x is an existential variable and t' is any term (identifier, constant, placeholder -, or existential variable), then their merge is t', and the resulting substitution is [x=t']. In the special case where t'=x, the merge is x and the resulting substitution is empty.
• If t is any term (identifier, constant, placeholder -, or existential variable) and x' is an existential variable, then their merge is the same as the merge of x and t.
• The merge of two attribute lists attrs1 and attrs2 is their union, considered as unordered lists, written attrs1 ∪ attrs2.

A typical uniqueness constraint is as follows:

Such a constraint is enforced as follows:

1. Suppose PROV instance I contains all of the hypotheses hyp₁ and ... and hyp_n.
2. Attempt to merge all of the equated terms in the conclusion t₁ = u₁ and ... and t_n = u_n.
3. If merging fails, then the constraint is unsatisfiable, so application of the constraint to I fails.
4. If merging succeeds with a substitution S, then S is applied to the instance I, yielding result I(S).

In the common case that a particular field of a relation uniquely determines the other fields, we call the uniqueness constraint a key constraint. Key constraints are written as follows:

Because of the presence of attributes, key constraints do not reduce directly to uniqueness constraints. Instead, we enforce key constraints as follows.

1. Suppose r(a₀;a₁,...a_n,attrs1) and r(b₀;b₁,...b_n,attrs2) hold in PROV instance I, where the key fields a_k = b_k are equal.
2. Attempt to merge all of the corresponding parameters a₀ = b₀ and ... and a_n = b_n.
3. If merging fails, then the constraint is unsatisfiable, so application of the key constraint to I fails.
4. If merging succeeds with substitution S, then we remove r(a₀;a₁,...a_n,attrs1) and r(b₀;b₁,...b_n,attrs2) from I, obtaining instance I', and return instance {r(S(a₀);S(a₁),...S(a_n),attrs1 ∪ attrs2)} ∪ S(I').

Thus, if a PROV instance contains an apparent violation of a uniqueness constraint or key constraint, merging can be used to determine whether the constraint can be satisfied by instantiating some existential variables with other terms. For key constraints, this is the same as merging pairs of statements whose keys are equal and whose coresponding arguments are compatible, because after merging respective arguments and attribute lists, the two statements become equal and one can be omitted.

We assume that the various identified objects of PROV have unique statements describing them within a PROV instance, through the following key constraints:

Likewise, we assume that the identifiers of relationships in PROV uniquely identify the corresponding statements a PROV instance, through the following key constraints:

5.2 Event Ordering Constraints

Given that provenance consists of a description of past entities and activities, valid provenance instances must satisfy ordering constraints between instantaneous events, which we introduce in this section. For instance, an entity can only be used after it was generated; hence, we say that an entity's generation event precedes any of this entity's usage events. Should this ordering constraint be violated, the associated generation and usage would not be credible. The rest of this section defines the temporal interpretation of provenance instances as a set of instantaneous event ordering constraints.

To allow for minimalistic clock assumptions, like Lamport [CLOCK], PROV relies on a notion of relative ordering of instantaneous events, without using physical clocks. This specification assumes that a preorder exists between instantaneous events.

Specifically, precedes is a preorder between instantaneous events. When we say e1 precedes e2, this means that e1 happened at the same time as or before e2. For symmetry, follows is defined as the inverse of precedes; that is, when we say e1 follows e2, this means that e1 happened at the same time as or after e2. Both relations are preorders, meaning that they are reflexive and transitive. Moreover, we sometimes consider strict forms of these orders: we say e1 strictly precedes e2 to indicate that e1 happened before e2. This is a transitive relation.

PROV also allows for time observations to be inserted in specific provenance statements, for each of the five kinds of instantaneous events introduced in this specification. Times in provenance records arising from different sources might be with respect to different timelines (e.g. different time zones) leading to apparent inconsistencies. For the purpose of checking ordering constraints, the times associated with events are irrelevant; thus, there is no inference that time ordering implies event ordering, or vice versa. However, an application may flag time values that appear inconsistent with the event ordering as possible inconsistencies. When generating provenance, an application should use a consistent timeline for related PROV statements within an instance.

A typical ordering constraint is as follows.

The conclusion of an ordering constraint is either precedes or strictly precedes. To check ordering constraints, we generate all precedes and strictly precedes relationships arising from the ordering constraints to form a directed graph, with edges marked precedes or strictly precedes, and check that there is no cycle containing a strictly precedes edge.

5.2.1 Activity constraints

In this section we discuss constraints from the perspective of the lifetime of an activity. An activity starts, then during its lifetime uses, generates or invalidates entities, and communicates with or starts other activities, and finally ends. The following constraints amount to checking that all of the events associated with an activity take place within the activity's lifetime, and the start and end events mark the start and endpoints of its lifetime.

Figure 2 summarizes the ordering constraints on activities in a graphical manner. For this and subsequent figures, an event time line points to the right. Activities are represented by rectangles, whereas entities are represented by circles. Usage, generation and invalidation are represented by the corresponding edges between entities and activities. The five kinds of instantaneous events are represented by vertical dotted lines (adjacent to the vertical sides of an activity's rectangle, or intersecting usage and generation edges). The ordering constraints are represented by triangles: an occurrence of a triangle between two instantaneous event vertical dotted lines represents that the event denoted by the left line precedes the event denoted by the right line.

Miscellanous suggestions about figures (originally from Tim Lebo):

• I think it would help if the "corresponding edges between entities and activities" where the same visual style as the vertical line marking the time the Usage, generation and derivation occurred. A matching visual style provides a Gestalt that matches the concept. I am looking at subfigures b and c in 5.2.

Figure 2 ^◊: Summary of instantaneous event ordering constraints for activities

---

The existence of an activity implies that the activity start event always precedes the corresponding activity end event. This is illustrated by Figure 2 (a) and expressed by Constraint 34 (start-precedes-end).

Constraint 34 (start-precedes-end)

IF wasStartedBy(start;a,_e1,_a1,_t1,_attrs1) and wasEndedBy(end;a,_e2,_a2,_t2,_attrs2) THEN start precedes end.

---

A usage implies ordering of events, since the usage event had to occur during the associated activity. This is illustrated by Figure 2 (b) and expressed by Constraint 35 (usage-within-activity).

Constraint 35 (usage-within-activity)

1. IF used(use;a,e,_t,_attrs) and wasStartedBy(start;a,_e1,_a1,_t1,_attrs1) THEN start precedes use.
2. IF used(use;a,e,_t,_attrs) and wasEndedBy(end;a,_e1,_a1,_t1,_attrs1) THEN use precedes end.

---

A generation implies ordering of events, since the generation event had to occur during the associated activity. This is illustrated by Figure 2 (c) and expressed by Constraint 36 (generation-within-activity).

Constraint 36 (generation-within-activity)

1. IF wasGeneratedBy(gen;_e,a,_t,_attrs) and wasStartedBy(start;a,_e1,_a1,_t1,_attrs1) THEN start precedes gen.
2. IF wasGeneratedBy(gen;_e,a,_t,_attrs) and wasEndedBy(end;a,_e1,_a1,_t1,_attrs1) THEN gen precedes end.

---

Communication between two activities a1 and a2 also implies ordering of events, since some entity must have been generated by the former and used by the latter, which implies that the start event of a1 cannot follow the end event of a2. This is illustrated by Figure 2 (d) and expressed by Constraint 37 (wasInformedBy-ordering).

Constraint 37 (wasInformedBy-ordering)

IF wasInformedBy(_id;a2,a1,_attrs) and wasStartedBy(start;a1,_e1,_a1',_t1,_attrs1) and wasEndedBy(end;a2,_e2,_a2',_t2,_attrs2) THEN start precedes end.

5.2.2 Entity constraints

The figure(s) in this section should have vertical lines with visual styles that match the diagonal arrow that they go with.

As with activities, entities have lifetimes: they are generated, then can be used, revised, or other entities can be derived from them, and finally they may be invalidated. The constraints on these events are illustrated graphically in Figure 3 and Figure 4.

Figure 3 ^◊: Summary of instantaneous event ordering constraints for entities

---

Generation of an entity precedes its invalidation. (This follows from other constraints if the entity is used, but we state it explicitly to cover the case of an entity that is generated and invalidated without being used.)

Constraint 38 (generation-precedes-invalidation)

IF wasGeneratedBy(gen;e,_a1,_t1,_attrs1) and wasInvalidatedBy(inv;e,_a2,_t2,_attrs2) THEN gen strictly precedes inv.

---

A usage and a generation for a given entity implies ordering of events, since the generation event had to precede the usage event. This is illustrated by Figure 3(a) and expressed by Constraint 39 (generation-precedes-usage).

Constraint 39 (generation-precedes-usage)

IF wasGeneratedBy(gen;e,_a1,_t1,_attrs1) and used(use;_a2,e,_t2,_attrs2) THEN gen precedes use.

---

All usages of an entity precede its invalidation, which is captured by Constraint 40 (usage-precedes-invalidation) (without any explicit graphical representation).

Constraint 40 (usage-precedes-invalidation)

IF used(use;_a1,e,_t1,_attrs1) and wasInvalidatedBy(inv;e,_a2,_t2,_attrs2) THEN use precedes inv.

---

If there is a derivation relationship linking e2 and e1, then this means that the entity e1 had some influence on the entity e2; for this to be possible, some event ordering must be satisfied. First, we consider derivations, where the activity and usage are known. In that case, the usage of e1 has to precede the generation of e2. This is illustrated by Figure 3 (b) and expressed by Constraint 41 (derivation-usage-generation-ordering).

Constraint 41 (derivation-usage-generation-ordering)

IF wasDerivedFrom(_d;_e2,_e1,_a,gen2,use1,_attrs) THEN use1 strictly precedes gen2.

---

When the activity, generation or usage is unknown, a similar constraint exists, except that the constraint refers to its generation event, as illustrated by Figure 3 (c) and expressed by Constraint 42 (derivation-generation-generation-ordering).

Constraint 42 (derivation-generation-generation-ordering)

IF wasDerivedFrom(_d;e2,e1,attrs) and wasGeneratedBy(gen1;e1,_a1,_t1,_attrs1) and wasGeneratedBy(gen2;e2,_a2,_t2,_attrs2) THEN gen1 strictly precedes gen2.

Note that event ordering is between generations of e1 and e2, as opposed to derivation where usage is known, which implies ordering between the usage of e1 and generation of e2.

---

The entity that triggered the start of an activity must exist before the activity starts. This is illustrated by Figure 4(a) and expressed by Constraint 43 (wasStartedBy-ordering).

Constraint 43 (wasStartedBy-ordering)

1. IF wasStartedBy(start;_a,e,_a1,_t1,_attrs1) and wasGeneratedBy(gen;e,_a2,_t2,_attrs2) THEN gen precedes start.
2. IF wasStartedBy(start;_a,e,_a1,_t1,_attrs1) and wasInvalidatedBy(inv;e,_a2,_t2,_attrs2) THEN start precedes inv.

---

Similarly, the entity that triggered the end of an activity must exist before the activity ends, as illustrated by Figure 4(b).

Constraint 44 (wasEndedBy-ordering)

1. IF wasEndedBy(end;_a,e,_a1,_t1,_attrs1) and wasGeneratedBy(gen;e,_a2,_t2,_attrs2) THEN gen precedes end.
2. IF wasEndedBy(end;_a,e,_a1,_t1,_attrs1) and wasInvalidatedBy(inv;e,_a2,_t2,_attrs2) THEN end precedes inv.

Figure 4 ^◊: Summary of instantaneous event ordering constraints for trigger entities

---

If an entity specalizes another, then its generation must follow the specialized entity's generation.

Constraint 45 (specialization-generation)

IF specializationOf(e2,e1) and wasGeneratedBy(gen1;e1,_a1,_t1,_attrs1) and wasGeneratedBy(gen2;e2,_a2,_t2,_attrs2) THEN gen1 precedes gen2.

---

Similarly, if an entity specalizes another, then its invalidation must follow the specialized entity's invalidation.

Constraint 46 (specialization-invalidation)

IF specializationOf(e2,e1) and wasInvalidatedBy(inv1;e1,_a1,_t1,_attrs1) and wasInvalidatedBy(inv2;e2,_a2,_t2,_attrs2) THEN inv2 precedes inv1.

5.2.3 Agent constraints

Like entities and activities, agents have lifetimes that follow a familiar pattern: an agent is generated, can participate in interactions such as starting, ending or association with an activity, attribution, or delegation, and finally the agent is invalidated.

Further constraints associated with agents appear in Figure 5 and are discussed below.

Figure 5 ^◊: Summary of instantaneous event ordering constraints for agents

---

An activity that was associated with an agent must have some overlap with the agent. The agent may be generated, or may only become associated with the activity, after the activity start: so, the agent is required to exist before the activity end. Likewise, the agent may be destructed, or may terminate its association with the activity, before the activity end: hence, the agent invalidation is required to happen after the activity start. This is illustrated by Figure 5 (a) and expressed by Constraint 47 (wasAssociatedWith-ordering).

Constraint 47 (wasAssociatedWith-ordering)

1. IF wasAssociatedWith(_assoc;a,ag,_pl,_attrs) and wasStartedBy(start;a,_e1,_a1,_t1,_attrs1) and wasInvalidatedBy(inv;ag,_a2,_t2,_attrs2) THEN start precedes inv.
2. IF wasAssociatedWith(_assoc;a,ag,_pl,_attrs) and wasGeneratedBy(gen;ag,_a1,_t1,_attrs1) and wasEndedBy(end;a,_e2,_a2,_t2,_attrs2) THEN gen precedes end.

---

An entity that was attributed to an agent must have some overlap with the agent. The agent is required to exist before the entity invalidation. Likewise, the entity generation must precede the agent destruction. This is illustrated by Figure 5 (b) and expressed by Constraint 48 (wasAttributedTo-ordering).

Constraint 48 (wasAttributedTo-ordering)

1. IF wasAttributedTo(_at;e,ag,_attrs) and wasGeneratedBy(gen;e,_a1,_t1,_attrs1) and wasInvalidatedBy(inv;ag,_a2,_t2,_attrs2) THEN gen precedes inv.
2. IF wasAttributedTo(_at;e,ag,_attrs) and wasGeneratedBy(gen;ag,_a1,_t1,_attrs1) and wasInvalidatedBy(inv;e,_a2,_t2,_attrs2) THEN gen precedes inv.

---

For delegation, two agents need to have some overlap in their lifetime.

Constraint 49 (actedOnBehalfOf-ordering)

IF actedOnBehalfOf(_del;ag2,ag1,_a,_attrs) and wasGeneratedBy(gen;ag1,_a1,_t1,_attrs1) and wasInvalidatedBy(inv;ag2,_a2,_t2,_attrs2) THEN gen precedes inv.

5.3 Impossibility constraints

Impossibility constraints require that certain patterns of statements never appear in valid PROV instances. Impossibility constraints have the following general form:

To check an impossibility constraint on instance I, we check whether there is any way of matching the pattern hyp₁, ..., hyp_n. If there is, then checking the constraint on I fails (which implies that I is invalid).

Influence is required to be irreflexive, that is, it is impossible for something to influence itself.

As noted previously, specialization is a strict partial order: it is irreflexive and transitive.

Furthermore, identifiers of basic relationships are disjoint.

Identifiers of entities, agents and activities cannot also be identifiers of properties.

5.4 Type Constraints

The following rule establishes types denoted by identifiers from their use within expressions. For this, the function typeOf gives the set of types denoted by an identifier. For example, typeOf(e) returns the set of types associated with identifier e. The function typeOf is not a term of PROV, but a construct introduced to validate PROV statements.

For any identifier id, typeOf(id) is a subset of {'entity', 'activity', 'agent', 'prov:Collection', 'prov:EmptyCollection'}. For identifiers that do not have a type, typeOf gives the empty set.

To check if a PROV instance satisfies type constraints, one obtains the types of identifiers by application of Constraint 54 (typing) and check no impossibility results from rules Constraint 55 (entity-activity-disjoint) and Constraint 56 (membership-empty-collection).

The set of entities and activities are disjoint, expressed by the following constraint:

An empty collection cannot contain any member, expressed by the following constraint:

6.1 Bundles

The definitions, inferences, and constraints, and the resulting notions of normalization, validity and equivalence, assume a PROV instance with exactly one bundle, the toplevel bundle, consisting of all PROV statements in the toplevel of the instance (that is, not enclosed in a named bundle). In this section, we describe how to deal with PROV instances consisting of multiple bundles. Briefly, each bundle is handled independently; there is no interaction between bundles from the perspective of applying definitions, inferences, or constraints, computing normal forms, or checking validity or equivalence.

We model a general PROV instance, containing n named bundles b₁...b_n, as a tuple (B₀,[b₁=B₁,...,b_n=B_n]) where B₀ is the set of statements of the toplevel bundle, and for each i, B_i is the set of statements of bundle b_i. This notation is shorthand for the following PROV-N syntax:

B0
bundle b1
  B1
endBundle
...
bundle bn
  Bn
endBundle

The normal form of a general PROV instance (B₀,[b₁=B₁,...,[b_n=B_n]) is (B'₀,[b₁=B'₁,...,b_n=B'_n]) where B'_i is the normal form of B_i for each i between 0 and n.

A general PROV instance is valid if each of the bundles B₀, ..., B_n are valid and none of the bundle identifiers b_i are repeated.

Two (valid) general PROV instances (B₀,[b₁=B₁,...,b_n=B_n]) and (B'₀,[b₁'=B'₁,...,b'_m=B'_m]) are equivalent if B₀ is equivalent to B'₀ and n = m and there exists a permutation P : {1..n} -> {1..n} such that for each i, b_i = b'_P(i) and B_i is equivalent to B'_P(i).