Implementing a Calculus for Distributed Access Control in Higher Order Logic and HOL - Computer Network Security - page 46

val P4AssocThm =
∀P Q R World w0 Ifn Jfn w1.
(( World,w0,Ifn,Jfn),w1) MD
((( P meet Q) meet R) eqp ( P meet Q meet R)) : thm
val P4CommuThm =
∀P Q World w0 Ifn Jfn w1.
(( World,w0,Ifn,Jfn),w1) MD (( P meet Q) eqp ( Q meet P)) : thm
val P4IdemThm =
∀P World w0 Ifn Jfn w1.
(( World,w0,Ifn,Jfn),w1) MD (( P meet P) eqp P) : thm
val P5Thm =
∀P Q R World w0 Ifn Jfn w1.
(( World,w0,Ifn,Jfn),w1) MD
((( P quoting Q) quoting R) eqp ( P quoting Q quoting R)) : thm
val P6LeftThm =
∀P Q R World w0 Ifn Jfn w1.
(( World,w0,Ifn,Jfn),w1) MD
(( P quoting Q meet R) eqp (( P quoting Q) meet P quoting R)) : thm
val P6RightThm =
∀P Q R World w0 Ifn Jfn w1.
(( World,w0,Ifn,Jfn),w1) MD
((( Q meet R) quoting P) eqp (( Q quoting P) meet R quoting P)) : thm
val P7Thm =
∀P Q World w0 Ifn Jfn w1.
(( World,w0,Ifn,Jfn),w1) MD
(( P speaks˙for Q) eqs P eqp ( P meet Q)) : thm
val P8Thm =
∀P Q s World w0 Ifn Jfn w1.
(( World,w0,Ifn,Jfn),w1) MD
(( P speaks˙for Q) imps ( P says s) imps Q says s) : thm
val P9Thm =
∀P Q World w0 Ifn Jfn w1.
(( World,w0,Ifn,Jfn),w1) MD
(( P eqp Q) eqs ( P speaks˙for Q) ands Q speaks˙for P) : thm
val P12Thm =
∀PQP World w0 Ifn Jfn w1.
(( World,w0,Ifn,Jfn),w1) MD
(((( P meet Q) speaks˙for P) ands Q speaks˙for P ) imps
Q speaks˙for P) : thm