• English only

Lab for Automated Reasoning and Analysis LARA

The property holds. Namely, suppose . Then there is a y such that and . Therefore, and . From and we have . Similarly, from and we have . Therefore, .

The property does not hold. As an example, take A={1,2}, B={p,q} and let (Sketch). By definitions of composition and inverse, both sides reduce to One way to prove it is to note that in the condition {P}r{Q} we can move quantification over s_2 inside and use properties of conjunction and implication to state it as: which is then equivalent to Therefore, the preconditions are precisely all subsets of the set on the right hand side, and so this set is the largest of them.

Alternatively, we can prove this property by showing by definition that 1) wp is a precondition and 2) that if we take any other precondition, it will be a subset of wp.

The property does not hold in general. As a counterexample, take three distinct states s_1, s_2, and s_3, and let Note: the property does hold for deterministic relations.  