Loading theory "UPF_Firewall.LTL_alike" (required by "UPF_Firewall.Examples" via "UPF_Firewall.DMZ" via "UPF_Firewall.DMZDatatype" via "UPF_Firewall.UPF-Firewall" via "UPF_Firewall.StatefulFW" via "UPF_Firewall.FTPVOIP" via "UPF_Firewall.FTP_WithPolicy" via "UPF_Firewall.FTP" via "UPF_Firewall.StatefulCore")
Loading theory "UPF_Firewall.NetworkCore" (required by "UPF_Firewall.Examples" via "UPF_Firewall.DMZ" via "UPF_Firewall.DMZDatatype" via "UPF_Firewall.UPF-Firewall" via "UPF_Firewall.PacketFilter" via "UPF_Firewall.NetworkModels" via "UPF_Firewall.DatatypeAddress")
Found termination order: "{}"
Found termination order: "{}"
Found termination order: "(\<lambda>p. length (snd p)) <*mlex*> {}"
Found termination order: "(\<lambda>p. length (snd p)) <*mlex*> {}"
Found termination order: "(\<lambda>p. length (snd (snd p))) <*mlex*> {}"
Found termination order: "(\<lambda>p. length (snd (snd p))) <*mlex*> {}"
Found termination order: "{}"
### theory "UPF_Firewall.LTL_alike"
### 0.728s elapsed time, 1.516s cpu time, 0.000s GC time
Loading theory "UPF_Firewall.Ports" (required by "UPF_Firewall.Examples" via "UPF_Firewall.DMZ" via "UPF_Firewall.DMZDatatype" via "UPF_Firewall.UPF-Firewall" via "UPF_Firewall.PacketFilter")
### theory "UPF_Firewall.Ports"
### 0.053s elapsed time, 0.108s cpu time, 0.000s GC time
### theory "UPF_Firewall.NetworkCore"
### 0.840s elapsed time, 1.744s cpu time, 0.000s GC time
Loading theory "UPF_Firewall.DatatypeAddress" (required by "UPF_Firewall.Examples" via "UPF_Firewall.DMZ" via "UPF_Firewall.DMZDatatype" via "UPF_Firewall.UPF-Firewall" via "UPF_Firewall.PacketFilter" via "UPF_Firewall.NetworkModels")
Loading theory "UPF_Firewall.DatatypePort" (required by "UPF_Firewall.Examples" via "UPF_Firewall.DMZ" via "UPF_Firewall.DMZDatatype" via "UPF_Firewall.UPF-Firewall" via "UPF_Firewall.PacketFilter" via "UPF_Firewall.NetworkModels")
### theory "UPF_Firewall.DatatypeAddress"
### 0.603s elapsed time, 1.212s cpu time, 0.000s GC time
Loading theory "UPF_Firewall.IPv4" (required by "UPF_Firewall.Examples" via "UPF_Firewall.DMZ" via "UPF_Firewall.DMZDatatype" via "UPF_Firewall.UPF-Firewall" via "UPF_Firewall.PacketFilter" via "UPF_Firewall.NetworkModels")
overloading
  src_port_ipv4 \<equiv> src_port ::
    int \<times> '\<alpha> \<times> '\<alpha> \<times> '\<beta>
    \<Rightarrow> '\<gamma>
overloading
  dest_port_ipv4 \<equiv> dest_port ::
    int \<times> '\<alpha> \<times> '\<alpha> \<times> '\<beta>
    \<Rightarrow> '\<gamma>
overloading
  subnet_of_ipv4 \<equiv> subnet_of ::
    '\<alpha> \<Rightarrow> '\<alpha> set set
### theory "UPF_Firewall.IPv4"
### 0.075s elapsed time, 0.152s cpu time, 0.000s GC time
Loading theory "UPF_Firewall.IPv4_TCPUDP" (required by "UPF_Firewall.Examples" via "UPF_Firewall.DMZ" via "UPF_Firewall.DMZDatatype" via "UPF_Firewall.UPF-Firewall" via "UPF_Firewall.PacketFilter" via "UPF_Firewall.NetworkModels")
overloading
  src_port_datatype \<equiv> src_port ::
    int \<times> '\<alpha> \<times> '\<alpha> \<times> '\<beta>
    \<Rightarrow> '\<gamma>
overloading
  dest_port_datatype \<equiv> dest_port ::
    int \<times> '\<alpha> \<times> '\<alpha> \<times> '\<beta>
    \<Rightarrow> '\<gamma>
overloading
  src_port_ipv4_TCPUDP \<equiv> src_port ::
    int \<times> '\<alpha> \<times> '\<alpha> \<times> '\<beta>
    \<Rightarrow> '\<gamma>
overloading
  subnet_of_datatype \<equiv> subnet_of ::
    '\<alpha> \<Rightarrow> '\<alpha> set set
overloading
  dest_port_ipv4_TCPUDP \<equiv> dest_port ::
    int \<times> '\<alpha> \<times> '\<alpha> \<times> '\<beta>
    \<Rightarrow> '\<gamma>
