Change trigger for emit event

gateway-event-b/CCTx_Abstract_Animation_m2.bcm

@@ -15,86 +15,86 @@
         <org.eventb.core.scCarrierSet name="TRANSACTIONS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_c1.buc|org.eventb.core.contextFile#CCTx_Abstract_DLT_c1|org.eventb.core.carrierSet#_lhTmNL7uEe6laZimEYihUg" org.eventb.core.type="ℙ(TRANSACTIONS)"/>
         <org.eventb.core.scCarrierSet name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_c1.buc|org.eventb.core.contextFile#CCTx_Abstract_DLT_c1|org.eventb.core.carrierSet#_lhTmNb7uEe6laZimEYihUg" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
     </org.eventb.core.scInternalContext>
-    <org.eventb.core.scInvariant name="CCTx_Abstract_DLT_c2" org.eventb.core.label="inv1;" org.eventb.core.predicate="received_transactions∈CROSS_CHAIN_SMART_CONTRACTS ↔ TRANSACTIONS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.invariant#_yREdZL7uEe6laZimEYihUg" org.eventb.core.theorem="false"/>
-    <org.eventb.core.scInvariant name="CCTx_Abstract_DLT_c3" org.eventb.core.label="inv2;" org.eventb.core.predicate="triggered_events∈CROSS_CHAIN_SMART_CONTRACTS ↔ CROSS_CHAIN_EVENTS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.invariant#_yREdZb7uEe6laZimEYihUg" org.eventb.core.theorem="false"/>
-    <org.eventb.core.scInvariant name="CCTx_Abstract_DLT_c4" org.eventb.core.label="inv3;" org.eventb.core.predicate="subscriptions∈GATEWAYS ↔ CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.invariant#_yREdZr7uEe6laZimEYihUg" org.eventb.core.theorem="false"/>
-    <org.eventb.core.scInvariant name="CCTx_Abstract_DLT_c5" org.eventb.core.label="inv4;" org.eventb.core.predicate="gateway_pending_transactions∈GATEWAYS ↔ CROSS_CHAIN_TRANSACTIONS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.invariant#_yREdZ77uEe6laZimEYihUg" org.eventb.core.theorem="false"/>
-    <org.eventb.core.scInvariant name="CCTx_Abstract_DLT_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="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.invariant#_yREdaL7uEe6laZimEYihUg" org.eventb.core.theorem="false"/>
+    <org.eventb.core.scInvariant name="CCTx_Abstract_DLT_c2" org.eventb.core.label="inv1" org.eventb.core.predicate="received_transactions∈CROSS_CHAIN_SMART_CONTRACTS ↔ TRANSACTIONS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.invariant#_zpKWcMQ4Ee609fto5wotHA" org.eventb.core.theorem="false"/>
+    <org.eventb.core.scInvariant name="CCTx_Abstract_DLT_c3" org.eventb.core.label="inv2" org.eventb.core.predicate="emitted_events∈CROSS_CHAIN_SMART_CONTRACTS ↔ CROSS_CHAIN_EVENTS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.invariant#_zpKWccQ4Ee609fto5wotHA" org.eventb.core.theorem="false"/>
+    <org.eventb.core.scInvariant name="CCTx_Abstract_DLT_c4" org.eventb.core.label="inv3" org.eventb.core.predicate="subscriptions∈GATEWAYS ↔ CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.invariant#_zpK9gMQ4Ee609fto5wotHA" org.eventb.core.theorem="false"/>
+    <org.eventb.core.scInvariant name="CCTx_Abstract_DLT_c5" org.eventb.core.label="inv4" org.eventb.core.predicate="gateway_pending_transactions∈GATEWAYS ↔ CROSS_CHAIN_TRANSACTIONS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.invariant#_zpK9gcQ4Ee609fto5wotHA" org.eventb.core.theorem="false"/>
+    <org.eventb.core.scInvariant name="CCTx_Abstract_DLT_c6" org.eventb.core.label="inv5" org.eventb.core.predicate="received_cross_chain_transactions∈CROSS_CHAIN_SMART_CONTRACTS ↔ CROSS_CHAIN_TRANSACTIONS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.invariant#_qTKs0MT7Ee609fto5wotHA" org.eventb.core.theorem="false"/>
     <org.eventb.core.scInvariant name="CCTx_Abstract_DLT_c7" org.eventb.core.label="inv11" org.eventb.core.predicate="subscribed∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.invariant#_VBL34sEUEe6yC4BToIaAqA" org.eventb.core.theorem="false"/>
     <org.eventb.core.scInvariant name="CCTx_Abstract_DLT_c8" org.eventb.core.label="inv12" org.eventb.core.predicate="initiated∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.invariant#_VBMe8MEUEe6yC4BToIaAqA" org.eventb.core.theorem="false"/>
-    <org.eventb.core.scInvariant name="CCTx_Abstract_DLT_c9" org.eventb.core.label="inv13" org.eventb.core.predicate="triggered∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.invariant#_VBMe8cEUEe6yC4BToIaAqA" org.eventb.core.theorem="false"/>
+    <org.eventb.core.scInvariant name="CCTx_Abstract_DLT_c9" org.eventb.core.label="inv13" org.eventb.core.predicate="emitted∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.invariant#_VBMe8cEUEe6yC4BToIaAqA" org.eventb.core.theorem="false"/>
     <org.eventb.core.scInvariant name="CCTx_Abstract_DLT_c:" org.eventb.core.label="inv14" org.eventb.core.predicate="gateway_processing∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.invariant#_VBNGAMEUEe6yC4BToIaAqA" org.eventb.core.theorem="false"/>
     <org.eventb.core.scInvariant name="CCTx_Abstract_DLT_c;" org.eventb.core.label="inv15" org.eventb.core.predicate="submit_cc_tx∈{0,1}" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.invariant#_VBNGAcEUEe6yC4BToIaAqA" org.eventb.core.theorem="false"/>
     <org.eventb.core.scVariable name="gateway_processing" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.variable#_m7KdIMBDEe6yC4BToIaAqA" org.eventb.core.type="ℤ"/>
-    <org.eventb.core.scVariable name="triggered_events" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.variable#_yREdar7uEe6laZimEYihUg" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_EVENTS)"/>
     <org.eventb.core.scVariable name="initiated" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.variable#_zZtTYMBBEe6yC4BToIaAqA" org.eventb.core.type="ℤ"/>
     <org.eventb.core.scVariable name="submit_cc_tx" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.variable#_xgjHcMBDEe6yC4BToIaAqA" org.eventb.core.type="ℤ"/>
     <org.eventb.core.scVariable name="subscribed" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.variable#_65EIQMA-Ee6yC4BToIaAqA" org.eventb.core.type="ℤ"/>
     <org.eventb.core.scVariable name="received_cross_chain_transactions" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.variable#_yREdbb7uEe6laZimEYihUg" 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="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.variable#_yREda77uEe6laZimEYihUg" org.eventb.core.type="ℙ(GATEWAYS×CROSS_CHAIN_SMART_CONTRACTS)"/>
