diff --git a/tesi/conv.py b/tesi/conv.py
index 120475a..ce5fd8b 100644
--- a/tesi/conv.py
+++ b/tesi/conv.py
@@ -3,10 +3,12 @@ import re
 from sys import argv
 
 allsymbols = json.load(open('./unicode-latex.json'))
-mysymbols = ['≡', '≠', '≼', '→', '←', '⊀', '⋠', '≺', '∀', '∈', 'ε','₀', '₂', '₁', '₃', 'ₐ', 'ₖ', 'ₘ', 'ₙ', 'ᵢ', 'ⁱ', '⋮']
+mysymbols = ['≡', '≠', '≼', '→', '←', '⊀', '⋠', '≺', '∀', '∈', 'ε','₀', '₂', '₁', '₃', 'ₐ', 'ₖ', 'ₘ', 'ₙ', 'ᵢ', 'ⁱ', '⋮', 'ₛ', 'ₜ', '≃', '⇔', '∧', '∅', 'ℕ', 'ⱼ', 'ʲ', '⊥', 'π']
+extrasymbols = {'〚': '\llbracket', '〛': '\rrbracket'}
 
 symbols = {s: allsymbols[s] for s in mysymbols}
-mathsymbols = {s: '$'+allsymbols[s]+'$' for s in symbols}
+symbols.update(extrasymbols)
+mathsymbols = {s: '$'+v+'$' for s, v in symbols.items()}
 
 def read_by_char(fname):
     # Yield character and True/False if inside mathmode block
diff --git a/tesi/tesi.pdf b/tesi/tesi.pdf
index 8c6afea..ac6cb94 100644
Binary files a/tesi/tesi.pdf and b/tesi/tesi.pdf differ
diff --git a/tesi/tesi_unicode.org b/tesi/tesi_unicode.org
index 54291e5..d967388 100644
--- a/tesi/tesi_unicode.org
+++ b/tesi/tesi_unicode.org
@@ -921,17 +921,17 @@ Theorem: Given an input space /S/ and a couple of decision trees, where
 the target decision tree Cₜ covers the input space /S/, we say that
 the two decision trees are equivalent when:
 
-| (equiv S Cₛ Cₜ gs = Yes) ∧ covers(Cₜ, S) ⇒ ∀vₛ≃vₜ ∈ S, Cₛ(vₛ) ≃gs Cₜ(vₜ)
+| equiv(S, Cₛ, Cₜ, gs) = Yes ∧ covers(Cₜ, S) → ∀vₛ≃vₜ ∈ S, Cₛ(vₛ) ≃gs Cₜ(vₜ)
 
 Similarly we say that a couple of decision trees in the presence of
 an input space /S/ are /not/ equivalent when:
 
-| (equiv S Cₛ Cₜ gs = No(vₛ,vₜ) ∧ covers(Cₜ, S) ⇒ vₛ≃vₜ ∈ S ∧ Cₛ(vₛ) ≠gs Cₜ(vₜ)
+| equiv(S, Cₛ, Cₜ, gs) = No(vₛ,vₜ) ∧ covers(Cₜ, S) → vₛ≃vₜ ∈ S ∧ Cₛ(vₛ) ≠gs Cₜ(vₜ)
 
 Corollary: For a full input space /S/, that is the universe of the
 target program we say:
 
-| (equiv S [|tₛ|]ₛ [|tₜ|]ₜ ∅ = Yes)  ⇔  tₛ ≃ tₜ
+| equiv(S, 〚tₛ〛ₛ, 〚tₜ〛ₜ, ∅) = Yes  ⇔  tₛ ≃ tₜ
 
 
 *** Proof of the correctness of the translation from source programs to source decision trees
@@ -1011,13 +1011,13 @@ we can say that the couple of decision trees are the same for
 every couple of source value /vₛ/ and target value /vₜ/ that are equivalent.
 \begin{comment}
 Define "covered"
-Is it correct to say the same? How to correctly distinguish in words ≊ and = ?
+Is it correct to say the same? How to correctly distinguish in words ≃ and = ?
 \end{comment}
-| equiv(S, Cₛ, Cₜ) = Yes and cover(Cₜ, S) → ∀ vₛ ≊ vₜ∈S ∧ Cₛ(vₛ) = Cₜ(vₜ)
+| equiv(S, Cₛ, Cₜ) = Yes and cover(Cₜ, S) → ∀ vₛ ≃ vₜ∈S ∧ Cₛ(vₛ) = Cₜ(vₜ)
 In the case where the algorithm returns No we have at least a couple
 of counter example values vₛ and vₜ for which the two decision trees
 outputs a different result.
-| equiv(S, Cₛ, Cₜ) = No(vₛ,vₜ) and cover(Cₜ, S) → ∀ vₛ ≊ vₜ∈S ∧ Cₛ(vₛ) ≠ Cₜ(vₜ)
+| equiv(S, Cₛ, Cₜ) = No(vₛ,vₜ) and cover(Cₜ, S) → ∀ vₛ ≃ vₜ∈S ∧ Cₛ(vₛ) ≠ Cₜ(vₜ)
 
 We define  the following
 | Forall(Yes) = Yes
@@ -1054,10 +1054,10 @@ In the other subcases S is always non-empty.
    subtree Cₜᵢ
    | equiv(Sᵢ, Cₛ, Cₜᵢ) = Yes ∀i
    or we have a counter example vₛ, vₜ for which
-   | vₛ≊vₜ∈Sₖ ∧ cₛ(vₛ) ≠ Cₜₖ(vₜ)
+   | vₛ≃vₜ∈Sₖ ∧ cₛ(vₛ) ≠ Cₜₖ(vₜ)
    then because 
    | vₜ∈(a→πₖ) ⇒ Cₜ(vₜ) = Cₜₖ(vₜ)
    then
-   | vₛ≊vₜ∈S ∧ Cₛ(vₛ)≠Cₜ(vₜ) 
+   | vₛ≃vₜ∈S ∧ Cₛ(vₛ)≠Cₜ(vₜ) 
    and the result of the algorithm is
    | equiv(Sᵢ, Cₛ, Cₜᵢ) = No(vₛ, vₜ) for some minimal k∈I