diff --git a/UserManagement/UserMachine.bcm b/UserManagement/UserMachine.bcm
index bf4e27961458207d229f8b7f82c20d2d8a74cb61..ed0efcb7adfd28097d8354a0e4b684a063f7ed50 100644
--- a/UserManagement/UserMachine.bcm
+++ b/UserManagement/UserMachine.bcm
@@ -1,63 +1,99 @@
 <?xml version="1.0" encoding="UTF-8" standalone="no"?>
 <org.eventb.core.scMachineFile org.eventb.core.accurate="true" org.eventb.core.configuration="org.eventb.core.fwd;ac.soton.xeventb.xmachine.base">
-    <org.eventb.core.scSeesContext name="'" org.eventb.core.scTarget="/UserManagement/UserContext.bcc" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.seesContext#_8y5v0AldEe-O984l8O-k1g"/>
+    <org.eventb.core.scSeesContext name="'" org.eventb.core.scTarget="/UserManagement/UserContext.bcc" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.seesContext#_Qg7ZUArBEe-O984l8O-k1g"/>
     <org.eventb.core.scInternalContext name="UserContext">
         <org.eventb.core.scCarrierSet name="USER" org.eventb.core.source="/UserManagement/UserContext.buc|org.eventb.core.contextFile#UserContext|org.eventb.core.carrierSet#_5NRswAk4Ee-O984l8O-k1g" org.eventb.core.type="ℙ(USER)"/>
         <org.eventb.core.scCarrierSet name="PASSWORD" org.eventb.core.source="/UserManagement/UserContext.buc|org.eventb.core.contextFile#UserContext|org.eventb.core.carrierSet#_5NRswQk4Ee-O984l8O-k1g" org.eventb.core.type="ℙ(PASSWORD)"/>
     </org.eventb.core.scInternalContext>
-    <org.eventb.core.scInvariant name="UserContexu" org.eventb.core.label="inv0" org.eventb.core.predicate="admin∈USER ⇸ PASSWORD" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_8y6W4QldEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
-    <org.eventb.core.scInvariant name="UserContexv" org.eventb.core.label="inv1" org.eventb.core.predicate="dentist∈USER ⇸ PASSWORD" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_8y6W4gldEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
-    <org.eventb.core.scInvariant name="UserContexw" org.eventb.core.label="inv2" org.eventb.core.predicate="patient∈USER ⇸ PASSWORD" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_8y6W4wldEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
-    <org.eventb.core.scInvariant name="UserContexx" org.eventb.core.label="inv3" org.eventb.core.predicate="dom(admin)⊆USER" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_8y6W5AldEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
-    <org.eventb.core.scInvariant name="UserContexy" org.eventb.core.label="inv4" org.eventb.core.predicate="dom(dentist)⊆USER" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_8y6W5QldEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
-    <org.eventb.core.scInvariant name="UserContexz" org.eventb.core.label="inv5" org.eventb.core.predicate="dom(patient)⊆USER" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_8y6W5gldEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
-    <org.eventb.core.scInvariant name="UserContex{" org.eventb.core.label="inv6" org.eventb.core.predicate="admin∩dentist∩patient=(∅ ⦂ ℙ(USER×PASSWORD))" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_8y6W5wldEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
-    <org.eventb.core.scInvariant name="UserContex|" org.eventb.core.label="inv7" org.eventb.core.predicate="registered=admin∪dentist∪patient" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_8y6W6AldEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
-    <org.eventb.core.scInvariant name="UserContex}" org.eventb.core.label="inv8" org.eventb.core.predicate="loggedin⊆registered" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_8y698AldEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
-    <org.eventb.core.scVariable name="loggedin" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.variable#_8y5v1AldEe-O984l8O-k1g" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
-    <org.eventb.core.scVariable name="patient" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.variable#_8y5v0wldEe-O984l8O-k1g" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
-    <org.eventb.core.scVariable name="dentist" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.variable#_8y5v0gldEe-O984l8O-k1g" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
-    <org.eventb.core.scVariable name="registered" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.variable#_8y6W4AldEe-O984l8O-k1g" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
-    <org.eventb.core.scVariable name="admin" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.variable#_8y5v0QldEe-O984l8O-k1g" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
-    <org.eventb.core.scEvent name="UserContex~" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="INITIALISATION" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y698QldEe-O984l8O-k1g">
-        <org.eventb.core.scAction name="'" org.eventb.core.assignment="admin ≔ ∅ ⦂ ℙ(USER×PASSWORD)" org.eventb.core.label="act0" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y698QldEe-O984l8O-k1g|org.eventb.core.action#_8y698gldEe-O984l8O-k1g"/>
-        <org.eventb.core.scAction name="(" org.eventb.core.assignment="dentist ≔ ∅ ⦂ ℙ(USER×PASSWORD)" org.eventb.core.label="act1" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y698QldEe-O984l8O-k1g|org.eventb.core.action#_8y698wldEe-O984l8O-k1g"/>
-        <org.eventb.core.scAction name=")" org.eventb.core.assignment="patient ≔ ∅ ⦂ ℙ(USER×PASSWORD)" org.eventb.core.label="act2" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y698QldEe-O984l8O-k1g|org.eventb.core.action#_8y699AldEe-O984l8O-k1g"/>
-        <org.eventb.core.scAction name="*" org.eventb.core.assignment="loggedin ≔ ∅ ⦂ ℙ(USER×PASSWORD)" org.eventb.core.label="act3" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y698QldEe-O984l8O-k1g|org.eventb.core.action#_8y699QldEe-O984l8O-k1g"/>
-        <org.eventb.core.scAction name="+" org.eventb.core.assignment="registered ≔ ∅ ⦂ ℙ(USER×PASSWORD)" org.eventb.core.label="act4" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y698QldEe-O984l8O-k1g|org.eventb.core.action#_8y699gldEe-O984l8O-k1g"/>
-    </org.eventb.core.scEvent>
-    <org.eventb.core.scEvent name="UserContey'" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="setRootAdmins" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y699wldEe-O984l8O-k1g">
-        <org.eventb.core.scGuard name="'" org.eventb.core.label="grd0" org.eventb.core.predicate="root∈USER" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y699wldEe-O984l8O-k1g|org.eventb.core.guard#_8y69-gldEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
-        <org.eventb.core.scGuard name="(" org.eventb.core.label="grd1" org.eventb.core.predicate="root_password∈PASSWORD" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y699wldEe-O984l8O-k1g|org.eventb.core.guard#_8y7lAAldEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
-        <org.eventb.core.scGuard name=")" org.eventb.core.label="grd2" org.eventb.core.predicate="admin=(∅ ⦂ ℙ(USER×PASSWORD))" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y699wldEe-O984l8O-k1g|org.eventb.core.guard#_8y7lAQldEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
-        <org.eventb.core.scParameter name="root_password" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y699wldEe-O984l8O-k1g|org.eventb.core.parameter#_8y69-QldEe-O984l8O-k1g" org.eventb.core.type="PASSWORD"/>
-        <org.eventb.core.scParameter name="root" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y699wldEe-O984l8O-k1g|org.eventb.core.parameter#_8y69-AldEe-O984l8O-k1g" org.eventb.core.type="USER"/>
-        <org.eventb.core.scAction name="root_passwore" org.eventb.core.assignment="admin ≔ {root ↦ root_password}" org.eventb.core.label="act0" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y699wldEe-O984l8O-k1g|org.eventb.core.action#_8y7lAgldEe-O984l8O-k1g"/>
-        <org.eventb.core.scAction name="root_passworf" org.eventb.core.assignment="registered ≔ {root ↦ root_password}" org.eventb.core.label="act1" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y699wldEe-O984l8O-k1g|org.eventb.core.action#_8y7lAwldEe-O984l8O-k1g"/>
-    </org.eventb.core.scEvent>
-    <org.eventb.core.scEvent name="UserContey(" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="registerNewPatient" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y7lBAldEe-O984l8O-k1g">
-        <org.eventb.core.scGuard name="'" org.eventb.core.label="grd0" org.eventb.core.predicate="new_patient∈USER" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y7lBAldEe-O984l8O-k1g|org.eventb.core.guard#_8y7lBwldEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
-        <org.eventb.core.scGuard name="(" org.eventb.core.label="grd1" org.eventb.core.predicate="new_patient_password∈PASSWORD" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y7lBAldEe-O984l8O-k1g|org.eventb.core.guard#_8y7lCAldEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
-        <org.eventb.core.scGuard name=")" org.eventb.core.label="grd2" org.eventb.core.predicate="new_patient∉dom(registered)" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y7lBAldEe-O984l8O-k1g|org.eventb.core.guard#_8y7lCQldEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
-        <org.eventb.core.scGuard name="*" org.eventb.core.label="grd3" org.eventb.core.predicate="card(admin)&gt;0" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y7lBAldEe-O984l8O-k1g|org.eventb.core.guard#_8y7lCgldEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
-        <org.eventb.core.scParameter name="new_patient_password" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y7lBAldEe-O984l8O-k1g|org.eventb.core.parameter#_8y7lBgldEe-O984l8O-k1g" org.eventb.core.type="PASSWORD"/>
-        <org.eventb.core.scParameter name="new_patient" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y7lBAldEe-O984l8O-k1g|org.eventb.core.parameter#_8y7lBQldEe-O984l8O-k1g" org.eventb.core.type="USER"/>
-        <org.eventb.core.scAction name="new_patient_passwore" org.eventb.core.assignment="patient ≔ patient∪{new_patient ↦ new_patient_password}" org.eventb.core.label="act1" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y7lBAldEe-O984l8O-k1g|org.eventb.core.action#_8y7lCwldEe-O984l8O-k1g"/>
-        <org.eventb.core.scAction name="new_patient_passworf" org.eventb.core.assignment="registered ≔ registered∪{new_patient ↦ new_patient_password}" org.eventb.core.label="act2" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y7lBAldEe-O984l8O-k1g|org.eventb.core.action#_8y7lDAldEe-O984l8O-k1g"/>
-    </org.eventb.core.scEvent>
-    <org.eventb.core.scEvent name="UserContey)" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="loginUser" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y7lDQldEe-O984l8O-k1g">
-        <org.eventb.core.scGuard name="'" org.eventb.core.label="grd0" org.eventb.core.predicate="user∈dom(registered)" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y7lDQldEe-O984l8O-k1g|org.eventb.core.guard#_8y8MEgldEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
-        <org.eventb.core.scGuard name="(" org.eventb.core.label="grd1" org.eventb.core.predicate="user_password=registered(user)" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y7lDQldEe-O984l8O-k1g|org.eventb.core.guard#_8y8MEwldEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
-        <org.eventb.core.scGuard name=")" org.eventb.core.label="grd2" org.eventb.core.predicate="user∉dom(loggedin)" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y7lDQldEe-O984l8O-k1g|org.eventb.core.guard#_8y8MFAldEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
-        <org.eventb.core.scParameter name="user_password" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y7lDQldEe-O984l8O-k1g|org.eventb.core.parameter#_8y8MEQldEe-O984l8O-k1g" org.eventb.core.type="PASSWORD"/>
-        <org.eventb.core.scParameter name="user" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y7lDQldEe-O984l8O-k1g|org.eventb.core.parameter#_8y8MEAldEe-O984l8O-k1g" org.eventb.core.type="USER"/>
-        <org.eventb.core.scAction name="user_passwore" org.eventb.core.assignment="loggedin ≔ loggedin∪{user ↦ user_password}" org.eventb.core.label="act0" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y7lDQldEe-O984l8O-k1g|org.eventb.core.action#_8y8MFQldEe-O984l8O-k1g"/>
-    </org.eventb.core.scEvent>
-    <org.eventb.core.scEvent name="UserContey*" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="logoutUser" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y8MFgldEe-O984l8O-k1g">
-        <org.eventb.core.scGuard name="'" org.eventb.core.label="grd0" org.eventb.core.predicate="user∈dom(loggedin)" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y8MFgldEe-O984l8O-k1g|org.eventb.core.guard#_8y8MGQldEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
-        <org.eventb.core.scGuard name="(" org.eventb.core.label="grd1" org.eventb.core.predicate="password=loggedin(user)" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y8MFgldEe-O984l8O-k1g|org.eventb.core.guard#_8y8MGgldEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
-        <org.eventb.core.scParameter name="password" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y8MFgldEe-O984l8O-k1g|org.eventb.core.parameter#_8y8MGAldEe-O984l8O-k1g" org.eventb.core.type="PASSWORD"/>
-        <org.eventb.core.scParameter name="user" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y8MFgldEe-O984l8O-k1g|org.eventb.core.parameter#_8y8MFwldEe-O984l8O-k1g" org.eventb.core.type="USER"/>
-        <org.eventb.core.scAction name="passwore" org.eventb.core.assignment="loggedin ≔ loggedin ∖ {user ↦ password}" org.eventb.core.label="act0" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y8MFgldEe-O984l8O-k1g|org.eventb.core.action#_8y8MGwldEe-O984l8O-k1g"/>
+    <org.eventb.core.scInvariant name="UserContexu" org.eventb.core.label="inv0" org.eventb.core.predicate="admin∈USER ⇸ PASSWORD" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8AZQrBEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
+    <org.eventb.core.scInvariant name="UserContexv" org.eventb.core.label="inv1" org.eventb.core.predicate="dentist∈USER ⇸ PASSWORD" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8AZgrBEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
+    <org.eventb.core.scInvariant name="UserContexw" org.eventb.core.label="inv2" org.eventb.core.predicate="patient∈USER ⇸ PASSWORD" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8AZwrBEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
+    <org.eventb.core.scInvariant name="UserContexx" org.eventb.core.label="inv3" org.eventb.core.predicate="dom(admin)⊆USER" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8AaArBEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
+    <org.eventb.core.scInvariant name="UserContexy" org.eventb.core.label="inv4" org.eventb.core.predicate="dom(dentist)⊆USER" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8AaQrBEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
+    <org.eventb.core.scInvariant name="UserContexz" org.eventb.core.label="inv5" org.eventb.core.predicate="dom(patient)⊆USER" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8AagrBEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
+    <org.eventb.core.scInvariant name="UserContex{" org.eventb.core.label="inv6" org.eventb.core.predicate="admin∩dentist∩patient=(∅ ⦂ ℙ(USER×PASSWORD))" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8AawrBEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
+    <org.eventb.core.scInvariant name="UserContex|" org.eventb.core.label="inv7" org.eventb.core.predicate="registered=admin∪dentist∪patient" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8ncArBEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
+    <org.eventb.core.scInvariant name="UserContex}" org.eventb.core.label="inv8" org.eventb.core.predicate="loggedin⊆registered" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8ncQrBEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
+    <org.eventb.core.scVariable name="loggedin" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.variable#_Qg8AYwrBEe-O984l8O-k1g" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+    <org.eventb.core.scVariable name="patient" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.variable#_Qg8AYgrBEe-O984l8O-k1g" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+    <org.eventb.core.scVariable name="dentist" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.variable#_Qg8AYQrBEe-O984l8O-k1g" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+    <org.eventb.core.scVariable name="registered" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.variable#_Qg8AZArBEe-O984l8O-k1g" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+    <org.eventb.core.scVariable name="admin" org.eventb.core.abstract="false" org.eventb.core.concrete="true" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.variable#_Qg8AYArBEe-O984l8O-k1g" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+    <org.eventb.core.scEvent name="UserContex~" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="INITIALISATION" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg8ncgrBEe-O984l8O-k1g">
+        <org.eventb.core.scAction name="'" org.eventb.core.assignment="admin ≔ ∅ ⦂ ℙ(USER×PASSWORD)" org.eventb.core.label="act0" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg8ncgrBEe-O984l8O-k1g|org.eventb.core.action#_Qg8ncwrBEe-O984l8O-k1g"/>
+        <org.eventb.core.scAction name="(" org.eventb.core.assignment="dentist ≔ ∅ ⦂ ℙ(USER×PASSWORD)" org.eventb.core.label="act1" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg8ncgrBEe-O984l8O-k1g|org.eventb.core.action#_Qg8ndArBEe-O984l8O-k1g"/>
+        <org.eventb.core.scAction name=")" org.eventb.core.assignment="patient ≔ ∅ ⦂ ℙ(USER×PASSWORD)" org.eventb.core.label="act2" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg8ncgrBEe-O984l8O-k1g|org.eventb.core.action#_Qg8ndQrBEe-O984l8O-k1g"/>
+        <org.eventb.core.scAction name="*" org.eventb.core.assignment="loggedin ≔ ∅ ⦂ ℙ(USER×PASSWORD)" org.eventb.core.label="act3" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg8ncgrBEe-O984l8O-k1g|org.eventb.core.action#_Qg8ndgrBEe-O984l8O-k1g"/>
+        <org.eventb.core.scAction name="+" org.eventb.core.assignment="registered ≔ ∅ ⦂ ℙ(USER×PASSWORD)" org.eventb.core.label="act4" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg8ncgrBEe-O984l8O-k1g|org.eventb.core.action#_Qg8ndwrBEe-O984l8O-k1g"/>
+    </org.eventb.core.scEvent>
+    <org.eventb.core.scEvent name="UserContey'" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="setRootAdmins" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg8neArBEe-O984l8O-k1g">
+        <org.eventb.core.scGuard name="'" org.eventb.core.label="grd0" org.eventb.core.predicate="root∈USER" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg8neArBEe-O984l8O-k1g|org.eventb.core.guard#_Qg8newrBEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
+        <org.eventb.core.scGuard name="(" org.eventb.core.label="grd1" org.eventb.core.predicate="root_password∈PASSWORD" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg8neArBEe-O984l8O-k1g|org.eventb.core.guard#_Qg8nfArBEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
+        <org.eventb.core.scGuard name=")" org.eventb.core.label="grd2" org.eventb.core.predicate="admin=(∅ ⦂ ℙ(USER×PASSWORD))" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg8neArBEe-O984l8O-k1g|org.eventb.core.guard#_Qg9OgArBEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
+        <org.eventb.core.scParameter name="root_password" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg8neArBEe-O984l8O-k1g|org.eventb.core.parameter#_Qg8negrBEe-O984l8O-k1g" org.eventb.core.type="PASSWORD"/>
+        <org.eventb.core.scParameter name="root" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg8neArBEe-O984l8O-k1g|org.eventb.core.parameter#_Qg8neQrBEe-O984l8O-k1g" org.eventb.core.type="USER"/>
+        <org.eventb.core.scAction name="root_passwore" org.eventb.core.assignment="admin ≔ {root ↦ root_password}" org.eventb.core.label="act0" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg8neArBEe-O984l8O-k1g|org.eventb.core.action#_Qg9OgQrBEe-O984l8O-k1g"/>
+        <org.eventb.core.scAction name="root_passworf" org.eventb.core.assignment="registered ≔ {root ↦ root_password}" org.eventb.core.label="act1" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg8neArBEe-O984l8O-k1g|org.eventb.core.action#_Qg9OggrBEe-O984l8O-k1g"/>
+    </org.eventb.core.scEvent>
+    <org.eventb.core.scEvent name="UserContey(" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="registerNewPatient" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg9OgwrBEe-O984l8O-k1g">
+        <org.eventb.core.scGuard name="'" org.eventb.core.label="grd0" org.eventb.core.predicate="new_patient∈USER" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg9OgwrBEe-O984l8O-k1g|org.eventb.core.guard#_Qg9OhgrBEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
+        <org.eventb.core.scGuard name="(" org.eventb.core.label="grd1" org.eventb.core.predicate="new_patient_password∈PASSWORD" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg9OgwrBEe-O984l8O-k1g|org.eventb.core.guard#_Qg9OhwrBEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
+        <org.eventb.core.scGuard name=")" org.eventb.core.label="grd2" org.eventb.core.predicate="new_patient∉dom(registered)" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg9OgwrBEe-O984l8O-k1g|org.eventb.core.guard#_Qg9OiArBEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
+        <org.eventb.core.scGuard name="*" org.eventb.core.label="grd3" org.eventb.core.predicate="card(admin)&gt;0" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg9OgwrBEe-O984l8O-k1g|org.eventb.core.guard#_Qg9OiQrBEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
+        <org.eventb.core.scParameter name="new_patient_password" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg9OgwrBEe-O984l8O-k1g|org.eventb.core.parameter#_Qg9OhQrBEe-O984l8O-k1g" org.eventb.core.type="PASSWORD"/>
+        <org.eventb.core.scParameter name="new_patient" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg9OgwrBEe-O984l8O-k1g|org.eventb.core.parameter#_Qg9OhArBEe-O984l8O-k1g" org.eventb.core.type="USER"/>
+        <org.eventb.core.scAction name="new_patient_passwore" org.eventb.core.assignment="patient ≔ patient∪{new_patient ↦ new_patient_password}" org.eventb.core.label="act1" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg9OgwrBEe-O984l8O-k1g|org.eventb.core.action#_Qg9OigrBEe-O984l8O-k1g"/>
+        <org.eventb.core.scAction name="new_patient_passworf" org.eventb.core.assignment="registered ≔ registered∪{new_patient ↦ new_patient_password}" org.eventb.core.label="act2" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg9OgwrBEe-O984l8O-k1g|org.eventb.core.action#_Qg9OiwrBEe-O984l8O-k1g"/>
+    </org.eventb.core.scEvent>
+    <org.eventb.core.scEvent name="UserContey)" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="loginUser" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg9OjArBEe-O984l8O-k1g">
+        <org.eventb.core.scGuard name="'" org.eventb.core.label="grd0" org.eventb.core.predicate="user∈dom(registered)" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg9OjArBEe-O984l8O-k1g|org.eventb.core.guard#_Qg91kgrBEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
+        <org.eventb.core.scGuard name="(" org.eventb.core.label="grd1" org.eventb.core.predicate="user_password=registered(user)" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg9OjArBEe-O984l8O-k1g|org.eventb.core.guard#_Qg91kwrBEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
+        <org.eventb.core.scGuard name=")" org.eventb.core.label="grd2" org.eventb.core.predicate="user∉dom(loggedin)" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg9OjArBEe-O984l8O-k1g|org.eventb.core.guard#_Qg91lArBEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
+        <org.eventb.core.scParameter name="user_password" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg9OjArBEe-O984l8O-k1g|org.eventb.core.parameter#_Qg91kQrBEe-O984l8O-k1g" org.eventb.core.type="PASSWORD"/>
+        <org.eventb.core.scParameter name="user" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg9OjArBEe-O984l8O-k1g|org.eventb.core.parameter#_Qg91kArBEe-O984l8O-k1g" org.eventb.core.type="USER"/>
+        <org.eventb.core.scAction name="user_passwore" org.eventb.core.assignment="loggedin ≔ loggedin∪{user ↦ user_password}" org.eventb.core.label="act0" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg9OjArBEe-O984l8O-k1g|org.eventb.core.action#_Qg91lQrBEe-O984l8O-k1g"/>
+    </org.eventb.core.scEvent>
+    <org.eventb.core.scEvent name="UserContey*" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="logoutUser" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg91lgrBEe-O984l8O-k1g">
+        <org.eventb.core.scGuard name="'" org.eventb.core.label="grd0" org.eventb.core.predicate="user∈dom(loggedin)" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg91lgrBEe-O984l8O-k1g|org.eventb.core.guard#_Qg91mQrBEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
+        <org.eventb.core.scGuard name="(" org.eventb.core.label="grd1" org.eventb.core.predicate="password=loggedin(user)" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg91lgrBEe-O984l8O-k1g|org.eventb.core.guard#_Qg91mgrBEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
+        <org.eventb.core.scParameter name="password" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg91lgrBEe-O984l8O-k1g|org.eventb.core.parameter#_Qg91mArBEe-O984l8O-k1g" org.eventb.core.type="PASSWORD"/>
+        <org.eventb.core.scParameter name="user" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg91lgrBEe-O984l8O-k1g|org.eventb.core.parameter#_Qg91lwrBEe-O984l8O-k1g" org.eventb.core.type="USER"/>
+        <org.eventb.core.scAction name="passwore" org.eventb.core.assignment="loggedin ≔ loggedin ∖ {user ↦ password}" org.eventb.core.label="act0" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg91lgrBEe-O984l8O-k1g|org.eventb.core.action#_Qg91mwrBEe-O984l8O-k1g"/>
+    </org.eventb.core.scEvent>
+    <org.eventb.core.scEvent name="UserContey+" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="changePatientPassword" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg91nArBEe-O984l8O-k1g">
+        <org.eventb.core.scGuard name="'" org.eventb.core.label="grd0" org.eventb.core.predicate="user∈dom(patient)" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg91nArBEe-O984l8O-k1g|org.eventb.core.guard#_Qg-cowrBEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
+        <org.eventb.core.scGuard name="(" org.eventb.core.label="grd1" org.eventb.core.predicate="password=loggedin(user)" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg91nArBEe-O984l8O-k1g|org.eventb.core.guard#_Qg-cpArBEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
+        <org.eventb.core.scGuard name=")" org.eventb.core.label="grd2" org.eventb.core.predicate="new_password∈PASSWORD" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg91nArBEe-O984l8O-k1g|org.eventb.core.guard#_Qg-cpQrBEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
+        <org.eventb.core.scGuard name="*" org.eventb.core.label="grd3" org.eventb.core.predicate="user∈dom(loggedin)" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg91nArBEe-O984l8O-k1g|org.eventb.core.guard#_Qg-cpgrBEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
+        <org.eventb.core.scParameter name="password" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg91nArBEe-O984l8O-k1g|org.eventb.core.parameter#_Qg-coQrBEe-O984l8O-k1g" org.eventb.core.type="PASSWORD"/>
+        <org.eventb.core.scParameter name="new_password" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg91nArBEe-O984l8O-k1g|org.eventb.core.parameter#_Qg-cogrBEe-O984l8O-k1g" org.eventb.core.type="PASSWORD"/>
+        <org.eventb.core.scParameter name="user" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg91nArBEe-O984l8O-k1g|org.eventb.core.parameter#_Qg-coArBEe-O984l8O-k1g" org.eventb.core.type="USER"/>
+        <org.eventb.core.scAction name="new_passwore" org.eventb.core.assignment="loggedin ≔ loggedin{user ↦ new_password}" org.eventb.core.label="act0" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg91nArBEe-O984l8O-k1g|org.eventb.core.action#_Qg-cpwrBEe-O984l8O-k1g"/>
+        <org.eventb.core.scAction name="new_passworf" org.eventb.core.assignment="registered ≔ registered{user ↦ new_password}" org.eventb.core.label="act1" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg91nArBEe-O984l8O-k1g|org.eventb.core.action#_Qg-cqArBEe-O984l8O-k1g"/>
+        <org.eventb.core.scAction name="new_passworg" org.eventb.core.assignment="patient ≔ patient{user ↦ new_password}" org.eventb.core.label="act2" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg91nArBEe-O984l8O-k1g|org.eventb.core.action#_Qg-cqQrBEe-O984l8O-k1g"/>
+    </org.eventb.core.scEvent>
+    <org.eventb.core.scEvent name="UserContey," org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="changeDentistPassword" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg-cqgrBEe-O984l8O-k1g">
+        <org.eventb.core.scGuard name="'" org.eventb.core.label="grd0" org.eventb.core.predicate="user∈dom(dentist)" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg-cqgrBEe-O984l8O-k1g|org.eventb.core.guard#_Qg_DsArBEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
+        <org.eventb.core.scGuard name="(" org.eventb.core.label="grd1" org.eventb.core.predicate="password=loggedin(user)" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg-cqgrBEe-O984l8O-k1g|org.eventb.core.guard#_Qg_DsQrBEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
+        <org.eventb.core.scGuard name=")" org.eventb.core.label="grd2" org.eventb.core.predicate="new_password∈PASSWORD" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg-cqgrBEe-O984l8O-k1g|org.eventb.core.guard#_Qg_DsgrBEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
+        <org.eventb.core.scGuard name="*" org.eventb.core.label="grd3" org.eventb.core.predicate="user∈dom(loggedin)" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg-cqgrBEe-O984l8O-k1g|org.eventb.core.guard#_Qg_DswrBEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
+        <org.eventb.core.scParameter name="password" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg-cqgrBEe-O984l8O-k1g|org.eventb.core.parameter#_Qg-crArBEe-O984l8O-k1g" org.eventb.core.type="PASSWORD"/>
+        <org.eventb.core.scParameter name="new_password" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg-cqgrBEe-O984l8O-k1g|org.eventb.core.parameter#_Qg-crQrBEe-O984l8O-k1g" org.eventb.core.type="PASSWORD"/>
+        <org.eventb.core.scParameter name="user" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg-cqgrBEe-O984l8O-k1g|org.eventb.core.parameter#_Qg-cqwrBEe-O984l8O-k1g" org.eventb.core.type="USER"/>
+        <org.eventb.core.scAction name="new_passwore" org.eventb.core.assignment="loggedin ≔ loggedin{user ↦ new_password}" org.eventb.core.label="act0" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg-cqgrBEe-O984l8O-k1g|org.eventb.core.action#_Qg_DtArBEe-O984l8O-k1g"/>
+        <org.eventb.core.scAction name="new_passworf" org.eventb.core.assignment="registered ≔ registered{user ↦ new_password}" org.eventb.core.label="act1" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg-cqgrBEe-O984l8O-k1g|org.eventb.core.action#_Qg_DtQrBEe-O984l8O-k1g"/>
+        <org.eventb.core.scAction name="new_passworg" org.eventb.core.assignment="dentist ≔ dentist{user ↦ new_password}" org.eventb.core.label="act2" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg-cqgrBEe-O984l8O-k1g|org.eventb.core.action#_Qg_DtgrBEe-O984l8O-k1g"/>
+    </org.eventb.core.scEvent>
+    <org.eventb.core.scEvent name="UserContey-" org.eventb.core.accurate="true" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.label="changeAdminPassword" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg_DtwrBEe-O984l8O-k1g">
+        <org.eventb.core.scGuard name="'" org.eventb.core.label="grd0" org.eventb.core.predicate="user∈dom(admin)" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg_DtwrBEe-O984l8O-k1g|org.eventb.core.guard#_Qg_DuwrBEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
+        <org.eventb.core.scGuard name="(" org.eventb.core.label="grd1" org.eventb.core.predicate="password=loggedin(user)" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg_DtwrBEe-O984l8O-k1g|org.eventb.core.guard#_Qg_DvArBEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
+        <org.eventb.core.scGuard name=")" org.eventb.core.label="grd2" org.eventb.core.predicate="new_password∈PASSWORD" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg_DtwrBEe-O984l8O-k1g|org.eventb.core.guard#_Qg_qwArBEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
+        <org.eventb.core.scGuard name="*" org.eventb.core.label="grd3" org.eventb.core.predicate="user∈dom(loggedin)" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg_DtwrBEe-O984l8O-k1g|org.eventb.core.guard#_Qg_qwQrBEe-O984l8O-k1g" org.eventb.core.theorem="false"/>
+        <org.eventb.core.scParameter name="password" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg_DtwrBEe-O984l8O-k1g|org.eventb.core.parameter#_Qg_DuQrBEe-O984l8O-k1g" org.eventb.core.type="PASSWORD"/>
+        <org.eventb.core.scParameter name="new_password" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg_DtwrBEe-O984l8O-k1g|org.eventb.core.parameter#_Qg_DugrBEe-O984l8O-k1g" org.eventb.core.type="PASSWORD"/>
+        <org.eventb.core.scParameter name="user" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg_DtwrBEe-O984l8O-k1g|org.eventb.core.parameter#_Qg_DuArBEe-O984l8O-k1g" org.eventb.core.type="USER"/>
+        <org.eventb.core.scAction name="new_passwore" org.eventb.core.assignment="loggedin ≔ loggedin{user ↦ new_password}" org.eventb.core.label="act0" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg_DtwrBEe-O984l8O-k1g|org.eventb.core.action#_Qg_qwgrBEe-O984l8O-k1g"/>
+        <org.eventb.core.scAction name="new_passworf" org.eventb.core.assignment="registered ≔ registered{user ↦ new_password}" org.eventb.core.label="act1" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg_DtwrBEe-O984l8O-k1g|org.eventb.core.action#_Qg_qwwrBEe-O984l8O-k1g"/>
+        <org.eventb.core.scAction name="new_passworg" org.eventb.core.assignment="admin ≔ admin{user ↦ new_password}" org.eventb.core.label="act2" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg_DtwrBEe-O984l8O-k1g|org.eventb.core.action#_Qg_qxArBEe-O984l8O-k1g"/>
     </org.eventb.core.scEvent>
 </org.eventb.core.scMachineFile>
