Information Technology Reference
In-Depth Information
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