Dual-Rule Deadlock Criterion

Abstract

A repair class is deadlocked exactly when it has no jointly allowed repair.

Theorem 1.1 (Deadlock is empty joint allowance).

$$\begin{array}{r}\forall Repair:\mathrm{Type},\\ \forall repairClass,allo{w}_1,allo{w}_2:Set(Repair),\\ \\ Deadlocked(repairClass,allo{w}_1,allo{w}_2)\iff \\ \mathrm{intersection}\left(repairClass,JointAllowed(allo{w}_1,allo{w}_2)\right)=\varnothing .\end{array}$$

Proof. Machine-checked in Lean as D5/S3/ConceptDynamics/GovernanceFixedPoint/DualRuleDeadlockCriterion.deadlocked_iff_empty_joint_allowance (✓ std3). ∎

Source. Repository-derived.

Commentary.

The frozen reachability predicate asks for a repair in both the repair class and the two rules’ joint allowance. Negating that witness is equivalent to emptiness of the same intersection.

References

• Truth anchor: D5/S3/ConceptDynamics/GovernanceFixedPoint/DualRuleDeadlockCriterion.deadlocked_iff_empty_joint_allowance
• Dependency: D5/S3/ConceptDynamics/GovernanceFixedPoint/Core