Remove todo

mambo.agda

@@ -30,7 +30,6 @@ data Formula : Type where
   ⊥ : Formula
   atom : Nat → Formula
   ∼_ : Formula → Formula
-  ◇_ : Formula → Formula
   □_ : Formula → Formula
   _∧_ : Formula → Formula → Formula
   _∨_ : Formula → Formula → Formula
@@ -47,6 +46,9 @@ X ⇔ Y = (X ⇒ Y) ∧ (Y ⇒ X)
 ⊤ : Formula
 ⊤ = ∼ ⊥
 
+◇_ : Formula → Formula
+◇ p = ∼ (□ (∼ p))
+
 infix 9 _∈_
 data _∈_ {A : Type} : A → List A → Type where
   zero : (x : A) (xs : List A) → x ∈ (x ∷ xs)
@@ -61,12 +63,12 @@ infix 2 _,_⊩_
 _,_⊩_ : {W : Type} (Model : M W) (x : W) (p : Formula) → Type 
 Model , x ⊩ ⊥ = Bottom
 Model , x ⊩ atom n = n ∈ M.L Model x
+Model , x ⊩ (∼ (□ (∼ p))) = ∃ λ y → M.R Model x y → Model , y ⊩ p -- Alias for ◇ p
 Model , x ⊩ (∼ p) = ¬ (Model , x ⊩ p)
 Model , x ⊩ (p ∧ q) = (Model , x ⊩ p) × (Model , x ⊩ q)
 Model , x ⊩ (p ∨ q) = (Model , x ⊩ p) ∪ (Model , x ⊩ q)
 Model , x ⊩ p ⇒ q = Model , x ⊩ p → Model , x ⊩ q
 Model , x ⊩ (□ p) = ∀ y → M.R Model x y → Model , y ⊩ p 
-Model , x ⊩ (◇ p) = ∃ λ y → M.R Model x y → Model , y ⊩ p
 
 data R : Nat → Nat → Type where
   zeroone : R 0 1
@@ -121,4 +123,3 @@ data _⊢_ : Context → Formula → Type where
   ¬ₑ : Γ ⊢ X → Γ ⊢ ∼ X → Γ ⊢ ⊥
   □ₑ : Γ ⊢ □ X → X ∈ Δ → Γ ++ boxed Δ ⊢ Y
   □ᵢ : X ∈ Δ → Γ ++ boxed Δ ⊢ □ X
-  -- TODO: Add ◇