diff --git a/UserManagement/UserMachine.bpo b/UserManagement/UserMachine.bpo
index b23c80af3dab182d2eae258e68a50e586252b9cf..2e6015611f95f61dc8f7bb9152d68c186c77571e 100644
--- a/UserManagement/UserMachine.bpo
+++ b/UserManagement/UserMachine.bpo
@@ -1,5 +1,5 @@
 <?xml version="1.0" encoding="UTF-8" standalone="no"?>
-<org.eventb.core.poFile org.eventb.core.poStamp="49">
+<org.eventb.core.poFile org.eventb.core.poStamp="54">
     <org.eventb.core.poPredicateSet name="CTXHYP" org.eventb.core.poStamp="0">
         <org.eventb.core.poIdentifier name="USER" org.eventb.core.type="ℙ(USER)"/>
         <org.eventb.core.poIdentifier name="PASSWORD" org.eventb.core.type="ℙ(PASSWORD)"/>
@@ -11,51 +11,51 @@
         <org.eventb.core.poIdentifier name="registered" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
         <org.eventb.core.poIdentifier name="admin" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
     </org.eventb.core.poPredicateSet>
-    <org.eventb.core.poSequent name="INITIALISATION/inv0/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="49">
+    <org.eventb.core.poSequent name="INITIALISATION/inv0/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="54">
         <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#EVTALLHYPUserContex~"/>
-        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="(∅ ⦂ ℙ(USER×PASSWORD))∈USER ⇸ PASSWORD" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_8y6W4QldEe-O984l8O-k1g"/>
-        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y698QldEe-O984l8O-k1g"/>
-        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_8y6W4QldEe-O984l8O-k1g"/>
+        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="(∅ ⦂ ℙ(USER×PASSWORD))∈USER ⇸ PASSWORD" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8AZQrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg8ncgrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8AZQrBEe-O984l8O-k1g"/>
         <org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poSequent#INITIALISATION\/inv0\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
         <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD0"/>
     </org.eventb.core.poSequent>
-    <org.eventb.core.poSequent name="INITIALISATION/inv1/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="49">
+    <org.eventb.core.poSequent name="INITIALISATION/inv1/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="54">
         <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#EVTALLHYPUserContex~"/>
