|
(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"
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.131 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