### theory "UPF_Firewall.DatatypePort"
### 0.623s elapsed time, 1.252s cpu time, 0.000s GC time
Loading theory "UPF_Firewall.IntegerAddress" (required by "UPF_Firewall.Examples" via "UPF_Firewall.DMZ" via "UPF_Firewall.DMZDatatype" via "UPF_Firewall.UPF-Firewall" via "UPF_Firewall.PacketFilter" via "UPF_Firewall.NetworkModels")
overloading
  subnet_of_ipv4_TCPUDP \<equiv> subnet_of ::
    '\<alpha> \<Rightarrow> '\<alpha> set set
overloading
  dest_protocol_ipv4_TCPUDP \<equiv> dest_protocol ::
    int \<times> '\<alpha> \<times> '\<alpha> \<times> '\<beta>
    \<Rightarrow> protocol
### theory "UPF_Firewall.IntegerAddress"
### 0.025s elapsed time, 0.052s cpu time, 0.000s GC time
Loading theory "UPF_Firewall.IntegerPort" (required by "UPF_Firewall.Examples" via "UPF_Firewall.DMZ" via "UPF_Firewall.DMZDatatype" via "UPF_Firewall.UPF-Firewall" via "UPF_Firewall.PacketFilter" via "UPF_Firewall.NetworkModels")
### theory "UPF_Firewall.IPv4_TCPUDP"
### 0.092s elapsed time, 0.184s cpu time, 0.000s GC time
Loading theory "UPF_Firewall.IntegerPort_TCPUDP" (required by "UPF_Firewall.Examples" via "UPF_Firewall.DMZ" via "UPF_Firewall.DMZDatatype" via "UPF_Firewall.UPF-Firewall" via "UPF_Firewall.PacketFilter" via "UPF_Firewall.NetworkModels")
overloading
  src_port_int \<equiv> src_port ::
    int \<times> '\<alpha> \<times> '\<alpha> \<times> '\<beta>
    \<Rightarrow> '\<gamma>
overloading
  dest_port_int \<equiv> dest_port ::
    int \<times> '\<alpha> \<times> '\<alpha> \<times> '\<beta>
    \<Rightarrow> '\<gamma>
overloading
  subnet_of_int \<equiv> subnet_of ::
    '\<alpha> \<Rightarrow> '\<alpha> set set
overloading
  src_port_int_TCPUDP \<equiv> src_port ::
    int \<times> '\<alpha> \<times> '\<alpha> \<times> '\<beta>
    \<Rightarrow> '\<gamma>
overloading
  dest_port_int_TCPUDP \<equiv> dest_port ::
    int \<times> '\<alpha> \<times> '\<alpha> \<times> '\<beta>
    \<Rightarrow> '\<gamma>
### theory "UPF_Firewall.IntegerPort"
### 0.061s elapsed time, 0.120s cpu time, 0.000s GC time
Loading theory "UPF_Firewall.PolicyCore" (required by "UPF_Firewall.Examples" via "UPF_Firewall.DMZ" via "UPF_Firewall.DMZDatatype" via "UPF_Firewall.UPF-Firewall" via "UPF_Firewall.PacketFilter" via "UPF_Firewall.ProtocolPortCombinators" via "UPF_Firewall.PortCombinators" via "UPF_Firewall.PolicyCombinators")
overloading
  subnet_of_int_TCPUDP \<equiv> subnet_of ::
    '\<alpha> \<Rightarrow> '\<alpha> set set
overloading
  src_protocol_int_TCPUDP \<equiv> src_protocol ::
    int \<times> '\<alpha> \<times> '\<alpha> \<times> '\<beta>
    \<Rightarrow> protocol
overloading
  dest_protocol_int_TCPUDP \<equiv> dest_protocol ::
    int \<times> '\<alpha> \<times> '\<alpha> \<times> '\<beta>
    \<Rightarrow> protocol
