[STATEMENT]
lemma nodes_inv:
  assumes "\<forall> x \<in> set ts. is_leveln_node n x \<and> is_measured_node x"
  and "length ts \<ge> 2"
  shows "\<forall> x \<in> set (nodes ts). is_leveln_node (Suc n) x \<and> is_measured_node x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>set (nodes ts). is_leveln_node (Suc n) x \<and> is_measured_node x
[PROOF STEP]
proof (insert assms, induct ts rule: nodes.induct)
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>a b. \<lbrakk>\<forall>x\<in>set [a, b]. is_leveln_node n x \<and> is_measured_node x; 2 \<le> length [a, b]\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes [a, b]). is_leveln_node (Suc n) x \<and> is_measured_node x
 2. \<And>a b c. \<lbrakk>\<forall>x\<in>set [a, b, c]. is_leveln_node n x \<and> is_measured_node x; 2 \<le> length [a, b, c]\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes [a, b, c]). is_leveln_node (Suc n) x \<and> is_measured_node x
 3. \<And>a b c d. \<lbrakk>\<forall>x\<in>set [a, b, c, d]. is_leveln_node n x \<and> is_measured_node x; 2 \<le> length [a, b, c, d]\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes [a, b, c, d]). is_leveln_node (Suc n) x \<and> is_measured_node x
 4. \<And>a b c v vb vc. \<lbrakk>\<lbrakk>\<forall>x\<in>set (v # vb # vc). is_leveln_node n x \<and> is_measured_node x; 2 \<le> length (v # vb # vc)\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes (v # vb # vc)). is_leveln_node (Suc n) x \<and> is_measured_node x; \<forall>x\<in>set (a # b # c # v # vb # vc). is_leveln_node n x \<and> is_measured_node x; 2 \<le> length (a # b # c # v # vb # vc)\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes (a # b # c # v # vb # vc)). is_leveln_node (Suc n) x \<and> is_measured_node x
 5. \<lbrakk>\<forall>x\<in>set []. is_leveln_node n x \<and> is_measured_node x; 2 \<le> length []\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes []). is_leveln_node (Suc n) x \<and> is_measured_node x
 6. \<And>v. \<lbrakk>\<forall>x\<in>set [v]. is_leveln_node n x \<and> is_measured_node x; 2 \<le> length [v]\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes [v]). is_leveln_node (Suc n) x \<and> is_measured_node x
[PROOF STEP]
case (1 a b)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set [a, b]. is_leveln_node n x \<and> is_measured_node x
2 \<le> length [a, b]

goal (6 subgoals):
 1. \<And>a b. \<lbrakk>\<forall>x\<in>set [a, b]. is_leveln_node n x \<and> is_measured_node x; 2 \<le> length [a, b]\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes [a, b]). is_leveln_node (Suc n) x \<and> is_measured_node x
 2. \<And>a b c. \<lbrakk>\<forall>x\<in>set [a, b, c]. is_leveln_node n x \<and> is_measured_node x; 2 \<le> length [a, b, c]\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes [a, b, c]). is_leveln_node (Suc n) x \<and> is_measured_node x
 3. \<And>a b c d. \<lbrakk>\<forall>x\<in>set [a, b, c, d]. is_leveln_node n x \<and> is_measured_node x; 2 \<le> length [a, b, c, d]\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes [a, b, c, d]). is_leveln_node (Suc n) x \<and> is_measured_node x
 4. \<And>a b c v vb vc. \<lbrakk>\<lbrakk>\<forall>x\<in>set (v # vb # vc). is_leveln_node n x \<and> is_measured_node x; 2 \<le> length (v # vb # vc)\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes (v # vb # vc)). is_leveln_node (Suc n) x \<and> is_measured_node x; \<forall>x\<in>set (a # b # c # v # vb # vc). is_leveln_node n x \<and> is_measured_node x; 2 \<le> length (a # b # c # v # vb # vc)\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes (a # b # c # v # vb # vc)). is_leveln_node (Suc n) x \<and> is_measured_node x
 5. \<lbrakk>\<forall>x\<in>set []. is_leveln_node n x \<and> is_measured_node x; 2 \<le> length []\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes []). is_leveln_node (Suc n) x \<and> is_measured_node x
 6. \<And>v. \<lbrakk>\<forall>x\<in>set [v]. is_leveln_node n x \<and> is_measured_node x; 2 \<le> length [v]\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes [v]). is_leveln_node (Suc n) x \<and> is_measured_node x
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set [a, b]. is_leveln_node n x \<and> is_measured_node x
2 \<le> length [a, b]

goal (1 subgoal):
 1. \<forall>x\<in>set (nodes [a, b]). is_leveln_node (Suc n) x \<and> is_measured_node x
[PROOF STEP]
by (simp add: node2_def)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set (nodes [a, b]). is_leveln_node (Suc n) x \<and> is_measured_node x

goal (5 subgoals):
 1. \<And>a b c. \<lbrakk>\<forall>x\<in>set [a, b, c]. is_leveln_node n x \<and> is_measured_node x; 2 \<le> length [a, b, c]\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes [a, b, c]). is_leveln_node (Suc n) x \<and> is_measured_node x
 2. \<And>a b c d. \<lbrakk>\<forall>x\<in>set [a, b, c, d]. is_leveln_node n x \<and> is_measured_node x; 2 \<le> length [a, b, c, d]\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes [a, b, c, d]). is_leveln_node (Suc n) x \<and> is_measured_node x
 3. \<And>a b c v vb vc. \<lbrakk>\<lbrakk>\<forall>x\<in>set (v # vb # vc). is_leveln_node n x \<and> is_measured_node x; 2 \<le> length (v # vb # vc)\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes (v # vb # vc)). is_leveln_node (Suc n) x \<and> is_measured_node x; \<forall>x\<in>set (a # b # c # v # vb # vc). is_leveln_node n x \<and> is_measured_node x; 2 \<le> length (a # b # c # v # vb # vc)\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes (a # b # c # v # vb # vc)). is_leveln_node (Suc n) x \<and> is_measured_node x
 4. \<lbrakk>\<forall>x\<in>set []. is_leveln_node n x \<and> is_measured_node x; 2 \<le> length []\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes []). is_leveln_node (Suc n) x \<and> is_measured_node x
 5. \<And>v. \<lbrakk>\<forall>x\<in>set [v]. is_leveln_node n x \<and> is_measured_node x; 2 \<le> length [v]\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes [v]). is_leveln_node (Suc n) x \<and> is_measured_node x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>a b c. \<lbrakk>\<forall>x\<in>set [a, b, c]. is_leveln_node n x \<and> is_measured_node x; 2 \<le> length [a, b, c]\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes [a, b, c]). is_leveln_node (Suc n) x \<and> is_measured_node x
 2. \<And>a b c d. \<lbrakk>\<forall>x\<in>set [a, b, c, d]. is_leveln_node n x \<and> is_measured_node x; 2 \<le> length [a, b, c, d]\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes [a, b, c, d]). is_leveln_node (Suc n) x \<and> is_measured_node x
 3. \<And>a b c v vb vc. \<lbrakk>\<lbrakk>\<forall>x\<in>set (v # vb # vc). is_leveln_node n x \<and> is_measured_node x; 2 \<le> length (v # vb # vc)\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes (v # vb # vc)). is_leveln_node (Suc n) x \<and> is_measured_node x; \<forall>x\<in>set (a # b # c # v # vb # vc). is_leveln_node n x \<and> is_measured_node x; 2 \<le> length (a # b # c # v # vb # vc)\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes (a # b # c # v # vb # vc)). is_leveln_node (Suc n) x \<and> is_measured_node x
 4. \<lbrakk>\<forall>x\<in>set []. is_leveln_node n x \<and> is_measured_node x; 2 \<le> length []\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes []). is_leveln_node (Suc n) x \<and> is_measured_node x
 5. \<And>v. \<lbrakk>\<forall>x\<in>set [v]. is_leveln_node n x \<and> is_measured_node x; 2 \<le> length [v]\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes [v]). is_leveln_node (Suc n) x \<and> is_measured_node x
