[STATEMENT]
lemma access_matrix_complete:
      fixes rs :: "'i::len simple_rule list"
      assumes matrix: "(V,E) = access_matrix c rs" and
              allow: "runFw s d c rs = Decision FinalAllow"
      shows "\<exists>s_repr d_repr s_range d_range. (s_repr, d_repr) \<in> set E \<and>
              (map_of V) s_repr = Some s_range \<and> s \<in> wordinterval_to_set s_range \<and>
              (map_of V) d_repr = Some d_range \<and> d \<in> wordinterval_to_set d_range"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>s_repr d_repr s_range d_range. (s_repr, d_repr) \<in> set E \<and> map_of V s_repr = Some s_range \<and> s \<in> wordinterval_to_set s_range \<and> map_of V d_repr = Some d_range \<and> d \<in> wordinterval_to_set d_range
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>s_repr d_repr s_range d_range. (s_repr, d_repr) \<in> set E \<and> map_of V s_repr = Some s_range \<and> s \<in> wordinterval_to_set s_range \<and> map_of V d_repr = Some d_range \<and> d \<in> wordinterval_to_set d_range
[PROOF STEP]
let ?part="(build_ip_partition c rs)"
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>s_repr d_repr s_range d_range. (s_repr, d_repr) \<in> set E \<and> map_of V s_repr = Some s_range \<and> s \<in> wordinterval_to_set s_range \<and> map_of V d_repr = Some d_range \<and> d \<in> wordinterval_to_set d_range
[PROOF STEP]
have V: "V = zip (map getOneIp ?part) ?part"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. V = zip (map getOneIp (build_ip_partition c rs)) (build_ip_partition c rs)
[PROOF STEP]
using matrix
[PROOF STATE]
proof (prove)
using this:
(V, E) = access_matrix c rs

goal (1 subgoal):
 1. V = zip (map getOneIp (build_ip_partition c rs)) (build_ip_partition c rs)
[PROOF STEP]
by(simp add: access_matrix_def Let_def)
[PROOF STATE]
proof (state)
this:
V = zip (map getOneIp (build_ip_partition c rs)) (build_ip_partition c rs)

goal (1 subgoal):
 1. \<exists>s_repr d_repr s_range d_range. (s_repr, d_repr) \<in> set E \<and> map_of V s_repr = Some s_range \<and> s \<in> wordinterval_to_set s_range \<and> map_of V d_repr = Some d_range \<and> d \<in> wordinterval_to_set d_range
[PROOF STEP]
have E: "E = [(s, d)\<leftarrow>all_pairs (map getOneIp ?part). runFw s d c rs = Decision FinalAllow]"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. E = filter (\<lambda>(s, d). runFw s d c rs = Decision FinalAllow) (all_pairs (map getOneIp (build_ip_partition c rs)))
[PROOF STEP]
using matrix
[PROOF STATE]
proof (prove)
using this:
(V, E) = access_matrix c rs

goal (1 subgoal):
 1. E = filter (\<lambda>(s, d). runFw s d c rs = Decision FinalAllow) (all_pairs (map getOneIp (build_ip_partition c rs)))
[PROOF STEP]
by(simp add: access_matrix_def Let_def)
[PROOF STATE]
proof (state)
this:
E = filter (\<lambda>(s, d). runFw s d c rs = Decision FinalAllow) (all_pairs (map getOneIp (build_ip_partition c rs)))

goal (1 subgoal):
 1. \<exists>s_repr d_repr s_range d_range. (s_repr, d_repr) \<in> set E \<and> map_of V s_repr = Some s_range \<and> s \<in> wordinterval_to_set s_range \<and> map_of V d_repr = Some d_range \<and> d \<in> wordinterval_to_set d_range
