Skip to content
Snippets Groups Projects
Normal view Permalink
CCTx_Ethereum_Fabric_Animation_m3.bpo 62 KiB
Newer Older
Guzman Llambias's avatar
Add Ethereum -> Fabric animation (WIP)
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 252 253 254 255 256 257 258 259 260 261 262 263 264 265 266 267 268 269 270 271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.poFile org.eventb.core.poStamp="7">
    <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.poIdentifier name="USERS" org.eventb.core.type="ℙ(USERS)"/>
        <org.eventb.core.poIdentifier name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
        <org.eventb.core.poIdentifier name="write" org.eventb.core.type="PERMISSIONS"/>
        <org.eventb.core.poIdentifier name="read" org.eventb.core.type="PERMISSIONS"/>
        <org.eventb.core.poIdentifier name="gateway_user" org.eventb.core.type="USERS"/>
        <org.eventb.core.poPredicate name="CROSS_CHAIN_SMART_CONTRACTW" org.eventb.core.predicate="partition(PERMISSIONS,{read},{write})" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_c2.buc|org.eventb.core.contextFile#CCTx_Ethereum_Fabric_c2|org.eventb.core.axiom#_olcsoL7uEe6laZimEYihUg"/>
        <org.eventb.core.poPredicate name="CROSS_CHAIN_SMART_CONTRACTX" org.eventb.core.predicate="gateway_user∈USERS" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_c2.buc|org.eventb.core.contextFile#CCTx_Ethereum_Fabric_c2|org.eventb.core.axiom#_olcsob7uEe6laZimEYihUg"/>
    </org.eventb.core.poPredicateSet>
    <org.eventb.core.poPredicateSet name="ABSHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poStamp="6">
        <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="authenticated_transactions" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_TRANSACTIONS×USERS)"/>
        <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="user_created" 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="write_grant" org.eventb.core.type="ℙ(USERS×PERMISSIONS)"/>
        <org.eventb.core.poIdentifier name="received_transactions" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×TRANSACTIONS)"/>
        <org.eventb.core.poIdentifier name="authenticated_users" org.eventb.core.type="ℙ(USERS)"/>
        <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.poPredicate name="received_cross_chain_transactiony" org.eventb.core.predicate="authenticated_users⊆USERS" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.invariant#_jV9TIsEWEe6yC4BToIaAqA"/>
        <org.eventb.core.poPredicate name="received_cross_chain_transactionz" org.eventb.core.predicate="authenticated_transactions∈received_cross_chain_transactions → authenticated_users" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.invariant#_jV9TI8EWEe6yC4BToIaAqA"/>
        <org.eventb.core.poPredicate name="received_cross_chain_transaction{" org.eventb.core.predicate="∀tx⦂CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_TRANSACTIONS·tx∈received_cross_chain_transactions⇒(∃u⦂USERS·u∈authenticated_users∧tx ↦ u∈authenticated_transactions)" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.invariant#_jV9TJMEWEe6yC4BToIaAqA"/>
        <org.eventb.core.poPredicate name="received_cross_chain_transaction|" org.eventb.core.predicate="write_grant∈authenticated_users ↔ {write}" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.invariant#_jV9TJcEWEe6yC4BToIaAqA"/>
        <org.eventb.core.poPredicate name="received_cross_chain_transaction}" org.eventb.core.predicate="authenticated_transactions[received_cross_chain_transactions]⊆dom(write_grant)" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.invariant#_jV9TJsEWEe6yC4BToIaAqA"/>
    </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="7">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|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_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_t-t3AMEVEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh"/>
        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh"/>
        <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_t-t3AMEVEe6yC4BToIaAqA"/>
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|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_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|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="7">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|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_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_t-t3AcEVEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh"/>
        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh"/>
        <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_t-t3AcEVEe6yC4BToIaAqA"/>
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|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_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|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="7">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|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_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_t-ueEMEVEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh"/>
        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh"/>
        <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_t-ueEMEVEe6yC4BToIaAqA"/>
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|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_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|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="7">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|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_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_t-ueEcEVEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh"/>
        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh"/>
        <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_t-ueEcEVEe6yC4BToIaAqA"/>
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|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_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|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="7">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|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_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_t-vFIMEVEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh"/>
        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh"/>
        <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_t-vFIMEVEe6yC4BToIaAqA"/>
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|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_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD4"/>
    </org.eventb.core.poSequent>
    <org.eventb.core.poSequent name="INITIALISATION/inv16/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="7">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|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_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_ZH0uYMEaEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh"/>
        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUh"/>
        <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_ZH0uYMEaEe6yC4BToIaAqA"/>
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poSequent#INITIALISATION\/inv16\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
        <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD5"/>
    </org.eventb.core.poSequent>
    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_cross_chain_transactiont" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poStamp="6">
        <org.eventb.core.poIdentifier name="gateway_processing'" org.eventb.core.type="ℤ"/>
        <org.eventb.core.poIdentifier name="authenticated_users'" org.eventb.core.type="ℙ(USERS)"/>
        <org.eventb.core.poIdentifier name="triggered_events'" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_EVENTS)"/>
        <org.eventb.core.poIdentifier name="authenticated_transactions'" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_TRANSACTIONS×USERS)"/>
        <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="write_grant'" org.eventb.core.type="ℙ(USERS×PERMISSIONS)"/>
        <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="user_created'" org.eventb.core.type="ℤ"/>
        <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_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#EVTIDENTreceived_cross_chain_transactiont" org.eventb.core.poStamp="6"/>
    <org.eventb.core.poSequent name="SUBSCRIBE_SMART_CONTRACT_EVENTS_IN_ETHEREUM/inv11/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="6">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|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_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_t-t3AMEVEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_1tlnkr7uEe6laZimEYihUg"/>
        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUi"/>
        <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_t-t3AMEVEe6yC4BToIaAqA"/>
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poSequent#SUBSCRIBE_SMART_CONTRACT_EVENTS_IN_ETHEREUM\/inv11\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
        <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD0"/>
    </org.eventb.core.poSequent>
    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_cross_chain_transactionu" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="6">
        <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_transactionu" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#EVTIDENTreceived_cross_chain_transactionu" org.eventb.core.poStamp="6">
        <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.poSequent name="INITIATE_CC_TX_IN_ETHEREUM/inv12/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="6">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|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_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_t-t3AcEVEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_1g9W8MBFEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUj"/>
        <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_t-t3AcEVEe6yC4BToIaAqA"/>
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poSequent#INITIATE_CC_TX_IN_ETHEREUM\/inv12\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
        <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD1"/>
    </org.eventb.core.poSequent>
    <org.eventb.core.poSequent name="INITIATE_CC_TX_IN_ETHEREUM/inv15/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="6">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|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_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_t-vFIMEVEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_1g9W8MBFEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUj"/>
        <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_t-vFIMEVEe6yC4BToIaAqA"/>
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poSequent#INITIATE_CC_TX_IN_ETHEREUM\/inv15\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
        <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|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_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="6">
        <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_transactionv" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#EVTIDENTreceived_cross_chain_transactionv" org.eventb.core.poStamp="6">
        <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_IN_ETHEREUM/inv12/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="6">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|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_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_t-t3AcEVEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_HT50IMBGEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUk"/>
        <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_t-t3AcEVEe6yC4BToIaAqA"/>
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poSequent#TRIGGER_CC_TX_EVENT_IN_ETHEREUM\/inv12\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
        <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD1"/>
    </org.eventb.core.poSequent>
    <org.eventb.core.poSequent name="TRIGGER_CC_TX_EVENT_IN_ETHEREUM/inv13/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="6">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|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_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_t-ueEMEVEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_HT50IMBGEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUk"/>
        <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_t-ueEMEVEe6yC4BToIaAqA"/>
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poSequent#TRIGGER_CC_TX_EVENT_IN_ETHEREUM\/inv13\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
        <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD2"/>
    </org.eventb.core.poSequent>
    <org.eventb.core.poSequent name="TRIGGER_CC_TX_EVENT_IN_ETHEREUM/inv15/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="6">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|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_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_t-vFIMEVEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_HT50IMBGEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUk"/>
        <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_t-vFIMEVEe6yC4BToIaAqA"/>
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poSequent#TRIGGER_CC_TX_EVENT_IN_ETHEREUM\/inv15\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
        <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|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_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="6">
        <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_transactionw" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#EVTIDENTreceived_cross_chain_transactionw" org.eventb.core.poStamp="6">
        <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_IN_ETHEREUM/inv13/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="6">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|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_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_t-ueEMEVEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_VePMJsBGEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUl"/>
        <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_t-ueEMEVEe6yC4BToIaAqA"/>
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poSequent#LISTEN_CC_TX_EVENT_IN_ETHEREUM\/inv13\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
        <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD2"/>
    </org.eventb.core.poSequent>
    <org.eventb.core.poSequent name="LISTEN_CC_TX_EVENT_IN_ETHEREUM/inv14/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="6">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#EVTALLHYPreceived_cross_chain_transactionx"/>
        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="1∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_t-ueEcEVEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_VePMJsBGEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUl"/>
        <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_t-ueEcEVEe6yC4BToIaAqA"/>
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poSequent#LISTEN_CC_TX_EVENT_IN_ETHEREUM\/inv14\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
        <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD3"/>
    </org.eventb.core.poSequent>
    <org.eventb.core.poSequent name="LISTEN_CC_TX_EVENT_IN_ETHEREUM/inv15/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="6">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|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_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_t-vFIMEVEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_VePMJsBGEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUl"/>
        <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_t-vFIMEVEe6yC4BToIaAqA"/>
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poSequent#LISTEN_CC_TX_EVENT_IN_ETHEREUM\/inv15\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
        <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|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_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="6">
        <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_transactionx" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#EVTIDENTreceived_cross_chain_transactionx" org.eventb.core.poStamp="6">
        <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_TO_FABRIC/inv14/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="6">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#EVTALLHYPreceived_cross_chain_transactiony"/>
        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="0∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_t-ueEcEVEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_hrEVZsBGEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUm"/>
        <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_t-ueEcEVEe6yC4BToIaAqA"/>
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poSequent#SUBMIT_CC_TX_TO_FABRIC\/inv14\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
        <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD3"/>
    </org.eventb.core.poSequent>
    <org.eventb.core.poSequent name="SUBMIT_CC_TX_TO_FABRIC/inv15/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="6">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|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_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_t-vFIMEVEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_hrEVZsBGEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUm"/>
        <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_t-vFIMEVEe6yC4BToIaAqA"/>
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poSequent#SUBMIT_CC_TX_TO_FABRIC\/inv15\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
        <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD4"/>
    </org.eventb.core.poSequent>
    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_cross_chain_transactiony" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="6">
        <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="authenticated_transactions'" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_TRANSACTIONS×USERS)"/>
        <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="user" org.eventb.core.type="USERS"/>
        <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="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#EVTIDENTreceived_cross_chain_transactiony" org.eventb.core.poStamp="6">
        <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.poPredicate name="PRD1" org.eventb.core.predicate="user∈authenticated_users" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_hrEVZsBGEe6yC4BToIaAqA|org.eventb.core.guard#_jV8sEcEWEe6yC4BToIaAqA"/>
        <org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="user ↦ write∈write_grant" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_hrEVZsBGEe6yC4BToIaAqA|org.eventb.core.guard#_jV8sEsEWEe6yC4BToIaAqA"/>
    </org.eventb.core.poPredicateSet>
    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_cross_chain_transactionz" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="0">
        <org.eventb.core.poIdentifier name="authenticated_users'" org.eventb.core.type="ℙ(USERS)"/>
    </org.eventb.core.poPredicateSet>
    <org.eventb.core.poPredicateSet name="EVTALLHYPreceived_cross_chain_transactionz" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#EVTIDENTreceived_cross_chain_transactionz" org.eventb.core.poStamp="0">
        <org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="gateway_user∉authenticated_users" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_K_21gMEXEe6yC4BToIaAqA|org.eventb.core.guard#_y4y5cMEXEe6yC4BToIaAqA"/>
    </org.eventb.core.poPredicateSet>
    <org.eventb.core.poPredicateSet name="ALLHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poStamp="6">
        <org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="subscribed∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_t-t3AMEVEe6yC4BToIaAqA"/>
        <org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="initiated∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_t-t3AcEVEe6yC4BToIaAqA"/>
        <org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="triggered∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_t-ueEMEVEe6yC4BToIaAqA"/>
        <org.eventb.core.poPredicate name="PRD3" org.eventb.core.predicate="gateway_processing∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_t-ueEcEVEe6yC4BToIaAqA"/>
        <org.eventb.core.poPredicate name="PRD4" org.eventb.core.predicate="submit_cc_tx∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_t-vFIMEVEe6yC4BToIaAqA"/>
        <org.eventb.core.poPredicate name="PRD5" org.eventb.core.predicate="user_created∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_Animation_m3|org.eventb.core.invariant#_ZH0uYMEaEe6yC4BToIaAqA"/>
    </org.eventb.core.poPredicateSet>
</org.eventb.core.poFile>