```(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
)))
```