Fix proofs

.project

+<?xml version="1.0" encoding="UTF-8"?>
+<projectDescription>
+	<name>cross-chain-transactions-event-b</name>
+	<comment></comment>
+	<projects>
+	</projects>
+	<buildSpec>
+	</buildSpec>
+	<natures>
+	</natures>
+</projectDescription>

BIG/BIG_m1.bcm

@@ -14,8 +14,8 @@
         <org.eventb.core.scCarrierSet name="TRANSACTIONS" org.eventb.core.source="/BIG/BIG_c1.buc|org.eventb.core.contextFile#BIG_c1|org.eventb.core.carrierSet#_OLUJEKsXEe6I4bA9GxwhqQ" org.eventb.core.type="ℙ(TRANSACTIONS)"/>
         <org.eventb.core.scCarrierSet name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.source="/BIG/BIG_c1.buc|org.eventb.core.contextFile#BIG_c1|org.eventb.core.carrierSet#_ISeO4KmBEe6I4bA9GxwhqQ" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
     </org.eventb.core.scInternalContext>
-    <org.eventb.core.scInvariant name="BIG_c2" org.eventb.core.label="inv1;" org.eventb.core.predicate="received_transactions∈CROSS_CHAIN_SMART_CONTRACTS ↠ TRANSACTIONS" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_o6juoKviEe6I4bA9GxwhqQ" org.eventb.core.theorem="false"/>
-    <org.eventb.core.scInvariant name="BIG_c3" org.eventb.core.label="inv2;" org.eventb.core.predicate="triggered_events∈CROSS_CHAIN_SMART_CONTRACTS ↠ CROSS_CHAIN_EVENTS" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_d6dcQKmHEe6I4bA9GxwhqQ" org.eventb.core.theorem="false"/>
+    <org.eventb.core.scInvariant name="BIG_c2" org.eventb.core.label="inv1;" org.eventb.core.predicate="received_transactions∈CROSS_CHAIN_SMART_CONTRACTS ↔ TRANSACTIONS" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_o6juoKviEe6I4bA9GxwhqQ" org.eventb.core.theorem="false"/>
+    <org.eventb.core.scInvariant name="BIG_c3" org.eventb.core.label="inv2;" org.eventb.core.predicate="triggered_events∈CROSS_CHAIN_SMART_CONTRACTS ↔ CROSS_CHAIN_EVENTS" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_d6dcQKmHEe6I4bA9GxwhqQ" org.eventb.core.theorem="false"/>
     <org.eventb.core.scInvariant name="BIG_c4" org.eventb.core.label="inv3;" org.eventb.core.predicate="subscriptions∈GATEWAYS ↔ CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_Q6dKkKpAEe6I4bA9GxwhqQ" org.eventb.core.theorem="false"/>
     <org.eventb.core.scInvariant name="BIG_c5" org.eventb.core.label="inv4;" org.eventb.core.predicate="gateway_pending_transactions∈GATEWAYS ↔ CROSS_CHAIN_TRANSACTIONS" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_c7TQ0KpBEe6I4bA9GxwhqQ" org.eventb.core.theorem="false"/>
     <org.eventb.core.scInvariant name="BIG_c6" org.eventb.core.label="inv6;" org.eventb.core.predicate="received_cross_chain_transactions∈CROSS_CHAIN_SMART_CONTRACTS ↔ CROSS_CHAIN_TRANSACTIONS" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_G1eDUKpbEe6I4bA9GxwhqQ" org.eventb.core.theorem="false"/>

BIG/BIG_m1.bpo

 <?xml version="1.0" encoding="UTF-8" standalone="no"?>
-<org.eventb.core.poFile org.eventb.core.poStamp="116">
+<org.eventb.core.poFile org.eventb.core.poStamp="118">
     <org.eventb.core.poPredicateSet name="CTXHYP" org.eventb.core.poStamp="113">
         <org.eventb.core.poIdentifier name="CROSS_CHAIN_EVENTS" org.eventb.core.type="ℙ(CROSS_CHAIN_EVENTS)"/>
         <org.eventb.core.poIdentifier name="CROSS_CHAIN_TRANSACTIONS" org.eventb.core.type="ℙ(CROSS_CHAIN_TRANSACTIONS)"/>
@@ -13,108 +13,69 @@
         <org.eventb.core.poPredicate name="CROSS_CHAIN_SMART_CONTRACTU" org.eventb.core.predicate="target_smart_contract∈CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.source="/BIG/BIG_c1.buc|org.eventb.core.contextFile#BIG_c1|org.eventb.core.axiom#_j4-vYKsXEe6I4bA9GxwhqQ"/>
         <org.eventb.core.poPredicate name="CROSS_CHAIN_SMART_CONTRACTV" org.eventb.core.predicate="gateway∈GATEWAYS" org.eventb.core.source="/BIG/BIG_c1.buc|org.eventb.core.contextFile#BIG_c1|org.eventb.core.axiom#_j4-vYasXEe6I4bA9GxwhqQ"/>
     </org.eventb.core.poPredicateSet>
-    <org.eventb.core.poPredicateSet name="ABSHYP" org.eventb.core.parentSet="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poStamp="116">
+    <org.eventb.core.poPredicateSet name="ABSHYP" org.eventb.core.parentSet="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poStamp="117">
         <org.eventb.core.poIdentifier name="triggered_events" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_EVENTS)"/>
         <org.eventb.core.poIdentifier name="received_cross_chain_transactions" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_TRANSACTIONS)"/>
+        <org.eventb.core.poIdentifier name="subscriptions" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_SMART_CONTRACTS)"/>
         <org.eventb.core.poIdentifier name="gateway_pending_transactions" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_TRANSACTIONS)"/>
         <org.eventb.core.poIdentifier name="received_transactions" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×TRANSACTIONS)"/>
     </org.eventb.core.poPredicateSet>
-    <org.eventb.core.poSequent name="INITIALISATION/inv11;/INV" org.eventb.core.accurate="false" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="116">
-        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#EVTALLHYPreceived_cross_chain_transactiont"/>
-        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="(∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×TRANSACTIONS))∈CROSS_CHAIN_SMART_CONTRACTS ↠ TRANSACTIONS" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_asVK0KvhEe6I4bA9GxwhqQ"/>
-        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#'"/>
-        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_asVK0KvhEe6I4bA9GxwhqQ"/>
-        <org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poSequent#INITIALISATION\/inv11;\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
-        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD0"/>
-    </org.eventb.core.poSequent>
-    <org.eventb.core.poSequent name="INITIALISATION/inv2;/INV" org.eventb.core.accurate="false" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="116">
-        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#EVTALLHYPreceived_cross_chain_transactiont"/>
-        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="(∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_EVENTS))∈CROSS_CHAIN_SMART_CONTRACTS ↠ CROSS_CHAIN_EVENTS" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_d6dcQKmHEe6I4bA9GxwhqQ"/>
-        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#'"/>
-        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_d6dcQKmHEe6I4bA9GxwhqQ"/>
-        <org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poSequent#INITIALISATION\/inv2;\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
-        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD1"/>
-    </org.eventb.core.poSequent>
-    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_cross_chain_transactiont" org.eventb.core.parentSet="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poStamp="116">
+    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_cross_chain_transactiont" org.eventb.core.parentSet="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poStamp="117">
         <org.eventb.core.poIdentifier name="triggered_events'" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_EVENTS)"/>
         <org.eventb.core.poIdentifier name="gateway_pending_transactions'" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_TRANSACTIONS)"/>
         <org.eventb.core.poIdentifier name="received_transactions'" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×TRANSACTIONS)"/>
+        <org.eventb.core.poIdentifier name="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.poPredicateSet>
-    <org.eventb.core.poPredicateSet name="EVTALLHYPreceived_cross_chain_transactiont" org.eventb.core.parentSet="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#EVTIDENTreceived_cross_chain_transactiont" org.eventb.core.poStamp="116"/>
-    <org.eventb.core.poPredicateSet name="EVTALLHYPreceived_cross_chain_transactionu" org.eventb.core.parentSet="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="116"/>
-    <org.eventb.core.poSequent name="SUBMIT_CROSS_CHAIN_TRANSACTION/inv11;/INV" org.eventb.core.accurate="false" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="116">
-        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#EVTALLHYPreceived_cross_chain_transactionv"/>
-        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="received_transactions∪{source_smart_contract ↦ transaction}∈CROSS_CHAIN_SMART_CONTRACTS ↠ TRANSACTIONS" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_asVK0KvhEe6I4bA9GxwhqQ"/>
-        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_58YTEKmAEe6I4bA9GxwhqQ"/>
-        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_asVK0KvhEe6I4bA9GxwhqQ"/>
-        <org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poSequent#SUBMIT_CROSS_CHAIN_TRANSACTION\/inv11;\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
-        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD0"/>
-    </org.eventb.core.poSequent>
-    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_cross_chain_transactionv" org.eventb.core.parentSet="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="116">
+    <org.eventb.core.poPredicateSet name="EVTALLHYPreceived_cross_chain_transactiont" org.eventb.core.parentSet="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#EVTIDENTreceived_cross_chain_transactiont" org.eventb.core.poStamp="117"/>
+    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_cross_chain_transactionu" org.eventb.core.parentSet="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="118">
+        <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="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#EVTIDENTreceived_cross_chain_transactionu" org.eventb.core.poStamp="118">
+        <org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="gateway ↦ source_smart_contract∉subscriptions" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_I9G5gKpAEe6I4bA9GxwhqQ|org.eventb.core.guard#_SAx1UKmDEe6I4bA9GxwhqQ"/>
+    </org.eventb.core.poPredicateSet>
+    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_cross_chain_transactionv" org.eventb.core.parentSet="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="118">
         <org.eventb.core.poIdentifier name="transaction" org.eventb.core.type="TRANSACTIONS"/>
         <org.eventb.core.poIdentifier name="received_transactions'" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×TRANSACTIONS)"/>
     </org.eventb.core.poPredicateSet>
-    <org.eventb.core.poPredicateSet name="EVTALLHYPreceived_cross_chain_transactionv" org.eventb.core.parentSet="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#EVTIDENTreceived_cross_chain_transactionv" org.eventb.core.poStamp="116">
+    <org.eventb.core.poPredicateSet name="EVTALLHYPreceived_cross_chain_transactionv" org.eventb.core.parentSet="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#EVTIDENTreceived_cross_chain_transactionv" org.eventb.core.poStamp="118">
         <org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="transaction∈TRANSACTIONS" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_58YTEKmAEe6I4bA9GxwhqQ|org.eventb.core.guard#_TlWCkqmHEe6I4bA9GxwhqQ"/>
         <org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="transaction∉received_transactions[{source_smart_contract}]" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_58YTEKmAEe6I4bA9GxwhqQ|org.eventb.core.guard#_HCtL8KmIEe6I4bA9GxwhqQ"/>
     </org.eventb.core.poPredicateSet>
-    <org.eventb.core.poSequent name="PROCESS_CROSS_CHAIN_TRANSACTION/inv11;/INV" org.eventb.core.accurate="false" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="116">
-        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#EVTALLHYPreceived_cross_chain_transactionw"/>
-        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="received_transactions ∖ {source_smart_contract ↦ transaction}∈CROSS_CHAIN_SMART_CONTRACTS ↠ TRANSACTIONS" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_asVK0KvhEe6I4bA9GxwhqQ"/>
-        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_TlWCkKmHEe6I4bA9GxwhqQ"/>
-        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_asVK0KvhEe6I4bA9GxwhqQ"/>
-        <org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poSequent#PROCESS_CROSS_CHAIN_TRANSACTION\/inv11;\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
-        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD0"/>
-    </org.eventb.core.poSequent>
-    <org.eventb.core.poSequent name="PROCESS_CROSS_CHAIN_TRANSACTION/inv2;/INV" org.eventb.core.accurate="false" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="116">
-        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#EVTALLHYPreceived_cross_chain_transactionw"/>
-        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="triggered_events∪{source_smart_contract ↦ cross_chain_event}∈CROSS_CHAIN_SMART_CONTRACTS ↠ CROSS_CHAIN_EVENTS" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_d6dcQKmHEe6I4bA9GxwhqQ"/>
-        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_TlWCkKmHEe6I4bA9GxwhqQ"/>
-        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_d6dcQKmHEe6I4bA9GxwhqQ"/>
-        <org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poSequent#PROCESS_CROSS_CHAIN_TRANSACTION\/inv2;\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
-        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD1"/>
-    </org.eventb.core.poSequent>
-    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_cross_chain_transactionw" org.eventb.core.parentSet="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="116">
+    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_cross_chain_transactionw" org.eventb.core.parentSet="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="118">
         <org.eventb.core.poIdentifier name="triggered_events'" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_EVENTS)"/>
         <org.eventb.core.poIdentifier name="transaction" org.eventb.core.type="TRANSACTIONS"/>
         <org.eventb.core.poIdentifier name="cross_chain_event" org.eventb.core.type="CROSS_CHAIN_EVENTS"/>
         <org.eventb.core.poIdentifier name="received_transactions'" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×TRANSACTIONS)"/>
     </org.eventb.core.poPredicateSet>