### theory "UPF_Firewall.IntegerPort_TCPUDP"
### 0.105s elapsed time, 0.212s cpu time, 0.000s GC time
Loading theory "UPF_Firewall.NetworkModels" (required by "UPF_Firewall.Examples" via "UPF_Firewall.DMZ" via "UPF_Firewall.DMZDatatype" via "UPF_Firewall.UPF-Firewall" via "UPF_Firewall.PacketFilter")
### theory "UPF_Firewall.PolicyCore"
### 0.345s elapsed time, 0.692s cpu time, 0.000s GC time
Loading theory "UPF_Firewall.PolicyCombinators" (required by "UPF_Firewall.Examples" via "UPF_Firewall.DMZ" via "UPF_Firewall.DMZDatatype" via "UPF_Firewall.UPF-Firewall" via "UPF_Firewall.PacketFilter" via "UPF_Firewall.ProtocolPortCombinators" via "UPF_Firewall.PortCombinators")
### theory "UPF_Firewall.PolicyCombinators"
### 0.091s elapsed time, 0.180s cpu time, 0.000s GC time
Loading theory "UPF_Firewall.PortCombinators" (required by "UPF_Firewall.Examples" via "UPF_Firewall.DMZ" via "UPF_Firewall.DMZDatatype" via "UPF_Firewall.UPF-Firewall" via "UPF_Firewall.PacketFilter" via "UPF_Firewall.ProtocolPortCombinators")
### theory "UPF_Firewall.PortCombinators"
### 0.497s elapsed time, 0.940s cpu time, 0.424s GC time
Loading theory "UPF_Firewall.ProtocolPortCombinators" (required by "UPF_Firewall.Examples" via "UPF_Firewall.DMZ" via "UPF_Firewall.DMZDatatype" via "UPF_Firewall.UPF-Firewall" via "UPF_Firewall.PacketFilter")
### theory "UPF_Firewall.NetworkModels"
### 0.970s elapsed time, 1.888s cpu time, 0.424s GC time
### theory "UPF_Firewall.ProtocolPortCombinators"
### 0.254s elapsed time, 0.516s cpu time, 0.000s GC time
Loading theory "UPF_Firewall.PacketFilter" (required by "UPF_Firewall.Examples" via "UPF_Firewall.DMZ" via "UPF_Firewall.DMZDatatype" via "UPF_Firewall.UPF-Firewall")
### theory "UPF_Firewall.PacketFilter"
### 0.352s elapsed time, 0.660s cpu time, 0.000s GC time
Loading theory "UPF_Firewall.FWNormalisationCore" (required by "UPF_Firewall.Examples" via "UPF_Firewall.DMZ" via "UPF_Firewall.DMZDatatype" via "UPF_Firewall.UPF-Firewall" via "UPF_Firewall.FWNormalisation" via "UPF_Firewall.NormalisationIPPProofs" via "UPF_Firewall.NormalisationIntegerPortProof" via "UPF_Firewall.NormalisationGenericProofs")
Loading theory "UPF_Firewall.NAT" (required by "UPF_Firewall.Examples" via "UPF_Firewall.DMZ" via "UPF_Firewall.DMZDatatype" via "UPF_Firewall.UPF-Firewall")
### theory "UPF_Firewall.NAT"
### 0.420s elapsed time, 0.852s cpu time, 0.000s GC time
Loading theory "UPF_Firewall.StatefulCore" (required by "UPF_Firewall.Examples" via "UPF_Firewall.DMZ" via "UPF_Firewall.DMZDatatype" via "UPF_Firewall.UPF-Firewall" via "UPF_Firewall.StatefulFW" via "UPF_Firewall.FTPVOIP" via "UPF_Firewall.FTP_WithPolicy" via "UPF_Firewall.FTP")
Found termination order:
  "(\<lambda>p. size_list (\<lambda>p. size (snd (snd p))) (fst p)) <*mlex*>
   {}"
Found termination order:
  "(\<lambda>p. size_list (\<lambda>p. size (snd (snd p))) (snd p)) <*mlex*>
   {}"
Found termination order:
  "(\<lambda>p. size_list (\<lambda>p. size (snd (snd p))) (snd p)) <*mlex*>
   {}"
### theory "UPF_Firewall.StatefulCore"
### 0.780s elapsed time, 1.572s cpu time, 0.000s GC time
Loading theory "UPF_Firewall.FTP" (required by "UPF_Firewall.Examples" via "UPF_Firewall.DMZ" via "UPF_Firewall.DMZDatatype" via "UPF_Firewall.UPF-Firewall" via "UPF_Firewall.StatefulFW" via "UPF_Firewall.FTPVOIP" via "UPF_Firewall.FTP_WithPolicy")
Found termination order: "{}"
Found termination order: "{}"
Found termination order:
  "(\<lambda>p.
       size_list (\<lambda>p. size (snd (snd (snd p)))) (snd p)) <*mlex*>
   {}"
Found termination order: "size <*mlex*> {}"
Found termination order: "size <*mlex*> {}"
Found termination order: "size_list size <*mlex*> {}"
Found termination order:
  "(\<lambda>p.
       size_list (\<lambda>p. size (snd (snd (snd p)))) (snd p)) <*mlex*>
   {}"
Found termination order: "{}"
Found termination order: "size_list size <*mlex*> {}"
Found termination order: "size_list size <*mlex*> {}"
Found termination order: "{}"
Found termination order: "{}"
Found termination order: "size <*mlex*> {}"
Found termination order: "{}"
Found termination order: "size <*mlex*> {}"
Found termination order: "size <*mlex*> {}"
Found termination order: "{}"
Found termination order: "(\<lambda>p. size_list size (fst p)) <*mlex*> {}"
Found termination order: "(\<lambda>p. size (snd p)) <*mlex*> {}"
Found termination order: "size <*mlex*> {}"
Found termination order: "(\<lambda>p. size_list size (snd p)) <*mlex*> {}"
Found termination order: "{}"
Found termination order:
  "(\<lambda>p.
       size_list (\<lambda>p. size (snd (snd (snd p))))
        (snd (snd (snd (snd (snd p)))))) <*mlex*>
   {}"
