# Proof Obligation Names (Rodin User Manual)

Do not edit! This content has been migrated to Subversion.
(Nightly Handbook Build)

Next is a table describing the names of context proof obligations:

 Well-definedness of an Axiom $m$ / WD $m$ is the axiom name Well-definedness of a Derived Axiom $m$ / WD $m$ is the axiom name Derived Axiom $m$ / THM $m$ is the axiom name

Next is a table showing the name of machine proof obligations:

 Well-definedness of an Invariant $v$ / WD $v$ is the invariant name Well-definedness of a Derived Invariant $m$ / WD $m$ is the invariant name Well-definedness of an event Guard $t$ / $d$ / WD $t$ is the event name $d$ is the action name Well-definedness of an event Action $t$ / $d$ / WD $t$ is the event name $d$ is the action name Feasibility of a non-det. event Action $t$ / $d$ / FIS $t$ is the event name $d$ is the action name Derived Invariant $m$ / THM $m$ is the invariant name Invariant Establishment INIT. / $v$ / INV $v$ is the invariant name Invariant Preservation $t$ / $v$ / INV $t$ is the event name $v$ is the invariant name

Next are the proof obligations concerned with machine refinements:

 Guard Strengthening $t$ / $d$ / GRD $t$ is the concrete event name $d$ is the abstract guard name Guard Strengthening (merge) $t$ / MRG $t$ is the concrete event name Action Simulation $t$ / $d$ / SIM $t$ is the concrete event name $d$ is the abstract action name Equality of a preserved Variable $t$ / $v$ / EQL $t$ is the concrete event name $v$ is the preserved variable

Next are the proof obligations concerned with the new events variant:

 Well definedness of Variant VWD Finiteness for a set Variant FIN Natural number for a numeric Variant $t$ / NAT $t$ is the new event name Decreasing of Variant $t$ / VAR $t$ is the new event name

Finally, here are the proof obligations concerned with witnesses:

 Well definedness of Witness $t$ / $p$ / WWD $t$ is the concrete event name $p$ is parameter name or a primed variable name Feasibility of non-det. Witness $t$ / $p$ / WFIS $t$ is the concrete event name $p$ is parameter name or a primed variable name

Remark: At the moment, the deadlock freeness proof obligation generation is missing. If you need it, you can generate it yourself as a derived invariant saying the the disjunction of the abstract guards imply the disjunction of the concrete guards.