[STATEMENT]
lemma nsplitTree_correct: "\<lbrakk>
  is_leveln_ftree n (s:: ('e,'a::monoid_add) FingerTreeStruc);
  is_measured_ftree s;
  \<And>(a::'a) (b::'a). p a \<Longrightarrow> p (a + b);
  \<not> p i;
  p (i + (gmft s));
  (nsplitTree p i s) = (l, nd, r)\<rbrakk>
  \<Longrightarrow> (toList s) = (toList l) @ (nodeToList nd) @ (toList r)
  \<and>
  \<not> p (i + (gmft l))
  \<and>
  p (i + (gmft l) + (gmn nd))
  \<and>
  is_leveln_ftree n l
  \<and>
  is_measured_ftree l
  \<and>
  is_leveln_ftree n r
  \<and>
  is_measured_ftree r
  \<and>
  is_leveln_node n nd
  \<and>
  is_measured_node nd
  "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>is_leveln_ftree n s; is_measured_ftree s; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft s); nsplitTree p i s = (l, nd, r)\<rbrakk> \<Longrightarrow> toList s = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
proof (induct p i s arbitrary: n l nd r rule: nsplitTree.induct)
[PROOF STATE]
proof (state)
goal (3 subgoals):
 1. \<And>p i n l nd r. \<lbrakk>is_leveln_ftree n Empty; is_measured_ftree Empty; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft Empty); nsplitTree p i Empty = (l, nd, r)\<rbrakk> \<Longrightarrow> toList Empty = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
 2. \<And>p i ea n l nd r. \<lbrakk>is_leveln_ftree n (Single ea); is_measured_ftree (Single ea); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Single ea)); nsplitTree p i (Single ea) = (l, nd, r)\<rbrakk> \<Longrightarrow> toList (Single ea) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
 3. \<And>p i uu_ pr m sf n l nd r. \<lbrakk>\<And>x xa n l nd r. \<lbrakk>x = i + gmd pr; xa = x + gmft m; \<not> p x; p xa; is_leveln_ftree n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> toList m = toList l @ nodeToList nd @ toList r \<and> \<not> p (x + gmft l) \<and> p (x + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd; is_leveln_ftree n (Deep uu_ pr m sf); is_measured_ftree (Deep uu_ pr m sf); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Deep uu_ pr m sf)); nsplitTree p i (Deep uu_ pr m sf) = (l, nd, r)\<rbrakk> \<Longrightarrow> toList (Deep uu_ pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
is_leveln_ftree n Empty
is_measured_ftree Empty
p_ ?a \<Longrightarrow> p_ (?a + ?b)
\<not> p_ i_
p_ (i_ + gmft Empty)
nsplitTree p_ i_ Empty = (l, nd, r)

goal (3 subgoals):
 1. \<And>p i n l nd r. \<lbrakk>is_leveln_ftree n Empty; is_measured_ftree Empty; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft Empty); nsplitTree p i Empty = (l, nd, r)\<rbrakk> \<Longrightarrow> toList Empty = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
 2. \<And>p i ea n l nd r. \<lbrakk>is_leveln_ftree n (Single ea); is_measured_ftree (Single ea); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Single ea)); nsplitTree p i (Single ea) = (l, nd, r)\<rbrakk> \<Longrightarrow> toList (Single ea) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
 3. \<And>p i uu_ pr m sf n l nd r. \<lbrakk>\<And>x xa n l nd r. \<lbrakk>x = i + gmd pr; xa = x + gmft m; \<not> p x; p xa; is_leveln_ftree n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> toList m = toList l @ nodeToList nd @ toList r \<and> \<not> p (x + gmft l) \<and> p (x + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd; is_leveln_ftree n (Deep uu_ pr m sf); is_measured_ftree (Deep uu_ pr m sf); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Deep uu_ pr m sf)); nsplitTree p i (Deep uu_ pr m sf) = (l, nd, r)\<rbrakk> \<Longrightarrow> toList (Deep uu_ pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
is_leveln_ftree n Empty
is_measured_ftree Empty
p_ ?a \<Longrightarrow> p_ (?a + ?b)
\<not> p_ i_
p_ (i_ + gmft Empty)
nsplitTree p_ i_ Empty = (l, nd, r)

goal (1 subgoal):
 1. toList Empty = toList l @ nodeToList nd @ toList r \<and> \<not> p_ (i_ + gmft l) \<and> p_ (i_ + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
toList Empty = toList l @ nodeToList nd @ toList r \<and> \<not> p_ (i_ + gmft l) \<and> p_ (i_ + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd

goal (2 subgoals):
 1. \<And>p i ea n l nd r. \<lbrakk>is_leveln_ftree n (Single ea); is_measured_ftree (Single ea); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Single ea)); nsplitTree p i (Single ea) = (l, nd, r)\<rbrakk> \<Longrightarrow> toList (Single ea) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
 2. \<And>p i uu_ pr m sf n l nd r. \<lbrakk>\<And>x xa n l nd r. \<lbrakk>x = i + gmd pr; xa = x + gmft m; \<not> p x; p xa; is_leveln_ftree n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> toList m = toList l @ nodeToList nd @ toList r \<and> \<not> p (x + gmft l) \<and> p (x + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd; is_leveln_ftree n (Deep uu_ pr m sf); is_measured_ftree (Deep uu_ pr m sf); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Deep uu_ pr m sf)); nsplitTree p i (Deep uu_ pr m sf) = (l, nd, r)\<rbrakk> \<Longrightarrow> toList (Deep uu_ pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>p i ea n l nd r. \<lbrakk>is_leveln_ftree n (Single ea); is_measured_ftree (Single ea); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Single ea)); nsplitTree p i (Single ea) = (l, nd, r)\<rbrakk> \<Longrightarrow> toList (Single ea) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
 2. \<And>p i uu_ pr m sf n l nd r. \<lbrakk>\<And>x xa n l nd r. \<lbrakk>x = i + gmd pr; xa = x + gmft m; \<not> p x; p xa; is_leveln_ftree n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> toList m = toList l @ nodeToList nd @ toList r \<and> \<not> p (x + gmft l) \<and> p (x + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd; is_leveln_ftree n (Deep uu_ pr m sf); is_measured_ftree (Deep uu_ pr m sf); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Deep uu_ pr m sf)); nsplitTree p i (Deep uu_ pr m sf) = (l, nd, r)\<rbrakk> \<Longrightarrow> toList (Deep uu_ pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
is_leveln_ftree n (Single ea_)
is_measured_ftree (Single ea_)
p_ ?a \<Longrightarrow> p_ (?a + ?b)
\<not> p_ i_
p_ (i_ + gmft (Single ea_))
nsplitTree p_ i_ (Single ea_) = (l, nd, r)

goal (2 subgoals):
 1. \<And>p i ea n l nd r. \<lbrakk>is_leveln_ftree n (Single ea); is_measured_ftree (Single ea); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Single ea)); nsplitTree p i (Single ea) = (l, nd, r)\<rbrakk> \<Longrightarrow> toList (Single ea) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
 2. \<And>p i uu_ pr m sf n l nd r. \<lbrakk>\<And>x xa n l nd r. \<lbrakk>x = i + gmd pr; xa = x + gmft m; \<not> p x; p xa; is_leveln_ftree n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> toList m = toList l @ nodeToList nd @ toList r \<and> \<not> p (x + gmft l) \<and> p (x + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd; is_leveln_ftree n (Deep uu_ pr m sf); is_measured_ftree (Deep uu_ pr m sf); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Deep uu_ pr m sf)); nsplitTree p i (Deep uu_ pr m sf) = (l, nd, r)\<rbrakk> \<Longrightarrow> toList (Deep uu_ pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
is_leveln_ftree n (Single ea_)
is_measured_ftree (Single ea_)
p_ ?a \<Longrightarrow> p_ (?a + ?b)
\<not> p_ i_
p_ (i_ + gmft (Single ea_))
nsplitTree p_ i_ (Single ea_) = (l, nd, r)

goal (1 subgoal):
 1. toList (Single ea_) = toList l @ nodeToList nd @ toList r \<and> \<not> p_ (i_ + gmft l) \<and> p_ (i_ + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
toList (Single ea_) = toList l @ nodeToList nd @ toList r \<and> \<not> p_ (i_ + gmft l) \<and> p_ (i_ + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd

goal (1 subgoal):
 1. \<And>p i uu_ pr m sf n l nd r. \<lbrakk>\<And>x xa n l nd r. \<lbrakk>x = i + gmd pr; xa = x + gmft m; \<not> p x; p xa; is_leveln_ftree n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> toList m = toList l @ nodeToList nd @ toList r \<and> \<not> p (x + gmft l) \<and> p (x + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd; is_leveln_ftree n (Deep uu_ pr m sf); is_measured_ftree (Deep uu_ pr m sf); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Deep uu_ pr m sf)); nsplitTree p i (Deep uu_ pr m sf) = (l, nd, r)\<rbrakk> \<Longrightarrow> toList (Deep uu_ pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>p i uu_ pr m sf n l nd r. \<lbrakk>\<And>x xa n l nd r. \<lbrakk>x = i + gmd pr; xa = x + gmft m; \<not> p x; p xa; is_leveln_ftree n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> toList m = toList l @ nodeToList nd @ toList r \<and> \<not> p (x + gmft l) \<and> p (x + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd; is_leveln_ftree n (Deep uu_ pr m sf); is_measured_ftree (Deep uu_ pr m sf); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Deep uu_ pr m sf)); nsplitTree p i (Deep uu_ pr m sf) = (l, nd, r)\<rbrakk> \<Longrightarrow> toList (Deep uu_ pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
case (3 p i uu "pr" m sf n l nd r)
[PROOF STATE]
proof (state)
this:
\<lbrakk>?x = i + gmd pr; ?xa = ?x + gmft m; \<not> p ?x; p ?xa; is_leveln_ftree ?n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p ?x; p (?x + gmft m); nsplitTree p ?x m = (?l, ?nd, ?r)\<rbrakk> \<Longrightarrow> toList m = toList ?l @ nodeToList ?nd @ toList ?r \<and> \<not> p (?x + gmft ?l) \<and> p (?x + gmft ?l + gmn ?nd) \<and> is_leveln_ftree ?n ?l \<and> is_measured_ftree ?l \<and> is_leveln_ftree ?n ?r \<and> is_measured_ftree ?r \<and> is_leveln_node ?n ?nd \<and> is_measured_node ?nd
is_leveln_ftree n (Deep uu pr m sf)
is_measured_ftree (Deep uu pr m sf)
p ?a \<Longrightarrow> p (?a + ?b)
\<not> p i
p (i + gmft (Deep uu pr m sf))
nsplitTree p i (Deep uu pr m sf) = (l, nd, r)

goal (1 subgoal):
 1. \<And>p i uu_ pr m sf n l nd r. \<lbrakk>\<And>x xa n l nd r. \<lbrakk>x = i + gmd pr; xa = x + gmft m; \<not> p x; p xa; is_leveln_ftree n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> toList m = toList l @ nodeToList nd @ toList r \<and> \<not> p (x + gmft l) \<and> p (x + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd; is_leveln_ftree n (Deep uu_ pr m sf); is_measured_ftree (Deep uu_ pr m sf); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Deep uu_ pr m sf)); nsplitTree p i (Deep uu_ pr m sf) = (l, nd, r)\<rbrakk> \<Longrightarrow> toList (Deep uu_ pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
thus ?case
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x = i + gmd pr; ?xa = ?x + gmft m; \<not> p ?x; p ?xa; is_leveln_ftree ?n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p ?x; p (?x + gmft m); nsplitTree p ?x m = (?l, ?nd, ?r)\<rbrakk> \<Longrightarrow> toList m = toList ?l @ nodeToList ?nd @ toList ?r \<and> \<not> p (?x + gmft ?l) \<and> p (?x + gmft ?l + gmn ?nd) \<and> is_leveln_ftree ?n ?l \<and> is_measured_ftree ?l \<and> is_leveln_ftree ?n ?r \<and> is_measured_ftree ?r \<and> is_leveln_node ?n ?nd \<and> is_measured_node ?nd
is_leveln_ftree n (Deep uu pr m sf)
is_measured_ftree (Deep uu pr m sf)
p ?a \<Longrightarrow> p (?a + ?b)
\<not> p i
p (i + gmft (Deep uu pr m sf))
nsplitTree p i (Deep uu pr m sf) = (l, nd, r)

goal (1 subgoal):
 1. toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
proof (cases "p (i + gmd pr)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<And>x xa n l nd r. \<lbrakk>x = i + gmd pr; xa = x + gmft m; \<not> p x; p xa; is_leveln_ftree n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> toList m = toList l @ nodeToList nd @ toList r \<and> \<not> p (x + gmft l) \<and> p (x + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd; is_leveln_ftree n (Deep uu pr m sf); is_measured_ftree (Deep uu pr m sf); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Deep uu pr m sf)); nsplitTree p i (Deep uu pr m sf) = (l, nd, r); p (i + gmd pr)\<rbrakk> \<Longrightarrow> toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
 2. \<lbrakk>\<And>x xa n l nd r. \<lbrakk>x = i + gmd pr; xa = x + gmft m; \<not> p x; p xa; is_leveln_ftree n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> toList m = toList l @ nodeToList nd @ toList r \<and> \<not> p (x + gmft l) \<and> p (x + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd; is_leveln_ftree n (Deep uu pr m sf); is_measured_ftree (Deep uu pr m sf); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Deep uu pr m sf)); nsplitTree p i (Deep uu pr m sf) = (l, nd, r); \<not> p (i + gmd pr)\<rbrakk> \<Longrightarrow> toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
p (i + gmd pr)

goal (2 subgoals):
 1. \<lbrakk>\<And>x xa n l nd r. \<lbrakk>x = i + gmd pr; xa = x + gmft m; \<not> p x; p xa; is_leveln_ftree n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> toList m = toList l @ nodeToList nd @ toList r \<and> \<not> p (x + gmft l) \<and> p (x + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd; is_leveln_ftree n (Deep uu pr m sf); is_measured_ftree (Deep uu pr m sf); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Deep uu pr m sf)); nsplitTree p i (Deep uu pr m sf) = (l, nd, r); p (i + gmd pr)\<rbrakk> \<Longrightarrow> toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
 2. \<lbrakk>\<And>x xa n l nd r. \<lbrakk>x = i + gmd pr; xa = x + gmft m; \<not> p x; p xa; is_leveln_ftree n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> toList m = toList l @ nodeToList nd @ toList r \<and> \<not> p (x + gmft l) \<and> p (x + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd; is_leveln_ftree n (Deep uu pr m sf); is_measured_ftree (Deep uu pr m sf); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Deep uu pr m sf)); nsplitTree p i (Deep uu pr m sf) = (l, nd, r); \<not> p (i + gmd pr)\<rbrakk> \<Longrightarrow> toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
with 3
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?x = i + gmd pr; ?xa = ?x + gmft m; \<not> p ?x; p ?xa; is_leveln_ftree ?n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p ?x; p (?x + gmft m); nsplitTree p ?x m = (?l, ?nd, ?r)\<rbrakk> \<Longrightarrow> toList m = toList ?l @ nodeToList ?nd @ toList ?r \<and> \<not> p (?x + gmft ?l) \<and> p (?x + gmft ?l + gmn ?nd) \<and> is_leveln_ftree ?n ?l \<and> is_measured_ftree ?l \<and> is_leveln_ftree ?n ?r \<and> is_measured_ftree ?r \<and> is_leveln_node ?n ?nd \<and> is_measured_node ?nd
is_leveln_ftree n (Deep uu pr m sf)
is_measured_ftree (Deep uu pr m sf)
p ?a \<Longrightarrow> p (?a + ?b)
\<not> p i
p (i + gmft (Deep uu pr m sf))
nsplitTree p i (Deep uu pr m sf) = (l, nd, r)
p (i + gmd pr)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x = i + gmd pr; ?xa = ?x + gmft m; \<not> p ?x; p ?xa; is_leveln_ftree ?n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p ?x; p (?x + gmft m); nsplitTree p ?x m = (?l, ?nd, ?r)\<rbrakk> \<Longrightarrow> toList m = toList ?l @ nodeToList ?nd @ toList ?r \<and> \<not> p (?x + gmft ?l) \<and> p (?x + gmft ?l + gmn ?nd) \<and> is_leveln_ftree ?n ?l \<and> is_measured_ftree ?l \<and> is_leveln_ftree ?n ?r \<and> is_measured_ftree ?r \<and> is_leveln_node ?n ?nd \<and> is_measured_node ?nd
is_leveln_ftree n (Deep uu pr m sf)
is_measured_ftree (Deep uu pr m sf)
p ?a \<Longrightarrow> p (?a + ?b)
\<not> p i
p (i + gmft (Deep uu pr m sf))
nsplitTree p i (Deep uu pr m sf) = (l, nd, r)
p (i + gmd pr)

goal (1 subgoal):
 1. toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>x xa n l nd r. \<lbrakk>x = i + gmd pr; xa = x + gmft m; \<not> p x; p xa; is_leveln_ftree n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> toList m = toList l @ nodeToList nd @ toList r \<and> \<not> p (x + gmft l) \<and> p (x + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd; is_leveln_ftree n (Deep uu pr m sf); is_measured_ftree (Deep uu pr m sf); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Deep uu pr m sf)); nsplitTree p i (Deep uu pr m sf) = (l, nd, r); p (i + gmd pr)\<rbrakk> \<Longrightarrow> toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
