# Theory GeneratorProps

Up to index of Isabelle/HOL/Tame

theory GeneratorProps
imports Plane3Props LowerBound
begin

```(*  ID:         \$Id: GeneratorProps.thy,v 1.4 2006/01/13 19:18:53 nipkow Exp \$
Author:     Tobias Nipkow
*)

header "Properties of Tame Graph Enumeration (1)"

theory GeneratorProps
imports Plane3Props LowerBound
begin

lemma genPolyTame_spec:
"generatePolygonTame n v f g = [g' ∈ generatePolygon n v f g . ¬ notame g']"

lemma genPolyTame_subset_genPoly:
"g' ∈ set(generatePolygonTame i v f g) ==>
g' ∈ set(generatePolygon i v f g)"

lemma next_tame0_subset_plane:
"set(next_tame0 p g) ⊆ set(next_plane p g)"
elim!:genPolyTame_subset_genPoly simp del:upt_Suc)

lemma genPoly_new_face:
"[|g' ∈ set (generatePolygon n v f g); minGraphProps g; f ∈ set (nonFinals g);
v ∈ \<V> f; n ≥ 3 |] ==>
∃f ∈ set(finals g') - set(finals g). |vertices f| = n"
apply(rename_tac "is")
apply(frule enumerator_length2)
apply arith
apply(frule (4) pre_subdivFace_indexToVertexList)
apply(arith)
apply(subgoal_tac "indexToVertexList f v is ≠ []")
prefer 2 apply(subst length_0_conv[symmetric]) apply simp
apply(clarsimp simp:neq_Nil_conv)
apply(rename_tac "ovs")
apply(subgoal_tac "|indexToVertexList f v is| = |ovs| + 1")
prefer 2 apply(simp)
apply(drule (1) pre_subdivFace_pre_subdivFace')
apply(drule (1) final_subdivFace')
apply (simp (no_asm_use))
apply(simp)
apply blast
done

(* Could prove = instead of >=, but who needs it? *)
lemma genPoly_incr_facesquander_lb:
assumes "g' ∈ set (generatePolygon n v f g)" "inv g"
"f ∈ set(nonFinals g)" "v ∈ \<V> f" "3 ≤ n"
shows "faceSquanderLowerBound g' ≥ faceSquanderLowerBound g + \<d> n"
proof -
from genPoly_new_face[OF prems(1) inv_mgp[OF prems(2)] prems(3-5)] obtain f
where f: "f ∈ set (finals g') - set(finals g)"
and size: "|vertices f| = n" by auto
have g': "g' ∈ set(next_plane0 (n - 3) g)" using prems(5)
by(rule_tac in_next_plane0I[OF prems(1,3-5)]) simp
note dist = minGraphProps11'[OF inv_mgp[OF prems(2)]]
note inv' = invariantE[OF inv_inv_next_plane0, OF g' prems(2)]
note dist' = minGraphProps11'[OF inv_mgp[OF inv']]
note subset = next_plane0_finals_subset[OF g']
have "faceSquanderLowerBound g' ≥
faceSquanderLowerBound g + \<d> |vertices f|"
proof(unfold faceSquanderLowerBound_def)
have "(∑f∈finals g \<d> |vertices f| ) + \<d> |vertices f| =
(∑f∈set(finals g). \<d> |vertices f| ) + \<d> |vertices f|"
also have "… = (∑f∈set(finals g) ∪ {f}. \<d> |vertices f| )"
using f by simp
also have "… ≤ (∑f∈set(finals g'). \<d> |vertices f| )"
using f subset by(fastsimp intro!: setsum_mono3)
also have "… = (∑f∈finals g' \<d> |vertices f| )"
finally show "(∑f∈finals g \<d> |vertices f| ) + \<d> |vertices f|
≤ ∑f∈finals g' \<d> |vertices f|" .
qed
with size show ?thesis by blast
qed

lemma ExcessTable_empty:
"∀x ∈ \<V> g. ¬ finalVertex g x ==> ExcessTable g (vertices g) = []"

constdefs
close :: "graph => vertex => vertex => bool"
"close g u v ≡
∃f ∈ set(facesAt g u). if |vertices f| = 4 then v = f • u ∨ v = f • (f • u)
else v = f • u"

(* FIXME This should be the def of delAround *)
lemma delAround_def: "deleteAround g u ps = [p ∈ ps. ¬ close g u (fst p)]"
by (induct ps) (auto simp: deleteAroundCons close_def)

lemma close_sym: assumes mgp: "minGraphProps g" and cl: "close g u v"
shows "close g v u"
proof -
obtain f where f: "f ∈ set(facesAt g u)" and
if: "if |vertices f| = 4 then v = f • u ∨ v = f • (f • u) else v = f • u"
using cl by (unfold close_def) blast
note uf = minGraphProps6[OF mgp f]
note distf = minGraphProps3[OF mgp minGraphProps5[OF mgp f]]
show ?thesis
proof cases
assume 4: "|vertices f| = 4"
hence "v = f • u ∨ v = f • (f • u)" using if by simp
thus ?thesis
proof
assume "v = f • u"
then obtain f' where "f' ∈ set(facesAt g v)" "f' • v = u"
using mgp_nextVertex_face_ex2[OF mgp f] by blast
thus ?thesis by(auto simp:close_def)
next
assume v: "v = f • (f • u)"
hence "f • (f • v) = u" using quad_next4_id[OF 4 distf uf] by simp
moreover have "f ∈ set(facesAt g v)" using v uf
by(simp add: minGraphProps7[OF mgp minGraphProps5[OF mgp f]])
ultimately show ?thesis using 4 by(auto simp:close_def)
qed
next
assume "|vertices f| ≠ 4"
hence "v = f • u" using if by simp
then obtain f' where "f' ∈ set(facesAt g v)" "f' • v = u"
using mgp_nextVertex_face_ex2[OF mgp f] by blast
thus ?thesis by(auto simp:close_def)
qed
qed

lemma preSep_conv:
assumes mgp: "minGraphProps g"
shows "preSeparated g V = (∀u∈V.∀v∈V. u ≠ v --> ¬ close g u v)" (is "?P = ?Q")
proof
assume preSep: ?P
show ?Q
proof(clarify)
fix u v assume uv: "u ∈ V" "v ∈ V" "u ≠ v" and cl: "close g u v"
from cl obtain f where f: "f ∈ set(facesAt g u)" and
if: "if |vertices f| = 4 then (v = f • u) ∨ (v = f • (f • u))
else (v = f • u)"
by (unfold close_def) blast
note uf = minGraphProps6[OF mgp f]
show False
proof cases
assume 4: "|vertices f| = 4"
hence "v = f • u ∨ v = f • (f • u)" using if by simp
thus False
proof
assume "v = f • u"
thus False using preSep f uv
next
assume "v = f • (f • u)"
moreover hence "v ∈ \<V> f" using `u ∈ \<V> f` by simp
moreover have "|vertices f| ≤ 4" using 4 by arith
ultimately show False using preSep f uv `u ∈ \<V> f`
apply(unfold preSeparated_def separated2_def separated3_def)
(* why does blast get stuck? *)
apply(subgoal_tac "f • (f • u) ∈ \<V> f ∩ V")
prefer 2 apply blast
by simp
qed
next
assume 4: "|vertices f| ≠ 4"
hence "v = f • u" using if by simp
thus False using preSep f uv
qed
qed
next
assume not_cl: ?Q
show ?P
show "separated2 g V"
proof (clarsimp simp:separated2_def)
fix v f assume "v ∈ V" and f: "f ∈ set (facesAt g v)" and "f • v ∈ V"
thus False using not_cl mgp_facesAt_no_loop[OF mgp f]
by(fastsimp simp: close_def split:split_if_asm)
qed
show "separated3 g V"
proof (clarsimp simp:separated3_def)
fix v f
assume "v ∈ V" and f: "f ∈ set (facesAt g v)" and len: "|vertices f| ≤ 4"
note distf = minGraphProps3[OF mgp minGraphProps5[OF mgp f]]
note vf = minGraphProps6[OF mgp f]
{ fix u assume "u ∈ \<V> f" and "u ∈ V"
have "u = v"
proof cases
assume 3: "|vertices f| = 3"
hence "\<V> f = {v, f • v, f • (f • v)}"
using vertices_triangle[OF _ vf distf] by simp
moreover
{ assume "u = f • v"
hence "u = v"
using not_cl f `u ∈ V` `v ∈ V` 3
by(force simp:close_def split:split_if_asm)
}
moreover
{ assume "u = f • (f • v)"
hence fu: "f • u = v"
by(simp add: tri_next3_id[OF 3 distf `v ∈ \<V> f`])
hence "(u,v) ∈ \<E> f" using nextVertex_in_edges[OF `u ∈ \<V> f`]
then obtain f' where "f' ∈ set(facesAt g v)" "(v,u) ∈  \<E> f'"
using mgp_edge_face_ex[OF mgp f] by blast
hence "u = v" using not_cl `u ∈ V` `v ∈ V` 3
by(force simp:close_def edges_face_eq split:split_if_asm)
}
ultimately show "u=v" using `u ∈ \<V> f` by blast
next
assume 3: "|vertices f| ≠ 3"
hence 4: "|vertices f| = 4"
using len mgp_vertices3[OF mgp minGraphProps5[OF mgp f]] by arith
hence "\<V> f = {v, f • v, f • (f • v), f • (f • (f • v))}"
using vertices_quad[OF _ vf distf] by simp
moreover
{ assume "u = f • v"
hence "u = v"
using not_cl f `u ∈ V` `v ∈ V` 4
by(force simp:close_def split:split_if_asm)
}
moreover
{ assume "u = f • (f • v)"
hence "u = v"
using not_cl f `u ∈ V` `v ∈ V` 4
by(force simp:close_def split:split_if_asm)
}
moreover
{ assume "u = f • (f • (f • v))"
hence fu: "f • u = v"
hence "(u,v) ∈ \<E> f" using nextVertex_in_edges[OF `u ∈ \<V> f`]
then obtain f' where "f' ∈ set(facesAt g v)" "(v,u) ∈  \<E> f'"
using mgp_edge_face_ex[OF mgp f] by blast
hence "u = v" using not_cl `u ∈ V` `v ∈ V` 4
by(force simp:close_def edges_face_eq split:split_if_asm)
}
ultimately show "u=v" using `u ∈ \<V> f` by blast
qed
}
thus "\<V> f ∩ V = {v}" using `v ∈ V` vf by blast
qed
qed
qed

lemma fin_aux: "finite B ==> finite{f A|A. A ⊆ B ∧ P A}"
apply(rule finite_subset[where B = "f ` Pow B"])
apply blast
apply simp
done

