[STATEMENT]
lemma split_face_edges_f12_bet:
assumes vors: "pre_split_face f ram1 ram2 vs"
              "(f12, f21) = split_face f ram1 ram2 vs"
              "vs \<noteq> []" "between (vertices f) ram1 ram2 = []"
shows "edges f12 = {(hd vs, ram1) , (ram1, ram2), (ram2, last vs)} \<union>
                   Edges(rev vs)" (is "?lhs = ?rhs")
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<E> f12 = {(hd vs, ram1), (ram1, ram2), (ram2, last vs)} \<union> Edges (rev vs)
[PROOF STEP]
proof (intro equalityI subsetI)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> \<E> f12 \<Longrightarrow> x \<in> {(hd vs, ram1), (ram1, ram2), (ram2, last vs)} \<union> Edges (rev vs)
 2. \<And>x. x \<in> {(hd vs, ram1), (ram1, ram2), (ram2, last vs)} \<union> Edges (rev vs) \<Longrightarrow> x \<in> \<E> f12
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. \<And>x. x \<in> \<E> f12 \<Longrightarrow> x \<in> {(hd vs, ram1), (ram1, ram2), (ram2, last vs)} \<union> Edges (rev vs)
 2. \<And>x. x \<in> {(hd vs, ram1), (ram1, ram2), (ram2, last vs)} \<union> Edges (rev vs) \<Longrightarrow> x \<in> \<E> f12
[PROOF STEP]
assume x: "x \<in> ?lhs"
[PROOF STATE]
proof (state)
this:
x \<in> \<E> f12

goal (2 subgoals):
 1. \<And>x. x \<in> \<E> f12 \<Longrightarrow> x \<in> {(hd vs, ram1), (ram1, ram2), (ram2, last vs)} \<union> Edges (rev vs)
 2. \<And>x. x \<in> {(hd vs, ram1), (ram1, ram2), (ram2, last vs)} \<union> Edges (rev vs) \<Longrightarrow> x \<in> \<E> f12
[PROOF STEP]
define c where "c = fst x"
[PROOF STATE]
proof (state)
this:
c = fst x

goal (2 subgoals):
 1. \<And>x. x \<in> \<E> f12 \<Longrightarrow> x \<in> {(hd vs, ram1), (ram1, ram2), (ram2, last vs)} \<union> Edges (rev vs)
 2. \<And>x. x \<in> {(hd vs, ram1), (ram1, ram2), (ram2, last vs)} \<union> Edges (rev vs) \<Longrightarrow> x \<in> \<E> f12
[PROOF STEP]
define d where "d = snd x"
[PROOF STATE]
proof (state)
this:
d = snd x

goal (2 subgoals):
 1. \<And>x. x \<in> \<E> f12 \<Longrightarrow> x \<in> {(hd vs, ram1), (ram1, ram2), (ram2, last vs)} \<union> Edges (rev vs)
 2. \<And>x. x \<in> {(hd vs, ram1), (ram1, ram2), (ram2, last vs)} \<union> Edges (rev vs) \<Longrightarrow> x \<in> \<E> f12
[PROOF STEP]
with c_def
[PROOF STATE]
proof (chain)
picking this:
c = fst x
d = snd x
[PROOF STEP]
have [simp]: "x = (c,d)"
[PROOF STATE]
proof (prove)
using this:
c = fst x
d = snd x

goal (1 subgoal):
 1. x = (c, d)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x = (c, d)

goal (2 subgoals):
 1. \<And>x. x \<in> \<E> f12 \<Longrightarrow> x \<in> {(hd vs, ram1), (ram1, ram2), (ram2, last vs)} \<union> Edges (rev vs)
 2. \<And>x. x \<in> {(hd vs, ram1), (ram1, ram2), (ram2, last vs)} \<union> Edges (rev vs) \<Longrightarrow> x \<in> \<E> f12
[PROOF STEP]
from vors
[PROOF STATE]
proof (chain)
picking this:
pre_split_face f ram1 ram2 vs
(f12, f21) = split_face f ram1 ram2 vs
vs \<noteq> []
between (vertices f) ram1 ram2 = []
[PROOF STEP]
have dist_f12: "distinct (vertices f12)"
[PROOF STATE]
proof (prove)
using this:
pre_split_face f ram1 ram2 vs
(f12, f21) = split_face f ram1 ram2 vs
vs \<noteq> []
between (vertices f) ram1 ram2 = []

goal (1 subgoal):
 1. distinct (vertices f12)
[PROOF STEP]
apply (rule_tac split_face_distinct1)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pre_split_face f ram1 ram2 vs; (f12, f21) = split_face f ram1 ram2 vs; vs \<noteq> []; between (vertices f) ram1 ram2 = []\<rbrakk> \<Longrightarrow> (f12, ?f21.4) = split_face ?oldF4 ?ram1.4 ?ram2.4 ?newVertexList4
 2. \<lbrakk>pre_split_face f ram1 ram2 vs; (f12, f21) = split_face f ram1 ram2 vs; vs \<noteq> []; between (vertices f) ram1 ram2 = []\<rbrakk> \<Longrightarrow> pre_split_face ?oldF4 ?ram1.4 ?ram2.4 ?newVertexList4
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
distinct (vertices f12)

goal (2 subgoals):
 1. \<And>x. x \<in> \<E> f12 \<Longrightarrow> x \<in> {(hd vs, ram1), (ram1, ram2), (ram2, last vs)} \<union> Edges (rev vs)
 2. \<And>x. x \<in> {(hd vs, ram1), (ram1, ram2), (ram2, last vs)} \<union> Edges (rev vs) \<Longrightarrow> x \<in> \<E> f12
[PROOF STEP]
from x vors
[PROOF STATE]
proof (chain)
picking this:
x \<in> \<E> f12
pre_split_face f ram1 ram2 vs
(f12, f21) = split_face f ram1 ram2 vs
vs \<noteq> []
between (vertices f) ram1 ram2 = []
[PROOF STEP]
show "x \<in> ?rhs"
[PROOF STATE]
proof (prove)
using this:
x \<in> \<E> f12
pre_split_face f ram1 ram2 vs
(f12, f21) = split_face f ram1 ram2 vs
vs \<noteq> []
between (vertices f) ram1 ram2 = []

goal (1 subgoal):
 1. x \<in> {(hd vs, ram1), (ram1, ram2), (ram2, last vs)} \<union> Edges (rev vs)
