diff --git a/BIG/Fabric_Ethereum_c2.bcc b/BIG/Fabric_Ethereum_c2.bcc
index 753604b94311311dd7e3853d33d2ea7adf2c674b..c6901de2fd1cf89845ad88e52311a8f4d322d4d0 100644
--- a/BIG/Fabric_Ethereum_c2.bcc
+++ b/BIG/Fabric_Ethereum_c2.bcc
@@ -14,5 +14,9 @@
         <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.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.scAxiom name="BIG_c2" org.eventb.core.label="axm11;" org.eventb.core.predicate="gateway_address∈ADDRESS" org.eventb.core.source="/BIG/Fabric_Ethereum_c2.buc|org.eventb.core.contextFile#Fabric_Ethereum_c2|org.eventb.core.axiom#_oy3_gLR4Ee64F9fr4UDNUA" org.eventb.core.theorem="false"/>
+    <org.eventb.core.scAxiom name="BIG_c3" org.eventb.core.label="axm12;" org.eventb.core.predicate="initial_deposit&gt;0" org.eventb.core.source="/BIG/Fabric_Ethereum_c2.buc|org.eventb.core.contextFile#Fabric_Ethereum_c2|org.eventb.core.axiom#_oy4mkLR4Ee64F9fr4UDNUA" org.eventb.core.theorem="false"/>
+    <org.eventb.core.scConstant name="initial_deposit" org.eventb.core.source="/BIG/Fabric_Ethereum_c2.buc|org.eventb.core.contextFile#Fabric_Ethereum_c2|org.eventb.core.constant#_oy5NobR4Ee64F9fr4UDNUA" org.eventb.core.type="ℤ"/>
+    <org.eventb.core.scCarrierSet name="ADDRESS" org.eventb.core.source="/BIG/Fabric_Ethereum_c2.buc|org.eventb.core.contextFile#Fabric_Ethereum_c2|org.eventb.core.carrierSet#_oy50sLR4Ee64F9fr4UDNUA" org.eventb.core.type="â„™(ADDRESS)"/>
+    <org.eventb.core.scConstant name="gateway_address" org.eventb.core.source="/BIG/Fabric_Ethereum_c2.buc|org.eventb.core.contextFile#Fabric_Ethereum_c2|org.eventb.core.constant#_oy5NoLR4Ee64F9fr4UDNUA" org.eventb.core.type="ADDRESS"/>
 </org.eventb.core.scContextFile>
diff --git a/BIG/Fabric_Ethereum_c2.bpo b/BIG/Fabric_Ethereum_c2.bpo
index 86a693c28d20591b275c7fd72d0c9489efcca74a..c442f9485e183639867ad45e397a36a07b05dd9f 100644
--- a/BIG/Fabric_Ethereum_c2.bpo
+++ b/BIG/Fabric_Ethereum_c2.bpo
@@ -1,6 +1,6 @@
 <?xml version="1.0" encoding="UTF-8" standalone="no"?>
-<org.eventb.core.poFile org.eventb.core.poStamp="9">
-    <org.eventb.core.poPredicateSet name="ABSHYP" org.eventb.core.poStamp="9">
+<org.eventb.core.poFile org.eventb.core.poStamp="10">
+    <org.eventb.core.poPredicateSet name="ABSHYP" 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)"/>
         <org.eventb.core.poIdentifier name="GATEWAYS" org.eventb.core.type="â„™(GATEWAYS)"/>
@@ -12,7 +12,12 @@
         <org.eventb.core.poPredicate name="CROSS_CHAIN_SMART_CONTRACTT" org.eventb.core.predicate="source_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-IUKsXEe6I4bA9GxwhqQ"/>
         <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.poIdentifier name="ACCOUNTS" org.eventb.core.type="â„™(ACCOUNTS)"/>
+        <org.eventb.core.poIdentifier name="ADDRESS" org.eventb.core.type="â„™(ADDRESS)"/>
+        <org.eventb.core.poIdentifier name="initial_deposit" org.eventb.core.type="ℤ"/>
+        <org.eventb.core.poIdentifier name="gateway_address" org.eventb.core.type="ADDRESS"/>
+    </org.eventb.core.poPredicateSet>
+    <org.eventb.core.poPredicateSet name="ALLHYP" org.eventb.core.parentSet="/BIG/Fabric_Ethereum_c2.bpo|org.eventb.core.poFile#Fabric_Ethereum_c2|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poStamp="10">
+        <org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="gateway_address∈ADDRESS" org.eventb.core.source="/BIG/Fabric_Ethereum_c2.buc|org.eventb.core.contextFile#Fabric_Ethereum_c2|org.eventb.core.axiom#_oy3_gLR4Ee64F9fr4UDNUA"/>
+        <org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="initial_deposit&gt;0" org.eventb.core.source="/BIG/Fabric_Ethereum_c2.buc|org.eventb.core.contextFile#Fabric_Ethereum_c2|org.eventb.core.axiom#_oy4mkLR4Ee64F9fr4UDNUA"/>
     </org.eventb.core.poPredicateSet>
-    <org.eventb.core.poPredicateSet name="ALLHYP" org.eventb.core.parentSet="/BIG/Fabric_Ethereum_c2.bpo|org.eventb.core.poFile#Fabric_Ethereum_c2|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poStamp="9"/>
 </org.eventb.core.poFile>
diff --git a/BIG/Fabric_Ethereum_c2.buc b/BIG/Fabric_Ethereum_c2.buc
index a153e18a949a1d20e718e7ce837d0b675f15d85e..7ade93ba0b382e1287b337a57cd34950b1730255 100644
--- a/BIG/Fabric_Ethereum_c2.buc
+++ b/BIG/Fabric_Ethereum_c2.buc
@@ -1,5 +1,9 @@
 <?xml version="1.0" encoding="UTF-8" standalone="no"?>
-<org.eventb.core.contextFile org.eventb.core.configuration="org.eventb.core.fwd;de.prob.symbolic.ctxBase" org.eventb.core.generated="false" org.eventb.emf.persistence.emf_id="_1wfRkasZEe6I4bA9GxwhqQ" org.eventb.texttools.text_lastmodified="1704383796522" org.eventb.texttools.text_representation="context Fabric_Ethereum_c2 extends BIG_c1&#10;&#10;sets ACCOUNTS&#10;&#10;end&#10;" version="3">
+<org.eventb.core.contextFile org.eventb.core.configuration="org.eventb.core.fwd;de.prob.symbolic.ctxBase" org.eventb.core.generated="false" org.eventb.emf.persistence.emf_id="_oyp9FbR4Ee64F9fr4UDNUA" org.eventb.texttools.text_lastmodified="1705414072162" org.eventb.texttools.text_representation="context Fabric_Ethereum_c2 extends BIG_c1&#10;&#10;sets ADDRESS&#10;&#10;constants gateway_address initial_deposit&#10;&#10;axioms&#10;&#9;@axm11: gateway_address ∈ ADDRESS&#10;&#9;@axm12: initial_deposit &gt; 0&#10;end&#10;" version="3">
     <org.eventb.core.extendsContext name="'" org.eventb.core.target="BIG_c1"/>
-    <org.eventb.core.carrierSet name="_u7_J0qsXEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="ACCOUNTS" org.eventb.emf.persistence.emf_id="_1wfRkKsZEe6I4bA9GxwhqQ"/>
+    <org.eventb.core.axiom name="_oy3_gLR4Ee64F9fr4UDNUA" org.eventb.core.generated="false" org.eventb.core.label="axm11;" org.eventb.core.predicate="gateway_address ∈ ADDRESS" org.eventb.emf.persistence.emf_id="_oyp9E7R4Ee64F9fr4UDNUA"/>
+    <org.eventb.core.axiom name="_oy4mkLR4Ee64F9fr4UDNUA" org.eventb.core.generated="false" org.eventb.core.label="axm12;" org.eventb.core.predicate="initial_deposit &gt; 0" org.eventb.emf.persistence.emf_id="_oyp9FLR4Ee64F9fr4UDNUA"/>
+    <org.eventb.core.constant name="_oy5NoLR4Ee64F9fr4UDNUA" org.eventb.core.generated="false" org.eventb.core.identifier="gateway_address" org.eventb.emf.persistence.emf_id="_oyp9EbR4Ee64F9fr4UDNUA"/>
+    <org.eventb.core.constant name="_oy5NobR4Ee64F9fr4UDNUA" org.eventb.core.generated="false" org.eventb.core.identifier="initial_deposit" org.eventb.emf.persistence.emf_id="_oyp9ErR4Ee64F9fr4UDNUA"/>
+    <org.eventb.core.carrierSet name="_oy50sLR4Ee64F9fr4UDNUA" org.eventb.core.generated="false" org.eventb.core.identifier="ADDRESS" org.eventb.emf.persistence.emf_id="_oyp9ELR4Ee64F9fr4UDNUA"/>
 </org.eventb.core.contextFile>
diff --git a/BIG/Fabric_Ethereum_m2.bcm b/BIG/Fabric_Ethereum_m2.bcm
index d5e7649a08dc31ddfb2ec3c8961be7a48c407e0d..b585607144f8a45633cb7a29f3ed7900757a0bf1 100644
--- a/BIG/Fabric_Ethereum_m2.bcm
+++ b/BIG/Fabric_Ethereum_m2.bcm
@@ -17,28 +17,34 @@
     </org.eventb.core.scInternalContext>
     <org.eventb.core.scInternalContext name="Fabric_Ethereum_c2">
         <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.scAxiom name="BIG_c2" org.eventb.core.label="axm11;" org.eventb.core.predicate="gateway_address∈ADDRESS" org.eventb.core.source="/BIG/Fabric_Ethereum_c2.buc|org.eventb.core.contextFile#Fabric_Ethereum_c2|org.eventb.core.axiom#_oy3_gLR4Ee64F9fr4UDNUA" org.eventb.core.theorem="false"/>
+        <org.eventb.core.scAxiom name="BIG_c3" org.eventb.core.label="axm12;" org.eventb.core.predicate="initial_deposit&gt;0" org.eventb.core.source="/BIG/Fabric_Ethereum_c2.buc|org.eventb.core.contextFile#Fabric_Ethereum_c2|org.eventb.core.axiom#_oy4mkLR4Ee64F9fr4UDNUA" org.eventb.core.theorem="false"/>
+        <org.eventb.core.scConstant name="initial_deposit" org.eventb.core.source="/BIG/Fabric_Ethereum_c2.buc|org.eventb.core.contextFile#Fabric_Ethereum_c2|org.eventb.core.constant#_oy5NobR4Ee64F9fr4UDNUA" org.eventb.core.type="ℤ"/>
+        <org.eventb.core.scCarrierSet name="ADDRESS" org.eventb.core.source="/BIG/Fabric_Ethereum_c2.buc|org.eventb.core.contextFile#Fabric_Ethereum_c2|org.eventb.core.carrierSet#_oy50sLR4Ee64F9fr4UDNUA" org.eventb.core.type="â„™(ADDRESS)"/>
+        <org.eventb.core.scConstant name="gateway_address" org.eventb.core.source="/BIG/Fabric_Ethereum_c2.buc|org.eventb.core.contextFile#Fabric_Ethereum_c2|org.eventb.core.constant#_oy5NoLR4Ee64F9fr4UDNUA" org.eventb.core.type="ADDRESS"/>
     </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"/>
