Define a predicate on the states that expresses that b is never less than r.

Form a detailed argument that proves the propositions in the following Prompts. Make sure your
response addresses all the items in the associated rubric on Canvas. Make sure to correctly utilize
and reference definitions and theorems from the textbook [1] as you develop your response. These
writing prompts are heavily inspired by problems in the course textbook [1].
Description
The stability of SFC, a beautiful city nestled by a bay, is governed by the quantities of two energy
sources B79X49 and R99a0y. SFC is stable when the quantity of B79X49 is greater than the
quantity of R99a0y. The quantities of these energies for any given day are symbolized as b and r,
respectively. Initially, b > r, and b and r are positive integers.
For as long as the inhabitants of the area have been around, there has been a general feeling of
unrest that is due to the fact that b > r. They hope for a day of stability and have monitored how the
energy quantities transition from one day to the next for a long time. Based on their observations,
after each day, exactly one of four things happens:
• Energy Transition 1: r increase by 1 unit.
• Energy Transition 2: b decreases by 1 unit.
• Energy Transition 3: b increases by 1 unit and r increases by 2 units.
• Energy Transition 4: b decreases by 2 units and r decreases by 1 unit.
A group of concerned citizens predicted that if there is ever a day when b < r, then SFC will crumble into the ocean and the lost forever. One thing that is known, is that if b = r, then stability will be reached and no more energy transition will occur and SFC will be peaceful for the rest of time. Your job is to build off of the known information with two goals in mind. You want to convince the people of SFC, that as long as the above energy transitions are the only possibilities and no more transitions are possible once b = r, then • SFC will never crumble into the ocean. • Eventually SFC will reach stability. Use the following prompts to guide you to this goal. Prompts 1. Before you begin to analyze the process of how the energy quantities change in SFC, let’s make sure you understand what happens for a couple of days with some example values. Suppose, that there are 16 units of B79X49 and 10 units of R99a0y one day in SFC. What are the quantities after 6 days of transitions if the order of transitions is 3, 1, 1, 4, 2, 2? Answer this by showing the quantities of b and r initially and after each day’s transition. Keep in mind that these example values are just being used initially to help you see how things work. For the rest of the prompts, keep the quantities arbitrary. 2. Model the somewhat mysterious process of energy transformation using a state machine model. Your model should at least include the following 3 items: (a) A description the state of SFC’s two main energy quantities as a set. Make sure to express what set(s) your state’s values come from. (b) At the beginning of SFC, there were two initial quantities for b and r. Considering this, symbolize the start state of your model. (c) Define the energy transitions as functions on the states of your model. 3. Using your model, (a) Define a predicate on the states that expresses that b is never less than r. (b) Verify that your predicate is a preserved invariant on the states. (c) Use the invariant to conclude that SFC will never fall into the ocean if the above description remains true. 4. Lastly, you need to show that eventually stability will be reached. (a) Define a variable on the states that you believe is strictly decreasing. (b) Prove that that variable is strictly decreasing. (c) Use the derived variable to show that eventually the energy transitions will stop and stability will be reached. (d) Express how many energy transitions are required to reach stability and briefly justify your claim. Responses 1. ... 2. (a) ... (b) ... (c) ... 3. (a) ... (b) ... (c) ... 4. (a) ... (b) ... (c) ... (d) ... References [1] Eric Lehman, F Thomson Leighton, and Albert R. Meyer. Mathematics for Computer Science. URL: https://ccsf-math-115.github.io/textbook/mcs_2018_ cropped.pdf. Creative Commons Attribution-ShareAlike 3.0 license.