|
(permutations_fseq
(perm_length 0
(perm_length-1 nil 3506271679
("" (skosimp*)
(("" (expand "permutation?")
(("" (skosimp*)
(("" (expand "bijective?")
(("" (flatten)
((""
(lemma
"injection_and_cardinal[below(length(A!1)),below(length(B!1))]")
((""
(inst -1 "fullset[below(length(A!1))]"
"fullset[below(length(B!1))]")
(("1" (split -1)
(("1"
(lemma
"surjection_and_cardinal[below(length(A!1)),below(length(B!1))]")
(("1"
(inst -1 "fullset[below(length(A!1))]"
"fullset[below(length(B!1))]")
(("1" (split -1)
(("1" (rewrite "card_below_fullset")
(("1" (rewrite "card_below_fullset")
(("1" (assert) nil)))))
("2" (inst + "f!1")
(("1" (hide -1 -2 -4 2)
(("1" (expand "surjective?")
(("1"
(skosimp*)
(("1"
(inst -1 "y!1")
(("1"
(skosimp*)
(("1"
(inst + "x!1")
(("1"
(expand "restrict")
(("1" (propax) nil)))
("2"
(expand "fullset")
(("2"
(propax)
nil)))))))))))))))
("2" (skosimp*)
(("2" (hide -1 -2 -3 2)
(("2"
(ground)
(("2" (grind) nil)))))))))))
("2" (rewrite "finite_below") nil)
("3" (rewrite "finite_below") nil)))))
("2" (inst + "f!1")
(("1" (hide -2 -3 2)
(("1" (expand "injective?")
(("1" (skosimp*)
(("1" (expand "restrict")
(("1" (inst - "x1!1" "x2!1")
(("1" (assert) nil)))))))))))
("2" (skosimp*)
(("2" (hide -1 -2 -3 2)
(("2" (grind) nil)))))))))
("2" (rewrite "finite_below") nil)
("3" (rewrite "finite_below") nil))))))))))))))
nil)
((permutation? const-decl "bool" permutations_fseq nil)
(bijective? const-decl "bool" functions nil)
(below type-eq-decl nil naturalnumbers nil)
(fsq type-eq-decl nil fsq nil)
(T formal-nonempty-type-decl nil permutations_fseq nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans 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)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(injection_and_cardinal formula-decl nil finite_sets_card_eq
"finite_sets/")
(finite_below formula-decl nil finite_sets_below "finite_sets/")
(f!1 skolem-const-decl "[below(length(A!1)) -> below(length(B!1))]"
permutations_fseq nil)
(restrict const-decl "R" restrict nil)
(surjective? const-decl "bool" functions nil)
(x!1 skolem-const-decl "below(length(A!1))" permutations_fseq nil)
(card_below_fullset formula-decl nil finite_sets_below
"finite_sets/")
(real_le_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(surjection_and_cardinal formula-decl nil finite_sets_card_eq
"finite_sets/")
(injective? const-decl "bool" functions nil)
(finite_set type-eq-decl nil finite_sets nil)
(B!1 skolem-const-decl "fsq[T]" permutations_fseq nil)
(A!1 skolem-const-decl "fsq[T]" permutations_fseq nil)
(set type-eq-decl nil sets nil)
(is_finite const-decl "bool" finite_sets nil)
(fullset const-decl "set" sets nil))
nil))
(perm_reflexive 0
(perm_reflexive-1 nil 3506271679
("" (skosimp*)
(("" (expand "permutation?")
(("" (inst 1 "(LAMBDA (ii: below(length(A!1))): ii)")
(("" (prop)
(("1" (expand "bijective?") (("1" (grind) nil)))
("2" (skosimp*) (("2" (assert) nil))))))))))
nil)
((permutation? const-decl "bool" permutations_fseq nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(surjective? const-decl "bool" functions nil)
(injective? const-decl "bool" functions nil)
(bijective? const-decl "bool" functions nil)
(below type-eq-decl nil naturalnumbers nil)
(fsq type-eq-decl nil fsq nil)
(T formal-nonempty-type-decl nil permutations_fseq nil)
(< const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(>= const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans 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)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil))
nil))
(perm_symmetric 0
(perm_symmetric-1 nil 3506271679
("" (skosimp*)
(("" (lemma "perm_length")
(("" (inst?)
(("" (assert)
(("" (hide -1)
(("" (expand "permutation?")
(("" (skosimp*)
(("" (case "length(A!1) = 0")
(("1" (inst 1 "(LAMBDA (ii: below(0)): 0)")
(("1" (grind) nil)
("2" (skosimp*) (("2" (assert) nil)))
("3" (skosimp*) nil) ("4" (skosimp*) nil)))
("2" (inst + "inverse(f!1)")
(("1" (rewrite "bij_inv_is_bij")
(("1" (assert)
(("1" (skosimp*)
(("1" (inst -2 "inverse(f!1)(ii!1)")
(("1"
(case-replace
"f!1(inverse(f!1)(ii!1)) = ii!1")
(("1" (assert) nil)
("2"
(hide -2 3)
(("2"
(expand "bijective?")
(("2"
(flatten)
(("2"
(lemma
"surjective_inverse[below(length(A!1)),below(length(B!1))]")
(("1"
(inst
-1
"inverse(f!1)(ii!1)"
"ii!1"
"f!1")
(("1" (assert) nil)
("2"
(hide 2)
(("2" (inst 1 "0") nil)))))
("2"
(assert)
(("2"
(inst 1 "0")
nil)))))))))))
("3" (inst 1 "0") nil)))
("2" (inst 1 "0") nil)))))))
("2" (inst 1 "0") nil)))
("2" (inst 1 "0")
(("2" (assert) nil))))))))))))))))))))
nil)
((perm_length formula-decl nil permutations_fseq nil)
(permutation? const-decl "bool" permutations_fseq nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(bijective? const-decl "bool" functions nil)
(surjective? const-decl "bool" functions nil)
(injective? const-decl "bool" functions nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(B!1 skolem-const-decl "fsq[T]" permutations_fseq 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)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(FALSE const-decl "bool" booleans nil)
(below type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(A!1 skolem-const-decl "fsq[T]" permutations_fseq nil)
(bij_inv_is_bij formula-decl nil function_inverse nil)
(surjective_inverse formula-decl nil function_inverse nil)
(f!1 skolem-const-decl "[below(length(A!1)) -> below(length(B!1))]"
permutations_fseq nil)
(inverse const-decl "D" function_inverse nil)
(TRUE const-decl "bool" booleans nil)
(fsq type-eq-decl nil fsq nil)
(T formal-nonempty-type-decl nil permutations_fseq nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil))
nil))
(perm_tran 0
(perm_tran-1 nil 3506271679
("" (skosimp*)
(("" (expand "permutation?")
(("" (skosimp*)
((""
(inst 1 "(LAMBDA (ii: below(length(A1!1))): f!2(f!1(ii)))")
(("" (prop)
(("1" (expand "bijective?")
(("1" (prop)
(("1" (expand "injective?")
(("1" (skosimp*)
(("1" (inst -5 "f!1(x1!1)" "f!1(x2!1)")
(("1" (inst -2 "x1!1" "x2!1")
(("1" (assert) nil)))))))))
("2" (expand "surjective?")
(("2" (skosimp*)
(("2" (inst -5 "y!1")
(("2" (skosimp*)
(("2" (replace -5 * rl)
(("2" (inst -2 "x!1")
(("2" (skosimp*)
(("2"
(inst 1 "x!2")
(("2" (assert) nil)))))))))))))))))))))
("2" (skosimp*)
(("2" (inst?)
(("2" (inst?) (("2" (assert) nil))))))))))))))))
nil)
((permutation? const-decl "bool" permutations_fseq nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans 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)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(T formal-nonempty-type-decl nil permutations_fseq nil)
(fsq type-eq-decl nil fsq nil)
(below type-eq-decl nil naturalnumbers nil)
(bijective? const-decl "bool" functions nil)
(surjective? const-decl "bool" functions nil)
(injective? const-decl "bool" functions nil))
nil))
(perm_in? 0
(perm_in?-1 nil 3506271679
("" (skosimp*)
(("" (iff 1)
(("" (prop)
(("1" (expand "in?")
(("1" (skosimp*)
(("1" (expand "permutation?")
(("1" (skosimp*)
(("1" (inst -3 "ii!1")
(("1" (inst 1 "f!1(ii!1)")
(("1" (assert) nil)))))))))))))
("2" (expand "in?")
(("2" (skosimp*)
(("2" (lemma "perm_symmetric")
(("2" (inst -1 "A1!1" "A2!1")
(("2" (assert)
(("2" (hide -3)
(("2" (expand "permutation?")
(("2" (skosimp*)
(("2" (inst -2 "ii!1")
(("2" (inst 1 "f!1(ii!1)")
(("2" (assert)
nil))))))))))))))))))))))))))
nil)
((perm_symmetric formula-decl nil permutations_fseq nil)
(in? const-decl "bool" fsq nil)
(permutation? const-decl "bool" permutations_fseq nil)
(number nonempty-type-decl nil numbers nil)
(boolean nonempty-type-decl nil booleans 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)
(bool nonempty-type-eq-decl nil booleans nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(< const-decl "bool" reals nil)
(T formal-nonempty-type-decl nil permutations_fseq nil)
(fsq type-eq-decl nil fsq nil)
(below type-eq-decl nil naturalnumbers nil))
nil)))
¤ Dauer der Verarbeitung: 0.24 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
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 ist noch experimentell.
|