[PROOF STEP]
have build_ip_partition_obtain:
      "\<exists>V. V \<in> set (build_ip_partition c rs) \<and> s \<in> wordinterval_to_set V" for s
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>V. V \<in> set (build_ip_partition c rs) \<and> s \<in> wordinterval_to_set V
[PROOF STEP]
using build_ip_partition_complete
[PROOF STATE]
proof (prove)
using this:
\<Union> (wordinterval_to_set ` set (build_ip_partition ?c ?rs)) = UNIV

goal (1 subgoal):
 1. \<exists>V. V \<in> set (build_ip_partition c rs) \<and> s \<in> wordinterval_to_set V
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>V. V \<in> set (build_ip_partition c rs) \<and> ?s \<in> wordinterval_to_set V

goal (1 subgoal):
 1. \<exists>s_repr d_repr s_range d_range. (s_repr, d_repr) \<in> set E \<and> map_of V s_repr = Some s_range \<and> s \<in> wordinterval_to_set s_range \<and> map_of V d_repr = Some d_range \<and> d \<in> wordinterval_to_set d_range
[PROOF STEP]
have distinct_map_getOneIp_build_ip_partition_obtain:
        "v \<in> set (build_ip_partition c rs) \<Longrightarrow>
           \<exists>s_repr. map_of (zip (map getOneIp (build_ip_partition c rs)) (build_ip_partition c rs)) s_repr = Some v"
      for v and rs :: "'i::len simple_rule list"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. v \<in> set (build_ip_partition c rs) \<Longrightarrow> \<exists>s_repr. map_of (zip (map getOneIp (build_ip_partition c rs)) (build_ip_partition c rs)) s_repr = Some v
[PROOF STEP]
proof(erule distinct_map_getOneIp_obtain)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. distinct (map getOneIp (build_ip_partition c rs))
[PROOF STEP]
show "distinct (map getOneIp (build_ip_partition c rs))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (map getOneIp (build_ip_partition c rs))
[PROOF STEP]
apply(rule map_getOneIp_distinct)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. distinct (build_ip_partition c rs)
 2. \<forall>x1\<in>set (build_ip_partition c rs). \<forall>x2\<in>set (build_ip_partition c rs). x1 \<noteq> x2 \<longrightarrow> wordinterval_to_set x1 \<inter> wordinterval_to_set x2 = {}
 3. \<forall>x\<in>set (build_ip_partition c rs). \<not> wordinterval_empty x
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. distinct (build_ip_partition c rs)
[PROOF STEP]
using build_ip_partition_distinct'
[PROOF STATE]
proof (prove)
using this:
distinct (build_ip_partition ?c ?rs)

goal (1 subgoal):
 1. distinct (build_ip_partition c rs)
[PROOF STEP]
by blast
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<forall>x1\<in>set (build_ip_partition c rs). \<forall>x2\<in>set (build_ip_partition c rs). x1 \<noteq> x2 \<longrightarrow> wordinterval_to_set x1 \<inter> wordinterval_to_set x2 = {}
 2. \<forall>x\<in>set (build_ip_partition c rs). \<not> wordinterval_empty x
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x1\<in>set (build_ip_partition c rs). \<forall>x2\<in>set (build_ip_partition c rs). x1 \<noteq> x2 \<longrightarrow> wordinterval_to_set x1 \<inter> wordinterval_to_set x2 = {}
[PROOF STEP]
using build_ip_partition_disjoint build_ip_partition_distinct'
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?V1.0 \<in> set (build_ip_partition ?c ?rs); ?V2.0 \<in> set (build_ip_partition ?c ?rs); ?V1.0 \<noteq> ?V2.0\<rbrakk> \<Longrightarrow> wordinterval_to_set ?V1.0 \<inter> wordinterval_to_set ?V2.0 = {}
distinct (build_ip_partition ?c ?rs)

goal (1 subgoal):
 1. \<forall>x1\<in>set (build_ip_partition c rs). \<forall>x2\<in>set (build_ip_partition c rs). x1 \<noteq> x2 \<longrightarrow> wordinterval_to_set x1 \<inter> wordinterval_to_set x2 = {}
[PROOF STEP]
by blast
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>set (build_ip_partition c rs). \<not> wordinterval_empty x
[PROOF STEP]
subgoal
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>set (build_ip_partition c rs). \<not> wordinterval_empty x
[PROOF STEP]
using build_ip_partition_no_empty_elems[simplified]
[PROOF STATE]
proof (prove)
using this:
?wi \<in> set (build_ip_partition ?c ?rs) \<Longrightarrow> wordinterval_to_set ?wi \<noteq> {}

goal (1 subgoal):
 1. \<forall>x\<in>set (build_ip_partition c rs). \<not> wordinterval_empty x
[PROOF STEP]
by auto
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
distinct (map getOneIp (build_ip_partition c rs))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
?v \<in> set (build_ip_partition c ?rs) \<Longrightarrow> \<exists>s_repr. map_of (zip (map getOneIp (build_ip_partition c ?rs)) (build_ip_partition c ?rs)) s_repr = Some ?v

goal (1 subgoal):
 1. \<exists>s_repr d_repr s_range d_range. (s_repr, d_repr) \<in> set E \<and> map_of V s_repr = Some s_range \<and> s \<in> wordinterval_to_set s_range \<and> map_of V d_repr = Some d_range \<and> d \<in> wordinterval_to_set d_range
[PROOF STEP]
from build_ip_partition_obtain
[PROOF STATE]
proof (chain)
picking this:
\<exists>V. V \<in> set (build_ip_partition c rs) \<and> ?s \<in> wordinterval_to_set V
[PROOF STEP]
obtain s_range where
      "s_range \<in> set ?part" and "s \<in> wordinterval_to_set s_range"
[PROOF STATE]
proof (prove)
using this:
\<exists>V. V \<in> set (build_ip_partition c rs) \<and> ?s \<in> wordinterval_to_set V

goal (1 subgoal):
 1. (\<And>s_range. \<lbrakk>s_range \<in> set (build_ip_partition c rs); s \<in> wordinterval_to_set s_range\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
s_range \<in> set (build_ip_partition c rs)
s \<in> wordinterval_to_set s_range

goal (1 subgoal):
 1. \<exists>s_repr d_repr s_range d_range. (s_repr, d_repr) \<in> set E \<and> map_of V s_repr = Some s_range \<and> s \<in> wordinterval_to_set s_range \<and> map_of V d_repr = Some d_range \<and> d \<in> wordinterval_to_set d_range
[PROOF STEP]
from this distinct_map_getOneIp_build_ip_partition_obtain V
[PROOF STATE]
proof (chain)
picking this:
s_range \<in> set (build_ip_partition c rs)
s \<in> wordinterval_to_set s_range
?v \<in> set (build_ip_partition c ?rs) \<Longrightarrow> \<exists>s_repr. map_of (zip (map getOneIp (build_ip_partition c ?rs)) (build_ip_partition c ?rs)) s_repr = Some ?v
V = zip (map getOneIp (build_ip_partition c rs)) (build_ip_partition c rs)
[PROOF STEP]
obtain s_repr where
      ex_s1: "(map_of V) s_repr = Some s_range" and ex_s2: "s \<in> wordinterval_to_set s_range"
[PROOF STATE]
proof (prove)
using this:
s_range \<in> set (build_ip_partition c rs)
s \<in> wordinterval_to_set s_range
?v \<in> set (build_ip_partition c ?rs) \<Longrightarrow> \<exists>s_repr. map_of (zip (map getOneIp (build_ip_partition c ?rs)) (build_ip_partition c ?rs)) s_repr = Some ?v
V = zip (map getOneIp (build_ip_partition c rs)) (build_ip_partition c rs)

goal (1 subgoal):
 1. (\<And>s_repr. \<lbrakk>map_of V s_repr = Some s_range; s \<in> wordinterval_to_set s_range\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
map_of V s_repr = Some s_range
s \<in> wordinterval_to_set s_range

goal (1 subgoal):
 1. \<exists>s_repr d_repr s_range d_range. (s_repr, d_repr) \<in> set E \<and> map_of V s_repr = Some s_range \<and> s \<in> wordinterval_to_set s_range \<and> map_of V d_repr = Some d_range \<and> d \<in> wordinterval_to_set d_range
[PROOF STEP]
from build_ip_partition_obtain
[PROOF STATE]
proof (chain)
picking this:
\<exists>V. V \<in> set (build_ip_partition c rs) \<and> ?s \<in> wordinterval_to_set V
[PROOF STEP]
obtain d_range where
      "d_range \<in> set ?part" and "d \<in> wordinterval_to_set d_range"
[PROOF STATE]
proof (prove)
using this:
\<exists>V. V \<in> set (build_ip_partition c rs) \<and> ?s \<in> wordinterval_to_set V

goal (1 subgoal):
 1. (\<And>d_range. \<lbrakk>d_range \<in> set (build_ip_partition c rs); d \<in> wordinterval_to_set d_range\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
d_range \<in> set (build_ip_partition c rs)
d \<in> wordinterval_to_set d_range

goal (1 subgoal):
 1. \<exists>s_repr d_repr s_range d_range. (s_repr, d_repr) \<in> set E \<and> map_of V s_repr = Some s_range \<and> s \<in> wordinterval_to_set s_range \<and> map_of V d_repr = Some d_range \<and> d \<in> wordinterval_to_set d_range
[PROOF STEP]
from this distinct_map_getOneIp_build_ip_partition_obtain V
[PROOF STATE]
proof (chain)
picking this:
d_range \<in> set (build_ip_partition c rs)
d \<in> wordinterval_to_set d_range
?v \<in> set (build_ip_partition c ?rs) \<Longrightarrow> \<exists>s_repr. map_of (zip (map getOneIp (build_ip_partition c ?rs)) (build_ip_partition c ?rs)) s_repr = Some ?v
V = zip (map getOneIp (build_ip_partition c rs)) (build_ip_partition c rs)
[PROOF STEP]
obtain d_repr where
      ex_d1: "(map_of V) d_repr = Some d_range" and ex_d2: "d \<in> wordinterval_to_set d_range"
[PROOF STATE]
proof (prove)
using this:
d_range \<in> set (build_ip_partition c rs)
d \<in> wordinterval_to_set d_range
?v \<in> set (build_ip_partition c ?rs) \<Longrightarrow> \<exists>s_repr. map_of (zip (map getOneIp (build_ip_partition c ?rs)) (build_ip_partition c ?rs)) s_repr = Some ?v
V = zip (map getOneIp (build_ip_partition c rs)) (build_ip_partition c rs)

goal (1 subgoal):
 1. (\<And>d_repr. \<lbrakk>map_of V d_repr = Some d_range; d \<in> wordinterval_to_set d_range\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
map_of V d_repr = Some d_range
d \<in> wordinterval_to_set d_range

goal (1 subgoal):
 1. \<exists>s_repr d_repr s_range d_range. (s_repr, d_repr) \<in> set E \<and> map_of V s_repr = Some s_range \<and> s \<in> wordinterval_to_set s_range \<and> map_of V d_repr = Some d_range \<and> d \<in> wordinterval_to_set d_range
[PROOF STEP]
have 1: "s_repr \<in> getOneIp ` set (build_ip_partition c rs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. s_repr \<in> getOneIp ` set (build_ip_partition c rs)
[PROOF STEP]
using V \<open>map_of V s_repr = Some s_range\<close>
[PROOF STATE]
proof (prove)
using this:
V = zip (map getOneIp (build_ip_partition c rs)) (build_ip_partition c rs)
map_of V s_repr = Some s_range

goal (1 subgoal):
 1. s_repr \<in> getOneIp ` set (build_ip_partition c rs)
[PROOF STEP]
by (fastforce elim: in_set_zipE dest: map_of_SomeD)
[PROOF STATE]
proof (state)
this:
s_repr \<in> getOneIp ` set (build_ip_partition c rs)

goal (1 subgoal):
 1. \<exists>s_repr d_repr s_range d_range. (s_repr, d_repr) \<in> set E \<and> map_of V s_repr = Some s_range \<and> s \<in> wordinterval_to_set s_range \<and> map_of V d_repr = Some d_range \<and> d \<in> wordinterval_to_set d_range
[PROOF STEP]
have 2: "d_repr \<in> getOneIp ` set (build_ip_partition c rs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. d_repr \<in> getOneIp ` set (build_ip_partition c rs)
[PROOF STEP]
using V \<open>map_of V d_repr = Some d_range\<close>
[PROOF STATE]
proof (prove)
using this:
V = zip (map getOneIp (build_ip_partition c rs)) (build_ip_partition c rs)
map_of V d_repr = Some d_range

goal (1 subgoal):
 1. d_repr \<in> getOneIp ` set (build_ip_partition c rs)
[PROOF STEP]
by (fastforce elim: in_set_zipE dest: map_of_SomeD)
[PROOF STATE]
proof (state)
this:
d_repr \<in> getOneIp ` set (build_ip_partition c rs)

goal (1 subgoal):
 1. \<exists>s_repr d_repr s_range d_range. (s_repr, d_repr) \<in> set E \<and> map_of V s_repr = Some s_range \<and> s \<in> wordinterval_to_set s_range \<and> map_of V d_repr = Some d_range \<and> d \<in> wordinterval_to_set d_range
[PROOF STEP]
have "runFw s_repr d_repr c rs = Decision FinalAllow"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. runFw s_repr d_repr c rs = Decision FinalAllow
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. runFw s_repr d_repr c rs = Decision FinalAllow
[PROOF STEP]
have f1: "(\<forall>w wa p ss. \<not> same_fw_behaviour_one w wa (p::parts_connection) ss \<or>
              (\<forall>wb wc. runFw w wb p ss = runFw wa wb p ss \<and> runFw wc w p ss = runFw wc wa p ss)) \<and>
              (\<forall>w wa p ss. (\<exists>wb wc. runFw w wb (p::parts_connection) ss \<noteq> runFw wa wb p ss \<or> runFw wc w p ss \<noteq> runFw wc wa p ss) \<or>
              same_fw_behaviour_one w wa p ss)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>w wa p ss. \<not> same_fw_behaviour_one w wa p ss \<or> (\<forall>wb wc. runFw w wb p ss = runFw wa wb p ss \<and> runFw wc w p ss = runFw wc wa p ss)) \<and> (\<forall>w wa p ss. (\<exists>wb wc. runFw w wb p ss \<noteq> runFw wa wb p ss \<or> runFw wc w p ss \<noteq> runFw wc wa p ss) \<or> same_fw_behaviour_one w wa p ss)
[PROOF STEP]
unfolding same_fw_behaviour_one_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>w wa p ss. \<not> (\<forall>d s. runFw w d p ss = runFw wa d p ss \<and> runFw s w p ss = runFw s wa p ss) \<or> (\<forall>wb wc. runFw w wb p ss = runFw wa wb p ss \<and> runFw wc w p ss = runFw wc wa p ss)) \<and> (\<forall>w wa p ss. (\<exists>wb wc. runFw w wb p ss \<noteq> runFw wa wb p ss \<or> runFw wc w p ss \<noteq> runFw wc wa p ss) \<or> (\<forall>d s. runFw w d p ss = runFw wa d p ss \<and> runFw s w p ss = runFw s wa p ss))
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
(\<forall>w wa p ss. \<not> same_fw_behaviour_one w wa p ss \<or> (\<forall>wb wc. runFw w wb p ss = runFw wa wb p ss \<and> runFw wc w p ss = runFw wc wa p ss)) \<and> (\<forall>w wa p ss. (\<exists>wb wc. runFw w wb p ss \<noteq> runFw wa wb p ss \<or> runFw wc w p ss \<noteq> runFw wc wa p ss) \<or> same_fw_behaviour_one w wa p ss)

goal (1 subgoal):
 1. runFw s_repr d_repr c rs = Decision FinalAllow
[PROOF STEP]
from \<open>s_range \<in> set (build_ip_partition c rs)\<close>
[PROOF STATE]
proof (chain)
picking this:
s_range \<in> set (build_ip_partition c rs)
[PROOF STEP]
have f2: "same_fw_behaviour_one s s_repr c rs"
[PROOF STATE]
proof (prove)
using this:
s_range \<in> set (build_ip_partition c rs)

goal (1 subgoal):
 1. same_fw_behaviour_one s s_repr c rs
[PROOF STEP]
by (metis (no_types) map_of_zip_map V build_ip_partition_no_empty_elems
            build_ip_partition_same_fw ex_s1 ex_s2 getOneIp_elem wordinterval_element_set_eq)
[PROOF STATE]
proof (state)
this:
same_fw_behaviour_one s s_repr c rs

goal (1 subgoal):
 1. runFw s_repr d_repr c rs = Decision FinalAllow
[PROOF STEP]
from \<open>d_range \<in> set (build_ip_partition c rs)\<close>
[PROOF STATE]
proof (chain)
picking this:
d_range \<in> set (build_ip_partition c rs)
[PROOF STEP]
have "same_fw_behaviour_one d_repr d c rs"
[PROOF STATE]
proof (prove)
using this:
d_range \<in> set (build_ip_partition c rs)

goal (1 subgoal):
 1. same_fw_behaviour_one d_repr d c rs
[PROOF STEP]
by (metis (no_types) map_of_zip_map V build_ip_partition_no_empty_elems
            build_ip_partition_same_fw ex_d1 ex_d2 getOneIp_elem wordinterval_element_set_eq)
[PROOF STATE]
proof (state)
this:
same_fw_behaviour_one d_repr d c rs

goal (1 subgoal):
 1. runFw s_repr d_repr c rs = Decision FinalAllow
[PROOF STEP]
with f1 f2
[PROOF STATE]
proof (chain)
picking this:
(\<forall>w wa p ss. \<not> same_fw_behaviour_one w wa p ss \<or> (\<forall>wb wc. runFw w wb p ss = runFw wa wb p ss \<and> runFw wc w p ss = runFw wc wa p ss)) \<and> (\<forall>w wa p ss. (\<exists>wb wc. runFw w wb p ss \<noteq> runFw wa wb p ss \<or> runFw wc w p ss \<noteq> runFw wc wa p ss) \<or> same_fw_behaviour_one w wa p ss)
same_fw_behaviour_one s s_repr c rs
same_fw_behaviour_one d_repr d c rs
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
(\<forall>w wa p ss. \<not> same_fw_behaviour_one w wa p ss \<or> (\<forall>wb wc. runFw w wb p ss = runFw wa wb p ss \<and> runFw wc w p ss = runFw wc wa p ss)) \<and> (\<forall>w wa p ss. (\<exists>wb wc. runFw w wb p ss \<noteq> runFw wa wb p ss \<or> runFw wc w p ss \<noteq> runFw wc wa p ss) \<or> same_fw_behaviour_one w wa p ss)
same_fw_behaviour_one s s_repr c rs
same_fw_behaviour_one d_repr d c rs

goal (1 subgoal):
 1. runFw s_repr d_repr c rs = Decision FinalAllow
[PROOF STEP]
using allow
[PROOF STATE]
proof (prove)
using this:
(\<forall>w wa p ss. \<not> same_fw_behaviour_one w wa p ss \<or> (\<forall>wb wc. runFw w wb p ss = runFw wa wb p ss \<and> runFw wc w p ss = runFw wc wa p ss)) \<and> (\<forall>w wa p ss. (\<exists>wb wc. runFw w wb p ss \<noteq> runFw wa wb p ss \<or> runFw wc w p ss \<noteq> runFw wc wa p ss) \<or> same_fw_behaviour_one w wa p ss)
same_fw_behaviour_one s s_repr c rs
same_fw_behaviour_one d_repr d c rs
runFw s d c rs = Decision FinalAllow

goal (1 subgoal):
 1. runFw s_repr d_repr c rs = Decision FinalAllow
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
runFw s_repr d_repr c rs = Decision FinalAllow

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
runFw s_repr d_repr c rs = Decision FinalAllow

goal (1 subgoal):
 1. \<exists>s_repr d_repr s_range d_range. (s_repr, d_repr) \<in> set E \<and> map_of V s_repr = Some s_range \<and> s \<in> wordinterval_to_set s_range \<and> map_of V d_repr = Some d_range \<and> d \<in> wordinterval_to_set d_range
[PROOF STEP]
hence ex1: "(s_repr, d_repr) \<in> set E"
[PROOF STATE]
proof (prove)
using this:
runFw s_repr d_repr c rs = Decision FinalAllow

goal (1 subgoal):
 1. (s_repr, d_repr) \<in> set E
[PROOF STEP]
by(simp add: E all_pairs_set 1 2)
[PROOF STATE]
proof (state)
this:
(s_repr, d_repr) \<in> set E

goal (1 subgoal):
 1. \<exists>s_repr d_repr s_range d_range. (s_repr, d_repr) \<in> set E \<and> map_of V s_repr = Some s_range \<and> s \<in> wordinterval_to_set s_range \<and> map_of V d_repr = Some d_range \<and> d \<in> wordinterval_to_set d_range
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
(s_repr, d_repr) \<in> set E

goal (1 subgoal):
 1. \<exists>s_repr d_repr s_range d_range. (s_repr, d_repr) \<in> set E \<and> map_of V s_repr = Some s_range \<and> s \<in> wordinterval_to_set s_range \<and> map_of V d_repr = Some d_range \<and> d \<in> wordinterval_to_set d_range
[PROOF STEP]
using ex1 ex_s1 ex_s2 ex_d1 ex_d2
[PROOF STATE]
proof (prove)
using this:
(s_repr, d_repr) \<in> set E
(s_repr, d_repr) \<in> set E
map_of V s_repr = Some s_range
s \<in> wordinterval_to_set s_range
map_of V d_repr = Some d_range
d \<in> wordinterval_to_set d_range

goal (1 subgoal):
 1. \<exists>s_repr d_repr s_range d_range. (s_repr, d_repr) \<in> set E \<and> map_of V s_repr = Some s_range \<and> s \<in> wordinterval_to_set s_range \<and> map_of V d_repr = Some d_range \<and> d \<in> wordinterval_to_set d_range
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>s_repr d_repr s_range d_range. (s_repr, d_repr) \<in> set E \<and> map_of V s_repr = Some s_range \<and> s \<in> wordinterval_to_set s_range \<and> map_of V d_repr = Some d_range \<and> d \<in> wordinterval_to_set d_range

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
theorem access_matrix:
      fixes rs :: "'i::len simple_rule list"
      assumes matrix: "(V,E) = access_matrix c rs"
      shows "(\<exists>s_repr d_repr s_range d_range. (s_repr, d_repr) \<in> set E \<and>
              (map_of V) s_repr = Some s_range \<and> s \<in> wordinterval_to_set s_range \<and>
              (map_of V) d_repr = Some d_range \<and> d \<in> wordinterval_to_set d_range)
             \<longleftrightarrow>
             runFw s d c rs = Decision FinalAllow"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<exists>s_repr d_repr s_range d_range. (s_repr, d_repr) \<in> set E \<and> map_of V s_repr = Some s_range \<and> s \<in> wordinterval_to_set s_range \<and> map_of V d_repr = Some d_range \<and> d \<in> wordinterval_to_set d_range) = (runFw s d c rs = Decision FinalAllow)
[PROOF STEP]
using matrix access_matrix_sound access_matrix_complete
[PROOF STATE]
proof (prove)
using this:
(V, E) = access_matrix c rs
\<lbrakk>(?V, ?E) = access_matrix ?c ?rs; (?s_repr, ?d_repr) \<in> set ?E; map_of ?V ?s_repr = Some ?s_range; ?s \<in> wordinterval_to_set ?s_range; map_of ?V ?d_repr = Some ?d_range; ?d \<in> wordinterval_to_set ?d_range\<rbrakk> \<Longrightarrow> runFw ?s ?d ?c ?rs = Decision FinalAllow
\<lbrakk>(?V, ?E) = access_matrix ?c ?rs; runFw ?s ?d ?c ?rs = Decision FinalAllow\<rbrakk> \<Longrightarrow> \<exists>s_repr d_repr s_range d_range. (s_repr, d_repr) \<in> set ?E \<and> map_of ?V s_repr = Some s_range \<and> ?s \<in> wordinterval_to_set s_range \<and> map_of ?V d_repr = Some d_range \<and> ?d \<in> wordinterval_to_set d_range

goal (1 subgoal):
 1. (\<exists>s_repr d_repr s_range d_range. (s_repr, d_repr) \<in> set E \<and> map_of V s_repr = Some s_range \<and> s \<in> wordinterval_to_set s_range \<and> map_of V d_repr = Some d_range \<and> d \<in> wordinterval_to_set d_range) = (runFw s d c rs = Decision FinalAllow)
[PROOF STEP]
by blast


[STATEMENT]
lemma access_matrix_pretty_ipv4_code[code]: "access_matrix_pretty_ipv4 = access_matrix_pretty_ipv4_code"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. access_matrix_pretty_ipv4 = access_matrix_pretty_ipv4_code
[PROOF STEP]
by(simp add: fun_eq_iff access_matrix_pretty_ipv4_def access_matrix_pretty_ipv4_code_def Let_def access_matrix_def map_prod_fun_zip)


[STATEMENT]
lemma access_matrix_pretty_ipv6_code[code]: "access_matrix_pretty_ipv6 = access_matrix_pretty_ipv6_code"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. access_matrix_pretty_ipv6 = access_matrix_pretty_ipv6_code
[PROOF STEP]
by(simp add: fun_eq_iff access_matrix_pretty_ipv6_def access_matrix_pretty_ipv6_code_def Let_def access_matrix_def map_prod_fun_zip)


[STATEMENT]
lemma "mk_parts_connection_TCP 10000 22 = parts_connection_ssh"
      "mk_parts_connection_TCP 10000 80 = parts_connection_http"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mk_parts_connection_TCP 10000 22 = parts_connection_ssh &&& mk_parts_connection_TCP 10000 80 = parts_connection_http
[PROOF STEP]
by(simp_all add: mk_parts_connection_TCP_def parts_connection_ssh_def parts_connection_http_def)


[STATEMENT]
lemma treesize_Leaf:
  assumes "treesize T = 0"
  shows "T = Leaf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. T = Leaf
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
treesize T = 0

goal (1 subgoal):
 1. T = Leaf
[PROOF STEP]
by (cases T) auto


[STATEMENT]
lemma treesize_Branching:
  assumes "treesize T = Suc n"
  shows "\<exists>l r. T = Branching l r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>l r. T = Branching l r
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
treesize T = Suc n

goal (1 subgoal):
 1. \<exists>l r. T = Branching l r
[PROOF STEP]
by (cases T) auto


[STATEMENT]
lemma path_inv_Leaf: "path p Leaf \<longleftrightarrow> p = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path p Leaf = (p = [])
[PROOF STEP]
by (induction p)  auto


[STATEMENT]
lemma path_inv_Cons: "path (a#ds) T \<longrightarrow> (\<exists>l r. T=Branching l r)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path (a # ds) T \<longrightarrow> (\<exists>l r. T = Branching l r)
[PROOF STEP]
by  (cases T) (auto simp add: path_inv_Leaf)


[STATEMENT]
lemma path_inv_Branching_Left: "path (Left#p) (Branching l r) \<longleftrightarrow> path p l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path (Left # p) (Branching l r) = path p l
[PROOF STEP]
using Left_def Right_def path.cases
[PROOF STATE]
proof (prove)
using this:
Left = True
Right = False
\<lbrakk>\<And>T. ?x = ([], T) \<Longrightarrow> ?P; \<And>d ds T1 T2. ?x = (d # ds, Branching T1 T2) \<Longrightarrow> ?P; \<And>v va. ?x = (v # va, Leaf) \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. path (Left # p) (Branching l r) = path p l
[PROOF STEP]
by (induction p) auto


[STATEMENT]
lemma path_inv_Branching_Right: "path (Right#p) (Branching l r) \<longleftrightarrow> path p r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path (Right # p) (Branching l r) = path p r
[PROOF STEP]
using Left_def Right_def path.cases
[PROOF STATE]
proof (prove)
using this:
Left = True
Right = False
\<lbrakk>\<And>T. ?x = ([], T) \<Longrightarrow> ?P; \<And>d ds T1 T2. ?x = (d # ds, Branching T1 T2) \<Longrightarrow> ?P; \<And>v va. ?x = (v # va, Leaf) \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. path (Right # p) (Branching l r) = path p r
[PROOF STEP]
by (induction p)  auto


[STATEMENT]
lemma path_inv_Branching:
  "path p (Branching l r) \<longleftrightarrow> (p=[] \<or> (\<exists>a p'. p=a#p'\<and> (a \<longrightarrow> path p' l) \<and> (\<not>a \<longrightarrow> path p' r)))" (is "?L \<longleftrightarrow> ?R")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path p (Branching l r) = (p = [] \<or> (\<exists>a p'. p = a # p' \<and> (a \<longrightarrow> path p' l) \<and> (\<not> a \<longrightarrow> path p' r)))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. path p (Branching l r) \<Longrightarrow> p = [] \<or> (\<exists>a p'. p = a # p' \<and> (a \<longrightarrow> path p' l) \<and> (\<not> a \<longrightarrow> path p' r))
 2. p = [] \<or> (\<exists>a p'. p = a # p' \<and> (a \<longrightarrow> path p' l) \<and> (\<not> a \<longrightarrow> path p' r)) \<Longrightarrow> path p (Branching l r)
[PROOF STEP]
assume ?L
[PROOF STATE]
proof (state)
this:
path p (Branching l r)

goal (2 subgoals):
 1. path p (Branching l r) \<Longrightarrow> p = [] \<or> (\<exists>a p'. p = a # p' \<and> (a \<longrightarrow> path p' l) \<and> (\<not> a \<longrightarrow> path p' r))
 2. p = [] \<or> (\<exists>a p'. p = a # p' \<and> (a \<longrightarrow> path p' l) \<and> (\<not> a \<longrightarrow> path p' r)) \<Longrightarrow> path p (Branching l r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
path p (Branching l r)
[PROOF STEP]
show ?R
[PROOF STATE]
proof (prove)
using this:
path p (Branching l r)

goal (1 subgoal):
 1. p = [] \<or> (\<exists>a p'. p = a # p' \<and> (a \<longrightarrow> path p' l) \<and> (\<not> a \<longrightarrow> path p' r))
[PROOF STEP]
by (induction p) auto
[PROOF STATE]
proof (state)
this:
p = [] \<or> (\<exists>a p'. p = a # p' \<and> (a \<longrightarrow> path p' l) \<and> (\<not> a \<longrightarrow> path p' r))

goal (1 subgoal):
 1. p = [] \<or> (\<exists>a p'. p = a # p' \<and> (a \<longrightarrow> path p' l) \<and> (\<not> a \<longrightarrow> path p' r)) \<Longrightarrow> path p (Branching l r)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p = [] \<or> (\<exists>a p'. p = a # p' \<and> (a \<longrightarrow> path p' l) \<and> (\<not> a \<longrightarrow> path p' r)) \<Longrightarrow> path p (Branching l r)
[PROOF STEP]
assume r: ?R
[PROOF STATE]
proof (state)
this:
p = [] \<or> (\<exists>a p'. p = a # p' \<and> (a \<longrightarrow> path p' l) \<and> (\<not> a \<longrightarrow> path p' r))

goal (1 subgoal):
 1. p = [] \<or> (\<exists>a p'. p = a # p' \<and> (a \<longrightarrow> path p' l) \<and> (\<not> a \<longrightarrow> path p' r)) \<Longrightarrow> path p (Branching l r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p = [] \<or> (\<exists>a p'. p = a # p' \<and> (a \<longrightarrow> path p' l) \<and> (\<not> a \<longrightarrow> path p' r))
[PROOF STEP]
show ?L
[PROOF STATE]
proof (prove)
using this:
p = [] \<or> (\<exists>a p'. p = a # p' \<and> (a \<longrightarrow> path p' l) \<and> (\<not> a \<longrightarrow> path p' r))

goal (1 subgoal):
 1. path p (Branching l r)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p = [] \<Longrightarrow> path p (Branching l r)
 2. \<exists>a p'. p = a # p' \<and> (a \<longrightarrow> path p' l) \<and> (\<not> a \<longrightarrow> path p' r) \<Longrightarrow> path p (Branching l r)
[PROOF STEP]
assume "p = []"
[PROOF STATE]
proof (state)
this:
p = []

goal (2 subgoals):
 1. p = [] \<Longrightarrow> path p (Branching l r)
 2. \<exists>a p'. p = a # p' \<and> (a \<longrightarrow> path p' l) \<and> (\<not> a \<longrightarrow> path p' r) \<Longrightarrow> path p (Branching l r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p = []
[PROOF STEP]
show ?L
[PROOF STATE]
proof (prove)
using this:
p = []

goal (1 subgoal):
 1. path p (Branching l r)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
path p (Branching l r)

goal (1 subgoal):
 1. \<exists>a p'. p = a # p' \<and> (a \<longrightarrow> path p' l) \<and> (\<not> a \<longrightarrow> path p' r) \<Longrightarrow> path p (Branching l r)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>a p'. p = a # p' \<and> (a \<longrightarrow> path p' l) \<and> (\<not> a \<longrightarrow> path p' r) \<Longrightarrow> path p (Branching l r)
[PROOF STEP]
assume "\<exists>a p'. p=a#p'\<and> (a \<longrightarrow> path p' l) \<and> (\<not>a \<longrightarrow> path p' r)"
[PROOF STATE]
proof (state)
this:
\<exists>a p'. p = a # p' \<and> (a \<longrightarrow> path p' l) \<and> (\<not> a \<longrightarrow> path p' r)

goal (1 subgoal):
 1. \<exists>a p'. p = a # p' \<and> (a \<longrightarrow> path p' l) \<and> (\<not> a \<longrightarrow> path p' r) \<Longrightarrow> path p (Branching l r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>a p'. p = a # p' \<and> (a \<longrightarrow> path p' l) \<and> (\<not> a \<longrightarrow> path p' r)
[PROOF STEP]
obtain a p' where "p=a#p'\<and> (a \<longrightarrow> path p' l) \<and> (\<not>a \<longrightarrow> path p' r)"
[PROOF STATE]
proof (prove)
using this:
\<exists>a p'. p = a # p' \<and> (a \<longrightarrow> path p' l) \<and> (\<not> a \<longrightarrow> path p' r)

goal (1 subgoal):
 1. (\<And>a p'. p = a # p' \<and> (a \<longrightarrow> path p' l) \<and> (\<not> a \<longrightarrow> path p' r) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p = a # p' \<and> (a \<longrightarrow> path p' l) \<and> (\<not> a \<longrightarrow> path p' r)

goal (1 subgoal):
 1. \<exists>a p'. p = a # p' \<and> (a \<longrightarrow> path p' l) \<and> (\<not> a \<longrightarrow> path p' r) \<Longrightarrow> path p (Branching l r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p = a # p' \<and> (a \<longrightarrow> path p' l) \<and> (\<not> a \<longrightarrow> path p' r)
[PROOF STEP]
show ?L
[PROOF STATE]
proof (prove)
using this:
p = a # p' \<and> (a \<longrightarrow> path p' l) \<and> (\<not> a \<longrightarrow> path p' r)

goal (1 subgoal):
 1. path p (Branching l r)
[PROOF STEP]
by (cases a) auto
[PROOF STATE]
proof (state)
this:
path p (Branching l r)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
path p (Branching l r)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma path_prefix:
  assumes "path (ds1@ds2) T"
  shows "path ds1 T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path ds1 T
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
path (ds1 @ ds2) T

goal (1 subgoal):
 1. path ds1 T
[PROOF STEP]
proof (induction ds1 arbitrary: T)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>T. path ([] @ ds2) T \<Longrightarrow> path [] T
 2. \<And>a ds1 T. \<lbrakk>\<And>T. path (ds1 @ ds2) T \<Longrightarrow> path ds1 T; path ((a # ds1) @ ds2) T\<rbrakk> \<Longrightarrow> path (a # ds1) T
[PROOF STEP]
case (Cons a ds1)
[PROOF STATE]
proof (state)
this:
path (ds1 @ ds2) ?T \<Longrightarrow> path ds1 ?T
path ((a # ds1) @ ds2) T

goal (2 subgoals):
 1. \<And>T. path ([] @ ds2) T \<Longrightarrow> path [] T
 2. \<And>a ds1 T. \<lbrakk>\<And>T. path (ds1 @ ds2) T \<Longrightarrow> path ds1 T; path ((a # ds1) @ ds2) T\<rbrakk> \<Longrightarrow> path (a # ds1) T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
path (ds1 @ ds2) ?T \<Longrightarrow> path ds1 ?T
path ((a # ds1) @ ds2) T
[PROOF STEP]
have "\<exists>l r. T = Branching l r"
[PROOF STATE]
proof (prove)
using this:
path (ds1 @ ds2) ?T \<Longrightarrow> path ds1 ?T
path ((a # ds1) @ ds2) T

goal (1 subgoal):
 1. \<exists>l r. T = Branching l r
[PROOF STEP]
using path_inv_Leaf
[PROOF STATE]
proof (prove)
using this:
path (ds1 @ ds2) ?T \<Longrightarrow> path ds1 ?T
path ((a # ds1) @ ds2) T
path ?p Leaf = (?p = [])

goal (1 subgoal):
 1. \<exists>l r. T = Branching l r
[PROOF STEP]
by (cases T) auto
[PROOF STATE]
proof (state)
this:
\<exists>l r. T = Branching l r

goal (2 subgoals):
 1. \<And>T. path ([] @ ds2) T \<Longrightarrow> path [] T
 2. \<And>a ds1 T. \<lbrakk>\<And>T. path (ds1 @ ds2) T \<Longrightarrow> path ds1 T; path ((a # ds1) @ ds2) T\<rbrakk> \<Longrightarrow> path (a # ds1) T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>l r. T = Branching l r
[PROOF STEP]
obtain l r where p_lr: "T = Branching l r"
[PROOF STATE]
proof (prove)
using this:
\<exists>l r. T = Branching l r

goal (1 subgoal):
 1. (\<And>l r. T = Branching l r \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
T = Branching l r

goal (2 subgoals):
 1. \<And>T. path ([] @ ds2) T \<Longrightarrow> path [] T
 2. \<And>a ds1 T. \<lbrakk>\<And>T. path (ds1 @ ds2) T \<Longrightarrow> path ds1 T; path ((a # ds1) @ ds2) T\<rbrakk> \<Longrightarrow> path (a # ds1) T
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path (a # ds1) T
[PROOF STEP]
proof (cases a)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. a \<Longrightarrow> path (a # ds1) T
 2. \<not> a \<Longrightarrow> path (a # ds1) T
[PROOF STEP]
assume atrue: "a"
[PROOF STATE]
proof (state)
this:
a

goal (2 subgoals):
 1. a \<Longrightarrow> path (a # ds1) T
 2. \<not> a \<Longrightarrow> path (a # ds1) T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
a
[PROOF STEP]
have "path ((ds1) @ ds2) l"
[PROOF STATE]
proof (prove)
using this:
a

goal (1 subgoal):
 1. path (ds1 @ ds2) l
[PROOF STEP]
using p_lr Cons(2) path_inv_Branching
[PROOF STATE]
proof (prove)
using this:
a
T = Branching l r
path ((a # ds1) @ ds2) T
path ?p (Branching ?l ?r) = (?p = [] \<or> (\<exists>a p'. ?p = a # p' \<and> (a \<longrightarrow> path p' ?l) \<and> (\<not> a \<longrightarrow> path p' ?r)))

goal (1 subgoal):
 1. path (ds1 @ ds2) l
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
path (ds1 @ ds2) l

goal (2 subgoals):
 1. a \<Longrightarrow> path (a # ds1) T
 2. \<not> a \<Longrightarrow> path (a # ds1) T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
path (ds1 @ ds2) l
[PROOF STEP]
have "path ds1 l"
[PROOF STATE]
proof (prove)
using this:
path (ds1 @ ds2) l

goal (1 subgoal):
 1. path ds1 l
[PROOF STEP]
using Cons(1)
[PROOF STATE]
proof (prove)
using this:
path (ds1 @ ds2) l
path (ds1 @ ds2) ?T \<Longrightarrow> path ds1 ?T

goal (1 subgoal):
 1. path ds1 l
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
path ds1 l

goal (2 subgoals):
 1. a \<Longrightarrow> path (a # ds1) T
 2. \<not> a \<Longrightarrow> path (a # ds1) T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
path ds1 l
[PROOF STEP]
show "path (a # ds1) T"
[PROOF STATE]
proof (prove)
using this:
path ds1 l

goal (1 subgoal):
 1. path (a # ds1) T
[PROOF STEP]
using p_lr atrue
[PROOF STATE]
proof (prove)
using this:
path ds1 l
T = Branching l r
a

goal (1 subgoal):
 1. path (a # ds1) T
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
path (a # ds1) T

goal (1 subgoal):
 1. \<not> a \<Longrightarrow> path (a # ds1) T
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<not> a \<Longrightarrow> path (a # ds1) T
[PROOF STEP]
assume afalse: "\<not>a"
[PROOF STATE]
proof (state)
this:
\<not> a

goal (1 subgoal):
 1. \<not> a \<Longrightarrow> path (a # ds1) T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<not> a
[PROOF STEP]
have "path ((ds1) @ ds2) r"
[PROOF STATE]
proof (prove)
using this:
\<not> a

goal (1 subgoal):
 1. path (ds1 @ ds2) r
[PROOF STEP]
using p_lr Cons(2) path_inv_Branching
[PROOF STATE]
proof (prove)
using this:
\<not> a
T = Branching l r
path ((a # ds1) @ ds2) T
path ?p (Branching ?l ?r) = (?p = [] \<or> (\<exists>a p'. ?p = a # p' \<and> (a \<longrightarrow> path p' ?l) \<and> (\<not> a \<longrightarrow> path p' ?r)))

goal (1 subgoal):
 1. path (ds1 @ ds2) r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
path (ds1 @ ds2) r

goal (1 subgoal):
 1. \<not> a \<Longrightarrow> path (a # ds1) T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
path (ds1 @ ds2) r
[PROOF STEP]
have "path ds1 r"
[PROOF STATE]
proof (prove)
using this:
path (ds1 @ ds2) r

goal (1 subgoal):
 1. path ds1 r
[PROOF STEP]
using Cons(1)
[PROOF STATE]
proof (prove)
using this:
path (ds1 @ ds2) r
path (ds1 @ ds2) ?T \<Longrightarrow> path ds1 ?T

goal (1 subgoal):
 1. path ds1 r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
path ds1 r

goal (1 subgoal):
 1. \<not> a \<Longrightarrow> path (a # ds1) T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
path ds1 r
[PROOF STEP]
show "path (a # ds1) T"
[PROOF STATE]
proof (prove)
using this:
path ds1 r

goal (1 subgoal):
 1. path (a # ds1) T
[PROOF STEP]
using p_lr afalse
[PROOF STATE]
proof (prove)
using this:
path ds1 r
T = Branching l r
\<not> a

goal (1 subgoal):
 1. path (a # ds1) T
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
path (a # ds1) T

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
path (a # ds1) T

goal (1 subgoal):
 1. \<And>T. path ([] @ ds2) T \<Longrightarrow> path [] T
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>T. path ([] @ ds2) T \<Longrightarrow> path [] T
[PROOF STEP]
case (Nil)
[PROOF STATE]
proof (state)
this:
path ([] @ ds2) T

goal (1 subgoal):
 1. \<And>T. path ([] @ ds2) T \<Longrightarrow> path [] T
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
path ([] @ ds2) T
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
path ([] @ ds2) T

goal (1 subgoal):
 1. path [] T
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
path [] T

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma branch_inv_Leaf: "branch b Leaf \<longleftrightarrow> b = []"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. branch b Leaf = (b = [])
[PROOF STEP]
by (cases b) auto


[STATEMENT]
lemma branch_inv_Branching_Left:
  "branch (Left#b) (Branching l r) \<longleftrightarrow> branch b l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. branch (Left # b) (Branching l r) = branch b l
[PROOF STEP]
by auto


[STATEMENT]
lemma branch_inv_Branching_Right:
  "branch (Right#b) (Branching l r) \<longleftrightarrow> branch b r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. branch (Right # b) (Branching l r) = branch b r
[PROOF STEP]
by auto


[STATEMENT]
lemma branch_inv_Branching:
  "branch b (Branching l r) \<longleftrightarrow>
     (\<exists>a b'. b=a#b'\<and> (a \<longrightarrow> branch b' l) \<and> (\<not>a \<longrightarrow>  branch b' r))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. branch b (Branching l r) = (\<exists>a b'. b = a # b' \<and> (a \<longrightarrow> branch b' l) \<and> (\<not> a \<longrightarrow> branch b' r))
[PROOF STEP]
by (induction b) auto


[STATEMENT]
lemma branch_inv_Leaf2:
  "T = Leaf \<longleftrightarrow> (\<forall>b. branch b T \<longrightarrow> b = [])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (T = Leaf) = (\<forall>b. branch b T \<longrightarrow> b = [])
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (T = Leaf) = (\<forall>b. branch b T \<longrightarrow> b = [])
[PROOF STEP]
{
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. (T = Leaf) = (\<forall>b. branch b T \<longrightarrow> b = [])
[PROOF STEP]
assume "T=Leaf"
[PROOF STATE]
proof (state)
this:
T = Leaf

goal (1 subgoal):
 1. (T = Leaf) = (\<forall>b. branch b T \<longrightarrow> b = [])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
T = Leaf
[PROOF STEP]
have "\<forall>b. branch b T \<longrightarrow> b = []"
[PROOF STATE]
proof (prove)
using this:
T = Leaf

goal (1 subgoal):
 1. \<forall>b. branch b T \<longrightarrow> b = []
[PROOF STEP]
using branch_inv_Leaf
[PROOF STATE]
proof (prove)
using this:
T = Leaf
branch ?b Leaf = (?b = [])

goal (1 subgoal):
 1. \<forall>b. branch b T \<longrightarrow> b = []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>b. branch b T \<longrightarrow> b = []

goal (1 subgoal):
 1. (T = Leaf) = (\<forall>b. branch b T \<longrightarrow> b = [])
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
T = Leaf \<Longrightarrow> \<forall>b. branch b T \<longrightarrow> b = []

goal (1 subgoal):
 1. (T = Leaf) = (\<forall>b. branch b T \<longrightarrow> b = [])
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
T = Leaf \<Longrightarrow> \<forall>b. branch b T \<longrightarrow> b = []

goal (1 subgoal):
 1. (T = Leaf) = (\<forall>b. branch b T \<longrightarrow> b = [])
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
T = Leaf \<Longrightarrow> \<forall>b. branch b T \<longrightarrow> b = []

goal (1 subgoal):
 1. (T = Leaf) = (\<forall>b. branch b T \<longrightarrow> b = [])
[PROOF STEP]
assume "\<forall>b. branch b T \<longrightarrow> b = []"
[PROOF STATE]
proof (state)
this:
\<forall>b. branch b T \<longrightarrow> b = []

goal (1 subgoal):
 1. (T = Leaf) = (\<forall>b. branch b T \<longrightarrow> b = [])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>b. branch b T \<longrightarrow> b = []
[PROOF STEP]
have "\<forall>b. branch b T \<longrightarrow> \<not>(\<exists>a b'. b = a # b')"
[PROOF STATE]
proof (prove)
using this:
\<forall>b. branch b T \<longrightarrow> b = []

goal (1 subgoal):
 1. \<forall>b. branch b T \<longrightarrow> (\<nexists>a b'. b = a # b')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>b. branch b T \<longrightarrow> (\<nexists>a b'. b = a # b')

goal (1 subgoal):
 1. (T = Leaf) = (\<forall>b. branch b T \<longrightarrow> b = [])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>b. branch b T \<longrightarrow> (\<nexists>a b'. b = a # b')
[PROOF STEP]
have "\<forall>b. branch b T \<longrightarrow> \<not>(\<exists>l r. branch b (Branching l r))"
[PROOF STATE]
proof (prove)
using this:
\<forall>b. branch b T \<longrightarrow> (\<nexists>a b'. b = a # b')

goal (1 subgoal):
 1. \<forall>b. branch b T \<longrightarrow> (\<nexists>l r. branch b (Branching l r))
[PROOF STEP]
using branch_inv_Branching
[PROOF STATE]
proof (prove)
using this:
\<forall>b. branch b T \<longrightarrow> (\<nexists>a b'. b = a # b')
branch ?b (Branching ?l ?r) = (\<exists>a b'. ?b = a # b' \<and> (a \<longrightarrow> branch b' ?l) \<and> (\<not> a \<longrightarrow> branch b' ?r))

goal (1 subgoal):
 1. \<forall>b. branch b T \<longrightarrow> (\<nexists>l r. branch b (Branching l r))
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<forall>b. branch b T \<longrightarrow> (\<nexists>l r. branch b (Branching l r))

goal (1 subgoal):
 1. (T = Leaf) = (\<forall>b. branch b T \<longrightarrow> b = [])
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<forall>b. branch b T \<longrightarrow> (\<nexists>l r. branch b (Branching l r))
[PROOF STEP]
have "T=Leaf"
[PROOF STATE]
proof (prove)
using this:
\<forall>b. branch b T \<longrightarrow> (\<nexists>l r. branch b (Branching l r))

goal (1 subgoal):
 1. T = Leaf
[PROOF STEP]
using has_branch[of T]
[PROOF STATE]
proof (prove)
using this:
\<forall>b. branch b T \<longrightarrow> (\<nexists>l r. branch b (Branching l r))
\<exists>b. branch b T

goal (1 subgoal):
 1. T = Leaf
[PROOF STEP]
by (metis branch.elims(2))
[PROOF STATE]
proof (state)
this:
T = Leaf

goal (1 subgoal):
 1. (T = Leaf) = (\<forall>b. branch b T \<longrightarrow> b = [])
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
\<forall>b. branch b T \<longrightarrow> b = [] \<Longrightarrow> T = Leaf

goal (1 subgoal):
 1. (T = Leaf) = (\<forall>b. branch b T \<longrightarrow> b = [])
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
T = Leaf \<Longrightarrow> \<forall>b. branch b T \<longrightarrow> b = []
\<forall>b. branch b T \<longrightarrow> b = [] \<Longrightarrow> T = Leaf
[PROOF STEP]
show "T = Leaf \<longleftrightarrow> (\<forall>b. branch b T \<longrightarrow> b = [])"
[PROOF STATE]
proof (prove)
using this:
T = Leaf \<Longrightarrow> \<forall>b. branch b T \<longrightarrow> b = []
\<forall>b. branch b T \<longrightarrow> b = [] \<Longrightarrow> T = Leaf

goal (1 subgoal):
 1. (T = Leaf) = (\<forall>b. branch b T \<longrightarrow> b = [])
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(T = Leaf) = (\<forall>b. branch b T \<longrightarrow> b = [])

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma branch_is_path:
  assumes"branch ds T"
  shows "path ds T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path ds T
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
branch ds T

goal (1 subgoal):
 1. path ds T
[PROOF STEP]
proof (induction T arbitrary: ds)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ds. branch ds Leaf \<Longrightarrow> path ds Leaf
 2. \<And>T1 T2 ds. \<lbrakk>\<And>ds. branch ds T1 \<Longrightarrow> path ds T1; \<And>ds. branch ds T2 \<Longrightarrow> path ds T2; branch ds (Branching T1 T2)\<rbrakk> \<Longrightarrow> path ds (Branching T1 T2)
[PROOF STEP]
case Leaf
[PROOF STATE]
proof (state)
this:
branch ds Leaf

goal (2 subgoals):
 1. \<And>ds. branch ds Leaf \<Longrightarrow> path ds Leaf
 2. \<And>T1 T2 ds. \<lbrakk>\<And>ds. branch ds T1 \<Longrightarrow> path ds T1; \<And>ds. branch ds T2 \<Longrightarrow> path ds T2; branch ds (Branching T1 T2)\<rbrakk> \<Longrightarrow> path ds (Branching T1 T2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
branch ds Leaf
[PROOF STEP]
have "ds = []"
[PROOF STATE]
proof (prove)
using this:
branch ds Leaf

goal (1 subgoal):
 1. ds = []
[PROOF STEP]
using branch_inv_Leaf
[PROOF STATE]
proof (prove)
using this:
branch ds Leaf
branch ?b Leaf = (?b = [])

goal (1 subgoal):
 1. ds = []
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ds = []

goal (2 subgoals):
 1. \<And>ds. branch ds Leaf \<Longrightarrow> path ds Leaf
 2. \<And>T1 T2 ds. \<lbrakk>\<And>ds. branch ds T1 \<Longrightarrow> path ds T1; \<And>ds. branch ds T2 \<Longrightarrow> path ds T2; branch ds (Branching T1 T2)\<rbrakk> \<Longrightarrow> path ds (Branching T1 T2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ds = []
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
ds = []

goal (1 subgoal):
 1. path ds Leaf
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
path ds Leaf

goal (1 subgoal):
 1. \<And>T1 T2 ds. \<lbrakk>\<And>ds. branch ds T1 \<Longrightarrow> path ds T1; \<And>ds. branch ds T2 \<Longrightarrow> path ds T2; branch ds (Branching T1 T2)\<rbrakk> \<Longrightarrow> path ds (Branching T1 T2)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>T1 T2 ds. \<lbrakk>\<And>ds. branch ds T1 \<Longrightarrow> path ds T1; \<And>ds. branch ds T2 \<Longrightarrow> path ds T2; branch ds (Branching T1 T2)\<rbrakk> \<Longrightarrow> path ds (Branching T1 T2)
[PROOF STEP]
case (Branching T\<^sub>1 T\<^sub>2)
[PROOF STATE]
proof (state)
this:
branch ?ds T\<^sub>1 \<Longrightarrow> path ?ds T\<^sub>1
branch ?ds T\<^sub>2 \<Longrightarrow> path ?ds T\<^sub>2
branch ds (Branching T\<^sub>1 T\<^sub>2)

goal (1 subgoal):
 1. \<And>T1 T2 ds. \<lbrakk>\<And>ds. branch ds T1 \<Longrightarrow> path ds T1; \<And>ds. branch ds T2 \<Longrightarrow> path ds T2; branch ds (Branching T1 T2)\<rbrakk> \<Longrightarrow> path ds (Branching T1 T2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
branch ?ds T\<^sub>1 \<Longrightarrow> path ?ds T\<^sub>1
branch ?ds T\<^sub>2 \<Longrightarrow> path ?ds T\<^sub>2
branch ds (Branching T\<^sub>1 T\<^sub>2)
[PROOF STEP]
obtain a b where ds_p: "ds = a # b \<and> (a \<longrightarrow> branch b T\<^sub>1) \<and> (\<not> a \<longrightarrow> branch b T\<^sub>2)"
[PROOF STATE]
proof (prove)
using this:
branch ?ds T\<^sub>1 \<Longrightarrow> path ?ds T\<^sub>1
branch ?ds T\<^sub>2 \<Longrightarrow> path ?ds T\<^sub>2
branch ds (Branching T\<^sub>1 T\<^sub>2)

goal (1 subgoal):
 1. (\<And>a b. ds = a # b \<and> (a \<longrightarrow> branch b T\<^sub>1) \<and> (\<not> a \<longrightarrow> branch b T\<^sub>2) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using branch_inv_Branching[of ds]
[PROOF STATE]
proof (prove)
using this:
branch ?ds T\<^sub>1 \<Longrightarrow> path ?ds T\<^sub>1
branch ?ds T\<^sub>2 \<Longrightarrow> path ?ds T\<^sub>2
branch ds (Branching T\<^sub>1 T\<^sub>2)
branch ds (Branching ?l ?r) = (\<exists>a b'. ds = a # b' \<and> (a \<longrightarrow> branch b' ?l) \<and> (\<not> a \<longrightarrow> branch b' ?r))

goal (1 subgoal):
 1. (\<And>a b. ds = a # b \<and> (a \<longrightarrow> branch b T\<^sub>1) \<and> (\<not> a \<longrightarrow> branch b T\<^sub>2) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ds = a # b \<and> (a \<longrightarrow> branch b T\<^sub>1) \<and> (\<not> a \<longrightarrow> branch b T\<^sub>2)

goal (1 subgoal):
 1. \<And>T1 T2 ds. \<lbrakk>\<And>ds. branch ds T1 \<Longrightarrow> path ds T1; \<And>ds. branch ds T2 \<Longrightarrow> path ds T2; branch ds (Branching T1 T2)\<rbrakk> \<Longrightarrow> path ds (Branching T1 T2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ds = a # b \<and> (a \<longrightarrow> branch b T\<^sub>1) \<and> (\<not> a \<longrightarrow> branch b T\<^sub>2)
[PROOF STEP]
have "(a \<longrightarrow> path b T\<^sub>1) \<and> (\<not>a \<longrightarrow> path b T\<^sub>2)"
[PROOF STATE]
proof (prove)
using this:
ds = a # b \<and> (a \<longrightarrow> branch b T\<^sub>1) \<and> (\<not> a \<longrightarrow> branch b T\<^sub>2)

goal (1 subgoal):
 1. (a \<longrightarrow> path b T\<^sub>1) \<and> (\<not> a \<longrightarrow> path b T\<^sub>2)
[PROOF STEP]
using Branching
[PROOF STATE]
proof (prove)
using this:
ds = a # b \<and> (a \<longrightarrow> branch b T\<^sub>1) \<and> (\<not> a \<longrightarrow> branch b T\<^sub>2)
branch ?ds T\<^sub>1 \<Longrightarrow> path ?ds T\<^sub>1
branch ?ds T\<^sub>2 \<Longrightarrow> path ?ds T\<^sub>2
branch ds (Branching T\<^sub>1 T\<^sub>2)

goal (1 subgoal):
 1. (a \<longrightarrow> path b T\<^sub>1) \<and> (\<not> a \<longrightarrow> path b T\<^sub>2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
(a \<longrightarrow> path b T\<^sub>1) \<and> (\<not> a \<longrightarrow> path b T\<^sub>2)

goal (1 subgoal):
 1. \<And>T1 T2 ds. \<lbrakk>\<And>ds. branch ds T1 \<Longrightarrow> path ds T1; \<And>ds. branch ds T2 \<Longrightarrow> path ds T2; branch ds (Branching T1 T2)\<rbrakk> \<Longrightarrow> path ds (Branching T1 T2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
(a \<longrightarrow> path b T\<^sub>1) \<and> (\<not> a \<longrightarrow> path b T\<^sub>2)
[PROOF STEP]
show "?case"
[PROOF STATE]
proof (prove)
using this:
(a \<longrightarrow> path b T\<^sub>1) \<and> (\<not> a \<longrightarrow> path b T\<^sub>2)

goal (1 subgoal):
 1. path ds (Branching T\<^sub>1 T\<^sub>2)
[PROOF STEP]
using ds_p
[PROOF STATE]
proof (prove)
using this:
(a \<longrightarrow> path b T\<^sub>1) \<and> (\<not> a \<longrightarrow> path b T\<^sub>2)
ds = a # b \<and> (a \<longrightarrow> branch b T\<^sub>1) \<and> (\<not> a \<longrightarrow> branch b T\<^sub>2)

goal (1 subgoal):
 1. path ds (Branching T\<^sub>1 T\<^sub>2)
[PROOF STEP]
by (cases a) auto
[PROOF STATE]
proof (state)
this:
path ds (Branching T\<^sub>1 T\<^sub>2)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma Branching_Leaf_Leaf_Tree:
  assumes "T = Branching T1 T2"
  shows "(\<exists>B. branch (B@[True]) T \<and> branch (B@[False]) T)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>B. branch (B @ [True]) T \<and> branch (B @ [False]) T
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
T = Branching T1 T2

goal (1 subgoal):
 1. \<exists>B. branch (B @ [True]) T \<and> branch (B @ [False]) T
[PROOF STEP]
proof (induction T arbitrary: T1 T2)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>T1 T2. Leaf = Branching T1 T2 \<Longrightarrow> \<exists>B. branch (B @ [True]) Leaf \<and> branch (B @ [False]) Leaf
 2. \<And>T1 T2 T1a T2a. \<lbrakk>\<And>T1a T2. T1 = Branching T1a T2 \<Longrightarrow> \<exists>B. branch (B @ [True]) T1 \<and> branch (B @ [False]) T1; \<And>T1 T2a. T2 = Branching T1 T2a \<Longrightarrow> \<exists>B. branch (B @ [True]) T2 \<and> branch (B @ [False]) T2; Branching T1 T2 = Branching T1a T2a\<rbrakk> \<Longrightarrow> \<exists>B. branch (B @ [True]) (Branching T1 T2) \<and> branch (B @ [False]) (Branching T1 T2)
[PROOF STEP]
case Leaf
[PROOF STATE]
proof (state)
this:
Leaf = Branching T1 T2

goal (2 subgoals):
 1. \<And>T1 T2. Leaf = Branching T1 T2 \<Longrightarrow> \<exists>B. branch (B @ [True]) Leaf \<and> branch (B @ [False]) Leaf
 2. \<And>T1 T2 T1a T2a. \<lbrakk>\<And>T1a T2. T1 = Branching T1a T2 \<Longrightarrow> \<exists>B. branch (B @ [True]) T1 \<and> branch (B @ [False]) T1; \<And>T1 T2a. T2 = Branching T1 T2a \<Longrightarrow> \<exists>B. branch (B @ [True]) T2 \<and> branch (B @ [False]) T2; Branching T1 T2 = Branching T1a T2a\<rbrakk> \<Longrightarrow> \<exists>B. branch (B @ [True]) (Branching T1 T2) \<and> branch (B @ [False]) (Branching T1 T2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
Leaf = Branching T1 T2
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
Leaf = Branching T1 T2

goal (1 subgoal):
 1. \<exists>B. branch (B @ [True]) Leaf \<and> branch (B @ [False]) Leaf
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<exists>B. branch (B @ [True]) Leaf \<and> branch (B @ [False]) Leaf

goal (1 subgoal):
 1. \<And>T1 T2 T1a T2a. \<lbrakk>\<And>T1a T2. T1 = Branching T1a T2 \<Longrightarrow> \<exists>B. branch (B @ [True]) T1 \<and> branch (B @ [False]) T1; \<And>T1 T2a. T2 = Branching T1 T2a \<Longrightarrow> \<exists>B. branch (B @ [True]) T2 \<and> branch (B @ [False]) T2; Branching T1 T2 = Branching T1a T2a\<rbrakk> \<Longrightarrow> \<exists>B. branch (B @ [True]) (Branching T1 T2) \<and> branch (B @ [False]) (Branching T1 T2)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>T1 T2 T1a T2a. \<lbrakk>\<And>T1a T2. T1 = Branching T1a T2 \<Longrightarrow> \<exists>B. branch (B @ [True]) T1 \<and> branch (B @ [False]) T1; \<And>T1 T2a. T2 = Branching T1 T2a \<Longrightarrow> \<exists>B. branch (B @ [True]) T2 \<and> branch (B @ [False]) T2; Branching T1 T2 = Branching T1a T2a\<rbrakk> \<Longrightarrow> \<exists>B. branch (B @ [True]) (Branching T1 T2) \<and> branch (B @ [False]) (Branching T1 T2)
[PROOF STEP]
case (Branching T1' T2')
[PROOF STATE]
proof (state)
this:
T1' = Branching ?T1.0 ?T2.0 \<Longrightarrow> \<exists>B. branch (B @ [True]) T1' \<and> branch (B @ [False]) T1'
T2' = Branching ?T1.0 ?T2.0 \<Longrightarrow> \<exists>B. branch (B @ [True]) T2' \<and> branch (B @ [False]) T2'
Branching T1' T2' = Branching T1 T2

goal (1 subgoal):
 1. \<And>T1 T2 T1a T2a. \<lbrakk>\<And>T1a T2. T1 = Branching T1a T2 \<Longrightarrow> \<exists>B. branch (B @ [True]) T1 \<and> branch (B @ [False]) T1; \<And>T1 T2a. T2 = Branching T1 T2a \<Longrightarrow> \<exists>B. branch (B @ [True]) T2 \<and> branch (B @ [False]) T2; Branching T1 T2 = Branching T1a T2a\<rbrakk> \<Longrightarrow> \<exists>B. branch (B @ [True]) (Branching T1 T2) \<and> branch (B @ [False]) (Branching T1 T2)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
T1' = Branching ?T1.0 ?T2.0 \<Longrightarrow> \<exists>B. branch (B @ [True]) T1' \<and> branch (B @ [False]) T1'
T2' = Branching ?T1.0 ?T2.0 \<Longrightarrow> \<exists>B. branch (B @ [True]) T2' \<and> branch (B @ [False]) T2'
Branching T1' T2' = Branching T1 T2

goal (1 subgoal):
 1. \<And>T1 T2 T1a T2a. \<lbrakk>\<And>T1a T2. T1 = Branching T1a T2 \<Longrightarrow> \<exists>B. branch (B @ [True]) T1 \<and> branch (B @ [False]) T1; \<And>T1 T2a. T2 = Branching T1 T2a \<Longrightarrow> \<exists>B. branch (B @ [True]) T2 \<and> branch (B @ [False]) T2; Branching T1 T2 = Branching T1a T2a\<rbrakk> \<Longrightarrow> \<exists>B. branch (B @ [True]) (Branching T1 T2) \<and> branch (B @ [False]) (Branching T1 T2)
[PROOF STEP]
assume "T1'=Leaf \<and> T2'=Leaf"
[PROOF STATE]
proof (state)
this:
T1' = Leaf \<and> T2' = Leaf

goal (1 subgoal):
 1. \<And>T1 T2 T1a T2a. \<lbrakk>\<And>T1a T2. T1 = Branching T1a T2 \<Longrightarrow> \<exists>B. branch (B @ [True]) T1 \<and> branch (B @ [False]) T1; \<And>T1 T2a. T2 = Branching T1 T2a \<Longrightarrow> \<exists>B. branch (B @ [True]) T2 \<and> branch (B @ [False]) T2; Branching T1 T2 = Branching T1a T2a\<rbrakk> \<Longrightarrow> \<exists>B. branch (B @ [True]) (Branching T1 T2) \<and> branch (B @ [False]) (Branching T1 T2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
T1' = Leaf \<and> T2' = Leaf
[PROOF STEP]
have "branch ([] @ [True]) (Branching T1' T2') \<and> branch ([] @ [False]) (Branching T1' T2')"
[PROOF STATE]
proof (prove)
using this:
T1' = Leaf \<and> T2' = Leaf

goal (1 subgoal):
 1. branch ([] @ [True]) (Branching T1' T2') \<and> branch ([] @ [False]) (Branching T1' T2')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
branch ([] @ [True]) (Branching T1' T2') \<and> branch ([] @ [False]) (Branching T1' T2')

goal (1 subgoal):
 1. \<And>T1 T2 T1a T2a. \<lbrakk>\<And>T1a T2. T1 = Branching T1a T2 \<Longrightarrow> \<exists>B. branch (B @ [True]) T1 \<and> branch (B @ [False]) T1; \<And>T1 T2a. T2 = Branching T1 T2a \<Longrightarrow> \<exists>B. branch (B @ [True]) T2 \<and> branch (B @ [False]) T2; Branching T1 T2 = Branching T1a T2a\<rbrakk> \<Longrightarrow> \<exists>B. branch (B @ [True]) (Branching T1 T2) \<and> branch (B @ [False]) (Branching T1 T2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
branch ([] @ [True]) (Branching T1' T2') \<and> branch ([] @ [False]) (Branching T1' T2')
[PROOF STEP]
have ?case
[PROOF STATE]
proof (prove)
using this:
branch ([] @ [True]) (Branching T1' T2') \<and> branch ([] @ [False]) (Branching T1' T2')

goal (1 subgoal):
 1. \<exists>B. branch (B @ [True]) (Branching T1' T2') \<and> branch (B @ [False]) (Branching T1' T2')
[PROOF STEP]
by metis
[PROOF STATE]
proof (state)
this:
\<exists>B. branch (B @ [True]) (Branching T1' T2') \<and> branch (B @ [False]) (Branching T1' T2')

goal (1 subgoal):
 1. \<And>T1 T2 T1a T2a. \<lbrakk>\<And>T1a T2. T1 = Branching T1a T2 \<Longrightarrow> \<exists>B. branch (B @ [True]) T1 \<and> branch (B @ [False]) T1; \<And>T1 T2a. T2 = Branching T1 T2a \<Longrightarrow> \<exists>B. branch (B @ [True]) T2 \<and> branch (B @ [False]) T2; Branching T1 T2 = Branching T1a T2a\<rbrakk> \<Longrightarrow> \<exists>B. branch (B @ [True]) (Branching T1 T2) \<and> branch (B @ [False]) (Branching T1 T2)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
T1' = Leaf \<and> T2' = Leaf \<Longrightarrow> \<exists>B. branch (B @ [True]) (Branching T1' T2') \<and> branch (B @ [False]) (Branching T1' T2')

goal (1 subgoal):
 1. \<And>T1 T2 T1a T2a. \<lbrakk>\<And>T1a T2. T1 = Branching T1a T2 \<Longrightarrow> \<exists>B. branch (B @ [True]) T1 \<and> branch (B @ [False]) T1; \<And>T1 T2a. T2 = Branching T1 T2a \<Longrightarrow> \<exists>B. branch (B @ [True]) T2 \<and> branch (B @ [False]) T2; Branching T1 T2 = Branching T1a T2a\<rbrakk> \<Longrightarrow> \<exists>B. branch (B @ [True]) (Branching T1 T2) \<and> branch (B @ [False]) (Branching T1 T2)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
T1' = Leaf \<and> T2' = Leaf \<Longrightarrow> \<exists>B. branch (B @ [True]) (Branching T1' T2') \<and> branch (B @ [False]) (Branching T1' T2')

goal (1 subgoal):
 1. \<And>T1 T2 T1a T2a. \<lbrakk>\<And>T1a T2. T1 = Branching T1a T2 \<Longrightarrow> \<exists>B. branch (B @ [True]) T1 \<and> branch (B @ [False]) T1; \<And>T1 T2a. T2 = Branching T1 T2a \<Longrightarrow> \<exists>B. branch (B @ [True]) T2 \<and> branch (B @ [False]) T2; Branching T1 T2 = Branching T1a T2a\<rbrakk> \<Longrightarrow> \<exists>B. branch (B @ [True]) (Branching T1 T2) \<and> branch (B @ [False]) (Branching T1 T2)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
T1' = Leaf \<and> T2' = Leaf \<Longrightarrow> \<exists>B. branch (B @ [True]) (Branching T1' T2') \<and> branch (B @ [False]) (Branching T1' T2')

goal (1 subgoal):
 1. \<And>T1 T2 T1a T2a. \<lbrakk>\<And>T1a T2. T1 = Branching T1a T2 \<Longrightarrow> \<exists>B. branch (B @ [True]) T1 \<and> branch (B @ [False]) T1; \<And>T1 T2a. T2 = Branching T1 T2a \<Longrightarrow> \<exists>B. branch (B @ [True]) T2 \<and> branch (B @ [False]) T2; Branching T1 T2 = Branching T1a T2a\<rbrakk> \<Longrightarrow> \<exists>B. branch (B @ [True]) (Branching T1 T2) \<and> branch (B @ [False]) (Branching T1 T2)
[PROOF STEP]
fix T11 T12
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>T1 T2 T1a T2a. \<lbrakk>\<And>T1a T2. T1 = Branching T1a T2 \<Longrightarrow> \<exists>B. branch (B @ [True]) T1 \<and> branch (B @ [False]) T1; \<And>T1 T2a. T2 = Branching T1 T2a \<Longrightarrow> \<exists>B. branch (B @ [True]) T2 \<and> branch (B @ [False]) T2; Branching T1 T2 = Branching T1a T2a\<rbrakk> \<Longrightarrow> \<exists>B. branch (B @ [True]) (Branching T1 T2) \<and> branch (B @ [False]) (Branching T1 T2)
[PROOF STEP]
assume "T1' = Branching T11 T12"
[PROOF STATE]
proof (state)
this:
T1' = Branching T11 T12

goal (1 subgoal):
 1. \<And>T1 T2 T1a T2a. \<lbrakk>\<And>T1a T2. T1 = Branching T1a T2 \<Longrightarrow> \<exists>B. branch (B @ [True]) T1 \<and> branch (B @ [False]) T1; \<And>T1 T2a. T2 = Branching T1 T2a \<Longrightarrow> \<exists>B. branch (B @ [True]) T2 \<and> branch (B @ [False]) T2; Branching T1 T2 = Branching T1a T2a\<rbrakk> \<Longrightarrow> \<exists>B. branch (B @ [True]) (Branching T1 T2) \<and> branch (B @ [False]) (Branching T1 T2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
T1' = Branching T11 T12
[PROOF STEP]
obtain B where "branch (B @ [True]) T1'
                       \<and> branch (B @ [False]) T1'"
[PROOF STATE]
proof (prove)
using this:
T1' = Branching T11 T12

goal (1 subgoal):
 1. (\<And>B. branch (B @ [True]) T1' \<and> branch (B @ [False]) T1' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using Branching
[PROOF STATE]
proof (prove)
using this:
T1' = Branching T11 T12
T1' = Branching ?T1.0 ?T2.0 \<Longrightarrow> \<exists>B. branch (B @ [True]) T1' \<and> branch (B @ [False]) T1'
T2' = Branching ?T1.0 ?T2.0 \<Longrightarrow> \<exists>B. branch (B @ [True]) T2' \<and> branch (B @ [False]) T2'
Branching T1' T2' = Branching T1 T2

goal (1 subgoal):
 1. (\<And>B. branch (B @ [True]) T1' \<and> branch (B @ [False]) T1' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
branch (B @ [True]) T1' \<and> branch (B @ [False]) T1'

goal (1 subgoal):
 1. \<And>T1 T2 T1a T2a. \<lbrakk>\<And>T1a T2. T1 = Branching T1a T2 \<Longrightarrow> \<exists>B. branch (B @ [True]) T1 \<and> branch (B @ [False]) T1; \<And>T1 T2a. T2 = Branching T1 T2a \<Longrightarrow> \<exists>B. branch (B @ [True]) T2 \<and> branch (B @ [False]) T2; Branching T1 T2 = Branching T1a T2a\<rbrakk> \<Longrightarrow> \<exists>B. branch (B @ [True]) (Branching T1 T2) \<and> branch (B @ [False]) (Branching T1 T2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
branch (B @ [True]) T1' \<and> branch (B @ [False]) T1'
[PROOF STEP]
have "branch (([True] @ B) @ [True]) (Branching T1' T2')
             \<and> branch (([True] @ B) @ [False]) (Branching T1' T2')"
[PROOF STATE]
proof (prove)
using this:
branch (B @ [True]) T1' \<and> branch (B @ [False]) T1'

goal (1 subgoal):
 1. branch (([True] @ B) @ [True]) (Branching T1' T2') \<and> branch (([True] @ B) @ [False]) (Branching T1' T2')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
branch (([True] @ B) @ [True]) (Branching T1' T2') \<and> branch (([True] @ B) @ [False]) (Branching T1' T2')

goal (1 subgoal):
 1. \<And>T1 T2 T1a T2a. \<lbrakk>\<And>T1a T2. T1 = Branching T1a T2 \<Longrightarrow> \<exists>B. branch (B @ [True]) T1 \<and> branch (B @ [False]) T1; \<And>T1 T2a. T2 = Branching T1 T2a \<Longrightarrow> \<exists>B. branch (B @ [True]) T2 \<and> branch (B @ [False]) T2; Branching T1 T2 = Branching T1a T2a\<rbrakk> \<Longrightarrow> \<exists>B. branch (B @ [True]) (Branching T1 T2) \<and> branch (B @ [False]) (Branching T1 T2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
branch (([True] @ B) @ [True]) (Branching T1' T2') \<and> branch (([True] @ B) @ [False]) (Branching T1' T2')
[PROOF STEP]
have ?case
[PROOF STATE]
proof (prove)
using this:
branch (([True] @ B) @ [True]) (Branching T1' T2') \<and> branch (([True] @ B) @ [False]) (Branching T1' T2')

goal (1 subgoal):
 1. \<exists>B. branch (B @ [True]) (Branching T1' T2') \<and> branch (B @ [False]) (Branching T1' T2')
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>B. branch (B @ [True]) (Branching T1' T2') \<and> branch (B @ [False]) (Branching T1' T2')

goal (1 subgoal):
 1. \<And>T1 T2 T1a T2a. \<lbrakk>\<And>T1a T2. T1 = Branching T1a T2 \<Longrightarrow> \<exists>B. branch (B @ [True]) T1 \<and> branch (B @ [False]) T1; \<And>T1 T2a. T2 = Branching T1 T2a \<Longrightarrow> \<exists>B. branch (B @ [True]) T2 \<and> branch (B @ [False]) T2; Branching T1 T2 = Branching T1a T2a\<rbrakk> \<Longrightarrow> \<exists>B. branch (B @ [True]) (Branching T1 T2) \<and> branch (B @ [False]) (Branching T1 T2)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
T1' = Branching ?T11.2 ?T12.2 \<Longrightarrow> \<exists>B. branch (B @ [True]) (Branching T1' T2') \<and> branch (B @ [False]) (Branching T1' T2')

goal (1 subgoal):
 1. \<And>T1 T2 T1a T2a. \<lbrakk>\<And>T1a T2. T1 = Branching T1a T2 \<Longrightarrow> \<exists>B. branch (B @ [True]) T1 \<and> branch (B @ [False]) T1; \<And>T1 T2a. T2 = Branching T1 T2a \<Longrightarrow> \<exists>B. branch (B @ [True]) T2 \<and> branch (B @ [False]) T2; Branching T1 T2 = Branching T1a T2a\<rbrakk> \<Longrightarrow> \<exists>B. branch (B @ [True]) (Branching T1 T2) \<and> branch (B @ [False]) (Branching T1 T2)
[PROOF STEP]
moreover
[PROOF STATE]
proof (state)
this:
T1' = Branching ?T11.2 ?T12.2 \<Longrightarrow> \<exists>B. branch (B @ [True]) (Branching T1' T2') \<and> branch (B @ [False]) (Branching T1' T2')

goal (1 subgoal):
 1. \<And>T1 T2 T1a T2a. \<lbrakk>\<And>T1a T2. T1 = Branching T1a T2 \<Longrightarrow> \<exists>B. branch (B @ [True]) T1 \<and> branch (B @ [False]) T1; \<And>T1 T2a. T2 = Branching T1 T2a \<Longrightarrow> \<exists>B. branch (B @ [True]) T2 \<and> branch (B @ [False]) T2; Branching T1 T2 = Branching T1a T2a\<rbrakk> \<Longrightarrow> \<exists>B. branch (B @ [True]) (Branching T1 T2) \<and> branch (B @ [False]) (Branching T1 T2)
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
T1' = Branching ?T11.2 ?T12.2 \<Longrightarrow> \<exists>B. branch (B @ [True]) (Branching T1' T2') \<and> branch (B @ [False]) (Branching T1' T2')

goal (1 subgoal):
 1. \<And>T1 T2 T1a T2a. \<lbrakk>\<And>T1a T2. T1 = Branching T1a T2 \<Longrightarrow> \<exists>B. branch (B @ [True]) T1 \<and> branch (B @ [False]) T1; \<And>T1 T2a. T2 = Branching T1 T2a \<Longrightarrow> \<exists>B. branch (B @ [True]) T2 \<and> branch (B @ [False]) T2; Branching T1 T2 = Branching T1a T2a\<rbrakk> \<Longrightarrow> \<exists>B. branch (B @ [True]) (Branching T1 T2) \<and> branch (B @ [False]) (Branching T1 T2)
[PROOF STEP]
fix T11 T12
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>T1 T2 T1a T2a. \<lbrakk>\<And>T1a T2. T1 = Branching T1a T2 \<Longrightarrow> \<exists>B. branch (B @ [True]) T1 \<and> branch (B @ [False]) T1; \<And>T1 T2a. T2 = Branching T1 T2a \<Longrightarrow> \<exists>B. branch (B @ [True]) T2 \<and> branch (B @ [False]) T2; Branching T1 T2 = Branching T1a T2a\<rbrakk> \<Longrightarrow> \<exists>B. branch (B @ [True]) (Branching T1 T2) \<and> branch (B @ [False]) (Branching T1 T2)
[PROOF STEP]
assume "T2' = Branching T11 T12"
[PROOF STATE]
proof (state)
this:
T2' = Branching T11 T12

goal (1 subgoal):
 1. \<And>T1 T2 T1a T2a. \<lbrakk>\<And>T1a T2. T1 = Branching T1a T2 \<Longrightarrow> \<exists>B. branch (B @ [True]) T1 \<and> branch (B @ [False]) T1; \<And>T1 T2a. T2 = Branching T1 T2a \<Longrightarrow> \<exists>B. branch (B @ [True]) T2 \<and> branch (B @ [False]) T2; Branching T1 T2 = Branching T1a T2a\<rbrakk> \<Longrightarrow> \<exists>B. branch (B @ [True]) (Branching T1 T2) \<and> branch (B @ [False]) (Branching T1 T2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
T2' = Branching T11 T12
[PROOF STEP]
obtain B where "branch (B @ [True]) T2'
                       \<and> branch (B @ [False]) T2'"
[PROOF STATE]
proof (prove)
using this:
T2' = Branching T11 T12

goal (1 subgoal):
 1. (\<And>B. branch (B @ [True]) T2' \<and> branch (B @ [False]) T2' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using Branching
[PROOF STATE]
proof (prove)
using this:
T2' = Branching T11 T12
T1' = Branching ?T1.0 ?T2.0 \<Longrightarrow> \<exists>B. branch (B @ [True]) T1' \<and> branch (B @ [False]) T1'
T2' = Branching ?T1.0 ?T2.0 \<Longrightarrow> \<exists>B. branch (B @ [True]) T2' \<and> branch (B @ [False]) T2'
Branching T1' T2' = Branching T1 T2

goal (1 subgoal):
 1. (\<And>B. branch (B @ [True]) T2' \<and> branch (B @ [False]) T2' \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
branch (B @ [True]) T2' \<and> branch (B @ [False]) T2'

goal (1 subgoal):
 1. \<And>T1 T2 T1a T2a. \<lbrakk>\<And>T1a T2. T1 = Branching T1a T2 \<Longrightarrow> \<exists>B. branch (B @ [True]) T1 \<and> branch (B @ [False]) T1; \<And>T1 T2a. T2 = Branching T1 T2a \<Longrightarrow> \<exists>B. branch (B @ [True]) T2 \<and> branch (B @ [False]) T2; Branching T1 T2 = Branching T1a T2a\<rbrakk> \<Longrightarrow> \<exists>B. branch (B @ [True]) (Branching T1 T2) \<and> branch (B @ [False]) (Branching T1 T2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
branch (B @ [True]) T2' \<and> branch (B @ [False]) T2'
[PROOF STEP]
have "branch (([False] @ B) @ [True]) (Branching T1' T2')
             \<and> branch (([False] @ B) @ [False]) (Branching T1' T2')"
[PROOF STATE]
proof (prove)
using this:
branch (B @ [True]) T2' \<and> branch (B @ [False]) T2'

goal (1 subgoal):
 1. branch (([False] @ B) @ [True]) (Branching T1' T2') \<and> branch (([False] @ B) @ [False]) (Branching T1' T2')
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
branch (([False] @ B) @ [True]) (Branching T1' T2') \<and> branch (([False] @ B) @ [False]) (Branching T1' T2')

goal (1 subgoal):
 1. \<And>T1 T2 T1a T2a. \<lbrakk>\<And>T1a T2. T1 = Branching T1a T2 \<Longrightarrow> \<exists>B. branch (B @ [True]) T1 \<and> branch (B @ [False]) T1; \<And>T1 T2a. T2 = Branching T1 T2a \<Longrightarrow> \<exists>B. branch (B @ [True]) T2 \<and> branch (B @ [False]) T2; Branching T1 T2 = Branching T1a T2a\<rbrakk> \<Longrightarrow> \<exists>B. branch (B @ [True]) (Branching T1 T2) \<and> branch (B @ [False]) (Branching T1 T2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
branch (([False] @ B) @ [True]) (Branching T1' T2') \<and> branch (([False] @ B) @ [False]) (Branching T1' T2')
[PROOF STEP]
have ?case
[PROOF STATE]
proof (prove)
using this:
branch (([False] @ B) @ [True]) (Branching T1' T2') \<and> branch (([False] @ B) @ [False]) (Branching T1' T2')

goal (1 subgoal):
 1. \<exists>B. branch (B @ [True]) (Branching T1' T2') \<and> branch (B @ [False]) (Branching T1' T2')
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>B. branch (B @ [True]) (Branching T1' T2') \<and> branch (B @ [False]) (Branching T1' T2')

goal (1 subgoal):
 1. \<And>T1 T2 T1a T2a. \<lbrakk>\<And>T1a T2. T1 = Branching T1a T2 \<Longrightarrow> \<exists>B. branch (B @ [True]) T1 \<and> branch (B @ [False]) T1; \<And>T1 T2a. T2 = Branching T1 T2a \<Longrightarrow> \<exists>B. branch (B @ [True]) T2 \<and> branch (B @ [False]) T2; Branching T1 T2 = Branching T1a T2a\<rbrakk> \<Longrightarrow> \<exists>B. branch (B @ [True]) (Branching T1 T2) \<and> branch (B @ [False]) (Branching T1 T2)
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
T2' = Branching ?T11.2 ?T12.2 \<Longrightarrow> \<exists>B. branch (B @ [True]) (Branching T1' T2') \<and> branch (B @ [False]) (Branching T1' T2')

goal (1 subgoal):
 1. \<And>T1 T2 T1a T2a. \<lbrakk>\<And>T1a T2. T1 = Branching T1a T2 \<Longrightarrow> \<exists>B. branch (B @ [True]) T1 \<and> branch (B @ [False]) T1; \<And>T1 T2a. T2 = Branching T1 T2a \<Longrightarrow> \<exists>B. branch (B @ [True]) T2 \<and> branch (B @ [False]) T2; Branching T1 T2 = Branching T1a T2a\<rbrakk> \<Longrightarrow> \<exists>B. branch (B @ [True]) (Branching T1 T2) \<and> branch (B @ [False]) (Branching T1 T2)
[PROOF STEP]
ultimately
[PROOF STATE]
proof (chain)
picking this:
T1' = Leaf \<and> T2' = Leaf \<Longrightarrow> \<exists>B. branch (B @ [True]) (Branching T1' T2') \<and> branch (B @ [False]) (Branching T1' T2')
T1' = Branching ?T11.2 ?T12.2 \<Longrightarrow> \<exists>B. branch (B @ [True]) (Branching T1' T2') \<and> branch (B @ [False]) (Branching T1' T2')
T2' = Branching ?T11.2 ?T12.2 \<Longrightarrow> \<exists>B. branch (B @ [True]) (Branching T1' T2') \<and> branch (B @ [False]) (Branching T1' T2')
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
T1' = Leaf \<and> T2' = Leaf \<Longrightarrow> \<exists>B. branch (B @ [True]) (Branching T1' T2') \<and> branch (B @ [False]) (Branching T1' T2')
T1' = Branching ?T11.2 ?T12.2 \<Longrightarrow> \<exists>B. branch (B @ [True]) (Branching T1' T2') \<and> branch (B @ [False]) (Branching T1' T2')
T2' = Branching ?T11.2 ?T12.2 \<Longrightarrow> \<exists>B. branch (B @ [True]) (Branching T1' T2') \<and> branch (B @ [False]) (Branching T1' T2')

goal (1 subgoal):
 1. \<exists>B. branch (B @ [True]) (Branching T1' T2') \<and> branch (B @ [False]) (Branching T1' T2')
[PROOF STEP]
using tree.exhaust
[PROOF STATE]
proof (prove)
using this:
T1' = Leaf \<and> T2' = Leaf \<Longrightarrow> \<exists>B. branch (B @ [True]) (Branching T1' T2') \<and> branch (B @ [False]) (Branching T1' T2')
T1' = Branching ?T11.2 ?T12.2 \<Longrightarrow> \<exists>B. branch (B @ [True]) (Branching T1' T2') \<and> branch (B @ [False]) (Branching T1' T2')
T2' = Branching ?T11.2 ?T12.2 \<Longrightarrow> \<exists>B. branch (B @ [True]) (Branching T1' T2') \<and> branch (B @ [False]) (Branching T1' T2')
\<lbrakk>?y = Leaf \<Longrightarrow> ?P; \<And>x21 x22. ?y = Branching x21 x22 \<Longrightarrow> ?P\<rbrakk> \<Longrightarrow> ?P

goal (1 subgoal):
 1. \<exists>B. branch (B @ [True]) (Branching T1' T2') \<and> branch (B @ [False]) (Branching T1' T2')
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>B. branch (B @ [True]) (Branching T1' T2') \<and> branch (B @ [False]) (Branching T1' T2')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma internal_inv_Leaf: "\<not>internal b Leaf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<not> internal b Leaf
[PROOF STEP]
using internal.simps
[PROOF STATE]
proof (prove)
using this:
internal [] (Branching ?l ?r) = True
internal (?d # ?ds) (Branching ?l ?r) = (if ?d then internal ?ds ?l else internal ?ds ?r)
internal (?v # ?va) Leaf = False
internal ?uu Leaf = False

goal (1 subgoal):
 1. \<not> internal b Leaf
[PROOF STEP]
by blast


[STATEMENT]
lemma internal_inv_Branching_Left:
  "internal (Left#b) (Branching l r) \<longleftrightarrow> internal b l"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. internal (Left # b) (Branching l r) = internal b l
[PROOF STEP]
by auto


[STATEMENT]
lemma internal_inv_Branching_Right:
  "internal (Right#b) (Branching l r) \<longleftrightarrow> internal b r"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. internal (Right # b) (Branching l r) = internal b r
[PROOF STEP]
by auto


[STATEMENT]
lemma internal_inv_Branching:
  "internal p (Branching l r) \<longleftrightarrow> (p=[] \<or> (\<exists>a p'. p=a#p'\<and> (a \<longrightarrow> internal p' l) \<and> (\<not>a \<longrightarrow> internal p' r)))" (is "?L \<longleftrightarrow> ?R")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. internal p (Branching l r) = (p = [] \<or> (\<exists>a p'. p = a # p' \<and> (a \<longrightarrow> internal p' l) \<and> (\<not> a \<longrightarrow> internal p' r)))
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. internal p (Branching l r) \<Longrightarrow> p = [] \<or> (\<exists>a p'. p = a # p' \<and> (a \<longrightarrow> internal p' l) \<and> (\<not> a \<longrightarrow> internal p' r))
 2. p = [] \<or> (\<exists>a p'. p = a # p' \<and> (a \<longrightarrow> internal p' l) \<and> (\<not> a \<longrightarrow> internal p' r)) \<Longrightarrow> internal p (Branching l r)
[PROOF STEP]
assume ?L
[PROOF STATE]
proof (state)
this:
internal p (Branching l r)

goal (2 subgoals):
 1. internal p (Branching l r) \<Longrightarrow> p = [] \<or> (\<exists>a p'. p = a # p' \<and> (a \<longrightarrow> internal p' l) \<and> (\<not> a \<longrightarrow> internal p' r))
 2. p = [] \<or> (\<exists>a p'. p = a # p' \<and> (a \<longrightarrow> internal p' l) \<and> (\<not> a \<longrightarrow> internal p' r)) \<Longrightarrow> internal p (Branching l r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
internal p (Branching l r)
[PROOF STEP]
show ?R
[PROOF STATE]
proof (prove)
using this:
internal p (Branching l r)

goal (1 subgoal):
 1. p = [] \<or> (\<exists>a p'. p = a # p' \<and> (a \<longrightarrow> internal p' l) \<and> (\<not> a \<longrightarrow> internal p' r))
[PROOF STEP]
by (metis internal.simps(2) neq_Nil_conv)
[PROOF STATE]
proof (state)
this:
p = [] \<or> (\<exists>a p'. p = a # p' \<and> (a \<longrightarrow> internal p' l) \<and> (\<not> a \<longrightarrow> internal p' r))

goal (1 subgoal):
 1. p = [] \<or> (\<exists>a p'. p = a # p' \<and> (a \<longrightarrow> internal p' l) \<and> (\<not> a \<longrightarrow> internal p' r)) \<Longrightarrow> internal p (Branching l r)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. p = [] \<or> (\<exists>a p'. p = a # p' \<and> (a \<longrightarrow> internal p' l) \<and> (\<not> a \<longrightarrow> internal p' r)) \<Longrightarrow> internal p (Branching l r)
[PROOF STEP]
assume r: ?R
[PROOF STATE]
proof (state)
this:
p = [] \<or> (\<exists>a p'. p = a # p' \<and> (a \<longrightarrow> internal p' l) \<and> (\<not> a \<longrightarrow> internal p' r))

goal (1 subgoal):
 1. p = [] \<or> (\<exists>a p'. p = a # p' \<and> (a \<longrightarrow> internal p' l) \<and> (\<not> a \<longrightarrow> internal p' r)) \<Longrightarrow> internal p (Branching l r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p = [] \<or> (\<exists>a p'. p = a # p' \<and> (a \<longrightarrow> internal p' l) \<and> (\<not> a \<longrightarrow> internal p' r))
[PROOF STEP]
show ?L
[PROOF STATE]
proof (prove)
using this:
p = [] \<or> (\<exists>a p'. p = a # p' \<and> (a \<longrightarrow> internal p' l) \<and> (\<not> a \<longrightarrow> internal p' r))

goal (1 subgoal):
 1. internal p (Branching l r)
[PROOF STEP]
proof
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. p = [] \<Longrightarrow> internal p (Branching l r)
 2. \<exists>a p'. p = a # p' \<and> (a \<longrightarrow> internal p' l) \<and> (\<not> a \<longrightarrow> internal p' r) \<Longrightarrow> internal p (Branching l r)
[PROOF STEP]
assume "p = []"
[PROOF STATE]
proof (state)
this:
p = []

goal (2 subgoals):
 1. p = [] \<Longrightarrow> internal p (Branching l r)
 2. \<exists>a p'. p = a # p' \<and> (a \<longrightarrow> internal p' l) \<and> (\<not> a \<longrightarrow> internal p' r) \<Longrightarrow> internal p (Branching l r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p = []
[PROOF STEP]
show ?L
[PROOF STATE]
proof (prove)
using this:
p = []

goal (1 subgoal):
 1. internal p (Branching l r)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
internal p (Branching l r)

goal (1 subgoal):
 1. \<exists>a p'. p = a # p' \<and> (a \<longrightarrow> internal p' l) \<and> (\<not> a \<longrightarrow> internal p' r) \<Longrightarrow> internal p (Branching l r)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>a p'. p = a # p' \<and> (a \<longrightarrow> internal p' l) \<and> (\<not> a \<longrightarrow> internal p' r) \<Longrightarrow> internal p (Branching l r)
[PROOF STEP]
assume "\<exists>a p'. p=a#p'\<and> (a \<longrightarrow> internal p' l) \<and> (\<not>a \<longrightarrow> internal p' r)"
[PROOF STATE]
proof (state)
this:
\<exists>a p'. p = a # p' \<and> (a \<longrightarrow> internal p' l) \<and> (\<not> a \<longrightarrow> internal p' r)

goal (1 subgoal):
 1. \<exists>a p'. p = a # p' \<and> (a \<longrightarrow> internal p' l) \<and> (\<not> a \<longrightarrow> internal p' r) \<Longrightarrow> internal p (Branching l r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<exists>a p'. p = a # p' \<and> (a \<longrightarrow> internal p' l) \<and> (\<not> a \<longrightarrow> internal p' r)
[PROOF STEP]
obtain a p' where "p=a#p'\<and> (a \<longrightarrow> internal p' l) \<and> (\<not>a \<longrightarrow> internal p' r)"
[PROOF STATE]
proof (prove)
using this:
\<exists>a p'. p = a # p' \<and> (a \<longrightarrow> internal p' l) \<and> (\<not> a \<longrightarrow> internal p' r)

goal (1 subgoal):
 1. (\<And>a p'. p = a # p' \<and> (a \<longrightarrow> internal p' l) \<and> (\<not> a \<longrightarrow> internal p' r) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
p = a # p' \<and> (a \<longrightarrow> internal p' l) \<and> (\<not> a \<longrightarrow> internal p' r)

goal (1 subgoal):
 1. \<exists>a p'. p = a # p' \<and> (a \<longrightarrow> internal p' l) \<and> (\<not> a \<longrightarrow> internal p' r) \<Longrightarrow> internal p (Branching l r)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
p = a # p' \<and> (a \<longrightarrow> internal p' l) \<and> (\<not> a \<longrightarrow> internal p' r)
[PROOF STEP]
show ?L
[PROOF STATE]
proof (prove)
using this:
p = a # p' \<and> (a \<longrightarrow> internal p' l) \<and> (\<not> a \<longrightarrow> internal p' r)

goal (1 subgoal):
 1. internal p (Branching l r)
[PROOF STEP]
by (cases a) auto
[PROOF STATE]
proof (state)
this:
internal p (Branching l r)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
internal p (Branching l r)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma internal_is_path:
  assumes "internal ds T"
  shows "path ds T"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. path ds T
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
internal ds T

goal (1 subgoal):
 1. path ds T
[PROOF STEP]
proof (induction T arbitrary: ds)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>ds. internal ds Leaf \<Longrightarrow> path ds Leaf
 2. \<And>T1 T2 ds. \<lbrakk>\<And>ds. internal ds T1 \<Longrightarrow> path ds T1; \<And>ds. internal ds T2 \<Longrightarrow> path ds T2; internal ds (Branching T1 T2)\<rbrakk> \<Longrightarrow> path ds (Branching T1 T2)
[PROOF STEP]
case Leaf
[PROOF STATE]
proof (state)
this:
internal ds Leaf

goal (2 subgoals):
 1. \<And>ds. internal ds Leaf \<Longrightarrow> path ds Leaf
 2. \<And>T1 T2 ds. \<lbrakk>\<And>ds. internal ds T1 \<Longrightarrow> path ds T1; \<And>ds. internal ds T2 \<Longrightarrow> path ds T2; internal ds (Branching T1 T2)\<rbrakk> \<Longrightarrow> path ds (Branching T1 T2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
internal ds Leaf
[PROOF STEP]
have "False"
[PROOF STATE]
proof (prove)
using this:
internal ds Leaf

goal (1 subgoal):
 1. False
[PROOF STEP]
using internal_inv_Leaf
[PROOF STATE]
proof (prove)
using this:
internal ds Leaf
\<not> internal ?b Leaf

goal (1 subgoal):
 1. False
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
False

goal (2 subgoals):
 1. \<And>ds. internal ds Leaf \<Longrightarrow> path ds Leaf
 2. \<And>T1 T2 ds. \<lbrakk>\<And>ds. internal ds T1 \<Longrightarrow> path ds T1; \<And>ds. internal ds T2 \<Longrightarrow> path ds T2; internal ds (Branching T1 T2)\<rbrakk> \<Longrightarrow> path ds (Branching T1 T2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
False
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
False

goal (1 subgoal):
 1. path ds Leaf
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
path ds Leaf

goal (1 subgoal):
 1. \<And>T1 T2 ds. \<lbrakk>\<And>ds. internal ds T1 \<Longrightarrow> path ds T1; \<And>ds. internal ds T2 \<Longrightarrow> path ds T2; internal ds (Branching T1 T2)\<rbrakk> \<Longrightarrow> path ds (Branching T1 T2)
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>T1 T2 ds. \<lbrakk>\<And>ds. internal ds T1 \<Longrightarrow> path ds T1; \<And>ds. internal ds T2 \<Longrightarrow> path ds T2; internal ds (Branching T1 T2)\<rbrakk> \<Longrightarrow> path ds (Branching T1 T2)
[PROOF STEP]
case (Branching T\<^sub>1 T\<^sub>2)
[PROOF STATE]
proof (state)
this:
internal ?ds T\<^sub>1 \<Longrightarrow> path ?ds T\<^sub>1
internal ?ds T\<^sub>2 \<Longrightarrow> path ?ds T\<^sub>2
internal ds (Branching T\<^sub>1 T\<^sub>2)

goal (1 subgoal):
 1. \<And>T1 T2 ds. \<lbrakk>\<And>ds. internal ds T1 \<Longrightarrow> path ds T1; \<And>ds. internal ds T2 \<Longrightarrow> path ds T2; internal ds (Branching T1 T2)\<rbrakk> \<Longrightarrow> path ds (Branching T1 T2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
internal ?ds T\<^sub>1 \<Longrightarrow> path ?ds T\<^sub>1
internal ?ds T\<^sub>2 \<Longrightarrow> path ?ds T\<^sub>2
internal ds (Branching T\<^sub>1 T\<^sub>2)
[PROOF STEP]
obtain a b where ds_p: "ds=[] \<or> ds = a # b \<and> (a \<longrightarrow> internal b T\<^sub>1) \<and> (\<not> a \<longrightarrow> internal b T\<^sub>2)"
[PROOF STATE]
proof (prove)
using this:
internal ?ds T\<^sub>1 \<Longrightarrow> path ?ds T\<^sub>1
internal ?ds T\<^sub>2 \<Longrightarrow> path ?ds T\<^sub>2
internal ds (Branching T\<^sub>1 T\<^sub>2)

goal (1 subgoal):
 1. (\<And>a b. ds = [] \<or> ds = a # b \<and> (a \<longrightarrow> internal b T\<^sub>1) \<and> (\<not> a \<longrightarrow> internal b T\<^sub>2) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using internal_inv_Branching
[PROOF STATE]
proof (prove)
using this:
internal ?ds T\<^sub>1 \<Longrightarrow> path ?ds T\<^sub>1
internal ?ds T\<^sub>2 \<Longrightarrow> path ?ds T\<^sub>2
internal ds (Branching T\<^sub>1 T\<^sub>2)
internal ?p (Branching ?l ?r) = (?p = [] \<or> (\<exists>a p'. ?p = a # p' \<and> (a \<longrightarrow> internal p' ?l) \<and> (\<not> a \<longrightarrow> internal p' ?r)))

goal (1 subgoal):
 1. (\<And>a b. ds = [] \<or> ds = a # b \<and> (a \<longrightarrow> internal b T\<^sub>1) \<and> (\<not> a \<longrightarrow> internal b T\<^sub>2) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
ds = [] \<or> ds = a # b \<and> (a \<longrightarrow> internal b T\<^sub>1) \<and> (\<not> a \<longrightarrow> internal b T\<^sub>2)

goal (1 subgoal):
 1. \<And>T1 T2 ds. \<lbrakk>\<And>ds. internal ds T1 \<Longrightarrow> path ds T1; \<And>ds. internal ds T2 \<Longrightarrow> path ds T2; internal ds (Branching T1 T2)\<rbrakk> \<Longrightarrow> path ds (Branching T1 T2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ds = [] \<or> ds = a # b \<and> (a \<longrightarrow> internal b T\<^sub>1) \<and> (\<not> a \<longrightarrow> internal b T\<^sub>2)
[PROOF STEP]
have "ds = [] \<or> (a \<longrightarrow> path b T\<^sub>1) \<and> (\<not>a \<longrightarrow> path b T\<^sub>2)"
[PROOF STATE]
proof (prove)
using this:
ds = [] \<or> ds = a # b \<and> (a \<longrightarrow> internal b T\<^sub>1) \<and> (\<not> a \<longrightarrow> internal b T\<^sub>2)

goal (1 subgoal):
 1. ds = [] \<or> (a \<longrightarrow> path b T\<^sub>1) \<and> (\<not> a \<longrightarrow> path b T\<^sub>2)
[PROOF STEP]
using Branching
[PROOF STATE]
proof (prove)
using this:
ds = [] \<or> ds = a # b \<and> (a \<longrightarrow> internal b T\<^sub>1) \<and> (\<not> a \<longrightarrow> internal b T\<^sub>2)
internal ?ds T\<^sub>1 \<Longrightarrow> path ?ds T\<^sub>1
internal ?ds T\<^sub>2 \<Longrightarrow> path ?ds T\<^sub>2
internal ds (Branching T\<^sub>1 T\<^sub>2)

goal (1 subgoal):
 1. ds = [] \<or> (a \<longrightarrow> path b T\<^sub>1) \<and> (\<not> a \<longrightarrow> path b T\<^sub>2)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
ds = [] \<or> (a \<longrightarrow> path b T\<^sub>1) \<and> (\<not> a \<longrightarrow> path b T\<^sub>2)

goal (1 subgoal):
 1. \<And>T1 T2 ds. \<lbrakk>\<And>ds. internal ds T1 \<Longrightarrow> path ds T1; \<And>ds. internal ds T2 \<Longrightarrow> path ds T2; internal ds (Branching T1 T2)\<rbrakk> \<Longrightarrow> path ds (Branching T1 T2)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
ds = [] \<or> (a \<longrightarrow> path b T\<^sub>1) \<and> (\<not> a \<longrightarrow> path b T\<^sub>2)
[PROOF STEP]
show "?case"
[PROOF STATE]
proof (prove)
using this:
ds = [] \<or> (a \<longrightarrow> path b T\<^sub>1) \<and> (\<not> a \<longrightarrow> path b T\<^sub>2)

goal (1 subgoal):
 1. path ds (Branching T\<^sub>1 T\<^sub>2)
[PROOF STEP]
using ds_p
[PROOF STATE]
proof (prove)
using this:
ds = [] \<or> (a \<longrightarrow> path b T\<^sub>1) \<and> (\<not> a \<longrightarrow> path b T\<^sub>2)
ds = [] \<or> ds = a # b \<and> (a \<longrightarrow> internal b T\<^sub>1) \<and> (\<not> a \<longrightarrow> internal b T\<^sub>2)

goal (1 subgoal):
 1. path ds (Branching T\<^sub>1 T\<^sub>2)
[PROOF STEP]
by (cases a) auto
[PROOF STATE]
proof (state)
this:
path ds (Branching T\<^sub>1 T\<^sub>2)

goal:
No subgoals!
[PROOF STEP]
qed