| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/groups/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 149 kB |
|
Quellcode-Bibliothek group_action.prfSprache: Lisp |
|||||||||||||||
|
(group_action (IMP_group_TCC1 0 (IMP_group_TCC1-1 nil 3529777709 ("" (rewrite "fullset_is_group") nil nil) ((fullset_is_group formula-decl nil group_action nil)) nil)) (group_action?_TCC1 0 (group_action?_TCC1-1 nil 3529395416 ("" (skosimp) (("" (rewrite "one_in") nil nil)) nil) ((one_in formula-decl nil monad "algebra/") (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (monad? const-decl "bool" monad_def "algebra/") (monad nonempty-type-eq-decl nil monad "algebra/") (group? const-decl "bool" group_def "algebra/") (group nonempty-type-eq-decl nil group "algebra/") (T formal-type-decl nil group_action nil) (* formal-const-decl "[T, T -> T]" group_action nil) (one formal-const-decl "T" group_action nil)) nil)) (group_action?_TCC2 0 (group_action?_TCC2-1 nil 3529395416 ("" (skosimp) (("" (rewrite "product_in") nil nil)) nil) ((product_in formula-decl nil group "algebra/") (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (group? const-decl "bool" group_def "algebra/") (group nonempty-type-eq-decl nil group "algebra/") (T formal-type-decl nil group_action nil) (* formal-const-decl "[T, T -> T]" group_action nil) (one formal-const-decl "T" group_action nil)) nil)) (stabilizer_TCC1 0 (stabilizer_TCC1-1 nil 3529496770 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (T formal-type-decl nil group_action nil) (set type-eq-decl nil sets nil) (* formal-const-decl "[T, T -> T]" group_action nil) (one formal-const-decl "T" group_action nil) (group? const-decl "bool" group_def "algebra/") (group nonempty-type-eq-decl nil group "algebra/") (T1 formal-type-decl nil group_action nil) (inv_exists? const-decl "bool" group_def "algebra/") (monoid? const-decl "bool" monoid_def "algebra/") (associative? const-decl "bool" operator_defs nil) (monad? const-decl "bool" monad_def "algebra/") (identity? const-decl "bool" operator_defs nil) (left_identity formula-decl nil monad "algebra/") (restrict const-decl "R" restrict nil) (right_identity formula-decl nil monad "algebra/") (one_member formula-decl nil monad "algebra/") (star_closed? const-decl "bool" groupoid_def "algebra/") (G!1 skolem-const-decl "group[T, *, one]" group_action nil) (extend const-decl "R" extend nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil)) nil)) (orbit_TCC1 0 (orbit_TCC1-1 nil 3529607419 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (T formal-type-decl nil group_action nil) (set type-eq-decl nil sets nil) (* formal-const-decl "[T, T -> T]" group_action nil) (one formal-const-decl "T" group_action nil) (group? const-decl "bool" group_def "algebra/") (group nonempty-type-eq-decl nil group "algebra/") (T1 formal-type-decl nil group_action nil) (inv_exists? const-decl "bool" group_def "algebra/") (monoid? const-decl "bool" monoid_def "algebra/") (associative? const-decl "bool" operator_defs nil) (monad? const-decl "bool" monad_def "algebra/") (identity? const-decl "bool" operator_defs nil) (left_identity formula-decl nil monad "algebra/") (restrict const-decl "R" restrict nil) (right_identity formula-decl nil monad "algebra/") (one_member formula-decl nil monad "algebra/") (star_closed? const-decl "bool" groupoid_def "algebra/") (G!1 skolem-const-decl "group[T, *, one]" group_action nil) (extend const-decl "R" extend nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil)) nil)) (Fix_TCC1 0 (Fix_TCC1-1 nil 3529669814 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (T formal-type-decl nil group_action nil) (set type-eq-decl nil sets nil) (* formal-const-decl "[T, T -> T]" group_action nil) (one formal-const-decl "T" group_action nil) (group? const-decl "bool" group_def "algebra/") (group nonempty-type-eq-decl nil group "algebra/") (inv_exists? const-decl "bool" group_def "algebra/") (monoid? const-decl "bool" monoid_def "algebra/") (associative? const-decl "bool" operator_defs nil) (monad? const-decl "bool" monad_def "algebra/") (identity? const-decl "bool" operator_defs nil) (left_identity formula-decl nil monad "algebra/") (restrict const-decl "R" restrict nil) (right_identity formula-decl nil monad "algebra/") (one_member formula-decl nil monad "algebra/") (star_closed? const-decl "bool" groupoid_def "algebra/") (G!1 skolem-const-decl "group[T, *, one]" group_action nil) (extend const-decl "R" extend nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil)) nil)) (stabilizer_is_subgroup 0 (stabilizer_is_subgroup-1 nil 3529497669 ("" (skosimp*) (("" (lemma "subgroup_def") (("" (inst?) (("" (assert) (("" (hide 2) (("" (prop) (("1" (expand "nonempty?") (("1" (expand "empty?") (("1" (expand "member") (("1" (inst - "one") (("1" (expand "stabilizer") (("1" (expand "extend") (("1" (ground) (("1" (expand "group_action?") (("1" (inst -2 "one" "one" "x!1") (("1" (assert) nil nil)) nil)) nil) ("2" (rewrite "one_in") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "star_closed?") (("2" (expand "member") (("2" (skosimp*) (("2" (typepred "x!2" "y!1") (("2" (expand "stabilizer") (("2" (expand "extend") (("2" (ground) (("1" (expand "group_action?") (("1" (copy -6) (("1" (inst -7 "x!2" "y!1" "x!1") (("1" (flatten) (("1" (replaces -8) (("1" (replaces -4) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide (-2 -4 -5)) (("2" (rewrite "product_in") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "inv_closed?") (("3" (skosimp*) (("3" (expand "member") (("3" (typepred "x!2") (("3" (expand "stabilizer") (("3" (expand "extend") (("3" (ground) (("1" (expand "group_action?") (("1" (inst -4 "inv(x!2)" "x!2" "x!1") (("1" (flatten) (("1" (rewrite "inv_left") (("1" (assert) nil nil)) nil)) nil) ("2" (hide (-2 -3 2)) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (rewrite "inv_in") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((one formal-const-decl "T" group_action nil) (* formal-const-decl "[T, T -> T]" group_action nil) (T formal-type-decl nil group_action nil) (subgroup_def formula-decl nil group "algebra/") (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (empty? const-decl "bool" sets nil) (extend const-decl "R" extend nil) (monad nonempty-type-eq-decl nil monad "algebra/") (monad? const-decl "bool" monad_def "algebra/") (one_in formula-decl nil monad "algebra/") (group_action? const-decl "bool" group_action nil) (left_identity formula-decl nil monad "algebra/") (member const-decl "bool" sets nil) (nonempty? const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (product_in formula-decl nil group "algebra/") (star_closed? const-decl "bool" groupoid_def "algebra/") (inv_in formula-decl nil group "algebra/") (inv_left formula-decl nil group "algebra/") (AND const-decl "[bool, bool -> bool]" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (inv const-decl "{y | x * y = one AND y * x = one}" group "algebra/") (x!2 skolem-const-decl "(stabilizer(G!1, X!1)(f!1, x!1))" group_action nil) (x!1 skolem-const-decl "(X!1)" group_action nil) (f!1 skolem-const-decl "F(G!1, X!1)" group_action nil) (X!1 skolem-const-decl "set[T1]" group_action nil) (inv macro-decl "T" normal_subgroups "algebra/") (G!1 skolem-const-decl "group[T, *, one]" group_action nil) (inv_closed? const-decl "bool" group "algebra/") (stabilizer const-decl "{S: set[T] | subset?(S, G)}" group_action nil) (subset? const-decl "bool" sets nil) (F type-eq-decl nil group_action nil) (T1 formal-type-decl nil group_action nil) (group nonempty-type-eq-decl nil group "algebra/") (group? const-decl "bool" group_def "algebra/") (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) shostak)) (singleton_iff_Fix 0 (singleton_iff_Fix-1 nil 3529670185 ("" (skosimp*) (("" (prop) (("1" (expand* "member" "Fix") (("1" (expand "extend" 1) (("1" (skosimp) (("1" (case "EXISTS (g:(G!1)): f!1(g,x!1) /= x!1") (("1" (skosimp) (("1" (decompose-equality -1) (("1" (inst -1 "f!1(g!2,x!1)") (("1" (iff) (("1" (prop) (("1" (expand "extend") (("1" (expand "singleton") (("1" (propax) nil nil)) nil)) nil) ("2" (expand "orbit") (("2" (expand "extend") (("2" (hide (1 3 4)) (("2" (inst 1 "g!2") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1) (("2" (inst 1 "g!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand* "member" "Fix") (("2" (expand "extend") (("2" (decompose-equality 1) (("2" (iff) (("2" (prop) (("1" (expand "singleton") (("1" (expand "orbit") (("1" (expand "extend") (("1" (assert) (("1" (skosimp) (("1" (inst -3 "g!1") (("1" (replaces -3) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "orbit") (("2" (expand "extend") (("2" (assert) nil nil)) nil)) nil) ("3" (expand "orbit") (("3" (expand "extend") (("3" (assert) (("3" (expand "singleton") (("3" (inst 1 "one") (("1" (replace -2 1) (("1" (hide (-1 -2 -3)) (("1" (expand "group_action?") (("1" (inst -1 "one" "one" "x!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (rewrite "one_in") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((extend const-decl "R" extend nil) (F type-eq-decl nil group_action nil) (/= const-decl "boolean" notequal nil) (T1 formal-type-decl nil group_action nil) (group nonempty-type-eq-decl nil group "algebra/") (group? const-decl "bool" group_def "algebra/") (one formal-const-decl "T" group_action nil) (* formal-const-decl "[T, T -> T]" group_action nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil group_action nil) (= const-decl "[T, T -> boolean]" equalities nil) (subset? const-decl "bool" sets nil) (orbit const-decl "{Y: set[T1] | subset?(Y, X)}" group_action nil) (FALSE const-decl "bool" booleans nil) (singleton? const-decl "bool" sets nil) (singleton const-decl "(singleton?)" sets nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set[T]" countable_props "sets_aux/") (finite_extend application-judgement "finite_set[T]" extend_set_props nil) (nonempty_extend application-judgement "(nonempty?[T])" extend_set_props nil) (member const-decl "bool" sets nil) (Fix const-decl "{Y: set[T1] | subset?(Y, X)}" group_action nil) (G!1 skolem-const-decl "group[T, *, one]" group_action nil) (left_identity formula-decl nil monad "algebra/") (group_action? const-decl "bool" group_action nil) (one_in formula-decl nil monad "algebra/") (monad? const-decl "bool" monad_def "algebra/") (monad nonempty-type-eq-decl nil monad "algebra/") (IF const-decl "[boolean, T, T -> T]" if_def nil)) shostak)) (empty_iff_eq_Fix 0 (empty_iff_eq_Fix-1 nil 3529676365 ("" (skosimp*) (("" (prop) (("1" (decompose-equality 1) (("1" (iff) (("1" (prop) (("1" (expand "empty?") (("1" (inst -2 "orbit(G!1,X!1)(f!1,x!1)") (("1" (expand "member") (("1" (expand "orbits_nFix") (("1" (expand "extend") (("1" (prop) (("1" (inst 1 "x!1") nil nil) ("2" (expand "orbits") (("2" (inst 1 "x!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -2) (("2" (expand "Fix") (("2" (expand "extend") (("2" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "empty?") (("2" (skosimp) (("2" (expand "member") (("2" (expand "orbits_nFix") (("2" (expand "extend") (("2" (ground) (("2" (skosimp) (("2" (typepred "x!2") (("2" (expand "member") (("2" (replace -4 -1) (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((empty? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (extend const-decl "R" extend nil) (orbits const-decl "setofsets[T1]" group_action nil) (NOT const-decl "[bool -> bool]" booleans nil) (G!1 skolem-const-decl "group[T, *, one]" group_action nil) (f!1 skolem-const-decl "F(G!1, X!1)" group_action nil) (orbits_nFix const-decl "setofsets[T1]" group_action nil) (orbit const-decl "{Y: set[T1] | subset?(Y, X)}" group_action nil) (setof type-eq-decl nil defined_types nil) (x!1 skolem-const-decl "T1" group_action nil) (X!1 skolem-const-decl "set[T1]" group_action nil) (T1 formal-type-decl nil group_action nil) (boolean nonempty-type-decl nil booleans nil) (Fix const-decl "{Y: set[T1] | subset?(Y, X)}" group_action nil) (subset? const-decl "bool" sets nil) (F type-eq-decl nil group_action nil) (group nonempty-type-eq-decl nil group "algebra/") (group? const-decl "bool" group_def "algebra/") (one formal-const-decl "T" group_action nil) (* formal-const-decl "[T, T -> T]" group_action nil) (T formal-type-decl nil group_action nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil)) shostak)) (orbits_nFix_disj_Fix 0 (orbits_nFix_disj_Fix-1 nil 3529671855 ("" (skosimp*) (("" (expand "disjoint?") (("" (expand "empty?") (("" (skosimp*) (("" (expand "member") (("" (expand "intersection") (("" (flatten) (("" (expand "member") (("" (expand "Union") (("" (skosimp) (("" (typepred "a!1") (("" (expand "orbits_nFix") (("" (expand "extend") (("" (prop) (("" (skosimp) (("" (typepred "x!2") (("" (expand "member") (("" (replace -3 -6) (("" (expand "orbit" -6) (("" (expand "extend") (("" (prop) (("" (skosimp) (("" (case "orbit(G!1, X!1)(f!1, x!1)(x!2)") (("1" (lemma "singleton_iff_Fix") (("1" (inst?) (("1" (assert) (("1" (decompose-equality -1) (("1" (inst -1 "x!2") (("1" (iff) (("1" (prop) (("1" (expand* "extend" "singleton") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-2 -6 1)) (("2" (expand "orbit") (("2" (expand "extend") (("2" (replaces -1) (("2" (inst 1 "inv(g!1)") (("1" (expand "group_action?") (("1" (inst -1 "inv(g!1)" "g!1" "x!2") (("1" (assert) (("1" (flatten) (("1" (assert) nil nil)) nil)) nil) ("2" (lemma "inv_in") (("2" (inst?) (("2" (expand "inv") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -1) (("2" (lemma "inv_in") (("2" (inst -1 "G!1" "g!1") (("2" (expand "inv") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((disjoint? const-decl "bool" sets nil) (intersection const-decl "set" sets nil) (subset? const-decl "bool" sets nil) (Fix const-decl "{Y: set[T1] | subset?(Y, X)}" group_action nil) (G!1 skolem-const-decl "group[T, *, one]" group_action nil) (inv macro-decl "T" normal_subgroups "algebra/") (g!1 skolem-const-decl "(G!1)" group_action nil) (inv const-decl "{y | x * y = one AND y * x = one}" group "algebra/") (AND const-decl "[bool, bool -> bool]" booleans nil) (inv_left formula-decl nil group "algebra/") (inv_in formula-decl nil group "algebra/") (group_action? const-decl "bool" group_action nil) (singleton_iff_Fix formula-decl nil group_action nil) (nonempty_extend application-judgement "(nonempty?[T])" extend_set_props nil) (finite_extend application-judgement "finite_set[T]" extend_set_props nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set[T]" countable_props "sets_aux/") (= const-decl "[T, T -> boolean]" equalities nil) (FALSE const-decl "bool" booleans nil) (singleton? const-decl "bool" sets nil) (singleton const-decl "(singleton?)" sets nil) (orbit const-decl "{Y: set[T1] | subset?(Y, X)}" group_action nil) (extend const-decl "R" extend nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (T formal-type-decl nil group_action nil) (set type-eq-decl nil sets nil) (* formal-const-decl "[T, T -> T]" group_action nil) (one formal-const-decl "T" group_action nil) (group? const-decl "bool" group_def "algebra/") (group nonempty-type-eq-decl nil group "algebra/") (T1 formal-type-decl nil group_action nil) (F type-eq-decl nil group_action nil) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (orbits_nFix const-decl "setofsets[T1]" group_action nil) (Union const-decl "set" sets nil) (member const-decl "bool" sets nil) (empty? const-decl "bool" sets nil)) shostak)) (orbits_is_union 0 (orbits_is_union-1 nil 3529673700 ("" (skosimp*) (("" (decompose-equality 1) (("" (iff) (("" (prop) (("1" (expand* "union" "member") (("1" (flatten) (("1" (expand "Union") (("1" (skosimp) (("1" (typepred "a!1") (("1" (expand "orbits") (("1" (skosimp) (("1" (case "member(x!2, Fix(G!1, X!1)(f!1))") (("1" (hide 2) (("1" (lemma "singleton_iff_Fix") (("1" (inst?) (("1" (assert) (("1" (replaces -1) (("1" (replaces -2) (("1" (expand* "extend" "singleton") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst 3 "a!1") (("2" (expand "orbits_nFix") (("2" (expand "extend") (("2" (inst 1 "x!2") (("2" (expand "member") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand* "union" "member") (("2" (prop) (("1" (expand "Union") (("1" (lemma "singleton_iff_Fix") (("1" (inst -1 "G!1" "X!1" "x!1" "f!1") (("1" (assert) (("1" (inst 1 "orbit(G!1, X!1)(f!1, x!1)") (("1" (replaces -1) (("1" (expand* "extend" "singleton") (("1" (prop) (("1" (expand "Fix") (("1" (expand "extend") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "orbits") (("2" (inst 1 "x!1") nil nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (expand "Fix") (("2" (expand "extend") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "Union") (("2" (skosimp) (("2" (inst?) (("2" (typepred "a!1") (("2" (expand "orbits_nFix") (("2" (expand "extend") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((Union_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas nil) (bool nonempty-type-eq-decl nil booleans nil) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (set type-eq-decl nil sets nil) (Union const-decl "set" sets nil) (T formal-type-decl nil group_action nil) (* formal-const-decl "[T, T -> T]" group_action nil) (one formal-const-decl "T" group_action nil) (group? const-decl "bool" group_def "algebra/") (group nonempty-type-eq-decl nil group "algebra/") (F type-eq-decl nil group_action nil) (orbits const-decl "setofsets[T1]" group_action nil) (union const-decl "set" sets nil) (subset? const-decl "bool" sets nil) (Fix const-decl "{Y: set[T1] | subset?(Y, X)}" group_action nil) (orbits_nFix const-decl "setofsets[T1]" group_action nil) (boolean nonempty-type-decl nil booleans nil) (T1 formal-type-decl nil group_action nil) (singleton_iff_Fix formula-decl nil group_action nil) (singleton const-decl "(singleton?)" sets nil) (extend const-decl "R" extend nil) (x!2 skolem-const-decl "(X!1)" group_action nil) (a!1 skolem-const-decl "(orbits(G!1, X!1)(f!1))" group_action nil) (f!1 skolem-const-decl "F(G!1, X!1)" group_action nil) (X!1 skolem-const-decl "set[T1]" group_action nil) (G!1 skolem-const-decl "group[T, *, one]" group_action nil) (NOT const-decl "[bool -> bool]" booleans nil) (member const-decl "bool" sets nil) (orbit const-decl "{Y: set[T1] | subset?(Y, X)}" group_action nil) (x!1 skolem-const-decl "T1" group_action nil) (a!1 skolem-const-decl "(orbits_nFix(G!1, X!1)(f!1))" group_action nil)) shostak)) (orbit_nonempty 0 (orbit_nonempty-1 nil 3529385375 ("" (skosimp*) (("" (expand* "group_action?" "nonempty?" "empty?") (("" (inst -1 "one" "one" "x!1") (("1" (flatten) (("1" (hide -2) (("1" (inst -2 "x!1") (("1" (expand* "member" "orbit") (("1" (expand "extend") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (rewrite "one_in") nil nil)) nil)) nil)) nil) ((nonempty? const-decl "bool" sets nil) (empty? const-decl "bool" sets nil) (group_action? const-decl "bool" group_action nil) (monad nonempty-type-eq-decl nil monad "algebra/") (monad? const-decl "bool" monad_def "algebra/") (one_in formula-decl nil monad "algebra/") (extend const-decl "R" extend nil) (member const-decl "bool" sets nil) (orbit const-decl "{Y: set[T1] | subset?(Y, X)}" group_action nil) (T1 formal-type-decl nil group_action nil) (T formal-type-decl nil group_action nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (* formal-const-decl "[T, T -> T]" group_action nil) (one formal-const-decl "T" group_action nil) (group? const-decl "bool" group_def "algebra/") (group nonempty-type-eq-decl nil group "algebra/") (G!1 skolem-const-decl "group[T, *, one]" group_action nil)) shostak)) (orbits_nonempty 0 (orbits_nonempty-1 nil 3529397020 ("" (skosimp) (("" (expand "nonempty?" 1) (("" (expand "empty?") (("" (inst -3 "orbit(G!1,X!1)(f!1, choose(X!1))") (("" (expand "member") (("" (expand "orbits") (("" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nonempty? const-decl "bool" sets nil) (X!1 skolem-const-decl "set[T1]" group_action nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T1 formal-type-decl nil group_action nil) (setof type-eq-decl nil defined_types nil) (T formal-type-decl nil group_action nil) (* formal-const-decl "[T, T -> T]" group_action nil) (one formal-const-decl "T" group_action nil) (group? const-decl "bool" group_def "algebra/") (group nonempty-type-eq-decl nil group "algebra/") (F type-eq-decl nil group_action nil) (subset? const-decl "bool" sets nil) (orbit const-decl "{Y: set[T1] | subset?(Y, X)}" group_action nil) (choose const-decl "(p)" sets nil) (orbits const-decl "setofsets[T1]" group_action nil) (member const-decl "bool" sets nil) (empty? const-decl "bool" sets nil)) shostak)) (set_orbits_is 0 (set_orbits_is-1 nil 3529397173 ("" (skosimp*) (("" (decompose-equality 1) (("" (iff) (("" (prop) (("1" (expand "Union") (("1" (skosimp) (("1" (typepred "a!1") (("1" (expand "orbits") (("1" (skosimp) (("1" (replaces -1) (("1" (expand "orbit") (("1" (expand "extend") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "Union") (("2" (inst 1 "orbit(G!1,X!1)(f!1, x!1)") (("1" (expand "orbit") (("1" (expand "extend") (("1" (assert) (("1" (inst 1 "one") (("1" (expand "group_action?") (("1" (inst -2 "one" "one" "x!1") (("1" (assert) nil nil)) nil)) nil) ("2" (rewrite "one_in") nil nil)) nil)) nil)) nil)) nil) ("2" (expand "orbits") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((Union_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas nil) (bool nonempty-type-eq-decl nil booleans nil) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (set type-eq-decl nil sets nil) (Union const-decl "set" sets nil) (T formal-type-decl nil group_action nil) (* formal-const-decl "[T, T -> T]" group_action nil) (one formal-const-decl "T" group_action nil) (group? const-decl "bool" group_def "algebra/") (group nonempty-type-eq-decl nil group "algebra/") (F type-eq-decl nil group_action nil) (orbits const-decl "setofsets[T1]" group_action nil) (boolean nonempty-type-decl nil booleans nil) (T1 formal-type-decl nil group_action nil) (extend const-decl "R" extend nil) (orbit const-decl "{Y: set[T1] | subset?(Y, X)}" group_action nil) (NOT const-decl "[bool -> bool]" booleans nil) (X!1 skolem-const-decl "set[T1]" group_action nil) (x!1 skolem-const-decl "T1" group_action nil) (subset? const-decl "bool" sets nil) (f!1 skolem-const-decl "F(G!1, X!1)" group_action nil) (G!1 skolem-const-decl "group[T, *, one]" group_action nil) (left_identity formula-decl nil monad "algebra/") (group_action? const-decl "bool" group_action nil) (one_in formula-decl nil monad "algebra/") (monad? const-decl "bool" monad_def "algebra/") (monad nonempty-type-eq-decl nil monad "algebra/")) shostak)) (orbit_is_finite 0 (orbit_is_finite-1 nil 3529397499 ("" (skosimp*) (("" (lemma "finite_subset[T1]") (("" (inst -1 "X!1" "orbit(G!1, X!1)(f!1, x!1)") (("" (assert) nil nil)) nil)) nil)) nil) ((T1 formal-type-decl nil group_action nil) (finite_subset formula-decl nil finite_sets nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (orbit const-decl "{Y: set[T1] | subset?(Y, X)}" group_action nil) (subset? const-decl "bool" sets nil) (F type-eq-decl nil group_action nil) (group nonempty-type-eq-decl nil group "algebra/") (group? const-decl "bool" group_def "algebra/") (one formal-const-decl "T" group_action nil) (* formal-const-decl "[T, T -> T]" group_action nil) (T formal-type-decl nil group_action nil) (finite_set type-eq-decl nil finite_sets nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (is_finite const-decl "bool" finite_sets nil) (X!1 skolem-const-decl "set[T1]" group_action nil)) shostak)) (orbits_disjoint 0 (orbits_disjoint-1 nil 3529397883 ("" (skosimp*) (("" (expand "disjoint?") (("" (expand "empty?") (("" (skosimp) (("" (expand "intersection") (("" (expand "member") (("" (flatten) (("" (typepred "B!1") (("" (typepred "A!1") (("" (expand "orbits") (("" (skosimp*) (("" (replaces -1) (("" (replaces -1) (("" (expand "orbit") (("" (expand "extend" (-2 -3)) (("" (prop) (("" (hide (-1 -3)) (("" (skosimp*) (("" (decompose-equality 1) (("" (iff) (("" (prop) (("1" (expand "extend") (("1" (prop) (("1" (hide (-1 -2)) (("1" (skosimp) (("1" (expand "group_action?") (("1" (copy -4) (("1" (inst -5 "g!3" "inv(g!2)*g!2" "x!2") (("1" (copy -1) (("1" (inst -2 "inv(g!2)" "g!2" "x!2") (("1" (flatten) (("1" (replaces -3) (("1" (replaces -5) (("1" (replaces -4) (("1" (copy -1) (("1" (inst -1 "inv(g!2)" "g!1" "x!3") (("1" (flatten) (("1" (replace -2 -7 rl) (("1" (inst -3 "g!3" "inv(g!2) * g!1" "x!3") (("1" (flatten) (("1" (replace -4 -8 rl) (("1" (rewrite "inv_left") (("1" (rewrite "one_right") (("1" (replaces -8) (("1" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (lemma "inv_in") (("2" (inst -1 "G!1" "g!2") (("2" (assert) (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (lemma "inv_in") (("2" (inst -1 "G!1" "g!2") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (rewrite "one_in") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "extend") (("2" (prop) (("2" (hide (-1 -2)) (("2" (skosimp) (("2" (expand "group_action?") (("2" (copy -4) (("2" (inst -5 "g!3" "inv(g!1)*g!1" "x!3") (("1" (copy -1) (("1" (inst -2 "inv(g!1)" "g!1" "x!3") (("1" (flatten) (("1" (replaces -3) (("1" (replaces -5) (("1" (replace -4 -6 rl) (("1" (copy -1) (("1" (inst -1 "inv(g!1)" "g!2" "x!2") (("1" (flatten) (("1" (replace -2 -8 rl) (("1" (inst -3 "g!3" "inv(g!1) * g!2" "x!2") (("1" (flatten) (("1" (replace -4 -9 rl) (("1" (rewrite "inv_left") (("1" (rewrite "one_right") (("1" (replaces -9) (("1" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (lemma "inv_in") (("2" (inst -1 "G!1" "g!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (lemma "inv_in") (("2" (inst -1 "G!1" "g!1") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (rewrite "one_in") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((disjoint? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (orbits const-decl "setofsets[T1]" group_action nil) (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (F type-eq-decl nil group_action nil) (T1 formal-type-decl nil group_action nil) (group nonempty-type-eq-decl nil group "algebra/") (group? const-decl "bool" group_def "algebra/") (one formal-const-decl "T" group_action nil) (* formal-const-decl "[T, T -> T]" group_action nil) (set type-eq-decl nil sets nil) (T formal-type-decl nil group_action nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (orbit const-decl "{Y: set[T1] | subset?(Y, X)}" group_action nil) (g!1 skolem-const-decl "(G!1)" group_action nil) (group_action? const-decl "bool" group_action nil) (G!1 skolem-const-decl "group[T, *, one]" group_action nil) (inv const-decl "{y | x * y = one AND y * x = one}" group "algebra/") (AND const-decl "[bool, bool -> bool]" booleans nil) (inv_left formula-decl nil group "algebra/") (inv macro-decl "T" normal_subgroups "algebra/") (g!2 skolem-const-decl "(G!1)" group_action nil) (one_right formula-decl nil group "algebra/") (inv_in formula-decl nil group "algebra/") (monad nonempty-type-eq-decl nil monad "algebra/") (monad? const-decl "bool" monad_def "algebra/") (one_in formula-decl nil monad "algebra/") (FALSE const-decl "bool" booleans nil) (= const-decl "[T, T -> boolean]" equalities nil) (extend const-decl "R" extend nil) (intersection const-decl "set" sets nil) (empty? const-decl "bool" sets nil)) shostak)) (orbits_partition 0 (orbits_partition-1 nil 3529419630 ("" (skosimp*) (("" (expand "finite_partition?") (("" (prop) (("1" (expand "partition?") (("1" (skosimp*) (("1" (lemma "orbits_disjoint") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (lemma "set_orbits_is") (("2" (inst?) (("2" (assert) (("2" (case "is_finite(Union(orbits(G!1, X!1)(f!1)))") (("1" (hide -2) (("1" (lemma "Union_finite[T1]") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (hide (-3 2)) (("2" (replaces -1) nil nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "every") (("3" (skosimp) (("3" (typepred "x!1") (("3" (expand "orbits") (("3" (skosimp) (("3" (lemma "orbit_is_finite") (("3" (inst -1 "G!1" "X!1" "x!2" "f!1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((finite_partition? const-decl "bool" lagrange_scaf "algebra/") (every const-decl "bool" sets nil) (NOT const-decl "[bool -> bool]" booleans nil) (orbit_is_finite formula-decl nil group_action nil) (set_orbits_is formula-decl nil group_action nil) (Union_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas nil) (Union_finite formula-decl nil finite_sets_of_sets nil) (is_finite const-decl "bool" finite_sets nil) (Union const-decl "set" sets nil) (partition? const-decl "bool" lagrange_scaf "algebra/") (orbits_disjoint formula-decl nil group_action nil) (orbits const-decl "setofsets[T1]" group_action nil) (setofsets type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (F type-eq-decl nil group_action nil) (T1 formal-type-decl nil group_action nil) (group nonempty-type-eq-decl nil group "algebra/") (group? const-decl "bool" group_def "algebra/") (one formal-const-decl "T" group_action nil) (* formal-const-decl "[T, T -> T]" group_action nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil group_action nil)) shostak)) (orbits_nFix_partition 0 (orbits_nFix_partition-1 nil 3529674691 ("" (skosimp*) (("" (lemma "orbits_partition") (("" (inst?) (("" (assert) (("" (expand "finite_partition?") (("" (prop) (("1" (expand "partition?") (("1" (skosimp*) (("1" (inst?) (("1" (assert) nil nil) ("2" (hide-all-but 1) (("2" (typepred "b!1") (("2" (expand "orbits_nFix") (("2" (expand "extend") (("2" (ground) nil nil)) nil)) nil)) nil)) nil) ("3" (hide-all-but 1) (("3" (typepred "a!1") (("3" (expand "orbits_nFix") (("3" (expand "extend") (("3" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide (-1 -3)) (("2" (lemma "finite_subset[set[T1]]") (("2" (inst -1 "orbits(G!1, X!1)(f!1)" "orbits_nFix(G!1, X!1)(f!1)") (("2" (assert) (("2" (hide (-1 2)) (("2" (expand "subset?") (("2" (skosimp*) (("2" (expand "member") (("2" (expand "orbits_nFix") (("2" (expand "extend") (("2" (prop) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide (-1 -2)) (("3" (expand "every") (("3" (skosimp) (("3" (inst?) (("3" (typepred "x!1") (("3" (expand "orbits_nFix") (("3" (expand "extend") (("3" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((orbits_partition formula-decl nil group_action nil) (extend const-decl "R" extend nil) (NOT const-decl "[bool -> bool]" booleans nil) (b!1 skolem-const-decl "(orbits_nFix(G!1, X!1)(f!1))" group_action nil) (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (orbits const-decl "setofsets[T1]" group_action nil) (G!1 skolem-const-decl "group[T, *, one]" group_action nil) (X!1 skolem-const-decl "set[T1]" group_action nil) (f!1 skolem-const-decl "F(G!1, X!1)" group_action nil) (orbits_nFix const-decl "setofsets[T1]" group_action nil) (a!1 skolem-const-decl "(orbits_nFix(G!1, X!1)(f!1))" group_action nil) (partition? const-decl "bool" lagrange_scaf "algebra/") (finite_subset formula-decl nil finite_sets nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (subset? const-decl "bool" sets nil) (member const-decl "bool" sets nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (every const-decl "bool" sets nil) (x!1 skolem-const-decl "(orbits_nFix(G!1, X!1)(f!1))" group_action nil) (finite_partition? const-decl "bool" lagrange_scaf "algebra/") (F type-eq-decl nil group_action nil) (T1 formal-type-decl nil group_action nil) (group nonempty-type-eq-decl nil group "algebra/") (group? const-decl "bool" group_def "algebra/") (one formal-const-decl "T" group_action nil) (* formal-const-decl "[T, T -> T]" group_action nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil group_action nil)) shostak)) (orbits_eq_index_aux_TCC1 0 (orbits_eq_index_aux_TCC1-1 nil 3529497668 ("" (skosimp*) (("" (lemma "stabilizer_is_subgroup") (("" (inst?) (("" (assert) (("" (expand "subgroup?") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ((stabilizer_is_subgroup formula-decl nil group_action nil) (subgroup? const-decl "bool" group_def "algebra/") (F type-eq-decl nil group_action nil) (T1 formal-type-decl nil group_action nil) (group nonempty-type-eq-decl nil group "algebra/") (group? const-decl "bool" group_def "algebra/") (one formal-const-decl "T" group_action nil) (* formal-const-decl "[T, T -> T]" group_action nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil group_action nil)) nil)) (orbits_eq_index_aux 0 (orbits_eq_index_aux-1 nil 3529617585 ("" (skosimp) (("" (lemma "stabilizer_is_subgroup") (("" (inst -1 "G!1" "X!1" "x!1" "f!1") (("" (assert) (("" (lemma "subgroup_is_group") (("" (inst?) (("" (assert) (("" (inst 1 "(LAMBDA (A:(left_cosets(G!1, stabilizer(G!1, X!1)(f!1, x!1)))) : f!1(lc_gen(G!1,stabi (("1" (expand "bijective?") (("1" (prop) (("1" (expand "injective?") (("1" (skosimp) (("1" (name-replace "b" "lc_gen(G!1, stabilizer(G!1, X!1)(f!1, x!1), x1!1)") (("1" (name-replace "c" "lc_gen(G!1, stabilizer(G!1, X!1)(f!1, x!1), x2!1)") (("1" (typepred "x1!1" "x2!1") (("1" (expand "left_cosets") (("1" (skosimp*) (("1" (case "stabilizer(G!1, X!1)(f!1, x!1)(inv[T, *, one](c) * b)") (("1" (lemma "lc_is_eq") (("1" (inst -1 "G!1" "stabilizer(G!1, X!1)(f!1, x!1)" "b" "c") (("1" (assert) (("1" (hide (-2 -3 2)) (("1" (inst 1 "inv[T, *, one](c) * b") (("1" (rewrite "assoc") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide (-1 -2 2)) (("2" (expand "stabilizer" 1) (("2" (expand "extend") (("2" (ground) (("1" (expand "group_action?") (("1" (copy -5) (("1" (inst -6 "inv[T, *, one](c)" "b" "x!1") (("1" (flatten) (("1" (replaces -7) (("1" (replaces -3) (("1" (inst -1 "inv[T, *, one](c)" "c" "x!1") (("1" (assert) nil nil) ("2" (rewrite "inv_in") nil nil)) nil)) nil)) nil)) nil) ("2" (rewrite "inv_in") nil nil)) nil)) nil)) nil) ("2" (rewrite "product_in") (("2" (rewrite "inv_in") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "surjective?") (("2" (skosimp) (("2" (typepred "y!1") (("2" (expand "orbit") (("2" (expand "extend") (("2" (ground) (("2" (skosimp) (("2" (inst 1 "g!1 * stabilizer(G!1, X!1)(f!1, x!1)") (("1" (typepred "lc_gen(G!1,stabilizer(G!1, X!1)(f!1, x!1) , g!1 * stabilizer(G!1, X!1)(f!1, x!1))") (("1" (name-replace "a!1" "lc_gen(G!1, stabilizer(G!1, X!1)(f!1, x!1), g!1 * stabilizer(G!1, X!1)(f!1, x!1))") (("1" (lemma "lc_eq") (("1" (inst -1 "G!1" "stabilizer(G!1, X!1)(f!1, x!1)" "g!1" "a!1") (("1" (prop) (("1" (skosimp*) (("1" (replaces -5) (("1" (hide (-2 -3 -4)) (("1" (typepred "h!1") (("1" (expand "stabilizer" -1) (("1" (expand "extend") (("1" (ground) (("1" (replaces -3) (("1" (expand "group_action?") (("1" (inst -5 "a!1" "h!1" "x!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "left_cosets") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (expand "orbit") (("2" (expand "extend") (("2" (inst?) (("2" (typepred "A!1") (("2" (expand "left_cosets") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (skosimp) (("3" (typepred "A!1") (("3" (expand "left_cosets") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((stabilizer_is_subgroup formula-decl nil group_action nil) (subset? const-decl "bool" sets nil) (stabilizer const-decl "{S: set[T] | subset?(S, G)}" group_action nil) (* const-decl "set[T]" cosets "algebra/") (= const-decl "[T, T -> boolean]" equalities nil) (x!1 skolem-const-decl "(X!1)" group_action nil) (f!1 skolem-const-decl "F(G!1, X!1)" group_action nil) (X!1 skolem-const-decl "set[T1]" group_action nil) (G!1 skolem-const-decl "group[T, *, one]" group_action nil) (left_cosets const-decl "setofsets[T]" right_left_cosets nil) (setofsets type-eq-decl nil sets nil) (subgroup type-eq-decl nil group "algebra/") (subgroup? const-decl "bool" group_def "algebra/") (setof type-eq-decl nil defined_types nil) (lc_gen const-decl "{a: T | G(a) AND lc = a * H}" cosets "algebra/") (AND const-decl "[bool, bool -> bool]" booleans nil) (left_cosets type-eq-decl nil cosets "algebra/") (orbit const-decl "{Y: set[T1] | subset?(Y, X)}" group_action nil) (inv const-decl "{y | x * y = one AND y * x = one}" group "algebra/") (left_identity formula-decl nil monad "algebra/") (inv_right formula-decl nil group "algebra/") (assoc formula-decl nil group "algebra/") (lc_is_eq formula-decl nil cosets "algebra/") (inv_in formula-decl nil group "algebra/") (inv_left formula-decl nil group "algebra/") (c skolem-const-decl "{a: T | G!1(a) AND x2!1 = a * stabilizer(G!1, X!1)(f!1, x!1)}" group_action nil) (x2!1 skolem-const-decl "(left_cosets(G!1, stabilizer(G!1, X!1)(f!1, x!1)))" group_action nil) (group_action? const-decl "bool" group_action nil) (product_in formula-decl nil group "algebra/") (extend const-decl "R" extend nil) (NOT const-decl "[bool -> bool]" booleans nil) (injective? const-decl "bool" functions nil) (g!1 skolem-const-decl "(G!1)" group_action nil) (lc_eq formula-decl nil cosets "algebra/") (surjective? const-decl "bool" functions nil) (bijective? const-decl "bool" functions nil) (A!1 skolem-const-decl "(left_cosets[T, *, one](G!1, stabilizer(G!1, X!1)(f!1, x!1)))" group_action nil) (subgroup_is_group formula-decl nil group "algebra/") (F type-eq-decl nil group_action nil) (T1 formal-type-decl nil group_action nil) (group nonempty-type-eq-decl nil group "algebra/") (group? const-decl "bool" group_def "algebra/") (one formal-const-decl "T" group_action nil) (* formal-const-decl "[T, T -> T]" group_action nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil group_action nil)) shostak)) (orbits_eq_index_TCC1 0 (orbits_eq_index_TCC1-1 nil 3529497668 ("" (skosimp*) (("" (lemma "stabilizer_is_subgroup") (("" (inst?) (("" (assert) (("" (expand "subgroup?") (("" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ((stabilizer_is_subgroup formula-decl nil group_action nil) (subgroup? const-decl "bool" group_def "algebra/") (F type-eq-decl nil group_action nil) (T1 formal-type-decl nil group_action nil) (finite_group nonempty-type-eq-decl nil group "algebra/") (finite_group? const-decl "bool" group_def "algebra/") (group nonempty-type-eq-decl nil group "algebra/") (group? const-decl "bool" group_def "algebra/") (one formal-const-decl "T" group_action nil) (* formal-const-decl "[T, T -> T]" group_action nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil group_action nil)) nil)) (orbits_eq_index_TCC2 0 (orbits_eq_index_TCC2-1 nil 3529497668 ("" (skosimp*) (("" (lemma "orbit_is_finite") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil) ((orbit_is_finite formula-decl nil group_action nil) (F type-eq-decl nil group_action nil) (T1 formal-type-decl nil group_action nil) (finite_group nonempty-type-eq-decl nil group "algebra/") (finite_group? const-decl "bool" group_def "algebra/") (group nonempty-type-eq-decl nil group "algebra/") (group? const-decl "bool" group_def "algebra/") (one formal-const-decl "T" group_action nil) (* formal-const-decl "[T, T -> T]" group_action nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil group_action nil)) nil)) (orbits_eq_index 0 (orbits_eq_index-1 nil 3529612554 ("" (skosimp) (("" (expand "index") (("" (lemma "orbits_eq_index_aux") (("" (inst -1 "G!1" "X!1" "x!1" "f!1") (("" (assert) (("" (skosimp) (("" (lemma "card_eq_bij[set[T],T1]") (("" (inst?) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((index const-decl "nat" right_left_cosets nil) (T formal-type-decl nil group_action nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (* formal-const-decl "[T, T -> T]" group_action nil) (one formal-const-decl "T" group_action nil) (group? const-decl "bool" group_def "algebra/") (group nonempty-type-eq-decl nil group "algebra/") (finite_group? const-decl "bool" group_def "algebra/") (finite_group nonempty-type-eq-decl nil group "algebra/") (T1 formal-type-decl nil group_action nil) (F type-eq-decl nil group_action nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (subgroup? const-decl "bool" group_def "algebra/") (subgroup type-eq-decl nil group "algebra/") (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (left_cosets const-decl "setofsets[T]" right_left_cosets nil) (subset? const-decl "bool" sets nil) (stabilizer const-decl "{S: set[T] | subset?(S, G)}" group_action nil) (orbit const-decl "{Y: set[T1] | subset?(Y, X)}" group_action nil) (card_eq_bij formula-decl nil finite_sets_card_eq "finite_sets/") (orbits_eq_index_aux formula-decl nil group_action nil)) shostak)) (counting_formula_TCC1 0 (counting_formula_TCC1-1 nil 3529497668 ("" (skosimp) (("" (lemma "card_partition_TCC2") (("" (inst?) (("1" (assert) (("1" (hide 2) (("1" (expand "nonempty?") (("1" (prop) (("1" (skosimp) (("1" (typepred "A!1") (("1" (expand "orbits") (("1" (skosimp) (("1" (replaces -1) (("1" (lemma "orbit_nonempty") (("1" (inst?) (("1" (assert) (("1" (expand "nonempty?") (("1" (rewrite "empty_card") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "orbits_nonempty") (("2" (inst?) (("2" (assert) (("2" (expand "nonempty?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (rewrite "orbits_partition") nil nil)) nil)) nil)) nil)) nil) ((set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T1 formal-type-decl nil group_action nil) (card_partition_TCC2 subtype-tcc nil class_equation_scaf nil) (orbits_partition formula-decl nil group_action nil) (nonempty? const-decl "bool" sets nil) (orbits_nonempty formula-decl nil group_action nil) (empty_card formula-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (subset? const-decl "bool" sets nil) (orbit const-decl "{Y: set[T1] | subset?(Y, X)}" group_action nil) (orbit_nonempty formula-decl nil group_action nil) (NOT const-decl "[bool -> bool]" booleans nil) (finite_partition type-eq-decl nil lagrange_scaf "algebra/") (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (finite_partition? const-decl "bool" lagrange_scaf "algebra/") (T formal-type-decl nil group_action nil) (* formal-const-decl "[T, T -> T]" group_action nil) (one formal-const-decl "T" group_action nil) (group? const-decl "bool" group_def "algebra/") (group nonempty-type-eq-decl nil group "algebra/") (F type-eq-decl nil group_action nil) (orbits const-decl "setofsets[T1]" group_action nil) (G!1 skolem-const-decl "group[T, *, one]" group_action nil) (X!1 skolem-const-decl "set[T1]" group_action nil) (f!1 skolem-const-decl "F(G!1, X!1)" group_action nil)) nil)) (counting_formula 0 (counting_formula-1 nil 3529521666 ("" (skosimp*) (("" (lemma "card_partition") (("" (inst?) (("1" (prop) (("1" (lemma "set_orbits_is") (("1" (inst -1 "G!1" "X!1" "f!1") (("1" (assert) nil nil)) nil)) nil) ("2" (hide 2) (("2" (rewrite "orbits_nonempty") nil nil)) nil) ("3" (hide 2) (("3" (skosimp) (("3" (typepred "A!1") (("3" (expand "orbits") (("3" (skosimp) (("3" (replaces -1) (("3" (lemma "orbit_nonempty") (("3" (inst?) (("3" (assert) (("3" (expand "nonempty?") (("3" (rewrite "empty_card") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (rewrite "orbits_partition") nil nil)) nil)) nil)) nil)) nil) ((set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T1 formal-type-decl nil group_action nil) (card_partition formula-decl nil class_equation_scaf nil) (orbits_partition formula-decl nil group_action nil) (Union_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas nil) (set_orbits_is formula-decl nil group_action nil) (orbits_nonempty formula-decl nil group_action nil) (nonempty? const-decl "bool" sets nil) (empty_card formula-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (subset? const-decl "bool" sets nil) (orbit const-decl "{Y: set[T1] | subset?(Y, X)}" group_action nil) (orbit_nonempty formula-decl nil group_action nil) (NOT const-decl "[bool -> bool]" booleans nil) (finite_partition type-eq-decl nil lagrange_scaf "algebra/") (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (finite_partition? const-decl "bool" lagrange_scaf "algebra/") (T formal-type-decl nil group_action nil) (* formal-const-decl "[T, T -> T]" group_action nil) (one formal-const-decl "T" group_action nil) (group? const-decl "bool" group_def "algebra/") (group nonempty-type-eq-decl nil group "algebra/") (F type-eq-decl nil group_action nil) (orbits const-decl "setofsets[T1]" group_action nil) (G!1 skolem-const-decl "group[T, *, one]" group_action nil) (X!1 skolem-const-decl "set[T1]" group_action nil) (f!1 skolem-const-decl "F(G!1, X!1)" group_action nil)) shostak)) (class_equation_TCC1 0 (class_equation_TCC1-1 nil 3529669814 ("" (skosimp) (("" (lemma "finite_subset[T1]") (("" (inst -1 "X!1" "Fix(G!1, X!1)(f!1)") (("" (assert) nil nil)) nil)) nil)) nil) ((T1 formal-type-decl nil group_action nil) (finite_subset formula-decl nil finite_sets nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (Fix const-decl "{Y: set[T1] | subset?(Y, X)}" group_action nil) (subset? const-decl "bool" sets nil) (F type-eq-decl nil group_action nil) (group nonempty-type-eq-decl nil group "algebra/") (group? const-decl "bool" group_def "algebra/") (one formal-const-decl "T" group_action nil) (* formal-const-decl "[T, T -> T]" group_action nil) (T formal-type-decl nil group_action nil) (finite_set type-eq-decl nil finite_sets nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (is_finite const-decl "bool" finite_sets nil) (X!1 skolem-const-decl "set[T1]" group_action nil)) nil)) (class_equation_TCC2 0 (class_equation_TCC2-1 nil 3529669814 ("" (skosimp) (("" (case "empty?(orbits_nFix(G!1, X!1)(f!1))") (("1" (case-replace "restrict[setof[T1], finite_set[T1], boolean](orbits_nFix(G!1, X!1)(f!1)) = emptyset" :hide? T) (("1" (rewrite "convergent_empty") nil nil) ("2" (hide 2) (("2" (decompose-equality 1) (("2" (expand "restrict") (("2" (expand* "emptyset" "empty?" "member") (("2" (inst -2 "x!1") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "card_partition_TCC2") (("2" (inst?) (("1" (assert) (("1" (hide 3) (("1" (expand "nonempty?") (("1" (hide 2) (("1" (skosimp) (("1" (typepred "A!1") (("1" (expand "orbits_nFix") (("1" (expand "extend") (("1" (prop) (("1" (hide -2) (("1" (expand "orbits") (("1" (skosimp) (("1" (replaces -1) (("1" (lemma "orbit_nonempty") (("1" (inst?) (("1" (assert) (("1" (expand "nonempty?") (("1" (rewrite "empty_card") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide (2 3)) (("2" (rewrite "orbits_nFix_partition") nil nil)) nil)) nil)) nil)) nil)) nil) ((orbits_nFix const-decl "setofsets[T1]" group_action nil) (setofsets type-eq-decl nil sets nil) (F type-eq-decl nil group_action nil) (group nonempty-type-eq-decl nil group "algebra/") (group? const-decl "bool" group_def "algebra/") (one formal-const-decl "T" group_action nil) (* formal-const-decl "[T, T -> T]" group_action nil) (T formal-type-decl nil group_action nil) (empty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T1 formal-type-decl nil group_action nil) (member const-decl "bool" sets nil) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (Card const-decl "nat" finite_sets nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (convergent_empty formula-decl nil convergence_set "sigma_set/") (emptyset const-decl "set" sets nil) (restrict const-decl "R" restrict nil) (= const-decl "[T, T -> boolean]" equalities nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_emptyset name-judgement "finite_set[finite_set[T1]]" group_action nil) (finite_emptyset name-judgement "finite_set[T]" countable_props "sets_aux/") (finite_emptyset name-judgement "finite_set[T]" finite_sets_inductions "finite_sets/") (finite_emptyset name-judgement "finite_set" finite_sets nil) (f!1 skolem-const-decl "F(G!1, X!1)" group_action nil) (X!1 skolem-const-decl "set[T1]" group_action nil) (G!1 skolem-const-decl "group[T, *, one]" group_action nil) (finite_partition? const-decl "bool" lagrange_scaf "algebra/") (finite_partition type-eq-decl nil lagrange_scaf "algebra/") (NOT const-decl "[bool -> bool]" booleans nil) (extend const-decl "R" extend nil) (orbit_nonempty formula-decl nil group_action nil) (orbit const-decl "{Y: set[T1] | subset?(Y, X)}" group_action nil) (subset? const-decl "bool" sets nil) (empty_card formula-decl nil finite_sets nil) (orbits const-decl "setofsets[T1]" group_action nil) (nonempty? const-decl "bool" sets nil) (orbits_nFix_partition formula-decl nil group_action nil) (card_partition_TCC2 subtype-tcc nil class_equation_scaf nil)) nil)) (class_equation 0 (class_equation-1 nil 3529674998 ("" (skosimp*) (("" (case "empty?(orbits_nFix(G!1, X!1)(f!1))") (("1" (case-replace "restrict[setof[T1], finite_set[T1], boolean](orbits_nFix(G!1, X!1)(f!1)) = emptyset" :hide? T) (("1" (rewrite "sigma_empty") (("1" (assert) (("1" (lemma "empty_iff_eq_Fix") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide 2) (("2" (decompose-equality 1) (("2" (grind) nil nil)) nil)) nil)) nil) ("2" (lemma "set_orbits_is") (("2" (inst?) (("2" (assert) (("2" (lemma "orbits_is_union") (("2" (inst?) (("2" (assert) (("2" (replaces -1) (("2" (lemma "orbits_nFix_disj_Fix") (("2" (inst?) (("2" (assert) (("2" (lemma "card_disj_union[T1]") (("2" (inst?) (("1" (assert) (("1" (lemma "card_partition") (("1" (inst?) (("1" (assert) (("1" (hide (-1 -2 -3 3)) (("1" (expand "nonempty?") (("1" (hide 2) (("1" (skosimp) (("1" (typepred "A!1") (("1" (expand "orbits_nFix") (("1" (expand "extend") (("1" (prop) (("1" (hide -1) (("1" (skosimp) (("1" (replaces -1) (("1" (lemma "orbit_nonempty") (("1" (inst?) (("1" (assert) (("1" (expand "nonempty?") (("1" (rewrite "empty_card") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (rewrite "orbits_nFix_partition") nil nil)) nil)) nil)) nil)) nil) ("2" (hide (-1 2 3)) (("2" (lemma "union_subset1[T1]") (("2" (inst -1 "Union(orbits_nFix(G!1, X!1)(f!1))" "Fix(G!1, X!1)(f!1)") (("2" (rewrite "union_commutative") (("2" (replaces -2) (("2" (lemma "finite_subset[T1]") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((orbits_nFix const-decl "setofsets[T1]" group_action nil) (setofsets type-eq-decl nil sets nil) (F type-eq-decl nil group_action nil) (group nonempty-type-eq-decl nil group "algebra/") (group? const-decl "bool" group_def "algebra/") (one formal-const-decl "T" group_action nil) (* formal-const-decl "[T, T -> T]" group_action nil) (T formal-type-decl nil group_action nil) (empty? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (setof type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T1 formal-type-decl nil group_action nil) (NOT const-decl "[bool -> bool]" booleans nil) (Fix const-decl "{Y: set[T1] | subset?(Y, X)}" group_action nil) (subset? const-decl "bool" sets nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (group_action? const-decl "bool" group_action nil) (nonempty? const-decl "bool" sets nil) (finite_group? const-decl "bool" group_def "algebra/") (injective? const-decl "bool" functions nil) (member const-decl "bool" sets nil) (extend const-decl "R" extend nil) (orbits const-decl "setofsets[T1]" group_action nil) (orbit const-decl "{Y: set[T1] | subset?(Y, X)}" group_action nil) (card const-decl "{n: nat | n = Card(S)}" finite_sets nil) (Card const-decl "nat" finite_sets nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (sigma_empty formula-decl nil sigma_set "sigma_set/") (empty_iff_eq_Fix formula-decl nil group_action nil) (nnint_plus_nnint_is_nnint application-judgement "nonneg_int" integers nil) (emptyset const-decl "set" sets nil) (restrict const-decl "R" restrict nil) (= const-decl "[T, T -> boolean]" equalities nil) (finite_set type-eq-decl nil finite_sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_emptyset name-judgement "finite_set[finite_set[T1]]" group_action nil) (finite_emptyset name-judgement "finite_set[T]" countable_props "sets_aux/") (finite_emptyset name-judgement "finite_set[T]" finite_sets_inductions "finite_sets/") (finite_emptyset name-judgement "finite_set" finite_sets nil) (orbits_is_union formula-decl nil group_action nil) (Union_surjective name-judgement "(surjective?[setofsets[T], set[T]])" sets_lemmas nil) (orbits_nFix_disj_Fix formula-decl nil group_action nil) (Union const-decl "set" sets nil) (G!1 skolem-const-decl "group[T, *, one]" group_action nil) (X!1 skolem-const-decl "set[T1]" group_action nil) (f!1 skolem-const-decl "F(G!1, X!1)" group_action nil) (card_partition formula-decl nil class_equation_scaf nil) (orbits_nFix_partition formula-decl nil group_action nil) (orbit_nonempty formula-decl nil group_action nil) (empty_card formula-decl nil finite_sets nil) (finite_partition type-eq-decl nil lagrange_scaf "algebra/") (finite_partition? const-decl "bool" lagrange_scaf "algebra/") (union_subset1 formula-decl nil sets_lemmas nil) (union_commutative formula-decl nil sets_lemmas nil) (finite_subset formula-decl nil finite_sets nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (card_disj_union formula-decl nil finite_sets nil) (real_plus_real_is_real application-judgement "real" reals nil) (set_orbits_is formula-decl nil group_action nil)) shostak)) (Fix_congruence_TCC1 0 (Fix_congruence_TCC1-1 nil 3529684292 ("" (skosimp*) (("" (expand* "finite_group?" "finite_monad?") (("" (typepred "G!1") (("" (expand "group?") (("" (flatten) (("" (expand "monoid?") (("" (flatten) (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((finite_monad? const-decl "bool" monad_def "algebra/") (finite_group? const-decl "bool" group_def "algebra/") (monoid? const-decl "bool" monoid_def "algebra/") (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (T formal-type-decl nil group_action nil) (set type-eq-decl nil sets nil) (* formal-const-decl "[T, T -> T]" group_action nil) (one formal-const-decl "T" group_action nil) (group? const-decl "bool" group_def "algebra/") (group nonempty-type-eq-decl nil group "algebra/")) nil)) (Fix_congruence_TCC2 0 (Fix_congruence_TCC2-1 nil 3529686733 ("" (subtype-tcc) nil nil) ((injective? const-decl "bool" functions nil) (is_finite const-decl "bool" finite_sets nil) (finite_group? const-decl "bool" group_def "algebra/")) nil)) (Fix_congruence 0 (Fix_congruence-1 nil 3529686786 ("" (skosimp*) (("" (lemma "divide_sigma") (("" (inst -1 "orbits_nFix(G!1, X!1)(f!1)" "p!1") (("1" (prop) (("1" (lemma "class_equation") (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (expand "nonempty?") (("2" (lemma "empty_iff_eq_Fix") (("2" (inst?) (("2" (assert) (("2" (replace -1 2 rl) (("2" (assert) (("2" (rewrite "divides_zero") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (hide 2) (("3" (skosimp) (("3" (prop) (("1" (typepred "A!1") (("1" (expand "orbits_nFix") (("1" (expand "extend") (("1" (ground) (("1" (skosimp) (("1" (replaces -2) (("1" (lemma "empty_card[T1]") (("1" (inst?) (("1" (assert) (("1" (lemma "orbit_nonempty") (("1" (inst?) (("1" (assert) (("1" (hide-all-but (-1 -2)) (("1" (expand "nonempty?") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "A!1") (("2" (expand "orbits_nFix") (("2" (expand "extend") (("2" (ground) (("2" (skosimp) (("2" (lemma "orbits_eq_index") (("2" (inst?) (("2" (assert) (("2" (hide -2) (("2" (replaces -2) (("2" (replace -1 1 rl) (("2" (hide -1) (("2" (lemma "Lagrange_index") (("2" (inst?) (("1" (prop) (("1" (expand "divides") (("1" (replace -3 -1) (("1" (lemma "divides_prime_power") (("1" (inst -1 "n!1" "p!1" "index(G!1, stabilizer(G!1, X!1)(f!1, x!1))") (("1" (assert) (("1" (prop) (("1" (skosimp) (("1" (case-replace "i!1 = 0" :hide? T) (("1" (rewrite "expt_x0") (("1" (hide-all-but (-2 -3 -5)) (("1" (replaces -1) (("1" (replaces -1) (("1" (rewrite "identity_mult") (("1" (expand "order") (("1" (lemma "same_card_subset[T]") (("1" (inst -1 "stabilizer(G!1, X!1)(f!1, x!1)" "G!1") (("1" (assert) (("1" (hide -2) (("1" (decompose-equality -1) (("1" (typepred "x!1") (("1" (expand "member") (("1" (expand "Fix") (("1" (expand "extend") (("1" (skosimp) (("1" (inst?) (("1" (iff) (("1" (typepred "g!1") (("1" (prop) (("1" (expand "stabilizer") (("1" (expand "extend") (("1" (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) ("2" (hide-all-but (-1 -2 1 2)) (("2" (inst 2 "p!1^(i!1 - 1)") (("1" (lemma "expt_plus") (("1" (inst -1 "1" "i!1 - 1" "p!1") (("1" (assert) (("1" (rewrite "expt_x1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (hide -2) (("2" (rewrite "int_exp") nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-1 1)) (("2" (expand "divides") (("2" (inst?) nil nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but 1) (("2" (expand "index") (("2" (case "nonempty?(left_cosets(G!1, stabilizer(G!1, X!1)(f!1, x!1)))") (("1" (rewrite "nonempty_card") nil nil) ("2" (hide 2) (("2" (expand* "nonempty?" "empty?" "member") (("2" (inst -1 "stabilizer(G!1, X!1)(f!1, x!1)") (("2" (expand "left_cosets") (("2" (inst 1 "one") (("1" (rewrite "left_coset_one") nil nil) ("2" (rewrite "one_in") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-6 1)) (("2" (rewrite "stabilizer_is_subgroup") nil nil)) nil)) nil) ("2" (hide-all-but (-1 -6 1)) (("2" (lemma "stabilizer_is_subgroup") (("2" (inst?) (("2" (assert) (("2" (hide -3) (("2" (lemma "finite_subgroups") (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide-all-but (-3 -6 1)) (("2" (rewrite "orbits_nFix_partition") nil nil)) nil)) nil)) nil)) nil) ((set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T1 formal-type-decl nil group_action nil) (divide_sigma formula-decl nil class_equation_scaf nil) (orbits_nFix_partition formula-decl nil group_action nil) (posint_exp application-judgement "posint" exponentiation nil) (int_minus_int_is_int application-judgement "int" integers nil) (class_equation formula-decl nil group_action nil) (empty_iff_eq_Fix formula-decl nil group_action nil) (divides_zero formula-decl nil divides nil) (nonempty? const-decl "bool" sets nil) (finite_group nonempty-type-eq-decl nil group "algebra/") (finite_group? const-decl "bool" group_def "algebra/") (Lagrange_index formula-decl nil lagrange_index nil) (finite_subgroups formula-decl nil group "algebra/") (real_gt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (subgroup? const-decl "bool" group_def "algebra/") (subgroup type-eq-decl nil group "algebra/") (nat nonempty-type-eq-decl nil naturalnumbers nil) (index const-decl "nat" right_left_cosets nil) (= const-decl "[T, T -> boolean]" equalities nil) (subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (same_card_subset formula-decl nil finite_sets nil) (identity_mult formula-decl nil number_fields nil) (numfield nonempty-type-eq-decl nil number_fields nil) (finite_monad? const-decl "bool" monad_def "algebra/") (finite_monad nonempty-type-eq-decl nil monad "algebra/") (order const-decl "posnat" monad "algebra/") (expt_x0 formula-decl nil exponentiation nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (posrat_exp application-judgement "posrat" exponentiation nil) (nnrat_exp application-judgement "nnrat" exponentiation nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (/= const-decl "boolean" notequal nil) (^ const-decl "real" exponentiation nil) (p!1 skolem-const-decl "posnat" group_action nil) (- const-decl "[numfield, numfield -> numfield]" number_fields nil) (i!1 skolem-const-decl "nat" group_action nil) (nzreal nonempty-type-eq-decl nil reals nil) (expt_x1 formula-decl nil exponentiation nil) (int_plus_int_is_int application-judgement "int" integers nil) (posrat_times_posrat_is_posrat application-judgement "posrat" rationals nil) (real_le_is_total_order name-judgement "(total_order?[real])" real_props nil) (expt_plus formula-decl nil exponentiation nil) (int_exp judgement-tcc nil exponentiation nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (left_coset_one formula-decl nil cosets "algebra/") (one_in formula-decl nil monad "algebra/") (monad? const-decl "bool" monad_def "algebra/") (monad nonempty-type-eq-decl nil monad "algebra/") (empty? const-decl "bool" sets nil) (nonempty_card formula-decl nil finite_sets nil) (left_cosets const-decl "setofsets[T]" right_left_cosets nil) (divides_prime_power formula-decl nil general_properties nil) (divides const-decl "bool" divides nil) (stabilizer_is_subgroup formula-decl nil group_action nil) (x!1 skolem-const-decl "{x: (X!1) | NOT member(x, Fix(G!1, X!1)(f!1))}" group_action nil) (stabilizer const-decl "{S: set[T] | subset?(S, G)}" group_action nil) (orbits_eq_index formula-decl nil group_action nil) (NOT const-decl "[bool -> bool]" booleans nil) (extend const-decl "R" extend nil) (empty_card formula-decl nil finite_sets nil) (orbit_nonempty formula-decl nil group_action nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (subset? const-decl "bool" sets nil) (orbit const-decl "{Y: set[T1] | subset?(Y, X)}" group_action nil) (member const-decl "bool" sets nil) (Fix const-decl "{Y: set[T1] | subset?(Y, X)}" group_action nil) (posnat nonempty-type-eq-decl nil integers nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (finite_partition type-eq-decl nil lagrange_scaf "algebra/") (setof type-eq-decl nil defined_types nil) (setofsets type-eq-decl nil sets nil) (finite_partition? const-decl "bool" lagrange_scaf "algebra/") (T formal-type-decl nil group_action nil) (* formal-const-decl "[T, T -> T]" group_action nil) (one formal-const-decl "T" group_action nil) (group? const-decl "bool" group_def "algebra/") (group nonempty-type-eq-decl nil group "algebra/") (F type-eq-decl nil group_action nil) (orbits_nFix const-decl "setofsets[T1]" group_action nil) (G!1 skolem-const-decl "group[T, *, one]" group_action nil) (X!1 skolem-const-decl "set[T1]" group_action nil) (f!1 skolem-const-decl "F(G!1, X!1)" group_action nil)) shostak)))
¤ 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.88Bemerkung: (vorverarbeitet am 2026-04-29) ¤*Bot Zugriff |
|
||||||||||||||
2026-05-26