-    <org.eventb.core.poPredicateSet name="EVTALLHYPreceived_cross_chain_transactionw" org.eventb.core.parentSet="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#EVTIDENTreceived_cross_chain_transactionw" org.eventb.core.poStamp="116">
+    <org.eventb.core.poPredicateSet name="EVTALLHYPreceived_cross_chain_transactionw" org.eventb.core.parentSet="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#EVTIDENTreceived_cross_chain_transactionw" org.eventb.core.poStamp="118">
         <org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="source_smart_contract ↦ transaction∈received_transactions" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_TlWCkKmHEe6I4bA9GxwhqQ|org.eventb.core.guard#_iUmtQKpAEe6I4bA9GxwhqQ"/>
         <org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="cross_chain_event∉triggered_events[{source_smart_contract}]" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_TlWCkKmHEe6I4bA9GxwhqQ|org.eventb.core.guard#_1SOwwKmDEe6I4bA9GxwhqQ"/>
     </org.eventb.core.poPredicateSet>
-    <org.eventb.core.poSequent name="LISTEN_SMART_CONTRACT_EVENT/inv2;/INV" org.eventb.core.accurate="false" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="116">
-        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#EVTALLHYPreceived_cross_chain_transactionx"/>
-        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="triggered_events ∖ {source_smart_contract ↦ cross_chain_event}∈CROSS_CHAIN_SMART_CONTRACTS ↠ CROSS_CHAIN_EVENTS" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_d6dcQKmHEe6I4bA9GxwhqQ"/>
-        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_8VKFEKpAEe6I4bA9GxwhqQ"/>
-        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_d6dcQKmHEe6I4bA9GxwhqQ"/>
-        <org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poSequent#LISTEN_SMART_CONTRACT_EVENT\/inv2;\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
-        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD1"/>
-    </org.eventb.core.poSequent>
-    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_cross_chain_transactionx" org.eventb.core.parentSet="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="116">
+    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_cross_chain_transactionx" org.eventb.core.parentSet="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="118">
         <org.eventb.core.poIdentifier name="cross_chain_transaction" org.eventb.core.type="CROSS_CHAIN_TRANSACTIONS"/>
         <org.eventb.core.poIdentifier name="triggered_events'" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_EVENTS)"/>
         <org.eventb.core.poIdentifier name="gateway_pending_transactions'" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_TRANSACTIONS)"/>
         <org.eventb.core.poIdentifier name="cross_chain_event" org.eventb.core.type="CROSS_CHAIN_EVENTS"/>
     </org.eventb.core.poPredicateSet>
-    <org.eventb.core.poPredicateSet name="EVTALLHYPreceived_cross_chain_transactionx" org.eventb.core.parentSet="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#EVTIDENTreceived_cross_chain_transactionx" org.eventb.core.poStamp="116">
+    <org.eventb.core.poPredicateSet name="EVTALLHYPreceived_cross_chain_transactionx" org.eventb.core.parentSet="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#EVTIDENTreceived_cross_chain_transactionx" org.eventb.core.poStamp="118">
         <org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="source_smart_contract ↦ cross_chain_event∈triggered_events" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_8VKFEKpAEe6I4bA9GxwhqQ|org.eventb.core.guard#_DMOGsKpFEe6I4bA9GxwhqQ"/>
-        <org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="gateway ↦ cross_chain_transaction∉gateway_pending_transactions" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_8VKFEKpAEe6I4bA9GxwhqQ|org.eventb.core.guard#_x51DwKpCEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="gateway ↦ source_smart_contract∈subscriptions" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_8VKFEKpAEe6I4bA9GxwhqQ|org.eventb.core.guard#_AezaEKmIEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="gateway ↦ cross_chain_transaction∉gateway_pending_transactions" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_8VKFEKpAEe6I4bA9GxwhqQ|org.eventb.core.guard#_x51DwKpCEe6I4bA9GxwhqQ"/>
     </org.eventb.core.poPredicateSet>
-    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_cross_chain_transactiony" org.eventb.core.parentSet="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="116">
+    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_cross_chain_transactiony" org.eventb.core.parentSet="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="118">
         <org.eventb.core.poIdentifier name="cross_chain_transaction" org.eventb.core.type="CROSS_CHAIN_TRANSACTIONS"/>
         <org.eventb.core.poIdentifier name="gateway_pending_transactions'" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_TRANSACTIONS)"/>
         <org.eventb.core.poIdentifier name="received_cross_chain_transactions'" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_TRANSACTIONS)"/>
     </org.eventb.core.poPredicateSet>
-    <org.eventb.core.poPredicateSet name="EVTALLHYPreceived_cross_chain_transactiony" org.eventb.core.parentSet="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#EVTIDENTreceived_cross_chain_transactiony" org.eventb.core.poStamp="116">
+    <org.eventb.core.poPredicateSet name="EVTALLHYPreceived_cross_chain_transactiony" org.eventb.core.parentSet="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#EVTIDENTreceived_cross_chain_transactiony" org.eventb.core.poStamp="118">
         <org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="gateway ↦ cross_chain_transaction∈gateway_pending_transactions" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_0sEN8KpaEe6I4bA9GxwhqQ|org.eventb.core.guard#_tUzFcKpaEe6I4bA9GxwhqQ"/>
     </org.eventb.core.poPredicateSet>
-    <org.eventb.core.poPredicateSet name="ALLHYP" org.eventb.core.parentSet="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poStamp="116">
-        <org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="received_transactions∈CROSS_CHAIN_SMART_CONTRACTS ↠ TRANSACTIONS" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_asVK0KvhEe6I4bA9GxwhqQ"/>
-        <org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="triggered_events∈CROSS_CHAIN_SMART_CONTRACTS ↠ CROSS_CHAIN_EVENTS" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_d6dcQKmHEe6I4bA9GxwhqQ"/>
-        <org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="gateway_pending_transactions∈GATEWAYS ↔ CROSS_CHAIN_TRANSACTIONS" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_c7TQ0KpBEe6I4bA9GxwhqQ"/>
-        <org.eventb.core.poPredicate name="PRD3" org.eventb.core.predicate="received_cross_chain_transactions∈CROSS_CHAIN_SMART_CONTRACTS ↔ CROSS_CHAIN_TRANSACTIONS" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_G1eDUKpbEe6I4bA9GxwhqQ"/>
+    <org.eventb.core.poPredicateSet name="ALLHYP" org.eventb.core.parentSet="/BIG/BIG_m1.bpo|org.eventb.core.poFile#BIG_m1|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poStamp="118">
+        <org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="received_transactions∈CROSS_CHAIN_SMART_CONTRACTS ↔ TRANSACTIONS" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_o6juoKviEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="triggered_events∈CROSS_CHAIN_SMART_CONTRACTS ↔ CROSS_CHAIN_EVENTS" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_d6dcQKmHEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="subscriptions∈GATEWAYS ↔ CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_Q6dKkKpAEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.poPredicate name="PRD3" org.eventb.core.predicate="gateway_pending_transactions∈GATEWAYS ↔ CROSS_CHAIN_TRANSACTIONS" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_c7TQ0KpBEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.poPredicate name="PRD4" org.eventb.core.predicate="received_cross_chain_transactions∈CROSS_CHAIN_SMART_CONTRACTS ↔ CROSS_CHAIN_TRANSACTIONS" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_G1eDUKpbEe6I4bA9GxwhqQ"/>
     </org.eventb.core.poPredicateSet>
 </org.eventb.core.poFile>

BIG/BIG_m1.bpo_tmp

-<?xml version="1.0" encoding="UTF-8"?>
-<org.eventb.core.poFile/>
\ No newline at end of file

BIG/BIG_m1.bpr

@@ -133,17 +133,10 @@
                         <org.eventb.core.prHypAction name="HIDE3" org.eventb.core.prHyps="p5"/>
                         <org.eventb.core.prHypAction name="HIDE4" org.eventb.core.prHyps="p6"/>
                         <org.eventb.core.prHypAction name="HIDE5" org.eventb.core.prHyps="p7"/>
-                        <org.eventb.core.prHypAction name="HIDE6" org.eventb.core.prHyps="p8"/>
-                        <org.eventb.core.prHypAction name="HIDE7" org.eventb.core.prHyps="p9"/>
                     </org.eventb.core.prAnte>
                 </org.eventb.core.prRule>
             </org.eventb.core.prAnte>
         </org.eventb.core.prRule>
-        <org.eventb.core.prPred name="p6" org.eventb.core.predicate="subscriptions∈GATEWAYS ↔ CROSS_CHAIN_SMART_CONTRACTS">
-            <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
-            <org.eventb.core.prIdent name="GATEWAYS" org.eventb.core.type="ℙ(GATEWAYS)"/>
-            <org.eventb.core.prIdent name="subscriptions" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_SMART_CONTRACTS)"/>
-        </org.eventb.core.prPred>
         <org.eventb.core.prPred name="p1" org.eventb.core.predicate="¬transaction∈received_transactions[{source_smart_contract}]">
             <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
             <org.eventb.core.prIdent name="TRANSACTIONS" org.eventb.core.type="ℙ(TRANSACTIONS)"/>
@@ -155,11 +148,6 @@
             <org.eventb.core.prIdent name="GATEWAYS" org.eventb.core.type="ℙ(GATEWAYS)"/>
             <org.eventb.core.prIdent name="gateway" org.eventb.core.type="GATEWAYS"/>
         </org.eventb.core.prPred>
-        <org.eventb.core.prPred name="p5" org.eventb.core.predicate="triggered_events∈CROSS_CHAIN_SMART_CONTRACTS ↔ CROSS_CHAIN_EVENTS">
-            <org.eventb.core.prIdent name="CROSS_CHAIN_EVENTS" org.eventb.core.type="ℙ(CROSS_CHAIN_EVENTS)"/>
-            <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
-            <org.eventb.core.prIdent name="triggered_events" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_EVENTS)"/>
-        </org.eventb.core.prPred>
         <org.eventb.core.prPred name="p0" org.eventb.core.predicate="transaction∉received_transactions[{source_smart_contract}]">
             <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
             <org.eventb.core.prIdent name="TRANSACTIONS" org.eventb.core.type="ℙ(TRANSACTIONS)"/>
@@ -167,7 +155,7 @@
             <org.eventb.core.prIdent name="source_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
             <org.eventb.core.prIdent name="transaction" org.eventb.core.type="TRANSACTIONS"/>
         </org.eventb.core.prPred>
-        <org.eventb.core.prPred name="p9" org.eventb.core.predicate="transaction∈TRANSACTIONS">
+        <org.eventb.core.prPred name="p7" org.eventb.core.predicate="transaction∈TRANSACTIONS">
             <org.eventb.core.prIdent name="TRANSACTIONS" org.eventb.core.type="ℙ(TRANSACTIONS)"/>
             <org.eventb.core.prIdent name="transaction" org.eventb.core.type="TRANSACTIONS"/>
         </org.eventb.core.prPred>
@@ -175,7 +163,7 @@
             <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
             <org.eventb.core.prIdent name="source_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
         </org.eventb.core.prPred>
