-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathDSR_ctx_1.bcc
More file actions
21 lines (21 loc) · 4.53 KB
/
DSR_ctx_1.bcc
File metadata and controls
21 lines (21 loc) · 4.53 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
<?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;de.prob.symbolic.ctxBase">
<org.eventb.core.scExtendsContext name="'" org.eventb.core.scTarget="/DSR2/DSR_ctx_0.bcc|org.eventb.core.scContextFile#DSR_ctx_0" org.eventb.core.source="/DSR2/DSR_ctx_1.buc|org.eventb.core.contextFile#DSR_ctx_1|org.eventb.core.extendsContext#'"/>
<org.eventb.core.scInternalContext name="DSR_ctx_0">
<org.eventb.core.scAxiom name="'" org.eventb.core.label="axm1" org.eventb.core.predicate="finite(NOEUDS)" org.eventb.core.source="/DSR2/DSR_ctx_0.buc|org.eventb.core.contextFile#DSR_ctx_0|org.eventb.core.axiom#(" org.eventb.core.theorem="false"/>
<org.eventb.core.scAxiom name="(" org.eventb.core.label="axm2" org.eventb.core.predicate="card(NOEUDS)=4" org.eventb.core.source="/DSR2/DSR_ctx_0.buc|org.eventb.core.contextFile#DSR_ctx_0|org.eventb.core.axiom#)" org.eventb.core.theorem="false"/>
<org.eventb.core.scAxiom name=")" org.eventb.core.label="axm3" org.eventb.core.predicate="finite(DONNEES)" org.eventb.core.source="/DSR2/DSR_ctx_0.buc|org.eventb.core.contextFile#DSR_ctx_0|org.eventb.core.axiom#+" org.eventb.core.theorem="false"/>
<org.eventb.core.scCarrierSet name="DONNEES" org.eventb.core.source="/DSR2/DSR_ctx_0.buc|org.eventb.core.contextFile#DSR_ctx_0|org.eventb.core.carrierSet#*" org.eventb.core.type="ℙ(DONNEES)"/>
<org.eventb.core.scCarrierSet name="NOEUDS" org.eventb.core.source="/DSR2/DSR_ctx_0.buc|org.eventb.core.contextFile#DSR_ctx_0|org.eventb.core.carrierSet#'" org.eventb.core.type="ℙ(NOEUDS)"/>
</org.eventb.core.scInternalContext>
<org.eventb.core.scAxiom name="DSR_ctx_1" org.eventb.core.label="axm1" org.eventb.core.predicate="ROUTES={r⦂ℙ(NOEUDS×NOEUDS)·r∈NOEUDS ⤔ NOEUDS∧finite(r)∧r∩(id ⦂ ℙ(NOEUDS×NOEUDS))=(∅ ⦂ ℙ(NOEUDS×NOEUDS))∧(r=(∅ ⦂ ℙ(NOEUDS×NOEUDS))∨(∃d⦂NOEUDS,a⦂NOEUDS·d∈dom(r)∧a∈ran(r)∧dom(r) ∖ {d}=ran(r) ∖ {a}))∧(∀s⦂ℙ(NOEUDS)·s⊆dom(r)∧s≠(∅ ⦂ ℙ(NOEUDS))⇒(∃n⦂NOEUDS·n∈s∧r(n)∉s)) ∣ r}" org.eventb.core.source="/DSR2/DSR_ctx_1.buc|org.eventb.core.contextFile#DSR_ctx_1|org.eventb.core.axiom#)" org.eventb.core.theorem="false"/>
<org.eventb.core.scAxiom name="DSR_ctx_2" org.eventb.core.label="axm13" org.eventb.core.predicate="(∅ ⦂ ℙ(NOEUDS×NOEUDS))∈ROUTES" org.eventb.core.source="/DSR2/DSR_ctx_1.buc|org.eventb.core.contextFile#DSR_ctx_1|org.eventb.core.axiom#8" org.eventb.core.theorem="false"/>
<org.eventb.core.scAxiom name="DSR_ctx_3" org.eventb.core.label="axm6" org.eventb.core.predicate="finite(ROUTES)" org.eventb.core.source="/DSR2/DSR_ctx_1.buc|org.eventb.core.contextFile#DSR_ctx_1|org.eventb.core.axiom#1" org.eventb.core.theorem="false"/>
<org.eventb.core.scAxiom name="DSR_ctx_4" org.eventb.core.label="axm7" org.eventb.core.predicate="⊤" org.eventb.core.source="/DSR2/DSR_ctx_1.buc|org.eventb.core.contextFile#DSR_ctx_1|org.eventb.core.axiom#2" org.eventb.core.theorem="false"/>
<org.eventb.core.scAxiom name="DSR_ctx_5" org.eventb.core.label="axm8" org.eventb.core.predicate="⊤" org.eventb.core.source="/DSR2/DSR_ctx_1.buc|org.eventb.core.contextFile#DSR_ctx_1|org.eventb.core.axiom#3" org.eventb.core.theorem="false"/>
<org.eventb.core.scAxiom name="DSR_ctx_6" org.eventb.core.label="axm9" org.eventb.core.predicate="⊤" org.eventb.core.source="/DSR2/DSR_ctx_1.buc|org.eventb.core.contextFile#DSR_ctx_1|org.eventb.core.axiom#4" org.eventb.core.theorem="false"/>
<org.eventb.core.scAxiom name="DSR_ctx_7" org.eventb.core.label="axm10" org.eventb.core.predicate="⊤" org.eventb.core.source="/DSR2/DSR_ctx_1.buc|org.eventb.core.contextFile#DSR_ctx_1|org.eventb.core.axiom#5" org.eventb.core.theorem="false"/>
<org.eventb.core.scAxiom name="DSR_ctx_8" org.eventb.core.label="axm11" org.eventb.core.predicate="⊤" org.eventb.core.source="/DSR2/DSR_ctx_1.buc|org.eventb.core.contextFile#DSR_ctx_1|org.eventb.core.axiom#6" org.eventb.core.theorem="false"/>
<org.eventb.core.scAxiom name="DSR_ctx_9" org.eventb.core.label="axm12" org.eventb.core.predicate="⊤" org.eventb.core.source="/DSR2/DSR_ctx_1.buc|org.eventb.core.contextFile#DSR_ctx_1|org.eventb.core.axiom#7" org.eventb.core.theorem="false"/>
<org.eventb.core.scConstant de.prob.symbolic.symbolicAttribute="false" name="ROUTES" org.eventb.core.source="/DSR2/DSR_ctx_1.buc|org.eventb.core.contextFile#DSR_ctx_1|org.eventb.core.constant#(" org.eventb.core.type="ℙ(ℙ(NOEUDS×NOEUDS))"/>
</org.eventb.core.scContextFile>