## 3.2.5 Well-definedness proof obligations

There are several locations where well-definedness proof obligations can be created. The mathematical notation of the well-definedness conditions of each operator are defined by the -operator (3.3.1.2).

For well-definedness conditions, the order of axioms, invariants and guards is important. Well-definedness conditions are not usually shown in Rodin if they are trivial ().

#### 3.2.5.1 Axioms

For an axiom , denotes (the conjunction of) all axioms declared in extended contexts and the axioms already declared in the current context before the axiom in question.

 Well-definedness of an axiom Name label/WD Goal

#### 3.2.5.2 Invariants

For an invariant , denotes (the conjunction of) all the model’s invariants declared before the theorem.

 Well-definedness of an invariant Name label/WD Goal

#### 3.2.5.3 Guards

For an invariant , denotes (the conjunction of) all the model’s invariants declared before the theorem.

 Well-definedness of a guard Name eventname/guardlabel/WD Goal

#### 3.2.5.4 Witnesses

A witness may contain well-definedness conditions.

 Well-definedness of a witness Name eventlabel/witnesslabel/WWD Goal

#### 3.2.5.5 Actions

The assignment of each action with the label in an event must be well-defined.

 Well-definedness of an action Name eventlabel/actionlabel/WD Goal

#### 3.2.5.6 Variants

A variant must be well-defined.

 Well-definedness of a variant Name VWD Goal