(seq_pigeonnil 3507100594"" (skosimp*)"" (case "length(w!1) = card(fullset[below(length(w!1))])" )"1" (replace -1)"1" (hide -1)"1" (lemma "injection_and_cardinal[below(length(w!1)),T]" )"1" (inst?)"1" (assert )"1" (hide 2)"1" "(LAMBDA (i: below(length(w!1))): w!1(i))" )"1" (expand "restrict" )"1" (expand "injective?" )"1" (skosimp*)"1" (inst?)"1" (inst -2 "x2!1" )"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite "card_below_fullset" ) nil nil )"3" (rewrite "finite_below" ) nil nil ))nil ))nil )"set" sets nil )"{n: nat | n = Card(S)}" finite_sets nil )"nat" finite_sets nil )nil naturalnumbers nil )"bool" reals nil ) (>= const-decl "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 finite_sequences nil )"finite_set[T]" seq_pigeon nil )nil finite_sets nil )"bool" finite_sets nil )set type-eq-decl nil sets nil )nil booleans nil )nil seq_pigeon nil )nil nat_types nil )nil naturalnumbers nil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil numbers nil )"bool" functions nil )"R" restrict nil )"[below[length(fs)] -> T]" finite_sequencesnil )"(total_order?[real])" nil )nil finite_sets_card_eq"finite_sets/" )nil finite_sets_below"finite_sets/" )nil finite_sets_below "finite_sets/" ))nil ))nil 3507100594"" (skosimp*)"" (lemma "seq_pigeon_lem" )"" (inst?)"" (assert )"" (skosimp*) (("" (inst?) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )nil seq_pigeon nil )"(strict_total_order?[real])" real_props 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 ) (< const-decl "bool" reals nil )nil naturalnumbers nil )nil finite_sequences nil )"finite_set[T]" seq_pigeon nil )nil finite_sets nil )"bool" finite_sets nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil seq_pigeon nil )nil nat_types nil )nil naturalnumbers nil ))nil )))quality 100%
¤ Dauer der Verarbeitung: 0.14 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
