[STATEMENT]
lemma app3_inv:
  assumes "is_leveln_ftree n t1"
  and "is_leveln_ftree n t2"
  and "is_measured_ftree t1"
  and "is_measured_ftree t2"
  and "\<forall> x\<in>set xs. (is_leveln_node n x \<and> is_measured_node x)"
  shows "is_leveln_ftree n (app3 t1 xs t2) \<and> is_measured_ftree (app3 t1 xs t2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_leveln_ftree n (app3 t1 xs t2) \<and> is_measured_ftree (app3 t1 xs t2)
[PROOF STEP]
proof (insert assms, induct t1 xs t2 arbitrary: n rule: app3.induct)
[PROOF STATE]
proof (state)
goal (7 subgoals):
 1. \<And>xs t n. \<lbrakk>is_leveln_ftree n Empty; is_leveln_ftree n t; is_measured_ftree Empty; is_measured_ftree t; \<forall>x\<in>set xs. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 Empty xs t) \<and> is_measured_ftree (app3 Empty xs t)
 2. \<And>v xs n. \<lbrakk>is_leveln_ftree n (Single v); is_leveln_ftree n Empty; is_measured_ftree (Single v); is_measured_ftree Empty; \<forall>x\<in>set xs. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Single v) xs Empty) \<and> is_measured_ftree (app3 (Single v) xs Empty)
 3. \<And>v va vb vc xs n. \<lbrakk>is_leveln_ftree n (Deep v va vb vc); is_leveln_ftree n Empty; is_measured_ftree (Deep v va vb vc); is_measured_ftree Empty; \<forall>x\<in>set xs. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Deep v va vb vc) xs Empty) \<and> is_measured_ftree (app3 (Deep v va vb vc) xs Empty)
 4. \<And>x xs v n. \<lbrakk>is_leveln_ftree n (Single x); is_leveln_ftree n (Single v); is_measured_ftree (Single x); is_measured_ftree (Single v); \<forall>x\<in>set xs. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Single x) xs (Single v)) \<and> is_measured_ftree (app3 (Single x) xs (Single v))
 5. \<And>x xs v va vb vc n. \<lbrakk>is_leveln_ftree n (Single x); is_leveln_ftree n (Deep v va vb vc); is_measured_ftree (Single x); is_measured_ftree (Deep v va vb vc); \<forall>x\<in>set xs. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Single x) xs (Deep v va vb vc)) \<and> is_measured_ftree (app3 (Single x) xs (Deep v va vb vc))
 6. \<And>v va vb vc xs x n. \<lbrakk>is_leveln_ftree n (Deep v va vb vc); is_leveln_ftree n (Single x); is_measured_ftree (Deep v va vb vc); is_measured_ftree (Single x); \<forall>x\<in>set xs. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Deep v va vb vc) xs (Single x)) \<and> is_measured_ftree (app3 (Deep v va vb vc) xs (Single x))
 7. \<And>uu_ pr1 m1 sf1 ts uv_ pr2 m2 sf2 n. \<lbrakk>\<And>n. \<lbrakk>is_leveln_ftree n m1; is_leveln_ftree n m2; is_measured_ftree m1; is_measured_ftree m2; \<forall>x\<in>set (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)). is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 m1 (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) m2) \<and> is_measured_ftree (app3 m1 (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) m2); is_leveln_ftree n (Deep uu_ pr1 m1 sf1); is_leveln_ftree n (Deep uv_ pr2 m2 sf2); is_measured_ftree (Deep uu_ pr1 m1 sf1); is_measured_ftree (Deep uv_ pr2 m2 sf2); \<forall>x\<in>set ts. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Deep uu_ pr1 m1 sf1) ts (Deep uv_ pr2 m2 sf2)) \<and> is_measured_ftree (app3 (Deep uu_ pr1 m1 sf1) ts (Deep uv_ pr2 m2 sf2))
[PROOF STEP]
case (1 xs t n)
[PROOF STATE]
proof (state)
this:
is_leveln_ftree n Empty
is_leveln_ftree n t
is_measured_ftree Empty
is_measured_ftree t
\<forall>x\<in>set xs. is_leveln_node n x \<and> is_measured_node x

goal (7 subgoals):
 1. \<And>xs t n. \<lbrakk>is_leveln_ftree n Empty; is_leveln_ftree n t; is_measured_ftree Empty; is_measured_ftree t; \<forall>x\<in>set xs. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 Empty xs t) \<and> is_measured_ftree (app3 Empty xs t)
 2. \<And>v xs n. \<lbrakk>is_leveln_ftree n (Single v); is_leveln_ftree n Empty; is_measured_ftree (Single v); is_measured_ftree Empty; \<forall>x\<in>set xs. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Single v) xs Empty) \<and> is_measured_ftree (app3 (Single v) xs Empty)
 3. \<And>v va vb vc xs n. \<lbrakk>is_leveln_ftree n (Deep v va vb vc); is_leveln_ftree n Empty; is_measured_ftree (Deep v va vb vc); is_measured_ftree Empty; \<forall>x\<in>set xs. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Deep v va vb vc) xs Empty) \<and> is_measured_ftree (app3 (Deep v va vb vc) xs Empty)
 4. \<And>x xs v n. \<lbrakk>is_leveln_ftree n (Single x); is_leveln_ftree n (Single v); is_measured_ftree (Single x); is_measured_ftree (Single v); \<forall>x\<in>set xs. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Single x) xs (Single v)) \<and> is_measured_ftree (app3 (Single x) xs (Single v))
 5. \<And>x xs v va vb vc n. \<lbrakk>is_leveln_ftree n (Single x); is_leveln_ftree n (Deep v va vb vc); is_measured_ftree (Single x); is_measured_ftree (Deep v va vb vc); \<forall>x\<in>set xs. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Single x) xs (Deep v va vb vc)) \<and> is_measured_ftree (app3 (Single x) xs (Deep v va vb vc))
 6. \<And>v va vb vc xs x n. \<lbrakk>is_leveln_ftree n (Deep v va vb vc); is_leveln_ftree n (Single x); is_measured_ftree (Deep v va vb vc); is_measured_ftree (Single x); \<forall>x\<in>set xs. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Deep v va vb vc) xs (Single x)) \<and> is_measured_ftree (app3 (Deep v va vb vc) xs (Single x))
 7. \<And>uu_ pr1 m1 sf1 ts uv_ pr2 m2 sf2 n. \<lbrakk>\<And>n. \<lbrakk>is_leveln_ftree n m1; is_leveln_ftree n m2; is_measured_ftree m1; is_measured_ftree m2; \<forall>x\<in>set (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)). is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 m1 (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) m2) \<and> is_measured_ftree (app3 m1 (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) m2); is_leveln_ftree n (Deep uu_ pr1 m1 sf1); is_leveln_ftree n (Deep uv_ pr2 m2 sf2); is_measured_ftree (Deep uu_ pr1 m1 sf1); is_measured_ftree (Deep uv_ pr2 m2 sf2); \<forall>x\<in>set ts. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Deep uu_ pr1 m1 sf1) ts (Deep uv_ pr2 m2 sf2)) \<and> is_measured_ftree (app3 (Deep uu_ pr1 m1 sf1) ts (Deep uv_ pr2 m2 sf2))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
is_leveln_ftree n Empty
is_leveln_ftree n t
is_measured_ftree Empty
is_measured_ftree t
\<forall>x\<in>set xs. is_leveln_node n x \<and> is_measured_node x

goal (1 subgoal):
 1. is_leveln_ftree n (app3 Empty xs t) \<and> is_measured_ftree (app3 Empty xs t)
[PROOF STEP]
using lconsNlist_inv
[PROOF STATE]
proof (prove)
using this:
is_leveln_ftree n Empty
is_leveln_ftree n t
is_measured_ftree Empty
is_measured_ftree t
\<forall>x\<in>set xs. is_leveln_node n x \<and> is_measured_node x
\<lbrakk>is_leveln_ftree ?n ?t; is_measured_ftree ?t; \<forall>x\<in>set ?xs. is_leveln_node ?n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree ?n (lconsNlist ?xs ?t) \<and> is_measured_ftree (lconsNlist ?xs ?t)

goal (1 subgoal):
 1. is_leveln_ftree n (app3 Empty xs t) \<and> is_measured_ftree (app3 Empty xs t)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
is_leveln_ftree n (app3 Empty xs t) \<and> is_measured_ftree (app3 Empty xs t)

goal (6 subgoals):
 1. \<And>v xs n. \<lbrakk>is_leveln_ftree n (Single v); is_leveln_ftree n Empty; is_measured_ftree (Single v); is_measured_ftree Empty; \<forall>x\<in>set xs. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Single v) xs Empty) \<and> is_measured_ftree (app3 (Single v) xs Empty)
 2. \<And>v va vb vc xs n. \<lbrakk>is_leveln_ftree n (Deep v va vb vc); is_leveln_ftree n Empty; is_measured_ftree (Deep v va vb vc); is_measured_ftree Empty; \<forall>x\<in>set xs. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Deep v va vb vc) xs Empty) \<and> is_measured_ftree (app3 (Deep v va vb vc) xs Empty)
 3. \<And>x xs v n. \<lbrakk>is_leveln_ftree n (Single x); is_leveln_ftree n (Single v); is_measured_ftree (Single x); is_measured_ftree (Single v); \<forall>x\<in>set xs. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Single x) xs (Single v)) \<and> is_measured_ftree (app3 (Single x) xs (Single v))
 4. \<And>x xs v va vb vc n. \<lbrakk>is_leveln_ftree n (Single x); is_leveln_ftree n (Deep v va vb vc); is_measured_ftree (Single x); is_measured_ftree (Deep v va vb vc); \<forall>x\<in>set xs. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Single x) xs (Deep v va vb vc)) \<and> is_measured_ftree (app3 (Single x) xs (Deep v va vb vc))
 5. \<And>v va vb vc xs x n. \<lbrakk>is_leveln_ftree n (Deep v va vb vc); is_leveln_ftree n (Single x); is_measured_ftree (Deep v va vb vc); is_measured_ftree (Single x); \<forall>x\<in>set xs. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Deep v va vb vc) xs (Single x)) \<and> is_measured_ftree (app3 (Deep v va vb vc) xs (Single x))
 6. \<And>uu_ pr1 m1 sf1 ts uv_ pr2 m2 sf2 n. \<lbrakk>\<And>n. \<lbrakk>is_leveln_ftree n m1; is_leveln_ftree n m2; is_measured_ftree m1; is_measured_ftree m2; \<forall>x\<in>set (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)). is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 m1 (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) m2) \<and> is_measured_ftree (app3 m1 (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) m2); is_leveln_ftree n (Deep uu_ pr1 m1 sf1); is_leveln_ftree n (Deep uv_ pr2 m2 sf2); is_measured_ftree (Deep uu_ pr1 m1 sf1); is_measured_ftree (Deep uv_ pr2 m2 sf2); \<forall>x\<in>set ts. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Deep uu_ pr1 m1 sf1) ts (Deep uv_ pr2 m2 sf2)) \<and> is_measured_ftree (app3 (Deep uu_ pr1 m1 sf1) ts (Deep uv_ pr2 m2 sf2))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (6 subgoals):
 1. \<And>v xs n. \<lbrakk>is_leveln_ftree n (Single v); is_leveln_ftree n Empty; is_measured_ftree (Single v); is_measured_ftree Empty; \<forall>x\<in>set xs. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Single v) xs Empty) \<and> is_measured_ftree (app3 (Single v) xs Empty)
 2. \<And>v va vb vc xs n. \<lbrakk>is_leveln_ftree n (Deep v va vb vc); is_leveln_ftree n Empty; is_measured_ftree (Deep v va vb vc); is_measured_ftree Empty; \<forall>x\<in>set xs. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Deep v va vb vc) xs Empty) \<and> is_measured_ftree (app3 (Deep v va vb vc) xs Empty)
 3. \<And>x xs v n. \<lbrakk>is_leveln_ftree n (Single x); is_leveln_ftree n (Single v); is_measured_ftree (Single x); is_measured_ftree (Single v); \<forall>x\<in>set xs. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Single x) xs (Single v)) \<and> is_measured_ftree (app3 (Single x) xs (Single v))
 4. \<And>x xs v va vb vc n. \<lbrakk>is_leveln_ftree n (Single x); is_leveln_ftree n (Deep v va vb vc); is_measured_ftree (Single x); is_measured_ftree (Deep v va vb vc); \<forall>x\<in>set xs. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Single x) xs (Deep v va vb vc)) \<and> is_measured_ftree (app3 (Single x) xs (Deep v va vb vc))
 5. \<And>v va vb vc xs x n. \<lbrakk>is_leveln_ftree n (Deep v va vb vc); is_leveln_ftree n (Single x); is_measured_ftree (Deep v va vb vc); is_measured_ftree (Single x); \<forall>x\<in>set xs. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Deep v va vb vc) xs (Single x)) \<and> is_measured_ftree (app3 (Deep v va vb vc) xs (Single x))
 6. \<And>uu_ pr1 m1 sf1 ts uv_ pr2 m2 sf2 n. \<lbrakk>\<And>n. \<lbrakk>is_leveln_ftree n m1; is_leveln_ftree n m2; is_measured_ftree m1; is_measured_ftree m2; \<forall>x\<in>set (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)). is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 m1 (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) m2) \<and> is_measured_ftree (app3 m1 (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) m2); is_leveln_ftree n (Deep uu_ pr1 m1 sf1); is_leveln_ftree n (Deep uv_ pr2 m2 sf2); is_measured_ftree (Deep uu_ pr1 m1 sf1); is_measured_ftree (Deep uv_ pr2 m2 sf2); \<forall>x\<in>set ts. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Deep uu_ pr1 m1 sf1) ts (Deep uv_ pr2 m2 sf2)) \<and> is_measured_ftree (app3 (Deep uu_ pr1 m1 sf1) ts (Deep uv_ pr2 m2 sf2))
