Skip to content
Snippets Groups Projects
Normal view Permalink
BIG_m1.bpo 21.2 KiB
Newer Older
Guzmán Llambías's avatar
Initial specification of big
Guzmán Llambías committed
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 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.poFile org.eventb.core.poStamp="116">
    <org.eventb.core.poPredicateSet name="CTXHYP" org.eventb.core.poStamp="113">
        <org.eventb.core.poIdentifier name="CROSS_CHAIN_EVENTS" org.eventb.core.type="ℙ(CROSS_CHAIN_EVENTS)"/>
        <org.eventb.core.poIdentifier name="CROSS_CHAIN_TRANSACTIONS" org.eventb.core.type="ℙ(CROSS_CHAIN_TRANSACTIONS)"/>
        <org.eventb.core.poIdentifier name="GATEWAYS" org.eventb.core.type="ℙ(GATEWAYS)"/>
        <org.eventb.core.poIdentifier name="TRANSACTIONS" org.eventb.core.type="ℙ(TRANSACTIONS)"/>
        <org.eventb.core.poIdentifier name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
        <org.eventb.core.poIdentifier name="source_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
        <org.eventb.core.poIdentifier name="gateway" org.eventb.core.type="GATEWAYS"/>
        <org.eventb.core.poIdentifier name="target_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
        <org.eventb.core.poPredicate name="CROSS_CHAIN_SMART_CONTRACTT" org.eventb.core.predicate="source_smart_contract∈CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.source="/BIG/BIG_c1.buc|org.eventb.core.contextFile#BIG_c1|org.eventb.core.axiom#_j4-IUKsXEe6I4bA9GxwhqQ"/>
        <org.eventb.core.poPredicate name="CROSS_CHAIN_SMART_CONTRACTU" org.eventb.core.predicate="target_smart_contract∈CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.source="/BIG/BIG_c1.buc|org.eventb.core.contextFile#BIG_c1|org.eventb.core.axiom#_j4-vYKsXEe6I4bA9GxwhqQ"/>
        <org.eventb.core.poPredicate name="CROSS_CHAIN_SMART_CONTRACTV" org.eventb.core.predicate="gateway∈GATEWAYS" org.eventb.core.source="/BIG/BIG_c1.buc|org.eventb.core.contextFile#BIG_c1|org.eventb.core.axiom#_j4-vYasXEe6I4bA9GxwhqQ"/>
    </org.eventb.core.poPredicateSet>
    <org.eventb.core.poPredicateSet name="ABSHYP" org.eventb.core.parentSet="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poStamp="116">
        <org.eventb.core.poIdentifier name="triggered_events" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_EVENTS)"/>
        <org.eventb.core.poIdentifier name="received_cross_chain_transactions" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_TRANSACTIONS)"/>
        <org.eventb.core.poIdentifier name="gateway_pending_transactions" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_TRANSACTIONS)"/>
        <org.eventb.core.poIdentifier name="received_transactions" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×TRANSACTIONS)"/>
    </org.eventb.core.poPredicateSet>
    <org.eventb.core.poSequent name="INITIALISATION/inv11;/INV" org.eventb.core.accurate="false" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="116">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#EVTALLHYPreceived_cross_chain_transactiont"/>
        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="(∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×TRANSACTIONS))∈CROSS_CHAIN_SMART_CONTRACTS ↠ TRANSACTIONS" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_asVK0KvhEe6I4bA9GxwhqQ"/>
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#'"/>
        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_asVK0KvhEe6I4bA9GxwhqQ"/>
        <org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poSequent#INITIALISATION\/inv11;\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD0"/>
    </org.eventb.core.poSequent>
    <org.eventb.core.poSequent name="INITIALISATION/inv2;/INV" org.eventb.core.accurate="false" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="116">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#EVTALLHYPreceived_cross_chain_transactiont"/>
        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="(∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_EVENTS))∈CROSS_CHAIN_SMART_CONTRACTS ↠ CROSS_CHAIN_EVENTS" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_d6dcQKmHEe6I4bA9GxwhqQ"/>
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#'"/>
        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_d6dcQKmHEe6I4bA9GxwhqQ"/>
        <org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poSequent#INITIALISATION\/inv2;\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD1"/>
    </org.eventb.core.poSequent>
    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_cross_chain_transactiont" org.eventb.core.parentSet="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poStamp="116">
        <org.eventb.core.poIdentifier name="triggered_events'" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_EVENTS)"/>
        <org.eventb.core.poIdentifier name="gateway_pending_transactions'" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_TRANSACTIONS)"/>
        <org.eventb.core.poIdentifier name="received_transactions'" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×TRANSACTIONS)"/>
        <org.eventb.core.poIdentifier name="received_cross_chain_transactions'" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_TRANSACTIONS)"/>
    </org.eventb.core.poPredicateSet>
    <org.eventb.core.poPredicateSet name="EVTALLHYPreceived_cross_chain_transactiont" org.eventb.core.parentSet="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#EVTIDENTreceived_cross_chain_transactiont" org.eventb.core.poStamp="116"/>
    <org.eventb.core.poPredicateSet name="EVTALLHYPreceived_cross_chain_transactionu" org.eventb.core.parentSet="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="116"/>
    <org.eventb.core.poSequent name="SUBMIT_CROSS_CHAIN_TRANSACTION/inv11;/INV" org.eventb.core.accurate="false" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="116">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#EVTALLHYPreceived_cross_chain_transactionv"/>
        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="received_transactions∪{source_smart_contract ↦ transaction}∈CROSS_CHAIN_SMART_CONTRACTS ↠ TRANSACTIONS" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_asVK0KvhEe6I4bA9GxwhqQ"/>
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_58YTEKmAEe6I4bA9GxwhqQ"/>
        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_asVK0KvhEe6I4bA9GxwhqQ"/>
        <org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poSequent#SUBMIT_CROSS_CHAIN_TRANSACTION\/inv11;\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD0"/>
    </org.eventb.core.poSequent>
    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_cross_chain_transactionv" org.eventb.core.parentSet="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="116">
        <org.eventb.core.poIdentifier name="transaction" org.eventb.core.type="TRANSACTIONS"/>
        <org.eventb.core.poIdentifier name="received_transactions'" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×TRANSACTIONS)"/>
    </org.eventb.core.poPredicateSet>
    <org.eventb.core.poPredicateSet name="EVTALLHYPreceived_cross_chain_transactionv" org.eventb.core.parentSet="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#EVTIDENTreceived_cross_chain_transactionv" org.eventb.core.poStamp="116">
        <org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="transaction∈TRANSACTIONS" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_58YTEKmAEe6I4bA9GxwhqQ|org.eventb.core.guard#_TlWCkqmHEe6I4bA9GxwhqQ"/>
        <org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="transaction∉received_transactions[{source_smart_contract}]" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_58YTEKmAEe6I4bA9GxwhqQ|org.eventb.core.guard#_HCtL8KmIEe6I4bA9GxwhqQ"/>
    </org.eventb.core.poPredicateSet>
    <org.eventb.core.poSequent name="PROCESS_CROSS_CHAIN_TRANSACTION/inv11;/INV" org.eventb.core.accurate="false" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="116">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#EVTALLHYPreceived_cross_chain_transactionw"/>
        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="received_transactions ∖ {source_smart_contract ↦ transaction}∈CROSS_CHAIN_SMART_CONTRACTS ↠ TRANSACTIONS" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_asVK0KvhEe6I4bA9GxwhqQ"/>
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_TlWCkKmHEe6I4bA9GxwhqQ"/>
        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_asVK0KvhEe6I4bA9GxwhqQ"/>
        <org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poSequent#PROCESS_CROSS_CHAIN_TRANSACTION\/inv11;\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD0"/>
    </org.eventb.core.poSequent>
    <org.eventb.core.poSequent name="PROCESS_CROSS_CHAIN_TRANSACTION/inv2;/INV" org.eventb.core.accurate="false" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="116">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#EVTALLHYPreceived_cross_chain_transactionw"/>
        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="triggered_events∪{source_smart_contract ↦ cross_chain_event}∈CROSS_CHAIN_SMART_CONTRACTS ↠ CROSS_CHAIN_EVENTS" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_d6dcQKmHEe6I4bA9GxwhqQ"/>
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_TlWCkKmHEe6I4bA9GxwhqQ"/>
        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_d6dcQKmHEe6I4bA9GxwhqQ"/>
        <org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poSequent#PROCESS_CROSS_CHAIN_TRANSACTION\/inv2;\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD1"/>
    </org.eventb.core.poSequent>
    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_cross_chain_transactionw" org.eventb.core.parentSet="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="116">
        <org.eventb.core.poIdentifier name="triggered_events'" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_EVENTS)"/>
        <org.eventb.core.poIdentifier name="transaction" org.eventb.core.type="TRANSACTIONS"/>
        <org.eventb.core.poIdentifier name="cross_chain_event" org.eventb.core.type="CROSS_CHAIN_EVENTS"/>
        <org.eventb.core.poIdentifier name="received_transactions'" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×TRANSACTIONS)"/>
    </org.eventb.core.poPredicateSet>
    <org.eventb.core.poPredicateSet name="EVTALLHYPreceived_cross_chain_transactionw" org.eventb.core.parentSet="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#EVTIDENTreceived_cross_chain_transactionw" org.eventb.core.poStamp="116">
        <org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="source_smart_contract ↦ transaction∈received_transactions" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_TlWCkKmHEe6I4bA9GxwhqQ|org.eventb.core.guard#_iUmtQKpAEe6I4bA9GxwhqQ"/>
        <org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="cross_chain_event∉triggered_events[{source_smart_contract}]" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_TlWCkKmHEe6I4bA9GxwhqQ|org.eventb.core.guard#_1SOwwKmDEe6I4bA9GxwhqQ"/>
    </org.eventb.core.poPredicateSet>
    <org.eventb.core.poSequent name="LISTEN_SMART_CONTRACT_EVENT/inv2;/INV" org.eventb.core.accurate="false" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="116">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#EVTALLHYPreceived_cross_chain_transactionx"/>
        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="triggered_events ∖ {source_smart_contract ↦ cross_chain_event}∈CROSS_CHAIN_SMART_CONTRACTS ↠ CROSS_CHAIN_EVENTS" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_d6dcQKmHEe6I4bA9GxwhqQ"/>
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_8VKFEKpAEe6I4bA9GxwhqQ"/>
        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_d6dcQKmHEe6I4bA9GxwhqQ"/>
        <org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poSequent#LISTEN_SMART_CONTRACT_EVENT\/inv2;\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD1"/>
    </org.eventb.core.poSequent>
    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_cross_chain_transactionx" org.eventb.core.parentSet="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="116">
        <org.eventb.core.poIdentifier name="cross_chain_transaction" org.eventb.core.type="CROSS_CHAIN_TRANSACTIONS"/>
        <org.eventb.core.poIdentifier name="triggered_events'" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_EVENTS)"/>
        <org.eventb.core.poIdentifier name="gateway_pending_transactions'" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_TRANSACTIONS)"/>
        <org.eventb.core.poIdentifier name="cross_chain_event" org.eventb.core.type="CROSS_CHAIN_EVENTS"/>
    </org.eventb.core.poPredicateSet>
    <org.eventb.core.poPredicateSet name="EVTALLHYPreceived_cross_chain_transactionx" org.eventb.core.parentSet="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#EVTIDENTreceived_cross_chain_transactionx" org.eventb.core.poStamp="116">
        <org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="source_smart_contract ↦ cross_chain_event∈triggered_events" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_8VKFEKpAEe6I4bA9GxwhqQ|org.eventb.core.guard#_DMOGsKpFEe6I4bA9GxwhqQ"/>
        <org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="gateway ↦ cross_chain_transaction∉gateway_pending_transactions" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_8VKFEKpAEe6I4bA9GxwhqQ|org.eventb.core.guard#_x51DwKpCEe6I4bA9GxwhqQ"/>
    </org.eventb.core.poPredicateSet>
    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_cross_chain_transactiony" org.eventb.core.parentSet="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="116">
        <org.eventb.core.poIdentifier name="cross_chain_transaction" org.eventb.core.type="CROSS_CHAIN_TRANSACTIONS"/>
        <org.eventb.core.poIdentifier name="gateway_pending_transactions'" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_TRANSACTIONS)"/>
        <org.eventb.core.poIdentifier name="received_cross_chain_transactions'" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_TRANSACTIONS)"/>
    </org.eventb.core.poPredicateSet>
    <org.eventb.core.poPredicateSet name="EVTALLHYPreceived_cross_chain_transactiony" org.eventb.core.parentSet="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#EVTIDENTreceived_cross_chain_transactiony" org.eventb.core.poStamp="116">
        <org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="gateway ↦ cross_chain_transaction∈gateway_pending_transactions" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_0sEN8KpaEe6I4bA9GxwhqQ|org.eventb.core.guard#_tUzFcKpaEe6I4bA9GxwhqQ"/>
    </org.eventb.core.poPredicateSet>
    <org.eventb.core.poPredicateSet name="ALLHYP" org.eventb.core.parentSet="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poStamp="116">
        <org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="received_transactions∈CROSS_CHAIN_SMART_CONTRACTS ↠ TRANSACTIONS" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_asVK0KvhEe6I4bA9GxwhqQ"/>
        <org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="triggered_events∈CROSS_CHAIN_SMART_CONTRACTS ↠ CROSS_CHAIN_EVENTS" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_d6dcQKmHEe6I4bA9GxwhqQ"/>
        <org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="gateway_pending_transactions∈GATEWAYS ↔ CROSS_CHAIN_TRANSACTIONS" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_c7TQ0KpBEe6I4bA9GxwhqQ"/>
        <org.eventb.core.poPredicate name="PRD3" org.eventb.core.predicate="received_cross_chain_transactions∈CROSS_CHAIN_SMART_CONTRACTS ↔ CROSS_CHAIN_TRANSACTIONS" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_G1eDUKpbEe6I4bA9GxwhqQ"/>
    </org.eventb.core.poPredicateSet>
</org.eventb.core.poFile>