-        <org.eventb.core.prPred name="p7" org.eventb.core.predicate="gateway_pending_transactions∈GATEWAYS ↔ CROSS_CHAIN_TRANSACTIONS">
+        <org.eventb.core.prPred name="p5" org.eventb.core.predicate="gateway_pending_transactions∈GATEWAYS ↔ CROSS_CHAIN_TRANSACTIONS">
             <org.eventb.core.prIdent name="CROSS_CHAIN_TRANSACTIONS" org.eventb.core.type="ℙ(CROSS_CHAIN_TRANSACTIONS)"/>
             <org.eventb.core.prIdent name="GATEWAYS" org.eventb.core.type="ℙ(GATEWAYS)"/>
             <org.eventb.core.prIdent name="gateway_pending_transactions" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_TRANSACTIONS)"/>
@@ -184,7 +172,7 @@
             <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
             <org.eventb.core.prIdent name="target_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
         </org.eventb.core.prPred>
-        <org.eventb.core.prPred name="p8" org.eventb.core.predicate="received_cross_chain_transactions∈CROSS_CHAIN_SMART_CONTRACTS ↔ CROSS_CHAIN_TRANSACTIONS">
+        <org.eventb.core.prPred name="p6" org.eventb.core.predicate="received_cross_chain_transactions∈CROSS_CHAIN_SMART_CONTRACTS ↔ CROSS_CHAIN_TRANSACTIONS">
             <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
             <org.eventb.core.prIdent name="CROSS_CHAIN_TRANSACTIONS" org.eventb.core.type="ℙ(CROSS_CHAIN_TRANSACTIONS)"/>
             <org.eventb.core.prIdent name="received_cross_chain_transactions" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_TRANSACTIONS)"/>
@@ -193,6 +181,84 @@
         <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.typeRewrites:1"/>
     </org.eventb.core.prProof>
     <org.eventb.core.prProof name="PROCESS_CROSS_CHAIN_TRANSACTION/inv11;/INV" org.eventb.core.confidence="0" org.eventb.core.prFresh="" org.eventb.core.prHyps="">
+        <org.eventb.core.lang name="L"/>
+        <org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prHyps="">
+            <org.eventb.core.prAnte name="'">
+                <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p0" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p1"/>
+                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="type rewrites" org.eventb.core.prHyps="">
+                    <org.eventb.core.prAnte name="'">
+                        <org.eventb.core.prHypAction name="HIDE0" org.eventb.core.prHyps="p2"/>
+                        <org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p3"/>
+                        <org.eventb.core.prHypAction name="HIDE2" org.eventb.core.prHyps="p4"/>
+                        <org.eventb.core.prHypAction name="HIDE3" org.eventb.core.prHyps="p5"/>
+                        <org.eventb.core.prHypAction name="HIDE4" org.eventb.core.prHyps="p6"/>
+                    </org.eventb.core.prAnte>
+                </org.eventb.core.prRule>
+            </org.eventb.core.prAnte>
+        </org.eventb.core.prRule>
+        <org.eventb.core.prPred name="p4" org.eventb.core.predicate="gateway∈GATEWAYS">
+            <org.eventb.core.prIdent name="GATEWAYS" org.eventb.core.type="ℙ(GATEWAYS)"/>
+            <org.eventb.core.prIdent name="gateway" org.eventb.core.type="GATEWAYS"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="¬cross_chain_event∈triggered_events[{source_smart_contract}]">
+            <org.eventb.core.prIdent name="CROSS_CHAIN_EVENTS" org.eventb.core.type="ℙ(CROSS_CHAIN_EVENTS)"/>
+            <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
+            <org.eventb.core.prIdent name="cross_chain_event" org.eventb.core.type="CROSS_CHAIN_EVENTS"/>
+            <org.eventb.core.prIdent name="source_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
+            <org.eventb.core.prIdent name="triggered_events" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_EVENTS)"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="cross_chain_event∉triggered_events[{source_smart_contract}]">
+            <org.eventb.core.prIdent name="CROSS_CHAIN_EVENTS" org.eventb.core.type="ℙ(CROSS_CHAIN_EVENTS)"/>
+            <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
+            <org.eventb.core.prIdent name="cross_chain_event" org.eventb.core.type="CROSS_CHAIN_EVENTS"/>
+            <org.eventb.core.prIdent name="source_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
+            <org.eventb.core.prIdent name="triggered_events" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_EVENTS)"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="source_smart_contract∈CROSS_CHAIN_SMART_CONTRACTS">
+            <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
+            <org.eventb.core.prIdent name="source_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p5" org.eventb.core.predicate="gateway_pending_transactions∈GATEWAYS ↔ CROSS_CHAIN_TRANSACTIONS">
+            <org.eventb.core.prIdent name="CROSS_CHAIN_TRANSACTIONS" org.eventb.core.type="ℙ(CROSS_CHAIN_TRANSACTIONS)"/>
+            <org.eventb.core.prIdent name="GATEWAYS" org.eventb.core.type="ℙ(GATEWAYS)"/>
+            <org.eventb.core.prIdent name="gateway_pending_transactions" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_TRANSACTIONS)"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="target_smart_contract∈CROSS_CHAIN_SMART_CONTRACTS">
+            <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
+            <org.eventb.core.prIdent name="target_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p6" org.eventb.core.predicate="received_cross_chain_transactions∈CROSS_CHAIN_SMART_CONTRACTS ↔ CROSS_CHAIN_TRANSACTIONS">
+            <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
+            <org.eventb.core.prIdent name="CROSS_CHAIN_TRANSACTIONS" org.eventb.core.type="ℙ(CROSS_CHAIN_TRANSACTIONS)"/>
+            <org.eventb.core.prIdent name="received_cross_chain_transactions" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_TRANSACTIONS)"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
+        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.typeRewrites:1"/>
+    </org.eventb.core.prProof>
+    <org.eventb.core.prProof name="INITIALISATION/inv2;/INV" org.eventb.core.confidence="0" org.eventb.core.prFresh="" org.eventb.core.prHyps="">
+        <org.eventb.core.lang name="L"/>
+        <org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="type rewrites" org.eventb.core.prHyps="">
+            <org.eventb.core.prAnte name="'">
+                <org.eventb.core.prHypAction name="HIDE0" org.eventb.core.prHyps="p0"/>
+                <org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p1"/>
+                <org.eventb.core.prHypAction name="HIDE2" org.eventb.core.prHyps="p2"/>
+            </org.eventb.core.prAnte>
+        </org.eventb.core.prRule>
+        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="gateway∈GATEWAYS">
+            <org.eventb.core.prIdent name="GATEWAYS" org.eventb.core.type="ℙ(GATEWAYS)"/>
+            <org.eventb.core.prIdent name="gateway" org.eventb.core.type="GATEWAYS"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="source_smart_contract∈CROSS_CHAIN_SMART_CONTRACTS">
+            <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
+            <org.eventb.core.prIdent name="source_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="target_smart_contract∈CROSS_CHAIN_SMART_CONTRACTS">
+            <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
+            <org.eventb.core.prIdent name="target_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.typeRewrites:1"/>
+    </org.eventb.core.prProof>
+    <org.eventb.core.prProof name="PROCESS_CROSS_CHAIN_TRANSACTION/inv1;/INV" org.eventb.core.confidence="0" org.eventb.core.prFresh="" org.eventb.core.prHyps="">
         <org.eventb.core.lang name="L"/>
         <org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prHyps="">
             <org.eventb.core.prAnte name="'">
@@ -205,12 +271,11 @@
                         <org.eventb.core.prHypAction name="HIDE3" org.eventb.core.prHyps="p5"/>
                         <org.eventb.core.prHypAction name="HIDE4" org.eventb.core.prHyps="p6"/>
                         <org.eventb.core.prHypAction name="HIDE5" org.eventb.core.prHyps="p7"/>
-                        <org.eventb.core.prHypAction name="HIDE6" org.eventb.core.prHyps="p8"/>
                     </org.eventb.core.prAnte>
                 </org.eventb.core.prRule>
             </org.eventb.core.prAnte>
         </org.eventb.core.prRule>
-        <org.eventb.core.prPred name="p6" org.eventb.core.predicate="subscriptions∈GATEWAYS ↔ CROSS_CHAIN_SMART_CONTRACTS">
+        <org.eventb.core.prPred name="p5" org.eventb.core.predicate="subscriptions∈GATEWAYS ↔ CROSS_CHAIN_SMART_CONTRACTS">
             <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
             <org.eventb.core.prIdent name="GATEWAYS" org.eventb.core.type="ℙ(GATEWAYS)"/>
             <org.eventb.core.prIdent name="subscriptions" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_SMART_CONTRACTS)"/>
@@ -219,11 +284,67 @@
             <org.eventb.core.prIdent name="GATEWAYS" org.eventb.core.type="ℙ(GATEWAYS)"/>
             <org.eventb.core.prIdent name="gateway" org.eventb.core.type="GATEWAYS"/>
         </org.eventb.core.prPred>
-        <org.eventb.core.prPred name="p5" org.eventb.core.predicate="triggered_events∈CROSS_CHAIN_SMART_CONTRACTS ↔ CROSS_CHAIN_EVENTS">
+        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="¬cross_chain_event∈triggered_events[{source_smart_contract}]">
             <org.eventb.core.prIdent name="CROSS_CHAIN_EVENTS" org.eventb.core.type="ℙ(CROSS_CHAIN_EVENTS)"/>
             <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
+            <org.eventb.core.prIdent name="cross_chain_event" org.eventb.core.type="CROSS_CHAIN_EVENTS"/>
+            <org.eventb.core.prIdent name="source_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
             <org.eventb.core.prIdent name="triggered_events" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_EVENTS)"/>
         </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="cross_chain_event∉triggered_events[{source_smart_contract}]">
+            <org.eventb.core.prIdent name="CROSS_CHAIN_EVENTS" org.eventb.core.type="ℙ(CROSS_CHAIN_EVENTS)"/>
+            <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
+            <org.eventb.core.prIdent name="cross_chain_event" org.eventb.core.type="CROSS_CHAIN_EVENTS"/>
+            <org.eventb.core.prIdent name="source_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
+            <org.eventb.core.prIdent name="triggered_events" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_EVENTS)"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="source_smart_contract∈CROSS_CHAIN_SMART_CONTRACTS">
+            <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
+            <org.eventb.core.prIdent name="source_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p6" org.eventb.core.predicate="gateway_pending_transactions∈GATEWAYS ↔ CROSS_CHAIN_TRANSACTIONS">
+            <org.eventb.core.prIdent name="CROSS_CHAIN_TRANSACTIONS" org.eventb.core.type="ℙ(CROSS_CHAIN_TRANSACTIONS)"/>
+            <org.eventb.core.prIdent name="GATEWAYS" org.eventb.core.type="ℙ(GATEWAYS)"/>
+            <org.eventb.core.prIdent name="gateway_pending_transactions" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_TRANSACTIONS)"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="target_smart_contract∈CROSS_CHAIN_SMART_CONTRACTS">
+            <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
+            <org.eventb.core.prIdent name="target_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p7" org.eventb.core.predicate="received_cross_chain_transactions∈CROSS_CHAIN_SMART_CONTRACTS ↔ CROSS_CHAIN_TRANSACTIONS">
+            <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
+            <org.eventb.core.prIdent name="CROSS_CHAIN_TRANSACTIONS" org.eventb.core.type="ℙ(CROSS_CHAIN_TRANSACTIONS)"/>
+            <org.eventb.core.prIdent name="received_cross_chain_transactions" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_TRANSACTIONS)"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
+        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.typeRewrites:1"/>
+    </org.eventb.core.prProof>
+    <org.eventb.core.prProof name="PROCESS_CROSS_CHAIN_TRANSACTION/inv2;/INV" org.eventb.core.confidence="0" org.eventb.core.prFresh="" org.eventb.core.prHyps="">
+        <org.eventb.core.lang name="L"/>
+        <org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prHyps="">
+            <org.eventb.core.prAnte name="'">
+                <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p0" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p1"/>
+                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="type rewrites" org.eventb.core.prHyps="">
+                    <org.eventb.core.prAnte name="'">
+                        <org.eventb.core.prHypAction name="HIDE0" org.eventb.core.prHyps="p2"/>
+                        <org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p3"/>
+                        <org.eventb.core.prHypAction name="HIDE2" org.eventb.core.prHyps="p4"/>
+                        <org.eventb.core.prHypAction name="HIDE3" org.eventb.core.prHyps="p5"/>
+                        <org.eventb.core.prHypAction name="HIDE4" org.eventb.core.prHyps="p6"/>
+                        <org.eventb.core.prHypAction name="HIDE5" org.eventb.core.prHyps="p7"/>
+                    </org.eventb.core.prAnte>
+                </org.eventb.core.prRule>
+            </org.eventb.core.prAnte>
+        </org.eventb.core.prRule>
+        <org.eventb.core.prPred name="p5" org.eventb.core.predicate="subscriptions∈GATEWAYS ↔ CROSS_CHAIN_SMART_CONTRACTS">
+            <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
+            <org.eventb.core.prIdent name="GATEWAYS" org.eventb.core.type="ℙ(GATEWAYS)"/>
+            <org.eventb.core.prIdent name="subscriptions" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_SMART_CONTRACTS)"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p4" org.eventb.core.predicate="gateway∈GATEWAYS">
+            <org.eventb.core.prIdent name="GATEWAYS" org.eventb.core.type="ℙ(GATEWAYS)"/>
+            <org.eventb.core.prIdent name="gateway" org.eventb.core.type="GATEWAYS"/>
+        </org.eventb.core.prPred>
         <org.eventb.core.prPred name="p1" org.eventb.core.predicate="¬cross_chain_event∈triggered_events[{source_smart_contract}]">
             <org.eventb.core.prIdent name="CROSS_CHAIN_EVENTS" org.eventb.core.type="ℙ(CROSS_CHAIN_EVENTS)"/>
             <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
