You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
This optimization can be applied at the Sigma^1_1 formula level. When n function quantifiers are all existential or all instance, and have the same arities bounds expressions, then we can combine them into a single function quantifier with an additional argument (bounded by n) selecting one of the n functions.
The text was updated successfully, but these errors were encountered:
morganthomas
changed the title
Optimization: combine like function quantifiers
Combine like function quantifiers
Nov 16, 2022
morganthomas
changed the title
Combine like function quantifiers
Optimization: Combine like function quantifiers
Nov 16, 2022
This optimization can be applied at the Sigma^1_1 formula level. When n function quantifiers are all existential or all instance, and have the same arities bounds expressions, then we can combine them into a single function quantifier with an additional argument (bounded by n) selecting one of the n functions.
The text was updated successfully, but these errors were encountered: