|
(well_nat
(well_lt_nat 0
(well_lt_nat-1 nil 3318616417
("" (skolem!)
(("" (lemma "wf_nat")
(("" (grind :if-match nil)
(("" (inst - "p!1")
(("" (split)
(("1" (skolem-typepred)
(("1" (expand "extend")
(("1" (prop)
(("1" (inst + "y!2")
(("1" (skolem!)
(("1" (inst - "x!1")
(("1" (expand "extend")
(("1" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
("2" (inst + "y!1")
(("2" (expand "extend") (("2" (propax) nil nil)) nil))
nil))
nil))
nil))
nil))
nil))
nil)
((wf_nat formula-decl nil naturalnumbers nil)
(extend const-decl "R" extend nil)
(FALSE const-decl "bool" booleans nil)
(pred type-eq-decl nil defined_types nil)
(x!1 skolem-const-decl "(p!1)" well_nat nil)
(y!2 skolem-const-decl "(extend[nat, (S!1), bool, FALSE](p!1))"
well_nat nil)
(p!1 skolem-const-decl "pred[(S!1)]" well_nat nil)
(S!1 skolem-const-decl "set[nat]" well_nat nil)
(boolean nonempty-type-decl nil booleans nil)
(bool nonempty-type-eq-decl nil booleans nil)
(NOT const-decl "[bool -> bool]" booleans nil)
(number nonempty-type-decl nil numbers nil)
(number_field_pred const-decl "[number -> boolean]" number_fields
nil)
(number_field nonempty-type-from-decl nil number_fields nil)
(real_pred const-decl "[number_field -> boolean]" reals nil)
(real nonempty-type-from-decl nil reals nil)
(rational_pred const-decl "[real -> boolean]" rationals nil)
(rational nonempty-type-from-decl nil rationals nil)
(integer_pred const-decl "[rational -> boolean]" integers nil)
(int nonempty-type-eq-decl nil integers nil)
(>= const-decl "bool" reals nil)
(nat nonempty-type-eq-decl nil naturalnumbers nil)
(set type-eq-decl nil sets nil)
(real_lt_is_strict_total_order name-judgement
"(strict_total_order?[real])" real_props nil)
(irreflexive_restrict application-judgement "(irreflexive?[S])"
restrict_order_props nil)
(antisymmetric_restrict application-judgement "(antisymmetric?[S])"
restrict_order_props nil)
(transitive_restrict application-judgement "(transitive?[S])"
restrict_order_props nil)
(strict_order_restrict application-judgement "(strict_order?[S])"
restrict_order_props nil)
(trichotomous_restrict application-judgement "(trichotomous?[S])"
restrict_order_props nil)
(strict_total_order_restrict application-judgement
"(strict_total_order?[S])" restrict_order_props nil)
(well_founded? const-decl "bool" orders nil)
(restrict const-decl "R" restrict nil)
(well_ordered? const-decl "bool" orders nil))
shostak))
(well_gt_nat 0
(well_gt_nat-1 nil 3318616896
("" (expand* "well_ordered?" "well_founded?")
(("" (skosimp* t)
(("" (lemma "non_empty_finite_has_greatest")
(("" (inst - "p!1" "<=")
(("1" (grind :if-match nil)
(("1" (inst + "t!1")
(("1" (skolem!)
(("1" (inst - "x!1") (("1" (assert) nil nil)) nil))
nil))
nil))
nil)
("2" (split)
(("1" (expand "is_finite")
(("1" (skolem!)
(("1"
(inst + "N!1"
"LAMBDA (x: (extend[nat, (F!1), bool, FALSE](p!1))): f!1(x)")
(("1" (expand "injective?")
(("1" (skosimp :preds? t)
(("1" (expand "extend")
(("1" (prop)
(("1" (inst - "x1!1" "x2!1")
(("1" (assert) nil nil)) nil))
nil))
nil))
nil))
nil)
("2" (skolem-typepred)
(("2" (expand "extend") (("2" (prop) nil nil))
nil))
nil))
nil))
nil))
nil)
("2" (grind) nil nil))
nil))
nil))
nil))
nil))
nil)
nil shostak)))
[ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
]
|
