|
(finite_cyclic_groups
(IMP_finite_groups_TCC1 0
(IMP_finite_groups_TCC1-1 nil 3408118121
("" (rewrite "fullset_is_group") nil nil)
((fullset_is_group formula-decl nil finite_cyclic_groups nil)) nil))
(prime_order_cycle 0
(prime_order_cycle-2 nil 3407853657
("" (skosimp*)
(("" (expand "cyclic?")
(("" (expand "order")
(("" (case "card(G!1) > 1")
(("1" (case "(EXISTS (a: (G!1)): a /= one)")
(("1" (skosimp*)
(("1" (name "HH" "generated_by(a!1)")
(("1" (inst + "a!1")
(("1" (assert)
(("1" (replace -1)
(("1" (case "subgroup?(HH,G!1)")
(("1" (lemma "Lagrange")
(("1" (inst?)
(("1" (assert)
(("1"
(expand "prime?")
(("1"
(inst - "order(HH)")
(("1"
(expand "order")
(("1"
(split -5)
(("1" (propax) nil nil)
("2"
(assert)
(("2"
(flatten)
(("2"
(lemma
"generated_by_card_1")
(("2"
(inst?)
(("2"
(inst - "G!1")
(("2"
(expand "member")
(("2"
(propax)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("3"
(flatten)
(("3"
(assert)
(("3"
(hide -2 -4)
(("3"
(expand "subgroup?")
(("3"
(lemma
"same_card_subset[T]")
(("3"
(inst - "HH" "G!1")
(("3"
(assert)
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (typepred "G!1")
(("2"
(lemma "finite_subgroups")
(("2"
(inst?)
(("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (lemma "generated_is_subgroup")
(("2" (inst?)
(("2" (inst - "G!1")
(("2" (assert) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (hide -2 2)
(("2" (lemma "card_2_has_2[T]")
(("2" (inst - "G!1")
(("2" (assert)
(("2" (skosimp*)
(("2" (inst-cp + "x!1")
(("2" (inst + "y!1") (("2" (assert) nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (expand "prime?") (("2" (flatten) nil nil)) nil))
nil))
nil))
nil))
nil)
((cyclic? const-decl "boolean" group nil)
(finite_group nonempty-type-eq-decl nil group nil)
(finite_group? const-decl "bool" group_def nil)
(one formal-const-decl "T" finite_cyclic_groups nil)
(* formal-const-decl "[T, T -> T]" finite_cyclic_groups nil)
(card const-decl "{n: nat | n = Card(S)}" finite_sets nil)
(Card const-decl "nat" finite_sets nil)
(= const-decl "[T, T -> boolean]" equalities 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)
(finite_set type-eq-decl nil finite_sets nil)
(is_finite const-decl "bool" finite_sets nil)
(set type-eq-decl nil sets nil)
(T formal-nonempty-type-decl nil finite_cyclic_groups nil)
(> const-decl "bool" reals nil)
(bool nonempty-type-eq-decl nil booleans 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)
(boolean nonempty-type-decl nil booleans nil)
(number nonempty-type-decl nil numbers nil)
(y!1 skolem-const-decl "T" finite_cyclic_groups nil)
(x!1 skolem-const-decl "T" finite_cyclic_groups nil)
(G!1 skolem-const-decl "finite_group[T, *, one]"
finite_cyclic_groups nil)
(real_ge_is_total_order name-judgement "(total_order?[real])"
real_props nil)
(card_2_has_2 formula-decl nil finite_sets nil)
(generated_is_subgroup formula-decl nil cyclic_group nil)
(Lagrange formula-decl nil lagrange nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(finite_subgroups formula-decl nil group nil)
(finite_monad nonempty-type-eq-decl nil monad nil)
(finite_monad? const-decl "bool" monad_def nil)
(posnat nonempty-type-eq-decl nil integers nil)
(nonneg_int nonempty-type-eq-decl nil integers nil)
(member const-decl "bool" sets nil)
(generated_by_card_1 formula-decl nil finite_groups nil)
(subset_is_partial_order name-judgement "(partial_order?[set[T]])"
sets_lemmas nil)
(same_card_subset formula-decl nil finite_sets nil)
(prime? const-decl "bool" primes "ints/")
(HH skolem-const-decl "group[T, *, one]" finite_cyclic_groups nil)
(subgroup? const-decl "bool" group_def nil)
(real_gt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(generated_by const-decl "group" group nil)
(group nonempty-type-eq-decl nil group nil)
(group? const-decl "bool" group_def nil)
(/= const-decl "boolean" notequal nil)
(order const-decl "posnat" monad nil))
nil)
(prime_order_cycle-1 nil 3407082460
(";;; Proof prime_order_cycle-3 for formula finite_cyclic_groups.prime_order_cycle"
(skosimp*)
((";;; Proof prime_order_cycle-3 for formula finite_cyclic_groups.prime_order_cycle"
(expand "cyclic?")
((";;; Proof prime_order_cycle-3 for formula finite_cyclic_groups.prime_order_cycle"
(expand "order")
((";;; Proof prime_order_cycle-3 for formula finite_cyclic_groups.prime_order_cycle"
(case "card(G!1) > 1")
(("1" (case "(EXISTS (a: (G!1)): a /= one)")
(("1" (skosimp*)
(("1" (name "HH" "generated_by(a!1)")
(("1" (inst + "a!1")
(("1" (assert)
(("1" (replace -1)
(("1" (case "subgroup?(HH,G!1)")
(("1" (lemma "Lagrange")
(("1" (inst?)
(("1" (assert)
(("1"
(expand "prime?")
(("1"
(inst - "order(HH)")
(("1"
(expand "order")
(("1"
(assert)
(("1"
(split -5)
(("1"
(assert)
(("1"
(expand "divides")
(("1" (propax) nil)))))
("2"
(flatten)
(("2"
(lemma
"generated_by_card_1")
(("2"
(inst?)
(("2"
(inst - "G!1")
(("2"
(expand "member")
(("2"
(assert)
nil)))))))))))
("3"
(flatten)
(("3"
(assert)
(("3"
(hide -2 -4)
(("3"
(expand "subgroup?")
(("3"
(lemma
"same_card_subset[T]")
(("3"
(inst - "HH" "G!1")
(("3"
(assert)
nil)))))))))))))))))))))))))
("2" (typepred "G!1")
(("2"
(lemma "finite_subgroups")
(("2"
(inst?)
(("2" (assert) nil)))))))))))
("2" (lemma "generated_is_subgroup")
(("2" (inst?)
(("2" (inst - "G!1")
(("2" (assert) nil)))))))))))))))))))
("2" (hide -2 2)
(("2" (lemma "card_2_has_2[T]")
(("2" (inst - "G!1")
(("2" (assert)
(("2" (skosimp*)
(("2" (inst-cp + "x!1")
(("2" (inst + "y!1")
(("2" (assert) nil)))))))))))))))))
("2" (expand "prime?") (("2" (flatten) nil))))))))))
";;; developed with shostak decision procedures")
((cyclic? const-decl "boolean" group nil)
(finite_group nonempty-type-eq-decl nil group nil)
(finite_group? const-decl "bool" group_def nil)
(generated_is_subgroup formula-decl nil group nil)
(Lagrange formula-decl nil lagrange nil)
(finite_subgroups formula-decl nil group nil)
(finite_monad nonempty-type-eq-decl nil monad nil)
(finite_monad? const-decl "bool" monad_def nil)
(subgroup? const-decl "bool" group_def nil)
(generated_by const-decl "group" group nil)
(group nonempty-type-eq-decl nil group nil)
(group? const-decl "bool" group_def nil)
(order const-decl "posnat" monad nil))
nil)))
¤ Dauer der Verarbeitung: 0.4 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