[PROOF STEP]
case "2_1"
[PROOF STATE]
proof (state)
this:
is_leveln_ftree n (Single v_)
is_leveln_ftree n Empty
is_measured_ftree (Single v_)
is_measured_ftree Empty
\<forall>x\<in>set xs_. is_leveln_node n x \<and> is_measured_node x

goal (6 subgoals):
 1. \<And>v xs n. \<lbrakk>is_leveln_ftree n (Single v); is_leveln_ftree n Empty; is_measured_ftree (Single v); is_measured_ftree Empty; \<forall>x\<in>set xs. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Single v) xs Empty) \<and> is_measured_ftree (app3 (Single v) xs Empty)
 2. \<And>v va vb vc xs n. \<lbrakk>is_leveln_ftree n (Deep v va vb vc); is_leveln_ftree n Empty; is_measured_ftree (Deep v va vb vc); is_measured_ftree Empty; \<forall>x\<in>set xs. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Deep v va vb vc) xs Empty) \<and> is_measured_ftree (app3 (Deep v va vb vc) xs Empty)
 3. \<And>x xs v n. \<lbrakk>is_leveln_ftree n (Single x); is_leveln_ftree n (Single v); is_measured_ftree (Single x); is_measured_ftree (Single v); \<forall>x\<in>set xs. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Single x) xs (Single v)) \<and> is_measured_ftree (app3 (Single x) xs (Single v))
 4. \<And>x xs v va vb vc n. \<lbrakk>is_leveln_ftree n (Single x); is_leveln_ftree n (Deep v va vb vc); is_measured_ftree (Single x); is_measured_ftree (Deep v va vb vc); \<forall>x\<in>set xs. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Single x) xs (Deep v va vb vc)) \<and> is_measured_ftree (app3 (Single x) xs (Deep v va vb vc))
 5. \<And>v va vb vc xs x n. \<lbrakk>is_leveln_ftree n (Deep v va vb vc); is_leveln_ftree n (Single x); is_measured_ftree (Deep v va vb vc); is_measured_ftree (Single x); \<forall>x\<in>set xs. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Deep v va vb vc) xs (Single x)) \<and> is_measured_ftree (app3 (Deep v va vb vc) xs (Single x))
 6. \<And>uu_ pr1 m1 sf1 ts uv_ pr2 m2 sf2 n. \<lbrakk>\<And>n. \<lbrakk>is_leveln_ftree n m1; is_leveln_ftree n m2; is_measured_ftree m1; is_measured_ftree m2; \<forall>x\<in>set (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)). is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 m1 (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) m2) \<and> is_measured_ftree (app3 m1 (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) m2); is_leveln_ftree n (Deep uu_ pr1 m1 sf1); is_leveln_ftree n (Deep uv_ pr2 m2 sf2); is_measured_ftree (Deep uu_ pr1 m1 sf1); is_measured_ftree (Deep uv_ pr2 m2 sf2); \<forall>x\<in>set ts. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Deep uu_ pr1 m1 sf1) ts (Deep uv_ pr2 m2 sf2)) \<and> is_measured_ftree (app3 (Deep uu_ pr1 m1 sf1) ts (Deep uv_ pr2 m2 sf2))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
is_leveln_ftree n (Single v_)
is_leveln_ftree n Empty
is_measured_ftree (Single v_)
is_measured_ftree Empty
\<forall>x\<in>set xs_. is_leveln_node n x \<and> is_measured_node x

goal (1 subgoal):
 1. is_leveln_ftree n (app3 (Single v_) xs_ Empty) \<and> is_measured_ftree (app3 (Single v_) xs_ Empty)
[PROOF STEP]
by (simp add: rconsNlist_inv)
[PROOF STATE]
proof (state)
this:
is_leveln_ftree n (app3 (Single v_) xs_ Empty) \<and> is_measured_ftree (app3 (Single v_) xs_ Empty)

goal (5 subgoals):
 1. \<And>v va vb vc xs n. \<lbrakk>is_leveln_ftree n (Deep v va vb vc); is_leveln_ftree n Empty; is_measured_ftree (Deep v va vb vc); is_measured_ftree Empty; \<forall>x\<in>set xs. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Deep v va vb vc) xs Empty) \<and> is_measured_ftree (app3 (Deep v va vb vc) xs Empty)
 2. \<And>x xs v n. \<lbrakk>is_leveln_ftree n (Single x); is_leveln_ftree n (Single v); is_measured_ftree (Single x); is_measured_ftree (Single v); \<forall>x\<in>set xs. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Single x) xs (Single v)) \<and> is_measured_ftree (app3 (Single x) xs (Single v))
 3. \<And>x xs v va vb vc n. \<lbrakk>is_leveln_ftree n (Single x); is_leveln_ftree n (Deep v va vb vc); is_measured_ftree (Single x); is_measured_ftree (Deep v va vb vc); \<forall>x\<in>set xs. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Single x) xs (Deep v va vb vc)) \<and> is_measured_ftree (app3 (Single x) xs (Deep v va vb vc))
 4. \<And>v va vb vc xs x n. \<lbrakk>is_leveln_ftree n (Deep v va vb vc); is_leveln_ftree n (Single x); is_measured_ftree (Deep v va vb vc); is_measured_ftree (Single x); \<forall>x\<in>set xs. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Deep v va vb vc) xs (Single x)) \<and> is_measured_ftree (app3 (Deep v va vb vc) xs (Single x))
 5. \<And>uu_ pr1 m1 sf1 ts uv_ pr2 m2 sf2 n. \<lbrakk>\<And>n. \<lbrakk>is_leveln_ftree n m1; is_leveln_ftree n m2; is_measured_ftree m1; is_measured_ftree m2; \<forall>x\<in>set (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)). is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 m1 (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) m2) \<and> is_measured_ftree (app3 m1 (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) m2); is_leveln_ftree n (Deep uu_ pr1 m1 sf1); is_leveln_ftree n (Deep uv_ pr2 m2 sf2); is_measured_ftree (Deep uu_ pr1 m1 sf1); is_measured_ftree (Deep uv_ pr2 m2 sf2); \<forall>x\<in>set ts. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Deep uu_ pr1 m1 sf1) ts (Deep uv_ pr2 m2 sf2)) \<and> is_measured_ftree (app3 (Deep uu_ pr1 m1 sf1) ts (Deep uv_ pr2 m2 sf2))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (5 subgoals):
 1. \<And>v va vb vc xs n. \<lbrakk>is_leveln_ftree n (Deep v va vb vc); is_leveln_ftree n Empty; is_measured_ftree (Deep v va vb vc); is_measured_ftree Empty; \<forall>x\<in>set xs. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Deep v va vb vc) xs Empty) \<and> is_measured_ftree (app3 (Deep v va vb vc) xs Empty)
 2. \<And>x xs v n. \<lbrakk>is_leveln_ftree n (Single x); is_leveln_ftree n (Single v); is_measured_ftree (Single x); is_measured_ftree (Single v); \<forall>x\<in>set xs. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Single x) xs (Single v)) \<and> is_measured_ftree (app3 (Single x) xs (Single v))
 3. \<And>x xs v va vb vc n. \<lbrakk>is_leveln_ftree n (Single x); is_leveln_ftree n (Deep v va vb vc); is_measured_ftree (Single x); is_measured_ftree (Deep v va vb vc); \<forall>x\<in>set xs. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Single x) xs (Deep v va vb vc)) \<and> is_measured_ftree (app3 (Single x) xs (Deep v va vb vc))
 4. \<And>v va vb vc xs x n. \<lbrakk>is_leveln_ftree n (Deep v va vb vc); is_leveln_ftree n (Single x); is_measured_ftree (Deep v va vb vc); is_measured_ftree (Single x); \<forall>x\<in>set xs. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Deep v va vb vc) xs (Single x)) \<and> is_measured_ftree (app3 (Deep v va vb vc) xs (Single x))
 5. \<And>uu_ pr1 m1 sf1 ts uv_ pr2 m2 sf2 n. \<lbrakk>\<And>n. \<lbrakk>is_leveln_ftree n m1; is_leveln_ftree n m2; is_measured_ftree m1; is_measured_ftree m2; \<forall>x\<in>set (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)). is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 m1 (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) m2) \<and> is_measured_ftree (app3 m1 (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) m2); is_leveln_ftree n (Deep uu_ pr1 m1 sf1); is_leveln_ftree n (Deep uv_ pr2 m2 sf2); is_measured_ftree (Deep uu_ pr1 m1 sf1); is_measured_ftree (Deep uv_ pr2 m2 sf2); \<forall>x\<in>set ts. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Deep uu_ pr1 m1 sf1) ts (Deep uv_ pr2 m2 sf2)) \<and> is_measured_ftree (app3 (Deep uu_ pr1 m1 sf1) ts (Deep uv_ pr2 m2 sf2))
[PROOF STEP]
case "2_2"
[PROOF STATE]
proof (state)
this:
is_leveln_ftree n (Deep v_ va_ vb_ vc_)
is_leveln_ftree n Empty
is_measured_ftree (Deep v_ va_ vb_ vc_)
is_measured_ftree Empty
\<forall>x\<in>set xs_. is_leveln_node n x \<and> is_measured_node x

goal (5 subgoals):
 1. \<And>v va vb vc xs n. \<lbrakk>is_leveln_ftree n (Deep v va vb vc); is_leveln_ftree n Empty; is_measured_ftree (Deep v va vb vc); is_measured_ftree Empty; \<forall>x\<in>set xs. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Deep v va vb vc) xs Empty) \<and> is_measured_ftree (app3 (Deep v va vb vc) xs Empty)
 2. \<And>x xs v n. \<lbrakk>is_leveln_ftree n (Single x); is_leveln_ftree n (Single v); is_measured_ftree (Single x); is_measured_ftree (Single v); \<forall>x\<in>set xs. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Single x) xs (Single v)) \<and> is_measured_ftree (app3 (Single x) xs (Single v))
 3. \<And>x xs v va vb vc n. \<lbrakk>is_leveln_ftree n (Single x); is_leveln_ftree n (Deep v va vb vc); is_measured_ftree (Single x); is_measured_ftree (Deep v va vb vc); \<forall>x\<in>set xs. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Single x) xs (Deep v va vb vc)) \<and> is_measured_ftree (app3 (Single x) xs (Deep v va vb vc))
 4. \<And>v va vb vc xs x n. \<lbrakk>is_leveln_ftree n (Deep v va vb vc); is_leveln_ftree n (Single x); is_measured_ftree (Deep v va vb vc); is_measured_ftree (Single x); \<forall>x\<in>set xs. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Deep v va vb vc) xs (Single x)) \<and> is_measured_ftree (app3 (Deep v va vb vc) xs (Single x))
 5. \<And>uu_ pr1 m1 sf1 ts uv_ pr2 m2 sf2 n. \<lbrakk>\<And>n. \<lbrakk>is_leveln_ftree n m1; is_leveln_ftree n m2; is_measured_ftree m1; is_measured_ftree m2; \<forall>x\<in>set (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)). is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 m1 (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) m2) \<and> is_measured_ftree (app3 m1 (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) m2); is_leveln_ftree n (Deep uu_ pr1 m1 sf1); is_leveln_ftree n (Deep uv_ pr2 m2 sf2); is_measured_ftree (Deep uu_ pr1 m1 sf1); is_measured_ftree (Deep uv_ pr2 m2 sf2); \<forall>x\<in>set ts. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Deep uu_ pr1 m1 sf1) ts (Deep uv_ pr2 m2 sf2)) \<and> is_measured_ftree (app3 (Deep uu_ pr1 m1 sf1) ts (Deep uv_ pr2 m2 sf2))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
is_leveln_ftree n (Deep v_ va_ vb_ vc_)
is_leveln_ftree n Empty
is_measured_ftree (Deep v_ va_ vb_ vc_)
is_measured_ftree Empty
\<forall>x\<in>set xs_. is_leveln_node n x \<and> is_measured_node x

goal (1 subgoal):
 1. is_leveln_ftree n (app3 (Deep v_ va_ vb_ vc_) xs_ Empty) \<and> is_measured_ftree (app3 (Deep v_ va_ vb_ vc_) xs_ Empty)
[PROOF STEP]
by (simp add: lconsNlist_inv rconsNlist_inv)
[PROOF STATE]
proof (state)
this:
is_leveln_ftree n (app3 (Deep v_ va_ vb_ vc_) xs_ Empty) \<and> is_measured_ftree (app3 (Deep v_ va_ vb_ vc_) xs_ Empty)