obtain l1 x r1 where
        l1xr1: "splitDigit p i pr = (l1,x,r1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>l1 x r1. splitDigit p i pr = (l1, x, r1) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases "splitDigit p i pr", blast)
[PROOF STATE]
proof (state)
this:
splitDigit p i pr = (l1, x, r1)

goal (1 subgoal):
 1. \<lbrakk>\<And>x xa n l nd r. \<lbrakk>x = i + gmd pr; xa = x + gmft m; \<not> p x; p xa; is_leveln_ftree n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> toList m = toList l @ nodeToList nd @ toList r \<and> \<not> p (x + gmft l) \<and> p (x + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd; is_leveln_ftree n (Deep uu pr m sf); is_measured_ftree (Deep uu pr m sf); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Deep uu pr m sf)); nsplitTree p i (Deep uu pr m sf) = (l, nd, r); p (i + gmd pr)\<rbrakk> \<Longrightarrow> toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
with True 3(7)
[PROOF STATE]
proof (chain)
picking this:
p (i + gmd pr)
nsplitTree p i (Deep uu pr m sf) = (l, nd, r)
splitDigit p i pr = (l1, x, r1)
[PROOF STEP]
have
        v1: "l = nlistToTree l1" "nd = x" "r = deepL r1 m sf"
[PROOF STATE]
proof (prove)
using this:
p (i + gmd pr)
nsplitTree p i (Deep uu pr m sf) = (l, nd, r)
splitDigit p i pr = (l1, x, r1)

goal (1 subgoal):
 1. l = nlistToTree l1 &&& nd = x &&& r = deepL r1 m sf
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l = nlistToTree l1
nd = x
r = deepL r1 m sf

goal (1 subgoal):
 1. \<lbrakk>\<And>x xa n l nd r. \<lbrakk>x = i + gmd pr; xa = x + gmft m; \<not> p x; p xa; is_leveln_ftree n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> toList m = toList l @ nodeToList nd @ toList r \<and> \<not> p (x + gmft l) \<and> p (x + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd; is_leveln_ftree n (Deep uu pr m sf); is_measured_ftree (Deep uu pr m sf); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Deep uu pr m sf)); nsplitTree p i (Deep uu pr m sf) = (l, nd, r); p (i + gmd pr)\<rbrakk> \<Longrightarrow> toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
from l1xr1
[PROOF STATE]
proof (chain)
picking this:
splitDigit p i pr = (l1, x, r1)
[PROOF STEP]
have
        v2: "digitToList pr = nlistToList l1 @ nodeToList x @ nlistToList r1"
        "length l1 \<le> 4" "length r1 \<le> 4"
[PROOF STATE]
proof (prove)
using this:
splitDigit p i pr = (l1, x, r1)

goal (1 subgoal):
 1. digitToList pr = nlistToList l1 @ nodeToList x @ nlistToList r1 &&& length l1 \<le> 4 &&& length r1 \<le> 4
[PROOF STEP]
by (auto simp add: splitDigit_list)
[PROOF STATE]
proof (state)
this:
digitToList pr = nlistToList l1 @ nodeToList x @ nlistToList r1
length l1 \<le> 4
length r1 \<le> 4

goal (1 subgoal):
 1. \<lbrakk>\<And>x xa n l nd r. \<lbrakk>x = i + gmd pr; xa = x + gmft m; \<not> p x; p xa; is_leveln_ftree n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> toList m = toList l @ nodeToList nd @ toList r \<and> \<not> p (x + gmft l) \<and> p (x + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd; is_leveln_ftree n (Deep uu pr m sf); is_measured_ftree (Deep uu pr m sf); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Deep uu pr m sf)); nsplitTree p i (Deep uu pr m sf) = (l, nd, r); p (i + gmd pr)\<rbrakk> \<Longrightarrow> toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
from 3(2,3)
[PROOF STATE]
proof (chain)
picking this:
is_leveln_ftree n (Deep uu pr m sf)
is_measured_ftree (Deep uu pr m sf)
[PROOF STEP]
have
        pr_m_sf_inv: "is_leveln_digit n pr \<and> is_measured_digit pr"
        "is_leveln_ftree (Suc n) m \<and> is_measured_ftree m"
        "is_leveln_digit n sf \<and> is_measured_digit sf"
[PROOF STATE]
proof (prove)
using this:
is_leveln_ftree n (Deep uu pr m sf)
is_measured_ftree (Deep uu pr m sf)

goal (1 subgoal):
 1. is_leveln_digit n pr \<and> is_measured_digit pr &&& is_leveln_ftree (Suc n) m \<and> is_measured_ftree m &&& is_leveln_digit n sf \<and> is_measured_digit sf
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
is_leveln_digit n pr \<and> is_measured_digit pr
is_leveln_ftree (Suc n) m \<and> is_measured_ftree m
is_leveln_digit n sf \<and> is_measured_digit sf

goal (1 subgoal):
 1. \<lbrakk>\<And>x xa n l nd r. \<lbrakk>x = i + gmd pr; xa = x + gmft m; \<not> p x; p xa; is_leveln_ftree n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> toList m = toList l @ nodeToList nd @ toList r \<and> \<not> p (x + gmft l) \<and> p (x + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd; is_leveln_ftree n (Deep uu pr m sf); is_measured_ftree (Deep uu pr m sf); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Deep uu pr m sf)); nsplitTree p i (Deep uu pr m sf) = (l, nd, r); p (i + gmd pr)\<rbrakk> \<Longrightarrow> toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
with 3(4,5) pr_m_sf_inv(1) True l1xr1
        splitDigit_inv[of p i "pr" n l1 x r1]
[PROOF STATE]
proof (chain)
picking this:
p ?a \<Longrightarrow> p (?a + ?b)
\<not> p i
is_leveln_digit n pr \<and> is_measured_digit pr
p (i + gmd pr)
splitDigit p i pr = (l1, x, r1)
\<lbrakk>\<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; is_measured_digit pr; is_leveln_digit n pr; p (i + gmd pr); splitDigit p i pr = (l1, x, r1)\<rbrakk> \<Longrightarrow> \<not> p (i + gmnl l1) \<and> p (i + gmnl l1 + gmn x) \<and> (\<forall>x\<in>set l1. is_measured_node x \<and> is_leveln_node n x) \<and> (\<forall>x\<in>set r1. is_measured_node x \<and> is_leveln_node n x) \<and> is_measured_node x \<and> is_leveln_node n x
is_leveln_digit n pr \<and> is_measured_digit pr
is_leveln_ftree (Suc n) m \<and> is_measured_ftree m
is_leveln_digit n sf \<and> is_measured_digit sf
[PROOF STEP]
have
        l1_x_r1_inv:
        "\<not> p (i + (gmnl l1))"
        "p (i + (gmnl l1) + (gmn x))"
        "\<forall> x \<in> set l1. (is_measured_node x \<and> is_leveln_node n x)"
        "\<forall> x \<in> set r1. (is_measured_node x \<and> is_leveln_node n x)"
        "is_measured_node x \<and> is_leveln_node n x"
[PROOF STATE]
proof (prove)
using this:
p ?a \<Longrightarrow> p (?a + ?b)
\<not> p i
is_leveln_digit n pr \<and> is_measured_digit pr
p (i + gmd pr)
splitDigit p i pr = (l1, x, r1)
\<lbrakk>\<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; is_measured_digit pr; is_leveln_digit n pr; p (i + gmd pr); splitDigit p i pr = (l1, x, r1)\<rbrakk> \<Longrightarrow> \<not> p (i + gmnl l1) \<and> p (i + gmnl l1 + gmn x) \<and> (\<forall>x\<in>set l1. is_measured_node x \<and> is_leveln_node n x) \<and> (\<forall>x\<in>set r1. is_measured_node x \<and> is_leveln_node n x) \<and> is_measured_node x \<and> is_leveln_node n x
is_leveln_digit n pr \<and> is_measured_digit pr
is_leveln_ftree (Suc n) m \<and> is_measured_ftree m
is_leveln_digit n sf \<and> is_measured_digit sf

goal (1 subgoal):
 1. (\<not> p (i + gmnl l1) &&& p (i + gmnl l1 + gmn x)) &&& \<forall>x\<in>set l1. is_measured_node x \<and> is_leveln_node n x &&& \<forall>x\<in>set r1. is_measured_node x \<and> is_leveln_node n x &&& is_measured_node x \<and> is_leveln_node n x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> p (i + gmnl l1)
p (i + gmnl l1 + gmn x)
\<forall>x\<in>set l1. is_measured_node x \<and> is_leveln_node n x
\<forall>x\<in>set r1. is_measured_node x \<and> is_leveln_node n x
is_measured_node x \<and> is_leveln_node n x

goal (1 subgoal):
 1. \<lbrakk>\<And>x xa n l nd r. \<lbrakk>x = i + gmd pr; xa = x + gmft m; \<not> p x; p xa; is_leveln_ftree n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> toList m = toList l @ nodeToList nd @ toList r \<and> \<not> p (x + gmft l) \<and> p (x + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd; is_leveln_ftree n (Deep uu pr m sf); is_measured_ftree (Deep uu pr m sf); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Deep uu pr m sf)); nsplitTree p i (Deep uu pr m sf) = (l, nd, r); p (i + gmd pr)\<rbrakk> \<Longrightarrow> toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
from v2 v1 l1_x_r1_inv(4) pr_m_sf_inv
[PROOF STATE]
proof (chain)
picking this:
digitToList pr = nlistToList l1 @ nodeToList x @ nlistToList r1
length l1 \<le> 4
length r1 \<le> 4
l = nlistToTree l1
nd = x
r = deepL r1 m sf
\<forall>x\<in>set r1. is_measured_node x \<and> is_leveln_node n x
is_leveln_digit n pr \<and> is_measured_digit pr
is_leveln_ftree (Suc n) m \<and> is_measured_ftree m
is_leveln_digit n sf \<and> is_measured_digit sf
[PROOF STEP]
have
        ziel1: "toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r"
