Previous topic  Top  Next topic  Print this Topic
 

Forall-Closing

 

If a top level ObjectLogic formula F has free variables, the transformation forall-closes the transformed formula. If F has an id or annotations, they apply to the forall-closed formula.  On the other hand, the re-transformation removes unnecessary forall-quantifiers on the top level of formulas and maps the id and annotations to the resulting formula.