lemma preSep_ne: "∃P ⊆ M. preSeparated g (fst ` P)"
by(unfold preSeparated_def separated2_def separated3_def) blast

lemma ExcessNotAtRec_conv_Max:
assumes mgp: "minGraphProps g"
shows "distinct(map fst ps) ==> ExcessNotAtRec ps g =
Max{ ∑p∈P. snd p |P. P ⊆ set ps ∧ preSeparated g (fst ` P)}"
(concl is "_ = Max(?M ps)" is "_ = Max{_ |P. ?S ps P}")
proof(induct ps rule: length_induct)
case (1 ps0)
note IH = 1(1) and dist = 1(2)
show ?case
proof (cases ps0)
case Nil thus ?thesis by(simp add:Max_def)
next
case (Cons p ps)
let ?ps = "deleteAround g (fst p) ps"
have le: "|?ps| ≤ |ps|" by(simp add:delAround_def)
have dist': "distinct(map fst ?ps)" using dist Cons
apply (clarsimp simp:delAround_def)
apply(drule distinct_filter[where P = "Not o close g (fst p)"])
done
have "ExcessNotAtRec ps0 g = max (Max(?M ps)) (snd p + Max(?M ?ps))"
using Cons IH le dist dist' by(simp)
also have "snd p + Max(?M ?ps) =
(Max{snd p + (∑p∈P. snd p) |P. ?S ?ps P})"
also have "{snd p + (∑p∈P. snd p) |P. ?S ?ps P} =
{setsum snd (insert p P) |P. ?S ?ps P}"
using dist Cons
apply (auto simp:delAround_def)
apply(rule_tac x=P in exI)
apply(fastsimp intro!: setsum_insert[THEN trans,symmetric] elim: finite_subset)
apply(rule_tac x=P in exI)
apply(fastsimp intro!: setsum_insert[THEN trans] elim: finite_subset)
done
also have "… = {setsum snd P |P.
P ⊆ insert p (set ?ps) ∧ p ∈ P ∧ preSeparated g (fst ` P)}"
apply(rule_tac x = "insert p P" in exI)
apply simp
apply(rule conjI) apply blast
apply (blast intro:close_sym[OF mgp])
apply(rule_tac x = "P-{p}" in exI)
apply blast
done
also have "… = {setsum snd P |P.
P ⊆ insert p (set ps) ∧ p ∈ P ∧ preSeparated g (fst ` P)}"
using Cons dist
apply(rule_tac x = "P" in exI)
apply simp
apply auto
done
also have "max (Max(?M ps)) (Max …) = Max(?M ps ∪ {setsum snd P |P.
P ⊆ insert p (set ps) ∧ p ∈ P ∧ preSeparated g (fst ` P)})"
(is "_ = Max ?U")
proof -
have "{setsum snd P |P.
P ⊆ insert p (set ps) ∧ p ∈ P ∧ preSeparated g (fst ` P)} ≠ {}"
apply simp
apply(rule_tac x="{p}" in exI)
thus ?thesis by(simp add: Max_Un fin_aux preSep_ne)
qed
also have "?U = ?M ps0" using Cons by simp blast
finally show ?thesis .
qed
qed

lemma dist_ExcessTab: "distinct (map fst (ExcessTable g (vertices g)))"

lemma mono_ExcessTab: "[|g' ∈ set (next_plane0p g); inv g |] ==>
set(ExcessTable g (vertices g)) ⊆ set(ExcessTable g' (vertices g'))"
apply(clarsimp simp:ExcessTable_def image_def)
apply(rule conjI)
apply(blast dest:next_plane0_vertices_subset inv_mgp)
apply (clarsimp simp:ExcessAt_def split:split_if_asm)
apply(frule (3) next_plane0_finalVertex_mono)
done

lemma close_antimono:
"[|g' ∈ set (next_plane0p g); inv g; u ∈ \<V> g; finalVertex g u |] ==>
close g' u v ==> close g u v"

lemma ExcessTab_final:
"p ∈ set(ExcessTable g (vertices g)) ==> finalVertex g (fst p)"
by(clarsimp simp:ExcessTable_def image_def ExcessAt_def split:split_if_asm)

lemma ExcessTab_vertex:
"p ∈ set(ExcessTable g (vertices g)) ==> fst p ∈ \<V> g"
by(clarsimp simp:ExcessTable_def image_def ExcessAt_def split:split_if_asm)

lemma next_plane0_incr_ExcessNotAt:
"[|g' ∈ set (next_plane0p g); inv g |] ==>
ExcessNotAt g None ≤ ExcessNotAt g' None"
apply(frule (1) invariantE[OF inv_inv_next_plane0])
apply(frule (1) mono_ExcessTab)
apply(simp add: ExcessNotAt_def ExcessNotAtRec_conv_Max[OF _ dist_ExcessTab])
apply(rule Max_mono)
prefer 2 apply (simp add: preSep_ne)
prefer 2 apply (simp add: fin_aux)
apply auto
apply(rule_tac x=P in exI)
apply auto
apply (blast intro:close_antimono ExcessTab_final ExcessTab_vertex)
done
(* close -> in neibhood ?? *)

lemma next_plane0_incr_squander_lb:
"[|g' ∈ set (next_plane0p g); inv g |] ==>
squanderLowerBound g ≤ squanderLowerBound g'"
apply(frule (1) next_plane0_incr_ExcessNotAt)
apply(drule (4) genPoly_incr_facesquander_lb)
apply arith
done

lemma inv_notame:
"[|g' ∈ set (next_plane0p g); inv g; notame g|]
==> notame g'"
apply(erule disjE)
apply(rule disjI1)
apply(clarify)
apply(frule inv_mgp)
apply(frule (2) next_plane0_incr_degree)
apply(frule (2) next_plane0_incr_except)
apply(frule (1) next_plane0_vertices_subset)
apply(case_tac "except g' v = 0")
apply(rule bexI) prefer 2 apply fast
apply simp
apply(rule bexI) prefer 2 apply fast
apply (simp split:split_if_asm)
apply(frule (1) next_plane0_incr_squander_lb)
apply(arith)
done

lemma inv_inv_notame:
"invariant(λg. inv g ∧ notame g) next_planep"
apply(blast intro: inv_notame mgp_next_plane0_if_next_plane[OF inv_mgp]
invariantE[OF inv_inv_next_plane])
done

lemma untame_notame:
"untame (λg. inv g ∧ notame g)"
proof(clarsimp simp add: notame_def untame_def tame45_def is_tame7_def
linorder_not_le linorder_not_less)
fix g assume "final g" "inv g" "tame g"
and cases: "(∃v∈\<V> g. (except g v = 0 --> 6 < degree g v) ∧
(0 < except g v --> 5 < degree g v))
∨ squanderTarget ≤ squanderLowerBound g"
(is "?A ∨ ?B" is "(∃v∈\<V> g. ?C v) ∨ _")
from cases show False
proof
assume ?A
then obtain v where v: "v ∈\<V> g" "?C v" by auto
show False
proof cases
assume "except g v = 0"
thus False using `tame g` v by(auto simp: tame_def tame45_def)
next
assume "except g v ≠ 0"
thus False using `tame g` v
by(auto simp: except_def filter_empty_conv tame_def tame45_def
minGraphProps_facesAt_eq[OF inv_mgp[OF `inv g`]] split:split_if_asm)
qed
next
assume ?B
thus False using total_weight_lowerbound[OF `inv g` `final g` `tame g`]
`tame g`  by(force simp add:tame_def tame7_def)
qed
qed

lemma polysizes_tame:
"[| g' ∈ set (generatePolygon n v f g); inv g; f ∈ set(nonFinals g);
v ∈ \<V> f; 3 ≤ n; n < 4+p; n ∉ set(polysizes p g) |]
==> notame g'"
apply(frule (4) in_next_plane0I)
apply(frule (4) genPoly_incr_facesquander_lb)
apply(frule (1) next_plane0_incr_ExcessNotAt)
polysizes_def squanderLowerBound_def)
done

lemma genPolyTame_notame:
"[| g' ∈ set (generatePolygon n v f g); g' ∉ set (generatePolygonTame n v f g);
inv g; 3 ≤ n |]
==> notame g'"
by(fastsimp simp:generatePolygon_def generatePolygonTame_def enum_enumerator
notame_def)

declare upt_Suc[simp del] (* FIXME global? *)
lemma excess_notame:
"[| inv g; g' ∈ set (next_planep g); g' ∉ set (next_tame0 p g) |]
==> notame g'"
apply(frule (1) mgp_next_plane0_if_next_plane[OF inv_mgp])
apply(rename_tac n)
apply(case_tac "n ∈ set(polysizes p g)")
apply(drule bspec) apply assumption
apply(subgoal_tac "minimalFace (nonFinals g) ∈ set(nonFinals g)")
apply(subgoal_tac "minimalVertex g (minimalFace (nonFinals g)) ∈ \<V>(minimalFace (nonFinals g))")
apply(blast intro:polysizes_tame)
apply(rule minimal_in_set)
apply(erule mgp_vertices_nonempty[OF inv_mgp])
done
declare upt_Suc[simp]

lemma next_tame0_comp: "[| Seedp [next_plane p]->* g; final g; tame g |]
==> Seedp [next_tame0 p]->* g"
apply(rule filterout_untame_succs[OF inv_inv_next_plane inv_inv_notame
untame_notame])
apply(blast intro:excess_notame)
apply assumption
apply(rule inv_Seed)
apply assumption
apply assumption
done

lemma next_tame1_comp:
"[| tame g; final g; Seedp [next_tame0 p]->* g |]
==> Seedp [next_tame1p]->* g"
apply (unfold next_tame1_def)
apply(rule make3Fin_complete)
apply(blast intro: inv_subset[OF inv_inv_next_plane next_tame0_subset_plane])
apply(rule next_tame0_subset_plane)
apply assumption+
done

lemma inv_inv_next_tame0: "invariant inv (next_tame0 p)"
by(rule inv_subset[OF inv_inv_next_plane next_tame0_subset_plane])

lemma inv_inv_next_tame1: "invariant inv next_tame1p"
apply(rule inv_comp_map[OF inv_inv_next_tame0])
by(blast intro:RTranCl_inv[OF inv_inv_next_plane] mk3Fin_in_RTranCl)

lemma inv_inv_next_tame: "invariant inv next_tamep"
apply(rule inv_subset[OF inv_inv_next_tame1])
apply auto
done

lemma mgp_TameEnum: "g ∈ TameEnump ==> minGraphProps g"
by (unfold TameEnumP_def)
(blast intro: RTranCl_inv[OF inv_inv_next_tame] inv_Seed inv_mgp)

end
```

lemma genPolyTame_spec:

`  generatePolygonTame n v f g = [g'∈generatePolygon n v f g . ¬ notame g']`

lemma genPolyTame_subset_genPoly:

`  g' ∈ set (generatePolygonTame i v f g) ==> g' ∈ set (generatePolygon i v f g)`

lemma next_tame0_subset_plane:

`  set (next_tame0p g) ⊆ set (next_planep g)`

lemma genPoly_new_face:

```  [| g' ∈ set (generatePolygon n v f g); minGraphProps g; f ∈ set (nonFinals g);
v ∈ \<V> f; 3 ≤ n |]
==> ∃f∈set (finals g') - set (finals g). |vertices f| = n```

lemma genPoly_incr_facesquander_lb:

```  [| g' ∈ set (generatePolygon n v f g); Invariants.inv g; f ∈ set (nonFinals g);
v ∈ \<V> f; 3 ≤ n |]
==> faceSquanderLowerBound g + \<d> n ≤ faceSquanderLowerBound g'```

lemma ExcessTable_empty:

`  ∀x∈\<V> g. ¬ finalVertex g x ==> ExcessTable g (vertices g) = []`

lemma delAround_def:

`  deleteAround g u ps = [p∈ps . ¬ close g u (fst p)]`

lemma close_sym:

`  [| minGraphProps g; close g u v |] ==> close g v u`

lemma preSep_conv:

`  minGraphProps g ==> preSeparated g V = (∀u∈V. ∀v∈V. u ≠ v --> ¬ close g u v)`

lemma fin_aux:

`  finite B ==> finite {f A |A. A ⊆ B ∧ P A}`

lemma preSep_ne:

`  ∃P⊆M. preSeparated g (fst ` P)`

lemma ExcessNotAtRec_conv_Max:

```  [| minGraphProps g; distinct (map fst ps) |]
==> ExcessNotAtRec ps g =
Max {setsum snd P |P. P ⊆ set ps ∧ preSeparated g (fst ` P)}```

lemma dist_ExcessTab:

`  distinct (map fst (ExcessTable g (vertices g)))`

lemma mono_ExcessTab:

```  [| g' ∈ set (next_plane0p g); Invariants.inv g |]
==> set (ExcessTable g (vertices g)) ⊆ set (ExcessTable g' (vertices g'))```

lemma close_antimono:

```  [| g' ∈ set (next_plane0p g); Invariants.inv g; u ∈ \<V> g; finalVertex g u;
close g' u v |]
==> close g u v```

lemma ExcessTab_final:

`  p ∈ set (ExcessTable g (vertices g)) ==> finalVertex g (fst p)`

lemma ExcessTab_vertex:

`  p ∈ set (ExcessTable g (vertices g)) ==> fst p ∈ \<V> g`

lemma next_plane0_incr_ExcessNotAt:

```  [| g' ∈ set (next_plane0p g); Invariants.inv g |]
==> ExcessNotAt g None ≤ ExcessNotAt g' None```

lemma next_plane0_incr_squander_lb:

```  [| g' ∈ set (next_plane0p g); Invariants.inv g |]
==> squanderLowerBound g ≤ squanderLowerBound g'```

lemma inv_notame:

`  [| g' ∈ set (next_plane0p g); Invariants.inv g; notame g |] ==> notame g'`

lemma inv_inv_notame:

`  invariant (λg. Invariants.inv g ∧ notame g) next_planep`

lemma untame_notame:

`  untame (λg. Invariants.inv g ∧ notame g)`

lemma polysizes_tame:

```  [| g' ∈ set (generatePolygon n v f g); Invariants.inv g; f ∈ set (nonFinals g);
v ∈ \<V> f; 3 ≤ n; n < 4 + p; n ∉ set (polysizes p g) |]
==> notame g'```

lemma genPolyTame_notame:

```  [| g' ∈ set (generatePolygon n v f g); g' ∉ set (generatePolygonTame n v f g);
Invariants.inv g; 3 ≤ n |]
==> notame g'```

lemma excess_notame:

```  [| Invariants.inv g; g' ∈ set (next_planep g); g' ∉ set (next_tame0p g) |]
==> notame g'```

lemma next_tame0_comp:

`  [| Seedp [next_planep]->* g; final g; tame g |] ==> Seedp [next_tame0p]->* g`

lemma next_tame1_comp:

`  [| tame g; final g; Seedp [next_tame0p]->* g |] ==> Seedp [next_tame1p]->* g`

lemma inv_inv_next_tame0:

`  invariant Invariants.inv next_tame0p`

lemma inv_inv_next_tame1:

`  invariant Invariants.inv next_tame1p`

lemma inv_inv_next_tame:

`  invariant Invariants.inv next_tamep`

lemma mgp_TameEnum:

`  g ∈ TameEnump ==> minGraphProps g`