Hola Nicolás:
Es cierto lo que decís, se usa el mismo nombre para dos funciones distintas:
- #x₁ : TERM → ℕ
- #x₁ : FORM → ℕ
Esto puede ser un poco confuso pero es una práctica frecuente cuando definimos funciones que recorren una fórmula y luego terminan recorriendo términos. Según el contexto nos damos cuenta cuál es la función que se está usando.
Se pueden usar nombres distintos TERM-#x₁ y FORM#-x₁ por ejemplo.
Y escribiríamos cosas así:
- FORM-#x₁(α □ β) = FORM-#x₁(α) + FORM-#x₁(β)
- FORM-#x₁(xᵢ='xⱼ) = TERM-#x₁(xᵢ) + TERM-#x₁(xⱼ)
Espero que aclare tus dudas. Cualquier cosa volvé a preguntar.