Quelle finite_groups.prf
Sprache: Lisp
(finite_groupsnil 3407081817"" (lemma "fullset_is_group" ) (("" (propax) nil nil )) nil )nil finite_groups nil )) nil ))nil 3306144725"" (skosimp*)"" (lemma "generated_is_subgroup" ("a" "a!1" "G" "G!1" ))"" (assert )"" (expand "subgroup?" )"" (assert )"" (typepred "G!1" )"" (expand "finite_group?" )"" (flatten)"" (lemma "finite_subset[T]" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"T" finite_groups nil )"[T, T -> T]" finite_groups nil )nil finite_groups nil )nil group nil )"bool" group_def nil )nil group nil )"bool" group_def nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil group nil )"bool" group_def nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" finite_sets nil )"finite_group[T, *, one]" finite_groups nil )"group" group nil )nil finite_sets nil )nil finite_sets nil )"(partial_order?[set[T]])" nil )"bool" sets nil ))nil 3293285775"" (skosimp*)"" (lemma "finite_generated_by" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil )nil finite_groups nil )"bool" sets nil )nil group nil )"bool" group_def nil )"T" finite_groups nil )"[T, T -> T]" finite_groups nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil finite_groups nil ))nil 3407237397"" (skosimp*)"" (case "S!1(a!1)" )"1" (assert )"1" (typepred "G!1" )"1" (expand "finite_group?" )"1" (flatten)"1" (lemma "finite_subset" ("s" "S!1" "A" "G!1" ))"1" (assert )"1" (lemma "nonempty_card" ("S" "S!1" ))"1" (flatten -1)"1" (hide -2)"1" (case-replace "nonempty?(S!1)" )"1" "X" "{t: T | EXISTS (n: posnat): n <= card(S!1) AND t = a!1 ^ n}" )"1" (replace -1)"1" case "subset?(X,S!1)" )"1" "N" "card(S!1)" )"1" replace -1)"1" case "FORALL (n:posnat): n < N => a!1^n /= one" )"1" case "FORALL (i,j:posnat): i <= N & j <= N & i /= j => a!1^i /= a!1^j" )"1" "card_bij" "S" "X" "N" "N" ))"1" case "(EXISTS (f: [(X) -> below[N]]): bijective?(f))" )"1" replace -1 -2)"1" "1" "same_card_subset" "A" "X" "B" "S!1" ))"1" assert )nil nil ))nil ))nil ))nil )"2" "2" "F" "LAMBDA (n: below[N]): IF n = 0 THEN a!1 ^ N ELSE a!1 ^ n ENDIF") "2" case "bijective?[below[N],(X)](F)" )"1" "bijective_inverse_exists[below[N],(X)]" "f" "F" ))"1" expand "exists1" )"1" "1" "1" "bij_inv_is_bij_alt[below[N],(X)]" "f" "F" "g" "x!1" ))"1" "x!1" )nil nil )"2" nil nil ))nil ))nil ))nil ))nil )"2" nil nil ))nil )"2" "2" expand "F" 1)"2" assert )"2" "2" expand "bijective?" )"2" "1" expand "injective?" )"1" "1" "x1!1=0" )"1" assert )"1" "N" "x2!1" )"1" assert )nil nil ))nil ))nil )"2" assert )"2" "x2!1=0" )"1" "x1!1" "N" )"1" assert )nil nil ))nil )"2" assert )"2" "x1!1" "x2!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "surjective?" )"2" "2" "y!1" )"2" expand "X" "2" "2" "2" expand "<=" "2" "1" replace "1" "n!1" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil )"2" replace "2" replace "2" replace "2" "0" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" assert )"3" "3" expand "X" 1)"3" expand "F" "3" "3" replace "3" "x1!1" )"3" "x1!1=0" )"1" "N" )"1" assert )nil nil ))nil )"2" assert )"2" "x1!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "generated_is_subgroup" "a" "a!1" "G" "G!1" ))"2" expand "subgroup?" )"2" assert )"2" "finite_subset" "s" "X" "A" "S!1" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "trichotomy" "x" "i!1-j!1" ))"2" "1" "cancel_right" "z" "a!1^(-j!1)" "x" "a!1^i!1" "y" "a!1^j!1" ))"1" rewrite "expt_mult" "1" rewrite "expt_mult" "1" assert )"1" "i!1-j!1" )"1" assert )"1" rewrite "expt_0" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil )"3" "cancel_right" "z" "a!1^(-i!1)" "x" "a!1 ^ i!1" "y" "a!1 ^ j!1" ))"3" rewrite "expt_mult" "3" rewrite "expt_mult" "3" assert )"3" "j!1-i!1" )"3" assert )"3" rewrite "expt_0" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" case "subset?(S!1,X)" )"1" "subset_antisymmetric" "a" "S!1" "b" "X" ))"1" (assert ) nil nil ))nil )"2" "2" expand "subset?" )"2" "2" expand "member" )"2" replace -6 1 rl)"2" expand "generated_by" )"2" assert )"2" replace "2" "2" "2" "n!1" )"2" case "EXISTS (k:below[N],j:int): i!1 = j*n!1+k" )"1" "1" "k!1" )"1" "k!1=0" )"1" replace "1" "expt_expt" "a" "a!1" "i" "n!1" "j" "j!1" ))"1" replace "1" assert )"1" replace "1" replace "1" "n!1" )"1" assert )"1" rewrite "one_expt" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" "expt_expt" "a" "a!1" "i" "n!1" "j" "j!1" ))"2" replace "2" assert )"2" rewrite "expt_mult" "2" replace "2" assert )"2" "k!1" )"2" assert )"2" rewrite "one_expt" )"2" assert )"2" rewrite "left_identity" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "fractional(i!1/n!1)*n!1" "floor(i!1/n!1)" )"1" "real_parts" "x" "i!1/n!1" ))"1" rewrite "div_cancel3" nil nil ))nil )"2" "fractional(i!1 / n!1)" )"2" "n!1" )"2" "n!1" )"2" assert )"2" expand "fractional" )"2" "i!1 / n!1 * n!1 = i!1" )"1" assert )nil nil )"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 )"2" expand "subset?" )"2" replace -1 * rl)"2" "2" "2" expand "member" )"2" expand "generated_by" )"2" "2" replace -2 1)"2" replace -11 1)"2" "2" "n!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "nonempty?" )"2" (expand "empty?" )"2" "a!1" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "generated_is_subgroup" "a" "a!1" "G" "G!1" ))"2" (expand "subgroup?" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (replace -2)"2" (hide-all-but 1)"2" (expand "generated_by" )"2" (inst + "1" )"2" (assert ) (("2" (rewrite "expt_1" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" sets nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil finite_groups nil )nil group nil )"bool" group_def nil )"T" finite_groups nil )"[T, T -> T]" finite_groups nil )NOT const-decl "[bool -> bool]" booleans nil )"(partial_order?[set[T]])" nil )"[bool, bool -> bool]" booleans nil )"bool" reals nil )"boolean" notequal nil )"int" integers nil )nil real_axioms nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"nzint" integers nil )nil group nil )"[numfield -> numfield]" number_fields nil )"(total_order?[real])" nil )nil group nil )"int" integers nil )nil group nil )nil finite_sets nil )"bool" exists1 nil )"bool" function_inverse_def nil )nil function_inverse_def nil )nil function_inverse_defnil )"[below[N] -> T]" finite_groups nil )"(total_order?[real])" nil )"bool" functions nil )"[T -> boolean]" finite_groups nil )"(strict_total_order?[real])" real_props nil )"posnat" finite_groups nil )"(nonempty?[T])" finite_groups nil )"{n: nat | n = Card(S!1)}" finite_groups nil )"bool" functions nil )IF const-decl "[boolean, T, T -> T]" if_def nil )nil finite_sets nil )"(strict_total_order?[real])" real_props nil )"bool" functions nil )nil nat_types nil )"bool" group_def nil )nil group nil )"bool" group_def nil )nil group nil )nil sets_lemmas nil )"group" group nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil monad nil )nil group nil )nil group nil )"(divides(n))" divides nil )"(divides(m))" divides nil )nil real_props nil )nil real_types nil )"rat" rationals nil )"rat" rationals nil )"odd_int" integers nil )"nonneg_int" nil )"even_int" integersnil )"posint" nil )nil real_types nil )nil extra_real_propsnil )nil floor_ceil nil )"real" reals nil )nil real_props nil )nil reals nil )nil integers nil )"{i | i <= x & x < i + 1}" floor_ceil nil )"posnat" finite_groups nil )"int" finite_groups nil )"[numfield, nznum -> numfield]" number_fields nil )nil number_fields nil )"{x | 0 <= x & x < 1}" floor_ceil nil )"rat" rationals nil )"real" reals nil )"bool" sets nil )"[T, T -> boolean]" equalities nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil )nil naturalnumbers nil )"nat" finite_sets nil )"{n: nat | n = Card(S)}" finite_sets nil )"T" group nil ) (empty? const-decl "bool" sets nil )nil finite_sets nil )nil finite_sets nil )"bool" finite_sets nil )nil finite_sets nil )"bool" sets nil )nil group nil ))nil )nil 3293256444"" (skosimp*)"" (case "S!1(a!1)" )"1" (assert )"1" (typepred "G!1" )"1" (expand "finite_group?" )"1" (flatten)"1" (lemma "finite_subset" ("s" "S!1" "A" "G!1" ))"1" (assert )"1" (lemma "nonempty_card" ("S" "S!1" ))"1" (flatten -1)"1" (hide -2)"1" (case-replace "nonempty?(S!1)" )"1" "X" "{t: T | EXISTS (n: posnat): n <= card(S!1) AND t = a!1 ^ n}" )"1" (replace -1)"1" case "subset?(X,S!1)" )"1" "N" "card(S!1)" )"1" replace -1)"1" case "FORALL (n:posnat): n < N => a!1^n /= one" )"1" case "FORALL (i,j:posnat): i <= N & j <= N & i /= j => a!1^i /= a!1^j" )"1" "card_bij" "S" "X" "N" "N" ))"1" case "(EXISTS (f: [(X) -> below[N]]): bijective?(f))" )"1" replace -1 -2)"1" "1" "same_card_subset" "A" "X" "B" "S!1" ))"1" assert )nil nil ))nil ))nil ))nil )"2" "2" "F" "LAMBDA (n: below[N]): IF n = 0 THEN a!1 ^ N ELSE a!1 ^ n ENDIF") "2" case "bijective?[below[N],(X)](F)" )"1" "bijective_inv_exists[below[N],(X)]" "f" "F" ))"1" expand "exists1" )"1" "1" "1" "bij_inv_is_bij_alt[below[N],(X)]" "f" "F" "g" "x!1" ))"1" "x!1" )nil nil )"2" nil nil ))nil ))nil ))nil ))nil )"2" "2" replace -1)"2" "2" expand "X" "2" expand "F" "2" "x1!1=0" )"1" "N" )"1" assert )nil nil ))nil )"2" "x1!1" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" expand "F" 1)"2" "2" expand "bijective?" )"2" "1" expand "injective?" )"1" "1" "x1!1=0" )"1" assert )"1" "N" "x2!1" )"1" assert )nil nil ))nil ))nil )"2" assert )"2" "x2!1=0" )"1" "x1!1" "N" )"1" assert )nil nil ))nil )"2" assert )"2" "x1!1" "x2!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "surjective?" )"2" "2" "y!1" )"2" expand "X" "2" "2" "2" expand "<=" "2" "1" replace "1" "n!1" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil )"2" replace "2" replace "2" replace "2" "0" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" expand "X" 1)"3" expand "F" 1)"3" "3" replace "3" "x1!1" )"3" "x1!1=0" )"1" "N" )"1" assert )nil nil ))nil )"2" assert )"2" "x1!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "generated_is_subgroup" "a" "a!1" "G" "G!1" ))"2" expand "subgroup?" )"2" assert )"2" "finite_subset" "s" "X" "A" "S!1" ))"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "trichotomy" "x" "i!1-j!1" ))"2" "1" "cancel_right" "z" "a!1^(-j!1)" "x" "a!1^i!1" "y" "a!1^j!1" ))"1" rewrite "expt_mult" "1" rewrite "expt_mult" "1" assert )"1" "i!1-j!1" )"1" assert )"1" rewrite "expt_0" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert ) nil nil )"3" "cancel_right" "z" "a!1^(-i!1)" "x" "a!1 ^ i!1" "y" "a!1 ^ j!1" ))"3" rewrite "expt_mult" "3" rewrite "expt_mult" "3" assert )"3" "j!1-i!1" )"3" assert )"3" rewrite "expt_0" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" case "subset?(S!1,X)" )"1" "subset_antisymmetric" "a" "S!1" "b" "X" ))"1" (assert ) nil nil ))nil )"2" "2" expand "subset?" )"2" "2" expand "member" )"2" replace -6 1 rl)"2" expand "generated_by" )"2" assert )"2" replace "2" "2" "2" "n!1" )"2" case "EXISTS (k:below[N],j:int): i!1 = j*n!1+k" )"1" "1" "k!1" )"1" "k!1=0" )"1" replace "1" "expt_expt" "a" "a!1" "i" "n!1" "j" "j!1" ))"1" replace "1" assert )"1" replace "1" replace "1" "n!1" )"1" assert )"1" rewrite "one_expt" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" "expt_expt" "a" "a!1" "i" "n!1" "j" "j!1" ))"2" replace "2" assert )"2" rewrite "expt_mult" "2" replace "2" assert )"2" "k!1" )"2" assert )"2" rewrite "one_expt" )"2" assert )"2" rewrite "left_identity" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "2" "fractional(i!1/n!1)*n!1" "floor(i!1/n!1)" )"1" "real_parts" "x" "i!1/n!1" ))"1" rewrite "div_cancel3" nil nil ))nil )"2" "fractional(i!1 / n!1)" )"2" "n!1" )"2" "n!1" )"2" assert )"2" expand "fractional" )"2" "i!1 / n!1 * n!1 = i!1" )"1" assert )nil nil )"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 )"2" expand "subset?" )"2" replace -1 * rl)"2" "2" "2" expand "member" )"2" expand "generated_by" )"2" "2" replace -2 1)"2" replace -11 1)"2" "2" "n!1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "nonempty?" )"2" (expand "empty?" )"2" "a!1" )"2" assert )"2" expand "member" )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "generated_is_subgroup" "a" "a!1" "G" "G!1" ))"2" (expand "subgroup?" )"2" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil )"2" (replace -2)"2" (hide-all-but 1)"2" (expand "generated_by" )"2" (inst + "1" )"2" (assert ) (("2" (rewrite "expt_1" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil )nil group nil )"bool" group_def nil )nil group nil )nil group nil )nil group nil )"bool" group_def nil )nil group nil )"bool" group_def nil )nil group nil )"group" group nil )nil monad nil )nil group nil )nil group nil ) (^ const-decl "T" group nil )nil group nil ))nil 3407237584"" (skosimp*)"" "finite_generated_by_def" ("a" "a!1" "G" "G!1" "S" "S!1" ))"" (assert )"" (typepred "G!1" )"" (expand "finite_group?" )"" (flatten)"" "generated_is_subgroup" ("a" "a!1" "G" "G!1" ))"" (expand "subgroup?" )"" (assert )"" (lemma "finite_subset" ("s" "S!1" "A" "G!1" ))"" (assert )"" (name "N" "card(S!1)" )"" (replace -1)"" case "EXISTS (i:posnat): i < N AND a!1^i = one" )"1" "1" "B" "{t: T | EXISTS (n: posnat): n <= i!1 AND t = a!1 ^ n}" )"1" case "subset?(B,S!1)" )"1" "finite_subset" "s" "B" "A" "S!1" ))"1" assert )"1" "smaller_card_subset" "A" "B" "B" "S!1" ))"1" assert )"1" case "card(B) <= i!1" )"1" assert )"1" "1" replace -13 -2)"1" assert )"1" replace "1" assert )"1" "1" case "n!1<=i!1" )"1" "n!1" )"1" assert )nil nil ))nil )"2" "i!1" )"2" "euclid_nat" )"2" "n!1" "i!1" )"2" "2" case "r!1=0" )"1" replace "1" "expt_expt" "a" "a!1" "i" "i!1" "j" "q!1" ))"1" replace "1" rewrite "one_expt" )"1" replace "1" assert )"1" "i!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "r!1" )"1" "expt_mult" "a" "a!1" "i" "i!1*q!1" "j" "r!1" ))"1" "expt_expt" "a" "a!1" "i" "i!1" "j" "q!1" ))"1" replace "1" rewrite "one_expt" )"1" replace "1" rewrite "left_identity" )"1" replace "1" assert )nil nil ))nil ))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" rewrite "card_def" )"2" "Card_injection[T]" "S" "B" "n" "i!1" ))"2" "1" nil nil )"2" "2" "F" "lambda (i:below[i!1]): a!1^(i+1)" )"2" case "surjective?[below[i!1],(B)](F)" )"1" "i!1" )"1" "inj_inv[below[i!1],(B)]" "f" "F" ))"1" assert )"1" "inverse(F)" )"1" assert )"1" expand "injective?" )"1" "1" "x1!1" )"1" "x2!1" )"1" expand "restrict" )"1" "x1!1" "x2!1" )"1" assert )"1" expand "inverse" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "0" )nil nil ))nil ))nil )"2" "0" )nil nil ))nil ))nil )"2" "2" replace "2" expand "surjective?" )"2" "2" "y!1" )"2" replace "2" assert )"2" "2" "n!1=i!1" )"1" assert )"1" replace "1" replace "1" case "i!1=0" )"1" assert )nil nil )"2" "i!1-1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "n!1=0" )"1" assert )nil nil )"2" "n!1-1" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" replace "3" replace "3" "3" "x1!1" )"3" "x1!1+1" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "subset?" )"2" "2" assert )"2" replace -2 -1 rl)"2" replace -10 1)"2" assert )"2" "generated_by(a!1)" )"2" expand "group?" )"2" expand "monoid?" )"2" "2" assert )"2" expand "monad?" )"2" "2" expand "member" )"2" assert )"2" "2" "n!1=N" )"1" assert )nil nil )"2" "n!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 ))nil )"2" "generated_by(a!1)" )"2" expand "group?" )"2" expand "monoid?" )"2" "2" assert )"2" expand "monad?" )"2" "2" expand "member" )"2" replace -17 -2 rl)"2" replace -15 -2)"2" assert )"2" "2" "n!1=N" )"1" assert )nil nil )"2" "n!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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" sets nil )nil group nil )"bool" group_def nil )"T" finite_groups nil )"[T, T -> T]" finite_groups nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil finite_groups nil )nil finite_groups nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" group_def nil )nil finite_sets nil )"bool" finite_sets nil )nil finite_sets nil )"{n: nat | n = Card(S)}" finite_sets nil )"nat" finite_sets nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"[T, T -> boolean]" equalities nil )nil numbers nil )nil integers nil )"bool" reals nil )nil integers nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" reals nil ) (^ const-decl "T" group nil )"bool" reals nil )"group" group nil )"bool" monoid_def nil )"bool" monad_def nil )nil finite_sets nil )nil euclidean_division nil )"posnat" finite_groups nil )"mod(i!1)" finite_groups nil )nil monad nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )nil group nil )"nonneg_int" nil )"(divides(n))" divides nil )"(divides(m))" divides nil )"nonneg_int" nil )"(strict_total_order?[real])" real_props nil )nil group nil )nil group nil )nil euclidean_division nil )"(total_order?[real])" nil )nil finite_sets nil )"posint" nil )nil nat_types nil )"[numfield, numfield -> numfield]" number_fields nil )"int" integers nil )"[numfield, numfield -> numfield]" number_fields nil )"int" integers nil )"(total_order?[real])" nil )"posnat" finite_groups nil )"bool" functions nil )"R" restrict nil )"D" function_inverse nil )"bool" booleans nil )nil function_inverse nil )"bool" functions nil )nil finite_sets nil )"(strict_total_order?[real])" real_props nil )"bool" sets nil )"(partial_order?[set[T]])" nil )nil group nil )"bool" group_def nil )nil group nil )"bool" sets nil ))nil )nil 3397484484"" (auto-rewrite "member" )"" (skosimp*)"" "finite_generated_by_def" "a" "a!1" "G" "G!1" "S" "S!1" ))"" (assert )"" (typepred "G!1" )"" (expand "finite_group?" )"" (flatten)"" "generated_is_subgroup" ("a" "a!1" "G" "G!1" ))"" (expand "subgroup?" )"" (assert )"" "finite_subset" ("s" "S!1" "A" "G!1" ))"" (assert )"" (name "N" "card(S!1)" )"" (replace -1)"" case "EXISTS (i:posnat): i < N AND a!1^i = one" )"1" "1" "B" "{t: T | EXISTS (n: posnat): n <= i!1 AND t = a!1 ^ n}" )"1" case "subset?(B,S!1)" )"1" "finite_subset" "s" "B" "A" "S!1" ))"1" assert )"1" "smaller_card_subset" "A" "B" "B" "S!1" ))"1" assert )"1" case "card(B) <= i!1" )"1" assert )"1" "1" replace -13 -2)"1" assert )"1" replace "1" assert )"1" "1" case "n!1<=i!1" )"1" "n!1" )"1" assert )nil nil ))nil )"2" "i!1" )"2" "euclid_nat" )"2" "n!1" "i!1" )"2" "2" case "r!1=0" )"1" replace "1" "expt_expt" "a" "a!1" "i" "i!1" "j" "q!1" ))"1" replace "1" rewrite "one_expt" )"1" replace "1" assert )"1" "i!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "r!1" )"1" "expt_mult" "a" "a!1" "i" "i!1*q!1" "j" "r!1" ))"1" "expt_expt" "a" "a!1" "i" "i!1" "j" "q!1" ))"1" replace "1" rewrite "one_expt" )"1" replace "1" rewrite "left_identity" )"1" replace "1" assert )nil nil ))nil ))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" rewrite "card_def" )"2" "Card_injection[T]" "S" "B" "n" "i!1" ))"2" "1" nil nil )"2" "2" "F" "lambda (i:below[i!1]): a!1^(i+1)" )"2" case "surjective?[below[i!1],(B)](F)" )"1" "i!1" )"1" "inj_inv[below[i!1],(B)]" "f" "F" ))"1" assert )"1" "inv(F)" )"1" assert )"1" expand "injective?" )"1" "1" "x1!1" )"1" "x2!1" )"1" expand "restrict" )"1" "x1!1" "x2!1" )"1" assert )"1" expand "inv" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "0" )nil nil ))nil ))nil )"2" "0" )nil nil ))nil ))nil )"2" "2" replace "2" expand "surjective?" )"2" "2" "y!1" )"2" replace "2" assert )"2" "2" "n!1=i!1" )"1" assert )"1" replace "1" replace "1" case "i!1=0" )"1" assert )nil nil )"2" "i!1-1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "n!1=0" )"1" assert )nil nil )"2" "n!1-1" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" replace "3" replace "3" "3" "x1!1" )"3" "x1!1+1" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "subset?" )"2" "2" assert )"2" replace -2 -1 rl)"2" replace -10 1)"2" assert )"2" "generated_by(a!1)" )"2" expand "group?" )"2" expand "monoid?" )"2" "2" assert )"2" expand "monad?" )"2" "2" expand "member" )"2" assert )"2" "2" "n!1=N" )"1" assert )nil nil )"2" "n!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 ))nil )"2" "generated_by(a!1)" )"2" expand "group?" )"2" expand "monoid?" )"2" "2" assert )"2" expand "monad?" )"2" "2" expand "member" )"2" replace -17 -2 rl)"2" replace -15 -2)"2" assert )"2" "2" "n!1=N" )"1" assert )nil nil )"2" "n!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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil group nil )"bool" group_def nil )"bool" group_def nil )"T" group nil )"group" group nil )"bool" monoid_def nil )"bool" monad_def nil )nil monad nil )nil group nil )nil group nil )nil group nil )nil group nil )"bool" group_def nil )nil group nil ))nil )nil 3293491013"" (skosimp*)"" "finite_generated_by_def" ("a" "a!1" "G" "G!1" "S" "S!1" ))"" (assert )"" (typepred "G!1" )"" (expand "finite_group?" )"" (flatten)"" "generated_is_subgroup" ("a" "a!1" "G" "G!1" ))"" (expand "subgroup?" )"" (assert )"" (lemma "finite_subset" ("s" "S!1" "A" "G!1" ))"" (assert )"" (name "N" "card(S!1)" )"" (replace -1)"" case "EXISTS (i:posnat): i < N AND a!1^i = one" )"1" "1" "B" "{t: T | EXISTS (n: posnat): n <= i!1 AND t = a!1 ^ n}" )"1" case "subset?(B,S!1)" )"1" "finite_subset" "s" "B" "A" "S!1" ))"1" assert )"1" "smaller_card_subset" "A" "B" "B" "S!1" ))"1" assert )"1" case "card(B) <= i!1" )"1" assert )"1" "1" replace -13 -2)"1" assert )"1" replace "1" assert )"1" "1" case "n!1<=i!1" )"1" "n!1" )"1" assert )nil nil ))nil )"2" "i!1" )"2" "euclid_nat" )"2" "n!1" "i!1" )"2" "2" case "r!1=0" )"1" replace "1" "expt_expt" "a" "a!1" "i" "i!1" "j" "q!1" ))"1" replace "1" rewrite "one_expt" )"1" replace "1" assert )"1" "i!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "r!1" )"1" "expt_mult" "a" "a!1" "i" "i!1*q!1" "j" "r!1" ))"1" "expt_expt" "a" "a!1" "i" "i!1" "j" "q!1" ))"1" replace "1" rewrite "one_expt" )"1" replace "1" rewrite "left_identity" )"1" replace "1" assert )nil nil ))nil ))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" rewrite "card_def" )"2" "Card_injection[T]" "S" "B" "n" "i!1" ))"2" "1" nil nil )"2" "2" "F" "lambda (i:below[i!1]): a!1^(i+1)" )"2" case "surjective?[below[i!1],(B)](F)" )"1" "i!1" )"1" "inj_inv[below[i!1],(B)]" "f" "F" ))"1" assert )"1" "inv(F)" )"1" assert )"1" expand "injective?" )"1" "1" "x1!1" )"1" "x2!1" )"1" expand "restrict" )"1" "x1!1" "x2!1" )"1" assert )"1" expand "inv" )"1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "0" )nil nil ))nil ))nil )"2" "0" )nil nil ))nil ))nil )"2" "2" replace "2" expand "surjective?" )"2" "2" "y!1" )"2" replace "2" assert )"2" "2" "n!1=i!1" )"1" assert )"1" replace "1" replace "1" case "i!1=0" )"1" assert )nil nil )"2" "i!1-1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "n!1=0" )"1" assert )nil nil )"2" "n!1-1" )"1" assert )nil nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"3" "3" replace "3" replace "3" "3" "x1!1" )"3" "x1!1+1" )"3" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "subset?" )"2" "2" assert )"2" replace -2 -1 rl)"2" replace -10 1)"2" assert )"2" "generated_by(a!1)" )"2" expand "group?" )"2" expand "monoid?" )"2" "2" assert )"2" expand "monad?" )"2" "2" expand "member" )"2" assert )"2" "2" "n!1=N" )"1" assert )nil nil )"2" "n!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 ))nil )"2" "generated_by(a!1)" )"2" expand "group?" )"2" expand "monoid?" )"2" "2" assert )"2" expand "monad?" )"2" "2" expand "member" )"2" replace -17 -2 rl)"2" replace -15 -2)"2" assert )"2" "2" "n!1=N" )"1" assert )nil nil )"2" "n!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 ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" group_def nil )"bool" group_def nil )"T" group nil )"group" group nil )"bool" monoid_def nil )"bool" monad_def nil )nil monad nil )nil group nil )nil group nil )nil group nil )nil group nil )"bool" group_def nil )nil group nil ))nil 3397224769"" (skosimp*)"" (lemma "finite_generated_by" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil )nil finite_groups nil )"bool" sets nil )nil group nil )"bool" group_def nil )"T" finite_groups nil )"[T, T -> T]" finite_groups nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil finite_groups nil ))nil ))nil 3397224781"" (skosimp*)"" (lemma "generated_by_lem" )"" (inst - "a!1" "0" )"" (expand "^" )"" (expand "power" )"" (assert )"" (lemma "card_one[T]" )"" (inst?)"" (assert )"" (skosimp*)"" (replace -1)"" (expand "singleton" )"" (assert )"" (replace -2 * rl)"" "generated_by_lem" )"" "a!1" "1" )"" expand "^" )"" expand "power" )"" expand "power" )"" assert )"" "right_identity" )"" "" assert )"" replace -1)"" "" replace -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 )"T" finite_groups nil )"[T, T -> T]" finite_groups nil )nil finite_groups nil )nil group nil )"T" group nil ) (member const-decl "bool" sets nil )"group" group nil )nil group nil )"bool" group_def nil )nil finite_sets nil )"bool" finite_sets nil )set type-eq-decl nil sets nil )nil booleans nil )"(singleton?)" sets nil )nil monad nil )nil finite_sets nil )"T" monoid_def nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil booleans nil )nil numbers nil ))nil ))nil 3293215122"" (skosimp*)"" "finite_generated_by_def" "a" "a!1" "G" "G!1" "S" "generated_by(a!1)" ))"1" (assert )"1" (expand "finite_order?" )"1" (expand "infinite_order?" )"1" (typepred "generated_by(a!1)" )"1" (expand "group?" )"1" (expand "monoid?" )"1" (flatten)"1" (assert )"1" (expand "monad?" )"1" (flatten)"1" (expand "member" )"1" (replace -6 -2)"1" assert )"1" "1" "n!1" )"1" "n!1" )"1" expand "^" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "nonempty?" )"2" (expand "empty?" )"2" (inst - "a!1" )"2" (expand "generated_by" )"2" (assert )"2" (expand "member" )"2" (inst + "1" ) (("2" (rewrite "expt_1" ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"group" group nil )nil group nil )"bool" group_def nil )"bool" sets nil )nil group nil )"bool" group_def nil )"T" finite_groups nil )"[T, T -> T]" finite_groups nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil finite_groups nil )nil finite_groups nil )"bool" monoid_def nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" monoid_def nil )"(total_order?[real])" nil )"(strict_total_order?[real])" real_props nil )"T" group nil )nil integers nil )nil integers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )"bool" reals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"bool" monad_def nil )"bool" monoid_def nil )"bool" sets nil )"bool" sets nil )nil group nil ))nil 3293196354"" (expand "nonempty?" )"" (expand "empty?" )"" (expand "member" )"" (skosimp*)"" "finite_generated_by_def" "a" "a!1" "G" "G!1" "S" "generated_by(a!1)" ))"1" (typepred "a!1" )"1" (expand "member" )"1" (typepred "generated_by(a!1)" )"1" (expand "group?" )"1" (expand "monoid?" )"1" (expand "monad?" )"1" (expand "groupoid?" )"1" (flatten)"1" (expand "member" )"1" replace -7 -2)"1" assert )"1" "1" "n!1" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "nonempty?" )"2" (expand "empty?" )"2" (expand "member" )"2" (expand "generated_by" )"2" (hide -2)"2" (inst - "a!1" )"2" (inst + "1" )"2" (rewrite "expt_1" ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" sets nil )nil group nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" monoid_def nil )"(total_order?[real])" nil )nil numbers nil )"[number -> boolean]" number_fieldsnil )nil number_fields nil )"[number_field -> boolean]" reals nil )nil reals nil )"[real -> boolean]" rationals nil )nil rationals nil )"[rational -> boolean]" integers nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" monad_def nil )nil finite_groups nil )nil finite_groups nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )"[T, T -> T]" finite_groups nil )"T" finite_groups nil )"bool" group_def nil )nil group nil )"bool" group_def nil )nil group nil )"group" group nil )"bool" sets nil )"bool" sets nil ))nil 3293312025"" (expand "member" ) (("" (skosimp) nil nil )) nil )"bool" sets nil )) shostak))nil 3293051767"" (skosimp*)"" (name "N" "period(G!1, a!1)" )"1" (typepred "period(G!1, a!1)" )"1" (replace -2)"1" (expand "period" )"1" (expand "member" )"1" "finite_generated_by_def" "a" "a!1" "G" "G!1" "S" "generated_by(a!1)" ))"1" (split -1)"1" (assert ) nil nil ) ("2" (assert ) nil nil )"3" (propax) nil nil ))nil )"2" (expand "nonempty?" )"2" (expand "empty?" )"2" (inst - "a!1" )"2" (expand "member" )"2" (expand "generated_by" )"2" (inst + "1" ) (("2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (assert )"2" (expand "member" ) (("2" (propax) nil nil )) nil )) nil ))nil ))nil )"posnat" finite_groups nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"bool" group_def nil )set type-eq-decl nil sets nil )nil booleans nil )nil group nil )"T" finite_groups nil )"[T, T -> T]" finite_groups nil )nil finite_groups nil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil numbers nil )"bool" sets nil )"bool" sets nil )"(strict_total_order?[real])" real_props nil )"group" group nil )nil group nil )"bool" group_def nil )"bool" sets nil )nil finite_groups nil )NOT const-decl "[bool -> bool]" booleans nil ))nil 3293050784"" (skolem!)"" (rewrite "subgroup_def" )"" (prop)"" (expand "inv_closed?" )"" (skolem!)"" (assert )"" (typepred "x!1" )"" (case "G!1(x!1)" )"1" (lemma "a_hat_period" ("a" "x!1" "G" "G!1" ))"1" (name "NN" "period(G!1,x!1)" )"1" (assert )"1" (typepred "period(G!1,x!1)" )"1" (replace -2)"1" "expt_def2" "a" "x!1" "i" "NN-1" ))"1" "expt_def1" "a" "x!1" "i" "NN-1" ))"1" "unique_inv" "x" "x!1" "y" "x!1^(NN-1)" ))"1" assert )"1" "NN=1" )"1" assert )"1" rewrite "expt_0" )"1" rewrite "expt_1" )"1" assert )"1" rewrite "left_identity" )"1" rewrite "right_identity" )"1" expand "member" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" case "FORALL (n:posnat): S!1(x!1^n)" )"1" "NN-1" )"1" assert )"1" expand "member" )"1" (assert ) nil nil ))nil ))nil )"2" (assert ) nil nil ))nil )"2" "2" "n" )"1" (assert ) nil nil )"2" (assert ) nil nil )"3" "3" "j!1=0" )"1" assert )"1" rewrite "expt_1" )nil nil ))nil )"2" rewrite "expt_def1" "2" assert )"2" expand "star_closed?" )"2" "x!1^j!1" "x!1" )"2" assert )"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 )"2" (propax) nil nil ))nil ))nil )"2" (expand "subset?" )"2" (inst - "x!1" )"2" (assert )"2" (expand "member" )"2" (propax) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil group nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )"bool" group_def nil )nil group nil )"bool" group_def nil )nil group nil )"bool" sets nil )nil finite_groups nil )"[T, T -> T]" finite_groups nil )"T" finite_groups nil )"(partial_order?[set[T]])" nil )"bool" group nil )"bool" sets nil )"posnat" finite_groups nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"[T, T -> boolean]" equalities nil )nil numbers nil )"int" integers nil )nil group nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil group nil )"T" group nil ) (expt_0 formula-decl nil group nil )nil monad nil )nil monad nil )nil group nil )"even_int" integersnil )"bool" groupoid_def nil )"posint" nil )"odd_int" integers nil )"posint" nil )nil naturalnumbers nil )nil naturalnumbers nil )nil defined_types nil )"[bool, bool -> bool]" booleans nil )"(total_order?[real])" nil )"posnat" finite_groups nil )"int" integers nil )"(strict_total_order?[real])" real_props nil )nil group nil )nil finite_groups nil )"bool" sets nil )NOT const-decl "[bool -> bool]" booleans nil ))nil 3407082430"" (skosimp*)"" (lemma "same_card_subset[T]" )"" (expand "order" )"" (expand "subgroup?" )"" (flatten)"" (inst - "H!1" "G!1" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )nil finite_groups nil )nil finite_sets nil )"bool" group_def nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )"bool" finite_sets nil )nil finite_sets nil )"[T, T -> T]" finite_groups nil )"T" finite_groups nil )"bool" group_def nil )nil group nil )"(partial_order?[set[T]])" nil )"posnat" monad nil ))nil ))nil 3293495877"" (expand "member" )"" (skosimp*)"" (use "generated_is_subgroup" )"" (expand "member" )"" (assert )"" (typepred "G!1" )"" (lemma "finite_subgroups" )"" (inst?)"" (assert )"" (expand "finite_group?" )"" (expand "finite_monad?" )"" (assert )"" (typepred "generated_by(a!1)" )"" (expand "group?" )"" expand "monoid?" )"" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )NOT const-decl "[bool -> bool]" booleans nil )"group" group nil )"bool" monoid_def nil )"bool" monad_def nil )nil group nil )nil booleans nil )nil booleans nil )set type-eq-decl nil sets nil )"bool" group_def nil )nil group nil )"bool" group_def nil )nil group nil )"T" finite_groups nil )"[T, T -> T]" finite_groups nil )nil finite_groups nil )nil group nil )"bool" sets nil ))nil 3406397797"" (skosimp*)"" (name "M" "period(G!1, a!1)" )"" (replace -1)"" (lemma "generated_is_subgroup" ("a" "a!1" "G" "G!1" ))"" (assert )"" (lemma "Lagrange" ("H" "generated_by(a!1)" "G" "G!1" ))"1" (assert )"1" (typepred "period(G!1, a!1)" )"1" (replace -4)"1" (expand "period" )"1" "min({n: posnat | a!1 ^ n = one})" )"1" (replace -7)"1" "finite_generated_by_one" "a" "a!1" "G" "G!1" "S" "generated_by(a!1)" ))"1" (assert )"1" expand "order" )"1" "N" "card(generated_by(a!1))" )"1" replace -1)"1" "nonempty_card" "S" "generated_by(a!1)" ))"1" replace -2)"1" case "generated_by(a!1)(a!1)" )"1" "1" "1" "1" "N" )"1" assert )"1" case "EXISTS (n:nat,m:below[M]): M*n+m = N" )"1" "1" "m!1" )"1" "expt_mult" "a" "a!1" "i" "M*n!1" "j" "m!1" ))"1" replace "1" replace "1" rewrite "expt_expt" "1" replace "1" rewrite "one_expt" )"1" case "m!1=0" )"1" case "n!1=1" )"1" assert )nil nil )"2" replace "2" "X" "generated_by(a!1)" )"2" replace "2" "finite_generated_by_def" "a" "a!1" "G" "G!1" "S" "X" ))"1" assert )"1" "card_bij_inv" "S" "X" "N" "M" ))"1" "1" "1" "1" assert )nil nil )"2" "lambda (i:below[M]): a!1^(i+1)" )"1" expand "bijective?" )"1" "1" expand "injective?" )"1" "1" "x1!1" )"1" "x2!1" )"1" "trich_lt" "x" "x1!1" "y" "x2!1" ))"1" "1" "cancel_right" "z" "a!1^(x2!1-x1!1)" "x" "a!1 ^ (1 + x1!1)" "y" "a!1 ^ (1 + x2!1)" ))"1" rewrite "expt_mult" "1" assert )"1" expand "subgroup?" )"1" "generated_by(a!1)" )"1" expand "group?" )"1" "1" expand "monoid?" )"1" "1" "cancel_left" "z" "a!1^(-(1+x2!1))" "x" "a!1 ^ (1 + x2!1)" "y" "a!1 ^ (1 + x2!1) * a!1 ^ (x2!1 - x1!1)" ))"1" "expt_mult" "a" "a!1" "i" "-(1+x2!1)" "j" "1+x2!1" ))"1" "1" rewrite "expt_0" "1" replace "1" rewrite "associative" "1" replace "1" assert )"1" "x2!1-x1!1" )"1" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil )"3" "cancel_right" "z" "a!1^(x1!1-x2!1)" "x" "a!1 ^ (1 + x1!1)" "y" "a!1 ^ (1 + x2!1)" ))"3" "expt_mult" "a" "a!1" "i" "1+x2!1" "j" "x1!1-x2!1" ))"3" "3" replace "3" replace "3" "3" "cancel_left" "z" "a!1^(-(1+x1!1))" "x" "a!1 ^ (1 + x1!1) * a!1 ^ (x1!1 - x2!1)" "y" "a!1 ^ (1 + x1!1)" ))"3" "expt_mult" "a" "a!1" "i" "-(1+x1!1)" "j" "1+x1!1" ))"3" rewrite "expt_0" "3" rewrite "associative" "3" replace "3" replace "3" replace "3" rewrite "left_identity" )"3" "x1!1-x2!1" )"1" assert )nil nil )"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 )"2" expand "surjective?" )"2" "2" "y!1" )"2" replace "2" "2" "2" case "EXISTS (n: nat, m: below[M]): M * n + m = n!2" )"1" "1" replace "1" "m!2=0" )"1" assert )"1" rewrite "expt_expt" "1" replace "1" replace "1" assert )"1" "M-1" )"1" assert )"1" replace "1" rewrite "one_expt" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "expt_mult" "2" rewrite "expt_expt" "2" replace "2" assert )"2" replace "2" "m!2-1" )"2" assert )"2" replace "2" rewrite "one_expt" )"2" rewrite "left_identity" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "euclid_nat" "a" "n!2" "b" "M" ))"2" "2" "q!1" "r!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" "2" "i!1" )"2" replace "2" "1+i!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "nonempty?" )"2" expand "empty?" )"2" "a!1" )"2" replace "2" expand "generated_by" )"2" assert )"2" "1" )"2" rewrite "expt_1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "m!1" )"1" assert )nil nil )"2" rewrite "left_identity" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "euclid_nat" "a" "N" "b" "M" ))"2" "2" "q!1" "r!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "nonempty?" )"2" expand "empty?" )"2" "a!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "generated_by" )"2" "1" )"2" assert )"2" rewrite "expt_1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "nonempty?" )"2" expand "empty?" )"2" "a!1" )"2" expand "generated_by" )"2" assert )"2" "1" )"2" rewrite "expt_1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "nonempty?" )"2" (expand "empty?" )"2" (expand "member" )"2" "M" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "subgroup?" )"2" (typepred "G!1" )"2" "finite_subset" "s" "generated_by(a!1)" "A" "G!1" ))"1" (assert )"1" (typepred "generated_by[T, *, one](a!1)" )"1" (expand "finite_group?" )"1" (propax) nil nil )) nil ))nil ))nil )"2" (expand "finite_group?" )"2" (flatten) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"posnat" finite_groups nil )nil integers nil )"bool" reals nil )nil integers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )"bool" group_def nil )set type-eq-decl nil sets nil )nil booleans nil )nil group nil )"T" finite_groups nil )"[T, T -> T]" finite_groups nil )nil finite_groups nil )"[T, T -> boolean]" equalities nil )nil booleans nil )nil numbers nil )nil group nil )"bool" group_def nil )nil group nil )nil lagrange nil )"group" group nil )NOT const-decl "[bool -> bool]" booleans nil )"(strict_total_order?[real])" real_props nil )"bool" finite_sets nil )nil finite_sets nil )nil naturalnumbers nil )"nat" finite_sets nil )"{n: nat | n = Card(S)}" finite_sets nil )nil finite_sets nil )"T" finite_groups nil )"{n: nat | n = Card[T](generated_by(a!1))}" nil )"nonneg_int" nil )"bool" reals nil )nil nat_types nil )nil number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )"[numfield, numfield -> numfield]" number_fields nil )nil group nil )nil group nil )"below[M]" finite_groups nil )"(strict_total_order?[real])" real_props nil )nil monad nil )nil finite_groups nil )nil finite_sets nil )"posint" nil )"posnat" finite_groups nil )"group[T, *, one]" finite_groups nil )"int" integers nil )"bool" group_def nil )"bool" monoid_def nil )"nzint" integers nil )nil group nil )"[numfield -> numfield]" number_fields nil )"(total_order?[real])" nil )"(partial_order?[set[T]])" nil )nil semigroup nil )nil group nil )"[numfield, numfield -> numfield]" number_fields nil )nil group nil )"posint" nil )"int" integers nil )"below[M]" finite_groups nil )"below[M]" finite_groups nil )nil real_props nil )"bool" functions nil )nil euclidean_division nil )nil euclidean_division nil )"bool" functions nil )"bool" functions nil )"(total_order?[real])" nil )"bool" sets nil )nil group nil )nil group nil )"(divides(m))" divides nil )"(divides(n))" divides nil )"nonneg_int" nil )"posnat" monad nil )nil finite_groups nil )"T" group nil )min const-decl"{a: posnat | S(a) AND (FORALL x: S(x) IMPLIES a <= x)}" "ints/" )"bool" reals nil )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" sets nil )nil finite_sets nil )"bool" sets nil ))nil )nil 3308047519"" (skosimp*)"" (name "M" "period(G!1, a!1)" )"" (replace -1)"" (lemma "generated_is_subgroup" ("a" "a!1" "G" "G!1" ))"" (assert )"" (lemma "lagrange" ("H" "generated_by(a!1)" "G" "G!1" ))"1" (assert )"1" (typepred "period(G!1, a!1)" )"1" (replace -4)"1" (expand "period" )"1" "min({n: posnat | a!1 ^ n = one})" )"1" (replace -7)"1" "finite_generated_by_one" "a" "a!1" "G" "G!1" "S" "generated_by(a!1)" ))"1" (assert )"1" expand "order" )"1" "N" "card(generated_by(a!1))" )"1" replace -1)"1" "nonempty_card" "S" "generated_by(a!1)" ))"1" replace -2)"1" case "generated_by(a!1)(a!1)" )"1" "1" "1" "1" "N" )"1" assert )"1" case "EXISTS (n:nat,m:below[M]): M*n+m = N" )"1" "1" "m!1" )"1" "expt_mult" "a" "a!1" "i" "M*n!1" "j" "m!1" ))"1" replace "1" replace "1" rewrite "expt_expt" "1" replace "1" rewrite "one_expt" )"1" case "m!1=0" )"1" case "n!1=1" )"1" assert )nil nil )"2" replace "2" "X" "generated_by(a!1)" )"2" replace "2" "finite_generated_by_def" "a" "a!1" "G" "G!1" "S" "X" ))"1" assert )"1" "card_bij_inv" "S" "X" "N" "M" ))"1" "1" "1" "1" assert )nil nil )"2" "lambda (i:below[M]): a!1^(i+1)" )"1" expand "bijective?" )"1" "1" expand "injective?" )"1" "1" "x1!1" )"1" "x2!1" )"1" "trich_lt" "x" "x1!1" "y" "x2!1" ))"1" "1" "cancel_right" "z" "a!1^(x2!1-x1!1)" "x" "a!1 ^ (1 + x1!1)" "y" "a!1 ^ (1 + x2!1)" ))"1" rewrite "expt_mult" "1" assert )"1" expand "subgroup?" )"1" "generated_by(a!1)" )"1" expand "group?" )"1" "1" expand "monoid?" )"1" "1" "cancel_left" "z" "a!1^(-(1+x2!1))" "x" "a!1 ^ (1 + x2!1)" "y" "a!1 ^ (1 + x2!1) * a!1 ^ (x2!1 - x1!1)" ))"1" "expt_mult" "a" "a!1" "i" "-(1+x2!1)" "j" "1+x2!1" ))"1" "1" rewrite "expt_0" "1" replace "1" rewrite "associative" "1" replace "1" assert )"1" "x2!1-x1!1" )"1" assert )"1" rewrite "left_identity" )"1" replace "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil )"3" "cancel_right" "z" "a!1^(x1!1-x2!1)" "x" "a!1 ^ (1 + x1!1)" "y" "a!1 ^ (1 + x2!1)" ))"3" "expt_mult" "a" "a!1" "i" "1+x2!1" "j" "x1!1-x2!1" ))"3" "3" replace "3" replace "3" "3" "cancel_left" "z" "a!1^(-(1+x1!1))" "x" "a!1 ^ (1 + x1!1) * a!1 ^ (x1!1 - x2!1)" "y" "a!1 ^ (1 + x1!1)" ))"3" "expt_mult" "a" "a!1" "i" "-(1+x1!1)" "j" "1+x1!1" ))"3" rewrite "expt_0" "3" rewrite "associative" "3" replace "3" replace "3" replace "3" rewrite "left_identity" )"3" "x1!1-x2!1" )"1" assert )nil nil )"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 )"2" expand "surjective?" )"2" "2" "y!1" )"2" replace "2" "2" "2" case "EXISTS (n: nat, m: below[M]): M * n + m = n!2" )"1" "1" replace "1" "m!2=0" )"1" assert )"1" rewrite "expt_expt" "1" replace "1" replace "1" assert )"1" "M-1" )"1" assert )"1" replace "1" rewrite "one_expt" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "expt_mult" "2" rewrite "expt_expt" "2" replace "2" assert )"2" replace "2" "m!2-1" )"2" assert )"2" replace "2" rewrite "one_expt" )"2" rewrite "left_identity" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "euclid_nat" "a" "n!2" "b" "M" ))"2" "2" "q!1" "r!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" "2" "i!1" )"2" replace "2" "1+i!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "nonempty?" )"2" expand "empty?" )"2" "a!1" )"2" replace "2" expand "generated_by" )"2" assert )"2" expand "member" )"2" "1" )"2" rewrite "expt_1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "m!1" )"1" assert )"1" rewrite "left_identity" )nil nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "euclid_nat" "a" "N" "b" "M" ))"2" "2" "q!1" "r!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "nonempty?" )"2" expand "empty?" )"2" "a!1" )"2" assert )"2" expand "member" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "generated_by" )"2" "1" )"2" assert )"2" rewrite "expt_1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "nonempty?" )"2" expand "empty?" )"2" "a!1" )"2" expand "generated_by" )"2" assert )"2" expand "member" )"2" "1" )"2" rewrite "expt_1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "nonempty?" )"2" (expand "empty?" )"2" (expand "member" )"2" "M" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "subgroup?" )"2" (typepred "G!1" )"2" "finite_subset" "s" "generated_by(a!1)" "A" "G!1" ))"1" (assert )"1" (typepred "generated_by[T, *, one](a!1)" )"1" (expand "finite_group?" )"1" (propax) nil nil )) nil ))nil ))nil )"2" (expand "finite_group?" )"2" (flatten) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" group_def nil )nil group nil )"bool" group_def nil )nil group nil )"group" group nil )nil group nil )nil group nil )"bool" group_def nil )"bool" monoid_def nil )nil group nil )nil monad nil )nil semigroup nil )nil group nil )nil group nil )nil group nil )nil group nil )"T" group nil ))nil )nil 3293308323"" (skosimp*)"" (name "M" "period(G!1, a!1)" )"" (replace -1)"" (lemma "generated_is_subgroup" ("a" "a!1" "G" "G!1" ))"" (assert )"" (lemma "lagrange" ("H" "generated_by(a!1)" "G" "G!1" ))"1" (assert )"1" (typepred "period(G!1, a!1)" )"1" (replace -4)"1" (expand "period" )"1" "min({n: posnat | a!1 ^ n = one})" )"1" (replace -7)"1" "finite_generated_by_one" "a" "a!1" "G" "G!1" "S" "generated_by(a!1)" ))"1" (assert )"1" expand "order" )"1" "N" "card(generated_by(a!1))" )"1" replace -1)"1" "nonempty_card" "S" "generated_by(a!1)" ))"1" replace -2)"1" case "generated_by(a!1)(a!1)" )"1" "1" "1" "1" "N" )"1" assert )"1" case "EXISTS (n:nat,m:below[M]): M*n+m = N" )"1" "1" "m!1" )"1" "expt_mult" "a" "a!1" "i" "M*n!1" "j" "m!1" ))"1" replace "1" replace "1" rewrite "expt_expt" "1" replace "1" rewrite "one_expt" )"1" case "m!1=0" )"1" case "n!1=1" )"1" assert )nil nil )"2" replace "2" "X" "generated_by(a!1)" )"2" replace "2" "finite_generated_by_def" "a" "a!1" "G" "G!1" "S" "X" ))"1" assert )"1" "card_bij_from" "S" "X" "N" "M" ))"1" "1" "1" "1" assert )nil nil )"2" "lambda (i:below[M]): a!1^(i+1)" )"1" expand "bijective?" )"1" "1" expand "injective?" )"1" "1" "x1!1" )"1" "x2!1" )"1" "trich_lt" "x" "x1!1" "y" "x2!1" ))"1" "1" "cancel_right" "z" "a!1^(x2!1-x1!1)" "x" "a!1 ^ (1 + x1!1)" "y" "a!1 ^ (1 + x2!1)" ))"1" rewrite "expt_mult" "1" assert )"1" expand "subgroup?" )"1" "generated_by(a!1)" )"1" expand "group?" )"1" "1" expand "monoid?" )"1" "1" "cancel_left" "z" "a!1^(-(1+x2!1))" "x" "a!1 ^ (1 + x2!1)" "y" "a!1 ^ (1 + x2!1) * a!1 ^ (x2!1 - x1!1)" ))"1" "expt_mult" "a" "a!1" "i" "-(1+x2!1)" "j" "1+x2!1" ))"1" "1" rewrite "expt_0" "1" replace "1" rewrite "associative" "1" replace "1" assert )"1" "x2!1-x1!1" )"1" assert )"1" rewrite "left_identity" )"1" replace "1" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" nil nil )"3" "cancel_right" "z" "a!1^(x1!1-x2!1)" "x" "a!1 ^ (1 + x1!1)" "y" "a!1 ^ (1 + x2!1)" ))"3" "expt_mult" "a" "a!1" "i" "1+x2!1" "j" "x1!1-x2!1" ))"3" "3" replace "3" replace "3" "3" "cancel_left" "z" "a!1^(-(1+x1!1))" "x" "a!1 ^ (1 + x1!1) * a!1 ^ (x1!1 - x2!1)" "y" "a!1 ^ (1 + x1!1)" ))"3" "expt_mult" "a" "a!1" "i" "-(1+x1!1)" "j" "1+x1!1" ))"3" rewrite "expt_0" "3" rewrite "associative" "3" replace "3" replace "3" replace "3" rewrite "left_identity" )"3" "x1!1-x2!1" )"1" assert )nil nil )"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 )"2" expand "surjective?" )"2" "2" "y!1" )"2" replace "2" "2" "2" case "EXISTS (n: nat, m: below[M]): M * n + m = n!2" )"1" "1" replace "1" "m!2=0" )"1" assert )"1" rewrite "expt_expt" "1" replace "1" replace "1" assert )"1" "M-1" )"1" assert )"1" replace "1" rewrite "one_expt" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" rewrite "expt_mult" "2" rewrite "expt_expt" "2" replace "2" assert )"2" replace "2" "m!2-1" )"2" assert )"2" replace "2" rewrite "one_expt" )"2" rewrite "left_identity" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "euclid_nat" "a" "n!2" "b" "M" ))"2" "2" "q!1" "r!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" replace "2" "2" "i!1" )"2" replace "2" "1+i!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "G!1" )"2" expand "finite_group?" )"2" "2" "finite_subset" "s" "X" "A" "G!1" ))"1" assert )"1" expand "subgroup?" )"1" nil nil ))nil ))nil )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "nonempty?" )"2" expand "empty?" )"2" "a!1" )"2" replace "2" expand "generated_by" )"2" assert )"2" expand "member" )"2" "1" )"2" rewrite "expt_1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "m!1" )"1" assert )"1" rewrite "left_identity" )nil nil ))nil )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" "2" "euclid_nat" "a" "N" "b" "M" ))"2" "2" "q!1" "r!1" )"2" assert )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "nonempty?" )"2" expand "empty?" )"2" "a!1" )"2" assert )"2" expand "member" )"2" nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" expand "generated_by" )"2" "1" )"2" assert )"2" rewrite "expt_1" )nil nil ))nil ))nil ))nil ))nil ))nil )"2" "finite_generated_by" )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "nonempty?" )"2" expand "empty?" )"2" "a!1" )"2" expand "generated_by" )"2" assert )"2" expand "member" )"2" "1" )"2" rewrite "expt_1" )nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "nonempty?" )"2" (expand "empty?" )"2" (expand "member" )"2" "M" )"2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (expand "subgroup?" )"2" (typepred "G!1" )"2" "finite_subset" "s" "generated_by(a!1)" "A" "G!1" ))"1" (assert )"1" (typepred "generated_by[T, *, one](a!1)" )"1" (expand "finite_group?" )"1" (propax) nil nil )) nil ))nil ))nil )"2" (expand "finite_group?" )"2" (flatten) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" group_def nil )nil group nil )"bool" group_def nil )nil group nil )"group" group nil )nil group nil )nil group nil )"bool" group_def nil )"bool" monoid_def nil )nil group nil )nil monad nil )nil semigroup nil )nil group nil )nil group nil )nil group nil )nil group nil )"T" group nil ))nil 3406397815"" (skosimp*)"" (lemma "period_is_generated_order" ("a" "a!1" "G" "G!1" ))"" (assert )"" (lemma "generated_is_subgroup" ("a" "a!1" "G" "G!1" ))"" (assert )"" (lemma "Lagrange" ("H" "generated_by(a!1)" "G" "G!1" ))"1" (assert ) nil nil )"2" (typepred "generated_by[T, *, one](a!1)" )"2" (typepred "G!1" )"2" (expand "finite_group?" )"2" (flatten)"2" (expand "subgroup?" )"2" "finite_subset" "s" "generated_by[T, *, one](a!1)" "A" "G!1" ))"1" (assert ) nil nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil group nil )"bool" group_def nil )"T" finite_groups nil )"[T, T -> T]" finite_groups nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil finite_groups nil )nil finite_groups nil )nil group nil )"bool" group_def nil )nil group nil )nil lagrange nil )"group" group nil )nil finite_sets nil )"bool" finite_sets nil )nil finite_sets nil )"(partial_order?[set[T]])" nil )"bool" group_def nil )NOT const-decl "[bool -> bool]" booleans nil )"bool" sets nil ))nil )nil 3293052104"" (skosimp*)"" (lemma "period_is_generated_order" ("a" "a!1" "G" "G!1" ))"" (assert )"" (lemma "generated_is_subgroup" ("a" "a!1" "G" "G!1" ))"" (assert )"" (lemma "lagrange" ("H" "generated_by(a!1)" "G" "G!1" ))"1" (assert ) nil nil )"2" (typepred "generated_by[T, *, one](a!1)" )"2" (typepred "G!1" )"2" (expand "finite_group?" )"2" (flatten)"2" (expand "subgroup?" )"2" "finite_subset" "s" "generated_by[T, *, one](a!1)" "A" "G!1" ))"1" (assert ) nil nil )"2" (propax) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" group_def nil )nil group nil )"bool" group_def nil )nil group nil )"group" group nil )"bool" group_def nil ))
Messung V0.5 in Prozent C=100 H=100 G=100
¤ 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.0.746Bemerkung:
(vorverarbeitet am 2026-04-26)
¤ *Bot Zugriff
2026-05-26
