Dynamic-Source-Routing-Protocol/DSR_ctx_2.bpo at main · alegoupil/Dynamic-Source-Routing-Protocol · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.poFile org.eventb.core.poStamp="12">
    <org.eventb.core.poPredicateSet name="ABSHYP" org.eventb.core.poStamp="10">
        <org.eventb.core.poIdentifier name="DONNEES" org.eventb.core.type="ℙ(DONNEES)"/>
        <org.eventb.core.poIdentifier name="NOEUDS" org.eventb.core.type="ℙ(NOEUDS)"/>
        <org.eventb.core.poPredicate name="DONNEET" 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.poPredicate name="DONNEEU" 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.poPredicate name="DONNEEV" 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.poIdentifier name="ROUTES" org.eventb.core.type="ℙ(ℙ(NOEUDS×NOEUDS))"/>
        <org.eventb.core.poPredicate name="DONNEEW" 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.poPredicate name="DONNEEX" 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.poPredicate name="DONNEEY" 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.poPredicate name="DONNEEZ" 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.poPredicate name="DONNEE[" 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.poPredicate name="DONNEE\" 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.poPredicate name="DONNEE]" 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.poPredicate name="DONNEE^" 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.poPredicate name="DONNEE_" 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.poIdentifier name="MaxSauts" org.eventb.core.type="ℤ"/>
    </org.eventb.core.poPredicateSet>
    <org.eventb.core.poPredicateSet name="ALLHYP" org.eventb.core.parentSet="/DSR2/DSR_ctx_2.bpo|org.eventb.core.poFile#DSR_ctx_2|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poStamp="12">
        <org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="MaxSauts∈ℕ" org.eventb.core.source="/DSR2/DSR_ctx_2.buc|org.eventb.core.contextFile#DSR_ctx_2|org.eventb.core.axiom#)"/>
        <org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="MaxSauts=2" org.eventb.core.source="/DSR2/DSR_ctx_2.buc|org.eventb.core.contextFile#DSR_ctx_2|org.eventb.core.axiom#*"/>
    </org.eventb.core.poPredicateSet>
</org.eventb.core.poFile>