-    <org.eventb.core.scInvariant name="Fabric_Ethereum_c3" org.eventb.core.label="inv1;" 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.theorem="false"/>
-    <org.eventb.core.scVariable name="balances" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.variable#_DPQj0KsaEe6I4bA9GxwhqQ" org.eventb.core.type="ℙ(ACCOUNTS×ℤ)"/>
+    <org.eventb.core.scInvariant name="Fabric_Ethereum_c3" org.eventb.core.label="inv11;" org.eventb.core.predicate="balances∈ADDRESS ⇸ ℕ" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.invariant#_BruvcLR5Ee6ab9MA5fTFUw" org.eventb.core.theorem="false"/>
+    <org.eventb.core.scInvariant name="Fabric_Ethereum_c4" org.eventb.core.label="inv12;" org.eventb.core.predicate="gateway_address∈dom(balances)" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.invariant#_Brv9kLR5Ee6ab9MA5fTFUw" org.eventb.core.theorem="false"/>
+    <org.eventb.core.scInvariant name="Fabric_Ethereum_c5" org.eventb.core.label="inv13;" org.eventb.core.predicate="balances(gateway_address)≥0" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.invariant#_Brv9kbR5Ee6ab9MA5fTFUw" org.eventb.core.theorem="false"/>
+    <org.eventb.core.scVariable name="balances" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.variable#_DPQj0KsaEe6I4bA9GxwhqQ" org.eventb.core.type="ℙ(ADDRESS×ℤ)"/>
     <org.eventb.core.scVariable name="triggered_events" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.variable#_YvZFkamHEe6I4bA9GxwhqQ" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_EVENTS)"/>
     <org.eventb.core.scVariable name="received_cross_chain_transactions" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.variable#_H2zkgKpbEe6I4bA9GxwhqQ" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_TRANSACTIONS)"/>
     <org.eventb.core.scVariable name="subscriptions" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.variable#_I9HgkapAEe6I4bA9GxwhqQ" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_SMART_CONTRACTS)"/>
     <org.eventb.core.scVariable name="gateway_pending_transactions" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.variable#_8T2BAKpBEe6I4bA9GxwhqQ" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_TRANSACTIONS)"/>
     <org.eventb.core.scVariable name="received_transactions" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.variable#_SAycYamDEe6I4bA9GxwhqQ" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×TRANSACTIONS)"/>
-    <org.eventb.core.scEvent name="received_cross_chain_transactiont" org.eventb.core.accurate="false" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="INITIALISATION" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.event#_sUpukKl_Ee6I4bA9GxwhqR">
+    <org.eventb.core.scEvent name="received_cross_chain_transactiont" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="INITIALISATION" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.event#_sUpukKl_Ee6I4bA9GxwhqR">
         <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/BIG/BIG_m1.bcm|org.eventb.core.scMachineFile#BIG_m1|org.eventb.core.scEvent#received_cross_chain_transactiont" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.event#_sUpukKl_Ee6I4bA9GxwhqR"/>
         <org.eventb.core.scAction name="'" org.eventb.core.assignment="received_transactions ≔ ∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×TRANSACTIONS)" org.eventb.core.label="act1;" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#'|org.eventb.core.action#_SAxOQKmDEe6I4bA9GxwhqQ"/>
         <org.eventb.core.scAction name="(" org.eventb.core.assignment="triggered_events ≔ ∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_EVENTS)" org.eventb.core.label="act2;" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#'|org.eventb.core.action#_TlWCkamHEe6I4bA9GxwhqQ"/>
         <org.eventb.core.scAction name=")" org.eventb.core.assignment="subscriptions ≔ ∅ ⦂ ℙ(GATEWAYS×CROSS_CHAIN_SMART_CONTRACTS)" org.eventb.core.label="act3;" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#'|org.eventb.core.action#_mv5M0KpAEe6I4bA9GxwhqQ"/>
         <org.eventb.core.scAction name="*" org.eventb.core.assignment="gateway_pending_transactions ≔ ∅ ⦂ ℙ(GATEWAYS×CROSS_CHAIN_TRANSACTIONS)" org.eventb.core.label="act4;" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#'|org.eventb.core.action#_8Ty9sKpBEe6I4bA9GxwhqQ"/>
         <org.eventb.core.scAction name="+" org.eventb.core.assignment="received_cross_chain_transactions ≔ ∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_TRANSACTIONS)" org.eventb.core.label="act6;" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#'|org.eventb.core.action#_J6KjYKpbEe6I4bA9GxwhqQ"/>
-        <org.eventb.core.scAction name="," org.eventb.core.assignment="balances :∣ ⊤" org.eventb.core.label="GEN" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.event#_sUpukKl_Ee6I4bA9GxwhqR"/>
+        <org.eventb.core.scAction name="," org.eventb.core.assignment="balances ≔ {gateway_address ↦ initial_deposit}" org.eventb.core.label="act11;" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.event#_sUpukKl_Ee6I4bA9GxwhqR|org.eventb.core.action#_BrsTMLR5Ee6ab9MA5fTFUw"/>
     </org.eventb.core.scEvent>
     <org.eventb.core.scEvent name="received_cross_chain_transactionu" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="SUBSCRIBE_SMART_CONTRACT_EVENTS" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.event#_sUpukKl_Ee6I4bA9GxwhqS">
         <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/BIG/BIG_m1.bcm|org.eventb.core.scMachineFile#BIG_m1|org.eventb.core.scEvent#received_cross_chain_transactionu" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.event#_sUpukKl_Ee6I4bA9GxwhqS|org.eventb.core.refinesEvent#'"/>
@@ -77,5 +83,17 @@
         <org.eventb.core.scAction name="cross_chain_transactioo" org.eventb.core.assignment="received_cross_chain_transactions ≔ received_cross_chain_transactions∪{target_smart_contract ↦ cross_chain_transaction}" org.eventb.core.label="act1;" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_0sEN8KpaEe6I4bA9GxwhqQ|org.eventb.core.action#_G1dcQKpbEe6I4bA9GxwhqQ"/>
         <org.eventb.core.scAction name="cross_chain_transactiop" org.eventb.core.assignment="gateway_pending_transactions ≔ gateway_pending_transactions ∖ {gateway ↦ cross_chain_transaction}" org.eventb.core.label="act2;" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_0sEN8KpaEe6I4bA9GxwhqQ|org.eventb.core.action#_G1dcQapbEe6I4bA9GxwhqQ"/>
         <org.eventb.core.scParameter name="cross_chain_transaction" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_0sEN8KpaEe6I4bA9GxwhqQ|org.eventb.core.parameter#_tUzFcapaEe6I4bA9GxwhqQ" org.eventb.core.type="CROSS_CHAIN_TRANSACTIONS"/>
+        <org.eventb.core.scGuard name="cross_chain_transactioq" org.eventb.core.label="grd11;" org.eventb.core.predicate="balances(gateway_address)≥fee" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.event#_sUpukKl_Ee6I4bA9GxwhqW|org.eventb.core.guard#_LUARQLR5Ee6ab9MA5fTFUw" org.eventb.core.theorem="false"/>
+        <org.eventb.core.scGuard name="cross_chain_transactior" org.eventb.core.label="grd12;" org.eventb.core.predicate="fee&gt;0" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.event#_sUpukKl_Ee6I4bA9GxwhqW|org.eventb.core.guard#_m9IJYLR5Ee6ab9MA5fTFUw" org.eventb.core.theorem="false"/>
+        <org.eventb.core.scParameter name="fee" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.event#_sUpukKl_Ee6I4bA9GxwhqW|org.eventb.core.parameter#_LUARQbR5Ee6ab9MA5fTFUw" org.eventb.core.type="ℤ"/>
+        <org.eventb.core.scAction name="cross_chain_transactios" org.eventb.core.assignment="balances ≔ balances{gateway_address ↦ balances(gateway_address) − fee}" org.eventb.core.label="act11;" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.event#_sUpukKl_Ee6I4bA9GxwhqW|org.eventb.core.action#_LT_qMLR5Ee6ab9MA5fTFUw"/>
+    </org.eventb.core.scEvent>
+    <org.eventb.core.scEvent name="received_cross_chain_transactionz" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="DEPOSIT_CRYPTOCURRENCY" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.event#_3N1_ELR5Ee6ab9MA5fTFUw">
+        <org.eventb.core.scGuard name="'" org.eventb.core.label="grd1;" org.eventb.core.predicate="user_address∈ADDRESS" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.event#_3N1_ELR5Ee6ab9MA5fTFUw|org.eventb.core.guard#_3N1_ErR5Ee6ab9MA5fTFUw" org.eventb.core.theorem="false"/>
+        <org.eventb.core.scGuard name="(" org.eventb.core.label="grd2;" org.eventb.core.predicate="amount&gt;0" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.event#_3N1_ELR5Ee6ab9MA5fTFUw|org.eventb.core.guard#_3N1_E7R5Ee6ab9MA5fTFUw" org.eventb.core.theorem="false"/>
+        <org.eventb.core.scGuard name=")" org.eventb.core.label="grd3;" org.eventb.core.predicate="user_address∈dom(balances)" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.event#_3N1_ELR5Ee6ab9MA5fTFUw|org.eventb.core.guard#_XCh4cLR6Ee6ab9MA5fTFUw" org.eventb.core.theorem="false"/>
+        <org.eventb.core.scParameter name="amount" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.event#_3N1_ELR5Ee6ab9MA5fTFUw|org.eventb.core.parameter#_3N1_FbR5Ee6ab9MA5fTFUw" org.eventb.core.type="ℤ"/>
+        <org.eventb.core.scParameter name="user_address" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.event#_3N1_ELR5Ee6ab9MA5fTFUw|org.eventb.core.parameter#_3N1_FLR5Ee6ab9MA5fTFUw" org.eventb.core.type="ADDRESS"/>
+        <org.eventb.core.scAction name="user_addrest" org.eventb.core.assignment="balances ≔ balances{user_address ↦ balances(user_address)+amount}" org.eventb.core.label="act1;" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.event#_3N1_ELR5Ee6ab9MA5fTFUw|org.eventb.core.action#_3N1_EbR5Ee6ab9MA5fTFUw"/>
     </org.eventb.core.scEvent>
 </org.eventb.core.scMachineFile>
diff --git a/BIG/Fabric_Ethereum_m2.bpo b/BIG/Fabric_Ethereum_m2.bpo
index 7d8e9dad720073d0f86fea5132439915a22a4a34..524225e0bc3fe4c1facbc054d6caead0c5e63431 100644
--- a/BIG/Fabric_Ethereum_m2.bpo
+++ b/BIG/Fabric_Ethereum_m2.bpo
@@ -1,6 +1,6 @@
 <?xml version="1.0" encoding="UTF-8" standalone="no"?>
-<org.eventb.core.poFile org.eventb.core.poStamp="14">
-    <org.eventb.core.poPredicateSet name="CTXHYP" org.eventb.core.poStamp="10">
+<org.eventb.core.poFile org.eventb.core.poStamp="20">
+    <org.eventb.core.poPredicateSet name="CTXHYP" org.eventb.core.poStamp="16">
         <org.eventb.core.poIdentifier name="CROSS_CHAIN_EVENTS" org.eventb.core.type="â„™(CROSS_CHAIN_EVENTS)"/>
         <org.eventb.core.poIdentifier name="CROSS_CHAIN_TRANSACTIONS" org.eventb.core.type="â„™(CROSS_CHAIN_TRANSACTIONS)"/>
         <org.eventb.core.poIdentifier name="GATEWAYS" org.eventb.core.type="â„™(GATEWAYS)"/>
@@ -12,83 +12,200 @@
         <org.eventb.core.poPredicate name="CROSS_CHAIN_SMART_CONTRACTT" org.eventb.core.predicate="source_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-IUKsXEe6I4bA9GxwhqQ"/>
         <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.poIdentifier name="ACCOUNTS" org.eventb.core.type="â„™(ACCOUNTS)"/>