-        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="(∅ ⦂ ℙ(USER×PASSWORD))∈USER ⇸ PASSWORD" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_8y6W4gldEe-O984l8O-k1g"/>
-        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y698QldEe-O984l8O-k1g"/>
-        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_8y6W4gldEe-O984l8O-k1g"/>
+        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="(∅ ⦂ ℙ(USER×PASSWORD))∈USER ⇸ PASSWORD" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8AZgrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg8ncgrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8AZgrBEe-O984l8O-k1g"/>
         <org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poSequent#INITIALISATION\/inv1\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
         <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD1"/>
     </org.eventb.core.poSequent>
-    <org.eventb.core.poSequent name="INITIALISATION/inv2/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="49">
+    <org.eventb.core.poSequent name="INITIALISATION/inv2/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="54">
         <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#EVTALLHYPUserContex~"/>
-        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="(∅ ⦂ ℙ(USER×PASSWORD))∈USER ⇸ PASSWORD" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_8y6W4wldEe-O984l8O-k1g"/>
-        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y698QldEe-O984l8O-k1g"/>
-        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_8y6W4wldEe-O984l8O-k1g"/>
+        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="(∅ ⦂ ℙ(USER×PASSWORD))∈USER ⇸ PASSWORD" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8AZwrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg8ncgrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8AZwrBEe-O984l8O-k1g"/>
         <org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poSequent#INITIALISATION\/inv2\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
         <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD2"/>
     </org.eventb.core.poSequent>
-    <org.eventb.core.poSequent name="INITIALISATION/inv6/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="49">
+    <org.eventb.core.poSequent name="INITIALISATION/inv6/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="54">
         <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#EVTALLHYPUserContex~"/>
-        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="(∅ ⦂ ℙ(USER×PASSWORD))∩(∅ ⦂ ℙ(USER×PASSWORD))∩(∅ ⦂ ℙ(USER×PASSWORD))=(∅ ⦂ ℙ(USER×PASSWORD))" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_8y6W5wldEe-O984l8O-k1g"/>
-        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y698QldEe-O984l8O-k1g"/>
-        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_8y6W5wldEe-O984l8O-k1g"/>
+        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="(∅ ⦂ ℙ(USER×PASSWORD))∩(∅ ⦂ ℙ(USER×PASSWORD))∩(∅ ⦂ ℙ(USER×PASSWORD))=(∅ ⦂ ℙ(USER×PASSWORD))" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8AawrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg8ncgrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8AawrBEe-O984l8O-k1g"/>
         <org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poSequent#INITIALISATION\/inv6\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
         <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD6"/>
     </org.eventb.core.poSequent>
-    <org.eventb.core.poSequent name="INITIALISATION/inv7/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="49">
+    <org.eventb.core.poSequent name="INITIALISATION/inv7/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="54">
         <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#EVTALLHYPUserContex~"/>
-        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="(∅ ⦂ ℙ(USER×PASSWORD))=(∅ ⦂ ℙ(USER×PASSWORD))∪(∅ ⦂ ℙ(USER×PASSWORD))∪(∅ ⦂ ℙ(USER×PASSWORD))" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_8y6W6AldEe-O984l8O-k1g"/>
-        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y698QldEe-O984l8O-k1g"/>
-        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_8y6W6AldEe-O984l8O-k1g"/>
+        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="(∅ ⦂ ℙ(USER×PASSWORD))=(∅ ⦂ ℙ(USER×PASSWORD))∪(∅ ⦂ ℙ(USER×PASSWORD))∪(∅ ⦂ ℙ(USER×PASSWORD))" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8ncArBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg8ncgrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8ncArBEe-O984l8O-k1g"/>
         <org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poSequent#INITIALISATION\/inv7\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
         <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD7"/>
     </org.eventb.core.poSequent>
-    <org.eventb.core.poSequent name="INITIALISATION/inv8/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="49">
+    <org.eventb.core.poSequent name="INITIALISATION/inv8/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  establishment" org.eventb.core.poStamp="54">
         <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#EVTALLHYPUserContex~"/>
-        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="(∅ ⦂ ℙ(USER×PASSWORD))⊆(∅ ⦂ ℙ(USER×PASSWORD))" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_8y698AldEe-O984l8O-k1g"/>
-        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y698QldEe-O984l8O-k1g"/>
-        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_8y698AldEe-O984l8O-k1g"/>
+        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="(∅ ⦂ ℙ(USER×PASSWORD))⊆(∅ ⦂ ℙ(USER×PASSWORD))" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8ncQrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg8ncgrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8ncQrBEe-O984l8O-k1g"/>
         <org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#CTXHYP" org.eventb.core.poSelHintSnd="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poSequent#INITIALISATION\/inv8\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
         <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD8"/>
     </org.eventb.core.poSequent>
@@ -67,161 +67,323 @@
         <org.eventb.core.poIdentifier name="dentist'" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
     </org.eventb.core.poPredicateSet>
     <org.eventb.core.poPredicateSet name="EVTALLHYPUserContex~" org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#EVTIDENTUserContex~" org.eventb.core.poStamp="0"/>
-    <org.eventb.core.poSequent name="setRootAdmins/inv0/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="49">
+    <org.eventb.core.poSequent name="setRootAdmins/inv0/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="54">
         <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#EVTALLHYPUserContey'"/>
-        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="{root ↦ root_password}∈USER ⇸ PASSWORD" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_8y6W4QldEe-O984l8O-k1g"/>
-        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y699wldEe-O984l8O-k1g"/>
-        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_8y6W4QldEe-O984l8O-k1g"/>
+        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="{root ↦ root_password}∈USER ⇸ PASSWORD" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8AZQrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg8neArBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8AZQrBEe-O984l8O-k1g"/>
         <org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poSequent#setRootAdmins\/inv0\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
         <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD0"/>
     </org.eventb.core.poSequent>
-    <org.eventb.core.poSequent name="setRootAdmins/inv6/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="49">
+    <org.eventb.core.poSequent name="setRootAdmins/inv6/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="54">
         <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#EVTALLHYPUserContey'"/>
-        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="{root ↦ root_password}∩dentist∩patient=(∅ ⦂ ℙ(USER×PASSWORD))" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_8y6W5wldEe-O984l8O-k1g"/>
-        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y699wldEe-O984l8O-k1g"/>
-        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_8y6W5wldEe-O984l8O-k1g"/>
+        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="{root ↦ root_password}∩dentist∩patient=(∅ ⦂ ℙ(USER×PASSWORD))" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8AawrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg8neArBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8AawrBEe-O984l8O-k1g"/>
         <org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poSequent#setRootAdmins\/inv6\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
         <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD6"/>
     </org.eventb.core.poSequent>
-    <org.eventb.core.poSequent name="setRootAdmins/inv7/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="49">
+    <org.eventb.core.poSequent name="setRootAdmins/inv7/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="54">
         <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#EVTALLHYPUserContey'"/>
-        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="{root ↦ root_password}={root ↦ root_password}∪dentist∪patient" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_8y6W6AldEe-O984l8O-k1g"/>
-        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y699wldEe-O984l8O-k1g"/>
-        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_8y6W6AldEe-O984l8O-k1g"/>
+        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="{root ↦ root_password}={root ↦ root_password}∪dentist∪patient" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8ncArBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg8neArBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8ncArBEe-O984l8O-k1g"/>
         <org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poSequent#setRootAdmins\/inv7\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
         <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD7"/>
     </org.eventb.core.poSequent>
-    <org.eventb.core.poSequent name="setRootAdmins/inv8/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="49">
+    <org.eventb.core.poSequent name="setRootAdmins/inv8/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="54">
         <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#EVTALLHYPUserContey'"/>
-        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="loggedin⊆{root ↦ root_password}" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_8y698AldEe-O984l8O-k1g"/>
-        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y699wldEe-O984l8O-k1g"/>
-        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_8y698AldEe-O984l8O-k1g"/>
+        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="loggedin⊆{root ↦ root_password}" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8ncQrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg8neArBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8ncQrBEe-O984l8O-k1g"/>
         <org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poSequent#setRootAdmins\/inv8\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
         <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD8"/>
     </org.eventb.core.poSequent>
-    <org.eventb.core.poPredicateSet name="EVTIDENTUserContey'" org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="49">
+    <org.eventb.core.poPredicateSet name="EVTIDENTUserContey'" org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="54">
         <org.eventb.core.poIdentifier name="root" org.eventb.core.type="USER"/>
         <org.eventb.core.poIdentifier name="registered'" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
         <org.eventb.core.poIdentifier name="admin'" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
         <org.eventb.core.poIdentifier name="root_password" org.eventb.core.type="PASSWORD"/>
     </org.eventb.core.poPredicateSet>
-    <org.eventb.core.poPredicateSet name="EVTALLHYPUserContey'" org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#EVTIDENTUserContey'" org.eventb.core.poStamp="49">
-        <org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="root∈USER" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y699wldEe-O984l8O-k1g|org.eventb.core.guard#_8y69-gldEe-O984l8O-k1g"/>
-        <org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="root_password∈PASSWORD" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y699wldEe-O984l8O-k1g|org.eventb.core.guard#_8y7lAAldEe-O984l8O-k1g"/>
-        <org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="admin=(∅ ⦂ ℙ(USER×PASSWORD))" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y699wldEe-O984l8O-k1g|org.eventb.core.guard#_8y7lAQldEe-O984l8O-k1g"/>
+    <org.eventb.core.poPredicateSet name="EVTALLHYPUserContey'" org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#EVTIDENTUserContey'" org.eventb.core.poStamp="54">
+        <org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="root∈USER" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg8neArBEe-O984l8O-k1g|org.eventb.core.guard#_Qg8newrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="root_password∈PASSWORD" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg8neArBEe-O984l8O-k1g|org.eventb.core.guard#_Qg8nfArBEe-O984l8O-k1g"/>
+        <org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="admin=(∅ ⦂ ℙ(USER×PASSWORD))" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg8neArBEe-O984l8O-k1g|org.eventb.core.guard#_Qg9OgArBEe-O984l8O-k1g"/>
     </org.eventb.core.poPredicateSet>
-    <org.eventb.core.poSequent name="registerNewPatient/grd3/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Guard" org.eventb.core.poStamp="49">
+    <org.eventb.core.poSequent name="registerNewPatient/grd3/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Guard" org.eventb.core.poStamp="54">
         <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#EVTHYPUserContey()"/>
-        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="finite(admin)" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y7lBAldEe-O984l8O-k1g|org.eventb.core.guard#_8y7lCgldEe-O984l8O-k1g"/>
-        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y7lBAldEe-O984l8O-k1g|org.eventb.core.guard#_8y7lCgldEe-O984l8O-k1g"/>
+        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="finite(admin)" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg9OgwrBEe-O984l8O-k1g|org.eventb.core.guard#_Qg9OiQrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg9OgwrBEe-O984l8O-k1g|org.eventb.core.guard#_Qg9OiQrBEe-O984l8O-k1g"/>
         <org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#EVTHYPUserContey()"/>
     </org.eventb.core.poSequent>
-    <org.eventb.core.poSequent name="registerNewPatient/inv2/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="49">
+    <org.eventb.core.poSequent name="registerNewPatient/inv2/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="54">
         <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#EVTALLHYPUserContey("/>
-        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="patient∪{new_patient ↦ new_patient_password}∈USER ⇸ PASSWORD" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_8y6W4wldEe-O984l8O-k1g"/>
-        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y7lBAldEe-O984l8O-k1g"/>
-        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_8y6W4wldEe-O984l8O-k1g"/>
+        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="patient∪{new_patient ↦ new_patient_password}∈USER ⇸ PASSWORD" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8AZwrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg9OgwrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8AZwrBEe-O984l8O-k1g"/>
         <org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poSequent#registerNewPatient\/inv2\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
         <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD2"/>
     </org.eventb.core.poSequent>
-    <org.eventb.core.poSequent name="registerNewPatient/inv6/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="49">
+    <org.eventb.core.poSequent name="registerNewPatient/inv6/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="54">
         <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#EVTALLHYPUserContey("/>
-        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="admin∩dentist∩(patient∪{new_patient ↦ new_patient_password})=(∅ ⦂ ℙ(USER×PASSWORD))" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_8y6W5wldEe-O984l8O-k1g"/>
-        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y7lBAldEe-O984l8O-k1g"/>
-        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_8y6W5wldEe-O984l8O-k1g"/>
+        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="admin∩dentist∩(patient∪{new_patient ↦ new_patient_password})=(∅ ⦂ ℙ(USER×PASSWORD))" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8AawrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg9OgwrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8AawrBEe-O984l8O-k1g"/>
         <org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poSequent#registerNewPatient\/inv6\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
         <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD6"/>
     </org.eventb.core.poSequent>
-    <org.eventb.core.poSequent name="registerNewPatient/inv7/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="49">
+    <org.eventb.core.poSequent name="registerNewPatient/inv7/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="54">
         <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#EVTALLHYPUserContey("/>
-        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="registered∪{new_patient ↦ new_patient_password}=admin∪dentist∪(patient∪{new_patient ↦ new_patient_password})" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_8y6W6AldEe-O984l8O-k1g"/>
-        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y7lBAldEe-O984l8O-k1g"/>
-        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_8y6W6AldEe-O984l8O-k1g"/>
+        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="registered∪{new_patient ↦ new_patient_password}=admin∪dentist∪(patient∪{new_patient ↦ new_patient_password})" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8ncArBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg9OgwrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8ncArBEe-O984l8O-k1g"/>
         <org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poSequent#registerNewPatient\/inv7\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
         <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD7"/>
     </org.eventb.core.poSequent>
-    <org.eventb.core.poSequent name="registerNewPatient/inv8/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="49">
+    <org.eventb.core.poSequent name="registerNewPatient/inv8/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="54">
         <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#EVTALLHYPUserContey("/>
-        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="loggedin⊆registered∪{new_patient ↦ new_patient_password}" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_8y698AldEe-O984l8O-k1g"/>
-        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y7lBAldEe-O984l8O-k1g"/>
-        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_8y698AldEe-O984l8O-k1g"/>
+        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="loggedin⊆registered∪{new_patient ↦ new_patient_password}" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8ncQrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg9OgwrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8ncQrBEe-O984l8O-k1g"/>
         <org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poSequent#registerNewPatient\/inv8\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
         <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD8"/>
     </org.eventb.core.poSequent>
-    <org.eventb.core.poPredicateSet name="EVTIDENTUserContey(" org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="49">
+    <org.eventb.core.poPredicateSet name="EVTIDENTUserContey(" org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="54">
         <org.eventb.core.poIdentifier name="new_patient" org.eventb.core.type="USER"/>
         <org.eventb.core.poIdentifier name="registered'" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
         <org.eventb.core.poIdentifier name="new_patient_password" org.eventb.core.type="PASSWORD"/>
         <org.eventb.core.poIdentifier name="patient'" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
     </org.eventb.core.poPredicateSet>
-    <org.eventb.core.poPredicateSet name="EVTHYPUserContey()" org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#EVTIDENTUserContey(" org.eventb.core.poStamp="49">
-        <org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="new_patient∈USER" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y7lBAldEe-O984l8O-k1g|org.eventb.core.guard#_8y7lBwldEe-O984l8O-k1g"/>
-        <org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="new_patient_password∈PASSWORD" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y7lBAldEe-O984l8O-k1g|org.eventb.core.guard#_8y7lCAldEe-O984l8O-k1g"/>
-        <org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="new_patient∉dom(registered)" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y7lBAldEe-O984l8O-k1g|org.eventb.core.guard#_8y7lCQldEe-O984l8O-k1g"/>
+    <org.eventb.core.poPredicateSet name="EVTHYPUserContey()" org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#EVTIDENTUserContey(" org.eventb.core.poStamp="54">
+        <org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="new_patient∈USER" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg9OgwrBEe-O984l8O-k1g|org.eventb.core.guard#_Qg9OhgrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="new_patient_password∈PASSWORD" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg9OgwrBEe-O984l8O-k1g|org.eventb.core.guard#_Qg9OhwrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="new_patient∉dom(registered)" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg9OgwrBEe-O984l8O-k1g|org.eventb.core.guard#_Qg9OiArBEe-O984l8O-k1g"/>
     </org.eventb.core.poPredicateSet>
-    <org.eventb.core.poPredicateSet name="EVTALLHYPUserContey(" org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#EVTHYPUserContey()" org.eventb.core.poStamp="49">
-        <org.eventb.core.poPredicate name="PRD3" org.eventb.core.predicate="card(admin)&gt;0" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y7lBAldEe-O984l8O-k1g|org.eventb.core.guard#_8y7lCgldEe-O984l8O-k1g"/>
+    <org.eventb.core.poPredicateSet name="EVTALLHYPUserContey(" org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#EVTHYPUserContey()" org.eventb.core.poStamp="54">
+        <org.eventb.core.poPredicate name="PRD3" org.eventb.core.predicate="card(admin)&gt;0" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg9OgwrBEe-O984l8O-k1g|org.eventb.core.guard#_Qg9OiQrBEe-O984l8O-k1g"/>
     </org.eventb.core.poPredicateSet>
-    <org.eventb.core.poSequent name="loginUser/grd1/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Guard" org.eventb.core.poStamp="49">
+    <org.eventb.core.poSequent name="loginUser/grd1/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Guard" org.eventb.core.poStamp="54">
         <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#EVTHYPUserContey)'"/>