[PROOF STATE]
proof (prove)
using this:
digitToList pr = nlistToList l1 @ nodeToList x @ nlistToList r1
length l1 \<le> 4
length r1 \<le> 4
l = nlistToTree l1
nd = x
r = deepL r1 m sf
\<forall>x\<in>set r1. is_measured_node x \<and> is_leveln_node n x
is_leveln_digit n pr \<and> is_measured_digit pr
is_leveln_ftree (Suc n) m \<and> is_measured_ftree m
is_leveln_digit n sf \<and> is_measured_digit sf

goal (1 subgoal):
 1. toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r
[PROOF STEP]
by (auto simp add: nlistToTree_list deepL_list)
[PROOF STATE]
proof (state)
this:
toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r

goal (1 subgoal):
 1. \<lbrakk>\<And>x xa n l nd r. \<lbrakk>x = i + gmd pr; xa = x + gmft m; \<not> p x; p xa; is_leveln_ftree n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> toList m = toList l @ nodeToList nd @ toList r \<and> \<not> p (x + gmft l) \<and> p (x + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd; is_leveln_ftree n (Deep uu pr m sf); is_measured_ftree (Deep uu pr m sf); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Deep uu pr m sf)); nsplitTree p i (Deep uu pr m sf) = (l, nd, r); p (i + gmd pr)\<rbrakk> \<Longrightarrow> toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
from l1_x_r1_inv(3) v1(1)
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>set l1. is_measured_node x \<and> is_leveln_node n x
l = nlistToTree l1
[PROOF STEP]
have
        v3: "gmft l = gmnl l1"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set l1. is_measured_node x \<and> is_leveln_node n x
l = nlistToTree l1

goal (1 subgoal):
 1. gmft l = gmnl l1
[PROOF STEP]
by (simp add: gmnl_gmft)
[PROOF STATE]
proof (state)
this:
gmft l = gmnl l1

goal (1 subgoal):
 1. \<lbrakk>\<And>x xa n l nd r. \<lbrakk>x = i + gmd pr; xa = x + gmft m; \<not> p x; p xa; is_leveln_ftree n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> toList m = toList l @ nodeToList nd @ toList r \<and> \<not> p (x + gmft l) \<and> p (x + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd; is_leveln_ftree n (Deep uu pr m sf); is_measured_ftree (Deep uu pr m sf); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Deep uu pr m sf)); nsplitTree p i (Deep uu pr m sf) = (l, nd, r); p (i + gmd pr)\<rbrakk> \<Longrightarrow> toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
with l1_x_r1_inv(1,2) v1
[PROOF STATE]
proof (chain)
picking this:
\<not> p (i + gmnl l1)
p (i + gmnl l1 + gmn x)
l = nlistToTree l1
nd = x
r = deepL r1 m sf
gmft l = gmnl l1
[PROOF STEP]
have
        ziel2: " \<not> p (i + gmft l)"
        "p (i + gmft l + gmn nd)"
[PROOF STATE]
proof (prove)
using this:
\<not> p (i + gmnl l1)
p (i + gmnl l1 + gmn x)
l = nlistToTree l1
nd = x
r = deepL r1 m sf
gmft l = gmnl l1

goal (1 subgoal):
 1. \<not> p (i + gmft l) &&& p (i + gmft l + gmn nd)
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
\<not> p (i + gmft l)
p (i + gmft l + gmn nd)

goal (1 subgoal):
 1. \<lbrakk>\<And>x xa n l nd r. \<lbrakk>x = i + gmd pr; xa = x + gmft m; \<not> p x; p xa; is_leveln_ftree n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> toList m = toList l @ nodeToList nd @ toList r \<and> \<not> p (x + gmft l) \<and> p (x + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd; is_leveln_ftree n (Deep uu pr m sf); is_measured_ftree (Deep uu pr m sf); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Deep uu pr m sf)); nsplitTree p i (Deep uu pr m sf) = (l, nd, r); p (i + gmd pr)\<rbrakk> \<Longrightarrow> toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
from l1_x_r1_inv(3,4,5) v1 v2(3) pr_m_sf_inv
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>set l1. is_measured_node x \<and> is_leveln_node n x
\<forall>x\<in>set r1. is_measured_node x \<and> is_leveln_node n x
is_measured_node x \<and> is_leveln_node n x
l = nlistToTree l1
nd = x
r = deepL r1 m sf
length r1 \<le> 4
is_leveln_digit n pr \<and> is_measured_digit pr
is_leveln_ftree (Suc n) m \<and> is_measured_ftree m
is_leveln_digit n sf \<and> is_measured_digit sf
[PROOF STEP]
have
        ziel3: "is_leveln_ftree n l \<and> is_measured_ftree l \<and>
        is_leveln_ftree n r \<and> is_measured_ftree r \<and>
        is_leveln_node n nd \<and> is_measured_node nd"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set l1. is_measured_node x \<and> is_leveln_node n x
\<forall>x\<in>set r1. is_measured_node x \<and> is_leveln_node n x
is_measured_node x \<and> is_leveln_node n x
l = nlistToTree l1
nd = x
r = deepL r1 m sf
length r1 \<le> 4
is_leveln_digit n pr \<and> is_measured_digit pr
is_leveln_ftree (Suc n) m \<and> is_measured_ftree m
is_leveln_digit n sf \<and> is_measured_digit sf

goal (1 subgoal):
 1. is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
by (auto simp add: nlistToTree_inv deepL_inv)
[PROOF STATE]
proof (state)
this:
is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd

goal (1 subgoal):
 1. \<lbrakk>\<And>x xa n l nd r. \<lbrakk>x = i + gmd pr; xa = x + gmft m; \<not> p x; p xa; is_leveln_ftree n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> toList m = toList l @ nodeToList nd @ toList r \<and> \<not> p (x + gmft l) \<and> p (x + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd; is_leveln_ftree n (Deep uu pr m sf); is_measured_ftree (Deep uu pr m sf); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Deep uu pr m sf)); nsplitTree p i (Deep uu pr m sf) = (l, nd, r); p (i + gmd pr)\<rbrakk> \<Longrightarrow> toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
from ziel1 ziel2 ziel3
[PROOF STATE]
proof (chain)
picking this:
toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r
\<not> p (i + gmft l)
p (i + gmft l + gmn nd)
is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r
\<not> p (i + gmft l)
p (i + gmft l + gmn nd)
is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd

goal (1 subgoal):
 1. toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd

goal (1 subgoal):
 1. \<lbrakk>\<And>x xa n l nd r. \<lbrakk>x = i + gmd pr; xa = x + gmft m; \<not> p x; p xa; is_leveln_ftree n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> toList m = toList l @ nodeToList nd @ toList r \<and> \<not> p (x + gmft l) \<and> p (x + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd; is_leveln_ftree n (Deep uu pr m sf); is_measured_ftree (Deep uu pr m sf); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Deep uu pr m sf)); nsplitTree p i (Deep uu pr m sf) = (l, nd, r); \<not> p (i + gmd pr)\<rbrakk> \<Longrightarrow> toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>x xa n l nd r. \<lbrakk>x = i + gmd pr; xa = x + gmft m; \<not> p x; p xa; is_leveln_ftree n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> toList m = toList l @ nodeToList nd @ toList r \<and> \<not> p (x + gmft l) \<and> p (x + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd; is_leveln_ftree n (Deep uu pr m sf); is_measured_ftree (Deep uu pr m sf); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Deep uu pr m sf)); nsplitTree p i (Deep uu pr m sf) = (l, nd, r); \<not> p (i + gmd pr)\<rbrakk> \<Longrightarrow> toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> p (i + gmd pr)

goal (1 subgoal):
 1. \<lbrakk>\<And>x xa n l nd r. \<lbrakk>x = i + gmd pr; xa = x + gmft m; \<not> p x; p xa; is_leveln_ftree n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> toList m = toList l @ nodeToList nd @ toList r \<and> \<not> p (x + gmft l) \<and> p (x + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd; is_leveln_ftree n (Deep uu pr m sf); is_measured_ftree (Deep uu pr m sf); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Deep uu pr m sf)); nsplitTree p i (Deep uu pr m sf) = (l, nd, r); \<not> p (i + gmd pr)\<rbrakk> \<Longrightarrow> toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
note case1 = this
[PROOF STATE]
proof (state)
this:
\<not> p (i + gmd pr)

goal (1 subgoal):
 1. \<lbrakk>\<And>x xa n l nd r. \<lbrakk>x = i + gmd pr; xa = x + gmft m; \<not> p x; p xa; is_leveln_ftree n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> toList m = toList l @ nodeToList nd @ toList r \<and> \<not> p (x + gmft l) \<and> p (x + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd; is_leveln_ftree n (Deep uu pr m sf); is_measured_ftree (Deep uu pr m sf); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Deep uu pr m sf)); nsplitTree p i (Deep uu pr m sf) = (l, nd, r); \<not> p (i + gmd pr)\<rbrakk> \<Longrightarrow> toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
with 3
[PROOF STATE]
proof (chain)
picking this:
\<lbrakk>?x = i + gmd pr; ?xa = ?x + gmft m; \<not> p ?x; p ?xa; is_leveln_ftree ?n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p ?x; p (?x + gmft m); nsplitTree p ?x m = (?l, ?nd, ?r)\<rbrakk> \<Longrightarrow> toList m = toList ?l @ nodeToList ?nd @ toList ?r \<and> \<not> p (?x + gmft ?l) \<and> p (?x + gmft ?l + gmn ?nd) \<and> is_leveln_ftree ?n ?l \<and> is_measured_ftree ?l \<and> is_leveln_ftree ?n ?r \<and> is_measured_ftree ?r \<and> is_leveln_node ?n ?nd \<and> is_measured_node ?nd
is_leveln_ftree n (Deep uu pr m sf)
is_measured_ftree (Deep uu pr m sf)
p ?a \<Longrightarrow> p (?a + ?b)
\<not> p i
p (i + gmft (Deep uu pr m sf))
nsplitTree p i (Deep uu pr m sf) = (l, nd, r)
\<not> p (i + gmd pr)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<lbrakk>?x = i + gmd pr; ?xa = ?x + gmft m; \<not> p ?x; p ?xa; is_leveln_ftree ?n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p ?x; p (?x + gmft m); nsplitTree p ?x m = (?l, ?nd, ?r)\<rbrakk> \<Longrightarrow> toList m = toList ?l @ nodeToList ?nd @ toList ?r \<and> \<not> p (?x + gmft ?l) \<and> p (?x + gmft ?l + gmn ?nd) \<and> is_leveln_ftree ?n ?l \<and> is_measured_ftree ?l \<and> is_leveln_ftree ?n ?r \<and> is_measured_ftree ?r \<and> is_leveln_node ?n ?nd \<and> is_measured_node ?nd
is_leveln_ftree n (Deep uu pr m sf)
is_measured_ftree (Deep uu pr m sf)
p ?a \<Longrightarrow> p (?a + ?b)
\<not> p i
p (i + gmft (Deep uu pr m sf))
nsplitTree p i (Deep uu pr m sf) = (l, nd, r)
\<not> p (i + gmd pr)

goal (1 subgoal):
 1. toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
proof (cases "p (i + gmd pr + gmft m)")
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<lbrakk>\<And>x xa n l nd r. \<lbrakk>x = i + gmd pr; xa = x + gmft m; \<not> p x; p xa; is_leveln_ftree n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> toList m = toList l @ nodeToList nd @ toList r \<and> \<not> p (x + gmft l) \<and> p (x + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd; is_leveln_ftree n (Deep uu pr m sf); is_measured_ftree (Deep uu pr m sf); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Deep uu pr m sf)); nsplitTree p i (Deep uu pr m sf) = (l, nd, r); \<not> p (i + gmd pr); p (i + gmd pr + gmft m)\<rbrakk> \<Longrightarrow> toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
 2. \<lbrakk>\<And>x xa n l nd r. \<lbrakk>x = i + gmd pr; xa = x + gmft m; \<not> p x; p xa; is_leveln_ftree n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> toList m = toList l @ nodeToList nd @ toList r \<and> \<not> p (x + gmft l) \<and> p (x + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd; is_leveln_ftree n (Deep uu pr m sf); is_measured_ftree (Deep uu pr m sf); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Deep uu pr m sf)); nsplitTree p i (Deep uu pr m sf) = (l, nd, r); \<not> p (i + gmd pr); \<not> p (i + gmd pr + gmft m)\<rbrakk> \<Longrightarrow> toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
case False
[PROOF STATE]
proof (state)
this:
\<not> p (i + gmd pr + gmft m)

goal (2 subgoals):
 1. \<lbrakk>\<And>x xa n l nd r. \<lbrakk>x = i + gmd pr; xa = x + gmft m; \<not> p x; p xa; is_leveln_ftree n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> toList m = toList l @ nodeToList nd @ toList r \<and> \<not> p (x + gmft l) \<and> p (x + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd; is_leveln_ftree n (Deep uu pr m sf); is_measured_ftree (Deep uu pr m sf); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Deep uu pr m sf)); nsplitTree p i (Deep uu pr m sf) = (l, nd, r); \<not> p (i + gmd pr); p (i + gmd pr + gmft m)\<rbrakk> \<Longrightarrow> toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
 2. \<lbrakk>\<And>x xa n l nd r. \<lbrakk>x = i + gmd pr; xa = x + gmft m; \<not> p x; p xa; is_leveln_ftree n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> toList m = toList l @ nodeToList nd @ toList r \<and> \<not> p (x + gmft l) \<and> p (x + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd; is_leveln_ftree n (Deep uu pr m sf); is_measured_ftree (Deep uu pr m sf); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Deep uu pr m sf)); nsplitTree p i (Deep uu pr m sf) = (l, nd, r); \<not> p (i + gmd pr); \<not> p (i + gmd pr + gmft m)\<rbrakk> \<Longrightarrow> toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
