<?xml version="1.0" encoding="UTF-8" standalone="no"?> <org.eventb.core.poFile org.eventb.core.poStamp="7"> <org.eventb.core.poPredicateSet name="ABSHYP" org.eventb.core.poStamp="7"> <org.eventb.core.poIdentifier name="TARGET_TRANSACTIONS" org.eventb.core.type="ℙ(TARGET_TRANSACTIONS)"/> <org.eventb.core.poIdentifier name="GATEWAYS" org.eventb.core.type="ℙ(GATEWAYS)"/> <org.eventb.core.poIdentifier name="SOURCE_TRANSACTIONS" org.eventb.core.type="ℙ(SOURCE_TRANSACTIONS)"/> <org.eventb.core.poIdentifier name="SMART_CONTRACT_EVENTS" org.eventb.core.type="ℙ(SMART_CONTRACT_EVENTS)"/> <org.eventb.core.poIdentifier name="CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.type="ℙ(CROSS_CHAIN_SMART_CONTRACTS)"/> <org.eventb.core.poIdentifier name="source_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/> <org.eventb.core.poIdentifier name="gateway" org.eventb.core.type="GATEWAYS"/> <org.eventb.core.poIdentifier name="target_smart_contract" org.eventb.core.type="CROSS_CHAIN_SMART_CONTRACTS"/> <org.eventb.core.poPredicate name="CROSS_CHAIN_SMART_CONTRACTT" org.eventb.core.predicate="source_smart_contract∈CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_c1.buc|org.eventb.core.contextFile#CCTx_Abstract_DLT_c1|org.eventb.core.axiom#_lhKcab7uEe6laZimEYihUg"/> <org.eventb.core.poPredicate name="CROSS_CHAIN_SMART_CONTRACTU" org.eventb.core.predicate="target_smart_contract∈CROSS_CHAIN_SMART_CONTRACTS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_c1.buc|org.eventb.core.contextFile#CCTx_Abstract_DLT_c1|org.eventb.core.axiom#_lhKcar7uEe6laZimEYihUg"/> <org.eventb.core.poPredicate name="CROSS_CHAIN_SMART_CONTRACTV" org.eventb.core.predicate="gateway∈GATEWAYS" org.eventb.core.source="/gateway-event-b/CCTx_Abstract_DLT_c1.buc|org.eventb.core.contextFile#CCTx_Abstract_DLT_c1|org.eventb.core.axiom#_lhKca77uEe6laZimEYihUg"/> <org.eventb.core.poIdentifier name="USERS" org.eventb.core.type="ℙ(USERS)"/> <org.eventb.core.poIdentifier name="PERMISSIONS" org.eventb.core.type="ℙ(PERMISSIONS)"/> <org.eventb.core.poIdentifier name="write" org.eventb.core.type="PERMISSIONS"/> <org.eventb.core.poIdentifier name="read" org.eventb.core.type="PERMISSIONS"/> <org.eventb.core.poIdentifier name="gateway_user" org.eventb.core.type="USERS"/> </org.eventb.core.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="7"> <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>