proof outlines for strong equivalence

src/command_line/procedures.rs

@@ -199,6 +199,10 @@ pub fn main() -> Result<()> {
                             .right()
                             .ok_or(anyhow!("no right program was provided"))?,
                     )?,
+                    proof_outline: files
+                        .proof_outline()
+                        .map(fol::Specification::from_file)
+                        .unwrap_or_else(|| Ok(fol::Specification::empty()))?,
                     decomposition,
                     formula_representation,
                     direction,

src/syntax_tree/fol.rs

@@ -13,6 +13,7 @@ use {
         },
         simplifying::fol::intuitionistic::join_nested_quantifiers,
         syntax_tree::{Node, impl_node},
+        translating::gamma::gamma_formula,
         verifying::problem,
     },
     clap::ValueEnum,
@@ -1071,6 +1072,15 @@ impl AnnotatedFormula {
         self.formula = self.formula.replace_placeholders(mapping);
         self
     }
+
+    pub fn apply_gamma_reduction(self) -> Self {
+        AnnotatedFormula {
+            role: self.role,
+            direction: self.direction,
+            name: self.name,
+            formula: gamma_formula(self.formula),
+        }
+    }
 }
 
 #[derive(Clone, Debug, Eq, PartialEq, Hash, IntoIterator)]

src/verifying/outline/mod.rs

@@ -22,6 +22,28 @@ pub struct GeneralLemma {
     pub consequences: Vec<problem::AnnotatedFormula>,
 }
 
+// Apply the gamma transformation to every formula in conjectures and consequences
+impl GeneralLemma {
+    pub fn apply_gamma_reduction(self) -> GeneralLemma {
+        let conjectures = self
+            .conjectures
+            .into_iter()
+            .map(|f| f.apply_gamma_reduction())
+            .collect();
+
+        let consequences = self
+            .consequences
+            .into_iter()
+            .map(|f| f.apply_gamma_reduction())
+            .collect();
+
+        GeneralLemma {
+            conjectures,
+            consequences,
+        }
+    }
+}
+
 impl TryFrom<fol::AnnotatedFormula> for GeneralLemma {
     type Error = ProofOutlineError;
 
@@ -393,6 +415,36 @@ impl ProofOutline {
         })
         .preface_warnings(warnings))
     }
+
+    pub fn apply_gamma_reduction(self) -> Self {
+        let forward_lemmas = self
+            .forward_lemmas
+            .into_iter()
+            .map(|l| l.apply_gamma_reduction())
+            .collect();
+        let backward_lemmas = self
+            .backward_lemmas
+            .into_iter()
+            .map(|l| l.apply_gamma_reduction())
+            .collect();
+        let forward_definitions = self
+            .forward_definitions
+            .into_iter()
+            .map(|d| d.apply_gamma_reduction())
+            .collect();
+        let backward_definitions = self
+            .backward_definitions
+            .into_iter()
+            .map(|d| d.apply_gamma_reduction())
+            .collect();
+
+        ProofOutline {
+            forward_lemmas,
+            backward_lemmas,
+            forward_definitions,
+            backward_definitions,
+        }
+    }
 }
 
 #[cfg(test)]

src/verifying/problem/mod.rs

@@ -2,6 +2,7 @@ use {
     crate::{
         command_line::arguments::Decomposition,
         syntax_tree::fol::{Formula, FunctionConstant, Predicate, Sort, Theory},
+        translating::gamma::gamma_formula,
     },
     anyhow::{Context as _, Result},
     indexmap::IndexSet,
@@ -62,6 +63,14 @@ impl AnnotatedFormula {
             formula: self.formula.rename_conflicting_symbols(possible_conflicts),
         }
     }
+
+    pub fn apply_gamma_reduction(self) -> Self {
+        AnnotatedFormula {
+            name: self.name,
+            role: self.role,
+            formula: gamma_formula(self.formula),
+        }
+    }
 }
 
 impl fmt::Display for AnnotatedFormula {