[PROOF STEP]
case (2 a b c)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set [a, b, c]. is_leveln_node n x \<and> is_measured_node x
2 \<le> length [a, b, c]

goal (5 subgoals):
 1. \<And>a b c. \<lbrakk>\<forall>x\<in>set [a, b, c]. is_leveln_node n x \<and> is_measured_node x; 2 \<le> length [a, b, c]\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes [a, b, c]). is_leveln_node (Suc n) x \<and> is_measured_node x
 2. \<And>a b c d. \<lbrakk>\<forall>x\<in>set [a, b, c, d]. is_leveln_node n x \<and> is_measured_node x; 2 \<le> length [a, b, c, d]\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes [a, b, c, d]). is_leveln_node (Suc n) x \<and> is_measured_node x
 3. \<And>a b c v vb vc. \<lbrakk>\<lbrakk>\<forall>x\<in>set (v # vb # vc). is_leveln_node n x \<and> is_measured_node x; 2 \<le> length (v # vb # vc)\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes (v # vb # vc)). is_leveln_node (Suc n) x \<and> is_measured_node x; \<forall>x\<in>set (a # b # c # v # vb # vc). is_leveln_node n x \<and> is_measured_node x; 2 \<le> length (a # b # c # v # vb # vc)\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes (a # b # c # v # vb # vc)). is_leveln_node (Suc n) x \<and> is_measured_node x
 4. \<lbrakk>\<forall>x\<in>set []. is_leveln_node n x \<and> is_measured_node x; 2 \<le> length []\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes []). is_leveln_node (Suc n) x \<and> is_measured_node x
 5. \<And>v. \<lbrakk>\<forall>x\<in>set [v]. is_leveln_node n x \<and> is_measured_node x; 2 \<le> length [v]\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes [v]). is_leveln_node (Suc n) x \<and> is_measured_node x
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set [a, b, c]. is_leveln_node n x \<and> is_measured_node x
2 \<le> length [a, b, c]

goal (1 subgoal):
 1. \<forall>x\<in>set (nodes [a, b, c]). is_leveln_node (Suc n) x \<and> is_measured_node x
[PROOF STEP]
by (simp add: node3_def)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set (nodes [a, b, c]). is_leveln_node (Suc n) x \<and> is_measured_node x

goal (4 subgoals):
 1. \<And>a b c d. \<lbrakk>\<forall>x\<in>set [a, b, c, d]. is_leveln_node n x \<and> is_measured_node x; 2 \<le> length [a, b, c, d]\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes [a, b, c, d]). is_leveln_node (Suc n) x \<and> is_measured_node x
 2. \<And>a b c v vb vc. \<lbrakk>\<lbrakk>\<forall>x\<in>set (v # vb # vc). is_leveln_node n x \<and> is_measured_node x; 2 \<le> length (v # vb # vc)\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes (v # vb # vc)). is_leveln_node (Suc n) x \<and> is_measured_node x; \<forall>x\<in>set (a # b # c # v # vb # vc). is_leveln_node n x \<and> is_measured_node x; 2 \<le> length (a # b # c # v # vb # vc)\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes (a # b # c # v # vb # vc)). is_leveln_node (Suc n) x \<and> is_measured_node x
 3. \<lbrakk>\<forall>x\<in>set []. is_leveln_node n x \<and> is_measured_node x; 2 \<le> length []\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes []). is_leveln_node (Suc n) x \<and> is_measured_node x
 4. \<And>v. \<lbrakk>\<forall>x\<in>set [v]. is_leveln_node n x \<and> is_measured_node x; 2 \<le> length [v]\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes [v]). is_leveln_node (Suc n) x \<and> is_measured_node x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>a b c d. \<lbrakk>\<forall>x\<in>set [a, b, c, d]. is_leveln_node n x \<and> is_measured_node x; 2 \<le> length [a, b, c, d]\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes [a, b, c, d]). is_leveln_node (Suc n) x \<and> is_measured_node x
 2. \<And>a b c v vb vc. \<lbrakk>\<lbrakk>\<forall>x\<in>set (v # vb # vc). is_leveln_node n x \<and> is_measured_node x; 2 \<le> length (v # vb # vc)\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes (v # vb # vc)). is_leveln_node (Suc n) x \<and> is_measured_node x; \<forall>x\<in>set (a # b # c # v # vb # vc). is_leveln_node n x \<and> is_measured_node x; 2 \<le> length (a # b # c # v # vb # vc)\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes (a # b # c # v # vb # vc)). is_leveln_node (Suc n) x \<and> is_measured_node x
 3. \<lbrakk>\<forall>x\<in>set []. is_leveln_node n x \<and> is_measured_node x; 2 \<le> length []\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes []). is_leveln_node (Suc n) x \<and> is_measured_node x
 4. \<And>v. \<lbrakk>\<forall>x\<in>set [v]. is_leveln_node n x \<and> is_measured_node x; 2 \<le> length [v]\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes [v]). is_leveln_node (Suc n) x \<and> is_measured_node x
[PROOF STEP]
case (3 a b c d)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set [a, b, c, d]. is_leveln_node n x \<and> is_measured_node x
2 \<le> length [a, b, c, d]

