Examples of the implementation of strongly cantorian domains

- 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]]