@@ -242,7 +363,68 @@
             <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
             <org.eventb.core.prIdent name="source_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
         </org.eventb.core.prPred>
-        <org.eventb.core.prPred name="p7" org.eventb.core.predicate="gateway_pending_transactions∈GATEWAYS ↔ CROSS_CHAIN_TRANSACTIONS">
+        <org.eventb.core.prPred name="p6" org.eventb.core.predicate="gateway_pending_transactions∈GATEWAYS ↔ CROSS_CHAIN_TRANSACTIONS">
+            <org.eventb.core.prIdent name="CROSS_CHAIN_TRANSACTIONS" org.eventb.core.type="ℙ(CROSS_CHAIN_TRANSACTIONS)"/>
+            <org.eventb.core.prIdent name="GATEWAYS" org.eventb.core.type="ℙ(GATEWAYS)"/>
+            <org.eventb.core.prIdent name="gateway_pending_transactions" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_TRANSACTIONS)"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="target_smart_contract∈CROSS_CHAIN_SMART_CONTRACTS">
+            <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
+            <org.eventb.core.prIdent name="target_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p7" org.eventb.core.predicate="received_cross_chain_transactions∈CROSS_CHAIN_SMART_CONTRACTS ↔ CROSS_CHAIN_TRANSACTIONS">
+            <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
+            <org.eventb.core.prIdent name="CROSS_CHAIN_TRANSACTIONS" org.eventb.core.type="ℙ(CROSS_CHAIN_TRANSACTIONS)"/>
+            <org.eventb.core.prIdent name="received_cross_chain_transactions" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_TRANSACTIONS)"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
+        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.typeRewrites:1"/>
+    </org.eventb.core.prProof>
+    <org.eventb.core.prProof name="LISTEN_SMART_CONTRACT_EVENT/inv2;/INV" org.eventb.core.confidence="0" org.eventb.core.prFresh="" org.eventb.core.prHyps="">
+        <org.eventb.core.lang name="L"/>
+        <org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prHyps="">
+            <org.eventb.core.prAnte name="'">
+                <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p0" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p1"/>
+                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="type rewrites" org.eventb.core.prHyps="">
+                    <org.eventb.core.prAnte name="'">
+                        <org.eventb.core.prHypAction name="HIDE0" org.eventb.core.prHyps="p2"/>
+                        <org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p3"/>
+                        <org.eventb.core.prHypAction name="HIDE2" org.eventb.core.prHyps="p4"/>
+                        <org.eventb.core.prHypAction name="HIDE3" org.eventb.core.prHyps="p5"/>
+                        <org.eventb.core.prHypAction name="HIDE4" org.eventb.core.prHyps="p6"/>
+                        <org.eventb.core.prHypAction name="HIDE5" org.eventb.core.prHyps="p7"/>
+                    </org.eventb.core.prAnte>
+                </org.eventb.core.prRule>
+            </org.eventb.core.prAnte>
+        </org.eventb.core.prRule>
+        <org.eventb.core.prPred name="p5" org.eventb.core.predicate="subscriptions∈GATEWAYS ↔ CROSS_CHAIN_SMART_CONTRACTS">
+            <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
+            <org.eventb.core.prIdent name="GATEWAYS" org.eventb.core.type="ℙ(GATEWAYS)"/>
+            <org.eventb.core.prIdent name="subscriptions" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_SMART_CONTRACTS)"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p4" org.eventb.core.predicate="gateway∈GATEWAYS">
+            <org.eventb.core.prIdent name="GATEWAYS" org.eventb.core.type="ℙ(GATEWAYS)"/>
+            <org.eventb.core.prIdent name="gateway" org.eventb.core.type="GATEWAYS"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="gateway ↦ cross_chain_transaction∉gateway_pending_transactions">
+            <org.eventb.core.prIdent name="CROSS_CHAIN_TRANSACTIONS" org.eventb.core.type="ℙ(CROSS_CHAIN_TRANSACTIONS)"/>
+            <org.eventb.core.prIdent name="GATEWAYS" org.eventb.core.type="ℙ(GATEWAYS)"/>
+            <org.eventb.core.prIdent name="cross_chain_transaction" org.eventb.core.type="CROSS_CHAIN_TRANSACTIONS"/>
+            <org.eventb.core.prIdent name="gateway" org.eventb.core.type="GATEWAYS"/>
+            <org.eventb.core.prIdent name="gateway_pending_transactions" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_TRANSACTIONS)"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="¬gateway ↦ cross_chain_transaction∈gateway_pending_transactions">
+            <org.eventb.core.prIdent name="CROSS_CHAIN_TRANSACTIONS" org.eventb.core.type="ℙ(CROSS_CHAIN_TRANSACTIONS)"/>
+            <org.eventb.core.prIdent name="GATEWAYS" org.eventb.core.type="ℙ(GATEWAYS)"/>
+            <org.eventb.core.prIdent name="cross_chain_transaction" org.eventb.core.type="CROSS_CHAIN_TRANSACTIONS"/>
+            <org.eventb.core.prIdent name="gateway" org.eventb.core.type="GATEWAYS"/>
+            <org.eventb.core.prIdent name="gateway_pending_transactions" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_TRANSACTIONS)"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="source_smart_contract∈CROSS_CHAIN_SMART_CONTRACTS">
+            <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
+            <org.eventb.core.prIdent name="source_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p6" org.eventb.core.predicate="gateway_pending_transactions∈GATEWAYS ↔ CROSS_CHAIN_TRANSACTIONS">
             <org.eventb.core.prIdent name="CROSS_CHAIN_TRANSACTIONS" org.eventb.core.type="ℙ(CROSS_CHAIN_TRANSACTIONS)"/>
             <org.eventb.core.prIdent name="GATEWAYS" org.eventb.core.type="ℙ(GATEWAYS)"/>
             <org.eventb.core.prIdent name="gateway_pending_transactions" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_TRANSACTIONS)"/>
@@ -251,7 +433,7 @@
             <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
             <org.eventb.core.prIdent name="target_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
         </org.eventb.core.prPred>
-        <org.eventb.core.prPred name="p8" org.eventb.core.predicate="received_cross_chain_transactions∈CROSS_CHAIN_SMART_CONTRACTS ↔ CROSS_CHAIN_TRANSACTIONS">
+        <org.eventb.core.prPred name="p7" org.eventb.core.predicate="received_cross_chain_transactions∈CROSS_CHAIN_SMART_CONTRACTS ↔ CROSS_CHAIN_TRANSACTIONS">
             <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
             <org.eventb.core.prIdent name="CROSS_CHAIN_TRANSACTIONS" org.eventb.core.type="ℙ(CROSS_CHAIN_TRANSACTIONS)"/>
             <org.eventb.core.prIdent name="received_cross_chain_transactions" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_TRANSACTIONS)"/>

BIG/BIG_m1.bps

 <?xml version="1.0" encoding="UTF-8" standalone="no"?>
-<org.eventb.core.psFile>
-    <org.eventb.core.psStatus name="INITIALISATION/inv11;/INV" org.eventb.core.confidence="0" org.eventb.core.poStamp="115" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="SUBMIT_CROSS_CHAIN_TRANSACTION/inv11;/INV" org.eventb.core.confidence="0" org.eventb.core.poStamp="115" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="PROCESS_CROSS_CHAIN_TRANSACTION/inv11;/INV" org.eventb.core.confidence="0" org.eventb.core.poStamp="115" org.eventb.core.psManual="false"/>
-</org.eventb.core.psFile>
+<org.eventb.core.psFile/>

BIG/BIG_m1.bum

 <?xml version="1.0" encoding="UTF-8" standalone="no"?>