-    <org.eventb.core.scVariable name="triggered" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.variable#_RNsgkMBCEe6yC4BToIaAqA" org.eventb.core.type="ℤ"/>
+    <org.eventb.core.scVariable name="emitted_events" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.variable#_RGqlAPKWEe60CqkwWvstGA" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_EVENTS)"/>
+    <org.eventb.core.scVariable name="emitted" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.variable#_TP7-oPKWEe60CqkwWvstGA" org.eventb.core.type="ℤ"/>
     <org.eventb.core.scVariable name="gateway_pending_transactions" org.eventb.core.abstract="true" org.eventb.core.concrete="true" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.variable#_yREdbL7uEe6laZimEYihUg" 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="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.variable#_yREdab7uEe6laZimEYihUg" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×TRANSACTIONS)"/>
-    <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="SUBSCRIBE_SMART_CONTRACT_EVENTS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqC">
+    <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="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqB">
+        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/gateway-event-b/CCTx_Abstract_DLT_m1.bcm|org.eventb.core.scMachineFile#CCTx_Abstract_DLT_m1|org.eventb.core.scEvent#received_cross_chain_transactiont" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqB"/>
+        <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="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#'|org.eventb.core.action#_zpBMgMQ4Ee609fto5wotHA"/>
+        <org.eventb.core.scAction name="(" org.eventb.core.assignment="emitted_events ≔ ∅ ⦂ ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_EVENTS)" org.eventb.core.label="act2" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#'|org.eventb.core.action#_zpBzkMQ4Ee609fto5wotHA"/>
+        <org.eventb.core.scAction name=")" org.eventb.core.assignment="subscriptions ≔ ∅ ⦂ ℙ(GATEWAYS×CROSS_CHAIN_SMART_CONTRACTS)" org.eventb.core.label="act3" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#'|org.eventb.core.action#_zpBzkcQ4Ee609fto5wotHA"/>
+        <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="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#'|org.eventb.core.action#_zpBzksQ4Ee609fto5wotHA"/>
+        <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="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#'|org.eventb.core.action#_zpCaoMQ4Ee609fto5wotHA"/>
+        <org.eventb.core.scAction name="," org.eventb.core.assignment="subscribed ≔ 0" org.eventb.core.label="act11" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqB|org.eventb.core.action#_VBQJUMEUEe6yC4BToIaAqA"/>
+        <org.eventb.core.scAction name="-" org.eventb.core.assignment="initiated ≔ 0" org.eventb.core.label="act12" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqB|org.eventb.core.action#_VBRXccEUEe6yC4BToIaAqA"/>
+        <org.eventb.core.scAction name="." org.eventb.core.assignment="emitted ≔ 0" org.eventb.core.label="act13" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqB|org.eventb.core.action#_kIrbcMEUEe6yC4BToIaAqA"/>
+        <org.eventb.core.scAction name="/" org.eventb.core.assignment="gateway_processing ≔ 0" org.eventb.core.label="act14" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqB|org.eventb.core.action#_VBPiQsEUEe6yC4BToIaAqA"/>
+        <org.eventb.core.scAction name="0" org.eventb.core.assignment="submit_cc_tx ≔ 0" org.eventb.core.label="act15" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqB|org.eventb.core.action#_VBPiQ8EUEe6yC4BToIaAqA"/>
+    </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="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqC">
         <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/gateway-event-b/CCTx_Abstract_DLT_m1.bcm|org.eventb.core.scMachineFile#CCTx_Abstract_DLT_m1|org.eventb.core.scEvent#received_cross_chain_transactionu" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqC|org.eventb.core.refinesEvent#'"/>
-        <org.eventb.core.scGuard name="'" org.eventb.core.label="grd1;" org.eventb.core.predicate="gateway ↦ source_smart_contract∉subscriptions" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_yQ9vtr7uEe6laZimEYihUg|org.eventb.core.guard#_yQ9vuL7uEe6laZimEYihUg" org.eventb.core.theorem="false"/>
-        <org.eventb.core.scAction name="(" org.eventb.core.assignment="subscriptions ≔ subscriptions∪{gateway ↦ source_smart_contract}" org.eventb.core.label="act1;" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_yQ9vtr7uEe6laZimEYihUg|org.eventb.core.action#_yQ9vt77uEe6laZimEYihUg"/>
-        <org.eventb.core.scAction name=")" org.eventb.core.assignment="subscribed ≔ 1" org.eventb.core.label="act11" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqC|org.eventb.core.action#_VBQJUMEUEe6yC4BToIaAqA"/>
+        <org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="gateway ↦ source_smart_contract∉subscriptions" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_yQ9vtr7uEe6laZimEYihUg|org.eventb.core.guard#_zpDBscQ4Ee609fto5wotHA" org.eventb.core.theorem="false"/>
+        <org.eventb.core.scAction name="(" org.eventb.core.assignment="subscriptions ≔ subscriptions∪{gateway ↦ source_smart_contract}" org.eventb.core.label="act1" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_yQ9vtr7uEe6laZimEYihUg|org.eventb.core.action#_zpDBsMQ4Ee609fto5wotHA"/>
+        <org.eventb.core.scAction name=")" org.eventb.core.assignment="subscribed ≔ 1" org.eventb.core.label="act11" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqC|org.eventb.core.action#_VBQwYMEUEe6yC4BToIaAqA"/>
     </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="INITIATE_CC_TX" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqD">
+    <org.eventb.core.scEvent name="received_cross_chain_transactionv" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="INITIATE_CC_TX" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqD">
         <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/gateway-event-b/CCTx_Abstract_DLT_m1.bcm|org.eventb.core.scMachineFile#CCTx_Abstract_DLT_m1|org.eventb.core.scEvent#received_cross_chain_transactionv" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqD|org.eventb.core.refinesEvent#'"/>
-        <org.eventb.core.scGuard name="'" org.eventb.core.label="grd1;" org.eventb.core.predicate="transaction∈TRANSACTIONS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_y397cMBFEe6yC4BToIaAqA|org.eventb.core.guard#_yQ9vu77uEe6laZimEYihUg" org.eventb.core.theorem="false"/>
-        <org.eventb.core.scGuard name="(" org.eventb.core.label="grd3;" org.eventb.core.predicate="transaction∉received_transactions[{source_smart_contract}]" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_y397cMBFEe6yC4BToIaAqA|org.eventb.core.guard#_yQ9vvL7uEe6laZimEYihUg" org.eventb.core.theorem="false"/>
-        <org.eventb.core.scAction name="transactioo" org.eventb.core.assignment="received_transactions ≔ received_transactions∪{source_smart_contract ↦ transaction}" org.eventb.core.label="act1;" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_y397cMBFEe6yC4BToIaAqA|org.eventb.core.action#_yQ9vur7uEe6laZimEYihUg"/>
+        <org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="transaction∈TRANSACTIONS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_y397cMBFEe6yC4BToIaAqA|org.eventb.core.guard#_zpDowcQ4Ee609fto5wotHA" org.eventb.core.theorem="false"/>
+        <org.eventb.core.scGuard name="(" org.eventb.core.label="grd3" org.eventb.core.predicate="transaction∉received_transactions[{source_smart_contract}]" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_y397cMBFEe6yC4BToIaAqA|org.eventb.core.guard#_zpEP0MQ4Ee609fto5wotHA" org.eventb.core.theorem="false"/>
+        <org.eventb.core.scAction name="transactioo" org.eventb.core.assignment="received_transactions ≔ received_transactions∪{source_smart_contract ↦ transaction}" org.eventb.core.label="act1" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_y397cMBFEe6yC4BToIaAqA|org.eventb.core.action#_zpDowMQ4Ee609fto5wotHA"/>
         <org.eventb.core.scParameter name="transaction" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_y397cMBFEe6yC4BToIaAqA|org.eventb.core.parameter#_yQ9vvb7uEe6laZimEYihUg" org.eventb.core.type="TRANSACTIONS"/>
