Quelle  OClosed_Transfer.thy

(*  Title:       OClosed_Transfer.thy
    License:     BSD 2-Clause. See LICENSE.
    Author:      Timothy Bourke
*)

section "Transfer open results onto closed models"

theory OClosed_Transfer
imports Closed OClosed_Lifting
begin

locale openproc =
  fixes np  :: "ip ==> ('s, ('m::msg) seq_action) automaton"
    and onp :: "ip ==> ((ip ==> 'g) × 'l, 'm seq_action) automaton"
    and sr  :: "'s ==> ('g × 'l)"
  assumes  init: "{ (σ, ζ) |σ ζ s. s ∈ init (np i)
                             ∧ (σ i, ζ) = sr s
                             ∧ (∀j. j≠i ⟶ σ j ∈ (fst o sr) ` init (np j)) } ⊆ init (onp i)"
      and init_notempty: "∀j. init (np j) ≠ {}"
      and trans: "∧s a s' σ σ'. [ σ i = fst (sr s);
                                  σ' i = fst (sr s');
                                  (s, a, s') ∈ trans (np i) ]
                   ==> ((σ, snd (sr s)), a, (σ', snd (sr s'))) ∈ trans (onp i)"
begin

lemma init_pnet_p_NodeS:
  assumes "NodeS i s R ∈ init (pnet np p)"
    shows "p = ⟨i; R⟩"
  using assms by (cases p) (auto simp add: node_comps)

lemma init_pnet_p_SubnetS:
  assumes "SubnetS s1 s2 ∈ init (pnet np p)"
  obtains p1 p2 where "p = (p1 ∥ p2)"
                  and "s1 ∈ init (pnet np p1)"
                  and "s2 ∈ init (pnet np p2)"
  using assms by (cases p) (auto simp add: node_comps)

lemma init_pnet_fst_sr_netgmap:
  assumes "s ∈ init (pnet np p)"
      and "i ∈ net_ips s"
      and "wf_net_tree p"
    shows "the (fst (netgmap sr s) i) ∈ (fst ∘ sr) ` init (np i)"
  using assms proof (induction s arbitrary: p)
    fix ii s R<sub>i</sub> p
    assume "NodeS ii s R<sub>i</sub> ∈ init (pnet np p)"
       and "i ∈ net_ips (NodeS ii s R<sub>i</sub>)"
       and "wf_net_tree p"
    note this(1)
    moreover then have "p = ⟨ii; R<sub>i</sub>⟩"
      by (rule init_pnet_p_NodeS)
    ultimately have "s ∈ init (np ii)"
      by (clarsimp simp: node_comps)
    with ‹i ∈ net_ips (NodeS ii s R<sub>i</sub>)›
      show "the (fst (netgmap sr (NodeS ii s R<sub>i</sub>)) i) ∈ (fst ∘ sr) ` init (np i)"
        by clarsimp
  next
    fix s1 s2 p
    assume IH1: "∧p. s1 ∈ init (pnet np p)
                  ==> i ∈ net_ips s1
                  ==> wf_net_tree p
                  ==> the (fst (netgmap sr s1) i) ∈ (fst ∘ sr) ` init (np i)"
       and IH2: "∧p. s2 ∈ init (pnet np p)
                  ==> i ∈ net_ips s2
                  ==> wf_net_tree p
                  ==> the (fst (netgmap sr s2) i) ∈ (fst ∘ sr) ` init (np i)"
       and "SubnetS s1 s2 ∈ init (pnet np p)"
       and "i ∈ net_ips (SubnetS s1 s2)"
       and "wf_net_tree p"
    from this(3) obtain p1 p2 where "p = (p1 ∥ p2)"
                                and "s1 ∈ init (pnet np p1)"
                                and "s2 ∈ init (pnet np p2)"
      by (rule init_pnet_p_SubnetS)
    from this(1) and ‹wf_net_tree p› have "wf_net_tree p1"
                                      and "wf_net_tree p2"
                                      and "net_tree_ips p1 ∩ net_tree_ips p2 = {}"
      by auto
    from ‹i ∈ net_ips (SubnetS s1 s2)› have "i ∈ net_ips s1 ∨ i ∈ net_ips s2"
      by simp
    thus "the (fst (netgmap sr (SubnetS s1 s2)) i) ∈ (fst ∘ sr) ` init (np i)"
    proof
      assume "i ∈ net_ips s1"
      hence "i ∉ net_ips s2"
      proof -
        from ‹s1 ∈ init (pnet np p1)› and ‹i ∈ net_ips s1› have "i∈net_tree_ips p1" ..
        with ‹net_tree_ips p1 ∩ net_tree_ips p2 = {}› have "i∉net_tree_ips p2" by auto
        with ‹s2 ∈ init (pnet np p2)› show ?thesis ..
      qed
      moreover from ‹s1 ∈ init (pnet np p1)›  ‹i ∈ net_ips s1› and ‹wf_net_tree p1›
        have "the (fst (netgmap sr s1) i) ∈ (fst ∘ sr) ` init (np i)"
          by (rule IH1)
      ultimately show ?thesis by simp
    next
      assume "i ∈ net_ips s2"
      moreover with ‹s2 ∈ init (pnet np p2)› have "the (fst (netgmap sr s2) i) ∈ (fst ∘ sr) ` init (np i)"
        using ‹wf_net_tree p2› by (rule IH2)
      moreover from ‹s2 ∈ init (pnet np p2)› and ‹i ∈ net_ips s2› have "i∈net_tree_ips p2" ..
      ultimately show ?thesis by simp
    qed
  qed

lemma init_lifted:
  assumes "wf_net_tree p"                                                          
  shows "{ (σ, snd (netgmap sr s)) |σ s. s ∈ init (pnet np p)
                               ∧ (∀i. if i∈net_tree_ips p then σ i = the (fst (netgmap sr s) i)
                                      else σ i ∈ (fst o sr) ` init (np i)) } ⊆ init (opnet onp p)"
  using assms proof (induction p)
    fix i R
    assume "wf_net_tree ⟨i; R⟩"
    show "{(σ, snd (netgmap sr s)) |σ s. s ∈ init (pnet np ⟨i; R⟩)
            ∧ (∀j. if j ∈ net_tree_ips ⟨i; R⟩ then σ j = the (fst (netgmap sr s) j)
                   else σ j ∈ (fst ∘ sr) ` init (np j))} ⊆ init (opnet onp ⟨i; R⟩)"
      by (clarsimp simp add: node_comps onode_comps)
         (rule subsetD [OF init], auto)
  next
    fix p1 p2
    assume IH1: "wf_net_tree p1
                ==> {(σ, snd (netgmap sr s)) |σ s. s ∈ init (pnet np p1)
                      ∧ (∀i. if i ∈ net_tree_ips p1 then σ i = the (fst (netgmap sr s) i)
                             else σ i ∈ (fst ∘ sr) ` init (np i))} ⊆ init (opnet onp p1)"
                (is "_ ==> ?S1 ⊆ _")
       and IH2: "wf_net_tree p2
                 ==> {(σ, snd (netgmap sr s)) |σ s. s ∈ init (pnet np p2)
                       ∧ (∀i. if i ∈ net_tree_ips p2 then σ i = the (fst (netgmap sr s) i)
                              else σ i ∈ (fst ∘ sr) ` init (np i))} ⊆ init (opnet onp p2)"
                (is "_ ==> ?S2 ⊆ _")
        and "wf_net_tree (p1 ∥ p2)"
    from this(3) have "wf_net_tree p1"
                  and "wf_net_tree p2"
                  and "net_tree_ips p1 ∩ net_tree_ips p2 = {}" by auto
    show "{(σ, snd (netgmap sr s)) |σ s. s ∈ init (pnet np (p1 ∥ p2))
            ∧ (∀i. if i ∈ net_tree_ips (p1 ∥ p2) then σ i = the (fst (netgmap sr s) i)
                   else σ i ∈ (fst ∘ sr) ` init (np i))} ⊆ init (opnet onp (p1 ∥ p2))"
    proof (rule, clarsimp simp only: split_paired_all pnet.simps automaton.simps)
      fix σ s1 s2
      assume σ_desc: "∀i. if i ∈ net_tree_ips (p1 ∥ p2)
                          then σ i = the (fst (netgmap sr (SubnetS s1 s2)) i)
                          else σ i ∈ (fst ∘ sr) ` init (np i)"
         and "s1 ∈ init (pnet np p1)"
         and "s2 ∈ init (pnet np p2)"
      from this(2-3) have "net_ips s1 = net_tree_ips p1"
                      and "net_ips s2 = net_tree_ips p2" by auto
      have "(σ, snd (netgmap sr s1)) ∈ ?S1"
      proof -
        { fix i
          assume "i ∈ net_tree_ips p1"
          with ‹net_tree_ips p1 ∩ net_tree_ips p2 = {}› have "i ∉ net_tree_ips p2" by auto
          with ‹s2 ∈ init (pnet np p2)› have "i ∉ net_ips s2" ..
          hence "the ((fst (netgmap sr s1) ++ fst (netgmap sr s2)) i) = the (fst (netgmap sr s1) i)"
            by simp
        }
        moreover
        { fix i
          assume "i ∉ net_tree_ips p1"
          have "σ i ∈ (fst ∘ sr) ` init (np i)"
          proof (cases "i ∈ net_tree_ips p2")
            assume "i ∉ net_tree_ips p2"
            with ‹i ∉ net_tree_ips p1› and σ_desc show ?thesis
              by (auto dest: spec [of _ i])
          next
            assume "i ∈ net_tree_ips p2"
            with ‹s2 ∈ init (pnet np p2)› have "i ∈ net_ips s2" ..
            with ‹s2 ∈ init (pnet np p2)› have "the (fst (netgmap sr s2) i) ∈ (fst ∘ sr) ` init (np i)"
              using ‹wf_net_tree p2› by (rule init_pnet_fst_sr_netgmap)
            with ‹i∈net_tree_ips p2› and ‹i∈net_ips s2› show ?thesis
              using σ_desc by simp
          qed
        }
        ultimately show ?thesis
          using ‹s1 ∈ init (pnet np p1)› and σ_desc by auto
      qed
      hence "(σ, snd (netgmap sr s1)) ∈ init (opnet onp p1)"
        by (rule subsetD [OF IH1 [OF ‹wf_net_tree p1›]])

      have "(σ, snd (netgmap sr s2)) ∈ ?S2"
      proof -
        { fix i
          assume "i ∈ net_tree_ips p2"
          with ‹s2 ∈ init (pnet np p2)› have "i ∈ net_ips s2" ..
          hence "the ((fst (netgmap sr s1) ++ fst (netgmap sr s2)) i) = the (fst (netgmap sr s2) i)"
            by simp
        }
        moreover
        { fix i
          assume "i ∉ net_tree_ips p2"
          have "σ i ∈ (fst ∘ sr) ` init (np i)"
          proof (cases "i ∈ net_tree_ips p1")
            assume "i ∉ net_tree_ips p1"
            with ‹i ∉ net_tree_ips p2› and σ_desc show ?thesis
              by (auto dest: spec [of _ i])
          next
            assume "i ∈ net_tree_ips p1"
            with ‹s1 ∈ init (pnet np p1)› have "i ∈ net_ips s1" ..
            with ‹s1 ∈ init (pnet np p1)› have "the (fst (netgmap sr s1) i) ∈ (fst ∘ sr) ` init (np i)"
              using ‹wf_net_tree p1› by (rule init_pnet_fst_sr_netgmap)
            moreover from ‹s2 ∈ init (pnet np p2)› and ‹i ∉ net_tree_ips p2› have "i∉net_ips s2" ..
            ultimately show ?thesis
              using ‹i∈net_tree_ips p1› ‹i∈net_ips s1› and ‹i∉net_tree_ips p2› σ_desc by simp
          qed
        }
        ultimately show ?thesis
          using ‹s2 ∈ init (pnet np p2)› and σ_desc by auto
      qed
      hence "(σ, snd (netgmap sr s2)) ∈ init (opnet onp p2)"
        by (rule subsetD [OF IH2 [OF ‹wf_net_tree p2›]])

      with ‹(σ, snd (netgmap sr s1)) ∈ init (opnet onp p1)›
        show "(σ, snd (netgmap sr (SubnetS s1 s2))) ∈ init (opnet onp (p1 ∥ p2))"
        using ‹net_tree_ips p1 ∩ net_tree_ips p2 = {}›
              ‹net_ips s1 = net_tree_ips p1›
              ‹net_ips s2 = net_tree_ips p2› by simp
    qed
  qed

lemma init_pnet_opnet [elim]:
  assumes "wf_net_tree p"
      and "s ∈ init (pnet np p)"
    shows "netgmap sr s ∈ netmask (net_tree_ips p) ` init (opnet onp p)"
  proof -
    from ‹wf_net_tree p›
      have "{ (σ, snd (netgmap sr s)) |σ s. s ∈ init (pnet np p)
                              ∧ (∀i. if i∈net_tree_ips p then σ i = the (fst (netgmap sr s) i)
                                     else σ i ∈ (fst o sr) ` init (np i)) } ⊆ init (opnet onp p)"
        (is "?S ⊆ _")
      by (rule init_lifted)
    hence "netmask (net_tree_ips p) ` ?S ⊆ netmask (net_tree_ips p) ` init (opnet onp p)"
      by (rule image_mono)
    moreover have "netgmap sr s ∈ netmask (net_tree_ips p) ` ?S"
    proof -
      { fix i
        from init_notempty have "∃s. s ∈ (fst ∘ sr) ` init (np i)" by auto
        hence "(SOME x. x ∈ (fst ∘ sr) ` init (np i)) ∈ (fst ∘ sr) ` init (np i)" ..
      }
      with ‹s ∈ init (pnet np p)› and init_notempty
        have "(λi. if i ∈ net_tree_ips p
                   then the (fst (netgmap sr s) i)
                   else SOME x. x ∈ (fst ∘ sr) ` init (np i), snd (netgmap sr s)) ∈ ?S"
          (is "?s ∈ ?S") by auto
      moreover have "netgmap sr s = netmask (net_tree_ips p) ?s"
      proof (intro prod_eqI ext)
        fix i
        show "fst (netgmap sr s) i = fst (netmask (net_tree_ips p) ?s) i"
        proof (cases "i ∈ net_tree_ips p")
          assume "i ∈ net_tree_ips p"
          with ‹s∈init (pnet np p)› have "i∈net_ips s" ..
          hence "Some (the (fst (netgmap sr s) i)) = fst (netgmap sr s) i"
            by (rule some_the_fst_netgmap)
          with ‹i∈net_tree_ips p› show ?thesis
            by simp
        next
          assume "i ∉ net_tree_ips p"
          moreover with ‹s∈init (pnet np p)› have "i∉net_ips s" ..
          ultimately show ?thesis
            by simp
        qed
      qed simp
      ultimately show ?thesis
        by (rule rev_image_eqI)
    qed
    ultimately show ?thesis
      by (rule rev_subsetD [rotated])
  qed

lemma transfer_connect:
  assumes "(s, connect(i, i'), s') ∈ trans (pnet np n)"
      and "s ∈ reachable (pnet np n) TT"
      and "netgmap sr s = netmask (net_tree_ips n) (σ, ζ)"
      and "wf_net_tree n"
  obtains σ' ζ' where "((σ, ζ), connect(i, i'), (σ', ζ')) ∈ trans (opnet onp n)"
                  and "∀j. j∉net_ips ζ ⟶ σ' j = σ j"
                  and "netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')"
  proof atomize_elim
    from assms have "((σ, snd (netgmap sr s)), connect(i, i'), (σ, snd (netgmap sr s'))) ∈ trans (opnet onp n)
                     ∧ netgmap sr s' = netmask (net_tree_ips n) (σ, snd (netgmap sr s'))"
      proof (induction n arbitrary: s s' ζ)
        fix ii R_i ns ns' ζ
        assume "(ns, connect(i, i'), ns') ∈ trans (pnet np ⟨ii; R_i⟩)"
           and "netgmap sr ns = netmask (net_tree_ips ⟨ii; R_i⟩) (σ, ζ)"
        from this(1) have "(ns, connect(i, i'), ns') ∈ node_sos (trans (np ii))"
          by (simp add: node_comps)
        moreover then obtain ni s s' R R' where "ns = NodeS ni s R"
                                            and "ns' = NodeS ni s' R'" ..
        ultimately have "(NodeS ni s R, connect(i, i'), NodeS ni s' R') ∈ node_sos (trans (np ii))"
          by simp
        moreover then have "s' = s" by auto
        ultimately have "((σ, NodeS ni (snd (sr s)) R), connect(i, i'), (σ, NodeS ni (snd (sr s)) R'))
                                                                      ∈ onode_sos (trans (onp ii))"
          by - (rule node_connectTE', auto intro!: onode_sos.intros [simplified])
        with ‹ns = NodeS ni s R› ‹ns' = NodeS ni s' R'› ‹s' = s›
             and ‹netgmap sr ns = netmask (net_tree_ips ⟨ii; R_i⟩) (σ, ζ)›
          show "((σ, snd (netgmap sr ns)), connect(i, i'), (σ, snd (netgmap sr ns'))) ∈ trans (opnet onp ⟨ii; R_i⟩)
                ∧ netgmap sr ns' = netmask (net_tree_ips ⟨ii; R_i⟩) (σ, snd (netgmap sr ns'))"
            by (simp add: onode_comps)
      next
        fix n1 n2 s s' ζ
        assume IH1: "∧s s' ζ. (s, connect(i, i'), s') ∈ trans (pnet np n1)
                      ==> s ∈ reachable (pnet np n1) TT
                      ==> netgmap sr s = netmask (net_tree_ips n1) (σ, ζ)
                      ==> wf_net_tree n1
                      ==> ((σ, snd (netgmap sr s)), connect(i, i'), (σ, snd (netgmap sr s'))) ∈ trans (opnet onp n1)
                          ∧ netgmap sr s' = netmask (net_tree_ips n1) (σ, snd (netgmap sr s'))"
           and IH2: "∧s s' ζ. (s, connect(i, i'), s') ∈ trans (pnet np n2)
                      ==> s ∈ reachable (pnet np n2) TT
                      ==> netgmap sr s = netmask (net_tree_ips n2) (σ, ζ)
                      ==> wf_net_tree n2
                      ==> ((σ, snd (netgmap sr s)), connect(i, i'), (σ, snd (netgmap sr s'))) ∈ trans (opnet onp n2)
                          ∧ netgmap sr s' = netmask (net_tree_ips n2) (σ, snd (netgmap sr s'))"
           and tr: "(s, connect(i, i'), s') ∈ trans (pnet np (n1 ∥ n2))"
           and sr: "s ∈ reachable (pnet np (n1 ∥ n2)) TT"
           and nm: "netgmap sr s = netmask (net_tree_ips (n1 ∥ n2)) (σ, ζ)"
           and "wf_net_tree (n1 ∥ n2)"
        from this(3) have "(s, connect(i, i'), s') ∈ pnet_sos (trans (pnet np n1))
                                                               (trans (pnet np n2))"
          by simp
        then obtain s1 s1' s2 s2' where "s = SubnetS s1 s2"
                                    and "s' = SubnetS s1' s2'"
                                    and "(s1, connect(i, i'), s1') ∈ trans (pnet np n1)"
                                    and "(s2, connect(i, i'), s2') ∈ trans (pnet np n2)"
          by (rule partial_connectTE) auto
        from this(1) and nm have "netgmap sr (SubnetS s1 s2) = netmask (net_tree_ips (n1 ∥ n2)) (σ, ζ)"
          by simp

        from ‹wf_net_tree (n1 ∥ n2)› have "wf_net_tree n1" and "wf_net_tree n2"
                                      and "net_tree_ips n1 ∩ net_tree_ips n2 = {}" by auto

        from sr ‹s = SubnetS s1 s2› have "s1 ∈ reachable (pnet np n1) TT" by (metis subnet_reachable(1))
        hence "net_ips s1 = net_tree_ips n1" by (rule pnet_net_ips_net_tree_ips)

        from sr ‹s = SubnetS s1 s2› have "s2 ∈ reachable (pnet np n2) TT" by (metis subnet_reachable(2))
        hence "net_ips s2 = net_tree_ips n2" by (rule pnet_net_ips_net_tree_ips)

        from nm ‹s = SubnetS s1 s2›
          have "netgmap sr (SubnetS s1 s2) = netmask (net_tree_ips (n1 ∥ n2)) (σ, ζ)" by simp
        hence "netgmap sr s1 = netmask (net_tree_ips n1) (σ, snd (netgmap sr s1))"
          using ‹net_tree_ips n1 ∩ net_tree_ips n2 = {}› ‹net_ips s1 = net_tree_ips n1›
                and ‹net_ips s2 = net_tree_ips n2› by (rule netgmap_subnet_split1)
        with ‹(s1, connect(i, i'), s1') ∈ trans (pnet np n1)›
         and ‹s1 ∈ reachable (pnet np n1) TT›
         have "((σ, snd (netgmap sr s1)), connect(i, i'), (σ, snd (netgmap sr s1'))) ∈ trans (opnet onp n1)"
          and "netgmap sr s1' = netmask (net_tree_ips n1) (σ, snd (netgmap sr s1'))"
           using ‹wf_net_tree n1› unfolding atomize_conj by (rule IH1)

        from ‹netgmap sr (SubnetS s1 s2) = netmask (net_tree_ips (n1 ∥ n2)) (σ, ζ)›
             ‹net_ips s1 = net_tree_ips n1› and ‹net_ips s2 = net_tree_ips n2›
          have "netgmap sr s2 = netmask (net_tree_ips n2) (σ, snd (netgmap sr s2))"
            by (rule netgmap_subnet_split2)
        with ‹(s2, connect(i, i'), s2') ∈ trans (pnet np n2)›
         and ‹s2 ∈ reachable (pnet np n2) TT›
         have "((σ, snd (netgmap sr s2)), connect(i, i'), (σ, snd (netgmap sr s2'))) ∈ trans (opnet onp n2)"
          and "netgmap sr s2' = netmask (net_tree_ips n2) (σ, snd (netgmap sr s2'))"
           using ‹wf_net_tree n2› unfolding atomize_conj by (rule IH2)

        have "((σ, snd (netgmap sr s)), connect(i, i'), (σ, snd (netgmap sr s')))
                                         ∈ trans (opnet onp (n1 ∥ n2))"
        proof -
          from ‹((σ, snd (netgmap sr s1)), connect(i, i'), (σ, snd (netgmap sr s1'))) ∈ trans (opnet onp n1)›
           and ‹((σ, snd (netgmap sr s2)), connect(i, i'), (σ, snd (netgmap sr s2'))) ∈ trans (opnet onp n2)›
            have "((σ, SubnetS (snd (netgmap sr s1)) (snd (netgmap sr s2))), connect(i, i'),
                   (σ, SubnetS (snd (netgmap sr s1')) (snd (netgmap sr s2'))))
                                           ∈ opnet_sos (trans (opnet onp n1)) (trans (opnet onp n2))"
              by (rule opnet_connect)
          with ‹s = SubnetS s1 s2› ‹s' = SubnetS s1' s2'› show ?thesis by simp
        qed

        moreover from ‹netgmap sr s1' = netmask (net_tree_ips n1) (σ, snd (netgmap sr s1'))›
                      ‹netgmap sr s2' = netmask (net_tree_ips n2) (σ, snd (netgmap sr s2'))›
                      ‹s' = SubnetS s1' s2'›
          have "netgmap sr s' = netmask (net_tree_ips (n1 ∥ n2)) (σ, snd (netgmap sr s'))" ..

        ultimately show "((σ, snd (netgmap sr s)), connect(i, i'), (σ, snd (netgmap sr s')))
                                                                ∈ trans (opnet onp (n1 ∥ n2))
                         ∧ netgmap sr s' = netmask (net_tree_ips (n1 ∥ n2)) (σ, snd (netgmap sr s'))" ..
      qed
    moreover from ‹netgmap sr s = netmask (net_tree_ips n) (σ, ζ)› have "ζ = snd (netgmap sr s)" by simp
    ultimately show " ∃σ' ζ'. ((σ, ζ), connect(i, i'), (σ', ζ')) ∈ trans (opnet onp n)
                              ∧ (∀j. j ∉ net_ips ζ ⟶ σ' j = σ j)
                              ∧ netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')" by auto
  qed

lemma transfer_disconnect:
  assumes "(s, disconnect(i, i'), s') ∈ trans (pnet np n)"
      and "s ∈ reachable (pnet np n) TT"
      and "netgmap sr s = netmask (net_tree_ips n) (σ, ζ)"
      and "wf_net_tree n"
  obtains σ' ζ' where "((σ, ζ), disconnect(i, i'), (σ', ζ')) ∈ trans (opnet onp n)"
                  and "∀j. j∉net_ips ζ ⟶ σ' j = σ j"
                  and "netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')"
  proof atomize_elim
    from assms have "((σ, snd (netgmap sr s)), disconnect(i, i'), (σ, snd (netgmap sr s'))) ∈ trans (opnet onp n)
                     ∧ netgmap sr s' = netmask (net_tree_ips n) (σ, snd (netgmap sr s'))"
      proof (induction n arbitrary: s s' ζ)
        fix ii R_i ns ns' ζ
        assume "(ns, disconnect(i, i'), ns') ∈ trans (pnet np ⟨ii; R_i⟩)"
           and "netgmap sr ns = netmask (net_tree_ips ⟨ii; R_i⟩) (σ, ζ)"
        from this(1) have "(ns, disconnect(i, i'), ns') ∈ node_sos (trans (np ii))"
          by (simp add: node_comps)
        moreover then obtain ni s s' R R' where "ns = NodeS ni s R"
                                            and "ns' = NodeS ni s' R'" ..
        ultimately have "(NodeS ni s R, disconnect(i, i'), NodeS ni s' R') ∈ node_sos (trans (np ii))"
          by simp
        moreover then have "s' = s" by auto
        ultimately have "((σ, NodeS ni (snd (sr s)) R), disconnect(i, i'), (σ, NodeS ni (snd (sr s)) R'))
                                                                      ∈ onode_sos (trans (onp ii))"
          by - (rule node_disconnectTE', auto intro!: onode_sos.intros [simplified])
        with ‹ns = NodeS ni s R› ‹ns' = NodeS ni s' R'› ‹s' = s›
             and ‹netgmap sr ns = netmask (net_tree_ips ⟨ii; R_i⟩) (σ, ζ)›
          show "((σ, snd (netgmap sr ns)), disconnect(i, i'), (σ, snd (netgmap sr ns'))) ∈ trans (opnet onp ⟨ii; R_i⟩)
                ∧ netgmap sr ns' = netmask (net_tree_ips ⟨ii; R_i⟩) (σ, snd (netgmap sr ns'))"
            by (simp add: onode_comps)
      next
        fix n1 n2 s s' ζ
        assume IH1: "∧s s' ζ. (s, disconnect(i, i'), s') ∈ trans (pnet np n1)
                      ==> s ∈ reachable (pnet np n1) TT
                      ==> netgmap sr s = netmask (net_tree_ips n1) (σ, ζ)
                      ==> wf_net_tree n1
                      ==> ((σ, snd (netgmap sr s)), disconnect(i, i'), (σ, snd (netgmap sr s'))) ∈ trans (opnet onp n1)
                          ∧ netgmap sr s' = netmask (net_tree_ips n1) (σ, snd (netgmap sr s'))"
           and IH2: "∧s s' ζ. (s, disconnect(i, i'), s') ∈ trans (pnet np n2)
                      ==> s ∈ reachable (pnet np n2) TT
                      ==> netgmap sr s = netmask (net_tree_ips n2) (σ, ζ)
                      ==> wf_net_tree n2
                      ==> ((σ, snd (netgmap sr s)), disconnect(i, i'), (σ, snd (netgmap sr s'))) ∈ trans (opnet onp n2)
                          ∧ netgmap sr s' = netmask (net_tree_ips n2) (σ, snd (netgmap sr s'))"
           and tr: "(s, disconnect(i, i'), s') ∈ trans (pnet np (n1 ∥ n2))"
           and sr: "s ∈ reachable (pnet np (n1 ∥ n2)) TT"
           and nm: "netgmap sr s = netmask (net_tree_ips (n1 ∥ n2)) (σ, ζ)"
           and "wf_net_tree (n1 ∥ n2)"
        from this(3) have "(s, disconnect(i, i'), s') ∈ pnet_sos (trans (pnet np n1))
                                                               (trans (pnet np n2))"
          by simp
        then obtain s1 s1' s2 s2' where "s = SubnetS s1 s2"
                                    and "s' = SubnetS s1' s2'"
                                    and "(s1, disconnect(i, i'), s1') ∈ trans (pnet np n1)"
                                    and "(s2, disconnect(i, i'), s2') ∈ trans (pnet np n2)"
          by (rule partial_disconnectTE) auto
        from this(1) and nm have "netgmap sr (SubnetS s1 s2) = netmask (net_tree_ips (n1 ∥ n2)) (σ, ζ)"
          by simp

        from ‹wf_net_tree (n1 ∥ n2)› have "wf_net_tree n1" and "wf_net_tree n2"
                                      and "net_tree_ips n1 ∩ net_tree_ips n2 = {}" by auto

        from sr ‹s = SubnetS s1 s2› have "s1 ∈ reachable (pnet np n1) TT" by (metis subnet_reachable(1))
        hence "net_ips s1 = net_tree_ips n1" by (rule pnet_net_ips_net_tree_ips)

        from sr ‹s = SubnetS s1 s2› have "s2 ∈ reachable (pnet np n2) TT" by (metis subnet_reachable(2))
        hence "net_ips s2 = net_tree_ips n2" by (rule pnet_net_ips_net_tree_ips)

        from nm ‹s = SubnetS s1 s2›
          have "netgmap sr (SubnetS s1 s2) = netmask (net_tree_ips (n1 ∥ n2)) (σ, ζ)" by simp
        hence "netgmap sr s1 = netmask (net_tree_ips n1) (σ, snd (netgmap sr s1))"
          using ‹net_tree_ips n1 ∩ net_tree_ips n2 = {}› ‹net_ips s1 = net_tree_ips n1›
                and ‹net_ips s2 = net_tree_ips n2› by (rule netgmap_subnet_split1)
        with ‹(s1, disconnect(i, i'), s1') ∈ trans (pnet np n1)›
         and ‹s1 ∈ reachable (pnet np n1) TT›
         have "((σ, snd (netgmap sr s1)), disconnect(i, i'), (σ, snd (netgmap sr s1'))) ∈ trans (opnet onp n1)"
          and "netgmap sr s1' = netmask (net_tree_ips n1) (σ, snd (netgmap sr s1'))"
           using ‹wf_net_tree n1› unfolding atomize_conj by (rule IH1)

        from ‹netgmap sr (SubnetS s1 s2) = netmask (net_tree_ips (n1 ∥ n2)) (σ, ζ)›
             ‹net_ips s1 = net_tree_ips n1› and ‹net_ips s2 = net_tree_ips n2›
          have "netgmap sr s2 = netmask (net_tree_ips n2) (σ, snd (netgmap sr s2))"
            by (rule netgmap_subnet_split2)
        with ‹(s2, disconnect(i, i'), s2') ∈ trans (pnet np n2)›
         and ‹s2 ∈ reachable (pnet np n2) TT›
         have "((σ, snd (netgmap sr s2)), disconnect(i, i'), (σ, snd (netgmap sr s2'))) ∈ trans (opnet onp n2)"
          and "netgmap sr s2' = netmask (net_tree_ips n2) (σ, snd (netgmap sr s2'))"
           using ‹wf_net_tree n2› unfolding atomize_conj by (rule IH2)

        have "((σ, snd (netgmap sr s)), disconnect(i, i'), (σ, snd (netgmap sr s')))
                                         ∈ trans (opnet onp (n1 ∥ n2))"
        proof -
          from ‹((σ, snd (netgmap sr s1)), disconnect(i, i'), (σ, snd (netgmap sr s1'))) ∈ trans (opnet onp n1)›
           and ‹((σ, snd (netgmap sr s2)), disconnect(i, i'), (σ, snd (netgmap sr s2'))) ∈ trans (opnet onp n2)›
            have "((σ, SubnetS (snd (netgmap sr s1)) (snd (netgmap sr s2))), disconnect(i, i'),
                   (σ, SubnetS (snd (netgmap sr s1')) (snd (netgmap sr s2'))))
                                           ∈ opnet_sos (trans (opnet onp n1)) (trans (opnet onp n2))"
              by (rule opnet_disconnect)
          with ‹s = SubnetS s1 s2› ‹s' = SubnetS s1' s2'› show ?thesis by simp
        qed

        moreover from ‹netgmap sr s1' = netmask (net_tree_ips n1) (σ, snd (netgmap sr s1'))›
                      ‹netgmap sr s2' = netmask (net_tree_ips n2) (σ, snd (netgmap sr s2'))›
                      ‹s' = SubnetS s1' s2'›
          have "netgmap sr s' = netmask (net_tree_ips (n1 ∥ n2)) (σ, snd (netgmap sr s'))" ..

        ultimately show "((σ, snd (netgmap sr s)), disconnect(i, i'), (σ, snd (netgmap sr s')))
                                                                ∈ trans (opnet onp (n1 ∥ n2))
                         ∧ netgmap sr s' = netmask (net_tree_ips (n1 ∥ n2)) (σ, snd (netgmap sr s'))" ..
      qed
    moreover from ‹netgmap sr s = netmask (net_tree_ips n) (σ, ζ)› have "ζ = snd (netgmap sr s)" by simp
    ultimately show "∃σ' ζ'. ((σ, ζ), disconnect(i, i'), (σ', ζ')) ∈ trans (opnet onp n)
                              ∧ (∀j. j ∉ net_ips ζ ⟶ σ' j = σ j)
                              ∧ netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')" by auto
  qed

lemma transfer_tau:
  assumes "(s, τ, s') ∈ trans (pnet np n)"
      and "s ∈ reachable (pnet np n) TT"
      and "netgmap sr s = netmask (net_tree_ips n) (σ, ζ)"
      and "wf_net_tree n"
  obtains σ' ζ' where "((σ, ζ), τ, (σ', ζ')) ∈ trans (opnet onp n)"
                  and "∀j. j∉net_ips ζ ⟶ σ' j = σ j"
                  and "netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')"
  proof atomize_elim
    from assms(4,2,1) obtain i where "i∈net_ips s"
                                 and "∀j. j≠i ⟶ netmap s' j = netmap s j"
                                 and "net_ip_action np τ i n s s'"
      by (metis pnet_tau_single_node)
    from this(2) have "∀j. j≠i ⟶ fst (netgmap sr s') j = fst (netgmap sr s) j"
      by (clarsimp intro!: netmap_is_fst_netgmap')
    from ‹(s, τ, s') ∈ trans (pnet np n)› have "net_ips s' = net_ips s"
      by (rule pnet_maintains_dom [THEN sym])
    define σ' where "σ' j = (if j = i then the (fst (netgmap sr s') i) else σ j)" for j
    from ‹∀j. j≠i ⟶ fst (netgmap sr s') j = fst (netgmap sr s) j›
         and ‹netgmap sr s = netmask (net_tree_ips n) (σ, ζ)›
      have "∀j. j≠i ⟶ σ' j = σ j"
        unfolding σ'_def by clarsimp

    from assms(2) have "net_ips s = net_tree_ips n"
      by (rule pnet_net_ips_net_tree_ips)

    from ‹netgmap sr s = netmask (net_tree_ips n) (σ, ζ)›
      have "ζ = snd (netgmap sr s)" by simp

    from ‹∀j. j≠i ⟶ fst (netgmap sr s') j = fst (netgmap sr s) j› ‹i ∈ net_ips s›
         ‹net_ips s = net_tree_ips n› ‹net_ips s' = net_ips s›
         ‹netgmap sr s = netmask (net_tree_ips n) (σ, ζ)›
      have "fst (netgmap sr s') = fst (netmask (net_tree_ips n) (σ', snd (netgmap sr s')))"
        unfolding σ'_def [abs_def] by - (rule ext, clarsimp)

    hence "netgmap sr s' = netmask (net_tree_ips n) (σ', snd (netgmap sr s'))"
      by (rule prod_eqI, simp)

    with assms(1, 3)
      have "((σ, snd (netgmap sr s)), τ, (σ', snd (netgmap sr s'))) ∈ trans (opnet onp n)"
        using assms(2,4) ‹i∈net_ips s› and ‹net_ip_action np τ i n s s'›
    proof (induction n arbitrary: s s' ζ)
      fix ii R_i ns ns' ζ
      assume "(ns, τ, ns') ∈ trans (pnet np ⟨ii; R_i⟩)"
         and nsr: "ns ∈ reachable (pnet np ⟨ii; R_i⟩) TT"
         and "netgmap sr ns = netmask (net_tree_ips ⟨ii; R_i⟩) (σ, ζ)"
         and "netgmap sr ns' = netmask (net_tree_ips ⟨ii; R_i⟩) (σ', snd (netgmap sr ns'))"
         and "i∈net_ips ns"
      from this(1) have "(ns, τ, ns') ∈ node_sos (trans (np ii))"
        by (simp add: node_comps)
      moreover with nsr obtain s s' R R' where "ns = NodeS ii s R"
                                           and "ns' = NodeS ii s' R'"
         by (metis net_node_reachable_is_node node_tauTE')
      moreover from ‹i ∈ net_ips ns› and ‹ns = NodeS ii s R› have "ii = i" by simp
      ultimately have ntr: "(NodeS i s R, τ, NodeS i s' R') ∈ node_sos (trans (np i))"
        by simp
      hence "R' = R" by (metis net_state.inject(1) node_tauTE')

      from ntr obtain a where "(s, a, s') ∈ trans (np i)"
                          and "(∃d. a = ¬unicast d ∧ d∉R) ∨ (a = τ)"
        by (rule node_tauTE') auto

      from ‹netgmap sr ns = netmask (net_tree_ips ⟨ii; R_i⟩) (σ, ζ)› ‹ns = NodeS ii s R› and ‹ii = i›
        have "σ i = fst (sr s)" by simp (metis map_upd_Some_unfold)

      moreover from ‹netgmap sr ns' = netmask (net_tree_ips ⟨ii; R_i⟩) (σ', snd (netgmap sr ns'))›
                    ‹ns' = NodeS ii s' R'› and ‹ii = i›
        have "σ' i = fst (sr s')"
          unfolding σ'_def [abs_def] by clarsimp (hypsubst_thin,
                                        metis (full_types, lifting) fun_upd_same option.sel)
      ultimately have "((σ, snd (sr s)), a, (σ', snd (sr s'))) ∈ trans (onp i)"
        using ‹(s, a, s') ∈ trans (np i)› by (rule trans)

      from ‹(∃d. a = ¬unicast d ∧ d∉R) ∨ (a = τ)› ‹∀j. j≠i ⟶ σ' j = σ j› ‹R'=R›
           and ‹((σ, snd (sr s)), a, (σ', snd (sr s'))) ∈ trans (onp i)›
        have "((σ, NodeS i (snd (sr s)) R), τ, (σ', NodeS i (snd (sr s')) R')) ∈ onode_sos (trans (onp i))"
          by (metis onode_sos.onode_notucast onode_sos.onode_tau)

      with ‹ns = NodeS ii s R› ‹ns' = NodeS ii s' R'› ‹ii = i›
        show "((σ, snd (netgmap sr ns)), τ, (σ', snd (netgmap sr ns'))) ∈ trans (opnet onp ⟨ii; R_i⟩)"
          by (simp add: onode_comps)
    next
      fix n1 n2 s s' ζ
      assume IH1: "∧s s' ζ. (s, τ, s') ∈ trans (pnet np n1)
                    ==> netgmap sr s = netmask (net_tree_ips n1) (σ, ζ)
                    ==> netgmap sr s' = netmask (net_tree_ips n1) (σ', snd (netgmap sr s'))
                    ==> s ∈ reachable (pnet np n1) TT
                    ==> wf_net_tree n1
                    ==> i∈net_ips s
                    ==> net_ip_action np τ i n1 s s'
                    ==> ((σ, snd (netgmap sr s)), τ, (σ', snd (netgmap sr s'))) ∈ trans (opnet onp n1)"
         and IH2: "∧s s' ζ. (s, τ, s') ∈ trans (pnet np n2)
                    ==> netgmap sr s = netmask (net_tree_ips n2) (σ, ζ)
                    ==> netgmap sr s' = netmask (net_tree_ips n2) (σ', snd (netgmap sr s'))
                    ==> s ∈ reachable (pnet np n2) TT
                    ==> wf_net_tree n2
                    ==> i∈net_ips s
                    ==> net_ip_action np τ i n2 s s'
                    ==> ((σ, snd (netgmap sr s)), τ, (σ', snd (netgmap sr s'))) ∈ trans (opnet onp n2)"
         and tr: "(s, τ, s') ∈ trans (pnet np (n1 ∥ n2))"
         and sr: "s ∈ reachable (pnet np (n1 ∥ n2)) TT"
         and nm: "netgmap sr s = netmask (net_tree_ips (n1 ∥ n2)) (σ, ζ)"
         and nm': "netgmap sr s' = netmask (net_tree_ips (n1 ∥ n2)) (σ', snd (netgmap sr s'))"
         and "wf_net_tree (n1 ∥ n2)"
         and "i∈net_ips s"
         and "net_ip_action np τ i (n1 ∥ n2) s s'"
      from tr have "(s, τ, s') ∈ pnet_sos (trans (pnet np n1)) (trans (pnet np n2))" by simp
      then obtain s1 s1' s2 s2' where "s = SubnetS s1 s2"
                                  and "s' = SubnetS s1' s2'"
        by (rule partial_tauTE) auto
      from this(1) and nm have "netgmap sr (SubnetS s1 s2) = netmask (net_tree_ips (n1 ∥ n2)) (σ, ζ)"
        by simp
      from ‹s' = SubnetS s1' s2'› and nm'
        have "netgmap sr (SubnetS s1' s2') = netmask (net_tree_ips (n1 ∥ n2)) (σ', snd (netgmap sr s'))"
          by simp

      from ‹wf_net_tree (n1 ∥ n2)› have "wf_net_tree n1"
                                    and "wf_net_tree n2"
                                    and "net_tree_ips n1 ∩ net_tree_ips n2 = {}" by auto

      from sr [simplified ‹s = SubnetS s1 s2›] have "s1 ∈ reachable (pnet np n1) TT"
        by (rule subnet_reachable(1))
      hence "net_ips s1 = net_tree_ips n1" by (rule pnet_net_ips_net_tree_ips)

      from sr [simplified ‹s = SubnetS s1 s2›] have "s2 ∈ reachable (pnet np n2) TT"
        by (rule subnet_reachable(2))
      hence "net_ips s2 = net_tree_ips n2" by (rule pnet_net_ips_net_tree_ips)

      from nm [simplified ‹s = SubnetS s1 s2›]
           ‹net_tree_ips n1 ∩ net_tree_ips n2 = {}›
           ‹net_ips s1 = net_tree_ips n1›
           ‹net_ips s2 = net_tree_ips n2›
        have "netgmap sr s1 = netmask (net_tree_ips n1) (σ, snd (netgmap sr s1))"
          by (rule netgmap_subnet_split1)

      from nm [simplified ‹s = SubnetS s1 s2›]
           ‹net_ips s1 = net_tree_ips n1›
           ‹net_ips s2 = net_tree_ips n2›
        have "netgmap sr s2 = netmask (net_tree_ips n2) (σ, snd (netgmap sr s2))"
          by (rule netgmap_subnet_split2)

      from ‹i∈net_ips s› and ‹s = SubnetS s1 s2› have "i∈net_ips s1 ∨ i∈net_ips s2" by auto
        thus "((σ, snd (netgmap sr s)), τ, (σ', snd (netgmap sr s'))) ∈ trans (opnet onp (n1 ∥ n2))"
      proof
        assume "i∈net_ips s1"
        with ‹s = SubnetS s1 s2› ‹s' = SubnetS s1' s2'› ‹net_ip_action np τ i (n1 ∥ n2) s s'›
          have "(s1, τ, s1') ∈ trans (pnet np n1)"
           and "net_ip_action np τ i n1 s1 s1'"
           and "s2' = s2" by simp_all

        from ‹net_ips s1 = net_tree_ips n1› and ‹(s1, τ, s1') ∈ trans (pnet np n1)›
          have "net_ips s1' = net_tree_ips n1" by (metis pnet_maintains_dom)

        from nm' [simplified ‹s' = SubnetS s1' s2'› ‹s2' = s2›]
                        ‹net_tree_ips n1 ∩ net_tree_ips n2 = {}›
                        ‹net_ips s1' = net_tree_ips n1›
                        ‹net_ips s2 = net_tree_ips n2›
          have "netgmap sr s1' = netmask (net_tree_ips n1) (σ', snd (netgmap sr s1'))"
            by (rule netgmap_subnet_split1)

        from ‹(s1, τ, s1') ∈ trans (pnet np n1)›
             ‹netgmap sr s1 = netmask (net_tree_ips n1) (σ, snd (netgmap sr s1))›
             ‹netgmap sr s1' = netmask (net_tree_ips n1) (σ', snd (netgmap sr s1'))›
             ‹s1 ∈ reachable (pnet np n1) TT›
             ‹wf_net_tree n1›
             ‹i∈net_ips s1›
             ‹net_ip_action np τ i n1 s1 s1'›
          have "((σ, snd (netgmap sr s1)), τ, (σ', snd (netgmap sr s1'))) ∈ trans (opnet onp n1)"
             by (rule IH1)

        with ‹s = SubnetS s1 s2› ‹s' = SubnetS s1' s2'› ‹s2' = s2› show ?thesis
          by (simp del: step_node_tau) (erule opnet_tau1)
      next
        assume "i∈net_ips s2"
        with ‹s = SubnetS s1 s2› ‹s' = SubnetS s1' s2'› ‹net_ip_action np τ i (n1 ∥ n2) s s'›
          have "(s2, τ, s2') ∈ trans (pnet np n2)"
           and "net_ip_action np τ i n2 s2 s2'"
           and "s1' = s1" by simp_all

        from ‹net_ips s2 = net_tree_ips n2› and ‹(s2, τ, s2') ∈ trans (pnet np n2)›
          have "net_ips s2' = net_tree_ips n2" by (metis pnet_maintains_dom)

        from nm' [simplified ‹s' = SubnetS s1' s2'› ‹s1' = s1›]
                        ‹net_ips s1 = net_tree_ips n1›
                        ‹net_ips s2' = net_tree_ips n2›
          have "netgmap sr s2' = netmask (net_tree_ips n2) (σ', snd (netgmap sr s2'))"
            by (rule netgmap_subnet_split2)

        from ‹(s2, τ, s2') ∈ trans (pnet np n2)›
             ‹netgmap sr s2 = netmask (net_tree_ips n2) (σ, snd (netgmap sr s2))›
             ‹netgmap sr s2' = netmask (net_tree_ips n2) (σ', snd (netgmap sr s2'))›
             ‹s2 ∈ reachable (pnet np n2) TT›
             ‹wf_net_tree n2›
             ‹i∈net_ips s2›
             ‹net_ip_action np τ i n2 s2 s2'›
          have "((σ, snd (netgmap sr s2)), τ, (σ', snd (netgmap sr s2'))) ∈ trans (opnet onp n2)"
             by (rule IH2)

        with ‹s = SubnetS s1 s2› ‹s' = SubnetS s1' s2'› ‹s1' = s1› show ?thesis
          by (simp del: step_node_tau) (erule opnet_tau2)
      qed
    qed
    with ‹ζ = snd (netgmap sr s)› have "((σ, ζ), τ, (σ', snd (netgmap sr s'))) ∈ trans (opnet onp n)"
      by simp
    moreover from ‹∀j. j≠i ⟶ σ' j = σ j› ‹i ∈ net_ips s› ‹ζ = snd (netgmap sr s)›
      have "∀j. j∉net_ips ζ ⟶ σ' j = σ j" by (metis net_ips_netgmap)
    ultimately have "((σ, ζ), τ, (σ', snd (netgmap sr s'))) ∈ trans (opnet onp n)
                     ∧ (∀j. j∉net_ips ζ ⟶ σ' j = σ j)
                     ∧ netgmap sr s' = netmask (net_tree_ips n) (σ', snd (netgmap sr s'))"
      using ‹netgmap sr s' = netmask (net_tree_ips n) (σ', snd (netgmap sr s'))› by simp
    thus "∃σ' ζ'. ((σ, ζ), τ, (σ', ζ')) ∈ trans (opnet onp n)
                  ∧ (∀j. j∉net_ips ζ ⟶ σ' j = σ j)
                  ∧ netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')" by auto
  qed

lemma transfer_deliver:
  assumes "(s, i:deliver(d), s') ∈ trans (pnet np n)"
      and "s ∈ reachable (pnet np n) TT"
      and "netgmap sr s = netmask (net_tree_ips n) (σ, ζ)"
      and "wf_net_tree n"
  obtains σ' ζ' where "((σ, ζ), i:deliver(d), (σ', ζ')) ∈ trans (opnet onp n)"
                  and "∀j. j∉net_ips ζ ⟶ σ' j = σ j"
                  and "netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')"
  proof atomize_elim
    from assms(4,2,1) obtain "i∈net_ips s"
                         and "∀j. j≠i ⟶ netmap s' j = netmap s j"
                         and "net_ip_action np (i:deliver(d)) i n s s'"
      by (metis delivered_to_net_ips pnet_deliver_single_node)
    from this(2) have "∀j. j≠i ⟶ fst (netgmap sr s') j = fst (netgmap sr s) j"
      by (clarsimp intro!: netmap_is_fst_netgmap')
    from ‹(s, i:deliver(d), s') ∈ trans (pnet np n)› have "net_ips s' = net_ips s"
      by (rule pnet_maintains_dom [THEN sym])
    define σ' where "σ' j = (if j = i then the (fst (netgmap sr s') i) else σ j)" for j
    from ‹∀j. j≠i ⟶ fst (netgmap sr s') j = fst (netgmap sr s) j›
         and ‹netgmap sr s = netmask (net_tree_ips n) (σ, ζ)›
      have "∀j. j≠i ⟶ σ' j = σ j"
        unfolding σ'_def by clarsimp

    from assms(2) have "net_ips s = net_tree_ips n"
      by (rule pnet_net_ips_net_tree_ips)

    from ‹netgmap sr s = netmask (net_tree_ips n) (σ, ζ)›
      have "ζ = snd (netgmap sr s)" by simp

    from ‹∀j. j≠i ⟶ fst (netgmap sr s') j = fst (netgmap sr s) j› ‹i ∈ net_ips s›
         ‹net_ips s = net_tree_ips n› ‹net_ips s' = net_ips s›
         ‹netgmap sr s = netmask (net_tree_ips n) (σ, ζ)›
      have "fst (netgmap sr s') = fst (netmask (net_tree_ips n) (σ', snd (netgmap sr s')))"
        unfolding σ'_def [abs_def] by - (rule ext, clarsimp)

    hence "netgmap sr s' = netmask (net_tree_ips n) (σ', snd (netgmap sr s'))"
      by (rule prod_eqI, simp)

    with assms(1, 3)
      have "((σ, snd (netgmap sr s)), i:deliver(d), (σ', snd (netgmap sr s'))) ∈ trans (opnet onp n)"
        using assms(2,4) ‹i∈net_ips s› and ‹net_ip_action np (i:deliver(d)) i n s s'›
    proof (induction n arbitrary: s s' ζ)
      fix ii R_i ns ns' ζ
      assume "(ns, i:deliver(d), ns') ∈ trans (pnet np ⟨ii; R_i⟩)"
         and nsr: "ns ∈ reachable (pnet np ⟨ii; R_i⟩) TT"
         and "netgmap sr ns = netmask (net_tree_ips ⟨ii; R_i⟩) (σ, ζ)"
         and "netgmap sr ns' = netmask (net_tree_ips ⟨ii; R_i⟩) (σ', snd (netgmap sr ns'))"
         and "i∈net_ips ns"
      from this(1) have "(ns, i:deliver(d), ns') ∈ node_sos (trans (np ii))"
        by (simp add: node_comps)
      moreover with nsr obtain s s' R R' where "ns = NodeS ii s R"
                                           and "ns' = NodeS ii s' R'"
         by (metis net_node_reachable_is_node node_sos_dest)
      moreover from ‹i ∈ net_ips ns› and ‹ns = NodeS ii s R› have "ii = i" by simp
      ultimately have ntr: "(NodeS i s R, i:deliver(d), NodeS i s' R') ∈ node_sos (trans (np i))"
        by simp
      hence "R' = R" by (metis net_state.inject(1) node_deliverTE')

      from ntr have "(s, deliver d, s') ∈ trans (np i)"
        by (rule node_deliverTE') simp

      from ‹netgmap sr ns = netmask (net_tree_ips ⟨ii; R_i⟩) (σ, ζ)› ‹ns = NodeS ii s R› and ‹ii = i›
        have "σ i = fst (sr s)" by simp (metis map_upd_Some_unfold)

      moreover from ‹netgmap sr ns' = netmask (net_tree_ips ⟨ii; R_i⟩) (σ', snd (netgmap sr ns'))›
                    ‹ns' = NodeS ii s' R'› and ‹ii = i›
        have "σ' i = fst (sr s')"
          unfolding σ'_def [abs_def] by clarsimp (hypsubst_thin,
                                        metis (lifting, full_types) fun_upd_same option.sel)
      ultimately have "((σ, snd (sr s)), deliver d, (σ', snd (sr s'))) ∈ trans (onp i)"
        using ‹(s, deliver d, s') ∈ trans (np i)› by (rule trans)

      with ‹∀j. j≠i ⟶ σ' j = σ j› ‹R'=R›
        have "((σ, NodeS i (snd (sr s)) R), i:deliver(d), (σ', NodeS i (snd (sr s')) R'))
                                                                      ∈ onode_sos (trans (onp i))"
          by (metis onode_sos.onode_deliver)

      with ‹ns = NodeS ii s R› ‹ns' = NodeS ii s' R'› ‹ii = i›
        show "((σ, snd (netgmap sr ns)), i:deliver(d), (σ', snd (netgmap sr ns'))) ∈ trans (opnet onp ⟨ii; R_i⟩)"
          by (simp add: onode_comps)
    next
      fix n1 n2 s s' ζ
      assume IH1: "∧s s' ζ. (s, i:deliver(d), s') ∈ trans (pnet np n1)
                    ==> netgmap sr s = netmask (net_tree_ips n1) (σ, ζ)
                    ==> netgmap sr s' = netmask (net_tree_ips n1) (σ', snd (netgmap sr s'))
                    ==> s ∈ reachable (pnet np n1) TT
                    ==> wf_net_tree n1
                    ==> i∈net_ips s
                    ==> net_ip_action np (i:deliver(d)) i n1 s s'
                    ==> ((σ, snd (netgmap sr s)), i:deliver(d), (σ', snd (netgmap sr s'))) ∈ trans (opnet onp n1)"
         and IH2: "∧s s' ζ. (s, i:deliver(d), s') ∈ trans (pnet np n2)
                    ==> netgmap sr s = netmask (net_tree_ips n2) (σ, ζ)
                    ==> netgmap sr s' = netmask (net_tree_ips n2) (σ', snd (netgmap sr s'))
                    ==> s ∈ reachable (pnet np n2) TT
                    ==> wf_net_tree n2
                    ==> i∈net_ips s
                    ==> net_ip_action np (i:deliver(d)) i n2 s s'
                    ==> ((σ, snd (netgmap sr s)), i:deliver(d), (σ', snd (netgmap sr s'))) ∈ trans (opnet onp n2)"
         and tr: "(s, i:deliver(d), s') ∈ trans (pnet np (n1 ∥ n2))"
         and sr: "s ∈ reachable (pnet np (n1 ∥ n2)) TT"
         and nm: "netgmap sr s = netmask (net_tree_ips (n1 ∥ n2)) (σ, ζ)"
         and nm': "netgmap sr s' = netmask (net_tree_ips (n1 ∥ n2)) (σ', snd (netgmap sr s'))"
         and "wf_net_tree (n1 ∥ n2)"
         and "i∈net_ips s"
         and "net_ip_action np (i:deliver(d)) i (n1 ∥ n2) s s'"
      from tr have "(s, i:deliver(d), s') ∈ pnet_sos (trans (pnet np n1)) (trans (pnet np n2))" by simp
      then obtain s1 s1' s2 s2' where "s = SubnetS s1 s2"
                                  and "s' = SubnetS s1' s2'"
        by (rule partial_deliverTE) auto
      from this(1) and nm have "netgmap sr (SubnetS s1 s2) = netmask (net_tree_ips (n1 ∥ n2)) (σ, ζ)"
        by simp
      from ‹s' = SubnetS s1' s2'› and nm'
        have "netgmap sr (SubnetS s1' s2') = netmask (net_tree_ips (n1 ∥ n2)) (σ', snd (netgmap sr s'))"
          by simp

      from ‹wf_net_tree (n1 ∥ n2)› have "wf_net_tree n1"
                                    and "wf_net_tree n2"
                                    and "net_tree_ips n1 ∩ net_tree_ips n2 = {}" by auto

      from sr [simplified ‹s = SubnetS s1 s2›] have "s1 ∈ reachable (pnet np n1) TT"
        by (rule subnet_reachable(1))
      hence "net_ips s1 = net_tree_ips n1" by (rule pnet_net_ips_net_tree_ips)

      from sr [simplified ‹s = SubnetS s1 s2›] have "s2 ∈ reachable (pnet np n2) TT"
        by (rule subnet_reachable(2))
      hence "net_ips s2 = net_tree_ips n2" by (rule pnet_net_ips_net_tree_ips)

      from nm [simplified ‹s = SubnetS s1 s2›]
           ‹net_tree_ips n1 ∩ net_tree_ips n2 = {}›
           ‹net_ips s1 = net_tree_ips n1›
           ‹net_ips s2 = net_tree_ips n2›
        have "netgmap sr s1 = netmask (net_tree_ips n1) (σ, snd (netgmap sr s1))"
          by (rule netgmap_subnet_split1)

      from nm [simplified ‹s = SubnetS s1 s2›]
           ‹net_ips s1 = net_tree_ips n1›
           ‹net_ips s2 = net_tree_ips n2›
        have "netgmap sr s2 = netmask (net_tree_ips n2) (σ, snd (netgmap sr s2))"
          by (rule netgmap_subnet_split2)

      from ‹i∈net_ips s› and ‹s = SubnetS s1 s2› have "i∈net_ips s1 ∨ i∈net_ips s2" by auto
        thus "((σ, snd (netgmap sr s)), i:deliver(d), (σ', snd (netgmap sr s'))) ∈ trans (opnet onp (n1 ∥ n2))"
      proof
        assume "i∈net_ips s1"
        with ‹s = SubnetS s1 s2› ‹s' = SubnetS s1' s2'› ‹net_ip_action np (i:deliver(d)) i (n1 ∥ n2) s s'›
          have "(s1, i:deliver(d), s1') ∈ trans (pnet np n1)"
           and "net_ip_action np (i:deliver(d)) i n1 s1 s1'"
           and "s2' = s2" by simp_all

        from ‹net_ips s1 = net_tree_ips n1› and ‹(s1, i:deliver(d), s1') ∈ trans (pnet np n1)›
          have "net_ips s1' = net_tree_ips n1" by (metis pnet_maintains_dom)

        from nm' [simplified ‹s' = SubnetS s1' s2'› ‹s2' = s2›]
                        ‹net_tree_ips n1 ∩ net_tree_ips n2 = {}›
                        ‹net_ips s1' = net_tree_ips n1›
                        ‹net_ips s2 = net_tree_ips n2›
          have "netgmap sr s1' = netmask (net_tree_ips n1) (σ', snd (netgmap sr s1'))"
            by (rule netgmap_subnet_split1)

        from ‹(s1, i:deliver(d), s1') ∈ trans (pnet np n1)›
             ‹netgmap sr s1 = netmask (net_tree_ips n1) (σ, snd (netgmap sr s1))›
             ‹netgmap sr s1' = netmask (net_tree_ips n1) (σ', snd (netgmap sr s1'))›
             ‹s1 ∈ reachable (pnet np n1) TT›
             ‹wf_net_tree n1›
             ‹i∈net_ips s1›
             ‹net_ip_action np (i:deliver(d)) i n1 s1 s1'›
          have "((σ, snd (netgmap sr s1)), i:deliver(d), (σ', snd (netgmap sr s1'))) ∈ trans (opnet onp n1)"
             by (rule IH1)

        with ‹s = SubnetS s1 s2› ‹s' = SubnetS s1' s2'› ‹s2' = s2› show ?thesis
          by simp (erule opnet_deliver1)
      next
        assume "i∈net_ips s2"
        with ‹s = SubnetS s1 s2› ‹s' = SubnetS s1' s2'› ‹net_ip_action np (i:deliver(d)) i (n1 ∥ n2) s s'›
          have "(s2, i:deliver(d), s2') ∈ trans (pnet np n2)"
           and "net_ip_action np (i:deliver(d)) i n2 s2 s2'"
           and "s1' = s1" by simp_all

        from ‹net_ips s2 = net_tree_ips n2› and ‹(s2, i:deliver(d), s2') ∈ trans (pnet np n2)›
          have "net_ips s2' = net_tree_ips n2" by (metis pnet_maintains_dom)

        from nm' [simplified ‹s' = SubnetS s1' s2'› ‹s1' = s1›]
                        ‹net_ips s1 = net_tree_ips n1›
                        ‹net_ips s2' = net_tree_ips n2›
          have "netgmap sr s2' = netmask (net_tree_ips n2) (σ', snd (netgmap sr s2'))"
            by (rule netgmap_subnet_split2)

        from ‹(s2, i:deliver(d), s2') ∈ trans (pnet np n2)›
             ‹netgmap sr s2 = netmask (net_tree_ips n2) (σ, snd (netgmap sr s2))›
             ‹netgmap sr s2' = netmask (net_tree_ips n2) (σ', snd (netgmap sr s2'))›
             ‹s2 ∈ reachable (pnet np n2) TT›
             ‹wf_net_tree n2›
             ‹i∈net_ips s2›
             ‹net_ip_action np (i:deliver(d)) i n2 s2 s2'›
          have "((σ, snd (netgmap sr s2)), i:deliver(d), (σ', snd (netgmap sr s2'))) ∈ trans (opnet onp n2)"
             by (rule IH2)

        with ‹s = SubnetS s1 s2› ‹s' = SubnetS s1' s2'› ‹s1' = s1› show ?thesis
          by simp (erule opnet_deliver2)
      qed
    qed
    with ‹ζ = snd (netgmap sr s)› have "((σ, ζ), i:deliver(d), (σ', snd (netgmap sr s'))) ∈ trans (opnet onp n)"
      by simp
    moreover from ‹∀j. j≠i ⟶ σ' j = σ j› ‹i ∈ net_ips s› ‹ζ = snd (netgmap sr s)›
      have "∀j. j∉net_ips ζ ⟶ σ' j = σ j" by (metis net_ips_netgmap)
    ultimately have "((σ, ζ), i:deliver(d), (σ', snd (netgmap sr s'))) ∈ trans (opnet onp n)
                     ∧ (∀j. j∉net_ips ζ ⟶ σ' j = σ j)
                     ∧ netgmap sr s' = netmask (net_tree_ips n) (σ', snd (netgmap sr s'))"
      using ‹netgmap sr s' = netmask (net_tree_ips n) (σ', snd (netgmap sr s'))› by simp
    thus "∃σ' ζ'. ((σ, ζ), i:deliver(d), (σ', ζ')) ∈ trans (opnet onp n)
                  ∧ (∀j. j∉net_ips ζ ⟶ σ' j = σ j)
                  ∧ netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')" by auto
  qed

lemma transfer_arrive':
  assumes "(s, H¬K:arrive(m), s') ∈ trans (pnet np n)"
      and "s ∈ reachable (pnet np n) TT"
      and "netgmap sr s = netmask (net_tree_ips n) (σ, ζ)"
      and "netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')"
      and "wf_net_tree n"
  shows "((σ, ζ), H¬K:arrive(m), (σ', ζ')) ∈ trans (opnet onp n)"
  proof -

    from assms(2) have "net_ips s = net_tree_ips n" ..
    with assms(1) have "net_ips s' = net_tree_ips n"
      by (metis pnet_maintains_dom)

    from ‹netgmap sr s = netmask (net_tree_ips n) (σ, ζ)›
      have "ζ = snd (netgmap sr s)" by simp

    from ‹netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')›
      have "ζ' = snd (netgmap sr s')"
       and "netgmap sr s' = netmask (net_tree_ips n) (σ', snd (netgmap sr s'))"
         by simp_all

    from assms(1-3) ‹netgmap sr s' = netmask (net_tree_ips n) (σ', snd (netgmap sr s'))› assms(5)
      have "((σ, snd (netgmap sr s)), H¬K:arrive(m), (σ', snd (netgmap sr s'))) ∈ trans (opnet onp n)"
      proof (induction n arbitrary: s s' ζ H K)
        fix ii R_i ns ns' ζ H K
        assume "(ns, H¬K:arrive(m), ns') ∈ trans (pnet np ⟨ii; R_i⟩)"
           and nsr: "ns ∈ reachable (pnet np ⟨ii; R_i⟩) TT"
           and "netgmap sr ns = netmask (net_tree_ips ⟨ii; R_i⟩) (σ, ζ)"
           and "netgmap sr ns' = netmask (net_tree_ips ⟨ii; R_i⟩) (σ', snd (netgmap sr ns'))"
        from this(1) have "(ns, H¬K:arrive(m), ns') ∈ node_sos (trans (np ii))"
          by (simp add: node_comps)
        moreover with nsr obtain s s' R where "ns = NodeS ii s R"
                                          and "ns' = NodeS ii s' R"
          by (metis net_node_reachable_is_node node_arriveTE')
        ultimately have "(NodeS ii s R, H¬K:arrive(m), NodeS ii s' R) ∈ node_sos (trans (np ii))"
          by simp
        from this(1) have "((σ, NodeS ii (snd (sr s)) R), H¬K:arrive(m), (σ', NodeS ii (snd (sr s')) R))
                                                                      ∈ onode_sos (trans (onp ii))"
        proof (rule node_arriveTE)
          assume "(s, receive m, s') ∈ trans (np ii)"
             and "H = {ii}"
             and "K = {}"
          from ‹netgmap sr ns = netmask (net_tree_ips ⟨ii; R_i⟩) (σ, ζ)› and ‹ns = NodeS ii s R›
            have "σ ii = fst (sr s)"
              by simp (metis map_upd_Some_unfold)
          moreover from ‹netgmap sr ns' = netmask (net_tree_ips ⟨ii; R_i⟩) (σ', snd (netgmap sr ns'))›
                        and ‹ns' = NodeS ii s' R›
            have "σ' ii = fst (sr s')" by simp (metis map_upd_Some_unfold)
          ultimately have "((σ, snd (sr s)), receive m, (σ', snd (sr s'))) ∈ trans (onp ii)"
            using ‹(s, receive m, s') ∈ trans (np ii)› by (rule trans)
          hence "((σ, NodeS ii (snd (sr s)) R), {ii}¬{}:arrive(m), (σ', NodeS ii (snd (sr s')) R))
                                                                      ∈ onode_sos (trans (onp ii))"
            by (rule onode_receive)
          with ‹H={ii}› and ‹K={}›
            show "((σ, NodeS ii (snd (sr s)) R), H¬K:arrive(m), (σ', NodeS ii (snd (sr s')) R))
                                                                      ∈ onode_sos (trans (onp ii))"
              by simp
        next
          assume "H = {}"
             and "s' = s"
             and "K = {ii}"
          from ‹s' = s› ‹netgmap sr ns' = netmask (net_tree_ips ⟨ii; R_i⟩) (σ', snd (netgmap sr ns'))›
                        ‹netgmap sr ns = netmask (net_tree_ips ⟨ii; R_i⟩) (σ, ζ)›
                        ‹ns = NodeS ii s R› and ‹ns' = NodeS ii s' R›
            have "σ' ii = σ ii" by simp (metis option.sel)
          hence "((σ, NodeS ii (snd (sr s)) R), {}¬{ii}:arrive(m), (σ', NodeS ii (snd (sr s)) R))
                                                                      ∈ onode_sos (trans (onp ii))"
            by (rule onode_arrive)
          with ‹H={}› ‹K={ii}› and ‹s' = s›
          show "((σ, NodeS ii (snd (sr s)) R), H¬K:arrive(m), (σ', NodeS ii (snd (sr s')) R))
                                                                     ∈ onode_sos (trans (onp ii))"
            by simp
        qed
      with ‹ns = NodeS ii s R› ‹ns' = NodeS ii s' R›
        show "((σ, snd (netgmap sr ns)), H¬K:arrive(m), (σ', snd (netgmap sr ns')))
                                                             ∈ trans (opnet onp ⟨ii; R_i⟩)"
          by (simp add: onode_comps)
    next
      fix n1 n2 s s' ζ H K
      assume IH1: "∧s s' ζ H K. (s, H¬K:arrive(m), s') ∈ trans (pnet np n1)
                         ==> s ∈ reachable (pnet np n1) TT
                         ==> netgmap sr s = netmask (net_tree_ips n1) (σ, ζ)
                         ==> netgmap sr s' = netmask (net_tree_ips n1) (σ', snd (netgmap sr s'))
                         ==> wf_net_tree n1
                         ==> ((σ, snd (netgmap sr s)), H¬K:arrive(m), σ', snd (netgmap sr s'))
                                                                        ∈ trans (opnet onp n1)"
        and IH2: "∧s s' ζ H K. (s, H¬K:arrive(m), s') ∈ trans (pnet np n2)
                         ==> s ∈ reachable (pnet np n2) TT
                         ==> netgmap sr s = netmask (net_tree_ips n2) (σ, ζ)
                         ==> netgmap sr s' = netmask (net_tree_ips n2) (σ', snd (netgmap sr s'))
                         ==> wf_net_tree n2
                         ==> ((σ, snd (netgmap sr s)), H¬K:arrive(m), σ', snd (netgmap sr s'))
                                                                        ∈ trans (opnet onp n2)"
        and "(s, H¬K:arrive(m), s') ∈ trans (pnet np (n1 ∥ n2))"
        and sr: "s ∈ reachable (pnet np (n1 ∥ n2)) TT"
        and nm: "netgmap sr s = netmask (net_tree_ips (n1 ∥ n2)) (σ, ζ)"
        and nm': "netgmap sr s' = netmask (net_tree_ips (n1 ∥ n2)) (σ', snd (netgmap sr s'))"
        and "wf_net_tree (n1 ∥ n2)"
      from this(3) have "(s, H¬K:arrive(m), s') ∈ pnet_sos (trans (pnet np n1))
                                                              (trans (pnet np n2))"
        by simp
      thus "((σ, snd (netgmap sr s)), H¬K:arrive(m), (σ', snd (netgmap sr s')))
                                                                   ∈ trans (opnet onp (n1 ∥ n2))"
      proof (rule partial_arriveTE)
        fix s1 s1' s2 s2' H1 H2 K1 K2
        assume "s = SubnetS s1 s2"
           and "s' = SubnetS s1' s2'"
           and tr1: "(s1, H1¬K1:arrive(m), s1') ∈ trans (pnet np n1)"
           and tr2: "(s2, H2¬K2:arrive(m), s2') ∈ trans (pnet np n2)"
           and "H = H1 ∪ H2"
           and "K = K1 ∪ K2"

        from ‹wf_net_tree (n1 ∥ n2)› have "wf_net_tree n1"
                                      and "wf_net_tree n2"
                                      and "net_tree_ips n1 ∩ net_tree_ips n2 = {}" by auto

        from sr [simplified ‹s = SubnetS s1 s2›] have "s1 ∈ reachable (pnet np n1) TT"
          by (rule subnet_reachable(1))
        hence "net_ips s1 = net_tree_ips n1" by (rule pnet_net_ips_net_tree_ips)
        with tr1 have "net_ips s1' = net_tree_ips n1" by (metis pnet_maintains_dom)

        from sr [simplified ‹s = SubnetS s1 s2›] have "s2 ∈ reachable (pnet np n2) TT"
          by (rule subnet_reachable(2))
        hence "net_ips s2 = net_tree_ips n2" by (rule pnet_net_ips_net_tree_ips)
        with tr2 have "net_ips s2' = net_tree_ips n2" by (metis pnet_maintains_dom)

        from ‹(s1, H1¬K1:arrive(m), s1') ∈ trans (pnet np n1)›
             ‹s1 ∈ reachable (pnet np n1) TT›
          have "((σ, snd (netgmap sr s1)), H1¬K1:arrive(m), (σ', snd (netgmap sr s1')))
                                                                            ∈ trans (opnet onp n1)"
          proof (rule IH1 [OF _ _ _ _ ‹wf_net_tree n1›])
            from nm [simplified ‹s = SubnetS s1 s2›]
                 ‹net_tree_ips n1 ∩ net_tree_ips n2 = {}›
                 ‹net_ips s1 = net_tree_ips n1›
                 ‹net_ips s2 = net_tree_ips n2›
              show "netgmap sr s1 = netmask (net_tree_ips n1) (σ, snd (netgmap sr s1))"
                by (rule netgmap_subnet_split1)
          next
            from nm' [simplified ‹s' = SubnetS s1' s2'›]
                 ‹net_tree_ips n1 ∩ net_tree_ips n2 = {}›
                 ‹net_ips s1' = net_tree_ips n1›
                 ‹net_ips s2' = net_tree_ips n2›
              show "netgmap sr s1' = netmask (net_tree_ips n1) (σ', snd (netgmap sr s1'))"
                by (rule netgmap_subnet_split1)
          qed

        moreover from ‹(s2, H2¬K2:arrive(m), s2') ∈ trans (pnet np n2)›
                      ‹s2 ∈ reachable (pnet np n2) TT›
          have "((σ, snd (netgmap sr s2)), H2¬K2:arrive(m), (σ', snd (netgmap sr s2')))
                                                                            ∈ trans (opnet onp n2)"
          proof (rule IH2 [OF _ _ _ _ ‹wf_net_tree n2›])
            from nm [simplified ‹s = SubnetS s1 s2›]
                 ‹net_ips s1 = net_tree_ips n1›
                 ‹net_ips s2 = net_tree_ips n2›
              show "netgmap sr s2 = netmask (net_tree_ips n2) (σ, snd (netgmap sr s2))"
                by (rule netgmap_subnet_split2)
          next
            from nm' [simplified ‹s' = SubnetS s1' s2'›]
                 ‹net_ips s1' = net_tree_ips n1›
                 ‹net_ips s2' = net_tree_ips n2›
              show "netgmap sr s2' = netmask (net_tree_ips n2) (σ', snd (netgmap sr s2'))"
                by (rule netgmap_subnet_split2)
          qed
        ultimately show "((σ, snd (netgmap sr s)), H¬K:arrive(m), (σ', snd (netgmap sr s')))
                                                                     ∈ trans (opnet onp (n1 ∥ n2))"
          using ‹s = SubnetS s1 s2› ‹s' = SubnetS s1' s2'› ‹H = H1 ∪ H2› ‹K = K1 ∪ K2›
            by simp (rule opnet_sos.opnet_arrive)
      qed
    qed
    with ‹ζ = snd (netgmap sr s)› and ‹ζ' = snd (netgmap sr s')›
      show "((σ, ζ), H¬K:arrive(m), (σ', ζ')) ∈ trans (opnet onp n)"
        by simp
  qed

lemma transfer_arrive:
  assumes "(s, H¬K:arrive(m), s') ∈ trans (pnet np n)"
      and "s ∈ reachable (pnet np n) TT"
      and "netgmap sr s = netmask (net_tree_ips n) (σ, ζ)"
      and "wf_net_tree n"
  obtains σ' ζ' where "((σ, ζ), H¬K:arrive(m), (σ', ζ')) ∈ trans (opnet onp n)"
                  and "∀j. j∉net_ips ζ ⟶ σ' j = σ j"
                  and "netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')"
  proof atomize_elim
    define σ' where "σ' i = (if i∈net_tree_ips n then the (fst (netgmap sr s') i) else σ i)" for i

    from assms(2) have "net_ips s = net_tree_ips n"
      by (rule pnet_net_ips_net_tree_ips)
    with assms(1) have "net_ips s' = net_tree_ips n"
      by (metis pnet_maintains_dom)

    have "netgmap sr s' = netmask (net_tree_ips n) (σ', snd (netgmap sr s'))"
    proof (rule prod_eqI)
      from ‹net_ips s' = net_tree_ips n›
        show "fst (netgmap sr s') = fst (netmask (net_tree_ips n) (σ', snd (netgmap sr s')))"
          unfolding σ'_def [abs_def] by - (rule ext, clarsimp)
    qed simp

    moreover with assms(1-3)
    have "((σ, ζ), H¬K:arrive(m), (σ', snd (netgmap sr s'))) ∈ trans (opnet onp n)"
      using ‹wf_net_tree n› by (rule transfer_arrive')

    moreover have "∀j. j∉net_ips ζ ⟶ σ' j = σ j"
    proof -
      have "∀j. j∉net_tree_ips n ⟶ σ' j = σ j" unfolding σ'_def by simp
      with assms(3) and ‹net_ips s = net_tree_ips n›
        show ?thesis
          by clarsimp (metis (mono_tags) net_ips_netgmap snd_conv)
    qed

    ultimately show "∃σ' ζ'. ((σ, ζ), H¬K:arrive(m), (σ', ζ')) ∈ trans (opnet onp n)
                          ∧ (∀j. j∉net_ips ζ ⟶ σ' j = σ j)
                          ∧ netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')" by auto
  qed

lemma transfer_cast:
  assumes "(s, mR:*cast(m), s') ∈ trans (pnet np n)"
      and "s ∈ reachable (pnet np n) TT"
      and "netgmap sr s = netmask (net_tree_ips n) (σ, ζ)"
      and "wf_net_tree n"
  obtains σ' ζ' where "((σ, ζ), mR:*cast(m), (σ', ζ')) ∈ trans (opnet onp n)"
                  and "∀j. j∉net_ips ζ ⟶ σ' j = σ j"
                  and "netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')"
  proof atomize_elim
    define σ' where "σ' i = (if i∈net_tree_ips n then the (fst (netgmap sr s') i) else σ i)" for i

    from assms(2) have "net_ips s = net_tree_ips n" ..
    with assms(1) have "net_ips s' = net_tree_ips n"
      by (metis pnet_maintains_dom)
    have "netgmap sr s' = netmask (net_tree_ips n) (σ', snd (netgmap sr s'))"
    proof (rule prod_eqI)
      from ‹net_ips s' = net_tree_ips n›
        show "fst (netgmap sr s') = fst (netmask (net_tree_ips n) (σ', snd (netgmap sr s')))"
      unfolding σ'_def [abs_def] by - (rule ext, clarsimp simp add: some_the_fst_netgmap)
    qed simp

    from ‹net_ips s' = net_tree_ips n› and ‹net_ips s = net_tree_ips n›
      have "∀j. j∉net_ips (snd (netgmap sr s)) ⟶ σ' j = σ j"
        unfolding σ'_def by simp

    from ‹netgmap sr s = netmask (net_tree_ips n) (σ, ζ)›
      have "ζ = snd (netgmap sr s)" by simp

    from assms(1-3) ‹netgmap sr s' = netmask (net_tree_ips n) (σ', snd (netgmap sr s'))› assms(4)
      have "((σ, snd (netgmap sr s)), mR:*cast(m), (σ', snd (netgmap sr s'))) ∈ trans (opnet onp n)"
      proof (induction n arbitrary: s s' ζ mR)
        fix ii R_i ns ns' ζ mR
        assume "(ns, mR:*cast(m), ns') ∈ trans (pnet np ⟨ii; R_i⟩)"
           and nsr: "ns ∈ reachable (pnet np ⟨ii; R_i⟩) TT"
           and "netgmap sr ns = netmask (net_tree_ips ⟨ii; R_i⟩) (σ, ζ)"
           and "netgmap sr ns' = netmask (net_tree_ips ⟨ii; R_i⟩) (σ', snd (netgmap sr ns'))"
        from this(1) have "(ns, mR:*cast(m), ns') ∈ node_sos (trans (np ii))"
          by (simp add: node_comps)
        moreover with nsr obtain s s' R where "ns = NodeS ii s R"
                                          and "ns' = NodeS ii s' R"
          by (metis net_node_reachable_is_node node_castTE')
        ultimately have "(NodeS ii s R, mR:*cast(m), NodeS ii s' R) ∈ node_sos (trans (np ii))"
          by simp

        from ‹netgmap sr ns = netmask (net_tree_ips ⟨ii; R_i⟩) (σ, ζ)› and ‹ns = NodeS ii s R›
          have "σ ii = fst (sr s)"
            by simp (metis map_upd_Some_unfold)
        from ‹netgmap sr ns' = netmask (net_tree_ips ⟨ii; R_i⟩) (σ', snd (netgmap sr ns'))›
             and ‹ns' = NodeS ii s' R›
          have "σ' ii = fst (sr s')" by simp (metis map_upd_Some_unfold)

        from ‹(NodeS ii s R, mR:*cast(m), NodeS ii s' R) ∈ node_sos (trans (np ii))›
          have "((σ, NodeS ii (snd (sr s)) R), mR:*cast(m), (σ', NodeS ii (snd (sr s')) R))
                                                                      ∈ onode_sos (trans (onp ii))"
        proof (rule node_castTE)
          assume "(s, broadcast m, s') ∈ trans (np ii)"
             and "mR = R"
          from ‹σ ii = fst (sr s)› ‹σ' ii = fst (sr s')› and this(1)
            have "((σ, snd (sr s)), broadcast m, (σ', snd (sr s'))) ∈ trans (onp ii)"
              by (rule trans)
          hence "((σ, NodeS ii (snd (sr s)) R), R:*cast(m), (σ', NodeS ii (snd (sr s')) R))
                                                                      ∈ onode_sos (trans (onp ii))"
            by (rule onode_bcast)
          with ‹mR = R› show "((σ, NodeS ii (snd (sr s)) R), mR:*cast(m), (σ', NodeS ii (snd (sr s')) R))
                                                                      ∈ onode_sos (trans (onp ii))"
              by simp
        next
          fix D
          assume "(s, groupcast D m, s') ∈ trans (np ii)"
             and "mR = R ∩ D"
          from ‹σ ii = fst (sr s)› ‹σ' ii = fst (sr s')› and this(1)
            have "((σ, snd (sr s)), groupcast D m, (σ', snd (sr s'))) ∈ trans (onp ii)"
              by (rule trans)
          hence "((σ, NodeS ii (snd (sr s)) R), (R ∩ D):*cast(m), (σ', NodeS ii (snd (sr s')) R))
                                                                      ∈ onode_sos (trans (onp ii))"
            by (rule onode_gcast)
          with ‹mR = R ∩ D› show "((σ, NodeS ii (snd (sr s)) R), mR:*cast(m), (σ', NodeS ii (snd (sr s')) R))
                                                                      ∈ onode_sos (trans (onp ii))"
              by simp
        next
          fix d
          assume "(s, unicast d m, s') ∈ trans (np ii)"
             and "d ∈ R"
             and "mR = {d}"
          from ‹σ ii = fst (sr s)› ‹σ' ii = fst (sr s')› and this(1)
            have "((σ, snd (sr s)), unicast d m, (σ', snd (sr s'))) ∈ trans (onp ii)"
              by (rule trans)
          hence "((σ, NodeS ii (snd (sr s)) R), {d}:*cast(m), (σ', NodeS ii (snd (sr s')) R))
                                                                      ∈ onode_sos (trans (onp ii))"
            using ‹d∈R› by (rule onode_ucast)
          with ‹mR={d}› show "((σ, NodeS ii (snd (sr s)) R), mR:*cast(m), (σ', NodeS ii (snd (sr s')) R))
                                                                      ∈ onode_sos (trans (onp ii))"
            by simp
        qed
      with ‹ns = NodeS ii s R› ‹ns' = NodeS ii s' R›
        show "((σ, snd (netgmap sr ns)), mR:*cast(m), (σ', snd (netgmap sr ns')))
                                                             ∈ trans (opnet onp ⟨ii; R_i⟩)"
          by (simp add: onode_comps)
    next
      fix n1 n2 s s' ζ mR
      assume IH1: "∧s s' ζ mR. (s, mR:*cast(m), s') ∈ trans (pnet np n1)
                         ==> s ∈ reachable (pnet np n1) TT
                         ==> netgmap sr s = netmask (net_tree_ips n1) (σ, ζ)
                         ==> netgmap sr s' = netmask (net_tree_ips n1) (σ', snd (netgmap sr s'))
                         ==> wf_net_tree n1
                         ==> ((σ, snd (netgmap sr s)), mR:*cast(m), σ', snd (netgmap sr s'))
                                                                        ∈ trans (opnet onp n1)"
        and IH2: "∧s s' ζ mR. (s, mR:*cast(m), s') ∈ trans (pnet np n2)
                         ==> s ∈ reachable (pnet np n2) TT
                         ==> netgmap sr s = netmask (net_tree_ips n2) (σ, ζ)
                         ==> netgmap sr s' = netmask (net_tree_ips n2) (σ', snd (netgmap sr s'))
                         ==> wf_net_tree n2
                         ==> ((σ, snd (netgmap sr s)), mR:*cast(m), σ', snd (netgmap sr s'))
                                                                        ∈ trans (opnet onp n2)"
        and "(s, mR:*cast(m), s') ∈ trans (pnet np (n1 ∥ n2))"
        and sr: "s ∈ reachable (pnet np (n1 ∥ n2)) TT"
        and nm: "netgmap sr s = netmask (net_tree_ips (n1 ∥ n2)) (σ, ζ)"
        and nm': "netgmap sr s' = netmask (net_tree_ips (n1 ∥ n2)) (σ', snd (netgmap sr s'))"
        and "wf_net_tree (n1 ∥ n2)"
      from this(3) have "(s, mR:*cast(m), s') ∈ pnet_sos (trans (pnet np n1)) (trans (pnet np n2))"
        by simp
      then obtain s1 s1' s2 s2' H K
        where "s = SubnetS s1 s2"
          and "s' = SubnetS s1' s2'"
          and "H ⊆ mR"
          and "K ∩ mR = {}"
          and trtr: "((s1, mR:*cast(m), s1') ∈ trans (pnet np n1)
                                  ∧ (s2, H¬K:arrive(m), s2') ∈ trans (pnet np n2))
                    ∨ ((s1, H¬K:arrive(m), s1') ∈ trans (pnet np n1)
                                  ∧ (s2, mR:*cast(m), s2') ∈ trans (pnet np n2))"
          by (rule partial_castTE) metis+

      from ‹wf_net_tree (n1 ∥ n2)› have "wf_net_tree n1"
                                    and "wf_net_tree n2"
                                    and "net_tree_ips n1 ∩ net_tree_ips n2 = {}" by auto

      from sr [simplified ‹s = SubnetS s1 s2›] have "s1 ∈ reachable (pnet np n1) TT"
        by (rule subnet_reachable(1))
      hence "net_ips s1 = net_tree_ips n1" by (rule pnet_net_ips_net_tree_ips)
      with trtr have "net_ips s1' = net_tree_ips n1" by (metis pnet_maintains_dom)

      from sr [simplified ‹s = SubnetS s1 s2›] have "s2 ∈ reachable (pnet np n2) TT"
        by (rule subnet_reachable(2))
      hence "net_ips s2 = net_tree_ips n2" by (rule pnet_net_ips_net_tree_ips)
      with trtr have "net_ips s2' = net_tree_ips n2" by (metis pnet_maintains_dom)

      from nm [simplified ‹s = SubnetS s1 s2›]
           ‹net_tree_ips n1 ∩ net_tree_ips n2 = {}›
           ‹net_ips s1 = net_tree_ips n1›
           ‹net_ips s2 = net_tree_ips n2›
        have "netgmap sr s1 = netmask (net_tree_ips n1) (σ, snd (netgmap sr s1))"
          by (rule netgmap_subnet_split1)

      from nm' [simplified ‹s' = SubnetS s1' s2'›]
           ‹net_tree_ips n1 ∩ net_tree_ips n2 = {}›
           ‹net_ips s1' = net_tree_ips n1›
           ‹net_ips s2' = net_tree_ips n2›
        have "netgmap sr s1' = netmask (net_tree_ips n1) (σ', snd (netgmap sr s1'))"
          by (rule netgmap_subnet_split1)

      from nm [simplified ‹s = SubnetS s1 s2›]
           ‹net_ips s1 = net_tree_ips n1›
           ‹net_ips s2 = net_tree_ips n2›
        have "netgmap sr s2 = netmask (net_tree_ips n2) (σ, snd (netgmap sr s2))"
          by (rule netgmap_subnet_split2)

      from nm' [simplified ‹s' = SubnetS s1' s2'›]
           ‹net_ips s1' = net_tree_ips n1›
           ‹net_ips s2' = net_tree_ips n2›
        have "netgmap sr s2' = netmask (net_tree_ips n2) (σ', snd (netgmap sr s2'))"
          by (rule netgmap_subnet_split2)

      from trtr show "((σ, snd (netgmap sr s)), mR:*cast(m), (σ', snd (netgmap sr s')))
                                                              ∈ trans (opnet onp (n1 ∥ n2))"
      proof (elim disjE conjE)
        assume "(s1, mR:*cast(m), s1') ∈ trans (pnet np n1)"
           and "(s2, H¬K:arrive(m), s2') ∈ trans (pnet np n2)"
        from ‹(s1, mR:*cast(m), s1') ∈ trans (pnet np n1)›
             ‹s1 ∈ reachable (pnet np n1) TT›
             ‹netgmap sr s1 = netmask (net_tree_ips n1) (σ, snd (netgmap sr s1))›
             ‹netgmap sr s1' = netmask (net_tree_ips n1) (σ', snd (netgmap sr s1'))›
             ‹wf_net_tree n1›
          have "((σ, snd (netgmap sr s1)), mR:*cast(m), (σ', snd (netgmap sr s1'))) ∈ trans (opnet onp n1)"
            by (rule IH1)

        moreover from ‹(s2, H¬K:arrive(m), s2') ∈ trans (pnet np n2)›
             ‹s2 ∈ reachable (pnet np n2) TT›
             ‹netgmap sr s2 = netmask (net_tree_ips n2) (σ, snd (netgmap sr s2))›
             ‹netgmap sr s2' = netmask (net_tree_ips n2) (σ', snd (netgmap sr s2'))›
             ‹wf_net_tree n2›
          have "((σ, snd (netgmap sr s2)), H¬K:arrive(m), (σ', snd (netgmap sr s2'))) ∈ trans (opnet onp n2)"
            by (rule transfer_arrive')

        ultimately have "((σ, SubnetS (snd (netgmap sr s1)) (snd (netgmap sr s2))), mR:*cast(m),
                          (σ', SubnetS (snd (netgmap sr s1')) (snd (netgmap sr s2'))))
                             ∈ opnet_sos (trans (opnet onp n1)) (trans (opnet onp n2))"
          using ‹H ⊆ mR› and ‹K ∩ mR = {}› by (rule opnet_sos.intros(1))
        with ‹s = SubnetS s1 s2› ‹s' = SubnetS s1' s2'› show ?thesis by simp
      next
        assume "(s1, H¬K:arrive(m), s1') ∈ trans (pnet np n1)"
           and "(s2, mR:*cast(m), s2') ∈ trans (pnet np n2)"
        from ‹(s1, H¬K:arrive(m), s1') ∈ trans (pnet np n1)›
             ‹s1 ∈ reachable (pnet np n1) TT›
             ‹netgmap sr s1 = netmask (net_tree_ips n1) (σ, snd (netgmap sr s1))›
             ‹netgmap sr s1' = netmask (net_tree_ips n1) (σ', snd (netgmap sr s1'))›
             ‹wf_net_tree n1›
          have "((σ, snd (netgmap sr s1)), H¬K:arrive(m), (σ', snd (netgmap sr s1'))) ∈ trans (opnet onp n1)"
            by (rule transfer_arrive')

        moreover from ‹(s2, mR:*cast(m), s2') ∈ trans (pnet np n2)›
             ‹s2 ∈ reachable (pnet np n2) TT›
             ‹netgmap sr s2 = netmask (net_tree_ips n2) (σ, snd (netgmap sr s2))›
             ‹netgmap sr s2' = netmask (net_tree_ips n2) (σ', snd (netgmap sr s2'))›
             ‹wf_net_tree n2›
          have "((σ, snd (netgmap sr s2)), mR:*cast(m), (σ', snd (netgmap sr s2'))) ∈ trans (opnet onp n2)"
            by (rule IH2)

        ultimately have "((σ, SubnetS (snd (netgmap sr s1)) (snd (netgmap sr s2))), mR:*cast(m),
                          (σ', SubnetS (snd (netgmap sr s1')) (snd (netgmap sr s2'))))
                             ∈ opnet_sos (trans (opnet onp n1)) (trans (opnet onp n2))"
          using ‹H ⊆ mR› and ‹K ∩ mR = {}› by (rule opnet_sos.intros(2))
        with ‹s = SubnetS s1 s2› ‹s' = SubnetS s1' s2'› show ?thesis by simp
      qed
    qed
    with ‹ζ = snd (netgmap sr s)› have "((σ, ζ), mR:*cast(m), (σ', snd (netgmap sr s'))) ∈ trans (opnet onp n)"
      by simp
    moreover from ‹∀j. j∉net_ips (snd (netgmap sr s)) ⟶ σ' j = σ j› ‹ζ = snd (netgmap sr s)›
      have "∀j. j∉net_ips ζ ⟶ σ' j = σ j" by simp
    moreover note ‹netgmap sr s' = netmask (net_tree_ips n) (σ', snd (netgmap sr s'))›
    ultimately show "∃σ' ζ'. ((σ, ζ), mR:*cast(m), (σ', ζ')) ∈ trans (opnet onp n)
                           ∧ (∀j. j∉net_ips ζ ⟶ σ' j = σ j)
                           ∧ netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')"
      by auto
  qed

lemma transfer_pnet_action:
  assumes "s ∈ reachable (pnet np n) TT"
      and "netgmap sr s = netmask (net_tree_ips n) (σ, ζ)"
      and "wf_net_tree n"
      and "(s, a, s') ∈ trans (pnet np n)"
  obtains σ' ζ' where "((σ, ζ), a, (σ', ζ')) ∈ trans (opnet onp n)"
                  and "∀j. j∉net_ips ζ ⟶ σ' j = σ j"
                  and "netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')"
  proof atomize_elim
    show "∃σ' ζ'. ((σ, ζ), a, (σ', ζ')) ∈ trans (opnet onp n)
                  ∧ (∀j. j∉net_ips ζ ⟶ σ' j = σ j)
                  ∧ netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')"
    proof (cases a)
      case node_cast
      with assms(4) show ?thesis
        by (auto elim!: transfer_cast [OF _ assms(1-3)])
    next
      case node_deliver
      with assms(4) show ?thesis
        by (auto elim!: transfer_deliver [OF _ assms(1-3)])
    next
      case node_arrive
      with assms(4) show ?thesis
        by (auto elim!: transfer_arrive [OF _ assms(1-3)])
    next
      case node_connect
      with assms(4) show ?thesis
        by (auto elim!: transfer_connect [OF _ assms(1-3)])
    next
      case node_disconnect
      with assms(4) show ?thesis
        by (auto elim!: transfer_disconnect [OF _ assms(1-3)])
    next
      case node_newpkt
      with assms(4) have False by (metis pnet_never_newpkt)
      thus ?thesis ..
    next
      case node_tau
      with assms(4) show ?thesis
        by (auto elim!: transfer_tau [OF _ assms(1-3), simplified])
    qed
  qed

lemma transfer_action_pnet_closed:
  assumes "(s, a, s') ∈ trans (closed (pnet np n))"
  obtains a' where "(s, a', s') ∈ trans (pnet np n)"
               and "∧σ ζ σ' ζ'. [ ((σ, ζ), a', (σ', ζ')) ∈ trans (opnet onp n);
                                  (∀j. j∉net_ips ζ ⟶ σ' j = σ j) ]
                            ==> ((σ, ζ), a, (σ', ζ')) ∈ trans (oclosed (opnet onp n))"
  proof (atomize_elim)
    from assms have "(s, a, s') ∈ cnet_sos (trans (pnet np n))" by simp
    thus "∃a'. (s, a', s') ∈ trans (pnet np n)
                ∧ (∀σ ζ σ' ζ'. ((σ, ζ), a', (σ', ζ')) ∈ trans (opnet onp n)
                               ⟶ (∀j. j ∉ net_ips ζ ⟶ σ' j = σ j)
                               ⟶ ((σ, ζ), a, (σ', ζ')) ∈ trans (oclosed (opnet onp n)))"
    proof cases
      case (cnet_cast R m) thus ?thesis
      by (auto intro!: exI [where x="R:*cast(m)"] dest!: ocnet_cast)
    qed (auto intro!: ocnet_sos.intros [simplified])
  qed

lemma transfer_action:
  assumes "s ∈ reachable (closed (pnet np n)) TT"
      and "netgmap sr s = netmask (net_tree_ips n) (σ, ζ)"
      and "wf_net_tree n"
      and "(s, a, s') ∈ trans (closed (pnet np n))"
  obtains σ' ζ' where "((σ, ζ), a, (σ', ζ')) ∈ trans (oclosed (opnet onp n))"
                  and "netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')"
  proof atomize_elim
    from assms(1) have "s ∈ reachable (pnet np n) TT" ..
    from assms(4)
      show "∃σ' ζ'. ((σ, ζ), a, (σ', ζ')) ∈ trans (oclosed (opnet onp n))
                    ∧ netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')"
        by (cases a)
           ((elim transfer_action_pnet_closed
                  transfer_pnet_action [OF ‹s ∈ reachable (pnet np n) TT› assms(2-3)])?,
            (auto intro!: exI)[1])+
  qed

lemma pnet_reachable_transfer':
  assumes "wf_net_tree n"
      and "s ∈ reachable (closed (pnet np n)) TT"
    shows "netgmap sr s ∈ netmask (net_tree_ips n) ` oreachable (oclosed (opnet onp n)) (λ_ _ _. True) U"
          (is " _ ∈ ?f ` ?oreachable n")
  using assms(2) proof induction
    fix s
    assume "s ∈ init (closed (pnet np n))"
    hence "s ∈ init (pnet np n)" by simp
    with ‹wf_net_tree n› have "netgmap sr s ∈ netmask (net_tree_ips n) ` init (opnet onp n)"
      by (rule init_pnet_opnet)
    hence "netgmap sr s ∈ netmask (net_tree_ips n) ` init (oclosed (opnet onp n))"
      by simp
    moreover have "netmask (net_tree_ips n) ` init (oclosed (opnet onp n))
                                        ⊆ netmask (net_tree_ips n) ` ?oreachable n"
      by (intro image_mono subsetI) (rule oreachable_init)
    ultimately show "netgmap sr s ∈ netmask (net_tree_ips n) ` ?oreachable n"
      by (rule rev_subsetD)
  next
    fix s a s'
    assume "s ∈ reachable (closed (pnet np n)) TT"
       and "netgmap sr s ∈ netmask (net_tree_ips n) ` ?oreachable n"
       and "(s, a, s') ∈ trans (closed (pnet np n))"
    from this(2) obtain σ ζ where "netgmap sr s = netmask (net_tree_ips n) (σ, ζ)"
                              and "(σ, ζ) ∈ ?oreachable n"
      by clarsimp
    from ‹s ∈ reachable (closed (pnet np n)) TT› this(1) ‹wf_net_tree n›
         and ‹(s, a, s') ∈ trans (closed (pnet np n))›
      obtain σ' ζ' where "((σ, ζ), a, (σ', ζ')) ∈ trans (oclosed (opnet onp n))"
                     and "netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')"
        by (rule transfer_action)
    from ‹(σ, ζ) ∈ ?oreachable n› and this(1) have "(σ', ζ') ∈ ?oreachable n"
      by (rule oreachable_local) simp
    with ‹netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')›
      show "netgmap sr s' ∈ netmask (net_tree_ips n) ` ?oreachable n" by (rule image_eqI)
  qed

definition
  someinit :: "nat ==> 'g"
where
  "someinit i ≡ SOME x. x ∈ (fst o sr) ` init (np i)"

definition
  initmissing :: "((nat ==> 'g option) × 'a) ==> (nat ==> 'g) × 'a"
where
  "initmissing σ = (λi. case (fst σ) i of None ==> someinit i | Some s ==> s, snd σ)"

lemma initmissing_def':
  "initmissing = apfst (default someinit)"
  by (auto simp add: initmissing_def default_def)

lemma netmask_initmissing_netgmap:
  "netmask (net_ips s) (initmissing (netgmap sr s)) = netgmap sr s"
  proof (intro prod_eqI ext)
    fix i
    show "fst (netmask (net_ips s) (initmissing (netgmap sr s))) i = fst (netgmap sr s) i"
      unfolding initmissing_def by (clarsimp split: option.split)
  qed (simp add: initmissing_def)

lemma snd_initmissing [simp]:
  "snd (initmissing x)= snd x"
  unfolding initmissing_def by simp

lemma initmnissing_snd_netgmap [simp]:
  assumes "initmissing (netgmap sr s) = (σ, ζ)"
    shows "snd (netgmap sr s) = ζ"
  using assms unfolding initmissing_def by simp


lemma in_net_ips_fst_init_missing [simp]:
  assumes "i ∈ net_ips s"
    shows "fst (initmissing (netgmap sr s)) i = the (fst (netgmap sr s) i)"
  using assms unfolding initmissing_def by (clarsimp split: option.split)

lemma not_in_net_ips_fst_init_missing [simp]:
  assumes "i ∉ net_ips s"
    shows "fst (initmissing (netgmap sr s)) i = someinit i"
  using assms unfolding initmissing_def by (clarsimp split: option.split)

lemma initmissing_oreachable_netmask [elim]:
  assumes "initmissing (netgmap sr s) ∈ oreachable (oclosed (opnet onp n)) (λ_ _ _. True) U"
          (is "_ ∈ ?oreachable n")
      and "net_ips s = net_tree_ips n"
    shows "netgmap sr s ∈ netmask (net_tree_ips n) ` ?oreachable n"
  proof -
    obtain σ ζ where "initmissing (netgmap sr s) = (σ, ζ)" by (metis surj_pair)
    with assms(1) have "(σ, ζ) ∈ ?oreachable n" by simp

    have "netgmap sr s = netmask (net_ips s) (σ, ζ)"
    proof (intro prod_eqI ext)
      fix i
      show "fst (netgmap sr s) i = fst (netmask (net_ips s) (σ, ζ)) i"
      proof (cases "i∈net_ips s")
        assume "i∈net_ips s"
        hence "fst (initmissing (netgmap sr s)) i = the (fst (netgmap sr s) i)"
          by (rule in_net_ips_fst_init_missing)
        moreover from ‹i∈net_ips s› have "Some (the (fst (netgmap sr s) i)) = fst (netgmap sr s) i"
          by (rule some_the_fst_netgmap)
        ultimately show ?thesis
          using ‹initmissing (netgmap sr s) = (σ, ζ)› by simp
      qed simp
    next
      from ‹initmissing (netgmap sr s) = (σ, ζ)›
        show "snd (netgmap sr s) = snd (netmask (net_ips s) (σ, ζ))"
          by simp
    qed
    with assms(2) have "netgmap sr s = netmask (net_tree_ips n) (σ, ζ)" by simp
    moreover from ‹(σ, ζ) ∈ ?oreachable n›
      have "netmask (net_ips s) (σ, ζ) ∈ netmask (net_ips s) ` ?oreachable n"
        by (rule imageI)
    ultimately show ?thesis
      by (simp only: assms(2))
  qed

lemma pnet_reachable_transfer:
  assumes "wf_net_tree n"
      and "s ∈ reachable (closed (pnet np n)) TT"
    shows "initmissing (netgmap sr s) ∈ oreachable (oclosed (opnet onp n)) (λ_ _ _. True) U"
          (is " _ ∈ ?oreachable n")
  using assms(2) proof induction
    fix s
    assume "s ∈ init (closed (pnet np n))"
    hence "s ∈ init (pnet np n)" by simp

    from ‹wf_net_tree n› have "initmissing (netgmap sr s) ∈ init (opnet onp n)"
    proof (rule init_lifted [THEN subsetD], intro CollectI exI conjI allI)
      show "initmissing (netgmap sr s) = (fst (initmissing (netgmap sr s)), snd (netgmap sr s))"
        by (metis snd_initmissing surjective_pairing)
    next
      from ‹s ∈ init (pnet np n)› show "s ∈ init (pnet np n)" ..
    next
      fix i
      show "if i ∈ net_tree_ips n
            then (fst (initmissing (netgmap sr s))) i = the (fst (netgmap sr s) i)
            else (fst (initmissing (netgmap sr s))) i ∈ (fst ∘ sr) ` init (np i)"
      proof (cases "i ∈ net_tree_ips n", simp_all only: if_True if_False)
        assume "i ∈ net_tree_ips n"
        with ‹s ∈ init (pnet np n)› have "i ∈ net_ips s" ..
        thus "fst (initmissing (netgmap sr s)) i = the (fst (netgmap sr s) i)" by simp
      next
        assume "i ∉ net_tree_ips n"
        with ‹s ∈ init (pnet np n)› have "i ∉ net_ips s" ..
        hence "fst (initmissing (netgmap sr s)) i = someinit i" by simp
        moreover have "someinit i ∈ (fst ∘ sr) ` init (np i)"
        unfolding someinit_def proof (rule someI_ex)
          from init_notempty show "∃x. x ∈ (fst o sr) ` init (np i)" by auto
        qed
        ultimately show "fst (initmissing (netgmap sr s)) i ∈ (fst ∘ sr) ` init (np i)"
          by simp
      qed
    qed
    hence "initmissing (netgmap sr s) ∈ init (oclosed (opnet onp n))" by simp
    thus "initmissing (netgmap sr s) ∈ ?oreachable n" ..
  next
    fix s a s'
    assume "s ∈ reachable (closed (pnet np n)) TT"
       and "(s, a, s') ∈ trans (closed (pnet np n))"
       and "initmissing (netgmap sr s) ∈ ?oreachable n"
    from this(1) have "s ∈ reachable (pnet np n) TT" ..
    hence "net_ips s = net_tree_ips n" by (rule pnet_net_ips_net_tree_ips)
    with ‹initmissing (netgmap sr s) ∈ ?oreachable n›
      have "netgmap sr s ∈ netmask (net_tree_ips n) ` ?oreachable n"
        by (rule initmissing_oreachable_netmask)

    obtain σ ζ where "(σ, ζ) = initmissing (netgmap sr s)" by (metis surj_pair)
    with ‹initmissing (netgmap sr s) ∈ ?oreachable n›
      have "(σ, ζ) ∈ ?oreachable n" by simp
    from ‹(σ, ζ) = initmissing (netgmap sr s)› and ‹net_ips s = net_tree_ips n› [symmetric]
      have "netgmap sr s = netmask (net_tree_ips n) (σ, ζ)"
        by (clarsimp simp add: netmask_initmissing_netgmap)

    with ‹s ∈ reachable (closed (pnet np n)) TT›
      obtain σ' ζ' where "((σ, ζ), a, (σ', ζ')) ∈ trans (oclosed (opnet onp n))"
                     and "netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')"
        using ‹wf_net_tree n› and ‹(s, a, s') ∈ trans (closed (pnet np n))›
        by (rule transfer_action)

    from ‹(σ, ζ) ∈ ?oreachable n› have "net_ips ζ = net_tree_ips n"
      by (rule opnet_net_ips_net_tree_ips [OF oclosed_oreachable_oreachable])
    with ‹((σ, ζ), a, (σ', ζ')) ∈ trans (oclosed (opnet onp n))›
      have "∀j. j∉net_tree_ips n ⟶ σ' j = σ j"
        by (clarsimp elim!: ocomplete_no_change)
    have "initmissing (netgmap sr s') = (σ', ζ')"
    proof (intro prod_eqI ext)
      fix i
      from ‹netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')›
           ‹∀j. j∉net_tree_ips n ⟶ σ' j = σ j›
           ‹(σ, ζ) = initmissing (netgmap sr s)›
           ‹net_ips s = net_tree_ips n›
      show "fst (initmissing (netgmap sr s')) i = fst (σ', ζ') i"
        unfolding initmissing_def by simp
    next
      from ‹netgmap sr s' = netmask (net_tree_ips n) (σ', ζ')›
        show "snd (initmissing (netgmap sr s')) = snd (σ', ζ')" by simp
    qed
    moreover from ‹(σ, ζ) ∈ ?oreachable n› ‹((σ, ζ), a, (σ', ζ')) ∈ trans (oclosed (opnet onp n))›
      have "(σ', ζ') ∈ ?oreachable n"
        by (rule oreachable_local) (rule TrueI)

    ultimately show "initmissing (netgmap sr s') ∈ ?oreachable n"
      by simp
  qed

definition
  netglobal :: "((nat ==> 'g) ==> bool) ==> 's net_state ==> bool"
where
  "netglobal P ≡ (λs. P (fst (initmissing (netgmap sr s))))"

lemma netglobalsimp [simp]:
  "netglobal P s = P (fst (initmissing (netgmap sr s)))"
  unfolding netglobal_def by simp

lemma netglobalE [elim]:
  assumes "netglobal P s"
      and "∧σ. [ P σ; fst (initmissing (netgmap sr s)) = σ ] ==> Q σ"
    shows "netglobal Q s"
  using assms by simp

lemma netglobal_weakenE [elim]:
  assumes "p ⊨!!! netglobal P"
      and "∧σ. P σ ==> Q σ"
    shows "p ⊨!!! netglobal Q"
  using assms(1) proof (rule invariant_weakenE)
    fix s
    assume "netglobal P s"
    thus "netglobal Q s"
      by (rule netglobalE) (erule assms(2))
  qed

lemma close_opnet:
  assumes "wf_net_tree n"
      and "oclosed (opnet onp n) ⊨ (λ_ _ _. True, U →) global P"
    shows "closed (pnet np n) ⊨!!! netglobal P"
  unfolding invariant_def proof
    fix s
    assume "s ∈ reachable (closed (pnet np n)) TT"
    with assms(1)
      have "initmissing (netgmap sr s) ∈ oreachable (oclosed (opnet onp n)) (λ_ _ _. True) U"
        by (rule pnet_reachable_transfer)
    with assms(2) have "global P (initmissing (netgmap sr s))" ..
    thus "netglobal P s" by simp
  qed

end

locale openproc_parq =
  op?: openproc np onp sr for np :: "ip ==> ('s, ('m::msg) seq_action) automaton" and onp sr
  + fixes qp :: "('t, 'm seq_action) automaton"
    assumes init_qp_notempty: "init qp ≠ {}"

sublocale openproc_parq ⊆ openproc "λi. np i ⟨⟨ qp"
                                   "λi. onp i ⟨⟨ qp"
                                   "λ(p, q). (fst (sr p), (snd (sr p), q))"
  proof unfold_locales
    fix i
    show "{ (σ, ζ) |σ ζ s. s ∈ init (np i ⟨⟨ qp)
                         ∧ (σ i, ζ) = ((λ(p, q). (fst (sr p), (snd (sr p), q))) s)
                         ∧ (∀j. j≠i ⟶ σ j ∈ (fst o (λ(p, q). (fst (sr p), (snd (sr p), q))))
                                                  ` init (np j ⟨⟨ qp)) } ⊆ init (onp i ⟨⟨ qp)"
       (is "?S ⊆ _")
    proof
      fix s
      assume "s ∈ ?S"
      then obtain σ p lq
        where "s = (σ, (snd (sr p), lq))"
          and "lq ∈ init qp"
          and "p ∈ init (np i)"
          and "σ i = fst (sr p)"
          and "∀j. j ≠ i ⟶ σ j ∈ (fst ∘ (λ(p, q). (fst (sr p), snd (sr p), q)))
                                                                        ` (init (np j) × init qp)"
        by auto
      from this(5) have "∀j. j ≠ i ⟶ σ j ∈ (fst ∘ sr) ` init (np j)"
        by auto
      with ‹p ∈ init (np i)› and ‹σ i = fst (sr p)› have "(σ, snd (sr p)) ∈ init (onp i)"
        by - (rule init [THEN subsetD], auto)
      with ‹lq∈ init qp› have "((σ, snd (sr p)), lq) ∈ init (onp i) × init qp"
        by simp
      hence "(σ, (snd (sr p), lq)) ∈ extg ` (init (onp i) × init qp)"
        by (rule rev_image_eqI) simp
      with ‹s = (σ, (snd (sr p), lq))› show "s ∈ init (onp i ⟨⟨ qp)"
        by simp
    qed
  next
    fix i s a s' σ σ'
    assume "σ i = fst ((λ(p, q). (fst (sr p), (snd (sr p), q))) s)"
       and "σ' i = fst ((λ(p, q). (fst (sr p), (snd (sr p), q))) s')"
       and "(s, a, s') ∈ trans (np i ⟨⟨ qp)"
    then obtain p q p' q' where "s = (p, q)"
                            and "s' = (p', q')"
                            and "σ i = fst (sr p)"
                            and "σ' i = fst (sr p')"
      by (clarsimp split: prod.split_asm)
    from this(1-2) and ‹(s, a, s') ∈ trans (np i ⟨⟨ qp)›
      have "((p, q), a, (p', q')) ∈ parp_sos (trans (np i)) (trans qp)" by simp
    hence "((σ, (snd (sr p), q)), a, (σ', (snd (sr p'), q'))) ∈ trans (onp i ⟨⟨ qp)"
    proof cases
      assume "q' = q"
         and "(p, a, p') ∈ trans (np i)"
         and "∧m. a ≠ receive m"
      from ‹σ i = fst (sr p)› and ‹σ' i = fst (sr p')› this(2)
        have "((σ, snd (sr p)), a, (σ', snd (sr p'))) ∈ trans (onp i)" by (rule trans)
      with ‹q' = q› and ‹∧m. a ≠ receive m›
        show "((σ, snd (sr p), q), a, (σ', (snd (sr p'), q'))) ∈ trans (onp i ⟨⟨ qp)"
          by (auto elim!: oparleft)
    next
      assume "p' = p"
         and "(q, a, q') ∈ trans qp"
         and "∧m. a ≠ send m"
      with ‹σ i = fst (sr p)› and ‹σ' i = fst (sr p')›
        show "((σ, snd (sr p), q), a, (σ', (snd (sr p'), q'))) ∈ trans (onp i ⟨⟨ qp)"
          by (auto elim!: oparright)
    next
      fix m
      assume "a = τ"
         and "(p, receive m, p') ∈ trans (np i)"
         and "(q, send m, q') ∈ trans qp"
      from ‹σ i = fst (sr p)› and ‹σ' i = fst (sr p')› this(2)
        have "((σ, snd (sr p)), receive m, (σ', snd (sr p'))) ∈ trans (onp i)"
          by (rule trans)
      with ‹(q, send m, q') ∈ trans qp› and ‹a = τ›
        show "((σ, snd (sr p), q), a, (σ', (snd (sr p'), q'))) ∈ trans (onp i ⟨⟨ qp)"
          by (simp del: step_seq_tau) (rule oparboth)
    qed
    with ‹s = (p, q)› ‹s' = (p', q')›
      show "((σ, snd ((λ(p, q). (fst (sr p), (snd (sr p), q))) s)), a,
                 (σ', snd ((λ(p, q). (fst (sr p), (snd (sr p), q))) s'))) ∈ trans (onp i ⟨⟨ qp)"
        by simp
  next
    show "∀j. init (np j ⟨⟨ qp) ≠ {}"
      by (clarsimp simp add: init_notempty init_qp_notempty)
  qed

end