[Simplification request] Top-level existential elimination

[PetarMax]

Simplification

Existential quantification in top-level positive constraints can be eliminated and the bound variables can be replaced with some fresh variables.

Example: #Exists X. { P(X) } => P(X0), for some X0 fresh.

I am assuming that this is a sound simplification when doing matching-logic proofs since it is sound when doing first-order logic proofs, and matching logic captures first-order logic.

This simplification cannot be applied under negation.

[ana-pantilie]

This could be part of

haskell-backend/kore/src/Kore/Simplify/Condition.hs

Line 167 in ac0e3c0

simplifyPredicates sideCondition original = do

. For each top level predicate, check if it has (multiple) exists at the top, remove the exists and refresh the bound variables.

[ana-pantilie]

https://github.com/runtimeverification/haskell-backend/blob/master/kore/src/Kore/Variables/Fresh.hs for refreshing variables