with case1 3
[PROOF STATE]
proof (chain)
picking this:
\<not> p (i + gmd pr)
\<lbrakk>?x = i + gmd pr; ?xa = ?x + gmft m; \<not> p ?x; p ?xa; is_leveln_ftree ?n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p ?x; p (?x + gmft m); nsplitTree p ?x m = (?l, ?nd, ?r)\<rbrakk> \<Longrightarrow> toList m = toList ?l @ nodeToList ?nd @ toList ?r \<and> \<not> p (?x + gmft ?l) \<and> p (?x + gmft ?l + gmn ?nd) \<and> is_leveln_ftree ?n ?l \<and> is_measured_ftree ?l \<and> is_leveln_ftree ?n ?r \<and> is_measured_ftree ?r \<and> is_leveln_node ?n ?nd \<and> is_measured_node ?nd
is_leveln_ftree n (Deep uu pr m sf)
is_measured_ftree (Deep uu pr m sf)
p ?a \<Longrightarrow> p (?a + ?b)
\<not> p i
p (i + gmft (Deep uu pr m sf))
nsplitTree p i (Deep uu pr m sf) = (l, nd, r)
\<not> p (i + gmd pr + gmft m)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> p (i + gmd pr)
\<lbrakk>?x = i + gmd pr; ?xa = ?x + gmft m; \<not> p ?x; p ?xa; is_leveln_ftree ?n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p ?x; p (?x + gmft m); nsplitTree p ?x m = (?l, ?nd, ?r)\<rbrakk> \<Longrightarrow> toList m = toList ?l @ nodeToList ?nd @ toList ?r \<and> \<not> p (?x + gmft ?l) \<and> p (?x + gmft ?l + gmn ?nd) \<and> is_leveln_ftree ?n ?l \<and> is_measured_ftree ?l \<and> is_leveln_ftree ?n ?r \<and> is_measured_ftree ?r \<and> is_leveln_node ?n ?nd \<and> is_measured_node ?nd
is_leveln_ftree n (Deep uu pr m sf)
is_measured_ftree (Deep uu pr m sf)
p ?a \<Longrightarrow> p (?a + ?b)
\<not> p i
p (i + gmft (Deep uu pr m sf))
nsplitTree p i (Deep uu pr m sf) = (l, nd, r)
\<not> p (i + gmd pr + gmft m)

goal (1 subgoal):
 1. toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<not> p (i + gmd pr); \<And>x xa n l nd r. \<lbrakk>x = i + gmd pr; xa = x + gmft m; \<not> p x; p xa; is_leveln_ftree n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> toList m = toList l @ nodeToList nd @ toList r \<and> \<not> p (x + gmft l) \<and> p (x + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd; is_leveln_ftree n (Deep uu pr m sf); is_measured_ftree (Deep uu pr m sf); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Deep uu pr m sf)); nsplitTree p i (Deep uu pr m sf) = (l, nd, r); \<not> p (i + gmd pr + gmft m)\<rbrakk> \<Longrightarrow> toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
obtain l1 x r1 where
          l1xr1: "splitDigit p (i + gmd pr + gmft m) sf = (l1,x,r1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>l1 x r1. splitDigit p (i + gmd pr + gmft m) sf = (l1, x, r1) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases "splitDigit p (i + gmd pr + gmft m) sf", blast)
[PROOF STATE]
proof (state)
this:
splitDigit p (i + gmd pr + gmft m) sf = (l1, x, r1)

goal (1 subgoal):
 1. \<lbrakk>\<not> p (i + gmd pr); \<And>x xa n l nd r. \<lbrakk>x = i + gmd pr; xa = x + gmft m; \<not> p x; p xa; is_leveln_ftree n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> toList m = toList l @ nodeToList nd @ toList r \<and> \<not> p (x + gmft l) \<and> p (x + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd; is_leveln_ftree n (Deep uu pr m sf); is_measured_ftree (Deep uu pr m sf); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Deep uu pr m sf)); nsplitTree p i (Deep uu pr m sf) = (l, nd, r); \<not> p (i + gmd pr + gmft m)\<rbrakk> \<Longrightarrow> toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
with case1 False 3(7)
[PROOF STATE]
proof (chain)
picking this:
\<not> p (i + gmd pr)
\<not> p (i + gmd pr + gmft m)
nsplitTree p i (Deep uu pr m sf) = (l, nd, r)
splitDigit p (i + gmd pr + gmft m) sf = (l1, x, r1)
[PROOF STEP]
have
          v1: "l = deepR pr m l1" "nd = x" "r = nlistToTree r1"
[PROOF STATE]
proof (prove)
using this:
\<not> p (i + gmd pr)
\<not> p (i + gmd pr + gmft m)
nsplitTree p i (Deep uu pr m sf) = (l, nd, r)
splitDigit p (i + gmd pr + gmft m) sf = (l1, x, r1)

goal (1 subgoal):
 1. l = deepR pr m l1 &&& nd = x &&& r = nlistToTree r1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l = deepR pr m l1
nd = x
r = nlistToTree r1

goal (1 subgoal):
 1. \<lbrakk>\<not> p (i + gmd pr); \<And>x xa n l nd r. \<lbrakk>x = i + gmd pr; xa = x + gmft m; \<not> p x; p xa; is_leveln_ftree n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> toList m = toList l @ nodeToList nd @ toList r \<and> \<not> p (x + gmft l) \<and> p (x + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd; is_leveln_ftree n (Deep uu pr m sf); is_measured_ftree (Deep uu pr m sf); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Deep uu pr m sf)); nsplitTree p i (Deep uu pr m sf) = (l, nd, r); \<not> p (i + gmd pr + gmft m)\<rbrakk> \<Longrightarrow> toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
from l1xr1
[PROOF STATE]
proof (chain)
picking this:
splitDigit p (i + gmd pr + gmft m) sf = (l1, x, r1)
[PROOF STEP]
have
          v2: "digitToList sf = nlistToList l1 @ nodeToList x @ nlistToList r1"
          "length l1 \<le> 4" "length r1 \<le> 4"
[PROOF STATE]
proof (prove)
using this:
splitDigit p (i + gmd pr + gmft m) sf = (l1, x, r1)

goal (1 subgoal):
 1. digitToList sf = nlistToList l1 @ nodeToList x @ nlistToList r1 &&& length l1 \<le> 4 &&& length r1 \<le> 4
[PROOF STEP]
by (auto simp add: splitDigit_list)
[PROOF STATE]
proof (state)
this:
digitToList sf = nlistToList l1 @ nodeToList x @ nlistToList r1
length l1 \<le> 4
length r1 \<le> 4

goal (1 subgoal):
 1. \<lbrakk>\<not> p (i + gmd pr); \<And>x xa n l nd r. \<lbrakk>x = i + gmd pr; xa = x + gmft m; \<not> p x; p xa; is_leveln_ftree n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> toList m = toList l @ nodeToList nd @ toList r \<and> \<not> p (x + gmft l) \<and> p (x + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd; is_leveln_ftree n (Deep uu pr m sf); is_measured_ftree (Deep uu pr m sf); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Deep uu pr m sf)); nsplitTree p i (Deep uu pr m sf) = (l, nd, r); \<not> p (i + gmd pr + gmft m)\<rbrakk> \<Longrightarrow> toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
from 3(2,3)
[PROOF STATE]
proof (chain)
picking this:
is_leveln_ftree n (Deep uu pr m sf)
is_measured_ftree (Deep uu pr m sf)
[PROOF STEP]
have
          pr_m_sf_inv: "is_leveln_digit n pr \<and> is_measured_digit pr"
          "is_leveln_ftree (Suc n) m \<and> is_measured_ftree m"
          "is_leveln_digit n sf \<and> is_measured_digit sf"
[PROOF STATE]
proof (prove)
using this:
is_leveln_ftree n (Deep uu pr m sf)
is_measured_ftree (Deep uu pr m sf)

goal (1 subgoal):
 1. is_leveln_digit n pr \<and> is_measured_digit pr &&& is_leveln_ftree (Suc n) m \<and> is_measured_ftree m &&& is_leveln_digit n sf \<and> is_measured_digit sf
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
is_leveln_digit n pr \<and> is_measured_digit pr
is_leveln_ftree (Suc n) m \<and> is_measured_ftree m
is_leveln_digit n sf \<and> is_measured_digit sf

goal (1 subgoal):
 1. \<lbrakk>\<not> p (i + gmd pr); \<And>x xa n l nd r. \<lbrakk>x = i + gmd pr; xa = x + gmft m; \<not> p x; p xa; is_leveln_ftree n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> toList m = toList l @ nodeToList nd @ toList r \<and> \<not> p (x + gmft l) \<and> p (x + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd; is_leveln_ftree n (Deep uu pr m sf); is_measured_ftree (Deep uu pr m sf); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Deep uu pr m sf)); nsplitTree p i (Deep uu pr m sf) = (l, nd, r); \<not> p (i + gmd pr + gmft m)\<rbrakk> \<Longrightarrow> toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
from 3(3,6)
[PROOF STATE]
proof (chain)
picking this:
is_measured_ftree (Deep uu pr m sf)
p (i + gmft (Deep uu pr m sf))
[PROOF STEP]
have
          v7: "p (i + gmd pr + gmft m + gmd sf)"
[PROOF STATE]
proof (prove)
using this:
is_measured_ftree (Deep uu pr m sf)
p (i + gmft (Deep uu pr m sf))

goal (1 subgoal):
 1. p (i + gmd pr + gmft m + gmd sf)
[PROOF STEP]
by (auto simp add: add.assoc)
[PROOF STATE]
proof (state)
this:
p (i + gmd pr + gmft m + gmd sf)

goal (1 subgoal):
 1. \<lbrakk>\<not> p (i + gmd pr); \<And>x xa n l nd r. \<lbrakk>x = i + gmd pr; xa = x + gmft m; \<not> p x; p xa; is_leveln_ftree n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> toList m = toList l @ nodeToList nd @ toList r \<and> \<not> p (x + gmft l) \<and> p (x + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd; is_leveln_ftree n (Deep uu pr m sf); is_measured_ftree (Deep uu pr m sf); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Deep uu pr m sf)); nsplitTree p i (Deep uu pr m sf) = (l, nd, r); \<not> p (i + gmd pr + gmft m)\<rbrakk> \<Longrightarrow> toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
with pr_m_sf_inv 3(4) pr_m_sf_inv(3) case1 False l1xr1
             splitDigit_inv[of p "i + gmd pr + gmft m" sf n l1 x r1]
[PROOF STATE]
proof (chain)
picking this:
is_leveln_digit n pr \<and> is_measured_digit pr
is_leveln_ftree (Suc n) m \<and> is_measured_ftree m
is_leveln_digit n sf \<and> is_measured_digit sf
p ?a \<Longrightarrow> p (?a + ?b)
is_leveln_digit n sf \<and> is_measured_digit sf
\<not> p (i + gmd pr)
\<not> p (i + gmd pr + gmft m)
splitDigit p (i + gmd pr + gmft m) sf = (l1, x, r1)
\<lbrakk>\<And>a b. p a \<Longrightarrow> p (a + b); \<not> p (i + gmd pr + gmft m); is_measured_digit sf; is_leveln_digit n sf; p (i + gmd pr + gmft m + gmd sf); splitDigit p (i + gmd pr + gmft m) sf = (l1, x, r1)\<rbrakk> \<Longrightarrow> \<not> p (i + gmd pr + gmft m + gmnl l1) \<and> p (i + gmd pr + gmft m + gmnl l1 + gmn x) \<and> (\<forall>x\<in>set l1. is_measured_node x \<and> is_leveln_node n x) \<and> (\<forall>x\<in>set r1. is_measured_node x \<and> is_leveln_node n x) \<and> is_measured_node x \<and> is_leveln_node n x
p (i + gmd pr + gmft m + gmd sf)
[PROOF STEP]
have l1_x_r1_inv:
          "\<not> p (i + gmd pr + gmft m + gmnl l1)"
          "p (i + gmd pr + gmft m + gmnl l1 + gmn x)"
          "\<forall> x \<in> set l1. (is_measured_node x \<and> is_leveln_node n x)"
          "\<forall> x \<in> set r1. (is_measured_node x \<and> is_leveln_node n x)"
          "is_measured_node x \<and> is_leveln_node n x"
