### 6.2. The alternation rule

This rule is for subdividing some prime `A`

into an `if`

construct with
this general form:

# [ `A`

]
if `B`

:
# [ `C`

]
...
else:
# [ `D`

]
...

The proof rule is:

Doing the intended function `C`

when `B`

is true, or doing the
intended function `D`

when
`B`

is false, must have the same
net affect as doing the intended function for `A`

.

Here's a brief example.

def sqrt(x):
'''Return the square root of x.
[ x is a number ->
if x is nonnegative ->
return the square root of x
else -> raise ValueError ]
'''
#-- 1
if x >= 0:
#-- 1.1
# [ return x to the one-half power ]
return x**0.5
else:
#-- 1.2
# [ raise ValueError ]
raise ValueError("You can't take the square root of a "
"negative number like {0:g}.".format(x))