Solution

ID: past-exam-of-the-computer-science-course-of-the-university-of-oxford/2015/computer-aided-formal-verification/3/a/solution

Write . All arguments depend only on this given satisfaction set; they do not require an additional convention for the printed notation . For a state , let . The power set is ordered by set inclusion.
Take and any . By the definition of , we have both and . By transitivity of set inclusion, , so . Since this applies to every member of ,
Thus is an order-preserving function, which is the meaning of monotonicity here. This proof does not need either finiteness or the absence of terminal states.

New to topics? Read the docs here!