[STATEMENT]
lemma size_list [simp]: " \<lbrakk>0 < size big; invar big; list big = []\<rbrakk> \<Longrightarrow> False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>0 < size big; invar big; Big.list big = []\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
proof(induction big rule: list.induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>common. \<lbrakk>0 < size (Common common); invar (Common common); Big.list (Common common) = []\<rbrakk> \<Longrightarrow> False
 2. \<And>extra uu_ uv_ remained big aux count. \<lbrakk>0 < size (Reverse (Current extra uu_ uv_ remained) big aux count); invar (Reverse (Current extra uu_ uv_ remained) big aux count); Big.list (Reverse (Current extra uu_ uv_ remained) big aux count) = []\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
case 1
[PROOF STATE]
proof (state)
this:
0 < size (Common common_)
invar (Common common_)
Big.list (Common common_) = []

goal (2 subgoals):
 1. \<And>common. \<lbrakk>0 < size (Common common); invar (Common common); Big.list (Common common) = []\<rbrakk> \<Longrightarrow> False
 2. \<And>extra uu_ uv_ remained big aux count. \<lbrakk>0 < size (Reverse (Current extra uu_ uv_ remained) big aux count); invar (Reverse (Current extra uu_ uv_ remained) big aux count); Big.list (Reverse (Current extra uu_ uv_ remained) big aux count) = []\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < size (Common common_)
invar (Common common_)
Big.list (Common common_) = []
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
0 < size (Common common_)
invar (Common common_)
Big.list (Common common_) = []

goal (1 subgoal):
 1. False
[PROOF STEP]
using list_size
[PROOF STATE]
proof (prove)
using this:
0 < size (Common common_)
invar (Common common_)
Big.list (Common common_) = []
\<lbrakk>0 < size ?common; Common.list ?common = []; invar ?common\<rbrakk> \<Longrightarrow> False

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

goal (1 subgoal):
 1. \<And>extra uu_ uv_ remained big aux count. \<lbrakk>0 < size (Reverse (Current extra uu_ uv_ remained) big aux count); invar (Reverse (Current extra uu_ uv_ remained) big aux count); Big.list (Reverse (Current extra uu_ uv_ remained) big aux count) = []\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>extra uu_ uv_ remained big aux count. \<lbrakk>0 < size (Reverse (Current extra uu_ uv_ remained) big aux count); invar (Reverse (Current extra uu_ uv_ remained) big aux count); Big.list (Reverse (Current extra uu_ uv_ remained) big aux count) = []\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
case 2
[PROOF STATE]
proof (state)
this:
0 < size (Reverse (Current extra_ uu_ uv_ remained_) big_ aux_ count_)
invar (Reverse (Current extra_ uu_ uv_ remained_) big_ aux_ count_)
Big.list (Reverse (Current extra_ uu_ uv_ remained_) big_ aux_ count_) = []

goal (1 subgoal):
 1. \<And>extra uu_ uv_ remained big aux count. \<lbrakk>0 < size (Reverse (Current extra uu_ uv_ remained) big aux count); invar (Reverse (Current extra uu_ uv_ remained) big aux count); Big.list (Reverse (Current extra uu_ uv_ remained) big aux count) = []\<rbrakk> \<Longrightarrow> False
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
0 < size (Reverse (Current extra_ uu_ uv_ remained_) big_ aux_ count_)
invar (Reverse (Current extra_ uu_ uv_ remained_) big_ aux_ count_)
Big.list (Reverse (Current extra_ uu_ uv_ remained_) big_ aux_ count_) = []
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
0 < size (Reverse (Current extra_ uu_ uv_ remained_) big_ aux_ count_)
invar (Reverse (Current extra_ uu_ uv_ remained_) big_ aux_ count_)
Big.list (Reverse (Current extra_ uu_ uv_ remained_) big_ aux_ count_) = []

goal (1 subgoal):
 1. False
[PROOF STEP]
by (metis list.distinct(1) list_Reverse)
[PROOF STATE]
proof (state)
this:
False

goal:
No subgoals!
[PROOF STEP]
qed