-        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="user∈dom(registered)∧registered∈USER ⇸ PASSWORD" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y7lDQldEe-O984l8O-k1g|org.eventb.core.guard#_8y8MEwldEe-O984l8O-k1g"/>
-        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y7lDQldEe-O984l8O-k1g|org.eventb.core.guard#_8y8MEwldEe-O984l8O-k1g"/>
+        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="user∈dom(registered)∧registered∈USER ⇸ PASSWORD" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg9OjArBEe-O984l8O-k1g|org.eventb.core.guard#_Qg91kwrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg9OjArBEe-O984l8O-k1g|org.eventb.core.guard#_Qg91kwrBEe-O984l8O-k1g"/>
         <org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#EVTHYPUserContey)'"/>
     </org.eventb.core.poSequent>
-    <org.eventb.core.poSequent name="loginUser/inv8/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="49">
+    <org.eventb.core.poSequent name="loginUser/inv8/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="54">
         <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#EVTALLHYPUserContey)"/>
-        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="loggedin∪{user ↦ user_password}⊆registered" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_8y698AldEe-O984l8O-k1g"/>
-        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y7lDQldEe-O984l8O-k1g"/>
-        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_8y698AldEe-O984l8O-k1g"/>
+        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="loggedin∪{user ↦ user_password}⊆registered" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8ncQrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg9OjArBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8ncQrBEe-O984l8O-k1g"/>
         <org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poSequent#loginUser\/inv8\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
         <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD8"/>
     </org.eventb.core.poSequent>
-    <org.eventb.core.poPredicateSet name="EVTIDENTUserContey)" org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="49">
+    <org.eventb.core.poPredicateSet name="EVTIDENTUserContey)" org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="54">
         <org.eventb.core.poIdentifier name="loggedin'" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
         <org.eventb.core.poIdentifier name="user" org.eventb.core.type="USER"/>
         <org.eventb.core.poIdentifier name="user_password" org.eventb.core.type="PASSWORD"/>
     </org.eventb.core.poPredicateSet>
-    <org.eventb.core.poPredicateSet name="EVTHYPUserContey)'" org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#EVTIDENTUserContey)" org.eventb.core.poStamp="49">
-        <org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="user∈dom(registered)" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y7lDQldEe-O984l8O-k1g|org.eventb.core.guard#_8y8MEgldEe-O984l8O-k1g"/>
+    <org.eventb.core.poPredicateSet name="EVTHYPUserContey)'" org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#EVTIDENTUserContey)" org.eventb.core.poStamp="54">
+        <org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="user∈dom(registered)" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg9OjArBEe-O984l8O-k1g|org.eventb.core.guard#_Qg91kgrBEe-O984l8O-k1g"/>
     </org.eventb.core.poPredicateSet>
-    <org.eventb.core.poPredicateSet name="EVTALLHYPUserContey)" org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#EVTHYPUserContey)'" org.eventb.core.poStamp="49">
-        <org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="user_password=registered(user)" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y7lDQldEe-O984l8O-k1g|org.eventb.core.guard#_8y8MEwldEe-O984l8O-k1g"/>
-        <org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="user∉dom(loggedin)" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y7lDQldEe-O984l8O-k1g|org.eventb.core.guard#_8y8MFAldEe-O984l8O-k1g"/>
+    <org.eventb.core.poPredicateSet name="EVTALLHYPUserContey)" org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#EVTHYPUserContey)'" org.eventb.core.poStamp="54">
+        <org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="user_password=registered(user)" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg9OjArBEe-O984l8O-k1g|org.eventb.core.guard#_Qg91kwrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="user∉dom(loggedin)" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg9OjArBEe-O984l8O-k1g|org.eventb.core.guard#_Qg91lArBEe-O984l8O-k1g"/>
     </org.eventb.core.poPredicateSet>
-    <org.eventb.core.poSequent name="logoutUser/grd1/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Guard" org.eventb.core.poStamp="49">
+    <org.eventb.core.poSequent name="logoutUser/grd1/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Guard" org.eventb.core.poStamp="54">
         <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#EVTHYPUserContey*'"/>
-        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="user∈dom(loggedin)∧loggedin∈USER ⇸ PASSWORD" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y8MFgldEe-O984l8O-k1g|org.eventb.core.guard#_8y8MGgldEe-O984l8O-k1g"/>
-        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y8MFgldEe-O984l8O-k1g|org.eventb.core.guard#_8y8MGgldEe-O984l8O-k1g"/>
+        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="user∈dom(loggedin)∧loggedin∈USER ⇸ PASSWORD" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg91lgrBEe-O984l8O-k1g|org.eventb.core.guard#_Qg91mgrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg91lgrBEe-O984l8O-k1g|org.eventb.core.guard#_Qg91mgrBEe-O984l8O-k1g"/>
         <org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#EVTHYPUserContey*'"/>
     </org.eventb.core.poSequent>
-    <org.eventb.core.poSequent name="logoutUser/inv8/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="49">
+    <org.eventb.core.poSequent name="logoutUser/inv8/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="54">
         <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#EVTALLHYPUserContey*"/>
-        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="loggedin ∖ {user ↦ password}⊆registered" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_8y698AldEe-O984l8O-k1g"/>
-        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y8MFgldEe-O984l8O-k1g"/>
-        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_8y698AldEe-O984l8O-k1g"/>
+        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="loggedin ∖ {user ↦ password}⊆registered" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8ncQrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg91lgrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8ncQrBEe-O984l8O-k1g"/>
         <org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poSequent#logoutUser\/inv8\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
         <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD8"/>
     </org.eventb.core.poSequent>
-    <org.eventb.core.poPredicateSet name="EVTIDENTUserContey*" org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="49">
+    <org.eventb.core.poPredicateSet name="EVTIDENTUserContey*" org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="54">
         <org.eventb.core.poIdentifier name="loggedin'" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
         <org.eventb.core.poIdentifier name="user" org.eventb.core.type="USER"/>
         <org.eventb.core.poIdentifier name="password" org.eventb.core.type="PASSWORD"/>
     </org.eventb.core.poPredicateSet>
-    <org.eventb.core.poPredicateSet name="EVTHYPUserContey*'" org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#EVTIDENTUserContey*" org.eventb.core.poStamp="49">
-        <org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="user∈dom(loggedin)" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y8MFgldEe-O984l8O-k1g|org.eventb.core.guard#_8y8MGQldEe-O984l8O-k1g"/>
-    </org.eventb.core.poPredicateSet>
-    <org.eventb.core.poPredicateSet name="EVTALLHYPUserContey*" org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#EVTHYPUserContey*'" org.eventb.core.poStamp="49">
-        <org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="password=loggedin(user)" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_8y8MFgldEe-O984l8O-k1g|org.eventb.core.guard#_8y8MGgldEe-O984l8O-k1g"/>
-    </org.eventb.core.poPredicateSet>
-    <org.eventb.core.poPredicateSet name="ALLHYP" org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poStamp="49">
-        <org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="admin∈USER ⇸ PASSWORD" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_8y6W4QldEe-O984l8O-k1g"/>
-        <org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="dentist∈USER ⇸ PASSWORD" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_8y6W4gldEe-O984l8O-k1g"/>
-        <org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="patient∈USER ⇸ PASSWORD" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_8y6W4wldEe-O984l8O-k1g"/>
-        <org.eventb.core.poPredicate name="PRD3" org.eventb.core.predicate="dom(admin)⊆USER" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_8y6W5AldEe-O984l8O-k1g"/>
-        <org.eventb.core.poPredicate name="PRD4" org.eventb.core.predicate="dom(dentist)⊆USER" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_8y6W5QldEe-O984l8O-k1g"/>
-        <org.eventb.core.poPredicate name="PRD5" org.eventb.core.predicate="dom(patient)⊆USER" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_8y6W5gldEe-O984l8O-k1g"/>
-        <org.eventb.core.poPredicate name="PRD6" org.eventb.core.predicate="admin∩dentist∩patient=(∅ ⦂ ℙ(USER×PASSWORD))" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_8y6W5wldEe-O984l8O-k1g"/>
-        <org.eventb.core.poPredicate name="PRD7" org.eventb.core.predicate="registered=admin∪dentist∪patient" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_8y6W6AldEe-O984l8O-k1g"/>
-        <org.eventb.core.poPredicate name="PRD8" org.eventb.core.predicate="loggedin⊆registered" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_8y698AldEe-O984l8O-k1g"/>
+    <org.eventb.core.poPredicateSet name="EVTHYPUserContey*'" org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#EVTIDENTUserContey*" org.eventb.core.poStamp="54">
+        <org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="user∈dom(loggedin)" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg91lgrBEe-O984l8O-k1g|org.eventb.core.guard#_Qg91mQrBEe-O984l8O-k1g"/>
+    </org.eventb.core.poPredicateSet>
+    <org.eventb.core.poPredicateSet name="EVTALLHYPUserContey*" org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#EVTHYPUserContey*'" org.eventb.core.poStamp="54">
+        <org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="password=loggedin(user)" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg91lgrBEe-O984l8O-k1g|org.eventb.core.guard#_Qg91mgrBEe-O984l8O-k1g"/>
+    </org.eventb.core.poPredicateSet>
+    <org.eventb.core.poSequent name="changePatientPassword/grd1/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Guard" org.eventb.core.poStamp="54">
+        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#EVTHYPUserContey+'"/>
+        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="user∈dom(loggedin)∧loggedin∈USER ⇸ PASSWORD" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg91nArBEe-O984l8O-k1g|org.eventb.core.guard#_Qg-cpArBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg91nArBEe-O984l8O-k1g|org.eventb.core.guard#_Qg-cpArBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#EVTHYPUserContey+'"/>
+    </org.eventb.core.poSequent>
+    <org.eventb.core.poSequent name="changePatientPassword/inv2/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="54">
+        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#EVTALLHYPUserContey+"/>
+        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="patient{user ↦ new_password}∈USER ⇸ PASSWORD" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8AZwrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg91nArBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8AZwrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poSequent#changePatientPassword\/inv2\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
+        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD2"/>
+    </org.eventb.core.poSequent>
+    <org.eventb.core.poSequent name="changePatientPassword/inv6/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="54">
+        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#EVTALLHYPUserContey+"/>
+        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="admin∩dentist∩(patient{user ↦ new_password})=(∅ ⦂ ℙ(USER×PASSWORD))" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8AawrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg91nArBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8AawrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poSequent#changePatientPassword\/inv6\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
+        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD6"/>
+    </org.eventb.core.poSequent>
+    <org.eventb.core.poSequent name="changePatientPassword/inv7/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="54">
+        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#EVTALLHYPUserContey+"/>
+        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="registered{user ↦ new_password}=admin∪dentist∪(patient{user ↦ new_password})" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8ncArBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg91nArBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8ncArBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poSequent#changePatientPassword\/inv7\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
+        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD7"/>
+    </org.eventb.core.poSequent>
+    <org.eventb.core.poSequent name="changePatientPassword/inv8/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="54">
+        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#EVTALLHYPUserContey+"/>
+        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="loggedin{user ↦ new_password}⊆registered{user ↦ new_password}" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8ncQrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg91nArBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8ncQrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poSequent#changePatientPassword\/inv8\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
+        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD8"/>
+    </org.eventb.core.poSequent>
+    <org.eventb.core.poPredicateSet name="EVTIDENTUserContey+" org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="54">
+        <org.eventb.core.poIdentifier name="loggedin'" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        <org.eventb.core.poIdentifier name="registered'" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        <org.eventb.core.poIdentifier name="user" org.eventb.core.type="USER"/>
+        <org.eventb.core.poIdentifier name="patient'" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        <org.eventb.core.poIdentifier name="password" org.eventb.core.type="PASSWORD"/>
+        <org.eventb.core.poIdentifier name="new_password" org.eventb.core.type="PASSWORD"/>
+    </org.eventb.core.poPredicateSet>
+    <org.eventb.core.poPredicateSet name="EVTHYPUserContey+'" org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#EVTIDENTUserContey+" org.eventb.core.poStamp="54">
+        <org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="user∈dom(patient)" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg91nArBEe-O984l8O-k1g|org.eventb.core.guard#_Qg-cowrBEe-O984l8O-k1g"/>
+    </org.eventb.core.poPredicateSet>
+    <org.eventb.core.poPredicateSet name="EVTALLHYPUserContey+" org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#EVTHYPUserContey+'" org.eventb.core.poStamp="54">
+        <org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="password=loggedin(user)" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg91nArBEe-O984l8O-k1g|org.eventb.core.guard#_Qg-cpArBEe-O984l8O-k1g"/>
+        <org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="new_password∈PASSWORD" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg91nArBEe-O984l8O-k1g|org.eventb.core.guard#_Qg-cpQrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poPredicate name="PRD3" org.eventb.core.predicate="user∈dom(loggedin)" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg91nArBEe-O984l8O-k1g|org.eventb.core.guard#_Qg-cpgrBEe-O984l8O-k1g"/>
+    </org.eventb.core.poPredicateSet>
+    <org.eventb.core.poSequent name="changeDentistPassword/grd1/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Guard" org.eventb.core.poStamp="54">
+        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#EVTHYPUserContey,'"/>
+        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="user∈dom(loggedin)∧loggedin∈USER ⇸ PASSWORD" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg-cqgrBEe-O984l8O-k1g|org.eventb.core.guard#_Qg_DsQrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg-cqgrBEe-O984l8O-k1g|org.eventb.core.guard#_Qg_DsQrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#EVTHYPUserContey,'"/>
+    </org.eventb.core.poSequent>
+    <org.eventb.core.poSequent name="changeDentistPassword/inv1/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="54">
+        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#EVTALLHYPUserContey,"/>
+        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="dentist{user ↦ new_password}∈USER ⇸ PASSWORD" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8AZgrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg-cqgrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8AZgrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poSequent#changeDentistPassword\/inv1\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
+        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD1"/>
+    </org.eventb.core.poSequent>
+    <org.eventb.core.poSequent name="changeDentistPassword/inv6/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="54">
+        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#EVTALLHYPUserContey,"/>
+        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="admin∩(dentist{user ↦ new_password})∩patient=(∅ ⦂ ℙ(USER×PASSWORD))" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8AawrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg-cqgrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8AawrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poSequent#changeDentistPassword\/inv6\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
+        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD6"/>
+    </org.eventb.core.poSequent>
+    <org.eventb.core.poSequent name="changeDentistPassword/inv7/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="54">
+        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#EVTALLHYPUserContey,"/>
+        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="registered{user ↦ new_password}=admin∪(dentist{user ↦ new_password})∪patient" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8ncArBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg-cqgrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8ncArBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poSequent#changeDentistPassword\/inv7\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
+        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD7"/>
+    </org.eventb.core.poSequent>
+    <org.eventb.core.poSequent name="changeDentistPassword/inv8/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="54">
+        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#EVTALLHYPUserContey,"/>
+        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="loggedin{user ↦ new_password}⊆registered{user ↦ new_password}" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8ncQrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg-cqgrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8ncQrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poSequent#changeDentistPassword\/inv8\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
+        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD8"/>
+    </org.eventb.core.poSequent>
+    <org.eventb.core.poPredicateSet name="EVTIDENTUserContey," org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="54">
+        <org.eventb.core.poIdentifier name="loggedin'" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        <org.eventb.core.poIdentifier name="registered'" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        <org.eventb.core.poIdentifier name="user" org.eventb.core.type="USER"/>
+        <org.eventb.core.poIdentifier name="password" org.eventb.core.type="PASSWORD"/>
+        <org.eventb.core.poIdentifier name="dentist'" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        <org.eventb.core.poIdentifier name="new_password" org.eventb.core.type="PASSWORD"/>
+    </org.eventb.core.poPredicateSet>
+    <org.eventb.core.poPredicateSet name="EVTHYPUserContey,'" org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#EVTIDENTUserContey," org.eventb.core.poStamp="0">
+        <org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="user∈dom(dentist)" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg-cqgrBEe-O984l8O-k1g|org.eventb.core.guard#_Qg_DsArBEe-O984l8O-k1g"/>
+    </org.eventb.core.poPredicateSet>
+    <org.eventb.core.poPredicateSet name="EVTALLHYPUserContey," org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#EVTHYPUserContey,'" org.eventb.core.poStamp="54">
+        <org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="password=loggedin(user)" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg-cqgrBEe-O984l8O-k1g|org.eventb.core.guard#_Qg_DsQrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="new_password∈PASSWORD" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg-cqgrBEe-O984l8O-k1g|org.eventb.core.guard#_Qg_DsgrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poPredicate name="PRD3" org.eventb.core.predicate="user∈dom(loggedin)" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg-cqgrBEe-O984l8O-k1g|org.eventb.core.guard#_Qg_DswrBEe-O984l8O-k1g"/>
+    </org.eventb.core.poPredicateSet>
+    <org.eventb.core.poSequent name="changeAdminPassword/grd1/WD" org.eventb.core.accurate="true" org.eventb.core.poDesc="Well-definedness of Guard" org.eventb.core.poStamp="54">
+        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#EVTHYPUserContey-'"/>
+        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="user∈dom(loggedin)∧loggedin∈USER ⇸ PASSWORD" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg_DtwrBEe-O984l8O-k1g|org.eventb.core.guard#_Qg_DvArBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg_DtwrBEe-O984l8O-k1g|org.eventb.core.guard#_Qg_DvArBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSelHint name="SEQHYS" org.eventb.core.poSelHintFst="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#EVTHYPUserContey-'"/>
+    </org.eventb.core.poSequent>
+    <org.eventb.core.poSequent name="changeAdminPassword/inv0/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="54">
+        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#EVTALLHYPUserContey-"/>
+        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="admin{user ↦ new_password}∈USER ⇸ PASSWORD" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8AZQrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg_DtwrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8AZQrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poSequent#changeAdminPassword\/inv0\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
+        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD0"/>
+    </org.eventb.core.poSequent>
+    <org.eventb.core.poSequent name="changeAdminPassword/inv6/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="54">
+        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#EVTALLHYPUserContey-"/>
+        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="(admin{user ↦ new_password})∩dentist∩patient=(∅ ⦂ ℙ(USER×PASSWORD))" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8AawrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg_DtwrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8AawrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poSequent#changeAdminPassword\/inv6\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
+        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD6"/>
+    </org.eventb.core.poSequent>
+    <org.eventb.core.poSequent name="changeAdminPassword/inv7/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="54">
+        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#EVTALLHYPUserContey-"/>
+        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="registered{user ↦ new_password}=(admin{user ↦ new_password})∪dentist∪patient" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8ncArBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg_DtwrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8ncArBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poSequent#changeAdminPassword\/inv7\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
+        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD7"/>
+    </org.eventb.core.poSequent>
+    <org.eventb.core.poSequent name="changeAdminPassword/inv8/INV" org.eventb.core.accurate="true" org.eventb.core.poDesc="Invariant  preservation" org.eventb.core.poStamp="54">
+        <org.eventb.core.poPredicateSet name="SEQHYP" org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#EVTALLHYPUserContey-"/>
+        <org.eventb.core.poPredicate name="SEQHYQ" org.eventb.core.predicate="loggedin{user ↦ new_password}⊆registered{user ↦ new_password}" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8ncQrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSource name="SEQHYR" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg_DtwrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSource name="SEQHYS" org.eventb.core.poRole="DEFAULT" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8ncQrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poSelHint name="SEQHYT" org.eventb.core.poSelHintFst="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poSelHintSnd="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poSequent#changeAdminPassword\/inv8\/INV|org.eventb.core.poPredicateSet#SEQHYP"/>
+        <org.eventb.core.poSelHint name="SEQHYU" org.eventb.core.poSelHintFst="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ALLHYP|org.eventb.core.poPredicate#PRD8"/>
+    </org.eventb.core.poSequent>
+    <org.eventb.core.poPredicateSet name="EVTIDENTUserContey-" org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ALLHYP" org.eventb.core.poStamp="0">
+        <org.eventb.core.poIdentifier name="loggedin'" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        <org.eventb.core.poIdentifier name="registered'" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        <org.eventb.core.poIdentifier name="user" org.eventb.core.type="USER"/>
+        <org.eventb.core.poIdentifier name="admin'" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        <org.eventb.core.poIdentifier name="password" org.eventb.core.type="PASSWORD"/>
+        <org.eventb.core.poIdentifier name="new_password" org.eventb.core.type="PASSWORD"/>
+    </org.eventb.core.poPredicateSet>
+    <org.eventb.core.poPredicateSet name="EVTHYPUserContey-'" org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#EVTIDENTUserContey-" org.eventb.core.poStamp="0">
+        <org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="user∈dom(admin)" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg_DtwrBEe-O984l8O-k1g|org.eventb.core.guard#_Qg_DuwrBEe-O984l8O-k1g"/>
+    </org.eventb.core.poPredicateSet>
+    <org.eventb.core.poPredicateSet name="EVTALLHYPUserContey-" org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#EVTHYPUserContey-'" org.eventb.core.poStamp="0">
+        <org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="password=loggedin(user)" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg_DtwrBEe-O984l8O-k1g|org.eventb.core.guard#_Qg_DvArBEe-O984l8O-k1g"/>
+        <org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="new_password∈PASSWORD" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg_DtwrBEe-O984l8O-k1g|org.eventb.core.guard#_Qg_qwArBEe-O984l8O-k1g"/>
+        <org.eventb.core.poPredicate name="PRD3" org.eventb.core.predicate="user∈dom(loggedin)" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.event#_Qg_DtwrBEe-O984l8O-k1g|org.eventb.core.guard#_Qg_qwQrBEe-O984l8O-k1g"/>
+    </org.eventb.core.poPredicateSet>
+    <org.eventb.core.poPredicateSet name="ALLHYP" org.eventb.core.parentSet="/UserManagement/UserMachine.bpo|org.eventb.core.poFile#UserMachine|org.eventb.core.poPredicateSet#ABSHYP" org.eventb.core.poStamp="54">
+        <org.eventb.core.poPredicate name="PRD0" org.eventb.core.predicate="admin∈USER ⇸ PASSWORD" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8AZQrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poPredicate name="PRD1" org.eventb.core.predicate="dentist∈USER ⇸ PASSWORD" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8AZgrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poPredicate name="PRD2" org.eventb.core.predicate="patient∈USER ⇸ PASSWORD" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8AZwrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poPredicate name="PRD3" org.eventb.core.predicate="dom(admin)⊆USER" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8AaArBEe-O984l8O-k1g"/>
+        <org.eventb.core.poPredicate name="PRD4" org.eventb.core.predicate="dom(dentist)⊆USER" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8AaQrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poPredicate name="PRD5" org.eventb.core.predicate="dom(patient)⊆USER" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8AagrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poPredicate name="PRD6" org.eventb.core.predicate="admin∩dentist∩patient=(∅ ⦂ ℙ(USER×PASSWORD))" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8AawrBEe-O984l8O-k1g"/>
+        <org.eventb.core.poPredicate name="PRD7" org.eventb.core.predicate="registered=admin∪dentist∪patient" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8ncArBEe-O984l8O-k1g"/>
+        <org.eventb.core.poPredicate name="PRD8" org.eventb.core.predicate="loggedin⊆registered" org.eventb.core.source="/UserManagement/UserMachine.bum|org.eventb.core.machineFile#UserMachine|org.eventb.core.invariant#_Qg8ncQrBEe-O984l8O-k1g"/>
     </org.eventb.core.poPredicateSet>
 </org.eventb.core.poFile>
