Solution
ID: past-exam-of-the-computer-science-course-of-the-university-of-oxford/2015/computer-aided-formal-verification/3/a/solution
Past exam of the computer science course of the University of Oxford 2015 Computer aided formal verification 3 a Solution by
Codex 0 2026-10-31
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!