(def-theorem netstates-exist
*"forsome(x:[hosts,states],total_q{x,[hosts,states]})"*
(theory routed-networks)
(proof
(
(instantiate-existential (*"lambda(h:hosts, nil{datagrams})"*))
(block
(script-comment *"`instantiate-existential' at (0)"*)
insistent-direct-inference
beta-reduce-repeatedly)
(block
(script-comment *"`instantiate-existential' at (1)"*)
sort-definedness
simplify)
)))

(def-atomic-sort netstates
*"lambda(n:[hosts -> states], total_q{n,[hosts -> states]})"*
(theory routed-networks))

(def-constant append%to%netstate
*"lambda(n:netstates, h:hosts, d:datagrams,
lambda(h_1:hosts, if(h_1 = h, append%to%state(n(h_1),d), n(h_1))))"*
(theory routed-networks))

(def-theorem append_to_netstate-is-total
*"total_q{append%to%netstate,
[netstates, hosts, datagrams -> [hosts -> [nn -> datagrams]]]}"*
(usages d-r-convergence)
(theory routed-networks)
(proof
(
insistent-direct-inference
(unfold-single-defined-constant-globally append%to%netstate)
)))

(def-theorem append_to_netstate-is-defined-in-netstates
*"forall(n:netstates, h:hosts, d:datagrams,
#(append%to%netstate(n,h,d),netstates))"*
(usages d-r-convergence)
(theory routed-networks)
(proof
(
direct-inference
(apply-macete-with-minor-premises
netstates-defining-axiom_routed-networks)
(cut-with-single-formula
*"#(append%to%netstate(n,h,d),[hosts,states])"*)
(block
(script-comment *"`cut-with-single-formula' at (0)"*)
beta-reduce-repeatedly
insistent-direct-inference
(unfold-single-defined-constant-globally append%to%netstate)
(raise-conditional (0))
simplify
(instantiate-theorem
netstates-defining-axiom_routed-networks (*"n"*)))
(block
(script-comment *"`cut-with-single-formula' at (1)"*)
(unfold-single-defined-constant-globally append%to%netstate)
sort-definedness
direct-inference
(case-split (*"xx_0=h"*))
(block
(script-comment *"`case-split' at (1)"*)
simplify
(apply-macete-with-minor-premises
append_to_state-is-defined-in-states))
simplify)
)))