-<org.eventb.core.machineFile org.eventb.core.configuration="org.eventb.core.fwd" org.eventb.core.generated="false" org.eventb.emf.persistence.emf_id="_oyeJzKviEe6I4bA9GxwhqQ" org.eventb.texttools.text_lastmodified="1704470038332" org.eventb.texttools.text_representation="machine BIG_m1 sees BIG_c1&#10;&#10;variables received_transactions triggered_events subscriptions gateway_pending_transactions received_cross_chain_transactions&#10;&#10;invariants&#10;&#9;@inv1: received_transactions ∈ CROSS_CHAIN_SMART_CONTRACTS ↠ TRANSACTIONS // Every transaction is submitted to a smart contract&#10;&#9;@inv2: triggered_events ∈ CROSS_CHAIN_SMART_CONTRACTS ↠ CROSS_CHAIN_EVENTS // Every event is triggered by a smart contract&#10;&#9;@inv3: subscriptions ∈ GATEWAYS ↔ CROSS_CHAIN_SMART_CONTRACTS&#10;&#9;@inv4: gateway_pending_transactions ∈ GATEWAYS ↔ CROSS_CHAIN_TRANSACTIONS&#10;&#9;@inv6: received_cross_chain_transactions ∈ CROSS_CHAIN_SMART_CONTRACTS ↔ CROSS_CHAIN_TRANSACTIONS&#10;&#10;events&#10;  event INITIALISATION&#10;  &#9;then&#10;  &#9;&#9;@act1: received_transactions ≔ ∅&#10;   &#9;&#9;@act2: triggered_events ≔ ∅&#10;   &#9;&#9;@act3: subscriptions ≔ ∅&#10;   &#9;&#9;@act4: gateway_pending_transactions ≔ ∅&#10;   &#9;&#9;@act6: received_cross_chain_transactions ≔ ∅&#10;  end&#10;&#10;  event SUBSCRIBE_SMART_CONTRACT_EVENTS&#10;  &#9;where&#10;  &#9;&#9;@grd1: gateway ↦ source_smart_contract ∉ subscriptions // The gateway is not already subscribed to the smart contract events&#10;  &#9;then&#10;&#9;&#9;@act1: subscriptions ≔ subscriptions  ∪ {gateway ↦ source_smart_contract} // The gateway is subscribed to listen to the smart contract events&#10;  end&#10;&#10;  event SUBMIT_CROSS_CHAIN_TRANSACTION&#10;&#9;any transaction&#10;&#9;where&#10;&#9;&#9;@grd1: transaction ∈ TRANSACTIONS&#10;&#9;&#9;@grd3: transaction ∉ received_transactions[{source_smart_contract}]&#10;&#9;then&#10;&#9;&#9;@act1: received_transactions ≔ received_transactions ∪ {source_smart_contract ↦ transaction}&#10;  end&#10;&#10;  event PROCESS_CROSS_CHAIN_TRANSACTION&#10;  &#9;any transaction cross_chain_event&#10;  &#9;where&#10;  &#9;&#9;@grd1: source_smart_contract ↦ transaction ∈ received_transactions // The smart contract has a pending transaction to process&#10;  &#9;&#9;@grd2: cross_chain_event ∉ triggered_events[{source_smart_contract}] // The smart contract will allways trigger a new event&#10;  &#9;then&#10;  &#9;&#9;@act1: triggered_events ≔  triggered_events ∪ {source_smart_contract ↦ cross_chain_event} // The smart contract triggers a new event related to the transaction processing&#10;  &#9;&#9;@act2: received_transactions ≔ received_transactions ∖ {source_smart_contract ↦ transaction} // The smart contract processed the transaction&#10;  end&#10;&#10;  event LISTEN_SMART_CONTRACT_EVENT&#10;  &#9;any cross_chain_event cross_chain_transaction&#10;  &#9;where&#10;  &#9;&#9;@grd1: source_smart_contract ↦ cross_chain_event ∈ triggered_events // The smart contract has triggered an event&#10;  &#9;&#9;@grd2: gateway ↦ source_smart_contract ∈ subscriptions // Exist a subscription to the smart contract events&#10;  &#9;&#9;@grd3: gateway ↦ cross_chain_transaction ∉ gateway_pending_transactions // The event was not already listened&#10;  &#9;then&#10;&#9;&#9;@act1: gateway_pending_transactions ≔ gateway_pending_transactions ∪ {gateway ↦ cross_chain_transaction} // The event is added to the cross-chain transactions to be processed by the gateway&#10;  &#9;&#9;@act2: triggered_events ≔ triggered_events ∖ {source_smart_contract ↦ cross_chain_event} // The event is listened and processed&#10;  end&#10;&#10;  event GATEWAY_PROCESS_CROSS_CHAIN_TRANSACTION&#10;  &#9;any cross_chain_transaction&#10;  &#9;when&#10;  &#9;&#9;@grd1: gateway ↦ cross_chain_transaction ∈ gateway_pending_transactions // There is one pending cross-chain transaction to process&#10;  &#9;then&#10;  &#9;&#9;@act1: received_cross_chain_transactions ≔ received_cross_chain_transactions ∪ {target_smart_contract ↦ cross_chain_transaction}&#10;  &#9;&#9;@act2: gateway_pending_transactions ≔  gateway_pending_transactions ∖ {gateway ↦ cross_chain_transaction}&#10;  end&#10;&#10;end&#10;" version="5">
+<org.eventb.core.machineFile org.eventb.core.configuration="org.eventb.core.fwd" org.eventb.core.generated="false" org.eventb.emf.persistence.emf_id="_559ZqKvjEe6I4bA9GxwhqQ" org.eventb.texttools.text_lastmodified="1704470582699" org.eventb.texttools.text_representation="machine BIG_m1 sees BIG_c1&#10;&#10;variables received_transactions triggered_events subscriptions gateway_pending_transactions received_cross_chain_transactions&#10;&#10;invariants&#10;&#9;@inv1: received_transactions ∈ CROSS_CHAIN_SMART_CONTRACTS ↔ TRANSACTIONS&#10;&#9;@inv2: triggered_events ∈ CROSS_CHAIN_SMART_CONTRACTS ↔ CROSS_CHAIN_EVENTS&#10;&#9;@inv3: subscriptions ∈ GATEWAYS ↔ CROSS_CHAIN_SMART_CONTRACTS&#10;&#9;@inv4: gateway_pending_transactions ∈ GATEWAYS ↔ CROSS_CHAIN_TRANSACTIONS&#10;&#9;@inv6: received_cross_chain_transactions ∈ CROSS_CHAIN_SMART_CONTRACTS ↔ CROSS_CHAIN_TRANSACTIONS&#10;&#10;events&#10;  event INITIALISATION&#10;  &#9;then&#10;  &#9;&#9;@act1: received_transactions ≔ ∅&#10;   &#9;&#9;@act2: triggered_events ≔ ∅&#10;   &#9;&#9;@act3: subscriptions ≔ ∅&#10;   &#9;&#9;@act4: gateway_pending_transactions ≔ ∅&#10;   &#9;&#9;@act6: received_cross_chain_transactions ≔ ∅&#10;  end&#10;&#10;  event SUBSCRIBE_SMART_CONTRACT_EVENTS&#10;  &#9;where&#10;  &#9;&#9;@grd1: gateway ↦ source_smart_contract ∉ subscriptions // The gateway is not already subscribed to the smart contract events&#10;  &#9;then&#10;&#9;&#9;@act1: subscriptions ≔ subscriptions  ∪ {gateway ↦ source_smart_contract} // The gateway is subscribed to listen to the smart contract events&#10;  end&#10;&#10;  event SUBMIT_CROSS_CHAIN_TRANSACTION&#10;&#9;any transaction&#10;&#9;where&#10;&#9;&#9;@grd1: transaction ∈ TRANSACTIONS&#10;&#9;&#9;@grd3: transaction ∉ received_transactions[{source_smart_contract}]&#10;&#9;then&#10;&#9;&#9;@act1: received_transactions ≔ received_transactions ∪ {source_smart_contract ↦ transaction}&#10;  end&#10;&#10;  event PROCESS_CROSS_CHAIN_TRANSACTION&#10;  &#9;any transaction cross_chain_event&#10;  &#9;where&#10;  &#9;&#9;@grd1: source_smart_contract ↦ transaction ∈ received_transactions // The smart contract has a pending transaction to process&#10;  &#9;&#9;@grd2: cross_chain_event ∉ triggered_events[{source_smart_contract}] // The smart contract will allways trigger a new event&#10;  &#9;then&#10;  &#9;&#9;@act1: triggered_events ≔  triggered_events ∪ {source_smart_contract ↦ cross_chain_event} // The smart contract triggers a new event related to the transaction processing&#10;  &#9;&#9;@act2: received_transactions ≔ received_transactions ∖ {source_smart_contract ↦ transaction} // The smart contract processed the transaction&#10;  end&#10;&#10;  event LISTEN_SMART_CONTRACT_EVENT&#10;  &#9;any cross_chain_event cross_chain_transaction&#10;  &#9;where&#10;  &#9;&#9;@grd1: source_smart_contract ↦ cross_chain_event ∈ triggered_events // The smart contract has triggered an event&#10;  &#9;&#9;@grd2: gateway ↦ source_smart_contract ∈ subscriptions // Exist a subscription to the smart contract events&#10;  &#9;&#9;@grd3: gateway ↦ cross_chain_transaction ∉ gateway_pending_transactions // The event was not already listened&#10;  &#9;then&#10;&#9;&#9;@act1: gateway_pending_transactions ≔ gateway_pending_transactions ∪ {gateway ↦ cross_chain_transaction} // The event is added to the cross-chain transactions to be processed by the gateway&#10;  &#9;&#9;@act2: triggered_events ≔ triggered_events ∖ {source_smart_contract ↦ cross_chain_event} // The event is listened and processed&#10;  end&#10;&#10;  event GATEWAY_PROCESS_CROSS_CHAIN_TRANSACTION&#10;  &#9;any cross_chain_transaction&#10;  &#9;when&#10;  &#9;&#9;@grd1: gateway ↦ cross_chain_transaction ∈ gateway_pending_transactions // There is one pending cross-chain transaction to process&#10;  &#9;then&#10;  &#9;&#9;@act1: received_cross_chain_transactions ≔ received_cross_chain_transactions ∪ {target_smart_contract ↦ cross_chain_transaction}&#10;  &#9;&#9;@act2: gateway_pending_transactions ≔  gateway_pending_transactions ∖ {gateway ↦ cross_chain_transaction}&#10;  end&#10;&#10;end&#10;" version="5">
     <org.eventb.core.seesContext name="_sUpukKl_Ee6I4bA9GxwhqQ" org.eventb.core.target="BIG_c1"/>
-    <org.eventb.core.event name="'" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="INITIALISATION" org.eventb.emf.persistence.emf_id="_oyeJr6viEe6I4bA9GxwhqQ">
-        <org.eventb.core.action name="_SAxOQKmDEe6I4bA9GxwhqQ" org.eventb.core.assignment="received_transactions ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act1;" org.eventb.emf.persistence.emf_id="_oyeJqqviEe6I4bA9GxwhqQ"/>
-        <org.eventb.core.action name="_TlWCkamHEe6I4bA9GxwhqQ" org.eventb.core.assignment="triggered_events ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act2;" org.eventb.emf.persistence.emf_id="_oyeJq6viEe6I4bA9GxwhqQ"/>
-        <org.eventb.core.action name="_mv5M0KpAEe6I4bA9GxwhqQ" org.eventb.core.assignment="subscriptions ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act3;" org.eventb.emf.persistence.emf_id="_oyeJrKviEe6I4bA9GxwhqQ"/>
-        <org.eventb.core.action name="_8Ty9sKpBEe6I4bA9GxwhqQ" org.eventb.core.assignment="gateway_pending_transactions ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act4;" org.eventb.emf.persistence.emf_id="_oyeJraviEe6I4bA9GxwhqQ"/>
-        <org.eventb.core.action name="_J6KjYKpbEe6I4bA9GxwhqQ" org.eventb.core.assignment="received_cross_chain_transactions ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act6;" org.eventb.emf.persistence.emf_id="_oyeJrqviEe6I4bA9GxwhqQ"/>
+    <org.eventb.core.event name="'" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="INITIALISATION" org.eventb.emf.persistence.emf_id="_558yj6vjEe6I4bA9GxwhqQ">
+        <org.eventb.core.action name="_SAxOQKmDEe6I4bA9GxwhqQ" org.eventb.core.assignment="received_transactions ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act1;" org.eventb.emf.persistence.emf_id="_558yiqvjEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.action name="_TlWCkamHEe6I4bA9GxwhqQ" org.eventb.core.assignment="triggered_events ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act2;" org.eventb.emf.persistence.emf_id="_558yi6vjEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.action name="_mv5M0KpAEe6I4bA9GxwhqQ" org.eventb.core.assignment="subscriptions ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act3;" org.eventb.emf.persistence.emf_id="_558yjKvjEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.action name="_8Ty9sKpBEe6I4bA9GxwhqQ" org.eventb.core.assignment="gateway_pending_transactions ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act4;" org.eventb.emf.persistence.emf_id="_558yjavjEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.action name="_J6KjYKpbEe6I4bA9GxwhqQ" org.eventb.core.assignment="received_cross_chain_transactions ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act6;" org.eventb.emf.persistence.emf_id="_558yjqvjEe6I4bA9GxwhqQ"/>
     </org.eventb.core.event>
-    <org.eventb.core.event name="_I9G5gKpAEe6I4bA9GxwhqQ" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="SUBSCRIBE_SMART_CONTRACT_EVENTS" org.eventb.emf.persistence.emf_id="_oyeJsqviEe6I4bA9GxwhqQ">
-        <org.eventb.core.action name="_a_IQYKmDEe6I4bA9GxwhqQ" org.eventb.core.assignment="subscriptions ≔ subscriptions  ∪ {gateway ↦ source_smart_contract}" org.eventb.core.comment="The gateway is subscribed to listen to the smart contract events" org.eventb.core.generated="false" org.eventb.core.label="act1;" org.eventb.emf.persistence.emf_id="_oyeJsaviEe6I4bA9GxwhqQ"/>
-        <org.eventb.core.guard name="_SAx1UKmDEe6I4bA9GxwhqQ" org.eventb.core.comment="The gateway is not already subscribed to the smart contract events" org.eventb.core.generated="false" org.eventb.core.label="grd1;" org.eventb.core.predicate="gateway ↦ source_smart_contract ∉ subscriptions" org.eventb.emf.persistence.emf_id="_oyeJsKviEe6I4bA9GxwhqQ"/>
+    <org.eventb.core.event name="_I9G5gKpAEe6I4bA9GxwhqQ" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="SUBSCRIBE_SMART_CONTRACT_EVENTS" org.eventb.emf.persistence.emf_id="_558ykqvjEe6I4bA9GxwhqQ">
+        <org.eventb.core.action name="_a_IQYKmDEe6I4bA9GxwhqQ" org.eventb.core.assignment="subscriptions ≔ subscriptions  ∪ {gateway ↦ source_smart_contract}" org.eventb.core.comment="The gateway is subscribed to listen to the smart contract events" org.eventb.core.generated="false" org.eventb.core.label="act1;" org.eventb.emf.persistence.emf_id="_558ykavjEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.guard name="_SAx1UKmDEe6I4bA9GxwhqQ" org.eventb.core.comment="The gateway is not already subscribed to the smart contract events" org.eventb.core.generated="false" org.eventb.core.label="grd1;" org.eventb.core.predicate="gateway ↦ source_smart_contract ∉ subscriptions" org.eventb.emf.persistence.emf_id="_558ykKvjEe6I4bA9GxwhqQ"/>
     </org.eventb.core.event>
