# definition of boole algebra

# definition of or

{:t = {:a :or :b}. :a :value :True.} log:implies {:t :value :True};
log:forAll :t, :a, :b.
{:t = {:a :or :b}. :b :value :True.} log:implies {:t :value :True};
log:forAll :t, :a, :b.
{:t = {:a :or :b}. :a :value :False. :b :value :False} log:implies
 {:t :value :False};log:forAll :t, :a, :b.

# definition of and

{:t = {:a :and :b}. :a :value :False.} log:implies {:t :value :False};
log:forAll :t, :a, :b.
{:t = {:a :or :b}. :b :value :False.} log:implies {:t :value :False};
log:forAll :t, :a, :b.
{:t = {:a :or :b}. :a :value :True. :b :value :True} log:implies
 {:t :value :True};log:forAll :t, :a, :b.

# definition of not
{:na :not :a. :a :value :True} log:implies {:na :value :False}; log:forAll
:na, :a.
{:na :not :a. :a :value :False} log:implies {:na :value :True}; log:forAll
:na, :a.

# reciprocity axiom

{:a :or :b.} log:implies {:b :or :a}; log:forAll :a, :b.
{:a :and :b} log:implies {:b :and :a}; lof:forAll :a, :b.

# associativity axiom
{{:a :or :b} :or :c} log:implies {:a :or {:b :or :c}}; log:forAll :a, :b, :c.
{{:a :and :b} :and :c} log:implies {:a :and {:b :and :c}};
      log:forAll :a, :b, :c.

# distributivity axiom
{:a :and {:b :or :c}} log:implies {{:a :and :b} :or {:a :and :c}};
   log:forAll :a, :b, :c.
{:a :or {:b :and :c}} log:implies {{:a :or :b} :and {:a :or :c}};
   log:forAll :a, :b, :c.


{:a :or :False} log:implies {:a :or :a};log:forAll :a.
{:a :and :True} log:implies {:a :and :a}; log:forAll :a.

{:t = {:a :or :na}. :na :not :a. } log:implies {:t :value :True};
   log:forAll :t, :a, :na.
{:t = {:a :and :na}. :na :not :a. } log:implies {:t :value :False};
   log:forAll :t, :a, :na.