goal (4 subgoals):
 1. \<And>x xs v n. \<lbrakk>is_leveln_ftree n (Single x); is_leveln_ftree n (Single v); is_measured_ftree (Single x); is_measured_ftree (Single v); \<forall>x\<in>set xs. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Single x) xs (Single v)) \<and> is_measured_ftree (app3 (Single x) xs (Single v))
 2. \<And>x xs v va vb vc n. \<lbrakk>is_leveln_ftree n (Single x); is_leveln_ftree n (Deep v va vb vc); is_measured_ftree (Single x); is_measured_ftree (Deep v va vb vc); \<forall>x\<in>set xs. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Single x) xs (Deep v va vb vc)) \<and> is_measured_ftree (app3 (Single x) xs (Deep v va vb vc))
 3. \<And>v va vb vc xs x n. \<lbrakk>is_leveln_ftree n (Deep v va vb vc); is_leveln_ftree n (Single x); is_measured_ftree (Deep v va vb vc); is_measured_ftree (Single x); \<forall>x\<in>set xs. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Deep v va vb vc) xs (Single x)) \<and> is_measured_ftree (app3 (Deep v va vb vc) xs (Single x))
 4. \<And>uu_ pr1 m1 sf1 ts uv_ pr2 m2 sf2 n. \<lbrakk>\<And>n. \<lbrakk>is_leveln_ftree n m1; is_leveln_ftree n m2; is_measured_ftree m1; is_measured_ftree m2; \<forall>x\<in>set (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)). is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 m1 (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) m2) \<and> is_measured_ftree (app3 m1 (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) m2); is_leveln_ftree n (Deep uu_ pr1 m1 sf1); is_leveln_ftree n (Deep uv_ pr2 m2 sf2); is_measured_ftree (Deep uu_ pr1 m1 sf1); is_measured_ftree (Deep uv_ pr2 m2 sf2); \<forall>x\<in>set ts. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Deep uu_ pr1 m1 sf1) ts (Deep uv_ pr2 m2 sf2)) \<and> is_measured_ftree (app3 (Deep uu_ pr1 m1 sf1) ts (Deep uv_ pr2 m2 sf2))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (4 subgoals):
 1. \<And>x xs v n. \<lbrakk>is_leveln_ftree n (Single x); is_leveln_ftree n (Single v); is_measured_ftree (Single x); is_measured_ftree (Single v); \<forall>x\<in>set xs. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Single x) xs (Single v)) \<and> is_measured_ftree (app3 (Single x) xs (Single v))
 2. \<And>x xs v va vb vc n. \<lbrakk>is_leveln_ftree n (Single x); is_leveln_ftree n (Deep v va vb vc); is_measured_ftree (Single x); is_measured_ftree (Deep v va vb vc); \<forall>x\<in>set xs. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Single x) xs (Deep v va vb vc)) \<and> is_measured_ftree (app3 (Single x) xs (Deep v va vb vc))
 3. \<And>v va vb vc xs x n. \<lbrakk>is_leveln_ftree n (Deep v va vb vc); is_leveln_ftree n (Single x); is_measured_ftree (Deep v va vb vc); is_measured_ftree (Single x); \<forall>x\<in>set xs. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Deep v va vb vc) xs (Single x)) \<and> is_measured_ftree (app3 (Deep v va vb vc) xs (Single x))
 4. \<And>uu_ pr1 m1 sf1 ts uv_ pr2 m2 sf2 n. \<lbrakk>\<And>n. \<lbrakk>is_leveln_ftree n m1; is_leveln_ftree n m2; is_measured_ftree m1; is_measured_ftree m2; \<forall>x\<in>set (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)). is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 m1 (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) m2) \<and> is_measured_ftree (app3 m1 (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) m2); is_leveln_ftree n (Deep uu_ pr1 m1 sf1); is_leveln_ftree n (Deep uv_ pr2 m2 sf2); is_measured_ftree (Deep uu_ pr1 m1 sf1); is_measured_ftree (Deep uv_ pr2 m2 sf2); \<forall>x\<in>set ts. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Deep uu_ pr1 m1 sf1) ts (Deep uv_ pr2 m2 sf2)) \<and> is_measured_ftree (app3 (Deep uu_ pr1 m1 sf1) ts (Deep uv_ pr2 m2 sf2))
[PROOF STEP]
case "3_1"
[PROOF STATE]
proof (state)
this:
is_leveln_ftree n (Single x_)
is_leveln_ftree n (Single v_)
is_measured_ftree (Single x_)
is_measured_ftree (Single v_)
\<forall>x\<in>set xs_. is_leveln_node n x \<and> is_measured_node x

goal (4 subgoals):
 1. \<And>x xs v n. \<lbrakk>is_leveln_ftree n (Single x); is_leveln_ftree n (Single v); is_measured_ftree (Single x); is_measured_ftree (Single v); \<forall>x\<in>set xs. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Single x) xs (Single v)) \<and> is_measured_ftree (app3 (Single x) xs (Single v))
 2. \<And>x xs v va vb vc n. \<lbrakk>is_leveln_ftree n (Single x); is_leveln_ftree n (Deep v va vb vc); is_measured_ftree (Single x); is_measured_ftree (Deep v va vb vc); \<forall>x\<in>set xs. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Single x) xs (Deep v va vb vc)) \<and> is_measured_ftree (app3 (Single x) xs (Deep v va vb vc))
 3. \<And>v va vb vc xs x n. \<lbrakk>is_leveln_ftree n (Deep v va vb vc); is_leveln_ftree n (Single x); is_measured_ftree (Deep v va vb vc); is_measured_ftree (Single x); \<forall>x\<in>set xs. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Deep v va vb vc) xs (Single x)) \<and> is_measured_ftree (app3 (Deep v va vb vc) xs (Single x))
 4. \<And>uu_ pr1 m1 sf1 ts uv_ pr2 m2 sf2 n. \<lbrakk>\<And>n. \<lbrakk>is_leveln_ftree n m1; is_leveln_ftree n m2; is_measured_ftree m1; is_measured_ftree m2; \<forall>x\<in>set (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)). is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 m1 (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) m2) \<and> is_measured_ftree (app3 m1 (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) m2); is_leveln_ftree n (Deep uu_ pr1 m1 sf1); is_leveln_ftree n (Deep uv_ pr2 m2 sf2); is_measured_ftree (Deep uu_ pr1 m1 sf1); is_measured_ftree (Deep uv_ pr2 m2 sf2); \<forall>x\<in>set ts. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Deep uu_ pr1 m1 sf1) ts (Deep uv_ pr2 m2 sf2)) \<and> is_measured_ftree (app3 (Deep uu_ pr1 m1 sf1) ts (Deep uv_ pr2 m2 sf2))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
is_leveln_ftree n (Single x_)
is_leveln_ftree n (Single v_)
is_measured_ftree (Single x_)
is_measured_ftree (Single v_)
\<forall>x\<in>set xs_. is_leveln_node n x \<and> is_measured_node x

goal (1 subgoal):
 1. is_leveln_ftree n (app3 (Single x_) xs_ (Single v_)) \<and> is_measured_ftree (app3 (Single x_) xs_ (Single v_))
[PROOF STEP]
by (simp add: lconsNlist_inv nlcons_invlevel nlcons_invmeas )
[PROOF STATE]
proof (state)
this:
is_leveln_ftree n (app3 (Single x_) xs_ (Single v_)) \<and> is_measured_ftree (app3 (Single x_) xs_ (Single v_))

goal (3 subgoals):
 1. \<And>x xs v va vb vc n. \<lbrakk>is_leveln_ftree n (Single x); is_leveln_ftree n (Deep v va vb vc); is_measured_ftree (Single x); is_measured_ftree (Deep v va vb vc); \<forall>x\<in>set xs. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Single x) xs (Deep v va vb vc)) \<and> is_measured_ftree (app3 (Single x) xs (Deep v va vb vc))
 2. \<And>v va vb vc xs x n. \<lbrakk>is_leveln_ftree n (Deep v va vb vc); is_leveln_ftree n (Single x); is_measured_ftree (Deep v va vb vc); is_measured_ftree (Single x); \<forall>x\<in>set xs. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Deep v va vb vc) xs (Single x)) \<and> is_measured_ftree (app3 (Deep v va vb vc) xs (Single x))
 3. \<And>uu_ pr1 m1 sf1 ts uv_ pr2 m2 sf2 n. \<lbrakk>\<And>n. \<lbrakk>is_leveln_ftree n m1; is_leveln_ftree n m2; is_measured_ftree m1; is_measured_ftree m2; \<forall>x\<in>set (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)). is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 m1 (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) m2) \<and> is_measured_ftree (app3 m1 (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) m2); is_leveln_ftree n (Deep uu_ pr1 m1 sf1); is_leveln_ftree n (Deep uv_ pr2 m2 sf2); is_measured_ftree (Deep uu_ pr1 m1 sf1); is_measured_ftree (Deep uv_ pr2 m2 sf2); \<forall>x\<in>set ts. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Deep uu_ pr1 m1 sf1) ts (Deep uv_ pr2 m2 sf2)) \<and> is_measured_ftree (app3 (Deep uu_ pr1 m1 sf1) ts (Deep uv_ pr2 m2 sf2))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>x xs v va vb vc n. \<lbrakk>is_leveln_ftree n (Single x); is_leveln_ftree n (Deep v va vb vc); is_measured_ftree (Single x); is_measured_ftree (Deep v va vb vc); \<forall>x\<in>set xs. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Single x) xs (Deep v va vb vc)) \<and> is_measured_ftree (app3 (Single x) xs (Deep v va vb vc))
 2. \<And>v va vb vc xs x n. \<lbrakk>is_leveln_ftree n (Deep v va vb vc); is_leveln_ftree n (Single x); is_measured_ftree (Deep v va vb vc); is_measured_ftree (Single x); \<forall>x\<in>set xs. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Deep v va vb vc) xs (Single x)) \<and> is_measured_ftree (app3 (Deep v va vb vc) xs (Single x))
 3. \<And>uu_ pr1 m1 sf1 ts uv_ pr2 m2 sf2 n. \<lbrakk>\<And>n. \<lbrakk>is_leveln_ftree n m1; is_leveln_ftree n m2; is_measured_ftree m1; is_measured_ftree m2; \<forall>x\<in>set (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)). is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 m1 (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) m2) \<and> is_measured_ftree (app3 m1 (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) m2); is_leveln_ftree n (Deep uu_ pr1 m1 sf1); is_leveln_ftree n (Deep uv_ pr2 m2 sf2); is_measured_ftree (Deep uu_ pr1 m1 sf1); is_measured_ftree (Deep uv_ pr2 m2 sf2); \<forall>x\<in>set ts. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Deep uu_ pr1 m1 sf1) ts (Deep uv_ pr2 m2 sf2)) \<and> is_measured_ftree (app3 (Deep uu_ pr1 m1 sf1) ts (Deep uv_ pr2 m2 sf2))
[PROOF STEP]
case "3_2"
[PROOF STATE]
proof (state)
this:
is_leveln_ftree n (Single x_)
is_leveln_ftree n (Deep v_ va_ vb_ vc_)
is_measured_ftree (Single x_)
is_measured_ftree (Deep v_ va_ vb_ vc_)
\<forall>x\<in>set xs_. is_leveln_node n x \<and> is_measured_node x

goal (3 subgoals):
 1. \<And>x xs v va vb vc n. \<lbrakk>is_leveln_ftree n (Single x); is_leveln_ftree n (Deep v va vb vc); is_measured_ftree (Single x); is_measured_ftree (Deep v va vb vc); \<forall>x\<in>set xs. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Single x) xs (Deep v va vb vc)) \<and> is_measured_ftree (app3 (Single x) xs (Deep v va vb vc))
 2. \<And>v va vb vc xs x n. \<lbrakk>is_leveln_ftree n (Deep v va vb vc); is_leveln_ftree n (Single x); is_measured_ftree (Deep v va vb vc); is_measured_ftree (Single x); \<forall>x\<in>set xs. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Deep v va vb vc) xs (Single x)) \<and> is_measured_ftree (app3 (Deep v va vb vc) xs (Single x))
 3. \<And>uu_ pr1 m1 sf1 ts uv_ pr2 m2 sf2 n. \<lbrakk>\<And>n. \<lbrakk>is_leveln_ftree n m1; is_leveln_ftree n m2; is_measured_ftree m1; is_measured_ftree m2; \<forall>x\<in>set (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)). is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 m1 (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) m2) \<and> is_measured_ftree (app3 m1 (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) m2); is_leveln_ftree n (Deep uu_ pr1 m1 sf1); is_leveln_ftree n (Deep uv_ pr2 m2 sf2); is_measured_ftree (Deep uu_ pr1 m1 sf1); is_measured_ftree (Deep uv_ pr2 m2 sf2); \<forall>x\<in>set ts. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Deep uu_ pr1 m1 sf1) ts (Deep uv_ pr2 m2 sf2)) \<and> is_measured_ftree (app3 (Deep uu_ pr1 m1 sf1) ts (Deep uv_ pr2 m2 sf2))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
is_leveln_ftree n (Single x_)
is_leveln_ftree n (Deep v_ va_ vb_ vc_)
is_measured_ftree (Single x_)
is_measured_ftree (Deep v_ va_ vb_ vc_)
\<forall>x\<in>set xs_. is_leveln_node n x \<and> is_measured_node x

goal (1 subgoal):
 1. is_leveln_ftree n (app3 (Single x_) xs_ (Deep v_ va_ vb_ vc_)) \<and> is_measured_ftree (app3 (Single x_) xs_ (Deep v_ va_ vb_ vc_))
[PROOF STEP]
by (simp only: app3.simps)
       (simp add: lconsNlist_inv nlcons_invlevel nlcons_invmeas)
[PROOF STATE]
proof (state)
this:
is_leveln_ftree n (app3 (Single x_) xs_ (Deep v_ va_ vb_ vc_)) \<and> is_measured_ftree (app3 (Single x_) xs_ (Deep v_ va_ vb_ vc_))

