CCTx_Fabric_Ethereum_Animation_m3.bpo

<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.poFile org.eventb.core.poStamp="23">
    <org.eventb.core.poPredicateSet name="CTXHYP" org.eventb.core.poStamp="23">
        <org.eventb.core.poIdentifier name="TARGET_TRANSACTIONS" org.eventb.core.type="ℙ(TARGET_TRANSACTIONS)"/>
        <org.eventb.core.poIdentifier name="GATEWAYS" org.eventb.core.type="ℙ(GATEWAYS)"/>
        <org.eventb.core.poIdentifier name="SOURCE_TRANSACTIONS" org.eventb.core.type="ℙ(SOURCE_TRANSACTIONS)"/>
        <org.eventb.core.poIdentifier name="SMART_CONTRACT_EVENTS" org.eventb.core.type="ℙ(SMART_CONTRACT_EVENTS)"/>
        <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="ADDRESS" org.eventb.core.type="ℙ(ADDRESS)"/>
        <org.eventb.core.poIdentifier name="gateway_address" org.eventb.core.type="ADDRESS"/>
        <org.eventb.core.poPredicate name="CROSS_CHAIN_SMART_CONTRACTW" org.eventb.core.predicate="gateway_address∈ADDRESS" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_c2.buc|org.eventb.core.contextFile#CCTx_Fabric_Ethereum_c2|org.eventb.core.axiom#_seJcgL7uEe6laZimEYihUg"/>
    </org.eventb.core.poPredicateSet>
    <org.eventb.core.poPredicateSet name="ABSHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poStamp="23">
        <org.eventb.core.poIdentifier name="gateway_processing" org.eventb.core.type="ℤ"/>
        <org.eventb.core.poIdentifier name="wallet_amount" org.eventb.core.type="ℤ"/>
        <org.eventb.core.poIdentifier name="initiated" org.eventb.core.type="ℤ"/>
        <org.eventb.core.poIdentifier name="received_target_transactions" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×TARGET_TRANSACTIONS)"/>
        <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="accounts" org.eventb.core.type="ℙ(ADDRESS×ℤ)"/>
        <org.eventb.core.poIdentifier name="gateway_pending_events" org.eventb.core.type="ℙ(GATEWAYS×TARGET_TRANSACTIONS)"/>
        <org.eventb.core.poIdentifier name="subscriptions" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_SMART_CONTRACTS)"/>
        <org.eventb.core.poIdentifier name="emitted_events" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×SMART_CONTRACT_EVENTS)"/>
        <org.eventb.core.poIdentifier name="received_source_transactions" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×SOURCE_TRANSACTIONS)"/>
        <org.eventb.core.poIdentifier name="emitted" org.eventb.core.type="ℤ"/>
        <org.eventb.core.poIdentifier name="wallet_created" org.eventb.core.type="ℤ"/>
        <org.eventb.core.poPredicate name="received_target_transactiont" org.eventb.core.predicate="received_source_transactions∈CROSS_CHAIN_SMART_CONTRACTS ↔ SOURCE_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#_zpKWcMQ4Ee609fto5wotHA"/>
        <org.eventb.core.poPredicate name="received_target_transactionu" org.eventb.core.predicate="emitted_events∈CROSS_CHAIN_SMART_CONTRACTS ↔ SMART_CONTRACT_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#_zpKWccQ4Ee609fto5wotHA"/>
        <org.eventb.core.poPredicate name="received_target_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#_zpK9gMQ4Ee609fto5wotHA"/>
        <org.eventb.core.poPredicate name="received_target_transactionw" org.eventb.core.predicate="gateway_pending_events∈GATEWAYS ↔ TARGET_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#_zpK9gcQ4Ee609fto5wotHA"/>
        <org.eventb.core.poPredicate name="received_target_transactionx" org.eventb.core.predicate="received_target_transactions∈CROSS_CHAIN_SMART_CONTRACTS ↔ TARGET_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#_qTKs0MT7Ee609fto5wotHA"/>
        <org.eventb.core.poPredicate name="received_target_transactiony" org.eventb.core.predicate="accounts∈ADDRESS ⇸ ℕ" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_m2|org.eventb.core.invariant#_XvjdQMEBEe6yC4BToIaAqA"/>
    </org.eventb.core.poPredicateSet>
    <org.eventb.core.poSequent name="INITIALISATION/inv31/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="23">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transactiont"/>
        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="0∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.invariant#_qWNdEMEGEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_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_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_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_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.invariant#_qWNdEMEGEe6yC4BToIaAqA"/>
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poSequent#INITIALISATION\/inv31\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
        <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD0"/>
    </org.eventb.core.poSequent>
    <org.eventb.core.poSequent name="INITIALISATION/inv32/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="23">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transactiont"/>
        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="0∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.invariant#_qWNdEcEGEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_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_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_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_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.invariant#_qWNdEcEGEe6yC4BToIaAqA"/>
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poSequent#INITIALISATION\/inv32\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
        <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD1"/>
    </org.eventb.core.poSequent>
    <org.eventb.core.poSequent name="INITIALISATION/inv33/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="23">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transactiont"/>
        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="0∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.invariant#_qWNdEsEGEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_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_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_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_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.invariant#_qWNdEsEGEe6yC4BToIaAqA"/>
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poSequent#INITIALISATION\/inv33\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
        <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD2"/>
    </org.eventb.core.poSequent>
    <org.eventb.core.poSequent name="INITIALISATION/inv34/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="23">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transactiont"/>
        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="0∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.invariant#_qWNdE8EGEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_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_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_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_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.invariant#_qWNdE8EGEe6yC4BToIaAqA"/>
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poSequent#INITIALISATION\/inv34\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
        <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD3"/>
    </org.eventb.core.poSequent>
    <org.eventb.core.poSequent name="INITIALISATION/inv35/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="23">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transactiont"/>
        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="0∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.invariant#_qWNdFMEGEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_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_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_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_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.invariant#_qWNdFMEGEe6yC4BToIaAqA"/>
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poSequent#INITIALISATION\/inv35\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
        <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD4"/>
    </org.eventb.core.poSequent>
    <org.eventb.core.poSequent name="INITIALISATION/inv36/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="23">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transactiont"/>
        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="0∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.invariant#_qWOEIMEGEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_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_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_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_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.invariant#_qWOEIMEGEe6yC4BToIaAqA"/>
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poSequent#INITIALISATION\/inv36\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
        <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD5"/>
    </org.eventb.core.poSequent>
    <org.eventb.core.poSequent name="INITIALISATION/inv37/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="23">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transactiont"/>
        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="0∈ℕ" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.invariant#_9cXZIMEHEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_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_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_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_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.invariant#_9cXZIMEHEe6yC4BToIaAqA"/>
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poSequent#INITIALISATION\/inv37\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
        <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD6"/>
    </org.eventb.core.poSequent>
    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_target_transactiont" org.eventb.core.parentSet="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poStamp="23">
        <org.eventb.core.poIdentifier name="gateway_processing'" org.eventb.core.type="ℤ"/>
        <org.eventb.core.poIdentifier name="gateway_pending_events'" org.eventb.core.type="ℙ(GATEWAYS×TARGET_TRANSACTIONS)"/>
        <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="wallet_created'" org.eventb.core.type="ℤ"/>
        <org.eventb.core.poIdentifier name="emitted'" org.eventb.core.type="ℤ"/>
        <org.eventb.core.poIdentifier name="accounts'" org.eventb.core.type="ℙ(ADDRESS×ℤ)"/>
        <org.eventb.core.poIdentifier name="wallet_amount'" org.eventb.core.type="ℤ"/>
        <org.eventb.core.poIdentifier name="subscriptions'" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_SMART_CONTRACTS)"/>
        <org.eventb.core.poIdentifier name="received_source_transactions'" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×SOURCE_TRANSACTIONS)"/>
        <org.eventb.core.poIdentifier name="initiated'" org.eventb.core.type="ℤ"/>
        <org.eventb.core.poIdentifier name="emitted_events'" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×SMART_CONTRACT_EVENTS)"/>
        <org.eventb.core.poIdentifier name="received_target_transactions'" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×TARGET_TRANSACTIONS)"/>
    </org.eventb.core.poPredicateSet>
    <org.eventb.core.poPredicateSet name="EVTALLHYPreceived_target_transactiont" org.eventb.core.parentSet="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#EVTIDENTreceived_target_transactiont" org.eventb.core.poStamp="23"/>
    <org.eventb.core.poSequent name="SUBSCRIBE_SMART_CONTRACT_EVENTS_IN_FABRIC/inv31/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="23">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transactionu"/>
        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="1∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.invariant#_qWNdEMEGEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_m2|org.eventb.core.event#_8rq0Tr7uEe6laZimEYihUg"/>
        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_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_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.invariant#_qWNdEMEGEe6yC4BToIaAqA"/>
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poSequent#SUBSCRIBE_SMART_CONTRACT_EVENTS_IN_FABRIC\/inv31\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
        <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD0"/>
    </org.eventb.core.poSequent>
    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_target_transactionu" org.eventb.core.parentSet="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="23">
        <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_target_transactionu" org.eventb.core.parentSet="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#EVTIDENTreceived_target_transactionu" org.eventb.core.poStamp="23">
        <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#_zpDBscQ4Ee609fto5wotHA"/>
    </org.eventb.core.poPredicateSet>
    <org.eventb.core.poSequent name="INITIATE_CC_TX_IN_FABRIC/inv32/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="23">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transactionv"/>
        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="1∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.invariant#_qWNdEcEGEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_m2|org.eventb.core.event#_2kWtoMBFEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_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_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.invariant#_qWNdEcEGEe6yC4BToIaAqA"/>
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poSequent#INITIATE_CC_TX_IN_FABRIC\/inv32\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
        <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_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_FABRIC/inv35/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="23">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transactionv"/>
        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="0∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.invariant#_qWNdFMEGEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_m2|org.eventb.core.event#_2kWtoMBFEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_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_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.invariant#_qWNdFMEGEe6yC4BToIaAqA"/>
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poSequent#INITIATE_CC_TX_IN_FABRIC\/inv35\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
        <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD4"/>
    </org.eventb.core.poSequent>
    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_target_transactionv" org.eventb.core.parentSet="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="23">
        <org.eventb.core.poIdentifier name="submit_cc_tx'" org.eventb.core.type="ℤ"/>
        <org.eventb.core.poIdentifier name="transaction" org.eventb.core.type="SOURCE_TRANSACTIONS"/>
        <org.eventb.core.poIdentifier name="received_source_transactions'" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×SOURCE_TRANSACTIONS)"/>
        <org.eventb.core.poIdentifier name="initiated'" org.eventb.core.type="ℤ"/>
    </org.eventb.core.poPredicateSet>
    <org.eventb.core.poPredicateSet name="EVTALLHYPreceived_target_transactionv" org.eventb.core.parentSet="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#EVTIDENTreceived_target_transactionv" org.eventb.core.poStamp="23">
        <org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="transaction∈SOURCE_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#_zpDowcQ4Ee609fto5wotHA"/>
        <org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="transaction∉received_source_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#_zpEP0MQ4Ee609fto5wotHA"/>
    </org.eventb.core.poPredicateSet>
    <org.eventb.core.poSequent name="EMIT_EVENT_IN_FABRIC/inv32/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="23">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transactionw"/>
        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="0∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.invariant#_qWNdEcEGEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_m2|org.eventb.core.event#_1TfoAPRhEe60CqkwWvstGA"/>
        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.event#_5dHIwPRhEe60CqkwWvstGA"/>
        <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.invariant#_qWNdEcEGEe6yC4BToIaAqA"/>
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poSequent#EMIT_EVENT_IN_FABRIC\/inv32\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
        <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD1"/>
    </org.eventb.core.poSequent>
    <org.eventb.core.poSequent name="EMIT_EVENT_IN_FABRIC/inv33/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="23">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transactionw"/>
        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="1∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.invariant#_qWNdEsEGEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_m2|org.eventb.core.event#_1TfoAPRhEe60CqkwWvstGA"/>
        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.event#_5dHIwPRhEe60CqkwWvstGA"/>
        <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.invariant#_qWNdEsEGEe6yC4BToIaAqA"/>
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poSequent#EMIT_EVENT_IN_FABRIC\/inv33\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
        <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD2"/>
    </org.eventb.core.poSequent>
    <org.eventb.core.poSequent name="EMIT_EVENT_IN_FABRIC/inv35/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="23">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transactionw"/>
        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="0∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.invariant#_qWNdFMEGEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_m2|org.eventb.core.event#_1TfoAPRhEe60CqkwWvstGA"/>
        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.event#_5dHIwPRhEe60CqkwWvstGA"/>
        <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.invariant#_qWNdFMEGEe6yC4BToIaAqA"/>
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poSequent#EMIT_EVENT_IN_FABRIC\/inv35\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
        <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD4"/>
    </org.eventb.core.poSequent>
    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_target_transactionw" org.eventb.core.parentSet="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="23">
        <org.eventb.core.poIdentifier name="submit_cc_tx'" org.eventb.core.type="ℤ"/>
        <org.eventb.core.poIdentifier name="transaction" org.eventb.core.type="SOURCE_TRANSACTIONS"/>
        <org.eventb.core.poIdentifier name="emitted'" org.eventb.core.type="ℤ"/>
        <org.eventb.core.poIdentifier name="emitted_event" org.eventb.core.type="SMART_CONTRACT_EVENTS"/>
        <org.eventb.core.poIdentifier name="received_source_transactions'" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×SOURCE_TRANSACTIONS)"/>
        <org.eventb.core.poIdentifier name="initiated'" org.eventb.core.type="ℤ"/>
        <org.eventb.core.poIdentifier name="emitted_events'" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×SMART_CONTRACT_EVENTS)"/>
    </org.eventb.core.poPredicateSet>
    <org.eventb.core.poPredicateSet name="EVTALLHYPreceived_target_transactionw" org.eventb.core.parentSet="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#EVTIDENTreceived_target_transactionw" org.eventb.core.poStamp="23">
        <org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="source_smart_contract ↦ transaction∈received_source_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#_WGbIAPRhEe60CqkwWvstGA|org.eventb.core.guard#_zpFd8cQ4Ee609fto5wotHA"/>
        <org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="emitted_event∉emitted_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#_WGbIAPRhEe60CqkwWvstGA|org.eventb.core.guard#_zpGFAMQ4Ee609fto5wotHA"/>
    </org.eventb.core.poPredicateSet>
    <org.eventb.core.poSequent name="LISTEN_EVENT_IN_FABRIC/inv33/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="23">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transactionx"/>
        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="0∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.invariant#_qWNdEsEGEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_m2|org.eventb.core.event#_1TfoAvRhEe60CqkwWvstGA"/>
        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.event#_5dHv0PRhEe60CqkwWvstGA"/>
        <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.invariant#_qWNdEsEGEe6yC4BToIaAqA"/>
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poSequent#LISTEN_EVENT_IN_FABRIC\/inv33\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
        <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD2"/>
    </org.eventb.core.poSequent>
    <org.eventb.core.poSequent name="LISTEN_EVENT_IN_FABRIC/inv34/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="23">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transactionx"/>
        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="1∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.invariant#_qWNdE8EGEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_m2|org.eventb.core.event#_1TfoAvRhEe60CqkwWvstGA"/>
        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.event#_5dHv0PRhEe60CqkwWvstGA"/>
        <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.invariant#_qWNdE8EGEe6yC4BToIaAqA"/>
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poSequent#LISTEN_EVENT_IN_FABRIC\/inv34\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
        <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD3"/>
    </org.eventb.core.poSequent>
    <org.eventb.core.poSequent name="LISTEN_EVENT_IN_FABRIC/inv35/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="23">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transactionx"/>
        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="0∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.invariant#_qWNdFMEGEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_m2|org.eventb.core.event#_1TfoAvRhEe60CqkwWvstGA"/>
        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.event#_5dHv0PRhEe60CqkwWvstGA"/>
        <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.invariant#_qWNdFMEGEe6yC4BToIaAqA"/>
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poSequent#LISTEN_EVENT_IN_FABRIC\/inv35\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
        <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD4"/>
    </org.eventb.core.poSequent>
    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_target_transactionx" org.eventb.core.parentSet="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="23">
        <org.eventb.core.poIdentifier name="gateway_processing'" org.eventb.core.type="ℤ"/>
        <org.eventb.core.poIdentifier name="gateway_pending_events'" org.eventb.core.type="ℙ(GATEWAYS×TARGET_TRANSACTIONS)"/>
        <org.eventb.core.poIdentifier name="submit_cc_tx'" org.eventb.core.type="ℤ"/>
        <org.eventb.core.poIdentifier name="pending_event" org.eventb.core.type="TARGET_TRANSACTIONS"/>
        <org.eventb.core.poIdentifier name="emitted'" org.eventb.core.type="ℤ"/>
        <org.eventb.core.poIdentifier name="emitted_event" org.eventb.core.type="SMART_CONTRACT_EVENTS"/>
        <org.eventb.core.poIdentifier name="emitted_events'" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×SMART_CONTRACT_EVENTS)"/>
    </org.eventb.core.poPredicateSet>
    <org.eventb.core.poPredicateSet name="EVTALLHYPreceived_target_transactionx" org.eventb.core.parentSet="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#EVTIDENTreceived_target_transactionx" org.eventb.core.poStamp="23">
        <org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="source_smart_contract ↦ emitted_event∈emitted_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#_WGbvEPRhEe60CqkwWvstGA|org.eventb.core.guard#_zpHTIcQ4Ee609fto5wotHA"/>
        <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#_WGbvEPRhEe60CqkwWvstGA|org.eventb.core.guard#_zpH6MMQ4Ee609fto5wotHA"/>
        <org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="gateway ↦ pending_event∉gateway_pending_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#_WGbvEPRhEe60CqkwWvstGA|org.eventb.core.guard#_zpH6McQ4Ee609fto5wotHA"/>
    </org.eventb.core.poPredicateSet>
    <org.eventb.core.poSequent name="SUBMIT_TX_TO_ETHEREUM/inv34/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="23">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transactiony"/>
        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="0∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.invariant#_qWNdE8EGEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_m2|org.eventb.core.event#_1TfoBPRhEe60CqkwWvstGA"/>
        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.event#_5dIW4PRhEe60CqkwWvstGA"/>
        <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.invariant#_qWNdE8EGEe6yC4BToIaAqA"/>
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poSequent#SUBMIT_TX_TO_ETHEREUM\/inv34\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
        <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD3"/>
    </org.eventb.core.poSequent>
    <org.eventb.core.poSequent name="SUBMIT_TX_TO_ETHEREUM/inv35/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="23">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transactiony"/>
        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="1∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.invariant#_qWNdFMEGEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_m2|org.eventb.core.event#_1TfoBPRhEe60CqkwWvstGA"/>
        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.event#_5dIW4PRhEe60CqkwWvstGA"/>
        <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.invariant#_qWNdFMEGEe6yC4BToIaAqA"/>
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poSequent#SUBMIT_TX_TO_ETHEREUM\/inv35\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
        <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD4"/>
    </org.eventb.core.poSequent>
    <org.eventb.core.poSequent name="SUBMIT_TX_TO_ETHEREUM/inv37/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="23">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transactiony"/>
        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="accounts(gateway_address) − fee∈ℕ" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.invariant#_9cXZIMEHEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_m2|org.eventb.core.event#_1TfoBPRhEe60CqkwWvstGA"/>
        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.event#_5dIW4PRhEe60CqkwWvstGA"/>
        <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.invariant#_9cXZIMEHEe6yC4BToIaAqA"/>
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poSequent#SUBMIT_TX_TO_ETHEREUM\/inv37\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
        <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD6"/>
    </org.eventb.core.poSequent>
    <org.eventb.core.poSequent name="SUBMIT_TX_TO_ETHEREUM/act33/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of action" org.eventb.core.poStamp="23">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transactiony"/>
        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="gateway_address∈dom(accounts)∧accounts∈ADDRESS ⇸ ℤ" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.event#_5dIW4PRhEe60CqkwWvstGA|org.eventb.core.action#_EcZmAMELEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.event#_5dIW4PRhEe60CqkwWvstGA|org.eventb.core.action#_EcZmAMELEe6yC4BToIaAqA"/>
        <org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transactiony"/>
    </org.eventb.core.poSequent>
    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_target_transactiony" org.eventb.core.parentSet="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="23">
        <org.eventb.core.poIdentifier name="gateway_processing'" org.eventb.core.type="ℤ"/>
        <org.eventb.core.poIdentifier name="gateway_pending_events'" org.eventb.core.type="ℙ(GATEWAYS×TARGET_TRANSACTIONS)"/>
        <org.eventb.core.poIdentifier name="submit_cc_tx'" org.eventb.core.type="ℤ"/>
        <org.eventb.core.poIdentifier name="transaction" org.eventb.core.type="TARGET_TRANSACTIONS"/>
        <org.eventb.core.poIdentifier name="pending_event" org.eventb.core.type="TARGET_TRANSACTIONS"/>
        <org.eventb.core.poIdentifier name="accounts'" org.eventb.core.type="ℙ(ADDRESS×ℤ)"/>
        <org.eventb.core.poIdentifier name="wallet_amount'" org.eventb.core.type="ℤ"/>
        <org.eventb.core.poIdentifier name="received_target_transactions'" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×TARGET_TRANSACTIONS)"/>
        <org.eventb.core.poIdentifier name="fee" org.eventb.core.type="ℤ"/>
    </org.eventb.core.poPredicateSet>
    <org.eventb.core.poPredicateSet name="EVTALLHYPreceived_target_transactiony" org.eventb.core.parentSet="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#EVTIDENTreceived_target_transactiony" org.eventb.core.poStamp="23">
        <org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="gateway ↦ pending_event∈gateway_pending_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#_WGc9MPRhEe60CqkwWvstGA|org.eventb.core.guard#_zpJvYcQ4Ee609fto5wotHA"/>
        <org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="transaction∈TARGET_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#_WGc9MPRhEe60CqkwWvstGA|org.eventb.core.guard#_L7ASUPRgEe60CqkwWvstGA"/>
        <org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="gateway_address∈dom(accounts)" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_m2|org.eventb.core.event#_1TfoBPRhEe60CqkwWvstGA|org.eventb.core.guard#_XvhBAcEBEe6yC4BToIaAqA"/>
        <org.eventb.core.poPredicate name="PRD3" org.eventb.core.predicate="accounts(gateway_address)≥fee" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_m2|org.eventb.core.event#_1TfoBPRhEe60CqkwWvstGA|org.eventb.core.guard#_XvhBAsEBEe6yC4BToIaAqA"/>
        <org.eventb.core.poPredicate name="PRD4" org.eventb.core.predicate="fee&gt;0" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_m2|org.eventb.core.event#_1TfoBPRhEe60CqkwWvstGA|org.eventb.core.guard#_XvhBA8EBEe6yC4BToIaAqA"/>
    </org.eventb.core.poPredicateSet>
    <org.eventb.core.poSequent name="CREATE_ADDRESS_IN_ETHEREUM/inv36/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="23">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transactionz"/>
        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="1∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.invariant#_qWOEIMEGEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_m2|org.eventb.core.event#_8rz9-L7uEe6laZimEYihUg"/>
        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUn"/>
        <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.invariant#_qWOEIMEGEe6yC4BToIaAqA"/>
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poSequent#CREATE_ADDRESS_IN_ETHEREUM\/inv36\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
        <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD5"/>
    </org.eventb.core.poSequent>
    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_target_transactionz" org.eventb.core.parentSet="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="0">
        <org.eventb.core.poIdentifier name="address" org.eventb.core.type="ADDRESS"/>
        <org.eventb.core.poIdentifier name="wallet_created'" org.eventb.core.type="ℤ"/>
        <org.eventb.core.poIdentifier name="accounts'" org.eventb.core.type="ℙ(ADDRESS×ℤ)"/>
    </org.eventb.core.poPredicateSet>
    <org.eventb.core.poPredicateSet name="EVTALLHYPreceived_target_transactionz" org.eventb.core.parentSet="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#EVTIDENTreceived_target_transactionz" org.eventb.core.poStamp="0">
        <org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="address∈ADDRESS" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_m2|org.eventb.core.event#_8rz9-L7uEe6laZimEYihUg|org.eventb.core.guard#_XvhoEcEBEe6yC4BToIaAqA"/>
        <org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="address∉dom(accounts)" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_m2|org.eventb.core.event#_8rz9-L7uEe6laZimEYihUg|org.eventb.core.guard#_XvhoEsEBEe6yC4BToIaAqA"/>
        <org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="address=gateway_address" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUn|org.eventb.core.guard#_wieyEMEGEe6yC4BToIaAqA"/>
    </org.eventb.core.poPredicateSet>
    <org.eventb.core.poSequent name="DEPOSIT_CRYPTOCURRENCY_IN_ETHEREUM/inv35/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="23">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transaction{"/>
        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="0∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.invariant#_qWNdFMEGEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_m2|org.eventb.core.event#_8rz9_b7uEe6laZimEYihUg"/>
        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUo"/>
        <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.invariant#_qWNdFMEGEe6yC4BToIaAqA"/>
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poSequent#DEPOSIT_CRYPTOCURRENCY_IN_ETHEREUM\/inv35\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
        <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD4"/>
    </org.eventb.core.poSequent>
    <org.eventb.core.poSequent name="DEPOSIT_CRYPTOCURRENCY_IN_ETHEREUM/inv37/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="23">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transaction{"/>
        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="accounts(address)+amount∈ℕ" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.invariant#_9cXZIMEHEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_m2|org.eventb.core.event#_8rz9_b7uEe6laZimEYihUg"/>
        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUo"/>
        <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.invariant#_9cXZIMEHEe6yC4BToIaAqA"/>
        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poSequent#DEPOSIT_CRYPTOCURRENCY_IN_ETHEREUM\/inv37\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
        <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD6"/>
    </org.eventb.core.poSequent>
    <org.eventb.core.poSequent name="DEPOSIT_CRYPTOCURRENCY_IN_ETHEREUM/act31/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of action" org.eventb.core.poStamp="23">
        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transaction{"/>
        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="address∈dom(accounts)∧accounts∈ADDRESS ⇸ ℤ" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUo|org.eventb.core.action#_7CFvEMEHEe6yC4BToIaAqA"/>
        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.event#_yREdbb7uEe6laZimEYihUo|org.eventb.core.action#_7CFvEMEHEe6yC4BToIaAqA"/>
        <org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#EVTALLHYPreceived_target_transaction{"/>
    </org.eventb.core.poSequent>
    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_target_transaction{" org.eventb.core.parentSet="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="0">
        <org.eventb.core.poIdentifier name="amount" org.eventb.core.type="ℤ"/>
        <org.eventb.core.poIdentifier name="submit_cc_tx'" org.eventb.core.type="ℤ"/>
        <org.eventb.core.poIdentifier name="address" org.eventb.core.type="ADDRESS"/>
        <org.eventb.core.poIdentifier name="accounts'" org.eventb.core.type="ℙ(ADDRESS×ℤ)"/>
        <org.eventb.core.poIdentifier name="wallet_amount'" org.eventb.core.type="ℤ"/>
    </org.eventb.core.poPredicateSet>
    <org.eventb.core.poPredicateSet name="EVTALLHYPreceived_target_transaction{" org.eventb.core.parentSet="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#EVTIDENTreceived_target_transaction{" org.eventb.core.poStamp="0">
        <org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="amount&gt;0" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_m2|org.eventb.core.event#_8rz9_b7uEe6laZimEYihUg|org.eventb.core.guard#_XvhoFMEBEe6yC4BToIaAqA"/>
        <org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="address∈dom(accounts)" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_m2|org.eventb.core.event#_8rz9_b7uEe6laZimEYihUg|org.eventb.core.guard#_XvhoFcEBEe6yC4BToIaAqA"/>
    </org.eventb.core.poPredicateSet>
    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_target_transaction|" org.eventb.core.parentSet="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="0">
        <org.eventb.core.poIdentifier name="transfer_amount" org.eventb.core.type="ℤ"/>
        <org.eventb.core.poIdentifier name="accounts'" org.eventb.core.type="ℙ(ADDRESS×ℤ)"/>
        <org.eventb.core.poIdentifier name="validator_fee" org.eventb.core.type="ℤ"/>
        <org.eventb.core.poIdentifier name="user_address" org.eventb.core.type="ADDRESS"/>
    </org.eventb.core.poPredicateSet>
    <org.eventb.core.poPredicateSet name="EVTALLHYPreceived_target_transaction|" org.eventb.core.parentSet="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#EVTIDENTreceived_target_transaction\|" org.eventb.core.poStamp="0">
        <org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="user_address∈dom(accounts)" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_m2|org.eventb.core.event#_8rz-A77uEe6laZimEYihUg|org.eventb.core.guard#_XviPIcEBEe6yC4BToIaAqA"/>
        <org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="accounts(user_address)≥validator_fee+transfer_amount" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_m2|org.eventb.core.event#_8rz-A77uEe6laZimEYihUg|org.eventb.core.guard#_XviPIsEBEe6yC4BToIaAqA"/>
        <org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="validator_fee&gt;0" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_m2|org.eventb.core.event#_8rz-A77uEe6laZimEYihUg|org.eventb.core.guard#_XviPI8EBEe6yC4BToIaAqA"/>
        <org.eventb.core.poPredicate name="PRD3" org.eventb.core.predicate="transfer_amount&gt;0" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_m2|org.eventb.core.event#_8rz-A77uEe6laZimEYihUg|org.eventb.core.guard#_Xvi2MMEBEe6yC4BToIaAqA"/>
        <org.eventb.core.poPredicate name="PRD4" org.eventb.core.predicate="gateway_address∈dom(accounts)" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_m2|org.eventb.core.event#_8rz-A77uEe6laZimEYihUg|org.eventb.core.guard#_Xvi2McEBEe6yC4BToIaAqA"/>
        <org.eventb.core.poPredicate name="PRD5" org.eventb.core.predicate="({user_address,gateway_address} ⩤ accounts)∪{gateway_address ↦ accounts(gateway_address)+transfer_amount}∪{user_address ↦ accounts(user_address) − transfer_amount − validator_fee}∈ADDRESS ⇸ ℕ" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_m2|org.eventb.core.event#_8rz-A77uEe6laZimEYihUg|org.eventb.core.guard#_Xvi2MsEBEe6yC4BToIaAqA"/>
    </org.eventb.core.poPredicateSet>
    <org.eventb.core.poPredicateSet name="ALLHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bpo|org.eventb.core.poFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poStamp="23">
        <org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="subscribed∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.invariant#_qWNdEMEGEe6yC4BToIaAqA"/>
        <org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="initiated∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.invariant#_qWNdEcEGEe6yC4BToIaAqA"/>
        <org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="emitted∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.invariant#_qWNdEsEGEe6yC4BToIaAqA"/>
        <org.eventb.core.poPredicate name="PRD3" org.eventb.core.predicate="gateway_processing∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.invariant#_qWNdE8EGEe6yC4BToIaAqA"/>
        <org.eventb.core.poPredicate name="PRD4" org.eventb.core.predicate="submit_cc_tx∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.invariant#_qWNdFMEGEe6yC4BToIaAqA"/>
        <org.eventb.core.poPredicate name="PRD5" org.eventb.core.predicate="wallet_created∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.invariant#_qWOEIMEGEe6yC4BToIaAqA"/>
        <org.eventb.core.poPredicate name="PRD6" org.eventb.core.predicate="wallet_amount∈ℕ" org.eventb.core.source="/gateway-event-b/CCTx_Fabric_Ethereum_Animation_m3.bum|org.eventb.core.machineFile#CCTx_Fabric_Ethereum_Animation_m3|org.eventb.core.invariant#_9cXZIMEHEe6yC4BToIaAqA"/>
    </org.eventb.core.poPredicateSet>
</org.eventb.core.poFile>