From 1384bd4766a179c2faf9fdbb50efc43171d72295 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ond=C5=99ej=20Huvar?= <492849@mail.muni.cz>
Date: Tue, 19 Dec 2023 10:49:49 +0100
Subject: [PATCH] Add basic tests for binder-forall equivalence.

---
 src/model_checking.rs | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/src/model_checking.rs b/src/model_checking.rs
index 1ae6ee7..e5e87c4 100644
--- a/src/model_checking.rs
+++ b/src/model_checking.rs
@@ -493,6 +493,12 @@ $DivK: (!PleC & DivJ)
                 "~(3{x}: 3{y}: (@{x}: ~{y} & AX {x}) & (@{y}: AX {y}))",
                 "V{x}: V{y}: (@{x}: {y} | ~(!{z}: AX {z})) | (@{y}: ~(!{z}: AX {z}))",
             ),
+            // binder and forall equivalence v1
+            ("!{x}: AG EF {x}", "V{x}: ({x} => (AG EF {x}))"),
+            // binder and forall equivalence v2
+            ("!{x}: AX {x}", "V{x}: ({x} => (AX {x}))"),
+            // binder and forall equivalence v3
+            ("!{x}: AF {x}", "V{x}: ({x} => (AF {x}))"),
         ];
 
         for (formula1, formula2) in equivalent_formulae_pairs {