<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.prFile version="1">
    <org.eventb.core.prProof name="SUBMIT_CC_TX/inv14/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
        <org.eventb.core.lang name="L"/>
        <org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
            <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p1">
                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p1" org.eventb.core.prHyps=""/>
            </org.eventb.core.prAnte>
        </org.eventb.core.prRule>
        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="⊤"/>
        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="0∈{0,1}"/>
        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
    </org.eventb.core.prProof>
    <org.eventb.core.prProof name="SUBMIT_CC_TX/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
        <org.eventb.core.lang name="L"/>
        <org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
            <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p1">
                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p1" org.eventb.core.prHyps=""/>
            </org.eventb.core.prAnte>
        </org.eventb.core.prRule>
        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="⊤"/>
        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="1∈{0,1}"/>
        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
    </org.eventb.core.prProof>
    <org.eventb.core.prProof name="INITIALISATION/inv11/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
        <org.eventb.core.lang name="L"/>
        <org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
            <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p1">
                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p1" org.eventb.core.prHyps=""/>
            </org.eventb.core.prAnte>
        </org.eventb.core.prRule>
        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="⊤"/>
        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="0∈{0,1}"/>
        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
    </org.eventb.core.prProof>
    <org.eventb.core.prProof name="INITIALISATION/inv12/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
        <org.eventb.core.lang name="L"/>
        <org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
            <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p1">
                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p1" org.eventb.core.prHyps=""/>
            </org.eventb.core.prAnte>
        </org.eventb.core.prRule>
        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="⊤"/>
        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="0∈{0,1}"/>
        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
    </org.eventb.core.prProof>
    <org.eventb.core.prProof name="INITIALISATION/inv13/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
        <org.eventb.core.lang name="L"/>
        <org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
            <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p1">
                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p1" org.eventb.core.prHyps=""/>
            </org.eventb.core.prAnte>
        </org.eventb.core.prRule>
        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="⊤"/>
        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="0∈{0,1}"/>
        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
    </org.eventb.core.prProof>
    <org.eventb.core.prProof name="INITIALISATION/inv14/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
        <org.eventb.core.lang name="L"/>
        <org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
            <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p1">
                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p1" org.eventb.core.prHyps=""/>
            </org.eventb.core.prAnte>
        </org.eventb.core.prRule>
        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="⊤"/>
        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="0∈{0,1}"/>
        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
    </org.eventb.core.prProof>
    <org.eventb.core.prProof name="INITIALISATION/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
        <org.eventb.core.lang name="L"/>
        <org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
            <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p1">
                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p1" org.eventb.core.prHyps=""/>
            </org.eventb.core.prAnte>
        </org.eventb.core.prRule>
        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="⊤"/>
        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="0∈{0,1}"/>
        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
    </org.eventb.core.prProof>
    <org.eventb.core.prProof name="SUBSCRIBE_SMART_CONTRACT_EVENTS/inv11/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
        <org.eventb.core.lang name="L"/>
        <org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
            <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p3">
                <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p1" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p2"/>
                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p3" org.eventb.core.prHyps=""/>
            </org.eventb.core.prAnte>
        </org.eventb.core.prRule>
        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="gateway ↦ source_smart_contract∉subscriptions">
            <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
            <org.eventb.core.prIdent name="GATEWAYS" org.eventb.core.type="ℙ(GATEWAYS)"/>
            <org.eventb.core.prIdent name="gateway" org.eventb.core.type="GATEWAYS"/>
            <org.eventb.core.prIdent name="source_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
            <org.eventb.core.prIdent name="subscriptions" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_SMART_CONTRACTS)"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="⊤"/>
        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="¬gateway ↦ source_smart_contract∈subscriptions">
            <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
            <org.eventb.core.prIdent name="GATEWAYS" org.eventb.core.type="ℙ(GATEWAYS)"/>
            <org.eventb.core.prIdent name="gateway" org.eventb.core.type="GATEWAYS"/>
            <org.eventb.core.prIdent name="source_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
            <org.eventb.core.prIdent name="subscriptions" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_SMART_CONTRACTS)"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="1∈{0,1}"/>
        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
    </org.eventb.core.prProof>
    <org.eventb.core.prProof name="INITIATE_CC_TX/inv12/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
        <org.eventb.core.lang name="L"/>
        <org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
            <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p3">
                <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p1" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p2"/>
                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p3" org.eventb.core.prHyps=""/>
            </org.eventb.core.prAnte>
        </org.eventb.core.prRule>
        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="⊤"/>
        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="¬transaction∈received_transactions[{source_smart_contract}]">
            <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
            <org.eventb.core.prIdent name="TRANSACTIONS" org.eventb.core.type="ℙ(TRANSACTIONS)"/>
            <org.eventb.core.prIdent name="received_transactions" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×TRANSACTIONS)"/>
            <org.eventb.core.prIdent name="source_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
            <org.eventb.core.prIdent name="transaction" org.eventb.core.type="TRANSACTIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="transaction∉received_transactions[{source_smart_contract}]">
            <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
            <org.eventb.core.prIdent name="TRANSACTIONS" org.eventb.core.type="ℙ(TRANSACTIONS)"/>
            <org.eventb.core.prIdent name="received_transactions" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×TRANSACTIONS)"/>
            <org.eventb.core.prIdent name="source_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
            <org.eventb.core.prIdent name="transaction" org.eventb.core.type="TRANSACTIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="1∈{0,1}"/>
        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
    </org.eventb.core.prProof>
    <org.eventb.core.prProof name="TRIGGER_CC_TX_EVENT/inv12/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
        <org.eventb.core.lang name="L"/>
        <org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
            <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p3">
                <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p1" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p2"/>
                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p3" org.eventb.core.prHyps=""/>
            </org.eventb.core.prAnte>
        </org.eventb.core.prRule>
        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="⊤"/>
        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="¬cross_chain_event∈triggered_events[{source_smart_contract}]">
            <org.eventb.core.prIdent name="CROSS_CHAIN_EVENTS" org.eventb.core.type="ℙ(CROSS_CHAIN_EVENTS)"/>
            <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
            <org.eventb.core.prIdent name="cross_chain_event" org.eventb.core.type="CROSS_CHAIN_EVENTS"/>
            <org.eventb.core.prIdent name="source_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
            <org.eventb.core.prIdent name="triggered_events" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_EVENTS)"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="cross_chain_event∉triggered_events[{source_smart_contract}]">
            <org.eventb.core.prIdent name="CROSS_CHAIN_EVENTS" org.eventb.core.type="ℙ(CROSS_CHAIN_EVENTS)"/>
            <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
            <org.eventb.core.prIdent name="cross_chain_event" org.eventb.core.type="CROSS_CHAIN_EVENTS"/>
            <org.eventb.core.prIdent name="source_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
            <org.eventb.core.prIdent name="triggered_events" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_EVENTS)"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="0∈{0,1}"/>
        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
    </org.eventb.core.prProof>
    <org.eventb.core.prProof name="TRIGGER_CC_TX_EVENT/inv13/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
        <org.eventb.core.lang name="L"/>
        <org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
            <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p3">
                <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p1" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p2"/>
                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p3" org.eventb.core.prHyps=""/>
            </org.eventb.core.prAnte>
        </org.eventb.core.prRule>
        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="⊤"/>
        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="¬cross_chain_event∈triggered_events[{source_smart_contract}]">
            <org.eventb.core.prIdent name="CROSS_CHAIN_EVENTS" org.eventb.core.type="ℙ(CROSS_CHAIN_EVENTS)"/>
            <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
            <org.eventb.core.prIdent name="cross_chain_event" org.eventb.core.type="CROSS_CHAIN_EVENTS"/>
            <org.eventb.core.prIdent name="source_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
            <org.eventb.core.prIdent name="triggered_events" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_EVENTS)"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="cross_chain_event∉triggered_events[{source_smart_contract}]">
            <org.eventb.core.prIdent name="CROSS_CHAIN_EVENTS" org.eventb.core.type="ℙ(CROSS_CHAIN_EVENTS)"/>
            <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
            <org.eventb.core.prIdent name="cross_chain_event" org.eventb.core.type="CROSS_CHAIN_EVENTS"/>
            <org.eventb.core.prIdent name="source_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
            <org.eventb.core.prIdent name="triggered_events" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_EVENTS)"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="1∈{0,1}"/>
        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
    </org.eventb.core.prProof>
    <org.eventb.core.prProof name="LISTEN_CC_TX_EVENT/inv13/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
        <org.eventb.core.lang name="L"/>
        <org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
            <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p3">
                <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p1" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p2"/>
                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p3" org.eventb.core.prHyps=""/>
            </org.eventb.core.prAnte>
        </org.eventb.core.prRule>
        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="⊤"/>
        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="gateway ↦ cross_chain_transaction∉gateway_pending_transactions">
            <org.eventb.core.prIdent name="CROSS_CHAIN_TRANSACTIONS" org.eventb.core.type="ℙ(CROSS_CHAIN_TRANSACTIONS)"/>
            <org.eventb.core.prIdent name="GATEWAYS" org.eventb.core.type="ℙ(GATEWAYS)"/>
            <org.eventb.core.prIdent name="cross_chain_transaction" org.eventb.core.type="CROSS_CHAIN_TRANSACTIONS"/>
            <org.eventb.core.prIdent name="gateway" org.eventb.core.type="GATEWAYS"/>
            <org.eventb.core.prIdent name="gateway_pending_transactions" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_TRANSACTIONS)"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="¬gateway ↦ cross_chain_transaction∈gateway_pending_transactions">
            <org.eventb.core.prIdent name="CROSS_CHAIN_TRANSACTIONS" org.eventb.core.type="ℙ(CROSS_CHAIN_TRANSACTIONS)"/>
            <org.eventb.core.prIdent name="GATEWAYS" org.eventb.core.type="ℙ(GATEWAYS)"/>
            <org.eventb.core.prIdent name="cross_chain_transaction" org.eventb.core.type="CROSS_CHAIN_TRANSACTIONS"/>
            <org.eventb.core.prIdent name="gateway" org.eventb.core.type="GATEWAYS"/>
            <org.eventb.core.prIdent name="gateway_pending_transactions" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_TRANSACTIONS)"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="0∈{0,1}"/>
        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
    </org.eventb.core.prProof>
    <org.eventb.core.prProof name="LISTEN_CC_TX_EVENT/inv14/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
        <org.eventb.core.lang name="L"/>
        <org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
            <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p3">
                <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p1" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p2"/>
                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p3" org.eventb.core.prHyps=""/>
            </org.eventb.core.prAnte>
        </org.eventb.core.prRule>
        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="⊤"/>
        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="gateway ↦ cross_chain_transaction∉gateway_pending_transactions">
            <org.eventb.core.prIdent name="CROSS_CHAIN_TRANSACTIONS" org.eventb.core.type="ℙ(CROSS_CHAIN_TRANSACTIONS)"/>
            <org.eventb.core.prIdent name="GATEWAYS" org.eventb.core.type="ℙ(GATEWAYS)"/>
            <org.eventb.core.prIdent name="cross_chain_transaction" org.eventb.core.type="CROSS_CHAIN_TRANSACTIONS"/>
            <org.eventb.core.prIdent name="gateway" org.eventb.core.type="GATEWAYS"/>
            <org.eventb.core.prIdent name="gateway_pending_transactions" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_TRANSACTIONS)"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="¬gateway ↦ cross_chain_transaction∈gateway_pending_transactions">
            <org.eventb.core.prIdent name="CROSS_CHAIN_TRANSACTIONS" org.eventb.core.type="ℙ(CROSS_CHAIN_TRANSACTIONS)"/>
            <org.eventb.core.prIdent name="GATEWAYS" org.eventb.core.type="ℙ(GATEWAYS)"/>
            <org.eventb.core.prIdent name="cross_chain_transaction" org.eventb.core.type="CROSS_CHAIN_TRANSACTIONS"/>
            <org.eventb.core.prIdent name="gateway" org.eventb.core.type="GATEWAYS"/>
            <org.eventb.core.prIdent name="gateway_pending_transactions" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_TRANSACTIONS)"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="1∈{0,1}"/>
        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
    </org.eventb.core.prProof>
    <org.eventb.core.prProof name="INITIATE_CC_TX/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
        <org.eventb.core.lang name="L"/>
        <org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
            <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p3">
                <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p1" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p2"/>
                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p3" org.eventb.core.prHyps=""/>
            </org.eventb.core.prAnte>
        </org.eventb.core.prRule>
        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="⊤"/>
        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="¬transaction∈received_transactions[{source_smart_contract}]">
            <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
            <org.eventb.core.prIdent name="TRANSACTIONS" org.eventb.core.type="ℙ(TRANSACTIONS)"/>
            <org.eventb.core.prIdent name="received_transactions" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×TRANSACTIONS)"/>
            <org.eventb.core.prIdent name="source_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
            <org.eventb.core.prIdent name="transaction" org.eventb.core.type="TRANSACTIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="transaction∉received_transactions[{source_smart_contract}]">
            <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
            <org.eventb.core.prIdent name="TRANSACTIONS" org.eventb.core.type="ℙ(TRANSACTIONS)"/>
            <org.eventb.core.prIdent name="received_transactions" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×TRANSACTIONS)"/>
            <org.eventb.core.prIdent name="source_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
            <org.eventb.core.prIdent name="transaction" org.eventb.core.type="TRANSACTIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="0∈{0,1}"/>
        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
    </org.eventb.core.prProof>
    <org.eventb.core.prProof name="TRIGGER_CC_TX_EVENT/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
        <org.eventb.core.lang name="L"/>
        <org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
            <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p3">
                <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p1" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p2"/>
                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p3" org.eventb.core.prHyps=""/>
            </org.eventb.core.prAnte>
        </org.eventb.core.prRule>
        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="⊤"/>
        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="¬cross_chain_event∈triggered_events[{source_smart_contract}]">
            <org.eventb.core.prIdent name="CROSS_CHAIN_EVENTS" org.eventb.core.type="ℙ(CROSS_CHAIN_EVENTS)"/>
            <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
            <org.eventb.core.prIdent name="cross_chain_event" org.eventb.core.type="CROSS_CHAIN_EVENTS"/>
            <org.eventb.core.prIdent name="source_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
            <org.eventb.core.prIdent name="triggered_events" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_EVENTS)"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="cross_chain_event∉triggered_events[{source_smart_contract}]">
            <org.eventb.core.prIdent name="CROSS_CHAIN_EVENTS" org.eventb.core.type="ℙ(CROSS_CHAIN_EVENTS)"/>
            <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
            <org.eventb.core.prIdent name="cross_chain_event" org.eventb.core.type="CROSS_CHAIN_EVENTS"/>
            <org.eventb.core.prIdent name="source_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
            <org.eventb.core.prIdent name="triggered_events" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_EVENTS)"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="0∈{0,1}"/>
        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
    </org.eventb.core.prProof>
    <org.eventb.core.prProof name="LISTEN_CC_TX_EVENT/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
        <org.eventb.core.lang name="L"/>
        <org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
            <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p3">
                <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p1" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p2"/>
                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p3" org.eventb.core.prHyps=""/>
            </org.eventb.core.prAnte>
        </org.eventb.core.prRule>
        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="⊤"/>
        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="gateway ↦ cross_chain_transaction∉gateway_pending_transactions">
            <org.eventb.core.prIdent name="CROSS_CHAIN_TRANSACTIONS" org.eventb.core.type="ℙ(CROSS_CHAIN_TRANSACTIONS)"/>
            <org.eventb.core.prIdent name="GATEWAYS" org.eventb.core.type="ℙ(GATEWAYS)"/>
            <org.eventb.core.prIdent name="cross_chain_transaction" org.eventb.core.type="CROSS_CHAIN_TRANSACTIONS"/>
            <org.eventb.core.prIdent name="gateway" org.eventb.core.type="GATEWAYS"/>
            <org.eventb.core.prIdent name="gateway_pending_transactions" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_TRANSACTIONS)"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="¬gateway ↦ cross_chain_transaction∈gateway_pending_transactions">
            <org.eventb.core.prIdent name="CROSS_CHAIN_TRANSACTIONS" org.eventb.core.type="ℙ(CROSS_CHAIN_TRANSACTIONS)"/>
            <org.eventb.core.prIdent name="GATEWAYS" org.eventb.core.type="ℙ(GATEWAYS)"/>
            <org.eventb.core.prIdent name="cross_chain_transaction" org.eventb.core.type="CROSS_CHAIN_TRANSACTIONS"/>
            <org.eventb.core.prIdent name="gateway" org.eventb.core.type="GATEWAYS"/>
            <org.eventb.core.prIdent name="gateway_pending_transactions" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_TRANSACTIONS)"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="0∈{0,1}"/>
        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
    </org.eventb.core.prProof>
    <org.eventb.core.prProof name="EMIT_CC_TX_EVENT/inv12/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
        <org.eventb.core.lang name="L"/>
        <org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
            <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p3">
                <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p1" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p2"/>
                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p3" org.eventb.core.prHyps=""/>
            </org.eventb.core.prAnte>
        </org.eventb.core.prRule>
        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="emitted_event∉emitted_events[{source_smart_contract}]">
            <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
            <org.eventb.core.prIdent name="EVENTS" org.eventb.core.type="ℙ(EVENTS)"/>
            <org.eventb.core.prIdent name="emitted_event" org.eventb.core.type="EVENTS"/>
            <org.eventb.core.prIdent name="emitted_events" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×EVENTS)"/>
            <org.eventb.core.prIdent name="source_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="⊤"/>
        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="0∈{0,1}"/>
        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="¬emitted_event∈emitted_events[{source_smart_contract}]">
            <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
            <org.eventb.core.prIdent name="EVENTS" org.eventb.core.type="ℙ(EVENTS)"/>
            <org.eventb.core.prIdent name="emitted_event" org.eventb.core.type="EVENTS"/>
            <org.eventb.core.prIdent name="emitted_events" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×EVENTS)"/>
            <org.eventb.core.prIdent name="source_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
    </org.eventb.core.prProof>
    <org.eventb.core.prProof name="EMIT_CC_TX_EVENT/inv13/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
        <org.eventb.core.lang name="L"/>
        <org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
            <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p3">
                <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p1" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p2"/>
                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p3" org.eventb.core.prHyps=""/>
            </org.eventb.core.prAnte>
        </org.eventb.core.prRule>
        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="emitted_event∉emitted_events[{source_smart_contract}]">
            <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
            <org.eventb.core.prIdent name="EVENTS" org.eventb.core.type="ℙ(EVENTS)"/>
            <org.eventb.core.prIdent name="emitted_event" org.eventb.core.type="EVENTS"/>
            <org.eventb.core.prIdent name="emitted_events" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×EVENTS)"/>
            <org.eventb.core.prIdent name="source_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="⊤"/>
        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="1∈{0,1}"/>
        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="¬emitted_event∈emitted_events[{source_smart_contract}]">
            <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
            <org.eventb.core.prIdent name="EVENTS" org.eventb.core.type="ℙ(EVENTS)"/>
            <org.eventb.core.prIdent name="emitted_event" org.eventb.core.type="EVENTS"/>
            <org.eventb.core.prIdent name="emitted_events" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×EVENTS)"/>
            <org.eventb.core.prIdent name="source_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
    </org.eventb.core.prProof>
    <org.eventb.core.prProof name="EMIT_CC_TX_EVENT/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
        <org.eventb.core.lang name="L"/>
        <org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
            <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p3">
                <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p1" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p2"/>
                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p3" org.eventb.core.prHyps=""/>
            </org.eventb.core.prAnte>
        </org.eventb.core.prRule>
        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="emitted_event∉emitted_events[{source_smart_contract}]">
            <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
            <org.eventb.core.prIdent name="EVENTS" org.eventb.core.type="ℙ(EVENTS)"/>
            <org.eventb.core.prIdent name="emitted_event" org.eventb.core.type="EVENTS"/>
            <org.eventb.core.prIdent name="emitted_events" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×EVENTS)"/>
            <org.eventb.core.prIdent name="source_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="⊤"/>
        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="0∈{0,1}"/>
        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="¬emitted_event∈emitted_events[{source_smart_contract}]">
            <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
            <org.eventb.core.prIdent name="EVENTS" org.eventb.core.type="ℙ(EVENTS)"/>
            <org.eventb.core.prIdent name="emitted_event" org.eventb.core.type="EVENTS"/>
            <org.eventb.core.prIdent name="emitted_events" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×EVENTS)"/>
            <org.eventb.core.prIdent name="source_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
    </org.eventb.core.prProof>
    <org.eventb.core.prProof name="EMIT_EVENT/inv12/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
        <org.eventb.core.lang name="L"/>
        <org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
            <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p3">
                <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p1" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p2"/>
                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p3" org.eventb.core.prHyps=""/>
            </org.eventb.core.prAnte>
        </org.eventb.core.prRule>
        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="emitted_event∉emitted_events[{source_smart_contract}]">
            <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
            <org.eventb.core.prIdent name="EVENTS" org.eventb.core.type="ℙ(EVENTS)"/>
            <org.eventb.core.prIdent name="emitted_event" org.eventb.core.type="EVENTS"/>
            <org.eventb.core.prIdent name="emitted_events" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×EVENTS)"/>
            <org.eventb.core.prIdent name="source_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="⊤"/>
        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="0∈{0,1}"/>
        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="¬emitted_event∈emitted_events[{source_smart_contract}]">
            <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
            <org.eventb.core.prIdent name="EVENTS" org.eventb.core.type="ℙ(EVENTS)"/>
            <org.eventb.core.prIdent name="emitted_event" org.eventb.core.type="EVENTS"/>
            <org.eventb.core.prIdent name="emitted_events" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×EVENTS)"/>
            <org.eventb.core.prIdent name="source_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
    </org.eventb.core.prProof>
    <org.eventb.core.prProof name="EMIT_EVENT/inv13/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
        <org.eventb.core.lang name="L"/>
        <org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
            <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p3">
                <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p1" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p2"/>
                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p3" org.eventb.core.prHyps=""/>
            </org.eventb.core.prAnte>
        </org.eventb.core.prRule>
        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="emitted_event∉emitted_events[{source_smart_contract}]">
            <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
            <org.eventb.core.prIdent name="EVENTS" org.eventb.core.type="ℙ(EVENTS)"/>
            <org.eventb.core.prIdent name="emitted_event" org.eventb.core.type="EVENTS"/>
            <org.eventb.core.prIdent name="emitted_events" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×EVENTS)"/>
            <org.eventb.core.prIdent name="source_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="⊤"/>
        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="1∈{0,1}"/>
        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="¬emitted_event∈emitted_events[{source_smart_contract}]">
            <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
            <org.eventb.core.prIdent name="EVENTS" org.eventb.core.type="ℙ(EVENTS)"/>
            <org.eventb.core.prIdent name="emitted_event" org.eventb.core.type="EVENTS"/>
            <org.eventb.core.prIdent name="emitted_events" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×EVENTS)"/>
            <org.eventb.core.prIdent name="source_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
    </org.eventb.core.prProof>
    <org.eventb.core.prProof name="EMIT_EVENT/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
        <org.eventb.core.lang name="L"/>
        <org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
            <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p3">
                <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p1" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p2"/>
                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p3" org.eventb.core.prHyps=""/>
            </org.eventb.core.prAnte>
        </org.eventb.core.prRule>
        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="emitted_event∉emitted_events[{source_smart_contract}]">
            <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
            <org.eventb.core.prIdent name="EVENTS" org.eventb.core.type="ℙ(EVENTS)"/>
            <org.eventb.core.prIdent name="emitted_event" org.eventb.core.type="EVENTS"/>
            <org.eventb.core.prIdent name="emitted_events" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×EVENTS)"/>
            <org.eventb.core.prIdent name="source_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="⊤"/>
        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="0∈{0,1}"/>
        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="¬emitted_event∈emitted_events[{source_smart_contract}]">
            <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
            <org.eventb.core.prIdent name="EVENTS" org.eventb.core.type="ℙ(EVENTS)"/>
            <org.eventb.core.prIdent name="emitted_event" org.eventb.core.type="EVENTS"/>
            <org.eventb.core.prIdent name="emitted_events" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×EVENTS)"/>
            <org.eventb.core.prIdent name="source_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
    </org.eventb.core.prProof>
    <org.eventb.core.prProof name="LISTEN_EVENT/inv13/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
        <org.eventb.core.lang name="L"/>
        <org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
            <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p3">
                <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p1" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p2"/>
                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p3" org.eventb.core.prHyps=""/>
            </org.eventb.core.prAnte>
        </org.eventb.core.prRule>
        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="⊤"/>
        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="gateway ↦ pending_event∉gateway_pending_events">
            <org.eventb.core.prIdent name="GATEWAYS" org.eventb.core.type="ℙ(GATEWAYS)"/>
            <org.eventb.core.prIdent name="TARGET_TRANSACTIONS" org.eventb.core.type="ℙ(TARGET_TRANSACTIONS)"/>
            <org.eventb.core.prIdent name="gateway" org.eventb.core.type="GATEWAYS"/>
            <org.eventb.core.prIdent name="gateway_pending_events" org.eventb.core.type="ℙ(GATEWAYS×TARGET_TRANSACTIONS)"/>
            <org.eventb.core.prIdent name="pending_event" org.eventb.core.type="TARGET_TRANSACTIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="0∈{0,1}"/>
        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="¬gateway ↦ pending_event∈gateway_pending_events">
            <org.eventb.core.prIdent name="GATEWAYS" org.eventb.core.type="ℙ(GATEWAYS)"/>
            <org.eventb.core.prIdent name="TARGET_TRANSACTIONS" org.eventb.core.type="ℙ(TARGET_TRANSACTIONS)"/>
            <org.eventb.core.prIdent name="gateway" org.eventb.core.type="GATEWAYS"/>
            <org.eventb.core.prIdent name="gateway_pending_events" org.eventb.core.type="ℙ(GATEWAYS×TARGET_TRANSACTIONS)"/>
            <org.eventb.core.prIdent name="pending_event" org.eventb.core.type="TARGET_TRANSACTIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
    </org.eventb.core.prProof>
    <org.eventb.core.prProof name="LISTEN_EVENT/inv14/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
        <org.eventb.core.lang name="L"/>
        <org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
            <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p3">
                <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p1" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p2"/>
                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p3" org.eventb.core.prHyps=""/>
            </org.eventb.core.prAnte>
        </org.eventb.core.prRule>
        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="⊤"/>
        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="gateway ↦ pending_event∉gateway_pending_events">
            <org.eventb.core.prIdent name="GATEWAYS" org.eventb.core.type="ℙ(GATEWAYS)"/>
            <org.eventb.core.prIdent name="TARGET_TRANSACTIONS" org.eventb.core.type="ℙ(TARGET_TRANSACTIONS)"/>
            <org.eventb.core.prIdent name="gateway" org.eventb.core.type="GATEWAYS"/>
            <org.eventb.core.prIdent name="gateway_pending_events" org.eventb.core.type="ℙ(GATEWAYS×TARGET_TRANSACTIONS)"/>
            <org.eventb.core.prIdent name="pending_event" org.eventb.core.type="TARGET_TRANSACTIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="1∈{0,1}"/>
        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="¬gateway ↦ pending_event∈gateway_pending_events">
            <org.eventb.core.prIdent name="GATEWAYS" org.eventb.core.type="ℙ(GATEWAYS)"/>
            <org.eventb.core.prIdent name="TARGET_TRANSACTIONS" org.eventb.core.type="ℙ(TARGET_TRANSACTIONS)"/>
            <org.eventb.core.prIdent name="gateway" org.eventb.core.type="GATEWAYS"/>
            <org.eventb.core.prIdent name="gateway_pending_events" org.eventb.core.type="ℙ(GATEWAYS×TARGET_TRANSACTIONS)"/>
            <org.eventb.core.prIdent name="pending_event" org.eventb.core.type="TARGET_TRANSACTIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
    </org.eventb.core.prProof>
    <org.eventb.core.prProof name="LISTEN_EVENT/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
        <org.eventb.core.lang name="L"/>
        <org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
            <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p3">
                <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p1" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p2"/>
                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p3" org.eventb.core.prHyps=""/>
            </org.eventb.core.prAnte>
        </org.eventb.core.prRule>
        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="⊤"/>
        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="gateway ↦ pending_event∉gateway_pending_events">
            <org.eventb.core.prIdent name="GATEWAYS" org.eventb.core.type="ℙ(GATEWAYS)"/>
            <org.eventb.core.prIdent name="TARGET_TRANSACTIONS" org.eventb.core.type="ℙ(TARGET_TRANSACTIONS)"/>
            <org.eventb.core.prIdent name="gateway" org.eventb.core.type="GATEWAYS"/>
            <org.eventb.core.prIdent name="gateway_pending_events" org.eventb.core.type="ℙ(GATEWAYS×TARGET_TRANSACTIONS)"/>
            <org.eventb.core.prIdent name="pending_event" org.eventb.core.type="TARGET_TRANSACTIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="0∈{0,1}"/>
        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="¬gateway ↦ pending_event∈gateway_pending_events">
            <org.eventb.core.prIdent name="GATEWAYS" org.eventb.core.type="ℙ(GATEWAYS)"/>
            <org.eventb.core.prIdent name="TARGET_TRANSACTIONS" org.eventb.core.type="ℙ(TARGET_TRANSACTIONS)"/>
            <org.eventb.core.prIdent name="gateway" org.eventb.core.type="GATEWAYS"/>
            <org.eventb.core.prIdent name="gateway_pending_events" org.eventb.core.type="ℙ(GATEWAYS×TARGET_TRANSACTIONS)"/>
            <org.eventb.core.prIdent name="pending_event" org.eventb.core.type="TARGET_TRANSACTIONS"/>
        </org.eventb.core.prPred>
        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
    </org.eventb.core.prProof>
    <org.eventb.core.prProof name="SUBMIT_TX/inv14/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
        <org.eventb.core.lang name="L"/>
        <org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
            <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p1">
                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p1" org.eventb.core.prHyps=""/>
            </org.eventb.core.prAnte>
        </org.eventb.core.prRule>
        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="⊤"/>
        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="0∈{0,1}"/>
        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
    </org.eventb.core.prProof>
    <org.eventb.core.prProof name="SUBMIT_TX/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
        <org.eventb.core.lang name="L"/>
        <org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
            <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p1">
                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p1" org.eventb.core.prHyps=""/>
            </org.eventb.core.prAnte>
        </org.eventb.core.prRule>
        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="⊤"/>
        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="1∈{0,1}"/>
        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
    </org.eventb.core.prProof>
</org.eventb.core.prFile>