Quelle cosets.prf
Sprache: Lisp
(cosetsnil 3406031997"" (rewrite "fullset_is_group" ) nil nil )nil cosets nil )) nil ))nil 3397484255"" (skosimp*)"" (expand "equivalence?" )"" (auto-rewrite "member" )"" (expand "congruent_mod" )"" (split)"1" (expand "reflexive?" )"1" (skosimp*)"1" (typepred "H!1" )"1" (expand "group?" )"1" (expand "monoid?" )"1" (flatten)"1" (assert )"1" (expand "monad?" )"1" (skosimp*)"1" "H!1" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "symmetric?" )"2" (skosimp*)"2" (typepred "H!1" )"2" (assert )"2" (rewrite "subgroup_def" )"2" (flatten)"2" (expand "inv_closed?" )"2" (inst - "x!1 * inv(y!1)" )"2" (rewrite "inv_star" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (expand "transitive?" )"3" (skosimp*)"3" (typepred "H!1" )"3" (rewrite "subgroup_def" )"3" (flatten)"3" (assert )"3" (expand "star_closed?" )"3" "x!1 * inv(y!1)" "y!1 * inv(z!1)" )"3" (rewrite "associative" )"3" "associative" )"3" "inv(y!1)" "y!1" "inv(z!1)" )"3" assert )"3" replace -1 -7 rl)"3" rewrite "inv_left" )"3" rewrite "left_identity" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" relations nil )nil monad nil )nil group nil )"bool" monoid_def nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil cosets nil )set type-eq-decl nil sets nil )"[T, T -> T]" cosets nil )"T" cosets nil )"bool" group_def nil )nil group nil )"bool" relations nil )"bool" sets nil )"{y | x * y = one AND y * x = one}" group nil )"[T, T -> boolean]" equalities nil )AND const-decl "[bool, bool -> bool]" booleans nil )nil group nil )nil group nil )"bool" group nil )"(partial_order?[set[T]])" nil )nil group nil )"bool" relations nil )nil group nil )nil monad nil )nil semigroup nil )"bool" groupoid_def nil )"bool" relations nil )"bool" cosets nil ))nil )nil 3292960999"" (expand "equivalence?" )"" (expand "congruent_mod" )"" (skosimp*)"" (split)"1" (expand "reflexive?" )"1" (skosimp*)"1" (typepred "H!1" )"1" (expand "group?" )"1" (expand "monoid?" )"1" (flatten)"1" (assert )"1" (expand "monad?" )"1" (skosimp*)"1" (typepred "H!1" )"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "symmetric?" )"2" (skosimp*)"2" (typepred "H!1" )"2" (assert )"2" (rewrite "subgroup_def" )"2" (flatten)"2" (expand "inv_closed?" )"2" (inst - "x!1 * inv(y!1)" )"2" (rewrite "inv_star" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" (expand "transitive?" )"3" (skosimp*)"3" (typepred "H!1" )"3" (rewrite "subgroup_def" )"3" (flatten)"3" (assert )"3" (expand "star_closed?" )"3" "x!1 * inv(y!1)" "y!1 * inv(z!1)" )"3" (rewrite "associative" )"3" (lemma "associative" )"3" "inv(y!1)" "y!1" "inv(z!1)" )"3" assert )"3" replace -1 -7 rl)"3" rewrite "left_identity" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" monad_def nil )nil group nil )"bool" monoid_def nil )nil group nil )"[T, T -> T]" group nil )"T" group nil )"bool" group_def nil )nil group nil )nil group nil )nil group nil )"bool" group nil )nil group nil )nil group nil )nil monad nil )nil semigroup nil )"bool" groupoid_def nil ))nil 3406294944"" (skosimp*)"" (expand "subset?" )"" (skosimp*)"" (assert )"" (expand "member" )"" (expand "*" )"" (skosimp*)"" (typepred "h!1" )"" (typepred "H!1" )"" (expand "subgroup?" )"" (expand "subset?" )"" (inst?)"" (assert )"" (expand "member" )"" replace -4)"" "" rewrite "star_closed" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" sets nil )"bool" sets nil )nil groupoid nil )"bool" groupoid_def nil )nil groupoid nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil cosets nil )set type-eq-decl nil sets nil )"[T, T -> T]" cosets nil )"T" cosets nil )"bool" group_def nil )nil group nil )"bool" group_def nil )nil group nil )"set[T]" cosets nil ))nil 3406302835"" (skosimp*)"" (expand "subset?" )"" (skosimp*)"" (assert )"" (expand "member" )"" (expand "*" )"" (skosimp*)"" (typepred "h!1" )"" (typepred "H!1" )"" (expand "subgroup?" )"" (expand "subset?" )"" (inst?)"" (assert )"" (expand "member" )"" replace -4)"" "" rewrite "star_closed" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" sets nil )"bool" sets nil )nil groupoid nil )"bool" groupoid_def nil )nil groupoid nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil cosets nil )set type-eq-decl nil sets nil )"[T, T -> T]" cosets nil )"T" cosets nil )"bool" group_def nil )nil group nil )"bool" group_def nil )nil group nil )"set[T]" cosets nil ))nil )nil 3406299017"" (skosimp*)"" (expand "subset?" )"" (skosimp*)"" (expand "member" )"" (expand "*" )"" (skosimp*)"" (inst + "h!1" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )nil shostak))nil 3405953020"" (skosimp*)"" (apply-extensionality 1 :hide? t)"" (expand "*" )"" (iff 1)"" (prop)"1" (skosimp*)"1" (replace -1)"1" (hide -1)"1" (assert )"1" (rewrite "left_identity[T,*,one]" )"1" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (inst?)"2" (rewrite "left_identity[T,*,one]" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )nil cosets nil )nil booleans nil )"T" cosets nil )"set[T]" cosets nil ) (set type-eq-decl nil sets nil )nil booleans nil )"T" cosets nil )"set[T]" cosets nil )nil monad nil )"[T, T -> T]" cosets nil ))nil )nil 3405952955"" (skosimp*) (("" (postpone) nil nil )) nil ) nil shostak))nil 3405953057"" (skosimp*)"" (apply-extensionality 1 :hide? t)"" (iff 1)"" (expand "*" )"" (prop)"1" (skosimp*)"1" (replace -1)"1" (hide -1)"1" (rewrite "right_identity" )"1" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (inst?) (("2" (rewrite "right_identity" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )nil cosets nil )nil booleans nil )"T" cosets nil )"set[T]" cosets nil ) (set type-eq-decl nil sets nil )nil booleans nil )"T" cosets nil )"set[T]" cosets nil )"[T, T -> T]" cosets nil )nil monad nil ))nil ))nil 3405953079"" (skosimp*)"" (lemma "fullset_is_group" )"" (expand "group?" )"" (expand "monoid?" )"" (flatten)"" (hide -1 -3)"" (expand "associative?" )"" (expand "restrict" )"" (apply-extensionality 1 :hide? t)"" (expand "*" )"" (iff 1)"" (prop)"1" (skosimp*)"1" (replace -1)"1" "h!1" )"1" "1" replace -1)"1" "h!2" )"1" assert )"1" "1" (assert ) nil nil )"2" expand "fullset" )"2" (propax) nil nil ))nil )"3" expand "fullset" )"3" (propax) nil nil ))nil )"4" expand "fullset" )"4" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (replace -1)"2" "2" "h!1" )"2" "b!1*h!1" )"1" "1" expand "fullset" )"1" (propax) nil nil ))nil )"2" expand "fullset" )"2" (propax) nil nil ))nil )"3" expand "fullset" )"3" (propax) nil nil ))nil ))nil )"2" (inst?) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil cosets nil )"bool" monoid_def nil )"R" restrict nil )"set" sets nil )"T" cosets nil )"T" cosets nil )"set[T]" cosets nil )"(S!1)" cosets nil )"[T, T -> boolean]" equalities nil )NOT const-decl "[bool -> bool]" booleans nil )"(S!1)" cosets nil )"[T, T -> T]" cosets nil )"set[T]" cosets nil ) (set type-eq-decl nil sets nil )nil booleans nil )nil cosets nil )nil booleans nil )"bool" operator_defs nil )"bool" group_def nil ))nil ))nil 3405953119"" (skosimp*)"" (lemma "fullset_is_group" )"" (expand "group?" )"" (expand "monoid?" )"" (flatten)"" (hide -1 -3)"" (expand "associative?" )"" (expand "restrict" )"" (apply-extensionality 1 :hide? t)"" (expand "*" )"" (iff 1)"" (prop)"1" (skosimp*)"1" (replace -1)"1" "h!1" )"1" "1" replace -1)"1" "h!2" )"1" assert )"1" "1" assert )"1" expand "fullset" )"1" (propax) nil nil ))nil ))nil )"2" expand "fullset" )"2" (propax) nil nil ))nil )"3" expand "fullset" )"3" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (replace -1)"2" "2" "h!1" )"2" "h!1*a!1" )"1" "1" (assert ) nil nil )"2" expand "fullset" )"2" (propax) nil nil ))nil )"3" expand "fullset" )"3" (propax) nil nil ))nil )"4" expand "fullset" )"4" (propax) nil nil ))nil ))nil )"2" (inst?) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil cosets nil )"bool" monoid_def nil )"R" restrict nil )"set" sets nil )"set[T]" cosets nil )"(S!1)" cosets nil )"T" cosets nil )"T" cosets nil )"[T, T -> boolean]" equalities nil )NOT const-decl "[bool -> bool]" booleans nil )"(S!1)" cosets nil )"[T, T -> T]" cosets nil )"set[T]" cosets nil ) (set type-eq-decl nil sets nil )nil booleans nil )nil cosets nil )nil booleans nil )"bool" operator_defs nil )"bool" group_def nil ))nil ))nil 3405953143"" (skosimp*)"" (lemma "fullset_is_group" )"" (expand "group?" )"" (expand "monoid?" )"" (flatten)"" (hide -1 -3)"" (expand "associative?" )"" (expand "restrict" )"" (apply-extensionality 1 :hide? t)"" (expand "*" )"" (iff 1)"" (prop)"1" (skosimp*)"1" (replace -1)"1" "1" "inv(a!1)*h!1*b!1" )"1" "a!1" "inv(a!1) * h!1" "b!1" )"1" replace -1 * rl)"1" "1" "a!1" "inv(a!1)" "h!1" )"1" replace -1 * rl)"1" rewrite "inv_right" )"1" rewrite "left_identity" )nil nil ))nil ))nil )"2" expand "fullset" )"2" (propax) nil nil ))nil )"3" expand "fullset" )"3" (propax) nil nil ))nil )"4" expand "fullset" )"4" (propax) nil nil ))nil ))nil ))nil ))nil )"2" expand "fullset" )"2" (propax) nil nil ))nil )"3" expand "fullset" )"3" (propax) nil nil ))nil )"4" expand "fullset" )"4" (propax) nil nil ))nil ))nil )"2" "h!1" )"2" "2" replace -1)"2" "h!2" )"2" "inv[T, *, one](a!1)" "a!1" "h!2" )"1" replace -2 * rl)"1" rewrite "inv_left" )"1" rewrite "left_identity" )nil nil ))nil ))nil )"2" expand "fullset" )"2" (propax) nil nil ))nil )"3" expand "fullset" )"3" (propax) nil nil ))nil )"4" expand "fullset" )"4" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (replace -1)"2" "2" "(a!1*h!1)*inv(b!1)" )"1" "a!1 * h!1" "inv(b!1)" "b!1" )"1" replace -1)"1" rewrite "inv_left" )"1" rewrite "right_identity" )nil nil ))nil ))nil )"2" expand "fullset" )"2" (propax) nil nil ))nil )"3" expand "fullset" )"3" (propax) nil nil ))nil )"4" expand "fullset" )"4" (propax) nil nil ))nil ))nil )"2" "h!1" )"2" "2" replace -1)"2" "h!2" )"2" "a!1" "(h!2 * b!1)" "inv[T, *, one](b!1)" )"1" replace -2)"1" "1" "1" "1" replace -1)"1" rewrite "inv_right" )"1" rewrite "right_identity" )nil nil ))nil ))nil )"2" expand "fullset" )"2" nil nil ))nil )"3" expand "fullset" )"3" nil nil ))nil )"4" expand "fullset" )"4" nil nil ))nil ))nil ))nil ))nil ))nil )"2" expand "fullset" )"2" (propax) nil nil ))nil )"3" expand "fullset" )"3" (propax) nil nil ))nil )"4" expand "fullset" )"4" (propax) 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 cosets nil )"bool" monoid_def nil )"R" restrict nil )"T" cosets nil )"({t: T | EXISTS (h: (S!1)): t = a!1 * h})" nil )"T" cosets nil )"{y | x * y = one AND y * x = one}" group nil )"T" cosets nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> T]" cosets nil )"[T, T -> boolean]" equalities nil )"set[T]" cosets nil )nil group nil )nil monad nil )"set" sets nil )nil group nil )"(S!1)" cosets nil )NOT const-decl "[bool -> bool]" booleans nil )"({t: T | EXISTS (h: (S!1)): t = h * b!1})" nil )nil monad nil )"(S!1)" cosets nil )"set[T]" cosets nil )"set[T]" cosets nil ) (set type-eq-decl nil sets nil )nil booleans nil )nil cosets nil )nil booleans nil )"bool" operator_defs nil )"bool" group_def nil ))nil ))nil 3406302438"" (skosimp*)"" (expand "subset?" )"" (skosimp*)"" (assert )"" (expand "member" )"" (expand "*" )"" (skosimp*)"" (inst + "h!1" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" sets nil )"bool" sets nil )"set[T]" cosets nil )"set[T]" cosets nil )"(S!1)" cosets nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil cosets nil )"set[T]" cosets nil ))nil ))nil 3406302482"" (skosimp*)"" (expand "subset?" )"" (skosimp*)"" (expand "member" )"" (expand "*" )"" (skosimp*)"" (inst + "h!1" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" sets nil )"bool" sets nil )"set[T]" cosets nil )"set[T]" cosets nil )"(S!1)" cosets nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil cosets nil )"set[T]" cosets nil ))nil ))nil 3406294305"" (skosimp*)"" (lemma "right_coset_subset" ) (("" (inst?) nil nil )) nil )) nil )nil cosets nil )nil cosets nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )"[T, T -> T]" cosets nil )"T" cosets nil )"bool" group_def nil )nil group nil )"bool" group_def nil )nil group nil ))nil ))nil 3406037458 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )set type-eq-decl nil sets nil )"bool" group_def nil )nil group nil )"bool" sets nil )"bool" sets nil )"T" cosets nil )"[T, T -> T]" cosets nil )nil cosets nil )"bool" group_def nil ))nil ))nil 3406037466"" (skosimp*)"" (expand "restrict" )"" (expand "right_coset" )"" (expand "restrict" )"" (apply-extensionality 1 :hide? t)"" (expand "image" )"" (expand "*" ) (("" (propax) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )"R" restrict nil )nil cosets nil )nil booleans nil )"bool" booleans nil )"set[R]" function_image nil )nil group nil )"bool" group_def nil )"T" cosets nil )"[T, T -> T]" cosets nil )"set[T]" cosets nil ) (set type-eq-decl nil sets nil )nil booleans nil )"bool" sets nil )"{s: set[T] | subset?(s, G)}" cosets nil ))nil 3292962829"" (skosimp*)"" (typepred "G!1" )"" (typepred "H!1" )"" (assert )"" case "subset?(right_coset(G!1, H!1)(a!1),{x: T | congruent_mod(G!1, H!1)(a!1, x)})" )"1" case "subset?({x: T | congruent_mod(G!1, H!1)(a!1, x)},right_coset(G!1, H!1)(a!1))" )"1" "subset_antisymmetric" "a" "right_coset(G!1, H!1)(a!1)" "b" "{x: T | congruent_mod(G!1, H!1)(a!1, x)}" ))"1" (assert ) nil nil )) nil )"2" (assert )"2" (expand "member" )"2" (hide -1 2)"2" (expand "subset?" )"2" (skosimp*)"2" (assert )"2" (expand "congruent_mod" -1 1)"2" (assert )"2" rewrite "subgroup_def" )"2" "2" expand "inv_closed?" )"2" "a!1 * inv(x!1)" )"1" rewrite "inv_star" )"1" assert )"1" rewrite "right_coset_image" )"1" assert )"1" expand "restrict" )"1" assert )"1" expand "image" )"1" expand "member" )"1" "x!1*inv(a!1)" )"1" rewrite "associative" )"1" rewrite "inv_left" )"1" rewrite "right_identity" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "member" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (expand "subset?" )"2" (skosimp*)"2" (rewrite "right_coset_image" )"2" (expand "restrict" )"2" (expand "image" )"2" (assert )"2" (expand "congruent_mod" )"2" (expand "member" )"2" "2" "x!2" )"2" replace -2 1)"2" rewrite "inv_star" )"2" rewrite "associative" "2" rewrite "inv_right" )"2" rewrite "left_identity" )"2" "inv_member" "G" "H!1" "x" "x!2" ))"2" expand "member" )"2" 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 group nil )"bool" group_def nil )"T" cosets nil )"[T, T -> T]" cosets nil )set type-eq-decl nil sets nil )nil cosets nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"bool" sets nil )nil group nil )nil monad nil )nil group nil )"(partial_order?[set[T]])" nil )nil sets_lemmas nil )nil group nil )"bool" group nil )nil group nil )nil group nil )nil cosets nil )"R" restrict nil )"set[R]" function_image nil )nil monad nil )nil group nil )nil semigroup nil )"bool" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"{y | x * y = one AND y * x = one}" group nil )"bool" sets nil )"bool" group_def nil )nil group nil )"{s: set[T] | subset?(s, G)}" cosets nil )"bool" cosets nil ))nil 3405953353"" (skosimp*)"" (expand "right_coset" )"" (expand "restrict" )"" (expand "image" )"" (expand "*" ) (("" (propax) nil nil )) nil )) nil ))nil ))nil ))nil )"{s: set[T] | subset?(s, G)}" cosets nil ))nil ))nil 3292974326"" (skosimp*)"" (expand "right_coset" )"" (expand "member" )"" (expand "nonempty?" )"" (expand "empty?" )"" (expand "member" )"" (expand "*" )"" (inst - "a!1" )"" (inst + "one" )"1" (rewrite "one_left" ) nil nil )"2" (assert ) (("2" (rewrite "one_in" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"{s: set[T] | subset?(s, G)}" cosets nil )"bool" sets nil )nil cosets nil )nil monad nil )"bool" monad_def nil )nil monad nil )nil group nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )"[T, T -> T]" cosets nil )"T" cosets nil )"bool" group_def nil )nil group nil )"group[T, *, one]" cosets nil )"set[T]" cosets nil )"bool" sets nil )"bool" sets nil ))nil 3406469955"" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )set type-eq-decl nil sets nil )"bool" group_def nil )nil group nil )"{s: set[T] | subset?(s, G)}" cosets nil )"bool" sets nil )"bool" sets nil )"T" cosets nil )"[T, T -> T]" cosets nil )nil cosets nil )"bool" group_def nil ))nil ))nil 3406302721"" (skosimp*)"" (typepred "G!1" )"" (expand "subgroup?" )"" (assert )"" (inst + "LAMBDA (x:(A!1)): x*inv(a!1)*b!1" )"1" (expand "bijective?" )"1" (split)"1" (expand "injective?" )"1" (skosimp*)"1" "cancel_right" "x" "x1!1" "z" "inv(a!1) * b!1" "y" "x2!1" ))"1" (expand "group?" )"1" (expand "monoid?" )"1" (flatten)"1" (expand "associative?" )"1" "x1!1" )"1" "x2!1" )"1" expand "inv_exists?" )"1" assert )"1" rewrite "associative" "1" rewrite "associative" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "surjective?" )"2" (skosimp*)"2" (typepred "y!1" )"2" (replace -7)"2" (rewrite "right_coset_is" -1)"1" (assert )"1" (expand "congruent_mod" )"1" assert )"1" "right_coset_is" "H" "H!1" "G" "G!1" "a" "a!1" ))"1" expand "subgroup?" )"1" assert )"1" case "A!1(y!1*inv(b!1)*a!1)" )"1" "y!1 * inv(b!1) * a!1" )"1" expand "group?" )"1" expand "monoid?" )"1" expand "associative?" )"1" "1" "inv_member" "x" "a!1" "G" "G!1" ))"1" "inv_member" "x" "b!1" "G" "G!1" ))"1" assert )"1" "1" case "G!1(y!1)" )"1" "y!1 * inv(b!1)" "a!1" "inv(a!1)" )"1" expand "restrict" )"1" assert )"1" "y!1" "inv(b!1)" "b!1" )"1" assert )"1" rewrite "associative" "1" rewrite "associative" "1" "associative" )"1" "inv(b!1)" "a!1" "inv(a!1)" )"1" replace "1" rewrite "inv_right" "1" rewrite "right_identity" )"1" rewrite "associative" "1" rewrite "inv_left" "1" assert )"1" rewrite "one_right" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" assert )"2" expand "inv" )"2" nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" "G!1" )"2" expand "group?" )"2" expand "monoid?" )"2" expand "monad?" )"2" "2" expand "groupoid?" )"2" expand "star_closed?" )"2" expand "member" )"2" "y!1" "inv(b!1)" )"1" expand "inv" )"1" nil nil ))nil )"2" expand "inv" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" rewrite "star_closed" )nil nil ))nil )"2" "2" "y!1" )"2" case "subset?(B!1, G!1)" )"1" expand "subset?" )"1" assert )"1" "1" assert )nil nil ))nil ))nil ))nil )"2" "B!1 = right_coset(G!1, H!1)(b!1)" )"1" "right_coset_subset" )"1" expand "right_coset" )"1" "G!1" "H!1" "b!1" )"1" expand "subgroup?" )"1" nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" replace -7)"2" expand "right_coset" )"2" replace -1)"2" expand "congruent_mod" )"2" assert )"2" rewrite "inv_star" "2" rewrite "inv_star" "2" rewrite "assoc" )"2" rewrite "assoc" )"2" rewrite "assoc" )"2" rewrite "inv_right" )"2" rewrite "one_left" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" (expand "subgroup?" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (typepred "x!1" )"2" (replace -7)"2" (rewrite "right_coset_is" 1)"1" (expand "congruent_mod" 1)"1" (rewrite "inv_star" 1)"1" (rewrite "associative" 1 :dir rl)"1" (rewrite "inv_star" 1)"1" (replace -6)"1" rewrite "right_coset_is" -1)"1" assert )"1" expand "congruent_mod" )"1" assert )"1" rewrite "inv_right" )"1" rewrite "left_identity" )nil nil ))nil ))nil ))nil ))nil )"2" expand "subgroup?" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "subgroup?" ) (("2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil group nil )"bool" group_def nil )"T" cosets nil )"[T, T -> T]" cosets nil )set type-eq-decl nil sets nil )nil cosets nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil )"(partial_order?[set[T]])" nil )"bool" sets nil )"bool" functions nil )"bool" functions nil )nil cosets nil )"bool" cosets nil )nil group nil )nil group nil )nil monad nil )nil group nil )"(B!1)" cosets nil )"bool" sets nil )nil cosets nil )"group[T, *, one]" cosets nil )nil group nil )"{s: set[T] | subset?(s, G)}" cosets nil )"group[T, *, one]" cosets nil )nil group nil )nil monad nil )nil group nil )"R" restrict nil )"bool" monad_def nil )"bool" groupoid_def nil )nil group nil )"bool" functions nil )nil group nil )"bool" monoid_def nil )"bool" operator_defs nil )nil semigroup nil )"bool" group_def nil )"set[T]" cosets nil )"set[T]" cosets nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"{y | x * y = one AND y * x = one}" group nil )"T" cosets nil )"T" cosets nil )"bool" group_def nil ))nil )nil 3397484291"" (auto-rewrite "member" )"" (skosimp*)"" (typepred "G!1" )"" (expand "subgroup?" )"" (assert )"" (inst + "LAMBDA (x:(A!1)): x*inv(a!1)*b!1" )"1" (expand "bijective?" )"1" (split)"1" (expand "injective?" )"1" (skosimp*)"1" "cancel_right" "x" "x1!1" "z" "inv(a!1) * b!1" "y" "x2!1" ))"1" (expand "group?" )"1" (expand "monoid?" )"1" (flatten)"1" expand "associative?" )"1" "x1!1" )"1" "x2!1" )"1" expand "inv_exists?" )"1" assert )"1" rewrite "associative" "1" rewrite "associative" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "surjective?" )"2" (skosimp*)"2" (typepred "y!1" )"2" (replace -7)"2" (rewrite "right_coset_is" -1)"1" (assert )"1" expand "congruent_mod" )"1" assert )"1" "right_coset_is" "H" "H!1" "G" "G!1" "a" "a!1" ))"1" expand "subgroup?" )"1" assert )"1" case "A!1(y!1*inv(b!1)*a!1)" )"1" "y!1 * inv(b!1) * a!1" )"1" expand "group?" )"1" expand "monoid?" )"1" expand "associative?" )"1" "1" "inv_member" "x" "a!1" "G" "G!1" ))"1" "inv_member" "x" "b!1" "G" "G!1" ))"1" assert )"1" "1" case "G!1(y!1)" )"1" "y!1 * inv(b!1)" "a!1" "inv(a!1)" )"1" expand "restrict" )"1" assert )"1" "y!1" "inv(b!1)" "b!1" )"1" assert )"1" rewrite "associative" "1" rewrite "associative" "1" "associative" )"1" "inv(b!1)" "a!1" "inv(a!1)" )"1" replace "1" rewrite "inv_right" "1" rewrite "right_identity" )"1" rewrite "associative" "1" rewrite "inv_left" "1" assert )"1" rewrite "one_right" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" "G!1" )"2" expand "group?" )"2" expand "monoid?" )"2" expand "monad?" )"2" "2" expand "groupoid?" )"2" expand "star_closed?" )"2" expand "member" )"2" "y!1" "inv(b!1)" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "y!1" )"2" case "subset?(B!1, G!1)" )"1" expand "subset?" )"1" assert )"1" "1" assert )nil nil ))nil ))nil ))nil )"2" "B!1 = right_coset(G!1, H!1)(b!1)" )"1" "right_coset_subgroup" )"1" expand "right_coset" )"1" "G!1" "H!1" "b!1" )"1" expand "subgroup?" )"1" nil nil ))nil )"2" expand "subgroup?" )"2" nil nil ))nil ))nil ))nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" replace -7)"2" expand "right_coset" )"2" replace -1)"2" expand "congruent_mod" )"2" assert )"2" rewrite "inv_star" "2" rewrite "inv_star" "2" rewrite "assoc" )"2" rewrite "assoc" )"2" rewrite "assoc" )"2" rewrite "inv_right" )"2" rewrite "one_left" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (hide 2)"2" expand "subgroup?" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (typepred "x!1" )"2" (replace -7)"2" (rewrite "right_coset_is" 1)"1" (expand "congruent_mod" 1)"1" (rewrite "inv_star" 1)"1" (rewrite "associative" 1 :dir rl)"1" (rewrite "inv_star" 1)"1" replace -6)"1" rewrite "right_coset_is" -1)"1" assert )"1" expand "congruent_mod" )"1" assert )"1" rewrite "inv_right" )"1" rewrite "left_identity" )nil nil ))nil ))nil ))nil ))nil )"2" expand "subgroup?" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "subgroup?" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" group_def nil )"bool" group_def nil )nil semigroup nil )"bool" monoid_def nil )nil group nil )nil group nil )"bool" groupoid_def nil )"bool" monad_def nil )nil monad nil )nil group nil )nil group nil )nil group nil )nil group nil )nil group nil )nil group nil )nil group nil )nil group nil )nil monad nil )"bool" group_def nil )nil group nil ))nil )nil 3292965473"" (skosimp*)"" (typepred "G!1" )"" (expand "subgroup?" )"" (assert )"" (inst + "LAMBDA (x:(A!1)): x*inv(a!1)*b!1" )"1" (expand "bijective?" )"1" (split)"1" (expand "injective?" )"1" (skosimp*)"1" "cancel_right" "x" "x1!1" "z" "inv(a!1) * b!1" "y" "x2!1" ))"1" (expand "group?" )"1" (expand "monoid?" )"1" (flatten)"1" (expand "associative?" )"1" "x1!1" )"1" "x2!1" )"1" expand "inv_exists?" )"1" assert )"1" rewrite "associative" "1" rewrite "associative" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "surjective?" )"2" (skosimp*)"2" (typepred "y!1" )"2" (replace -8 -2)"2" (rewrite "right_coset_is" -2)"1" (assert )"1" (expand "congruent_mod" )"1" assert )"1" "right_coset_is" "H" "H!1" "G" "G!1" "a" "a!1" ))"1" expand "subgroup?" )"1" assert )"1" case "A!1(y!1*inv(b!1)*a!1)" )"1" "y!1 * inv(b!1) * a!1" )"1" expand "group?" )"1" expand "monoid?" )"1" expand "associative?" )"1" "1" "inv_member" "x" "a!1" "G" "G!1" ))"1" "inv_member" "x" "b!1" "G" "G!1" ))"1" assert )"1" "1" "y!1 * inv(b!1)" "a!1" "inv(a!1)" )"1" assert )"1" "y!1" "inv(b!1)" "b!1" )"1" assert )"1" rewrite "associative" "1" rewrite "associative" "1" "associative" )"1" "inv(b!1)" "a!1" "inv(a!1)" )"1" rewrite "inv_right" "1" rewrite "right_identity" )"1" replace "1" rewrite "associative" "1" rewrite "right_identity" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" assert )"2" "G!1" )"2" expand "group?" )"2" expand "monoid?" )"2" expand "monad?" )"2" "2" expand "groupoid?" )"2" expand "star_closed?" )"2" expand "member" )"2" "y!1" "inv(b!1)" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" replace -8 1)"2" replace -1 1)"2" assert )"2" expand "congruent_mod" )"2" "inv_star" "x" "y!1*inv(b!1)" "y" "a!1" ))"2" replace -1 1)"2" expand "group?" )"2" expand "monoid?" )"2" expand "associative?" )"2" "2" "2" rewrite "inv_star" "2" expand "inv_exists?" )"2" rewrite "associative" "2" rewrite "associative" "2" rewrite "associative" "2" rewrite "left_identity" )"2" "2" "inv_member" "x" "b!1" "G" "G!1" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" expand "group?" )"3" "3" expand "monoid?" )"3" "3" "3" "inv_member" "x" "b!1" "G" "G!1" ))"3" assert )"3" "3" expand "monad?" )"3" expand "groupoid?" )"3" expand "star_closed?" )"3" "3" expand "member" )"3" "y!1" "inv(b!1)" )"3" "y!1 * inv(b!1)" "a!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "subgroup?" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (skosimp*)"2" (typepred "x!1" )"2" (replace -8 1)"2" (rewrite "right_coset_is" 1)"1" (expand "congruent_mod" 1)"1" (rewrite "inv_star" 1)"1" (rewrite "associative" 1 :dir rl)"1" (rewrite "inv_star" 1)"1" (split)"1" expand "group?" )"1" expand "monoid?" )"1" "1" expand "inv_exists?" )"1" "a!1" )"1" "1" "unique_inv" "x" "a!1" "y" "y!1" ))"1" "1" "y!1" )"1" "1" "1" assert )"1" "1" "inv_member" "x" "a!1" "G" "G!1" ))"1" expand "member" )"1" assert )"1" "1" expand "monad?" )"1" expand "groupoid?" )"1" "1" expand "star_closed?" )"1" expand "member" )"1" "x!1" "inv(a!1)" )"1" "x!1*inv(a!1)" "b!1" )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 )"2" replace -7 -2)"2" rewrite "right_coset_is" -2)"1" assert )"1" expand "congruent_mod" )"1" assert )"1" rewrite "left_identity" )nil nil ))nil ))nil ))nil )"2" expand "subgroup?" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "subgroup?" ) (("2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil group nil )"bool" group_def nil )"T" group nil )"[T, T -> T]" group nil )nil group nil )nil group nil )nil group nil )nil monad nil )nil group nil )"bool" groupoid_def nil )"bool" monad_def nil )nil monad nil )nil group nil )nil group nil )nil group nil )nil group nil )"bool" monoid_def nil )nil semigroup nil )"bool" group_def nil )"bool" group_def nil ))nil 3406294466"" (skosimp*)"" (lemma "left_coset_subset" ) (("" (inst?) nil nil )) nil )) nil )nil cosets nil )nil cosets nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )"[T, T -> T]" cosets nil )"T" cosets nil )"bool" group_def nil )nil group nil )"bool" group_def nil )nil group nil ))nil ))nil 3406039868"" (skosimp*)"" (expand "restrict" )"" (expand "left_coset" )"" (expand "image" )"" (expand "restrict" )"" (apply-extensionality 1 :hide? t)"" (expand "*" ) (("" (propax) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )"R" restrict nil )"set[R]" function_image nil )"bool" sets nil )nil booleans nil )set type-eq-decl nil sets nil ) (* const-decl "set[T]" cosets nil )"[T, T -> T]" cosets nil )"T" cosets nil )"bool" group_def nil )nil group nil )"bool" booleans nil )"[T, T -> boolean]" equalities nil )nil cosets nil )nil booleans nil )"{s: set[T] | subset?(s, G)}" cosets nil ))nil 3405953366"" (skosimp*)"" (expand "left_coset" )"" (expand "restrict" )"" (expand "image" )"" (expand "*" ) (("" (propax) nil nil )) nil )) nil ))nil ))nil ))nil )"{s: set[T] | subset?(s, G)}" cosets nil ))nil ))nil 3406471386"" (skosimp*)"" (expand "nonempty?" )"" (expand "empty?" )"" (expand "member" )"" (typepred "lc!1" )"" (skosimp*)"" (inst - "a!1" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )"bool" sets nil )"bool" sets nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil cosets nil )set type-eq-decl nil sets nil )"[T, T -> T]" cosets nil )"T" cosets nil )"bool" group_def nil )nil group nil )"[T, T -> boolean]" equalities nil )"set[T]" cosets nil )"bool" group_def nil )nil group nil )nil cosets nil )"bool" sets nil ))nil ))nil 3406471386 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )set type-eq-decl nil sets nil )"bool" group_def nil )nil group nil )"bool" group_def nil )"bool" monoid_def nil )"bool" operator_defs nil )"bool" monad_def nil )identity ? const-decl "bool" operator_defs nil )nil monad nil )"R" restrict nil )nil monad nil )nil monad nil )"bool" groupoid_def nil )"group[T, *, one]" cosets nil )"group[T, *, one]" cosets nil )"(G!1)" cosets nil )"bool" sets nil )"bool" sets nil )"T" cosets nil )"[T, T -> T]" cosets nil )nil cosets nil )"bool" group_def nil ))nil ))nil 3406471506"" (skosimp*) (("" (assert ) nil nil )) nil ) nil shostak))nil 3406471460"" (skosimp*)"" (expand "nonempty?" )"" (expand "empty?" )"" (expand "member" )"" (typepred "rc!1" )"" (skosimp*)"" (inst - "a!1" ) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil )"bool" sets nil )"bool" sets nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil cosets nil )set type-eq-decl nil sets nil )"[T, T -> T]" cosets nil )"T" cosets nil )"bool" group_def nil )nil group nil )"[T, T -> boolean]" equalities nil )"set[T]" cosets nil )"bool" group_def nil )nil group nil )nil cosets nil )"bool" sets nil ))nil )nil 3406471453";;; Proof rc_gen_TCC1-1 for formula cosets.rc_gen_TCC1" ";;; Proof lc_gen_TCC1-1 for formula cosets.lc_gen_TCC1" ";;; developed with shostak decision procedures" "" (skosimp*) expand "nonempty?" ) (expand "empty?" ) (expand "member" )"lc!1" ) (skosimp*) (inst - "a!1" ) (assert ))";;; Proof rc_gen_TCC1-1 for formula cosets.rc_gen_TCC1" nil ))";;; developed with shostak decision procedures") nil nil )nil 3406471386 ("" (subtype-tcc) nil nil ) nil nil ))nil 3406471386 ("" (subtype-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )set type-eq-decl nil sets nil )"bool" group_def nil )nil group nil )"bool" group_def nil )"bool" monoid_def nil )"bool" operator_defs nil )"bool" monad_def nil )identity ? const-decl "bool" operator_defs nil )nil monad nil )"R" restrict nil )nil monad nil )nil monad nil )"bool" groupoid_def nil )"group[T, *, one]" cosets nil )"group[T, *, one]" cosets nil )"(G!1)" cosets nil )"bool" sets nil )"bool" sets nil )"T" cosets nil )"[T, T -> T]" cosets nil )nil cosets nil )"bool" group_def nil ))nil ))nil 3406471511"" (skosimp*) (("" (assert ) nil nil )) nil ) nil shostak))nil 3406564023"" (skosimp*)"" (case "(a!1 * H!1)(a!1) = (b!1 * H!1)(a!1)" )"1" (expand "*" )"1" (case "(EXISTS (h: (H!1)): a!1 = a!1 * h)" )"1" (assert ) nil nil )"2" (hide 2)"2" (inst + "one" )"1" (rewrite "one_right" ) nil nil )"2" (assert ) (("2" (rewrite "one_in" ) nil nil )) nil ))nil ))nil ))nil ))nil )"2" (hide 2) (("2" (assert ) nil nil )) nil ))nil ))nil )nil group nil )"bool" group_def nil )"T" cosets nil )"[T, T -> T]" cosets nil )"set[T]" cosets nil ) (set type-eq-decl nil sets nil )nil cosets nil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil booleans nil )"group[T, *, one]" cosets nil )nil group nil )nil monad nil )"bool" monad_def nil )nil monad nil ))nil ))nil 3406564055"" (skosimp*)"" (replace -2)"" (apply-extensionality 1 :hide? t)"" (expand "*" )"" (iff 1)"" (prop)"1" (skosimp*)"1" (inst + "h!1*h!2" )"1" (assert ) (("1" (rewrite "assoc" ) nil nil )) nil )"2" (rewrite "star_closed" ) nil nil ))nil ))nil )"2" (skosimp*)"2" (replace -1)"2" (inst + "inv(h!1)*h!2" )"1" (rewrite "assoc" )"1" (case-replace "b!1 * h!1 * inv(h!1) = b!1" )"1" (hide 2)"1" (rewrite "associative" )"1" (rewrite "inv_right" )"1" (rewrite "one_right" ) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (rewrite "star_closed" )"2" (rewrite "inv_in" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"(H!1)" cosets nil )"(H!1)" cosets nil )"group[T, *, one]" cosets nil )nil group nil )nil groupoid nil )"bool" groupoid_def nil )nil groupoid nil )nil group nil )nil semigroup nil )nil monad nil )nil group nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"{y | x * y = one AND y * x = one}" group nil )"(H!1)" cosets nil )nil booleans nil )set type-eq-decl nil sets nil ) (* const-decl "set[T]" cosets nil )"[T, T -> T]" cosets nil )"T" cosets nil )"bool" group_def nil )nil group nil )nil booleans nil )nil cosets nil ))nil ))nil 3406567898"" (skosimp*)"" (case "(H!1 * a!1)(a!1) = (H!1 * b!1)(a!1)" )"1" (expand "*" )"1" (case "(EXISTS (h: (H!1)): a!1 = h * a!1)" )"1" (assert ) nil nil )"2" (hide 2)"2" (inst + "one" )"1" (assert ) (("1" (rewrite "one_left" ) nil nil )) nil )"2" (rewrite "one_in" ) nil nil ))nil ))nil ))nil ))nil )"2" (hide 2) (("2" (assert ) nil nil )) nil ))nil ))nil )nil group nil )"bool" group_def nil )"T" cosets nil )"[T, T -> T]" cosets nil )"set[T]" cosets nil ) (set type-eq-decl nil sets nil )nil cosets nil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil booleans nil )"group[T, *, one]" cosets nil )nil monad nil )nil monad nil )"bool" monad_def nil )nil monad nil ))nil 3406568037"" (skosimp*)"" (replace -2)"" (apply-extensionality 1 :hide? t)"" (expand "*" )"" (iff 1)"" (prop)"1" (skosimp*)"1" (inst + "h!2*h!1" )"1" (assert ) (("1" (rewrite "assoc" ) nil nil )) nil )"2" (rewrite "star_closed" ) nil nil ))nil ))nil )"2" (skosimp*)"2" (replace -1)"2" (inst + "h!2*inv(h!1)" )"1" (rewrite "assoc" )"1" (case-replace "b!1 * h!1 * inv(h!1) = b!1" )"1" "h!2 * inv(h!1) * h!1 = h!2" )"1" (hide 2)"1" (rewrite "associative" )"1" rewrite "inv_left" )"1" (rewrite "one_right" ) nil nil ))nil ))nil ))nil ))nil )"2" (rewrite "associative" )"2" (rewrite "inv_right" )"2" (rewrite "one_right" ) nil nil )) nil ))nil ))nil ))nil )"2" (rewrite "star_closed" )"2" (rewrite "inv_in" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"(H!1)" cosets nil )"(H!1)" cosets nil )"group[T, *, one]" cosets nil )nil group nil )nil groupoid nil )"bool" groupoid_def nil )nil groupoid nil )nil group nil )nil group nil )nil group nil )nil monad nil )nil semigroup nil )"(H!1)" cosets nil )AND const-decl "[bool, bool -> bool]" booleans nil )"[T, T -> boolean]" equalities nil )"{y | x * y = one AND y * x = one}" group nil )nil booleans nil )set type-eq-decl nil sets nil ) (* const-decl "set[T]" cosets nil )"[T, T -> T]" cosets nil )"T" cosets nil )"bool" group_def nil )nil group nil )nil booleans nil )nil cosets nil ))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ Dauer der Verarbeitung: 0.155 Sekunden
(vorverarbeitet am 2026-04-27)
¤ *© Formatika GbR, Deutschland
2026-05-26
