(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)
        )))