goal (2 subgoals):
 1. \<And>v va vb vc xs x n. \<lbrakk>is_leveln_ftree n (Deep v va vb vc); is_leveln_ftree n (Single x); is_measured_ftree (Deep v va vb vc); is_measured_ftree (Single x); \<forall>x\<in>set xs. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Deep v va vb vc) xs (Single x)) \<and> is_measured_ftree (app3 (Deep v va vb vc) xs (Single x))
 2. \<And>uu_ pr1 m1 sf1 ts uv_ pr2 m2 sf2 n. \<lbrakk>\<And>n. \<lbrakk>is_leveln_ftree n m1; is_leveln_ftree n m2; is_measured_ftree m1; is_measured_ftree m2; \<forall>x\<in>set (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)). is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 m1 (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) m2) \<and> is_measured_ftree (app3 m1 (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) m2); is_leveln_ftree n (Deep uu_ pr1 m1 sf1); is_leveln_ftree n (Deep uv_ pr2 m2 sf2); is_measured_ftree (Deep uu_ pr1 m1 sf1); is_measured_ftree (Deep uv_ pr2 m2 sf2); \<forall>x\<in>set ts. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Deep uu_ pr1 m1 sf1) ts (Deep uv_ pr2 m2 sf2)) \<and> is_measured_ftree (app3 (Deep uu_ pr1 m1 sf1) ts (Deep uv_ pr2 m2 sf2))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>v va vb vc xs x n. \<lbrakk>is_leveln_ftree n (Deep v va vb vc); is_leveln_ftree n (Single x); is_measured_ftree (Deep v va vb vc); is_measured_ftree (Single x); \<forall>x\<in>set xs. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Deep v va vb vc) xs (Single x)) \<and> is_measured_ftree (app3 (Deep v va vb vc) xs (Single x))
 2. \<And>uu_ pr1 m1 sf1 ts uv_ pr2 m2 sf2 n. \<lbrakk>\<And>n. \<lbrakk>is_leveln_ftree n m1; is_leveln_ftree n m2; is_measured_ftree m1; is_measured_ftree m2; \<forall>x\<in>set (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)). is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 m1 (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) m2) \<and> is_measured_ftree (app3 m1 (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) m2); is_leveln_ftree n (Deep uu_ pr1 m1 sf1); is_leveln_ftree n (Deep uv_ pr2 m2 sf2); is_measured_ftree (Deep uu_ pr1 m1 sf1); is_measured_ftree (Deep uv_ pr2 m2 sf2); \<forall>x\<in>set ts. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Deep uu_ pr1 m1 sf1) ts (Deep uv_ pr2 m2 sf2)) \<and> is_measured_ftree (app3 (Deep uu_ pr1 m1 sf1) ts (Deep uv_ pr2 m2 sf2))
[PROOF STEP]
case 4
[PROOF STATE]
proof (state)
this:
is_leveln_ftree n (Deep v_ va_ vb_ vc_)
is_leveln_ftree n (Single x_)
is_measured_ftree (Deep v_ va_ vb_ vc_)
is_measured_ftree (Single x_)
\<forall>x\<in>set xs_. is_leveln_node n x \<and> is_measured_node x

goal (2 subgoals):
 1. \<And>v va vb vc xs x n. \<lbrakk>is_leveln_ftree n (Deep v va vb vc); is_leveln_ftree n (Single x); is_measured_ftree (Deep v va vb vc); is_measured_ftree (Single x); \<forall>x\<in>set xs. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Deep v va vb vc) xs (Single x)) \<and> is_measured_ftree (app3 (Deep v va vb vc) xs (Single x))
 2. \<And>uu_ pr1 m1 sf1 ts uv_ pr2 m2 sf2 n. \<lbrakk>\<And>n. \<lbrakk>is_leveln_ftree n m1; is_leveln_ftree n m2; is_measured_ftree m1; is_measured_ftree m2; \<forall>x\<in>set (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)). is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 m1 (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) m2) \<and> is_measured_ftree (app3 m1 (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) m2); is_leveln_ftree n (Deep uu_ pr1 m1 sf1); is_leveln_ftree n (Deep uv_ pr2 m2 sf2); is_measured_ftree (Deep uu_ pr1 m1 sf1); is_measured_ftree (Deep uv_ pr2 m2 sf2); \<forall>x\<in>set ts. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Deep uu_ pr1 m1 sf1) ts (Deep uv_ pr2 m2 sf2)) \<and> is_measured_ftree (app3 (Deep uu_ pr1 m1 sf1) ts (Deep uv_ pr2 m2 sf2))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
is_leveln_ftree n (Deep v_ va_ vb_ vc_)
is_leveln_ftree n (Single x_)
is_measured_ftree (Deep v_ va_ vb_ vc_)
is_measured_ftree (Single x_)
\<forall>x\<in>set xs_. is_leveln_node n x \<and> is_measured_node x

goal (1 subgoal):
 1. is_leveln_ftree n (app3 (Deep v_ va_ vb_ vc_) xs_ (Single x_)) \<and> is_measured_ftree (app3 (Deep v_ va_ vb_ vc_) xs_ (Single x_))
[PROOF STEP]
by (simp only: app3.simps)
       (simp add: rconsNlist_inv nrcons_invlevel nrcons_invmeas)
[PROOF STATE]
proof (state)
this:
is_leveln_ftree n (app3 (Deep v_ va_ vb_ vc_) xs_ (Single x_)) \<and> is_measured_ftree (app3 (Deep v_ va_ vb_ vc_) xs_ (Single x_))

goal (1 subgoal):
 1. \<And>uu_ pr1 m1 sf1 ts uv_ pr2 m2 sf2 n. \<lbrakk>\<And>n. \<lbrakk>is_leveln_ftree n m1; is_leveln_ftree n m2; is_measured_ftree m1; is_measured_ftree m2; \<forall>x\<in>set (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)). is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 m1 (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) m2) \<and> is_measured_ftree (app3 m1 (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) m2); is_leveln_ftree n (Deep uu_ pr1 m1 sf1); is_leveln_ftree n (Deep uv_ pr2 m2 sf2); is_measured_ftree (Deep uu_ pr1 m1 sf1); is_measured_ftree (Deep uv_ pr2 m2 sf2); \<forall>x\<in>set ts. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Deep uu_ pr1 m1 sf1) ts (Deep uv_ pr2 m2 sf2)) \<and> is_measured_ftree (app3 (Deep uu_ pr1 m1 sf1) ts (Deep uv_ pr2 m2 sf2))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>uu_ pr1 m1 sf1 ts uv_ pr2 m2 sf2 n. \<lbrakk>\<And>n. \<lbrakk>is_leveln_ftree n m1; is_leveln_ftree n m2; is_measured_ftree m1; is_measured_ftree m2; \<forall>x\<in>set (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)). is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 m1 (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) m2) \<and> is_measured_ftree (app3 m1 (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) m2); is_leveln_ftree n (Deep uu_ pr1 m1 sf1); is_leveln_ftree n (Deep uv_ pr2 m2 sf2); is_measured_ftree (Deep uu_ pr1 m1 sf1); is_measured_ftree (Deep uv_ pr2 m2 sf2); \<forall>x\<in>set ts. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Deep uu_ pr1 m1 sf1) ts (Deep uv_ pr2 m2 sf2)) \<and> is_measured_ftree (app3 (Deep uu_ pr1 m1 sf1) ts (Deep uv_ pr2 m2 sf2))
[PROOF STEP]
case (5 uu pr1 m1 sf1 ts uv pr2 m2 sf2 n)
[PROOF STATE]
proof (state)
this:
\<lbrakk>is_leveln_ftree ?n m1; is_leveln_ftree ?n m2; is_measured_ftree m1; is_measured_ftree m2; \<forall>x\<in>set (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)). is_leveln_node ?n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree ?n (app3 m1 (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) m2) \<and> is_measured_ftree (app3 m1 (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) m2)
is_leveln_ftree n (Deep uu pr1 m1 sf1)
is_leveln_ftree n (Deep uv pr2 m2 sf2)
is_measured_ftree (Deep uu pr1 m1 sf1)
is_measured_ftree (Deep uv pr2 m2 sf2)
\<forall>x\<in>set ts. is_leveln_node n x \<and> is_measured_node x

goal (1 subgoal):
 1. \<And>uu_ pr1 m1 sf1 ts uv_ pr2 m2 sf2 n. \<lbrakk>\<And>n. \<lbrakk>is_leveln_ftree n m1; is_leveln_ftree n m2; is_measured_ftree m1; is_measured_ftree m2; \<forall>x\<in>set (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)). is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 m1 (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) m2) \<and> is_measured_ftree (app3 m1 (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) m2); is_leveln_ftree n (Deep uu_ pr1 m1 sf1); is_leveln_ftree n (Deep uv_ pr2 m2 sf2); is_measured_ftree (Deep uu_ pr1 m1 sf1); is_measured_ftree (Deep uv_ pr2 m2 sf2); \<forall>x\<in>set ts. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Deep uu_ pr1 m1 sf1) ts (Deep uv_ pr2 m2 sf2)) \<and> is_measured_ftree (app3 (Deep uu_ pr1 m1 sf1) ts (Deep uv_ pr2 m2 sf2))
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>is_leveln_ftree ?n m1; is_leveln_ftree ?n m2; is_measured_ftree m1; is_measured_ftree m2; \<forall>x\<in>set (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)). is_leveln_node ?n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree ?n (app3 m1 (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) m2) \<and> is_measured_ftree (app3 m1 (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) m2)
is_leveln_ftree n (Deep uu pr1 m1 sf1)
is_leveln_ftree n (Deep uv pr2 m2 sf2)
is_measured_ftree (Deep uu pr1 m1 sf1)
is_measured_ftree (Deep uv pr2 m2 sf2)
\<forall>x\<in>set ts. is_leveln_node n x \<and> is_measured_node x

goal (1 subgoal):
 1. is_leveln_ftree n (app3 (Deep uu pr1 m1 sf1) ts (Deep uv pr2 m2 sf2)) \<and> is_measured_ftree (app3 (Deep uu pr1 m1 sf1) ts (Deep uv pr2 m2 sf2))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>n. \<lbrakk>is_leveln_ftree n m1; is_leveln_ftree n m2; is_measured_ftree m1; is_measured_ftree m2; \<forall>x\<in>set (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)). is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 m1 (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) m2) \<and> is_measured_ftree (app3 m1 (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) m2); is_leveln_ftree n (Deep uu pr1 m1 sf1); is_leveln_ftree n (Deep uv pr2 m2 sf2); is_measured_ftree (Deep uu pr1 m1 sf1); is_measured_ftree (Deep uv pr2 m2 sf2); \<forall>x\<in>set ts. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Deep uu pr1 m1 sf1) ts (Deep uv pr2 m2 sf2)) \<and> is_measured_ftree (app3 (Deep uu pr1 m1 sf1) ts (Deep uv pr2 m2 sf2))
[PROOF STEP]
have v1: "is_leveln_ftree (Suc n) m1"
      and v2: "is_leveln_ftree (Suc n) m2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_leveln_ftree (Suc n) m1 &&& is_leveln_ftree (Suc n) m2
[PROOF STEP]
using "5.prems"
[PROOF STATE]
proof (prove)
using this:
is_leveln_ftree n (Deep uu pr1 m1 sf1)
is_leveln_ftree n (Deep uv pr2 m2 sf2)
is_measured_ftree (Deep uu pr1 m1 sf1)
is_measured_ftree (Deep uv pr2 m2 sf2)
\<forall>x\<in>set ts. is_leveln_node n x \<and> is_measured_node x

goal (1 subgoal):
 1. is_leveln_ftree (Suc n) m1 &&& is_leveln_ftree (Suc n) m2
[PROOF STEP]
by (simp_all add: is_leveln_ftree_def)
[PROOF STATE]
proof (state)
this:
is_leveln_ftree (Suc n) m1
is_leveln_ftree (Suc n) m2

goal (1 subgoal):
 1. \<lbrakk>\<And>n. \<lbrakk>is_leveln_ftree n m1; is_leveln_ftree n m2; is_measured_ftree m1; is_measured_ftree m2; \<forall>x\<in>set (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)). is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 m1 (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) m2) \<and> is_measured_ftree (app3 m1 (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) m2); is_leveln_ftree n (Deep uu pr1 m1 sf1); is_leveln_ftree n (Deep uv pr2 m2 sf2); is_measured_ftree (Deep uu pr1 m1 sf1); is_measured_ftree (Deep uv pr2 m2 sf2); \<forall>x\<in>set ts. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Deep uu pr1 m1 sf1) ts (Deep uv pr2 m2 sf2)) \<and> is_measured_ftree (app3 (Deep uu pr1 m1 sf1) ts (Deep uv pr2 m2 sf2))
[PROOF STEP]
have v3: "is_measured_ftree m1"
      and v4: "is_measured_ftree m2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_measured_ftree m1 &&& is_measured_ftree m2
[PROOF STEP]
using "5.prems"
[PROOF STATE]
proof (prove)
using this:
is_leveln_ftree n (Deep uu pr1 m1 sf1)
is_leveln_ftree n (Deep uv pr2 m2 sf2)
is_measured_ftree (Deep uu pr1 m1 sf1)
is_measured_ftree (Deep uv pr2 m2 sf2)
\<forall>x\<in>set ts. is_leveln_node n x \<and> is_measured_node x

goal (1 subgoal):
 1. is_measured_ftree m1 &&& is_measured_ftree m2
[PROOF STEP]
by (simp_all add: is_measured_ftree_def)
[PROOF STATE]
proof (state)
this:
is_measured_ftree m1
is_measured_ftree m2

