[STATEMENT]
lemma nsplitTree_invpres: "\<lbrakk>
  is_leveln_ftree n (s:: ('e,'a::monoid_add) FingerTreeStruc);
  is_measured_ftree s;
  \<not> p i;
  p (i + (gmft s));
  (nsplitTree p i s) = (l, nd, r)\<rbrakk>
  \<Longrightarrow>
  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; \<not> p i; p (i + gmft s); nsplitTree p i s = (l, nd, r)\<rbrakk> \<Longrightarrow> 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; \<not> p i; p (i + gmft Empty); nsplitTree p i Empty = (l, nd, r)\<rbrakk> \<Longrightarrow> 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); \<not> p i; p (i + gmft (Single ea)); nsplitTree p i (Single ea) = (l, nd, r)\<rbrakk> \<Longrightarrow> 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; \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> 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); \<not> p i; p (i + gmft (Deep uu_ pr m sf)); nsplitTree p i (Deep uu_ pr m sf) = (l, nd, r)\<rbrakk> \<Longrightarrow> 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
\<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; \<not> p i; p (i + gmft Empty); nsplitTree p i Empty = (l, nd, r)\<rbrakk> \<Longrightarrow> 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); \<not> p i; p (i + gmft (Single ea)); nsplitTree p i (Single ea) = (l, nd, r)\<rbrakk> \<Longrightarrow> 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; \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> 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); \<not> p i; p (i + gmft (Deep uu_ pr m sf)); nsplitTree p i (Deep uu_ pr m sf) = (l, nd, r)\<rbrakk> \<Longrightarrow> 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
\<not> p_ i_
p_ (i_ + gmft Empty)
nsplitTree p_ i_ Empty = (l, nd, r)

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
[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 (2 subgoals):
 1. \<And>p i ea n l nd r. \<lbrakk>is_leveln_ftree n (Single ea); is_measured_ftree (Single ea); \<not> p i; p (i + gmft (Single ea)); nsplitTree p i (Single ea) = (l, nd, r)\<rbrakk> \<Longrightarrow> 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; \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> 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); \<not> p i; p (i + gmft (Deep uu_ pr m sf)); nsplitTree p i (Deep uu_ pr m sf) = (l, nd, r)\<rbrakk> \<Longrightarrow> 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); \<not> p i; p (i + gmft (Single ea)); nsplitTree p i (Single ea) = (l, nd, r)\<rbrakk> \<Longrightarrow> 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; \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> 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); \<not> p i; p (i + gmft (Deep uu_ pr m sf)); nsplitTree p i (Deep uu_ pr m sf) = (l, nd, r)\<rbrakk> \<Longrightarrow> 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_)
