Newer
Older
<?xml version="1.0" encoding="UTF-8" standalone="no"?>
<org.eventb.core.poFile org.eventb.core.poStamp="0">
<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="0">
<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="grants" org.eventb.core.type="ℙ(USERS×PERMISSIONS)"/>
<org.eventb.core.poIdentifier name="triggered" org.eventb.core.type="ℤ"/>
<org.eventb.core.poIdentifier name="write_granted" 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="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="grants∈authenticated_users ↔ PERMISSIONS" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.invariant#_OTstIMHNEe609fto5wotHA"/>
<org.eventb.core.poPredicate name="received_cross_chain_transaction}" org.eventb.core.predicate="∀u⦂USERS·u∈authenticated_transactions[received_cross_chain_transactions]⇒u ↦ write∈grants" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.invariant#_jCLrMcHJEe6yC4BToIaAqA"/>
</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="0">
<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#_DmAl8MHOEe609fto5wotHA"/>
<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#_DmAl8MHOEe609fto5wotHA"/>
<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="0">
<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#_DmB0EMHOEe609fto5wotHA"/>
<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#_DmB0EMHOEe609fto5wotHA"/>
<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="0">
<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#_DmCbIMHOEe609fto5wotHA"/>
<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#_DmCbIMHOEe609fto5wotHA"/>
<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="0">
<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#_DmDCMMHOEe609fto5wotHA"/>
<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#_DmDCMMHOEe609fto5wotHA"/>
<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="0">
<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#_DmDpQMHOEe609fto5wotHA"/>
<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#_DmDpQMHOEe609fto5wotHA"/>
<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="0">
<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#_DmEQUMHOEe609fto5wotHA"/>
<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#_DmEQUMHOEe609fto5wotHA"/>
<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.poSequent name="INITIALISATION/inv17/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant establishment" org.eventb.core.poStamp="0">
<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#_2MNd0MHOEe609fto5wotHA"/>
<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#_2MNd0MHOEe609fto5wotHA"/>
<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\/inv17\/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#PRD6"/>
</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="0">
<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="write_granted'" org.eventb.core.type="ℤ"/>
<org.eventb.core.poIdentifier name="subscribed'" org.eventb.core.type="ℤ"/>
<org.eventb.core.poIdentifier name="received_transactions'" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×TRANSACTIONS)"/>
<org.eventb.core.poIdentifier name="subscriptions'" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_SMART_CONTRACTS)"/>
<org.eventb.core.poIdentifier name="received_cross_chain_transactions'" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_TRANSACTIONS)"/>
<org.eventb.core.poIdentifier name="user_created'" org.eventb.core.type="ℤ"/>
<org.eventb.core.poIdentifier name="grants'" org.eventb.core.type="ℙ(USERS×PERMISSIONS)"/>
<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="0"/>
<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="0">
<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#_DmAl8MHOEe609fto5wotHA"/>
<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#_DmAl8MHOEe609fto5wotHA"/>
<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="0">
<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="0">
<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="0">
<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#_DmB0EMHOEe609fto5wotHA"/>
<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#_DmB0EMHOEe609fto5wotHA"/>
<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="0">
<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#_DmDpQMHOEe609fto5wotHA"/>
<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#_DmDpQMHOEe609fto5wotHA"/>
<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="0">
<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="0">
<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="0">
<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#_DmB0EMHOEe609fto5wotHA"/>
<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#_DmB0EMHOEe609fto5wotHA"/>
<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="0">
<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#_DmCbIMHOEe609fto5wotHA"/>
<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#_DmCbIMHOEe609fto5wotHA"/>
<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="0">
<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#_DmDpQMHOEe609fto5wotHA"/>
<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#_DmDpQMHOEe609fto5wotHA"/>
<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="0">
<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="0">
<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="0">
<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#_DmCbIMHOEe609fto5wotHA"/>
<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#_DmCbIMHOEe609fto5wotHA"/>
<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="0">
<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#_DmDCMMHOEe609fto5wotHA"/>
<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#_DmDCMMHOEe609fto5wotHA"/>
<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="0">
<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#_DmDpQMHOEe609fto5wotHA"/>
<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#_DmDpQMHOEe609fto5wotHA"/>
<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="0">
<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="0">
<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="0">
<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#_DmDCMMHOEe609fto5wotHA"/>
<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#_DmDCMMHOEe609fto5wotHA"/>
<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="0">
<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#_DmDpQMHOEe609fto5wotHA"/>
<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#_DmDpQMHOEe609fto5wotHA"/>
<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="0">
<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="0">
<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∈grants" 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.poSequent name="CREATE_GATEWAY_USER/inv16/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0">
<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_transactionz"/>
<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#_DmEQUMHOEe609fto5wotHA"/>
<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#_K_21gMEXEe6yC4BToIaAqA"/>
<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#_yREdbb7uEe6laZimEYihUn"/>
<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#_DmEQUMHOEe609fto5wotHA"/>
<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#CREATE_GATEWAY_USER\/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_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.poIdentifier name="user_created'" org.eventb.core.type="ℤ"/>
</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>
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
<org.eventb.core.poSequent name="GRANT_PERMISSION/inv17/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant preservation" org.eventb.core.poStamp="0">
<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_transaction{"/>
<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#_2MNd0MHOEe609fto5wotHA"/>
<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#_KHHS0MEbEe6yC4BToIaAqA"/>
<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#_yREdbb7uEe6laZimEYihUo"/>
<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#_2MNd0MHOEe609fto5wotHA"/>
<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#GRANT_PERMISSION\/inv17\/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#PRD6"/>
</org.eventb.core.poSequent>
<org.eventb.core.poPredicateSet name="EVTIDENTreceived_cross_chain_transaction{" 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="permission" org.eventb.core.type="PERMISSIONS"/>
<org.eventb.core.poIdentifier name="write_granted'" org.eventb.core.type="ℤ"/>
<org.eventb.core.poIdentifier name="user" org.eventb.core.type="USERS"/>
<org.eventb.core.poIdentifier name="grants'" org.eventb.core.type="ℙ(USERS×PERMISSIONS)"/>
</org.eventb.core.poPredicateSet>
<org.eventb.core.poPredicateSet name="EVTALLHYPreceived_cross_chain_transaction{" 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_transaction{" org.eventb.core.poStamp="0">
<org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="permission∈PERMISSIONS" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_KHHS0MEbEe6yC4BToIaAqA|org.eventb.core.guard#_KHH54cEbEe6yC4BToIaAqA"/>
<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#_KHHS0MEbEe6yC4BToIaAqA|org.eventb.core.guard#_KHH54sEbEe6yC4BToIaAqA"/>
<org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="user ↦ permission∉grants" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_m2.bum|org.eventb.core.machineFile#CCTx_Ethereum_Fabric_m2|org.eventb.core.event#_KHHS0MEbEe6yC4BToIaAqA|org.eventb.core.guard#_5yZW0MHNEe609fto5wotHA"/>
<org.eventb.core.poPredicate name="PRD3" org.eventb.core.predicate="user=gateway_user" 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#_yREdbb7uEe6laZimEYihUo|org.eventb.core.guard#_yeWE8cHOEe609fto5wotHA"/>
<org.eventb.core.poPredicate name="PRD4" org.eventb.core.predicate="permission=write" 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#_yREdbb7uEe6laZimEYihUo|org.eventb.core.guard#_-iJ1EMHOEe609fto5wotHA"/>
</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="0">
<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#_DmAl8MHOEe609fto5wotHA"/>
<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#_DmB0EMHOEe609fto5wotHA"/>
<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#_DmCbIMHOEe609fto5wotHA"/>
<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#_DmDCMMHOEe609fto5wotHA"/>
<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#_DmDpQMHOEe609fto5wotHA"/>
<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#_DmEQUMHOEe609fto5wotHA"/>
<org.eventb.core.poPredicate name="PRD6" org.eventb.core.predicate="write_granted∈{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#_2MNd0MHOEe609fto5wotHA"/>
</org.eventb.core.poPredicateSet>
</org.eventb.core.poFile>