diff --git a/UserManagement/UserMachine.bpr b/UserManagement/UserMachine.bpr
index 517c5aa7d5469ce8da5139940c122c439b4c1e74..820f0ecc5302551c2915b2c06ef5325a84563414 100644
--- a/UserManagement/UserMachine.bpr
+++ b/UserManagement/UserMachine.bpr
@@ -1595,4 +1595,496 @@
         <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.eq:1"/>
         <org.eventb.core.prReas name="r2" org.eventb.core.prRID="org.eventb.core.seqprover.autoRewritesL4:0"/>
     </org.eventb.core.prProof>
+    <org.eventb.core.prProof name="changePatientPassword/grd1/WD" org.eventb.core.confidence="0" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="" org.eventb.core.prSets="PASSWORD,USER">
+        <org.eventb.core.lang name="L"/>
+        <org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="type rewrites" org.eventb.core.prHyps="">
+            <org.eventb.core.prAnte name="'">
+                <org.eventb.core.prHypAction name="HIDE0" org.eventb.core.prHyps="p1"/>
+                <org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p2"/>
+                <org.eventb.core.prHypAction name="HIDE2" org.eventb.core.prHyps="p3"/>
+                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="∧ goal" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
+                    <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p4"/>
+                    <org.eventb.core.prAnte name="(" org.eventb.core.prGoal="p5"/>
+                </org.eventb.core.prRule>
+            </org.eventb.core.prAnte>
+        </org.eventb.core.prRule>
+        <org.eventb.core.prIdent name="loggedin" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        <org.eventb.core.prIdent name="user" org.eventb.core.type="USER"/>
+        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="dom(admin)⊆USER">
+            <org.eventb.core.prIdent name="admin" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="dom(patient)⊆USER">
+            <org.eventb.core.prIdent name="patient" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p4" org.eventb.core.predicate="user∈dom(loggedin)"/>
+        <org.eventb.core.prPred name="p5" org.eventb.core.predicate="loggedin∈USER ⇸ PASSWORD"/>
+        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="user∈dom(loggedin)∧loggedin∈USER ⇸ PASSWORD"/>
+        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="dom(dentist)⊆USER">
+            <org.eventb.core.prIdent name="dentist" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.typeRewrites:1"/>
+        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.conj:0"/>
+    </org.eventb.core.prProof>
+    <org.eventb.core.prProof name="changePatientPassword/inv2/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1,p2,p3,p4,p5,p6,p7,p8,p9,p10" org.eventb.core.prSets="PASSWORD,USER">
+        <org.eventb.core.lang name="L"/>
+        <org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="type rewrites" org.eventb.core.prHyps="">
+            <org.eventb.core.prAnte name="'">
+                <org.eventb.core.prHypAction name="HIDE0" org.eventb.core.prHyps="p11"/>
+                <org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p12"/>
+                <org.eventb.core.prHypAction name="HIDE2" org.eventb.core.prHyps="p13"/>
+                <org.eventb.core.prHypAction name="HIDE3" org.eventb.core.prHyps="p14"/>
+                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="ML" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p3,p10,p7,p8,p1,p2,p4,p5,p6,p9">
+                    <org.eventb.core.prString name=".arg" org.eventb.core.prSValue="0;1:500"/>
+                </org.eventb.core.prRule>
+            </org.eventb.core.prAnte>
+        </org.eventb.core.prRule>
+        <org.eventb.core.prIdent name="admin" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        <org.eventb.core.prIdent name="dentist" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        <org.eventb.core.prIdent name="loggedin" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        <org.eventb.core.prIdent name="new_password" org.eventb.core.type="PASSWORD"/>
+        <org.eventb.core.prIdent name="password" org.eventb.core.type="PASSWORD"/>
+        <org.eventb.core.prIdent name="patient" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        <org.eventb.core.prIdent name="registered" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        <org.eventb.core.prIdent name="user" org.eventb.core.type="USER"/>
+        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="registered=admin∪dentist∪patient"/>
+        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="loggedin⊆registered"/>
+        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="admin∈USER ⇸ PASSWORD"/>
+        <org.eventb.core.prPred name="p5" org.eventb.core.predicate="password=loggedin(user)"/>
+        <org.eventb.core.prPred name="p6" org.eventb.core.predicate="user∈dom(loggedin)"/>
+        <org.eventb.core.prPred name="p7" org.eventb.core.predicate="patient∈USER ⇸ PASSWORD"/>
+        <org.eventb.core.prPred name="p9" org.eventb.core.predicate="loggedin∈USER ⇸ PASSWORD"/>
+        <org.eventb.core.prPred name="p14" org.eventb.core.predicate="new_password∈PASSWORD"/>
+        <org.eventb.core.prPred name="p12" org.eventb.core.predicate="dom(dentist)⊆USER"/>
+        <org.eventb.core.prPred name="p4" org.eventb.core.predicate="user∈dom(patient)"/>
+        <org.eventb.core.prPred name="p11" org.eventb.core.predicate="dom(admin)⊆USER"/>
+        <org.eventb.core.prPred name="p13" org.eventb.core.predicate="dom(patient)⊆USER"/>
+        <org.eventb.core.prPred name="p8" org.eventb.core.predicate="admin∩dentist∩patient=(∅ ⦂ ℙ(USER×PASSWORD))"/>
+        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="patient{user ↦ new_password}∈USER ⇸ PASSWORD"/>
+        <org.eventb.core.prPred name="p10" org.eventb.core.predicate="dentist∈USER ⇸ PASSWORD"/>
+        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.typeRewrites:1"/>
+        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="com.clearsy.atelierb.provers.core.externalML:1"/>
+    </org.eventb.core.prProof>
+    <org.eventb.core.prProof name="changePatientPassword/inv6/INV" org.eventb.core.confidence="0" org.eventb.core.prFresh="" org.eventb.core.prHyps="">
+        <org.eventb.core.lang name="L"/>
+        <org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="type rewrites" org.eventb.core.prHyps="">
+            <org.eventb.core.prAnte name="'">
+                <org.eventb.core.prHypAction name="HIDE0" org.eventb.core.prHyps="p0"/>
+                <org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p1"/>
+                <org.eventb.core.prHypAction name="HIDE2" org.eventb.core.prHyps="p2"/>
+                <org.eventb.core.prHypAction name="HIDE3" org.eventb.core.prHyps="p3"/>
+            </org.eventb.core.prAnte>
+        </org.eventb.core.prRule>
+        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="dom(admin)⊆USER">
+            <org.eventb.core.prIdent name="PASSWORD" org.eventb.core.type="ℙ(PASSWORD)"/>
+            <org.eventb.core.prIdent name="USER" org.eventb.core.type="ℙ(USER)"/>
+            <org.eventb.core.prIdent name="admin" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="dom(patient)⊆USER">
+            <org.eventb.core.prIdent name="PASSWORD" org.eventb.core.type="ℙ(PASSWORD)"/>
+            <org.eventb.core.prIdent name="USER" org.eventb.core.type="ℙ(USER)"/>
+            <org.eventb.core.prIdent name="patient" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="new_password∈PASSWORD">
+            <org.eventb.core.prIdent name="PASSWORD" org.eventb.core.type="ℙ(PASSWORD)"/>
+            <org.eventb.core.prIdent name="new_password" org.eventb.core.type="PASSWORD"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="dom(dentist)⊆USER">
+            <org.eventb.core.prIdent name="PASSWORD" org.eventb.core.type="ℙ(PASSWORD)"/>
+            <org.eventb.core.prIdent name="USER" org.eventb.core.type="ℙ(USER)"/>
+            <org.eventb.core.prIdent name="dentist" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.typeRewrites:1"/>
+    </org.eventb.core.prProof>
+    <org.eventb.core.prProof name="changePatientPassword/inv7/INV" org.eventb.core.confidence="0" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1" org.eventb.core.prSets="PASSWORD,USER">
+        <org.eventb.core.lang name="L"/>
+        <org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="type rewrites" org.eventb.core.prHyps="">
+            <org.eventb.core.prAnte name="'">
+                <org.eventb.core.prHypAction name="HIDE0" org.eventb.core.prHyps="p2"/>
+                <org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p3"/>
+                <org.eventb.core.prHypAction name="HIDE2" org.eventb.core.prHyps="p4"/>
+                <org.eventb.core.prHypAction name="HIDE3" org.eventb.core.prHyps="p5"/>
+                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh with registered=admin∪dentist∪patient" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1">
+                    <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p6"/>
+                </org.eventb.core.prRule>
+            </org.eventb.core.prAnte>
+        </org.eventb.core.prRule>
+        <org.eventb.core.prIdent name="admin" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        <org.eventb.core.prIdent name="dentist" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        <org.eventb.core.prIdent name="new_password" org.eventb.core.type="PASSWORD"/>
+        <org.eventb.core.prIdent name="patient" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        <org.eventb.core.prIdent name="registered" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        <org.eventb.core.prIdent name="user" org.eventb.core.type="USER"/>
+        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="registered=admin∪dentist∪patient"/>
+        <org.eventb.core.prPred name="p6" org.eventb.core.predicate="(admin∪dentist∪patient){user ↦ new_password}=admin∪dentist∪(patient{user ↦ new_password})"/>
+        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="registered{user ↦ new_password}=admin∪dentist∪(patient{user ↦ new_password})"/>
+        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="dom(admin)⊆USER"/>
+        <org.eventb.core.prPred name="p4" org.eventb.core.predicate="dom(patient)⊆USER"/>
+        <org.eventb.core.prPred name="p5" org.eventb.core.predicate="new_password∈PASSWORD"/>
+        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="dom(dentist)⊆USER"/>
+        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.typeRewrites:1"/>
+        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.eq:1"/>
+    </org.eventb.core.prProof>
+    <org.eventb.core.prProof name="changePatientPassword/inv8/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1,p2,p3,p4" org.eventb.core.prSets="PASSWORD,USER">
+        <org.eventb.core.lang name="L"/>
+        <org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="type rewrites" org.eventb.core.prHyps="">
+            <org.eventb.core.prAnte name="'">
+                <org.eventb.core.prHypAction name="HIDE0" org.eventb.core.prHyps="p5"/>
+                <org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p6"/>
+                <org.eventb.core.prHypAction name="HIDE2" org.eventb.core.prHyps="p7"/>
+                <org.eventb.core.prHypAction name="HIDE3" org.eventb.core.prHyps="p8"/>
+                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="PP" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1,p2,p3,p4">
+                    <org.eventb.core.prString name=".arg" org.eventb.core.prSValue="R500"/>
+                </org.eventb.core.prRule>
+            </org.eventb.core.prAnte>
+        </org.eventb.core.prRule>
+        <org.eventb.core.prIdent name="loggedin" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        <org.eventb.core.prIdent name="new_password" org.eventb.core.type="PASSWORD"/>
+        <org.eventb.core.prIdent name="password" org.eventb.core.type="PASSWORD"/>
+        <org.eventb.core.prIdent name="patient" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        <org.eventb.core.prIdent name="registered" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        <org.eventb.core.prIdent name="user" org.eventb.core.type="USER"/>
+        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="loggedin⊆registered"/>
+        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="user∈dom(patient)"/>
+        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="password=loggedin(user)"/>
+        <org.eventb.core.prPred name="p5" org.eventb.core.predicate="dom(admin)⊆USER">
+            <org.eventb.core.prIdent name="admin" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p4" org.eventb.core.predicate="user∈dom(loggedin)"/>
+        <org.eventb.core.prPred name="p7" org.eventb.core.predicate="dom(patient)⊆USER"/>
+        <org.eventb.core.prPred name="p8" org.eventb.core.predicate="new_password∈PASSWORD"/>
+        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="loggedin{user ↦ new_password}⊆registered{user ↦ new_password}"/>
+        <org.eventb.core.prPred name="p6" org.eventb.core.predicate="dom(dentist)⊆USER">
+            <org.eventb.core.prIdent name="dentist" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.typeRewrites:1"/>
+        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="com.clearsy.atelierb.provers.core.externalPP:1"/>
+    </org.eventb.core.prProof>
+    <org.eventb.core.prProof name="changeDentistPassword/grd1/WD" org.eventb.core.confidence="0" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="" org.eventb.core.prSets="PASSWORD,USER">
+        <org.eventb.core.lang name="L"/>
+        <org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="type rewrites" org.eventb.core.prHyps="">
+            <org.eventb.core.prAnte name="'">
+                <org.eventb.core.prHypAction name="HIDE0" org.eventb.core.prHyps="p1"/>
+                <org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p2"/>
+                <org.eventb.core.prHypAction name="HIDE2" org.eventb.core.prHyps="p3"/>
+                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="∧ goal" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
+                    <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p4"/>
+                    <org.eventb.core.prAnte name="(" org.eventb.core.prGoal="p5"/>
+                </org.eventb.core.prRule>
+            </org.eventb.core.prAnte>
+        </org.eventb.core.prRule>
+        <org.eventb.core.prIdent name="loggedin" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        <org.eventb.core.prIdent name="user" org.eventb.core.type="USER"/>
+        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="dom(admin)⊆USER">
+            <org.eventb.core.prIdent name="admin" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="dom(patient)⊆USER">
+            <org.eventb.core.prIdent name="patient" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p4" org.eventb.core.predicate="user∈dom(loggedin)"/>
+        <org.eventb.core.prPred name="p5" org.eventb.core.predicate="loggedin∈USER ⇸ PASSWORD"/>
+        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="user∈dom(loggedin)∧loggedin∈USER ⇸ PASSWORD"/>
+        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="dom(dentist)⊆USER">
+            <org.eventb.core.prIdent name="dentist" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.typeRewrites:1"/>
+        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.conj:0"/>
+    </org.eventb.core.prProof>
+    <org.eventb.core.prProof name="changeDentistPassword/inv1/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1,p2,p3,p4,p5,p6,p7,p8,p9,p10" org.eventb.core.prSets="PASSWORD,USER">
+        <org.eventb.core.lang name="L"/>
+        <org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="type rewrites" org.eventb.core.prHyps="">
+            <org.eventb.core.prAnte name="'">
+                <org.eventb.core.prHypAction name="HIDE0" org.eventb.core.prHyps="p11"/>
+                <org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p12"/>
+                <org.eventb.core.prHypAction name="HIDE2" org.eventb.core.prHyps="p13"/>
+                <org.eventb.core.prHypAction name="HIDE3" org.eventb.core.prHyps="p14"/>
+                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="ML" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p4,p10,p7,p8,p2,p3,p1,p5,p6,p9">
+                    <org.eventb.core.prString name=".arg" org.eventb.core.prSValue="0;1:500"/>
+                </org.eventb.core.prRule>
+            </org.eventb.core.prAnte>
+        </org.eventb.core.prRule>
+        <org.eventb.core.prIdent name="admin" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        <org.eventb.core.prIdent name="dentist" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        <org.eventb.core.prIdent name="loggedin" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        <org.eventb.core.prIdent name="new_password" org.eventb.core.type="PASSWORD"/>
+        <org.eventb.core.prIdent name="password" org.eventb.core.type="PASSWORD"/>
+        <org.eventb.core.prIdent name="patient" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        <org.eventb.core.prIdent name="registered" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        <org.eventb.core.prIdent name="user" org.eventb.core.type="USER"/>
+        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="user∈dom(dentist)"/>
+        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="registered=admin∪dentist∪patient"/>
+        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="loggedin⊆registered"/>
+        <org.eventb.core.prPred name="p4" org.eventb.core.predicate="admin∈USER ⇸ PASSWORD"/>
+        <org.eventb.core.prPred name="p5" org.eventb.core.predicate="password=loggedin(user)"/>
+        <org.eventb.core.prPred name="p6" org.eventb.core.predicate="user∈dom(loggedin)"/>
+        <org.eventb.core.prPred name="p7" org.eventb.core.predicate="patient∈USER ⇸ PASSWORD"/>
+        <org.eventb.core.prPred name="p9" org.eventb.core.predicate="loggedin∈USER ⇸ PASSWORD"/>
+        <org.eventb.core.prPred name="p14" org.eventb.core.predicate="new_password∈PASSWORD"/>
+        <org.eventb.core.prPred name="p12" org.eventb.core.predicate="dom(dentist)⊆USER"/>
+        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="dentist{user ↦ new_password}∈USER ⇸ PASSWORD"/>
+        <org.eventb.core.prPred name="p11" org.eventb.core.predicate="dom(admin)⊆USER"/>
+        <org.eventb.core.prPred name="p13" org.eventb.core.predicate="dom(patient)⊆USER"/>
+        <org.eventb.core.prPred name="p8" org.eventb.core.predicate="admin∩dentist∩patient=(∅ ⦂ ℙ(USER×PASSWORD))"/>
+        <org.eventb.core.prPred name="p10" org.eventb.core.predicate="dentist∈USER ⇸ PASSWORD"/>
+        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.typeRewrites:1"/>
+        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="com.clearsy.atelierb.provers.core.externalML:1"/>
+    </org.eventb.core.prProof>
+    <org.eventb.core.prProof name="changeDentistPassword/inv6/INV" org.eventb.core.confidence="0" org.eventb.core.prFresh="" org.eventb.core.prHyps="">
+        <org.eventb.core.lang name="L"/>
+        <org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="type rewrites" org.eventb.core.prHyps="">
+            <org.eventb.core.prAnte name="'">
+                <org.eventb.core.prHypAction name="HIDE0" org.eventb.core.prHyps="p0"/>
+                <org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p1"/>
+                <org.eventb.core.prHypAction name="HIDE2" org.eventb.core.prHyps="p2"/>
+                <org.eventb.core.prHypAction name="HIDE3" org.eventb.core.prHyps="p3"/>
+            </org.eventb.core.prAnte>
+        </org.eventb.core.prRule>
+        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="dom(admin)⊆USER">
+            <org.eventb.core.prIdent name="PASSWORD" org.eventb.core.type="ℙ(PASSWORD)"/>
+            <org.eventb.core.prIdent name="USER" org.eventb.core.type="ℙ(USER)"/>
+            <org.eventb.core.prIdent name="admin" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="dom(patient)⊆USER">
+            <org.eventb.core.prIdent name="PASSWORD" org.eventb.core.type="ℙ(PASSWORD)"/>
+            <org.eventb.core.prIdent name="USER" org.eventb.core.type="ℙ(USER)"/>
+            <org.eventb.core.prIdent name="patient" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="new_password∈PASSWORD">
+            <org.eventb.core.prIdent name="PASSWORD" org.eventb.core.type="ℙ(PASSWORD)"/>
+            <org.eventb.core.prIdent name="new_password" org.eventb.core.type="PASSWORD"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="dom(dentist)⊆USER">
+            <org.eventb.core.prIdent name="PASSWORD" org.eventb.core.type="ℙ(PASSWORD)"/>
+            <org.eventb.core.prIdent name="USER" org.eventb.core.type="ℙ(USER)"/>
+            <org.eventb.core.prIdent name="dentist" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.typeRewrites:1"/>
+    </org.eventb.core.prProof>
+    <org.eventb.core.prProof name="changeDentistPassword/inv7/INV" org.eventb.core.confidence="0" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1" org.eventb.core.prSets="PASSWORD,USER">
+        <org.eventb.core.lang name="L"/>
+        <org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="type rewrites" org.eventb.core.prHyps="">
+            <org.eventb.core.prAnte name="'">
+                <org.eventb.core.prHypAction name="HIDE0" org.eventb.core.prHyps="p2"/>
+                <org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p3"/>
+                <org.eventb.core.prHypAction name="HIDE2" org.eventb.core.prHyps="p4"/>
+                <org.eventb.core.prHypAction name="HIDE3" org.eventb.core.prHyps="p5"/>
+                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh with registered=admin∪dentist∪patient" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1">
+                    <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p6"/>
+                </org.eventb.core.prRule>
+            </org.eventb.core.prAnte>
+        </org.eventb.core.prRule>
+        <org.eventb.core.prIdent name="admin" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        <org.eventb.core.prIdent name="dentist" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        <org.eventb.core.prIdent name="new_password" org.eventb.core.type="PASSWORD"/>
+        <org.eventb.core.prIdent name="patient" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        <org.eventb.core.prIdent name="registered" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        <org.eventb.core.prIdent name="user" org.eventb.core.type="USER"/>
+        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="registered=admin∪dentist∪patient"/>
+        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="dom(admin)⊆USER"/>
+        <org.eventb.core.prPred name="p6" org.eventb.core.predicate="(admin∪dentist∪patient){user ↦ new_password}=admin∪(dentist{user ↦ new_password})∪patient"/>
+        <org.eventb.core.prPred name="p4" org.eventb.core.predicate="dom(patient)⊆USER"/>
+        <org.eventb.core.prPred name="p5" org.eventb.core.predicate="new_password∈PASSWORD"/>
+        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="registered{user ↦ new_password}=admin∪(dentist{user ↦ new_password})∪patient"/>
+        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="dom(dentist)⊆USER"/>
+        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.typeRewrites:1"/>
+        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.eq:1"/>
+    </org.eventb.core.prProof>
+    <org.eventb.core.prProof name="changeDentistPassword/inv8/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1,p2,p3,p4" org.eventb.core.prSets="PASSWORD,USER">
+        <org.eventb.core.lang name="L"/>
+        <org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="type rewrites" org.eventb.core.prHyps="">
+            <org.eventb.core.prAnte name="'">
+                <org.eventb.core.prHypAction name="HIDE0" org.eventb.core.prHyps="p5"/>
+                <org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p6"/>
+                <org.eventb.core.prHypAction name="HIDE2" org.eventb.core.prHyps="p7"/>
+                <org.eventb.core.prHypAction name="HIDE3" org.eventb.core.prHyps="p8"/>
+                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="PP" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p2,p1,p3,p4">
+                    <org.eventb.core.prString name=".arg" org.eventb.core.prSValue="R500"/>
+                </org.eventb.core.prRule>
+            </org.eventb.core.prAnte>
+        </org.eventb.core.prRule>
+        <org.eventb.core.prIdent name="dentist" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        <org.eventb.core.prIdent name="loggedin" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        <org.eventb.core.prIdent name="new_password" org.eventb.core.type="PASSWORD"/>
+        <org.eventb.core.prIdent name="password" org.eventb.core.type="PASSWORD"/>
+        <org.eventb.core.prIdent name="registered" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        <org.eventb.core.prIdent name="user" org.eventb.core.type="USER"/>
+        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="user∈dom(dentist)"/>
+        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="loggedin⊆registered"/>
+        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="password=loggedin(user)"/>
+        <org.eventb.core.prPred name="p5" org.eventb.core.predicate="dom(admin)⊆USER">
+            <org.eventb.core.prIdent name="admin" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p4" org.eventb.core.predicate="user∈dom(loggedin)"/>
+        <org.eventb.core.prPred name="p7" org.eventb.core.predicate="dom(patient)⊆USER">
+            <org.eventb.core.prIdent name="patient" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p8" org.eventb.core.predicate="new_password∈PASSWORD"/>
+        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="loggedin{user ↦ new_password}⊆registered{user ↦ new_password}"/>
+        <org.eventb.core.prPred name="p6" org.eventb.core.predicate="dom(dentist)⊆USER"/>
+        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.typeRewrites:1"/>
+        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="com.clearsy.atelierb.provers.core.externalPP:1"/>
+    </org.eventb.core.prProof>
+    <org.eventb.core.prProof name="changeAdminPassword/grd1/WD" org.eventb.core.confidence="0" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="" org.eventb.core.prSets="PASSWORD,USER">
+        <org.eventb.core.lang name="L"/>
+        <org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="type rewrites" org.eventb.core.prHyps="">
+            <org.eventb.core.prAnte name="'">
+                <org.eventb.core.prHypAction name="HIDE0" org.eventb.core.prHyps="p1"/>
+                <org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p2"/>
+                <org.eventb.core.prHypAction name="HIDE2" org.eventb.core.prHyps="p3"/>
+                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="∧ goal" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="">
+                    <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p4"/>
+                    <org.eventb.core.prAnte name="(" org.eventb.core.prGoal="p5"/>
+                </org.eventb.core.prRule>
+            </org.eventb.core.prAnte>
+        </org.eventb.core.prRule>
+        <org.eventb.core.prIdent name="loggedin" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        <org.eventb.core.prIdent name="user" org.eventb.core.type="USER"/>
+        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="dom(admin)⊆USER">
+            <org.eventb.core.prIdent name="admin" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="dom(patient)⊆USER">
+            <org.eventb.core.prIdent name="patient" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p4" org.eventb.core.predicate="user∈dom(loggedin)"/>
+        <org.eventb.core.prPred name="p5" org.eventb.core.predicate="loggedin∈USER ⇸ PASSWORD"/>
+        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="user∈dom(loggedin)∧loggedin∈USER ⇸ PASSWORD"/>
+        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="dom(dentist)⊆USER">
+            <org.eventb.core.prIdent name="dentist" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.typeRewrites:1"/>
+        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.conj:0"/>
+    </org.eventb.core.prProof>
+    <org.eventb.core.prProof name="changeAdminPassword/inv0/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1,p2,p3,p4,p5,p6,p7,p8,p9,p10" org.eventb.core.prSets="PASSWORD,USER">
+        <org.eventb.core.lang name="L"/>
+        <org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="type rewrites" org.eventb.core.prHyps="">
+            <org.eventb.core.prAnte name="'">
+                <org.eventb.core.prHypAction name="HIDE0" org.eventb.core.prHyps="p11"/>
+                <org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p12"/>
+                <org.eventb.core.prHypAction name="HIDE2" org.eventb.core.prHyps="p13"/>
+                <org.eventb.core.prHypAction name="HIDE3" org.eventb.core.prHyps="p14"/>
+                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="ML" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p4,p10,p7,p8,p1,p3,p2,p5,p6,p9">
+                    <org.eventb.core.prString name=".arg" org.eventb.core.prSValue="0;1:500"/>
+                </org.eventb.core.prRule>
+            </org.eventb.core.prAnte>
+        </org.eventb.core.prRule>
+        <org.eventb.core.prIdent name="admin" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        <org.eventb.core.prIdent name="dentist" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        <org.eventb.core.prIdent name="loggedin" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        <org.eventb.core.prIdent name="new_password" org.eventb.core.type="PASSWORD"/>
+        <org.eventb.core.prIdent name="password" org.eventb.core.type="PASSWORD"/>
+        <org.eventb.core.prIdent name="patient" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        <org.eventb.core.prIdent name="registered" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        <org.eventb.core.prIdent name="user" org.eventb.core.type="USER"/>
+        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="registered=admin∪dentist∪patient"/>
+        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="loggedin⊆registered"/>
+        <org.eventb.core.prPred name="p4" org.eventb.core.predicate="admin∈USER ⇸ PASSWORD"/>
+        <org.eventb.core.prPred name="p5" org.eventb.core.predicate="password=loggedin(user)"/>
+        <org.eventb.core.prPred name="p6" org.eventb.core.predicate="user∈dom(loggedin)"/>
+        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="admin{user ↦ new_password}∈USER ⇸ PASSWORD"/>
+        <org.eventb.core.prPred name="p7" org.eventb.core.predicate="patient∈USER ⇸ PASSWORD"/>
+        <org.eventb.core.prPred name="p9" org.eventb.core.predicate="loggedin∈USER ⇸ PASSWORD"/>
+        <org.eventb.core.prPred name="p14" org.eventb.core.predicate="new_password∈PASSWORD"/>
+        <org.eventb.core.prPred name="p12" org.eventb.core.predicate="dom(dentist)⊆USER"/>
+        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="user∈dom(admin)"/>
+        <org.eventb.core.prPred name="p11" org.eventb.core.predicate="dom(admin)⊆USER"/>
+        <org.eventb.core.prPred name="p13" org.eventb.core.predicate="dom(patient)⊆USER"/>
+        <org.eventb.core.prPred name="p8" org.eventb.core.predicate="admin∩dentist∩patient=(∅ ⦂ ℙ(USER×PASSWORD))"/>
+        <org.eventb.core.prPred name="p10" org.eventb.core.predicate="dentist∈USER ⇸ PASSWORD"/>
+        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.typeRewrites:1"/>
+        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="com.clearsy.atelierb.provers.core.externalML:1"/>
+    </org.eventb.core.prProof>
+    <org.eventb.core.prProof name="changeAdminPassword/inv6/INV" org.eventb.core.confidence="0" org.eventb.core.prFresh="" org.eventb.core.prHyps="">
+        <org.eventb.core.lang name="L"/>
+        <org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="type rewrites" org.eventb.core.prHyps="">
+            <org.eventb.core.prAnte name="'">
+                <org.eventb.core.prHypAction name="HIDE0" org.eventb.core.prHyps="p0"/>
+                <org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p1"/>
+                <org.eventb.core.prHypAction name="HIDE2" org.eventb.core.prHyps="p2"/>
+                <org.eventb.core.prHypAction name="HIDE3" org.eventb.core.prHyps="p3"/>
+            </org.eventb.core.prAnte>
+        </org.eventb.core.prRule>
+        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="dom(admin)⊆USER">
+            <org.eventb.core.prIdent name="PASSWORD" org.eventb.core.type="ℙ(PASSWORD)"/>
+            <org.eventb.core.prIdent name="USER" org.eventb.core.type="ℙ(USER)"/>
+            <org.eventb.core.prIdent name="admin" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="dom(patient)⊆USER">
+            <org.eventb.core.prIdent name="PASSWORD" org.eventb.core.type="ℙ(PASSWORD)"/>
+            <org.eventb.core.prIdent name="USER" org.eventb.core.type="ℙ(USER)"/>
+            <org.eventb.core.prIdent name="patient" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="new_password∈PASSWORD">
+            <org.eventb.core.prIdent name="PASSWORD" org.eventb.core.type="ℙ(PASSWORD)"/>
+            <org.eventb.core.prIdent name="new_password" org.eventb.core.type="PASSWORD"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="dom(dentist)⊆USER">
+            <org.eventb.core.prIdent name="PASSWORD" org.eventb.core.type="ℙ(PASSWORD)"/>
+            <org.eventb.core.prIdent name="USER" org.eventb.core.type="ℙ(USER)"/>
+            <org.eventb.core.prIdent name="dentist" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.typeRewrites:1"/>
+    </org.eventb.core.prProof>
+    <org.eventb.core.prProof name="changeAdminPassword/inv7/INV" org.eventb.core.confidence="0" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1" org.eventb.core.prSets="PASSWORD,USER">
+        <org.eventb.core.lang name="L"/>
+        <org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="type rewrites" org.eventb.core.prHyps="">
+            <org.eventb.core.prAnte name="'">
+                <org.eventb.core.prHypAction name="HIDE0" org.eventb.core.prHyps="p2"/>
+                <org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p3"/>
+                <org.eventb.core.prHypAction name="HIDE2" org.eventb.core.prHyps="p4"/>
+                <org.eventb.core.prHypAction name="HIDE3" org.eventb.core.prHyps="p5"/>
+                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="eh with registered=admin∪dentist∪patient" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1">
+                    <org.eventb.core.prAnte name="'" org.eventb.core.prGoal="p6"/>
+                </org.eventb.core.prRule>
+            </org.eventb.core.prAnte>
+        </org.eventb.core.prRule>
+        <org.eventb.core.prIdent name="admin" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        <org.eventb.core.prIdent name="dentist" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        <org.eventb.core.prIdent name="new_password" org.eventb.core.type="PASSWORD"/>
+        <org.eventb.core.prIdent name="patient" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        <org.eventb.core.prIdent name="registered" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        <org.eventb.core.prIdent name="user" org.eventb.core.type="USER"/>
+        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="registered=admin∪dentist∪patient"/>
+        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="dom(admin)⊆USER"/>
+        <org.eventb.core.prPred name="p4" org.eventb.core.predicate="dom(patient)⊆USER"/>
+        <org.eventb.core.prPred name="p6" org.eventb.core.predicate="(admin∪dentist∪patient){user ↦ new_password}=(admin{user ↦ new_password})∪dentist∪patient"/>
+        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="registered{user ↦ new_password}=(admin{user ↦ new_password})∪dentist∪patient"/>
+        <org.eventb.core.prPred name="p5" org.eventb.core.predicate="new_password∈PASSWORD"/>
+        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="dom(dentist)⊆USER"/>
+        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.typeRewrites:1"/>
+        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="org.eventb.core.seqprover.eq:1"/>
+    </org.eventb.core.prProof>
+    <org.eventb.core.prProof name="changeAdminPassword/inv8/INV" org.eventb.core.confidence="1000" org.eventb.core.prFresh="" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p1,p2,p3,p4" org.eventb.core.prSets="PASSWORD,USER">
+        <org.eventb.core.lang name="L"/>
+        <org.eventb.core.prRule name="r0" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="type rewrites" org.eventb.core.prHyps="">
+            <org.eventb.core.prAnte name="'">
+                <org.eventb.core.prHypAction name="HIDE0" org.eventb.core.prHyps="p5"/>
+                <org.eventb.core.prHypAction name="HIDE1" org.eventb.core.prHyps="p6"/>
+                <org.eventb.core.prHypAction name="HIDE2" org.eventb.core.prHyps="p7"/>
+                <org.eventb.core.prHypAction name="HIDE3" org.eventb.core.prHyps="p8"/>
+                <org.eventb.core.prRule name="r1" org.eventb.core.confidence="1000" org.eventb.core.prDisplay="PP" org.eventb.core.prGoal="p0" org.eventb.core.prHyps="p2,p1,p3,p4">
+                    <org.eventb.core.prString name=".arg" org.eventb.core.prSValue="R500"/>
+                </org.eventb.core.prRule>
+            </org.eventb.core.prAnte>
+        </org.eventb.core.prRule>
+        <org.eventb.core.prIdent name="admin" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        <org.eventb.core.prIdent name="loggedin" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        <org.eventb.core.prIdent name="new_password" org.eventb.core.type="PASSWORD"/>
+        <org.eventb.core.prIdent name="password" org.eventb.core.type="PASSWORD"/>
+        <org.eventb.core.prIdent name="registered" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        <org.eventb.core.prIdent name="user" org.eventb.core.type="USER"/>
+        <org.eventb.core.prPred name="p1" org.eventb.core.predicate="user∈dom(admin)"/>
+        <org.eventb.core.prPred name="p2" org.eventb.core.predicate="loggedin⊆registered"/>
+        <org.eventb.core.prPred name="p3" org.eventb.core.predicate="password=loggedin(user)"/>
+        <org.eventb.core.prPred name="p5" org.eventb.core.predicate="dom(admin)⊆USER"/>
+        <org.eventb.core.prPred name="p4" org.eventb.core.predicate="user∈dom(loggedin)"/>
+        <org.eventb.core.prPred name="p7" org.eventb.core.predicate="dom(patient)⊆USER">
+            <org.eventb.core.prIdent name="patient" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prPred name="p8" org.eventb.core.predicate="new_password∈PASSWORD"/>
+        <org.eventb.core.prPred name="p0" org.eventb.core.predicate="loggedin{user ↦ new_password}⊆registered{user ↦ new_password}"/>
+        <org.eventb.core.prPred name="p6" org.eventb.core.predicate="dom(dentist)⊆USER">
+            <org.eventb.core.prIdent name="dentist" org.eventb.core.type="ℙ(USER×PASSWORD)"/>
+        </org.eventb.core.prPred>
+        <org.eventb.core.prReas name="r0" org.eventb.core.prRID="org.eventb.core.seqprover.typeRewrites:1"/>
+        <org.eventb.core.prReas name="r1" org.eventb.core.prRID="com.clearsy.atelierb.provers.core.externalPP:1"/>
+    </org.eventb.core.prProof>
 </org.eventb.core.prFile>
