```
(def-constant empty%state
"nil{datagrams}"
(theory datagrams))
```

```
(def-theorem states-exist
"forsome(x:[nn,datagrams],f_seq_q{x})"
(theory datagrams)
(proof
(

(instantiate-existential ("empty%state"))
(unfold-single-defined-constant-globally empty%state)
(apply-macete-with-minor-premises tr%nil-is-fseq)
)))
```

```
(def-atomic-sort states
"lambda(s:[nn -> datagrams], f_seq_q{s})"
(theory datagrams))
```

```
(def-theorem empty_state-is-a-state
"#(empty%state,states)"
(theory datagrams)
(proof
(
(apply-macete-with-minor-premises states-defining-axiom_datagrams)
(unfold-single-defined-constant-globally empty%state)
(apply-macete-with-minor-premises tr%nil-is-fseq)
)))
```

```
(def-constant append%to%state
"lambda(s:states, d:datagrams,
append(s,cons(d,empty%state)))"
(theory datagrams))
```

```
(def-theorem append_to_state-is-total
"total_q{append%to%state,[states,datagrams -> [nn -> datagrams]]}"
(usages d-r-convergence)
(theory datagrams)
(proof
(
insistent-direct-inference
(unfold-single-defined-constant-globally append%to%state)
)))
```

```
(def-theorem append_to_state-is-defined-in-states
"forall(s:states, d:datagrams, #(append%to%state(s,d),states))"
(usages d-r-convergence)
(theory datagrams)
(proof
(
(apply-macete-with-minor-premises states-defining-axiom_datagrams)
beta-reduce-repeatedly
direct-inference
(unfold-single-defined-constant-globally append%to%state)
(unfold-single-defined-constant-globally empty%state)
(apply-macete-with-minor-premises tr%append-is-fseq)
(apply-macete-with-minor-premises tr%cons-to-nil-is-fseq)
(instantiate-theorem states-defining-axiom_datagrams ("s_\$0"))
(simplify-antecedent "with(s_\$0:states,not(#(s_\$0,states)));")
)))
```

```
(def-constant state%embedding
"lambda(f:[nn -> nn],s_1,s_2:states,
dom{f} = dom{s_1}
and
forall(m,n:nn, m < n and n < length{s_1} implies f(m) < f(n))
and
forall(n:nn, #(s_1(n)) implies s_1(n) = s_2(f(n))))"
(theory datagrams))
```