Found termination order: "{}"
### theory "UPF_Firewall.FTP"
### 3.427s elapsed time, 6.812s cpu time, 0.704s GC time
Loading theory "UPF_Firewall.FTP_WithPolicy" (required by "UPF_Firewall.Examples" via "UPF_Firewall.DMZ" via "UPF_Firewall.DMZDatatype" via "UPF_Firewall.UPF-Firewall" via "UPF_Firewall.StatefulFW" via "UPF_Firewall.FTPVOIP")
Found termination order: "{}"
Found termination order: "size_list size <*mlex*> {}"
Found termination order: "size_list size <*mlex*> {}"
Found termination order: "size_list size <*mlex*> {}"
Found termination order: "{}"
### theory "UPF_Firewall.FTP_WithPolicy"
### 0.998s elapsed time, 1.940s cpu time, 0.600s GC time
Loading theory "UPF_Firewall.VOIP" (required by "UPF_Firewall.Examples" via "UPF_Firewall.DMZ" via "UPF_Firewall.DMZDatatype" via "UPF_Firewall.UPF-Firewall" via "UPF_Firewall.StatefulFW" via "UPF_Firewall.FTPVOIP")
Found termination order: "{}"
Found termination order: "size_list size <*mlex*> {}"
Found termination order: "size_list size <*mlex*> {}"
Found termination order: "size_list size <*mlex*> {}"
Found termination order: "size <*mlex*> {}"
Found termination order: "size_list size <*mlex*> {}"
Found termination order: "size_list size <*mlex*> {}"
Found termination order: "size_list size <*mlex*> {}"
Found termination order: "size_list size <*mlex*> {}"
Found termination order:
  "(\<lambda>p.
       size_list (\<lambda>p. size (snd (snd (snd p))))
        (snd (snd p))) <*mlex*>
   {}"
Found termination order: "{}"
Found termination order: "{}"
Found termination order: "{}"
Found termination order: "(\<lambda>p. length (fst p)) <*mlex*> {}"
Found termination order:
  "(\<lambda>p. size_list size (fst (snd p))) <*mlex*> {}"
Found termination order: "(\<lambda>p. size_list size (fst p)) <*mlex*> {}"
Found termination order: "(\<lambda>p. size_list size (fst p)) <*mlex*> {}"
Found termination order: "size_list size <*mlex*> length <*mlex*> {}"
Found termination order: "size_list size <*mlex*> {}"
Found termination order: "size <*mlex*> {}"
Found termination order: "size_list size <*mlex*> {}"
Found termination order: "{}"
Found termination order: "size_list size <*mlex*> {}"
Found termination order: "size <*mlex*> {}"
Found termination order:
  "(\<lambda>p.
       size_list (\<lambda>p. size (snd (snd (snd p))))
        (snd (snd (snd (snd (snd (snd (snd p)))))))) <*mlex*>
   {}"
### theory "UPF_Firewall.VOIP"
### 6.617s elapsed time, 13.396s cpu time, 4.392s GC time
Loading theory "UPF_Firewall.FTPVOIP" (required by "UPF_Firewall.Examples" via "UPF_Firewall.DMZ" via "UPF_Firewall.DMZDatatype" via "UPF_Firewall.UPF-Firewall" via "UPF_Firewall.StatefulFW")
Found termination order: "size <*mlex*> {}"
Found termination order: "size <*mlex*> {}"
Found termination order: "size_list size <*mlex*> {}"
Found termination order: "size_list size <*mlex*> {}"
Found termination order: "size <*mlex*> {}"
Found termination order: "{}"
Found termination order: "size_list size <*mlex*> {}"
Found termination order:
  "(\<lambda>p.
       size_list (\<lambda>p. size (snd (snd (snd p)))) (snd p)) <*mlex*>
   {}"
Found termination order: "size_list size <*mlex*> {}"
### theory "UPF_Firewall.FWNormalisationCore"
### 14.522s elapsed time, 29.092s cpu time, 6.020s GC time
Loading theory "UPF_Firewall.ElementaryRules" (required by "UPF_Firewall.Examples" via "UPF_Firewall.DMZ" via "UPF_Firewall.DMZDatatype" via "UPF_Firewall.UPF-Firewall" via "UPF_Firewall.FWNormalisation")
### theory "UPF_Firewall.ElementaryRules"
### 0.066s elapsed time, 0.140s cpu time, 0.000s GC time
Loading theory "UPF_Firewall.NormalisationGenericProofs" (required by "UPF_Firewall.Examples" via "UPF_Firewall.DMZ" via "UPF_Firewall.DMZDatatype" via "UPF_Firewall.UPF-Firewall" via "UPF_Firewall.FWNormalisation" via "UPF_Firewall.NormalisationIPPProofs" via "UPF_Firewall.NormalisationIntegerPortProof")
Found termination order:
  "(\<lambda>p.
       size_list (\<lambda>p. size (snd (snd (snd p)))) (snd p)) <*mlex*>
   {}"
Found termination order: "{}"
### theory "UPF_Firewall.NormalisationGenericProofs"
### 2.029s elapsed time, 4.024s cpu time, 0.544s GC time
Loading theory "UPF_Firewall.NormalisationIntegerPortProof" (required by "UPF_Firewall.Examples" via "UPF_Firewall.DMZ" via "UPF_Firewall.DMZDatatype" via "UPF_Firewall.UPF-Firewall" via "UPF_Firewall.FWNormalisation" via "UPF_Firewall.NormalisationIPPProofs")
Found termination order: "{}"
Found termination order:
  "(\<lambda>p.
       size_list (\<lambda>p. size (snd (snd (snd p))))
        (snd (snd p))) <*mlex*>
   {}"