+        <org.eventb.core.poIdentifier name="ADDRESS" org.eventb.core.type="â„™(ADDRESS)"/>
+        <org.eventb.core.poIdentifier name="initial_deposit" org.eventb.core.type="ℤ"/>
+        <org.eventb.core.poIdentifier name="gateway_address" org.eventb.core.type="ADDRESS"/>
+        <org.eventb.core.poPredicate name="CROSS_CHAIN_SMART_CONTRACTW" org.eventb.core.predicate="gateway_address∈ADDRESS" org.eventb.core.source="/BIG/Fabric_Ethereum_c2.buc|org.eventb.core.contextFile#Fabric_Ethereum_c2|org.eventb.core.axiom#_oy3_gLR4Ee64F9fr4UDNUA"/>
+        <org.eventb.core.poPredicate name="CROSS_CHAIN_SMART_CONTRACTX" org.eventb.core.predicate="initial_deposit&gt;0" org.eventb.core.source="/BIG/Fabric_Ethereum_c2.buc|org.eventb.core.contextFile#Fabric_Ethereum_c2|org.eventb.core.axiom#_oy4mkLR4Ee64F9fr4UDNUA"/>
     </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="14">
-        <org.eventb.core.poIdentifier name="balances" org.eventb.core.type="ℙ(ACCOUNTS×ℤ)"/>
+    <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="17">
+        <org.eventb.core.poIdentifier name="balances" org.eventb.core.type="ℙ(ADDRESS×ℤ)"/>
         <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#_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_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"/>
     </org.eventb.core.poPredicateSet>
-    <org.eventb.core.poSequent name="INITIALISATION/inv1;/INV" org.eventb.core.accurate="false" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="11">
+    <org.eventb.core.poSequent name="inv13;/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Invariant" org.eventb.core.poStamp="17">
+        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#HYPFabric_Ethereum_c4"/>
+        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="gateway_address∈dom(balances)∧balances∈ADDRESS ⇸ ℤ" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.invariant#_Brv9kbR5Ee6ab9MA5fTFUw"/>
+        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.invariant#_Brv9kbR5Ee6ab9MA5fTFUw"/>
+        <org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poSelHintSnd="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#HYPFabric_Ethereum_c4"/>
+    </org.eventb.core.poSequent>
+    <org.eventb.core.poSequent name="INITIALISATION/inv11;/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="17">
+        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#EVTALLHYPreceived_cross_chain_transactiont"/>
+        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="{gateway_address ↦ initial_deposit}∈ADDRESS ⇸ ℕ" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.invariant#_BruvcLR5Ee6ab9MA5fTFUw"/>
+        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" 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="CONCRETE" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.event#_sUpukKl_Ee6I4bA9GxwhqR"/>
+        <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.invariant#_BruvcLR5Ee6ab9MA5fTFUw"/>
+        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poSequent#INITIALISATION\/inv11;\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
+        <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#HYPFabric_Ethereum_c4|org.eventb.core.poPredicate#PRD0"/>
+    </org.eventb.core.poSequent>
+    <org.eventb.core.poSequent name="INITIALISATION/inv12;/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="17">
         <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#EVTALLHYPreceived_cross_chain_transactiont"/>
-        <org.eventb.core.poPredicate name="SEQHYQ" 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.poPredicate name="SEQHYQ" org.eventb.core.predicate="gateway_address∈dom({gateway_address ↦ initial_deposit})" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.invariant#_Brv9kLR5Ee6ab9MA5fTFUw"/>
         <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" 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="CONCRETE" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.event#_sUpukKl_Ee6I4bA9GxwhqR"/>
-        <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" 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.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poSequent#INITIALISATION\/inv1;\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
-        <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD0"/>
+        <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.invariant#_Brv9kLR5Ee6ab9MA5fTFUw"/>
+        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poSequent#INITIALISATION\/inv12;\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
+        <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#HYPFabric_Ethereum_c4|org.eventb.core.poPredicate#PRD1"/>
     </org.eventb.core.poSequent>
-    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_cross_chain_transactiont" 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="11">
+    <org.eventb.core.poSequent name="INITIALISATION/inv13;/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="17">
+        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#EVTALLHYPreceived_cross_chain_transactiont"/>
+        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="{gateway_address ↦ initial_deposit}(gateway_address)≥0" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.invariant#_Brv9kbR5Ee6ab9MA5fTFUw"/>
+        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" 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="CONCRETE" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.event#_sUpukKl_Ee6I4bA9GxwhqR"/>
+        <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.invariant#_Brv9kbR5Ee6ab9MA5fTFUw"/>
+        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poSequent#INITIALISATION\/inv13;\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
+        <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD2"/>
+    </org.eventb.core.poSequent>
+    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_cross_chain_transactiont" 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="17">
         <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="balances'" org.eventb.core.type="ℙ(ACCOUNTS×ℤ)"/>
+        <org.eventb.core.poIdentifier name="balances'" org.eventb.core.type="ℙ(ADDRESS×ℤ)"/>
         <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/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="14">
+    <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="17"/>
+    <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="17">
         <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="14">
+    <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="17">
         <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="14">
+    <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="17">
         <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="14">
+    <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="17">
         <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="14">
+    <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="17">
         <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="14">
+    <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="17">
         <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="14">
+    <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="17">
         <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="14">
+    <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="17">
         <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="14">
+    <org.eventb.core.poSequent name="GATEWAY_PROCESS_CROSS_CHAIN_TRANSACTION/grd11;/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Guard" org.eventb.core.poStamp="18">
+        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#EVTHYPreceived_cross_chain_transactiony'"/>
+        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="gateway_address∈dom(balances)∧balances∈ADDRESS ⇸ ℤ" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.event#_sUpukKl_Ee6I4bA9GxwhqW|org.eventb.core.guard#_LUARQLR5Ee6ab9MA5fTFUw"/>
+        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.event#_sUpukKl_Ee6I4bA9GxwhqW|org.eventb.core.guard#_LUARQLR5Ee6ab9MA5fTFUw"/>
+        <org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#EVTHYPreceived_cross_chain_transactiony'"/>
+    </org.eventb.core.poSequent>
+    <org.eventb.core.poSequent name="GATEWAY_PROCESS_CROSS_CHAIN_TRANSACTION/inv11;/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="19">
+        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#EVTALLHYPreceived_cross_chain_transactiony"/>
+        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="balances{gateway_address ↦ balances(gateway_address) − fee}∈ADDRESS ⇸ ℕ" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.invariant#_BruvcLR5Ee6ab9MA5fTFUw"/>
+        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_0sEN8KpaEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.event#_sUpukKl_Ee6I4bA9GxwhqW"/>
+        <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.invariant#_BruvcLR5Ee6ab9MA5fTFUw"/>
+        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poSequent#GATEWAY_PROCESS_CROSS_CHAIN_TRANSACTION\/inv11;\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
+        <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#HYPFabric_Ethereum_c4|org.eventb.core.poPredicate#PRD0"/>
+    </org.eventb.core.poSequent>
+    <org.eventb.core.poSequent name="GATEWAY_PROCESS_CROSS_CHAIN_TRANSACTION/inv12;/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="19">
+        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#EVTALLHYPreceived_cross_chain_transactiony"/>
+        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="gateway_address∈dom(balances{gateway_address ↦ balances(gateway_address) − fee})" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.invariant#_Brv9kLR5Ee6ab9MA5fTFUw"/>
+        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_0sEN8KpaEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.event#_sUpukKl_Ee6I4bA9GxwhqW"/>
+        <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.invariant#_Brv9kLR5Ee6ab9MA5fTFUw"/>
+        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poSequent#GATEWAY_PROCESS_CROSS_CHAIN_TRANSACTION\/inv12;\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
+        <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#HYPFabric_Ethereum_c4|org.eventb.core.poPredicate#PRD1"/>
+    </org.eventb.core.poSequent>
+    <org.eventb.core.poSequent name="GATEWAY_PROCESS_CROSS_CHAIN_TRANSACTION/inv13;/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="19">
+        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#EVTALLHYPreceived_cross_chain_transactiony"/>
+        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="(balances{gateway_address ↦ balances(gateway_address) − fee})(gateway_address)≥0" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.invariant#_Brv9kbR5Ee6ab9MA5fTFUw"/>
+        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="ABSTRACT" org.eventb.core.source="/BIG/BIG_m1.bum|org.eventb.core.machineFile#BIG_m1|org.eventb.core.event#_0sEN8KpaEe6I4bA9GxwhqQ"/>
+        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="CONCRETE" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.event#_sUpukKl_Ee6I4bA9GxwhqW"/>
+        <org.eventb.core.poSource name="SEQHYT" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.invariant#_Brv9kbR5Ee6ab9MA5fTFUw"/>
+        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poSequent#GATEWAY_PROCESS_CROSS_CHAIN_TRANSACTION\/inv13;\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
+        <org.eventb.core.poSelHint name="SEQHYV" org.eventb.core.poSelHintFst="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD2"/>
+    </org.eventb.core.poSequent>
+    <org.eventb.core.poSequent name="GATEWAY_PROCESS_CROSS_CHAIN_TRANSACTION/act11;/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of action" org.eventb.core.poStamp="19">
+        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#EVTALLHYPreceived_cross_chain_transactiony"/>
+        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="gateway_address∈dom(balances)∧balances∈ADDRESS ⇸ ℤ" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.event#_sUpukKl_Ee6I4bA9GxwhqW|org.eventb.core.action#_LT_qMLR5Ee6ab9MA5fTFUw"/>
+        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.event#_sUpukKl_Ee6I4bA9GxwhqW|org.eventb.core.action#_LT_qMLR5Ee6ab9MA5fTFUw"/>
+        <org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#EVTALLHYPreceived_cross_chain_transactiony"/>
+    </org.eventb.core.poSequent>
+    <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="18">
         <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="balances'" org.eventb.core.type="ℙ(ADDRESS×ℤ)"/>
         <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="fee" org.eventb.core.type="ℤ"/>
     </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="14">
+    <org.eventb.core.poPredicateSet name="EVTHYPreceived_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="0">
         <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="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 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#EVTHYPreceived_cross_chain_transactiony'" org.eventb.core.poStamp="19">
