(well_foundednessnil 3318615614"" (skolem!)"" (expand * "empty?" "member" "descending?" "well_founded?" )"" (prop)"1" (skolem!)"1" (inst - "LAMBDA x: EXISTS n: x = x!1(n)" )"1" (split)"1" (skosimp* t)"1" (replace -2 :hide? t)"1" (inst - "x!1(1 + n!1)" )"1" (inst?) nil nil ) ("2" (inst?) nil nil )) nil ))nil ))nil )"2" (inst + "x!1(0)" ) (("2" (inst?) nil nil )) nil ))nil ))nil ))nil )"2" (skosimp*)"2" (rewrite "skolemize_forall[(p!1), (p!1)]" )"2" (skolem!)"2" (inst - "LAMBDA n: iterate(f!1, n)(y!1)" )"2" (skolem!)"2" (expand "iterate" 1 1) (("2" (inst?) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" sets nil )"bool" orders nil )"bool" monotone_sequences nil )"bool" sets nil )"T" function_iterate nil )"T" well_foundedness nil )"pred[T]" well_foundedness nil )nil skolemization nil )"nat" well_foundedness nil )"[numfield, numfield -> numfield]" number_fields nil )nil number_fields nil )"sequence[T]" well_foundedness nil )"posint" nil )NOT const-decl "[bool -> bool]" booleans nil )nil sequences nil )"[T, T -> boolean]" equalities nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )nil defined_types nil )nil booleans nil )nil booleans nil )nil well_foundedness nil ))nil 3318615593"" (skolem-typepred)"" (rewrite "no_infinite_descending_sequence" )"" (expand * "empty?" "member" "descending?" "irreflexive?" )"" (skolem!)"" (inst - "LAMBDA n: x!2" ) (("" (skolem!) nil nil )) nil ))nil ))nil ))nil ))nil )nil well_foundednessnil )nil sequences nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"bool" sets nil )"bool" monotone_sequences nil )"bool" relations nil )"bool" sets nil )"bool" orders nil )nil defined_types nil )nil well_foundedness nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil ))nil 3318615593"" (judgement-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil well_foundedness nil )nil defined_types nil )"bool" orders nil )"bool" orders nil )"bool" orders nil )"bool" orders nil )"bool" relations nil )"bool" orders nil )"bool" relations nil )"bool" well_foundedness nil ))nil ))nil 3318615593"" (judgement-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil well_foundedness nil )nil defined_types nil )"bool" well_foundedness nil )"bool" relations nil )"bool" orders nil ))nil ))nil 3318615593"" (skolem-typepred)"" (expand * "strict_order?" "well_founded_order?" )"" (prop)"" (rewrite "well_founded_is_irreflexive" ) nil nil )) nil ))nil ))nil )"bool" orders nil )nil well_foundednessnil )"bool" orders nil )"bool" well_foundedness nil )nil defined_types nil )nil well_foundedness nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil ))nil 3318615593"" (skolem-typepred)"" (expand * "well_founded_order?" "well_founded?" )"" (skosimp*)"" "LAMBDA (y: T): EXISTS (x: T): preorder_closure[T](rel!1)(x, y) & p!1(x)" )"" (prop)"1" (skosimp* t)"1" (rewrite "preorder_closure_reflexive_transitive" )"1" (expand * "reflexive_closure" "union" "member" )"1" (split)"1" (hide 1)"1" (rewrite "transitive_closure_step_r" )"1" (expand "o" )"1" (skosimp)"1" (inst - "y!3" )"1" "x!1" )"1" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (inst + "x!1" )"2" (skolem!)"2" (rewrite "transitive_closure_step_r" )"2" (expand "o" )"2" (skosimp)"2" "y!3" )"1" (assert ) nil nil )"2" "2" (assert ) nil nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"2" (inst? 2)"2" (skolem!)"2" (inst + "y!1" )"2" (inst + "x!1" )"2" expand * "preorder_closure" "transitive_closure" "IUnion" )"2" (skolem!) (("2" (inst?) nil nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )"bool" well_foundedness nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" orders nil )"(preorder?)" closure_ops nil )"T" well_foundedness nil )"(transitive?)" closure_ops nil )"set[T]" indexed_sets nil )nil integers nil )"bool" reals nil )nil integers nil )nil naturalnumbers nil )"bool" reals nil )nil integers nil )"[rational -> boolean]" integers nil )nil rationals nil )"[real -> boolean]" rationals nil )nil reals nil )"[number_field -> boolean]" reals nil )nil number_fields nil )"[number -> boolean]" number_fieldsnil )nil numbers nil )"set" sets nil )"bool" sets nil )"(reflexive?)" closure_ops nil )"T" well_foundedness nil )"T" well_foundedness nil )"bool" relation_props nil )"(well_founded?[T])" well_foundedness nil )"T" well_foundedness nil )"pred[T]" well_foundedness nil )nil closure_ops nil )"(preorder?)" well_foundedness nil )nil closure_opsnil )"bool" orders nil )nil defined_types nil )nil well_foundedness nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil )))quality 100%
¤ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
