| products/sources/formale sprachen/PVS/groups/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: right_left_cosets.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(right_left_cosets
(IMP_lagrange_TCC1 0 (IMP_lagrange_TCC1-1 nil 3530611400 ("" (rewrite "fullset_is_group") nil nil) ((fullset_is_group formula-decl nil right_left_cosets nil)) nil)) (nonempty_left_coset_TCC1 0 (nonempty_left_coset_TCC1-1 nil 3528677081 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (T formal-type-decl nil right_left_cosets nil) (set type-eq-decl nil sets nil) (* formal-const-decl "[T, T -> T]" right_left_cosets nil) (one formal-const-decl "T" right_left_cosets nil) (group? const-decl "bool" group_def "algebra/") (group nonempty-type-eq-decl nil group "algebra/") (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (subgroup? const-decl "bool" group_def "algebra/")) nil)) (nonempty_left_coset 0 (nonempty_left_coset-1 nil 3528677207 ("" (skosimp*) (("" (expand "left_coset") (("" (expand "member") (("" (expand "nonempty?") (("" (expand "empty?") (("" (expand "member") (("" (expand "*") (("" (inst - "a!1") (("" (inst + "one") (("1" (rewrite "one_right") nil nil) ("2" (rewrite "one_in") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((left_coset const-decl "{s: set[T] | subset?(s, G)}" cosets "algebra/") (nonempty? const-decl "bool" sets nil) (T formal-type-decl nil right_left_cosets nil) (monad nonempty-type-eq-decl nil monad "algebra/") (monad? const-decl "bool" monad_def "algebra/") (one_in formula-decl nil monad "algebra/") (one_right formula-decl nil group "algebra/") (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]" right_left_cosets nil) (one formal-const-decl "T" right_left_cosets nil) (group? const-decl "bool" group_def "algebra/") (group nonempty-type-eq-decl nil group "algebra/") (H!1 skolem-const-decl "group[T, *, one]" right_left_cosets nil) (* const-decl "set[T]" cosets "algebra/") (empty? const-decl "bool" sets nil) (member const-decl "bool" sets nil)) shostak)) (left_coset_finite_TCC1 0 (left_coset_finite_TCC1-1 nil 3528677081 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (T formal-type-decl nil right_left_cosets nil) (set type-eq-decl nil sets nil) (* formal-const-decl "[T, T -> T]" right_left_cosets nil) (one formal-const-decl "T" right_left_cosets nil) (group? const-decl "bool" group_def "algebra/") (group nonempty-type-eq-decl nil group "algebra/") (finite_group? const-decl "bool" group_def "algebra/") (finite_group nonempty-type-eq-decl nil group "algebra/") (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (subgroup? const-decl "bool" group_def "algebra/")) nil)) (left_coset_finite 0 (left_coset_finite-1 nil 3528677376 ("" (skosimp) (("" (assert) (("" (typepred "G!1") (("" (expand "finite_group?") (("" (flatten) (("" (expand "left_coset") (("" (lemma "left_coset_subset") (("" (inst -1 "G!1" "H!1" "a!1") (("" (lemma "finite_subset[T]") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((member const-decl "bool" sets nil) (left_coset const-decl "{s: set[T] | subset?(s, G)}" cosets "algebra/") (group? const-decl "bool" group_def "algebra/") (group nonempty-type-eq-decl nil group "algebra/") (subgroup? const-decl "bool" group_def "algebra/") (subgroup type-eq-decl nil group "algebra/") (is_finite const-decl "bool" finite_sets nil) (G!1 skolem-const-decl "finite_group[T, *, one]" right_left_cosets nil) (* const-decl "set[T]" cosets "algebra/") (finite_set type-eq-decl nil finite_sets nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (finite_subset formula-decl nil finite_sets nil) (left_coset_subset formula-decl nil cosets "algebra/") (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (T formal-type-decl nil right_left_cosets nil) (set type-eq-decl nil sets nil) (* formal-const-decl "[T, T -> T]" right_left_cosets nil) (one formal-const-decl "T" right_left_cosets nil) (finite_group? const-decl "bool" group_def "algebra/") (finite_group nonempty-type-eq-decl nil group "algebra/")) shostak)) (left_coset_correspondence 0 (left_coset_correspondence-1 nil 3528677400 ("" (skosimp*) (("" (typepred "G!1") (("" (expand "subgroup?") (("" (assert) (("" (inst + "LAMBDA (x:(H!1)): a!1*x") (("1" (expand "bijective?") (("1" (split) (("1" (expand "injective?") (("1" (skosimp*) (("1" (rewrite "cancel_left") nil nil)) nil)) nil) ("2" (expand "surjective?") (("2" (skosimp*) (("2" (typepred "y!1") (("2" (replaces -5) (("2" (expand "left_coset") (("2" (expand "*") (("2" (skosimp) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (replaces -4) (("2" (expand "left_coset") (("2" (expand "*") (("2" (inst 1 "x!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((group nonempty-type-eq-decl nil group "algebra/") (group? const-decl "bool" group_def "algebra/") (one formal-const-decl "T" right_left_cosets nil) (* formal-const-decl "[T, T -> T]" right_left_cosets nil) (set type-eq-decl nil sets nil) (T formal-type-decl nil right_left_cosets nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (member const-decl "bool" sets nil) (bijective? const-decl "bool" functions nil) (surjective? const-decl "bool" functions nil) (left_coset const-decl "{s: set[T] | subset?(s, G)}" cosets "algebra/") (* const-decl "set[T]" cosets "algebra/") (injective? const-decl "bool" functions nil) (cancel_left formula-decl nil group "algebra/") (a!1 skolem-const-decl "T" right_left_cosets nil) (A!1 skolem-const-decl "set[T]" right_left_cosets nil) (H!1 skolem-const-decl "group[T, *, one]" right_left_cosets nil) (subgroup? const-decl "bool" group_def "algebra/")) shostak)) (left_coset_correspondence_inv 0 (left_coset_correspondence_inv-1 nil 3530284707 ("" (skosimp*) (("" (typepred "G!1") (("" (expand "subgroup?") (("" (assert) (("" (inst + "LAMBDA (x:(H!1)): a!1*x*inv(a!1)") (("1" (expand "bijective?") (("1" (split) (("1" (expand "injective?") (("1" (skosimp*) (("1" (rewrite "cancel_right") (("1" (rewrite "cancel_left") nil nil)) nil)) nil)) nil) ("2" (expand "surjective?") (("2" (skosimp*) (("2" (typepred "y!1") (("2" (hide (-2 -3 -4)) (("2" (expand "*") (("2" (skosimp) (("2" (inst 1 "inv(a!1)*h!1") (("1" (replaces -1) (("1" (rewrite "assoc") nil nil)) nil) ("2" (typepred "h!1") (("2" (skosimp) (("2" (replaces -1) (("2" (typepred "h!2") (("2" (rewrite "assoc") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "*" 1 1) (("2" (typepred "x!1") (("2" (inst?) (("2" (expand "*" 1 1) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((group nonempty-type-eq-decl nil group "algebra/") (group? const-decl "bool" group_def "algebra/") (one formal-const-decl "T" right_left_cosets nil) (* formal-const-decl "[T, T -> T]" right_left_cosets nil) (set type-eq-decl nil sets nil) (T formal-type-decl nil right_left_cosets nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (member const-decl "bool" sets nil) (x!1 skolem-const-decl "(H!1)" right_left_cosets nil) (bijective? const-decl "bool" functions nil) (surjective? const-decl "bool" functions nil) (h!1 skolem-const-decl "({t: T | EXISTS (h: (H!1)): t = a!1 * h})" right_left_cosets nil) (one_left formula-decl nil group "algebra/") (inv_right formula-decl nil group "algebra/") (assoc formula-decl nil group "algebra/") (inv_left formula-decl nil group "algebra/") (injective? const-decl "bool" functions nil) (cancel_right formula-decl nil group "algebra/") (cancel_left formula-decl nil group "algebra/") (H!1 skolem-const-decl "group[T, *, one]" right_left_cosets nil) (* const-decl "set[T]" cosets "algebra/") (* const-decl "set[T]" cosets "algebra/") (a!1 skolem-const-decl "T" right_left_cosets nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (inv const-decl "{y | x * y = one AND y * x = one}" group "algebra/") (subgroup? const-decl "bool" group_def "algebra/")) shostak)) (finite_left_coset_correspondence_TCC1 0 (finite_left_coset_correspondence_TCC1-1 nil 3528677081 ("" (skosimp) (("" (assert) (("" (lemma "left_coset_finite") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((member const-decl "bool" sets nil) (T formal-type-decl nil right_left_cosets 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]" right_left_cosets nil) (one formal-const-decl "T" right_left_cosets nil) (group? const-decl "bool" group_def "algebra/") (group nonempty-type-eq-decl nil group "algebra/") (finite_group? const-decl "bool" group_def "algebra/") (finite_group nonempty-type-eq-decl nil group "algebra/") (left_coset_finite formula-decl nil right_left_cosets nil)) nil)) (finite_left_coset_correspondence_TCC2 0 (finite_left_coset_correspondence_TCC2-1 nil 3528677081 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (T formal-type-decl nil right_left_cosets nil) (set type-eq-decl nil sets nil) (* formal-const-decl "[T, T -> T]" right_left_cosets nil) (one formal-const-decl "T" right_left_cosets nil) (group? const-decl "bool" group_def "algebra/") (group nonempty-type-eq-decl nil group "algebra/") (finite_group? const-decl "bool" group_def "algebra/") (finite_group nonempty-type-eq-decl nil group "algebra/") (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (subgroup? const-decl "bool" group_def "algebra/")) nil)) (finite_left_coset_correspondence_TCC3 0 (finite_left_coset_correspondence_TCC3-1 nil 3528677081 ("" (skosimp) (("" (lemma "left_coset_finite") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil) ((left_coset_finite formula-decl nil right_left_cosets nil) (member const-decl "bool" sets nil) (finite_group nonempty-type-eq-decl nil group "algebra/") (finite_group? const-decl "bool" group_def "algebra/") (group nonempty-type-eq-decl nil group "algebra/") (group? const-decl "bool" group_def "algebra/") (one formal-const-decl "T" right_left_cosets nil) (* formal-const-decl "[T, T -> T]" right_left_cosets 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 right_left_cosets nil)) nil)) (finite_left_coset_correspondence 0 (finite_left_coset_correspondence-1 nil 3528677432 ("" (skosimp) (("" (assert) (("" (name-replace "A" "left_coset(G!1, H!1)(a!1)" :hide? nil) (("" (name-replace "B" "left_coset(G!1, H!1)(b!1)" :hide? nil) (("" (lemma "card_eq_bij[T,T]") (("" (inst?) (("" (assert) (("" (hide (-4 -5 2)) (("" (lemma "left_coset_correspondence") (("" (inst -1 "G!1" "H!1" "a!1" "A") (("" (lemma "left_coset_correspondence") (("" (inst -1 "G!1" "H!1" "b!1" "B") (("" (assert) (("" (skosimp*) (("" (lemma "bijective_inverse_exists[(H!1), (A)]") (("" (inst -1 "f!2") (("" (expand "exists1") (("" (flatten) (("" (hide -2) (("" (skolem * "f!3") (("" (inst 1 "f!1 o f!3") (("" (lemma "bij_inv_is_bij_alt[(H!1), (A)]") (("" (inst -1 "f!2" "f!3") (("" (hide-all-but (-1 -3 1)) (("" (lemma "composition_bijective[(A), (H!1), (B)]") (("" (inst?) (("" (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) ((member const-decl "bool" sets nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (H!1 skolem-const-decl "group[T, *, one]" right_left_cosets nil) (G!1 skolem-const-decl "finite_group[T, *, one]" right_left_cosets nil) (A skolem-const-decl "{s: set[T] | subset?(s, G!1)}" right_left_cosets nil) (bijective? const-decl "bool" functions nil) (f!2 skolem-const-decl "[(H!1) -> (A)]" right_left_cosets nil) (bij_inv_is_bij_alt formula-decl nil function_inverse_def nil) (composition_bijective formula-decl nil func_composition "finite_sets/") (f!3 skolem-const-decl "[(A) -> (H!1)]" right_left_cosets nil) (inverse? const-decl "bool" function_inverse_def nil) (O const-decl "T3" function_props nil) (exists1 const-decl "bool" exists1 nil) (bijective_inverse_exists formula-decl nil function_inverse_def nil) (left_coset_correspondence formula-decl nil right_left_cosets nil) (card_eq_bij formula-decl nil finite_sets_card_eq "finite_sets/") (finite_group nonempty-type-eq-decl nil group "algebra/") (finite_group? const-decl "bool" group_def "algebra/") (left_coset const-decl "{s: set[T] | subset?(s, G)}" cosets "algebra/") (subset? const-decl "bool" sets nil) (subgroup type-eq-decl nil group "algebra/") (subgroup? const-decl "bool" group_def "algebra/") (group? const-decl "bool" group_def "algebra/") (group nonempty-type-eq-decl nil group "algebra/") (one formal-const-decl "T" right_left_cosets nil) (* formal-const-decl "[T, T -> T]" right_left_cosets nil) (= const-decl "[T, T -> boolean]" equalities 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 right_left_cosets nil)) shostak)) (set_left_cosets_full 0 (set_left_cosets_full-1 nil 3528677586 ("" (skosimp*) (("" (apply-extensionality 1 :hide? t) (("" (expand "Union") (("" (iff 1) (("" (prop) (("1" (skosimp*) (("1" (typepred "a!1") (("1" (expand "left_cosets") (("1" (skosimp*) (("1" (replace -1) (("1" (hide -1) (("1" (expand "*") (("1" (skosimp*) (("1" (replace -1) (("1" (hide -1) (("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) ("2" (inst + "x!1*H!1") (("1" (expand "*") (("1" (inst + "one") (("1" (rewrite "one_right") nil nil) ("2" (rewrite "one_in") nil nil)) nil)) nil) ("2" (expand "left_cosets") (("2" (inst + "x!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T formal-type-decl nil right_left_cosets nil) (boolean nonempty-type-decl nil booleans nil) (left_cosets const-decl "setofsets[T]" right_left_cosets nil) (subgroup type-eq-decl nil group "algebra/") (subgroup? const-decl "bool" group_def "algebra/") (group? const-decl "bool" group_def "algebra/") (group nonempty-type-eq-decl nil group "algebra/") (one formal-const-decl "T" right_left_cosets nil) (* formal-const-decl "[T, T -> T]" right_left_cosets 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" right_left_cosets nil) (H!1 skolem-const-decl "subgroup[T, *, one](G!1)" right_left_cosets nil) (G!1 skolem-const-decl "group[T, *, one]" right_left_cosets nil) (one_right formula-decl nil group "algebra/") (one_in formula-decl nil monad "algebra/") (monad? const-decl "bool" monad_def "algebra/") (monad nonempty-type-eq-decl nil monad "algebra/") (* const-decl "set[T]" cosets "algebra/") (subset? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (star_closed formula-decl nil groupoid "algebra/") (star_closed? const-decl "bool" groupoid_def "algebra/") (groupoid nonempty-type-eq-decl nil groupoid "algebra/") (NOT const-decl "[bool -> bool]" booleans nil)) shostak)) (left_cosets_disjoint 0 (left_cosets_disjoint-1 nil 3528677536 ("" (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!2*inv(h!1)*h!3") (("1" (case-replace "x!1*inv(h!1) = a!1") (("1" (assert) (("1" (replace -4 -1) (("1" (rewrite "assoc" -1 :dir rl) (("1" (rewrite "associative" 1 :dir rl) (("1" (replace -1) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (hide -1 -3) (("2" (replaces -1) (("2" (rewrite "assoc" :dir rl) 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!1*inv(h!2)*h!3") (("1" (replace -1) (("1" (hide -1) (("1" (rewrite "assoc") (("1" (rewrite "assoc") (("1" (replace -1 1 rl) (("1" (case-replace "x!1*inv(h!2) = a!2") (("1" (hide -1 2) (("1" (replaces -1) (("1" (rewrite "associative" 1) 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) (left_cosets type-eq-decl nil cosets "algebra/") (subgroup type-eq-decl nil group "algebra/") (subgroup? const-decl "bool" group_def "algebra/") (* const-decl "set[T]" cosets "algebra/") (= const-decl "[T, T -> boolean]" equalities nil) (group nonempty-type-eq-decl nil group "algebra/") (group? const-decl "bool" group_def "algebra/") (one formal-const-decl "T" right_left_cosets nil) (* formal-const-decl "[T, T -> T]" right_left_cosets nil) (set type-eq-decl nil sets nil) (T formal-type-decl nil right_left_cosets nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (h!3 skolem-const-decl "(H!1)" right_left_cosets nil) (groupoid nonempty-type-eq-decl nil groupoid "algebra/") (star_closed? const-decl "bool" groupoid_def "algebra/") (star_closed formula-decl nil groupoid "algebra/") (inv_in formula-decl nil group "algebra/") (associative formula-decl nil semigroup "algebra/") (assoc formula-decl nil group "algebra/") (one_right formula-decl nil group "algebra/") (inv_right formula-decl nil group "algebra/") (G!1 skolem-const-decl "group[T, *, one]" right_left_cosets nil) (H!1 skolem-const-decl "subgroup[T, *, one](G!1)" right_left_cosets nil) (h!2 skolem-const-decl "(H!1)" right_left_cosets nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (inv const-decl "{y | x * y = one AND y * x = one}" group "algebra/") (h!1 skolem-const-decl "(H!1)" right_left_cosets nil) (h!3 skolem-const-decl "(H!1)" right_left_cosets nil) (intersection const-decl "set" sets nil) (empty? const-decl "bool" sets nil)) shostak)) (left_cosets_partition 0 (left_cosets_partition-1 nil 3528677626 ("" (skosimp*) (("" (expand "finite_partition?") (("" (lemma "set_left_cosets_full") (("" (inst - "G!1" "H!1") (("" (typepred "G!1") (("" (prop) (("1" (expand "partition?") (("1" (skosimp*) (("1" (lemma "left_cosets_disjoint") (("1" (inst - "G!1" "H!1" "a!1" "b!1") (("1" (assert) nil nil) ("2" (typepred "b!1") (("2" (expand "left_cosets") (("2" (propax) nil nil)) nil)) nil) ("3" (typepred "a!1") (("3" (expand "left_cosets") (("3" (propax) 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 "left_cosets") (("3" (skosimp*) (("3" (replace -1) (("3" (lemma "left_coset_finite") (("3" (inst -1 "H!1" "a!1" "G!1") (("3" (assert) (("3" (expand "left_coset") (("3" (propax) 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 "algebra/") (T formal-type-decl nil right_left_cosets 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]" right_left_cosets nil) (one formal-const-decl "T" right_left_cosets nil) (group? const-decl "bool" group_def "algebra/") (group nonempty-type-eq-decl nil group "algebra/") (finite_group? const-decl "bool" group_def "algebra/") (finite_group nonempty-type-eq-decl nil group "algebra/") (subgroup? const-decl "bool" group_def "algebra/") (subgroup type-eq-decl nil group "algebra/") (* const-decl "set[T]" cosets "algebra/") (a!1 skolem-const-decl "(left_cosets(G!1, H!1))" right_left_cosets nil) (H!1 skolem-const-decl "subgroup[T, *, one](G!1)" right_left_cosets nil) (left_cosets const-decl "setofsets[T]" right_left_cosets nil) (setofsets type-eq-decl nil sets 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]" right_left_cosets nil) (b!1 skolem-const-decl "(left_cosets(G!1, H!1))" right_left_cosets nil) (left_cosets type-eq-decl nil cosets "algebra/") (Union_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas nil) (left_cosets_disjoint formula-decl nil right_left_cosets nil) (partition? const-decl "bool" lagrange_scaf "algebra/") (Union_finite formula-decl nil finite_sets_of_sets nil) (left_coset const-decl "{s: set[T] | subset?(s, G)}" cosets "algebra/") (member const-decl "bool" sets nil) (left_coset_finite formula-decl nil right_left_cosets nil) (every const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (set_left_cosets_full formula-decl nil right_left_cosets nil)) shostak)) (set_right_cosets_full_1 0 (set_right_cosets_full_1-1 nil 3528677991 ("" (skosimp*) (("" (apply-extensionality 1 :hide? t) (("" (expand "Union") (("" (iff 1) (("" (prop) (("1" (skosimp*) (("1" (typepred "a!1") (("1" (expand "right_cosets") (("1" (skosimp*) (("1" (replaces -1) (("1" (expand "*") (("1" (skosimp*) (("1" (replaces -2) (("1" (replaces -1) (("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) ("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 "right_cosets") (("2" (inst + "x!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((T formal-type-decl nil right_left_cosets nil) (boolean nonempty-type-decl nil booleans nil) (right_cosets const-decl "setofsets[T]" right_left_cosets nil) (subgroup type-eq-decl nil group "algebra/") (subgroup? const-decl "bool" group_def "algebra/") (group? const-decl "bool" group_def "algebra/") (group nonempty-type-eq-decl nil group "algebra/") (one formal-const-decl "T" right_left_cosets nil) (* formal-const-decl "[T, T -> T]" right_left_cosets 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" right_left_cosets nil) (H!1 skolem-const-decl "subgroup[T, *, one](G!1)" right_left_cosets nil) (G!1 skolem-const-decl "group[T, *, one]" right_left_cosets nil) (one_left formula-decl nil group "algebra/") (one_in formula-decl nil monad "algebra/") (monad? const-decl "bool" monad_def "algebra/") (monad nonempty-type-eq-decl nil monad "algebra/") (subset? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (star_closed formula-decl nil groupoid "algebra/") (star_closed? const-decl "bool" groupoid_def "algebra/") (groupoid nonempty-type-eq-decl nil groupoid "algebra/") (* const-decl "set[T]" cosets "algebra/") (NOT const-decl "[bool -> bool]" booleans nil)) shostak)) (right_left_correspondence 0 (right_left_correspondence-1 nil 3528678027 ("" (skosimp*) (("" (inst 1 "(LAMBDA (A: (right_cosets(G!1,H!1))): inv(rc_gen(G!1,H!1,A)) * H!1)") (("1" (expand "bijective?") (("1" (split) (("1" (expand "injective?") (("1" (skosimp*) (("1" (typepred "x1!1" "x2!1") (("1" (lemma "lc_eq") (("1" (inst -1 "G!1" "H!1" "inv(rc_gen(G!1, H!1, x1!1))" "inv(rc_gen(G!1, H!1, x2!1))") (("1" (assert) (("1" (skosimp) (("1" (rewrite "divby") (("1" (case "rc_gen(G!1, H!1, x2!1) = h!1 * rc_gen(G!1, H!1, x1!1)") (("1" (hide (-2 -5)) (("1" (lemma "rc_is_eq") (("1" (inst -1 "G!1" "H!1" "rc_gen(G!1, H!1, x2!1)" "rc_gen(G!1, H!1, x1!1)") (("1" (prop) (("1" (assert) nil nil) ("2" (hide-all-but (-1 1)) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (replace -1 1 rl) (("2" (rewrite "assoc" :dir rl) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "surjective?") (("2" (skosimp) (("2" (typepred "y!1") (("2" (expand "left_cosets") (("2" (skosimp) (("2" (inst 1 "H!1 * inv(a!1)") (("1" (replace -1 1) (("1" (lemma "lc_is_eq") (("1" (inst -1 "G!1" "H!1" "inv(rc_gen(G!1, H!1, H!1 * inv(a!1)))" "a!1") (("1" (assert) (("1" (hide 2) (("1" (typepred "rc_gen(G!1, H!1, H!1 * inv(a!1))") (("1" (lemma "rc_eq") (("1" (inst -1 "G!1" "H!1" "inv(a!1)" "rc_gen(G!1, H!1, H!1 * inv(a!1))") (("1" (assert) (("1" (skosimp) (("1" (hide-all-but (-1 1)) (("1" (inst 1 "h!1") (("1" (lemma "inv_inv") (("1" (inst?) (("1" (name-replace "c" "rc_gen(G!1, H!1, H!1 * inv(a!1))") (("1" (replaces -2) (("1" (rewrite "inv_star") (("1" (replace -1 1 rl) (("1" (rewrite "assoc" :dir rl) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide (-1 -2 2)) (("2" (inst?) (("2" (rewrite "inv_in") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "right_cosets") (("2" (inst?) (("2" (rewrite "inv_in") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (expand "left_cosets") (("2" (inst?) (("1" (rewrite "inv_in") nil nil) ("2" (typepred "A!1") (("2" (expand "right_cosets") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (typepred "A!1") (("3" (expand "right_cosets") (("3" (propax) nil nil)) nil)) nil)) nil) ("4" (skosimp) nil nil)) nil)) nil) ((H!1 skolem-const-decl "group[T, *, one]" right_left_cosets nil) (G!1 skolem-const-decl "group[T, *, one]" right_left_cosets nil) (right_cosets const-decl "setofsets[T]" right_left_cosets nil) (setofsets type-eq-decl nil sets nil) (subgroup type-eq-decl nil group "algebra/") (subgroup? const-decl "bool" group_def "algebra/") (group? const-decl "bool" group_def "algebra/") (set type-eq-decl nil sets nil) (group nonempty-type-eq-decl nil group "algebra/") (one formal-const-decl "T" right_left_cosets nil) (* formal-const-decl "[T, T -> T]" right_left_cosets nil) (setof type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil right_left_cosets nil) (* const-decl "set[T]" cosets "algebra/") (= const-decl "[T, T -> boolean]" equalities nil) (rc_gen const-decl "{a: T | G(a) AND rc = H * a}" cosets "algebra/") (right_cosets type-eq-decl nil cosets "algebra/") (inv const-decl "{y | x * y = one AND y * x = one}" group "algebra/") (AND const-decl "[bool, bool -> bool]" booleans nil) (* const-decl "set[T]" cosets "algebra/") (left_cosets const-decl "setofsets[T]" right_left_cosets nil) (lc_eq formula-decl nil cosets "algebra/") (divby formula-decl nil group "algebra/") (inv_inv formula-decl nil group "algebra/") (inv_left formula-decl nil group "algebra/") (one_right formula-decl nil group "algebra/") (assoc formula-decl nil group "algebra/") (rc_is_eq formula-decl nil cosets "algebra/") (NOT const-decl "[bool -> bool]" booleans nil) (injective? const-decl "bool" functions nil) (a!1 skolem-const-decl "(G!1)" right_left_cosets nil) (lc_is_eq formula-decl nil cosets "algebra/") (inv_star formula-decl nil group "algebra/") (rc_eq formula-decl nil cosets "algebra/") (inv_in formula-decl nil group "algebra/") (surjective? const-decl "bool" functions nil) (bijective? const-decl "bool" functions nil) (A!1 skolem-const-decl "(right_cosets(G!1, H!1))" right_left_cosets nil)) shostak)) (finite_right_left_correspondence_TCC1 0 (finite_right_left_correspondence_TCC1-1 nil 3528677081 ("" (skosimp*) (("" (lemma "set_right_cosets_full_1") (("" (inst - "G!1" "H!1") (("" (typepred "G!1") (("" (lemma "Union_finite[T]") (("" (inst?) (("" (assert) (("" (hide 2) (("" (replace -2) (("" (expand "finite_group?") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((set_right_cosets_full_1 formula-decl nil right_left_cosets nil) (NOT const-decl "[bool -> bool]" booleans nil) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (right_cosets const-decl "setofsets[T]" right_left_cosets nil) (Union_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas nil) (Union_finite formula-decl nil finite_sets_of_sets nil) (subgroup type-eq-decl nil group "algebra/") (subgroup? const-decl "bool" group_def "algebra/") (finite_group nonempty-type-eq-decl nil group "algebra/") (finite_group? const-decl "bool" group_def "algebra/") (group nonempty-type-eq-decl nil group "algebra/") (group? const-decl "bool" group_def "algebra/") (one formal-const-decl "T" right_left_cosets nil) (* formal-const-decl "[T, T -> T]" right_left_cosets 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 right_left_cosets nil)) nil)) (finite_right_left_correspondence_TCC2 0 (finite_right_left_correspondence_TCC2-1 nil 3528677081 ("" (skosimp*) (("" (lemma "set_left_cosets_full") (("" (inst - "G!1" "H!1") (("" (typepred "G!1") (("" (lemma "Union_finite[T]") (("" (inst?) (("" (assert) (("" (hide 2) (("" (replace -2) (("" (expand "finite_group?") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((set_left_cosets_full formula-decl nil right_left_cosets nil) (NOT const-decl "[bool -> bool]" booleans nil) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (left_cosets const-decl "setofsets[T]" right_left_cosets nil) (Union_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas nil) (Union_finite formula-decl nil finite_sets_of_sets nil) (subgroup type-eq-decl nil group "algebra/") (subgroup? const-decl "bool" group_def "algebra/") (finite_group nonempty-type-eq-decl nil group "algebra/") (finite_group? const-decl "bool" group_def "algebra/") (group nonempty-type-eq-decl nil group "algebra/") (group? const-decl "bool" group_def "algebra/") (one formal-const-decl "T" right_left_cosets nil) (* formal-const-decl "[T, T -> T]" right_left_cosets 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 right_left_cosets nil)) nil)) (finite_right_left_correspondence 0 (finite_right_left_correspondence-1 nil 3528678094 ("" (skosimp) (("" (lemma "card_eq_bij[set[T], set[T]]") (("" (inst -1 "right_cosets(G!1, H!1)" "left_cosets(G!1, H!1)") (("" (assert) (("" (hide 2) (("" (lemma "right_left_correspondence") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) 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 right_left_cosets nil) (card_eq_bij formula-decl nil finite_sets_card_eq "finite_sets/") (right_left_correspondence formula-decl nil right_left_cosets nil) (left_cosets const-decl "setofsets[T]" right_left_cosets nil) (finite_group nonempty-type-eq-decl nil group "algebra/") (finite_group? const-decl "bool" group_def "algebra/") (right_cosets const-decl "setofsets[T]" right_left_cosets nil) (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (subgroup type-eq-decl nil group "algebra/") (subgroup? const-decl "bool" group_def "algebra/") (group? const-decl "bool" group_def "algebra/") (group nonempty-type-eq-decl nil group "algebra/") (one formal-const-decl "T" right_left_cosets nil) (* formal-const-decl "[T, T -> T]" right_left_cosets nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil)) shostak)) (index_TCC1 0 (index_TCC1-1 nil 3528677081 ("" (skosimp*) (("" (lemma "set_left_cosets_full") (("" (inst - "G!1" "H!1") (("" (typepred "G!1") (("" (lemma "Union_finite[T]") (("" (inst?) (("" (assert) (("" (hide 2) (("" (replace -2) (("" (expand "finite_group?") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((set_left_cosets_full formula-decl nil right_left_cosets nil) (NOT const-decl "[bool -> bool]" booleans nil) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (left_cosets const-decl "setofsets[T]" right_left_cosets nil) (Union_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas nil) (Union_finite formula-decl nil finite_sets_of_sets nil) (subgroup type-eq-decl nil group "algebra/") (subgroup? const-decl "bool" group_def "algebra/") (finite_group nonempty-type-eq-decl nil group "algebra/") (finite_group? const-decl "bool" group_def "algebra/") (group nonempty-type-eq-decl nil group "algebra/") (group? const-decl "bool" group_def "algebra/") (one formal-const-decl "T" right_left_cosets nil) (* formal-const-decl "[T, T -> T]" right_left_cosets 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 right_left_cosets nil)) nil)) (index_gt1 0 (index_gt1-1 nil 3530550237 ("" (skosimp*) (("" (expand "index") (("" (case "nonempty?(left_cosets(G!1, H!1))") (("1" (rewrite "nonempty_card") (("1" (assert) nil nil)) nil) ("2" (hide 2) (("2" (expand* "nonempty?" "empty?" "member") (("2" (inst -1 "H!1") (("2" (expand "left_cosets") (("2" (inst 1 "one") (("1" (rewrite "left_coset_one") nil nil) ("2" (rewrite "one_in") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((index const-decl "nat" right_left_cosets nil) (G!1 skolem-const-decl "finite_group[T, *, one]" right_left_cosets nil) (left_coset_one formula-decl nil cosets "algebra/") (one_in formula-decl nil monad "algebra/") (monad? const-decl "bool" monad_def "algebra/") (monad nonempty-type-eq-decl nil monad "algebra/") (member const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (nonempty_card formula-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (T formal-type-decl nil right_left_cosets nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (setof type-eq-decl nil defined_types nil) (set type-eq-decl nil sets nil) (nonempty? const-decl "bool" sets nil) (* formal-const-decl "[T, T -> T]" right_left_cosets nil) (one formal-const-decl "T" right_left_cosets nil) (group nonempty-type-eq-decl nil group "algebra/") (group? const-decl "bool" group_def "algebra/") (subgroup? const-decl "bool" group_def "algebra/") (subgroup type-eq-decl nil group "algebra/") (setofsets type-eq-decl nil sets nil) (left_cosets const-decl "setofsets[T]" right_left_cosets nil) (finite_group? const-decl "bool" group_def "algebra/") (finite_group nonempty-type-eq-decl nil group "algebra/")) shostak)) (divide_TCC1 0 (divide_TCC1-1 nil 3530434541 ("" (skosimp*) (("" (inst 1 "one") (("1" (rewrite "left_coset_one") nil nil) ("2" (rewrite "one_in") nil nil)) nil)) nil) ((G!1 skolem-const-decl "group[T, *, one]" right_left_cosets nil) (group nonempty-type-eq-decl nil group "algebra/") (group? const-decl "bool" group_def "algebra/") (one formal-const-decl "T" right_left_cosets nil) (* formal-const-decl "[T, T -> T]" right_left_cosets 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 right_left_cosets nil) (normal_subgroup type-eq-decl nil normal_subgroups "algebra/") (normal_subgroup? const-decl "boolean" normal_subgroups "algebra/") (left_coset_one formula-decl nil cosets "algebra/") (monad nonempty-type-eq-decl nil monad "algebra/") (monad? const-decl "bool" monad_def "algebra/") (one_in formula-decl nil monad "algebra/")) nil)) (divide_TCC2 0 (divide_TCC2-1 nil 3530434541 ("" (skosimp*) (("" (rewrite "left_cosets_group[T,*,one]") nil nil)) nil) ((left_cosets_group formula-decl nil factor_groups "algebra/") (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (group? const-decl "bool" group_def "algebra/") (group nonempty-type-eq-decl nil group "algebra/") (normal_subgroup? const-decl "boolean" normal_subgroups "algebra/") (normal_subgroup type-eq-decl nil normal_subgroups "algebra/") (T formal-type-decl nil right_left_cosets nil) (* formal-const-decl "[T, T -> T]" right_left_cosets nil) (one formal-const-decl "T" right_left_cosets nil)) nil)) (divide_TCC3 0 (divide_TCC3-1 nil 3530434541 ("" (skosimp*) (("" (inst 1 "N!1") (("" (inst 1 "one") (("1" (rewrite "left_coset_one") nil nil) ("2" (rewrite "one_in") nil nil)) nil)) nil)) nil) ((T formal-type-decl nil right_left_cosets 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]" right_left_cosets nil) (one formal-const-decl "T" right_left_cosets nil) (group? const-decl "bool" group_def "algebra/") (group nonempty-type-eq-decl nil group "algebra/") (= const-decl "[T, T -> boolean]" equalities nil) (* const-decl "set[T]" cosets "algebra/") (normal_subgroup? const-decl "boolean" normal_subgroups "algebra/") (normal_subgroup type-eq-decl nil normal_subgroups "algebra/") (left_cosets type-eq-decl nil cosets "algebra/") (N!1 skolem-const-decl "normal_subgroup[T, *, one](G!1)" right_left_cosets nil) (G!1 skolem-const-decl "group[T, *, one]" right_left_cosets nil) (monad nonempty-type-eq-decl nil monad "algebra/") (monad? const-decl "bool" monad_def "algebra/") (one_in formula-decl nil monad "algebra/") (left_coset_one formula-decl nil cosets "algebra/")) nil)) (divide_TCC4 0 (divide_TCC4-1 nil 3530434541 ("" (skosimp*) (("" (typepred "N!1") (("" (expand "normal_subgroup?") (("" (assert) nil nil)) nil)) nil)) nil) ((normal_subgroup type-eq-decl nil normal_subgroups "algebra/") (normal_subgroup? const-decl "boolean" normal_subgroups "algebra/") (group nonempty-type-eq-decl nil group "algebra/") (group? const-decl "bool" group_def "algebra/") (one formal-const-decl "T" right_left_cosets nil) (* formal-const-decl "[T, T -> T]" right_left_cosets nil) (set type-eq-decl nil sets nil) (T formal-type-decl nil right_left_cosets nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) nil)) (divide_TCC5 0 (divide_TCC5-1 nil 3530434541 ("" (skosimp*) (("" (expand "group?") (("" (prop) (("1" (expand "monoid?") (("1" (prop) (("1" (expand "monad?") (("1" (prop) (("1" (expand "star_closed?") (("1" (skosimp*) (("1" (assert) (("1" (expand "restrict") (("1" (expand "left_cosets") --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.87 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.Bot Zugriff |