goal (4 subgoals):
 1. \<And>a b c d. \<lbrakk>\<forall>x\<in>set [a, b, c, d]. is_leveln_node n x \<and> is_measured_node x; 2 \<le> length [a, b, c, d]\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes [a, b, c, d]). is_leveln_node (Suc n) x \<and> is_measured_node x
 2. \<And>a b c v vb vc. \<lbrakk>\<lbrakk>\<forall>x\<in>set (v # vb # vc). is_leveln_node n x \<and> is_measured_node x; 2 \<le> length (v # vb # vc)\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes (v # vb # vc)). is_leveln_node (Suc n) x \<and> is_measured_node x; \<forall>x\<in>set (a # b # c # v # vb # vc). is_leveln_node n x \<and> is_measured_node x; 2 \<le> length (a # b # c # v # vb # vc)\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes (a # b # c # v # vb # vc)). is_leveln_node (Suc n) x \<and> is_measured_node x
 3. \<lbrakk>\<forall>x\<in>set []. is_leveln_node n x \<and> is_measured_node x; 2 \<le> length []\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes []). is_leveln_node (Suc n) x \<and> is_measured_node x
 4. \<And>v. \<lbrakk>\<forall>x\<in>set [v]. is_leveln_node n x \<and> is_measured_node x; 2 \<le> length [v]\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes [v]). is_leveln_node (Suc n) x \<and> is_measured_node x
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set [a, b, c, d]. is_leveln_node n x \<and> is_measured_node x
2 \<le> length [a, b, c, d]

goal (1 subgoal):
 1. \<forall>x\<in>set (nodes [a, b, c, d]). is_leveln_node (Suc n) x \<and> is_measured_node x
[PROOF STEP]
by (simp add: node2_def)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set (nodes [a, b, c, d]). is_leveln_node (Suc n) x \<and> is_measured_node x

goal (3 subgoals):
 1. \<And>a b c v vb vc. \<lbrakk>\<lbrakk>\<forall>x\<in>set (v # vb # vc). is_leveln_node n x \<and> is_measured_node x; 2 \<le> length (v # vb # vc)\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes (v # vb # vc)). is_leveln_node (Suc n) x \<and> is_measured_node x; \<forall>x\<in>set (a # b # c # v # vb # vc). is_leveln_node n x \<and> is_measured_node x; 2 \<le> length (a # b # c # v # vb # vc)\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes (a # b # c # v # vb # vc)). is_leveln_node (Suc n) x \<and> is_measured_node x
 2. \<lbrakk>\<forall>x\<in>set []. is_leveln_node n x \<and> is_measured_node x; 2 \<le> length []\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes []). is_leveln_node (Suc n) x \<and> is_measured_node x
 3. \<And>v. \<lbrakk>\<forall>x\<in>set [v]. is_leveln_node n x \<and> is_measured_node x; 2 \<le> length [v]\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes [v]). is_leveln_node (Suc n) x \<and> is_measured_node x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>a b c v vb vc. \<lbrakk>\<lbrakk>\<forall>x\<in>set (v # vb # vc). is_leveln_node n x \<and> is_measured_node x; 2 \<le> length (v # vb # vc)\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes (v # vb # vc)). is_leveln_node (Suc n) x \<and> is_measured_node x; \<forall>x\<in>set (a # b # c # v # vb # vc). is_leveln_node n x \<and> is_measured_node x; 2 \<le> length (a # b # c # v # vb # vc)\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes (a # b # c # v # vb # vc)). is_leveln_node (Suc n) x \<and> is_measured_node x
 2. \<lbrakk>\<forall>x\<in>set []. is_leveln_node n x \<and> is_measured_node x; 2 \<le> length []\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes []). is_leveln_node (Suc n) x \<and> is_measured_node x
 3. \<And>v. \<lbrakk>\<forall>x\<in>set [v]. is_leveln_node n x \<and> is_measured_node x; 2 \<le> length [v]\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes [v]). is_leveln_node (Suc n) x \<and> is_measured_node x
[PROOF STEP]
case (4 a b c v vb vc)
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<forall>x\<in>set (v # vb # vc). is_leveln_node n x \<and> is_measured_node x; 2 \<le> length (v # vb # vc)\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes (v # vb # vc)). is_leveln_node (Suc n) x \<and> is_measured_node x
\<forall>x\<in>set (a # b # c # v # vb # vc). is_leveln_node n x \<and> is_measured_node x
2 \<le> length (a # b # c # v # vb # vc)

goal (3 subgoals):
 1. \<And>a b c v vb vc. \<lbrakk>\<lbrakk>\<forall>x\<in>set (v # vb # vc). is_leveln_node n x \<and> is_measured_node x; 2 \<le> length (v # vb # vc)\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes (v # vb # vc)). is_leveln_node (Suc n) x \<and> is_measured_node x; \<forall>x\<in>set (a # b # c # v # vb # vc). is_leveln_node n x \<and> is_measured_node x; 2 \<le> length (a # b # c # v # vb # vc)\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes (a # b # c # v # vb # vc)). is_leveln_node (Suc n) x \<and> is_measured_node x
 2. \<lbrakk>\<forall>x\<in>set []. is_leveln_node n x \<and> is_measured_node x; 2 \<le> length []\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes []). is_leveln_node (Suc n) x \<and> is_measured_node x
 3. \<And>v. \<lbrakk>\<forall>x\<in>set [v]. is_leveln_node n x \<and> is_measured_node x; 2 \<le> length [v]\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes [v]). is_leveln_node (Suc n) x \<and> is_measured_node x
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>\<forall>x\<in>set (v # vb # vc). is_leveln_node n x \<and> is_measured_node x; 2 \<le> length (v # vb # vc)\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes (v # vb # vc)). is_leveln_node (Suc n) x \<and> is_measured_node x
\<forall>x\<in>set (a # b # c # v # vb # vc). is_leveln_node n x \<and> is_measured_node x
2 \<le> length (a # b # c # v # vb # vc)

goal (1 subgoal):
 1. \<forall>x\<in>set (nodes (a # b # c # v # vb # vc)). is_leveln_node (Suc n) x \<and> is_measured_node x
[PROOF STEP]
by (simp add: node3_def)
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set (nodes (a # b # c # v # vb # vc)). is_leveln_node (Suc n) x \<and> is_measured_node x

goal (2 subgoals):
 1. \<lbrakk>\<forall>x\<in>set []. is_leveln_node n x \<and> is_measured_node x; 2 \<le> length []\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes []). is_leveln_node (Suc n) x \<and> is_measured_node x
 2. \<And>v. \<lbrakk>\<forall>x\<in>set [v]. is_leveln_node n x \<and> is_measured_node x; 2 \<le> length [v]\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes [v]). is_leveln_node (Suc n) x \<and> is_measured_node x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<forall>x\<in>set []. is_leveln_node n x \<and> is_measured_node x; 2 \<le> length []\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes []). is_leveln_node (Suc n) x \<and> is_measured_node x
 2. \<And>v. \<lbrakk>\<forall>x\<in>set [v]. is_leveln_node n x \<and> is_measured_node x; 2 \<le> length [v]\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes [v]). is_leveln_node (Suc n) x \<and> is_measured_node x
[PROOF STEP]
show "\<lbrakk>\<forall>x\<in>set []. is_leveln_node n x \<and> is_measured_node x; 2 \<le> length []\<rbrakk>
    \<Longrightarrow> \<forall>x\<in>set (nodes []). is_leveln_node (Suc n) x \<and> is_measured_node x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>x\<in>set []. is_leveln_node n x \<and> is_measured_node x; 2 \<le> length []\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes []). is_leveln_node (Suc n) x \<and> is_measured_node x
[PROOF STEP]
by  simp
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<forall>x\<in>set []. is_leveln_node n x \<and> is_measured_node x; 2 \<le> length []\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes []). is_leveln_node (Suc n) x \<and> is_measured_node x

goal (1 subgoal):
 1. \<And>v. \<lbrakk>\<forall>x\<in>set [v]. is_leveln_node n x \<and> is_measured_node x; 2 \<le> length [v]\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes [v]). is_leveln_node (Suc n) x \<and> is_measured_node x
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>v. \<lbrakk>\<forall>x\<in>set [v]. is_leveln_node n x \<and> is_measured_node x; 2 \<le> length [v]\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes [v]). is_leveln_node (Suc n) x \<and> is_measured_node x
[PROOF STEP]
show
    "\<And>v. \<lbrakk>\<forall>x\<in>set [v]. is_leveln_node n x \<and> is_measured_node x; 2 \<le> length [v]\<rbrakk>
    \<Longrightarrow> \<forall>x\<in>set (nodes [v]). is_leveln_node (Suc n) x \<and> is_measured_node x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>v. \<lbrakk>\<forall>x\<in>set [v]. is_leveln_node n x \<and> is_measured_node x; 2 \<le> length [v]\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes [v]). is_leveln_node (Suc n) x \<and> is_measured_node x
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<forall>x\<in>set [?v]. is_leveln_node n x \<and> is_measured_node x; 2 \<le> length [?v]\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes [?v]). is_leveln_node (Suc n) x \<and> is_measured_node x

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nodes_inv2:
  assumes "is_leveln_digit n sf1"
  and "is_measured_digit sf1"
  and "is_leveln_digit n pr2"
  and "is_measured_digit pr2"
  and "\<forall> x \<in> set ts. is_leveln_node n x \<and> is_measured_node x"
  shows
  "\<forall>x\<in>set (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)).
                is_leveln_node (Suc n) x \<and> is_measured_node x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>set (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)). is_leveln_node (Suc n) x \<and> is_measured_node x
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<forall>x\<in>set (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)). is_leveln_node (Suc n) x \<and> is_measured_node x
[PROOF STEP]
have v1:" \<forall>x\<in>set (digitToNlist sf1 @ ts @ digitToNlist pr2).
                 is_leveln_node n x \<and> is_measured_node x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<forall>x\<in>set (digitToNlist sf1 @ ts @ digitToNlist pr2). is_leveln_node n x \<and> is_measured_node x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
