|
(noetherian
(R_is_Noet_iff_TC_is 0
(R_is_Noet_iff_TC_is-1 nil 3374059634
("" (skeep)
(("" (split)
(("1" (flatten)
(("1" (expand "noetherian?")
(("1" (lemma "transitive_closure_preserves_well_foundedness")
(("1" (inst -1 "converse(R)")
(("1" (hide -2)
(("1"
(case-replace "transitive_closure[T] = TC" :hide? t)
(("1" (rewrite "TC_converse")
(("1" (lemma "well_founded_order_is_well_founded")
(("1" (inst -1 "converse(TC(R))") nil nil)) nil))
nil)
("2" (hide-all-but 1)
(("2" (expand* "transitive_closure" "TC") nil nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (flatten)
(("2" (expand "noetherian?")
(("2" (expand "well_founded?")
(("2" (skeep)
(("2" (inst?)
(("2" (assert)
(("2" (prop)
(("2" (hide -2)
(("2" (skolem * "y")
(("2" (inst 1 "y")
(("2" (skeep)
(("2" (inst -1 "x")
(("2"
(expand "converse")
(("2"
(expand* "TC" "IUnion")
(("2"
(inst 1 "1")
(("2"
(rewrite "iterate_1")
nil
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((transitive_converse application-judgement "(transitive?[T])"
relation_converse_props nil)
(noetherian? const-decl "bool" noetherian nil)
(R skolem-const-decl "PRED[[T, T]]" noetherian nil)
(PRED type-eq-decl nil defined_types nil)
(converse const-decl "pred[[T2, T1]]" relation_defs nil)
(well_founded? const-decl "bool" orders nil)
(pred type-eq-decl nil defined_types nil)
(bool nonempty-type-eq-decl nil booleans nil)
(boolean nonempty-type-decl nil booleans nil)
(TC const-decl "transitive" relations_closure nil)
(transitive type-eq-decl nil relations_closure nil)
(transitive_closure const-decl "(transitive?)" closure_ops
"orders/")
(= const-decl "[T, T -> boolean]" equalities nil)
(transitive? const-decl "bool" relations nil)
(well_founded_order_is_well_founded judgement-tcc nil
well_foundedness "orders/")
(well_founded_order? const-decl "bool" well_foundedness "orders/")
(TC_converse formula-decl nil relations_closure nil)
(transitive_closure_preserves_well_foundedness judgement-tcc nil
well_foundedness "orders/")
(T formal-type-decl nil noetherian nil)
(IUnion const-decl "set[T]" indexed_sets nil)
(iterate_1 formula-decl nil relation_iterate "orders/")
(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))
shostak))
(noetherian_induction 0
(noetherian_induction-1 nil 3374059706
("" (skolem * ("S1" "P"))
(("" (flatten)
(("" (typepred "S1")
(("" (lemma "R_is_Noet_iff_TC_is")
(("" (inst?)
(("" (assert)
(("" (hide -2)
((""
(rewrite "wf_induction[T, converse(TC(S1))]" :subst
("p" "P"))
(("1" (hide (-1 2))
(("1" (skeep)
(("1" (inst -2 "x")
(("1" (expand "converse")
(("1" (assert) nil nil)) nil))
nil))
nil))
nil)
("2" (hide (-2 2))
(("2" (expand "noetherian?")
(("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil))
nil)
((R_is_Noet_iff_TC_is formula-decl nil noetherian nil)
(well_founded? const-decl "bool" orders nil)
(transitive_converse application-judgement "(transitive?[T])"
relation_converse_props nil)
(wf_induction formula-decl nil wf_induction nil)
(pred type-eq-decl nil defined_types nil)
(converse const-decl "pred[[T2, T1]]" relation_defs nil)
(transitive? const-decl "bool" relations nil)
(transitive type-eq-decl nil relations_closure nil)
(TC const-decl "transitive" relations_closure 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 noetherian nil)
(PRED type-eq-decl nil defined_types nil)
(noetherian? const-decl "bool" noetherian nil)
(noetherian type-eq-decl nil noetherian nil))
shostak)))
[ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
]
|