### theory "UPF_Firewall.NormalisationIntegerPortProof"
### 0.696s elapsed time, 1.404s cpu time, 0.000s GC time
### Ignoring duplicate rewrite rule:
### src_port (?a1, ?x1, ?d1, ?e1) \<equiv> fst (snd ?x1)
### Ignoring duplicate rewrite rule:
### dest_port (?a1, ?d1, ?x1, ?e1) \<equiv> fst (snd ?x1)
### Ignoring duplicate rewrite rule:
### src_port ?x \<equiv> (fst \<circ> snd \<circ> fst \<circ> snd) ?x
### Ignoring duplicate rewrite rule:
### dest_port ?x \<equiv>
### (fst \<circ> snd \<circ> fst \<circ> snd \<circ> snd) ?x
### Ignoring duplicate rewrite rule:
### src_protocol ?x \<equiv> (snd \<circ> snd \<circ> fst \<circ> snd) ?x
### Ignoring duplicate rewrite rule:
### dest_protocol ?x \<equiv>
### (snd \<circ> snd \<circ> fst \<circ> snd \<circ> snd) ?x
### Ignoring duplicate rewrite rule:
### subnet_of ?x \<equiv> {{(a, b, c). a = fst ?x}}
Found termination order: "{}"
### Ignoring duplicate rewrite rule:
### src_port (?a1, ?x1, ?d1, ?e1) \<equiv> fst (snd ?x1)
### Ignoring duplicate rewrite rule:
### dest_port (?a1, ?d1, ?x1, ?e1) \<equiv> fst (snd ?x1)
### Ignoring duplicate rewrite rule:
### src_port ?x \<equiv> (fst \<circ> snd \<circ> fst \<circ> snd) ?x
### Ignoring duplicate rewrite rule:
### dest_port ?x \<equiv>
### (fst \<circ> snd \<circ> fst \<circ> snd \<circ> snd) ?x
### Ignoring duplicate rewrite rule:
### src_protocol ?x \<equiv> (snd \<circ> snd \<circ> fst \<circ> snd) ?x
### Ignoring duplicate rewrite rule:
### dest_protocol ?x \<equiv>
### (snd \<circ> snd \<circ> fst \<circ> snd \<circ> snd) ?x
### Ignoring duplicate rewrite rule:
### subnet_of ?x \<equiv> {{(a, b, c). a = fst ?x}}
### Ignoring duplicate rewrite rule:
### src_port (?a1, ?x1, ?d1, ?e1) \<equiv> fst (snd ?x1)
### Ignoring duplicate rewrite rule:
### dest_port (?a1, ?d1, ?x1, ?e1) \<equiv> fst (snd ?x1)
### Ignoring duplicate rewrite rule:
### src_port ?x \<equiv> (fst \<circ> snd \<circ> fst \<circ> snd) ?x
### Ignoring duplicate rewrite rule:
### dest_port ?x \<equiv>
### (fst \<circ> snd \<circ> fst \<circ> snd \<circ> snd) ?x
### Ignoring duplicate rewrite rule:
### src_protocol ?x \<equiv> (snd \<circ> snd \<circ> fst \<circ> snd) ?x
### Ignoring duplicate rewrite rule:
### dest_protocol ?x \<equiv>
### (snd \<circ> snd \<circ> fst \<circ> snd \<circ> snd) ?x
### Ignoring duplicate rewrite rule:
### subnet_of ?x \<equiv> {{(a, b, c). a = fst ?x}}
### Ignoring duplicate rewrite rule:
### src_port (?a1, ?x1, ?d1, ?e1) \<equiv> fst (snd ?x1)
### Ignoring duplicate rewrite rule:
### dest_port (?a1, ?d1, ?x1, ?e1) \<equiv> fst (snd ?x1)
### Ignoring duplicate rewrite rule:
### src_port ?x \<equiv> (fst \<circ> snd \<circ> fst \<circ> snd) ?x
### Ignoring duplicate rewrite rule:
### dest_port ?x \<equiv>
### (fst \<circ> snd \<circ> fst \<circ> snd \<circ> snd) ?x
### Ignoring duplicate rewrite rule:
### src_protocol ?x \<equiv> (snd \<circ> snd \<circ> fst \<circ> snd) ?x
### Ignoring duplicate rewrite rule:
### dest_protocol ?x \<equiv>
### (snd \<circ> snd \<circ> fst \<circ> snd \<circ> snd) ?x
### Ignoring duplicate rewrite rule:
### subnet_of ?x \<equiv> {{(a, b, c). a = fst ?x}}
Found termination order: "{}"
Found termination order:
  "(\<lambda>p.
       size_list (\<lambda>p. size (snd (snd (snd p))))
        (snd (snd (snd (snd (snd (snd (snd p)))))))) <*mlex*>
   {}"
