- declareconstant "bool"; (* attaching a type label to the inner quantified statement in the term with nested quantifiers that caused problems above causes the prover to be able to stratify it *) - s "forall@[bool:forsome@[?1=?2]]"; (* the bool type label can be defined in such a way as to make the following "axioms" easily proved theorems *) - axiom "FORALLBOOL" "forall@?x" "bool:forall@?x"; - axiom "FORSOMEBOOL" "forsome@?x" "bool:forsome@?x"; (* the theorems FORALLBOOL, FORSOMEBOOL witness the fact that the functions forall, forsome have output of boolean type, thus are "scout" *) - makescout "forall" "FORALLBOOL"; - makescout "forsome" "FORSOMEBOOL"; - s "forall@[forsome@[?1=?2]]"; (* the information that forall and forsome are scout is enough to allow this term to be stratified; it removes any problem of stratification due to nested quantifiers *) {forall @ [forsome @ [?1 = ?2]]} (* no error message! *) forall @ [forsome @ [?1 = ?2]]