[PROOF STATE]
proof (prove)
using this:
is_leveln_digit n pr \<and> is_measured_digit pr
is_leveln_ftree (Suc n) m \<and> is_measured_ftree m
is_leveln_digit n sf \<and> is_measured_digit sf
p ?a \<Longrightarrow> p (?a + ?b)
is_leveln_digit n sf \<and> is_measured_digit sf
\<not> p (i + gmd pr)
\<not> p (i + gmd pr + gmft m)
splitDigit p (i + gmd pr + gmft m) sf = (l1, x, r1)
\<lbrakk>\<And>a b. p a \<Longrightarrow> p (a + b); \<not> p (i + gmd pr + gmft m); is_measured_digit sf; is_leveln_digit n sf; p (i + gmd pr + gmft m + gmd sf); splitDigit p (i + gmd pr + gmft m) sf = (l1, x, r1)\<rbrakk> \<Longrightarrow> \<not> p (i + gmd pr + gmft m + gmnl l1) \<and> p (i + gmd pr + gmft m + gmnl l1 + gmn x) \<and> (\<forall>x\<in>set l1. is_measured_node x \<and> is_leveln_node n x) \<and> (\<forall>x\<in>set r1. is_measured_node x \<and> is_leveln_node n x) \<and> is_measured_node x \<and> is_leveln_node n x
p (i + gmd pr + gmft m + gmd sf)

goal (1 subgoal):
 1. (\<not> p (i + gmd pr + gmft m + gmnl l1) &&& p (i + gmd pr + gmft m + gmnl l1 + gmn x)) &&& \<forall>x\<in>set l1. is_measured_node x \<and> is_leveln_node n x &&& \<forall>x\<in>set r1. is_measured_node x \<and> is_leveln_node n x &&& is_measured_node x \<and> is_leveln_node n x
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> p (i + gmd pr + gmft m + gmnl l1)
p (i + gmd pr + gmft m + gmnl l1 + gmn x)
\<forall>x\<in>set l1. is_measured_node x \<and> is_leveln_node n x
\<forall>x\<in>set r1. is_measured_node x \<and> is_leveln_node n x
is_measured_node x \<and> is_leveln_node n x

goal (1 subgoal):
 1. \<lbrakk>\<not> p (i + gmd pr); \<And>x xa n l nd r. \<lbrakk>x = i + gmd pr; xa = x + gmft m; \<not> p x; p xa; is_leveln_ftree n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> toList m = toList l @ nodeToList nd @ toList r \<and> \<not> p (x + gmft l) \<and> p (x + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd; is_leveln_ftree n (Deep uu pr m sf); is_measured_ftree (Deep uu pr m sf); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Deep uu pr m sf)); nsplitTree p i (Deep uu pr m sf) = (l, nd, r); \<not> p (i + gmd pr + gmft m)\<rbrakk> \<Longrightarrow> toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
from v2 v1 l1_x_r1_inv(3) pr_m_sf_inv
[PROOF STATE]
proof (chain)
picking this:
digitToList sf = nlistToList l1 @ nodeToList x @ nlistToList r1
length l1 \<le> 4
length r1 \<le> 4
l = deepR pr m l1
nd = x
r = nlistToTree r1
\<forall>x\<in>set l1. is_measured_node x \<and> is_leveln_node n x
is_leveln_digit n pr \<and> is_measured_digit pr
is_leveln_ftree (Suc n) m \<and> is_measured_ftree m
is_leveln_digit n sf \<and> is_measured_digit sf
[PROOF STEP]
have
          ziel1: "toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r"
[PROOF STATE]
proof (prove)
using this:
digitToList sf = nlistToList l1 @ nodeToList x @ nlistToList r1
length l1 \<le> 4
length r1 \<le> 4
l = deepR pr m l1
nd = x
r = nlistToTree r1
\<forall>x\<in>set l1. is_measured_node x \<and> is_leveln_node n x
is_leveln_digit n pr \<and> is_measured_digit pr
is_leveln_ftree (Suc n) m \<and> is_measured_ftree m
is_leveln_digit n sf \<and> is_measured_digit sf

goal (1 subgoal):
 1. toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r
[PROOF STEP]
by (auto simp add: nlistToTree_list deepR_list)
[PROOF STATE]
proof (state)
this:
toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r

goal (1 subgoal):
 1. \<lbrakk>\<not> p (i + gmd pr); \<And>x xa n l nd r. \<lbrakk>x = i + gmd pr; xa = x + gmft m; \<not> p x; p xa; is_leveln_ftree n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> toList m = toList l @ nodeToList nd @ toList r \<and> \<not> p (x + gmft l) \<and> p (x + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd; is_leveln_ftree n (Deep uu pr m sf); is_measured_ftree (Deep uu pr m sf); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Deep uu pr m sf)); nsplitTree p i (Deep uu pr m sf) = (l, nd, r); \<not> p (i + gmd pr + gmft m)\<rbrakk> \<Longrightarrow> toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
from l1_x_r1_inv(4) v1(3)
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>set r1. is_measured_node x \<and> is_leveln_node n x
r = nlistToTree r1
[PROOF STEP]
have
          v3: "gmft r = gmnl r1"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set r1. is_measured_node x \<and> is_leveln_node n x
r = nlistToTree r1

goal (1 subgoal):
 1. gmft r = gmnl r1
[PROOF STEP]
by (simp add: gmnl_gmft)
[PROOF STATE]
proof (state)
this:
gmft r = gmnl r1

goal (1 subgoal):
 1. \<lbrakk>\<not> p (i + gmd pr); \<And>x xa n l nd r. \<lbrakk>x = i + gmd pr; xa = x + gmft m; \<not> p x; p xa; is_leveln_ftree n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> toList m = toList l @ nodeToList nd @ toList r \<and> \<not> p (x + gmft l) \<and> p (x + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd; is_leveln_ftree n (Deep uu pr m sf); is_measured_ftree (Deep uu pr m sf); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Deep uu pr m sf)); nsplitTree p i (Deep uu pr m sf) = (l, nd, r); \<not> p (i + gmd pr + gmft m)\<rbrakk> \<Longrightarrow> toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
with l1_x_r1_inv(1,2,3) pr_m_sf_inv v1 v2
[PROOF STATE]
proof (chain)
picking this:
\<not> p (i + gmd pr + gmft m + gmnl l1)
p (i + gmd pr + gmft m + gmnl l1 + gmn x)
\<forall>x\<in>set l1. is_measured_node x \<and> is_leveln_node n x
is_leveln_digit n pr \<and> is_measured_digit pr
is_leveln_ftree (Suc n) m \<and> is_measured_ftree m
is_leveln_digit n sf \<and> is_measured_digit sf
l = deepR pr m l1
nd = x
r = nlistToTree r1
digitToList sf = nlistToList l1 @ nodeToList x @ nlistToList r1
length l1 \<le> 4
length r1 \<le> 4
gmft r = gmnl r1
[PROOF STEP]
have
          ziel2: " \<not> p (i + gmft l)"
          "p (i + gmft l + gmn nd)"
[PROOF STATE]
proof (prove)
using this:
\<not> p (i + gmd pr + gmft m + gmnl l1)
p (i + gmd pr + gmft m + gmnl l1 + gmn x)
\<forall>x\<in>set l1. is_measured_node x \<and> is_leveln_node n x
is_leveln_digit n pr \<and> is_measured_digit pr
is_leveln_ftree (Suc n) m \<and> is_measured_ftree m
is_leveln_digit n sf \<and> is_measured_digit sf
l = deepR pr m l1
nd = x
r = nlistToTree r1
digitToList sf = nlistToList l1 @ nodeToList x @ nlistToList r1
length l1 \<le> 4
length r1 \<le> 4
gmft r = gmnl r1

goal (1 subgoal):
 1. \<not> p (i + gmft l) &&& p (i + gmft l + gmn nd)
[PROOF STEP]
by (auto simp add: gmftR_gmnl add.assoc)
[PROOF STATE]
proof (state)
this:
\<not> p (i + gmft l)
p (i + gmft l + gmn nd)

goal (1 subgoal):
 1. \<lbrakk>\<not> p (i + gmd pr); \<And>x xa n l nd r. \<lbrakk>x = i + gmd pr; xa = x + gmft m; \<not> p x; p xa; is_leveln_ftree n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> toList m = toList l @ nodeToList nd @ toList r \<and> \<not> p (x + gmft l) \<and> p (x + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd; is_leveln_ftree n (Deep uu pr m sf); is_measured_ftree (Deep uu pr m sf); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Deep uu pr m sf)); nsplitTree p i (Deep uu pr m sf) = (l, nd, r); \<not> p (i + gmd pr + gmft m)\<rbrakk> \<Longrightarrow> toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
from l1_x_r1_inv(3,4,5) v1 v2(2) pr_m_sf_inv
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>set l1. is_measured_node x \<and> is_leveln_node n x
\<forall>x\<in>set r1. is_measured_node x \<and> is_leveln_node n x
is_measured_node x \<and> is_leveln_node n x
l = deepR pr m l1
nd = x
r = nlistToTree r1
length l1 \<le> 4
is_leveln_digit n pr \<and> is_measured_digit pr
is_leveln_ftree (Suc n) m \<and> is_measured_ftree m
is_leveln_digit n sf \<and> is_measured_digit sf
[PROOF STEP]
have
          ziel3: "is_leveln_ftree n l \<and> is_measured_ftree l \<and>
          is_leveln_ftree n r \<and> is_measured_ftree r \<and>
          is_leveln_node n nd \<and> is_measured_node nd"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set l1. is_measured_node x \<and> is_leveln_node n x
\<forall>x\<in>set r1. is_measured_node x \<and> is_leveln_node n x
is_measured_node x \<and> is_leveln_node n x
l = deepR pr m l1
nd = x
r = nlistToTree r1
length l1 \<le> 4
is_leveln_digit n pr \<and> is_measured_digit pr
is_leveln_ftree (Suc n) m \<and> is_measured_ftree m
is_leveln_digit n sf \<and> is_measured_digit sf

goal (1 subgoal):
 1. is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
by (auto simp add: nlistToTree_inv deepR_inv)
[PROOF STATE]
proof (state)
this:
is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd

goal (1 subgoal):
 1. \<lbrakk>\<not> p (i + gmd pr); \<And>x xa n l nd r. \<lbrakk>x = i + gmd pr; xa = x + gmft m; \<not> p x; p xa; is_leveln_ftree n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> toList m = toList l @ nodeToList nd @ toList r \<and> \<not> p (x + gmft l) \<and> p (x + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd; is_leveln_ftree n (Deep uu pr m sf); is_measured_ftree (Deep uu pr m sf); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Deep uu pr m sf)); nsplitTree p i (Deep uu pr m sf) = (l, nd, r); \<not> p (i + gmd pr + gmft m)\<rbrakk> \<Longrightarrow> toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
from ziel1 ziel2 ziel3
[PROOF STATE]
proof (chain)
picking this:
toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r
\<not> p (i + gmft l)
p (i + gmft l + gmn nd)
is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r
\<not> p (i + gmft l)
p (i + gmft l + gmn nd)
is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd

goal (1 subgoal):
 1. toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd

goal (1 subgoal):
 1. \<lbrakk>\<And>x xa n l nd r. \<lbrakk>x = i + gmd pr; xa = x + gmft m; \<not> p x; p xa; is_leveln_ftree n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> toList m = toList l @ nodeToList nd @ toList r \<and> \<not> p (x + gmft l) \<and> p (x + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd; is_leveln_ftree n (Deep uu pr m sf); is_measured_ftree (Deep uu pr m sf); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Deep uu pr m sf)); nsplitTree p i (Deep uu pr m sf) = (l, nd, r); \<not> p (i + gmd pr); p (i + gmd pr + gmft m)\<rbrakk> \<Longrightarrow> toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<And>x xa n l nd r. \<lbrakk>x = i + gmd pr; xa = x + gmft m; \<not> p x; p xa; is_leveln_ftree n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> toList m = toList l @ nodeToList nd @ toList r \<and> \<not> p (x + gmft l) \<and> p (x + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd; is_leveln_ftree n (Deep uu pr m sf); is_measured_ftree (Deep uu pr m sf); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Deep uu pr m sf)); nsplitTree p i (Deep uu pr m sf) = (l, nd, r); \<not> p (i + gmd pr); p (i + gmd pr + gmft m)\<rbrakk> \<Longrightarrow> toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
case True
[PROOF STATE]
proof (state)
this:
p (i + gmd pr + gmft m)

goal (1 subgoal):
 1. \<lbrakk>\<And>x xa n l nd r. \<lbrakk>x = i + gmd pr; xa = x + gmft m; \<not> p x; p xa; is_leveln_ftree n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> toList m = toList l @ nodeToList nd @ toList r \<and> \<not> p (x + gmft l) \<and> p (x + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd; is_leveln_ftree n (Deep uu pr m sf); is_measured_ftree (Deep uu pr m sf); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Deep uu pr m sf)); nsplitTree p i (Deep uu pr m sf) = (l, nd, r); \<not> p (i + gmd pr); p (i + gmd pr + gmft m)\<rbrakk> \<Longrightarrow> toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
