|
(cosets
(IMP_group_TCC1 0
(IMP_group_TCC1-1 nil 3406031997
("" (rewrite "fullset_is_group") nil nil)
((fullset_is_group formula-decl nil cosets nil)) nil))
(congruence_is_equivalence 0
(congruence_is_equivalence-2 nil 3397484255
("" (skosimp*)
(("" (expand "equivalence?")
(("" (auto-rewrite "member")
(("" (expand "congruent_mod")
(("" (split)
(("1" (expand "reflexive?")
(("1" (skosimp*)
(("1" (typepred "H!1")
(("1" (expand "group?")
(("1" (expand "monoid?")
(("1" (flatten)
(("1" (assert)
(("1" (expand "monad?")
(("1" (skosimp*)
(("1"
(typepred "H!1")
(("1" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "symmetric?")
(("2" (skosimp*)
(("2" (typepred "H!1")
(("2" (assert)
(("2" (rewrite "subgroup_def")
(("2" (flatten)
(("2" (expand "inv_closed?")
(("2" (inst - "x!1 * inv(y!1)")
(("2" (rewrite "inv_star")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (expand "transitive?")
(("3" (skosimp*)
(("3" (typepred "H!1")
(("3" (rewrite "subgroup_def")
(("3" (flatten)
(("3" (assert)
(("3" (expand "star_closed?")
(("3"
(inst - "x!1 * inv(y!1)" "y!1 * inv(z!1)")
(("3" (rewrite "associative")
(("3"
(lemma "associative")
(("3"
(inst - "inv(y!1)" "y!1" "inv(z!1)")
(("3"
(assert)
(("3"
(replace -1 -7 rl)
(("3"
(rewrite "inv_left")
(("3"
(rewrite "left_identity")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((equivalence? const-decl "bool" relations nil)
(one_member formula-decl nil monad nil)
(inv_right formula-decl nil group nil)
(monoid? const-decl "bool" monoid_def 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-nonempty-type-decl nil cosets nil)
(set type-eq-decl nil sets nil)
(* formal-const-decl "[T, T -> T]" cosets nil)
(one formal-const-decl "T" cosets nil)
(group? const-decl "bool" group_def nil)
(group nonempty-type-eq-decl nil group nil)
(reflexive? const-decl "bool" relations nil)
(member const-decl "bool" sets nil)
(inv const-decl "{y | x * y = one AND y * x = one}" group nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(inv_inv formula-decl nil group nil)
(inv_star formula-decl nil group nil)
(inv_closed? const-decl "bool" group nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(subgroup_def formula-decl nil group nil)
(symmetric? const-decl "bool" relations nil)
(inv_left formula-decl nil group nil)
(left_identity formula-decl nil monad nil)
(associative formula-decl nil semigroup nil)
(star_closed? const-decl "bool" groupoid_def nil)
(transitive? const-decl "bool" relations nil)
(congruent_mod const-decl "bool" cosets nil))
nil)
(congruence_is_equivalence-1 nil 3292960999
("" (expand "equivalence?")
(("" (expand "congruent_mod")
(("" (skosimp*)
(("" (split)
(("1" (expand "reflexive?")
(("1" (skosimp*)
(("1" (typepred "H!1")
(("1" (expand "group?")
(("1" (expand "monoid?")
(("1" (flatten)
(("1" (assert)
(("1" (expand "monad?")
(("1" (skosimp*)
(("1" (typepred "H!1")
(("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "symmetric?")
(("2" (skosimp*)
(("2" (typepred "H!1")
(("2" (assert)
(("2" (rewrite "subgroup_def")
(("2" (flatten)
(("2" (expand "inv_closed?")
(("2" (inst - "x!1 * inv(y!1)")
(("2" (rewrite "inv_star")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (expand "transitive?")
(("3" (skosimp*)
(("3" (typepred "H!1")
(("3" (rewrite "subgroup_def")
(("3" (flatten)
(("3" (assert)
(("3" (expand "star_closed?")
(("3"
(inst - "x!1 * inv(y!1)" "y!1 * inv(z!1)")
(("3" (rewrite "associative")
(("3" (lemma "associative")
(("3"
(inst - "inv(y!1)" "y!1" "inv(z!1)")
(("3"
(assert)
(("3"
(replace -1 -7 rl)
(("3"
(rewrite "left_identity")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((monad? const-decl "bool" monad_def nil)
(inv_right formula-decl nil group nil)
(monoid? const-decl "bool" monoid_def nil)
(T formal-nonempty-type-decl nil group nil)
(* formal-const-decl "[T, T -> T]" group nil)
(one formal-const-decl "T" group nil)
(group? const-decl "bool" group_def nil)
(group nonempty-type-eq-decl nil group nil)
(inv_inv formula-decl nil group nil)
(inv_star formula-decl nil group nil)
(inv_closed? const-decl "bool" group nil)
(subgroup_def formula-decl nil group nil)
(inv_left formula-decl nil group nil)
(left_identity formula-decl nil monad nil)
(associative formula-decl nil semigroup nil)
(star_closed? const-decl "bool" groupoid_def nil))
shostak))
(left_coset_subset 0
(left_coset_subset-1 nil 3406294944
("" (skosimp*)
(("" (expand "subset?")
(("" (skosimp*)
(("" (assert)
(("" (expand "member")
(("" (expand "*")
(("" (skosimp*)
(("" (typepred "h!1")
(("" (typepred "H!1")
(("" (expand "subgroup?")
(("" (expand "subset?")
(("" (inst?)
(("" (assert)
(("" (expand "member")
((""
(replace -4)
((""
(hide -4)
((""
(rewrite "star_closed")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((subset? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(star_closed formula-decl nil groupoid nil)
(star_closed? const-decl "bool" groupoid_def nil)
(groupoid nonempty-type-eq-decl nil groupoid 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-nonempty-type-decl nil cosets nil)
(set type-eq-decl nil sets nil)
(* formal-const-decl "[T, T -> T]" cosets nil)
(one formal-const-decl "T" cosets nil)
(group? const-decl "bool" group_def nil)
(group nonempty-type-eq-decl nil group nil)
(subgroup? const-decl "bool" group_def nil)
(subgroup type-eq-decl nil group nil)
(* const-decl "set[T]" cosets nil))
shostak))
(right_coset_subset 0
(right_coset_subset-2 nil 3406302835
("" (skosimp*)
(("" (expand "subset?")
(("" (skosimp*)
(("" (assert)
(("" (expand "member")
(("" (expand "*")
(("" (skosimp*)
(("" (typepred "h!1")
(("" (typepred "H!1")
(("" (expand "subgroup?")
(("" (expand "subset?")
(("" (inst?)
(("" (assert)
(("" (expand "member")
((""
(replace -4)
((""
(hide -4)
((""
(rewrite "star_closed")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((subset? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(star_closed formula-decl nil groupoid nil)
(star_closed? const-decl "bool" groupoid_def nil)
(groupoid nonempty-type-eq-decl nil groupoid 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-nonempty-type-decl nil cosets nil)
(set type-eq-decl nil sets nil)
(* formal-const-decl "[T, T -> T]" cosets nil)
(one formal-const-decl "T" cosets nil)
(group? const-decl "bool" group_def nil)
(group nonempty-type-eq-decl nil group nil)
(subgroup? const-decl "bool" group_def nil)
(subgroup type-eq-decl nil group nil)
(* const-decl "set[T]" cosets nil))
nil)
(right_coset_subset-1 nil 3406299017
("" (skosimp*)
(("" (expand "subset?")
(("" (skosimp*)
(("" (expand "member")
(("" (expand "*")
(("" (skosimp*)
(("" (inst + "h!1")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
nil shostak))
(left_coset_one 0
(left_coset_one-2 nil 3405953020
("" (skosimp*)
(("" (apply-extensionality 1 :hide? t)
(("" (expand "*")
(("" (iff 1)
(("" (prop)
(("1" (skosimp*)
(("1" (replace -1)
(("1" (hide -1)
(("1" (assert)
(("1" (rewrite "left_identity[T,*,one]")
(("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (inst?)
(("2" (rewrite "left_identity[T,*,one]") nil nil)) nil))
nil))
nil))
nil))
nil))
nil)
((T formal-nonempty-type-decl nil cosets nil)
(boolean nonempty-type-decl nil booleans nil)
(one formal-const-decl "T" cosets nil)
(* const-decl "set[T]" cosets nil) (set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(x!1 skolem-const-decl "T" cosets nil)
(S!1 skolem-const-decl "set[T]" cosets nil)
(left_identity formula-decl nil monad nil)
(* formal-const-decl "[T, T -> T]" cosets nil))
nil)
(left_coset_one-1 nil 3405952955
("" (skosimp*) (("" (postpone) nil nil)) nil) nil shostak))
(right_coset_one 0
(right_coset_one-1 nil 3405953057
("" (skosimp*)
(("" (apply-extensionality 1 :hide? t)
(("" (iff 1)
(("" (expand "*")
(("" (prop)
(("1" (skosimp*)
(("1" (replace -1)
(("1" (hide -1)
(("1" (rewrite "right_identity")
(("1" (assert) nil nil)) nil))
nil))
nil))
nil)
("2" (inst?) (("2" (rewrite "right_identity") nil nil))
nil))
nil))
nil))
nil))
nil))
nil)
((T formal-nonempty-type-decl nil cosets nil)
(boolean nonempty-type-decl nil booleans nil)
(one formal-const-decl "T" cosets nil)
(* const-decl "set[T]" cosets nil) (set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(x!1 skolem-const-decl "T" cosets nil)
(S!1 skolem-const-decl "set[T]" cosets nil)
(* formal-const-decl "[T, T -> T]" cosets nil)
(right_identity formula-decl nil monad nil))
nil))
(left_coset_assoc 0
(left_coset_assoc-1 nil 3405953079
("" (skosimp*)
(("" (lemma "fullset_is_group")
(("" (expand "group?")
(("" (expand "monoid?")
(("" (flatten)
(("" (hide -1 -3)
(("" (expand "associative?")
(("" (expand "restrict")
(("" (apply-extensionality 1 :hide? t)
(("" (expand "*")
(("" (iff 1)
(("" (prop)
(("1" (skosimp*)
(("1" (replace -1)
(("1"
(typepred "h!1")
(("1"
(skosimp*)
(("1"
(replace -1)
(("1"
(inst + "h!2")
(("1"
(assert)
(("1"
(inst?)
(("1" (assert) nil nil)
("2"
(expand "fullset")
(("2" (propax) nil nil))
nil)
("3"
(expand "fullset")
(("3" (propax) nil nil))
nil)
("4"
(expand "fullset")
(("4" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (replace -1)
(("2"
(hide -1)
(("2"
(typepred "h!1")
(("2"
(inst + "b!1*h!1")
(("1"
(inst?)
(("1"
(expand "fullset")
(("1" (propax) nil nil))
nil)
("2"
(expand "fullset")
(("2" (propax) nil nil))
nil)
("3"
(expand "fullset")
(("3" (propax) nil nil))
nil))
nil)
("2" (inst?) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((fullset_is_group formula-decl nil cosets nil)
(monoid? const-decl "bool" monoid_def nil)
(restrict const-decl "R" restrict nil)
(fullset const-decl "set" sets nil)
(a!1 skolem-const-decl "T" cosets nil)
(b!1 skolem-const-decl "T" cosets nil)
(S!1 skolem-const-decl "set[T]" cosets nil)
(h!2 skolem-const-decl "(S!1)" cosets nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(h!1 skolem-const-decl "(S!1)" cosets nil)
(* formal-const-decl "[T, T -> T]" cosets nil)
(* const-decl "set[T]" cosets nil) (set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(T formal-nonempty-type-decl nil cosets nil)
(boolean nonempty-type-decl nil booleans nil)
(associative? const-decl "bool" operator_defs nil)
(group? const-decl "bool" group_def nil))
nil))
(right_coset_assoc 0
(right_coset_assoc-1 nil 3405953119
("" (skosimp*)
(("" (lemma "fullset_is_group")
(("" (expand "group?")
(("" (expand "monoid?")
(("" (flatten)
(("" (hide -1 -3)
(("" (expand "associative?")
(("" (expand "restrict")
(("" (apply-extensionality 1 :hide? t)
(("" (expand "*")
(("" (iff 1)
(("" (prop)
(("1" (skosimp*)
(("1" (replace -1)
(("1"
(typepred "h!1")
(("1"
(skosimp*)
(("1"
(replace -1)
(("1"
(inst + "h!2")
(("1"
(assert)
(("1"
(inst?)
(("1"
(assert)
(("1"
(expand "fullset")
(("1" (propax) nil nil))
nil))
nil)
("2"
(expand "fullset")
(("2" (propax) nil nil))
nil)
("3"
(expand "fullset")
(("3" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (replace -1)
(("2"
(hide -1)
(("2"
(typepred "h!1")
(("2"
(inst + "h!1*a!1")
(("1"
(inst?)
(("1" (assert) nil nil)
("2"
(expand "fullset")
(("2" (propax) nil nil))
nil)
("3"
(expand "fullset")
(("3" (propax) nil nil))
nil)
("4"
(expand "fullset")
(("4" (propax) nil nil))
nil))
nil)
("2" (inst?) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((fullset_is_group formula-decl nil cosets nil)
(monoid? const-decl "bool" monoid_def nil)
(restrict const-decl "R" restrict nil)
(fullset const-decl "set" sets nil)
(S!1 skolem-const-decl "set[T]" cosets nil)
(h!2 skolem-const-decl "(S!1)" cosets nil)
(a!1 skolem-const-decl "T" cosets nil)
(b!1 skolem-const-decl "T" cosets nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(h!1 skolem-const-decl "(S!1)" cosets nil)
(* formal-const-decl "[T, T -> T]" cosets nil)
(* const-decl "set[T]" cosets nil) (set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(T formal-nonempty-type-decl nil cosets nil)
(boolean nonempty-type-decl nil booleans nil)
(associative? const-decl "bool" operator_defs nil)
(group? const-decl "bool" group_def nil))
nil))
(lr_coset_assoc 0
(lr_coset_assoc-1 nil 3405953143
("" (skosimp*)
(("" (lemma "fullset_is_group")
(("" (expand "group?")
(("" (expand "monoid?")
(("" (flatten)
(("" (hide -1 -3)
(("" (expand "associative?")
(("" (expand "restrict")
(("" (apply-extensionality 1 :hide? t)
(("" (expand "*")
(("" (iff 1)
(("" (prop)
(("1" (skosimp*)
(("1" (replace -1)
(("1"
(hide -1)
(("1"
(inst + "inv(a!1)*h!1*b!1")
(("1"
(inst
-
"a!1"
"inv(a!1) * h!1"
"b!1")
(("1"
(replace -1 * rl)
(("1"
(reveal -1)
(("1"
(inst
-
"a!1"
"inv(a!1)"
"h!1")
(("1"
(replace -1 * rl)
(("1"
(rewrite "inv_right")
(("1"
(rewrite
"left_identity")
nil
nil))
nil))
nil)
("2"
(expand "fullset")
(("2" (propax) nil nil))
nil)
("3"
(expand "fullset")
(("3" (propax) nil nil))
nil)
("4"
(expand "fullset")
(("4" (propax) nil nil))
nil))
nil))
nil))
nil)
("2"
(expand "fullset")
(("2" (propax) nil nil))
nil)
("3"
(expand "fullset")
(("3" (propax) nil nil))
nil)
("4"
(expand "fullset")
(("4" (propax) nil nil))
nil))
nil)
("2"
(typepred "h!1")
(("2"
(skosimp*)
(("2"
(replace -1)
(("2"
(inst + "h!2")
(("2"
(inst
-2
"inv[T, *, one](a!1)"
"a!1"
"h!2")
(("1"
(replace -2 * rl)
(("1"
(rewrite "inv_left")
(("1"
(rewrite
"left_identity")
nil
nil))
nil))
nil)
("2"
(expand "fullset")
(("2" (propax) nil nil))
nil)
("3"
(expand "fullset")
(("3" (propax) nil nil))
nil)
("4"
(expand "fullset")
(("4" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (replace -1)
(("2"
(hide -1)
(("2"
(inst + "(a!1*h!1)*inv(b!1)")
(("1"
(inst
-
"a!1 * h!1"
"inv(b!1)"
"b!1")
(("1"
(replace -1)
(("1"
(rewrite "inv_left")
(("1"
(rewrite "right_identity")
nil
nil))
nil))
nil)
("2"
(expand "fullset")
(("2" (propax) nil nil))
nil)
("3"
(expand "fullset")
(("3" (propax) nil nil))
nil)
("4"
(expand "fullset")
(("4" (propax) nil nil))
nil))
nil)
("2"
(typepred "h!1")
(("2"
(skosimp*)
(("2"
(replace -1)
(("2"
(inst + "h!2")
(("2"
(inst
-
"a!1"
"(h!2 * b!1)"
"inv[T, *, one](b!1)")
(("1"
(replace -2)
(("1"
(reveal -1)
(("1"
(hide -3)
(("1"
(inst?)
(("1"
(replace -1)
(("1"
(rewrite
"inv_right")
(("1"
(rewrite
"right_identity")
nil
nil))
nil))
nil)
("2"
(expand
"fullset")
(("2"
(propax)
nil
nil))
nil)
("3"
(expand
"fullset")
(("3"
(propax)
nil
nil))
nil)
("4"
(expand
"fullset")
(("4"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand "fullset")
(("2" (propax) nil nil))
nil)
("3"
(expand "fullset")
(("3" (propax) nil nil))
nil)
("4"
(expand "fullset")
(("4" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((fullset_is_group formula-decl nil cosets nil)
(monoid? const-decl "bool" monoid_def nil)
(restrict const-decl "R" restrict nil)
(b!1 skolem-const-decl "T" cosets nil)
(h!1 skolem-const-decl "({t: T | EXISTS (h: (S!1)): t = a!1 * h})"
cosets nil)
(a!1 skolem-const-decl "T" cosets nil)
(inv const-decl "{y | x * y = one AND y * x = one}" group nil)
(one formal-const-decl "T" cosets nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(* formal-const-decl "[T, T -> T]" cosets nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(S!1 skolem-const-decl "set[T]" cosets nil)
(inv_right formula-decl nil group nil)
(left_identity formula-decl nil monad nil)
(fullset const-decl "set" sets nil)
(inv_left formula-decl nil group nil)
(h!2 skolem-const-decl "(S!1)" cosets nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(h!1 skolem-const-decl "({t: T | EXISTS (h: (S!1)): t = h * b!1})"
cosets nil)
(right_identity formula-decl nil monad nil)
(h!2 skolem-const-decl "(S!1)" cosets nil)
(* const-decl "set[T]" cosets nil)
(* const-decl "set[T]" cosets nil) (set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(T formal-nonempty-type-decl nil cosets nil)
(boolean nonempty-type-decl nil booleans nil)
(associative? const-decl "bool" operator_defs nil)
(group? const-decl "bool" group_def nil))
nil))
(subset_left_coset 0
(subset_left_coset-1 nil 3406302438
("" (skosimp*)
(("" (expand "subset?")
(("" (skosimp*)
(("" (assert)
(("" (expand "member")
(("" (expand "*")
(("" (skosimp*)
(("" (inst + "h!1")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((subset? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(R!1 skolem-const-decl "set[T]" cosets nil)
(S!1 skolem-const-decl "set[T]" cosets nil)
(h!1 skolem-const-decl "(S!1)" cosets nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-nonempty-type-decl nil cosets nil)
(* const-decl "set[T]" cosets nil))
nil))
(subset_right_coset 0
(subset_right_coset-1 nil 3406302482
("" (skosimp*)
(("" (expand "subset?")
(("" (skosimp*)
(("" (expand "member")
(("" (expand "*")
(("" (skosimp*)
(("" (inst + "h!1")
(("" (inst?) (("" (assert) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((subset? const-decl "bool" sets nil)
(member const-decl "bool" sets nil)
(R!1 skolem-const-decl "set[T]" cosets nil)
(S!1 skolem-const-decl "set[T]" cosets nil)
(h!1 skolem-const-decl "(S!1)" cosets nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(T formal-nonempty-type-decl nil cosets nil)
(* const-decl "set[T]" cosets nil))
nil))
(right_coset_TCC1 0
(right_coset_TCC1-1 nil 3406294305
("" (skosimp*)
(("" (lemma "right_coset_subset") (("" (inst?) nil nil)) nil)) nil)
((right_coset_subset formula-decl nil cosets nil)
(T formal-nonempty-type-decl nil cosets nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil)
(* formal-const-decl "[T, T -> T]" cosets nil)
(one formal-const-decl "T" cosets nil)
(group? const-decl "bool" group_def nil)
(group nonempty-type-eq-decl nil group nil)
(subgroup? const-decl "bool" group_def nil)
(subgroup type-eq-decl nil group nil))
nil))
(right_coset_image_TCC1 0
(right_coset_image_TCC1-1 nil 3406037458 ("" (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)
(set type-eq-decl nil sets nil)
(group? const-decl "bool" group_def nil)
(group nonempty-type-eq-decl nil group nil)
(member const-decl "bool" sets nil)
(subset? const-decl "bool" sets nil)
(one formal-const-decl "T" cosets nil)
(* formal-const-decl "[T, T -> T]" cosets nil)
(T formal-nonempty-type-decl nil cosets nil)
(subgroup? const-decl "bool" group_def nil))
nil))
(right_coset_image 0
(right_coset_image-1 nil 3406037466
("" (skosimp*)
(("" (expand "restrict")
(("" (expand "right_coset")
(("" (expand "restrict")
(("" (apply-extensionality 1 :hide? t)
(("" (expand "image")
(("" (expand "*") (("" (propax) nil nil)) nil)) nil))
nil))
nil))
nil))
nil))
nil)
((restrict const-decl "R" restrict nil)
(T formal-nonempty-type-decl nil cosets nil)
(boolean nonempty-type-decl nil booleans nil)
(TRUE const-decl "bool" booleans nil)
(image const-decl "set[R]" function_image nil)
(group nonempty-type-eq-decl nil group nil)
(group? const-decl "bool" group_def nil)
(one formal-const-decl "T" cosets nil)
(* formal-const-decl "[T, T -> T]" cosets nil)
(* const-decl "set[T]" cosets nil) (set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(member const-decl "bool" sets nil)
(right_coset const-decl "{s: set[T] | subset?(s, G)}" cosets nil))
shostak))
(right_coset_is 0
(right_coset_is-1 nil 3292962829
("" (skosimp*)
(("" (typepred "G!1")
(("" (typepred "H!1")
(("" (assert)
((""
(case "subset?(right_coset(G!1, H!1)(a!1),{x: T | congruent_mod(G!1, H!1)(a!1, x)})")
(("1"
(case "subset?({x: T | congruent_mod(G!1, H!1)(a!1, x)},right_coset(G!1, H!1)(a!1))")
(("1"
(lemma "subset_antisymmetric"
("a" "right_coset(G!1, H!1)(a!1)" "b"
"{x: T | congruent_mod(G!1, H!1)(a!1, x)}"))
(("1" (assert) nil nil)) nil)
("2" (assert)
(("2" (expand "member")
(("2" (hide -1 2)
(("2" (expand "subset?")
(("2" (skosimp*)
(("2" (assert)
(("2" (expand "congruent_mod" -1 1)
(("2" (assert)
(("2"
(rewrite "subgroup_def")
(("2"
(flatten)
(("2"
(expand "inv_closed?")
(("2"
(inst - "a!1 * inv(x!1)")
(("1"
(rewrite "inv_star")
(("1"
(assert)
(("1"
(rewrite
"right_coset_image")
(("1"
(assert)
(("1"
(expand "restrict")
(("1"
(assert)
(("1"
(expand "image")
(("1"
(expand "member")
(("1"
(inst
+
"x!1*inv(a!1)")
(("1"
(rewrite
"associative")
(("1"
(rewrite
"inv_left")
(("1"
(rewrite
"right_identity")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand "member")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide 2)
(("2" (expand "subset?")
(("2" (skosimp*)
(("2" (rewrite "right_coset_image")
(("2" (expand "restrict")
(("2" (expand "image")
(("2" (assert)
(("2" (expand "congruent_mod")
(("2" (expand "member")
(("2"
(skosimp*)
(("2"
(typepred "x!2")
(("2"
(replace -2 1)
(("2"
(rewrite "inv_star")
(("2"
(rewrite
"associative"
1
:dir
rl)
(("2"
(rewrite "inv_right")
(("2"
(rewrite "left_identity")
(("2"
(lemma
"inv_member"
("G" "H!1" "x" "x!2"))
(("2"
(expand "member")
(("2"
(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)
((group nonempty-type-eq-decl nil group nil)
(group? const-decl "bool" group_def nil)
(one formal-const-decl "T" cosets nil)
(* formal-const-decl "[T, T -> T]" cosets nil)
(set type-eq-decl nil sets nil)
(T formal-nonempty-type-decl nil cosets nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(member const-decl "bool" sets nil)
(inv_member formula-decl nil group nil)
(left_identity formula-decl nil monad nil)
(inv_right formula-decl nil group nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(subset_antisymmetric formula-decl nil sets_lemmas nil)
(subgroup_def formula-decl nil group nil)
(inv_closed? const-decl "bool" group nil)
(inv_star formula-decl nil group nil)
(inv_inv formula-decl nil group nil)
(right_coset_image formula-decl nil cosets nil)
(restrict const-decl "R" restrict nil)
(image const-decl "set[R]" function_image nil)
(right_identity formula-decl nil monad nil)
(inv_left formula-decl nil group nil)
(associative formula-decl nil semigroup nil)
(TRUE const-decl "bool" booleans nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(inv const-decl "{y | x * y = one AND y * x = one}" group nil)
(subset? const-decl "bool" sets nil)
(subgroup? const-decl "bool" group_def nil)
(subgroup type-eq-decl nil group nil)
(right_coset const-decl "{s: set[T] | subset?(s, G)}" cosets nil)
(congruent_mod const-decl "bool" cosets nil))
shostak))
(right_coset_def 0
(right_coset_def-1 nil 3405953353
("" (skosimp*)
(("" (expand "right_coset")
(("" (expand "restrict")
(("" (expand "image")
(("" (expand "*") (("" (propax) nil nil)) nil)) nil))
nil))
nil))
nil)
((right_coset const-decl "{s: set[T] | subset?(s, G)}" cosets nil))
nil))
(nonempty_right_coset 0
(nonempty_right_coset-1 nil 3292974326
("" (skosimp*)
(("" (expand "right_coset")
(("" (expand "member")
(("" (expand "nonempty?")
(("" (expand "empty?")
(("" (expand "member")
(("" (expand "*")
(("" (inst - "a!1")
(("" (inst + "one")
(("1" (rewrite "one_left") nil nil)
("2" (assert) (("2" (rewrite "one_in") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((right_coset const-decl "{s: set[T] | subset?(s, G)}" cosets nil)
(nonempty? const-decl "bool" sets nil)
(T formal-nonempty-type-decl nil cosets nil)
(one_in formula-decl nil monad nil)
(monad? const-decl "bool" monad_def nil)
(monad nonempty-type-eq-decl nil monad nil)
(one_left formula-decl nil group 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]" cosets nil)
(one formal-const-decl "T" cosets nil)
(group? const-decl "bool" group_def nil)
(group nonempty-type-eq-decl nil group nil)
(H!1 skolem-const-decl "group[T, *, one]" cosets nil)
(* const-decl "set[T]" cosets nil)
(empty? const-decl "bool" sets nil)
(member const-decl "bool" sets nil))
shostak))
(right_coset_correspondence_TCC1 0
(right_coset_correspondence_TCC1-1 nil 3406469955
("" (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)
(set type-eq-decl nil sets nil)
(group? const-decl "bool" group_def nil)
(group nonempty-type-eq-decl nil group nil)
(right_coset const-decl "{s: set[T] | subset?(s, G)}" cosets nil)
(member const-decl "bool" sets nil)
(subset? const-decl "bool" sets nil)
(one formal-const-decl "T" cosets nil)
(* formal-const-decl "[T, T -> T]" cosets nil)
(T formal-nonempty-type-decl nil cosets nil)
(subgroup? const-decl "bool" group_def nil))
nil))
(right_coset_correspondence 0
(right_coset_correspondence-3 nil 3406302721
("" (skosimp*)
(("" (typepred "G!1")
(("" (expand "subgroup?")
(("" (assert)
(("" (inst + "LAMBDA (x:(A!1)): x*inv(a!1)*b!1")
(("1" (expand "bijective?")
(("1" (split)
(("1" (expand "injective?")
(("1" (skosimp*)
(("1"
(lemma "cancel_right"
("x" "x1!1" "z" "inv(a!1) * b!1" "y" "x2!1"))
(("1" (expand "group?")
(("1" (expand "monoid?")
(("1" (flatten)
(("1" (expand "associative?")
(("1"
(typepred "x1!1")
(("1"
(typepred "x2!1")
(("1"
(expand "inv_exists?")
(("1"
(assert)
(("1"
(rewrite
"associative"
1
:dir
rl)
(("1"
(rewrite
"associative"
1
:dir
rl)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "surjective?")
(("2" (skosimp*)
(("2" (typepred "y!1")
(("2" (replace -7)
(("2" (rewrite "right_coset_is" -1)
(("1" (assert)
(("1" (expand "congruent_mod")
(("1"
(assert)
(("1"
(lemma
"right_coset_is"
("H" "H!1" "G" "G!1" "a" "a!1"))
(("1"
(expand "subgroup?")
(("1"
(assert)
(("1"
(case "A!1(y!1*inv(b!1)*a!1)")
(("1"
(inst
+
"y!1 * inv(b!1) * a!1")
(("1"
(expand "group?")
(("1"
(expand "monoid?")
(("1"
(expand "associative?")
(("1"
(flatten)
(("1"
(lemma
"inv_member"
("x"
"a!1"
"G"
"G!1"))
(("1"
(lemma
"inv_member"
("x"
"b!1"
"G"
"G!1"))
(("1"
(assert)
(("1"
(hide-all-but
(-1
-2
-6
-7
-11
-12
1))
(("1"
(case
"G!1(y!1)")
(("1"
(inst-cp
-
"y!1 * inv(b!1)"
"a!1"
"inv(a!1)")
(("1"
(expand
"restrict")
(("1"
(assert)
(("1"
(inst
-
"y!1"
"inv(b!1)"
"b!1")
(("1"
(assert)
(("1"
(rewrite
"associative"
1)
(("1"
(rewrite
"associative"
1)
(("1"
(lemma
"associative")
(("1"
(inst-cp
-
"inv(b!1)"
"a!1"
"inv(a!1)")
(("1"
(replace
-2)
(("1"
(rewrite
"inv_right"
-2)
(("1"
(rewrite
"right_identity")
(("1"
(rewrite
"associative"
1)
(("1"
(rewrite
"inv_left"
+)
(("1"
(assert)
(("1"
(rewrite
"one_right")
nil
nil))
--> --------------------
--> maximum size reached
--> --------------------
¤ Dauer der Verarbeitung: 0.124 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