diff --git a/UserManagement/UserMachine.bps b/UserManagement/UserMachine.bps
index 9ec3b693cdcb1e61f5252c7dc01ce7c2396ff8d7..678ffe0708084aef5bd0642864c3fb37f89fc672 100644
--- a/UserManagement/UserMachine.bps
+++ b/UserManagement/UserMachine.bps
@@ -1,22 +1,37 @@
 <?xml version="1.0" encoding="UTF-8" standalone="no"?>
 <org.eventb.core.psFile>
-    <org.eventb.core.psStatus name="INITIALISATION/inv0/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="49" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="INITIALISATION/inv1/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="49" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="INITIALISATION/inv2/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="49" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="INITIALISATION/inv6/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="49" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="INITIALISATION/inv7/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="49" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="INITIALISATION/inv8/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="49" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="setRootAdmins/inv0/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="49" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="setRootAdmins/inv6/INV" org.eventb.core.confidence="0" org.eventb.core.poStamp="49" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="setRootAdmins/inv7/INV" org.eventb.core.confidence="0" org.eventb.core.poStamp="49" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="setRootAdmins/inv8/INV" org.eventb.core.confidence="0" org.eventb.core.poStamp="49" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="registerNewPatient/grd3/WD" org.eventb.core.confidence="1000" org.eventb.core.poStamp="49" org.eventb.core.psBroken="true" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="registerNewPatient/inv2/INV" org.eventb.core.confidence="0" org.eventb.core.poStamp="49" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="registerNewPatient/inv6/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="49" org.eventb.core.psBroken="true" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="registerNewPatient/inv7/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="49" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="registerNewPatient/inv8/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="49" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="loginUser/grd1/WD" org.eventb.core.confidence="0" org.eventb.core.poStamp="49" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="loginUser/inv8/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="49" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="logoutUser/grd1/WD" org.eventb.core.confidence="0" org.eventb.core.poStamp="49" org.eventb.core.psManual="false"/>
-    <org.eventb.core.psStatus name="logoutUser/inv8/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="49" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="INITIALISATION/inv0/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="54" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="INITIALISATION/inv1/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="54" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="INITIALISATION/inv2/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="54" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="INITIALISATION/inv6/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="54" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="INITIALISATION/inv7/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="54" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="INITIALISATION/inv8/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="54" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="setRootAdmins/inv0/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="54" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="setRootAdmins/inv6/INV" org.eventb.core.confidence="0" org.eventb.core.poStamp="54" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="setRootAdmins/inv7/INV" org.eventb.core.confidence="0" org.eventb.core.poStamp="54" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="setRootAdmins/inv8/INV" org.eventb.core.confidence="0" org.eventb.core.poStamp="54" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="registerNewPatient/grd3/WD" org.eventb.core.confidence="1000" org.eventb.core.poStamp="54" org.eventb.core.psBroken="true" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="registerNewPatient/inv2/INV" org.eventb.core.confidence="0" org.eventb.core.poStamp="54" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="registerNewPatient/inv6/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="54" org.eventb.core.psBroken="true" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="registerNewPatient/inv7/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="54" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="registerNewPatient/inv8/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="54" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="loginUser/grd1/WD" org.eventb.core.confidence="0" org.eventb.core.poStamp="54" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="loginUser/inv8/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="54" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="logoutUser/grd1/WD" org.eventb.core.confidence="0" org.eventb.core.poStamp="54" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="logoutUser/inv8/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="54" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="changePatientPassword/grd1/WD" org.eventb.core.confidence="0" org.eventb.core.poStamp="54" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="changePatientPassword/inv2/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="54" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="changePatientPassword/inv6/INV" org.eventb.core.confidence="0" org.eventb.core.poStamp="54" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="changePatientPassword/inv7/INV" org.eventb.core.confidence="0" org.eventb.core.poStamp="54" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="changePatientPassword/inv8/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="54" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="changeDentistPassword/grd1/WD" org.eventb.core.confidence="0" org.eventb.core.poStamp="54" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="changeDentistPassword/inv1/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="54" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="changeDentistPassword/inv6/INV" org.eventb.core.confidence="0" org.eventb.core.poStamp="54" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="changeDentistPassword/inv7/INV" org.eventb.core.confidence="0" org.eventb.core.poStamp="54" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="changeDentistPassword/inv8/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="54" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="changeAdminPassword/grd1/WD" org.eventb.core.confidence="0" org.eventb.core.poStamp="54" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="changeAdminPassword/inv0/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="54" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="changeAdminPassword/inv6/INV" org.eventb.core.confidence="0" org.eventb.core.poStamp="54" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="changeAdminPassword/inv7/INV" org.eventb.core.confidence="0" org.eventb.core.poStamp="54" org.eventb.core.psManual="false"/>
+    <org.eventb.core.psStatus name="changeAdminPassword/inv8/INV" org.eventb.core.confidence="1000" org.eventb.core.poStamp="54" org.eventb.core.psManual="false"/>
 </org.eventb.core.psFile>
