[STATEMENT]
lemma Exit_path_Low_path:
  assumes "n -as\<rightarrow>* (_Exit_)" and "inner_node n"
  obtains a' as' where "as = as'@[a']" and "n -as'\<rightarrow>* (_Low_)"
  and "kind a' = (\<lambda>s. True)\<^sub>\<surd>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>as' a'. \<lbrakk>as = as' @ [a']; n -as'\<rightarrow>* (_Low_); kind a' = (\<lambda>s. True)\<^sub>\<surd>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
proof(atomize_elim)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<exists>as' a'. as = as' @ [a'] \<and> n -as'\<rightarrow>* (_Low_) \<and> kind a' = (\<lambda>s. True)\<^sub>\<surd>
[PROOF STEP]
from \<open>n -as\<rightarrow>* (_Exit_)\<close>
[PROOF STATE]
proof (chain)
picking this:
n -as\<rightarrow>* (_Exit_)
[PROOF STEP]
show "\<exists>as' a'. as = as'@[a'] \<and> n -as'\<rightarrow>* (_Low_) \<and> kind a' = (\<lambda>s. True)\<^sub>\<surd>"
[PROOF STATE]
proof (prove)
using this:
n -as\<rightarrow>* (_Exit_)

goal (1 subgoal):
 1. \<exists>as' a'. as = as' @ [a'] \<and> n -as'\<rightarrow>* (_Low_) \<and> kind a' = (\<lambda>s. True)\<^sub>\<surd>
[PROOF STEP]
proof(induct as rule:rev_induct)
[PROOF STATE]
proof (state)
goal (2 subgoals):
 1. n -[]\<rightarrow>* (_Exit_) \<Longrightarrow> \<exists>as' a'. [] = as' @ [a'] \<and> n -as'\<rightarrow>* (_Low_) \<and> kind a' = (\<lambda>s. True)\<^sub>\<surd>
 2. \<And>x xs. \<lbrakk>n -xs\<rightarrow>* (_Exit_) \<Longrightarrow> \<exists>as' a'. xs = as' @ [a'] \<and> n -as'\<rightarrow>* (_Low_) \<and> kind a' = (\<lambda>s. True)\<^sub>\<surd>; n -xs @ [x]\<rightarrow>* (_Exit_)\<rbrakk> \<Longrightarrow> \<exists>as' a'. xs @ [x] = as' @ [a'] \<and> n -as'\<rightarrow>* (_Low_) \<and> kind a' = (\<lambda>s. True)\<^sub>\<surd>
[PROOF STEP]
case Nil
[PROOF STATE]
proof (state)
this:
n -[]\<rightarrow>* (_Exit_)

goal (2 subgoals):
 1. n -[]\<rightarrow>* (_Exit_) \<Longrightarrow> \<exists>as' a'. [] = as' @ [a'] \<and> n -as'\<rightarrow>* (_Low_) \<and> kind a' = (\<lambda>s. True)\<^sub>\<surd>
 2. \<And>x xs. \<lbrakk>n -xs\<rightarrow>* (_Exit_) \<Longrightarrow> \<exists>as' a'. xs = as' @ [a'] \<and> n -as'\<rightarrow>* (_Low_) \<and> kind a' = (\<lambda>s. True)\<^sub>\<surd>; n -xs @ [x]\<rightarrow>* (_Exit_)\<rbrakk> \<Longrightarrow> \<exists>as' a'. xs @ [x] = as' @ [a'] \<and> n -as'\<rightarrow>* (_Low_) \<and> kind a' = (\<lambda>s. True)\<^sub>\<surd>
[PROOF STEP]
with \<open>inner_node n\<close>
[PROOF STATE]
proof (chain)
picking this:
inner_node n
n -[]\<rightarrow>* (_Exit_)
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
inner_node n
n -[]\<rightarrow>* (_Exit_)

goal (1 subgoal):
 1. \<exists>as' a'. [] = as' @ [a'] \<and> n -as'\<rightarrow>* (_Low_) \<and> kind a' = (\<lambda>s. True)\<^sub>\<surd>
[PROOF STEP]
by fastforce
[PROOF STATE]
proof (state)
this:
\<exists>as' a'. [] = as' @ [a'] \<and> n -as'\<rightarrow>* (_Low_) \<and> kind a' = (\<lambda>s. True)\<^sub>\<surd>

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>n -xs\<rightarrow>* (_Exit_) \<Longrightarrow> \<exists>as' a'. xs = as' @ [a'] \<and> n -as'\<rightarrow>* (_Low_) \<and> kind a' = (\<lambda>s. True)\<^sub>\<surd>; n -xs @ [x]\<rightarrow>* (_Exit_)\<rbrakk> \<Longrightarrow> \<exists>as' a'. xs @ [x] = as' @ [a'] \<and> n -as'\<rightarrow>* (_Low_) \<and> kind a' = (\<lambda>s. True)\<^sub>\<surd>
[PROOF STEP]
next
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>n -xs\<rightarrow>* (_Exit_) \<Longrightarrow> \<exists>as' a'. xs = as' @ [a'] \<and> n -as'\<rightarrow>* (_Low_) \<and> kind a' = (\<lambda>s. True)\<^sub>\<surd>; n -xs @ [x]\<rightarrow>* (_Exit_)\<rbrakk> \<Longrightarrow> \<exists>as' a'. xs @ [x] = as' @ [a'] \<and> n -as'\<rightarrow>* (_Low_) \<and> kind a' = (\<lambda>s. True)\<^sub>\<surd>
[PROOF STEP]
case (snoc a' as')
[PROOF STATE]
proof (state)
this:
n -as'\<rightarrow>* (_Exit_) \<Longrightarrow> \<exists>as'a a'. as' = as'a @ [a'] \<and> n -as'a\<rightarrow>* (_Low_) \<and> kind a' = (\<lambda>s. True)\<^sub>\<surd>
n -as' @ [a']\<rightarrow>* (_Exit_)

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>n -xs\<rightarrow>* (_Exit_) \<Longrightarrow> \<exists>as' a'. xs = as' @ [a'] \<and> n -as'\<rightarrow>* (_Low_) \<and> kind a' = (\<lambda>s. True)\<^sub>\<surd>; n -xs @ [x]\<rightarrow>* (_Exit_)\<rbrakk> \<Longrightarrow> \<exists>as' a'. xs @ [x] = as' @ [a'] \<and> n -as'\<rightarrow>* (_Low_) \<and> kind a' = (\<lambda>s. True)\<^sub>\<surd>
[PROOF STEP]
from \<open>n -as'@[a']\<rightarrow>* (_Exit_)\<close>
[PROOF STATE]
proof (chain)
picking this:
n -as' @ [a']\<rightarrow>* (_Exit_)
[PROOF STEP]
have "n -as'\<rightarrow>* sourcenode a'" and "valid_edge a'" and "targetnode a' = (_Exit_)"
[PROOF STATE]
proof (prove)
using this:
n -as' @ [a']\<rightarrow>* (_Exit_)

goal (1 subgoal):
 1. n -as'\<rightarrow>* sourcenode a' &&& valid_edge a' &&& targetnode a' = (_Exit_)
