(graph_inductionsnil 3307708422 ("" (grind) nil nil )"graph[T]" graph_inductions nil )"{n: nat | n = Card(S)}" finite_sets nil )"nat" finite_sets nil )"bool" finite_sets nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"bool" reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )nil naturalnumbers nil )set type-eq-decl nil sets nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"set[T]" doubletons nil )nil doubletons nil )"[bool, bool -> bool]" booleans nil )nil finite_sets nil )nil graphs nil )nil graphs nil )"(total_order?[real])" nil )"graph[T]" graph_inductions nil )nil graph_inductions nil )"nat" graphs nil )"boolean" notequal nil ))nil ))nil 3307708422"" (skosimp)"" (lemma "size_prep" )"" (inst -1 "P!1" )"" (flatten)"" (hide -1)"" (split -1)"1" (propax) nil nil )"2" (hide 2)"2" (induct "n" 1 "NAT_induction" )"2" (skosimp*)"2" (inst -3 "G!1" )"2" (split -3)"1" (propax) nil nil )"2" (skosimp*)"2" (inst -2 "size(GG!1)" )"2" (assert ) (("2" (inst?) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil graph_inductions nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"nat" graphs nil )nil naturalnumbers nil )"(strict_total_order?[real])" real_props nil )nil defined_types nil )nil graphs nil )"[bool, bool -> bool]" booleans nil )nil graphs nil )nil finite_sets nil )nil doubletons nil )"set[T]" doubletons nil )"[T, T -> boolean]" equalities nil )"boolean" notequal nil )AND const-decl "[bool, bool -> bool]" booleans nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil graph_inductions nil ))nil ))nil 3307708422"" (skosimp*)"" (lemma "graph_induction_vert" )"" (inst -1 "(LAMBDA (GG: graph[T]): NOT P!1(GG))" )"" (prop)"1" (inst?) nil nil )"2" (skosimp*)"2" (inst -3 "G!2" )"2" (assert )"2" (skosimp*)"2" (inst -1 "GG!1" ) (("2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil graph_inductions nil )"(strict_total_order?[real])" real_props nil )NOT const-decl "[bool -> bool]" booleans nil )nil defined_types nil )nil graphs nil )"[bool, bool -> bool]" booleans nil )nil graphs nil )nil finite_sets nil )nil doubletons nil )"set[T]" doubletons nil )"[T, T -> boolean]" equalities nil )"boolean" notequal nil )AND const-decl "[bool, bool -> bool]" booleans nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil graph_inductions nil ))nil ))nil 3307708422"" (skosimp*)"" (prop)"1" (skosimp*) (("1" (inst?) nil nil )) nil )"2" (skosimp*)"2" (inst?) (("2" (assert ) (("2" (inst?) nil nil )) nil ))nil ))nil ))nil ))nil )nil graphs nil )"[bool, bool -> bool]" booleans nil )nil graphs nil )nil finite_sets nil )nil doubletons nil )"set[T]" doubletons nil )"[T, T -> boolean]" equalities nil )"boolean" notequal nil )AND const-decl "[bool, bool -> bool]" booleans nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil graph_inductions nil )"nat" graph_ops nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil ))nil ))nil 3307708422"" (skosimp)"" (lemma "num_edges_prep" )"" (inst -1 "P!1" )"" (flatten)"" (hide -1)"" (split -1)"1" (propax) nil nil )"2" (hide 2)"2" (induct "n" 1 "NAT_induction" )"2" (skosimp*)"2" (inst -3 "G!1" )"2" (split -3)"1" (propax) nil nil )"2" (skosimp*)"2" (inst -2 "num_edges(GG!1)" )"2" (assert ) (("2" (inst?) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil graph_inductions nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil naturalnumbers nil )"nat" graph_ops nil )nil naturalnumbers nil )"(strict_total_order?[real])" real_props nil )nil defined_types nil )nil graphs nil )"[bool, bool -> bool]" booleans nil )nil graphs nil )nil finite_sets nil )nil doubletons nil )"set[T]" doubletons nil )"[T, T -> boolean]" equalities nil )"boolean" notequal nil )AND const-decl "[bool, bool -> bool]" booleans nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil graph_inductions nil ))nil )))quality 100%
¤ Dauer der Verarbeitung: 0.18 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
