|
(cayleys
(S_TCC1 0
(S_TCC1-1 nil 3397579169
("" (lemma "fullset_is_group")
(("" (expand "group?")
(("" (expand "monoid?")
(("" (expand "monad?")
(("" (flatten)
(("" (assert)
(("" (expand "semigroup?") (("" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((group? const-decl "bool" group_def nil)
(monad? const-decl "bool" monad_def nil)
(member const-decl "bool" sets nil)
(monoid? const-decl "bool" monoid_def nil)
(fullset_is_group formula-decl nil cayleys nil))
nil))
(cayley_prep_TCC1 0
(cayley_prep_TCC1-1 nil 3407761054
("" (lemma "fullset_is_group") (("" (propax) nil nil)) nil)
((fullset_is_group formula-decl nil cayleys nil)) nil))
(cayley_prep_TCC2 0
(cayley_prep_TCC2-1 nil 3407763770 ("" (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-nonempty-type-decl nil cayleys nil)
(set type-eq-decl nil sets nil)
(* formal-const-decl "[T, T -> T]" cayleys nil)
(one formal-const-decl "T" cayleys nil)
(group? const-decl "bool" group_def nil)
(group nonempty-type-eq-decl nil group nil)
(member const-decl "bool" sets nil)
(star_closed? const-decl "bool" groupoid_def nil)
(restrict const-decl "R" restrict nil)
(identity? const-decl "bool" operator_defs nil)
(monad? const-decl "bool" monad_def nil)
(associative? const-decl "bool" operator_defs nil)
(monoid? const-decl "bool" monoid_def nil)
(inv_exists? const-decl "bool" group_def nil))
nil))
(cayley_prep 0
(cayley_prep-1 nil 3407761162
("" (skosimp*)
(("" (expand "bijective?")
(("" (prop)
(("1" (expand "injective?")
(("1" (skosimp*)
(("1" (lemma "cancel_left[T,*,one]")
(("1" (inst?) (("1" (assert) nil nil)) nil)) nil))
nil))
nil)
("2" (expand "surjective?")
(("2" (skosimp*)
(("2" (typepred "y!1")
(("2" (inst + "inv[T,*,one](a!1)*y!1")
(("1" (rewrite "assoc[T,*,one]")
(("1" (rewrite "inv_right[T,*,one]")
(("1" (rewrite "one_left[T,*,one]") nil nil)) nil))
nil)
("2" (lemma "inv_in[T,*,one]")
(("2" (inst?)
(("2" (assert)
(("2" (typepred "G!1")
(("2" (expand "group?")
(("2" (expand "monoid?")
(("2" (expand "monad?")
(("2"
(expand "groupoid?")
(("2"
(expand "star_closed?")
(("2"
(flatten)
(("2"
(assert)
(("2" (inst?) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((bijective? const-decl "bool" functions nil)
(surjective? const-decl "bool" functions nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(inv_in formula-decl nil group nil)
(monad? const-decl "bool" monad_def nil)
(member const-decl "bool" sets nil)
(star_closed? const-decl "bool" groupoid_def nil)
(monoid? const-decl "bool" monoid_def nil)
(assoc formula-decl nil group nil)
(one_left formula-decl nil group nil)
(inv_right formula-decl nil group nil)
(G!1 skolem-const-decl "group[T, *, one]" cayleys 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)
(a!1 skolem-const-decl "(G!1)" cayleys nil)
(y!1 skolem-const-decl "(G!1)" cayleys nil)
(injective? const-decl "bool" functions nil)
(one formal-const-decl "T" cayleys nil)
(* formal-const-decl "[T, T -> T]" cayleys nil)
(T formal-nonempty-type-decl nil cayleys nil)
(cancel_left formula-decl nil group nil)
(group nonempty-type-eq-decl nil group nil)
(group? const-decl "bool" group_def nil)
(set type-eq-decl nil sets nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil))
shostak))
(trans_is_group_TCC1 0
(trans_is_group_TCC1-1 nil 3407763770 ("" (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-nonempty-type-decl nil cayleys nil)
(set type-eq-decl nil sets nil)
(* formal-const-decl "[T, T -> T]" cayleys nil)
(one formal-const-decl "T" cayleys nil)
(group? const-decl "bool" group_def nil)
(group nonempty-type-eq-decl nil group nil)
(inv_exists? const-decl "bool" group_def nil)
(monoid? const-decl "bool" monoid_def nil)
(monad? const-decl "bool" monad_def nil)
(identity? const-decl "bool" operator_defs nil)
(member const-decl "bool" sets nil)
(star_closed? const-decl "bool" groupoid_def nil)
(restrict const-decl "R" restrict nil)
(associative? const-decl "bool" operator_defs nil))
nil))
(trans_is_group_TCC2 0
(trans_is_group_TCC2-1 nil 3407763770 ("" (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-nonempty-type-decl nil cayleys nil)
(set type-eq-decl nil sets nil)
(* formal-const-decl "[T, T -> T]" cayleys nil)
(one formal-const-decl "T" cayleys nil)
(group? const-decl "bool" group_def nil)
(group nonempty-type-eq-decl nil group nil)
(G!1 skolem-const-decl "group[T, *, one]" cayleys nil)
(inv_exists? const-decl "bool" group_def nil)
(monoid? const-decl "bool" monoid_def nil)
(associative? const-decl "bool" operator_defs nil)
(monad? const-decl "bool" monad_def nil)
(identity? const-decl "bool" operator_defs nil)
(restrict const-decl "R" restrict nil)
(star_closed? const-decl "bool" groupoid_def nil)
(member const-decl "bool" sets nil)
(empty? const-decl "bool" sets nil)
(nonempty? const-decl "bool" sets nil))
nil))
(trans_is_group_TCC3 0
(trans_is_group_TCC3-1 nil 3407763770
("" (skosimp*)
(("" (inst + "(LAMBDA (x:(G!1)): x)") (("" (grind) nil nil)) nil))
nil)
((T formal-nonempty-type-decl nil cayleys 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]" cayleys nil)
(one formal-const-decl "T" cayleys nil)
(group? const-decl "bool" group_def nil)
(group nonempty-type-eq-decl nil group nil)
(bijective? const-decl "bool" functions nil)
(maps type-eq-decl nil A_group nil)
(G!1 skolem-const-decl "group[T, *, one]" cayleys nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(surjective? const-decl "bool" functions nil)
(injective? const-decl "bool" functions nil))
nil))
(trans_is_group 0
(trans_is_group-1 nil 3407764162
("" (skosimp*)
(("" (expand "ML")
(("" (expand "restrict")
(("" (expand "group?")
(("" (prop)
(("1" (expand "monoid?")
(("1" (prop)
(("1" (expand "monad?")
(("1" (prop)
(("1" (grind :if-match nil)
(("1" (expand "o")
(("1" (expand "al")
(("1" (inst + "x!2*x!3")
(("1" (assert)
(("1"
(apply-extensionality 1 :hide? t)
(("1"
(rewrite "assoc[T,*,one]")
nil
nil))
nil))
nil)
("2" (typepred "G!1")
(("2"
(expand "group?")
(("2"
(expand "monoid?")
(("2"
(expand "monad?")
(("2"
(expand "star_closed?")
(("2"
(flatten)
(("2"
(assert)
(("2" (inst?) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "member")
(("2" (expand "al")
(("2" (expand "id")
(("2" (expand "identity")
(("2" (inst + "one")
(("1"
(apply-extensionality 1 :hide? t)
(("1"
(rewrite "one_left[T,*,one]")
nil
nil)
("2"
(skosimp*)
(("2"
(rewrite "one_left[T,*,one]")
(("2"
(typepred "s!1")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil)
("2"
(rewrite "one_in[T,*,one]")
(("1"
(typepred "G!1")
(("1"
(expand "group?")
(("1"
(expand "monoid?")
(("1" (propax) nil nil))
nil))
nil))
nil)
("2"
(lemma "fullset_is_group")
(("2"
(expand "group?")
(("2"
(expand "monoid?")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (expand "restrict")
(("3" (expand "identity?")
(("3" (skosimp*)
(("3" (expand "op")
(("3" (expand "restrict")
(("3"
(expand "o")
(("3"
(expand "id")
(("3"
(expand "identity")
(("3"
(prop)
(("1"
(apply-extensionality
1
:hide?
t)
nil
nil)
("2"
(apply-extensionality
1
:hide?
t)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "restrict")
(("2" (expand "op")
(("2" (expand "restrict")
(("2" (expand "o")
(("2" (expand "associative?")
(("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "inv_exists?")
(("2" (expand "op")
(("2" (expand "o")
(("2" (expand "id")
(("2" (expand "identity")
(("2" (expand "restrict")
(("2" (skosimp*)
(("2" (typepred "x!1")
(("2" (skosimp*)
(("2"
(inst + "al(G!1,inv[T,*,one](x!2))")
(("1"
(prop)
(("1"
(apply-extensionality 1 :hide? t)
(("1"
(expand "al")
(("1"
(replace -2)
(("1"
(assert)
(("1"
(rewrite "assoc[T,*,one]")
(("1"
(rewrite
"inv_right[T,*,one]")
(("1"
(rewrite
"one_left[T,*,one]")
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp*)
(("2"
(assert)
(("2"
(expand "al")
(("2"
(lemma "inv_in[T,*,one]")
(("2"
(inst?)
(("2"
(typepred "G!1")
(("2"
(expand "group?")
(("2"
(expand "monoid?")
(("2"
(expand "monad?")
(("2"
(expand
"star_closed?")
(("2"
(flatten)
(("2"
(assert)
(("2"
(inst?)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(skosimp*)
(("3"
(rewrite "inv_in[T,*,one]")
nil
nil))
nil))
nil)
("2"
(apply-extensionality 1 :hide? t)
(("1"
(expand "al")
(("1"
(replace -2)
(("1"
(assert)
(("1"
(rewrite "assoc[T,*,one]")
(("1"
(rewrite
"inv_left[T,*,one]")
(("1"
(rewrite
"one_left[T,*,one]")
nil
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(skosimp*)
(("2"
(typepred "x!2")
(("2"
(rewrite "inv_in[T,*,one]")
nil
nil))
nil))
nil))
nil))
nil)
("2"
(prop)
(("1"
(skosimp*)
(("1"
(expand "al")
(("1"
(lemma "inv_in[T,*,one]")
(("1"
(inst?)
(("1"
(typepred "x1!1")
(("1"
(typepred "G!1")
(("1"
(expand "group?")
(("1"
(expand "monoid?")
(("1"
(expand "monad?")
(("1"
(expand
"star_closed?")
(("1"
(flatten)
(("1"
(assert)
(("1"
(inst?)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(expand "al")
(("2"
(expand "bijective?")
(("2"
(prop)
(("1"
(expand "injective?")
(("1"
(skosimp*)
(("1"
(typepred "x1!1")
(("1"
(typepred "x2!1")
(("1"
(replace -6)
(("1"
(assert)
(("1"
(inst
-4
"x1!1"
"x2!1")
(("1"
(assert)
(("1"
(lemma
"cancel_left[T,*,one]")
(("1"
(inst?)
(("1"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2"
(hide -1)
(("2"
(expand "surjective?")
(("2"
(skosimp*)
(("2"
(inst + "x!2*y!1")
(("1"
(rewrite
"assoc[T,*,one]")
(("1"
(rewrite
"inv_left[T,*,one]")
(("1"
(rewrite
"one_left[T,*,one]")
nil
nil))
nil))
nil)
("2"
(typepred "G!1")
(("2"
(expand "group?")
(("2"
(expand
"monoid?")
(("2"
(expand
"monad?")
(("2"
(expand
"star_closed?")
(("2"
(expand
"member")
(("2"
(inst?)
(("2"
(flatten)
(("2"
(inst?)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(inst + "inv[T, *, one](x!2)")
(("3"
(lemma "inv_in[T,*,one]")
(("3" (inst?) nil nil))
nil))
nil))
nil)
("3"
(lemma "inv_in[T,*,one]")
(("3" (inst?) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((ML const-decl "set[maps(S)]" cayleys nil)
(group? const-decl "bool" group_def nil)
(y!1 skolem-const-decl "(G!1)" cayleys nil)
(cancel_left formula-decl nil group nil)
(inv_in formula-decl nil group nil)
(inv_right formula-decl nil group nil)
(inv_left formula-decl nil group nil)
(x!2 skolem-const-decl "(G!1)" cayleys nil)
(inv const-decl "{y | x * y = one AND y * x = one}" group nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(monoid? const-decl "bool" monoid_def nil)
(composition_bijective application-judgement "(bijective?[T1, T3])"
function_props nil)
(monad? const-decl "bool" monad_def nil)
(id const-decl "maps(S)" A_group nil)
(one_left formula-decl nil group nil)
(fullset_is_group formula-decl nil cayleys nil)
(one_in formula-decl nil monad nil)
(monad nonempty-type-eq-decl nil monad nil)
(fullset const-decl "set" sets nil)
(identity const-decl "(bijective?[T, T])" identity nil)
(T formal-nonempty-type-decl nil cayleys nil)
(op const-decl "[maps(S), maps(S) -> maps(S)]" A_group nil)
(member const-decl "bool" sets nil)
(star_closed? const-decl "bool" groupoid_def nil)
(al const-decl "[(S) -> T]" cayleys nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(maps type-eq-decl nil A_group nil)
(bijective? const-decl "bool" functions nil)
(group nonempty-type-eq-decl nil group nil)
(one formal-const-decl "T" cayleys nil)
(* formal-const-decl "[T, T -> T]" cayleys nil)
(set type-eq-decl nil sets nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(surjective? const-decl "bool" functions nil)
(injective? const-decl "bool" functions nil)
(identity? const-decl "bool" operator_defs nil)
(associative? const-decl "bool" operator_defs nil)
(inv_exists? const-decl "bool" group_def nil)
(assoc formula-decl nil group nil)
(x!3 skolem-const-decl "(G!1)" cayleys nil)
(x!2 skolem-const-decl "(G!1)" cayleys nil)
(G!1 skolem-const-decl "group[T, *, one]" cayleys nil)
(O const-decl "T3" function_props nil)
(restrict const-decl "R" restrict nil))
shostak))
(Cayleys_TCC1 0
(Cayleys_TCC1-1 nil 3407763770
("" (skosimp*) (("" (rewrite "trans_is_group") nil nil)) nil)
((trans_is_group formula-decl nil cayleys nil)
(T formal-nonempty-type-decl nil cayleys 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]" cayleys nil)
(one formal-const-decl "T" cayleys nil)
(group? const-decl "bool" group_def nil)
(group nonempty-type-eq-decl nil group nil))
nil))
(Cayleys_TCC2 0
(Cayleys_TCC2-1 nil 3407763770
("" (skosimp*)
(("" (rewrite "A_is_group")
(("" (hide 2)
(("" (expand "nonempty?")
(("" (expand "empty?")
(("" (expand "member")
(("" (inst - "one")
(("" (lemma "one_in[T,*,one]")
(("1" (inst?)
(("1" (typepred "G!1")
(("1" (expand "group?")
(("1" (expand "monoid?")
(("1" (flatten) nil nil)) nil))
nil))
nil))
nil)
("2" (lemma "fullset_is_group")
(("2" (expand "group?")
(("2" (expand "monoid?")
(("2" (flatten) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((A_is_group formula-decl nil A_group nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(set type-eq-decl nil sets nil)
(nonempty? const-decl "bool" sets nil)
(* formal-const-decl "[T, T -> T]" cayleys nil)
(one formal-const-decl "T" cayleys nil)
(group? const-decl "bool" group_def nil)
(group nonempty-type-eq-decl nil group nil)
(T formal-nonempty-type-decl nil cayleys nil)
(member const-decl "bool" sets nil)
(one_in formula-decl nil monad nil)
(fullset const-decl "set" sets nil)
(monad? const-decl "bool" monad_def nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(monoid? const-decl "bool" monoid_def nil)
(G!1 skolem-const-decl "group[T, *, one]" cayleys nil)
(monad nonempty-type-eq-decl nil monad nil)
(fullset_is_group formula-decl nil cayleys nil)
(empty? const-decl "bool" sets nil))
nil))
(Cayleys 0
(Cayleys-2 nil 3407763539
("" (skosimp*)
(("" (expand "isomorphic?")
(("" (expand "isomorphism?")
(("" (inst + "(LAMBDA (a:(G!1)): (LAMBDA (s:(G!1)): a*s))")
(("1" (prop)
(("1" (expand "bijective?")
(("1" (prop)
(("1" (expand "injective?")
(("1" (skosimp*)
(("1"
(case "(LAMBDA (s: (G!1)): x1!1 * s)(one) = (LAMBDA (s: (G!1)): x2!1 * s)(one)")
(("1" (assert)
(("1" (hide -2)
(("1" (rewrite "one_right[T,*,one]")
(("1" (rewrite "one_right[T,*,one]") nil
nil))
nil))
nil))
nil)
("2" (replace -1) (("2" (propax) nil nil)) nil)
("3" (hide -1 2)
(("3" (rewrite "one_in[T,*,one]")
(("1" (typepred "G!1")
(("1" (expand "group?")
(("1"
(expand "monoid?")
(("1" (propax) nil nil))
nil))
nil))
nil)
("2" (lemma "fullset_is_group")
(("2" (expand "group?")
(("2"
(expand "monoid?")
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "surjective?")
(("2" (skosimp*)
(("2" (typepred "y!1")
(("2" (expand "ML")
(("2" (expand "restrict")
(("2" (skosimp*)
(("2" (expand "al")
(("2"
(inst + "x!1")
(("2"
(replace -2)
(("2" (propax) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "homomorphism?")
(("2" (skosimp*)
(("2" (apply-extensionality 1 :hide? t)
(("1" (expand "op")
(("1" (expand "restrict")
(("1" (expand "o")
(("1" (typepred "G!1")
(("1" (expand "group?")
(("1" (expand "monoid?")
(("1"
(expand "monad?")
(("1"
(expand "groupoid?")
(("1"
(flatten)
(("1"
(expand "associative?")
(("1"
(expand "restrict")
(("1" (inst?) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "cayley_prep") (("2" (inst?) nil nil))
nil)
("3" (skosimp*)
(("3" (typepred "G!1")
(("3" (expand "group?")
(("3" (expand "monoid?")
(("3" (flatten)
(("3" (expand "monad?")
(("3"
(expand "groupoid?")
(("3"
(expand "star_closed?")
(("3"
(flatten)
(("3"
(assert)
(("3" (inst?) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("4" (expand "bijective?")
(("4" (prop)
(("1" (expand "injective?")
(("1" (skosimp*)
(("1" (lemma "cancel_left[T,*,one]")
(("1" (inst?) (("1" (assert) nil nil))
nil))
nil))
nil))
nil)
("2" (expand "surjective?")
(("2" (skosimp*)
(("2" (typepred "y!1")
(("2" (inst + "inv[T,*,one](a!1)*y!1")
(("1"
(rewrite "assoc[T,*,one]")
(("1"
(rewrite "inv_right[T,*,one]")
(("1"
(rewrite "one_left[T,*,one]")
nil
nil))
nil))
nil)
("2"
(lemma "inv_in[T,*,one]")
(("2"
(inst?)
(("2"
(typepred "G!1")
(("2"
(expand "group?")
(("2"
(expand "monoid?")
(("2"
(flatten)
(("2"
(expand "monad?")
(("2"
(expand "groupoid?")
(("2"
(expand "star_closed?")
(("2"
(flatten)
(("2"
(assert)
(("2"
(inst?)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("5" (skosimp*)
(("5" (typepred "s!1")
(("5" (typepred "a!1")
(("5" (typepred "G!1")
(("5" (expand "group?")
(("5" (expand "monoid?")
(("5"
(expand "monad?")
(("5"
(flatten)
(("5"
(assert)
(("5"
(expand "groupoid?")
(("5"
(expand "star_closed?")
(("5"
(assert)
(("5" (inst?) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (skosimp*)
(("2" (lemma "cayley_prep")
(("2" (inst?)
(("2" (assert)
(("2" (expand "ML")
(("2" (expand "restrict")
(("2" (expand "al")
(("2" (inst + "a!1") nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3" (skosimp*)
(("3" (typepred "s!1")
(("3" (typepred "a!1")
(("3" (typepred "G!1")
(("3" (expand "group?")
(("3" (expand "monoid?")
(("3" (expand "monad?")
(("3" (flatten)
(("3" (assert)
(("3" (expand "groupoid?")
(("3"
(expand "star_closed?")
(("3"
(assert)
(("3" (inst?) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((isomorphic? const-decl "bool" homomorphisms nil)
(G!1 skolem-const-decl "group[T, *, one]" cayleys nil)
(group nonempty-type-eq-decl nil group nil)
(group? const-decl "bool" group_def nil)
(one formal-const-decl "T" cayleys nil)
(* formal-const-decl "[T, T -> T]" cayleys 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 cayleys nil)
(ML const-decl "set[maps(S)]" cayleys nil)
(maps type-eq-decl nil A_group nil)
(semigroup nonempty-type-eq-decl nil semigroup nil)
(restrict const-decl "R" restrict nil)
(associative? const-decl "bool" operator_defs nil)
(star_closed? const-decl "bool" groupoid_def nil)
(bijective? const-decl "bool" functions nil)
(AND const-decl "[bool, bool -> bool]" booleans nil)
(homomorphism? const-decl "bool" homomorphisms nil)
(nonempty? const-decl "bool" sets nil)
(op const-decl "[maps(S), maps(S) -> maps(S)]" A_group nil)
(b!1 skolem-const-decl "(G!1)" cayleys nil)
(a!1 skolem-const-decl "(G!1)" cayleys nil)
(O const-decl "T3" function_props nil)
(cayley_prep formula-decl nil cayleys nil)
(member const-decl "bool" sets nil)
(cancel_left formula-decl nil group nil)
(inv const-decl "{y | x * y = one AND y * x = one}" group nil)
(y!1 skolem-const-decl "(G!1)" cayleys nil)
(inv_right formula-decl nil group nil)
(one_left formula-decl nil group nil)
(assoc formula-decl nil group nil)
(inv_in formula-decl nil group nil)
(surjective? const-decl "bool" functions nil)
(al const-decl "[(S) -> T]" cayleys nil)
(injective? const-decl "bool" functions nil)
(= const-decl "[T, T -> boolean]" equalities nil)
(one_right formula-decl nil group nil)
(fullset const-decl "set" sets nil)
(monad nonempty-type-eq-decl nil monad nil)
(monad? const-decl "bool" monad_def nil)
(one_in formula-decl nil monad nil)
(monoid? const-decl "bool" monoid_def nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(fullset_is_group formula-decl nil cayleys nil)
(isomorphism? const-decl "bool" homomorphisms nil))
nil)
(Cayleys-1 nil 3397576546
("" (skosimp*)
(("" (expand "isomorphic?")
(("" (expand "isomorphism?")
(("" (expand "homomorphism?")
(("" (inst + "(LAMBDA (a:(G!1)): (LAMBDA (s:(G!1)): a*s))")
(("1" (expand "restrict")
(("1" (prop)
(("1" (expand "bijective?")
(("1" (prop)
(("1" (expand "injective?")
(("1" (skosimp*)
(("1"
(case "(LAMBDA (s: (G!1)): x1!1 * s)(one) = (LAMBDA (s: (G!1)): x2!1 * s)(one)")
(("1" (hide -2)
(("1" (assert)
(("1"
(rewrite "right_identity[(G!1),*,one]")
(("1"
(rewrite
"right_identity[(G!1),*,one]")
(("1"
(inst + "one")
(("1"
(assert)
(("1"
(lemma "one_in[(G!1),*,one]")
(("1"
(inst?)
(("1" (postpone) nil nil))
nil)
("2" (postpone) nil nil)
("3" (postpone) nil nil)
("4" (postpone) nil nil))
nil))
nil))
nil)
("2" (postpone) nil nil)
("3" (postpone) nil nil))
nil)
("2" (postpone) nil nil)
("3" (postpone) nil nil)
("4" (postpone) nil nil))
nil))
nil))
nil)
("2" (postpone) nil nil)
("3" (postpone) nil nil))
nil))
nil))
nil)
("2" (postpone) nil nil))
nil))
nil)
("2" (postpone) nil nil))
nil))
nil)
("2" (postpone) nil nil) ("3" (postpone) nil nil)
("4" (postpone) nil nil))
nil))
nil))
nil))
nil))
nil)
nil shostak)))
¤ Dauer der Verarbeitung: 0.120 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.
|