[PROOF STEP]
by(auto elim:path_split_snoc)
[PROOF STATE]
proof (state)
this:
n -as'\<rightarrow>* sourcenode a'
valid_edge a'
targetnode a' = (_Exit_)

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>n -xs\<rightarrow>* (_Exit_) \<Longrightarrow> \<exists>as' a'. xs = as' @ [a'] \<and> n -as'\<rightarrow>* (_Low_) \<and> kind a' = (\<lambda>s. True)\<^sub>\<surd>; n -xs @ [x]\<rightarrow>* (_Exit_)\<rbrakk> \<Longrightarrow> \<exists>as' a'. xs @ [x] = as' @ [a'] \<and> n -as'\<rightarrow>* (_Low_) \<and> kind a' = (\<lambda>s. True)\<^sub>\<surd>
[PROOF STEP]
{
[PROOF STATE]
proof (state)
this:
n -as'\<rightarrow>* sourcenode a'
valid_edge a'
targetnode a' = (_Exit_)

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>n -xs\<rightarrow>* (_Exit_) \<Longrightarrow> \<exists>as' a'. xs = as' @ [a'] \<and> n -as'\<rightarrow>* (_Low_) \<and> kind a' = (\<lambda>s. True)\<^sub>\<surd>; n -xs @ [x]\<rightarrow>* (_Exit_)\<rbrakk> \<Longrightarrow> \<exists>as' a'. xs @ [x] = as' @ [a'] \<and> n -as'\<rightarrow>* (_Low_) \<and> kind a' = (\<lambda>s. True)\<^sub>\<surd>
[PROOF STEP]
assume "sourcenode a' = (_Entry_)"
[PROOF STATE]
proof (state)
this:
sourcenode a' = (_Entry_)

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>n -xs\<rightarrow>* (_Exit_) \<Longrightarrow> \<exists>as' a'. xs = as' @ [a'] \<and> n -as'\<rightarrow>* (_Low_) \<and> kind a' = (\<lambda>s. True)\<^sub>\<surd>; n -xs @ [x]\<rightarrow>* (_Exit_)\<rbrakk> \<Longrightarrow> \<exists>as' a'. xs @ [x] = as' @ [a'] \<and> n -as'\<rightarrow>* (_Low_) \<and> kind a' = (\<lambda>s. True)\<^sub>\<surd>
[PROOF STEP]
with \<open>n -as'\<rightarrow>* sourcenode a'\<close>
[PROOF STATE]
proof (chain)
picking this:
n -as'\<rightarrow>* sourcenode a'
sourcenode a' = (_Entry_)
[PROOF STEP]
have "n = (_Entry_)"
[PROOF STATE]
proof (prove)
using this:
n -as'\<rightarrow>* sourcenode a'
sourcenode a' = (_Entry_)

goal (1 subgoal):
 1. n = (_Entry_)
[PROOF STEP]
by(blast intro!:path_Entry_target)
[PROOF STATE]
proof (state)
this:
n = (_Entry_)

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>n -xs\<rightarrow>* (_Exit_) \<Longrightarrow> \<exists>as' a'. xs = as' @ [a'] \<and> n -as'\<rightarrow>* (_Low_) \<and> kind a' = (\<lambda>s. True)\<^sub>\<surd>; n -xs @ [x]\<rightarrow>* (_Exit_)\<rbrakk> \<Longrightarrow> \<exists>as' a'. xs @ [x] = as' @ [a'] \<and> n -as'\<rightarrow>* (_Low_) \<and> kind a' = (\<lambda>s. True)\<^sub>\<surd>
[PROOF STEP]
with \<open>inner_node n\<close>
[PROOF STATE]
proof (chain)
picking this:
inner_node n
n = (_Entry_)
[PROOF STEP]
have False
[PROOF STATE]
proof (prove)
using this:
inner_node n
n = (_Entry_)

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

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>n -xs\<rightarrow>* (_Exit_) \<Longrightarrow> \<exists>as' a'. xs = as' @ [a'] \<and> n -as'\<rightarrow>* (_Low_) \<and> kind a' = (\<lambda>s. True)\<^sub>\<surd>; n -xs @ [x]\<rightarrow>* (_Exit_)\<rbrakk> \<Longrightarrow> \<exists>as' a'. xs @ [x] = as' @ [a'] \<and> n -as'\<rightarrow>* (_Low_) \<and> kind a' = (\<lambda>s. True)\<^sub>\<surd>
[PROOF STEP]
}
[PROOF STATE]
proof (state)
this:
sourcenode a' = (_Entry_) \<Longrightarrow> False

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>n -xs\<rightarrow>* (_Exit_) \<Longrightarrow> \<exists>as' a'. xs = as' @ [a'] \<and> n -as'\<rightarrow>* (_Low_) \<and> kind a' = (\<lambda>s. True)\<^sub>\<surd>; n -xs @ [x]\<rightarrow>* (_Exit_)\<rbrakk> \<Longrightarrow> \<exists>as' a'. xs @ [x] = as' @ [a'] \<and> n -as'\<rightarrow>* (_Low_) \<and> kind a' = (\<lambda>s. True)\<^sub>\<surd>
[PROOF STEP]
with \<open>valid_edge a'\<close> \<open>targetnode a' = (_Exit_)\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a'
targetnode a' = (_Exit_)
sourcenode a' = (_Entry_) \<Longrightarrow> False
[PROOF STEP]
have "sourcenode a' = (_Low_)"
[PROOF STATE]
proof (prove)
using this:
valid_edge a'
targetnode a' = (_Exit_)
sourcenode a' = (_Entry_) \<Longrightarrow> False

goal (1 subgoal):
 1. sourcenode a' = (_Low_)
[PROOF STEP]
by(blast dest!:Exit_edge_Entry_or_Low)
[PROOF STATE]
proof (state)
this:
sourcenode a' = (_Low_)

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>n -xs\<rightarrow>* (_Exit_) \<Longrightarrow> \<exists>as' a'. xs = as' @ [a'] \<and> n -as'\<rightarrow>* (_Low_) \<and> kind a' = (\<lambda>s. True)\<^sub>\<surd>; n -xs @ [x]\<rightarrow>* (_Exit_)\<rbrakk> \<Longrightarrow> \<exists>as' a'. xs @ [x] = as' @ [a'] \<and> n -as'\<rightarrow>* (_Low_) \<and> kind a' = (\<lambda>s. True)\<^sub>\<surd>
[PROOF STEP]
from Low_source_Exit_edge
[PROOF STATE]
proof (chain)
picking this:
\<exists>a. valid_edge a \<and> sourcenode a = (_Low_) \<and> targetnode a = (_Exit_) \<and> kind a = (\<lambda>s. True)\<^sub>\<surd>
[PROOF STEP]
obtain ax where "valid_edge ax" and "sourcenode ax = (_Low_)"
      and "targetnode ax = (_Exit_)" and "kind ax = (\<lambda>s. True)\<^sub>\<surd>"
[PROOF STATE]
proof (prove)
using this:
\<exists>a. valid_edge a \<and> sourcenode a = (_Low_) \<and> targetnode a = (_Exit_) \<and> kind a = (\<lambda>s. True)\<^sub>\<surd>

goal (1 subgoal):
 1. (\<And>ax. \<lbrakk>valid_edge ax; sourcenode ax = (_Low_); targetnode ax = (_Exit_); kind ax = (\<lambda>s. True)\<^sub>\<surd>\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
valid_edge ax
sourcenode ax = (_Low_)
targetnode ax = (_Exit_)
kind ax = (\<lambda>s. True)\<^sub>\<surd>

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>n -xs\<rightarrow>* (_Exit_) \<Longrightarrow> \<exists>as' a'. xs = as' @ [a'] \<and> n -as'\<rightarrow>* (_Low_) \<and> kind a' = (\<lambda>s. True)\<^sub>\<surd>; n -xs @ [x]\<rightarrow>* (_Exit_)\<rbrakk> \<Longrightarrow> \<exists>as' a'. xs @ [x] = as' @ [a'] \<and> n -as'\<rightarrow>* (_Low_) \<and> kind a' = (\<lambda>s. True)\<^sub>\<surd>
[PROOF STEP]
with \<open>valid_edge a'\<close> \<open>targetnode a' = (_Exit_)\<close> \<open>sourcenode a' = (_Low_)\<close>
[PROOF STATE]
proof (chain)
picking this:
valid_edge a'
targetnode a' = (_Exit_)
sourcenode a' = (_Low_)
valid_edge ax
sourcenode ax = (_Low_)
targetnode ax = (_Exit_)
kind ax = (\<lambda>s. True)\<^sub>\<surd>
[PROOF STEP]
have "a' = ax"
[PROOF STATE]
proof (prove)
using this:
valid_edge a'
targetnode a' = (_Exit_)
sourcenode a' = (_Low_)
valid_edge ax
sourcenode ax = (_Low_)
targetnode ax = (_Exit_)
kind ax = (\<lambda>s. True)\<^sub>\<surd>

goal (1 subgoal):
 1. a' = ax