goal (1 subgoal):
 1. \<lbrakk>\<And>n. \<lbrakk>is_leveln_ftree n m1; is_leveln_ftree n m2; is_measured_ftree m1; is_measured_ftree m2; \<forall>x\<in>set (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)). is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 m1 (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) m2) \<and> is_measured_ftree (app3 m1 (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) m2); is_leveln_ftree n (Deep uu pr1 m1 sf1); is_leveln_ftree n (Deep uv pr2 m2 sf2); is_measured_ftree (Deep uu pr1 m1 sf1); is_measured_ftree (Deep uv pr2 m2 sf2); \<forall>x\<in>set ts. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Deep uu pr1 m1 sf1) ts (Deep uv pr2 m2 sf2)) \<and> is_measured_ftree (app3 (Deep uu pr1 m1 sf1) ts (Deep uv pr2 m2 sf2))
[PROOF STEP]
have v5: "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"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (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
[PROOF STEP]
using "5.prems"
[PROOF STATE]
proof (prove)
using this:
is_leveln_ftree n (Deep uu pr1 m1 sf1)
is_leveln_ftree n (Deep uv pr2 m2 sf2)
is_measured_ftree (Deep uu pr1 m1 sf1)
is_measured_ftree (Deep uv pr2 m2 sf2)
\<forall>x\<in>set ts. is_leveln_node n x \<and> is_measured_node x

goal (1 subgoal):
 1. (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
[PROOF STEP]
by (simp_all add: is_leveln_ftree_def is_measured_ftree_def)
[PROOF STATE]
proof (state)
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. \<lbrakk>\<And>n. \<lbrakk>is_leveln_ftree n m1; is_leveln_ftree n m2; is_measured_ftree m1; is_measured_ftree m2; \<forall>x\<in>set (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)). is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 m1 (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) m2) \<and> is_measured_ftree (app3 m1 (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) m2); is_leveln_ftree n (Deep uu pr1 m1 sf1); is_leveln_ftree n (Deep uv pr2 m2 sf2); is_measured_ftree (Deep uu pr1 m1 sf1); is_measured_ftree (Deep uv pr2 m2 sf2); \<forall>x\<in>set ts. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Deep uu pr1 m1 sf1) ts (Deep uv pr2 m2 sf2)) \<and> is_measured_ftree (app3 (Deep uu pr1 m1 sf1) ts (Deep uv pr2 m2 sf2))
[PROOF STEP]
note v6 = nodes_inv2[OF v5]
[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 (1 subgoal):
 1. \<lbrakk>\<And>n. \<lbrakk>is_leveln_ftree n m1; is_leveln_ftree n m2; is_measured_ftree m1; is_measured_ftree m2; \<forall>x\<in>set (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)). is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 m1 (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) m2) \<and> is_measured_ftree (app3 m1 (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) m2); is_leveln_ftree n (Deep uu pr1 m1 sf1); is_leveln_ftree n (Deep uv pr2 m2 sf2); is_measured_ftree (Deep uu pr1 m1 sf1); is_measured_ftree (Deep uv pr2 m2 sf2); \<forall>x\<in>set ts. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Deep uu pr1 m1 sf1) ts (Deep uv pr2 m2 sf2)) \<and> is_measured_ftree (app3 (Deep uu pr1 m1 sf1) ts (Deep uv pr2 m2 sf2))
[PROOF STEP]
note v7 = "5.hyps"[OF v1 v2 v3 v4 v6]
[PROOF STATE]
proof (state)
this:
is_leveln_ftree (Suc n) (app3 m1 (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) m2) \<and> is_measured_ftree (app3 m1 (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) m2)

goal (1 subgoal):
 1. \<lbrakk>\<And>n. \<lbrakk>is_leveln_ftree n m1; is_leveln_ftree n m2; is_measured_ftree m1; is_measured_ftree m2; \<forall>x\<in>set (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)). is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 m1 (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) m2) \<and> is_measured_ftree (app3 m1 (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) m2); is_leveln_ftree n (Deep uu pr1 m1 sf1); is_leveln_ftree n (Deep uv pr2 m2 sf2); is_measured_ftree (Deep uu pr1 m1 sf1); is_measured_ftree (Deep uv pr2 m2 sf2); \<forall>x\<in>set ts. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Deep uu pr1 m1 sf1) ts (Deep uv pr2 m2 sf2)) \<and> is_measured_ftree (app3 (Deep uu pr1 m1 sf1) ts (Deep uv pr2 m2 sf2))
[PROOF STEP]
have v8: "is_leveln_digit n sf2"
      "is_measured_digit sf2"
      "is_leveln_digit n pr1"
      "is_measured_digit pr1"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (is_leveln_digit n sf2 &&& is_measured_digit sf2) &&& is_leveln_digit n pr1 &&& is_measured_digit pr1
[PROOF STEP]
using "5.prems"
[PROOF STATE]
proof (prove)
using this:
is_leveln_ftree n (Deep uu pr1 m1 sf1)
is_leveln_ftree n (Deep uv pr2 m2 sf2)
is_measured_ftree (Deep uu pr1 m1 sf1)
is_measured_ftree (Deep uv pr2 m2 sf2)
\<forall>x\<in>set ts. is_leveln_node n x \<and> is_measured_node x

goal (1 subgoal):
 1. (is_leveln_digit n sf2 &&& is_measured_digit sf2) &&& is_leveln_digit n pr1 &&& is_measured_digit pr1
[PROOF STEP]
by (simp_all add: is_leveln_ftree_def is_measured_ftree_def)
[PROOF STATE]
proof (state)
this:
is_leveln_digit n sf2
is_measured_digit sf2
is_leveln_digit n pr1
is_measured_digit pr1

goal (1 subgoal):
 1. \<lbrakk>\<And>n. \<lbrakk>is_leveln_ftree n m1; is_leveln_ftree n m2; is_measured_ftree m1; is_measured_ftree m2; \<forall>x\<in>set (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)). is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 m1 (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) m2) \<and> is_measured_ftree (app3 m1 (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) m2); is_leveln_ftree n (Deep uu pr1 m1 sf1); is_leveln_ftree n (Deep uv pr2 m2 sf2); is_measured_ftree (Deep uu pr1 m1 sf1); is_measured_ftree (Deep uv pr2 m2 sf2); \<forall>x\<in>set ts. is_leveln_node n x \<and> is_measured_node x\<rbrakk> \<Longrightarrow> is_leveln_ftree n (app3 (Deep uu pr1 m1 sf1) ts (Deep uv pr2 m2 sf2)) \<and> is_measured_ftree (app3 (Deep uu pr1 m1 sf1) ts (Deep uv pr2 m2 sf2))
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_leveln_ftree n (app3 (Deep uu pr1 m1 sf1) ts (Deep uv pr2 m2 sf2)) \<and> is_measured_ftree (app3 (Deep uu pr1 m1 sf1) ts (Deep uv pr2 m2 sf2))
[PROOF STEP]
using v7 v8
[PROOF STATE]
proof (prove)
using this:
is_leveln_ftree (Suc n) (app3 m1 (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) m2) \<and> is_measured_ftree (app3 m1 (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) m2)
is_leveln_digit n sf2
is_measured_digit sf2
is_leveln_digit n pr1
is_measured_digit pr1

goal (1 subgoal):
 1. is_leveln_ftree n (app3 (Deep uu pr1 m1 sf1) ts (Deep uv pr2 m2 sf2)) \<and> is_measured_ftree (app3 (Deep uu pr1 m1 sf1) ts (Deep uv pr2 m2 sf2))
[PROOF STEP]
by (simp add: is_leveln_ftree_def is_measured_ftree_def deep_def)
[PROOF STATE]
proof (state)
this:
is_leveln_ftree n (app3 (Deep uu pr1 m1 sf1) ts (Deep uv pr2 m2 sf2)) \<and> is_measured_ftree (app3 (Deep uu pr1 m1 sf1) ts (Deep uv pr2 m2 sf2))

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
is_leveln_ftree n (app3 (Deep uu pr1 m1 sf1) ts (Deep uv pr2 m2 sf2)) \<and> is_measured_ftree (app3 (Deep uu pr1 m1 sf1) ts (Deep uv pr2 m2 sf2))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nodes_list: "length xs \<ge> 2 \<Longrightarrow> nlistToList (nodes xs) = nlistToList xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. 2 \<le> length xs \<Longrightarrow> nlistToList (nodes xs) = nlistToList xs
[PROOF STEP]
by (induct xs rule: nodes.induct) (auto simp add: node2_def node3_def)


[STATEMENT]
lemma nlistToList_app:
  "nlistToList (xs@ys) = (nlistToList xs) @ (nlistToList ys)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nlistToList (xs @ ys) = nlistToList xs @ nlistToList ys
[PROOF STEP]
by (induct xs arbitrary: ys, simp_all)


[STATEMENT]
lemma nlistListLCons: "toList (lconsNlist xs t) = (nlistToList xs) @ (toList t)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. toList (lconsNlist xs t) = nlistToList xs @ toList t
[PROOF STEP]
by (induct xs) (auto simp add: nlcons_list)


[STATEMENT]
lemma nlistListRCons: "toList (rconsNlist t xs) = (toList t) @ (nlistToList xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. toList (rconsNlist t xs) = toList t @ nlistToList xs
[PROOF STEP]
by (induct xs arbitrary: t) (auto simp add: nrcons_list)


[STATEMENT]
lemma app3_list_lem1:
  "nlistToList (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) =
       digitToList sf1 @ nlistToList ts @ digitToList pr2"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nlistToList (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) = digitToList sf1 @ nlistToList ts @ digitToList pr2
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. nlistToList (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) = digitToList sf1 @ nlistToList ts @ digitToList pr2
[PROOF STEP]
have len1: "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]
by (cases sf1,cases pr2,simp_all)
[PROOF STATE]
proof (state)
this:
2 \<le> length (digitToNlist sf1 @ ts @ digitToNlist pr2)

goal (1 subgoal):
 1. nlistToList (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) = digitToList sf1 @ nlistToList ts @ digitToList pr2