with case1 3
[PROOF STATE]
proof (chain)
picking this:
\<not> p (i + gmd pr)
\<lbrakk>?x = i + gmd pr; ?xa = ?x + gmft m; \<not> p ?x; p ?xa; is_leveln_ftree ?n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p ?x; p (?x + gmft m); nsplitTree p ?x m = (?l, ?nd, ?r)\<rbrakk> \<Longrightarrow> toList m = toList ?l @ nodeToList ?nd @ toList ?r \<and> \<not> p (?x + gmft ?l) \<and> p (?x + gmft ?l + gmn ?nd) \<and> is_leveln_ftree ?n ?l \<and> is_measured_ftree ?l \<and> is_leveln_ftree ?n ?r \<and> is_measured_ftree ?r \<and> is_leveln_node ?n ?nd \<and> is_measured_node ?nd
is_leveln_ftree n (Deep uu pr m sf)
is_measured_ftree (Deep uu pr m sf)
p ?a \<Longrightarrow> p (?a + ?b)
\<not> p i
p (i + gmft (Deep uu pr m sf))
nsplitTree p i (Deep uu pr m sf) = (l, nd, r)
p (i + gmd pr + gmft m)
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> p (i + gmd pr)
\<lbrakk>?x = i + gmd pr; ?xa = ?x + gmft m; \<not> p ?x; p ?xa; is_leveln_ftree ?n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p ?x; p (?x + gmft m); nsplitTree p ?x m = (?l, ?nd, ?r)\<rbrakk> \<Longrightarrow> toList m = toList ?l @ nodeToList ?nd @ toList ?r \<and> \<not> p (?x + gmft ?l) \<and> p (?x + gmft ?l + gmn ?nd) \<and> is_leveln_ftree ?n ?l \<and> is_measured_ftree ?l \<and> is_leveln_ftree ?n ?r \<and> is_measured_ftree ?r \<and> is_leveln_node ?n ?nd \<and> is_measured_node ?nd
is_leveln_ftree n (Deep uu pr m sf)
is_measured_ftree (Deep uu pr m sf)
p ?a \<Longrightarrow> p (?a + ?b)
\<not> p i
p (i + gmft (Deep uu pr m sf))
nsplitTree p i (Deep uu pr m sf) = (l, nd, r)
p (i + gmd pr + gmft m)

goal (1 subgoal):
 1. toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<lbrakk>\<not> p (i + gmd pr); \<And>x xa n l nd r. \<lbrakk>x = i + gmd pr; xa = x + gmft m; \<not> p x; p xa; is_leveln_ftree n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> toList m = toList l @ nodeToList nd @ toList r \<and> \<not> p (x + gmft l) \<and> p (x + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd; is_leveln_ftree n (Deep uu pr m sf); is_measured_ftree (Deep uu pr m sf); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Deep uu pr m sf)); nsplitTree p i (Deep uu pr m sf) = (l, nd, r); p (i + gmd pr + gmft m)\<rbrakk> \<Longrightarrow> toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
obtain l1 x r1 where
          l1_x_r1 :"nsplitTree p (i + gmd pr) m = (l1, x, r1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>l1 x r1. nsplitTree p (i + gmd pr) m = (l1, x, r1) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases "nsplitTree p (i + gmd pr) m") blast
[PROOF STATE]
proof (state)
this:
nsplitTree p (i + gmd pr) m = (l1, x, r1)

goal (1 subgoal):
 1. \<lbrakk>\<not> p (i + gmd pr); \<And>x xa n l nd r. \<lbrakk>x = i + gmd pr; xa = x + gmft m; \<not> p x; p xa; is_leveln_ftree n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> toList m = toList l @ nodeToList nd @ toList r \<and> \<not> p (x + gmft l) \<and> p (x + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd; is_leveln_ftree n (Deep uu pr m sf); is_measured_ftree (Deep uu pr m sf); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Deep uu pr m sf)); nsplitTree p i (Deep uu pr m sf) = (l, nd, r); p (i + gmd pr + gmft m)\<rbrakk> \<Longrightarrow> toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
from 3(2,3)
[PROOF STATE]
proof (chain)
picking this:
is_leveln_ftree n (Deep uu pr m sf)
is_measured_ftree (Deep uu pr m sf)
[PROOF STEP]
have
          pr_m_sf_inv: "is_leveln_digit n pr \<and> is_measured_digit pr"
          "is_leveln_ftree (Suc n) m \<and> is_measured_ftree m"
          "is_leveln_digit n sf \<and> is_measured_digit sf"
[PROOF STATE]
proof (prove)
using this:
is_leveln_ftree n (Deep uu pr m sf)
is_measured_ftree (Deep uu pr m sf)

goal (1 subgoal):
 1. is_leveln_digit n pr \<and> is_measured_digit pr &&& is_leveln_ftree (Suc n) m \<and> is_measured_ftree m &&& is_leveln_digit n sf \<and> is_measured_digit sf
[PROOF STEP]
by simp_all
[PROOF STATE]
proof (state)
this:
is_leveln_digit n pr \<and> is_measured_digit pr
is_leveln_ftree (Suc n) m \<and> is_measured_ftree m
is_leveln_digit n sf \<and> is_measured_digit sf

goal (1 subgoal):
 1. \<lbrakk>\<not> p (i + gmd pr); \<And>x xa n l nd r. \<lbrakk>x = i + gmd pr; xa = x + gmft m; \<not> p x; p xa; is_leveln_ftree n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> toList m = toList l @ nodeToList nd @ toList r \<and> \<not> p (x + gmft l) \<and> p (x + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd; is_leveln_ftree n (Deep uu pr m sf); is_measured_ftree (Deep uu pr m sf); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Deep uu pr m sf)); nsplitTree p i (Deep uu pr m sf) = (l, nd, r); p (i + gmd pr + gmft m)\<rbrakk> \<Longrightarrow> toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
with True case1
          "3.hyps"[of "i + gmd pr" "i + gmd pr + gmft m" "Suc n" l1 x r1]
          3(4) l1_x_r1
[PROOF STATE]
proof (chain)
picking this:
p (i + gmd pr + gmft m)
\<not> p (i + gmd pr)
\<lbrakk>i + gmd pr = i + gmd pr; i + gmd pr + gmft m = i + gmd pr + gmft m; \<not> p (i + gmd pr); p (i + gmd pr + gmft m); is_leveln_ftree (Suc n) m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p (i + gmd pr); p (i + gmd pr + gmft m); nsplitTree p (i + gmd pr) m = (l1, x, r1)\<rbrakk> \<Longrightarrow> toList m = toList l1 @ nodeToList x @ toList r1 \<and> \<not> p (i + gmd pr + gmft l1) \<and> p (i + gmd pr + gmft l1 + gmn x) \<and> is_leveln_ftree (Suc n) l1 \<and> is_measured_ftree l1 \<and> is_leveln_ftree (Suc n) r1 \<and> is_measured_ftree r1 \<and> is_leveln_node (Suc n) x \<and> is_measured_node x
p ?a \<Longrightarrow> p (?a + ?b)
nsplitTree p (i + gmd pr) m = (l1, x, r1)
is_leveln_digit n pr \<and> is_measured_digit pr
is_leveln_ftree (Suc n) m \<and> is_measured_ftree m
is_leveln_digit n sf \<and> is_measured_digit sf
[PROOF STEP]
have l1_x_r1_inv:
          "\<not> p (i + gmd pr + gmft l1)"
          "p (i + gmd pr + gmft l1 + gmn x)"
          "is_leveln_ftree (Suc n) l1 \<and> is_measured_ftree l1"
          "is_leveln_ftree (Suc n) r1 \<and> is_measured_ftree r1"
          "is_leveln_node (Suc n) x \<and> is_measured_node x"
          and l1_x_r1_list:
          "toList m = toList l1 @ nodeToList x @ toList r1"
[PROOF STATE]
proof (prove)
using this:
p (i + gmd pr + gmft m)
\<not> p (i + gmd pr)
\<lbrakk>i + gmd pr = i + gmd pr; i + gmd pr + gmft m = i + gmd pr + gmft m; \<not> p (i + gmd pr); p (i + gmd pr + gmft m); is_leveln_ftree (Suc n) m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p (i + gmd pr); p (i + gmd pr + gmft m); nsplitTree p (i + gmd pr) m = (l1, x, r1)\<rbrakk> \<Longrightarrow> toList m = toList l1 @ nodeToList x @ toList r1 \<and> \<not> p (i + gmd pr + gmft l1) \<and> p (i + gmd pr + gmft l1 + gmn x) \<and> is_leveln_ftree (Suc n) l1 \<and> is_measured_ftree l1 \<and> is_leveln_ftree (Suc n) r1 \<and> is_measured_ftree r1 \<and> is_leveln_node (Suc n) x \<and> is_measured_node x
p ?a \<Longrightarrow> p (?a + ?b)
nsplitTree p (i + gmd pr) m = (l1, x, r1)
is_leveln_digit n pr \<and> is_measured_digit pr
is_leveln_ftree (Suc n) m \<and> is_measured_ftree m
is_leveln_digit n sf \<and> is_measured_digit sf

goal (1 subgoal):
 1. ((\<not> p (i + gmd pr + gmft l1) &&& p (i + gmd pr + gmft l1 + gmn x)) &&& is_leveln_ftree (Suc n) l1 \<and> is_measured_ftree l1 &&& is_leveln_ftree (Suc n) r1 \<and> is_measured_ftree r1 &&& is_leveln_node (Suc n) x \<and> is_measured_node x) &&& toList m = toList l1 @ nodeToList x @ toList r1
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
\<not> p (i + gmd pr + gmft l1)
p (i + gmd pr + gmft l1 + gmn x)
is_leveln_ftree (Suc n) l1 \<and> is_measured_ftree l1
is_leveln_ftree (Suc n) r1 \<and> is_measured_ftree r1
is_leveln_node (Suc n) x \<and> is_measured_node x
toList m = toList l1 @ nodeToList x @ toList r1

goal (1 subgoal):
 1. \<lbrakk>\<not> p (i + gmd pr); \<And>x xa n l nd r. \<lbrakk>x = i + gmd pr; xa = x + gmft m; \<not> p x; p xa; is_leveln_ftree n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> toList m = toList l @ nodeToList nd @ toList r \<and> \<not> p (x + gmft l) \<and> p (x + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd; is_leveln_ftree n (Deep uu pr m sf); is_measured_ftree (Deep uu pr m sf); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Deep uu pr m sf)); nsplitTree p i (Deep uu pr m sf) = (l, nd, r); p (i + gmd pr + gmft m)\<rbrakk> \<Longrightarrow> toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
obtain l2 x2 r2 where l2_x2_r2:
          "splitDigit p (i + gmd pr + gmft l1) (nodeToDigit x) = (l2,x2,r2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>l2 x2 r2. splitDigit p (i + gmd pr + gmft l1) (nodeToDigit x) = (l2, x2, r2) \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by (cases "splitDigit p (i + gmd pr + gmft l1) (nodeToDigit x)",blast)
[PROOF STATE]
proof (state)
this:
splitDigit p (i + gmd pr + gmft l1) (nodeToDigit x) = (l2, x2, r2)

goal (1 subgoal):
 1. \<lbrakk>\<not> p (i + gmd pr); \<And>x xa n l nd r. \<lbrakk>x = i + gmd pr; xa = x + gmft m; \<not> p x; p xa; is_leveln_ftree n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> toList m = toList l @ nodeToList nd @ toList r \<and> \<not> p (x + gmft l) \<and> p (x + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd; is_leveln_ftree n (Deep uu pr m sf); is_measured_ftree (Deep uu pr m sf); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Deep uu pr m sf)); nsplitTree p i (Deep uu pr m sf) = (l, nd, r); p (i + gmd pr + gmft m)\<rbrakk> \<Longrightarrow> toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
from l1_x_r1_inv(2,5)
[PROOF STATE]
proof (chain)
picking this:
p (i + gmd pr + gmft l1 + gmn x)
is_leveln_node (Suc n) x \<and> is_measured_node x
[PROOF STEP]
have
          ndx_inv: "is_leveln_digit n (nodeToDigit x) \<and>
          is_measured_digit (nodeToDigit x)"
          "p (i + gmd pr + gmft l1 + gmd (nodeToDigit x))"
[PROOF STATE]
proof (prove)
using this:
p (i + gmd pr + gmft l1 + gmn x)
is_leveln_node (Suc n) x \<and> is_measured_node x

goal (1 subgoal):
 1. is_leveln_digit n (nodeToDigit x) \<and> is_measured_digit (nodeToDigit x) &&& p (i + gmd pr + gmft l1 + gmd (nodeToDigit x))
[PROOF STEP]
by (auto simp add: nodeToDigit_inv gmn_gmd)
[PROOF STATE]
proof (state)
this:
is_leveln_digit n (nodeToDigit x) \<and> is_measured_digit (nodeToDigit x)
p (i + gmd pr + gmft l1 + gmd (nodeToDigit x))

goal (1 subgoal):
 1. \<lbrakk>\<not> p (i + gmd pr); \<And>x xa n l nd r. \<lbrakk>x = i + gmd pr; xa = x + gmft m; \<not> p x; p xa; is_leveln_ftree n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> toList m = toList l @ nodeToList nd @ toList r \<and> \<not> p (x + gmft l) \<and> p (x + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd; is_leveln_ftree n (Deep uu pr m sf); is_measured_ftree (Deep uu pr m sf); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Deep uu pr m sf)); nsplitTree p i (Deep uu pr m sf) = (l, nd, r); p (i + gmd pr + gmft m)\<rbrakk> \<Longrightarrow> toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
note spdi = splitDigit_inv[of p "i + gmd pr + gmft l1"
                                      "nodeToDigit x" n l2 x2 r2]
[PROOF STATE]
proof (state)
this:
\<lbrakk>\<And>a b. p a \<Longrightarrow> p (a + b); \<not> p (i + gmd pr + gmft l1); is_measured_digit (nodeToDigit x); is_leveln_digit n (nodeToDigit x); p (i + gmd pr + gmft l1 + gmd (nodeToDigit x)); splitDigit p (i + gmd pr + gmft l1) (nodeToDigit x) = (l2, x2, r2)\<rbrakk> \<Longrightarrow> \<not> p (i + gmd pr + gmft l1 + gmnl l2) \<and> p (i + gmd pr + gmft l1 + gmnl l2 + gmn x2) \<and> (\<forall>x\<in>set l2. is_measured_node x \<and> is_leveln_node n x) \<and> (\<forall>x\<in>set r2. is_measured_node x \<and> is_leveln_node n x) \<and> is_measured_node x2 \<and> is_leveln_node n x2

