(def-language octet-language
    (extensible 
      (*octet-type* octet))
    (base-types octet)
    (constants
      (logxor (octet octet octet))
      (logand (octet octet octet))
      (logneg (octet octet))))

(def-theory pre-octets 
    (language octet-language)
    (component-theories h-o-real-arithmetic)
    (axioms
      ("forall(x:octet,logxor(x,logneg(x))=0#8)")
      (logand-is-idempotent
        "forall(x:octet,logand(x,x)=x)" rewrite)
      (associativity-of-logand
        "forall(x,y,z:octet,logand(logand(x,y),z)=logand(x,logand(y,z)))")
      ("forall(c,y,z:octet, 
              logand(c,logxor(y,z))=logxor(logand(c,y),logand(c,z)))")
      ("forall(x:octet,logand(255#8,x)=x)")
      ("forall(x,y:octet,logand(x,y)=logand(y,x))")
      (associativity-of-logxor
        "forall(x,y,z:octet,logxor(logxor(x,y),z)=logxor(x,logxor(y,z)))")
      ("forall(x:octet,logxor(x,0#8)=x)")
      ("forall(x,y:octet,logxor(x,y)=logxor(y,x))")))

(def-theorem logand-is-total 
    "total_q{logand,[octet,octet -> octet]}"
    (usages d-r-convergence)
    (theory pre-octets)
    (proof
      (
        insistent-direct-inference
        (instantiate-theorem associativity-of-logand ("x_0" "x_1" "x_1"))
        )))

(def-theorem logxor-is-total 
    "total_q{logxor,[octet,octet -> octet]}"
    (usages d-r-convergence)
    (theory pre-octets)
    (proof
      (
        insistent-direct-inference
        (instantiate-theorem associativity-of-logxor ("x_0" "x_1" "x_1"))
        )))

(def-constant atomic%octet 
    "lambda(x:octet, 
          not(x=0#8) 
            and 
          forall(y:octet, logand(x,y)=y implies y=x or y=0#8))"
    (theory pre-octets))

(def-theory octets 
    (component-theories pre-octets)
    (axioms
      (atom-1 "atomic%octet(1#8)")
      (atom-2 "atomic%octet(2#8)")
      (atom-4 "atomic%octet(4#8)")
      (atom-8 "atomic%octet(8#8)")
      (atom-16 "atomic%octet(16#8)")
      (atom-32 "atomic%octet(32#8)")
      (atom-64 "atomic%octet(64#8)")
      (atom-128 "atomic%octet(128#8)")
      ))

(def-algebraic-processor octet-algebraic-processor
    (language octets)
    (base ((scalars *octet-type*)
	    
	    
	  (operations
	    (+ logxor)
	    (* logand)
	    (- logneg))
	  use-numerals-for-ground-terms
	  commutes)))

(def-theory-processors octets
  (algebraic-simplifier (octet-algebraic-processor logxor logand logneg))
  (algebraic-term-comparator octet-algebraic-processor))

(def-theorem logand-simplification-lemma-1 
    "forall(o_1,o_2:octet, 
          logand(logand(o_1,o_2),o_2) = logand(o_1,o_2))"
    lemma
    (theory octets)
    (proof
      (
        simplify
        (apply-macete-with-minor-premises logand-is-idempotent)
        simplify
        )))

(def-theorem octet-unit-decomposition 
    "with(o:octet,
          255#8 = 
          logxor(1#8,
                        logxor(2#8,
                                      logxor(4#8,
                                                    logxor(8#8,
                                                                  logxor(16#8,
                                                                                logxor(32#8,
                                                                                              logxor(64#8,
                                                                                                            128#8))))))))"
    (theory octets)
    (proof
      (
        simplify
        )))

(def-theorem octet-decomposition 
    "forall(o:octet,
          o = 
          logxor(logand(1#8,o),
                        logxor(logand(2#8,o),
                                      logxor(logand(4#8,o),
                                                    logxor(logand(8#8,o),
                                                                  logxor(logand(16#8,o),
                                                                                logxor(logand(32#8,o),
                                                                                              logxor(logand(64#8,o),
                                                                                                            logand(128#8,o)))))))))"
    (theory octets)
    (proof
      (
        simplify
        )))

(def-constant octet%to%nn 
    "lambda(o:octet,
        if(logand(1#8,o) = 1#8,1,0) * 2^0
          +
        if(logand(2#8,o) = 2#8,1,0) * 2^1
          +
        if(logand(4#8,o) = 4#8,1,0) * 2^2
          +
        if(logand(8#8,o) = 8#8,1,0) * 2^3
          +
        if(logand(16#8,o) = 16#8,1,0) * 2^4
          +
        if(logand(32#8,o) = 32#8,1,0) * 2^5
          +
        if(logand(64#8,o) = 64#8,1,0) * 2^6
          +
        if(logand(128#8,o) = 128#8,1,0) * 2^7)"
    (theory octets))

(def-theorem octet%to%nn-is-injective 
    "forall(o_1,o_2:octet, 
          octet%to%nn(o_1) = octet%to%nn(o_2) implies o_1 = o_2)"
    (theory octets)
    (proof
      (
        (informal-justification 
          "follows from the fact that two polynomials in a natural number n 
            with natural number coefficients less than n are equal iff their 
            coefficients are equal.")
        )))

(def-constant octet%lt 
    "lambda(o_1,o_2:octet, octet%to%nn(o_1) < octet%to%nn(o_2))"
    (usages rewrite)
    (theory octets))

(def-constant octet%le 
    "lambda(o_1,o_2:octet, octet%to%nn(o_1) < octet%to%nn(o_2) or o_1 =o_2)"
    (usages rewrite)
    (theory octets))

(def-theorem octet%lt-irreflexivity 
    "forall(o:octet, not(octet%lt(o,o)))"
    (theory octets)
    (proof
      (
        (unfold-single-defined-constant-globally octet%lt)
        simplify
        )))

(def-theorem octet%lt-trichotomy 
    "forall(o_1,o_2:octet, 
          octet%lt(o_1,o_2) or o_1 = o_2 or octet%lt(o_2,o_1))"
    (theory octets)
    (proof
      (
        (unfold-single-defined-constant-globally octet%lt)
        direct-inference
        (instantiate-theorem trichotomy ("octet%to%nn(o_2)" "octet%to%nn(o_1)"))
        direct-inference
        (block 
            (script-comment "`instantiate-theorem' at (0 1)") direct-inference
            (contrapose "with(o_2,o_1:octet,not(o_1=o_2));")
            (instantiate-theorem octet%to%nn-is-injective ("o_1" "o_2"))
            )
        direct-inference
        (block 
            (script-comment "`instantiate-theorem' at (1 1 0)")
            (unfold-single-defined-constant (0) octet%to%nn) simplify
            )
        (unfold-single-defined-constant (0) octet%to%nn)
        )))

(def-theorem octet%lt-transitivity 
    "forall(o_1,o_2,o_3:octet, 
          octet%lt(o_1,o_2) and octet%lt(o_2,o_3) implies octet%lt(o_1,o_3))"
    (theory octets)
    (proof
      (
        (unfold-single-defined-constant-globally octet%lt)
        direct-and-antecedent-inference-strategy
        (apply-macete-with-minor-premises transitivity)
        auto-instantiate-existential
        )))