(def-constant smtp%connection"lambda(s_1:states,s_2:filtered%states,f:[nn -> nn], a_1,a_2:addresses,p_1,p_2:ports, 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], a_1,a_2:addresses,p_1,p_2:ports, 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], a_1,a_2:addresses,p_1,p_2:ports, 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"lambda(senders,receivers:sets[addresses], forall(s_1:states,s_2:filtered%states,f:[nn -> nn], a_1,a_2:addresses,p_1,p_2:ports, smtp%connection(s_1,s_2,f,a_1,a_2,p_1,p_2) and senders subseteq internal and receivers subseteq internal 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"lambda(d:datagrams, b:directions, senders,receivers:sets[addresses], filter%condition(d,b, inbound, external, receivers, tcp, lambda(p:ports, p > 1023), lambda(p:ports, p = 25), truth))"(theory single-filter-theory))

(def-constant smtp%filter%condition%2"lambda(d:datagrams, b:directions, senders,receivers:sets[addresses], filter%condition(d,b, outbound, receivers, external, tcp, lambda(p:ports, p = 25), lambda(p:ports, p > 1023), falsehood))"(theory single-filter-theory))

(def-constant smtp%filter%condition%3"lambda(d:datagrams, b:directions, senders,receivers:sets[addresses], 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"lambda(d:datagrams, b:directions, senders,receivers:sets[addresses], 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"lambda(senders,receivers:sets[addresses], forall(d:datagrams,b:directions,s:filtered%states, if(smtp%filter%condition%1(d,b,senders,receivers), filter(d,b,s), smtp%filter%condition%2(d,b,senders,receivers), filter(d,b,s), smtp%filter%condition%3(d,b,senders,receivers), filter(d,b,s), smtp%filter%condition%4(d,b,senders,receivers), filter(d,b,s), not(filter(d,b,s)))))"(theory single-filter-theory))

(def-theorem smtp-filter-correctness-1"forall(senders,receivers:sets[addresses], smtp%filter%specification(senders,receivers) 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"with(p_2,p_1:ports,a_2,a_1:addresses,f:datagrams, 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"forall(senders,receivers:sets[addresses], smtp%filter%specification(senders,receivers) implies limited%smtp%connections(senders,receivers))"(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"with(p_2,p_1:ports,a_2,a_1:addresses,f:datagrams, 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"a_1""source%address(s_1(0))"(0 1)) (force-substitution"a_2""destination%address(s_1(0))"(0 1)) (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 ("source%address(s_1(0))")) (instantiate-universal-antecedent"with(senders:sets[addresses],senders subseteq internal);"("source%address(s_1(0))"))) (block (script-comment"`direct-and-antecedent-inference-strategy' at (0 1 0 1 0 0)") (instantiate-theorem external-and-internal-are-disjoint ("destination%address(s_1(0))")) (instantiate-universal-antecedent"with(receivers:sets[addresses],receivers subseteq internal);"("destination%address(s_1(0))")))) (apply-macete-with-minor-premises filtered_states-are-closed-under-takefirst) )))

(def-theorem smtp-filter-correctness-3"forall(senders,receivers:sets[addresses], smtp%filter%specification(senders,receivers) and receivers subseteq internal implies limited%externally%initiated%tcp%connections(receivers))"(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"with(d:datagrams,receivers:sets[addresses], destination%address(d) in internal diff receivers);") simplify-insistently )))