Context.bpo

<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.poFile org.eventb.core.poStamp="0">
    <org.eventb.core.poPredicateSet name="ABSHYP" org.eventb.core.poStamp="0">
        <org.eventb.core.poIdentifier name="GROUPS" org.eventb.core.type="ℙ(GROUPS)"/>
        <org.eventb.core.poIdentifier name="USERS" org.eventb.core.type="ℙ(USERS)"/>
        <org.eventb.core.poIdentifier name="IdPath" org.eventb.core.type="ℙ(ℤ×GROUPS)"/>
    </org.eventb.core.poPredicateSet>
    <org.eventb.core.poPredicateSet name="ALLHYP" org.eventb.core.parentSet="/TestRBAC/Context.bpo|org.eventb.core.poFile#Context|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poStamp="0">
        <org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="finite(USERS)" org.eventb.core.source="/TestRBAC/Context.buc|org.eventb.core.contextFile#Context|org.eventb.core.axiom#)"/>
        <org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="finite(GROUPS)" org.eventb.core.source="/TestRBAC/Context.buc|org.eventb.core.contextFile#Context|org.eventb.core.axiom#*"/>
        <org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="IdPath∈ℕ → GROUPS" org.eventb.core.source="/TestRBAC/Context.buc|org.eventb.core.contextFile#Context|org.eventb.core.axiom#,"/>
    </org.eventb.core.poPredicateSet>
</org.eventb.core.poFile>