\(\texttt{app}\) di una lista e la lista vuota equivale alla prima list. $$ \forall l_1 \in L_A .\; \texttt{app}(l_1,[]) = l_1 $$
\(\texttt{app}\) è associativa. $$ \forall l_1,l_2,l_3 \in L_A .\; \texttt{app}(\texttt{app}(l_1,l_2),l_3) = \texttt{app}(l_1,\texttt{app}(l_2,l_3))$$
Interazione fra \(\texttt{rev}\) e \(\texttt{app}\) (distributività di \(\texttt{rev}\) su \(\texttt{app}\)). $$ \forall l_1,l_2 \in L_A .\; \texttt{rev}(\texttt{app}(l_1,l_2)) = \texttt{app}(\texttt{rev}(l_2),\texttt{rev}(l_1)) $$
La lunghezza della lista ottenuta concatenando due liste è equivalente alla somma delle lunghezze delle due liste. $$ \forall l_1,l_2 \in L_A .\; \texttt{len}(\texttt{app}(l_1,l_2)) = \texttt{len}(l_1) + \texttt{len}(l_2) $$
Rovesciare una lista non cambia la sua lungezza. $$ \forall l \in L_A . \; \texttt{len}(\texttt{rev}(l)) = \texttt{len}(l) $$
Interazione fra \(\texttt{belList}\) e \(\texttt{app}\). $$ \forall l_1,l_2 \in L_A .\; \forall b \in A .\; \texttt{belList}(\texttt{app}(l_1,l_2),b) = \texttt{belList}(l_1,b) \vee \texttt{belList}(l_2,b) $$
Interazione fra \(\texttt{belList}\) e \(\texttt{rev}\). $$ \forall l \in L_A . \; \forall b \in A. \; \texttt{belList}(\texttt{rev}(l),b) = \texttt{belList}(l,b) $$
Interazione fra \(\texttt{sumList}\) e \(\texttt{app}\). $$ \forall l_1,l_2 \in L_\mathbb{N} . \; \texttt{sumList}(\texttt{app}(l_1,l_2)) = \texttt{sumList}(l_1) + \texttt{sumList}(l_2) $$
\(\texttt{rev}\) è un involuzione (la sua funzione inversa è sé stessa). $$ \forall l \in L_A . \; \texttt{rev}(\texttt{rev}(l)) = l $$
\(\texttt{insert}\) rispetta la proprietà \(\texttt{ordinatoL}\): $$ \forall l\in L_\mathbb{N} .\; \forall n\in \mathbb{N} .\; \texttt{ordinatoL}(l) = true \implies \texttt{ordinatoL}(\texttt{insert}(n,l)) = true $$
\(\texttt{sort}\) ordina le liste: $$ \forall l\in L_\mathbb{N} .\; \texttt{ordinatoL}(\texttt{sort}(l)) = \texttt{true} $$
\(\texttt{belList}\) della visita anticipa (\(\texttt{visit2}\)) di un albero è equivalente a \(\texttt{belBT}\) dell'albero. $$ \forall t \in BT_A . \; \forall b \in A. \; \texttt{belList}(\texttt{visist2}(t),b) = \texttt{belBT}(t,b) $$
\(\texttt{sumList}\) della visita anticipa (\(\texttt{visit2}\)) di un albero è equivalente a \(\texttt{sumBT}\) dell'albero. $$ \forall t \in BT_\mathbb{N} . \; \texttt{sumList}(\texttt{visit2}(t)) = \texttt{sumBT}(t) $$
\(\texttt{ins}\) rispetta la proprietà \(\texttt{ordinatoPP}\), ovvero, se un albero binario è ordinato, allora rimarrà ordinato se aggiungiamo un nodo utilizzando \(\texttt{ins}\). $$ \forall t \in BT_\mathbb{N} . \; \forall n \in \mathbb{N} . \; \texttt{ordinatoPP}(t) \implies \texttt{ordinatoPP}(\texttt{ins}(n,t)) $$
\(\texttt{invBT}\) è una involuzione (la sua funzione inversa è sé stessa): $$ \forall t\in BT_A .\; \texttt{invBT}(\texttt{invBT}(t)) = t $$
Invertire un albero binario (di numeri naturali) non cambia la sua somma: $$ \forall t\in BT_\mathbb{N} .\; \texttt{sumBT}(\texttt{invBT}(t)) = \texttt{sumBT}(t) $$
\(\texttt{len}\) della visita anticipa (\(\texttt{visit2}\)) di un albero è equivalente a \(\texttt{size}\) dell'albero: $$ \forall t \in BT_\mathbb{A} . \; \texttt{len}(\texttt{visit2}(t)) = \texttt{size}(t) $$
Invertire un albero binario è poi fare una visita simmetrica è uguale a fare una visita simmetrica ed applicare \(\texttt{rev}\) al risultato ottenuto: $$ \forall t\in BT_A .\; \texttt{visitS}(\texttt{invBT}(t)) = \texttt{rev}(\texttt{visitS}(t)) $$
\(\texttt{add}\) è corretta. $$ \forall n,m \in \mathcal{N}Term . \; \texttt{val}(\texttt{add}(n,m)) = \texttt{val}(n) + \texttt{val}(m) $$
\(\texttt{mul}\) è corretta. $$ \forall n,m \in \mathcal{N}Term . \; \texttt{val}(\texttt{mul}(n,m)) = \texttt{val}(n) * \texttt{val}(m) $$
\(\texttt{exp}\) è corretta. $$ \forall n,m \in \mathcal{N}Term . \; \texttt{val}(\texttt{exp}(n,m)) = \texttt{val}(m) ^ {\texttt{val}(n)} $$
Unità di \(\texttt{add}\). $$ \forall n \in \mathcal{N}Term . \; \texttt{add}(n, Z) = n $$
\(\texttt{add}\) di un qualsiasi \(\mathcal{N}Term\) e il succesore di un'altro \(\mathcal{N}Term\) equivale al succesore della somma di essi. $$ \forall n \in \mathcal{N}Term . \; \texttt{add}(n, S(m)) = S(add(n,m)) $$
\(\texttt{add}\) è associativa. $$ \forall n,m,o \in \mathcal{N}Term . \; \texttt{add}(\texttt{add}(n,m),o) = \texttt{add}(n,\texttt{add}(m,o)) $$
\(\texttt{add}\) è commutativa. $$ \forall n,m \in \mathcal{N}Term . \; \texttt{add}(n,m) = \texttt{add}(m, n) $$
\(\texttt{mul}\) di \(Z\) (Assorbimento di \(\texttt{mul}\)). $$ \forall n \in \mathcal{N}Term . \; \texttt{mul}(n,Z) = Z $$
\(\texttt{mul}\) di un succesore di un qualsiasi numero naturale. $$ \forall n,m \in \mathcal{N}Term . \; \texttt{mul}(n,m) = \texttt{add}(m, n) $$
\(\texttt{mul}\) è commutativa. $$ \forall n,m \in \mathcal{N}Term . \; \texttt{mul}(n,m) = \texttt{mul}(m,n) $$
\(\texttt{mul}\) è distributiva su \(\texttt{add}\). $$ \forall n,m,o \in \mathcal{N}Term . \; \texttt{mul}(\texttt{add}(n,m),o) = \texttt{add}(\texttt{mul}(n,o),\texttt{mul}(m,o)) $$
\(\texttt{mul}\) è associativa. $$ \forall n,m,o \in \mathcal{N}Term . \; \texttt{mul}(\texttt{mul}(n,m),o) = \texttt{mul}(n,\texttt{mul}(m, o)) $$
\(\texttt{even}\) è l'opposto di \(\texttt{odd}\): $$ \forall n \in \mathcal{N}Term . \; \texttt{even}(n) = \texttt{not}(\texttt{odd}(n)) $$
Un numero sommato a se stesso è pari: $$ \forall n \in \mathcal{N}Term . \; \texttt{even}(\texttt{add}(n, n)) = \texttt{true} $$