-        <org.eventb.core.scAction name="transactiop" org.eventb.core.assignment="initiated ≔ 1" org.eventb.core.label="act11" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqD|org.eventb.core.action#_VBQwYMEUEe6yC4BToIaAqA"/>
-        <org.eventb.core.scAction name="transactioq" org.eventb.core.assignment="submit_cc_tx ≔ 0" org.eventb.core.label="act12" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqD|org.eventb.core.action#_VBRXccEUEe6yC4BToIaAqA"/>
+        <org.eventb.core.scAction name="transactiop" org.eventb.core.assignment="initiated ≔ 1" org.eventb.core.label="act11" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqD|org.eventb.core.action#_VBRXcMEUEe6yC4BToIaAqA"/>
+        <org.eventb.core.scAction name="transactioq" org.eventb.core.assignment="submit_cc_tx ≔ 0" org.eventb.core.label="act12" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqD|org.eventb.core.action#_VBR-gcEUEe6yC4BToIaAqA"/>
     </org.eventb.core.scEvent>
-    <org.eventb.core.scEvent name="received_cross_chain_transactionv" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="TRIGGER_CC_TX_EVENT" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqE">
-        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/gateway-event-b/CCTx_Abstract_DLT_m1.bcm|org.eventb.core.scMachineFile#CCTx_Abstract_DLT_m1|org.eventb.core.scEvent#received_cross_chain_transactionw" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqE|org.eventb.core.refinesEvent#'"/>
-        <org.eventb.core.scGuard name="'" org.eventb.core.label="grd1;" org.eventb.core.predicate="source_smart_contract ↦ transaction∈received_transactions" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_E_KKUMBGEe6yC4BToIaAqA|org.eventb.core.guard#_yQ9vwb7uEe6laZimEYihUg" org.eventb.core.theorem="false"/>
-        <org.eventb.core.scGuard name="(" org.eventb.core.label="grd2;" org.eventb.core.predicate="cross_chain_event∉triggered_events[{source_smart_contract}]" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_E_KKUMBGEe6yC4BToIaAqA|org.eventb.core.guard#_yQ9vwr7uEe6laZimEYihUg" org.eventb.core.theorem="false"/>
-        <org.eventb.core.scAction name="cross_chain_evenu" org.eventb.core.assignment="triggered_events ≔ triggered_events∪{source_smart_contract ↦ cross_chain_event}" org.eventb.core.label="act1;" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_E_KKUMBGEe6yC4BToIaAqA|org.eventb.core.action#_yQ9vv77uEe6laZimEYihUg"/>
-        <org.eventb.core.scAction name="cross_chain_evenv" org.eventb.core.assignment="received_transactions ≔ received_transactions ∖ {source_smart_contract ↦ transaction}" org.eventb.core.label="act2;" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_E_KKUMBGEe6yC4BToIaAqA|org.eventb.core.action#_yQ9vwL7uEe6laZimEYihUg"/>
-        <org.eventb.core.scParameter name="cross_chain_event" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_E_KKUMBGEe6yC4BToIaAqA|org.eventb.core.parameter#_yQ9vxL7uEe6laZimEYihUg" org.eventb.core.type="CROSS_CHAIN_EVENTS"/>
-        <org.eventb.core.scParameter name="transaction" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_E_KKUMBGEe6yC4BToIaAqA|org.eventb.core.parameter#_yQ9vw77uEe6laZimEYihUg" org.eventb.core.type="TRANSACTIONS"/>
-        <org.eventb.core.scAction name="cross_chain_evenw" org.eventb.core.assignment="triggered ≔ 1" org.eventb.core.label="act11" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqE|org.eventb.core.action#_VBRXcMEUEe6yC4BToIaAqA"/>
-        <org.eventb.core.scAction name="cross_chain_evenx" org.eventb.core.assignment="initiated ≔ 0" org.eventb.core.label="act12" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqE|org.eventb.core.action#_VBR-gcEUEe6yC4BToIaAqA"/>
-        <org.eventb.core.scAction name="cross_chain_eveny" org.eventb.core.assignment="submit_cc_tx ≔ 0" org.eventb.core.label="act13" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqE|org.eventb.core.action#_kIrbcMEUEe6yC4BToIaAqA"/>
+    <org.eventb.core.scEvent name="received_cross_chain_transactionw" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="EMIT_CC_TX_EVENT" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_RGg0TPKWEe60CqkwWvstGA">
+        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/gateway-event-b/CCTx_Abstract_DLT_m1.bcm|org.eventb.core.scMachineFile#CCTx_Abstract_DLT_m1|org.eventb.core.scEvent#received_cross_chain_transactionw" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_RGg0TPKWEe60CqkwWvstGA|org.eventb.core.refinesEvent#_RGg0TfKWEe60CqkwWvstGA"/>
+        <org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="source_smart_contract ↦ transaction∈received_transactions" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_Pk5swPKVEe60CqkwWvstGA|org.eventb.core.guard#_zpFd8cQ4Ee609fto5wotHA" org.eventb.core.theorem="false"/>
+        <org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="cross_chain_event∉emitted_events[{source_smart_contract}]" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_Pk5swPKVEe60CqkwWvstGA|org.eventb.core.guard#_zpGFAMQ4Ee609fto5wotHA" org.eventb.core.theorem="false"/>
+        <org.eventb.core.scAction name="cross_chain_evenu" org.eventb.core.assignment="emitted_events ≔ emitted_events∪{source_smart_contract ↦ cross_chain_event}" org.eventb.core.label="act1" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_Pk5swPKVEe60CqkwWvstGA|org.eventb.core.action#_zpE24MQ4Ee609fto5wotHA"/>
+        <org.eventb.core.scAction name="cross_chain_evenv" org.eventb.core.assignment="received_transactions ≔ received_transactions ∖ {source_smart_contract ↦ transaction}" org.eventb.core.label="act2" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_Pk5swPKVEe60CqkwWvstGA|org.eventb.core.action#_zpFd8MQ4Ee609fto5wotHA"/>
+        <org.eventb.core.scParameter name="cross_chain_event" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_Pk5swPKVEe60CqkwWvstGA|org.eventb.core.parameter#_yQ9vxL7uEe6laZimEYihUg" org.eventb.core.type="CROSS_CHAIN_EVENTS"/>
+        <org.eventb.core.scParameter name="transaction" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_Pk5swPKVEe60CqkwWvstGA|org.eventb.core.parameter#_yQ9vw77uEe6laZimEYihUg" org.eventb.core.type="TRANSACTIONS"/>
+        <org.eventb.core.scAction name="cross_chain_evenw" org.eventb.core.assignment="emitted ≔ 1" org.eventb.core.label="act11" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_RGg0TPKWEe60CqkwWvstGA|org.eventb.core.action#_VBR-gMEUEe6yC4BToIaAqA"/>
+        <org.eventb.core.scAction name="cross_chain_evenx" org.eventb.core.assignment="initiated ≔ 0" org.eventb.core.label="act12" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_RGg0TPKWEe60CqkwWvstGA|org.eventb.core.action#_VBL34cEUEe6yC4BToIaAqA"/>
+        <org.eventb.core.scAction name="cross_chain_eveny" org.eventb.core.assignment="submit_cc_tx ≔ 0" org.eventb.core.label="act13" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_RGg0TPKWEe60CqkwWvstGA|org.eventb.core.action#_k8Z-cMEUEe6yC4BToIaAqA"/>
     </org.eventb.core.scEvent>
