(def-language pre-network-language
    (base-types hosts spnets)
    (sorts (loopbacks spnets))
    (constants 
      (iface%relation "[hosts, spnets -> prop]")
      (loopback%spnet "[hosts -> loopbacks]")
      ))

(def-theory pre-networks 
    (language pre-network-language)
    (component-theories h-o-real-arithmetic)
    (axioms
      (loopback_spnet-is-bijective
        "bijective_q{loopback%spnet}")
      (loopback_spnet-gives-spnet-with-a-single-host
        "forall(h:hosts, 
              indic{h_1:hosts, iface%relation(h_1,loopback%spnet(h))} 
                = 
              singleton{h})")
      ))

(def-theorem loopback_spnet-host 
    "forall(h:hosts, iface%relation(h,loopback%spnet(h)))"
    (theory pre-networks)
    (proof
      (
        direct-inference
        (instantiate-theorem 
          loopback_spnet-gives-spnet-with-a-single-host 
          ("h"))
        (contrapose "with(p:prop,p);")
        extensionality
        (instantiate-existential ("h"))
        simplify
        )))

(def-theorem loopback_spnet-is-total 
    "total_q{loopback%spnet,[hosts -> loopbacks]}"
    (theory pre-networks)
    (usages d-r-convergence)
    (proof
      (
        insistent-direct-inference
        (instantiate-theorem loopback_spnet-host ("x_0"))
        )))

(def-cartesian-product pre%ifaces
    (hosts spnets)
    (constructor make%pre%iface)
    (accessors iface%host iface%spnet)
    (theory pre-networks))

(def-theorem interfaces-exist 
    "forsome(x:pre%ifaces,
          iface%relation(iface%host(x),iface%spnet(x)))"
    (theory pre-networks)
    (proof
      (
        (instantiate-existential 
          ("with(h:hosts,make%pre%iface(h,loopback%spnet(h)))"))
        simplify
        (apply-macete-with-minor-premises loopback_spnet-host)
        )))

(def-atomic-sort ifaces 
    "lambda(p:pre%ifaces, 
          iface%relation(iface%host(p), iface%spnet(p)))"
    (theory pre-networks))

(def-constant loopback%iface 
    "lambda(h:hosts, make%pre%iface(h,loopback%spnet(h)))"
    (theory pre-networks))

(def-constant hosts%of%spnet 
    "lambda(s:spnets, indic{h:hosts, iface%relation(h,s)})"
    (theory pre-networks))

(def-constant is%loopback%spnet 
    "lambda(s:spnets, f_card{hosts%of%spnet(s)} = 1)"
    (theory pre-networks))

(def-theorem loopback_spnet-gives-a-loopback-spnet 
    "forall(h:hosts, is%loopback%spnet(loopback%spnet(h)))"
    (theory pre-networks)
    (proof
      (
        direct-inference
        (unfold-single-defined-constant-globally is%loopback%spnet)
        (apply-macete-with-minor-premises tr%singleton-has-f-card-one)
        (block 
            (script-comment "`apply-macete-with-minor-premises' at (0)")
            (instantiate-existential ("h"))
            (unfold-single-defined-constant-globally hosts%of%spnet)
            (instantiate-theorem 
              loopback_spnet-gives-spnet-with-a-single-host
              ("h")))
        simplify
        )))

(def-constant is%point%to%point%spnet 
    "lambda(s:spnets, f_card{hosts%of%spnet(s)} = 2)"
    (theory pre-networks))

(def-constant spnets%of%host 
    "lambda(h:hosts, indic{s:spnets, iface%relation(h,s)})"
    (theory pre-networks))

(def-constant is%single%homed 
    "lambda(h:hosts, 2 = f_card{spnets%of%host(h)})"
    (theory pre-networks))

(def-constant is%multi%homed 
    "lambda(h:hosts, 3 <= f_card{spnets%of%host(h)})"
    (theory pre-networks))

(def-language network-language
    (embedded-languages pre-networks octets)
    (constants 
      (address%relation "[ifaces, addresses -> prop]")
      (mask%relation "[ifaces, masks -> prop]")
      ))

(def-theory networks 
    (language network-language)
    (component-theories pre-networks octets)
    (axioms
      (loopback-interface-has-loopback%address
        "forall(h:hosts, 
              address%relation(loopback%iface(h),loopback%address))")
      (loopback-interface-has-loopback%mask
        "forall(h:hosts, 
              mask%relation(loopback%iface(h),loopback%mask))")
      ))

