text‹This is an optimized definition of plane graphs and the one we
as our point of reference. In every step only one fixed nonfinal
(the smallest one) and one edge in that face are picked.›
definition minimalVertex :: "graph → face → vertex"where "minimalVertex g f ≡ minimal (height g) (vertices f)"
definition next_plane :: "nat → graph → graph list" (‹next'_plane›) where "next_plane g ≡ let fs = nonFinals g in if fs = [] then [] else let f = minimalFace fs; v = minimalVertex g f in ⊔∈[3..<Suc(maxGon p)] generatePolygon i v f g"
definition PlaneGraphsP :: "nat → graph set" (‹PlaneGraphs›) where "PlaneGraphs≡ {g. Seed [next_plane]→* g ∧ final g}"
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung und die Messung sind noch experimentell.