[PROOF STEP]
by(fastforce intro:edge_det)
[PROOF STATE]
proof (state)
this:
a' = ax

goal (1 subgoal):
 1. \<And>x xs. \<lbrakk>n -xs\<rightarrow>* (_Exit_) \<Longrightarrow> \<exists>as' a'. xs = as' @ [a'] \<and> n -as'\<rightarrow>* (_Low_) \<and> kind a' = (\<lambda>s. True)\<^sub>\<surd>; n -xs @ [x]\<rightarrow>* (_Exit_)\<rbrakk> \<Longrightarrow> \<exists>as' a'. xs @ [x] = as' @ [a'] \<and> n -as'\<rightarrow>* (_Low_) \<and> kind a' = (\<lambda>s. True)\<^sub>\<surd>
[PROOF STEP]
with \<open>n -as'\<rightarrow>* sourcenode a'\<close> \<open>sourcenode a' = (_Low_)\<close> \<open>kind ax = (\<lambda>s. True)\<^sub>\<surd>\<close>
[PROOF STATE]
proof (chain)
picking this:
n -as'\<rightarrow>* sourcenode a'
sourcenode a' = (_Low_)
kind ax = (\<lambda>s. True)\<^sub>\<surd>
a' = ax
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
using this:
n -as'\<rightarrow>* sourcenode a'
sourcenode a' = (_Low_)
kind ax = (\<lambda>s. True)\<^sub>\<surd>
a' = ax

goal (1 subgoal):
 1. \<exists>as'a a'a. as' @ [a'] = as'a @ [a'a] \<and> n -as'a\<rightarrow>* (_Low_) \<and> kind a'a = (\<lambda>s. True)\<^sub>\<surd>
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<exists>as'a a'a. as' @ [a'] = as'a @ [a'a] \<and> n -as'a\<rightarrow>* (_Low_) \<and> kind a'a = (\<lambda>s. True)\<^sub>\<surd>