-    <org.eventb.core.event name="_58YTEKmAEe6I4bA9GxwhqQ" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="SUBMIT_CROSS_CHAIN_TRANSACTION" org.eventb.emf.persistence.emf_id="_oyeJt6viEe6I4bA9GxwhqQ">
-        <org.eventb.core.action name="_AeyzAKmIEe6I4bA9GxwhqQ" org.eventb.core.assignment="received_transactions ≔ received_transactions ∪ {source_smart_contract ↦ transaction}" org.eventb.core.generated="false" org.eventb.core.label="act1;" org.eventb.emf.persistence.emf_id="_oyeJtqviEe6I4bA9GxwhqQ"/>
-        <org.eventb.core.guard name="_TlWCkqmHEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.label="grd1;" org.eventb.core.predicate="transaction ∈ TRANSACTIONS" org.eventb.emf.persistence.emf_id="_oyeJtKviEe6I4bA9GxwhqQ"/>
-        <org.eventb.core.guard name="_HCtL8KmIEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.label="grd3;" org.eventb.core.predicate="transaction ∉ received_transactions[{source_smart_contract}]" org.eventb.emf.persistence.emf_id="_oyeJtaviEe6I4bA9GxwhqQ"/>
-        <org.eventb.core.parameter name="_SAx1UqmDEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="transaction" org.eventb.emf.persistence.emf_id="_oyeJs6viEe6I4bA9GxwhqQ"/>
+    <org.eventb.core.event name="_58YTEKmAEe6I4bA9GxwhqQ" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="SUBMIT_CROSS_CHAIN_TRANSACTION" org.eventb.emf.persistence.emf_id="_559Zk6vjEe6I4bA9GxwhqQ">
+        <org.eventb.core.action name="_AeyzAKmIEe6I4bA9GxwhqQ" org.eventb.core.assignment="received_transactions ≔ received_transactions ∪ {source_smart_contract ↦ transaction}" org.eventb.core.generated="false" org.eventb.core.label="act1;" org.eventb.emf.persistence.emf_id="_559ZkqvjEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.guard name="_TlWCkqmHEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.label="grd1;" org.eventb.core.predicate="transaction ∈ TRANSACTIONS" org.eventb.emf.persistence.emf_id="_559ZkKvjEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.guard name="_HCtL8KmIEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.label="grd3;" org.eventb.core.predicate="transaction ∉ received_transactions[{source_smart_contract}]" org.eventb.emf.persistence.emf_id="_559ZkavjEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.parameter name="_SAx1UqmDEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="transaction" org.eventb.emf.persistence.emf_id="_558yk6vjEe6I4bA9GxwhqQ"/>
     </org.eventb.core.event>
-    <org.eventb.core.event name="_TlWCkKmHEe6I4bA9GxwhqQ" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="PROCESS_CROSS_CHAIN_TRANSACTION" org.eventb.emf.persistence.emf_id="_oyeJvqviEe6I4bA9GxwhqQ">
-        <org.eventb.core.action name="_I9G5gapAEe6I4bA9GxwhqQ" org.eventb.core.assignment="triggered_events ≔  triggered_events ∪ {source_smart_contract ↦ cross_chain_event}" org.eventb.core.comment="The smart contract triggers a new event related to the transaction processing" org.eventb.core.generated="false" org.eventb.core.label="act1;" org.eventb.emf.persistence.emf_id="_oyeJvKviEe6I4bA9GxwhqQ"/>
-        <org.eventb.core.action name="_gaDEIKmHEe6I4bA9GxwhqQ" org.eventb.core.assignment="received_transactions ≔ received_transactions ∖ {source_smart_contract ↦ transaction}" org.eventb.core.comment="The smart contract processed the transaction" org.eventb.core.generated="false" org.eventb.core.label="act2;" org.eventb.emf.persistence.emf_id="_oyeJvaviEe6I4bA9GxwhqQ"/>
-        <org.eventb.core.guard name="_iUmtQKpAEe6I4bA9GxwhqQ" org.eventb.core.comment="The smart contract has a pending transaction to process" org.eventb.core.generated="false" org.eventb.core.label="grd1;" org.eventb.core.predicate="source_smart_contract ↦ transaction ∈ received_transactions" org.eventb.emf.persistence.emf_id="_oyeJuqviEe6I4bA9GxwhqQ"/>
-        <org.eventb.core.guard name="_1SOwwKmDEe6I4bA9GxwhqQ" org.eventb.core.comment="The smart contract will allways trigger a new event" org.eventb.core.generated="false" org.eventb.core.label="grd2;" org.eventb.core.predicate="cross_chain_event ∉ triggered_events[{source_smart_contract}]" org.eventb.emf.persistence.emf_id="_oyeJu6viEe6I4bA9GxwhqQ"/>
-        <org.eventb.core.parameter name="_TlWCk6mHEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="transaction" org.eventb.emf.persistence.emf_id="_oyeJuKviEe6I4bA9GxwhqQ"/>
-        <org.eventb.core.parameter name="_AezaEamIEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="cross_chain_event" org.eventb.emf.persistence.emf_id="_oyeJuaviEe6I4bA9GxwhqQ"/>
+    <org.eventb.core.event name="_TlWCkKmHEe6I4bA9GxwhqQ" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="PROCESS_CROSS_CHAIN_TRANSACTION" org.eventb.emf.persistence.emf_id="_559ZmqvjEe6I4bA9GxwhqQ">
+        <org.eventb.core.action name="_I9G5gapAEe6I4bA9GxwhqQ" org.eventb.core.assignment="triggered_events ≔  triggered_events ∪ {source_smart_contract ↦ cross_chain_event}" org.eventb.core.comment="The smart contract triggers a new event related to the transaction processing" org.eventb.core.generated="false" org.eventb.core.label="act1;" org.eventb.emf.persistence.emf_id="_559ZmKvjEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.action name="_gaDEIKmHEe6I4bA9GxwhqQ" org.eventb.core.assignment="received_transactions ≔ received_transactions ∖ {source_smart_contract ↦ transaction}" org.eventb.core.comment="The smart contract processed the transaction" org.eventb.core.generated="false" org.eventb.core.label="act2;" org.eventb.emf.persistence.emf_id="_559ZmavjEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.guard name="_iUmtQKpAEe6I4bA9GxwhqQ" org.eventb.core.comment="The smart contract has a pending transaction to process" org.eventb.core.generated="false" org.eventb.core.label="grd1;" org.eventb.core.predicate="source_smart_contract ↦ transaction ∈ received_transactions" org.eventb.emf.persistence.emf_id="_559ZlqvjEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.guard name="_1SOwwKmDEe6I4bA9GxwhqQ" org.eventb.core.comment="The smart contract will allways trigger a new event" org.eventb.core.generated="false" org.eventb.core.label="grd2;" org.eventb.core.predicate="cross_chain_event ∉ triggered_events[{source_smart_contract}]" org.eventb.emf.persistence.emf_id="_559Zl6vjEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.parameter name="_TlWCk6mHEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="transaction" org.eventb.emf.persistence.emf_id="_559ZlKvjEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.parameter name="_AezaEamIEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="cross_chain_event" org.eventb.emf.persistence.emf_id="_559ZlavjEe6I4bA9GxwhqQ"/>
     </org.eventb.core.event>
-    <org.eventb.core.event name="_8VKFEKpAEe6I4bA9GxwhqQ" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="LISTEN_SMART_CONTRACT_EVENT" org.eventb.emf.persistence.emf_id="_oyeJxqviEe6I4bA9GxwhqQ">
-        <org.eventb.core.action name="_8T0y4KpBEe6I4bA9GxwhqQ" org.eventb.core.assignment="gateway_pending_transactions ≔ gateway_pending_transactions ∪ {gateway ↦ cross_chain_transaction}" org.eventb.core.comment="The event is added to the cross-chain transactions to be processed by the gateway" org.eventb.core.generated="false" org.eventb.core.label="act1;" org.eventb.emf.persistence.emf_id="_oyeJxKviEe6I4bA9GxwhqQ"/>
-        <org.eventb.core.action name="_NAy78KpBEe6I4bA9GxwhqQ" org.eventb.core.assignment="triggered_events ≔ triggered_events ∖ {source_smart_contract ↦ cross_chain_event}" org.eventb.core.comment="The event is listened and processed" org.eventb.core.generated="false" org.eventb.core.label="act2;" org.eventb.emf.persistence.emf_id="_oyeJxaviEe6I4bA9GxwhqQ"/>
-        <org.eventb.core.guard name="_DMOGsKpFEe6I4bA9GxwhqQ" org.eventb.core.comment="The smart contract has triggered an event" org.eventb.core.generated="false" org.eventb.core.label="grd1;" org.eventb.core.predicate="source_smart_contract ↦ cross_chain_event ∈ triggered_events" org.eventb.emf.persistence.emf_id="_oyeJwaviEe6I4bA9GxwhqQ"/>
-        <org.eventb.core.guard name="_AezaEKmIEe6I4bA9GxwhqQ" org.eventb.core.comment="Exist a subscription to the smart contract events" org.eventb.core.generated="false" org.eventb.core.label="grd2;" org.eventb.core.predicate="gateway ↦ source_smart_contract ∈ subscriptions" org.eventb.emf.persistence.emf_id="_oyeJwqviEe6I4bA9GxwhqQ"/>
-        <org.eventb.core.guard name="_x51DwKpCEe6I4bA9GxwhqQ" org.eventb.core.comment="The event was not already listened" org.eventb.core.generated="false" org.eventb.core.label="grd3;" org.eventb.core.predicate="gateway ↦ cross_chain_transaction ∉ gateway_pending_transactions" org.eventb.emf.persistence.emf_id="_oyeJw6viEe6I4bA9GxwhqQ"/>
-        <org.eventb.core.parameter name="_8VKsIqpAEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="cross_chain_event" org.eventb.emf.persistence.emf_id="_oyeJv6viEe6I4bA9GxwhqQ"/>
-        <org.eventb.core.parameter name="_8T1Z8qpBEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="cross_chain_transaction" org.eventb.emf.persistence.emf_id="_oyeJwKviEe6I4bA9GxwhqQ"/>
+    <org.eventb.core.event name="_8VKFEKpAEe6I4bA9GxwhqQ" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="LISTEN_SMART_CONTRACT_EVENT" org.eventb.emf.persistence.emf_id="_559ZoqvjEe6I4bA9GxwhqQ">
+        <org.eventb.core.action name="_8T0y4KpBEe6I4bA9GxwhqQ" org.eventb.core.assignment="gateway_pending_transactions ≔ gateway_pending_transactions ∪ {gateway ↦ cross_chain_transaction}" org.eventb.core.comment="The event is added to the cross-chain transactions to be processed by the gateway" org.eventb.core.generated="false" org.eventb.core.label="act1;" org.eventb.emf.persistence.emf_id="_559ZoKvjEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.action name="_NAy78KpBEe6I4bA9GxwhqQ" org.eventb.core.assignment="triggered_events ≔ triggered_events ∖ {source_smart_contract ↦ cross_chain_event}" org.eventb.core.comment="The event is listened and processed" org.eventb.core.generated="false" org.eventb.core.label="act2;" org.eventb.emf.persistence.emf_id="_559ZoavjEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.guard name="_DMOGsKpFEe6I4bA9GxwhqQ" org.eventb.core.comment="The smart contract has triggered an event" org.eventb.core.generated="false" org.eventb.core.label="grd1;" org.eventb.core.predicate="source_smart_contract ↦ cross_chain_event ∈ triggered_events" org.eventb.emf.persistence.emf_id="_559ZnavjEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.guard name="_AezaEKmIEe6I4bA9GxwhqQ" org.eventb.core.comment="Exist a subscription to the smart contract events" org.eventb.core.generated="false" org.eventb.core.label="grd2;" org.eventb.core.predicate="gateway ↦ source_smart_contract ∈ subscriptions" org.eventb.emf.persistence.emf_id="_559ZnqvjEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.guard name="_x51DwKpCEe6I4bA9GxwhqQ" org.eventb.core.comment="The event was not already listened" org.eventb.core.generated="false" org.eventb.core.label="grd3;" org.eventb.core.predicate="gateway ↦ cross_chain_transaction ∉ gateway_pending_transactions" org.eventb.emf.persistence.emf_id="_559Zn6vjEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.parameter name="_8VKsIqpAEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="cross_chain_event" org.eventb.emf.persistence.emf_id="_559Zm6vjEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.parameter name="_8T1Z8qpBEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="cross_chain_transaction" org.eventb.emf.persistence.emf_id="_559ZnKvjEe6I4bA9GxwhqQ"/>
     </org.eventb.core.event>