Found termination order:
  "(\<lambda>p.
       size_list (\<lambda>p. size (snd (snd (snd p))))
        (snd (snd (snd (snd (snd p)))))) <*mlex*>
   {}"
### theory "UPF_Firewall.FTPVOIP"
### 9.651s elapsed time, 19.196s cpu time, 1.532s GC time
Loading theory "UPF_Firewall.StatefulFW" (required by "UPF_Firewall.Examples" via "UPF_Firewall.DMZ" via "UPF_Firewall.DMZDatatype" via "UPF_Firewall.UPF-Firewall")
### theory "UPF_Firewall.StatefulFW"
### 0.022s elapsed time, 0.044s cpu time, 0.000s GC time
### Metis: Unused theorems: "FWNormalisationCore.Combinators.simps_1", "FWNormalisationCore.Combinators.simps_2", "FWNormalisationCore.Combinators.simps_3", "FWNormalisationCore.Combinators.simps_4", "FWNormalisationCore.Combinators.simps_6", "FWNormalisationCore.Combinators.simps_7", "FWNormalisationCore.Combinators.simps_8", "FWNormalisationCore.Combinators.simps_9", "FWNormalisationCore.Combinators.simps_10", "FWNormalisationCore.Combinators.simps_11", "FWNormalisationCore.Combinators.simps_12", "FWNormalisationCore.Combinators.simps_13", "FWNormalisationCore.Combinators.simps_14", "FWNormalisationCore.Combinators.simps_15", "FWNormalisationCore.Combinators.simps_16", "FWNormalisationCore.Combinators.simps_17", "FWNormalisationCore.Combinators.simps_18", "FWNormalisationCore.Combinators.simps_19", "FWNormalisationCore.Combinators.simps_20", "FWNormalisationCore.Combinators.simps_21", "FWNormalisationCore.Combinators.simps_22", "FWNormalisationCore.Combinators.simps_23", "FWNormalisationCore.Combinators.simps_24", "FWNormalisationCore.Combinators.simps_25", "FWNormalisationCore.Combinators.simps_26", "FWNormalisationCore.Combinators.simps_27", "FWNormalisationCore.Combinators.simps_28", "FWNormalisationCore.Combinators.simps_29", "FWNormalisationCore.Combinators.simps_30", "FWNormalisationCore.Combinators.simps_31", "FWNormalisationCore.Combinators.simps_32", "FWNormalisationCore.Combinators.simps_33", "FWNormalisationCore.Combinators.simps_34", "FWNormalisationCore.Combinators.simps_35", "FWNormalisationCore.Combinators.simps_36", "FWNormalisationCore.Combinators.simps_37", "FWNormalisationCore.Combinators.simps_38", "FWNormalisationCore.Combinators.simps_39", "FWNormalisationCore.Combinators.simps_40", "FWNormalisationCore.Combinators.simps_41", "FWNormalisationCore.Combinators.simps_42", "FWNormalisationCore.Combinators.simps_43", "FWNormalisationCore.Combinators.simps_44", "FWNormalisationCore.Combinators.simps_45", "FWNormalisationCore.Combinators.simps_46", "FWNormalisationCore.Combinators.simps_47", "FWNormalisationCore.Combinators.simps_48", "FWNormalisationCore.Combinators.simps_49", "FWNormalisationCore.Combinators.simps_50", "FWNormalisationCore.Combinators.simps_51"
### Metis: Falling back on "metis (full_types)"...
### Metis: Falling back on "metis (mono_tags)"...
### Metis: Unused theorems: "FWNormalisationCore.Combinators.simps_1", "FWNormalisationCore.Combinators.simps_2", "FWNormalisationCore.Combinators.simps_3", "FWNormalisationCore.Combinators.simps_4", "FWNormalisationCore.Combinators.simps_5", "FWNormalisationCore.Combinators.simps_6", "FWNormalisationCore.Combinators.simps_8", "FWNormalisationCore.Combinators.simps_9", "FWNormalisationCore.Combinators.simps_10", "FWNormalisationCore.Combinators.simps_11", "FWNormalisationCore.Combinators.simps_12", "FWNormalisationCore.Combinators.simps_13", "FWNormalisationCore.Combinators.simps_14", "FWNormalisationCore.Combinators.simps_15", "FWNormalisationCore.Combinators.simps_16", "FWNormalisationCore.Combinators.simps_17", "FWNormalisationCore.Combinators.simps_18", "FWNormalisationCore.Combinators.simps_19", "FWNormalisationCore.Combinators.simps_20", "FWNormalisationCore.Combinators.simps_21", "FWNormalisationCore.Combinators.simps_22", "FWNormalisationCore.Combinators.simps_23", "FWNormalisationCore.Combinators.simps_24", "FWNormalisationCore.Combinators.simps_25", "FWNormalisationCore.Combinators.simps_26", "FWNormalisationCore.Combinators.simps_27", "FWNormalisationCore.Combinators.simps_28", "FWNormalisationCore.Combinators.simps_29", "FWNormalisationCore.Combinators.simps_30", "FWNormalisationCore.Combinators.simps_31", "FWNormalisationCore.Combinators.simps_32", "FWNormalisationCore.Combinators.simps_33", "FWNormalisationCore.Combinators.simps_34", "FWNormalisationCore.Combinators.simps_35", "FWNormalisationCore.Combinators.simps_36", "FWNormalisationCore.Combinators.simps_37", "FWNormalisationCore.Combinators.simps_38", "FWNormalisationCore.Combinators.simps_39", "FWNormalisationCore.Combinators.simps_40", "FWNormalisationCore.Combinators.simps_41", "FWNormalisationCore.Combinators.simps_42", "FWNormalisationCore.Combinators.simps_43", "FWNormalisationCore.Combinators.simps_44", "FWNormalisationCore.Combinators.simps_45", "FWNormalisationCore.Combinators.simps_46", "FWNormalisationCore.Combinators.simps_47", "FWNormalisationCore.Combinators.simps_48", "FWNormalisationCore.Combinators.simps_49", "FWNormalisationCore.Combinators.simps_50", "FWNormalisationCore.Combinators.simps_51"
### Metis: Unused theorems: "FWNormalisationCore.Combinators.simps_1", "FWNormalisationCore.Combinators.simps_2", "FWNormalisationCore.Combinators.simps_3", "FWNormalisationCore.Combinators.simps_4", "FWNormalisationCore.Combinators.simps_5", "FWNormalisationCore.Combinators.simps_6", "FWNormalisationCore.Combinators.simps_7", "FWNormalisationCore.Combinators.simps_8", "FWNormalisationCore.Combinators.simps_10", "FWNormalisationCore.Combinators.simps_11", "FWNormalisationCore.Combinators.simps_12", "FWNormalisationCore.Combinators.simps_13", "FWNormalisationCore.Combinators.simps_14", "FWNormalisationCore.Combinators.simps_15", "FWNormalisationCore.Combinators.simps_16", "FWNormalisationCore.Combinators.simps_17", "FWNormalisationCore.Combinators.simps_18", "FWNormalisationCore.Combinators.simps_19", "FWNormalisationCore.Combinators.simps_20", "FWNormalisationCore.Combinators.simps_21", "FWNormalisationCore.Combinators.simps_22", "FWNormalisationCore.Combinators.simps_23", "FWNormalisationCore.Combinators.simps_24", "FWNormalisationCore.Combinators.simps_25", "FWNormalisationCore.Combinators.simps_26", "FWNormalisationCore.Combinators.simps_27", "FWNormalisationCore.Combinators.simps_28", "FWNormalisationCore.Combinators.simps_29", "FWNormalisationCore.Combinators.simps_30", "FWNormalisationCore.Combinators.simps_31", "FWNormalisationCore.Combinators.simps_32", "FWNormalisationCore.Combinators.simps_33", "FWNormalisationCore.Combinators.simps_34", "FWNormalisationCore.Combinators.simps_35", "FWNormalisationCore.Combinators.simps_36", "FWNormalisationCore.Combinators.simps_37", "FWNormalisationCore.Combinators.simps_38", "FWNormalisationCore.Combinators.simps_39", "FWNormalisationCore.Combinators.simps_40", "FWNormalisationCore.Combinators.simps_41", "FWNormalisationCore.Combinators.simps_42", "FWNormalisationCore.Combinators.simps_43", "FWNormalisationCore.Combinators.simps_44", "FWNormalisationCore.Combinators.simps_45", "FWNormalisationCore.Combinators.simps_46", "FWNormalisationCore.Combinators.simps_47", "FWNormalisationCore.Combinators.simps_48", "FWNormalisationCore.Combinators.simps_49", "FWNormalisationCore.Combinators.simps_50", "FWNormalisationCore.Combinators.simps_51"
cases:
  True
    :
    let "?case" = "?Q"
    assume "a \<noteq> c"
  False
    :
    let "?case" = "?Q"
    assume "\<not> a \<noteq> c"