+        <org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="balances(gateway_address)≥fee" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.event#_sUpukKl_Ee6I4bA9GxwhqW|org.eventb.core.guard#_LUARQLR5Ee6ab9MA5fTFUw"/>
+        <org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="fee&gt;0" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.event#_sUpukKl_Ee6I4bA9GxwhqW|org.eventb.core.guard#_m9IJYLR5Ee6ab9MA5fTFUw"/>
+    </org.eventb.core.poPredicateSet>
+    <org.eventb.core.poSequent name="DEPOSIT_CRYPTOCURRENCY/inv11;/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="20">
+        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#EVTALLHYPreceived_cross_chain_transactionz"/>
+        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="balances{user_address ↦ balances(user_address)+amount}∈ADDRESS ⇸ ℕ" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.invariant#_BruvcLR5Ee6ab9MA5fTFUw"/>
+        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.event#_3N1_ELR5Ee6ab9MA5fTFUw"/>
+        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.invariant#_BruvcLR5Ee6ab9MA5fTFUw"/>
+        <org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poSequent#DEPOSIT_CRYPTOCURRENCY\/inv11;\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
+        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#HYPFabric_Ethereum_c4|org.eventb.core.poPredicate#PRD0"/>
+    </org.eventb.core.poSequent>
+    <org.eventb.core.poSequent name="DEPOSIT_CRYPTOCURRENCY/inv12;/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="20">
+        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#EVTALLHYPreceived_cross_chain_transactionz"/>
+        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="gateway_address∈dom(balances{user_address ↦ balances(user_address)+amount})" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.invariant#_Brv9kLR5Ee6ab9MA5fTFUw"/>
+        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.event#_3N1_ELR5Ee6ab9MA5fTFUw"/>
+        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.invariant#_Brv9kLR5Ee6ab9MA5fTFUw"/>
+        <org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poSequent#DEPOSIT_CRYPTOCURRENCY\/inv12;\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
+        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#HYPFabric_Ethereum_c4|org.eventb.core.poPredicate#PRD1"/>
+    </org.eventb.core.poSequent>
+    <org.eventb.core.poSequent name="DEPOSIT_CRYPTOCURRENCY/inv13;/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="20">
+        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#EVTALLHYPreceived_cross_chain_transactionz"/>
+        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="(balances{user_address ↦ balances(user_address)+amount})(gateway_address)≥0" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.invariant#_Brv9kbR5Ee6ab9MA5fTFUw"/>
+        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.event#_3N1_ELR5Ee6ab9MA5fTFUw"/>
+        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.invariant#_Brv9kbR5Ee6ab9MA5fTFUw"/>
+        <org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poSequent#DEPOSIT_CRYPTOCURRENCY\/inv13;\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
+        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD2"/>
+    </org.eventb.core.poSequent>
+    <org.eventb.core.poSequent name="DEPOSIT_CRYPTOCURRENCY/act1;/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of action" org.eventb.core.poStamp="20">
+        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#EVTALLHYPreceived_cross_chain_transactionz"/>
+        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="user_address∈dom(balances)∧balances∈ADDRESS ⇸ ℤ" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.event#_3N1_ELR5Ee6ab9MA5fTFUw|org.eventb.core.action#_3N1_EbR5Ee6ab9MA5fTFUw"/>
+        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.event#_3N1_ELR5Ee6ab9MA5fTFUw|org.eventb.core.action#_3N1_EbR5Ee6ab9MA5fTFUw"/>
+        <org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#EVTALLHYPreceived_cross_chain_transactionz"/>
+    </org.eventb.core.poSequent>
+    <org.eventb.core.poPredicateSet name="EVTIDENTreceived_cross_chain_transactionz" 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="0">
+        <org.eventb.core.poIdentifier name="amount" org.eventb.core.type="ℤ"/>
+        <org.eventb.core.poIdentifier name="balances'" org.eventb.core.type="ℙ(ADDRESS×ℤ)"/>
+        <org.eventb.core.poIdentifier name="user_address" org.eventb.core.type="ADDRESS"/>
+    </org.eventb.core.poPredicateSet>
+    <org.eventb.core.poPredicateSet name="EVTALLHYPreceived_cross_chain_transactionz" org.eventb.core.parentSet="/BIG/Fabric_Ethereum_m2.bpo|org.eventb.core.poFile#Fabric_Ethereum_m2|org.eventb.core.poPredicateSet#EVTIDENTreceived_cross_chain_transactionz" org.eventb.core.poStamp="20">
+        <org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="user_address∈ADDRESS" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.event#_3N1_ELR5Ee6ab9MA5fTFUw|org.eventb.core.guard#_3N1_ErR5Ee6ab9MA5fTFUw"/>
+        <org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="amount&gt;0" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.event#_3N1_ELR5Ee6ab9MA5fTFUw|org.eventb.core.guard#_3N1_E7R5Ee6ab9MA5fTFUw"/>
+        <org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="user_address∈dom(balances)" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.event#_3N1_ELR5Ee6ab9MA5fTFUw|org.eventb.core.guard#_XCh4cLR6Ee6ab9MA5fTFUw"/>
+    </org.eventb.core.poPredicateSet>
+    <org.eventb.core.poPredicateSet name="HYPFabric_Ethereum_c4" 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="0">
+        <org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="balances∈ADDRESS ⇸ ℕ" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.invariant#_BruvcLR5Ee6ab9MA5fTFUw"/>
+        <org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="gateway_address∈dom(balances)" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.invariant#_Brv9kLR5Ee6ab9MA5fTFUw"/>
+    </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#HYPFabric_Ethereum_c4" org.eventb.core.poStamp="17">
+        <org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="balances(gateway_address)≥0" org.eventb.core.source="/BIG/Fabric_Ethereum_m2.bum|org.eventb.core.machineFile#Fabric_Ethereum_m2|org.eventb.core.invariant#_Brv9kbR5Ee6ab9MA5fTFUw"/>
     </org.eventb.core.poPredicateSet>
 </org.eventb.core.poFile>
diff --git a/BIG/Fabric_Ethereum_m2.bpr b/BIG/Fabric_Ethereum_m2.bpr
index 33fc5c29e9f4a30bc19efe3d345ff2fbde06ddb4..2765d18a88cf86686b697c36fdbb8e9ca0d04bcb 100644
--- a/BIG/Fabric_Ethereum_m2.bpr
+++ b/BIG/Fabric_Ethereum_m2.bpr
@@ -23,4 +23,612 @@
         </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="inv13;/WD" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1,p2" org.eventb.core.prSets="ADDRESS">