goal:
No subgoals!
[PROOF STEP]
qed
[PROOF STATE]
proof (state)
this:
\<exists>as' a'. as = as' @ [a'] \<and> n -as'\<rightarrow>* (_Low_) \<and> kind a' = (\<lambda>s. True)\<^sub>\<surd>

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma mult_poly_p_mult_ideal:
  \<open>mult_poly_p q (p, r) (p', r') \<Longrightarrow>
     (polynomial_of_mset p' * polynomial_of_mset q + polynomial_of_mset r') - (polynomial_of_mset p * polynomial_of_mset q + polynomial_of_mset r)
       \<in> ideal polynomial_bool\<close>
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. mult_poly_p q (p, r) (p', r') \<Longrightarrow> polynomial_of_mset p' * polynomial_of_mset q + polynomial_of_mset r' - (polynomial_of_mset p * polynomial_of_mset q + polynomial_of_mset r) \<in> More_Modules.ideal polynomial_bool
[PROOF STEP]
proof (induction rule: mult_poly_p_induct)
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. \<And>xs n p r. polynomial_of_mset p * polynomial_of_mset q + polynomial_of_mset ({#(remdups_mset (xs + ys), n * m). (ys, m) \<in># q#} + r) - (polynomial_of_mset (add_mset (xs, n) p) * polynomial_of_mset q + polynomial_of_mset r) \<in> More_Modules.ideal polynomial_bool
[PROOF STEP]
case (mult_step xs n p r)
[PROOF STATE]
proof (state)
this:

goal (1 subgoal):
 1. \<And>xs n p r. polynomial_of_mset p * polynomial_of_mset q + polynomial_of_mset ({#(remdups_mset (xs + ys), n * m). (ys, m) \<in># q#} + r) - (polynomial_of_mset (add_mset (xs, n) p) * polynomial_of_mset q + polynomial_of_mset r) \<in> More_Modules.ideal polynomial_bool
[PROOF STEP]
show ?case
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. polynomial_of_mset p * polynomial_of_mset q + polynomial_of_mset ({#(remdups_mset (xs + ys), n * m). (ys, m) \<in># q#} + r) - (polynomial_of_mset (add_mset (xs, n) p) * polynomial_of_mset q + polynomial_of_mset r) \<in> More_Modules.ideal polynomial_bool
[PROOF STEP]
by (auto simp: algebra_simps polynomial_of_mset_mult_map)
[PROOF STATE]
proof (state)
this:
polynomial_of_mset p * polynomial_of_mset q + polynomial_of_mset ({#(remdups_mset (xs + ys), n * m). (ys, m) \<in># q#} + r) - (polynomial_of_mset (add_mset (xs, n) p) * polynomial_of_mset q + polynomial_of_mset r) \<in> More_Modules.ideal polynomial_bool

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma rem_cycles_removes_last: "j \<notin> set (rem_cycles i j xs)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. j \<notin> set (rem_cycles i j xs)
[PROOF STEP]
by (meson remove_all_rev_removes remove_all_subs rev_subsetD)


[STATEMENT]
lemma cycle_free_cycle_free_up_to:
  "cycle_free m n \<Longrightarrow> k \<le> n \<Longrightarrow> cycle_free_up_to m k n"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>cycle_free m n; k \<le> n\<rbrakk> \<Longrightarrow> cycle_free_up_to m k n
[PROOF STEP]
unfolding cycle_free_def cycle_free_up_to_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<forall>i xs. i \<le> n \<and> set xs \<subseteq> {0..n} \<longrightarrow> (\<forall>j\<le>n. len m i j (rem_cycles i j xs) \<le> len m i j xs) \<and> \<one> \<le> len m i i xs; k \<le> n\<rbrakk> \<Longrightarrow> \<forall>i xs. i \<le> n \<and> set xs \<subseteq> {0..k} \<longrightarrow> (\<forall>j\<le>n. len m i j (rem_cycles i j xs) \<le> len m i j xs) \<and> \<one> \<le> len m i i xs
[PROOF STEP]
by force


[STATEMENT]
lemma wf_interp_for_formula_FExists:
  "\<lbrakk>wf_formula (length I) (FExists \<phi>); w \<noteq> []\<rbrakk>\<Longrightarrow>
    wf_interp_for_formula (w, I) (FExists \<phi>) \<longleftrightarrow>
    (\<forall>p < length w. wf_interp_for_formula (w, Inl p # I) \<phi>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wf_formula (length I) (FExists \<phi>); w \<noteq> []\<rbrakk> \<Longrightarrow> wf_interp_for_formula (w, I) (FExists \<phi>) = (\<forall>p<length w. wf_interp_for_formula (w, Inl p # I) \<phi>)
[PROOF STEP]
by (auto simp: nth_Cons' split: if_split_asm)


[STATEMENT]
lemma wprepare_add_one2_Oc[simp]: "wprepare_add_one2 m lm (b, []) \<Longrightarrow> wprepare_add_one2 m lm (b, [Oc])"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wprepare_add_one2 m lm (b, []) \<Longrightarrow> wprepare_add_one2 m lm (b, [Oc])
[PROOF STEP]
apply(simp only: wprepare_invs, auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma wadjust_start_snd_nonempty[simp]: "wadjust_start m rs (c, []) = False"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. wadjust_start m rs (c, []) = False
[PROOF STEP]
apply(auto simp: wadjust_start.simps)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma wadjust_loop_on_left_moving_B_Bk_move[simp]:
  "\<lbrakk>wadjust_loop_on_left_moving_B m rs (c, Bk # list); hd c = Bk\<rbrakk>
    \<Longrightarrow>  wadjust_loop_on_left_moving_B m rs (tl c, Bk # Bk # list)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>wadjust_loop_on_left_moving_B m rs (c, Bk # list); hd c = Bk\<rbrakk> \<Longrightarrow> wadjust_loop_on_left_moving_B m rs (tl c, Bk # Bk # list)
[PROOF STEP]
apply(simp only: wadjust_loop_on_left_moving_B.simps)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>\<exists>ml mr nl nr rn. c = Bk \<up> nl @ Oc # Oc \<up> ml @ Bk # Oc \<up> Suc m \<and> Bk # list = Bk \<up> nr @ Bk # Bk # Oc \<up> mr @ Bk \<up> rn \<and> ml + mr = Suc rs \<and> 0 < mr; hd c = Bk\<rbrakk> \<Longrightarrow> \<exists>ml mr nl nr rn. tl c = Bk \<up> nl @ Oc # Oc \<up> ml @ Bk # Oc \<up> Suc m \<and> Bk # Bk # list = Bk \<up> nr @ Bk # Bk # Oc \<up> mr @ Bk \<up> rn \<and> ml + mr = Suc rs \<and> 0 < mr
[PROOF STEP]
apply(erule_tac exE)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>ml mr nl nr rn. \<lbrakk>hd c = Bk; c = Bk \<up> nl @ Oc # Oc \<up> ml @ Bk # Oc \<up> Suc m \<and> Bk # list = Bk \<up> nr @ Bk # Bk # Oc \<up> mr @ Bk \<up> rn \<and> ml + mr = Suc rs \<and> 0 < mr\<rbrakk> \<Longrightarrow> \<exists>ml mr nl nr rn. tl c = Bk \<up> nl @ Oc # Oc \<up> ml @ Bk # Oc \<up> Suc m \<and> Bk # Bk # list = Bk \<up> nr @ Bk # Bk # Oc \<up> mr @ Bk \<up> rn \<and> ml + mr = Suc rs \<and> 0 < mr
[PROOF STEP]
by (metis (no_types, lifting) cell.distinct(1) list.sel(1)
      replicate_Suc_iff_anywhere self_append_conv2 tl_append2 tl_replicate)


[STATEMENT]
lemma map_iarray_list_of: "map IArray (map IArray.list_of bss) = bss"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. map IArray (map IArray.list_of bss) = bss
[PROOF STEP]
using iarray_list_of
[PROOF STATE]
proof (prove)
using this:
IArray (IArray.list_of ?xs) = ?xs

goal (1 subgoal):
 1. map IArray (map IArray.list_of bss) = bss
[PROOF STEP]
by (induction bss) auto


[STATEMENT]
lemma ordinal_less_plusL_iff: "(y < x + y) = (y < x * \<omega>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (y < x + y) = (y < x * \<omega>)
[PROOF STEP]
apply safe
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. y < x + y \<Longrightarrow> y < x * \<omega>
 2. y < x * \<omega> \<Longrightarrow> y < x + y
[PROOF STEP]
apply (rule ccontr, simp add: linorder_not_less)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>y < x + y; x * \<omega> \<le> y\<rbrakk> \<Longrightarrow> False
 2. y < x * \<omega> \<Longrightarrow> y < x + y
[PROOF STEP]
apply (drule ordinal_plus_absorb, simp)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. y < x * \<omega> \<Longrightarrow> y < x + y
[PROOF STEP]
apply (erule ordinal_less_plusL)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma atUV_add_mset[simp]: "
  atUV U V (add_mset c c2) \<longleftrightarrow>
  (
    (atUV U V c2) \<or>
    (atU U {#c#} \<and> atU V c2) \<or>
    (atU V {#c#} \<and> atU U c2)
  )"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atUV U V (add_mset c c2) = (atUV U V c2 \<or> atU U {#c#} \<and> atU V c2 \<or> atU V {#c#} \<and> atU U c2)
[PROOF STEP]
unfolding add_mset_add_single[of c c2]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. atUV U V (c2 + {#c#}) = (atUV U V c2 \<or> atU U {#c#} \<and> atU V c2 \<or> atU V {#c#} \<and> atU U c2)
[PROOF STEP]
unfolding atUV_union
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (atUV U V c2 \<or> atUV U V {#c#} \<or> atU U c2 \<and> atU V {#c#} \<or> atU V c2 \<and> atU U {#c#}) = (atUV U V c2 \<or> atU U {#c#} \<and> atU V c2 \<or> atU V {#c#} \<and> atU U c2)
[PROOF STEP]
by auto


[STATEMENT]
lemma ord_of_nat_succ[nat_omega_simps]: "succ (a\<^sub>\<nat>) = (Suc a)\<^sub>\<nat>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ZFC_in_HOL.succ (a\<^sub>\<nat>) = Suc a\<^sub>\<nat>
[PROOF STEP]
by auto


[STATEMENT]
lemma bd_FGcontra_cinfinite: "cinfinite bd_FGcontra"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cinfinite bd_FGcontra
[PROOF STEP]
unfolding bd_FGcontra_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. cinfinite bd_F
[PROOF STEP]
using bd_F_cinfinite
[PROOF STATE]
proof (prove)
using this:
cinfinite bd_F

goal (1 subgoal):
 1. cinfinite bd_F
[PROOF STEP]
.


[STATEMENT]
lemma primerec_rec_disj_2[intro]: "primerec rec_disj (Suc (Suc 0))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. primerec rec_disj (Suc (Suc 0))
[PROOF STEP]
apply(simp add: rec_disj_def, auto)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. primerec rec_add ?k12
 2. Suc (Suc 0) = ?k12
 3. \<And>i. i < Suc (Suc 0) \<Longrightarrow> primerec ([recf.id (Suc (Suc 0)) 0, recf.id (Suc (Suc 0)) (Suc 0)] ! i) (Suc (Suc 0))
[PROOF STEP]
apply(auto dest!:less_2_cases[unfolded numeral_eqs_upto_12 One_nat_def])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma perm_rem_same:
  assumes "bij f" "f y = y" shows "perm_rem x f y = f y"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. perm_rem x f y = f y
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
bij f
f y = y

goal (1 subgoal):
 1. perm_rem x f y = f y
[PROOF STEP]
by (auto simp: perm_rem_def bij_iff transpose_def)


[STATEMENT]
lemma constraints_set_vars_geq_vec_def:
  "set (vars_from_index_geq_vec start b) =
   {GEQ (lp_monom 1 (i+start)) (b$i) |i. i \<in> {0..<dim_vec b}}"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. set (vars_from_index_geq_vec start b) = {GEQ (lp_monom 1 (i + start)) (b $ i) |i. i \<in> {0..<dim_vec b}}
[PROOF STEP]
using set_comprehension_list_comprehension[of
      "(\<lambda>i. GEQ (lp_monom 1 (i+start)) (b$i))" "dim_vec b"]
[PROOF STATE]
proof (prove)
using this:
set (map (\<lambda>i. GEQ (lp_monom 1 (i + start)) (b $ i)) [dim_vec b..<?a]) = {GEQ (lp_monom 1 (i + start)) (b $ i) |i. i \<in> {dim_vec b..<?a}}

goal (1 subgoal):
 1. set (vars_from_index_geq_vec start b) = {GEQ (lp_monom 1 (i + start)) (b $ i) |i. i \<in> {0..<dim_vec b}}
[PROOF STEP]
by auto


[STATEMENT]
lemma vars_from_index_geq_sat:
  assumes "\<langle>x\<rangle> \<Turnstile>\<^sub>c\<^sub>s set (vars_from_index_geq_vec start b)"
  assumes "i < dim_vec b"
  shows "\<langle>x\<rangle> (i+start) \<ge> b$i"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. b $ i \<le> \<langle>x\<rangle> (i + start)
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. b $ i \<le> \<langle>x\<rangle> (i + start)
[PROOF STEP]
have e_e:"GEQ (lp_monom 1 (i+start)) (b$i) \<in> set (vars_from_index_geq_vec start b)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. GEQ (lp_monom 1 (i + start)) (b $ i) \<in> set (vars_from_index_geq_vec start b)
[PROOF STEP]
using constraints_set_vars_geq_vec_def[of start b]
[PROOF STATE]
proof (prove)
using this:
set (vars_from_index_geq_vec start b) = {GEQ (lp_monom 1 (i + start)) (b $ i) |i. i \<in> {0..<dim_vec b}}

goal (1 subgoal):
 1. GEQ (lp_monom 1 (i + start)) (b $ i) \<in> set (vars_from_index_geq_vec start b)
[PROOF STEP]
using assms(2)
[PROOF STATE]
proof (prove)
using this:
set (vars_from_index_geq_vec start b) = {GEQ (lp_monom 1 (i + start)) (b $ i) |i. i \<in> {0..<dim_vec b}}
i < dim_vec b

goal (1 subgoal):
 1. GEQ (lp_monom 1 (i + start)) (b $ i) \<in> set (vars_from_index_geq_vec start b)
[PROOF STEP]
by auto
[PROOF STATE]
proof (state)
this:
GEQ (lp_monom 1 (i + start)) (b $ i) \<in> set (vars_from_index_geq_vec start b)

goal (1 subgoal):
 1. b $ i \<le> \<langle>x\<rangle> (i + start)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
GEQ (lp_monom 1 (i + start)) (b $ i) \<in> set (vars_from_index_geq_vec start b)
[PROOF STEP]
have "\<langle>x\<rangle> \<Turnstile>\<^sub>c GEQ (lp_monom 1 (i+start)) (b$i)"
[PROOF STATE]
proof (prove)
using this:
GEQ (lp_monom 1 (i + start)) (b $ i) \<in> set (vars_from_index_geq_vec start b)

goal (1 subgoal):
 1. \<langle>x\<rangle> \<Turnstile>\<^sub>c GEQ (lp_monom 1 (i + start)) (b $ i)
[PROOF STEP]
using assms(1)
[PROOF STATE]
proof (prove)
using this:
GEQ (lp_monom 1 (i + start)) (b $ i) \<in> set (vars_from_index_geq_vec start b)
\<langle>x\<rangle> \<Turnstile>\<^sub>c\<^sub>s set (vars_from_index_geq_vec start b)

goal (1 subgoal):
 1. \<langle>x\<rangle> \<Turnstile>\<^sub>c GEQ (lp_monom 1 (i + start)) (b $ i)
[PROOF STEP]
by blast
[PROOF STATE]
proof (state)
this:
\<langle>x\<rangle> \<Turnstile>\<^sub>c GEQ (lp_monom 1 (i + start)) (b $ i)

goal (1 subgoal):
 1. b $ i \<le> \<langle>x\<rangle> (i + start)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
\<langle>x\<rangle> \<Turnstile>\<^sub>c GEQ (lp_monom 1 (i + start)) (b $ i)
[PROOF STEP]
have "(lp_monom 1 (i+start)) \<lbrace>\<langle>x\<rangle>\<rbrace> \<ge> (b$i)"
[PROOF STATE]
proof (prove)
using this:
\<langle>x\<rangle> \<Turnstile>\<^sub>c GEQ (lp_monom 1 (i + start)) (b $ i)

goal (1 subgoal):
 1. b $ i \<le> lp_monom 1 (i + start) \<lbrace> \<langle>x\<rangle> \<rbrace>
[PROOF STEP]
using satisfies_constraint.simps(4)[of "\<langle>x\<rangle>" "lp_monom 1 (i + start)" "b$i"]
[PROOF STATE]
proof (prove)
using this:
\<langle>x\<rangle> \<Turnstile>\<^sub>c GEQ (lp_monom 1 (i + start)) (b $ i)
\<langle>x\<rangle> \<Turnstile>\<^sub>c GEQ (lp_monom 1 (i + start)) (b $ i) = (b $ i *R 1 \<le> lp_monom 1 (i + start) \<lbrace> \<langle>x\<rangle> \<rbrace>)

goal (1 subgoal):
 1. b $ i \<le> lp_monom 1 (i + start) \<lbrace> \<langle>x\<rangle> \<rbrace>
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
b $ i \<le> lp_monom 1 (i + start) \<lbrace> \<langle>x\<rangle> \<rbrace>

goal (1 subgoal):
 1. b $ i \<le> \<langle>x\<rangle> (i + start)
[PROOF STEP]
then
[PROOF STATE]
proof (chain)
picking this:
b $ i \<le> lp_monom 1 (i + start) \<lbrace> \<langle>x\<rangle> \<rbrace>
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
using this:
b $ i \<le> lp_monom 1 (i + start) \<lbrace> \<langle>x\<rangle> \<rbrace>

goal (1 subgoal):
 1. b $ i \<le> \<langle>x\<rangle> (i + start)
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
b $ i \<le> \<langle>x\<rangle> (i + start)

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma map_upds_apply_eq_Some:
  "((m(xs[\<mapsto>]ys)) x = Some y) =
  (let xs' = take (size ys) xs
   in if x \<in> set xs' then ys ! last_index xs' x = y else m x = Some y)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((m(xs [\<mapsto>] ys)) x = Some y) = (let xs' = take (length ys) xs in if x \<in> set xs' then ys ! last_index xs' x = y else m x = Some y)
[PROOF STEP]
by(simp add:fun_upds_apply Let_def)


[STATEMENT]
lemma fim1_state: "i < m \<Longrightarrow> i \<noteq> 0 \<Longrightarrow> fim1_state state = fs ! (i - 1)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>i < m; i \<noteq> 0\<rbrakk> \<Longrightarrow> fim1_state state = fs ! (i - 1)
[PROOF STEP]
using get_nth_im1[OF to_list_repr(1)]
[PROOF STATE]
proof (prove)
using this:
i \<noteq> 0 \<Longrightarrow> get_nth_im1 f = map ((!) fs) [0..<m] ! (i - 1)

goal (1 subgoal):
 1. \<lbrakk>i < m; i \<noteq> 0\<rbrakk> \<Longrightarrow> fim1_state state = fs ! (i - 1)
[PROOF STEP]
unfolding state
[PROOF STATE]
proof (prove)
using this:
i \<noteq> 0 \<Longrightarrow> get_nth_im1 f = map ((!) fs) [0..<m] ! (i - 1)

goal (1 subgoal):
 1. \<lbrakk>i < m; i \<noteq> 0\<rbrakk> \<Longrightarrow> fim1_state (f, mu, ds) = fs ! (i - 1)
[PROOF STEP]
by auto


[STATEMENT]
lemma set_take_nth:
  assumes "x \<in> set (take i xs)"
  shows "\<exists> j < length xs. j < i \<and> xs ! j = x"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<exists>j<length xs. j < i \<and> xs ! j = x
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
x \<in> set (take i xs)

goal (1 subgoal):
 1. \<exists>j<length xs. j < i \<and> xs ! j = x
[PROOF STEP]
by (metis in_set_conv_nth length_take min_less_iff_conj nth_take)


[STATEMENT]
lemma splitFace_f12_f21_neq_norm:
 "pre_splitFace g ram1 ram2 oldF vs \<Longrightarrow> minGraphProps g \<Longrightarrow>
 (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs \<Longrightarrow>
  normFace f12 \<noteq> normFace f21"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs\<rbrakk> \<Longrightarrow> normFace f12 \<noteq> normFace f21
[PROOF STEP]
apply (subgoal_tac "minGraphProps' newGraph")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph\<rbrakk> \<Longrightarrow> normFace f12 \<noteq> normFace f21
 2. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs\<rbrakk> \<Longrightarrow> minGraphProps' newGraph
[PROOF STEP]
apply (subgoal_tac "f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph")
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph; f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph\<rbrakk> \<Longrightarrow> normFace f12 \<noteq> normFace f21
 2. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph\<rbrakk> \<Longrightarrow> f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph
 3. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs\<rbrakk> \<Longrightarrow> minGraphProps' newGraph
[PROOF STEP]
apply (subgoal_tac "pre_split_face oldF ram1 ram2 vs")
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph; f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph; pre_split_face oldF ram1 ram2 vs\<rbrakk> \<Longrightarrow> normFace f12 \<noteq> normFace f21
 2. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph; f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph\<rbrakk> \<Longrightarrow> pre_split_face oldF ram1 ram2 vs
 3. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph\<rbrakk> \<Longrightarrow> f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph
 4. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs\<rbrakk> \<Longrightarrow> minGraphProps' newGraph
[PROOF STEP]
apply (frule split_face_f12_f21_neq_norm)
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph; f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph; pre_split_face oldF ram1 ram2 vs\<rbrakk> \<Longrightarrow> 2 < |vertices oldF|
 2. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph; f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph; pre_split_face oldF ram1 ram2 vs\<rbrakk> \<Longrightarrow> 2 < |vertices ?f12.3|
 3. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph; f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph; pre_split_face oldF ram1 ram2 vs\<rbrakk> \<Longrightarrow> 2 < |vertices ?f21.3|
 4. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph; f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph; pre_split_face oldF ram1 ram2 vs\<rbrakk> \<Longrightarrow> (?f12.3, ?f21.3) = split_face oldF ram1 ram2 vs
 5. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph; f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph; pre_split_face oldF ram1 ram2 vs; normFace ?f12.3 \<noteq> normFace ?f21.3\<rbrakk> \<Longrightarrow> normFace f12 \<noteq> normFace f21
 6. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph; f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph\<rbrakk> \<Longrightarrow> pre_split_face oldF ram1 ram2 vs
 7. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph\<rbrakk> \<Longrightarrow> f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph
 8. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs\<rbrakk> \<Longrightarrow> minGraphProps' newGraph
[PROOF STEP]
apply (rule minGraphProps2)
[PROOF STATE]
proof (prove)
goal (9 subgoals):
 1. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph; f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph; pre_split_face oldF ram1 ram2 vs\<rbrakk> \<Longrightarrow> minGraphProps ?g9
 2. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph; f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph; pre_split_face oldF ram1 ram2 vs\<rbrakk> \<Longrightarrow> oldF \<in> \<F> ?g9
 3. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph; f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph; pre_split_face oldF ram1 ram2 vs\<rbrakk> \<Longrightarrow> 2 < |vertices ?f12.3|
 4. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph; f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph; pre_split_face oldF ram1 ram2 vs\<rbrakk> \<Longrightarrow> 2 < |vertices ?f21.3|
 5. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph; f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph; pre_split_face oldF ram1 ram2 vs\<rbrakk> \<Longrightarrow> (?f12.3, ?f21.3) = split_face oldF ram1 ram2 vs
 6. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph; f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph; pre_split_face oldF ram1 ram2 vs; normFace ?f12.3 \<noteq> normFace ?f21.3\<rbrakk> \<Longrightarrow> normFace f12 \<noteq> normFace f21
 7. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph; f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph\<rbrakk> \<Longrightarrow> pre_split_face oldF ram1 ram2 vs
 8. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph\<rbrakk> \<Longrightarrow> f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph
 9. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs\<rbrakk> \<Longrightarrow> minGraphProps' newGraph
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph; f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph; pre_split_face oldF ram1 ram2 vs\<rbrakk> \<Longrightarrow> oldF \<in> \<F> g
 2. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph; f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph; pre_split_face oldF ram1 ram2 vs\<rbrakk> \<Longrightarrow> 2 < |vertices ?f12.3|
 3. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph; f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph; pre_split_face oldF ram1 ram2 vs\<rbrakk> \<Longrightarrow> 2 < |vertices ?f21.3|
 4. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph; f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph; pre_split_face oldF ram1 ram2 vs\<rbrakk> \<Longrightarrow> (?f12.3, ?f21.3) = split_face oldF ram1 ram2 vs
 5. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph; f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph; pre_split_face oldF ram1 ram2 vs; normFace ?f12.3 \<noteq> normFace ?f21.3\<rbrakk> \<Longrightarrow> normFace f12 \<noteq> normFace f21
 6. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph; f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph\<rbrakk> \<Longrightarrow> pre_split_face oldF ram1 ram2 vs
 7. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph\<rbrakk> \<Longrightarrow> f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph
 8. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs\<rbrakk> \<Longrightarrow> minGraphProps' newGraph
[PROOF STEP]
apply(erule pre_splitFace_oldF)
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph; f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph; pre_split_face oldF ram1 ram2 vs\<rbrakk> \<Longrightarrow> 2 < |vertices ?f12.3|
 2. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph; f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph; pre_split_face oldF ram1 ram2 vs\<rbrakk> \<Longrightarrow> 2 < |vertices ?f21.3|
 3. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph; f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph; pre_split_face oldF ram1 ram2 vs\<rbrakk> \<Longrightarrow> (?f12.3, ?f21.3) = split_face oldF ram1 ram2 vs
 4. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph; f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph; pre_split_face oldF ram1 ram2 vs; normFace ?f12.3 \<noteq> normFace ?f21.3\<rbrakk> \<Longrightarrow> normFace f12 \<noteq> normFace f21
 5. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph; f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph\<rbrakk> \<Longrightarrow> pre_split_face oldF ram1 ram2 vs
 6. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph\<rbrakk> \<Longrightarrow> f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph
 7. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs\<rbrakk> \<Longrightarrow> minGraphProps' newGraph
[PROOF STEP]
apply (subgoal_tac "2 < | vertices f12 |")
[PROOF STATE]
proof (prove)
goal (8 subgoals):
 1. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph; f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph; pre_split_face oldF ram1 ram2 vs; 2 < |vertices f12|\<rbrakk> \<Longrightarrow> 2 < |vertices ?f12.3|
 2. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph; f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph; pre_split_face oldF ram1 ram2 vs\<rbrakk> \<Longrightarrow> 2 < |vertices f12|
 3. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph; f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph; pre_split_face oldF ram1 ram2 vs\<rbrakk> \<Longrightarrow> 2 < |vertices ?f21.3|
 4. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph; f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph; pre_split_face oldF ram1 ram2 vs\<rbrakk> \<Longrightarrow> (?f12.3, ?f21.3) = split_face oldF ram1 ram2 vs
 5. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph; f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph; pre_split_face oldF ram1 ram2 vs; normFace ?f12.3 \<noteq> normFace ?f21.3\<rbrakk> \<Longrightarrow> normFace f12 \<noteq> normFace f21
 6. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph; f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph\<rbrakk> \<Longrightarrow> pre_split_face oldF ram1 ram2 vs
 7. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph\<rbrakk> \<Longrightarrow> f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph
 8. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs\<rbrakk> \<Longrightarrow> minGraphProps' newGraph
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph; f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph; pre_split_face oldF ram1 ram2 vs\<rbrakk> \<Longrightarrow> 2 < |vertices f12|
 2. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph; f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph; pre_split_face oldF ram1 ram2 vs\<rbrakk> \<Longrightarrow> 2 < |vertices ?f21.3|
 3. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph; f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph; pre_split_face oldF ram1 ram2 vs\<rbrakk> \<Longrightarrow> (f12, ?f21.3) = split_face oldF ram1 ram2 vs
 4. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph; f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph; pre_split_face oldF ram1 ram2 vs; normFace f12 \<noteq> normFace ?f21.3\<rbrakk> \<Longrightarrow> normFace f12 \<noteq> normFace f21
 5. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph; f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph\<rbrakk> \<Longrightarrow> pre_split_face oldF ram1 ram2 vs
 6. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph\<rbrakk> \<Longrightarrow> f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph
 7. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs\<rbrakk> \<Longrightarrow> minGraphProps' newGraph
[PROOF STEP]
apply (force simp: minGraphProps'_def)
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph; f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph; pre_split_face oldF ram1 ram2 vs\<rbrakk> \<Longrightarrow> 2 < |vertices ?f21.3|
 2. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph; f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph; pre_split_face oldF ram1 ram2 vs\<rbrakk> \<Longrightarrow> (f12, ?f21.3) = split_face oldF ram1 ram2 vs
 3. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph; f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph; pre_split_face oldF ram1 ram2 vs; normFace f12 \<noteq> normFace ?f21.3\<rbrakk> \<Longrightarrow> normFace f12 \<noteq> normFace f21
 4. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph; f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph\<rbrakk> \<Longrightarrow> pre_split_face oldF ram1 ram2 vs
 5. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph\<rbrakk> \<Longrightarrow> f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph
 6. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs\<rbrakk> \<Longrightarrow> minGraphProps' newGraph
[PROOF STEP]
apply (subgoal_tac "2 < | vertices f21 |")
[PROOF STATE]
proof (prove)
goal (7 subgoals):
 1. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph; f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph; pre_split_face oldF ram1 ram2 vs; 2 < |vertices f21|\<rbrakk> \<Longrightarrow> 2 < |vertices ?f21.3|
 2. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph; f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph; pre_split_face oldF ram1 ram2 vs\<rbrakk> \<Longrightarrow> 2 < |vertices f21|
 3. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph; f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph; pre_split_face oldF ram1 ram2 vs\<rbrakk> \<Longrightarrow> (f12, ?f21.3) = split_face oldF ram1 ram2 vs
 4. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph; f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph; pre_split_face oldF ram1 ram2 vs; normFace f12 \<noteq> normFace ?f21.3\<rbrakk> \<Longrightarrow> normFace f12 \<noteq> normFace f21
 5. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph; f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph\<rbrakk> \<Longrightarrow> pre_split_face oldF ram1 ram2 vs
 6. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph\<rbrakk> \<Longrightarrow> f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph
 7. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs\<rbrakk> \<Longrightarrow> minGraphProps' newGraph
[PROOF STEP]
apply assumption
[PROOF STATE]
proof (prove)
goal (6 subgoals):
 1. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph; f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph; pre_split_face oldF ram1 ram2 vs\<rbrakk> \<Longrightarrow> 2 < |vertices f21|
 2. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph; f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph; pre_split_face oldF ram1 ram2 vs\<rbrakk> \<Longrightarrow> (f12, f21) = split_face oldF ram1 ram2 vs
 3. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph; f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph; pre_split_face oldF ram1 ram2 vs; normFace f12 \<noteq> normFace f21\<rbrakk> \<Longrightarrow> normFace f12 \<noteq> normFace f21
 4. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph; f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph\<rbrakk> \<Longrightarrow> pre_split_face oldF ram1 ram2 vs
 5. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph\<rbrakk> \<Longrightarrow> f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph
 6. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs\<rbrakk> \<Longrightarrow> minGraphProps' newGraph
[PROOF STEP]
apply (force simp: minGraphProps'_def)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph; f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph; pre_split_face oldF ram1 ram2 vs\<rbrakk> \<Longrightarrow> (f12, f21) = split_face oldF ram1 ram2 vs
 2. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph; f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph; pre_split_face oldF ram1 ram2 vs; normFace f12 \<noteq> normFace f21\<rbrakk> \<Longrightarrow> normFace f12 \<noteq> normFace f21
 3. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph; f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph\<rbrakk> \<Longrightarrow> pre_split_face oldF ram1 ram2 vs
 4. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph\<rbrakk> \<Longrightarrow> f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph
 5. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs\<rbrakk> \<Longrightarrow> minGraphProps' newGraph
[PROOF STEP]
apply (simp add: splitFace_def split_def)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph; f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph; pre_split_face oldF ram1 ram2 vs; normFace f12 \<noteq> normFace f21\<rbrakk> \<Longrightarrow> normFace f12 \<noteq> normFace f21
 2. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph; f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph\<rbrakk> \<Longrightarrow> pre_split_face oldF ram1 ram2 vs
 3. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph\<rbrakk> \<Longrightarrow> f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph
 4. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs\<rbrakk> \<Longrightarrow> minGraphProps' newGraph
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph; f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph\<rbrakk> \<Longrightarrow> pre_split_face oldF ram1 ram2 vs
 2. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph\<rbrakk> \<Longrightarrow> f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph
 3. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs\<rbrakk> \<Longrightarrow> minGraphProps' newGraph
[PROOF STEP]
apply force
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' newGraph\<rbrakk> \<Longrightarrow> f12 \<in> \<F> newGraph \<and> f21 \<in> \<F> newGraph
 2. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs\<rbrakk> \<Longrightarrow> minGraphProps' newGraph
[PROOF STEP]
apply (simp add: splitFace_def split_def)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; f12 = fst (split_face oldF ram1 ram2 vs) \<and> f21 = snd (split_face oldF ram1 ram2 vs) \<and> newGraph = Graph (replace oldF [snd (split_face oldF ram1 ram2 vs)] (faces g) @ [fst (split_face oldF ram1 ram2 vs)]) (countVertices g + |vs|) ((if ram2 < |if ram1 < |faceListAt g| then replacefacesAt [] oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] ((replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g)))[ram1 := replace oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g)) ! ram1)]) else replacefacesAt [] oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g)))| then replacefacesAt [] oldF [fst (split_face oldF ram1 ram2 vs), snd (split_face oldF ram1 ram2 vs)] ((if ram1 < |replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g))| then replacefacesAt [] oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] ((replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g)))[ram1 := replace oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g)) ! ram1)]) else replacefacesAt [] oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g))))[ram2 := replace oldF [fst (split_face oldF ram1 ram2 vs), snd (split_face oldF ram1 ram2 vs)] ((if ram1 < |replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g))| then replacefacesAt [] oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] ((replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g)))[ram1 := replace oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g)) ! ram1)]) else replacefacesAt [] oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g)))) ! ram2)]) else replacefacesAt [] oldF [fst (split_face oldF ram1 ram2 vs), snd (split_face oldF ram1 ram2 vs)] (if ram1 < |replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g))| then replacefacesAt [] oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] ((replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g)))[ram1 := replace oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g)) ! ram1)]) else replacefacesAt [] oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g))))) @ replicate |vs| [fst (split_face oldF ram1 ram2 vs), snd (split_face oldF ram1 ram2 vs)]) (heights g @ heightsNewVertices (heights g ! ram1) (heights g ! ram2) |vs|); minGraphProps' (Graph (replace oldF [snd (split_face oldF ram1 ram2 vs)] (faces g) @ [fst (split_face oldF ram1 ram2 vs)]) (countVertices g + |vs|) ((if ram2 < |if ram1 < |faceListAt g| then replacefacesAt [] oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] ((replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g)))[ram1 := replace oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g)) ! ram1)]) else replacefacesAt [] oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g)))| then replacefacesAt [] oldF [fst (split_face oldF ram1 ram2 vs), snd (split_face oldF ram1 ram2 vs)] ((if ram1 < |replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g))| then replacefacesAt [] oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] ((replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g)))[ram1 := replace oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g)) ! ram1)]) else replacefacesAt [] oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g))))[ram2 := replace oldF [fst (split_face oldF ram1 ram2 vs), snd (split_face oldF ram1 ram2 vs)] ((if ram1 < |replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g))| then replacefacesAt [] oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] ((replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g)))[ram1 := replace oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g)) ! ram1)]) else replacefacesAt [] oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g)))) ! ram2)]) else replacefacesAt [] oldF [fst (split_face oldF ram1 ram2 vs), snd (split_face oldF ram1 ram2 vs)] (if ram1 < |replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g))| then replacefacesAt [] oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] ((replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g)))[ram1 := replace oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g)) ! ram1)]) else replacefacesAt [] oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g))))) @ replicate |vs| [fst (split_face oldF ram1 ram2 vs), snd (split_face oldF ram1 ram2 vs)]) (heights g @ heightsNewVertices (heights g ! ram1) (heights g ! ram2) |vs|))\<rbrakk> \<Longrightarrow> snd (split_face oldF ram1 ram2 vs) = fst (split_face oldF ram1 ram2 vs) \<or> snd (split_face oldF ram1 ram2 vs) \<in> set (replace oldF [snd (split_face oldF ram1 ram2 vs)] (faces g))
 2. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs\<rbrakk> \<Longrightarrow> minGraphProps' newGraph
