Rodin HandbookThis work is sponsored by the Deploy Project This work is sponsored by the ADVANCE Project This work is licensed under a Creative Commons Attribution 3.0 Unported License 
3.2.5 Welldefinedness proof obligationsThere are several locations where welldefinedness proof obligations can be created. The mathematical notation of the welldefinedness conditions of each operator are defined by the operator (3.3.1.2). For welldefinedness conditions, the order of axioms, invariants and guards is important. Welldefinedness conditions are not usually shown in Rodin if they are trivial (). 3.2.5.1 AxiomsFor 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.
3.2.5.2 InvariantsFor an invariant , denotes (the conjunction of) all the model’s invariants declared before the theorem.
3.2.5.3 GuardsFor an invariant , denotes (the conjunction of) all the model’s invariants declared before the theorem.
3.2.5.4 WitnessesA witness may contain welldefinedness conditions.
3.2.5.5 ActionsThe assignment of each action with the label in an event must be welldefined.
3.2.5.6 VariantsA variant must be welldefined.