+        <org.eventb.core.lang name="L"/>
+        <org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="generalized MP" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p2">
+            <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p3">
+                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p3" org.eventb.core.prHyps="">
+                    <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p4">
+                        <org.eventb.core.prRule name="r2" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="functional goal" org.eventb.core.prGoal="p4" org.eventb.core.prHyps="p1"/>
+                    </org.eventb.core.prAnte>
+                </org.eventb.core.prRule>
+            </org.eventb.core.prAnte>
+        </org.eventb.core.prRule>
+        <org.eventb.core.prIdent name="balances" org.eventb.core.type="ℙ(ADDRESS×ℤ)"/>
+        <org.eventb.core.prIdent name="gateway_address" org.eventb.core.type="ADDRESS"/>
+        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="balances∈ADDRESS ⇸ ℕ"/>
+        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="gateway_address∈dom(balances)∧balances∈ADDRESS ⇸ ℤ"/>
+        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="gateway_address∈dom(balances)"/>
+        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="⊤∧balances∈ADDRESS ⇸ ℤ"/>
+        <org.eventb.core.prPred name="p4" org.eventb.core.predicate="balances∈ADDRESS ⇸ ℤ"/>
+        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
+        <org.eventb.core.prReas name="r2" org.eventb.core.prRID="org.eventb.core.seqprover.isFunGoal"/>
+        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.genMPL4"/>
+    </org.eventb.core.prProof>
+    <org.eventb.core.prProof name="INITIALISATION/inv11;/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1" org.eventb.core.prSets="ADDRESS">
+        <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="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.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="ML" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1">
+                    <org.eventb.core.prString name=".arg" org.eventb.core.prSValue="0;1:500"/>
+                </org.eventb.core.prRule>
+            </org.eventb.core.prAnte>
+        </org.eventb.core.prRule>
+        <org.eventb.core.prIdent name="gateway_address" org.eventb.core.type="ADDRESS"/>
+        <org.eventb.core.prIdent name="initial_deposit" org.eventb.core.type="ℤ"/>
+        <org.eventb.core.prPred name="p5" org.eventb.core.predicate="gateway_address∈ADDRESS"/>
+        <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="initial_deposit&gt;0"/>
+        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="{gateway_address ↦ initial_deposit}∈ADDRESS ⇸ ℕ"/>
+        <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="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.prReas name="r1" org.eventb.core.prRID="com.clearsy.atelierb.provers.core.externalML:1"/>
+        <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="INITIALISATION/inv12;/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="" org.eventb.core.prSets="ADDRESS">
+        <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.prGoal="p0" org.eventb.core.prHyps="">
+            <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p1">
+                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p1" org.eventb.core.prHyps=""/>
+            </org.eventb.core.prAnte>
+        </org.eventb.core.prRule>
+        <org.eventb.core.prIdent name="gateway_address" org.eventb.core.type="ADDRESS"/>
+        <org.eventb.core.prIdent name="initial_deposit" org.eventb.core.type="ℤ"/>
+        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="⊤"/>
+        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="gateway_address∈dom({gateway_address ↦ initial_deposit})"/>
+        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
+        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
+    </org.eventb.core.prProof>
+    <org.eventb.core.prProof name="INITIALISATION/inv13;/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1" org.eventb.core.prSets="ADDRESS">
+        <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.prGoal="p0" org.eventb.core.prHyps="">
+            <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p3">
+                <org.eventb.core.prHypAction name="HIDE0" org.eventb.core.prHyps="p2"/>
+                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="hyp" org.eventb.core.prGoal="p3" org.eventb.core.prHyps="p1"/>
+            </org.eventb.core.prAnte>
+        </org.eventb.core.prRule>
+        <org.eventb.core.prIdent name="gateway_address" org.eventb.core.type="ADDRESS"/>
+        <org.eventb.core.prIdent name="initial_deposit" org.eventb.core.type="ℤ"/>
+        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="initial_deposit&gt;0"/>
+        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="initial_deposit≥0"/>
+        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="{gateway_address ↦ initial_deposit}(gateway_address)≥0"/>
+        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="gateway_address∈dom({gateway_address ↦ initial_deposit})"/>
+        <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.hyp"/>
+    </org.eventb.core.prProof>
+    <org.eventb.core.prProof name="GATEWAY_PROCESS_CROSS_CHAIN_TRANSACTION/grd11;/WD" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1,p2" org.eventb.core.prSets="ADDRESS">
+        <org.eventb.core.lang name="L"/>
+        <org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="generalized MP" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1,p2">
+            <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p3">
+                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p3" org.eventb.core.prHyps="">
+                    <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p4">
+                        <org.eventb.core.prRule name="r2" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p4" org.eventb.core.prHyps=""/>
+                    </org.eventb.core.prAnte>
+                </org.eventb.core.prRule>
+            </org.eventb.core.prAnte>
+        </org.eventb.core.prRule>
+        <org.eventb.core.prIdent name="balances" org.eventb.core.type="ℙ(ADDRESS×ℤ)"/>
+        <org.eventb.core.prIdent name="gateway_address" org.eventb.core.type="ADDRESS"/>
+        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="⊤∧⊤"/>
+        <org.eventb.core.prPred name="p4" org.eventb.core.predicate="⊤"/>
+        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="gateway_address∈dom(balances)∧balances∈ADDRESS ⇸ ℤ"/>
+        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="gateway_address∈dom(balances)"/>
+        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="balances∈ADDRESS ⇸ ℤ"/>
+        <org.eventb.core.prReas name="r2" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
+        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
+        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.genMPL4"/>
+    </org.eventb.core.prProof>
+    <org.eventb.core.prProof name="GATEWAY_PROCESS_CROSS_CHAIN_TRANSACTION/inv11;/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1,p2,p3,p4,p5,p6,p7" org.eventb.core.prSets="ADDRESS,CROSS_CHAIN_TRANSACTIONS,GATEWAYS">
+        <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="p8"/>
+                <org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p9"/>
+                <org.eventb.core.prHypAction name="HIDE2" org.eventb.core.prHyps="p10"/>
+                <org.eventb.core.prHypAction name="HIDE3" org.eventb.core.prHyps="p11"/>
+                <org.eventb.core.prHypAction name="HIDE4" org.eventb.core.prHyps="p12"/>
+                <org.eventb.core.prHypAction name="HIDE5" org.eventb.core.prHyps="p13"/>
+                <org.eventb.core.prHypAction name="HIDE6" org.eventb.core.prHyps="p14"/>
+                <org.eventb.core.prHypAction name="HIDE7" org.eventb.core.prHyps="p15"/>
+                <org.eventb.core.prHypAction name="HIDE8" org.eventb.core.prHyps="p16"/>
+                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="ML" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p2,p1,p4,p7,p5,p3,p6">
+                    <org.eventb.core.prString name=".arg" org.eventb.core.prSValue="0;1:500"/>
+                </org.eventb.core.prRule>
+            </org.eventb.core.prAnte>
+        </org.eventb.core.prRule>
+        <org.eventb.core.prIdent name="balances" org.eventb.core.type="ℙ(ADDRESS×ℤ)"/>
+        <org.eventb.core.prIdent name="cross_chain_transaction" org.eventb.core.type="CROSS_CHAIN_TRANSACTIONS"/>
+        <org.eventb.core.prIdent name="fee" org.eventb.core.type="ℤ"/>
+        <org.eventb.core.prIdent name="gateway" org.eventb.core.type="GATEWAYS"/>
+        <org.eventb.core.prIdent name="gateway_address" org.eventb.core.type="ADDRESS"/>
+        <org.eventb.core.prIdent name="gateway_pending_transactions" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_TRANSACTIONS)"/>
+        <org.eventb.core.prIdent name="initial_deposit" org.eventb.core.type="ℤ"/>
+        <org.eventb.core.prPred name="p14" 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="subscriptions" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_SMART_CONTRACTS)"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p10" org.eventb.core.predicate="gateway∈GATEWAYS"/>
+        <org.eventb.core.prPred name="p4" org.eventb.core.predicate="gateway_address∈dom(balances)"/>
+        <org.eventb.core.prPred name="p15" org.eventb.core.predicate="gateway_pending_transactions∈GATEWAYS ↔ CROSS_CHAIN_TRANSACTIONS"/>
+        <org.eventb.core.prPred name="p9" 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="p12" org.eventb.core.predicate="received_transactions∈CROSS_CHAIN_SMART_CONTRACTS ↔ TRANSACTIONS">
+            <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)"/>
+            <org.eventb.core.prIdent name="received_transactions" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×TRANSACTIONS)"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p7" org.eventb.core.predicate="balances(gateway_address)≥0"/>
+        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="balances∈ADDRESS ⇸ ℕ"/>
+        <org.eventb.core.prPred name="p11" org.eventb.core.predicate="gateway_address∈ADDRESS"/>
+        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="initial_deposit&gt;0"/>
+        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="gateway ↦ cross_chain_transaction∈gateway_pending_transactions"/>
+        <org.eventb.core.prPred name="p13" 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="p8" 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="p16" 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="received_cross_chain_transactions" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_TRANSACTIONS)"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="balances{gateway_address ↦ balances(gateway_address) − fee}∈ADDRESS ⇸ ℕ"/>
+        <org.eventb.core.prPred name="p5" org.eventb.core.predicate="balances∈ADDRESS ⇸ ℤ"/>
+        <org.eventb.core.prPred name="p6" org.eventb.core.predicate="balances(gateway_address)≥fee"/>
+        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="com.clearsy.atelierb.provers.core.externalML:1"/>
+        <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="GATEWAY_PROCESS_CROSS_CHAIN_TRANSACTION/inv12;/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1,p2,p3,p4,p5,p6,p7" org.eventb.core.prSets="ADDRESS,CROSS_CHAIN_TRANSACTIONS,GATEWAYS">
+        <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="p8"/>
+                <org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p9"/>
+                <org.eventb.core.prHypAction name="HIDE2" org.eventb.core.prHyps="p10"/>
+                <org.eventb.core.prHypAction name="HIDE3" org.eventb.core.prHyps="p11"/>
+                <org.eventb.core.prHypAction name="HIDE4" org.eventb.core.prHyps="p12"/>
+                <org.eventb.core.prHypAction name="HIDE5" org.eventb.core.prHyps="p13"/>
+                <org.eventb.core.prHypAction name="HIDE6" org.eventb.core.prHyps="p14"/>
+                <org.eventb.core.prHypAction name="HIDE7" org.eventb.core.prHyps="p15"/>
+                <org.eventb.core.prHypAction name="HIDE8" org.eventb.core.prHyps="p16"/>
+                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="ML" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p2,p1,p4,p7,p5,p3,p6">
+                    <org.eventb.core.prString name=".arg" org.eventb.core.prSValue="0;1:500"/>
+                </org.eventb.core.prRule>
+            </org.eventb.core.prAnte>
+        </org.eventb.core.prRule>
+        <org.eventb.core.prIdent name="balances" org.eventb.core.type="ℙ(ADDRESS×ℤ)"/>
+        <org.eventb.core.prIdent name="cross_chain_transaction" org.eventb.core.type="CROSS_CHAIN_TRANSACTIONS"/>
+        <org.eventb.core.prIdent name="fee" org.eventb.core.type="ℤ"/>
+        <org.eventb.core.prIdent name="gateway" org.eventb.core.type="GATEWAYS"/>
+        <org.eventb.core.prIdent name="gateway_address" org.eventb.core.type="ADDRESS"/>
+        <org.eventb.core.prIdent name="gateway_pending_transactions" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_TRANSACTIONS)"/>
+        <org.eventb.core.prIdent name="initial_deposit" org.eventb.core.type="ℤ"/>
+        <org.eventb.core.prPred name="p14" 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="subscriptions" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_SMART_CONTRACTS)"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p10" org.eventb.core.predicate="gateway∈GATEWAYS"/>
+        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="gateway_address∈dom(balances{gateway_address ↦ balances(gateway_address) − fee})"/>
+        <org.eventb.core.prPred name="p4" org.eventb.core.predicate="gateway_address∈dom(balances)"/>
+        <org.eventb.core.prPred name="p15" org.eventb.core.predicate="gateway_pending_transactions∈GATEWAYS ↔ CROSS_CHAIN_TRANSACTIONS"/>
+        <org.eventb.core.prPred name="p9" 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="p12" org.eventb.core.predicate="received_transactions∈CROSS_CHAIN_SMART_CONTRACTS ↔ TRANSACTIONS">
+            <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)"/>
+            <org.eventb.core.prIdent name="received_transactions" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×TRANSACTIONS)"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p7" org.eventb.core.predicate="balances(gateway_address)≥0"/>
+        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="balances∈ADDRESS ⇸ ℕ"/>
+        <org.eventb.core.prPred name="p11" org.eventb.core.predicate="gateway_address∈ADDRESS"/>
+        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="initial_deposit&gt;0"/>
+        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="gateway ↦ cross_chain_transaction∈gateway_pending_transactions"/>
+        <org.eventb.core.prPred name="p13" 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="p8" 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="p16" 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="received_cross_chain_transactions" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_TRANSACTIONS)"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p5" org.eventb.core.predicate="balances∈ADDRESS ⇸ ℤ"/>
+        <org.eventb.core.prPred name="p6" org.eventb.core.predicate="balances(gateway_address)≥fee"/>
+        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="com.clearsy.atelierb.provers.core.externalML:1"/>
+        <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="GATEWAY_PROCESS_CROSS_CHAIN_TRANSACTION/inv13;/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1,p2,p3,p4,p5,p6,p7,p8,p9" org.eventb.core.prSets="ADDRESS,CROSS_CHAIN_TRANSACTIONS,GATEWAYS">
+        <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.prGoal="p0" org.eventb.core.prHyps="">
+            <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p10">
+                <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="p11"/>
+                        <org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p12"/>
+                        <org.eventb.core.prHypAction name="HIDE2" org.eventb.core.prHyps="p13"/>
+                        <org.eventb.core.prHypAction name="HIDE3" org.eventb.core.prHyps="p14"/>
+                        <org.eventb.core.prHypAction name="HIDE4" org.eventb.core.prHyps="p15"/>
+                        <org.eventb.core.prHypAction name="HIDE5" org.eventb.core.prHyps="p16"/>
+                        <org.eventb.core.prHypAction name="HIDE6" org.eventb.core.prHyps="p17"/>
+                        <org.eventb.core.prHypAction name="HIDE7" org.eventb.core.prHyps="p18"/>
+                        <org.eventb.core.prHypAction name="HIDE8" org.eventb.core.prHyps="p19"/>
+                        <org.eventb.core.prRule name="r2" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="ML" org.eventb.core.prGoal="p10" org.eventb.core.prHyps="p2,p1,p5,p9,p7,p3,p8,p4,p6">
+                            <org.eventb.core.prString name=".arg" org.eventb.core.prSValue="0;1:500"/>
+                        </org.eventb.core.prRule>
+                    </org.eventb.core.prAnte>
+                </org.eventb.core.prRule>
+            </org.eventb.core.prAnte>
+        </org.eventb.core.prRule>
+        <org.eventb.core.prIdent name="balances" org.eventb.core.type="ℙ(ADDRESS×ℤ)"/>
+        <org.eventb.core.prIdent name="cross_chain_transaction" org.eventb.core.type="CROSS_CHAIN_TRANSACTIONS"/>
+        <org.eventb.core.prIdent name="fee" org.eventb.core.type="ℤ"/>
+        <org.eventb.core.prIdent name="gateway" org.eventb.core.type="GATEWAYS"/>
+        <org.eventb.core.prIdent name="gateway_address" org.eventb.core.type="ADDRESS"/>
+        <org.eventb.core.prIdent name="gateway_pending_transactions" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_TRANSACTIONS)"/>
+        <org.eventb.core.prIdent name="initial_deposit" org.eventb.core.type="ℤ"/>
+        <org.eventb.core.prPred name="p17" 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="subscriptions" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_SMART_CONTRACTS)"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p13" org.eventb.core.predicate="gateway∈GATEWAYS"/>
+        <org.eventb.core.prPred name="p4" org.eventb.core.predicate="gateway_address∈dom(balances{gateway_address ↦ balances(gateway_address) − fee})"/>
+        <org.eventb.core.prPred name="p5" org.eventb.core.predicate="gateway_address∈dom(balances)"/>
+        <org.eventb.core.prPred name="p18" org.eventb.core.predicate="gateway_pending_transactions∈GATEWAYS ↔ CROSS_CHAIN_TRANSACTIONS"/>
+        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="(balances{gateway_address ↦ balances(gateway_address) − fee})(gateway_address)≥0"/>
+        <org.eventb.core.prPred name="p12" 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="p15" org.eventb.core.predicate="received_transactions∈CROSS_CHAIN_SMART_CONTRACTS ↔ TRANSACTIONS">
+            <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)"/>
+            <org.eventb.core.prIdent name="received_transactions" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×TRANSACTIONS)"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p9" org.eventb.core.predicate="balances(gateway_address)≥0"/>
+        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="balances∈ADDRESS ⇸ ℕ"/>
+        <org.eventb.core.prPred name="p14" org.eventb.core.predicate="gateway_address∈ADDRESS"/>
+        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="initial_deposit&gt;0"/>
+        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="gateway ↦ cross_chain_transaction∈gateway_pending_transactions"/>
+        <org.eventb.core.prPred name="p16" 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="p11" 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="p10" org.eventb.core.predicate="balances(gateway_address) − fee≥0"/>
+        <org.eventb.core.prPred name="p19" 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="received_cross_chain_transactions" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_TRANSACTIONS)"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p6" org.eventb.core.predicate="balances{gateway_address ↦ balances(gateway_address) − fee}∈ADDRESS ⇸ ℤ"/>
+        <org.eventb.core.prPred name="p7" org.eventb.core.predicate="balances∈ADDRESS ⇸ ℤ"/>
+        <org.eventb.core.prPred name="p8" org.eventb.core.predicate="balances(gateway_address)≥fee"/>
+        <org.eventb.core.prReas name="r2" org.eventb.core.prRID="com.clearsy.atelierb.provers.core.externalML:1"/>
+        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.typeRewrites:1"/>
+        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
+    </org.eventb.core.prProof>
+    <org.eventb.core.prProof name="GATEWAY_PROCESS_CROSS_CHAIN_TRANSACTION/act11;/WD" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1,p2" org.eventb.core.prSets="ADDRESS">
+        <org.eventb.core.lang name="L"/>
+        <org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="generalized MP" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1,p2">
+            <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p3">
+                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p3" org.eventb.core.prHyps="">
+                    <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p4">
+                        <org.eventb.core.prRule name="r2" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p4" org.eventb.core.prHyps=""/>
+                    </org.eventb.core.prAnte>
+                </org.eventb.core.prRule>
+            </org.eventb.core.prAnte>
+        </org.eventb.core.prRule>
+        <org.eventb.core.prIdent name="balances" org.eventb.core.type="ℙ(ADDRESS×ℤ)"/>
+        <org.eventb.core.prIdent name="gateway_address" org.eventb.core.type="ADDRESS"/>
+        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="⊤∧⊤"/>
+        <org.eventb.core.prPred name="p4" org.eventb.core.predicate="⊤"/>
+        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="gateway_address∈dom(balances)∧balances∈ADDRESS ⇸ ℤ"/>
+        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="gateway_address∈dom(balances)"/>
+        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="balances∈ADDRESS ⇸ ℤ"/>
+        <org.eventb.core.prReas name="r2" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
+        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
+        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.genMPL4"/>
+    </org.eventb.core.prProof>
+    <org.eventb.core.prProof name="DEPOSIT_CRYPTOCURRENCY/inv11;/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1,p2,p3,p4,p5,p6,p7" org.eventb.core.prSets="ADDRESS">
+        <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="p8"/>
+                <org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p9"/>
+                <org.eventb.core.prHypAction name="HIDE2" org.eventb.core.prHyps="p10"/>
+                <org.eventb.core.prHypAction name="HIDE3" org.eventb.core.prHyps="p11"/>
+                <org.eventb.core.prHypAction name="HIDE4" org.eventb.core.prHyps="p12"/>
+                <org.eventb.core.prHypAction name="HIDE5" org.eventb.core.prHyps="p13"/>
+                <org.eventb.core.prHypAction name="HIDE6" org.eventb.core.prHyps="p14"/>
+                <org.eventb.core.prHypAction name="HIDE7" org.eventb.core.prHyps="p15"/>
+                <org.eventb.core.prHypAction name="HIDE8" org.eventb.core.prHyps="p16"/>
+                <org.eventb.core.prHypAction name="HIDE9" org.eventb.core.prHyps="p17"/>
+                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="ML" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p2,p1,p4,p7,p5,p3,p6">
+                    <org.eventb.core.prString name=".arg" org.eventb.core.prSValue="0;1:500"/>
+                </org.eventb.core.prRule>
+            </org.eventb.core.prAnte>
+        </org.eventb.core.prRule>
+        <org.eventb.core.prIdent name="amount" org.eventb.core.type="ℤ"/>
+        <org.eventb.core.prIdent name="balances" org.eventb.core.type="ℙ(ADDRESS×ℤ)"/>
+        <org.eventb.core.prIdent name="gateway_address" org.eventb.core.type="ADDRESS"/>
+        <org.eventb.core.prIdent name="initial_deposit" org.eventb.core.type="ℤ"/>
+        <org.eventb.core.prIdent name="user_address" org.eventb.core.type="ADDRESS"/>
+        <org.eventb.core.prPred name="p14" 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="p10" 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="p4" org.eventb.core.predicate="gateway_address∈dom(balances)"/>
+        <org.eventb.core.prPred name="p15" 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="p9" 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="p0" org.eventb.core.predicate="balances{user_address ↦ balances(user_address)+amount}∈ADDRESS ⇸ ℕ"/>
+        <org.eventb.core.prPred name="p12" org.eventb.core.predicate="received_transactions∈CROSS_CHAIN_SMART_CONTRACTS ↔ TRANSACTIONS">
+            <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)"/>
+            <org.eventb.core.prIdent name="received_transactions" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×TRANSACTIONS)"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p7" org.eventb.core.predicate="balances(gateway_address)≥0"/>
+        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="balances∈ADDRESS ⇸ ℕ"/>
+        <org.eventb.core.prPred name="p11" org.eventb.core.predicate="gateway_address∈ADDRESS"/>
+        <org.eventb.core.prPred name="p17" org.eventb.core.predicate="user_address∈ADDRESS"/>
+        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="initial_deposit&gt;0"/>
+        <org.eventb.core.prPred name="p13" 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="p3" org.eventb.core.predicate="amount&gt;0"/>
+        <org.eventb.core.prPred name="p8" 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="p16" 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.prPred name="p5" org.eventb.core.predicate="balances∈ADDRESS ⇸ ℤ"/>
+        <org.eventb.core.prPred name="p6" org.eventb.core.predicate="user_address∈dom(balances)"/>
+        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="com.clearsy.atelierb.provers.core.externalML:1"/>
+        <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="DEPOSIT_CRYPTOCURRENCY/inv12;/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1,p2,p3,p4,p5,p6,p7" org.eventb.core.prSets="ADDRESS">
+        <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="p8"/>
+                <org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p9"/>
+                <org.eventb.core.prHypAction name="HIDE2" org.eventb.core.prHyps="p10"/>
+                <org.eventb.core.prHypAction name="HIDE3" org.eventb.core.prHyps="p11"/>
+                <org.eventb.core.prHypAction name="HIDE4" org.eventb.core.prHyps="p12"/>
+                <org.eventb.core.prHypAction name="HIDE5" org.eventb.core.prHyps="p13"/>
+                <org.eventb.core.prHypAction name="HIDE6" org.eventb.core.prHyps="p14"/>
+                <org.eventb.core.prHypAction name="HIDE7" org.eventb.core.prHyps="p15"/>
+                <org.eventb.core.prHypAction name="HIDE8" org.eventb.core.prHyps="p16"/>
+                <org.eventb.core.prHypAction name="HIDE9" org.eventb.core.prHyps="p17"/>
+                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="ML" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p2,p1,p4,p7,p5,p3,p6">
+                    <org.eventb.core.prString name=".arg" org.eventb.core.prSValue="0;1:500"/>
+                </org.eventb.core.prRule>
+            </org.eventb.core.prAnte>
+        </org.eventb.core.prRule>
+        <org.eventb.core.prIdent name="amount" org.eventb.core.type="ℤ"/>
+        <org.eventb.core.prIdent name="balances" org.eventb.core.type="ℙ(ADDRESS×ℤ)"/>
+        <org.eventb.core.prIdent name="gateway_address" org.eventb.core.type="ADDRESS"/>
+        <org.eventb.core.prIdent name="initial_deposit" org.eventb.core.type="ℤ"/>
+        <org.eventb.core.prIdent name="user_address" org.eventb.core.type="ADDRESS"/>
+        <org.eventb.core.prPred name="p14" 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="p10" 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="p4" org.eventb.core.predicate="gateway_address∈dom(balances)"/>
+        <org.eventb.core.prPred name="p15" 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="p9" 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="p12" org.eventb.core.predicate="received_transactions∈CROSS_CHAIN_SMART_CONTRACTS ↔ TRANSACTIONS">
+            <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)"/>
+            <org.eventb.core.prIdent name="received_transactions" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×TRANSACTIONS)"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p7" org.eventb.core.predicate="balances(gateway_address)≥0"/>
+        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="balances∈ADDRESS ⇸ ℕ"/>
+        <org.eventb.core.prPred name="p11" org.eventb.core.predicate="gateway_address∈ADDRESS"/>
+        <org.eventb.core.prPred name="p17" org.eventb.core.predicate="user_address∈ADDRESS"/>
+        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="initial_deposit&gt;0"/>
+        <org.eventb.core.prPred name="p13" 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="gateway_address∈dom(balances{user_address ↦ balances(user_address)+amount})"/>
+        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="amount&gt;0"/>
+        <org.eventb.core.prPred name="p8" 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="p16" 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.prPred name="p5" org.eventb.core.predicate="balances∈ADDRESS ⇸ ℤ"/>
+        <org.eventb.core.prPred name="p6" org.eventb.core.predicate="user_address∈dom(balances)"/>
+        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="com.clearsy.atelierb.provers.core.externalML:1"/>
+        <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="DEPOSIT_CRYPTOCURRENCY/inv13;/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1,p2,p3,p4,p5,p6,p7,p8,p9" org.eventb.core.prSets="ADDRESS">
+        <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="p10"/>
+                <org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p11"/>
+                <org.eventb.core.prHypAction name="HIDE2" org.eventb.core.prHyps="p12"/>
+                <org.eventb.core.prHypAction name="HIDE3" org.eventb.core.prHyps="p13"/>
+                <org.eventb.core.prHypAction name="HIDE4" org.eventb.core.prHyps="p14"/>
+                <org.eventb.core.prHypAction name="HIDE5" org.eventb.core.prHyps="p15"/>
+                <org.eventb.core.prHypAction name="HIDE6" org.eventb.core.prHyps="p16"/>
+                <org.eventb.core.prHypAction name="HIDE7" org.eventb.core.prHyps="p17"/>
+                <org.eventb.core.prHypAction name="HIDE8" org.eventb.core.prHyps="p18"/>
+                <org.eventb.core.prHypAction name="HIDE9" org.eventb.core.prHyps="p19"/>
+                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="ovr in goal" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
+                    <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p21" org.eventb.core.prHyps="p20">
+                        <org.eventb.core.prRule name="r2" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh with gateway_address=user_address" org.eventb.core.prHyps="p20">
+                            <org.eventb.core.prAnte name="'">
+                                <org.eventb.core.prHypAction name="FORWARD_INF0" org.eventb.core.prHyps="p9" org.eventb.core.prInfHyps="p22"/>
+                                <org.eventb.core.prHypAction name="DESELECT1" org.eventb.core.prHyps="p9"/>
+                                <org.eventb.core.prHypAction name="HIDE2" org.eventb.core.prHyps="p20"/>
+                                <org.eventb.core.prRule name="r3" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="ML" org.eventb.core.prGoal="p21" org.eventb.core.prHyps="p2,p1,p5,p9,p7,p4,p8,p3,p6,p22">
+                                    <org.eventb.core.prString name=".arg" org.eventb.core.prSValue="0;1:500"/>
+                                </org.eventb.core.prRule>
+                            </org.eventb.core.prAnte>
+                        </org.eventb.core.prRule>
+                    </org.eventb.core.prAnte>
+                    <org.eventb.core.prAnte name="(" org.eventb.core.prGoal="p24" org.eventb.core.prHyps="p23">
+                        <org.eventb.core.prRule name="r4" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="Functional image simplification in goal" org.eventb.core.prGoal="p24" org.eventb.core.prHyps="p1">
+                            <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p9">
+                                <org.eventb.core.prRule name="r5" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="hyp" org.eventb.core.prGoal="p9" org.eventb.core.prHyps="p9"/>
+                            </org.eventb.core.prAnte>
+                            <org.eventb.core.prString name=".pos" org.eventb.core.prSValue="0"/>
+                        </org.eventb.core.prRule>
+                    </org.eventb.core.prAnte>
+                    <org.eventb.core.prString name=".pos" org.eventb.core.prSValue="0"/>
+                </org.eventb.core.prRule>
+            </org.eventb.core.prAnte>
+        </org.eventb.core.prRule>
+        <org.eventb.core.prIdent name="amount" org.eventb.core.type="ℤ"/>
+        <org.eventb.core.prIdent name="balances" org.eventb.core.type="ℙ(ADDRESS×ℤ)"/>
+        <org.eventb.core.prIdent name="gateway_address" org.eventb.core.type="ADDRESS"/>
+        <org.eventb.core.prIdent name="initial_deposit" org.eventb.core.type="ℤ"/>
+        <org.eventb.core.prIdent name="user_address" org.eventb.core.type="ADDRESS"/>
+        <org.eventb.core.prPred name="p16" 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="p17" 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="p14" org.eventb.core.predicate="received_transactions∈CROSS_CHAIN_SMART_CONTRACTS ↔ TRANSACTIONS">
+            <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)"/>
+            <org.eventb.core.prIdent name="received_transactions" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×TRANSACTIONS)"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p9" org.eventb.core.predicate="balances(gateway_address)≥0"/>
+        <org.eventb.core.prPred name="p23" org.eventb.core.predicate="¬gateway_address=user_address"/>
+        <org.eventb.core.prPred name="p21" org.eventb.core.predicate="balances(user_address)+amount≥0"/>
+        <org.eventb.core.prPred name="p19" org.eventb.core.predicate="user_address∈ADDRESS"/>
+        <org.eventb.core.prPred name="p15" 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="p20" org.eventb.core.predicate="gateway_address=user_address"/>
+        <org.eventb.core.prPred name="p18" 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.prPred name="p7" org.eventb.core.predicate="balances∈ADDRESS ⇸ ℤ"/>
+        <org.eventb.core.prPred name="p8" org.eventb.core.predicate="user_address∈dom(balances)"/>
+        <org.eventb.core.prPred name="p12" 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="(balances{user_address ↦ balances(user_address)+amount})(gateway_address)≥0"/>
+        <org.eventb.core.prPred name="p5" org.eventb.core.predicate="gateway_address∈dom(balances)"/>
+        <org.eventb.core.prPred name="p11" 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="p24" org.eventb.core.predicate="({user_address} ⩤ balances)(gateway_address)≥0"/>
+        <org.eventb.core.prPred name="p6" org.eventb.core.predicate="balances{user_address ↦ balances(user_address)+amount}∈ADDRESS ⇸ ℤ"/>
+        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="balances∈ADDRESS ⇸ ℕ"/>
+        <org.eventb.core.prPred name="p13" org.eventb.core.predicate="gateway_address∈ADDRESS"/>
+        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="initial_deposit&gt;0"/>
+        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="gateway_address∈dom(balances{user_address ↦ balances(user_address)+amount})"/>
+        <org.eventb.core.prPred name="p4" org.eventb.core.predicate="amount&gt;0"/>
+        <org.eventb.core.prPred name="p10" 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="p22" org.eventb.core.predicate="balances(user_address)≥0"/>
+        <org.eventb.core.prReas name="r2" org.eventb.core.prRID="org.eventb.core.seqprover.eqL1:1"/>
+        <org.eventb.core.prReas name="r3" org.eventb.core.prRID="com.clearsy.atelierb.provers.core.externalML:1"/>
+        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.typeRewrites:1"/>
+        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.funOvr:1"/>
+        <org.eventb.core.prReas name="r4" org.eventb.core.prRID="org.eventb.core.seqprover.funImgSimplifies:0"/>
+        <org.eventb.core.prReas name="r5" org.eventb.core.prRID="org.eventb.core.seqprover.hyp"/>
+    </org.eventb.core.prProof>
+    <org.eventb.core.prProof name="DEPOSIT_CRYPTOCURRENCY/act1;/WD" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1,p2" org.eventb.core.prSets="ADDRESS">
+        <org.eventb.core.lang name="L"/>
+        <org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="generalized MP" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1,p2">
+            <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p3">
+                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="simplification rewrites" org.eventb.core.prGoal="p3" org.eventb.core.prHyps="">
+                    <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p4">
+                        <org.eventb.core.prRule name="r2" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p4" org.eventb.core.prHyps=""/>
+                    </org.eventb.core.prAnte>
+                </org.eventb.core.prRule>
+            </org.eventb.core.prAnte>
+        </org.eventb.core.prRule>
+        <org.eventb.core.prIdent name="balances" org.eventb.core.type="ℙ(ADDRESS×ℤ)"/>
+        <org.eventb.core.prIdent name="user_address" org.eventb.core.type="ADDRESS"/>
+        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="⊤∧⊤"/>
+        <org.eventb.core.prPred name="p4" org.eventb.core.predicate="⊤"/>
+        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="user_address∈dom(balances)∧balances∈ADDRESS ⇸ ℤ"/>
+        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="user_address∈dom(balances)"/>
+        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="balances∈ADDRESS ⇸ ℤ"/>
+        <org.eventb.core.prReas name="r2" org.eventb.core.prRID="org.eventb.core.seqprover.trueGoal"/>
+        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
+        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.genMPL4"/>
+    </org.eventb.core.prProof>
 </org.eventb.core.prFile>