[PROOF STEP]
have "(nlistToList (digitToNlist sf1 @ ts @ digitToNlist pr2))
       = (digitToList sf1 @ nlistToList ts @ digitToList pr2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nlistToList (digitToNlist sf1 @ ts @ digitToNlist pr2) = digitToList sf1 @ nlistToList ts @ digitToList pr2
[PROOF STEP]
apply (cases sf1, cases pr2)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>x1 x1a. \<lbrakk>sf1 = One x1; pr2 = One x1a\<rbrakk> \<Longrightarrow> nlistToList (digitToNlist sf1 @ ts @ digitToNlist pr2) = digitToList sf1 @ nlistToList ts @ digitToList pr2
 2. \<And>x1 x21 x22. \<lbrakk>sf1 = One x1; pr2 = Two x21 x22\<rbrakk> \<Longrightarrow> nlistToList (digitToNlist sf1 @ ts @ digitToNlist pr2) = digitToList sf1 @ nlistToList ts @ digitToList pr2
 3. \<And>x1 x31 x32 x33. \<lbrakk>sf1 = One x1; pr2 = Three x31 x32 x33\<rbrakk> \<Longrightarrow> nlistToList (digitToNlist sf1 @ ts @ digitToNlist pr2) = digitToList sf1 @ nlistToList ts @ digitToList pr2
 4. \<And>x1 x41 x42 x43 x44. \<lbrakk>sf1 = One x1; pr2 = Four x41 x42 x43 x44\<rbrakk> \<Longrightarrow> nlistToList (digitToNlist sf1 @ ts @ digitToNlist pr2) = digitToList sf1 @ nlistToList ts @ digitToList pr2
 5. \<And>x21 x22. sf1 = Two x21 x22 \<Longrightarrow> nlistToList (digitToNlist sf1 @ ts @ digitToNlist pr2) = digitToList sf1 @ nlistToList ts @ digitToList pr2
 6. \<And>x31 x32 x33. sf1 = Three x31 x32 x33 \<Longrightarrow> nlistToList (digitToNlist sf1 @ ts @ digitToNlist pr2) = digitToList sf1 @ nlistToList ts @ digitToList pr2
 7. \<And>x41 x42 x43 x44. sf1 = Four x41 x42 x43 x44 \<Longrightarrow> nlistToList (digitToNlist sf1 @ ts @ digitToNlist pr2) = digitToList sf1 @ nlistToList ts @ digitToList pr2
[PROOF STEP]
apply (simp_all add: nlistToList_app)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x21 x22. sf1 = Two x21 x22 \<Longrightarrow> nlistToList (digitToNlist pr2) = digitToList pr2
 2. \<And>x31 x32 x33. sf1 = Three x31 x32 x33 \<Longrightarrow> nlistToList (digitToNlist pr2) = digitToList pr2
 3. \<And>x41 x42 x43 x44. sf1 = Four x41 x42 x43 x44 \<Longrightarrow> nlistToList (digitToNlist pr2) = digitToList pr2
[PROOF STEP]
apply (cases pr2, auto)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x31 x32 x33. sf1 = Three x31 x32 x33 \<Longrightarrow> nlistToList (digitToNlist pr2) = digitToList pr2
 2. \<And>x41 x42 x43 x44. sf1 = Four x41 x42 x43 x44 \<Longrightarrow> nlistToList (digitToNlist pr2) = digitToList pr2
[PROOF STEP]
apply (cases pr2, auto)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x41 x42 x43 x44. sf1 = Four x41 x42 x43 x44 \<Longrightarrow> nlistToList (digitToNlist pr2) = digitToList pr2
[PROOF STEP]
apply (cases pr2, auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
nlistToList (digitToNlist sf1 @ ts @ digitToNlist pr2) = digitToList sf1 @ nlistToList ts @ digitToList pr2

goal (1 subgoal):
 1. nlistToList (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) = digitToList sf1 @ nlistToList ts @ digitToList pr2
[PROOF STEP]
with nodes_list[OF len1]
[PROOF STATE]
proof (chain)
picking this:
nlistToList (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) = nlistToList (digitToNlist sf1 @ ts @ digitToNlist pr2)
nlistToList (digitToNlist sf1 @ ts @ digitToNlist pr2) = digitToList sf1 @ nlistToList ts @ digitToList pr2
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
nlistToList (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) = nlistToList (digitToNlist sf1 @ ts @ digitToNlist pr2)
nlistToList (digitToNlist sf1 @ ts @ digitToNlist pr2) = digitToList sf1 @ nlistToList ts @ digitToList pr2

goal (1 subgoal):
 1. nlistToList (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) = digitToList sf1 @ nlistToList ts @ digitToList pr2
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
nlistToList (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) = digitToList sf1 @ nlistToList ts @ digitToList pr2

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma app3_list:
  "toList (app3 t1 xs t2) = (toList t1) @ (nlistToList xs) @ (toList t2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. toList (app3 t1 xs t2) = toList t1 @ nlistToList xs @ toList t2
[PROOF STEP]
apply (induct t1 xs t2 rule: app3.induct)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<And>xs t. toList (app3 Empty xs t) = toList Empty @ nlistToList xs @ toList t
 2. \<And>v xs. toList (app3 (Single v) xs Empty) = toList (Single v) @ nlistToList xs @ toList Empty
 3. \<And>v va vb vc xs. toList (app3 (Deep v va vb vc) xs Empty) = toList (Deep v va vb vc) @ nlistToList xs @ toList Empty
 4. \<And>x xs v. toList (app3 (Single x) xs (Single v)) = toList (Single x) @ nlistToList xs @ toList (Single v)
 5. \<And>x xs v va vb vc. toList (app3 (Single x) xs (Deep v va vb vc)) = toList (Single x) @ nlistToList xs @ toList (Deep v va vb vc)
 6. \<And>v va vb vc xs x. toList (app3 (Deep v va vb vc) xs (Single x)) = toList (Deep v va vb vc) @ nlistToList xs @ toList (Single x)
 7. \<And>uu_ pr1 m1 sf1 ts uv_ pr2 m2 sf2. toList (app3 m1 (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) m2) = toList m1 @ nlistToList (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) @ toList m2 \<Longrightarrow> toList (app3 (Deep uu_ pr1 m1 sf1) ts (Deep uv_ pr2 m2 sf2)) = toList (Deep uu_ pr1 m1 sf1) @ nlistToList ts @ toList (Deep uv_ pr2 m2 sf2)
[PROOF STEP]
apply (simp_all add: nlistListLCons nlistListRCons nlcons_list nrcons_list)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>pr1 m1 sf1 ts pr2 m2 sf2. toList (app3 m1 (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) m2) = toList m1 @ nlistToList (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) @ toList m2 \<Longrightarrow> toList (deep pr1 (app3 m1 (nodes (digitToNlist sf1 @ ts @ digitToNlist pr2)) m2) sf2) = digitToList pr1 @ toList m1 @ digitToList sf1 @ nlistToList ts @ digitToList pr2 @ toList m2 @ digitToList sf2
[PROOF STEP]
apply (simp add: app3_list_lem1 deep_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma app_correct:
  assumes "ft_invar t1" "ft_invar t2"
  shows "toList (app t1 t2) = (toList t1) @ (toList t2)"
    and "ft_invar (app t1 t2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. toList (app t1 t2) = toList t1 @ toList t2 &&& ft_invar (app t1 t2)
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
ft_invar t1
ft_invar t2

goal (1 subgoal):
 1. toList (app t1 t2) = toList t1 @ toList t2 &&& ft_invar (app t1 t2)
[PROOF STEP]
by (auto simp add: app3_inv app3_list ft_invar_def app_def)


[STATEMENT]
lemma app_inv: "\<lbrakk>ft_invar t1;ft_invar t2\<rbrakk> \<Longrightarrow> ft_invar (app t1 t2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>ft_invar t1; ft_invar t2\<rbrakk> \<Longrightarrow> ft_invar (app t1 t2)
[PROOF STEP]
by (auto simp add: app3_inv ft_invar_def app_def)


[STATEMENT]
lemma app_list[simp]: "toList (app t1 t2) = (toList t1) @ (toList t2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. toList (app t1 t2) = toList t1 @ toList t2
[PROOF STEP]
by (simp add: app3_list app_def)


[STATEMENT]
lemma nlistToTree_inv:
  "\<forall> x \<in> set nl. is_measured_node x \<Longrightarrow> is_measured_ftree (nlistToTree nl)"
  "\<forall> x \<in> set nl. is_leveln_node n x \<Longrightarrow> is_leveln_ftree n (nlistToTree nl)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<forall>x\<in>set nl. is_measured_node x \<Longrightarrow> is_measured_ftree (nlistToTree nl)) &&& (\<forall>x\<in>set nl. is_leveln_node n x \<Longrightarrow> is_leveln_ftree n (nlistToTree nl))
[PROOF STEP]
by (unfold nlistToTree_def, induct nl, auto simp add: nlcons_invmeas)
     (induct nl, auto simp add: nlcons_invlevel)


[STATEMENT]
lemma nlistToTree_list: "toList (nlistToTree nl) = nlistToList nl"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. toList (nlistToTree nl) = nlistToList nl
[PROOF STEP]
by (auto simp add: nlistToTree_def nlistListLCons)


[STATEMENT]
lemma deepL_inv:
  assumes "is_leveln_ftree (Suc n) m \<and> is_measured_ftree m"
  and "is_leveln_digit n sf \<and> is_measured_digit sf"
  and "\<forall> x \<in> set pr. (is_measured_node x \<and> is_leveln_node n x) \<and> length pr \<le> 4"
  shows  "is_leveln_ftree n (deepL pr m sf) \<and> is_measured_ftree (deepL pr m sf)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. is_leveln_ftree n (deepL pr m sf) \<and> is_measured_ftree (deepL pr m sf)
[PROOF STEP]
apply (insert assms)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_leveln_ftree (Suc n) m \<and> is_measured_ftree m; is_leveln_digit n sf \<and> is_measured_digit sf; \<forall>x\<in>set pr. (is_measured_node x \<and> is_leveln_node n x) \<and> length pr \<le> 4\<rbrakk> \<Longrightarrow> is_leveln_ftree n (deepL pr m sf) \<and> is_measured_ftree (deepL pr m sf)
[PROOF STEP]
apply (induct "pr" m sf rule: deepL.induct)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m sf. \<lbrakk>is_leveln_ftree (Suc n) m \<and> is_measured_ftree m; is_leveln_digit n sf \<and> is_measured_digit sf; \<forall>x\<in>set []. (is_measured_node x \<and> is_leveln_node n x) \<and> length [] \<le> 4\<rbrakk> \<Longrightarrow> is_leveln_ftree n (deepL [] m sf) \<and> is_measured_ftree (deepL [] m sf)
 2. \<And>v va m sf. \<lbrakk>is_leveln_ftree (Suc n) m \<and> is_measured_ftree m; is_leveln_digit n sf \<and> is_measured_digit sf; \<forall>x\<in>set (v # va). (is_measured_node x \<and> is_leveln_node n x) \<and> length (v # va) \<le> 4\<rbrakk> \<Longrightarrow> is_leveln_ftree n (deepL (v # va) m sf) \<and> is_measured_ftree (deepL (v # va) m sf)
[PROOF STEP]
apply (simp split: viewnres_split)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>m sf. \<lbrakk>is_leveln_ftree (Suc n) m \<and> is_measured_ftree m; is_leveln_digit n sf \<and> is_measured_digit sf\<rbrakk> \<Longrightarrow> (viewLn m = None \<longrightarrow> is_leveln_ftree n (digitToTree sf) \<and> is_measured_ftree (digitToTree sf)) \<and> (\<forall>a b. viewLn m = Some (a, b) \<longrightarrow> is_leveln_ftree n (deep (nodeToDigit a) b sf) \<and> is_measured_ftree (deep (nodeToDigit a) b sf))
 2. \<And>v va m sf. \<lbrakk>is_leveln_ftree (Suc n) m \<and> is_measured_ftree m; is_leveln_digit n sf \<and> is_measured_digit sf; \<forall>x\<in>set (v # va). (is_measured_node x \<and> is_leveln_node n x) \<and> length (v # va) \<le> 4\<rbrakk> \<Longrightarrow> is_leveln_ftree n (deepL (v # va) m sf) \<and> is_measured_ftree (deepL (v # va) m sf)
[PROOF STEP]
apply auto[1]
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>m sf. \<lbrakk>is_leveln_ftree (Suc n) m; is_measured_ftree m; is_leveln_digit n sf; is_measured_digit sf; viewLn m = None\<rbrakk> \<Longrightarrow> is_leveln_ftree n (digitToTree sf)
 2. \<And>m sf. \<lbrakk>is_leveln_ftree (Suc n) m; is_measured_ftree m; is_leveln_digit n sf; is_measured_digit sf; viewLn m = None\<rbrakk> \<Longrightarrow> is_measured_ftree (digitToTree sf)
 3. \<And>m sf a b. \<lbrakk>is_leveln_ftree (Suc n) m; is_measured_ftree m; is_leveln_digit n sf; is_measured_digit sf; viewLn m = Some (a, b)\<rbrakk> \<Longrightarrow> is_leveln_ftree n (deep (nodeToDigit a) b sf)
 4. \<And>m sf a b. \<lbrakk>is_leveln_ftree (Suc n) m; is_measured_ftree m; is_leveln_digit n sf; is_measured_digit sf; viewLn m = Some (a, b)\<rbrakk> \<Longrightarrow> is_measured_ftree (deep (nodeToDigit a) b sf)
 5. \<And>v va m sf. \<lbrakk>is_leveln_ftree (Suc n) m \<and> is_measured_ftree m; is_leveln_digit n sf \<and> is_measured_digit sf; \<forall>x\<in>set (v # va). (is_measured_node x \<and> is_leveln_node n x) \<and> length (v # va) \<le> 4\<rbrakk> \<Longrightarrow> is_leveln_ftree n (deepL (v # va) m sf) \<and> is_measured_ftree (deepL (v # va) m sf)
[PROOF STEP]
apply (simp_all add: digitToTree_inv deep_def)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>m sf a b. \<lbrakk>is_leveln_ftree (Suc n) m; is_measured_ftree m; is_leveln_digit n sf; is_measured_digit sf; viewLn m = Some (a, b)\<rbrakk> \<Longrightarrow> is_leveln_digit n (nodeToDigit a) \<and> is_leveln_ftree (Suc n) b
 2. \<And>m sf a b. \<lbrakk>is_leveln_ftree (Suc n) m; is_measured_ftree m; is_leveln_digit n sf; is_measured_digit sf; viewLn m = Some (a, b)\<rbrakk> \<Longrightarrow> is_measured_digit (nodeToDigit a) \<and> is_measured_ftree b
 3. \<And>v va m sf. \<lbrakk>is_leveln_ftree (Suc n) m \<and> is_measured_ftree m; is_leveln_digit n sf \<and> is_measured_digit sf; is_measured_node v \<and> is_leveln_node n v \<and> length va \<le> 3 \<and> (\<forall>x\<in>set va. is_measured_node x \<and> is_leveln_node n x \<and> length va \<le> 3)\<rbrakk> \<Longrightarrow> is_leveln_digit n (nlistToDigit (v # va)) \<and> is_measured_digit (nlistToDigit (v # va))
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>m sf a b. \<lbrakk>is_leveln_ftree (Suc n) m; is_measured_ftree m; is_leveln_digit n sf; is_measured_digit sf; viewLn m = Some (a, b)\<rbrakk> \<Longrightarrow> is_leveln_digit n (nodeToDigit a) \<and> is_leveln_ftree (Suc n) b
 2. \<And>m sf a b. \<lbrakk>is_leveln_ftree (Suc n) m; is_measured_ftree m; is_leveln_digit n sf; is_measured_digit sf; viewLn m = Some (a, b)\<rbrakk> \<Longrightarrow> is_measured_digit (nodeToDigit a) \<and> is_measured_ftree b
 3. \<And>v va m sf. \<lbrakk>is_leveln_ftree (Suc n) m \<and> is_measured_ftree m; is_leveln_digit n sf \<and> is_measured_digit sf; is_measured_node v \<and> is_leveln_node n v \<and> length va \<le> 3 \<and> (\<forall>x\<in>set va. is_measured_node x \<and> is_leveln_node n x \<and> length va \<le> 3)\<rbrakk> \<Longrightarrow> is_leveln_digit n (nlistToDigit (v # va)) \<and> is_measured_digit (nlistToDigit (v # va))
[PROOF STEP]
fix m sf Node FingerTreeStruc
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>m sf a b. \<lbrakk>is_leveln_ftree (Suc n) m; is_measured_ftree m; is_leveln_digit n sf; is_measured_digit sf; viewLn m = Some (a, b)\<rbrakk> \<Longrightarrow> is_leveln_digit n (nodeToDigit a) \<and> is_leveln_ftree (Suc n) b
 2. \<And>m sf a b. \<lbrakk>is_leveln_ftree (Suc n) m; is_measured_ftree m; is_leveln_digit n sf; is_measured_digit sf; viewLn m = Some (a, b)\<rbrakk> \<Longrightarrow> is_measured_digit (nodeToDigit a) \<and> is_measured_ftree b
 3. \<And>v va m sf. \<lbrakk>is_leveln_ftree (Suc n) m \<and> is_measured_ftree m; is_leveln_digit n sf \<and> is_measured_digit sf; is_measured_node v \<and> is_leveln_node n v \<and> length va \<le> 3 \<and> (\<forall>x\<in>set va. is_measured_node x \<and> is_leveln_node n x \<and> length va \<le> 3)\<rbrakk> \<Longrightarrow> is_leveln_digit n (nlistToDigit (v # va)) \<and> is_measured_digit (nlistToDigit (v # va))
[PROOF STEP]
assume "is_leveln_ftree (Suc n) m" "is_measured_ftree m"
         "is_leveln_digit n sf" "is_measured_digit sf"
         "viewLn m = Some (Node, FingerTreeStruc)"
[PROOF STATE]
proof (state)
this:
is_leveln_ftree (Suc n) m
is_measured_ftree m
is_leveln_digit n sf
is_measured_digit sf
viewLn m = Some (Node, FingerTreeStruc)

goal (3 subgoals):
 1. \<And>m sf a b. \<lbrakk>is_leveln_ftree (Suc n) m; is_measured_ftree m; is_leveln_digit n sf; is_measured_digit sf; viewLn m = Some (a, b)\<rbrakk> \<Longrightarrow> is_leveln_digit n (nodeToDigit a) \<and> is_leveln_ftree (Suc n) b
 2. \<And>m sf a b. \<lbrakk>is_leveln_ftree (Suc n) m; is_measured_ftree m; is_leveln_digit n sf; is_measured_digit sf; viewLn m = Some (a, b)\<rbrakk> \<Longrightarrow> is_measured_digit (nodeToDigit a) \<and> is_measured_ftree b
 3. \<And>v va m sf. \<lbrakk>is_leveln_ftree (Suc n) m \<and> is_measured_ftree m; is_leveln_digit n sf \<and> is_measured_digit sf; is_measured_node v \<and> is_leveln_node n v \<and> length va \<le> 3 \<and> (\<forall>x\<in>set va. is_measured_node x \<and> is_leveln_node n x \<and> length va \<le> 3)\<rbrakk> \<Longrightarrow> is_leveln_digit n (nlistToDigit (v # va)) \<and> is_measured_digit (nlistToDigit (v # va))
[PROOF STEP]
thus "is_leveln_digit n (nodeToDigit Node)
        \<and> is_leveln_ftree (Suc n) FingerTreeStruc"
[PROOF STATE]
proof (prove)
using this:
is_leveln_ftree (Suc n) m
is_measured_ftree m
is_leveln_digit n sf
is_measured_digit sf
viewLn m = Some (Node, FingerTreeStruc)

goal (1 subgoal):
 1. is_leveln_digit n (nodeToDigit Node) \<and> is_leveln_ftree (Suc n) FingerTreeStruc
[PROOF STEP]
by (simp add: viewLn_inv[of m "Suc n" Node FingerTreeStruc] nodeToDigit_inv)
[PROOF STATE]
proof (state)
this:
is_leveln_digit n (nodeToDigit Node) \<and> is_leveln_ftree (Suc n) FingerTreeStruc

goal (2 subgoals):
 1. \<And>m sf a b. \<lbrakk>is_leveln_ftree (Suc n) m; is_measured_ftree m; is_leveln_digit n sf; is_measured_digit sf; viewLn m = Some (a, b)\<rbrakk> \<Longrightarrow> is_measured_digit (nodeToDigit a) \<and> is_measured_ftree b
 2. \<And>v va m sf. \<lbrakk>is_leveln_ftree (Suc n) m \<and> is_measured_ftree m; is_leveln_digit n sf \<and> is_measured_digit sf; is_measured_node v \<and> is_leveln_node n v \<and> length va \<le> 3 \<and> (\<forall>x\<in>set va. is_measured_node x \<and> is_leveln_node n x \<and> length va \<le> 3)\<rbrakk> \<Longrightarrow> is_leveln_digit n (nlistToDigit (v # va)) \<and> is_measured_digit (nlistToDigit (v # va))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>m sf a b. \<lbrakk>is_leveln_ftree (Suc n) m; is_measured_ftree m; is_leveln_digit n sf; is_measured_digit sf; viewLn m = Some (a, b)\<rbrakk> \<Longrightarrow> is_measured_digit (nodeToDigit a) \<and> is_measured_ftree b
 2. \<And>v va m sf. \<lbrakk>is_leveln_ftree (Suc n) m \<and> is_measured_ftree m; is_leveln_digit n sf \<and> is_measured_digit sf; is_measured_node v \<and> is_leveln_node n v \<and> length va \<le> 3 \<and> (\<forall>x\<in>set va. is_measured_node x \<and> is_leveln_node n x \<and> length va \<le> 3)\<rbrakk> \<Longrightarrow> is_leveln_digit n (nlistToDigit (v # va)) \<and> is_measured_digit (nlistToDigit (v # va))
[PROOF STEP]
fix m sf Node FingerTreeStruc
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>m sf a b. \<lbrakk>is_leveln_ftree (Suc n) m; is_measured_ftree m; is_leveln_digit n sf; is_measured_digit sf; viewLn m = Some (a, b)\<rbrakk> \<Longrightarrow> is_measured_digit (nodeToDigit a) \<and> is_measured_ftree b
 2. \<And>v va m sf. \<lbrakk>is_leveln_ftree (Suc n) m \<and> is_measured_ftree m; is_leveln_digit n sf \<and> is_measured_digit sf; is_measured_node v \<and> is_leveln_node n v \<and> length va \<le> 3 \<and> (\<forall>x\<in>set va. is_measured_node x \<and> is_leveln_node n x \<and> length va \<le> 3)\<rbrakk> \<Longrightarrow> is_leveln_digit n (nlistToDigit (v # va)) \<and> is_measured_digit (nlistToDigit (v # va))
[PROOF STEP]
assume assms1:
    "is_leveln_ftree (Suc n) m" "is_measured_ftree m"
    "is_leveln_digit n sf" "is_measured_digit sf"
    "viewLn m = Some (Node, FingerTreeStruc)"
[PROOF STATE]
proof (state)
this:
is_leveln_ftree (Suc n) m
is_measured_ftree m
is_leveln_digit n sf
is_measured_digit sf
viewLn m = Some (Node, FingerTreeStruc)

goal (2 subgoals):
 1. \<And>m sf a b. \<lbrakk>is_leveln_ftree (Suc n) m; is_measured_ftree m; is_leveln_digit n sf; is_measured_digit sf; viewLn m = Some (a, b)\<rbrakk> \<Longrightarrow> is_measured_digit (nodeToDigit a) \<and> is_measured_ftree b
 2. \<And>v va m sf. \<lbrakk>is_leveln_ftree (Suc n) m \<and> is_measured_ftree m; is_leveln_digit n sf \<and> is_measured_digit sf; is_measured_node v \<and> is_leveln_node n v \<and> length va \<le> 3 \<and> (\<forall>x\<in>set va. is_measured_node x \<and> is_leveln_node n x \<and> length va \<le> 3)\<rbrakk> \<Longrightarrow> is_leveln_digit n (nlistToDigit (v # va)) \<and> is_measured_digit (nlistToDigit (v # va))
[PROOF STEP]
thus "is_measured_digit (nodeToDigit Node) \<and> is_measured_ftree FingerTreeStruc"
[PROOF STATE]
proof (prove)
using this:
is_leveln_ftree (Suc n) m
is_measured_ftree m
is_leveln_digit n sf
is_measured_digit sf
viewLn m = Some (Node, FingerTreeStruc)

goal (1 subgoal):
 1. is_measured_digit (nodeToDigit Node) \<and> is_measured_ftree FingerTreeStruc
[PROOF STEP]
apply (auto simp only: viewLn_inv[of m "Suc n" Node FingerTreeStruc])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_leveln_ftree (Suc n) m; is_measured_ftree m; is_leveln_digit n sf; is_measured_digit sf; viewLn m = Some (Node, FingerTreeStruc)\<rbrakk> \<Longrightarrow> is_measured_digit (nodeToDigit Node)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>is_leveln_ftree (Suc n) m; is_measured_ftree m; is_leveln_digit n sf; is_measured_digit sf; viewLn m = Some (Node, FingerTreeStruc)\<rbrakk> \<Longrightarrow> is_measured_digit (nodeToDigit Node)
[PROOF STEP]
from assms1
[PROOF STATE]
proof (chain)
picking this:
is_leveln_ftree (Suc n) m
is_measured_ftree m
is_leveln_digit n sf
is_measured_digit sf
viewLn m = Some (Node, FingerTreeStruc)
[PROOF STEP]
have "is_measured_node Node \<and> is_leveln_node (Suc n) Node"
[PROOF STATE]
proof (prove)
using this:
is_leveln_ftree (Suc n) m
is_measured_ftree m
is_leveln_digit n sf
is_measured_digit sf
viewLn m = Some (Node, FingerTreeStruc)

goal (1 subgoal):
 1. is_measured_node Node \<and> is_leveln_node (Suc n) Node
[PROOF STEP]
by (simp add: viewLn_inv[of m "Suc n" Node FingerTreeStruc])
[PROOF STATE]
proof (state)
this:
is_measured_node Node \<and> is_leveln_node (Suc n) Node

goal (1 subgoal):
 1. \<lbrakk>is_leveln_ftree (Suc n) m; is_measured_ftree m; is_leveln_digit n sf; is_measured_digit sf; viewLn m = Some (Node, FingerTreeStruc)\<rbrakk> \<Longrightarrow> is_measured_digit (nodeToDigit Node)
[PROOF STEP]
thus "is_measured_digit (nodeToDigit Node)"
[PROOF STATE]
proof (prove)
using this:
is_measured_node Node \<and> is_leveln_node (Suc n) Node

goal (1 subgoal):
 1. is_measured_digit (nodeToDigit Node)
[PROOF STEP]
by (auto simp add: nodeToDigit_inv)
[PROOF STATE]
proof (state)
this:
is_measured_digit (nodeToDigit Node)

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
is_measured_digit (nodeToDigit Node) \<and> is_measured_ftree FingerTreeStruc

goal (1 subgoal):
 1. \<And>v va m sf. \<lbrakk>is_leveln_ftree (Suc n) m \<and> is_measured_ftree m; is_leveln_digit n sf \<and> is_measured_digit sf; is_measured_node v \<and> is_leveln_node n v \<and> length va \<le> 3 \<and> (\<forall>x\<in>set va. is_measured_node x \<and> is_leveln_node n x \<and> length va \<le> 3)\<rbrakk> \<Longrightarrow> is_leveln_digit n (nlistToDigit (v # va)) \<and> is_measured_digit (nlistToDigit (v # va))
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>v va m sf. \<lbrakk>is_leveln_ftree (Suc n) m \<and> is_measured_ftree m; is_leveln_digit n sf \<and> is_measured_digit sf; is_measured_node v \<and> is_leveln_node n v \<and> length va \<le> 3 \<and> (\<forall>x\<in>set va. is_measured_node x \<and> is_leveln_node n x \<and> length va \<le> 3)\<rbrakk> \<Longrightarrow> is_leveln_digit n (nlistToDigit (v # va)) \<and> is_measured_digit (nlistToDigit (v # va))
[PROOF STEP]
fix v va
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>v va m sf. \<lbrakk>is_leveln_ftree (Suc n) m \<and> is_measured_ftree m; is_leveln_digit n sf \<and> is_measured_digit sf; is_measured_node v \<and> is_leveln_node n v \<and> length va \<le> 3 \<and> (\<forall>x\<in>set va. is_measured_node x \<and> is_leveln_node n x \<and> length va \<le> 3)\<rbrakk> \<Longrightarrow> is_leveln_digit n (nlistToDigit (v # va)) \<and> is_measured_digit (nlistToDigit (v # va))
[PROOF STEP]
assume
    "is_measured_node v \<and> is_leveln_node n (v:: ('a,'b) Node) \<and>
    length  (va::('a, 'b) Node list) \<le> 3 \<and>
    (\<forall>x\<in>set va. is_measured_node x \<and> is_leveln_node n x \<and> length va \<le> 3)"
[PROOF STATE]
proof (state)
this:
is_measured_node v \<and> is_leveln_node n v \<and> length va \<le> 3 \<and> (\<forall>x\<in>set va. is_measured_node x \<and> is_leveln_node n x \<and> length va \<le> 3)

goal (1 subgoal):
 1. \<And>v va m sf. \<lbrakk>is_leveln_ftree (Suc n) m \<and> is_measured_ftree m; is_leveln_digit n sf \<and> is_measured_digit sf; is_measured_node v \<and> is_leveln_node n v \<and> length va \<le> 3 \<and> (\<forall>x\<in>set va. is_measured_node x \<and> is_leveln_node n x \<and> length va \<le> 3)\<rbrakk> \<Longrightarrow> is_leveln_digit n (nlistToDigit (v # va)) \<and> is_measured_digit (nlistToDigit (v # va))
[PROOF STEP]
thus "is_leveln_digit n (nlistToDigit (v # va))
       \<and> is_measured_digit (nlistToDigit (v # va))"
[PROOF STATE]
proof (prove)
using this:
is_measured_node v \<and> is_leveln_node n v \<and> length va \<le> 3 \<and> (\<forall>x\<in>set va. is_measured_node x \<and> is_leveln_node n x \<and> length va \<le> 3)

goal (1 subgoal):
 1. is_leveln_digit n (nlistToDigit (v # va)) \<and> is_measured_digit (nlistToDigit (v # va))
[PROOF STEP]
by(cases "v#va" rule: nlistToDigit.cases,simp_all)
[PROOF STATE]
proof (state)
this:
is_leveln_digit n (nlistToDigit (v # va)) \<and> is_measured_digit (nlistToDigit (v # va))

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma nlistToDigit_list:
  assumes "1 \<le> length xs \<and> length xs \<le> 4"
  shows "digitToList(nlistToDigit xs) = nlistToList xs"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. digitToList (nlistToDigit xs) = nlistToList xs
[PROOF STEP]
by (insert assms, cases xs rule: nlistToDigit.cases,auto)


[STATEMENT]
lemma deepL_list:
  assumes "is_leveln_ftree (Suc n) m \<and> is_measured_ftree m"
  and "is_leveln_digit n sf \<and> is_measured_digit sf"
  and "\<forall> x \<in> set pr. (is_measured_node x \<and> is_leveln_node n x) \<and> length pr \<le> 4"
  shows "toList (deepL pr m sf) = nlistToList pr @ toList m @ digitToList sf"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. toList (deepL pr m sf) = nlistToList pr @ toList m @ digitToList sf
[PROOF STEP]
proof (insert assms, induct "pr" m sf rule: deepL.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>m sf. \<lbrakk>is_leveln_ftree (Suc n) m \<and> is_measured_ftree m; is_leveln_digit n sf \<and> is_measured_digit sf; \<forall>x\<in>set []. (is_measured_node x \<and> is_leveln_node n x) \<and> length [] \<le> 4\<rbrakk> \<Longrightarrow> toList (deepL [] m sf) = nlistToList [] @ toList m @ digitToList sf
 2. \<And>v va m sf. \<lbrakk>is_leveln_ftree (Suc n) m \<and> is_measured_ftree m; is_leveln_digit n sf \<and> is_measured_digit sf; \<forall>x\<in>set (v # va). (is_measured_node x \<and> is_leveln_node n x) \<and> length (v # va) \<le> 4\<rbrakk> \<Longrightarrow> toList (deepL (v # va) m sf) = nlistToList (v # va) @ toList m @ digitToList sf
[PROOF STEP]
case (1 m sf)
[PROOF STATE]
proof (state)
this:
is_leveln_ftree (Suc n) m \<and> is_measured_ftree m
is_leveln_digit n sf \<and> is_measured_digit sf
\<forall>x\<in>set []. (is_measured_node x \<and> is_leveln_node n x) \<and> length [] \<le> 4

goal (2 subgoals):
 1. \<And>m sf. \<lbrakk>is_leveln_ftree (Suc n) m \<and> is_measured_ftree m; is_leveln_digit n sf \<and> is_measured_digit sf; \<forall>x\<in>set []. (is_measured_node x \<and> is_leveln_node n x) \<and> length [] \<le> 4\<rbrakk> \<Longrightarrow> toList (deepL [] m sf) = nlistToList [] @ toList m @ digitToList sf
 2. \<And>v va m sf. \<lbrakk>is_leveln_ftree (Suc n) m \<and> is_measured_ftree m; is_leveln_digit n sf \<and> is_measured_digit sf; \<forall>x\<in>set (v # va). (is_measured_node x \<and> is_leveln_node n x) \<and> length (v # va) \<le> 4\<rbrakk> \<Longrightarrow> toList (deepL (v # va) m sf) = nlistToList (v # va) @ toList m @ digitToList sf
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
is_leveln_ftree (Suc n) m \<and> is_measured_ftree m
is_leveln_digit n sf \<and> is_measured_digit sf
\<forall>x\<in>set []. (is_measured_node x \<and> is_leveln_node n x) \<and> length [] \<le> 4

goal (1 subgoal):
 1. toList (deepL [] m sf) = nlistToList [] @ toList m @ digitToList sf
[PROOF STEP]
proof (auto split: viewnres_split simp add: deep_def)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>is_leveln_ftree (Suc n) m; is_measured_ftree m; is_leveln_digit n sf; is_measured_digit sf; viewLn m = None\<rbrakk> \<Longrightarrow> toList (digitToTree sf) = toList m @ digitToList sf
 2. \<And>a b. \<lbrakk>is_leveln_ftree (Suc n) m; is_measured_ftree m; is_leveln_digit n sf; is_measured_digit sf; viewLn m = Some (a, b)\<rbrakk> \<Longrightarrow> digitToList (nodeToDigit a) @ toList b = toList m
[PROOF STEP]
assume "viewLn m = None"
[PROOF STATE]
proof (state)
this:
viewLn m = None

goal (2 subgoals):
 1. \<lbrakk>is_leveln_ftree (Suc n) m; is_measured_ftree m; is_leveln_digit n sf; is_measured_digit sf; viewLn m = None\<rbrakk> \<Longrightarrow> toList (digitToTree sf) = toList m @ digitToList sf
 2. \<And>a b. \<lbrakk>is_leveln_ftree (Suc n) m; is_measured_ftree m; is_leveln_digit n sf; is_measured_digit sf; viewLn m = Some (a, b)\<rbrakk> \<Longrightarrow> digitToList (nodeToDigit a) @ toList b = toList m
[PROOF STEP]
hence "m = Empty"
[PROOF STATE]
proof (prove)
using this:
viewLn m = None

goal (1 subgoal):
 1. m = Empty
[PROOF STEP]
by (metis viewLn_empty)
[PROOF STATE]
proof (state)
this:
m = Empty

goal (2 subgoals):
 1. \<lbrakk>is_leveln_ftree (Suc n) m; is_measured_ftree m; is_leveln_digit n sf; is_measured_digit sf; viewLn m = None\<rbrakk> \<Longrightarrow> toList (digitToTree sf) = toList m @ digitToList sf
 2. \<And>a b. \<lbrakk>is_leveln_ftree (Suc n) m; is_measured_ftree m; is_leveln_digit n sf; is_measured_digit sf; viewLn m = Some (a, b)\<rbrakk> \<Longrightarrow> digitToList (nodeToDigit a) @ toList b = toList m
[PROOF STEP]
hence "toList m = []"
[PROOF STATE]
proof (prove)
using this:
m = Empty

goal (1 subgoal):
 1. toList m = []
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
toList m = []

goal (2 subgoals):
 1. \<lbrakk>is_leveln_ftree (Suc n) m; is_measured_ftree m; is_leveln_digit n sf; is_measured_digit sf; viewLn m = None\<rbrakk> \<Longrightarrow> toList (digitToTree sf) = toList m @ digitToList sf
 2. \<And>a b. \<lbrakk>is_leveln_ftree (Suc n) m; is_measured_ftree m; is_leveln_digit n sf; is_measured_digit sf; viewLn m = Some (a, b)\<rbrakk> \<Longrightarrow> digitToList (nodeToDigit a) @ toList b = toList m
[PROOF STEP]
thus "toList (digitToTree sf) = toList m @ digitToList sf"
[PROOF STATE]
proof (prove)
using this:
toList m = []

goal (1 subgoal):
 1. toList (digitToTree sf) = toList m @ digitToList sf
[PROOF STEP]
by (simp add:digitToTree_list)
[PROOF STATE]
proof (state)
this:
toList (digitToTree sf) = toList m @ digitToList sf

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>is_leveln_ftree (Suc n) m; is_measured_ftree m; is_leveln_digit n sf; is_measured_digit sf; viewLn m = Some (a, b)\<rbrakk> \<Longrightarrow> digitToList (nodeToDigit a) @ toList b = toList m
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>is_leveln_ftree (Suc n) m; is_measured_ftree m; is_leveln_digit n sf; is_measured_digit sf; viewLn m = Some (a, b)\<rbrakk> \<Longrightarrow> digitToList (nodeToDigit a) @ toList b = toList m
[PROOF STEP]
fix nd t
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>a b. \<lbrakk>is_leveln_ftree (Suc n) m; is_measured_ftree m; is_leveln_digit n sf; is_measured_digit sf; viewLn m = Some (a, b)\<rbrakk> \<Longrightarrow> digitToList (nodeToDigit a) @ toList b = toList m
[PROOF STEP]
assume "viewLn m = Some (nd, t)"
      "is_leveln_ftree (Suc n) m" "is_measured_ftree m"
[PROOF STATE]
proof (state)
this:
viewLn m = Some (nd, t)
is_leveln_ftree (Suc n) m
is_measured_ftree m

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>is_leveln_ftree (Suc n) m; is_measured_ftree m; is_leveln_digit n sf; is_measured_digit sf; viewLn m = Some (a, b)\<rbrakk> \<Longrightarrow> digitToList (nodeToDigit a) @ toList b = toList m
[PROOF STEP]
hence "nodeToList nd @ toList t = toList m"
[PROOF STATE]
proof (prove)
using this:
viewLn m = Some (nd, t)
is_leveln_ftree (Suc n) m
is_measured_ftree m

goal (1 subgoal):
 1. nodeToList nd @ toList t = toList m
[PROOF STEP]
by (metis viewLn_list)
[PROOF STATE]
proof (state)
this:
nodeToList nd @ toList t = toList m

goal (1 subgoal):
 1. \<And>a b. \<lbrakk>is_leveln_ftree (Suc n) m; is_measured_ftree m; is_leveln_digit n sf; is_measured_digit sf; viewLn m = Some (a, b)\<rbrakk> \<Longrightarrow> digitToList (nodeToDigit a) @ toList b = toList m
[PROOF STEP]
thus "digitToList (nodeToDigit nd) @ toList t = toList m"
[PROOF STATE]
proof (prove)
using this:
nodeToList nd @ toList t = toList m

goal (1 subgoal):
 1. digitToList (nodeToDigit nd) @ toList t = toList m
[PROOF STEP]
by (simp add: nodeToDigit_list)
[PROOF STATE]
proof (state)
this:
digitToList (nodeToDigit nd) @ toList t = toList m

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
toList (deepL [] m sf) = nlistToList [] @ toList m @ digitToList sf

goal (1 subgoal):
 1. \<And>v va m sf. \<lbrakk>is_leveln_ftree (Suc n) m \<and> is_measured_ftree m; is_leveln_digit n sf \<and> is_measured_digit sf; \<forall>x\<in>set (v # va). (is_measured_node x \<and> is_leveln_node n x) \<and> length (v # va) \<le> 4\<rbrakk> \<Longrightarrow> toList (deepL (v # va) m sf) = nlistToList (v # va) @ toList m @ digitToList sf
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>v va m sf. \<lbrakk>is_leveln_ftree (Suc n) m \<and> is_measured_ftree m; is_leveln_digit n sf \<and> is_measured_digit sf; \<forall>x\<in>set (v # va). (is_measured_node x \<and> is_leveln_node n x) \<and> length (v # va) \<le> 4\<rbrakk> \<Longrightarrow> toList (deepL (v # va) m sf) = nlistToList (v # va) @ toList m @ digitToList sf
[PROOF STEP]
case (2 v va m sf)
[PROOF STATE]
proof (state)
this:
is_leveln_ftree (Suc n) m \<and> is_measured_ftree m
is_leveln_digit n sf \<and> is_measured_digit sf
\<forall>x\<in>set (v # va). (is_measured_node x \<and> is_leveln_node n x) \<and> length (v # va) \<le> 4

goal (1 subgoal):
 1. \<And>v va m sf. \<lbrakk>is_leveln_ftree (Suc n) m \<and> is_measured_ftree m; is_leveln_digit n sf \<and> is_measured_digit sf; \<forall>x\<in>set (v # va). (is_measured_node x \<and> is_leveln_node n x) \<and> length (v # va) \<le> 4\<rbrakk> \<Longrightarrow> toList (deepL (v # va) m sf) = nlistToList (v # va) @ toList m @ digitToList sf
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
is_leveln_ftree (Suc n) m \<and> is_measured_ftree m
is_leveln_digit n sf \<and> is_measured_digit sf
\<forall>x\<in>set (v # va). (is_measured_node x \<and> is_leveln_node n x) \<and> length (v # va) \<le> 4

goal (1 subgoal):
 1. toList (deepL (v # va) m sf) = nlistToList (v # va) @ toList m @ digitToList sf
[PROOF STEP]
apply (unfold deepL.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_leveln_ftree (Suc n) m \<and> is_measured_ftree m; is_leveln_digit n sf \<and> is_measured_digit sf; \<forall>x\<in>set (v # va). (is_measured_node x \<and> is_leveln_node n x) \<and> length (v # va) \<le> 4\<rbrakk> \<Longrightarrow> toList (deep (nlistToDigit (v # va)) m sf) = nlistToList (v # va) @ toList m @ digitToList sf
[PROOF STEP]
apply (simp add: deep_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_leveln_ftree (Suc n) m \<and> is_measured_ftree m; is_leveln_digit n sf \<and> is_measured_digit sf; is_measured_node v \<and> is_leveln_node n v \<and> length va \<le> 3 \<and> (\<forall>x\<in>set va. is_measured_node x \<and> is_leveln_node n x \<and> length va \<le> 3)\<rbrakk> \<Longrightarrow> digitToList (nlistToDigit (v # va)) = nodeToList v @ nlistToList va
[PROOF STEP]
apply (simp add: nlistToDigit_list)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
toList (deepL (v # va) m sf) = nlistToList (v # va) @ toList m @ digitToList sf

goal:
No subgoals!
[PROOF STEP]
qed