\<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); \<not> p i; p (i + gmft (Single ea)); nsplitTree p i (Single ea) = (l, nd, r)\<rbrakk> \<Longrightarrow> 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; \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> 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); \<not> p i; p (i + gmft (Deep uu_ pr m sf)); nsplitTree p i (Deep uu_ pr m sf) = (l, nd, r)\<rbrakk> \<Longrightarrow> 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_)
\<not> p_ i_
p_ (i_ + gmft (Single ea_))
nsplitTree p_ i_ (Single ea_) = (l, nd, r)

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
[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. \<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; \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> 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); \<not> p i; p (i + gmft (Deep uu_ pr m sf)); nsplitTree p i (Deep uu_ pr m sf) = (l, nd, r)\<rbrakk> \<Longrightarrow> 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; \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> 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); \<not> p i; p (i + gmft (Deep uu_ pr m sf)); nsplitTree p i (Deep uu_ pr m sf) = (l, nd, r)\<rbrakk> \<Longrightarrow> 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; \<not> p ?x; p (?x + gmft m); nsplitTree p ?x m = (?l, ?nd, ?r)\<rbrakk> \<Longrightarrow> 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)
\<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; \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> 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); \<not> p i; p (i + gmft (Deep uu_ pr m sf)); nsplitTree p i (Deep uu_ pr m sf) = (l, nd, r)\<rbrakk> \<Longrightarrow> 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; \<not> p ?x; p (?x + gmft m); nsplitTree p ?x m = (?l, ?nd, ?r)\<rbrakk> \<Longrightarrow> 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)
\<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. 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; \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> 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); \<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> 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; \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> 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); \<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> 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; \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> 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); \<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> 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; \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> 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); \<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> 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; \<not> p ?x; p (?x + gmft m); nsplitTree p ?x m = (?l, ?nd, ?r)\<rbrakk> \<Longrightarrow> 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)
\<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; \<not> p ?x; p (?x + gmft m); nsplitTree p ?x m = (?l, ?nd, ?r)\<rbrakk> \<Longrightarrow> 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)
\<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. 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; \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> 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); \<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> 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; \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> 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); \<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> 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
[PROOF STATE]
proof (chain)
picking this:
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; \<not> p ?x; p (?x + gmft m); nsplitTree p ?x m = (?l, ?nd, ?r)\<rbrakk> \<Longrightarrow> 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)
\<not> p i
p (i + gmft (Deep uu pr m sf))
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)
\<lbrakk>?x = i + gmd pr; ?xa = ?x + gmft m; \<not> p ?x; p ?xa; is_leveln_ftree ?n m; is_measured_ftree m; \<not> p ?x; p (?x + gmft m); nsplitTree p ?x m = (?l, ?nd, ?r)\<rbrakk> \<Longrightarrow> 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)
\<not> p i
p (i + gmft (Deep uu pr m sf))
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; \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> 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); \<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> 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; \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> 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); \<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> 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; \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> 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); \<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> 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" l1 x r1 n]
[PROOF STATE]
proof (chain)
picking this:
\<not> p i
p (i + gmft (Deep uu pr m sf))
is_leveln_digit n pr \<and> is_measured_digit pr
p (i + gmd pr)
splitDigit p i pr = (l1, x, r1)
\<lbrakk>splitDigit p i pr = (l1, x, r1); is_measured_digit pr; is_leveln_digit n pr\<rbrakk> \<Longrightarrow> (\<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:
        "\<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:
\<not> p i
p (i + gmft (Deep uu pr m sf))
is_leveln_digit n pr \<and> is_measured_digit pr
p (i + gmd pr)
splitDigit p i pr = (l1, x, r1)
\<lbrakk>splitDigit p i pr = (l1, x, r1); is_measured_digit pr; is_leveln_digit n pr\<rbrakk> \<Longrightarrow> (\<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. \<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:
\<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; \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> 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); \<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> 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 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; \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> 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); \<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> 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 ?thesis
[PROOF STATE]
proof (prove)
using 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. 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:
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:
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; \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> 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); \<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> 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; \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> 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); \<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> 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; \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> 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); \<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> 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; \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> 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); \<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> 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; \<not> p ?x; p (?x + gmft m); nsplitTree p ?x m = (?l, ?nd, ?r)\<rbrakk> \<Longrightarrow> 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)
\<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; \<not> p ?x; p (?x + gmft m); nsplitTree p ?x m = (?l, ?nd, ?r)\<rbrakk> \<Longrightarrow> 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)
\<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. 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; \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> 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); \<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> 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; \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> 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); \<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> 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; \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> 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); \<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> 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; \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> 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); \<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> 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; \<not> p ?x; p (?x + gmft m); nsplitTree p ?x m = (?l, ?nd, ?r)\<rbrakk> \<Longrightarrow> 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)
\<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; \<not> p ?x; p (?x + gmft m); nsplitTree p ?x m = (?l, ?nd, ?r)\<rbrakk> \<Longrightarrow> 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)
\<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. 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; \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> 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); \<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> 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; \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> 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); \<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> 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
[PROOF STATE]
proof (chain)
picking this:
\<not> p (i + gmd pr)
\<not> p (i + gmd pr + gmft m)
\<lbrakk>?x = i + gmd pr; ?xa = ?x + gmft m; \<not> p ?x; p ?xa; is_leveln_ftree ?n m; is_measured_ftree m; \<not> p ?x; p (?x + gmft m); nsplitTree p ?x m = (?l, ?nd, ?r)\<rbrakk> \<Longrightarrow> 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)
\<not> p i
p (i + gmft (Deep uu pr m sf))
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)
\<lbrakk>?x = i + gmd pr; ?xa = ?x + gmft m; \<not> p ?x; p ?xa; is_leveln_ftree ?n m; is_measured_ftree m; \<not> p ?x; p (?x + gmft m); nsplitTree p ?x m = (?l, ?nd, ?r)\<rbrakk> \<Longrightarrow> 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)
\<not> p i
p (i + gmft (Deep uu pr m sf))
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; \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> 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); \<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> 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; \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> 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); \<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> 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; \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> 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); \<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> 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
[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; \<not> p ?x; p (?x + gmft m); nsplitTree p ?x m = (?l, ?nd, ?r)\<rbrakk> \<Longrightarrow> 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)
\<not> p i
p (i + gmft (Deep uu pr m sf))
nsplitTree p i (Deep uu pr m sf) = (l, nd, r)
[PROOF STEP]
have
          v7: "p (i + gmd pr + gmft m + gmd sf)"