diff --git a/UserManagement/UserMachine.bum b/UserManagement/UserMachine.bum
index 502ecb37c6d76eb64264e2fa2e7b5484768ff7ab..9b90521ef04d7e7170fa816bead27b7d920e7bbe 100644
--- a/UserManagement/UserMachine.bum
+++ b/UserManagement/UserMachine.bum
@@ -1,59 +1,95 @@
 <?xml version="1.0" encoding="UTF-8" standalone="no"?>
 <org.eventb.core.machineFile org.eventb.core.configuration="org.eventb.core.fwd;ac.soton.xeventb.xmachine.base" org.eventb.core.generated="false" version="5">
-    <org.eventb.core.seesContext name="_8y5v0AldEe-O984l8O-k1g" org.eventb.core.target="UserContext"/>
-    <org.eventb.core.variable name="_8y5v0QldEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.identifier="admin"/>
-    <org.eventb.core.variable name="_8y5v0gldEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.identifier="dentist"/>
-    <org.eventb.core.variable name="_8y5v0wldEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.identifier="patient"/>
-    <org.eventb.core.variable name="_8y5v1AldEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.identifier="loggedin"/>
-    <org.eventb.core.variable name="_8y6W4AldEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.identifier="registered"/>
-    <org.eventb.core.invariant name="_8y6W4QldEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.label="inv0" org.eventb.core.predicate="admin ∈ USER ⇸ PASSWORD"/>
-    <org.eventb.core.invariant name="_8y6W4gldEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.label="inv1" org.eventb.core.predicate="dentist ∈ USER ⇸ PASSWORD"/>
-    <org.eventb.core.invariant name="_8y6W4wldEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.label="inv2" org.eventb.core.predicate="patient ∈ USER ⇸ PASSWORD"/>
-    <org.eventb.core.invariant name="_8y6W5AldEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.label="inv3" org.eventb.core.predicate="dom(admin) ⊆ USER"/>
-    <org.eventb.core.invariant name="_8y6W5QldEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.label="inv4" org.eventb.core.predicate="dom(dentist) ⊆ USER"/>
-    <org.eventb.core.invariant name="_8y6W5gldEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.label="inv5" org.eventb.core.predicate="dom(patient) ⊆ USER"/>
-    <org.eventb.core.invariant name="_8y6W5wldEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.label="inv6" org.eventb.core.predicate="admin ∩ dentist ∩ patient = ∅"/>
-    <org.eventb.core.invariant name="_8y6W6AldEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.label="inv7" org.eventb.core.predicate="registered = admin ∪ dentist ∪ patient"/>
-    <org.eventb.core.invariant name="_8y698AldEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.label="inv8" org.eventb.core.predicate="loggedin ⊆ registered"/>
-    <org.eventb.core.event name="_8y698QldEe-O984l8O-k1g" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="INITIALISATION">
-        <org.eventb.core.action name="_8y698gldEe-O984l8O-k1g" org.eventb.core.assignment="admin ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act0"/>
-        <org.eventb.core.action name="_8y698wldEe-O984l8O-k1g" org.eventb.core.assignment="dentist ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act1"/>
-        <org.eventb.core.action name="_8y699AldEe-O984l8O-k1g" org.eventb.core.assignment="patient ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act2"/>
-        <org.eventb.core.action name="_8y699QldEe-O984l8O-k1g" org.eventb.core.assignment="loggedin ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act3"/>
-        <org.eventb.core.action name="_8y699gldEe-O984l8O-k1g" org.eventb.core.assignment="registered ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act4"/>
-    </org.eventb.core.event>
-    <org.eventb.core.event name="_8y699wldEe-O984l8O-k1g" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="setRootAdmins">
-        <org.eventb.core.parameter name="_8y69-AldEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.identifier="root"/>
-        <org.eventb.core.parameter name="_8y69-QldEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.identifier="root_password"/>
-        <org.eventb.core.guard name="_8y69-gldEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.label="grd0" org.eventb.core.predicate="root ∈ USER"/>
-        <org.eventb.core.guard name="_8y7lAAldEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.label="grd1" org.eventb.core.predicate="root_password ∈ PASSWORD"/>
-        <org.eventb.core.guard name="_8y7lAQldEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.label="grd2" org.eventb.core.predicate="admin = ∅"/>
-        <org.eventb.core.action name="_8y7lAgldEe-O984l8O-k1g" org.eventb.core.assignment="admin ≔ {root ↦ root_password}" org.eventb.core.generated="false" org.eventb.core.label="act0"/>
-        <org.eventb.core.action name="_8y7lAwldEe-O984l8O-k1g" org.eventb.core.assignment="registered ≔ {root ↦ root_password}" org.eventb.core.generated="false" org.eventb.core.label="act1"/>
-    </org.eventb.core.event>
-    <org.eventb.core.event name="_8y7lBAldEe-O984l8O-k1g" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="registerNewPatient">
-        <org.eventb.core.parameter name="_8y7lBQldEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.identifier="new_patient"/>
-        <org.eventb.core.parameter name="_8y7lBgldEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.identifier="new_patient_password"/>
-        <org.eventb.core.guard name="_8y7lBwldEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.label="grd0" org.eventb.core.predicate="new_patient ∈ USER"/>
-        <org.eventb.core.guard name="_8y7lCAldEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.label="grd1" org.eventb.core.predicate="new_patient_password ∈ PASSWORD"/>
-        <org.eventb.core.guard name="_8y7lCQldEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.label="grd2" org.eventb.core.predicate="new_patient ∉ dom(registered)"/>
-        <org.eventb.core.guard name="_8y7lCgldEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.label="grd3" org.eventb.core.predicate="card(admin) &gt; 0"/>
-        <org.eventb.core.action name="_8y7lCwldEe-O984l8O-k1g" org.eventb.core.assignment="patient ≔ patient ∪ {new_patient ↦ new_patient_password}" org.eventb.core.generated="false" org.eventb.core.label="act1"/>
-        <org.eventb.core.action name="_8y7lDAldEe-O984l8O-k1g" org.eventb.core.assignment="registered ≔ registered ∪ {new_patient ↦ new_patient_password}" org.eventb.core.generated="false" org.eventb.core.label="act2"/>
-    </org.eventb.core.event>
-    <org.eventb.core.event name="_8y7lDQldEe-O984l8O-k1g" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="loginUser">
-        <org.eventb.core.parameter name="_8y8MEAldEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.identifier="user"/>
-        <org.eventb.core.parameter name="_8y8MEQldEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.identifier="user_password"/>
-        <org.eventb.core.guard name="_8y8MEgldEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.label="grd0" org.eventb.core.predicate="user ∈ dom(registered)"/>
-        <org.eventb.core.guard name="_8y8MEwldEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.label="grd1" org.eventb.core.predicate="user_password = registered(user)"/>
-        <org.eventb.core.guard name="_8y8MFAldEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.label="grd2" org.eventb.core.predicate="user ∉ dom(loggedin)"/>
-        <org.eventb.core.action name="_8y8MFQldEe-O984l8O-k1g" org.eventb.core.assignment="loggedin ≔ loggedin ∪ {user ↦ user_password}" org.eventb.core.generated="false" org.eventb.core.label="act0"/>
-    </org.eventb.core.event>
-    <org.eventb.core.event name="_8y8MFgldEe-O984l8O-k1g" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="logoutUser">
-        <org.eventb.core.parameter name="_8y8MFwldEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.identifier="user"/>
-        <org.eventb.core.parameter name="_8y8MGAldEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.identifier="password"/>
-        <org.eventb.core.guard name="_8y8MGQldEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.label="grd0" org.eventb.core.predicate="user ∈ dom(loggedin)"/>
-        <org.eventb.core.guard name="_8y8MGgldEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.label="grd1" org.eventb.core.predicate="password = loggedin(user)"/>
-        <org.eventb.core.action name="_8y8MGwldEe-O984l8O-k1g" org.eventb.core.assignment="loggedin ≔ loggedin ∖ {user ↦ password}" org.eventb.core.generated="false" org.eventb.core.label="act0"/>
+    <org.eventb.core.seesContext name="_Qg7ZUArBEe-O984l8O-k1g" org.eventb.core.target="UserContext"/>
+    <org.eventb.core.variable name="_Qg8AYArBEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.identifier="admin"/>
+    <org.eventb.core.variable name="_Qg8AYQrBEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.identifier="dentist"/>
+    <org.eventb.core.variable name="_Qg8AYgrBEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.identifier="patient"/>
+    <org.eventb.core.variable name="_Qg8AYwrBEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.identifier="loggedin"/>
+    <org.eventb.core.variable name="_Qg8AZArBEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.identifier="registered"/>
+    <org.eventb.core.invariant name="_Qg8AZQrBEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.label="inv0" org.eventb.core.predicate="admin ∈ USER ⇸ PASSWORD"/>
+    <org.eventb.core.invariant name="_Qg8AZgrBEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.label="inv1" org.eventb.core.predicate="dentist ∈ USER ⇸ PASSWORD"/>
+    <org.eventb.core.invariant name="_Qg8AZwrBEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.label="inv2" org.eventb.core.predicate="patient ∈ USER ⇸ PASSWORD"/>
+    <org.eventb.core.invariant name="_Qg8AaArBEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.label="inv3" org.eventb.core.predicate="dom(admin) ⊆ USER"/>
+    <org.eventb.core.invariant name="_Qg8AaQrBEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.label="inv4" org.eventb.core.predicate="dom(dentist) ⊆ USER"/>
+    <org.eventb.core.invariant name="_Qg8AagrBEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.label="inv5" org.eventb.core.predicate="dom(patient) ⊆ USER"/>
+    <org.eventb.core.invariant name="_Qg8AawrBEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.label="inv6" org.eventb.core.predicate="admin ∩ dentist ∩ patient = ∅"/>
+    <org.eventb.core.invariant name="_Qg8ncArBEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.label="inv7" org.eventb.core.predicate="registered = admin ∪ dentist ∪ patient"/>
+    <org.eventb.core.invariant name="_Qg8ncQrBEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.label="inv8" org.eventb.core.predicate="loggedin ⊆ registered"/>
+    <org.eventb.core.event name="_Qg8ncgrBEe-O984l8O-k1g" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="INITIALISATION">
+        <org.eventb.core.action name="_Qg8ncwrBEe-O984l8O-k1g" org.eventb.core.assignment="admin ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act0"/>
+        <org.eventb.core.action name="_Qg8ndArBEe-O984l8O-k1g" org.eventb.core.assignment="dentist ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act1"/>
+        <org.eventb.core.action name="_Qg8ndQrBEe-O984l8O-k1g" org.eventb.core.assignment="patient ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act2"/>
+        <org.eventb.core.action name="_Qg8ndgrBEe-O984l8O-k1g" org.eventb.core.assignment="loggedin ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act3"/>
+        <org.eventb.core.action name="_Qg8ndwrBEe-O984l8O-k1g" org.eventb.core.assignment="registered ≔ ∅" org.eventb.core.generated="false" org.eventb.core.label="act4"/>
+    </org.eventb.core.event>
+    <org.eventb.core.event name="_Qg8neArBEe-O984l8O-k1g" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="setRootAdmins">
+        <org.eventb.core.parameter name="_Qg8neQrBEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.identifier="root"/>
+        <org.eventb.core.parameter name="_Qg8negrBEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.identifier="root_password"/>
+        <org.eventb.core.guard name="_Qg8newrBEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.label="grd0" org.eventb.core.predicate="root ∈ USER"/>
+        <org.eventb.core.guard name="_Qg8nfArBEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.label="grd1" org.eventb.core.predicate="root_password ∈ PASSWORD"/>
+        <org.eventb.core.guard name="_Qg9OgArBEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.label="grd2" org.eventb.core.predicate="admin = ∅"/>
+        <org.eventb.core.action name="_Qg9OgQrBEe-O984l8O-k1g" org.eventb.core.assignment="admin ≔ {root ↦ root_password}" org.eventb.core.generated="false" org.eventb.core.label="act0"/>
+        <org.eventb.core.action name="_Qg9OggrBEe-O984l8O-k1g" org.eventb.core.assignment="registered ≔ {root ↦ root_password}" org.eventb.core.generated="false" org.eventb.core.label="act1"/>
+    </org.eventb.core.event>
+    <org.eventb.core.event name="_Qg9OgwrBEe-O984l8O-k1g" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="registerNewPatient">
+        <org.eventb.core.parameter name="_Qg9OhArBEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.identifier="new_patient"/>
+        <org.eventb.core.parameter name="_Qg9OhQrBEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.identifier="new_patient_password"/>
+        <org.eventb.core.guard name="_Qg9OhgrBEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.label="grd0" org.eventb.core.predicate="new_patient ∈ USER"/>
+        <org.eventb.core.guard name="_Qg9OhwrBEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.label="grd1" org.eventb.core.predicate="new_patient_password ∈ PASSWORD"/>
+        <org.eventb.core.guard name="_Qg9OiArBEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.label="grd2" org.eventb.core.predicate="new_patient ∉ dom(registered)"/>
+        <org.eventb.core.guard name="_Qg9OiQrBEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.label="grd3" org.eventb.core.predicate="card(admin) &gt; 0"/>
+        <org.eventb.core.action name="_Qg9OigrBEe-O984l8O-k1g" org.eventb.core.assignment="patient ≔ patient ∪ {new_patient ↦ new_patient_password}" org.eventb.core.generated="false" org.eventb.core.label="act1"/>
+        <org.eventb.core.action name="_Qg9OiwrBEe-O984l8O-k1g" org.eventb.core.assignment="registered ≔ registered ∪ {new_patient ↦ new_patient_password}" org.eventb.core.generated="false" org.eventb.core.label="act2"/>
+    </org.eventb.core.event>
+    <org.eventb.core.event name="_Qg9OjArBEe-O984l8O-k1g" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="loginUser">
+        <org.eventb.core.parameter name="_Qg91kArBEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.identifier="user"/>
+        <org.eventb.core.parameter name="_Qg91kQrBEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.identifier="user_password"/>
+        <org.eventb.core.guard name="_Qg91kgrBEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.label="grd0" org.eventb.core.predicate="user ∈ dom(registered)"/>
+        <org.eventb.core.guard name="_Qg91kwrBEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.label="grd1" org.eventb.core.predicate="user_password = registered(user)"/>
+        <org.eventb.core.guard name="_Qg91lArBEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.label="grd2" org.eventb.core.predicate="user ∉ dom(loggedin)"/>
+        <org.eventb.core.action name="_Qg91lQrBEe-O984l8O-k1g" org.eventb.core.assignment="loggedin ≔ loggedin ∪ {user ↦ user_password}" org.eventb.core.generated="false" org.eventb.core.label="act0"/>
+    </org.eventb.core.event>
+    <org.eventb.core.event name="_Qg91lgrBEe-O984l8O-k1g" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="logoutUser">
+        <org.eventb.core.parameter name="_Qg91lwrBEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.identifier="user"/>
+        <org.eventb.core.parameter name="_Qg91mArBEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.identifier="password"/>
+        <org.eventb.core.guard name="_Qg91mQrBEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.label="grd0" org.eventb.core.predicate="user ∈ dom(loggedin)"/>
+        <org.eventb.core.guard name="_Qg91mgrBEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.label="grd1" org.eventb.core.predicate="password = loggedin(user)"/>
+        <org.eventb.core.action name="_Qg91mwrBEe-O984l8O-k1g" org.eventb.core.assignment="loggedin ≔ loggedin ∖ {user ↦ password}" org.eventb.core.generated="false" org.eventb.core.label="act0"/>
+    </org.eventb.core.event>
+    <org.eventb.core.event name="_Qg91nArBEe-O984l8O-k1g" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="changePatientPassword">
+        <org.eventb.core.parameter name="_Qg-coArBEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.identifier="user"/>
+        <org.eventb.core.parameter name="_Qg-coQrBEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.identifier="password"/>
+        <org.eventb.core.parameter name="_Qg-cogrBEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.identifier="new_password"/>
+        <org.eventb.core.guard name="_Qg-cowrBEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.label="grd0" org.eventb.core.predicate="user ∈ dom(patient)"/>
+        <org.eventb.core.guard name="_Qg-cpArBEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.label="grd1" org.eventb.core.predicate="password = loggedin(user)"/>
+        <org.eventb.core.guard name="_Qg-cpQrBEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.label="grd2" org.eventb.core.predicate="new_password ∈ PASSWORD"/>
+        <org.eventb.core.guard name="_Qg-cpgrBEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.label="grd3" org.eventb.core.predicate="user ∈ dom(loggedin)"/>
+        <org.eventb.core.action name="_Qg-cpwrBEe-O984l8O-k1g" org.eventb.core.assignment="loggedin ≔ loggedin  {user ↦ new_password}" org.eventb.core.generated="false" org.eventb.core.label="act0"/>
+        <org.eventb.core.action name="_Qg-cqArBEe-O984l8O-k1g" org.eventb.core.assignment="registered ≔ registered  {user ↦ new_password}" org.eventb.core.generated="false" org.eventb.core.label="act1"/>
+        <org.eventb.core.action name="_Qg-cqQrBEe-O984l8O-k1g" org.eventb.core.assignment="patient ≔ patient  {user ↦ new_password}" org.eventb.core.generated="false" org.eventb.core.label="act2"/>
+    </org.eventb.core.event>
+    <org.eventb.core.event name="_Qg-cqgrBEe-O984l8O-k1g" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="changeDentistPassword">
+        <org.eventb.core.parameter name="_Qg-cqwrBEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.identifier="user"/>
+        <org.eventb.core.parameter name="_Qg-crArBEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.identifier="password"/>
+        <org.eventb.core.parameter name="_Qg-crQrBEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.identifier="new_password"/>
+        <org.eventb.core.guard name="_Qg_DsArBEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.label="grd0" org.eventb.core.predicate="user ∈ dom(dentist)"/>
+        <org.eventb.core.guard name="_Qg_DsQrBEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.label="grd1" org.eventb.core.predicate="password = loggedin(user)"/>
+        <org.eventb.core.guard name="_Qg_DsgrBEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.label="grd2" org.eventb.core.predicate="new_password ∈ PASSWORD"/>
+        <org.eventb.core.guard name="_Qg_DswrBEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.label="grd3" org.eventb.core.predicate="user ∈ dom(loggedin)"/>
+        <org.eventb.core.action name="_Qg_DtArBEe-O984l8O-k1g" org.eventb.core.assignment="loggedin ≔ loggedin  {user ↦ new_password}" org.eventb.core.generated="false" org.eventb.core.label="act0"/>
+        <org.eventb.core.action name="_Qg_DtQrBEe-O984l8O-k1g" org.eventb.core.assignment="registered ≔ registered  {user ↦ new_password}" org.eventb.core.generated="false" org.eventb.core.label="act1"/>
+        <org.eventb.core.action name="_Qg_DtgrBEe-O984l8O-k1g" org.eventb.core.assignment="dentist ≔ dentist  {user ↦ new_password}" org.eventb.core.generated="false" org.eventb.core.label="act2"/>
+    </org.eventb.core.event>
+    <org.eventb.core.event name="_Qg_DtwrBEe-O984l8O-k1g" org.eventb.core.convergence="0" org.eventb.core.extended="false" org.eventb.core.generated="false" org.eventb.core.label="changeAdminPassword">
+        <org.eventb.core.parameter name="_Qg_DuArBEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.identifier="user"/>
+        <org.eventb.core.parameter name="_Qg_DuQrBEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.identifier="password"/>
+        <org.eventb.core.parameter name="_Qg_DugrBEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.identifier="new_password"/>
+        <org.eventb.core.guard name="_Qg_DuwrBEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.label="grd0" org.eventb.core.predicate="user ∈ dom(admin)"/>
+        <org.eventb.core.guard name="_Qg_DvArBEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.label="grd1" org.eventb.core.predicate="password = loggedin(user)"/>
+        <org.eventb.core.guard name="_Qg_qwArBEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.label="grd2" org.eventb.core.predicate="new_password ∈ PASSWORD"/>
+        <org.eventb.core.guard name="_Qg_qwQrBEe-O984l8O-k1g" org.eventb.core.generated="false" org.eventb.core.label="grd3" org.eventb.core.predicate="user ∈ dom(loggedin)"/>
+        <org.eventb.core.action name="_Qg_qwgrBEe-O984l8O-k1g" org.eventb.core.assignment="loggedin ≔ loggedin  {user ↦ new_password}" org.eventb.core.generated="false" org.eventb.core.label="act0"/>
+        <org.eventb.core.action name="_Qg_qwwrBEe-O984l8O-k1g" org.eventb.core.assignment="registered ≔ registered  {user ↦ new_password}" org.eventb.core.generated="false" org.eventb.core.label="act1"/>
+        <org.eventb.core.action name="_Qg_qxArBEe-O984l8O-k1g" org.eventb.core.assignment="admin ≔ admin  {user ↦ new_password}" org.eventb.core.generated="false" org.eventb.core.label="act2"/>
     </org.eventb.core.event>
 </org.eventb.core.machineFile>
