| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/Isabelle/Archive-of-Formal-Proofs/thys/Flyspeck-Tame/ (Sammlung formaler Beweise Version 2026-5©) Datei vom 31.4.2026 mit Größe 871 B |
|
Quelle TameEnum.thySprache: 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.8 Sekunden (vorverarbeitet am 2026-06-10) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-06-09