The command abstract implements an abstract compiler for PVS assertions based on boolean abstractions. It then invokes the basic command abs-simp which implements the abstract compiler. The command abs-simp assumes that all definitions have been rewritten. This allows a more efficient computation of the abstraction. The parameter proof-counter indicates the maximal number of calls to the decision procedure when abstracting each atom of the sequent.
Any number allows to compute a faithful abstraction.
However, it is preferable that the number is at least equal twice the length of the list of predicates. In this case the original goal is returned. P is not a predicate. Predicate P has free variables. State predicates have different domains.