goal (1 subgoal):
 1. \<lbrakk>\<not> p (i + gmd pr); \<And>x xa n l nd r. \<lbrakk>x = i + gmd pr; xa = x + gmft m; \<not> p x; p xa; is_leveln_ftree n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> toList m = toList l @ nodeToList nd @ toList r \<and> \<not> p (x + gmft l) \<and> p (x + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd; is_leveln_ftree n (Deep uu pr m sf); is_measured_ftree (Deep uu pr m sf); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Deep uu pr m sf)); nsplitTree p i (Deep uu pr m sf) = (l, nd, r); p (i + gmd pr + gmft m)\<rbrakk> \<Longrightarrow> toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
from ndx_inv l1_x_r1_inv(1) l2_x2_r2 3(4)
[PROOF STATE]
proof (chain)
picking this:
is_leveln_digit n (nodeToDigit x) \<and> is_measured_digit (nodeToDigit x)
p (i + gmd pr + gmft l1 + gmd (nodeToDigit x))
\<not> p (i + gmd pr + gmft l1)
splitDigit p (i + gmd pr + gmft l1) (nodeToDigit x) = (l2, x2, r2)
p ?a \<Longrightarrow> p (?a + ?b)
[PROOF STEP]
have
          l2_x2_r2_inv:"\<not> p (i + gmd pr + gmft l1 + gmnl l2)"
          "p (i + gmd pr + gmft l1 + gmnl l2 + gmn x2)"
          "\<forall>x\<in>set l2. is_measured_node x \<and> is_leveln_node n x"
          "\<forall>x\<in>set r2. is_measured_node x \<and> is_leveln_node n x"
          "is_measured_node x2 \<and> is_leveln_node n x2"
[PROOF STATE]
proof (prove)
using this:
is_leveln_digit n (nodeToDigit x) \<and> is_measured_digit (nodeToDigit x)
p (i + gmd pr + gmft l1 + gmd (nodeToDigit x))
\<not> p (i + gmd pr + gmft l1)
splitDigit p (i + gmd pr + gmft l1) (nodeToDigit x) = (l2, x2, r2)
p ?a \<Longrightarrow> p (?a + ?b)

goal (1 subgoal):
 1. (\<not> p (i + gmd pr + gmft l1 + gmnl l2) &&& p (i + gmd pr + gmft l1 + gmnl l2 + gmn x2)) &&& \<forall>x\<in>set l2. is_measured_node x \<and> is_leveln_node n x &&& \<forall>x\<in>set r2. is_measured_node x \<and> is_leveln_node n x &&& is_measured_node x2 \<and> is_leveln_node n x2
[PROOF STEP]
by (auto simp add: spdi)
[PROOF STATE]
proof (state)
this:
\<not> p (i + gmd pr + gmft l1 + gmnl l2)
p (i + gmd pr + gmft l1 + gmnl l2 + gmn x2)
\<forall>x\<in>set l2. is_measured_node x \<and> is_leveln_node n x
\<forall>x\<in>set r2. is_measured_node x \<and> is_leveln_node n x
is_measured_node x2 \<and> is_leveln_node n x2

goal (1 subgoal):
 1. \<lbrakk>\<not> p (i + gmd pr); \<And>x xa n l nd r. \<lbrakk>x = i + gmd pr; xa = x + gmft m; \<not> p x; p xa; is_leveln_ftree n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> toList m = toList l @ nodeToList nd @ toList r \<and> \<not> p (x + gmft l) \<and> p (x + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd; is_leveln_ftree n (Deep uu pr m sf); is_measured_ftree (Deep uu pr m sf); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Deep uu pr m sf)); nsplitTree p i (Deep uu pr m sf) = (l, nd, r); p (i + gmd pr + gmft m)\<rbrakk> \<Longrightarrow> toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
note spdl =  splitDigit_list[of p "i + gmd pr + gmft l1"
                                        "nodeToDigit x" l2 x2 r2]
[PROOF STATE]
proof (state)
this:
splitDigit p (i + gmd pr + gmft l1) (nodeToDigit x) = (l2, x2, r2) \<Longrightarrow> digitToList (nodeToDigit x) = nlistToList l2 @ nodeToList x2 @ nlistToList r2 \<and> length l2 \<le> 4 \<and> length r2 \<le> 4

goal (1 subgoal):
 1. \<lbrakk>\<not> p (i + gmd pr); \<And>x xa n l nd r. \<lbrakk>x = i + gmd pr; xa = x + gmft m; \<not> p x; p xa; is_leveln_ftree n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> toList m = toList l @ nodeToList nd @ toList r \<and> \<not> p (x + gmft l) \<and> p (x + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd; is_leveln_ftree n (Deep uu pr m sf); is_measured_ftree (Deep uu pr m sf); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Deep uu pr m sf)); nsplitTree p i (Deep uu pr m sf) = (l, nd, r); p (i + gmd pr + gmft m)\<rbrakk> \<Longrightarrow> toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
from l2_x2_r2
[PROOF STATE]
proof (chain)
picking this:
splitDigit p (i + gmd pr + gmft l1) (nodeToDigit x) = (l2, x2, r2)
[PROOF STEP]
have
          l2_x2_r2_list:
          "digitToList (nodeToDigit x) =
            nlistToList l2 @ nodeToList x2 @ nlistToList r2"
          "length l2 \<le> 4 \<and> length r2 \<le> 4"
[PROOF STATE]
proof (prove)
using this:
splitDigit p (i + gmd pr + gmft l1) (nodeToDigit x) = (l2, x2, r2)

goal (1 subgoal):
 1. digitToList (nodeToDigit x) = nlistToList l2 @ nodeToList x2 @ nlistToList r2 &&& length l2 \<le> 4 \<and> length r2 \<le> 4
[PROOF STEP]
by (auto simp add: spdl)
[PROOF STATE]
proof (state)
this:
digitToList (nodeToDigit x) = nlistToList l2 @ nodeToList x2 @ nlistToList r2
length l2 \<le> 4 \<and> length r2 \<le> 4

goal (1 subgoal):
 1. \<lbrakk>\<not> p (i + gmd pr); \<And>x xa n l nd r. \<lbrakk>x = i + gmd pr; xa = x + gmft m; \<not> p x; p xa; is_leveln_ftree n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> toList m = toList l @ nodeToList nd @ toList r \<and> \<not> p (x + gmft l) \<and> p (x + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd; is_leveln_ftree n (Deep uu pr m sf); is_measured_ftree (Deep uu pr m sf); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Deep uu pr m sf)); nsplitTree p i (Deep uu pr m sf) = (l, nd, r); p (i + gmd pr + gmft m)\<rbrakk> \<Longrightarrow> toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
from case1 True 3(7) l1_x_r1 l2_x2_r2
[PROOF STATE]
proof (chain)
picking this:
\<not> p (i + gmd pr)
p (i + gmd pr + gmft m)
nsplitTree p i (Deep uu pr m sf) = (l, nd, r)
nsplitTree p (i + gmd pr) m = (l1, x, r1)
splitDigit p (i + gmd pr + gmft l1) (nodeToDigit x) = (l2, x2, r2)
[PROOF STEP]
have
          l_nd_r:
          "l = deepR pr l1 l2"
          "nd = x2"
          "r = deepL r2 r1 sf"
[PROOF STATE]
proof (prove)
using this:
\<not> p (i + gmd pr)
p (i + gmd pr + gmft m)
nsplitTree p i (Deep uu pr m sf) = (l, nd, r)
nsplitTree p (i + gmd pr) m = (l1, x, r1)
splitDigit p (i + gmd pr + gmft l1) (nodeToDigit x) = (l2, x2, r2)

goal (1 subgoal):
 1. l = deepR pr l1 l2 &&& nd = x2 &&& r = deepL r2 r1 sf
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
l = deepR pr l1 l2
nd = x2
r = deepL r2 r1 sf

goal (1 subgoal):
 1. \<lbrakk>\<not> p (i + gmd pr); \<And>x xa n l nd r. \<lbrakk>x = i + gmd pr; xa = x + gmft m; \<not> p x; p xa; is_leveln_ftree n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> toList m = toList l @ nodeToList nd @ toList r \<and> \<not> p (x + gmft l) \<and> p (x + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd; is_leveln_ftree n (Deep uu pr m sf); is_measured_ftree (Deep uu pr m sf); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Deep uu pr m sf)); nsplitTree p i (Deep uu pr m sf) = (l, nd, r); p (i + gmd pr + gmft m)\<rbrakk> \<Longrightarrow> toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
note dr1 = deepR_inv[OF l1_x_r1_inv(3) pr_m_sf_inv(1)]
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set ?sf. (is_measured_node x \<and> is_leveln_node n x) \<and> length ?sf \<le> 4 \<Longrightarrow> is_leveln_ftree n (deepR pr l1 ?sf) \<and> is_measured_ftree (deepR pr l1 ?sf)

goal (1 subgoal):
 1. \<lbrakk>\<not> p (i + gmd pr); \<And>x xa n l nd r. \<lbrakk>x = i + gmd pr; xa = x + gmft m; \<not> p x; p xa; is_leveln_ftree n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> toList m = toList l @ nodeToList nd @ toList r \<and> \<not> p (x + gmft l) \<and> p (x + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd; is_leveln_ftree n (Deep uu pr m sf); is_measured_ftree (Deep uu pr m sf); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Deep uu pr m sf)); nsplitTree p i (Deep uu pr m sf) = (l, nd, r); p (i + gmd pr + gmft m)\<rbrakk> \<Longrightarrow> toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
from dr1 l2_x2_r2_inv(3) l2_x2_r2_list(2) l_nd_r
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>set ?sf. (is_measured_node x \<and> is_leveln_node n x) \<and> length ?sf \<le> 4 \<Longrightarrow> is_leveln_ftree n (deepR pr l1 ?sf) \<and> is_measured_ftree (deepR pr l1 ?sf)
\<forall>x\<in>set l2. is_measured_node x \<and> is_leveln_node n x
length l2 \<le> 4 \<and> length r2 \<le> 4
l = deepR pr l1 l2
nd = x2
r = deepL r2 r1 sf
[PROOF STEP]
have
          l_inv: "is_leveln_ftree n l \<and> is_measured_ftree l"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set ?sf. (is_measured_node x \<and> is_leveln_node n x) \<and> length ?sf \<le> 4 \<Longrightarrow> is_leveln_ftree n (deepR pr l1 ?sf) \<and> is_measured_ftree (deepR pr l1 ?sf)
\<forall>x\<in>set l2. is_measured_node x \<and> is_leveln_node n x
length l2 \<le> 4 \<and> length r2 \<le> 4
l = deepR pr l1 l2
nd = x2
r = deepL r2 r1 sf

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

goal (1 subgoal):
 1. \<lbrakk>\<not> p (i + gmd pr); \<And>x xa n l nd r. \<lbrakk>x = i + gmd pr; xa = x + gmft m; \<not> p x; p xa; is_leveln_ftree n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> toList m = toList l @ nodeToList nd @ toList r \<and> \<not> p (x + gmft l) \<and> p (x + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd; is_leveln_ftree n (Deep uu pr m sf); is_measured_ftree (Deep uu pr m sf); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Deep uu pr m sf)); nsplitTree p i (Deep uu pr m sf) = (l, nd, r); p (i + gmd pr + gmft m)\<rbrakk> \<Longrightarrow> toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
note dl1 = deepL_inv[OF l1_x_r1_inv(4) pr_m_sf_inv(3)]
[PROOF STATE]
proof (state)
this:
\<forall>x\<in>set ?pr. (is_measured_node x \<and> is_leveln_node n x) \<and> length ?pr \<le> 4 \<Longrightarrow> is_leveln_ftree n (deepL ?pr r1 sf) \<and> is_measured_ftree (deepL ?pr r1 sf)

goal (1 subgoal):
 1. \<lbrakk>\<not> p (i + gmd pr); \<And>x xa n l nd r. \<lbrakk>x = i + gmd pr; xa = x + gmft m; \<not> p x; p xa; is_leveln_ftree n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> toList m = toList l @ nodeToList nd @ toList r \<and> \<not> p (x + gmft l) \<and> p (x + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd; is_leveln_ftree n (Deep uu pr m sf); is_measured_ftree (Deep uu pr m sf); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Deep uu pr m sf)); nsplitTree p i (Deep uu pr m sf) = (l, nd, r); p (i + gmd pr + gmft m)\<rbrakk> \<Longrightarrow> toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
from dl1 l2_x2_r2_inv(4) l2_x2_r2_list(2) l_nd_r
[PROOF STATE]
proof (chain)
picking this:
\<forall>x\<in>set ?pr. (is_measured_node x \<and> is_leveln_node n x) \<and> length ?pr \<le> 4 \<Longrightarrow> is_leveln_ftree n (deepL ?pr r1 sf) \<and> is_measured_ftree (deepL ?pr r1 sf)
\<forall>x\<in>set r2. is_measured_node x \<and> is_leveln_node n x
length l2 \<le> 4 \<and> length r2 \<le> 4
l = deepR pr l1 l2
nd = x2
r = deepL r2 r1 sf
[PROOF STEP]
have
          r_inv: "is_leveln_ftree n r \<and> is_measured_ftree r"
[PROOF STATE]
proof (prove)
using this:
\<forall>x\<in>set ?pr. (is_measured_node x \<and> is_leveln_node n x) \<and> length ?pr \<le> 4 \<Longrightarrow> is_leveln_ftree n (deepL ?pr r1 sf) \<and> is_measured_ftree (deepL ?pr r1 sf)
\<forall>x\<in>set r2. is_measured_node x \<and> is_leveln_node n x
length l2 \<le> 4 \<and> length r2 \<le> 4
l = deepR pr l1 l2
nd = x2
r = deepL r2 r1 sf

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