-    <org.eventb.core.scEvent name="received_cross_chain_transactionw" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="LISTEN_CC_TX_EVENT" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqF">
+    <org.eventb.core.scEvent name="received_cross_chain_transactionx" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="LISTEN_CC_TX_EVENT" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqF">
         <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/gateway-event-b/CCTx_Abstract_DLT_m1.bcm|org.eventb.core.scMachineFile#CCTx_Abstract_DLT_m1|org.eventb.core.scEvent#received_cross_chain_transactionx" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqF|org.eventb.core.refinesEvent#'"/>
-        <org.eventb.core.scGuard name="'" org.eventb.core.label="grd1;" org.eventb.core.predicate="source_smart_contract ↦ cross_chain_event∈triggered_events" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_THog4MBGEe6yC4BToIaAqA|org.eventb.core.guard#_yQ9vyL7uEe6laZimEYihUg" org.eventb.core.theorem="false"/>
-        <org.eventb.core.scGuard name="(" org.eventb.core.label="grd2;" org.eventb.core.predicate="gateway ↦ source_smart_contract∈subscriptions" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_THog4MBGEe6yC4BToIaAqA|org.eventb.core.guard#_yQ9vyb7uEe6laZimEYihUg" org.eventb.core.theorem="false"/>
-        <org.eventb.core.scGuard name=")" org.eventb.core.label="grd3;" org.eventb.core.predicate="gateway ↦ cross_chain_transaction∉gateway_pending_transactions" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_THog4MBGEe6yC4BToIaAqA|org.eventb.core.guard#_yQ9vyr7uEe6laZimEYihUg" org.eventb.core.theorem="false"/>
-        <org.eventb.core.scAction name="cross_chain_transactioo" org.eventb.core.assignment="gateway_pending_transactions ≔ gateway_pending_transactions∪{gateway ↦ cross_chain_transaction}" org.eventb.core.label="act1;" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_THog4MBGEe6yC4BToIaAqA|org.eventb.core.action#_yQ9vxr7uEe6laZimEYihUg"/>
-        <org.eventb.core.scAction name="cross_chain_transactiop" org.eventb.core.assignment="triggered_events ≔ triggered_events ∖ {source_smart_contract ↦ cross_chain_event}" org.eventb.core.label="act2;" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_THog4MBGEe6yC4BToIaAqA|org.eventb.core.action#_yQ9vx77uEe6laZimEYihUg"/>
+        <org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="source_smart_contract ↦ cross_chain_event∈emitted_events" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_THog4MBGEe6yC4BToIaAqA|org.eventb.core.guard#_zpHTIcQ4Ee609fto5wotHA" org.eventb.core.theorem="false"/>
+        <org.eventb.core.scGuard name="(" org.eventb.core.label="grd2" org.eventb.core.predicate="gateway ↦ source_smart_contract∈subscriptions" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_THog4MBGEe6yC4BToIaAqA|org.eventb.core.guard#_zpH6MMQ4Ee609fto5wotHA" org.eventb.core.theorem="false"/>
+        <org.eventb.core.scGuard name=")" org.eventb.core.label="grd3" org.eventb.core.predicate="gateway ↦ cross_chain_transaction∉gateway_pending_transactions" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_THog4MBGEe6yC4BToIaAqA|org.eventb.core.guard#_zpH6McQ4Ee609fto5wotHA" org.eventb.core.theorem="false"/>
+        <org.eventb.core.scAction name="cross_chain_transactioo" org.eventb.core.assignment="gateway_pending_transactions ≔ gateway_pending_transactions∪{gateway ↦ cross_chain_transaction}" org.eventb.core.label="act1" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_THog4MBGEe6yC4BToIaAqA|org.eventb.core.action#_zpGsEMQ4Ee609fto5wotHA"/>
+        <org.eventb.core.scAction name="cross_chain_transactiop" org.eventb.core.assignment="emitted_events ≔ emitted_events ∖ {source_smart_contract ↦ cross_chain_event}" org.eventb.core.label="act2" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_THog4MBGEe6yC4BToIaAqA|org.eventb.core.action#_zpHTIMQ4Ee609fto5wotHA"/>
         <org.eventb.core.scParameter name="cross_chain_event" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_THog4MBGEe6yC4BToIaAqA|org.eventb.core.parameter#_yQ9vy77uEe6laZimEYihUg" org.eventb.core.type="CROSS_CHAIN_EVENTS"/>
         <org.eventb.core.scParameter name="cross_chain_transaction" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_THog4MBGEe6yC4BToIaAqA|org.eventb.core.parameter#_yQ9vzL7uEe6laZimEYihUg" org.eventb.core.type="CROSS_CHAIN_TRANSACTIONS"/>
-        <org.eventb.core.scAction name="cross_chain_transactioq" org.eventb.core.assignment="gateway_processing ≔ 1" org.eventb.core.label="act11" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqF|org.eventb.core.action#_VBR-gMEUEe6yC4BToIaAqA"/>
-        <org.eventb.core.scAction name="cross_chain_transactior" org.eventb.core.assignment="triggered ≔ 0" org.eventb.core.label="act12" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqF|org.eventb.core.action#_VBL34cEUEe6yC4BToIaAqA"/>
-        <org.eventb.core.scAction name="cross_chain_transactios" org.eventb.core.assignment="submit_cc_tx ≔ 0" org.eventb.core.label="act13" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqF|org.eventb.core.action#_k8Z-cMEUEe6yC4BToIaAqA"/>
+        <org.eventb.core.scAction name="cross_chain_transactioq" org.eventb.core.assignment="gateway_processing ≔ 1" org.eventb.core.label="act11" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqF|org.eventb.core.action#_VBL34MEUEe6yC4BToIaAqA"/>
+        <org.eventb.core.scAction name="cross_chain_transactior" org.eventb.core.assignment="emitted ≔ 0" org.eventb.core.label="act12" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqF|org.eventb.core.action#_isfxUMEUEe6yC4BToIaAqA"/>
+        <org.eventb.core.scAction name="cross_chain_transactios" org.eventb.core.assignment="submit_cc_tx ≔ 0" org.eventb.core.label="act13" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqF|org.eventb.core.action#_VBPiQcEUEe6yC4BToIaAqA"/>
     </org.eventb.core.scEvent>
-    <org.eventb.core.scEvent name="received_cross_chain_transactionx" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="SUBMIT_CC_TX" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqG">
+    <org.eventb.core.scEvent name="received_cross_chain_transactiony" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="SUBMIT_CC_TX" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqG">
         <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/gateway-event-b/CCTx_Abstract_DLT_m1.bcm|org.eventb.core.scMachineFile#CCTx_Abstract_DLT_m1|org.eventb.core.scEvent#received_cross_chain_transactiony" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqG|org.eventb.core.refinesEvent#'"/>
