```(def-script subnet-simplification 1
(
(unfold-single-defined-constant-globally \$1)
(unfold-single-defined-constant-globally subnet)
simplify
))
```

```
(theory octets))
```

```
(theory octets)
(proof
(
)))
```

```
"lambda(o_1:octet,
(theory octets))
```

```
"forall(o_1:octet,
(theory octets)
(proof
(
)))
```

```
"lambda(o_1,o_2:octet,
(theory octets))
```

```
"forall(o_1,o_2:octet,
=
indic{a:addresses, octet_1(a) = o_1 and octet_2(a) = o_2})"
(theory octets)
(proof
(
)))
```

```
"lambda(o_1,o_2,o_3:octet,
(theory octets))
```

```
"forall(o_1,o_2,o_3:octet,
=
octet_1(a) = o_1 and octet_2(a) = o_2 and octet_3(a) = o_3})"
(theory octets)
(proof
(
)))
```

```
(theory octets)
(proof
(
direct-inference
extensionality
direct-inference
(unfold-single-defined-constant-globally subnet)
simplify
simplify
)))
```

```
(def-constant all%protocols
"indic{p:protocols,truth}"
(theory single-filter-theory))
```

```
(def-constant all%ports
"indic{p:protocols,truth}"
(theory single-filter-theory))
```