-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathContext.bcc
9 lines (9 loc) · 1.53 KB
/
Context.bcc
1
2
3
4
5
6
7
8
9
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.scContextFile org.eventb.core.accurate="true" org.eventb.core.configuration="org.eventb.core.fwd">
<org.eventb.core.scAxiom name="'" org.eventb.core.label="axm1" 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.theorem="false"/>
<org.eventb.core.scAxiom name="(" org.eventb.core.label="axm2" 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.theorem="false"/>
<org.eventb.core.scAxiom name=")" org.eventb.core.label="axm3" 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.theorem="false"/>
<org.eventb.core.scCarrierSet name="GROUPS" org.eventb.core.source="/TestRBAC/Context.buc|org.eventb.core.contextFile#Context|org.eventb.core.carrierSet#(" org.eventb.core.type="ℙ(GROUPS)"/>
<org.eventb.core.scCarrierSet name="USERS" org.eventb.core.source="/TestRBAC/Context.buc|org.eventb.core.contextFile#Context|org.eventb.core.carrierSet#'" org.eventb.core.type="ℙ(USERS)"/>
<org.eventb.core.scConstant name="IdPath" org.eventb.core.source="/TestRBAC/Context.buc|org.eventb.core.contextFile#Context|org.eventb.core.constant#+" org.eventb.core.type="ℙ(ℤ×GROUPS)"/>
</org.eventb.core.scContextFile>