|
(seq_pigeon
(seq_pigeon_lem 0
(seq_pigeon_lem-1 nil 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"
(inst 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)
((fullset const-decl "set" sets nil)
(card const-decl "{n: nat | n = Card(S)}" finite_sets nil)
(Card const-decl "nat" finite_sets nil)
(below type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil) (>= const-decl "bool" reals nil)
(int nonempty-type-eq-decl nil integers nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(rational nonempty-type-from-decl nil rationals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(real nonempty-type-from-decl nil reals nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(finseq type-eq-decl nil finite_sequences nil)
(S formal-const-decl "finite_set[T]" seq_pigeon nil)
(finite_set type-eq-decl nil finite_sets nil)
(is_finite const-decl "bool" finite_sets nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(T formal-type-decl nil seq_pigeon nil)
(below type-eq-decl nil nat_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(injective? const-decl "bool" functions nil)
(restrict const-decl "R" restrict nil)
(finseq_appl const-decl "[below[length(fs)] -> T]" finite_sequences
nil)
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(injection_and_cardinal formula-decl nil finite_sets_card_eq
"finite_sets/")
(card_below_fullset formula-decl nil finite_sets_below
"finite_sets/")
(finite_below formula-decl nil finite_sets_below "finite_sets/"))
nil))
(seq_pigeon_hole 0
(seq_pigeon_hole-1 nil 3507100594
("" (skosimp*)
(("" (lemma "seq_pigeon_lem")
(("" (inst?)
(("" (assert)
(("" (skosimp*) (("" (inst?) (("" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((seq_pigeon_lem formula-decl nil seq_pigeon nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil) (< const-decl "bool" reals nil)
(below type-eq-decl nil naturalnumbers nil)
(finseq type-eq-decl nil finite_sequences nil)
(S formal-const-decl "finite_set[T]" seq_pigeon nil)
(finite_set type-eq-decl nil finite_sets nil)
(is_finite const-decl "bool" finite_sets nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-type-decl nil seq_pigeon nil)
(below type-eq-decl nil nat_types nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil))
nil)))
[ Dauer der Verarbeitung: 0.2 Sekunden
(vorverarbeitet)
]
|
