Add basic tests for binder-forall equivalence.

sybila · Dec 19, 2023 · 1384bd4 · 1384bd4
1 parent 23c2c9d
commit 1384bd4
Showing 1 changed file with 6 additions and 0 deletions.
diff --git 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 {