diff --git a/BIG/Fabric_Ethereum_m2.bps b/BIG/Fabric_Ethereum_m2.bps
index 90cd9acf661cb6b2573898ddd7ffc5a46aa0b485..3e6dafb32c2a72d0ddf56a28092bab65fd1e7edd 100644
--- a/BIG/Fabric_Ethereum_m2.bps
+++ b/BIG/Fabric_Ethereum_m2.bps
@@ -1,4 +1,16 @@
 <?xml version="1.0" encoding="UTF-8" standalone="no"?>
 <org.eventb.core.psFile>
-    <org.eventb.core.psStatus name="INITIALISATION/inv1;/INV" org.eventb.core.confidence="0" org.eventb.core.poStamp="11" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="inv13;/WD" org.eventb.core.confidence="1000" org.eventb.core.poStamp="17" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="INITIALISATION/inv11;/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="17" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="INITIALISATION/inv12;/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="17" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="INITIALISATION/inv13;/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="17" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="GATEWAY_PROCESS_CROSS_CHAIN_TRANSACTION/grd11;/WD" org.eventb.core.confidence="1000" org.eventb.core.poStamp="18" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="GATEWAY_PROCESS_CROSS_CHAIN_TRANSACTION/inv11;/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="19" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="GATEWAY_PROCESS_CROSS_CHAIN_TRANSACTION/inv12;/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="19" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="GATEWAY_PROCESS_CROSS_CHAIN_TRANSACTION/inv13;/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="19" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="GATEWAY_PROCESS_CROSS_CHAIN_TRANSACTION/act11;/WD" org.eventb.core.confidence="1000" org.eventb.core.poStamp="19" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="DEPOSIT_CRYPTOCURRENCY/inv11;/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="20" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="DEPOSIT_CRYPTOCURRENCY/inv12;/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="20" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="DEPOSIT_CRYPTOCURRENCY/inv13;/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="20" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="DEPOSIT_CRYPTOCURRENCY/act1;/WD" org.eventb.core.confidence="1000" org.eventb.core.poStamp="20" org.eventb.core.psManual="false"/>
 </org.eventb.core.psFile>
