Skip to content
Snippets Groups Projects
Normal view Permalink
CCTx_Abstract_Animation_m2.bpo 51.5 KiB
Newer Older
Guzman Llambias's avatar
Improve abstract machine animation
Guzman Llambias 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 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142 143 144 145 146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167 168 169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.poFile org.eventb.core.poStamp="3">
    <org.eventb.core.poPredicateSet name="CTXHYP" org.eventb.core.poStamp="0">
        <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="/gateway-event-b/CCTx_Abstract_DLT_c1.buc|org.eventb.core.contextFile#CCTx_Abstract_DLT_c1|org.eventb.core.axiom#_lhKcab7uEe6laZimEYihUg"/>
        <org.eventb.core.poPredicate name="CROSS_CHAIN_SMART_CONTRACTU" org.eventb.core.predicate="target_smart_contract∈CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_c1.buc|org.eventb.core.contextFile#CCTx_Abstract_DLT_c1|org.eventb.core.axiom#_lhKcar7uEe6laZimEYihUg"/>
        <org.eventb.core.poPredicate name="CROSS_CHAIN_SMART_CONTRACTV" org.eventb.core.predicate="gateway∈GATEWAYS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_c1.buc|org.eventb.core.contextFile#CCTx_Abstract_DLT_c1|org.eventb.core.axiom#_lhKca77uEe6laZimEYihUg"/>
    </org.eventb.core.poPredicateSet>
    <org.eventb.core.poPredicateSet name="ABSHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poStamp="1">
        <org.eventb.core.poIdentifier name="gateway_processing" org.eventb.core.type="ℤ"/>
        <org.eventb.core.poIdentifier name="triggered_events" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_EVENTS)"/>
        <org.eventb.core.poIdentifier name="initiated" org.eventb.core.type="ℤ"/>
        <org.eventb.core.poIdentifier name="submit_cc_tx" org.eventb.core.type="ℤ"/>
        <org.eventb.core.poIdentifier name="subscribed" org.eventb.core.type="ℤ"/>
        <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="subscriptions" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_SMART_CONTRACTS)"/>
        <org.eventb.core.poIdentifier name="triggered" org.eventb.core.type="ℤ"/>
        <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.poPredicate name="received_cross_chain_transactiont" org.eventb.core.predicate="received_transactions∈CROSS_CHAIN_SMART_CONTRACTS ↔ TRANSACTIONS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.invariant#_yREdZL7uEe6laZimEYihUg"/>
        <org.eventb.core.poPredicate name="received_cross_chain_transactionu" org.eventb.core.predicate="triggered_events∈CROSS_CHAIN_SMART_CONTRACTS ↔ CROSS_CHAIN_EVENTS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.invariant#_yREdZb7uEe6laZimEYihUg"/>
        <org.eventb.core.poPredicate name="received_cross_chain_transactionv" org.eventb.core.predicate="subscriptions∈GATEWAYS ↔ CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.invariant#_yREdZr7uEe6laZimEYihUg"/>
        <org.eventb.core.poPredicate name="received_cross_chain_transactionw" org.eventb.core.predicate="gateway_pending_transactions∈GATEWAYS ↔ CROSS_CHAIN_TRANSACTIONS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.invariant#_yREdZ77uEe6laZimEYihUg"/>
        <org.eventb.core.poPredicate name="received_cross_chain_transactionx" org.eventb.core.predicate="received_cross_chain_transactions∈CROSS_CHAIN_SMART_CONTRACTS ↔ CROSS_CHAIN_TRANSACTIONS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.invariant#_yREdaL7uEe6laZimEYihUg"/>
    </org.eventb.core.poPredicateSet>
    <org.eventb.core.poSequent name="INITIATE_CC_TX/inv12/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="3">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poPredicateSet#EVTALLHYPreceived_cross_chain_transactiont"/>
        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="1∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.invariant#_VBMe8MEUEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_y397cMBFEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqD"/>
        <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.invariant#_VBMe8MEUEe6yC4BToIaAqA"/>
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poSequent#INITIATE_CC_TX\/inv12\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
        <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD1"/>
    </org.eventb.core.poSequent>
    <org.eventb.core.poSequent name="INITIATE_CC_TX/inv15/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="3">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poPredicateSet#EVTALLHYPreceived_cross_chain_transactiont"/>
        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="0∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.invariant#_VBNGAcEUEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_y397cMBFEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqD"/>
        <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.invariant#_VBNGAcEUEe6yC4BToIaAqA"/>
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poSequent#INITIATE_CC_TX\/inv15\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
        <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD4"/>
    </org.eventb.core.poSequent>
    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_cross_chain_transactiont" org.eventb.core.parentSet="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="3">
        <org.eventb.core.poIdentifier name="submit_cc_tx'" org.eventb.core.type="ℤ"/>
        <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.poIdentifier name="initiated'" org.eventb.core.type="ℤ"/>
    </org.eventb.core.poPredicateSet>
    <org.eventb.core.poPredicateSet name="EVTALLHYPreceived_cross_chain_transactiont" org.eventb.core.parentSet="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poPredicateSet#EVTIDENTreceived_cross_chain_transactiont" org.eventb.core.poStamp="3">
        <org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="transaction∈TRANSACTIONS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_y397cMBFEe6yC4BToIaAqA|org.eventb.core.guard#_yQ9vu77uEe6laZimEYihUg"/>
        <org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="transaction∉received_transactions[{source_smart_contract}]" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_y397cMBFEe6yC4BToIaAqA|org.eventb.core.guard#_yQ9vvL7uEe6laZimEYihUg"/>
    </org.eventb.core.poPredicateSet>
    <org.eventb.core.poSequent name="TRIGGER_CC_TX_EVENT/inv12/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="3">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poPredicateSet#EVTALLHYPreceived_cross_chain_transactionu"/>
        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="0∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.invariant#_VBMe8MEUEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_E_KKUMBGEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqE"/>
        <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.invariant#_VBMe8MEUEe6yC4BToIaAqA"/>
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poSequent#TRIGGER_CC_TX_EVENT\/inv12\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
        <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD1"/>
    </org.eventb.core.poSequent>
    <org.eventb.core.poSequent name="TRIGGER_CC_TX_EVENT/inv13/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="3">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poPredicateSet#EVTALLHYPreceived_cross_chain_transactionu"/>
        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="1∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.invariant#_VBMe8cEUEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_E_KKUMBGEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqE"/>
        <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.invariant#_VBMe8cEUEe6yC4BToIaAqA"/>
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poSequent#TRIGGER_CC_TX_EVENT\/inv13\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
        <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD2"/>
    </org.eventb.core.poSequent>
    <org.eventb.core.poSequent name="TRIGGER_CC_TX_EVENT/inv15/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="3">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poPredicateSet#EVTALLHYPreceived_cross_chain_transactionu"/>
        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="0∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.invariant#_VBNGAcEUEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_E_KKUMBGEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqE"/>
        <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.invariant#_VBNGAcEUEe6yC4BToIaAqA"/>
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poSequent#TRIGGER_CC_TX_EVENT\/inv15\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
        <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD4"/>
    </org.eventb.core.poSequent>
    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_cross_chain_transactionu" org.eventb.core.parentSet="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="3">
        <org.eventb.core.poIdentifier name="triggered_events'" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_EVENTS)"/>
        <org.eventb.core.poIdentifier name="submit_cc_tx'" org.eventb.core.type="ℤ"/>
        <org.eventb.core.poIdentifier name="triggered'" org.eventb.core.type="ℤ"/>
        <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.poIdentifier name="initiated'" org.eventb.core.type="ℤ"/>
    </org.eventb.core.poPredicateSet>
    <org.eventb.core.poPredicateSet name="EVTALLHYPreceived_cross_chain_transactionu" org.eventb.core.parentSet="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poPredicateSet#EVTIDENTreceived_cross_chain_transactionu" org.eventb.core.poStamp="3">
        <org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="source_smart_contract ↦ transaction∈received_transactions" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_E_KKUMBGEe6yC4BToIaAqA|org.eventb.core.guard#_yQ9vwb7uEe6laZimEYihUg"/>
        <org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="cross_chain_event∉triggered_events[{source_smart_contract}]" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_E_KKUMBGEe6yC4BToIaAqA|org.eventb.core.guard#_yQ9vwr7uEe6laZimEYihUg"/>
    </org.eventb.core.poPredicateSet>
    <org.eventb.core.poSequent name="LISTEN_CC_TX_EVENT/inv13/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="3">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poPredicateSet#EVTALLHYPreceived_cross_chain_transactionv"/>
        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="0∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.invariant#_VBMe8cEUEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_THog4MBGEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqF"/>
        <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.invariant#_VBMe8cEUEe6yC4BToIaAqA"/>
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poSequent#LISTEN_CC_TX_EVENT\/inv13\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
        <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD2"/>
    </org.eventb.core.poSequent>
    <org.eventb.core.poSequent name="LISTEN_CC_TX_EVENT/inv14/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="3">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poPredicateSet#EVTALLHYPreceived_cross_chain_transactionv"/>
        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="1∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.invariant#_VBNGAMEUEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_THog4MBGEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqF"/>
        <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.invariant#_VBNGAMEUEe6yC4BToIaAqA"/>
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poSequent#LISTEN_CC_TX_EVENT\/inv14\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
        <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD3"/>
    </org.eventb.core.poSequent>
    <org.eventb.core.poSequent name="LISTEN_CC_TX_EVENT/inv15/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="3">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poPredicateSet#EVTALLHYPreceived_cross_chain_transactionv"/>
        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="0∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.invariant#_VBNGAcEUEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_THog4MBGEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqF"/>
        <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.invariant#_VBNGAcEUEe6yC4BToIaAqA"/>
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poSequent#LISTEN_CC_TX_EVENT\/inv15\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
        <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD4"/>
    </org.eventb.core.poSequent>
    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_cross_chain_transactionv" org.eventb.core.parentSet="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="3">
        <org.eventb.core.poIdentifier name="cross_chain_transaction" org.eventb.core.type="CROSS_CHAIN_TRANSACTIONS"/>
        <org.eventb.core.poIdentifier name="gateway_processing'" org.eventb.core.type="ℤ"/>
        <org.eventb.core.poIdentifier name="triggered_events'" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_EVENTS)"/>
        <org.eventb.core.poIdentifier name="submit_cc_tx'" org.eventb.core.type="ℤ"/>
        <org.eventb.core.poIdentifier name="triggered'" org.eventb.core.type="ℤ"/>
        <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_transactionv" org.eventb.core.parentSet="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poPredicateSet#EVTIDENTreceived_cross_chain_transactionv" org.eventb.core.poStamp="3">
        <org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="source_smart_contract ↦ cross_chain_event∈triggered_events" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_THog4MBGEe6yC4BToIaAqA|org.eventb.core.guard#_yQ9vyL7uEe6laZimEYihUg"/>
        <org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="gateway ↦ source_smart_contract∈subscriptions" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_THog4MBGEe6yC4BToIaAqA|org.eventb.core.guard#_yQ9vyb7uEe6laZimEYihUg"/>
        <org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="gateway ↦ cross_chain_transaction∉gateway_pending_transactions" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_THog4MBGEe6yC4BToIaAqA|org.eventb.core.guard#_yQ9vyr7uEe6laZimEYihUg"/>
    </org.eventb.core.poPredicateSet>
    <org.eventb.core.poSequent name="SUBMIT_CC_TX/inv14/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="3">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poPredicateSet#EVTALLHYPreceived_cross_chain_transactionw"/>
        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="0∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.invariant#_VBNGAMEUEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_fwqd8MBGEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqG"/>
        <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.invariant#_VBNGAMEUEe6yC4BToIaAqA"/>
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poSequent#SUBMIT_CC_TX\/inv14\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
        <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD3"/>
    </org.eventb.core.poSequent>
    <org.eventb.core.poSequent name="SUBMIT_CC_TX/inv15/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="3">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poPredicateSet#EVTALLHYPreceived_cross_chain_transactionw"/>
        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="1∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.invariant#_VBNGAcEUEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_fwqd8MBGEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqG"/>
        <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.invariant#_VBNGAcEUEe6yC4BToIaAqA"/>
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poSequent#SUBMIT_CC_TX\/inv15\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
        <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD4"/>
    </org.eventb.core.poSequent>
    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_cross_chain_transactionw" org.eventb.core.parentSet="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="3">
        <org.eventb.core.poIdentifier name="cross_chain_transaction" org.eventb.core.type="CROSS_CHAIN_TRANSACTIONS"/>
        <org.eventb.core.poIdentifier name="gateway_processing'" org.eventb.core.type="ℤ"/>
        <org.eventb.core.poIdentifier name="submit_cc_tx'" org.eventb.core.type="ℤ"/>
        <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_transactionw" org.eventb.core.parentSet="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poPredicateSet#EVTIDENTreceived_cross_chain_transactionw" org.eventb.core.poStamp="3">
        <org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="gateway ↦ cross_chain_transaction∈gateway_pending_transactions" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_fwqd8MBGEe6yC4BToIaAqA|org.eventb.core.guard#_yREdYr7uEe6laZimEYihUg"/>
    </org.eventb.core.poPredicateSet>
    <org.eventb.core.poSequent name="INITIALISATION/inv11/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="3">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poPredicateSet#EVTALLHYPreceived_cross_chain_transactionx"/>
        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="0∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.invariant#_VBL34sEUEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#'"/>
        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqB"/>
        <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.invariant#_VBL34sEUEe6yC4BToIaAqA"/>
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poSequent#INITIALISATION\/inv11\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
        <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD0"/>
    </org.eventb.core.poSequent>
    <org.eventb.core.poSequent name="INITIALISATION/inv12/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="3">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poPredicateSet#EVTALLHYPreceived_cross_chain_transactionx"/>
        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="0∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.invariant#_VBMe8MEUEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#'"/>
        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqB"/>
        <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.invariant#_VBMe8MEUEe6yC4BToIaAqA"/>
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poSequent#INITIALISATION\/inv12\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
        <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD1"/>
    </org.eventb.core.poSequent>
    <org.eventb.core.poSequent name="INITIALISATION/inv13/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="3">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poPredicateSet#EVTALLHYPreceived_cross_chain_transactionx"/>
        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="0∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.invariant#_VBMe8cEUEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#'"/>
        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqB"/>
        <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.invariant#_VBMe8cEUEe6yC4BToIaAqA"/>
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poSequent#INITIALISATION\/inv13\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
        <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD2"/>
    </org.eventb.core.poSequent>
    <org.eventb.core.poSequent name="INITIALISATION/inv14/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="3">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poPredicateSet#EVTALLHYPreceived_cross_chain_transactionx"/>
        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="0∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.invariant#_VBNGAMEUEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#'"/>
        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqB"/>
        <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.invariant#_VBNGAMEUEe6yC4BToIaAqA"/>
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poSequent#INITIALISATION\/inv14\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
        <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD3"/>
    </org.eventb.core.poSequent>
    <org.eventb.core.poSequent name="INITIALISATION/inv15/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="3">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poPredicateSet#EVTALLHYPreceived_cross_chain_transactionx"/>
        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="0∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.invariant#_VBNGAcEUEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#'"/>
        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqB"/>
        <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.invariant#_VBNGAcEUEe6yC4BToIaAqA"/>
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poSequent#INITIALISATION\/inv15\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
        <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD4"/>
    </org.eventb.core.poSequent>
    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_cross_chain_transactionx" org.eventb.core.parentSet="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poStamp="3">
        <org.eventb.core.poIdentifier name="gateway_processing'" org.eventb.core.type="ℤ"/>
        <org.eventb.core.poIdentifier name="triggered_events'" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_EVENTS)"/>
        <org.eventb.core.poIdentifier name="submit_cc_tx'" org.eventb.core.type="ℤ"/>
        <org.eventb.core.poIdentifier name="triggered'" org.eventb.core.type="ℤ"/>
        <org.eventb.core.poIdentifier name="gateway_pending_transactions'" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_TRANSACTIONS)"/>
        <org.eventb.core.poIdentifier name="subscribed'" org.eventb.core.type="ℤ"/>
        <org.eventb.core.poIdentifier name="received_transactions'" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×TRANSACTIONS)"/>
        <org.eventb.core.poIdentifier name="subscriptions'" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_SMART_CONTRACTS)"/>
        <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="initiated'" org.eventb.core.type="ℤ"/>
    </org.eventb.core.poPredicateSet>
    <org.eventb.core.poPredicateSet name="EVTALLHYPreceived_cross_chain_transactionx" org.eventb.core.parentSet="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poPredicateSet#EVTIDENTreceived_cross_chain_transactionx" org.eventb.core.poStamp="3"/>
    <org.eventb.core.poSequent name="SUBSCRIBE_SMART_CONTRACT_EVENTS/inv11/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="3">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poPredicateSet#EVTALLHYPreceived_cross_chain_transactiony"/>
        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="1∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.invariant#_VBL34sEUEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_yQ9vtr7uEe6laZimEYihUg"/>
        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqC"/>
        <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.invariant#_VBL34sEUEe6yC4BToIaAqA"/>
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poSequent#SUBSCRIBE_SMART_CONTRACT_EVENTS\/inv11\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
        <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD0"/>
    </org.eventb.core.poSequent>
    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_cross_chain_transactiony" org.eventb.core.parentSet="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="3">
        <org.eventb.core.poIdentifier name="subscribed'" org.eventb.core.type="ℤ"/>
        <org.eventb.core.poIdentifier name="subscriptions'" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_SMART_CONTRACTS)"/>
    </org.eventb.core.poPredicateSet>
    <org.eventb.core.poPredicateSet name="EVTALLHYPreceived_cross_chain_transactiony" org.eventb.core.parentSet="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poPredicateSet#EVTIDENTreceived_cross_chain_transactiony" org.eventb.core.poStamp="3">
        <org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="gateway ↦ source_smart_contract∉subscriptions" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_yQ9vtr7uEe6laZimEYihUg|org.eventb.core.guard#_yQ9vuL7uEe6laZimEYihUg"/>
    </org.eventb.core.poPredicateSet>
    <org.eventb.core.poPredicateSet name="ALLHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Abstract_Animation_m2.bpo|org.eventb.core.poFile#CCTx_Abstract_Animation_m2|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poStamp="1">
        <org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="subscribed∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.invariant#_VBL34sEUEe6yC4BToIaAqA"/>
        <org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="initiated∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.invariant#_VBMe8MEUEe6yC4BToIaAqA"/>
        <org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="triggered∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.invariant#_VBMe8cEUEe6yC4BToIaAqA"/>
        <org.eventb.core.poPredicate name="PRD3" org.eventb.core.predicate="gateway_processing∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.invariant#_VBNGAMEUEe6yC4BToIaAqA"/>
        <org.eventb.core.poPredicate name="PRD4" org.eventb.core.predicate="submit_cc_tx∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.invariant#_VBNGAcEUEe6yC4BToIaAqA"/>
    </org.eventb.core.poPredicateSet>
</org.eventb.core.poFile>