-        <org.eventb.core.scGuard name="'" org.eventb.core.label="grd1;" org.eventb.core.predicate="gateway ↦ cross_chain_transaction∈gateway_pending_transactions" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_fwqd8MBGEe6yC4BToIaAqA|org.eventb.core.guard#_yREdYr7uEe6laZimEYihUg" org.eventb.core.theorem="false"/>
-        <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="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_fwqd8MBGEe6yC4BToIaAqA|org.eventb.core.action#_yREdYL7uEe6laZimEYihUg"/>
-        <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="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_fwqd8MBGEe6yC4BToIaAqA|org.eventb.core.action#_yREdYb7uEe6laZimEYihUg"/>
+        <org.eventb.core.scGuard name="'" org.eventb.core.label="grd1" org.eventb.core.predicate="gateway ↦ cross_chain_transaction∈gateway_pending_transactions" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_fwqd8MBGEe6yC4BToIaAqA|org.eventb.core.guard#_zpJvYcQ4Ee609fto5wotHA" org.eventb.core.theorem="false"/>
+        <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="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_fwqd8MBGEe6yC4BToIaAqA|org.eventb.core.action#_zpJIUMQ4Ee609fto5wotHA"/>
+        <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="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_fwqd8MBGEe6yC4BToIaAqA|org.eventb.core.action#_zpJvYMQ4Ee609fto5wotHA"/>
         <org.eventb.core.scParameter name="cross_chain_transaction" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#_fwqd8MBGEe6yC4BToIaAqA|org.eventb.core.parameter#_yREdY77uEe6laZimEYihUg" org.eventb.core.type="CROSS_CHAIN_TRANSACTIONS"/>
-        <org.eventb.core.scAction name="cross_chain_transactioq" org.eventb.core.assignment="submit_cc_tx ≔ 1" org.eventb.core.label="act11" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqG|org.eventb.core.action#_VBL34MEUEe6yC4BToIaAqA"/>
-        <org.eventb.core.scAction name="cross_chain_transactior" org.eventb.core.assignment="gateway_processing ≔ 0" org.eventb.core.label="act12" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqG|org.eventb.core.action#_isfxUMEUEe6yC4BToIaAqA"/>
-    </org.eventb.core.scEvent>
-    <org.eventb.core.scEvent name="received_cross_chain_transactiony" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="true" org.eventb.core.label="INITIALISATION" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqB">
-        <org.eventb.core.scRefinesEvent name="'" org.eventb.core.scTarget="/gateway-event-b/CCTx_Abstract_DLT_m1.bcm|org.eventb.core.scMachineFile#CCTx_Abstract_DLT_m1|org.eventb.core.scEvent#received_cross_chain_transactiont" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqB"/>
-        <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="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#'|org.eventb.core.action#_yQ9vsb7uEe6laZimEYihUg"/>
-        <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="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#'|org.eventb.core.action#_yQ9vsr7uEe6laZimEYihUg"/>
-        <org.eventb.core.scAction name=")" org.eventb.core.assignment="subscriptions ≔ ∅ ⦂ ℙ(GATEWAYS×CROSS_CHAIN_SMART_CONTRACTS)" org.eventb.core.label="act3;" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#'|org.eventb.core.action#_yQ9vs77uEe6laZimEYihUg"/>
-        <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="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#'|org.eventb.core.action#_yQ9vtL7uEe6laZimEYihUg"/>
-        <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="/gateway-event-b/CCTx_Abstract_DLT_m1.bum|org.eventb.core.machineFile#CCTx_Abstract_DLT_m1|org.eventb.core.event#'|org.eventb.core.action#_yQ9vtb7uEe6laZimEYihUg"/>
-        <org.eventb.core.scAction name="," org.eventb.core.assignment="subscribed ≔ 0" org.eventb.core.label="act11" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqB|org.eventb.core.action#_VBO7MMEUEe6yC4BToIaAqA"/>
-        <org.eventb.core.scAction name="-" org.eventb.core.assignment="initiated ≔ 0" org.eventb.core.label="act12" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqB|org.eventb.core.action#_VBPiQMEUEe6yC4BToIaAqA"/>
-        <org.eventb.core.scAction name="." org.eventb.core.assignment="triggered ≔ 0" org.eventb.core.label="act13" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqB|org.eventb.core.action#_VBPiQcEUEe6yC4BToIaAqA"/>
-        <org.eventb.core.scAction name="/" org.eventb.core.assignment="gateway_processing ≔ 0" org.eventb.core.label="act14" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqB|org.eventb.core.action#_VBPiQsEUEe6yC4BToIaAqA"/>
-        <org.eventb.core.scAction name="0" org.eventb.core.assignment="submit_cc_tx ≔ 0" org.eventb.core.label="act15" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqB|org.eventb.core.action#_VBPiQ8EUEe6yC4BToIaAqA"/>
+        <org.eventb.core.scAction name="cross_chain_transactioq" org.eventb.core.assignment="submit_cc_tx ≔ 1" org.eventb.core.label="act11" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqG|org.eventb.core.action#_VBO7MMEUEe6yC4BToIaAqA"/>
+        <org.eventb.core.scAction name="cross_chain_transactior" org.eventb.core.assignment="gateway_processing ≔ 0" org.eventb.core.label="act12" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_Animation_m2.bum|org.eventb.core.machineFile#CCTx_Abstract_Animation_m2|org.eventb.core.event#_zZtTYMBBEe6yC4BToIaAqG|org.eventb.core.action#_VBPiQMEUEe6yC4BToIaAqA"/>
     </org.eventb.core.scEvent>
 </org.eventb.core.scMachineFile>

gateway-event-b/CCTx_Abstract_Animation_m2.bps

 <?xml version="1.0" encoding="UTF-8" standalone="no"?>
 <org.eventb.core.psFile>
-    <org.eventb.core.psStatus name="SUBSCRIBE_SMART_CONTRACT_EVENTS/inv11/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="4" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="INITIATE_CC_TX/inv12/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="4" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="INITIATE_CC_TX/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="4" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="TRIGGER_CC_TX_EVENT/inv12/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="4" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="TRIGGER_CC_TX_EVENT/inv13/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="4" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="TRIGGER_CC_TX_EVENT/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="4" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="LISTEN_CC_TX_EVENT/inv13/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="4" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="LISTEN_CC_TX_EVENT/inv14/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="4" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="LISTEN_CC_TX_EVENT/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="4" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="SUBMIT_CC_TX/inv14/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="4" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="SUBMIT_CC_TX/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="4" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="INITIALISATION/inv11/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="4" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="INITIALISATION/inv12/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="4" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="INITIALISATION/inv13/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="4" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="INITIALISATION/inv14/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="4" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="INITIALISATION/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="4" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="SUBSCRIBE_SMART_CONTRACT_EVENTS/inv11/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="INITIATE_CC_TX/inv12/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="INITIATE_CC_TX/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="SUBMIT_CC_TX/inv14/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="SUBMIT_CC_TX/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="7" org.eventb.core.psManual="false"/>
 </org.eventb.core.psFile>

gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bpr

@@ -861,4 +861,154 @@
         <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.trueGoal"/>
     </org.eventb.core.prProof>