diff --git a/BIG/Fabric_Ethereum_m2.bum b/BIG/Fabric_Ethereum_m2.bum
index 4edd2bad99f8ca767539106dfc472b7774884ed1..3e4f277ee37db105abbcb954be1b69596629ec41 100644
--- a/BIG/Fabric_Ethereum_m2.bum
+++ b/BIG/Fabric_Ethereum_m2.bum
@@ -1,28 +1,44 @@
 <?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="_MkFlQ6saEe6I4bA9GxwhqQ" org.eventb.texttools.text_lastmodified="1704383949573" org.eventb.texttools.text_representation="machine Fabric_Ethereum_m2 refines BIG_m1  sees Fabric_Ethereum_c2&#10;&#10;variables received_transactions triggered_events subscriptions gateway_pending_transactions&#10;received_cross_chain_transactions balances&#10;&#10;invariants&#10;&#9;@inv1: balances ∈ ACCOUNTS ↔ ℕ1&#10;&#10;events&#10;  event INITIALISATION extends INITIALISATION&#10;  end&#10;&#10;  event SUBSCRIBE_SMART_CONTRACT_EVENTS extends SUBSCRIBE_SMART_CONTRACT_EVENTS&#10;  end&#10;&#10;  event SUBMIT_CROSS_CHAIN_TRANSACTION extends SUBMIT_CROSS_CHAIN_TRANSACTION&#10;  end&#10;&#10;  event PROCESS_CROSS_CHAIN_TRANSACTION extends PROCESS_CROSS_CHAIN_TRANSACTION&#10;  end&#10;&#10;  event LISTEN_SMART_CONTRACT_EVENT extends LISTEN_SMART_CONTRACT_EVENT&#10;  end&#10;&#10;  event GATEWAY_PROCESS_CROSS_CHAIN_TRANSACTION extends GATEWAY_PROCESS_CROSS_CHAIN_TRANSACTION&#10;  end&#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="_XCO9obR6Ee6ab9MA5fTFUw" org.eventb.texttools.text_lastmodified="1705414811994" org.eventb.texttools.text_representation="machine Fabric_Ethereum_m2 refines BIG_m1  sees Fabric_Ethereum_c2&#10;&#10;variables received_transactions triggered_events subscriptions gateway_pending_transactions&#10;received_cross_chain_transactions balances&#10;&#10;invariants&#10;  @inv11; balances ∈ ADDRESS ⇸ ℕ&#10;  @inv12; gateway_address ∈ dom(balances)&#10;  @inv13; balances(gateway_address) ≥ 0&#10;&#10;events&#10;  event INITIALISATION extends INITIALISATION&#10;  &#9;then&#10;  &#9;&#9;@act11: balances ≔ {gateway_address ↦ initial_deposit}&#10;  end&#10;&#10;  event SUBSCRIBE_SMART_CONTRACT_EVENTS extends SUBSCRIBE_SMART_CONTRACT_EVENTS&#10;  end&#10;&#10;  event SUBMIT_CROSS_CHAIN_TRANSACTION extends SUBMIT_CROSS_CHAIN_TRANSACTION&#10;  end&#10;&#10;  event PROCESS_CROSS_CHAIN_TRANSACTION extends PROCESS_CROSS_CHAIN_TRANSACTION&#10;  end&#10;&#10;  event LISTEN_SMART_CONTRACT_EVENT extends LISTEN_SMART_CONTRACT_EVENT&#10;  end&#10;&#10;  event GATEWAY_PROCESS_CROSS_CHAIN_TRANSACTION extends GATEWAY_PROCESS_CROSS_CHAIN_TRANSACTION&#10;  &#9;any fee&#10;  &#9;where&#10;  &#9;&#9;@grd11: balances(gateway_address) ≥ fee&#10;  &#9;&#9;@grd12: fee &gt; 0&#10;  &#9;then&#10;  &#9;&#9;@act11: balances(gateway_address) ≔ balances(gateway_address) − fee&#10;  end&#10;&#10;  event DEPOSIT_CRYPTOCURRENCY&#10;  &#9;any user_address amount&#10;  &#9;where&#10;  &#9;&#9;@grd1: user_address ∈ ADDRESS&#10;  &#9;&#9;@grd2: amount &gt; 0&#10;  &#9;&#9;@grd3: user_address ∈ dom(balances)&#10;  &#9;then&#10;  &#9;&#9;@act1: balances(user_address) ≔ balances(user_address) + amount&#10;  end&#10;end&#10;" version="5">
     <org.eventb.core.refinesMachine name="'" org.eventb.core.target="BIG_m1"/>
     <org.eventb.core.seesContext name="_wnFu0KsZEe6I4bA9GxwhqQ" org.eventb.core.target="Fabric_Ethereum_c2"/>