[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; \<not> p ?x; p (?x + gmft m); nsplitTree p ?x m = (?l, ?nd, ?r)\<rbrakk> \<Longrightarrow> 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)
\<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. 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; \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> 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); \<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> 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 l1 x r1 n]
[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
\<not> p i
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>splitDigit p (i + gmd pr + gmft m) sf = (l1, x, r1); is_measured_digit sf; is_leveln_digit n sf\<rbrakk> \<Longrightarrow> (\<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:
          "\<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
\<not> p i
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>splitDigit p (i + gmd pr + gmft m) sf = (l1, x, r1); is_measured_digit sf; is_leveln_digit n sf\<rbrakk> \<Longrightarrow> (\<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. \<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:
\<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; \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> 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); \<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> 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 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; \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> 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); \<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> 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 ziel3
[PROOF STATE]
proof (chain)
picking 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
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using 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. 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:
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:
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; \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> 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); \<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> 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; \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> 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); \<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> 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; \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> 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); \<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> 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; \<not> p ?x; p (?x + gmft m); nsplitTree p ?x m = (?l, ?nd, ?r)\<rbrakk> \<Longrightarrow> 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)
\<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; \<not> p ?x; p (?x + gmft m); nsplitTree p ?x m = (?l, ?nd, ?r)\<rbrakk> \<Longrightarrow> 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)
\<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. 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; \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> 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); \<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> 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; \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> 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); \<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> 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; \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> 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); \<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> 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(6) 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; \<not> p (i + gmd pr); p (i + gmd pr + gmft m); nsplitTree p (i + gmd pr) m = (l1, x, r1)\<rbrakk> \<Longrightarrow> 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
nsplitTree p i (Deep uu pr m sf) = (l, nd, r)
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:
          "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"
[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; \<not> p (i + gmd pr); p (i + gmd pr + gmft m); nsplitTree p (i + gmd pr) m = (l1, x, r1)\<rbrakk> \<Longrightarrow> 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
nsplitTree p i (Deep uu pr m sf) = (l, nd, r)
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. 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
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
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

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; \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> 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); \<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> 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; \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> 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); \<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> 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
[PROOF STATE]
proof (chain)
picking this:
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
[PROOF STEP]
have
          ndx_inv: "is_leveln_digit n (nodeToDigit x) \<and>
          is_measured_digit (nodeToDigit x)"
[PROOF STATE]
proof (prove)
using this:
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

goal (1 subgoal):
 1. is_leveln_digit n (nodeToDigit x) \<and> is_measured_digit (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)

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; \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> 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); \<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> 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" l2 x2 r2 n]
[PROOF STATE]
proof (state)
this:
\<lbrakk>splitDigit p (i + gmd pr + gmft l1) (nodeToDigit x) = (l2, x2, r2); is_measured_digit (nodeToDigit x); is_leveln_digit n (nodeToDigit x)\<rbrakk> \<Longrightarrow> (\<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; \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> 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); \<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> 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)
is_leveln_ftree (Suc n) l1 \<and> is_measured_ftree l1
splitDigit p (i + gmd pr + gmft l1) (nodeToDigit x) = (l2, x2, r2)
\<not> p i
[PROOF STEP]
have
          l2_x2_r2_inv:
          "\<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)
is_leveln_ftree (Suc n) l1 \<and> is_measured_ftree l1
splitDigit p (i + gmd pr + gmft l1) (nodeToDigit x) = (l2, x2, r2)
\<not> p i

goal (1 subgoal):
 1. \<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:
\<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; \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> 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); \<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> 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; \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> 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); \<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> 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; \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> 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); \<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> 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(6) 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; \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> 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); \<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> 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(1) 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; \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> 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); \<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> 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 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
\<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
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
\<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
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; \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> 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); \<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> 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(2) 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; \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> 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); \<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> 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 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 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
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 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
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; \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> 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); \<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> 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:
\<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:
\<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; \<not> p x; p (x + gmft m); nsplitTree p x m = (l, nd, r)\<rbrakk> \<Longrightarrow> 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); \<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> 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_inv r_inv nd_inv
[PROOF STATE]
proof (chain)
picking this:
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
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
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

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 simp
[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:
No subgoals!
[PROOF STEP]
qed
[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:
No subgoals!
[PROOF STEP]
qed
[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:
No subgoals!
[PROOF STEP]
qed
[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:
No subgoals!
[PROOF STEP]
qed