is_leveln_digit n sf1
is_measured_digit sf1
is_leveln_digit n pr2
is_measured_digit pr2
\<forall>x\<in>set ts. is_leveln_node n x \<and> is_measured_node x

goal (1 subgoal):
 1. \<forall>x\<in>set (digitToNlist sf1 @ ts @ digitToNlist pr2). is_leveln_node n x \<and> is_measured_node x
[PROOF STEP]
apply (simp add: digitToNlist_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_leveln_digit n sf1; is_measured_digit sf1; is_leveln_digit n pr2; is_measured_digit pr2; \<forall>x\<in>set ts. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (rec_Digit (\<lambda>a. [a]) (\<lambda>a b. [a, b]) (\<lambda>a b c. [a, b, c]) (\<lambda>a b c d. [a, b, c, d]) sf1) \<union> (set ts \<union> set (rec_Digit (\<lambda>a. [a]) (\<lambda>a b. [a, b]) (\<lambda>a b c. [a, b, c]) (\<lambda>a b c d. [a, b, c, d]) pr2)). is_leveln_node n x \<and> is_measured_node x
[PROOF STEP]
apply (cases sf1)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x1. \<lbrakk>is_leveln_digit n sf1; is_measured_digit sf1; is_leveln_digit n pr2; is_measured_digit pr2; \<forall>x\<in>set ts. is_leveln_node n x \<and> is_measured_node x; sf1 = One x1\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (rec_Digit (\<lambda>a. [a]) (\<lambda>a b. [a, b]) (\<lambda>a b c. [a, b, c]) (\<lambda>a b c d. [a, b, c, d]) sf1) \<union> (set ts \<union> set (rec_Digit (\<lambda>a. [a]) (\<lambda>a b. [a, b]) (\<lambda>a b c. [a, b, c]) (\<lambda>a b c d. [a, b, c, d]) pr2)). is_leveln_node n x \<and> is_measured_node x
 2. \<And>x21 x22. \<lbrakk>is_leveln_digit n sf1; is_measured_digit sf1; is_leveln_digit n pr2; is_measured_digit pr2; \<forall>x\<in>set ts. is_leveln_node n x \<and> is_measured_node x; sf1 = Two x21 x22\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (rec_Digit (\<lambda>a. [a]) (\<lambda>a b. [a, b]) (\<lambda>a b c. [a, b, c]) (\<lambda>a b c d. [a, b, c, d]) sf1) \<union> (set ts \<union> set (rec_Digit (\<lambda>a. [a]) (\<lambda>a b. [a, b]) (\<lambda>a b c. [a, b, c]) (\<lambda>a b c d. [a, b, c, d]) pr2)). is_leveln_node n x \<and> is_measured_node x
 3. \<And>x31 x32 x33. \<lbrakk>is_leveln_digit n sf1; is_measured_digit sf1; is_leveln_digit n pr2; is_measured_digit pr2; \<forall>x\<in>set ts. is_leveln_node n x \<and> is_measured_node x; sf1 = Three x31 x32 x33\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (rec_Digit (\<lambda>a. [a]) (\<lambda>a b. [a, b]) (\<lambda>a b c. [a, b, c]) (\<lambda>a b c d. [a, b, c, d]) sf1) \<union> (set ts \<union> set (rec_Digit (\<lambda>a. [a]) (\<lambda>a b. [a, b]) (\<lambda>a b c. [a, b, c]) (\<lambda>a b c d. [a, b, c, d]) pr2)). is_leveln_node n x \<and> is_measured_node x
 4. \<And>x41 x42 x43 x44. \<lbrakk>is_leveln_digit n sf1; is_measured_digit sf1; is_leveln_digit n pr2; is_measured_digit pr2; \<forall>x\<in>set ts. is_leveln_node n x \<and> is_measured_node x; sf1 = Four x41 x42 x43 x44\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (rec_Digit (\<lambda>a. [a]) (\<lambda>a b. [a, b]) (\<lambda>a b c. [a, b, c]) (\<lambda>a b c d. [a, b, c, d]) sf1) \<union> (set ts \<union> set (rec_Digit (\<lambda>a. [a]) (\<lambda>a b. [a, b]) (\<lambda>a b c. [a, b, c]) (\<lambda>a b c d. [a, b, c, d]) pr2)). is_leveln_node n x \<and> is_measured_node x
[PROOF STEP]
apply (cases pr2)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>x1 x1a. \<lbrakk>is_leveln_digit n sf1; is_measured_digit sf1; is_leveln_digit n pr2; is_measured_digit pr2; \<forall>x\<in>set ts. is_leveln_node n x \<and> is_measured_node x; sf1 = One x1; pr2 = One x1a\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (rec_Digit (\<lambda>a. [a]) (\<lambda>a b. [a, b]) (\<lambda>a b c. [a, b, c]) (\<lambda>a b c d. [a, b, c, d]) sf1) \<union> (set ts \<union> set (rec_Digit (\<lambda>a. [a]) (\<lambda>a b. [a, b]) (\<lambda>a b c. [a, b, c]) (\<lambda>a b c d. [a, b, c, d]) pr2)). is_leveln_node n x \<and> is_measured_node x
 2. \<And>x1 x21 x22. \<lbrakk>is_leveln_digit n sf1; is_measured_digit sf1; is_leveln_digit n pr2; is_measured_digit pr2; \<forall>x\<in>set ts. is_leveln_node n x \<and> is_measured_node x; sf1 = One x1; pr2 = Two x21 x22\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (rec_Digit (\<lambda>a. [a]) (\<lambda>a b. [a, b]) (\<lambda>a b c. [a, b, c]) (\<lambda>a b c d. [a, b, c, d]) sf1) \<union> (set ts \<union> set (rec_Digit (\<lambda>a. [a]) (\<lambda>a b. [a, b]) (\<lambda>a b c. [a, b, c]) (\<lambda>a b c d. [a, b, c, d]) pr2)). is_leveln_node n x \<and> is_measured_node x
 3. \<And>x1 x31 x32 x33. \<lbrakk>is_leveln_digit n sf1; is_measured_digit sf1; is_leveln_digit n pr2; is_measured_digit pr2; \<forall>x\<in>set ts. is_leveln_node n x \<and> is_measured_node x; sf1 = One x1; pr2 = Three x31 x32 x33\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (rec_Digit (\<lambda>a. [a]) (\<lambda>a b. [a, b]) (\<lambda>a b c. [a, b, c]) (\<lambda>a b c d. [a, b, c, d]) sf1) \<union> (set ts \<union> set (rec_Digit (\<lambda>a. [a]) (\<lambda>a b. [a, b]) (\<lambda>a b c. [a, b, c]) (\<lambda>a b c d. [a, b, c, d]) pr2)). is_leveln_node n x \<and> is_measured_node x
 4. \<And>x1 x41 x42 x43 x44. \<lbrakk>is_leveln_digit n sf1; is_measured_digit sf1; is_leveln_digit n pr2; is_measured_digit pr2; \<forall>x\<in>set ts. is_leveln_node n x \<and> is_measured_node x; sf1 = One x1; pr2 = Four x41 x42 x43 x44\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (rec_Digit (\<lambda>a. [a]) (\<lambda>a b. [a, b]) (\<lambda>a b c. [a, b, c]) (\<lambda>a b c d. [a, b, c, d]) sf1) \<union> (set ts \<union> set (rec_Digit (\<lambda>a. [a]) (\<lambda>a b. [a, b]) (\<lambda>a b c. [a, b, c]) (\<lambda>a b c d. [a, b, c, d]) pr2)). is_leveln_node n x \<and> is_measured_node x
 5. \<And>x21 x22. \<lbrakk>is_leveln_digit n sf1; is_measured_digit sf1; is_leveln_digit n pr2; is_measured_digit pr2; \<forall>x\<in>set ts. is_leveln_node n x \<and> is_measured_node x; sf1 = Two x21 x22\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (rec_Digit (\<lambda>a. [a]) (\<lambda>a b. [a, b]) (\<lambda>a b c. [a, b, c]) (\<lambda>a b c d. [a, b, c, d]) sf1) \<union> (set ts \<union> set (rec_Digit (\<lambda>a. [a]) (\<lambda>a b. [a, b]) (\<lambda>a b c. [a, b, c]) (\<lambda>a b c d. [a, b, c, d]) pr2)). is_leveln_node n x \<and> is_measured_node x
 6. \<And>x31 x32 x33. \<lbrakk>is_leveln_digit n sf1; is_measured_digit sf1; is_leveln_digit n pr2; is_measured_digit pr2; \<forall>x\<in>set ts. is_leveln_node n x \<and> is_measured_node x; sf1 = Three x31 x32 x33\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (rec_Digit (\<lambda>a. [a]) (\<lambda>a b. [a, b]) (\<lambda>a b c. [a, b, c]) (\<lambda>a b c d. [a, b, c, d]) sf1) \<union> (set ts \<union> set (rec_Digit (\<lambda>a. [a]) (\<lambda>a b. [a, b]) (\<lambda>a b c. [a, b, c]) (\<lambda>a b c d. [a, b, c, d]) pr2)). is_leveln_node n x \<and> is_measured_node x
 7. \<And>x41 x42 x43 x44. \<lbrakk>is_leveln_digit n sf1; is_measured_digit sf1; is_leveln_digit n pr2; is_measured_digit pr2; \<forall>x\<in>set ts. is_leveln_node n x \<and> is_measured_node x; sf1 = Four x41 x42 x43 x44\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (rec_Digit (\<lambda>a. [a]) (\<lambda>a b. [a, b]) (\<lambda>a b c. [a, b, c]) (\<lambda>a b c d. [a, b, c, d]) sf1) \<union> (set ts \<union> set (rec_Digit (\<lambda>a. [a]) (\<lambda>a b. [a, b]) (\<lambda>a b c. [a, b, c]) (\<lambda>a b c d. [a, b, c, d]) pr2)). is_leveln_node n x \<and> is_measured_node x
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x21 x22. \<lbrakk>is_leveln_node n x21 \<and> is_leveln_node n x22; is_measured_node x21 \<and> is_measured_node x22; is_leveln_digit n pr2; is_measured_digit pr2; \<forall>x\<in>set ts. is_leveln_node n x \<and> is_measured_node x; sf1 = Two x21 x22\<rbrakk> \<Longrightarrow> \<forall>x\<in>set ts \<union> set (rec_Digit (\<lambda>a. [a]) (\<lambda>a b. [a, b]) (\<lambda>a b c. [a, b, c]) (\<lambda>a b c d. [a, b, c, d]) pr2). is_leveln_node n x \<and> is_measured_node x
 2. \<And>x31 x32 x33. \<lbrakk>is_leveln_node n x31 \<and> is_leveln_node n x32 \<and> is_leveln_node n x33; is_measured_node x31 \<and> is_measured_node x32 \<and> is_measured_node x33; is_leveln_digit n pr2; is_measured_digit pr2; \<forall>x\<in>set ts. is_leveln_node n x \<and> is_measured_node x; sf1 = Three x31 x32 x33\<rbrakk> \<Longrightarrow> \<forall>x\<in>set ts \<union> set (rec_Digit (\<lambda>a. [a]) (\<lambda>a b. [a, b]) (\<lambda>a b c. [a, b, c]) (\<lambda>a b c d. [a, b, c, d]) pr2). is_leveln_node n x \<and> is_measured_node x
 3. \<And>x41 x42 x43 x44. \<lbrakk>is_leveln_node n x41 \<and> is_leveln_node n x42 \<and> is_leveln_node n x43 \<and> is_leveln_node n x44; is_measured_node x41 \<and> is_measured_node x42 \<and> is_measured_node x43 \<and> is_measured_node x44; is_leveln_digit n pr2; is_measured_digit pr2; \<forall>x\<in>set ts. is_leveln_node n x \<and> is_measured_node x; sf1 = Four x41 x42 x43 x44\<rbrakk> \<Longrightarrow> \<forall>x\<in>set ts \<union> set (rec_Digit (\<lambda>a. [a]) (\<lambda>a b. [a, b]) (\<lambda>a b c. [a, b, c]) (\<lambda>a b c d. [a, b, c, d]) pr2). is_leveln_node n x \<and> is_measured_node x
[PROOF STEP]
apply (cases pr2)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>x21 x22 x1. \<lbrakk>is_leveln_node n x21 \<and> is_leveln_node n x22; is_measured_node x21 \<and> is_measured_node x22; is_leveln_digit n pr2; is_measured_digit pr2; \<forall>x\<in>set ts. is_leveln_node n x \<and> is_measured_node x; sf1 = Two x21 x22; pr2 = One x1\<rbrakk> \<Longrightarrow> \<forall>x\<in>set ts \<union> set (rec_Digit (\<lambda>a. [a]) (\<lambda>a b. [a, b]) (\<lambda>a b c. [a, b, c]) (\<lambda>a b c d. [a, b, c, d]) pr2). is_leveln_node n x \<and> is_measured_node x
 2. \<And>x21 x22 x21a x22a. \<lbrakk>is_leveln_node n x21 \<and> is_leveln_node n x22; is_measured_node x21 \<and> is_measured_node x22; is_leveln_digit n pr2; is_measured_digit pr2; \<forall>x\<in>set ts. is_leveln_node n x \<and> is_measured_node x; sf1 = Two x21 x22; pr2 = Two x21a x22a\<rbrakk> \<Longrightarrow> \<forall>x\<in>set ts \<union> set (rec_Digit (\<lambda>a. [a]) (\<lambda>a b. [a, b]) (\<lambda>a b c. [a, b, c]) (\<lambda>a b c d. [a, b, c, d]) pr2). is_leveln_node n x \<and> is_measured_node x
 3. \<And>x21 x22 x31 x32 x33. \<lbrakk>is_leveln_node n x21 \<and> is_leveln_node n x22; is_measured_node x21 \<and> is_measured_node x22; is_leveln_digit n pr2; is_measured_digit pr2; \<forall>x\<in>set ts. is_leveln_node n x \<and> is_measured_node x; sf1 = Two x21 x22; pr2 = Three x31 x32 x33\<rbrakk> \<Longrightarrow> \<forall>x\<in>set ts \<union> set (rec_Digit (\<lambda>a. [a]) (\<lambda>a b. [a, b]) (\<lambda>a b c. [a, b, c]) (\<lambda>a b c d. [a, b, c, d]) pr2). is_leveln_node n x \<and> is_measured_node x
 4. \<And>x21 x22 x41 x42 x43 x44. \<lbrakk>is_leveln_node n x21 \<and> is_leveln_node n x22; is_measured_node x21 \<and> is_measured_node x22; is_leveln_digit n pr2; is_measured_digit pr2; \<forall>x\<in>set ts. is_leveln_node n x \<and> is_measured_node x; sf1 = Two x21 x22; pr2 = Four x41 x42 x43 x44\<rbrakk> \<Longrightarrow> \<forall>x\<in>set ts \<union> set (rec_Digit (\<lambda>a. [a]) (\<lambda>a b. [a, b]) (\<lambda>a b c. [a, b, c]) (\<lambda>a b c d. [a, b, c, d]) pr2). is_leveln_node n x \<and> is_measured_node x
 5. \<And>x31 x32 x33. \<lbrakk>is_leveln_node n x31 \<and> is_leveln_node n x32 \<and> is_leveln_node n x33; is_measured_node x31 \<and> is_measured_node x32 \<and> is_measured_node x33; is_leveln_digit n pr2; is_measured_digit pr2; \<forall>x\<in>set ts. is_leveln_node n x \<and> is_measured_node x; sf1 = Three x31 x32 x33\<rbrakk> \<Longrightarrow> \<forall>x\<in>set ts \<union> set (rec_Digit (\<lambda>a. [a]) (\<lambda>a b. [a, b]) (\<lambda>a b c. [a, b, c]) (\<lambda>a b c d. [a, b, c, d]) pr2). is_leveln_node n x \<and> is_measured_node x
 6. \<And>x41 x42 x43 x44. \<lbrakk>is_leveln_node n x41 \<and> is_leveln_node n x42 \<and> is_leveln_node n x43 \<and> is_leveln_node n x44; is_measured_node x41 \<and> is_measured_node x42 \<and> is_measured_node x43 \<and> is_measured_node x44; is_leveln_digit n pr2; is_measured_digit pr2; \<forall>x\<in>set ts. is_leveln_node n x \<and> is_measured_node x; sf1 = Four x41 x42 x43 x44\<rbrakk> \<Longrightarrow> \<forall>x\<in>set ts \<union> set (rec_Digit (\<lambda>a. [a]) (\<lambda>a b. [a, b]) (\<lambda>a b c. [a, b, c]) (\<lambda>a b c d. [a, b, c, d]) pr2). is_leveln_node n x \<and> is_measured_node x
[PROOF STEP]
apply (simp_all)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x31 x32 x33. \<lbrakk>is_leveln_node n x31 \<and> is_leveln_node n x32 \<and> is_leveln_node n x33; is_measured_node x31 \<and> is_measured_node x32 \<and> is_measured_node x33; is_leveln_digit n pr2; is_measured_digit pr2; \<forall>x\<in>set ts. is_leveln_node n x \<and> is_measured_node x; sf1 = Three x31 x32 x33\<rbrakk> \<Longrightarrow> \<forall>x\<in>set ts \<union> set (rec_Digit (\<lambda>a. [a]) (\<lambda>a b. [a, b]) (\<lambda>a b c. [a, b, c]) (\<lambda>a b c d. [a, b, c, d]) pr2). is_leveln_node n x \<and> is_measured_node x
 2. \<And>x41 x42 x43 x44. \<lbrakk>is_leveln_node n x41 \<and> is_leveln_node n x42 \<and> is_leveln_node n x43 \<and> is_leveln_node n x44; is_measured_node x41 \<and> is_measured_node x42 \<and> is_measured_node x43 \<and> is_measured_node x44; is_leveln_digit n pr2; is_measured_digit pr2; \<forall>x\<in>set ts. is_leveln_node n x \<and> is_measured_node x; sf1 = Four x41 x42 x43 x44\<rbrakk> \<Longrightarrow> \<forall>x\<in>set ts \<union> set (rec_Digit (\<lambda>a. [a]) (\<lambda>a b. [a, b]) (\<lambda>a b c. [a, b, c]) (\<lambda>a b c d. [a, b, c, d]) pr2). is_leveln_node n x \<and> is_measured_node x
[PROOF STEP]
apply (cases pr2)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x31 x32 x33 x1. \<lbrakk>is_leveln_node n x31 \<and> is_leveln_node n x32 \<and> is_leveln_node n x33; is_measured_node x31 \<and> is_measured_node x32 \<and> is_measured_node x33; is_leveln_digit n pr2; is_measured_digit pr2; \<forall>x\<in>set ts. is_leveln_node n x \<and> is_measured_node x; sf1 = Three x31 x32 x33; pr2 = One x1\<rbrakk> \<Longrightarrow> \<forall>x\<in>set ts \<union> set (rec_Digit (\<lambda>a. [a]) (\<lambda>a b. [a, b]) (\<lambda>a b c. [a, b, c]) (\<lambda>a b c d. [a, b, c, d]) pr2). is_leveln_node n x \<and> is_measured_node x
 2. \<And>x31 x32 x33 x21 x22. \<lbrakk>is_leveln_node n x31 \<and> is_leveln_node n x32 \<and> is_leveln_node n x33; is_measured_node x31 \<and> is_measured_node x32 \<and> is_measured_node x33; is_leveln_digit n pr2; is_measured_digit pr2; \<forall>x\<in>set ts. is_leveln_node n x \<and> is_measured_node x; sf1 = Three x31 x32 x33; pr2 = Two x21 x22\<rbrakk> \<Longrightarrow> \<forall>x\<in>set ts \<union> set (rec_Digit (\<lambda>a. [a]) (\<lambda>a b. [a, b]) (\<lambda>a b c. [a, b, c]) (\<lambda>a b c d. [a, b, c, d]) pr2). is_leveln_node n x \<and> is_measured_node x
 3. \<And>x31 x32 x33 x31a x32a x33a. \<lbrakk>is_leveln_node n x31 \<and> is_leveln_node n x32 \<and> is_leveln_node n x33; is_measured_node x31 \<and> is_measured_node x32 \<and> is_measured_node x33; is_leveln_digit n pr2; is_measured_digit pr2; \<forall>x\<in>set ts. is_leveln_node n x \<and> is_measured_node x; sf1 = Three x31 x32 x33; pr2 = Three x31a x32a x33a\<rbrakk> \<Longrightarrow> \<forall>x\<in>set ts \<union> set (rec_Digit (\<lambda>a. [a]) (\<lambda>a b. [a, b]) (\<lambda>a b c. [a, b, c]) (\<lambda>a b c d. [a, b, c, d]) pr2). is_leveln_node n x \<and> is_measured_node x
 4. \<And>x31 x32 x33 x41 x42 x43 x44. \<lbrakk>is_leveln_node n x31 \<and> is_leveln_node n x32 \<and> is_leveln_node n x33; is_measured_node x31 \<and> is_measured_node x32 \<and> is_measured_node x33; is_leveln_digit n pr2; is_measured_digit pr2; \<forall>x\<in>set ts. is_leveln_node n x \<and> is_measured_node x; sf1 = Three x31 x32 x33; pr2 = Four x41 x42 x43 x44\<rbrakk> \<Longrightarrow> \<forall>x\<in>set ts \<union> set (rec_Digit (\<lambda>a. [a]) (\<lambda>a b. [a, b]) (\<lambda>a b c. [a, b, c]) (\<lambda>a b c d. [a, b, c, d]) pr2). is_leveln_node n x \<and> is_measured_node x
 5. \<And>x41 x42 x43 x44. \<lbrakk>is_leveln_node n x41 \<and> is_leveln_node n x42 \<and> is_leveln_node n x43 \<and> is_leveln_node n x44; is_measured_node x41 \<and> is_measured_node x42 \<and> is_measured_node x43 \<and> is_measured_node x44; is_leveln_digit n pr2; is_measured_digit pr2; \<forall>x\<in>set ts. is_leveln_node n x \<and> is_measured_node x; sf1 = Four x41 x42 x43 x44\<rbrakk> \<Longrightarrow> \<forall>x\<in>set ts \<union> set (rec_Digit (\<lambda>a. [a]) (\<lambda>a b. [a, b]) (\<lambda>a b c. [a, b, c]) (\<lambda>a b c d. [a, b, c, d]) pr2). is_leveln_node n x \<and> is_measured_node x
[PROOF STEP]
apply (simp_all)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x41 x42 x43 x44. \<lbrakk>is_leveln_node n x41 \<and> is_leveln_node n x42 \<and> is_leveln_node n x43 \<and> is_leveln_node n x44; is_measured_node x41 \<and> is_measured_node x42 \<and> is_measured_node x43 \<and> is_measured_node x44; is_leveln_digit n pr2; is_measured_digit pr2; \<forall>x\<in>set ts. is_leveln_node n x \<and> is_measured_node x; sf1 = Four x41 x42 x43 x44\<rbrakk> \<Longrightarrow> \<forall>x\<in>set ts \<union> set (rec_Digit (\<lambda>a. [a]) (\<lambda>a b. [a, b]) (\<lambda>a b c. [a, b, c]) (\<lambda>a b c d. [a, b, c, d]) pr2). is_leveln_node n x \<and> is_measured_node x
[PROOF STEP]
apply (cases pr2)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x41 x42 x43 x44 x1. \<lbrakk>is_leveln_node n x41 \<and> is_leveln_node n x42 \<and> is_leveln_node n x43 \<and> is_leveln_node n x44; is_measured_node x41 \<and> is_measured_node x42 \<and> is_measured_node x43 \<and> is_measured_node x44; is_leveln_digit n pr2; is_measured_digit pr2; \<forall>x\<in>set ts. is_leveln_node n x \<and> is_measured_node x; sf1 = Four x41 x42 x43 x44; pr2 = One x1\<rbrakk> \<Longrightarrow> \<forall>x\<in>set ts \<union> set (rec_Digit (\<lambda>a. [a]) (\<lambda>a b. [a, b]) (\<lambda>a b c. [a, b, c]) (\<lambda>a b c d. [a, b, c, d]) pr2). is_leveln_node n x \<and> is_measured_node x
 2. \<And>x41 x42 x43 x44 x21 x22. \<lbrakk>is_leveln_node n x41 \<and> is_leveln_node n x42 \<and> is_leveln_node n x43 \<and> is_leveln_node n x44; is_measured_node x41 \<and> is_measured_node x42 \<and> is_measured_node x43 \<and> is_measured_node x44; is_leveln_digit n pr2; is_measured_digit pr2; \<forall>x\<in>set ts. is_leveln_node n x \<and> is_measured_node x; sf1 = Four x41 x42 x43 x44; pr2 = Two x21 x22\<rbrakk> \<Longrightarrow> \<forall>x\<in>set ts \<union> set (rec_Digit (\<lambda>a. [a]) (\<lambda>a b. [a, b]) (\<lambda>a b c. [a, b, c]) (\<lambda>a b c d. [a, b, c, d]) pr2). is_leveln_node n x \<and> is_measured_node x
 3. \<And>x41 x42 x43 x44 x31 x32 x33. \<lbrakk>is_leveln_node n x41 \<and> is_leveln_node n x42 \<and> is_leveln_node n x43 \<and> is_leveln_node n x44; is_measured_node x41 \<and> is_measured_node x42 \<and> is_measured_node x43 \<and> is_measured_node x44; is_leveln_digit n pr2; is_measured_digit pr2; \<forall>x\<in>set ts. is_leveln_node n x \<and> is_measured_node x; sf1 = Four x41 x42 x43 x44; pr2 = Three x31 x32 x33\<rbrakk> \<Longrightarrow> \<forall>x\<in>set ts \<union> set (rec_Digit (\<lambda>a. [a]) (\<lambda>a b. [a, b]) (\<lambda>a b c. [a, b, c]) (\<lambda>a b c d. [a, b, c, d]) pr2). is_leveln_node n x \<and> is_measured_node x
 4. \<And>x41 x42 x43 x44 x41a x42a x43a x44a. \<lbrakk>is_leveln_node n x41 \<and> is_leveln_node n x42 \<and> is_leveln_node n x43 \<and> is_leveln_node n x44; is_measured_node x41 \<and> is_measured_node x42 \<and> is_measured_node x43 \<and> is_measured_node x44; is_leveln_digit n pr2; is_measured_digit pr2; \<forall>x\<in>set ts. is_leveln_node n x \<and> is_measured_node x; sf1 = Four x41 x42 x43 x44; pr2 = Four x41a x42a x43a x44a\<rbrakk> \<Longrightarrow> \<forall>x\<in>set ts \<union> set (rec_Digit (\<lambda>a. [a]) (\<lambda>a b. [a, b]) (\<lambda>a b c. [a, b, c]) (\<lambda>a b c d. [a, b, c, d]) pr2). is_leveln_node n x \<and> is_measured_node x
[PROOF STEP]
apply (simp_all)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set (digitToNlist sf1 @ ts @ digitToNlist pr2). is_leveln_node n x \<and> is_measured_node x

goal (1 subgoal):
 1. \<forall>x\<in>set (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)). is_leveln_node (Suc n) x \<and> is_measured_node x
