(R1.1.1)

canActivate(mgr, Register-RA-manager(mgr2)) <-
hasActivated(mgr, RA-manager()),
RA-manager-regs(n, mgr2),
n=0

(R1.1.2)

canDeactivate(mgr, x, Register-RA-manager(mgr2)) <-
hasActivated(mgr, RA-manager())

(R1.1.3)

RA-manager-regs(count<x>, mgr) <-
hasActivated(x, Register-RA-manager(mgr))

(R1.1.4)

canActivate(mgr, RA-manager()) <-
hasActivated(x, Register-RA-manager(mgr))

(R1.1.5)

canDeactivate(mgr, mgr, RA-manager()) <-

(R1.1.6)

isDeactivated(mgr, RA-manager()) <-
isDeactivated(x, Register-RA-manager(mgr))

(R1.2.1)

canReqCred(x, "NHS".hasActivated(x, NHS-registration-authority(ra, start, end))) <-
ra = "RA-ADB"

(R1.2.2)

canActivate(srv, NHS-service()) <-
canActivate(srv, Registration-authority())

(R1.2.3)

canActivate(srv, NHS-service()) <-
srv = "Spine"

(R1.2.4)

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

(R1.2.5)

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

(R2.1.1)

canActivate(mgr, NHS-clinician-cert(org, cli, spcty, start, end)) <-
hasActivated(mgr, RA-manager()),
hasActivated(y, NHS-health-org-cert(org, start2, end2)),
start in [start2, end2], end in [start2, end2], start < end

(R2.1.2)

canDeactivate(mgr, x, NHS-clinician-cert(org, cli, spcty, start, end)) <-
hasActivated(mgr, RA-manager())

(R2.1.3)

isDeactivated(mgr, NHS-clinician-cert(org, cli, spcty, start, end)) <-
isDeactivated(x, NHS-health-org-cert(org, start2, end2)),
other-NHS-health-org-regs(n, x, org, start2, end2),
n = 0,
start in [start2, end2], end in [start2, end2], start < end

(R2.1.4)

canReqCred(e, "RA-ADB".hasActivated(x, NHS-clinician-cert(org, cli, spcty, start, end))) <-
hasActivated(y, NHS-health-org-cert(org, start2, end2)),
e=org,
Current-time() in [start2, end2]

(R2.1.5)

canReqCred(e, "RA-ADB".hasActivated(x, NHS-clinician-cert(org, cli, spcty, start, end))) <-
canActivate(e, NHS-service())

(R2.1.6)

canReqCred(e, "RA-ADB".hasActivated(x,
NHS-clinician-cert(org, cli, spcty, start, end))) <-
e=cli

(R2.2.1)

canActivate(mgr, NHS-Caldicott-guardian-cert(org, cg, start, end)) <-
hasActivated(mgr, RA-manager()),
hasActivated(x, NHS-health-org-cert(org, start2, end2)),
start in [start2, end2], end in [start2, end2], start < end

(R2.2.2)

canDeactivate(mgr, x, NHS-Caldicott-guardian-cert(org, cg, start, end)) <-
hasActivated(mgr, RA-manager())

(R2.2.3)

isDeactivated(mgr, NHS-Caldicott-guardian-cert(org, cg, start, end)) <-
isDeactivated(x, NHS-health-org-cert(org, start2, end2)),
other-NHS-health-org-regs(n, x, org, start2, end2),
start in [start2, end2], end in [start2, end2], start < end,
n=0

(R2.2.4)

canReqCred(e, "RA-ADB".hasActivated(x,
NHS-Caldicott-guardian-cert(org, cg, start, end))) <-
e=cg

(R2.2.5)

canReqCred(e, "RA-ADB".hasActivated(x,
NHS-Caldicott-guardian-cert(org, cg, start, end))) <-
hasActivated(y, NHS-health-org-cert(org, start2, end2)),
e=org,
Current-time() in [start2, end2]

(R2.2.6)

canReqCred(e, "RA-ADB".hasActivated(x,
NHS-Caldicott-guardian-cert(org, cg, start, end))) <-
canActivate(e, NHS-service())

(R2.3.1)

canActivate(mgr, NHS-health-org-cert(org, start, end)) <-
hasActivated(mgr, RA-manager())

(R2.3.2)

canDeactivate(mgr, x, NHS-health-org-cert(org, start, end)) <-
hasActivated(mgr, RA-manager())

(R2.3.3i)

other-NHS-health-org-regs(count<y>, x, org, start, end) <-
hasActivated(y, NHS-health-org-cert(org, start2, end2)),
start in [start2, end2], end in [start2, end2], start<end,
x != y

(R2.3.3ii)
other-NHS-health-org-regs(count<y>, x, org, start, end) <-
hasActivated(y, NHS-health-org-cert(org, start2, end2)),
start in [start2, end2], end in [start2, end2], start<end,
start != start2

(R2.3.3iii)
other-NHS-health-org-regs(count<y>, x, org, start, end) <-
hasActivated(y, NHS-health-org-cert(org, start2, end2)),
start in [start2, end2], end in [start2, end2], start<end,
end != end2

(R2.3.4)

canReqCred(e, "RA-ADB".hasActivated(x,
NHS-health-org-cert(org, start, end))) <-
hasActivated(y, NHS-Caldicott-guardian-cert(org, cg, start2, end2)),
Current-time() in [start2, end2],
e=cg

(R2.3.5)

canReqCred(e, "RA-ADB".hasActivated(x,
NHS-health-org-cert(org, start, end))) <-
hasActivated(y, NHS-clinician-cert(org, cli, spcty, start2, end2)),
Current-time() in [start2, end2],
e=cli

(R2.3.6)

canReqCred(e, "RA-ADB".hasActivated(x,
NHS-health-org-cert(org, start, end))) <-
e = org

(R2.3.7)

canReqCred(e, "RA-ADB".hasActivated(x,
NHS-health-org-cert(org2, start, end))) <-
ra.hasActivated(y, NHS-health-org-cert(org, start2, end2)),
canActivate(ra, Registration-authority()),
e=org

(R2.3.8)

canReqCred(e, "RA-ADB".hasActivated(x,
NHS-health-org-cert(org2, start, end))) <-
org@ra.hasActivated(y, NHS-health-org-cert(org, start2, end2)),
canActivate(ra, Registration-authority()),
e=org

(R2.3.9)

canReqCred(e, "RA-ADB".hasActivated(x,
NHS-health-org-cert(org, start, end))) <-
canActivate(e, NHS-service())

(R3.1.1)

canActivate(cli, Workgroup-member(org, group, spcty)) <-
hasActivated(x, NHS-health-org-cert(org, start, end)),
org@org.hasActivated(x, Register-team-member(cli, group, spcty)),
Current-time() in [start, end]

(R3.1.2)

canActivate(cli, Workgroup-member(org, group, spcty)) <-
hasActivated(x, NHS-health-org-cert(org, start, end)),
org@org.hasActivated(x, Register-ward-member(cli, group, spcty)),
Current-time() in [start, end]

(R3.1.3)

canReqCred(spine, "RA-ADB".canActivate(cli,Workgroup-member(org, group, spcty))) <-
spine = "Spine"