diff --git a/UserManagement/UserMachine.bumx b/UserManagement/UserMachine.bumx
index a922e8b270e17f6a0109bd7d823af9527a1a3f89..bf6cd4fcef54dfc7de654de6ddd4b45321530ce8 100644
--- a/UserManagement/UserMachine.bumx
+++ b/UserManagement/UserMachine.bumx
@@ -114,4 +114,68 @@ events
 		@act0: loggedin ≔ loggedin ∖ {user ↦ password}
 	end
 	
+	/*
+	 * REQ11
+	 * A logged in user can change their password
+	 */
+	event changePatientPassword
+	any
+		user
+		password
+		new_password
+	where
+		@grd0: user ∈ dom(patient)
+		@grd1: password = loggedin(user)
+		@grd2: new_password ∈ PASSWORD
+		@grd3: user ∈ dom(loggedin) // Patient must be logged in
+	then
+		@act0: loggedin ≔ loggedin  {user ↦ new_password}
+		@act1: registered ≔ registered  {user ↦ new_password}
+		@act2: patient ≔ patient  {user ↦ new_password}
+	end
+	
+	
+	/*
+	 * REQ11
+	 * A logged in user can change their password
+	 */
+	event changeDentistPassword
+	any
+		user
+		password
+		new_password
+	where
+		@grd0: user ∈ dom(dentist)
+		@grd1: password = loggedin(user)
+		@grd2: new_password ∈ PASSWORD
+		@grd3: user ∈ dom(loggedin) // Patient must be logged in
+	then
+		@act0: loggedin ≔ loggedin  {user ↦ new_password}
+		@act1: registered ≔ registered  {user ↦ new_password}
+		@act2: dentist ≔ dentist  {user ↦ new_password}
+	end
+	
+	/*
+	 * REQ11
+	 * A logged in user can change their password
+	 */
+	event changeAdminPassword
+	any
+		user
+		password
+		new_password
+	where
+		@grd0: user ∈ dom(admin)
+		@grd1: password = loggedin(user)
+		@grd2: new_password ∈ PASSWORD
+		@grd3: user ∈ dom(loggedin) // Patient must be logged in
+	then
+		@act0: loggedin ≔ loggedin  {user ↦ new_password}
+		@act1: registered ≔ registered  {user ↦ new_password}
+		@act2: admin ≔ admin  {user ↦ new_password}
+	end
+
+	
+		
+	
 end