adding support for partially quantified lemmas

src/simplifying/fol/ht.rs

@@ -112,7 +112,7 @@ fn remove_idempotences(formula: Formula) -> Formula {
     }
 }
 
-fn join_nested_quantifiers(formula: Formula) -> Formula {
+pub(crate) fn join_nested_quantifiers(formula: Formula) -> Formula {
     // Remove nested quantifiers
     // e.g. q X ( q Y F(X,Y) ) => q X Y F(X,Y)
 

src/syntax_tree/fol.rs

@@ -11,6 +11,7 @@ use {
             TheoryParser, UnaryConnectiveParser, UnaryOperatorParser, UserGuideEntryParser,
             UserGuideParser, VariableParser,
         },
+        simplifying::fol::ht::join_nested_quantifiers,
         syntax_tree::{impl_node, Node},
         verifying::problem,
     },
@@ -819,6 +820,10 @@ impl Formula {
         self.quantify(Quantifier::Forall, variables)
     }
 
+    pub fn universal_closure_with_quantifier_joining(self) -> Formula {
+        join_nested_quantifiers(self.universal_closure())
+    }
+
     pub fn rename_conflicting_symbols(self, possible_conflicts: &IndexSet<Predicate>) -> Formula {
         match self {
             Formula::AtomicFormula(a) => {
@@ -944,6 +949,15 @@ impl AnnotatedFormula {
         }
     }
 
+    pub fn universal_closure_with_quantifier_joining(&self) -> Self {
+        AnnotatedFormula {
+            role: self.role,
+            direction: self.direction,
+            name: self.name.clone(),
+            formula: self.formula.clone().universal_closure_with_quantifier_joining(),
+        }
+    }
+
     pub fn replace_placeholders(mut self, mapping: &IndexMap<String, FunctionConstant>) -> Self {
         self.formula = self.formula.replace_placeholders(mapping);
         self

src/verifying/outline/mod.rs

@@ -337,7 +337,7 @@ impl ProofOutline {
             match anf.role {
                 fol::Role::Lemma | fol::Role::InductiveLemma => {
                     let general_lemma: GeneralLemma = anf
-                        .universal_closure()
+                        .universal_closure_with_quantifier_joining()
                         .replace_placeholders(placeholders)
                         .try_into()?;
                     match anf.direction {