f B then f else g) else (if A’ then f else h)
|
|      =  (f inc_B + g inc_B’)inc_A + (f inc_A’ + h inc_A)inc_A’
|
|         &lt;since A’’ = A&gt;
|
|      =  f inc_B inc_A + g inc_B’ inc_A + f inc_A’ inc_A’ + h inc_A inc_A’
|
|         &lt;by (15)&gt;
|
|      =  f inc_(A |^| B) + g inc_(A |^| B’) + f inc_A’
|
|         &lt;by (25)&gt;
|
|      =  f(inc_(A |^| B) + inc_A’) + g inc_(A |^| B’)
|
|         &lt;by (15) since the sum in parentheses is defined by (25)&gt;
|
|      =  