[PROOF STEP]
apply (simp add: split_face_def is_nextElem_def is_sublist_def dist_f12)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<exists>as bs. rev vs @ [ram1, ram2] = as @ c # d # bs) \<or> c = ram2 \<and> d = last vs; pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram1 \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
[PROOF STEP]
apply (case_tac " c = ram2 \<and> d = last vs")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>(\<exists>as bs. rev vs @ [ram1, ram2] = as @ c # d # bs) \<or> c = ram2 \<and> d = last vs; pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<and> d = last vs\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram1 \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
 2. \<lbrakk>(\<exists>as bs. rev vs @ [ram1, ram2] = as @ c # d # bs) \<or> c = ram2 \<and> d = last vs; pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; \<not> (c = ram2 \<and> d = last vs)\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram1 \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>(\<exists>as bs. rev vs @ [ram1, ram2] = as @ c # d # bs) \<or> c = ram2 \<and> d = last vs; pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; \<not> (c = ram2 \<and> d = last vs)\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram1 \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>as bs. rev vs @ [ram1, ram2] = as @ c # d # bs; pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram1 \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
[PROOF STEP]
apply (elim exE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram1 \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
[PROOF STEP]
apply (case_tac "c = ram1")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c = ram1\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram1 \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
 2. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram1 \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ ram1 # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; ram1 = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ ram1 # d # bs; c = ram1\<rbrakk> \<Longrightarrow> ram1 = hd vs \<and> d = ram1 \<or> d = ram2 \<or> ram1 = ram2 \<and> d = last vs \<or> (d, ram1) \<in> Edges vs
 2. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram1 \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
[PROOF STEP]
apply (subgoal_tac "rev vs = as")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ ram1 # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; ram1 = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ ram1 # d # bs; c = ram1; rev vs = as\<rbrakk> \<Longrightarrow> ram1 = hd vs \<and> d = ram1 \<or> d = ram2 \<or> ram1 = ram2 \<and> d = last vs \<or> (d, ram1) \<in> Edges vs
 2. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ ram1 # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; ram1 = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ ram1 # d # bs; c = ram1\<rbrakk> \<Longrightarrow> rev vs = as
 3. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram1 \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ ram1 # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; ram1 = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ ram1 # d # bs; c = ram1\<rbrakk> \<Longrightarrow> rev vs = as
 2. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram1 \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
[PROOF STEP]
apply (rule dist_at1)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ ram1 # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; ram1 = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ ram1 # d # bs; c = ram1\<rbrakk> \<Longrightarrow> distinct (?vs10 as bs)
 2. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ ram1 # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; ram1 = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ ram1 # d # bs; c = ram1\<rbrakk> \<Longrightarrow> ?vs10 as bs = rev vs @ ?r10 as bs # ?b10 as bs
 3. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ ram1 # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; ram1 = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ ram1 # d # bs; c = ram1\<rbrakk> \<Longrightarrow> ?vs10 as bs = as @ ?r10 as bs # ?d10 as bs
 4. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram1 \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
[PROOF STEP]
apply (rule dist_f12)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ ram1 # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; ram1 = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ ram1 # d # bs; c = ram1\<rbrakk> \<Longrightarrow> vertices f12 = rev vs @ ?r10 as bs # ?b10 as bs
 2. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ ram1 # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; ram1 = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ ram1 # d # bs; c = ram1\<rbrakk> \<Longrightarrow> vertices f12 = as @ ?r10 as bs # ?d10 as bs
 3. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram1 \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
[PROOF STEP]
apply (rule sym)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ ram1 # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; ram1 = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ ram1 # d # bs; c = ram1\<rbrakk> \<Longrightarrow> rev vs @ ?r10 as bs # ?b10 as bs = vertices f12
 2. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ ram1 # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; ram1 = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ ram1 # d # bs; c = ram1\<rbrakk> \<Longrightarrow> vertices f12 = as @ ?r10 as bs # ?d10 as bs
 3. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram1 \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ ram1 # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; ram1 = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ ram1 # d # bs; c = ram1\<rbrakk> \<Longrightarrow> vertices f12 = as @ ram1 # ?d10 as bs
 2. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram1 \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram1 \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
[PROOF STEP]
(* a \<noteq> ram1 *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram1 \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
[PROOF STEP]
apply (case_tac "c \<in> set(rev vs)")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<in> set (rev vs)\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram1 \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
 2. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<notin> set (rev vs)\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram1 \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
[PROOF STEP]
apply (subgoal_tac "distinct(rev vs)")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<in> set (rev vs); distinct (rev vs)\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram1 \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
 2. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<in> set (rev vs)\<rbrakk> \<Longrightarrow> distinct (rev vs)
 3. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<notin> set (rev vs)\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram1 \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
[PROOF STEP]
apply (simp only: in_set_conv_decomp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ c # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; \<exists>ys zs. rev vs = ys @ c # zs; distinct (rev vs)\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> False \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
 2. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<in> set (rev vs)\<rbrakk> \<Longrightarrow> distinct (rev vs)
 3. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<notin> set (rev vs)\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram1 \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
[PROOF STEP]
apply (elim exE)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>as bs ys zs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ c # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; distinct (rev vs); rev vs = ys @ c # zs\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> False \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
 2. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<in> set (rev vs)\<rbrakk> \<Longrightarrow> distinct (rev vs)
 3. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<notin> set (rev vs)\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram1 \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>as bs ys zs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ c # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; ys @ c # zs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; distinct ys \<and> c \<notin> set zs \<and> distinct zs \<and> c \<notin> set ys \<and> set ys \<inter> set zs = {}; rev vs = ys @ c # zs\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
 2. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<in> set (rev vs)\<rbrakk> \<Longrightarrow> distinct (rev vs)
 3. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<notin> set (rev vs)\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram1 \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
[PROOF STEP]
apply (case_tac "zs")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>as bs ys zs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ c # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; ys @ c # zs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; distinct ys \<and> c \<notin> set zs \<and> distinct zs \<and> c \<notin> set ys \<and> set ys \<inter> set zs = {}; rev vs = ys @ c # zs; zs = []\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
 2. \<And>as bs ys zs a list. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ c # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; ys @ c # zs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; distinct ys \<and> c \<notin> set zs \<and> distinct zs \<and> c \<notin> set ys \<and> set ys \<inter> set zs = {}; rev vs = ys @ c # zs; zs = a # list\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
 3. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<in> set (rev vs)\<rbrakk> \<Longrightarrow> distinct (rev vs)
 4. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<notin> set (rev vs)\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram1 \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>as bs ys zs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ c # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; ys @ [c, ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; distinct ys \<and> c \<notin> set ys; rev vs = ys @ [c]; zs = []\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
 2. \<And>as bs ys zs a list. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ c # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; ys @ c # zs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; distinct ys \<and> c \<notin> set zs \<and> distinct zs \<and> c \<notin> set ys \<and> set ys \<inter> set zs = {}; rev vs = ys @ c # zs; zs = a # list\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
 3. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<in> set (rev vs)\<rbrakk> \<Longrightarrow> distinct (rev vs)
 4. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<notin> set (rev vs)\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram1 \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
[PROOF STEP]
apply (subgoal_tac "ys = as")
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>as bs ys zs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ c # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; ys @ [c, ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; distinct ys \<and> c \<notin> set ys; rev vs = ys @ [c]; zs = []; ys = as\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
 2. \<And>as bs ys zs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ c # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; ys @ [c, ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; distinct ys \<and> c \<notin> set ys; rev vs = ys @ [c]; zs = []\<rbrakk> \<Longrightarrow> ys = as
 3. \<And>as bs ys zs a list. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ c # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; ys @ c # zs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; distinct ys \<and> c \<notin> set zs \<and> distinct zs \<and> c \<notin> set ys \<and> set ys \<inter> set zs = {}; rev vs = ys @ c # zs; zs = a # list\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
 4. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<in> set (rev vs)\<rbrakk> \<Longrightarrow> distinct (rev vs)
 5. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<notin> set (rev vs)\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram1 \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
[PROOF STEP]
apply (simp add:rev_swap)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>as bs ys zs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ c # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; ys @ [c, ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; distinct ys \<and> c \<notin> set ys; rev vs = ys @ [c]; zs = []\<rbrakk> \<Longrightarrow> ys = as
 2. \<And>as bs ys zs a list. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ c # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; ys @ c # zs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; distinct ys \<and> c \<notin> set zs \<and> distinct zs \<and> c \<notin> set ys \<and> set ys \<inter> set zs = {}; rev vs = ys @ c # zs; zs = a # list\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
 3. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<in> set (rev vs)\<rbrakk> \<Longrightarrow> distinct (rev vs)
 4. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<notin> set (rev vs)\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram1 \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
[PROOF STEP]
apply (rule dist_at1)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>as bs ys zs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ c # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; ys @ [c, ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; distinct ys \<and> c \<notin> set ys; rev vs = ys @ [c]; zs = []\<rbrakk> \<Longrightarrow> distinct (?vs23 as bs ys zs)
 2. \<And>as bs ys zs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ c # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; ys @ [c, ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; distinct ys \<and> c \<notin> set ys; rev vs = ys @ [c]; zs = []\<rbrakk> \<Longrightarrow> ?vs23 as bs ys zs = ys @ ?r23 as bs ys zs # ?b23 as bs ys zs
 3. \<And>as bs ys zs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ c # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; ys @ [c, ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; distinct ys \<and> c \<notin> set ys; rev vs = ys @ [c]; zs = []\<rbrakk> \<Longrightarrow> ?vs23 as bs ys zs = as @ ?r23 as bs ys zs # ?d23 as bs ys zs
 4. \<And>as bs ys zs a list. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ c # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; ys @ c # zs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; distinct ys \<and> c \<notin> set zs \<and> distinct zs \<and> c \<notin> set ys \<and> set ys \<inter> set zs = {}; rev vs = ys @ c # zs; zs = a # list\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
 5. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<in> set (rev vs)\<rbrakk> \<Longrightarrow> distinct (rev vs)
 6. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<notin> set (rev vs)\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram1 \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
[PROOF STEP]
apply (rule dist_f12)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>as bs ys zs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ c # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; ys @ [c, ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; distinct ys \<and> c \<notin> set ys; rev vs = ys @ [c]; zs = []\<rbrakk> \<Longrightarrow> vertices f12 = ys @ ?r23 as bs ys zs # ?b23 as bs ys zs
 2. \<And>as bs ys zs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ c # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; ys @ [c, ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; distinct ys \<and> c \<notin> set ys; rev vs = ys @ [c]; zs = []\<rbrakk> \<Longrightarrow> vertices f12 = as @ ?r23 as bs ys zs # ?d23 as bs ys zs
 3. \<And>as bs ys zs a list. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ c # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; ys @ c # zs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; distinct ys \<and> c \<notin> set zs \<and> distinct zs \<and> c \<notin> set ys \<and> set ys \<inter> set zs = {}; rev vs = ys @ c # zs; zs = a # list\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
 4. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<in> set (rev vs)\<rbrakk> \<Longrightarrow> distinct (rev vs)
 5. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<notin> set (rev vs)\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram1 \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
[PROOF STEP]
apply (rule sym)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>as bs ys zs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ c # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; ys @ [c, ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; distinct ys \<and> c \<notin> set ys; rev vs = ys @ [c]; zs = []\<rbrakk> \<Longrightarrow> ys @ ?r23 as bs ys zs # ?b23 as bs ys zs = vertices f12
 2. \<And>as bs ys zs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ c # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; ys @ [c, ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; distinct ys \<and> c \<notin> set ys; rev vs = ys @ [c]; zs = []\<rbrakk> \<Longrightarrow> vertices f12 = as @ ?r23 as bs ys zs # ?d23 as bs ys zs
 3. \<And>as bs ys zs a list. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ c # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; ys @ c # zs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; distinct ys \<and> c \<notin> set zs \<and> distinct zs \<and> c \<notin> set ys \<and> set ys \<inter> set zs = {}; rev vs = ys @ c # zs; zs = a # list\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
 4. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<in> set (rev vs)\<rbrakk> \<Longrightarrow> distinct (rev vs)
 5. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<notin> set (rev vs)\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram1 \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>as bs ys zs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ c # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; ys @ [c, ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; distinct ys \<and> c \<notin> set ys; rev vs = ys @ [c]; zs = []\<rbrakk> \<Longrightarrow> vertices f12 = as @ c # ?d23 as bs ys zs
 2. \<And>as bs ys zs a list. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ c # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; ys @ c # zs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; distinct ys \<and> c \<notin> set zs \<and> distinct zs \<and> c \<notin> set ys \<and> set ys \<inter> set zs = {}; rev vs = ys @ c # zs; zs = a # list\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
 3. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<in> set (rev vs)\<rbrakk> \<Longrightarrow> distinct (rev vs)
 4. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<notin> set (rev vs)\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram1 \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>as bs ys zs a list. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ c # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; ys @ c # zs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; distinct ys \<and> c \<notin> set zs \<and> distinct zs \<and> c \<notin> set ys \<and> set ys \<inter> set zs = {}; rev vs = ys @ c # zs; zs = a # list\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
 2. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<in> set (rev vs)\<rbrakk> \<Longrightarrow> distinct (rev vs)
 3. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<notin> set (rev vs)\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram1 \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>as bs ys zs a list. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ c # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; ys @ c # a # list @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; distinct ys \<and> c \<noteq> a \<and> c \<notin> set list \<and> a \<notin> set list \<and> distinct list \<and> c \<notin> set ys \<and> a \<notin> set ys \<and> set ys \<inter> set list = {}; rev vs = ys @ c # a # list; zs = a # list\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
 2. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<in> set (rev vs)\<rbrakk> \<Longrightarrow> distinct (rev vs)
 3. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<notin> set (rev vs)\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram1 \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
[PROOF STEP]
apply (subgoal_tac "ys = as")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>as bs ys zs a list. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ c # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; ys @ c # a # list @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; distinct ys \<and> c \<noteq> a \<and> c \<notin> set list \<and> a \<notin> set list \<and> distinct list \<and> c \<notin> set ys \<and> a \<notin> set ys \<and> set ys \<inter> set list = {}; rev vs = ys @ c # a # list; zs = a # list; ys = as\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
 2. \<And>as bs ys zs a list. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ c # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; ys @ c # a # list @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; distinct ys \<and> c \<noteq> a \<and> c \<notin> set list \<and> a \<notin> set list \<and> distinct list \<and> c \<notin> set ys \<and> a \<notin> set ys \<and> set ys \<inter> set list = {}; rev vs = ys @ c # a # list; zs = a # list\<rbrakk> \<Longrightarrow> ys = as
 3. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<in> set (rev vs)\<rbrakk> \<Longrightarrow> distinct (rev vs)
 4. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<notin> set (rev vs)\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram1 \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
[PROOF STEP]
apply (simp add: Edges_def is_sublist_def rev_swap)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>as bs ys zs list. \<lbrakk>pre_split_face f ram1 ram2 (rev list @ d # c # rev as); f12 = Face (as @ c # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # rev list @ d # c # rev as) Nonfinal; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> (if as = [] then ram2 else last (rev as)); list @ [ram1, ram2] = bs; c \<noteq> ram1; distinct as \<and> c \<noteq> d \<and> c \<notin> set list \<and> d \<notin> set list \<and> distinct list \<and> c \<notin> set as \<and> d \<notin> set as \<and> set as \<inter> set list = {}; vs = rev list @ d # c # rev as; zs = d # list; ys = as\<rbrakk> \<Longrightarrow> (as = [] \<longrightarrow> c = hd (rev list @ [d, c]) \<and> d = ram1 \<or> (\<exists>as bs. rev list @ [d, c] = as @ d # c # bs)) \<and> (as \<noteq> [] \<longrightarrow> c = hd (rev list @ d # c # rev as) \<and> d = ram1 \<or> c = ram2 \<and> d = last (rev as) \<or> (\<exists>asa bs. rev list @ d # c # rev as = asa @ d # c # bs))
 2. \<And>as bs ys zs a list. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ c # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; ys @ c # a # list @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; distinct ys \<and> c \<noteq> a \<and> c \<notin> set list \<and> a \<notin> set list \<and> distinct list \<and> c \<notin> set ys \<and> a \<notin> set ys \<and> set ys \<inter> set list = {}; rev vs = ys @ c # a # list; zs = a # list\<rbrakk> \<Longrightarrow> ys = as
 3. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<in> set (rev vs)\<rbrakk> \<Longrightarrow> distinct (rev vs)
 4. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<notin> set (rev vs)\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram1 \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>as bs ys zs list. \<lbrakk>pre_split_face f ram1 ram2 (rev list @ d # c # rev as); f12 = Face (as @ c # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # rev list @ d # c # rev as) Nonfinal; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> (if as = [] then ram2 else last (rev as)); list @ [ram1, ram2] = bs; c \<noteq> ram1; distinct as \<and> c \<noteq> d \<and> c \<notin> set list \<and> d \<notin> set list \<and> distinct list \<and> c \<notin> set as \<and> d \<notin> set as \<and> set as \<inter> set list = {}; vs = rev list @ d # c # rev as; zs = d # list; ys = as\<rbrakk> \<Longrightarrow> as = [] \<longrightarrow> c = hd (rev list @ [d, c]) \<and> d = ram1 \<or> (\<exists>as bs. rev list @ [d, c] = as @ d # c # bs)
 2. \<And>as bs ys zs list. \<lbrakk>pre_split_face f ram1 ram2 (rev list @ d # c # rev as); f12 = Face (as @ c # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # rev list @ d # c # rev as) Nonfinal; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> (if as = [] then ram2 else last (rev as)); list @ [ram1, ram2] = bs; c \<noteq> ram1; distinct as \<and> c \<noteq> d \<and> c \<notin> set list \<and> d \<notin> set list \<and> distinct list \<and> c \<notin> set as \<and> d \<notin> set as \<and> set as \<inter> set list = {}; vs = rev list @ d # c # rev as; zs = d # list; ys = as\<rbrakk> \<Longrightarrow> as \<noteq> [] \<longrightarrow> c = hd (rev list @ d # c # rev as) \<and> d = ram1 \<or> c = ram2 \<and> d = last (rev as) \<or> (\<exists>asa bs. rev list @ d # c # rev as = asa @ d # c # bs)
 3. \<And>as bs ys zs a list. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ c # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; ys @ c # a # list @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; distinct ys \<and> c \<noteq> a \<and> c \<notin> set list \<and> a \<notin> set list \<and> distinct list \<and> c \<notin> set ys \<and> a \<notin> set ys \<and> set ys \<inter> set list = {}; rev vs = ys @ c # a # list; zs = a # list\<rbrakk> \<Longrightarrow> ys = as
 4. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<in> set (rev vs)\<rbrakk> \<Longrightarrow> distinct (rev vs)
 5. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<notin> set (rev vs)\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram1 \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
[PROOF STEP]
apply (subgoal_tac "\<exists>as bs. rev list @ [d, c] = as @ d # c # bs")
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<And>as bs ys zs list. \<lbrakk>pre_split_face f ram1 ram2 (rev list @ d # c # rev as); f12 = Face (as @ c # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # rev list @ d # c # rev as) Nonfinal; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> (if as = [] then ram2 else last (rev as)); list @ [ram1, ram2] = bs; c \<noteq> ram1; distinct as \<and> c \<noteq> d \<and> c \<notin> set list \<and> d \<notin> set list \<and> distinct list \<and> c \<notin> set as \<and> d \<notin> set as \<and> set as \<inter> set list = {}; vs = rev list @ d # c # rev as; zs = d # list; ys = as; \<exists>as bs. rev list @ [d, c] = as @ d # c # bs\<rbrakk> \<Longrightarrow> as = [] \<longrightarrow> c = hd (rev list @ [d, c]) \<and> d = ram1 \<or> (\<exists>as bs. rev list @ [d, c] = as @ d # c # bs)
 2. \<And>as bs ys zs list. \<lbrakk>pre_split_face f ram1 ram2 (rev list @ d # c # rev as); f12 = Face (as @ c # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # rev list @ d # c # rev as) Nonfinal; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> (if as = [] then ram2 else last (rev as)); list @ [ram1, ram2] = bs; c \<noteq> ram1; distinct as \<and> c \<noteq> d \<and> c \<notin> set list \<and> d \<notin> set list \<and> distinct list \<and> c \<notin> set as \<and> d \<notin> set as \<and> set as \<inter> set list = {}; vs = rev list @ d # c # rev as; zs = d # list; ys = as\<rbrakk> \<Longrightarrow> \<exists>as bs. rev list @ [d, c] = as @ d # c # bs
 3. \<And>as bs ys zs list. \<lbrakk>pre_split_face f ram1 ram2 (rev list @ d # c # rev as); f12 = Face (as @ c # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # rev list @ d # c # rev as) Nonfinal; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> (if as = [] then ram2 else last (rev as)); list @ [ram1, ram2] = bs; c \<noteq> ram1; distinct as \<and> c \<noteq> d \<and> c \<notin> set list \<and> d \<notin> set list \<and> distinct list \<and> c \<notin> set as \<and> d \<notin> set as \<and> set as \<inter> set list = {}; vs = rev list @ d # c # rev as; zs = d # list; ys = as\<rbrakk> \<Longrightarrow> as \<noteq> [] \<longrightarrow> c = hd (rev list @ d # c # rev as) \<and> d = ram1 \<or> c = ram2 \<and> d = last (rev as) \<or> (\<exists>asa bs. rev list @ d # c # rev as = asa @ d # c # bs)
 4. \<And>as bs ys zs a list. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ c # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; ys @ c # a # list @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; distinct ys \<and> c \<noteq> a \<and> c \<notin> set list \<and> a \<notin> set list \<and> distinct list \<and> c \<notin> set ys \<and> a \<notin> set ys \<and> set ys \<inter> set list = {}; rev vs = ys @ c # a # list; zs = a # list\<rbrakk> \<Longrightarrow> ys = as
 5. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<in> set (rev vs)\<rbrakk> \<Longrightarrow> distinct (rev vs)
 6. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<notin> set (rev vs)\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram1 \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>as bs ys zs list. \<lbrakk>pre_split_face f ram1 ram2 (rev list @ d # c # rev as); f12 = Face (as @ c # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # rev list @ d # c # rev as) Nonfinal; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> (if as = [] then ram2 else last (rev as)); list @ [ram1, ram2] = bs; c \<noteq> ram1; distinct as \<and> c \<noteq> d \<and> c \<notin> set list \<and> d \<notin> set list \<and> distinct list \<and> c \<notin> set as \<and> d \<notin> set as \<and> set as \<inter> set list = {}; vs = rev list @ d # c # rev as; zs = d # list; ys = as\<rbrakk> \<Longrightarrow> \<exists>as bs. rev list @ [d, c] = as @ d # c # bs
 2. \<And>as bs ys zs list. \<lbrakk>pre_split_face f ram1 ram2 (rev list @ d # c # rev as); f12 = Face (as @ c # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # rev list @ d # c # rev as) Nonfinal; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> (if as = [] then ram2 else last (rev as)); list @ [ram1, ram2] = bs; c \<noteq> ram1; distinct as \<and> c \<noteq> d \<and> c \<notin> set list \<and> d \<notin> set list \<and> distinct list \<and> c \<notin> set as \<and> d \<notin> set as \<and> set as \<inter> set list = {}; vs = rev list @ d # c # rev as; zs = d # list; ys = as\<rbrakk> \<Longrightarrow> as \<noteq> [] \<longrightarrow> c = hd (rev list @ d # c # rev as) \<and> d = ram1 \<or> c = ram2 \<and> d = last (rev as) \<or> (\<exists>asa bs. rev list @ d # c # rev as = asa @ d # c # bs)
 3. \<And>as bs ys zs a list. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ c # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; ys @ c # a # list @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; distinct ys \<and> c \<noteq> a \<and> c \<notin> set list \<and> a \<notin> set list \<and> distinct list \<and> c \<notin> set ys \<and> a \<notin> set ys \<and> set ys \<inter> set list = {}; rev vs = ys @ c # a # list; zs = a # list\<rbrakk> \<Longrightarrow> ys = as
 4. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<in> set (rev vs)\<rbrakk> \<Longrightarrow> distinct (rev vs)
 5. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<notin> set (rev vs)\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram1 \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
[PROOF STEP]
apply (intro exI)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>as bs ys zs list. \<lbrakk>pre_split_face f ram1 ram2 (rev list @ d # c # rev as); f12 = Face (as @ c # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # rev list @ d # c # rev as) Nonfinal; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> (if as = [] then ram2 else last (rev as)); list @ [ram1, ram2] = bs; c \<noteq> ram1; distinct as \<and> c \<noteq> d \<and> c \<notin> set list \<and> d \<notin> set list \<and> distinct list \<and> c \<notin> set as \<and> d \<notin> set as \<and> set as \<inter> set list = {}; vs = rev list @ d # c # rev as; zs = d # list; ys = as\<rbrakk> \<Longrightarrow> rev list @ [d, c] = ?as39 as bs ys zs list @ d # c # ?bs40 as bs ys zs list
 2. \<And>as bs ys zs list. \<lbrakk>pre_split_face f ram1 ram2 (rev list @ d # c # rev as); f12 = Face (as @ c # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # rev list @ d # c # rev as) Nonfinal; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> (if as = [] then ram2 else last (rev as)); list @ [ram1, ram2] = bs; c \<noteq> ram1; distinct as \<and> c \<noteq> d \<and> c \<notin> set list \<and> d \<notin> set list \<and> distinct list \<and> c \<notin> set as \<and> d \<notin> set as \<and> set as \<inter> set list = {}; vs = rev list @ d # c # rev as; zs = d # list; ys = as\<rbrakk> \<Longrightarrow> as \<noteq> [] \<longrightarrow> c = hd (rev list @ d # c # rev as) \<and> d = ram1 \<or> c = ram2 \<and> d = last (rev as) \<or> (\<exists>asa bs. rev list @ d # c # rev as = asa @ d # c # bs)
 3. \<And>as bs ys zs a list. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ c # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; ys @ c # a # list @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; distinct ys \<and> c \<noteq> a \<and> c \<notin> set list \<and> a \<notin> set list \<and> distinct list \<and> c \<notin> set ys \<and> a \<notin> set ys \<and> set ys \<inter> set list = {}; rev vs = ys @ c # a # list; zs = a # list\<rbrakk> \<Longrightarrow> ys = as
 4. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<in> set (rev vs)\<rbrakk> \<Longrightarrow> distinct (rev vs)
 5. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<notin> set (rev vs)\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram1 \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>as bs ys zs list. \<lbrakk>pre_split_face f ram1 ram2 (rev list @ d # c # rev as); f12 = Face (as @ c # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # rev list @ d # c # rev as) Nonfinal; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> (if as = [] then ram2 else last (rev as)); list @ [ram1, ram2] = bs; c \<noteq> ram1; distinct as \<and> c \<noteq> d \<and> c \<notin> set list \<and> d \<notin> set list \<and> distinct list \<and> c \<notin> set as \<and> d \<notin> set as \<and> set as \<inter> set list = {}; vs = rev list @ d # c # rev as; zs = d # list; ys = as\<rbrakk> \<Longrightarrow> as \<noteq> [] \<longrightarrow> c = hd (rev list @ d # c # rev as) \<and> d = ram1 \<or> c = ram2 \<and> d = last (rev as) \<or> (\<exists>asa bs. rev list @ d # c # rev as = asa @ d # c # bs)
 2. \<And>as bs ys zs a list. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ c # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; ys @ c # a # list @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; distinct ys \<and> c \<noteq> a \<and> c \<notin> set list \<and> a \<notin> set list \<and> distinct list \<and> c \<notin> set ys \<and> a \<notin> set ys \<and> set ys \<inter> set list = {}; rev vs = ys @ c # a # list; zs = a # list\<rbrakk> \<Longrightarrow> ys = as
 3. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<in> set (rev vs)\<rbrakk> \<Longrightarrow> distinct (rev vs)
 4. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<notin> set (rev vs)\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram1 \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
[PROOF STEP]
apply (subgoal_tac "\<exists>asa bs. rev list @ d # c # rev as = asa @ d # c # bs")
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>as bs ys zs list. \<lbrakk>pre_split_face f ram1 ram2 (rev list @ d # c # rev as); f12 = Face (as @ c # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # rev list @ d # c # rev as) Nonfinal; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> (if as = [] then ram2 else last (rev as)); list @ [ram1, ram2] = bs; c \<noteq> ram1; distinct as \<and> c \<noteq> d \<and> c \<notin> set list \<and> d \<notin> set list \<and> distinct list \<and> c \<notin> set as \<and> d \<notin> set as \<and> set as \<inter> set list = {}; vs = rev list @ d # c # rev as; zs = d # list; ys = as; \<exists>asa bs. rev list @ d # c # rev as = asa @ d # c # bs\<rbrakk> \<Longrightarrow> as \<noteq> [] \<longrightarrow> c = hd (rev list @ d # c # rev as) \<and> d = ram1 \<or> c = ram2 \<and> d = last (rev as) \<or> (\<exists>asa bs. rev list @ d # c # rev as = asa @ d # c # bs)
 2. \<And>as bs ys zs list. \<lbrakk>pre_split_face f ram1 ram2 (rev list @ d # c # rev as); f12 = Face (as @ c # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # rev list @ d # c # rev as) Nonfinal; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> (if as = [] then ram2 else last (rev as)); list @ [ram1, ram2] = bs; c \<noteq> ram1; distinct as \<and> c \<noteq> d \<and> c \<notin> set list \<and> d \<notin> set list \<and> distinct list \<and> c \<notin> set as \<and> d \<notin> set as \<and> set as \<inter> set list = {}; vs = rev list @ d # c # rev as; zs = d # list; ys = as\<rbrakk> \<Longrightarrow> \<exists>asa bs. rev list @ d # c # rev as = asa @ d # c # bs
 3. \<And>as bs ys zs a list. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ c # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; ys @ c # a # list @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; distinct ys \<and> c \<noteq> a \<and> c \<notin> set list \<and> a \<notin> set list \<and> distinct list \<and> c \<notin> set ys \<and> a \<notin> set ys \<and> set ys \<inter> set list = {}; rev vs = ys @ c # a # list; zs = a # list\<rbrakk> \<Longrightarrow> ys = as
 4. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<in> set (rev vs)\<rbrakk> \<Longrightarrow> distinct (rev vs)
 5. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<notin> set (rev vs)\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram1 \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>as bs ys zs list. \<lbrakk>pre_split_face f ram1 ram2 (rev list @ d # c # rev as); f12 = Face (as @ c # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # rev list @ d # c # rev as) Nonfinal; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> (if as = [] then ram2 else last (rev as)); list @ [ram1, ram2] = bs; c \<noteq> ram1; distinct as \<and> c \<noteq> d \<and> c \<notin> set list \<and> d \<notin> set list \<and> distinct list \<and> c \<notin> set as \<and> d \<notin> set as \<and> set as \<inter> set list = {}; vs = rev list @ d # c # rev as; zs = d # list; ys = as\<rbrakk> \<Longrightarrow> \<exists>asa bs. rev list @ d # c # rev as = asa @ d # c # bs
 2. \<And>as bs ys zs a list. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ c # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; ys @ c # a # list @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; distinct ys \<and> c \<noteq> a \<and> c \<notin> set list \<and> a \<notin> set list \<and> distinct list \<and> c \<notin> set ys \<and> a \<notin> set ys \<and> set ys \<inter> set list = {}; rev vs = ys @ c # a # list; zs = a # list\<rbrakk> \<Longrightarrow> ys = as
 3. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<in> set (rev vs)\<rbrakk> \<Longrightarrow> distinct (rev vs)
 4. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<notin> set (rev vs)\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram1 \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
[PROOF STEP]
apply (intro exI)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>as bs ys zs list. \<lbrakk>pre_split_face f ram1 ram2 (rev list @ d # c # rev as); f12 = Face (as @ c # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # rev list @ d # c # rev as) Nonfinal; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> (if as = [] then ram2 else last (rev as)); list @ [ram1, ram2] = bs; c \<noteq> ram1; distinct as \<and> c \<noteq> d \<and> c \<notin> set list \<and> d \<notin> set list \<and> distinct list \<and> c \<notin> set as \<and> d \<notin> set as \<and> set as \<inter> set list = {}; vs = rev list @ d # c # rev as; zs = d # list; ys = as\<rbrakk> \<Longrightarrow> rev list @ d # c # rev as = ?asa43 as bs ys zs list @ d # c # ?bs44 as bs ys zs list
 2. \<And>as bs ys zs a list. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ c # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; ys @ c # a # list @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; distinct ys \<and> c \<noteq> a \<and> c \<notin> set list \<and> a \<notin> set list \<and> distinct list \<and> c \<notin> set ys \<and> a \<notin> set ys \<and> set ys \<inter> set list = {}; rev vs = ys @ c # a # list; zs = a # list\<rbrakk> \<Longrightarrow> ys = as
 3. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<in> set (rev vs)\<rbrakk> \<Longrightarrow> distinct (rev vs)
 4. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<notin> set (rev vs)\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram1 \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>as bs ys zs a list. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ c # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; ys @ c # a # list @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; distinct ys \<and> c \<noteq> a \<and> c \<notin> set list \<and> a \<notin> set list \<and> distinct list \<and> c \<notin> set ys \<and> a \<notin> set ys \<and> set ys \<inter> set list = {}; rev vs = ys @ c # a # list; zs = a # list\<rbrakk> \<Longrightarrow> ys = as
 2. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<in> set (rev vs)\<rbrakk> \<Longrightarrow> distinct (rev vs)
 3. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<notin> set (rev vs)\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram1 \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
[PROOF STEP]
apply (rule dist_at1)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>as bs ys zs a list. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ c # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; ys @ c # a # list @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; distinct ys \<and> c \<noteq> a \<and> c \<notin> set list \<and> a \<notin> set list \<and> distinct list \<and> c \<notin> set ys \<and> a \<notin> set ys \<and> set ys \<inter> set list = {}; rev vs = ys @ c # a # list; zs = a # list\<rbrakk> \<Longrightarrow> distinct (?vs46 as bs ys zs a list)
 2. \<And>as bs ys zs a list. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ c # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; ys @ c # a # list @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; distinct ys \<and> c \<noteq> a \<and> c \<notin> set list \<and> a \<notin> set list \<and> distinct list \<and> c \<notin> set ys \<and> a \<notin> set ys \<and> set ys \<inter> set list = {}; rev vs = ys @ c # a # list; zs = a # list\<rbrakk> \<Longrightarrow> ?vs46 as bs ys zs a list = ys @ ?r46 as bs ys zs a list # ?b46 as bs ys zs a list
 3. \<And>as bs ys zs a list. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ c # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; ys @ c # a # list @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; distinct ys \<and> c \<noteq> a \<and> c \<notin> set list \<and> a \<notin> set list \<and> distinct list \<and> c \<notin> set ys \<and> a \<notin> set ys \<and> set ys \<inter> set list = {}; rev vs = ys @ c # a # list; zs = a # list\<rbrakk> \<Longrightarrow> ?vs46 as bs ys zs a list = as @ ?r46 as bs ys zs a list # ?d46 as bs ys zs a list
 4. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<in> set (rev vs)\<rbrakk> \<Longrightarrow> distinct (rev vs)
 5. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<notin> set (rev vs)\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram1 \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
[PROOF STEP]
apply (rule dist_f12)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>as bs ys zs a list. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ c # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; ys @ c # a # list @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; distinct ys \<and> c \<noteq> a \<and> c \<notin> set list \<and> a \<notin> set list \<and> distinct list \<and> c \<notin> set ys \<and> a \<notin> set ys \<and> set ys \<inter> set list = {}; rev vs = ys @ c # a # list; zs = a # list\<rbrakk> \<Longrightarrow> vertices f12 = ys @ ?r46 as bs ys zs a list # ?b46 as bs ys zs a list
 2. \<And>as bs ys zs a list. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ c # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; ys @ c # a # list @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; distinct ys \<and> c \<noteq> a \<and> c \<notin> set list \<and> a \<notin> set list \<and> distinct list \<and> c \<notin> set ys \<and> a \<notin> set ys \<and> set ys \<inter> set list = {}; rev vs = ys @ c # a # list; zs = a # list\<rbrakk> \<Longrightarrow> vertices f12 = as @ ?r46 as bs ys zs a list # ?d46 as bs ys zs a list
 3. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<in> set (rev vs)\<rbrakk> \<Longrightarrow> distinct (rev vs)
 4. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<notin> set (rev vs)\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram1 \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
[PROOF STEP]
apply (rule sym)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>as bs ys zs a list. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ c # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; ys @ c # a # list @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; distinct ys \<and> c \<noteq> a \<and> c \<notin> set list \<and> a \<notin> set list \<and> distinct list \<and> c \<notin> set ys \<and> a \<notin> set ys \<and> set ys \<inter> set list = {}; rev vs = ys @ c # a # list; zs = a # list\<rbrakk> \<Longrightarrow> ys @ ?r46 as bs ys zs a list # ?b46 as bs ys zs a list = vertices f12
 2. \<And>as bs ys zs a list. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ c # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; ys @ c # a # list @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; distinct ys \<and> c \<noteq> a \<and> c \<notin> set list \<and> a \<notin> set list \<and> distinct list \<and> c \<notin> set ys \<and> a \<notin> set ys \<and> set ys \<inter> set list = {}; rev vs = ys @ c # a # list; zs = a # list\<rbrakk> \<Longrightarrow> vertices f12 = as @ ?r46 as bs ys zs a list # ?d46 as bs ys zs a list
 3. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<in> set (rev vs)\<rbrakk> \<Longrightarrow> distinct (rev vs)
 4. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<notin> set (rev vs)\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram1 \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>as bs ys zs a list. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ c # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; ys @ c # a # list @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; distinct ys \<and> c \<noteq> a \<and> c \<notin> set list \<and> a \<notin> set list \<and> distinct list \<and> c \<notin> set ys \<and> a \<notin> set ys \<and> set ys \<inter> set list = {}; rev vs = ys @ c # a # list; zs = a # list\<rbrakk> \<Longrightarrow> vertices f12 = as @ c # ?d46 as bs ys zs a list
 2. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<in> set (rev vs)\<rbrakk> \<Longrightarrow> distinct (rev vs)
 3. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<notin> set (rev vs)\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram1 \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<in> set (rev vs)\<rbrakk> \<Longrightarrow> distinct (rev vs)
 2. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<notin> set (rev vs)\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram1 \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
[PROOF STEP]
apply (simp add: pre_split_face_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<notin> set (rev vs)\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram1 \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
[PROOF STEP]
(* c \<notin> set vs *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<notin> set (rev vs)\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram1 \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
[PROOF STEP]
apply (subgoal_tac "c = ram2")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<notin> set (rev vs); c = ram2\<rbrakk> \<Longrightarrow> c = hd vs \<and> d = ram1 \<or> c = ram1 \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs
 2. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<notin> set (rev vs)\<rbrakk> \<Longrightarrow> c = ram2
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ ram2 # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ ram2 # d # bs; ram2 \<noteq> ram1; ram2 \<notin> set vs; c = ram2\<rbrakk> \<Longrightarrow> ram2 = hd vs \<and> d = ram1 \<or> (d, ram2) \<in> Edges vs
 2. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<notin> set (rev vs)\<rbrakk> \<Longrightarrow> c = ram2
[PROOF STEP]
apply (subgoal_tac "rev vs @ [ram1] = as")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ ram2 # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ ram2 # d # bs; ram2 \<noteq> ram1; ram2 \<notin> set vs; c = ram2; rev vs @ [ram1] = as\<rbrakk> \<Longrightarrow> ram2 = hd vs \<and> d = ram1 \<or> (d, ram2) \<in> Edges vs
 2. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ ram2 # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ ram2 # d # bs; ram2 \<noteq> ram1; ram2 \<notin> set vs; c = ram2\<rbrakk> \<Longrightarrow> rev vs @ [ram1] = as
 3. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<notin> set (rev vs)\<rbrakk> \<Longrightarrow> c = ram2
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ ram2 # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ ram2 # d # bs; ram2 \<noteq> ram1; ram2 \<notin> set vs; c = ram2\<rbrakk> \<Longrightarrow> rev vs @ [ram1] = as
 2. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<notin> set (rev vs)\<rbrakk> \<Longrightarrow> c = ram2
[PROOF STEP]
apply (rule dist_at1)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ ram2 # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ ram2 # d # bs; ram2 \<noteq> ram1; ram2 \<notin> set vs; c = ram2\<rbrakk> \<Longrightarrow> distinct (?vs60 as bs)
 2. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ ram2 # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ ram2 # d # bs; ram2 \<noteq> ram1; ram2 \<notin> set vs; c = ram2\<rbrakk> \<Longrightarrow> ?vs60 as bs = (rev vs @ [ram1]) @ ?r60 as bs # ?b60 as bs
 3. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ ram2 # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ ram2 # d # bs; ram2 \<noteq> ram1; ram2 \<notin> set vs; c = ram2\<rbrakk> \<Longrightarrow> ?vs60 as bs = as @ ?r60 as bs # ?d60 as bs
 4. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<notin> set (rev vs)\<rbrakk> \<Longrightarrow> c = ram2
[PROOF STEP]
apply (rule dist_f12)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ ram2 # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ ram2 # d # bs; ram2 \<noteq> ram1; ram2 \<notin> set vs; c = ram2\<rbrakk> \<Longrightarrow> vertices f12 = (rev vs @ [ram1]) @ ?r60 as bs # ?b60 as bs
 2. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ ram2 # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ ram2 # d # bs; ram2 \<noteq> ram1; ram2 \<notin> set vs; c = ram2\<rbrakk> \<Longrightarrow> vertices f12 = as @ ?r60 as bs # ?d60 as bs
 3. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<notin> set (rev vs)\<rbrakk> \<Longrightarrow> c = ram2
[PROOF STEP]
apply (rule sym)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ ram2 # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ ram2 # d # bs; ram2 \<noteq> ram1; ram2 \<notin> set vs; c = ram2\<rbrakk> \<Longrightarrow> (rev vs @ [ram1]) @ ?r60 as bs # ?b60 as bs = vertices f12
 2. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ ram2 # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ ram2 # d # bs; ram2 \<noteq> ram1; ram2 \<notin> set vs; c = ram2\<rbrakk> \<Longrightarrow> vertices f12 = as @ ?r60 as bs # ?d60 as bs
 3. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<notin> set (rev vs)\<rbrakk> \<Longrightarrow> c = ram2
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (as @ ram2 # d # bs) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ ram2 # d # bs; ram2 \<noteq> ram1; ram2 \<notin> set vs; c = ram2\<rbrakk> \<Longrightarrow> vertices f12 = as @ ram2 # ?d60 as bs
 2. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<notin> set (rev vs)\<rbrakk> \<Longrightarrow> c = ram2
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<notin> set (rev vs)\<rbrakk> \<Longrightarrow> c = ram2
[PROOF STEP]
(* c \<noteq> ram2 *)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<notin> set (rev vs)\<rbrakk> \<Longrightarrow> c = ram2
[PROOF STEP]
apply (subgoal_tac "c \<in> set (rev vs @ ram1 # [ram2])")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<notin> set (rev vs); c \<in> set (rev vs @ [ram1, ram2])\<rbrakk> \<Longrightarrow> c = ram2
 2. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<notin> set (rev vs)\<rbrakk> \<Longrightarrow> c \<in> set (rev vs @ [ram1, ram2])
[PROOF STEP]
apply (thin_tac "rev vs @ ram1 # [ram2] = as @ c # d # bs")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; c \<noteq> ram1; c \<notin> set (rev vs); c \<in> set (rev vs @ [ram1, ram2])\<rbrakk> \<Longrightarrow> c = ram2
 2. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<notin> set (rev vs)\<rbrakk> \<Longrightarrow> c \<in> set (rev vs @ [ram1, ram2])
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = ram2 \<longrightarrow> d \<noteq> last vs; rev vs @ [ram1, ram2] = as @ c # d # bs; c \<noteq> ram1; c \<notin> set (rev vs)\<rbrakk> \<Longrightarrow> c \<in> set (rev vs @ [ram1, ram2])
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<in> {(hd vs, ram1), (ram1, ram2), (ram2, last vs)} \<union> Edges (rev vs)

goal (1 subgoal):
 1. \<And>x. x \<in> {(hd vs, ram1), (ram1, ram2), (ram2, last vs)} \<union> Edges (rev vs) \<Longrightarrow> x \<in> \<E> f12
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {(hd vs, ram1), (ram1, ram2), (ram2, last vs)} \<union> Edges (rev vs) \<Longrightarrow> x \<in> \<E> f12
[PROOF STEP]
fix x
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x. x \<in> {(hd vs, ram1), (ram1, ram2), (ram2, last vs)} \<union> Edges (rev vs) \<Longrightarrow> x \<in> \<E> f12
[PROOF STEP]
assume x: "x \<in> ?rhs"
[PROOF STATE]
proof (state)
this:
x \<in> {(hd vs, ram1), (ram1, ram2), (ram2, last vs)} \<union> Edges (rev vs)

goal (1 subgoal):
 1. \<And>x. x \<in> {(hd vs, ram1), (ram1, ram2), (ram2, last vs)} \<union> Edges (rev vs) \<Longrightarrow> x \<in> \<E> f12
[PROOF STEP]
define c where "c = fst x"
[PROOF STATE]
proof (state)
this:
c = fst x

goal (1 subgoal):
 1. \<And>x. x \<in> {(hd vs, ram1), (ram1, ram2), (ram2, last vs)} \<union> Edges (rev vs) \<Longrightarrow> x \<in> \<E> f12
[PROOF STEP]
define d where "d = snd x"
[PROOF STATE]
proof (state)
this:
d = snd x

goal (1 subgoal):
 1. \<And>x. x \<in> {(hd vs, ram1), (ram1, ram2), (ram2, last vs)} \<union> Edges (rev vs) \<Longrightarrow> x \<in> \<E> f12
[PROOF STEP]
with c_def
[PROOF STATE]
proof (chain)
picking this:
c = fst x
d = snd x
[PROOF STEP]
have [simp]: "x = (c,d)"
[PROOF STATE]
proof (prove)
using this:
c = fst x
d = snd x

goal (1 subgoal):
 1. x = (c, d)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x = (c, d)

goal (1 subgoal):
 1. \<And>x. x \<in> {(hd vs, ram1), (ram1, ram2), (ram2, last vs)} \<union> Edges (rev vs) \<Longrightarrow> x \<in> \<E> f12
[PROOF STEP]
from vors
[PROOF STATE]
proof (chain)
picking this:
pre_split_face f ram1 ram2 vs
(f12, f21) = split_face f ram1 ram2 vs
vs \<noteq> []
between (vertices f) ram1 ram2 = []
[PROOF STEP]
have dist_f12: "distinct (vertices f12)"
[PROOF STATE]
proof (prove)
using this:
pre_split_face f ram1 ram2 vs
(f12, f21) = split_face f ram1 ram2 vs
vs \<noteq> []
between (vertices f) ram1 ram2 = []

goal (1 subgoal):
 1. distinct (vertices f12)
[PROOF STEP]
apply (rule_tac split_face_distinct1)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pre_split_face f ram1 ram2 vs; (f12, f21) = split_face f ram1 ram2 vs; vs \<noteq> []; between (vertices f) ram1 ram2 = []\<rbrakk> \<Longrightarrow> (f12, ?f21.4) = split_face ?oldF4 ?ram1.4 ?ram2.4 ?newVertexList4
 2. \<lbrakk>pre_split_face f ram1 ram2 vs; (f12, f21) = split_face f ram1 ram2 vs; vs \<noteq> []; between (vertices f) ram1 ram2 = []\<rbrakk> \<Longrightarrow> pre_split_face ?oldF4 ?ram1.4 ?ram2.4 ?newVertexList4
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
distinct (vertices f12)

goal (1 subgoal):
 1. \<And>x. x \<in> {(hd vs, ram1), (ram1, ram2), (ram2, last vs)} \<union> Edges (rev vs) \<Longrightarrow> x \<in> \<E> f12
[PROOF STEP]
from x vors
[PROOF STATE]
proof (chain)
picking this:
x \<in> {(hd vs, ram1), (ram1, ram2), (ram2, last vs)} \<union> Edges (rev vs)
pre_split_face f ram1 ram2 vs
(f12, f21) = split_face f ram1 ram2 vs
vs \<noteq> []
between (vertices f) ram1 ram2 = []
[PROOF STEP]
show "x \<in> ?lhs"
[PROOF STATE]
proof (prove)
using this:
x \<in> {(hd vs, ram1), (ram1, ram2), (ram2, last vs)} \<union> Edges (rev vs)
pre_split_face f ram1 ram2 vs
(f12, f21) = split_face f ram1 ram2 vs
vs \<noteq> []
between (vertices f) ram1 ram2 = []

goal (1 subgoal):
 1. x \<in> \<E> f12
[PROOF STEP]
apply (simp add: dist_f12 is_nextElem_def is_sublist_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c = hd vs \<and> d = ram1 \<or> c = ram1 \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs; pre_split_face f ram1 ram2 vs; (f12, f21) = split_face f ram1 ram2 vs; vs \<noteq> []; between (vertices f) ram1 ram2 = []\<rbrakk> \<Longrightarrow> (\<exists>as bs. vertices f12 = as @ c # d # bs) \<or> vertices f12 \<noteq> [] \<and> c = last (vertices f12) \<and> d = hd (vertices f12)
[PROOF STEP]
apply (simp add: split_face_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c = hd vs \<and> d = ram1 \<or> c = ram1 \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs; pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []\<rbrakk> \<Longrightarrow> (\<exists>as bs. rev vs @ [ram1, ram2] = as @ c # d # bs) \<or> c = ram2 \<and> d = last vs
[PROOF STEP]
apply (case_tac "c = hd vs \<and> d = ram1")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>c = hd vs \<and> d = ram1 \<or> c = ram1 \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs; pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = hd vs \<and> d = ram1\<rbrakk> \<Longrightarrow> (\<exists>as bs. rev vs @ [ram1, ram2] = as @ c # d # bs) \<or> c = ram2 \<and> d = last vs
 2. \<lbrakk>c = hd vs \<and> d = ram1 \<or> c = ram1 \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs; pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; \<not> (c = hd vs \<and> d = ram1)\<rbrakk> \<Longrightarrow> (\<exists>as bs. rev vs @ [ram1, ram2] = as @ c # d # bs) \<or> c = ram2 \<and> d = last vs
[PROOF STEP]
apply (case_tac "vs")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>c = hd vs \<and> d = ram1 \<or> c = ram1 \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs; pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = hd vs \<and> d = ram1; vs = []\<rbrakk> \<Longrightarrow> (\<exists>as bs. rev vs @ [ram1, ram2] = as @ c # d # bs) \<or> c = ram2 \<and> d = last vs
 2. \<And>a list. \<lbrakk>c = hd vs \<and> d = ram1 \<or> c = ram1 \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs; pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = hd vs \<and> d = ram1; vs = a # list\<rbrakk> \<Longrightarrow> (\<exists>as bs. rev vs @ [ram1, ram2] = as @ c # d # bs) \<or> c = ram2 \<and> d = last vs
 3. \<lbrakk>c = hd vs \<and> d = ram1 \<or> c = ram1 \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs; pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; \<not> (c = hd vs \<and> d = ram1)\<rbrakk> \<Longrightarrow> (\<exists>as bs. rev vs @ [ram1, ram2] = as @ c # d # bs) \<or> c = ram2 \<and> d = last vs
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a list. \<lbrakk>c = hd vs \<and> d = ram1 \<or> c = ram1 \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs; pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = hd vs \<and> d = ram1; vs = a # list\<rbrakk> \<Longrightarrow> (\<exists>as bs. rev vs @ [ram1, ram2] = as @ c # d # bs) \<or> c = ram2 \<and> d = last vs
 2. \<lbrakk>c = hd vs \<and> d = ram1 \<or> c = ram1 \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs; pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; \<not> (c = hd vs \<and> d = ram1)\<rbrakk> \<Longrightarrow> (\<exists>as bs. rev vs @ [ram1, ram2] = as @ c # d # bs) \<or> c = ram2 \<and> d = last vs
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c = hd vs \<and> d = ram1 \<or> c = ram1 \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs; pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; \<not> (c = hd vs \<and> d = ram1)\<rbrakk> \<Longrightarrow> (\<exists>as bs. rev vs @ [ram1, ram2] = as @ c # d # bs) \<or> c = ram2 \<and> d = last vs
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c = ram1 \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs; pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = hd vs \<longrightarrow> d \<noteq> ram1\<rbrakk> \<Longrightarrow> (\<exists>as bs. rev vs @ [ram1, ram2] = as @ c # d # bs) \<or> c = ram2 \<and> d = last vs
[PROOF STEP]
apply (case_tac "c = ram1 \<and> d = ram2")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>c = ram1 \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs; pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = hd vs \<longrightarrow> d \<noteq> ram1; c = ram1 \<and> d = ram2\<rbrakk> \<Longrightarrow> (\<exists>as bs. rev vs @ [ram1, ram2] = as @ c # d # bs) \<or> c = ram2 \<and> d = last vs
 2. \<lbrakk>c = ram1 \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs; pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = hd vs \<longrightarrow> d \<noteq> ram1; \<not> (c = ram1 \<and> d = ram2)\<rbrakk> \<Longrightarrow> (\<exists>as bs. rev vs @ [ram1, ram2] = as @ c # d # bs) \<or> c = ram2 \<and> d = last vs
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c = ram1 \<and> d = ram2 \<or> c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs; pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = hd vs \<longrightarrow> d \<noteq> ram1; \<not> (c = ram1 \<and> d = ram2)\<rbrakk> \<Longrightarrow> (\<exists>as bs. rev vs @ [ram1, ram2] = as @ c # d # bs) \<or> c = ram2 \<and> d = last vs
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs; pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = hd vs \<longrightarrow> d \<noteq> ram1; c = ram1 \<longrightarrow> d \<noteq> ram2\<rbrakk> \<Longrightarrow> (\<exists>as bs. rev vs @ [ram1, ram2] = as @ c # d # bs) \<or> c = ram2 \<and> d = last vs
[PROOF STEP]
apply (case_tac "c = ram2 \<and> d = last vs")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs; pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = hd vs \<longrightarrow> d \<noteq> ram1; c = ram1 \<longrightarrow> d \<noteq> ram2; c = ram2 \<and> d = last vs\<rbrakk> \<Longrightarrow> (\<exists>as bs. rev vs @ [ram1, ram2] = as @ c # d # bs) \<or> c = ram2 \<and> d = last vs
 2. \<lbrakk>c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs; pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = hd vs \<longrightarrow> d \<noteq> ram1; c = ram1 \<longrightarrow> d \<noteq> ram2; \<not> (c = ram2 \<and> d = last vs)\<rbrakk> \<Longrightarrow> (\<exists>as bs. rev vs @ [ram1, ram2] = as @ c # d # bs) \<or> c = ram2 \<and> d = last vs
[PROOF STEP]
apply (case_tac "vs" rule:rev_exhaust)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs; pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = hd vs \<longrightarrow> d \<noteq> ram1; c = ram1 \<longrightarrow> d \<noteq> ram2; c = ram2 \<and> d = last vs; vs = []\<rbrakk> \<Longrightarrow> (\<exists>as bs. rev vs @ [ram1, ram2] = as @ c # d # bs) \<or> c = ram2 \<and> d = last vs
 2. \<And>ys y. \<lbrakk>c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs; pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = hd vs \<longrightarrow> d \<noteq> ram1; c = ram1 \<longrightarrow> d \<noteq> ram2; c = ram2 \<and> d = last vs; vs = ys @ [y]\<rbrakk> \<Longrightarrow> (\<exists>as bs. rev vs @ [ram1, ram2] = as @ c # d # bs) \<or> c = ram2 \<and> d = last vs
 3. \<lbrakk>c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs; pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = hd vs \<longrightarrow> d \<noteq> ram1; c = ram1 \<longrightarrow> d \<noteq> ram2; \<not> (c = ram2 \<and> d = last vs)\<rbrakk> \<Longrightarrow> (\<exists>as bs. rev vs @ [ram1, ram2] = as @ c # d # bs) \<or> c = ram2 \<and> d = last vs
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>ys y. \<lbrakk>c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs; pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = hd vs \<longrightarrow> d \<noteq> ram1; c = ram1 \<longrightarrow> d \<noteq> ram2; c = ram2 \<and> d = last vs; vs = ys @ [y]\<rbrakk> \<Longrightarrow> (\<exists>as bs. rev vs @ [ram1, ram2] = as @ c # d # bs) \<or> c = ram2 \<and> d = last vs
 2. \<lbrakk>c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs; pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = hd vs \<longrightarrow> d \<noteq> ram1; c = ram1 \<longrightarrow> d \<noteq> ram2; \<not> (c = ram2 \<and> d = last vs)\<rbrakk> \<Longrightarrow> (\<exists>as bs. rev vs @ [ram1, ram2] = as @ c # d # bs) \<or> c = ram2 \<and> d = last vs
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>c = ram2 \<and> d = last vs \<or> (d, c) \<in> Edges vs; pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = hd vs \<longrightarrow> d \<noteq> ram1; c = ram1 \<longrightarrow> d \<noteq> ram2; \<not> (c = ram2 \<and> d = last vs)\<rbrakk> \<Longrightarrow> (\<exists>as bs. rev vs @ [ram1, ram2] = as @ c # d # bs) \<or> c = ram2 \<and> d = last vs
[PROOF STEP]
apply (simp add: Edges_def is_sublist_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>as bs. vs = as @ d # c # bs; pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = hd vs \<longrightarrow> d \<noteq> ram1; c = ram1 \<longrightarrow> d \<noteq> ram2; c = ram2 \<longrightarrow> d \<noteq> last vs\<rbrakk> \<Longrightarrow> (\<exists>as bs. rev vs @ [ram1, ram2] = as @ c # d # bs) \<or> c = ram2 \<and> d = last vs
[PROOF STEP]
apply (elim exE)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 vs; f12 = Face (rev vs @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # vs) Nonfinal; vs \<noteq> []; between (vertices f) ram1 ram2 = []; c = hd vs \<longrightarrow> d \<noteq> ram1; c = ram1 \<longrightarrow> d \<noteq> ram2; c = ram2 \<longrightarrow> d \<noteq> last vs; vs = as @ d # c # bs\<rbrakk> \<Longrightarrow> (\<exists>as bs. rev vs @ [ram1, ram2] = as @ c # d # bs) \<or> c = ram2 \<and> d = last vs
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 (as @ d # c # bs); f12 = Face (rev bs @ c # d # rev as @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # as @ d # c # bs) Nonfinal; between (vertices f) ram1 ram2 = []; c = hd (as @ d # c # bs) \<longrightarrow> d \<noteq> ram1; c = ram1 \<longrightarrow> d \<noteq> ram2; c = ram2 \<longrightarrow> d \<noteq> (if bs = [] then ram2 else last bs); vs = as @ d # c # bs\<rbrakk> \<Longrightarrow> (bs = [] \<longrightarrow> (\<exists>asa bs. c # d # rev as @ [ram1, ram2] = asa @ c # d # bs) \<or> c = ram2 \<and> d = c) \<and> (bs \<noteq> [] \<longrightarrow> (\<exists>asa bsa. rev bs @ c # d # rev as @ [ram1, ram2] = asa @ c # d # bsa) \<or> c = ram2 \<and> d = last bs)
[PROOF STEP]
apply (rule conjI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 (as @ d # c # bs); f12 = Face (rev bs @ c # d # rev as @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # as @ d # c # bs) Nonfinal; between (vertices f) ram1 ram2 = []; c = hd (as @ d # c # bs) \<longrightarrow> d \<noteq> ram1; c = ram1 \<longrightarrow> d \<noteq> ram2; c = ram2 \<longrightarrow> d \<noteq> (if bs = [] then ram2 else last bs); vs = as @ d # c # bs\<rbrakk> \<Longrightarrow> bs = [] \<longrightarrow> (\<exists>asa bs. c # d # rev as @ [ram1, ram2] = asa @ c # d # bs) \<or> c = ram2 \<and> d = c
 2. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 (as @ d # c # bs); f12 = Face (rev bs @ c # d # rev as @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # as @ d # c # bs) Nonfinal; between (vertices f) ram1 ram2 = []; c = hd (as @ d # c # bs) \<longrightarrow> d \<noteq> ram1; c = ram1 \<longrightarrow> d \<noteq> ram2; c = ram2 \<longrightarrow> d \<noteq> (if bs = [] then ram2 else last bs); vs = as @ d # c # bs\<rbrakk> \<Longrightarrow> bs \<noteq> [] \<longrightarrow> (\<exists>asa bsa. rev bs @ c # d # rev as @ [ram1, ram2] = asa @ c # d # bsa) \<or> c = ram2 \<and> d = last bs
[PROOF STEP]
apply (rule impI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 (as @ d # c # bs); f12 = Face (rev bs @ c # d # rev as @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # as @ d # c # bs) Nonfinal; between (vertices f) ram1 ram2 = []; c = hd (as @ d # c # bs) \<longrightarrow> d \<noteq> ram1; c = ram1 \<longrightarrow> d \<noteq> ram2; c = ram2 \<longrightarrow> d \<noteq> (if bs = [] then ram2 else last bs); vs = as @ d # c # bs; bs = []\<rbrakk> \<Longrightarrow> (\<exists>asa bs. c # d # rev as @ [ram1, ram2] = asa @ c # d # bs) \<or> c = ram2 \<and> d = c
 2. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 (as @ d # c # bs); f12 = Face (rev bs @ c # d # rev as @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # as @ d # c # bs) Nonfinal; between (vertices f) ram1 ram2 = []; c = hd (as @ d # c # bs) \<longrightarrow> d \<noteq> ram1; c = ram1 \<longrightarrow> d \<noteq> ram2; c = ram2 \<longrightarrow> d \<noteq> (if bs = [] then ram2 else last bs); vs = as @ d # c # bs\<rbrakk> \<Longrightarrow> bs \<noteq> [] \<longrightarrow> (\<exists>asa bsa. rev bs @ c # d # rev as @ [ram1, ram2] = asa @ c # d # bsa) \<or> c = ram2 \<and> d = last bs
[PROOF STEP]
apply (rule disjI1)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 (as @ d # c # bs); f12 = Face (rev bs @ c # d # rev as @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # as @ d # c # bs) Nonfinal; between (vertices f) ram1 ram2 = []; c = hd (as @ d # c # bs) \<longrightarrow> d \<noteq> ram1; c = ram1 \<longrightarrow> d \<noteq> ram2; c = ram2 \<longrightarrow> d \<noteq> (if bs = [] then ram2 else last bs); vs = as @ d # c # bs; bs = []\<rbrakk> \<Longrightarrow> \<exists>asa bs. c # d # rev as @ [ram1, ram2] = asa @ c # d # bs
 2. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 (as @ d # c # bs); f12 = Face (rev bs @ c # d # rev as @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # as @ d # c # bs) Nonfinal; between (vertices f) ram1 ram2 = []; c = hd (as @ d # c # bs) \<longrightarrow> d \<noteq> ram1; c = ram1 \<longrightarrow> d \<noteq> ram2; c = ram2 \<longrightarrow> d \<noteq> (if bs = [] then ram2 else last bs); vs = as @ d # c # bs\<rbrakk> \<Longrightarrow> bs \<noteq> [] \<longrightarrow> (\<exists>asa bsa. rev bs @ c # d # rev as @ [ram1, ram2] = asa @ c # d # bsa) \<or> c = ram2 \<and> d = last bs
[PROOF STEP]
apply (intro exI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 (as @ d # c # bs); f12 = Face (rev bs @ c # d # rev as @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # as @ d # c # bs) Nonfinal; between (vertices f) ram1 ram2 = []; c = hd (as @ d # c # bs) \<longrightarrow> d \<noteq> ram1; c = ram1 \<longrightarrow> d \<noteq> ram2; c = ram2 \<longrightarrow> d \<noteq> (if bs = [] then ram2 else last bs); vs = as @ d # c # bs; bs = []\<rbrakk> \<Longrightarrow> c # d # rev as @ [ram1, ram2] = ?as62 as bs @ c # d # ?bs63 as bs
 2. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 (as @ d # c # bs); f12 = Face (rev bs @ c # d # rev as @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # as @ d # c # bs) Nonfinal; between (vertices f) ram1 ram2 = []; c = hd (as @ d # c # bs) \<longrightarrow> d \<noteq> ram1; c = ram1 \<longrightarrow> d \<noteq> ram2; c = ram2 \<longrightarrow> d \<noteq> (if bs = [] then ram2 else last bs); vs = as @ d # c # bs\<rbrakk> \<Longrightarrow> bs \<noteq> [] \<longrightarrow> (\<exists>asa bsa. rev bs @ c # d # rev as @ [ram1, ram2] = asa @ c # d # bsa) \<or> c = ram2 \<and> d = last bs
[PROOF STEP]
apply (subgoal_tac "c # d # rev as @ [ram1, ram2] = [] @ c # d # rev as @ [ram1,ram2]")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 (as @ d # c # bs); f12 = Face (rev bs @ c # d # rev as @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # as @ d # c # bs) Nonfinal; between (vertices f) ram1 ram2 = []; c = hd (as @ d # c # bs) \<longrightarrow> d \<noteq> ram1; c = ram1 \<longrightarrow> d \<noteq> ram2; c = ram2 \<longrightarrow> d \<noteq> (if bs = [] then ram2 else last bs); vs = as @ d # c # bs; bs = []; c # d # rev as @ [ram1, ram2] = [] @ c # d # rev as @ [ram1, ram2]\<rbrakk> \<Longrightarrow> c # d # rev as @ [ram1, ram2] = ?as62 as bs @ c # d # ?bs63 as bs
 2. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 (as @ d # c # bs); f12 = Face (rev bs @ c # d # rev as @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # as @ d # c # bs) Nonfinal; between (vertices f) ram1 ram2 = []; c = hd (as @ d # c # bs) \<longrightarrow> d \<noteq> ram1; c = ram1 \<longrightarrow> d \<noteq> ram2; c = ram2 \<longrightarrow> d \<noteq> (if bs = [] then ram2 else last bs); vs = as @ d # c # bs; bs = []\<rbrakk> \<Longrightarrow> c # d # rev as @ [ram1, ram2] = [] @ c # d # rev as @ [ram1, ram2]
 3. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 (as @ d # c # bs); f12 = Face (rev bs @ c # d # rev as @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # as @ d # c # bs) Nonfinal; between (vertices f) ram1 ram2 = []; c = hd (as @ d # c # bs) \<longrightarrow> d \<noteq> ram1; c = ram1 \<longrightarrow> d \<noteq> ram2; c = ram2 \<longrightarrow> d \<noteq> (if bs = [] then ram2 else last bs); vs = as @ d # c # bs\<rbrakk> \<Longrightarrow> bs \<noteq> [] \<longrightarrow> (\<exists>asa bsa. rev bs @ c # d # rev as @ [ram1, ram2] = asa @ c # d # bsa) \<or> c = ram2 \<and> d = last bs
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 (as @ d # c # bs); f12 = Face (rev bs @ c # d # rev as @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # as @ d # c # bs) Nonfinal; between (vertices f) ram1 ram2 = []; c = hd (as @ d # c # bs) \<longrightarrow> d \<noteq> ram1; c = ram1 \<longrightarrow> d \<noteq> ram2; c = ram2 \<longrightarrow> d \<noteq> (if bs = [] then ram2 else last bs); vs = as @ d # c # bs; bs = []\<rbrakk> \<Longrightarrow> c # d # rev as @ [ram1, ram2] = [] @ c # d # rev as @ [ram1, ram2]
 2. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 (as @ d # c # bs); f12 = Face (rev bs @ c # d # rev as @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # as @ d # c # bs) Nonfinal; between (vertices f) ram1 ram2 = []; c = hd (as @ d # c # bs) \<longrightarrow> d \<noteq> ram1; c = ram1 \<longrightarrow> d \<noteq> ram2; c = ram2 \<longrightarrow> d \<noteq> (if bs = [] then ram2 else last bs); vs = as @ d # c # bs\<rbrakk> \<Longrightarrow> bs \<noteq> [] \<longrightarrow> (\<exists>asa bsa. rev bs @ c # d # rev as @ [ram1, ram2] = asa @ c # d # bsa) \<or> c = ram2 \<and> d = last bs
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 (as @ d # c # bs); f12 = Face (rev bs @ c # d # rev as @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # as @ d # c # bs) Nonfinal; between (vertices f) ram1 ram2 = []; c = hd (as @ d # c # bs) \<longrightarrow> d \<noteq> ram1; c = ram1 \<longrightarrow> d \<noteq> ram2; c = ram2 \<longrightarrow> d \<noteq> (if bs = [] then ram2 else last bs); vs = as @ d # c # bs\<rbrakk> \<Longrightarrow> bs \<noteq> [] \<longrightarrow> (\<exists>asa bsa. rev bs @ c # d # rev as @ [ram1, ram2] = asa @ c # d # bsa) \<or> c = ram2 \<and> d = last bs
[PROOF STEP]
apply (rule impI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 (as @ d # c # bs); f12 = Face (rev bs @ c # d # rev as @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # as @ d # c # bs) Nonfinal; between (vertices f) ram1 ram2 = []; c = hd (as @ d # c # bs) \<longrightarrow> d \<noteq> ram1; c = ram1 \<longrightarrow> d \<noteq> ram2; c = ram2 \<longrightarrow> d \<noteq> (if bs = [] then ram2 else last bs); vs = as @ d # c # bs; bs \<noteq> []\<rbrakk> \<Longrightarrow> (\<exists>asa bsa. rev bs @ c # d # rev as @ [ram1, ram2] = asa @ c # d # bsa) \<or> c = ram2 \<and> d = last bs
[PROOF STEP]
apply (rule disjI1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 (as @ d # c # bs); f12 = Face (rev bs @ c # d # rev as @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # as @ d # c # bs) Nonfinal; between (vertices f) ram1 ram2 = []; c = hd (as @ d # c # bs) \<longrightarrow> d \<noteq> ram1; c = ram1 \<longrightarrow> d \<noteq> ram2; c = ram2 \<longrightarrow> d \<noteq> (if bs = [] then ram2 else last bs); vs = as @ d # c # bs; bs \<noteq> []\<rbrakk> \<Longrightarrow> \<exists>asa bsa. rev bs @ c # d # rev as @ [ram1, ram2] = asa @ c # d # bsa
[PROOF STEP]
apply (intro exI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>as bs. \<lbrakk>pre_split_face f ram1 ram2 (as @ d # c # bs); f12 = Face (rev bs @ c # d # rev as @ [ram1, ram2]) Nonfinal \<and> f21 = Face (ram2 # between (vertices f) ram2 ram1 @ ram1 # as @ d # c # bs) Nonfinal; between (vertices f) ram1 ram2 = []; c = hd (as @ d # c # bs) \<longrightarrow> d \<noteq> ram1; c = ram1 \<longrightarrow> d \<noteq> ram2; c = ram2 \<longrightarrow> d \<noteq> (if bs = [] then ram2 else last bs); vs = as @ d # c # bs; bs \<noteq> []\<rbrakk> \<Longrightarrow> rev bs @ c # d # rev as @ [ram1, ram2] = ?as69 as bs @ c # d # ?bs70 as bs
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
x \<in> \<E> f12

goal:
No subgoals!
[PROOF STEP]
qed