-    <org.eventb.core.event name="_0sEN8KpaEe6I4bA9GxwhqQ" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="GATEWAY_PROCESS_CROSS_CHAIN_TRANSACTION" org.eventb.emf.persistence.emf_id="_oyeJy6viEe6I4bA9GxwhqQ">
-        <org.eventb.core.action name="_G1dcQKpbEe6I4bA9GxwhqQ" org.eventb.core.assignment="received_cross_chain_transactions ≔ received_cross_chain_transactions ∪ {target_smart_contract ↦ cross_chain_transaction}" org.eventb.core.generated="false" org.eventb.core.label="act1;" org.eventb.emf.persistence.emf_id="_oyeJyaviEe6I4bA9GxwhqQ"/>
-        <org.eventb.core.action name="_G1dcQapbEe6I4bA9GxwhqQ" org.eventb.core.assignment="gateway_pending_transactions ≔  gateway_pending_transactions ∖ {gateway ↦ cross_chain_transaction}" org.eventb.core.generated="false" org.eventb.core.label="act2;" org.eventb.emf.persistence.emf_id="_oyeJyqviEe6I4bA9GxwhqQ"/>
-        <org.eventb.core.guard name="_tUzFcKpaEe6I4bA9GxwhqQ" org.eventb.core.comment="There is one pending cross-chain transaction to process" org.eventb.core.generated="false" org.eventb.core.label="grd1;" org.eventb.core.predicate="gateway ↦ cross_chain_transaction ∈ gateway_pending_transactions" org.eventb.emf.persistence.emf_id="_oyeJyKviEe6I4bA9GxwhqQ"/>
-        <org.eventb.core.parameter name="_tUzFcapaEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="cross_chain_transaction" org.eventb.emf.persistence.emf_id="_oyeJx6viEe6I4bA9GxwhqQ"/>
+    <org.eventb.core.event name="_0sEN8KpaEe6I4bA9GxwhqQ" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="GATEWAY_PROCESS_CROSS_CHAIN_TRANSACTION" org.eventb.emf.persistence.emf_id="_559Zp6vjEe6I4bA9GxwhqQ">
+        <org.eventb.core.action name="_G1dcQKpbEe6I4bA9GxwhqQ" org.eventb.core.assignment="received_cross_chain_transactions ≔ received_cross_chain_transactions ∪ {target_smart_contract ↦ cross_chain_transaction}" org.eventb.core.generated="false" org.eventb.core.label="act1;" org.eventb.emf.persistence.emf_id="_559ZpavjEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.action name="_G1dcQapbEe6I4bA9GxwhqQ" org.eventb.core.assignment="gateway_pending_transactions ≔  gateway_pending_transactions ∖ {gateway ↦ cross_chain_transaction}" org.eventb.core.generated="false" org.eventb.core.label="act2;" org.eventb.emf.persistence.emf_id="_559ZpqvjEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.guard name="_tUzFcKpaEe6I4bA9GxwhqQ" org.eventb.core.comment="There is one pending cross-chain transaction to process" org.eventb.core.generated="false" org.eventb.core.label="grd1;" org.eventb.core.predicate="gateway ↦ cross_chain_transaction ∈ gateway_pending_transactions" org.eventb.emf.persistence.emf_id="_559ZpKvjEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.parameter name="_tUzFcapaEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="cross_chain_transaction" org.eventb.emf.persistence.emf_id="_559Zo6vjEe6I4bA9GxwhqQ"/>
     </org.eventb.core.event>
-    <org.eventb.core.invariant name="_o6juoKviEe6I4bA9GxwhqQ" org.eventb.core.comment="Every transaction is submitted to a smart contract" org.eventb.core.generated="false" org.eventb.core.label="inv1;" org.eventb.core.predicate="received_transactions ∈ CROSS_CHAIN_SMART_CONTRACTS ↠ TRANSACTIONS" org.eventb.emf.persistence.emf_id="_oyeJpaviEe6I4bA9GxwhqQ"/>
-    <org.eventb.core.invariant name="_d6dcQKmHEe6I4bA9GxwhqQ" org.eventb.core.comment="Every event is triggered by a smart contract" org.eventb.core.generated="false" org.eventb.core.label="inv2;" org.eventb.core.predicate="triggered_events ∈ CROSS_CHAIN_SMART_CONTRACTS ↠ CROSS_CHAIN_EVENTS" org.eventb.emf.persistence.emf_id="_oyeJpqviEe6I4bA9GxwhqQ"/>
-    <org.eventb.core.invariant name="_Q6dKkKpAEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.label="inv3;" org.eventb.core.predicate="subscriptions ∈ GATEWAYS ↔ CROSS_CHAIN_SMART_CONTRACTS" org.eventb.emf.persistence.emf_id="_oyeJp6viEe6I4bA9GxwhqQ"/>
-    <org.eventb.core.invariant name="_c7TQ0KpBEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.label="inv4;" org.eventb.core.predicate="gateway_pending_transactions ∈ GATEWAYS ↔ CROSS_CHAIN_TRANSACTIONS" org.eventb.emf.persistence.emf_id="_oyeJqKviEe6I4bA9GxwhqQ"/>
-    <org.eventb.core.invariant name="_G1eDUKpbEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.label="inv6;" org.eventb.core.predicate="received_cross_chain_transactions ∈ CROSS_CHAIN_SMART_CONTRACTS ↔ CROSS_CHAIN_TRANSACTIONS" org.eventb.emf.persistence.emf_id="_oyeJqaviEe6I4bA9GxwhqQ"/>
-    <org.eventb.core.variable name="_SAycYamDEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="received_transactions" org.eventb.emf.persistence.emf_id="_oyeJoKviEe6I4bA9GxwhqQ"/>
-    <org.eventb.core.variable name="_YvZFkamHEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="triggered_events" org.eventb.emf.persistence.emf_id="_oyeJoaviEe6I4bA9GxwhqQ"/>
-    <org.eventb.core.variable name="_I9HgkapAEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="subscriptions" org.eventb.emf.persistence.emf_id="_oyeJoqviEe6I4bA9GxwhqQ"/>
-    <org.eventb.core.variable name="_8T2BAKpBEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="gateway_pending_transactions" org.eventb.emf.persistence.emf_id="_oyeJo6viEe6I4bA9GxwhqQ"/>
-    <org.eventb.core.variable name="_H2zkgKpbEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="received_cross_chain_transactions" org.eventb.emf.persistence.emf_id="_oyeJpKviEe6I4bA9GxwhqQ"/>
+    <org.eventb.core.invariant name="_o6juoKviEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.label="inv1;" org.eventb.core.predicate="received_transactions ∈ CROSS_CHAIN_SMART_CONTRACTS ↔ TRANSACTIONS" org.eventb.emf.persistence.emf_id="_558yhavjEe6I4bA9GxwhqQ"/>
+    <org.eventb.core.invariant name="_d6dcQKmHEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.label="inv2;" org.eventb.core.predicate="triggered_events ∈ CROSS_CHAIN_SMART_CONTRACTS ↔ CROSS_CHAIN_EVENTS" org.eventb.emf.persistence.emf_id="_558yhqvjEe6I4bA9GxwhqQ"/>
+    <org.eventb.core.invariant name="_Q6dKkKpAEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.label="inv3;" org.eventb.core.predicate="subscriptions ∈ GATEWAYS ↔ CROSS_CHAIN_SMART_CONTRACTS" org.eventb.emf.persistence.emf_id="_558yh6vjEe6I4bA9GxwhqQ"/>
+    <org.eventb.core.invariant name="_c7TQ0KpBEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.label="inv4;" org.eventb.core.predicate="gateway_pending_transactions ∈ GATEWAYS ↔ CROSS_CHAIN_TRANSACTIONS" org.eventb.emf.persistence.emf_id="_558yiKvjEe6I4bA9GxwhqQ"/>
+    <org.eventb.core.invariant name="_G1eDUKpbEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.label="inv6;" org.eventb.core.predicate="received_cross_chain_transactions ∈ CROSS_CHAIN_SMART_CONTRACTS ↔ CROSS_CHAIN_TRANSACTIONS" org.eventb.emf.persistence.emf_id="_558yiavjEe6I4bA9GxwhqQ"/>
+    <org.eventb.core.variable name="_SAycYamDEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="received_transactions" org.eventb.emf.persistence.emf_id="_558ygKvjEe6I4bA9GxwhqQ"/>
+    <org.eventb.core.variable name="_YvZFkamHEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="triggered_events" org.eventb.emf.persistence.emf_id="_558ygavjEe6I4bA9GxwhqQ"/>
+    <org.eventb.core.variable name="_I9HgkapAEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="subscriptions" org.eventb.emf.persistence.emf_id="_558ygqvjEe6I4bA9GxwhqQ"/>
+    <org.eventb.core.variable name="_8T2BAKpBEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="gateway_pending_transactions" org.eventb.emf.persistence.emf_id="_558yg6vjEe6I4bA9GxwhqQ"/>
+    <org.eventb.core.variable name="_H2zkgKpbEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="received_cross_chain_transactions" org.eventb.emf.persistence.emf_id="_558yhKvjEe6I4bA9GxwhqQ"/>
 </org.eventb.core.machineFile>

BIG/Fabric_Ethereum_m2.bcm

@@ -19,8 +19,8 @@
         <org.eventb.core.scExtendsContext name="'" org.eventb.core.scTarget="/BIG/BIG_c1.bcc|org.eventb.core.scContextFile#BIG_c1" org.eventb.core.source="/BIG/Fabric_Ethereum_c2.buc|org.eventb.core.contextFile#Fabric_Ethereum_c2|org.eventb.core.extendsContext#'"/>
         <org.eventb.core.scCarrierSet name="ACCOUNTS" org.eventb.core.source="/BIG/Fabric_Ethereum_c2.buc|org.eventb.core.contextFile#Fabric_Ethereum_c2|org.eventb.core.carrierSet#_u7_J0qsXEe6I4bA9GxwhqQ" org.eventb.core.type="ℙ(ACCOUNTS)"/>
     </org.eventb.core.scInternalContext>
-    <org.eventb.core.scInvariant name="BIG_c2" org.eventb.core.label="inv11;" org.eventb.core.predicate="received_transactions∈CROSS_CHAIN_SMART_CONTRACTS ↠ TRANSACTIONS" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_asVK0KvhEe6I4bA9GxwhqQ" org.eventb.core.theorem="false"/>
-    <org.eventb.core.scInvariant name="BIG_c3" org.eventb.core.label="inv2;" org.eventb.core.predicate="triggered_events∈CROSS_CHAIN_SMART_CONTRACTS ↔ CROSS_CHAIN_EVENTS" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_d6dcQKmHEe6I4bA9GxwhqQ" org.eventb.core.theorem="false"/>
+    <org.eventb.core.scInvariant name="BIG_c2" org.eventb.core.label="inv1;" org.eventb.core.predicate="received_transactions∈CROSS_CHAIN_SMART_CONTRACTS ↠ TRANSACTIONS" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_o6juoKviEe6I4bA9GxwhqQ" org.eventb.core.theorem="false"/>
+    <org.eventb.core.scInvariant name="BIG_c3" org.eventb.core.label="inv2;" org.eventb.core.predicate="triggered_events∈CROSS_CHAIN_SMART_CONTRACTS ↠ CROSS_CHAIN_EVENTS" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_d6dcQKmHEe6I4bA9GxwhqQ" org.eventb.core.theorem="false"/>
     <org.eventb.core.scInvariant name="BIG_c4" org.eventb.core.label="inv3;" org.eventb.core.predicate="subscriptions∈GATEWAYS ↔ CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_Q6dKkKpAEe6I4bA9GxwhqQ" org.eventb.core.theorem="false"/>
     <org.eventb.core.scInvariant name="BIG_c5" org.eventb.core.label="inv4;" org.eventb.core.predicate="gateway_pending_transactions∈GATEWAYS ↔ CROSS_CHAIN_TRANSACTIONS" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_c7TQ0KpBEe6I4bA9GxwhqQ" org.eventb.core.theorem="false"/>
     <org.eventb.core.scInvariant name="BIG_c6" org.eventb.core.label="inv6;" org.eventb.core.predicate="received_cross_chain_transactions∈CROSS_CHAIN_SMART_CONTRACTS ↔ CROSS_CHAIN_TRANSACTIONS" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_G1eDUKpbEe6I4bA9GxwhqQ" org.eventb.core.theorem="false"/>

