Dynamic-Source-Routing-Protocol/DSR_ctx_0.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
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.poFile org.eventb.core.poStamp="7">
    <org.eventb.core.poPredicateSet name="ABSHYP" org.eventb.core.poStamp="0">
        <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.poPredicateSet>
    <org.eventb.core.poSequent name="axm2/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Axiom" org.eventb.core.poStamp="0">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/DSR2/DSR_ctx_0.bpo|org.eventb.core.poFile#DSR_ctx_0|org.eventb.core.poPredicateSet#HYP'"/>
        <org.eventb.core.poPredicate name="SEQHYQ" 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.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/DSR2/DSR_ctx_0.buc|org.eventb.core.contextFile#DSR_ctx_0|org.eventb.core.axiom#)"/>
        <org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/DSR2/DSR_ctx_0.bpo|org.eventb.core.poFile#DSR_ctx_0|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poSelHintSnd="/DSR2/DSR_ctx_0.bpo|org.eventb.core.poFile#DSR_ctx_0|org.eventb.core.poPredicateSet#HYP'"/>
    </org.eventb.core.poSequent>
    <org.eventb.core.poPredicateSet name="HYP'" org.eventb.core.parentSet="/DSR2/DSR_ctx_0.bpo|org.eventb.core.poFile#DSR_ctx_0|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poStamp="0">
        <org.eventb.core.poPredicate name="PRD0" 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.poPredicateSet>
    <org.eventb.core.poPredicateSet name="ALLHYP" org.eventb.core.parentSet="/DSR2/DSR_ctx_0.bpo|org.eventb.core.poFile#DSR_ctx_0|org.eventb.core.poPredicateSet#HYP'" org.eventb.core.poStamp="7">
        <org.eventb.core.poPredicate name="PRD1" 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="PRD2" 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.poPredicateSet>
</org.eventb.core.poFile>