[PROOF STEP]
have v2: "length (digitToNlist sf1 @ ts @ digitToNlist pr2) \<ge> 2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 \<le> length (digitToNlist sf1 @ ts @ digitToNlist pr2)
[PROOF STEP]
apply (cases sf1)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x1. sf1 = One x1 \<Longrightarrow> 2 \<le> length (digitToNlist sf1 @ ts @ digitToNlist pr2)
 2. \<And>x21 x22. sf1 = Two x21 x22 \<Longrightarrow> 2 \<le> length (digitToNlist sf1 @ ts @ digitToNlist pr2)
 3. \<And>x31 x32 x33. sf1 = Three x31 x32 x33 \<Longrightarrow> 2 \<le> length (digitToNlist sf1 @ ts @ digitToNlist pr2)
 4. \<And>x41 x42 x43 x44. sf1 = Four x41 x42 x43 x44 \<Longrightarrow> 2 \<le> length (digitToNlist sf1 @ ts @ digitToNlist pr2)
[PROOF STEP]
apply (cases pr2)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>x1 x1a. \<lbrakk>sf1 = One x1; pr2 = One x1a\<rbrakk> \<Longrightarrow> 2 \<le> length (digitToNlist sf1 @ ts @ digitToNlist pr2)
 2. \<And>x1 x21 x22. \<lbrakk>sf1 = One x1; pr2 = Two x21 x22\<rbrakk> \<Longrightarrow> 2 \<le> length (digitToNlist sf1 @ ts @ digitToNlist pr2)
 3. \<And>x1 x31 x32 x33. \<lbrakk>sf1 = One x1; pr2 = Three x31 x32 x33\<rbrakk> \<Longrightarrow> 2 \<le> length (digitToNlist sf1 @ ts @ digitToNlist pr2)
 4. \<And>x1 x41 x42 x43 x44. \<lbrakk>sf1 = One x1; pr2 = Four x41 x42 x43 x44\<rbrakk> \<Longrightarrow> 2 \<le> length (digitToNlist sf1 @ ts @ digitToNlist pr2)
 5. \<And>x21 x22. sf1 = Two x21 x22 \<Longrightarrow> 2 \<le> length (digitToNlist sf1 @ ts @ digitToNlist pr2)
 6. \<And>x31 x32 x33. sf1 = Three x31 x32 x33 \<Longrightarrow> 2 \<le> length (digitToNlist sf1 @ ts @ digitToNlist pr2)
 7. \<And>x41 x42 x43 x44. sf1 = Four x41 x42 x43 x44 \<Longrightarrow> 2 \<le> length (digitToNlist sf1 @ ts @ digitToNlist pr2)
