```
(def-constant smtp%connection
"lambda(s_1:states,s_2:filtered%states,f:[nn -> nn],
tcp%connection(s_1,s_2,f,a_1,a_2,p_1,p_2)
and
(p_1 > 1023 and p_2 = 25))"
(theory single-filter-theory))
```

```
(def-constant only%smtp%connections
"forall(s_1:states,s_2:filtered%states,f:[nn -> nn],
tcp%connection(s_1,s_2,f,a_1,a_2,p_1,p_2)
implies
smtp%connection(s_1,s_2,f,a_1,a_2,p_1,p_2))"
(theory single-filter-theory))
```

```
(def-constant no%smtp%connections
"forall(s_1:states,s_2:filtered%states,f:[nn -> nn],
tcp%connection(s_1,s_2,f,a_1,a_2,p_1,p_2)
implies
not(smtp%connection(s_1,s_2,f,a_1,a_2,p_1,p_2)))"
(theory single-filter-theory))
```

```
(def-constant limited%smtp%connections
forall(s_1:states,s_2:filtered%states,f:[nn -> nn],
smtp%connection(s_1,s_2,f,a_1,a_2,p_1,p_2)
and
senders subseteq internal
and
implies
(a_1 in external implies a_2 in receivers)
and
(a_2 in external implies a_1 in senders)))"
(theory single-filter-theory))
```

```
(def-constant smtp%filter%condition%1
filter%condition(d,b,
inbound,
external,
tcp,
lambda(p:ports, p > 1023),
lambda(p:ports, p = 25),
truth))"
(theory single-filter-theory))
```

```
(def-constant smtp%filter%condition%2
filter%condition(d,b,
outbound,
external,
tcp,
lambda(p:ports, p = 25),
lambda(p:ports, p > 1023),
falsehood))"
(theory single-filter-theory))
```

```
(def-constant smtp%filter%condition%3
filter%condition(d,b,
outbound,
senders,
external,
tcp,
lambda(p:ports, p > 1023),
lambda(p:ports, p = 25),
truth))"
(theory single-filter-theory))
```

```
(def-constant smtp%filter%condition%4
filter%condition(d,b,
inbound,
external,
senders,
tcp,
lambda(p:ports, p = 25),
lambda(p:ports, p > 1023),
falsehood))"
(theory single-filter-theory))
```

```
(def-constant smtp%filter%specification
forall(d:datagrams,b:directions,s:filtered%states,
not(filter(d,b,s)))))"
(theory single-filter-theory))

```

```
(def-theorem smtp-filter-correctness-1
implies
only%smtp%connections)"
(theory single-filter-theory)
(proof
(
unfold-defined-constants
(unfold-single-defined-constant-globally smtp%connection)
direct-inference
direct-inference
direct-inference
direct-inference
direct-inference
(instantiate-theorem
first-datagram-in-tcp_connection-lemma
("s_1" "s_2" "f" "a_1" "a_2" "p_1" "p_2"))
(instantiate-theorem
tcp_connection-embedding-lemma
("s_1" "s_2" "f" "a_1" "a_2" "p_1" "p_2" "0"))
(instantiate-theorem
filtered_states-defining-axiom-lemma
("s_2" "f(0)"))
(incorporate-antecedent
has%profile(f,a_1,a_2,p_1,p_2,tcp));")
(unfold-single-defined-constant-globally has%profile)
direct-inference
(instantiate-universal-antecedent
"with(p:prop,
forall(d:datagrams,b:directions,s:filtered%states,p));"
("s_2(f(0))" "b" "takefirst{s_2,f(0)}"))
(block
(script-comment "`instantiate-universal-antecedent' at (0 0)")
(incorporate-antecedent "with(p:prop,if(p, p, p));")
simplify
(backchain-backwards "with(p:prop,p and p and p and p and p);")
(backchain-backwards "with(p:prop,p and p and p and p and p);")
(force-substitution "s_2(f(0))" "s_1(0)" (0 1 2 3))
(weaken (4 3 2 0))
(unfold-single-defined-constant-globally smtp%filter%condition%1)
(unfold-single-defined-constant-globally smtp%filter%condition%2)
(unfold-single-defined-constant-globally smtp%filter%condition%3)
(unfold-single-defined-constant-globally smtp%filter%condition%4)
(unfold-single-defined-constant-globally filter%condition)
simplify)
(apply-macete-with-minor-premises
filtered_states-are-closed-under-takefirst)
)))
```

```
(def-theorem smtp-filter-correctness-2
implies
(theory single-filter-theory)
(proof
(
unfold-defined-constants
(unfold-single-defined-constant-globally smtp%connection)
direct-inference
direct-inference
direct-inference
direct-inference
(instantiate-theorem
first-datagram-in-tcp_connection-lemma
("s_1" "s_2" "f" "a_1" "a_2" "p_1" "p_2"))
(instantiate-theorem
tcp_connection-embedding-lemma
("s_1" "s_2" "f" "a_1" "a_2" "p_1" "p_2" "0"))
(instantiate-theorem
filtered_states-defining-axiom-lemma
("s_2" "f(0)"))
(incorporate-antecedent
has%profile(f,a_1,a_2,p_1,p_2,tcp));")
(unfold-single-defined-constant-globally has%profile)
direct-inference
(instantiate-universal-antecedent
"with(p:prop,
forall(d:datagrams,b:directions,s:filtered%states,p));"
("s_2(f(0))" "b" "takefirst{s_2,f(0)}"))
(block
(script-comment "`instantiate-universal-antecedent' at (0 0)")
(incorporate-antecedent "with(p:prop,if(p, p, p));")
simplify
(force-substitution "s_2(f(0))" "s_1(0)" (0 1 2 3))
(weaken (3 2 0))
(unfold-single-defined-constant-globally smtp%filter%condition%1)
(unfold-single-defined-constant-globally smtp%filter%condition%2)
(unfold-single-defined-constant-globally smtp%filter%condition%3)
(unfold-single-defined-constant-globally smtp%filter%condition%4)
(unfold-single-defined-constant-globally filter%condition)
simplify
(antecedent-inference "with(p:prop,p and p and p);")
direct-and-antecedent-inference-strategy
(block
(script-comment
"`direct-and-antecedent-inference-strategy' at (0 0 0 1 0)")
(instantiate-theorem
external-and-internal-are-disjoint
(instantiate-universal-antecedent
(block
(script-comment
"`direct-and-antecedent-inference-strategy' at (0 1 0 1 0 0)")
(instantiate-theorem
external-and-internal-are-disjoint
(instantiate-universal-antecedent
(apply-macete-with-minor-premises
filtered_states-are-closed-under-takefirst)
)))
```

```
(def-theorem smtp-filter-correctness-3
and
implies
(theory single-filter-theory)
(proof
(
unfold-defined-constants
direct-and-antecedent-inference-strategy
(instantiate-universal-antecedent
"with(p:prop,
forall(d:datagrams,b:directions,s:filtered%states,p));"
("d" "inbound" "s"))
(incorporate-antecedent "with(p:prop,if(p, p, p));")
simplify
(unfold-single-defined-constant-globally smtp%filter%condition%1)
(unfold-single-defined-constant-globally smtp%filter%condition%2)
(unfold-single-defined-constant-globally smtp%filter%condition%3)
(unfold-single-defined-constant-globally smtp%filter%condition%4)
(unfold-single-defined-constant-globally filter%condition)
direct-and-antecedent-inference-strategy
(weaken (9 7 5 4 3 2 0))
(incorporate-antecedent