+    <org.eventb.core.prProof name="EMIT_CC_TX_EVENT_IN_ETHEREUM/inv12/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
+        <org.eventb.core.lang name="L"/>
+        <org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="Partition rewrites in hyp (partition(PERMISSIONS,{read},{write}))" org.eventb.core.prHyps="">
+            <org.eventb.core.prAnte name="'">
+                <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p1" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p2,p3"/>
+                <org.eventb.core.prHypAction name="SELECT1" org.eventb.core.prHyps="p2,p3"/>
+                <org.eventb.core.prRule name="r1" 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="p6">
+                        <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p4" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p5"/>
+                        <org.eventb.core.prRule name="r2" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p6" org.eventb.core.prHyps=""/>
+                    </org.eventb.core.prAnte>
+                </org.eventb.core.prRule>
+            </org.eventb.core.prAnte>
+            <org.eventb.core.prString name=".pos" org.eventb.core.prSValue=""/>
+        </org.eventb.core.prRule>
+        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="¬read=write">
+            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
+            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
+            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p6" org.eventb.core.predicate="⊤"/>
+        <org.eventb.core.prPred name="p4" org.eventb.core.predicate="cross_chain_event∉emitted_events[{source_smart_contract}]">
+            <org.eventb.core.prIdent name="CROSS_CHAIN_EVENTS" org.eventb.core.type="ℙ(CROSS_CHAIN_EVENTS)"/>
+            <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
+            <org.eventb.core.prIdent name="cross_chain_event" org.eventb.core.type="CROSS_CHAIN_EVENTS"/>
+            <org.eventb.core.prIdent name="emitted_events" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_EVENTS)"/>
+            <org.eventb.core.prIdent name="source_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p5" org.eventb.core.predicate="¬cross_chain_event∈emitted_events[{source_smart_contract}]">
+            <org.eventb.core.prIdent name="CROSS_CHAIN_EVENTS" org.eventb.core.type="ℙ(CROSS_CHAIN_EVENTS)"/>
+            <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
+            <org.eventb.core.prIdent name="cross_chain_event" org.eventb.core.type="CROSS_CHAIN_EVENTS"/>
+            <org.eventb.core.prIdent name="emitted_events" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_EVENTS)"/>
+            <org.eventb.core.prIdent name="source_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="partition(PERMISSIONS,{read},{write})">
+            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
+            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
+            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="0∈{0,1}"/>
+        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="PERMISSIONS={read,write}">
+            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
+            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
+            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.partitionRewrites"/>
+        <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.prProof>
+    <org.eventb.core.prProof name="EMIT_CC_TX_EVENT_IN_ETHEREUM/inv13/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
+        <org.eventb.core.lang name="L"/>
+        <org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="Partition rewrites in hyp (partition(PERMISSIONS,{read},{write}))" org.eventb.core.prHyps="">
+            <org.eventb.core.prAnte name="'">
+                <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p1" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p2,p3"/>
+                <org.eventb.core.prHypAction name="SELECT1" org.eventb.core.prHyps="p2,p3"/>
+                <org.eventb.core.prRule name="r1" 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="p6">
+                        <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p4" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p5"/>
+                        <org.eventb.core.prRule name="r2" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p6" org.eventb.core.prHyps=""/>
+                    </org.eventb.core.prAnte>
+                </org.eventb.core.prRule>
+            </org.eventb.core.prAnte>
+            <org.eventb.core.prString name=".pos" org.eventb.core.prSValue=""/>
+        </org.eventb.core.prRule>
+        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="¬read=write">
+            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
+            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
+            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p6" org.eventb.core.predicate="⊤"/>
+        <org.eventb.core.prPred name="p4" org.eventb.core.predicate="cross_chain_event∉emitted_events[{source_smart_contract}]">
+            <org.eventb.core.prIdent name="CROSS_CHAIN_EVENTS" org.eventb.core.type="ℙ(CROSS_CHAIN_EVENTS)"/>
+            <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
+            <org.eventb.core.prIdent name="cross_chain_event" org.eventb.core.type="CROSS_CHAIN_EVENTS"/>
+            <org.eventb.core.prIdent name="emitted_events" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_EVENTS)"/>
+            <org.eventb.core.prIdent name="source_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p5" org.eventb.core.predicate="¬cross_chain_event∈emitted_events[{source_smart_contract}]">
+            <org.eventb.core.prIdent name="CROSS_CHAIN_EVENTS" org.eventb.core.type="ℙ(CROSS_CHAIN_EVENTS)"/>
+            <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
+            <org.eventb.core.prIdent name="cross_chain_event" org.eventb.core.type="CROSS_CHAIN_EVENTS"/>
+            <org.eventb.core.prIdent name="emitted_events" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_EVENTS)"/>
+            <org.eventb.core.prIdent name="source_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="partition(PERMISSIONS,{read},{write})">
+            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
+            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
+            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="1∈{0,1}"/>
+        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="PERMISSIONS={read,write}">
+            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
+            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
+            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.partitionRewrites"/>
+        <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.prProof>
+    <org.eventb.core.prProof name="EMIT_CC_TX_EVENT_IN_ETHEREUM/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
+        <org.eventb.core.lang name="L"/>
+        <org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="Partition rewrites in hyp (partition(PERMISSIONS,{read},{write}))" org.eventb.core.prHyps="">
+            <org.eventb.core.prAnte name="'">
+                <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p1" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p2,p3"/>
+                <org.eventb.core.prHypAction name="SELECT1" org.eventb.core.prHyps="p2,p3"/>
+                <org.eventb.core.prRule name="r1" 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="p6">
+                        <org.eventb.core.prHypAction name="REWRITE0" org.eventb.core.prHidden="p4" org.eventb.core.prHyps="" org.eventb.core.prInfHyps="p5"/>
+                        <org.eventb.core.prRule name="r2" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="⊤ goal" org.eventb.core.prGoal="p6" org.eventb.core.prHyps=""/>
+                    </org.eventb.core.prAnte>
+                </org.eventb.core.prRule>
+            </org.eventb.core.prAnte>
+            <org.eventb.core.prString name=".pos" org.eventb.core.prSValue=""/>
+        </org.eventb.core.prRule>
+        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="¬read=write">
+            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
+            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
+            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p6" org.eventb.core.predicate="⊤"/>
+        <org.eventb.core.prPred name="p4" org.eventb.core.predicate="cross_chain_event∉emitted_events[{source_smart_contract}]">
+            <org.eventb.core.prIdent name="CROSS_CHAIN_EVENTS" org.eventb.core.type="ℙ(CROSS_CHAIN_EVENTS)"/>
+            <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
+            <org.eventb.core.prIdent name="cross_chain_event" org.eventb.core.type="CROSS_CHAIN_EVENTS"/>
+            <org.eventb.core.prIdent name="emitted_events" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_EVENTS)"/>
+            <org.eventb.core.prIdent name="source_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p5" org.eventb.core.predicate="¬cross_chain_event∈emitted_events[{source_smart_contract}]">
+            <org.eventb.core.prIdent name="CROSS_CHAIN_EVENTS" org.eventb.core.type="ℙ(CROSS_CHAIN_EVENTS)"/>
+            <org.eventb.core.prIdent name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
+            <org.eventb.core.prIdent name="cross_chain_event" org.eventb.core.type="CROSS_CHAIN_EVENTS"/>
+            <org.eventb.core.prIdent name="emitted_events" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS×CROSS_CHAIN_EVENTS)"/>
+            <org.eventb.core.prIdent name="source_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="partition(PERMISSIONS,{read},{write})">
+            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
+            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
+            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="0∈{0,1}"/>
+        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="PERMISSIONS={read,write}">
+            <org.eventb.core.prIdent name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/>
+            <org.eventb.core.prIdent name="read" org.eventb.core.type="PERMISSIONS"/>
+            <org.eventb.core.prIdent name="write" org.eventb.core.type="PERMISSIONS"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.partitionRewrites"/>
+        <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.prProof>
 </org.eventb.core.prFile>