[PROOF STEP]
apply simp_all
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
2 \<le> length (digitToNlist sf1 @ ts @ digitToNlist pr2)

goal (1 subgoal):
 1. \<forall>x\<in>set (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)). is_leveln_node (Suc n) x \<and> is_measured_node x
[PROOF STEP]
thus ?thesis
[PROOF STATE]
proof (prove)
using this:
2 \<le> length (digitToNlist sf1 @ ts @ digitToNlist pr2)

goal (1 subgoal):
 1. \<forall>x\<in>set (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)). is_leveln_node (Suc n) x \<and> is_measured_node x
[PROOF STEP]
using v1 nodes_inv[of "digitToNlist sf1 @ ts @ digitToNlist pr2"]
[PROOF STATE]
proof (prove)
using this:
2 \<le> length (digitToNlist sf1 @ ts @ digitToNlist pr2)
\<forall>x\<in>set (digitToNlist sf1 @ ts @ digitToNlist pr2). is_leveln_node n x \<and> is_measured_node x
\<lbrakk>\<forall>x\<in>set (digitToNlist sf1 @ ts @ digitToNlist pr2). is_leveln_node ?n x \<and> is_measured_node x; 2 \<le> length (digitToNlist sf1 @ ts @ digitToNlist pr2)\<rbrakk> \<Longrightarrow> \<forall>x\<in>set (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)). is_leveln_node (Suc ?n) x \<and> is_measured_node x

goal (1 subgoal):
 1. \<forall>x\<in>set (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)). is_leveln_node (Suc n) x \<and> is_measured_node x
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)). is_leveln_node (Suc n) x \<and> is_measured_node x

goal:
No subgoals!
[PROOF STEP]
qed