| products/sources/formale Sprachen/PVS/algebra/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: Sprache: IsabelleOriginal von: PVS© |
|
||||||
|
(lagrange
(IMP_group_TCC1 0 (IMP_group_TCC1-1 nil 3407081425 ("" (lemma "fullset_is_group") (("" (propax) nil nil)) nil) ((fullset_is_group formula-decl nil lagrange nil)) nil)) (right_coset_finite_TCC1 0 (right_coset_finite_TCC1-1 nil 3407079606 ("" (subtype-tcc) nil nil) ((finite_group nonempty-type-eq-decl nil group nil) (finite_group? const-decl "bool" group_def nil) (set type-eq-decl nil sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (star_closed? const-decl "bool" groupoid_def nil) (one formal-const-decl "T" lagrange nil) (* formal-const-decl "[T, T -> T]" lagrange nil) (T formal-nonempty-type-decl nil lagrange nil) (one_member formula-decl nil monad nil) (right_identity formula-decl nil monad nil) (restrict const-decl "R" restrict nil) (left_identity formula-decl nil monad nil) (identity? const-decl "bool" operator_defs nil) (monad? const-decl "bool" monad_def nil) (associative? const-decl "bool" operator_defs nil) (monoid? const-decl "bool" monoid_def nil) (inv_exists? const-decl "bool" group_def nil) (group? const-decl "bool" group_def nil) (subgroup? const-decl "bool" group_def nil)) nil)) (right_coset_finite 0 (right_coset_finite-2 nil 3407079635 ("" (skosimp*) (("" (lemma "right_coset_is" ("G" "G!1" "H" "H!1" "a" "a!1")) (("" (assert) (("" (replace -1 1) (("" (hide -1) (("" (typepred "G!1") (("" (expand "finite_group?") (("" (flatten) (("" (case "subset?({x: T | congruent_mod(G!1, H!1)(a!1, x)},G!1)") (("1" (lemma "finite_subset[T]") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (expand "subset?") (("2" (skosimp*) (("2" (expand "member") (("2" (expand "congruent_mod") (("2" (expand "member") (("2" (expand "subgroup?") (("2" (flatten) (("2" (expand "subset?") (("2" (expand "member") (("2" (inst - "a!1 * inv(x!1)") (("2" (assert) (("2" (lemma "inv_in") (("2" (inst - "G!1" "a!1") (("2" (lemma "star_closed") (("2" (inst - "G!1" "inv(a!1)" "a!1 * inv(x!1)") (("2" (rewrite "assoc") (("2" (rewrite "inv_left") (("2" (rewrite "one_left") (("2" (lemma "inv_member") (("2" (inst?) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((one formal-const-decl "T" lagrange nil) (* formal-const-decl "[T, T -> T]" lagrange nil) (T formal-nonempty-type-decl nil lagrange nil) (finite_group nonempty-type-eq-decl nil group nil) (finite_group? const-decl "bool" group_def nil) (group nonempty-type-eq-decl nil group nil) (group? const-decl "bool" group_def nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (right_coset_is formula-decl nil cosets nil) (NOT const-decl "[bool -> bool]" booleans nil) (inv const-decl "{y | x * y = one AND y * x = one}" group nil) (= const-decl "[T, T -> boolean]" equalities nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (inv_in formula-decl nil group nil) (star_closed formula-decl nil groupoid nil) (assoc formula-decl nil group nil) (inv_left formula-decl nil group nil) (left_identity formula-decl nil monad nil) (inv_member formula-decl nil group nil) (star_closed? const-decl "bool" groupoid_def nil) (groupoid nonempty-type-eq-decl nil groupoid nil) (a!1 skolem-const-decl "T" lagrange nil) (finite_subset formula-decl nil finite_sets nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (finite_set type-eq-decl nil finite_sets nil) (G!1 skolem-const-decl "finite_group[T, *, one]" lagrange nil) (is_finite const-decl "bool" finite_sets nil) (subset? const-decl "bool" sets nil) (subgroup? const-decl "bool" group_def nil) (subgroup type-eq-decl nil group nil) (congruent_mod const-decl "bool" cosets nil) (member const-decl "bool" sets nil)) nil) (right_coset_finite-1 nil 3407079610 ("" (postpone) nil nil) nil shostak)) (finite_right_coset_correspondence_TCC1 0 (finite_right_coset_correspondence_TCC1-1 nil 3407079606 ("" (skosimp*) (("" (rewrite "right_coset_finite") nil nil)) nil) ((right_coset_finite formula-decl nil lagrange nil) (T formal-nonempty-type-decl nil lagrange nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (* formal-const-decl "[T, T -> T]" lagrange nil) (one formal-const-decl "T" lagrange nil) (finite_group? const-decl "bool" group_def nil) (finite_group nonempty-type-eq-decl nil group nil)) nil)) (finite_right_coset_correspondence_TCC2 0 (finite_right_coset_correspondence_TCC2-2 nil 3407079880 ("" (expand "member") (("" (skosimp*) nil nil)) nil) ((member const-decl "bool" sets nil)) nil) (finite_right_coset_correspondence_TCC2-1 nil 3407079606 ("" (subtype-tcc) nil nil) nil nil)) (finite_right_coset_correspondence_TCC3 0 (finite_right_coset_correspondence_TCC3-1 nil 3407079606 ("" (skosimp*) (("" (rewrite "right_coset_finite") nil nil)) nil) ((right_coset_finite formula-decl nil lagrange nil) (T formal-nonempty-type-decl nil lagrange nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (* formal-const-decl "[T, T -> T]" lagrange nil) (one formal-const-decl "T" lagrange nil) (finite_group? const-decl "bool" group_def nil) (finite_group nonempty-type-eq-decl nil group nil)) nil)) (finite_right_coset_correspondence 0 (finite_right_coset_correspondence-1 nil 3407079666 ("" (skosimp*) (("" (lemma "right_coset_finite" ("G" "G!1" "H" "H!1" "a" "a!1")) (("" (lemma "right_coset_finite" ("G" "G!1" "H" "H!1" "a" "b!1")) (("" (assert) (("" (name "A" "right_coset(G!1, H!1)(a!1)") (("" (name "B" "right_coset(G!1, H!1)(b!1)") (("" (lemma "right_coset_correspondence" ("A" "A" "B" "B" "G" "G!1" "H" "H!1" "a" "a!1" "b" "b!1")) (("" (assert) (("" (skolem!) (("" (replace -3) (("" (replace -2) (("" (case "card(A) = card(B) IFF (EXISTS (g:[(A)->(B)]): bijective?(g))") (("1" (replace -1 1) (("1" (hide -1) (("1" (inst + "f!1") nil nil)) nil)) nil) ("2" (hide 2) (("2" (prop) (("1" (inst + "f!1") nil nil) ("2" (skolem!) (("2" (lemma "card_bij" ("S" "A" "N" "card(B)")) (("2" (replace -1 1) (("2" (hide -1) (("2" (lemma "bij_exists" ("S" "B")) (("2" (skolem!) (("2" (lemma "composition_bijective[(A),(B),below[card(B)]]" ("f1" "f!1" "f2" "f!2")) (("1" (inst + "f!2 o f!1") nil nil) ("2" (propax) nil nil) ("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((finite_group nonempty-type-eq-decl nil group nil) (finite_group? const-decl "bool" group_def nil) (one formal-const-decl "T" lagrange nil) (* formal-const-decl "[T, T -> T]" lagrange 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-nonempty-type-decl nil lagrange nil) (right_coset_finite formula-decl nil lagrange nil) (member const-decl "bool" sets nil) (bijective? const-decl "bool" functions nil) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (Card const-decl "nat" finite_sets nil) (nat nonempty-type-eq-decl nil naturalnumbers 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) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (number nonempty-type-decl nil numbers nil) (IFF const-decl "[bool, bool -> bool]" booleans nil) (card_bij formula-decl nil finite_sets nil) (O const-decl "T3" function_props nil) (below type-eq-decl nil nat_types nil) (< const-decl "bool" reals nil) (below type-eq-decl nil naturalnumbers nil) (composition_bijective judgement-tcc nil function_props nil) (bij_exists formula-decl nil finite_sets nil) (right_coset_correspondence formula-decl nil cosets nil) (= const-decl "[T, T -> boolean]" equalities nil) (group nonempty-type-eq-decl nil group nil) (group? const-decl "bool" group_def nil) (subgroup? const-decl "bool" group_def nil) (subgroup type-eq-decl nil group nil) (subset? const-decl "bool" sets nil) (right_coset const-decl "{s: set[T] | subset?(s, G)}" cosets nil)) nil)) (set_right_cosets_full 0 (set_right_cosets_full-1 nil 3406313720 ("" (skosimp*) (("" (apply-extensionality 1 :hide? t) (("" (expand "Union") (("" (iff 1) (("" (prop) (("1" (skosimp*) (("1" (typepred "a!1") (("1" (expand "extend") (("1" (ground) (("1" (skosimp*) (("1" (replace -1) (("1" (hide -1) (("1" (expand "*") (("1" (skosimp*) (("1" (replace -2) (("1" (hide -2) (("1" (typepred "a!2") (("1" (typepred "h!1") (("1" (typepred "H!1") (("1" (expand "subgroup?") (("1" (expand "subset?") (("1" (inst?) (("1" (expand "member") (("1" (rewrite "star_closed") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst + "H!1*x!1") (("1" (expand "*") (("1" (inst + "one") (("1" (rewrite "one_left") nil nil) ("2" (rewrite "one_in") nil nil)) nil)) nil) ("2" (expand "extend") (("2" (expand "fullset") (("2" (ground) (("2" (inst + "x!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T formal-nonempty-type-decl nil lagrange nil) (boolean nonempty-type-decl nil booleans nil) (fullset const-decl "set" sets nil) (extend const-decl "R" extend nil) (FALSE const-decl "bool" booleans nil) (right_cosets type-eq-decl nil cosets nil) (subgroup type-eq-decl nil group nil) (subgroup? const-decl "bool" group_def nil) (* const-decl "set[T]" cosets nil) (= const-decl "[T, T -> boolean]" equalities nil) (group nonempty-type-eq-decl nil group nil) (group? const-decl "bool" group_def nil) (one formal-const-decl "T" lagrange nil) (* formal-const-decl "[T, T -> T]" lagrange nil) (Union const-decl "set" sets nil) (set type-eq-decl nil sets nil) (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (Union_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas nil) (x!1 skolem-const-decl "T" lagrange nil) (H!1 skolem-const-decl "subgroup[T, *, one](G!1)" lagrange nil) (G!1 skolem-const-decl "group[T, *, one]" lagrange nil) (one_left formula-decl nil group nil) (one_in formula-decl nil monad nil) (monad? const-decl "bool" monad_def nil) (monad nonempty-type-eq-decl nil monad nil) (groupoid nonempty-type-eq-decl nil groupoid nil) (star_closed? const-decl "bool" groupoid_def nil) (star_closed formula-decl nil groupoid nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil)) shostak)) (right_cosets_disjoint 0 (right_cosets_disjoint-2 nil 3406394811 ("" (skosimp*) (("" (expand "disjoint?") (("" (expand "empty?") (("" (assert) (("" (expand "intersection") (("" (assert) (("" (skosimp*) (("" (typepred "B!1") (("" (typepred "A!1") (("" (skosimp*) (("" (replace -1) (("" (hide -1) (("" (replace -1) (("" (hide -1) (("" (expand "*") (("" (apply-extensionality 1 :hide? t) (("" (iff 1) (("" (skosimp*) (("" (prop) (("1" (skosimp*) (("1" (inst + "h!3*inv(h!1)*h!2") (("1" (case-replace "inv(h!1)*x!1 = a!1") (("1" (assert) (("1" (replace -4 -1) (("1" (rewrite "assoc" -1) (("1" (rewrite "associative" 1) (("1" (rewrite "associative" 1) (("1" (replace -1) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide -1 -3) (("2" (lemma "cancel_left") (("2" (inst?) (("2" (inst - "h!1*a!1") (("2" (flatten) (("2" (hide -1) (("2" (split -1) (("1" (rewrite "assoc" -1) (("1" (rewrite "inv_left") (("1" (rewrite "one_left") nil nil)) nil)) nil) ("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "star_closed") (("2" (rewrite "star_closed") (("2" (rewrite "inv_in") nil nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (inst + "h!3*inv(h!2)*h!1") (("1" (replace -1) (("1" (hide -1) (("1" (lemma "divby") (("1" (inst - "x!1" "h!2" "a!2") (("1" (assert) (("1" (hide -3) (("1" (replace -2) (("1" (hide -2) (("1" (rewrite "associative" :dir rl) (("1" (rewrite "associative") (("1" (rewrite "associative") (("1" (rewrite "associative") (("1" (rewrite "associative") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "star_closed") (("2" (rewrite "star_closed") (("2" (rewrite "inv_in") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((disjoint? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (right_cosets type-eq-decl nil cosets nil) (subgroup type-eq-decl nil group nil) (subgroup? const-decl "bool" group_def nil) (* const-decl "set[T]" cosets nil) (= const-decl "[T, T -> boolean]" equalities nil) (group nonempty-type-eq-decl nil group nil) (group? const-decl "bool" group_def nil) (one formal-const-decl "T" lagrange nil) (* formal-const-decl "[T, T -> T]" lagrange nil) (set type-eq-decl nil sets nil) (T formal-nonempty-type-decl nil lagrange nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (divby formula-decl nil group nil) (h!3 skolem-const-decl "(H!1)" lagrange nil) (groupoid nonempty-type-eq-decl nil groupoid nil) (star_closed? const-decl "bool" groupoid_def nil) (star_closed formula-decl nil groupoid nil) (inv_in formula-decl nil group nil) (associative formula-decl nil semigroup nil) (assoc formula-decl nil group nil) (inv_left formula-decl nil group nil) (left_identity formula-decl nil monad nil) (cancel_left formula-decl nil group nil) (G!1 skolem-const-decl "group[T, *, one]" lagrange nil) (H!1 skolem-const-decl "subgroup[T, *, one](G!1)" lagrange nil) (h!3 skolem-const-decl "(H!1)" lagrange nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (inv const-decl "{y | x * y = one AND y * x = one}" group nil) (h!1 skolem-const-decl "(H!1)" lagrange nil) (h!2 skolem-const-decl "(H!1)" lagrange nil) (intersection const-decl "set" sets nil) (empty? const-decl "bool" sets nil)) nil) (right_cosets_disjoint-1 nil 3406392205 ("" (skosimp*) (("" (expand "disjoint?") (("" (expand "empty?") (("" (assert) (("" (expand "intersection") (("" (assert) (("" (skosimp*) (("" (typepred "B!1") (("" (typepred "A!1") (("" (skosimp*) (("" (lemma "right_coset_def") (("" (inst - "G!1" "H!1" "_") (("" (assert) (("" (inst-cp - "a!1") (("" (inst - "a!2") (("" (assert) (("" (replace -1 :dir rl) (("" (replace -2 :dir rl) (("" (hide -1 -2) (("" (rewrite "right_coset_is") (("" (rewrite "right_coset_is") (("" (replace -1) (("" (hide -1) (("" (replace -1) (("" (hide -1) (("" (apply-extensionality 1 :hide? t) (("" (expand "congruent_mod") (("" (assert) (("" (iff 1) (("" (prop) (("1" (postpone) nil nil) ("2" (postpone) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) nil shostak)) (right_cosets_partition 0 (right_cosets_partition-1 nil 3406386334 ("" (skosimp*) (("" (expand "finite_partition?") (("" (lemma "set_right_cosets_full") (("" (inst - "G!1" "H!1") (("" (typepred "G!1") (("" (prop) (("1" (expand "partition?") (("1" (skosimp*) (("1" (lemma "right_cosets_disjoint") (("1" (inst - "G!1" "H!1" "a!1" "b!1") (("1" (typepred "b!1") (("1" (expand "extend") (("1" (ground) nil nil)) nil)) nil) ("2" (typepred "a!1") (("2" (expand "extend") (("2" (ground) (("2" (skosimp*) (("2" (assert) (("2" (typepred "b!1") (("2" (expand "extend") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (typepred "a!1") (("3" (expand "extend") (("3" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "Union_finite[T]") (("2" (inst?) (("2" (assert) (("2" (hide 2) (("2" (replace -2) (("2" (expand "finite_group?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "every") (("3" (skosimp*) (("3" (typepred "x!1") (("3" (expand "extend") (("3" (ground) (("3" (skosimp*) (("3" (replace -1) (("3" (hide -1) (("3" (lemma "right_coset_finite") (("3" (inst - "G!1" "H!1" "a!1") (("1" (assert) (("1" (expand "right_coset") (("1" (propax) nil nil)) nil)) nil) ("2" (lemma "finite_subgroups") (("2" (assert) (("2" (typepred "H!1") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((finite_partition? const-decl "bool" lagrange_scaf nil) (T formal-nonempty-type-decl nil lagrange nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (* formal-const-decl "[T, T -> T]" lagrange nil) (one formal-const-decl "T" lagrange nil) (group? const-decl "bool" group_def nil) (group nonempty-type-eq-decl nil group nil) (finite_group? const-decl "bool" group_def nil) (finite_group nonempty-type-eq-decl nil group nil) (subgroup? const-decl "bool" group_def nil) (subgroup type-eq-decl nil group nil) (a!1 skolem-const-decl "(extend[setof[T], right_cosets[T, *, one](G!1, H!1), bool, FALSE] (fullset[right_cosets[T, *, one](G!1, H!1)]))" lagrange nil) (fullset const-decl "set" sets nil) (extend const-decl "R" extend nil) (FALSE const-decl "bool" booleans nil) (right_cosets type-eq-decl nil cosets nil) (H!1 skolem-const-decl "subgroup[T, *, one](G!1)" lagrange nil) (* const-decl "set[T]" cosets nil) (setof type-eq-decl nil defined_types nil) (= const-decl "[T, T -> boolean]" equalities nil) (G!1 skolem-const-decl "finite_group[T, *, one]" lagrange nil) (b!1 skolem-const-decl "(extend[setof[T], right_cosets[T, *, one](G!1, H!1), bool, FALSE] (fullset[right_cosets[T, *, one](G!1, H!1)]))" lagrange nil) (Union_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas nil) (right_cosets_disjoint formula-decl nil lagrange nil) (partition? const-decl "bool" lagrange_scaf nil) (setofsets type-eq-decl nil sets nil) (Union_finite formula-decl nil finite_sets_of_sets nil) (right_coset const-decl "{s: set[T] | subset?(s, G)}" cosets nil) (member const-decl "bool" sets nil) (finite_subgroups formula-decl nil group nil) (right_coset_finite formula-decl nil lagrange nil) (every const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (set_right_cosets_full formula-decl nil lagrange nil)) shostak)) (Lagrange 0 (Lagrange-1 nil 3406312742 ("" (skosimp*) (("" (lemma "set_right_cosets_full") (("" (inst - "G!1" "H!1") (("" (lemma "card_eq_part[T]") (("" (inst?) (("1" (assert) (("1" (inst - "H!1") (("1" (split -1) (("1" (replace -2) (("1" (expand "order") (("1" (expand "divides") (("1" (inst + "card(extend[setof[T], right_cosets(G!1, H!1), bool, FALSE] (fullset[right_cosets(G!1, H!1)]))") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (skosimp*) (("2" (lemma "finite_right_coset_correspondence") (("2" (inst?) (("2" (typepred "A!1") (("2" (expand "extend") (("2" (ground) (("2" (skosimp*) (("2" (typepred "B!1") (("2" (expand "extend") (("2" (ground) (("2" (skosimp*) (("2" (inst -5 "a!1" "a!2") (("2" (assert) (("2" (expand "fullset") (("2" (expand "right_coset") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp*) (("3" (hide 3) (("3" (lemma "right_cosets_disjoint") (("3" (inst - "G!1" "H!1" "A!1" "B!1") (("1" (assert) nil nil) ("2" (typepred "B!1") (("2" (typepred "A!1") (("2" (expand "extend") (("2" (ground) nil nil)) nil)) nil)) nil) ("3" (typepred "A!1") (("3" (expand "extend") (("3" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (hide 2) (("4" (expand "extend") (("4" (ground) (("1" (skosimp*) (("1" (replace -1) (("1" (hide -1) (("1" (expand "fullset") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (inst + "one") (("1" (rewrite "right_coset_one") nil nil) ("2" (rewrite "one_in") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (lemma "right_cosets_partition") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((set_right_cosets_full formula-decl nil lagrange nil) (card_eq_part formula-decl nil lagrange_scaf nil) (right_cosets_partition formula-decl nil lagrange nil) (Union_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas nil) (order const-decl "posnat" monad 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) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (Card const-decl "nat" finite_sets nil) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (divides const-decl "bool" divides nil) (right_coset const-decl "{s: set[T] | subset?(s, G)}" cosets nil) (member const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (finite_right_coset_correspondence formula-decl nil lagrange nil) (A!1 skolem-const-decl "(extend[setof[T], right_cosets[T, *, one](G!1, H!1), bool, FALSE] (fullset[right_cosets[T, *, one](G!1, H!1)]))" lagrange nil) (B!1 skolem-const-decl "(extend[setof[T], right_cosets[T, *, one](G!1, H!1), bool, FALSE] (fullset[right_cosets[T, *, one](G!1, H!1)]))" lagrange nil) (right_cosets_disjoint formula-decl nil lagrange nil) (right_coset_one formula-decl nil cosets nil) (one_in formula-decl nil monad nil) (monad? const-decl "bool" monad_def nil) (monad nonempty-type-eq-decl nil monad nil) (finite_partition type-eq-decl nil lagrange_scaf nil) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (finite_partition? const-decl "bool" lagrange_scaf nil) (= const-decl "[T, T -> boolean]" equalities nil) (* const-decl "set[T]" cosets nil) (right_cosets type-eq-decl nil cosets nil) (FALSE const-decl "bool" booleans nil) (extend const-decl "R" extend nil) (fullset const-decl "set" sets nil) (subgroup type-eq-decl nil group nil) (group nonempty-type-eq-decl nil group nil) (T formal-nonempty-type-decl nil lagrange nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (* formal-const-decl "[T, T -> T]" lagrange nil) (one formal-const-decl "T" lagrange nil) (group? const-decl "bool" group_def nil) (subgroup? const-decl "bool" group_def nil) (finite_group? const-decl "bool" group_def nil) (finite_group nonempty-type-eq-decl nil group nil) (H!1 skolem-const-decl "finite_group[T, *, one]" lagrange nil) (G!1 skolem-const-decl "finite_group[T, *, one]" lagrange nil)) shostak))) ¤ Dauer der Verarbeitung: 0.116 Sekunden (vorverarbeitet) ¤ |
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
