I. Boolean expressions (8.1)
 A. pointwise extension
 B. reasoning about Boolean expressions (8.2)
II. Conditional Expressions (8.3)
 A. conditionals
------------------------------------------
                CONDITIONALS
             ^
cond.t.t1.t2 = 
  (\choose x :: (t ==> x == t1)
                /\ (!t ==> x == t2))
  * assuming x is not free in t, t1 or t2

Sugar:                   ^
 if t then t1 else t2 fi = cond.t.t1.t2

Inference Rules:

  Phi |- t
  ___________________________(if true rule)
  Phi |- if t then t1 else t2 fi == t1

  Phi |- !t
  __________________________(if false rule)
  Phi |- if t then t1 else t2 fi == t2

------------------------------------------
        what does the definition of cond mean?
  can you fill in the details of the predicate calculus step?
  How would you  prove the other inference rule:
        _____________________________________(if same rule)
        Phi |- if t then t' else t' fi == t'
     from the previous two rules?
------------------------------------------
          FOCUSING RULES

Let ~ be a reflexive relation.

Phi, t |- t1 ~ t1'
___________________________(if focus true)
Phi |- if t then t1 else t2 fi
       ~ if t then t1' else t2 fi

Phi, !t |- t2 ~ t2'
__________________________(if focus false)
Phi |- if t then t1 else t2 fi
       ~ if t then t1 else t2' fi
------------------------------------------
        how would you prove these?
        Why must ~ be reflexive?
 B. conditional expressions and state transformers
 C. proving properties about conditional state transformers
------------------------------------------
        ADDING CONDITIONALS
     TO STRAIGHT-LINE PROGRAMS

  f ::= id | x := e | f1; f2
      | if b then f1 else f2 fi

where
 x is a list of distinct state attributes,
 e is a corresponding expression list,
 b is a Boolean expression     
------------------------------------------
        how would you prove that
             var x : Nat |- (x := x + 2); (x := x - 2) == id  ?
        are pointwise extended functions pointwise functional?
        are expressions in general pointwise functional?
 D. Example proof
   can you prove that
       var x, y |- (x := x max y) == if x <= y then x := y else id fi ?
   what does "generalization" mean in the middle (big) step of the
   proof on p. 148?