suma (suc (x), y) = suc (suma (x, y))

Cualquiera de las dos ecuaciones es válida, siendo redundante poner ambas.

Ejercicio: Escribir la deducción ecuacional para llegar desde el ejemplo "suma (suc(suc(cero)), suc(cero))" hasta su término canónico. Comprobar que es el mismo que con la otra ecuación.

igual (cero, cero) = cierto
igual (suc (x), cero) = falso
igual (cero, suc (x)) = falso
 igual (suc(x), suc (y))= igual (x, y)

Una alternativa para la tercera ecuación sería

igual (x, y) = igual (y, x)

de este modo que si tuviéramos un término de la forma "igual (cero, suc (x))" aplicaríamos primero esta ecuación y a continuación podríamos aplicar la segunda para ver que su valor es falso.

El conjunto es impuro porque podemos tener varios términos que representen un mismo valor.

    cero = pred (suc (cero)) = pred (suc (suc (pred (cero))))

No es suficiente ya que no es aplicable a términos como suc(pred(cero)), suc(suc(pred(pred(cero)) en que la operación "suc" antecede a "pred".

Ejercicio: escribir las ecuaciones que arreglen el problema anterior.

pred (suc (x)) = suc (pred (x))

Aplicando esta ecuación primero, se puede aplicar a continuación la primera de las ecuaciones.

vacío: -> conjunto                                                crea el conjunto vacío
añadir: natural x conjunto -> conjunto
unión: conjunto x conjunto -> conjunto
intersección: conjunto x conjunto -> conjunto
pertenece: natural x conjunto -> bool
cardinal: conjunto -> natural
esvacío: conjunto -> bool

Como se ha dicho, en los conjuntos no importa el orden en que se añaden los elementos, por tanto se ha de escribir una ecuación que lo diga explícitamente. Ejercicio: escribir dicha ecuación antes de volver a la página anterior.

Falta otra ecuación que haga equivalentes los conjuntos en que se haya insertado dos veces el mismo elemento. Ejercicio: escribir dicha ecuación antes de volver a la página anterior.

No hace falta más ecuaciones.

unión (vacío, C) = C
unión (añadir (x, C), C2) = unión (C, añadir (x, C2))

Cabe remarcar que en la segunda ecuación no importa si al añadir x a C2, éste ya estaba incluido, porque ya se han definido las ecuaciones que especifican que no importa si se añade dos veces un mismo elemento a un conjunto.

Ejercicio: escribir una alternativa para la parte derecha de la segunda ecuación. La solución puede verse en la especificación final de conjuntos.

pertenece (x, vacío) = falso
pertenece (x, añadir (x, C)) = cierto
x=/=y ==> pertenece (x, añadir (y, C)) = pertenece (x, C)

intersección (vacío, C) = vacío
pertenece (x, C2) ==> intersección (añadir (x, C), C2) = añadir (x, intersección (C, C2))
no pertenece (x, C2) ==> intersección (añadir (x, C), C2) = intersección (C, C2)

Es incorrecta porque si se añade dos veces el mismo elemento a un conjunto no se puede garantizar que se apliquen antes las ecuaciones que eliminan duplicados a la que calcula el cardinal del conjunto.
Por ejemplo, si tenemos el conjunto  añadir (x, añadir (x, vacío))   se pueden aplicar las ecuaciones de las siguientes formas:
 

cardinal (añadir (x, añadir (x, vacío))) cardinal (añadir (x, vacío))   --  2ª ecuación generadora suc (cardinal (vacío))   --  2ª ecuación cardinal suc (cero)   -- 1ª ecuación cardinal

cardinal (añadir (x, añadir (x, vacío)) suc (cardinal (añadir (x, vacío)))    -- 2ª ecuación cardinal suc (suc (cardinal (vacío)))   -- 2ª ecuación cardinal suc (suc (cero))   -- 1ª ecuación cardinal

Puede verse la inconsistencia al salir resultados diferentes, por tanto las ecuaciones no pueden ser válidas.
Para arreglarlo dividiremos la 2ª ecuación del cardinal en dos posibilidades, dependiendo de si el elemento a contar está o no en el resto del conjunto.

Ejercicio: escribir las ecuaciones correctas del cardinal. La solución puede verse en la especificación final de conjuntos.

esvacío (vacío) = cierto
esvacío (añadir (x, C) = falso