diff --git a/algumas_notas_suplementares.md b/algumas_notas_suplementares.md
new file mode 100644
index 0000000..b8b1c52
--- /dev/null
+++ b/algumas_notas_suplementares.md
@@ -0,0 +1,53 @@
+# O que é isto?
+Este documento pretende tornar mais claro o funcionamento do polymani.pl. Para
+isso explicamos brevemente a estrutura e o funcionamento de alguns predicados mais
+que de outro modo poderiam parecer "abstratas".
+
+## Estrutura
+### Frontend
+O frontend tem todos os predicados usados para interação conforme especificado
+no assignment1.pdf.
+
+Por outro lado, para que uma melhor experiência de utilização fosse possível, tomamos a liberdade de implementar dois predicados auxiliares que, para inputs inválidos, disponibilizam uma explicação mais amigável do erro.
+
+### Backend
+Abaixo descrevem-se alguns predicados selecionados com vista a tornar a
+compreensão dos mesmos mais rápida e simples. Em alguns casos o objectivo foi
+destacar algumas particularidades que podem não ser evidentes numa primeira
+leitura.
+
+#### power
+As comparações CLPFD permitiram-nos comparar se uma determinada variavel
+pertencia um determinado domínio sem para isso termos de sacrificar a
+reversibilidade das variáveis. CLPFD stands for Constraint Logic Programming
+over Finite Domains.
+
+#### term
+Um termo é uma sequência de monómios sem adições.
+Este é um elemento fundamental deste programa tendo sido extensivamente testado.
+
+O primeiro predicado valida números reais definidos.
+
+O segundo predicado valida números indefinidos com a CLPR. A verificação de que
+N não é um compound é necessária para assegurar que N não é uma potencia (estas
+sao tratadas pelo terceiro e quarto predicado).
+
+O quinto predicado faz chamadas recursivas para validar uma multiplicação de
+monómios.
+
+#### simplify_term
+Começamos por convert um termo numa list de monómios.
+
+Ordenamos os monómios do por ordem crescente (isto é, de menor grau para maior
+grau).
+
+Se existir um zero na lista (um dos monómios é zero), sabemos que a qualquer
+coisa a múltiplicar por zero (recorde-se a definição de termo) é zero. Assim
+unificamos Term_Out com zero e terminamos a rotina com um green cut.
+
+Se não, 
+  se existir apenas um elemento na lista, esta já se encontra simplificada;
+  se não, aplicamos as seguintes regras de simplificação:
+    eliminar todos os monómios que têm a constante 1
+    juntar monómios semelhantes (com a mesma variável)
+