diff --git a/anno3/vpc/orale/ltximg/org-ltximg_24983fbc72a7cd009dabdf26995f474fa11d6e16.png b/anno3/vpc/orale/ltximg/org-ltximg_24983fbc72a7cd009dabdf26995f474fa11d6e16.png
new file mode 100644
index 0000000..b882856
Binary files /dev/null and b/anno3/vpc/orale/ltximg/org-ltximg_24983fbc72a7cd009dabdf26995f474fa11d6e16.png differ
diff --git a/anno3/vpc/orale/preparazione.org b/anno3/vpc/orale/preparazione.org
index 58357a4..cb9c6a6 100644
--- a/anno3/vpc/orale/preparazione.org
+++ b/anno3/vpc/orale/preparazione.org
@@ -133,7 +133,10 @@ Legge del comportamente ciclico:
 | ∃m₀, ∃σ∈L(S) | mₒ[σ>m₀ ∧ σ=x
 * 2.1 Algebra dei Processi
 Descrizione astratta di sistemi concorrenti e non deterministici.
-Si focalizza sulle transizioni eseguite piu` che sugli stati raggiunti.
+Si focalizza sulle transizioni eseguite piu` che sugli stati
+raggiunti.
+Un processo e` composto da termini interni (sottocomponenti) e puo`
+interagire con l'ambiente esterno.
 ** CCS: Calculus of Communicating Systems
 - A, B, C: agenti
 - a, b, c: azioni
@@ -143,7 +146,7 @@ Grammatica:
 | E := nil | (E) | a.E | E + E' | E‖E' | E\L | E[f]
 ** CSP: Communicating Sequential Processes
 Due primitive: eventi (azioni) e processi.
-| P := STOP | skip | a → P | P + Q | P ⊓ Q | P □ Q | P ‖ₛ Q | E / a
+| P := STOP | skip | a → P | P ⊓ Q | P □ Q | P ‖ₛ Q | E / a
 A lezione abbiamo visto:
 | P :=     nil     | a.P   | P + Q |                 P ‖ₛ Q | E / a
 ** Structural Operational Semantics
@@ -373,20 +376,35 @@ trace decorate: stessa sequenza di azioni e una volta eseguite stesso
 insieme di azioni possibili
 bisimulazione: stessa sequenza di azioni e ricorsivamente stesso
 comportamento
+- Trace:
+  due automi sono ~ₜ se generano lo stesso linguaggio.
+  Nel caso di PA, due proc sono equivalentiₜ se possono produrre la
+  stessa sequenza di azioni.
+  dati p,q:
+     + p $\underrightarrow{a}$ p' implica ∃q' | q $\underrgightarrow{a}$ q'
+     + q $\underrightarrow{a}$ q' implica ∃p' | p $\underrgightarrow{a}$ p'
+  
 - Failure:
   definisco Fail(P) = (σ,X):
   dopo aver eseguito σ, tutte le azioni in X non possono piu` essere
   abilitate.
 - Simulazione: ∀p,q⊆P×P
-  p ~ q iff ( ∀a: p $\underrightarrow{a}$ p' → ∃q:
+  p ~ q iff ( ∀a: p $\underrightarrow{a}$ p' → ∃q':
   q\underrightarrow{a}$q' ∧ p' ~ q')
 - Bisimulazione: ∀p,q⊆P×P
-  p≈q iff ∀a: p $\underrightarrow{a}$ p' → ∃q: q $\underrightarrow{a}$  q'
+  p≈q iff ∀a: p $\underrightarrow{a}$ p' → ∃q': q $\underrightarrow{a}$  q'
   and
-          ∀a: q $\underrightarrow{a}$ q' → ∃p: p $\underrightarrow{a}$p'
+          ∀a: q $\underrightarrow{a}$ q' → ∃p': p $\underrightarrow{a}$p'
 ** Congruenza
 La bisimulazione e` una congruenza, ovvero 
 B≈ᶜC → A≈A[B/C]
+** Observational equivalence
+Prendiamo due processi P, Q e un osservatore R.
+osservare P e Q significa avere R in interleaving con P e Q:
+| P‖ₛR e Q‖ₛR
+| P→ₐP₁; P₁→ₑ
+| Q→ₐQ₁⊓Q₂; Q₁→ₑ; Q₂→ₕ
+
 * Fairness
 - Absolute Fairness: GF(exᵢ)
   un processo puo` essere eseguitp infinite volte.
@@ -399,3 +417,11 @@ La weak fairness e` piu` stringente perche` richiede che da un punto
 in avanti il processo rimanga in stato di abilitazione.
 La strong fairness rilassa questo vincolo "e si accontenta" che il
 processo vada in stato di abilitazione prima di essere eseguito.
+* Automa di Buchi
+A = <S, ∑, Δ, F>
+- S: insieme degli stati
+- ∑: alfabeto
+- Δ: ⊂ S×∑×S
+- F: multiset stati accentanti
+run accettante: lim(run(A))= {q| q si ripete infinite volte}
+∀Fᵢ∈F: Fᵢ∩lim(run) ≠ ∅
diff --git a/anno3/vpc/orale/ripeti.org b/anno3/vpc/orale/ripeti.org
new file mode 100644
index 0000000..1fcd51c
--- /dev/null
+++ b/anno3/vpc/orale/ripeti.org
@@ -0,0 +1,47 @@
+Rete di petri: grafo bipartito, Sistema: stato composito
+Rete colorata: cd: P∪T → C, Post[p,t]: cd(t) → bag(cd(p))
+| Transition system: <V, ∑, T, ∑₀, R (→)>
+* Semantiche:
+** Peled: (Induzione Strutturale)
+σⁱ il suffisso sᵢ, sᵢ₊₁, ... (σ⁰ = σ)
+| σⁱ ⊧ p, p is proposition if sᵢ ⊧ p                  
+** Katoen:
+Diciamo che R⁰(s) = s, Rⁿ⁺¹ = R(Rⁿ(s))
+| M,s ⊧ φ if ∀σ| σ₀ = s, σ ⊧ φ (ogni path che parte da s soddisfa φ)
+| M,s ⊧ p if p ∈ L(S)
+** Katoen CTL:
+| Pₘ(s) = {σ ∈ Sʷ| σ₀ = s}   σ path - sequenza di s
+Per induzione strutturale su ϕ:
+| M,s ⊧ p iff p∈L(S)
+| M,s ⊧ ¬φ iff ¬(M,s ⊧ φ)
+** TCTL
+CTL + Formula clocks, definito su TTS.
+D = set formula clocks
+| ϕ ::= p | ¬(ϕ) | ϕ∨ϕ | E[ϕUϕ] | A[ϕUϕ] | α∈Cstr(C∪D) | z in ϕ
+Dati s = (l,v), w∈V(D):
+| s,w ⊧ p if p∈Label(l)
+| s,w ⊧ α if v∪w ⊧ α
+| s,w ⊧ ¬ϕ if ¬(s,w ⊧ ϕ)
+| s,w ⊧ ϕ ∨ ψ if (s,w⊧ϕ ∨ s,w⊧(ψ)
+| s,w ⊧ z in ϕ if s,reset z in w ⊧ ϕ
+| s,w ⊧ E(ϕUψ) if ∃σ∈Pₘ(s), ∃(i,d)∈Pos(σ): 
+       | ∀(j,d')≤(i,d) σ(j,d'),wⱼ ⊧ ϕ    ∧   σ(i,d),wᵢ⊧ψ
+     (dove wⱼ = w+▵(σ,j), wᵢ = w+▵(σ,i))
+| s,w ⊧ E(ϕUψ) if ∀σ∈Pₘ(s), ∃(i,d)∈Pos(σ): 
+       | ∀(j,d')≤(i,d) σ(j,d'),wⱼ ⊧ ϕ    ∧   σ(i,d),wᵢ⊧ψ
+     (dove wⱼ = w+▵(σ,j), wᵢ = w+▵(σ,i))
+
+σ e` una RT trajectory: sequenza infinita di stati
+| σ = s₀ →δ₀→ s₁ →δ₁→ s₂ →...
+| pos di σ = coppia (i,δ)
+| loc(i,δ) = lᵢ
+| val(i,δ) = vᵢ+δ
+| state(i,δ) = (loc,val)
+** Automa di Buchi
+A = <S, ∑, Δ, F>
+- S: insieme degli stati
+- ∑: alfabeto
+- Δ: ⊂ S×∑×S
+- F: multiset stati accentanti
+run accettante: lim(run(A))= {q| q si ripete infinite volte}
+∀Fᵢ∈F: Fᵢ∩lim(run) ≠ ∅
diff --git a/todo.org b/todo.org
index aa56e6e..57a266d 100644
--- a/todo.org
+++ b/todo.org
@@ -1,13 +1,13 @@
-* TODO VPC [23/24]
-- [-] Teoria [31/36]
-  - [ ] PN consistente?
-  - [ ] vedi perche \neg\models != \models\neg
+* TODO VPC [24/24]
+- [X] Teoria [36/36]
+  - [X] PN consistente?
+  - [X] vedi perche \neg\models != \models\neg
+  - [X] fai buchi
+  - [X] Vedi step semantic e enabling degree
   - [X] Pronuncia / nome P_m(S)
   - [X] In ctl come dico:  M,s ⊧ φ if ∀σ| σ₀ = s, σ ⊧ φ (ogni path
-  - [ ] ripeti fairness
-  - [ ] fai buchi
+  - [X] ripeti fairness
   - [X] fai equivalenze
-  - [ ] Vedi step semantic e enabling degree
   - [X] Come metti a parole \to ?
   - [X] Hierarchy of equivalences
   - [X] Automa di Buchi