cases:
  1
    :
    fix l_
    let "?case" =
          "all_in_list [] l_ \<longrightarrow>
           singleCombinators [] \<longrightarrow>
           FWNormalisationCore.sorted (qsort [] l_) l_"
  2
    :
    fix x_ xs_ l_
    let "?case" =
          "all_in_list (x_ # xs_) l_ \<longrightarrow>
           singleCombinators (x_ # xs_) \<longrightarrow>
           FWNormalisationCore.sorted (qsort (x_ # xs_) l_) l_"
    assume
      hyps :
        "all_in_list (filter (\<lambda>y. \<not> smaller x_ y l_) xs_)
          l_ \<longrightarrow>
         singleCombinators
          (filter (\<lambda>y. \<not> smaller x_ y l_)
            xs_) \<longrightarrow>
         FWNormalisationCore.sorted
          (qsort (filter (\<lambda>y. \<not> smaller x_ y l_) xs_) l_) l_"
        "all_in_list (filter (\<lambda>y. smaller x_ y l_) xs_)
          l_ \<longrightarrow>
         singleCombinators
          (filter (\<lambda>y. smaller x_ y l_) xs_) \<longrightarrow>
         FWNormalisationCore.sorted
          (qsort (filter (\<lambda>y. smaller x_ y l_) xs_) l_) l_"
      and prems :
cases:
  Nil
    :
    let "?case" =
          "OnlyTwoNets [] \<longrightarrow>
           NetsCollected2 [] \<longrightarrow>
           NetsCollected [] \<longrightarrow>
           noDenyAll1 [] \<longrightarrow>
           allNetsDistinct [] \<longrightarrow> separated []"
  Cons
    :
    fix a_ p_
    let "?case" =
          "OnlyTwoNets (a_ # p_) \<longrightarrow>
           NetsCollected2 (a_ # p_) \<longrightarrow>
           NetsCollected (a_ # p_) \<longrightarrow>
           noDenyAll1 (a_ # p_) \<longrightarrow>
           allNetsDistinct (a_ # p_) \<longrightarrow> separated (a_ # p_)"
    assume
      hyps :
        "OnlyTwoNets p_ \<longrightarrow>
         NetsCollected2 p_ \<longrightarrow>
         NetsCollected p_ \<longrightarrow>
         noDenyAll1 p_ \<longrightarrow>
         allNetsDistinct p_ \<longrightarrow> separated p_"
      and prems :
  True
    :
    let "?case" = "?Q"
    assume "a = DenyAll"
  False
    :
    let "?case" = "?Q"
    assume "a \<noteq> DenyAll"
isabelle document -d /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/UPF_Firewall/outline -o pdf -n outline -t /proof,/ML
isabelle document -d /media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/UPF_Firewall/document -o pdf -n document
*** Failed to load theory "UPF_Firewall.NormalisationIPPProofs" (unresolved "UPF_Firewall.NormalisationIntegerPortProof")
*** Failed to load theory "UPF_Firewall.FWNormalisation" (unresolved "UPF_Firewall.NormalisationIPPProofs")
*** Failed to load theory "UPF_Firewall.UPF-Firewall" (unresolved "UPF_Firewall.FWNormalisation")
*** Failed to load theory "UPF_Firewall.DMZDatatype" (unresolved "UPF_Firewall.UPF-Firewall")
*** Failed to load theory "UPF_Firewall.DMZInteger" (unresolved "UPF_Firewall.UPF-Firewall")
*** Failed to load theory "UPF_Firewall.DMZ" (unresolved "UPF_Firewall.DMZDatatype", "UPF_Firewall.DMZInteger")
*** Failed to load theory "UPF_Firewall.NAT-FW" (unresolved "UPF_Firewall.UPF-Firewall")
*** Failed to load theory "UPF_Firewall.PersonalFirewallDatatype" (unresolved "UPF_Firewall.UPF-Firewall")
*** Failed to load theory "UPF_Firewall.PersonalFirewallInt" (unresolved "UPF_Firewall.UPF-Firewall")
*** Failed to load theory "UPF_Firewall.PersonalFirewallIpv4" (unresolved "UPF_Firewall.UPF-Firewall")
*** Failed to load theory "UPF_Firewall.PersonalFirewall" (unresolved "UPF_Firewall.PersonalFirewallDatatype", "UPF_Firewall.PersonalFirewallInt", "UPF_Firewall.PersonalFirewallIpv4")
*** Failed to load theory "UPF_Firewall.Transformation01" (unresolved "UPF_Firewall.UPF-Firewall")
*** Failed to load theory "UPF_Firewall.Transformation02" (unresolved "UPF_Firewall.UPF-Firewall")
*** Failed to load theory "UPF_Firewall.Transformation" (unresolved "UPF_Firewall.Transformation01", "UPF_Firewall.Transformation02")
*** Failed to load theory "UPF_Firewall.VoIP" (unresolved "UPF_Firewall.UPF-Firewall")
*** Failed to load theory "UPF_Firewall.Examples" (unresolved "UPF_Firewall.DMZ", "UPF_Firewall.NAT-FW", "UPF_Firewall.PersonalFirewall", "UPF_Firewall.Transformation", "UPF_Firewall.VoIP")
*** Latex error:
***   File `UPF-Firewall.tex' not found.
*** Latex error (line 134 of "/media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/UPF_Firewall/document/root.tex"):
***   Emergency stop.
***   <read *> 
***            
***     \input{UPF-Firewall}
*** Latex error (line 134 of "/media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/UPF_Firewall/document/root.tex"):
***    ==> Fatal error occurred, no output PDF file produced!
*** Failed to build document in "/media/data/jenkins/workspace/afp-repo-afp/browser_info/AFP/UPF_Firewall/document"
*** Type unification failed: Clash of types "_ set" and "_ \<Rightarrow> _"
*** 
*** Type error in application: incompatible operand type
*** 
*** Operator:  (\<noteq>) (C DenyAll) ::
***   (int \<times>
***    (int \<times> int) \<times> (int \<times> int) \<times> DummyContent
***    \<Rightarrow> unit decision option)
***   \<Rightarrow> bool
*** Operand:   {} :: ??'a set
*** 
*** At command "lemma" (line 873 of "~~/afp/thys/UPF_Firewall/FWNormalisation/NormalisationIntegerPortProof.thy")