Relational Weakest-Precondition Composition

Abstract

Universal weakest preconditions compose in reverse process order.

Theorem 1.1 (Weakest preconditions propagate backward through a composite).

$$\forall X\in Type,Y\in Type,Z\in Type,R\in \mathrm{SetRel}\left(X,Y\right),S\in \mathrm{SetRel}\left(Y,Z\right),Q\in \mathrm{Set}\left(Z\right),\mathrm{universalWeakestPrecondition}\left(\mathrm{SetRelComp}\left(R,S\right),Q\right)=\mathrm{universalWeakestPrecondition}\left(R,\mathrm{universalWeakestPrecondition}\left(S,Q\right)\right)$$

Proof. Machine-checked in Lean as D5/S3/ObserverMemory/Knowledge/RelationalWeakestPreconditionComposition.universal_weakest_precondition_composition (✓ std3). ∎

Source. Repository-derived.

Commentary.

The two relations have the source, intermediate, and final carriers shown in the formula. The predicate transformer is the canonical relational core, and the proof applies the pinned library composition law directly.

References

• Truth anchor: D5/S3/ObserverMemory/Knowledge/RelationalWeakestPreconditionComposition.universal_weakest_precondition_composition
• Dependency: D5/S3/ObserverMemory/Knowledge/RelationalPreconditionAdjunction