(* RT^D backchaining spec. *)

(* core types *)
entity : type.
role_name : type.
role_expr : type.

(* role expression constructors *)
^ : entity -> role_expr.
role : entity -> role_name -> role_expr.
linked_role : entity -> role_name -> role_name -> role_expr.
inter : list role_expr -> role_expr.

(* credentials are facts *)
credential : entity -> role_name -> role_expr -> o.

delegation : entity -> entity -> role_expr -> entity -> o.

(* role membership predicates *)
for_role : entity -> entity -> role_expr -> o.
for_roles : entity -> entity -> list role_expr -> o.

delegation B1 D (role A R) B2,
for_role B1 D (role A R) =>
{!(for_role B2 D (role A R))}.

credential A R (^ B) =>
{!(for_role B B (role A R))}.

credential A R0 (role B R1),
for_role D E (role B R1) =>
{!(for_role D E (role A R0))}. 

credential A R0 (linked_role B R1 R2),
for_role A0 A0 (role B R1),
for_role D E (role A0 R2) =>
{!(for_role D E (role A R0))}.

credential A R (inter Res),
for_roles D E Res =>
{!(for_role D E (role A R))}.

for_roles D E nil.
for_roles D E (role A R::Res) <=
  (for_role D E (role A R),
   for_roles D E Res).