Dynamic-Source-Routing-Protocol/DSR_ctx_1.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
26
27
28
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.poFile org.eventb.core.poStamp="66">
    <org.eventb.core.poPredicateSet name="ABSHYP" org.eventb.core.poStamp="66">
        <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.poPredicateSet>
    <org.eventb.core.poSequent name="axm1/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Axiom" org.eventb.core.poStamp="66">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/DSR2/DSR_ctx_1.bpo|org.eventb.core.poFile#DSR_ctx_1|org.eventb.core.poPredicateSet#ABSHYP"/>
        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="∀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⇒n∈dom(r)∧r∈NOEUDS ⇸ NOEUDS))" org.eventb.core.source="/DSR2/DSR_ctx_1.buc|org.eventb.core.contextFile#DSR_ctx_1|org.eventb.core.axiom#)"/>
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/DSR2/DSR_ctx_1.buc|org.eventb.core.contextFile#DSR_ctx_1|org.eventb.core.axiom#)"/>
        <org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/DSR2/DSR_ctx_1.bpo|org.eventb.core.poFile#DSR_ctx_1|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poSelHintSnd="/DSR2/DSR_ctx_1.bpo|org.eventb.core.poFile#DSR_ctx_1|org.eventb.core.poPredicateSet#ABSHYP"/>
    </org.eventb.core.poSequent>
    <org.eventb.core.poPredicateSet name="ALLHYP" org.eventb.core.parentSet="/DSR2/DSR_ctx_1.bpo|org.eventb.core.poFile#DSR_ctx_1|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poStamp="66">
        <org.eventb.core.poPredicate name="PRD0" 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="PRD1" 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="PRD2" 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="PRD3" 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="PRD4" 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="PRD5" 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="PRD6" 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="PRD7" 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="PRD8" 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.poPredicateSet>
</org.eventb.core.poFile>