[PROOF STEP]
apply (rule disjI2)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; f12 = fst (split_face oldF ram1 ram2 vs) \<and> f21 = snd (split_face oldF ram1 ram2 vs) \<and> newGraph = Graph (replace oldF [snd (split_face oldF ram1 ram2 vs)] (faces g) @ [fst (split_face oldF ram1 ram2 vs)]) (countVertices g + |vs|) ((if ram2 < |if ram1 < |faceListAt g| then replacefacesAt [] oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] ((replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g)))[ram1 := replace oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g)) ! ram1)]) else replacefacesAt [] oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g)))| then replacefacesAt [] oldF [fst (split_face oldF ram1 ram2 vs), snd (split_face oldF ram1 ram2 vs)] ((if ram1 < |replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g))| then replacefacesAt [] oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] ((replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g)))[ram1 := replace oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g)) ! ram1)]) else replacefacesAt [] oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g))))[ram2 := replace oldF [fst (split_face oldF ram1 ram2 vs), snd (split_face oldF ram1 ram2 vs)] ((if ram1 < |replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g))| then replacefacesAt [] oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] ((replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g)))[ram1 := replace oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g)) ! ram1)]) else replacefacesAt [] oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g)))) ! ram2)]) else replacefacesAt [] oldF [fst (split_face oldF ram1 ram2 vs), snd (split_face oldF ram1 ram2 vs)] (if ram1 < |replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g))| then replacefacesAt [] oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] ((replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g)))[ram1 := replace oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g)) ! ram1)]) else replacefacesAt [] oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g))))) @ replicate |vs| [fst (split_face oldF ram1 ram2 vs), snd (split_face oldF ram1 ram2 vs)]) (heights g @ heightsNewVertices (heights g ! ram1) (heights g ! ram2) |vs|); minGraphProps' (Graph (replace oldF [snd (split_face oldF ram1 ram2 vs)] (faces g) @ [fst (split_face oldF ram1 ram2 vs)]) (countVertices g + |vs|) ((if ram2 < |if ram1 < |faceListAt g| then replacefacesAt [] oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] ((replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g)))[ram1 := replace oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g)) ! ram1)]) else replacefacesAt [] oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g)))| then replacefacesAt [] oldF [fst (split_face oldF ram1 ram2 vs), snd (split_face oldF ram1 ram2 vs)] ((if ram1 < |replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g))| then replacefacesAt [] oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] ((replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g)))[ram1 := replace oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g)) ! ram1)]) else replacefacesAt [] oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g))))[ram2 := replace oldF [fst (split_face oldF ram1 ram2 vs), snd (split_face oldF ram1 ram2 vs)] ((if ram1 < |replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g))| then replacefacesAt [] oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] ((replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g)))[ram1 := replace oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g)) ! ram1)]) else replacefacesAt [] oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g)))) ! ram2)]) else replacefacesAt [] oldF [fst (split_face oldF ram1 ram2 vs), snd (split_face oldF ram1 ram2 vs)] (if ram1 < |replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g))| then replacefacesAt [] oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] ((replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g)))[ram1 := replace oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g)) ! ram1)]) else replacefacesAt [] oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g))))) @ replicate |vs| [fst (split_face oldF ram1 ram2 vs), snd (split_face oldF ram1 ram2 vs)]) (heights g @ heightsNewVertices (heights g ! ram1) (heights g ! ram2) |vs|))\<rbrakk> \<Longrightarrow> snd (split_face oldF ram1 ram2 vs) \<in> set (replace oldF [snd (split_face oldF ram1 ram2 vs)] (faces g))
 2. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs\<rbrakk> \<Longrightarrow> minGraphProps' newGraph
