+-- | If we rotate a direction (other than left or right)
+-- counter-clockwise with respect to the y-axis, we should get a new
+-- direction.
+prop_ccwy_rotation_changes_direction :: Cardinal -> Property
+prop_ccwy_rotation_changes_direction c =
+ c `elem` [F, B, D, T, FL, FR, FD, FT, BL, BR, BD, BT, LD, LT,
+ RD, RT, FLD, FLT, FRD, FRT, BLD, BLT, BRD, BRT]
+ ==> ccwy c /= c
+
+
+-- | If we rotate a direction (other than left or right) clockwise
+-- with respect to the y-axis, we should get a new direction.
+prop_cwy_rotation_changes_direction :: Cardinal -> Property
+prop_cwy_rotation_changes_direction c =
+ c `elem` [F, B, D, T, FL, FR, FD, FT, BL, BR, BD, BT, LD, LT,
+ RD, RT, FLD, FLT, FRD, FRT, BLD, BLT, BRD, BRT]
+ ==> cwy c /= c
+
+
+-- | If we rotate a direction (other than top or down)
+-- counter-clockwise with respect to the z-axis, we should get a new
+-- direction.
+prop_ccwz_rotation_changes_direction :: Cardinal -> Property
+prop_ccwz_rotation_changes_direction c =
+ c `elem` [L, R, F, B, FL, FR, FD, FT, BL, BR, BD, BT, LD, LT,
+ RD, RT, FLD, FLT, FRD, FRT, BLD, BLT, BRD, BRT]
+ ==> ccwz c /= c
+
+
+-- | If we rotate a direction (other than top or down) clockwise with
+-- respect to the z-axis, we should get a new direction.
+prop_cwz_rotation_changes_direction :: Cardinal -> Property
+prop_cwz_rotation_changes_direction c =
+ c `elem` [L, R, F, B, FL, FR, FD, FT, BL, BR, BD, BT, LD, LT,
+ RD, RT, FLD, FLT, FRD, FRT, BLD, BLT, BRD, BRT]
+ ==> cwz c /= c
+
+
+-- | If we are given a direction c, there should only be one direction
+-- d which, when rotated counter-clockwise with respect to the
+-- x-axis, produces c.
+prop_ccwx_rotation_result_unique :: Cardinal -> Property
+prop_ccwx_rotation_result_unique c =
+ c `elem` all_directions ==>
+ (length [ d | d <- all_directions, ccwx d == c ]) == 1
+
+-- | If we are given a direction c, there should only be one direction
+-- d which, when rotated clockwise with respect to the x-axis,
+-- produces c.
+prop_cwx_rotation_result_unique :: Cardinal -> Property
+prop_cwx_rotation_result_unique c =
+ c `elem` all_directions ==>
+ (length [ d | d <- all_directions, cwx d == c ]) == 1
+
+
+-- | If we are given a direction c, there should only be one direction
+-- d which, when rotated counter-clockwise with respect to the
+-- y-axis, produces c.
+prop_ccwy_rotation_result_unique :: Cardinal -> Property
+prop_ccwy_rotation_result_unique c =
+ c `elem` all_directions ==>
+ (length [ d | d <- all_directions, ccwy d == c ]) == 1
+
+
+-- | If we are given a direction c, there should only be one direction
+-- d which, when rotated clockwise with respect to the y-axis,
+-- produces c.
+prop_cwy_rotation_result_unique :: Cardinal -> Property
+prop_cwy_rotation_result_unique c =
+ c `elem` all_directions ==>
+ (length [ d | d <- all_directions, cwy d == c ]) == 1
+
+
+-- | If we are given a direction c, there should only be one direction
+-- d which, when rotated counter-clockwise with respect to the
+-- z-axis, produces c.
+prop_ccwz_rotation_result_unique :: Cardinal -> Property
+prop_ccwz_rotation_result_unique c =
+ c `elem` all_directions ==>
+ (length [ d | d <- all_directions, ccwz d == c ]) == 1
+
+
+-- | If we are given a direction c, there should only be one direction
+-- d which, when rotated clockwise with respect to the z-axis,
+-- produces c.
+prop_cwz_rotation_result_unique :: Cardinal -> Property
+prop_cwz_rotation_result_unique c =
+ c `elem` all_directions ==>
+ (length [ d | d <- all_directions, cwz d == c ]) == 1
+
+