-    <org.eventb.core.event name="_sUpukKl_Ee6I4bA9GxwhqR" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="INITIALISATION" org.eventb.emf.persistence.emf_id="_MkFlN6saEe6I4bA9GxwhqQ"/>
-    <org.eventb.core.event name="_sUpukKl_Ee6I4bA9GxwhqS" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="SUBSCRIBE_SMART_CONTRACT_EVENTS" org.eventb.emf.persistence.emf_id="_MkFlOasaEe6I4bA9GxwhqQ">
+    <org.eventb.core.event name="_sUpukKl_Ee6I4bA9GxwhqR" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="INITIALISATION" org.eventb.emf.persistence.emf_id="_XCO9irR6Ee6ab9MA5fTFUw">
+        <org.eventb.core.action name="_BrsTMLR5Ee6ab9MA5fTFUw" org.eventb.core.assignment="balances ≔ {gateway_address ↦ initial_deposit}" org.eventb.core.generated="false" org.eventb.core.label="act11;" org.eventb.emf.persistence.emf_id="_XCO9ibR6Ee6ab9MA5fTFUw"/>
+    </org.eventb.core.event>
+    <org.eventb.core.event name="_sUpukKl_Ee6I4bA9GxwhqS" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="SUBSCRIBE_SMART_CONTRACT_EVENTS" org.eventb.emf.persistence.emf_id="_XCO9jLR6Ee6ab9MA5fTFUw">
         <org.eventb.core.refinesEvent name="'" org.eventb.core.target="SUBSCRIBE_SMART_CONTRACT_EVENTS"/>
     </org.eventb.core.event>
-    <org.eventb.core.event name="_sUpukKl_Ee6I4bA9GxwhqT" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="SUBMIT_CROSS_CHAIN_TRANSACTION" org.eventb.emf.persistence.emf_id="_MkFlO6saEe6I4bA9GxwhqQ">
+    <org.eventb.core.event name="_sUpukKl_Ee6I4bA9GxwhqT" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="SUBMIT_CROSS_CHAIN_TRANSACTION" org.eventb.emf.persistence.emf_id="_XCO9jrR6Ee6ab9MA5fTFUw">
         <org.eventb.core.refinesEvent name="'" org.eventb.core.target="SUBMIT_CROSS_CHAIN_TRANSACTION"/>
     </org.eventb.core.event>
-    <org.eventb.core.event name="_sUpukKl_Ee6I4bA9GxwhqU" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="PROCESS_CROSS_CHAIN_TRANSACTION" org.eventb.emf.persistence.emf_id="_MkFlPasaEe6I4bA9GxwhqQ">
+    <org.eventb.core.event name="_sUpukKl_Ee6I4bA9GxwhqU" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="PROCESS_CROSS_CHAIN_TRANSACTION" org.eventb.emf.persistence.emf_id="_XCO9kLR6Ee6ab9MA5fTFUw">
         <org.eventb.core.refinesEvent name="'" org.eventb.core.target="PROCESS_CROSS_CHAIN_TRANSACTION"/>
     </org.eventb.core.event>
-    <org.eventb.core.event name="_sUpukKl_Ee6I4bA9GxwhqV" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="LISTEN_SMART_CONTRACT_EVENT" org.eventb.emf.persistence.emf_id="_MkFlP6saEe6I4bA9GxwhqQ">
+    <org.eventb.core.event name="_sUpukKl_Ee6I4bA9GxwhqV" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="LISTEN_SMART_CONTRACT_EVENT" org.eventb.emf.persistence.emf_id="_XCO9krR6Ee6ab9MA5fTFUw">
         <org.eventb.core.refinesEvent name="'" org.eventb.core.target="LISTEN_SMART_CONTRACT_EVENT"/>
     </org.eventb.core.event>
-    <org.eventb.core.event name="_sUpukKl_Ee6I4bA9GxwhqW" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="GATEWAY_PROCESS_CROSS_CHAIN_TRANSACTION" org.eventb.emf.persistence.emf_id="_MkFlQasaEe6I4bA9GxwhqQ">
+    <org.eventb.core.event name="_sUpukKl_Ee6I4bA9GxwhqW" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.generated="false" org.eventb.core.label="GATEWAY_PROCESS_CROSS_CHAIN_TRANSACTION" org.eventb.emf.persistence.emf_id="_XCO9mLR6Ee6ab9MA5fTFUw">
         <org.eventb.core.refinesEvent name="'" org.eventb.core.target="GATEWAY_PROCESS_CROSS_CHAIN_TRANSACTION"/>
+        <org.eventb.core.action name="_LT_qMLR5Ee6ab9MA5fTFUw" org.eventb.core.assignment="balances(gateway_address) ≔ balances(gateway_address) − fee" org.eventb.core.generated="false" org.eventb.core.label="act11;" org.eventb.emf.persistence.emf_id="_XCO9l7R6Ee6ab9MA5fTFUw"/>
+        <org.eventb.core.guard name="_LUARQLR5Ee6ab9MA5fTFUw" org.eventb.core.generated="false" org.eventb.core.label="grd11;" org.eventb.core.predicate="balances(gateway_address) ≥ fee" org.eventb.emf.persistence.emf_id="_XCO9lbR6Ee6ab9MA5fTFUw"/>
+        <org.eventb.core.guard name="_m9IJYLR5Ee6ab9MA5fTFUw" org.eventb.core.generated="false" org.eventb.core.label="grd12;" org.eventb.core.predicate="fee &gt; 0" org.eventb.emf.persistence.emf_id="_XCO9lrR6Ee6ab9MA5fTFUw"/>
+        <org.eventb.core.parameter name="_LUARQbR5Ee6ab9MA5fTFUw" org.eventb.core.generated="false" org.eventb.core.identifier="fee" org.eventb.emf.persistence.emf_id="_XCO9lLR6Ee6ab9MA5fTFUw"/>
+    </org.eventb.core.event>
+    <org.eventb.core.event name="_3N1_ELR5Ee6ab9MA5fTFUw" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="DEPOSIT_CRYPTOCURRENCY" org.eventb.emf.persistence.emf_id="_XCO9oLR6Ee6ab9MA5fTFUw">
+        <org.eventb.core.action name="_3N1_EbR5Ee6ab9MA5fTFUw" org.eventb.core.assignment="balances(user_address) ≔ balances(user_address) + amount" org.eventb.core.generated="false" org.eventb.core.label="act1;" org.eventb.emf.persistence.emf_id="_XCO9n7R6Ee6ab9MA5fTFUw"/>
+        <org.eventb.core.guard name="_3N1_ErR5Ee6ab9MA5fTFUw" org.eventb.core.generated="false" org.eventb.core.label="grd1;" org.eventb.core.predicate="user_address ∈ ADDRESS" org.eventb.emf.persistence.emf_id="_XCO9nLR6Ee6ab9MA5fTFUw"/>
+        <org.eventb.core.guard name="_3N1_E7R5Ee6ab9MA5fTFUw" org.eventb.core.generated="false" org.eventb.core.label="grd2;" org.eventb.core.predicate="amount &gt; 0" org.eventb.emf.persistence.emf_id="_XCO9nbR6Ee6ab9MA5fTFUw"/>
+        <org.eventb.core.guard name="_XCh4cLR6Ee6ab9MA5fTFUw" org.eventb.core.generated="false" org.eventb.core.label="grd3;" org.eventb.core.predicate="user_address ∈ dom(balances)" org.eventb.emf.persistence.emf_id="_XCO9nrR6Ee6ab9MA5fTFUw"/>
+        <org.eventb.core.parameter name="_3N1_FLR5Ee6ab9MA5fTFUw" org.eventb.core.generated="false" org.eventb.core.identifier="user_address" org.eventb.emf.persistence.emf_id="_XCO9mrR6Ee6ab9MA5fTFUw"/>
+        <org.eventb.core.parameter name="_3N1_FbR5Ee6ab9MA5fTFUw" org.eventb.core.generated="false" org.eventb.core.identifier="amount" org.eventb.emf.persistence.emf_id="_XCO9m7R6Ee6ab9MA5fTFUw"/>
     </org.eventb.core.event>
-    <org.eventb.core.invariant name="_sn-N4KsZEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.label="inv1;" org.eventb.core.predicate="balances ∈ ACCOUNTS ↔ ℕ1" org.eventb.emf.persistence.emf_id="_MkFlNqsaEe6I4bA9GxwhqQ"/>
-    <org.eventb.core.variable name="_SAycYamDEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="received_transactions" org.eventb.emf.persistence.emf_id="_MkFlMKsaEe6I4bA9GxwhqQ"/>
-    <org.eventb.core.variable name="_YvZFkamHEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="triggered_events" org.eventb.emf.persistence.emf_id="_MkFlMasaEe6I4bA9GxwhqQ"/>
-    <org.eventb.core.variable name="_I9HgkapAEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="subscriptions" org.eventb.emf.persistence.emf_id="_MkFlMqsaEe6I4bA9GxwhqQ"/>
-    <org.eventb.core.variable name="_8T2BAKpBEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="gateway_pending_transactions" org.eventb.emf.persistence.emf_id="_MkFlM6saEe6I4bA9GxwhqQ"/>
-    <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="_MkFlNKsaEe6I4bA9GxwhqQ"/>
-    <org.eventb.core.variable name="_DPQj0KsaEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="balances" org.eventb.emf.persistence.emf_id="_MkFlNasaEe6I4bA9GxwhqQ"/>
+    <org.eventb.core.invariant name="_BruvcLR5Ee6ab9MA5fTFUw" org.eventb.core.generated="false" org.eventb.core.label="inv11;" org.eventb.core.predicate="balances ∈ ADDRESS ⇸ ℕ" org.eventb.emf.persistence.emf_id="_XCO9hrR6Ee6ab9MA5fTFUw"/>
+    <org.eventb.core.invariant name="_Brv9kLR5Ee6ab9MA5fTFUw" org.eventb.core.generated="false" org.eventb.core.label="inv12;" org.eventb.core.predicate="gateway_address ∈ dom(balances)" org.eventb.emf.persistence.emf_id="_XCO9h7R6Ee6ab9MA5fTFUw"/>
+    <org.eventb.core.invariant name="_Brv9kbR5Ee6ab9MA5fTFUw" org.eventb.core.generated="false" org.eventb.core.label="inv13;" org.eventb.core.predicate="balances(gateway_address) ≥ 0" org.eventb.emf.persistence.emf_id="_XCO9iLR6Ee6ab9MA5fTFUw"/>
+    <org.eventb.core.variable name="_SAycYamDEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="received_transactions" org.eventb.emf.persistence.emf_id="_XCO9gLR6Ee6ab9MA5fTFUw"/>
+    <org.eventb.core.variable name="_YvZFkamHEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="triggered_events" org.eventb.emf.persistence.emf_id="_XCO9gbR6Ee6ab9MA5fTFUw"/>
+    <org.eventb.core.variable name="_I9HgkapAEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="subscriptions" org.eventb.emf.persistence.emf_id="_XCO9grR6Ee6ab9MA5fTFUw"/>
+    <org.eventb.core.variable name="_8T2BAKpBEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="gateway_pending_transactions" org.eventb.emf.persistence.emf_id="_XCO9g7R6Ee6ab9MA5fTFUw"/>
+    <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="_XCO9hLR6Ee6ab9MA5fTFUw"/>
+    <org.eventb.core.variable name="_DPQj0KsaEe6I4bA9GxwhqQ" org.eventb.core.generated="false" org.eventb.core.identifier="balances" org.eventb.emf.persistence.emf_id="_XCO9hbR6Ee6ab9MA5fTFUw"/>
 </org.eventb.core.machineFile>