header {* Neglectable Final Graphs *}
theory TameEnum
imports Generator
begin
definition is_tame :: "graph => bool" where
"is_tame g ≡ tame10 g ∧ tame11a g ∧ tame12o g ∧ is_tame13a g"
definition next_tame :: "nat => graph => graph list" ("next'_tame⇘_⇙") where
"next_tame⇘p⇙ ≡ filter (λg. ¬ final g ∨ is_tame g) o next_tame0⇘p⇙"
definition TameEnumP :: "nat => graph set" ("TameEnum⇘_⇙") where
"TameEnum⇘p⇙ ≡ {g. Seed⇘p⇙ [next_tame⇘p⇙]->* g ∧ final g}"
definition TameEnum :: "graph set" where
"TameEnum ≡ \<Union>p≤3. TameEnum⇘p⇙"
end