 
  
 
 
 
 
CMU 15-671Models of Software SystemsFall 1995
Sets, Relations, Functions; Proof Techniques 
Garlan & Wing Homework 3  Due: 13 September 1995
 
 
 
 
 
Problem 1.
Chapter 5 of SEM: 5.1, 5.2, 5.4, 5.6, 5.9, 5.13
Problem 2.
Chapter 6 of SEM: 6.1, 6.2, 6.3, 6.11
Problem 3.
Simplify this expression using the One-Point Rule.
 
  
   
Problem 4.
[GS, Chapter 4, Problem 4.10]
Prove Modus ponens,   , using
equational reasoning.  Hint: You should also use one of the proof
techniques discussed in Handout 3.
 , using
equational reasoning.  Hint: You should also use one of the proof
techniques discussed in Handout 3.
Problem 5.
[GS, Chapter 4, Problem 4.13]
Let   be the minimum of integers x and y,
defined by
  be the minimum of integers x and y,
defined by
  =
  =   .
Prove that
 .
Prove that   is symmetric, i.e.,
  is symmetric, i.e.,   .
Use an equational reasoning style of proof.  How many cases do you
have to consider?  You may use the necessary rules of integer
arithmetic,
for example, that
 .
Use an equational reasoning style of proof.  How many cases do you
have to consider?  You may use the necessary rules of integer
arithmetic,
for example, that   and that
  and that   .
 .