BIG/Fabric_Ethereum_m2.bpo

 <?xml version="1.0" encoding="UTF-8" standalone="no"?>
-<org.eventb.core.poFile org.eventb.core.poStamp="13">
+<org.eventb.core.poFile org.eventb.core.poStamp="14">
     <org.eventb.core.poPredicateSet name="CTXHYP" org.eventb.core.poStamp="10">
         <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)"/>
@@ -14,15 +14,15 @@
         <org.eventb.core.poPredicate name="CROSS_CHAIN_SMART_CONTRACTV" org.eventb.core.predicate="gateway∈GATEWAYS" org.eventb.core.source="/BIG/BIG_c1.buc|org.eventb.core.contextFile#BIG_c1|org.eventb.core.axiom#_j4-vYasXEe6I4bA9GxwhqQ"/>
         <org.eventb.core.poIdentifier name="ACCOUNTS" org.eventb.core.type="ℙ(ACCOUNTS)"/>
     </org.eventb.core.poPredicateSet>
-    <org.eventb.core.poPredicateSet name="ABSHYP" org.eventb.core.parentSet="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poStamp="13">
+    <org.eventb.core.poPredicateSet name="ABSHYP" org.eventb.core.parentSet="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poStamp="14">
         <org.eventb.core.poIdentifier name="balances" org.eventb.core.type="ℙ(ACCOUNTS×ℤ)"/>
         <org.eventb.core.poIdentifier name="triggered_events" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_EVENTS)"/>
         <org.eventb.core.poIdentifier name="received_cross_chain_transactions" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_TRANSACTIONS)"/>
         <org.eventb.core.poIdentifier name="subscriptions" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_SMART_CONTRACTS)"/>
         <org.eventb.core.poIdentifier name="gateway_pending_transactions" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_TRANSACTIONS)"/>
         <org.eventb.core.poIdentifier name="received_transactions" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×TRANSACTIONS)"/>
-        <org.eventb.core.poPredicate name="received_cross_chain_transactiont" org.eventb.core.predicate="received_transactions∈CROSS_CHAIN_SMART_CONTRACTS ↠ TRANSACTIONS" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_asVK0KvhEe6I4bA9GxwhqQ"/>
-        <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="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_d6dcQKmHEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.poPredicate name="received_cross_chain_transactiont" org.eventb.core.predicate="received_transactions∈CROSS_CHAIN_SMART_CONTRACTS ↠ TRANSACTIONS" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_o6juoKviEe6I4bA9GxwhqQ"/>
+        <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="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_d6dcQKmHEe6I4bA9GxwhqQ"/>
         <org.eventb.core.poPredicate name="received_cross_chain_transactionv" org.eventb.core.predicate="subscriptions∈GATEWAYS ↔ CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_Q6dKkKpAEe6I4bA9GxwhqQ"/>
         <org.eventb.core.poPredicate name="received_cross_chain_transactionw" org.eventb.core.predicate="gateway_pending_transactions∈GATEWAYS ↔ CROSS_CHAIN_TRANSACTIONS" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_c7TQ0KpBEe6I4bA9GxwhqQ"/>
         <org.eventb.core.poPredicate name="received_cross_chain_transactionx" org.eventb.core.predicate="received_cross_chain_transactions∈CROSS_CHAIN_SMART_CONTRACTS ↔ CROSS_CHAIN_TRANSACTIONS" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.invariant#_G1eDUKpbEe6I4bA9GxwhqQ"/>
@@ -45,50 +45,50 @@
         <org.eventb.core.poIdentifier name="received_cross_chain_transactions'" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_TRANSACTIONS)"/>
     </org.eventb.core.poPredicateSet>
     <org.eventb.core.poPredicateSet name="EVTALLHYPreceived_cross_chain_transactiont" org.eventb.core.parentSet="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#EVTIDENTreceived_cross_chain_transactiont" org.eventb.core.poStamp="11"/>
-    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_cross_chain_transactionu" org.eventb.core.parentSet="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="13">
+    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_cross_chain_transactionu" org.eventb.core.parentSet="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="14">
         <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="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#EVTIDENTreceived_cross_chain_transactionu" org.eventb.core.poStamp="13">
+    <org.eventb.core.poPredicateSet name="EVTALLHYPreceived_cross_chain_transactionu" org.eventb.core.parentSet="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#EVTIDENTreceived_cross_chain_transactionu" org.eventb.core.poStamp="14">
         <org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="gateway ↦ source_smart_contract∉subscriptions" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_I9G5gKpAEe6I4bA9GxwhqQ|org.eventb.core.guard#_SAx1UKmDEe6I4bA9GxwhqQ"/>
     </org.eventb.core.poPredicateSet>
-    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_cross_chain_transactionv" org.eventb.core.parentSet="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="13">
+    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_cross_chain_transactionv" org.eventb.core.parentSet="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="14">
         <org.eventb.core.poIdentifier name="transaction" org.eventb.core.type="TRANSACTIONS"/>
         <org.eventb.core.poIdentifier name="received_transactions'" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×TRANSACTIONS)"/>
     </org.eventb.core.poPredicateSet>
-    <org.eventb.core.poPredicateSet name="EVTALLHYPreceived_cross_chain_transactionv" org.eventb.core.parentSet="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#EVTIDENTreceived_cross_chain_transactionv" org.eventb.core.poStamp="13">
+    <org.eventb.core.poPredicateSet name="EVTALLHYPreceived_cross_chain_transactionv" org.eventb.core.parentSet="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#EVTIDENTreceived_cross_chain_transactionv" org.eventb.core.poStamp="14">
         <org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="transaction∈TRANSACTIONS" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_58YTEKmAEe6I4bA9GxwhqQ|org.eventb.core.guard#_TlWCkqmHEe6I4bA9GxwhqQ"/>
         <org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="transaction∉received_transactions[{source_smart_contract}]" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_58YTEKmAEe6I4bA9GxwhqQ|org.eventb.core.guard#_HCtL8KmIEe6I4bA9GxwhqQ"/>
     </org.eventb.core.poPredicateSet>
-    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_cross_chain_transactionw" org.eventb.core.parentSet="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="13">
+    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_cross_chain_transactionw" org.eventb.core.parentSet="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="14">
         <org.eventb.core.poIdentifier name="triggered_events'" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_EVENTS)"/>
         <org.eventb.core.poIdentifier name="transaction" org.eventb.core.type="TRANSACTIONS"/>
         <org.eventb.core.poIdentifier name="cross_chain_event" org.eventb.core.type="CROSS_CHAIN_EVENTS"/>
         <org.eventb.core.poIdentifier name="received_transactions'" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×TRANSACTIONS)"/>
     </org.eventb.core.poPredicateSet>
-    <org.eventb.core.poPredicateSet name="EVTALLHYPreceived_cross_chain_transactionw" org.eventb.core.parentSet="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#EVTIDENTreceived_cross_chain_transactionw" org.eventb.core.poStamp="13">
+    <org.eventb.core.poPredicateSet name="EVTALLHYPreceived_cross_chain_transactionw" org.eventb.core.parentSet="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#EVTIDENTreceived_cross_chain_transactionw" org.eventb.core.poStamp="14">
         <org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="source_smart_contract ↦ transaction∈received_transactions" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_TlWCkKmHEe6I4bA9GxwhqQ|org.eventb.core.guard#_iUmtQKpAEe6I4bA9GxwhqQ"/>
         <org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="cross_chain_event∉triggered_events[{source_smart_contract}]" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_TlWCkKmHEe6I4bA9GxwhqQ|org.eventb.core.guard#_1SOwwKmDEe6I4bA9GxwhqQ"/>
     </org.eventb.core.poPredicateSet>
-    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_cross_chain_transactionx" org.eventb.core.parentSet="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="13">
+    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_cross_chain_transactionx" org.eventb.core.parentSet="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="14">
         <org.eventb.core.poIdentifier name="cross_chain_transaction" org.eventb.core.type="CROSS_CHAIN_TRANSACTIONS"/>
         <org.eventb.core.poIdentifier name="triggered_events'" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_EVENTS)"/>
         <org.eventb.core.poIdentifier name="gateway_pending_transactions'" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_TRANSACTIONS)"/>
         <org.eventb.core.poIdentifier name="cross_chain_event" org.eventb.core.type="CROSS_CHAIN_EVENTS"/>
     </org.eventb.core.poPredicateSet>
-    <org.eventb.core.poPredicateSet name="EVTALLHYPreceived_cross_chain_transactionx" org.eventb.core.parentSet="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#EVTIDENTreceived_cross_chain_transactionx" org.eventb.core.poStamp="13">
+    <org.eventb.core.poPredicateSet name="EVTALLHYPreceived_cross_chain_transactionx" org.eventb.core.parentSet="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#EVTIDENTreceived_cross_chain_transactionx" org.eventb.core.poStamp="14">
         <org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="source_smart_contract ↦ cross_chain_event∈triggered_events" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_8VKFEKpAEe6I4bA9GxwhqQ|org.eventb.core.guard#_DMOGsKpFEe6I4bA9GxwhqQ"/>
         <org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="gateway ↦ source_smart_contract∈subscriptions" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_8VKFEKpAEe6I4bA9GxwhqQ|org.eventb.core.guard#_AezaEKmIEe6I4bA9GxwhqQ"/>
         <org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="gateway ↦ cross_chain_transaction∉gateway_pending_transactions" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_8VKFEKpAEe6I4bA9GxwhqQ|org.eventb.core.guard#_x51DwKpCEe6I4bA9GxwhqQ"/>
     </org.eventb.core.poPredicateSet>
-    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_cross_chain_transactiony" org.eventb.core.parentSet="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="13">
+    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_cross_chain_transactiony" org.eventb.core.parentSet="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="14">
         <org.eventb.core.poIdentifier name="cross_chain_transaction" org.eventb.core.type="CROSS_CHAIN_TRANSACTIONS"/>
         <org.eventb.core.poIdentifier name="gateway_pending_transactions'" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_TRANSACTIONS)"/>
         <org.eventb.core.poIdentifier name="received_cross_chain_transactions'" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_TRANSACTIONS)"/>
     </org.eventb.core.poPredicateSet>
-    <org.eventb.core.poPredicateSet name="EVTALLHYPreceived_cross_chain_transactiony" org.eventb.core.parentSet="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#EVTIDENTreceived_cross_chain_transactiony" org.eventb.core.poStamp="13">
+    <org.eventb.core.poPredicateSet name="EVTALLHYPreceived_cross_chain_transactiony" org.eventb.core.parentSet="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#EVTIDENTreceived_cross_chain_transactiony" org.eventb.core.poStamp="14">
         <org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="gateway ↦ cross_chain_transaction∈gateway_pending_transactions" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_0sEN8KpaEe6I4bA9GxwhqQ|org.eventb.core.guard#_tUzFcKpaEe6I4bA9GxwhqQ"/>
     </org.eventb.core.poPredicateSet>
-    <org.eventb.core.poPredicateSet name="ALLHYP" org.eventb.core.parentSet="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poStamp="13">
+    <org.eventb.core.poPredicateSet name="ALLHYP" org.eventb.core.parentSet="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poStamp="14">
         <org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="balances∈ACCOUNTS ↔ ℕ1" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.invariant#_sn-N4KsZEe6I4bA9GxwhqQ"/>
     </org.eventb.core.poPredicateSet>
 </org.eventb.core.poFile>