DSR_ctx_1.buc

<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.contextFile org.eventb.core.configuration="org.eventb.core.fwd;de.prob.symbolic.ctxBase" version="3">
    <org.eventb.core.extendsContext name="'" org.eventb.core.target="DSR_ctx_0"/>
    <org.eventb.core.constant de.prob.symbolic.symbolicAttribute="false" name="(" org.eventb.core.identifier="ROUTES"/>
    <org.eventb.core.axiom name=")" org.eventb.core.label="axm1" org.eventb.core.predicate="ROUTES =&#10;          { r ∣&#10;              r ∈ NOEUDS ⤔ NOEUDS ∧&#10;              finite(r) ∧&#10;              r ∩ id = ∅ ∧&#10;&#9;&#9;&#9;  (r=∅∨∃d,a·d∈dom(r)∧a∈ran(r)∧(dom(r)∖{d})=(ran(r)∖{a})) ∧&#10;&#9;&#9;&#9;  (∀s·s⊆dom(r)∧s≠∅⇒∃n·n∈s∧r(n)∉s)&#10;          }"/>
    <org.eventb.core.axiom name="8" org.eventb.core.label="axm13" org.eventb.core.predicate="∅∈ROUTES"/>
    <org.eventb.core.axiom name="1" org.eventb.core.label="axm6" org.eventb.core.predicate="finite(ROUTES)"/>
    <org.eventb.core.axiom name="2" org.eventb.core.comment="iter∈(NOEUDS↔NOEUDS)×ℕ→(NOEUDS↔NOEUDS)" org.eventb.core.label="axm7" org.eventb.core.predicate="⊤"/>
    <org.eventb.core.axiom name="3" org.eventb.core.comment="iter(ROUTES↦1)=ROUTES" org.eventb.core.label="axm8" org.eventb.core.predicate="⊤"/>
    <org.eventb.core.axiom name="4" org.eventb.core.comment="∀n·n∈ℕ⇒iter(Route↦(n+1)) = Route; iter(Route↦n)" org.eventb.core.label="axm9" org.eventb.core.predicate="⊤"/>
    <org.eventb.core.axiom name="5" org.eventb.core.comment="iclosure ∈ ((NOEUDS↔NOEUDS) → (NOEUDS↔NOEUDS))" org.eventb.core.label="axm10" org.eventb.core.predicate="⊤"/>
    <org.eventb.core.axiom name="6" org.eventb.core.comment="iclosure(Route) = (⋃n·(n∈ℕ1)∣ iter(Route↦n))" org.eventb.core.label="axm11" org.eventb.core.predicate="⊤"/>
    <org.eventb.core.axiom name="7" org.eventb.core.comment="∀r,s·r∈ROUTES∧s⊆dom(r)∧s≠∅⇒(∃n·n∈s⇒r(n)∉s)" org.eventb.core.label="axm12" org.eventb.core.predicate="⊤"/>
</org.eventb.core.contextFile>