goal (1 subgoal):
 1. \<lbrakk>\<not> p (i + gmd pr); \<And>x xa n l nd r. \<lbrakk>x = i + gmd pr; xa = x + gmft m; \<not> p x; p xa; is_leveln_ftree n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> toList m = toList l @ nodeToList nd @ toList r \<and> \<not> p (x + gmft l) \<and> p (x + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd; is_leveln_ftree n (Deep uu pr m sf); is_measured_ftree (Deep uu pr m sf); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Deep uu pr m sf)); nsplitTree p i (Deep uu pr m sf) = (l, nd, r); p (i + gmd pr + gmft m)\<rbrakk> \<Longrightarrow> toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
from l2_x2_r2_inv l_nd_r
[PROOF STATE]
proof (chain)
picking this:
\<not> p (i + gmd pr + gmft l1 + gmnl l2)
p (i + gmd pr + gmft l1 + gmnl l2 + gmn x2)
\<forall>x\<in>set l2. is_measured_node x \<and> is_leveln_node n x
\<forall>x\<in>set r2. is_measured_node x \<and> is_leveln_node n x
is_measured_node x2 \<and> is_leveln_node n x2
l = deepR pr l1 l2
nd = x2
r = deepL r2 r1 sf
[PROOF STEP]
have
          nd_inv: "is_leveln_node n nd \<and> is_measured_node nd"
[PROOF STATE]
proof (prove)
using this:
\<not> p (i + gmd pr + gmft l1 + gmnl l2)
p (i + gmd pr + gmft l1 + gmnl l2 + gmn x2)
\<forall>x\<in>set l2. is_measured_node x \<and> is_leveln_node n x
\<forall>x\<in>set r2. is_measured_node x \<and> is_leveln_node n x
is_measured_node x2 \<and> is_leveln_node n x2
l = deepR pr l1 l2
nd = x2
r = deepL r2 r1 sf

goal (1 subgoal):
 1. is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
is_leveln_node n nd \<and> is_measured_node nd

goal (1 subgoal):
 1. \<lbrakk>\<not> p (i + gmd pr); \<And>x xa n l nd r. \<lbrakk>x = i + gmd pr; xa = x + gmft m; \<not> p x; p xa; is_leveln_ftree n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> toList m = toList l @ nodeToList nd @ toList r \<and> \<not> p (x + gmft l) \<and> p (x + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd; is_leveln_ftree n (Deep uu pr m sf); is_measured_ftree (Deep uu pr m sf); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Deep uu pr m sf)); nsplitTree p i (Deep uu pr m sf) = (l, nd, r); p (i + gmd pr + gmft m)\<rbrakk> \<Longrightarrow> toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
from l_nd_r(1,2) l2_x2_r2_inv(1,2,3)
             l1_x_r1_inv(3) l2_x2_r2_list(2) pr_m_sf_inv(1)
[PROOF STATE]
proof (chain)
picking this:
l = deepR pr l1 l2
nd = x2
\<not> p (i + gmd pr + gmft l1 + gmnl l2)
p (i + gmd pr + gmft l1 + gmnl l2 + gmn x2)
\<forall>x\<in>set l2. is_measured_node x \<and> is_leveln_node n x
is_leveln_ftree (Suc n) l1 \<and> is_measured_ftree l1
length l2 \<le> 4 \<and> length r2 \<le> 4
is_leveln_digit n pr \<and> is_measured_digit pr
[PROOF STEP]
have split_point:
          " \<not> p (i + gmft l)"
          "p (i + gmft l + gmn nd)"
[PROOF STATE]
proof (prove)
using this:
l = deepR pr l1 l2
nd = x2
\<not> p (i + gmd pr + gmft l1 + gmnl l2)
p (i + gmd pr + gmft l1 + gmnl l2 + gmn x2)
\<forall>x\<in>set l2. is_measured_node x \<and> is_leveln_node n x
is_leveln_ftree (Suc n) l1 \<and> is_measured_ftree l1
length l2 \<le> 4 \<and> length r2 \<le> 4
is_leveln_digit n pr \<and> is_measured_digit pr

goal (1 subgoal):
 1. \<not> p (i + gmft l) &&& p (i + gmft l + gmn nd)
[PROOF STEP]
by (auto simp add: gmftR_gmnl add.assoc)
[PROOF STATE]
proof (state)
this:
\<not> p (i + gmft l)
p (i + gmft l + gmn nd)

goal (1 subgoal):
 1. \<lbrakk>\<not> p (i + gmd pr); \<And>x xa n l nd r. \<lbrakk>x = i + gmd pr; xa = x + gmft m; \<not> p x; p xa; is_leveln_ftree n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> toList m = toList l @ nodeToList nd @ toList r \<and> \<not> p (x + gmft l) \<and> p (x + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd; is_leveln_ftree n (Deep uu pr m sf); is_measured_ftree (Deep uu pr m sf); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Deep uu pr m sf)); nsplitTree p i (Deep uu pr m sf) = (l, nd, r); p (i + gmd pr + gmft m)\<rbrakk> \<Longrightarrow> toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
from l2_x2_r2_list
[PROOF STATE]
proof (chain)
picking this:
digitToList (nodeToDigit x) = nlistToList l2 @ nodeToList x2 @ nlistToList r2
length l2 \<le> 4 \<and> length r2 \<le> 4
[PROOF STEP]
have x_list:
          "nodeToList x = nlistToList l2 @ nodeToList x2 @ nlistToList r2"
[PROOF STATE]
proof (prove)
using this:
digitToList (nodeToDigit x) = nlistToList l2 @ nodeToList x2 @ nlistToList r2
length l2 \<le> 4 \<and> length r2 \<le> 4

goal (1 subgoal):
 1. nodeToList x = nlistToList l2 @ nodeToList x2 @ nlistToList r2
[PROOF STEP]
by (simp add: nodeToDigit_list)
[PROOF STATE]
proof (state)
this:
nodeToList x = nlistToList l2 @ nodeToList x2 @ nlistToList r2

goal (1 subgoal):
 1. \<lbrakk>\<not> p (i + gmd pr); \<And>x xa n l nd r. \<lbrakk>x = i + gmd pr; xa = x + gmft m; \<not> p x; p xa; is_leveln_ftree n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> toList m = toList l @ nodeToList nd @ toList r \<and> \<not> p (x + gmft l) \<and> p (x + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd; is_leveln_ftree n (Deep uu pr m sf); is_measured_ftree (Deep uu pr m sf); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Deep uu pr m sf)); nsplitTree p i (Deep uu pr m sf) = (l, nd, r); p (i + gmd pr + gmft m)\<rbrakk> \<Longrightarrow> toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
from l1_x_r1_inv(3) pr_m_sf_inv(1)
             l2_x2_r2_inv(3) l2_x2_r2_list(2) l_nd_r(1)
[PROOF STATE]
proof (chain)
picking this:
is_leveln_ftree (Suc n) l1 \<and> is_measured_ftree l1
is_leveln_digit n pr \<and> is_measured_digit pr
\<forall>x\<in>set l2. is_measured_node x \<and> is_leveln_node n x
length l2 \<le> 4 \<and> length r2 \<le> 4
l = deepR pr l1 l2
[PROOF STEP]
have l_list: "toList l = digitToList pr @ toList l1 @ nlistToList l2"
[PROOF STATE]
proof (prove)
using this:
is_leveln_ftree (Suc n) l1 \<and> is_measured_ftree l1
is_leveln_digit n pr \<and> is_measured_digit pr
\<forall>x\<in>set l2. is_measured_node x \<and> is_leveln_node n x
length l2 \<le> 4 \<and> length r2 \<le> 4
l = deepR pr l1 l2

goal (1 subgoal):
 1. toList l = digitToList pr @ toList l1 @ nlistToList l2
[PROOF STEP]
by (auto simp add: deepR_list)
[PROOF STATE]
proof (state)
this:
toList l = digitToList pr @ toList l1 @ nlistToList l2

goal (1 subgoal):
 1. \<lbrakk>\<not> p (i + gmd pr); \<And>x xa n l nd r. \<lbrakk>x = i + gmd pr; xa = x + gmft m; \<not> p x; p xa; is_leveln_ftree n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> toList m = toList l @ nodeToList nd @ toList r \<and> \<not> p (x + gmft l) \<and> p (x + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd; is_leveln_ftree n (Deep uu pr m sf); is_measured_ftree (Deep uu pr m sf); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Deep uu pr m sf)); nsplitTree p i (Deep uu pr m sf) = (l, nd, r); p (i + gmd pr + gmft m)\<rbrakk> \<Longrightarrow> toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
from l1_x_r1_inv(4) pr_m_sf_inv(3) l2_x2_r2_inv(4)
             l2_x2_r2_list(2) l_nd_r(3)
[PROOF STATE]
proof (chain)
picking this:
is_leveln_ftree (Suc n) r1 \<and> is_measured_ftree r1
is_leveln_digit n sf \<and> is_measured_digit sf
\<forall>x\<in>set r2. is_measured_node x \<and> is_leveln_node n x
length l2 \<le> 4 \<and> length r2 \<le> 4
r = deepL r2 r1 sf
[PROOF STEP]
have r_list: "toList r = nlistToList r2 @ toList r1 @ digitToList sf"
[PROOF STATE]
proof (prove)
using this:
is_leveln_ftree (Suc n) r1 \<and> is_measured_ftree r1
is_leveln_digit n sf \<and> is_measured_digit sf
\<forall>x\<in>set r2. is_measured_node x \<and> is_leveln_node n x
length l2 \<le> 4 \<and> length r2 \<le> 4
r = deepL r2 r1 sf

goal (1 subgoal):
 1. toList r = nlistToList r2 @ toList r1 @ digitToList sf
[PROOF STEP]
by (auto simp add: deepL_list)
[PROOF STATE]
proof (state)
this:
toList r = nlistToList r2 @ toList r1 @ digitToList sf

goal (1 subgoal):
 1. \<lbrakk>\<not> p (i + gmd pr); \<And>x xa n l nd r. \<lbrakk>x = i + gmd pr; xa = x + gmft m; \<not> p x; p xa; is_leveln_ftree n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> toList m = toList l @ nodeToList nd @ toList r \<and> \<not> p (x + gmft l) \<and> p (x + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd; is_leveln_ftree n (Deep uu pr m sf); is_measured_ftree (Deep uu pr m sf); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Deep uu pr m sf)); nsplitTree p i (Deep uu pr m sf) = (l, nd, r); p (i + gmd pr + gmft m)\<rbrakk> \<Longrightarrow> toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
from x_list l1_x_r1_list l_list r_list l_nd_r
[PROOF STATE]
proof (chain)
picking this:
nodeToList x = nlistToList l2 @ nodeToList x2 @ nlistToList r2
toList m = toList l1 @ nodeToList x @ toList r1
toList l = digitToList pr @ toList l1 @ nlistToList l2
toList r = nlistToList r2 @ toList r1 @ digitToList sf
l = deepR pr l1 l2
nd = x2
r = deepL r2 r1 sf
[PROOF STEP]
have  "toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r"
[PROOF STATE]
proof (prove)
using this:
nodeToList x = nlistToList l2 @ nodeToList x2 @ nlistToList r2
toList m = toList l1 @ nodeToList x @ toList r1
toList l = digitToList pr @ toList l1 @ nlistToList l2
toList r = nlistToList r2 @ toList r1 @ digitToList sf
l = deepR pr l1 l2
nd = x2
r = deepL r2 r1 sf

goal (1 subgoal):
 1. toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r

goal (1 subgoal):
 1. \<lbrakk>\<not> p (i + gmd pr); \<And>x xa n l nd r. \<lbrakk>x = i + gmd pr; xa = x + gmft m; \<not> p x; p xa; is_leveln_ftree n m; is_measured_ftree m; \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> toList m = toList l @ nodeToList nd @ toList r \<and> \<not> p (x + gmft l) \<and> p (x + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd; is_leveln_ftree n (Deep uu pr m sf); is_measured_ftree (Deep uu pr m sf); \<And>a b. p a \<Longrightarrow> p (a + b); \<not> p i; p (i + gmft (Deep uu pr m sf)); nsplitTree p i (Deep uu pr m sf) = (l, nd, r); p (i + gmd pr + gmft m)\<rbrakk> \<Longrightarrow> toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
with split_point l_inv r_inv nd_inv
[PROOF STATE]
proof (chain)
picking this:
\<not> p (i + gmft l)
p (i + gmft l + gmn nd)
is_leveln_ftree n l \<and> is_measured_ftree l
is_leveln_ftree n r \<and> is_measured_ftree r
is_leveln_node n nd \<and> is_measured_node nd
toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
\<not> p (i + gmft l)
p (i + gmft l + gmn nd)
is_leveln_ftree n l \<and> is_measured_ftree l
is_leveln_ftree n r \<and> is_measured_ftree r
is_leveln_node n nd \<and> is_measured_node nd
toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r

goal (1 subgoal):
 1. toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
toList (Deep uu pr m sf) = toList l @ nodeToList nd @ toList r \<and> \<not> p (i + gmft l) \<and> p (i + gmft l + gmn nd) \<and> is_leveln_ftree n l \<and> is_measured_ftree l \<and> is_leveln_ftree n r \<and> is_measured_ftree r \<and> is_leveln_node n nd \<and> is_measured_node nd

goal:
No subgoals!
[PROOF STEP]
qed