(P1.1.1)

canActivate(adm, PDS-manager()) <-
hasActivated(x, Register-PDS-manager(adm)),
no-main-role-active(adm)

(P1.1.2)

canDeactivate(adm, adm, PDS-manager()) <-

(P1.1.3)

isDeactivated(adm, PDS-manager()) <-
isDeactivated(x, Register-PDS-manager(adm))

(P1.1.4)

count-PDS-manager-activations(count<u>, user) <-
hasActivated(u, PDS-manager()),
u = user

(P1.1.5)

canActivate(adm1, Register-PDS-manager(adm2)) <-
hasActivated(adm1, PDS-manager()),
pds-admin-regs(n, adm2),
n=0

(P1.1.6)

canDeactivate(adm1, x, Register-PDS-manager(adm2)) <-
hasActivated(adm1, PDS-manager())
(P1.1.7)

pds-admin-regs(count<x>, adm) <-
hasActivated(x, Register-PDS-manager(adm))

(P1.2.1)

canActivate(pat, Patient()) <-
hasActivated(x, Register-patient(pat)),
no-main-role-active(pat)

(P1.2.2)

canDeactivate(pat, pat, Patient()) <-

(P1.2.3)

isDeactivated(pat, Patient()) <-
isDeactivated(x, Register-patient(pat))

(P1.2.4)

count-patient-activations(count<u>, user) <-
hasActivated(u, Patient()),
u = user

(P1.3.1)

canActivate(ag, Agent(pat)) <-
hasActivated(x, Register-patient(ag)),
no-main-role-active(ag),
"Spine"@"Spine".canActivate(ag, Agent(pat))

(P1.3.2)

canDeactivate(ag, ag, Agent(pat)) <-

(P1.3.3)

isDeactivated(ag, Agent(pat)) <-
isDeactivated(x, Register-patient(ag))

(P1.3.4)

isDeactivated(ag, Agent(pat)) <-
isDeactivated(x, Register-patient(pat))

(P1.3.5)

count-agent-activations(count<u>, user) <-
hasActivated(u, Agent(pat)),
u = user

(P1.4.1)

canActivate(x, Professional-user(ra, org)) <-
no-main-role-active(cli),
ra.hasActivated(x, NHS-clinician-cert(org, cli, spcty, start, end)),
canActivate(ra, Registration-authority()),
Current-time() in [start, end]

(P1.4.2)

canActivate(x, Professional-user(ra, org)) <-
no-main-role-active(cli),
ra@ra.hasActivated(x, NHS-clinician-cert(org, cli, spcty, start, end)),
canActivate(ra, Registration-authority()),
Current-time() in [start, end]

(P1.4.3)

canActivate(x, Professional-user(ra, org)) <-
no-main-role-active(cg),
ra.hasActivated(x, NHS-Caldicott-guardian-cert(org, cg, start, end)),
canActivate(ra, Registration-authority()),
Current-time() in [start, end]

(P1.4.4)

canActivate(x, Professional-user(ra, org)) <-
no-main-role-active(cg),
ra@ra.hasActivated(x, NHS-Caldicott-guardian-cert(org, cg, start, end)),
canActivate(ra, Registration-authority()),
Current-time() in [start, end]

(P1.4.5)

canDeactivate(x, x, Professional-user(ra, org)) <-
(P1.4.6)

count-professional-user-activations(count<u>, user) <-
hasActivated(u, Professional-user(ra, org)),
u = user

(P1.5.1)

no-main-role-active(user) <-
count-agent-activations(n, user),
count-patient-activations(n, user),
count-PDS-manager-activations(n, user),
count-professional-user-activations(n, user),
n=0

(P1.5.2)

canActivate(ra, Registration-authority()) <-
"NHS".hasActivated(x, NHS-registration-authority(ra, start, end)),
Current-time() in [start, end]

(P1.5.3)

canActivate(ra, Registration-authority()) <-
ra@"NHS".hasActivated(x, NHS-registration-authority(ra, start, end)),
Current-time() in [start, end]

(P2.1.1)

canActivate(adm, Register-patient(pat)) <-
hasActivated(adm, PDS-manager()),
patient-regs(n, pat),
n=0

(P2.1.2)

canDeactivate(adm, x, Register-patient(pat)) <-
hasActivated(adm, PDS-manager())

(P2.1.3)

patient-regs(count<x>, pat) <-
hasActivated(x, Register-patient(pat))

(P2.2.1)

canReqCred(pat, "PDS".hasActivated(x, Register-patient(pat))) <-
hasActivated(pat, Patient())

(P2.2.2)

canReqCred(ag, "PDS".hasActivated(x, Register-patient(pat))) <-
hasActivated(ag, Agent(pat))

(P2.2.3)

canReqCred(usr, "PDS".hasActivated(x, Register-patient(pat))) <-
hasActivated(usr, Professional-user(ra, org))

(P2.2.4)

canReqCred(org, "PDS".hasActivated(x, Register-patient(pat))) <-
ra.hasActivated(x, NHS-health-org-cert(org, start, end)),
canActivate(ra, Registration-authority())

(P2.2.5)

canReqCred(org, "PDS".hasActivated(x, Register-patient(pat))) <-
org@ra.hasActivated(x, NHS-health-org-cert(org, start, end)),
canActivate(ra, Registration-authority())

(P2.2.5)

canReqCred(ra, "PDS".hasActivated(x, Register-patient(pat))) <-
canActivate(ra, Registration-authority())

(P2.2.5)

canReqCred(spine, "PDS".hasActivated(x, Register-patient(pat))) <-
spine="Spine"