| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Archive-of-Formal-Proofs/thys/Flyspeck-Tame/ (Archive of formal Proofs Version 2026-5©) Datei vom 31.4.2026 mit Größe 871 B |
|
Quelle TameEnum.thy Sprache: Isabelle |
|||||||||||||||||||||||||
|
(* Author: Gertrud Bauer, Tobias Nipkow *) section ‹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 ≡ filter (λg. ¬ final g ∨ is_tame g) ∘ next_tame0" definition TameEnumP :: "nat → graph set" (‹TameEnum›) where "TameEnum ≡ {g. Seed [next_tame]→* g ∧ final g}" definition TameEnum :: "graph set" where "TameEnum ≡ ∪p≤3. TameEnum" end
¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet am 2026-11-04) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||||||||||||
2026-11-01