[PROOF STEP]
apply (erule replace3[OF pre_splitFace_oldF])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>minGraphProps g; f12 = fst (split_face oldF ram1 ram2 vs) \<and> f21 = snd (split_face oldF ram1 ram2 vs) \<and> newGraph = Graph (replace oldF [snd (split_face oldF ram1 ram2 vs)] (faces g) @ [fst (split_face oldF ram1 ram2 vs)]) (countVertices g + |vs|) ((if ram2 < |if ram1 < |faceListAt g| then replacefacesAt [] oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] ((replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g)))[ram1 := replace oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g)) ! ram1)]) else replacefacesAt [] oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g)))| then replacefacesAt [] oldF [fst (split_face oldF ram1 ram2 vs), snd (split_face oldF ram1 ram2 vs)] ((if ram1 < |replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g))| then replacefacesAt [] oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] ((replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g)))[ram1 := replace oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g)) ! ram1)]) else replacefacesAt [] oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g))))[ram2 := replace oldF [fst (split_face oldF ram1 ram2 vs), snd (split_face oldF ram1 ram2 vs)] ((if ram1 < |replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g))| then replacefacesAt [] oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] ((replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g)))[ram1 := replace oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g)) ! ram1)]) else replacefacesAt [] oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g)))) ! ram2)]) else replacefacesAt [] oldF [fst (split_face oldF ram1 ram2 vs), snd (split_face oldF ram1 ram2 vs)] (if ram1 < |replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g))| then replacefacesAt [] oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] ((replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g)))[ram1 := replace oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g)) ! ram1)]) else replacefacesAt [] oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g))))) @ replicate |vs| [fst (split_face oldF ram1 ram2 vs), snd (split_face oldF ram1 ram2 vs)]) (heights g @ heightsNewVertices (heights g ! ram1) (heights g ! ram2) |vs|); minGraphProps' (Graph (replace oldF [snd (split_face oldF ram1 ram2 vs)] (faces g) @ [fst (split_face oldF ram1 ram2 vs)]) (countVertices g + |vs|) ((if ram2 < |if ram1 < |faceListAt g| then replacefacesAt [] oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] ((replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g)))[ram1 := replace oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g)) ! ram1)]) else replacefacesAt [] oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g)))| then replacefacesAt [] oldF [fst (split_face oldF ram1 ram2 vs), snd (split_face oldF ram1 ram2 vs)] ((if ram1 < |replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g))| then replacefacesAt [] oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] ((replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g)))[ram1 := replace oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g)) ! ram1)]) else replacefacesAt [] oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g))))[ram2 := replace oldF [fst (split_face oldF ram1 ram2 vs), snd (split_face oldF ram1 ram2 vs)] ((if ram1 < |replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g))| then replacefacesAt [] oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] ((replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g)))[ram1 := replace oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g)) ! ram1)]) else replacefacesAt [] oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g)))) ! ram2)]) else replacefacesAt [] oldF [fst (split_face oldF ram1 ram2 vs), snd (split_face oldF ram1 ram2 vs)] (if ram1 < |replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g))| then replacefacesAt [] oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] ((replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g)))[ram1 := replace oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g)) ! ram1)]) else replacefacesAt [] oldF [snd (split_face oldF ram1 ram2 vs), fst (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram2 ram1) oldF [snd (split_face oldF ram1 ram2 vs)] (replacefacesAt (between (vertices oldF) ram1 ram2) oldF [fst (split_face oldF ram1 ram2 vs)] (faceListAt g))))) @ replicate |vs| [fst (split_face oldF ram1 ram2 vs), snd (split_face oldF ram1 ram2 vs)]) (heights g @ heightsNewVertices (heights g ! ram1) (heights g ! ram2) |vs|))\<rbrakk> \<Longrightarrow> snd (split_face oldF ram1 ram2 vs) \<in> set [snd (split_face oldF ram1 ram2 vs)]
 2. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs\<rbrakk> \<Longrightarrow> minGraphProps' newGraph
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs\<rbrakk> \<Longrightarrow> minGraphProps' newGraph
[PROOF STEP]
apply (frule splitFace_holds_minGraphProps')
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs\<rbrakk> \<Longrightarrow> minGraphProps' g
 2. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' (snd (snd (splitFace g ram1 ram2 oldF vs)))\<rbrakk> \<Longrightarrow> minGraphProps' newGraph
[PROOF STEP]
apply (simp add: minGraphProps_def minGraphProps'_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<lbrakk>pre_splitFace g ram1 ram2 oldF vs; minGraphProps g; (f12, f21, newGraph) = splitFace g ram1 ram2 oldF vs; minGraphProps' (snd (snd (splitFace g ram1 ram2 oldF vs)))\<rbrakk> \<Longrightarrow> minGraphProps' newGraph
[PROOF STEP]
by (simp add: splitFace_def split_def)