gateway-event-b/CCTx_Ethereum_Fabric_Animation_m3.bps

 <?xml version="1.0" encoding="UTF-8" standalone="no"?>
 <org.eventb.core.psFile>
-    <org.eventb.core.psStatus name="INITIALISATION/inv11/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="INITIALISATION/inv12/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="INITIALISATION/inv13/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="INITIALISATION/inv14/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="INITIALISATION/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="INITIALISATION/inv16/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="INITIALISATION/inv17/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="SUBSCRIBE_SMART_CONTRACT_EVENTS_IN_ETHEREUM/inv11/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="INITIATE_CC_TX_IN_ETHEREUM/inv12/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="INITIATE_CC_TX_IN_ETHEREUM/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="TRIGGER_CC_TX_EVENT_IN_ETHEREUM/inv12/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="TRIGGER_CC_TX_EVENT_IN_ETHEREUM/inv13/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="TRIGGER_CC_TX_EVENT_IN_ETHEREUM/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="LISTEN_CC_TX_EVENT_IN_ETHEREUM/inv13/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="LISTEN_CC_TX_EVENT_IN_ETHEREUM/inv14/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="LISTEN_CC_TX_EVENT_IN_ETHEREUM/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="SUBMIT_CC_TX_TO_FABRIC/inv14/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="SUBMIT_CC_TX_TO_FABRIC/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="CREATE_GATEWAY_USER/inv16/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="GRANT_PERMISSION/inv17/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="0" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="INITIALISATION/inv11/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="INITIALISATION/inv12/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="INITIALISATION/inv13/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="INITIALISATION/inv14/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="INITIALISATION/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="INITIALISATION/inv16/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="INITIALISATION/inv17/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="SUBSCRIBE_SMART_CONTRACT_EVENTS_IN_ETHEREUM/inv11/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="INITIATE_CC_TX_IN_ETHEREUM/inv12/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="INITIATE_CC_TX_IN_ETHEREUM/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="EMIT_CC_TX_EVENT_IN_ETHEREUM/inv12/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="EMIT_CC_TX_EVENT_IN_ETHEREUM/inv13/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="EMIT_CC_TX_EVENT_IN_ETHEREUM/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="LISTEN_CC_TX_EVENT_IN_ETHEREUM/inv13/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="LISTEN_CC_TX_EVENT_IN_ETHEREUM/inv14/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="LISTEN_CC_TX_EVENT_IN_ETHEREUM/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="SUBMIT_CC_TX_TO_FABRIC/inv14/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="SUBMIT_CC_TX_TO_FABRIC/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="CREATE_GATEWAY_USER/inv16/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="GRANT_PERMISSION/inv17/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="5" org.eventb.core.psManual="false"/>
 </org.eventb.core.psFile>

gateway-event-b/CCTx_Ethereum_Fabric_c2.bcc

@@ -14,8 +14,8 @@
         <org.eventb.core.scCarrierSet name="TRANSACTIONS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_c1.buc|org.eventb.core.contextFile#CCTx_Abstract_DLT_c1|org.eventb.core.carrierSet#_lhTmNL7uEe6laZimEYihUg" org.eventb.core.type="ℙ(TRANSACTIONS)"/>
         <org.eventb.core.scCarrierSet name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_c1.buc|org.eventb.core.contextFile#CCTx_Abstract_DLT_c1|org.eventb.core.carrierSet#_lhTmNb7uEe6laZimEYihUg" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/>
     </org.eventb.core.scInternalContext>
-    <org.eventb.core.scAxiom name="CCTx_Abstract_DLT_c2" org.eventb.core.label="axm11;" org.eventb.core.predicate="partition(PERMISSIONS,{read},{write})" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_c2.buc|org.eventb.core.contextFile#CCTx_Ethereum_Fabric_c2|org.eventb.core.axiom#_olcsoL7uEe6laZimEYihUg" org.eventb.core.theorem="false"/>
-    <org.eventb.core.scAxiom name="CCTx_Abstract_DLT_c3" org.eventb.core.label="axm12;" org.eventb.core.predicate="gateway_user∈USERS" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_c2.buc|org.eventb.core.contextFile#CCTx_Ethereum_Fabric_c2|org.eventb.core.axiom#_olcsob7uEe6laZimEYihUg" org.eventb.core.theorem="false"/>
+    <org.eventb.core.scAxiom name="CCTx_Abstract_DLT_c2" org.eventb.core.label="axm11" org.eventb.core.predicate="partition(PERMISSIONS,{read},{write})" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_c2.buc|org.eventb.core.contextFile#CCTx_Ethereum_Fabric_c2|org.eventb.core.axiom#_c2chsMQ6Ee609fto5wotHA" org.eventb.core.theorem="false"/>
+    <org.eventb.core.scAxiom name="CCTx_Abstract_DLT_c3" org.eventb.core.label="axm12" org.eventb.core.predicate="gateway_user∈USERS" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_c2.buc|org.eventb.core.contextFile#CCTx_Ethereum_Fabric_c2|org.eventb.core.axiom#_c2dIwMQ6Ee609fto5wotHA" org.eventb.core.theorem="false"/>
     <org.eventb.core.scConstant name="write" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_c2.buc|org.eventb.core.contextFile#CCTx_Ethereum_Fabric_c2|org.eventb.core.constant#_olcso77uEe6laZimEYihUg" org.eventb.core.type="PERMISSIONS"/>
     <org.eventb.core.scCarrierSet name="USERS" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_c2.buc|org.eventb.core.contextFile#CCTx_Ethereum_Fabric_c2|org.eventb.core.carrierSet#_olcspr7uEe6laZimEYihUg" org.eventb.core.type="ℙ(USERS)"/>
     <org.eventb.core.scConstant name="read" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_c2.buc|org.eventb.core.contextFile#CCTx_Ethereum_Fabric_c2|org.eventb.core.constant#_olcsor7uEe6laZimEYihUg" org.eventb.core.type="PERMISSIONS"/>

gateway-event-b/CCTx_Ethereum_Fabric_c2.bpo

 <?xml version="1.0" encoding="UTF-8" standalone="no"?>
-<org.eventb.core.poFile org.eventb.core.poStamp="4">
+<org.eventb.core.poFile org.eventb.core.poStamp="5">
     <org.eventb.core.poPredicateSet name="ABSHYP" org.eventb.core.poStamp="4">
         <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)"/>
@@ -18,8 +18,8 @@
         <org.eventb.core.poIdentifier name="read" org.eventb.core.type="PERMISSIONS"/>
         <org.eventb.core.poIdentifier name="gateway_user" org.eventb.core.type="USERS"/>
     </org.eventb.core.poPredicateSet>
