Add more info in the readme

README.md

@@ -1,8 +1,10 @@
-# mambo
+# Mambo
+
+This was my weekend turned a bit more project from Christmas, really fun thinking thingy, would be interesting to show the relation to other similar systems as LTL and CTL.
 
 ## Resources used
 - https://vcvpaiva.github.io/includes/pubs/2011-Basic_Constructive_Modality.pdf
 - https://arxiv.org/html/2408.16428v1
-- https://www.sciencedirect.com/science/article/pii/S157106611000037X?ref=pdf_download&fr=RR-2&rr=9b2f4a90ee93dc47
+- https://www.sciencedirect.com/science/article/pii/S157106611000037X
 - https://builds.openlogicproject.org/courses/boxes-and-diamonds/bd-screen.pdf
 - https://www.cambridge.org/us/universitypress/subjects/computer-science/programming-languages-and-applied-logic/logic-computer-science-modelling-and-reasoning-about-systems-2nd-edition?format=PB&isbn=9780521543101

mambo.agda

@@ -185,20 +185,20 @@ inBoth {A} {Γ} {Γ'} {X} x {X₁} (zero x₁ xs) = zero X Γ'
 inBoth {A} {Γ} {Γ'} {X} x {X₁} (succ x₁ xs x₂) = succ X₁ Γ' (x x₂)
 
 weak : Δ / Γ ⊢ A → Γ ⊆ Γ' → Δ / Γ' ⊢ A
-weak {Δ} {Γ} {A} {Γ'} (var x) x₁ = var (x₁ x)
-weak {Δ} {Γ} {A} {Γ'} (mp x x₂) x₁ = mp (weak x x₁) (weak x₂ x₁)
-weak {Δ} {Γ} {A} {Γ'} (∧ᵢ x x₂) x₁ = ∧ᵢ (weak x x₁) (weak x₂ x₁)
-weak {Δ} {Γ} {A} {Γ'} (∧ₑ₁ x) x₁ = ∧ₑ₁ (weak x x₁)
-weak {Δ} {Γ} {A} {Γ'} (∧ₑ₂ x) x₁ = ∧ₑ₂ (weak x x₁)
-weak {Δ} {Γ} {A} {Γ'} (∨ᵢ₁ x) x₁ = ∨ᵢ₁ (weak x x₁)
-weak {Δ} {Γ} {A} {Γ'} (∨ᵢ₂ x) x₁ = ∨ᵢ₂ (weak x x₁)
-weak {Δ} {Γ} {A} {Γ'} (∨ₑ x x₂ x₃) x₁ = ∨ₑ (weak x x₁) (weak x₂ (inBoth x₁)) (weak x₃ (inBoth x₁))
-weak {Δ} {Γ} {A} {Γ'} (⇒ᵢ x) x₁ = ⇒ᵢ (weak x (inBoth x₁))
-weak {Δ} {Γ} {A} {Γ'} (¬ᵢ x) x₁ = ¬ᵢ (weak x (inBoth x₁))
-weak {Δ} {Γ} {A} {Γ'} (¬ₑ x x₂) x₁ = ¬ₑ (weak x x₁) (weak x₂ x₁)
-weak {Δ} {Γ} {A} {Γ'} (⊥ₑ x) x₁ = ⊥ₑ (weak x x₁)
-weak {Δ} {Γ} {A} {Γ'} (□ᵢ x) x₁ = □ᵢ x
-weak {Δ} {Γ} {A} {Γ'} (□ₑ x x₂) x₁ = □ₑ (weak x x₁) (weak x₂ x₁)
+weak (var x) x₁ = var (x₁ x)
+weak (mp x x₂) x₁ = mp (weak x x₁) (weak x₂ x₁)
+weak (∧ᵢ x x₂) x₁ = ∧ᵢ (weak x x₁) (weak x₂ x₁)
+weak (∧ₑ₁ x) x₁ = ∧ₑ₁ (weak x x₁)
+weak (∧ₑ₂ x) x₁ = ∧ₑ₂ (weak x x₁)
+weak (∨ᵢ₁ x) x₁ = ∨ᵢ₁ (weak x x₁)
+weak (∨ᵢ₂ x) x₁ = ∨ᵢ₂ (weak x x₁)
+weak (∨ₑ x x₂ x₃) x₁ = ∨ₑ (weak x x₁) (weak x₂ (inBoth x₁)) (weak x₃ (inBoth x₁))
+weak (⇒ᵢ x) x₁ = ⇒ᵢ (weak x (inBoth x₁))
+weak (¬ᵢ x) x₁ = ¬ᵢ (weak x (inBoth x₁))
+weak (¬ₑ x x₂) x₁ = ¬ₑ (weak x x₁) (weak x₂ x₁)
+weak (⊥ₑ x) x₁ = ⊥ₑ (weak x x₁)
+weak (□ᵢ x) x₁ = □ᵢ x
+weak (□ₑ x x₂) x₁ = □ₑ (weak x x₁) (weak x₂ x₁)
 
 weak-modal : Δ / Γ ⊢ A → Δ ⊆ Δ' → Δ' / Γ ⊢ A
 weak-modal (var x) x₁ = var x
@@ -285,3 +285,25 @@ ExampleSyn3 {A} {B} = ⇒ᵢ (□ₑ (∧ₑ₁ (var (zero ((□ A) ∧ (□ B))
 ExampleSyn4 : ∙ / ∙ ⊢ □ (A ⇒ B) ⇒ (◇ A ⇒ ◇ B)
 ExampleSyn4 {A} {B} = ⇒ᵢ (⇒ᵢ (¬ᵢ (□ₑ (var (zero (□ (∼ B)) (∙ , (□ (A ⇒ B)) , (◇ A)))) (□ₑ (var (succ (□ (A ⇒ B)) (∙ , (□ (A ⇒ B)) , (◇ A)) (succ (□ (A ⇒ B)) (∙ , (□ (A ⇒ B))) (zero (□ (A ⇒ B)) ∙)))) (¬ₑ (var (succ (∼ (□ (∼ A))) (∙ , (□ (A ⇒ B)) , (◇ A))
                                                                                                                                                                                                                       (zero (∼ (□ (∼ A))) (∙ , (□ (A ⇒ B)))))) (□ᵢ (¬ᵢ (¬ₑ (var (succ ( ∼ B) (∙ , (∼ B) , (A ⇒ B)) (succ (∼ B) (∙ , (∼ B)) (zero (∼ B) ∙)))) (mp (var (succ (A ⇒ B) (∙ , (∼ B) , (A ⇒ B)) (zero (A ⇒ B) (∙ , (∼ B))))) (var (zero A (∙ , (∼ B) , (A ⇒ B)))))))))))))
+
+ExampleSyn5 : ∙ / ∙ ⊢ □ ( A ⇒ B ) ⇒ ( □ A ⇒ □ B )
+ExampleSyn5 {A} {B} = ⇒ᵢ (⇒ᵢ (□ₑ (var (zero (□ A) (∙ , (□ (A ⇒ B))))) (□ₑ (var (succ (□ (A ⇒ B)) (∙ , (□ (A ⇒ B))) (zero (□ (A ⇒ B)) ∙))) (□ᵢ (mp (var (zero (A ⇒ B) (∙ , A))) (var (succ A (∙ , A) (zero A ∙))))))))
+
+ExampleSyn6 : ∙ / ∙ ⊢ (◇ A) ⇔ (∼ □ ∼ A)
+ExampleSyn6 {A} = ∧ᵢ (⇒ᵢ (var (zero (∼ (□ (∼ A))) ∙))) (⇒ᵢ (var (zero (◇ A) ∙)))
+
+ExampleSyn7 : ∙ / ∙ ⊢ □ A ⇒ (◇ (A ⇒ B) ⇒ ◇ B)
+ExampleSyn7 {A} {B} = ⇒ᵢ (⇒ᵢ (□ₑ (var (succ (□ A) (∙ , (□ A)) (zero (□ A) ∙))) (¬ᵢ (□ₑ (var (zero (□ (∼ B)) (∙ , (□ A) , (◇ (A ⇒ B))))) (¬ₑ (var (succ (∼ (□ (∼ (A ⇒ B)))) (∙ , (□ A) , (◇ (A ⇒ B)))
+                                                                                                                                                   (zero (∼ (□ (∼ (A ⇒ B)))) (∙ , (□ A))))) (□ᵢ (¬ᵢ (¬ₑ (var (succ (∼ B) (∙ , A , (∼ B)) (zero (∼ B) (∙ , A)))) (mp (var (zero (A ⇒ B) (∙ , A , (∼ B)))) (var (succ A (∙ , A , (∼ B)) (succ A (∙ , A) (zero A ∙)))))))))))))
+
+ExampleSyn8 : ∙ / ∙ ⊢ □ ∼ A ⇒ □ (A ⇒ B)
+ExampleSyn8 {A} {B} = ⇒ᵢ (□ₑ (var (zero (□ (∼ A)) ∙)) (□ᵢ (⇒ᵢ (⊥ₑ (¬ₑ (var (succ (∼ A) (∙ , (∼ A)) (zero (∼ A) ∙))) (var (zero A (∙ , (∼ A)))))))))
+
+ExampleSyn9 : ∙ / ∙ ⊢ (□ A) ∨ (□ B) ⇒ □ (A ∨ B)
+ExampleSyn9 {A} {B} = ⇒ᵢ (∨ₑ (var (zero ((□ A) ∨ (□ B)) ∙)) (□ₑ (var (zero (□ A) (∙ , ((□ A) ∨ (□ B))))) (□ᵢ (∨ᵢ₁ (var (zero A ∙))))) (□ₑ (var (zero (□ B) (∙ , ((□ A) ∨ (□ B))))) (□ᵢ (∨ᵢ₂ (var (zero B ∙))))))
+
+ExampleSyn10 : ∙ / ∙ ⊢ ◇ A ⇒ ◇ (A ∨ B)
+ExampleSyn10 {A} {B} = ⇒ᵢ (¬ᵢ (□ₑ (var (zero (□ (∼ (A ∨ B))) (∙ , (◇ A)))) (¬ₑ (var (succ ( ◇ A) (∙ , (◇ A)) (zero (∼ (□ (∼ A))) ∙))) (□ᵢ (¬ᵢ (¬ₑ (var (succ (∼ (A ∨ B)) (∙ , (∼ (A ∨ B))) (zero (∼ (A ∨ B)) ∙))) (∨ᵢ₁ (var (zero A (∙ , (∼ (A ∨ B))))))))))))
+
+ExampleSyn11 : ∙ / ∙ ⊢ ◇ A ⇒ □ B ⇒ □ ( A ⇒ B )
+ExampleSyn11 {A} {B} = ⇒ᵢ (⇒ᵢ (□ₑ (var (zero (□ B) (∙ , (◇ A)))) (□ᵢ (⇒ᵢ (var (succ B (∙ , B) (zero B ∙)))))))