(def-constant addr%to%iface 
    "lambda(a:addresses, iota(i:ifaces, address%relation(i,a)))"
    (theory networks))

(def-constant ifaces%of%host 
    "lambda(h:hosts,
          indic{i:ifaces,
              forsome(s:spnets, 
                  i = make%pre%iface(h,s) and iface%relation(h,s))})"
    (theory networks))

(def-theorem iface-is-an-iface-of-host 
    "forall(i:ifaces, i in ifaces%of%host(iface%host(i)))"
    (theory networks)
    (proof
      (
        direct-inference
        (unfold-single-defined-constant-globally ifaces%of%host)
        simplify-insistently
        (instantiate-existential ("iface%spnet(i)"))
        simplify
        (apply-macete-with-minor-premises 
          ifaces-in-quasi-sort_pre-networks)
        )))

(def-constant ifaces%of%spnet 
    "lambda(s:spnets,
          indic{i:ifaces,
              forsome(h:hosts,
                  i = make%pre%iface(h,s) and iface%relation(h,s))})"
    (theory networks))

(def-constant addresses%of%host 
    "lambda(h:hosts,
          indic{a:addresses, 
              forsome(i:ifaces, 
                  h = iface%host(i) and address%relation(i,a))})"
    (theory networks))

(def-constant masks%of%host 
    "lambda(h:hosts,
          indic{m:masks, 
              forsome(i:ifaces, 
                  h = iface%host(i) and mask%relation(i,m))})"
    (theory networks))

(def-constant addresses%of%spnet 
    "lambda(s:spnets,
          indic{a:addresses, 
              forsome(i:ifaces, 
                  s = iface%spnet(i) and address%relation(i,a))})"
    (theory networks))

(def-constant masks%of%spnet 
    "lambda(s:spnets,
          indic{m:masks,
              forsome(i:ifaces, 
                  s = iface%spnet(i) and mask%relation(i,m))})"
    (theory networks))

(def-constant spnet%is%conventional 
    "lambda(s:spnets, 
          forsome(m:masks,
              forall(i:ifaces, 
                  iface%spnet(i) = s implies mask%relation(i,m))))"
    (theory networks))

(def-constant network%is%conventional 
    "forall(s:spnets, spnet%is%conventional(s))"
    (theory networks))

(def-constant spnet%mask 
    "lambda(s:spnets, 
          iota(m:masks, 
              forall(i:ifaces, 
                  iface%spnet(i) = s implies mask%relation(i,m))))"
    (theory networks))

(def-constant spnet%address 
    "lambda(s:spnets,
          iota(a:addresses,
              forall(i:ifaces, b:addresses,
                  iface%spnet(i) = s
                    and
                  address%relation(i,b) 
                    implies
                  a = address%and(b,spnet%mask(s)))))"
    (theory networks))

(def-constant directly%connected 
    "lambda(h_1,h_2:hosts, 
          forsome(s:spnets, 
              h_1 in hosts%of%spnet(s) and h_2 in hosts%of%spnet(s)))"
    (theory networks))

(def-recursive-constant connected 
  Remark: This entry is multiply defined. See:  [1] [2]
    "lambda(con:[hosts,hosts -> prop],
          lambda(h_1,h_2:hosts, 
              directly%connected(h_1,h_2) 
                or
              forsome(h_3:hosts, directly%connected(h_1,h_3) and con(h_3,h_2))))"
    (theory networks))

(def-theorem host-spnet-inversion 
    "forall(h:hosts, s:spnets, 
          h in hosts%of%spnet(s) iff s in spnets%of%host(h))"
    (theory networks)
    (proof
      (
        direct-inference
        unfold-defined-constants
        simplify-insistently
        )))

(def-theorem hosts-are-self-connected 
    "forall(h:hosts, connected(h,h))"
    (theory networks)
    (proof
      (
        direct-inference
        (unfold-single-defined-constant-globally connected)
        direct-and-antecedent-inference-strategy
        (contrapose "with(p:prop,p);")
        (unfold-single-defined-constant-globally directly%connected)
        (instantiate-existential ("loopback%spnet(h)"))
        (unfold-single-defined-constant-globally hosts%of%spnet)
        simplify-insistently
        (apply-macete-with-minor-premises loopback_spnet-host)
        )))