-    <org.eventb.core.poPredicateSet name="ALLHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_c2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_c2|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poStamp="4">
-        <org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="partition(PERMISSIONS,{read},{write})" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_c2.buc|org.eventb.core.contextFile#CCTx_Ethereum_Fabric_c2|org.eventb.core.axiom#_olcsoL7uEe6laZimEYihUg"/>
-        <org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="gateway_user∈USERS" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_c2.buc|org.eventb.core.contextFile#CCTx_Ethereum_Fabric_c2|org.eventb.core.axiom#_olcsob7uEe6laZimEYihUg"/>
+    <org.eventb.core.poPredicateSet name="ALLHYP" org.eventb.core.parentSet="/gateway-event-b/CCTx_Ethereum_Fabric_c2.bpo|org.eventb.core.poFile#CCTx_Ethereum_Fabric_c2|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poStamp="5">
+        <org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="partition(PERMISSIONS,{read},{write})" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_c2.buc|org.eventb.core.contextFile#CCTx_Ethereum_Fabric_c2|org.eventb.core.axiom#_c2chsMQ6Ee609fto5wotHA"/>
+        <org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="gateway_user∈USERS" org.eventb.core.source="/gateway-event-b/CCTx_Ethereum_Fabric_c2.buc|org.eventb.core.contextFile#CCTx_Ethereum_Fabric_c2|org.eventb.core.axiom#_c2dIwMQ6Ee609fto5wotHA"/>
     </org.eventb.core.poPredicateSet>
 </org.eventb.core.poFile>

gateway-event-b/CCTx_Ethereum_Fabric_c2.buc

 <?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="_olS7p77uEe6laZimEYihUg" org.eventb.texttools.text_lastmodified="1706564263002" org.eventb.texttools.text_representation="context CCTx_Ethereum_Fabric_c2 extends CCTx_Abstract_DLT_c1&#10;&#10;sets PERMISSIONS USERS&#10;&#10;constants read write gateway_user&#10;&#10;axioms&#10;  @axm11; partition(PERMISSIONS, {read}, {write}) // Two only type of permissions exist: read and write&#10;  @axm12; gateway_user ∈ USERS // The gateway has an Hyperledger Fabric user&#10;end" 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="_c2YQRcQ6Ee609fto5wotHA" org.eventb.texttools.text_lastmodified="1707146581829" org.eventb.texttools.text_representation="context CCTx_Ethereum_Fabric_c2 extends CCTx_Abstract_DLT_c1&#10;&#10;sets PERMISSIONS USERS&#10;&#10;constants read write gateway_user&#10;&#10;axioms&#10;  @axm11 partition(PERMISSIONS, {read}, {write}) // Two only types of permissions exist: read and write&#10;  @axm12 gateway_user ∈ USERS // The gateway has an Hyperledger Fabric user&#10;end" version="3">
     <org.eventb.core.extendsContext name="'" org.eventb.core.target="CCTx_Abstract_DLT_c1"/>
-    <org.eventb.core.axiom name="_olcsoL7uEe6laZimEYihUg" org.eventb.core.comment="Two only type of permissions exist: read and write" org.eventb.core.generated="false" org.eventb.core.label="axm11;" org.eventb.core.predicate="partition(PERMISSIONS, {read}, {write})" org.eventb.emf.persistence.emf_id="_olS7pb7uEe6laZimEYihUg"/>
-    <org.eventb.core.axiom name="_olcsob7uEe6laZimEYihUg" org.eventb.core.comment="The gateway has an Hyperledger Fabric user" org.eventb.core.generated="false" org.eventb.core.label="axm12;" org.eventb.core.predicate="gateway_user ∈ USERS" org.eventb.emf.persistence.emf_id="_olS7pr7uEe6laZimEYihUg"/>
-    <org.eventb.core.constant name="_olcsor7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="read" org.eventb.emf.persistence.emf_id="_olS7or7uEe6laZimEYihUg"/>
-    <org.eventb.core.constant name="_olcso77uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="write" org.eventb.emf.persistence.emf_id="_olS7o77uEe6laZimEYihUg"/>
-    <org.eventb.core.constant name="_olcspL7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="gateway_user" org.eventb.emf.persistence.emf_id="_olS7pL7uEe6laZimEYihUg"/>
-    <org.eventb.core.carrierSet name="_olcspb7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="PERMISSIONS" org.eventb.emf.persistence.emf_id="_olS7oL7uEe6laZimEYihUg"/>
-    <org.eventb.core.carrierSet name="_olcspr7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="USERS" org.eventb.emf.persistence.emf_id="_olS7ob7uEe6laZimEYihUg"/>
+    <org.eventb.core.axiom name="_c2chsMQ6Ee609fto5wotHA" org.eventb.core.comment="Two only types of permissions exist: read and write" org.eventb.core.generated="false" org.eventb.core.label="axm11" org.eventb.core.predicate="partition(PERMISSIONS, {read}, {write})" org.eventb.emf.persistence.emf_id="_c2YQQ8Q6Ee609fto5wotHA"/>
+    <org.eventb.core.axiom name="_c2dIwMQ6Ee609fto5wotHA" org.eventb.core.comment="The gateway has an Hyperledger Fabric user" org.eventb.core.generated="false" org.eventb.core.label="axm12" org.eventb.core.predicate="gateway_user ∈ USERS" org.eventb.emf.persistence.emf_id="_c2YQRMQ6Ee609fto5wotHA"/>
+    <org.eventb.core.constant name="_olcsor7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="read" org.eventb.emf.persistence.emf_id="_c2YQQMQ6Ee609fto5wotHA"/>
+    <org.eventb.core.constant name="_olcso77uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="write" org.eventb.emf.persistence.emf_id="_c2YQQcQ6Ee609fto5wotHA"/>
+    <org.eventb.core.constant name="_olcspL7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="gateway_user" org.eventb.emf.persistence.emf_id="_c2YQQsQ6Ee609fto5wotHA"/>
+    <org.eventb.core.carrierSet name="_olcspb7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="PERMISSIONS" org.eventb.emf.persistence.emf_id="_c2XpMMQ6Ee609fto5wotHA"/>
+    <org.eventb.core.carrierSet name="_olcspr7uEe6laZimEYihUg" org.eventb.core.generated="false" org.eventb.core.identifier="USERS" org.eventb.emf.persistence.emf_id="_c2XpMcQ6Ee609fto5wotHA"/>
 </org.eventb.core.contextFile>

gateway-event-b/CCTx_Ethereum_Fabric_m2.bps

 <?xml version="1.0" encoding="UTF-8" standalone="no"?>
 <org.eventb.core.psFile>
-    <org.eventb.core.psStatus name="INITIALISATION/inv12/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="26" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="INITIALISATION/inv13/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="26" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="INITIALISATION/inv14/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="28" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="INITIALISATION/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="28" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="SUBMIT_CC_TX_TO_FABRIC/inv12/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="28" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="SUBMIT_CC_TX_TO_FABRIC/inv13/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="28" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="SUBMIT_CC_TX_TO_FABRIC/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="28" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="CREATE_GATEWAY_USER/inv12/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="28" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="CREATE_GATEWAY_USER/inv13/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="28" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="CREATE_GATEWAY_USER/inv14/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="28" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="GRANT_PERMISSION/inv14/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="29" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="GRANT_PERMISSION/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="29" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="SUBMIT_CC_TX_TO_FABRIC/inv12/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="33" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="SUBMIT_CC_TX_TO_FABRIC/inv13/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="33" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="SUBMIT_CC_TX_TO_FABRIC/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="33" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="CREATE_GATEWAY_USER/inv12/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="33" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="CREATE_GATEWAY_USER/inv13/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="33" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="CREATE_GATEWAY_USER/inv14/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="33" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="GRANT_PERMISSION/inv14/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="33" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="GRANT_PERMISSION/inv15/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="33" org.eventb.core.psManual="false"/>
 </org.eventb.core.psFile>