With real-world ADTs, some of the equations may hold only when some additional predicate is true. When an equation depends on an additional predicate, we call it a conditional equation.

Suppose, for example, we start with an empty FMap, add an entry for "blue", another entry for "green", and then a second entry for "blue". What's the size of that FMap? Is its size 2 or 3?

An algebraic specification for FMap will answer that question.