(minmax_ordersnil 3315155075"" "LAMBDA (lesseq: pred[[T, T]]): LAMBDA (S: (LAMBDA (S): has_greatest?(S, lesseq))): choose[(S)]({t: (S) | greatest?(t, S, lesseq)})" )"" (grind :if-match nil ) (("" (inst? -3) nil nil )) nil )) nil )"bool" sets nil )"bool" sets nil )"bool" bounded_orders nil )NOT const-decl "[bool -> bool]" booleans nil )"(p)" sets nil )"bool" sets nil )"bool" minmax_orders nil )"bool" minmax_orders nil )set type-eq-decl nil sets nil )nil defined_types nil )nil booleans nil )nil booleans nil )nil minmax_orders nil ))nil ))nil 3315155267 ("" (grind) nil nil )"T" minmax_orders nil )"set[T]" minmax_orders nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil minmax_orders nil )"bool" bounded_orders nil )"bool" minmax_orders nil )"bool" bounded_orders nil ))nil 3315155075"" (judgement-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )set type-eq-decl nil sets nil )nil defined_types nil )"bool" minmax_orders nil )"(greatest?)" minmax_orders nil )nil minmax_orders nil )"bool" bounded_orders nil )"bool" bounded_orders nil ))nil ))nil 3315155075"" (skolem-typepred)"" (expand * "least_bounded_above?" "has_greatest?" )"" (skolem!)"" (inst?)"" (rewrite "greatest_is_least_upper_bound" ) nil nil ))nil ))nil ))nil ))nil )"bool" bounded_orders nil )"bool" minmax_orders nil )nil minmax_orders nil )"bool" minmax_orders nil )nil defined_types nil )set type-eq-decl nil sets nil )nil minmax_orders nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil ))nil 3315155075"" (skolem-typepred)"" (rewrite "has_greatest_is_least_bounded_above" ) nil nil )) nil )nil nil )"bool" minmax_orders nil )nil defined_types nil )set type-eq-decl nil sets nil )"bool" relations nil )nil defined_types nil )nil minmax_orders nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil ))nil 3315155331"" (skolem-typepred)"" (use "unique_least_upper_bound" )"" (rewrite "greatest_is_least_upper_bound" ) nil nil )) nil ))nil )nil bounded_orders nil )"(antisymmetric?[T])" minmax_orders nil )"(LAMBDA (S): has_greatest?(S, ale!1))" nil )"(LAMBDA (t): least_upper_bound?(t, S, <=))" nil )"bool" bounded_orders nil )"{t: (S) | greatest?(t, S, <=)}" minmax_ordersnil )"bool" minmax_orders nil )"bool" bounded_orders nil )nil minmax_orders nil )"bool" minmax_orders nil )nil defined_types nil )set type-eq-decl nil sets nil )"bool" relations nil )nil defined_types nil )nil minmax_orders nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil 3315155424"" (skolem-typepred)"" (rewrite "greatest_iff_least_upper_bound" )"" (rewrite "greatest_iff_least_upper_bound" )"" (flatten) (("" (use "unique_least_upper_bound" ) nil nil ))nil ))nil ))nil ))nil )nil minmax_orders nil )nil bounded_orders nil )"bool" bounded_orders nil )"(LAMBDA (t): greatest?(t, S!1, lesseqp!1))" nil )"(antisymmetric?[T])" minmax_ordersnil )"set[T]" minmax_orders nil )"(LAMBDA (t): greatest?(t, S!1, lesseqp!1))" nil )"bool" minmax_orders nil )nil defined_types nil )set type-eq-decl nil sets nil )"bool" relations nil )nil defined_types nil )nil minmax_orders nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil 3315155468"" (skosimp :preds? t)"" expand * "maximal?" "greatest?" "member" "upper_bound?" "antisymmetric?" )"" (prop)"" (skosimp)"" (inst - "r!1" )"" (inst - "t!1" "r!1" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"bool" minmax_orders nil )"bool" bounded_orders nil )"bool" minmax_orders nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil minmax_orders nil )nil defined_types nil )"bool" relations nil ))nil 3315155503"" (skosimp :preds? t)"" expand * "maximal?" "greatest?" "member" "upper_bound?" "dichotomous?" )"" (prop)"" (skolem!)"" (inst + "r!1" )"" (inst - "t!1" "r!1" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"bool" minmax_orders nil )"bool" bounded_orders nil )"bool" minmax_orders nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil minmax_orders nil )nil defined_types nil )"bool" orders nil ))nil 3315156295"" (skolem-typepred)"" (use "max_lem[T, le!1]" )"" (assert )"" expand * "has_greatest?" "greatest?" "member" "upper_bound?" )"" (inst? +) (("" (ground) nil nil )) nil )) nil ))nil ))nil ))nil )nil finite_sets_minmax "finite_sets/" )max const-decl"{a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES x <= a)}" "finite_sets/" )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" minmax_orders nil )"bool" bounded_orders nil )"bool" minmax_orders nil )"bool" orders nil )nil defined_types nil )nil finite_sets nil )"bool" sets nil )nil finite_sets nil )"bool" finite_sets nil )set type-eq-decl nil sets nil )nil minmax_orders nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil 3315156353"" (skolem!)"" (invoke (typepred "%1" ) (! 1 r))"" (expand * "greatest?" "upper_bound?" )"" (flatten) (("" (inst - "m!1" ) nil nil )) nil )) nil ))nil ))nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil minmax_orders nil )set type-eq-decl nil sets nil )nil defined_types nil )"bool" minmax_orders nil )"bool" minmax_orders nil )"{t: (S) | greatest?(t, S, <=)}" minmax_ordersnil )"bool" bounded_orders nil ))nil 3315156389"" (skosimp)"" (invoke (typepred "%1" "%2" ) (! 1 l) (! 1 r))"" (expand "greatest?" )"" (flatten)"" (hide -2)"" (expand "upper_bound?" )"" (inst?)"" (expand * "subset?" "member" )"" (inst?) (("" (assert ) nil nil )) nil )) nil ))nil ))nil ))nil ))nil ))nil ))nil ))nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil minmax_orders nil )set type-eq-decl nil sets nil )nil defined_types nil )"bool" minmax_orders nil )"bool" minmax_orders nil )"{t: (S) | greatest?(t, S, <=)}" minmax_ordersnil )"(LAMBDA (S): has_greatest?(S, lesseqp!1))" nil )"(LAMBDA (S): has_greatest?(S, lesseqp!1))" nil )"pred[[T, T]]" minmax_orders nil )"bool" sets nil )"bool" sets nil )"bool" bounded_orders nil ))nil 3315156422"" (skolem-typepred)"" (rewrite "greatest_iff_least_upper_bound" )"" (prop)"1" (rewrite "greatest_equals_lub" )"1" (rewrite "lub_def" ) nil nil )) nil )"2" (use "greatest_member" ) (("2" (assert ) nil nil )) nil )"3" (rewrite "greatest_equals_lub" )"3" (rewrite "lub_def" ) nil nil )) nil ))nil ))nil ))nil )nil minmax_orders nil )nil minmax_orders nil )nil bounded_orders nil )"bool" bounded_orders nil )"bool" minmax_orders nil )nil defined_types nil )set type-eq-decl nil sets nil )"bool" relations nil )nil defined_types nil )nil minmax_orders nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil 3315156724"" (skolem-typepred)"" (invoke (typepred "%1" ) (! 1 l 1))"" (expand "greatest?" )"" (prop)"1" expand * "upper_bound?" "partial_order?" "preorder?" "transitive?" )"1" (skosimp :preds? t)"1" (inst?)"1" (inst - "r!1" "greatest(lesseqp!1)(S!1)" "t!1" )"1" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (expand "upper_bound?" ) (("2" (inst?) nil nil )) nil ))nil ))nil ))nil ))nil )"bool" minmax_orders nil )"{t: (S) | greatest?(t, S, <=)}" minmax_ordersnil )"bool" bounded_orders nil )"bool" orders nil )"bool" relations nil )"bool" minmax_orders nil )set type-eq-decl nil sets nil )"bool" orders nil )nil defined_types nil )nil minmax_orders nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil 3315155075"" "LAMBDA (lesseq: pred[[T, T]]): LAMBDA (S: (LAMBDA (S): has_least?(S, lesseq))): choose[(S)]({t: (S) | least?(t, S, lesseq)})" )"" (grind :if-match nil ) (("" (inst? -3) nil nil )) nil )) nil )"bool" sets nil )"bool" sets nil )"bool" bounded_orders nil )NOT const-decl "[bool -> bool]" booleans nil )"(p)" sets nil )"bool" sets nil )"bool" minmax_orders nil )"bool" minmax_orders nil )set type-eq-decl nil sets nil )nil defined_types nil )nil booleans nil )nil booleans nil )nil minmax_orders nil ))nil ))nil 3315156851 ("" (grind) nil nil )"T" minmax_orders nil )"set[T]" minmax_orders nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )nil minmax_orders nil )"bool" bounded_orders nil )"bool" minmax_orders nil )"bool" bounded_orders nil ))nil 3315155075"" (judgement-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )set type-eq-decl nil sets nil )nil defined_types nil )"bool" minmax_orders nil )"(least?)" minmax_orders nil )nil minmax_orders nil )"bool" bounded_orders nil )"bool" bounded_orders nil ))nil ))nil 3315155075"" (skolem-typepred)"" (expand * "greatest_bounded_below?" "has_least?" )"" (skolem!)"" (inst?)"" (rewrite "least_is_greatest_lower_bound" ) nil nil ))nil ))nil ))nil ))nil )"bool" bounded_orders nil )"bool" minmax_orders nil )nil minmax_orders nil )"bool" minmax_orders nil )nil defined_types nil )set type-eq-decl nil sets nil )nil minmax_orders nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil ))nil 3315155075"" (skolem-typepred)"" (rewrite "has_least_is_greatest_bounded_below" ) nil nil )) nil )nil nil )"bool" minmax_orders nil )nil defined_types nil )set type-eq-decl nil sets nil )"bool" relations nil )nil defined_types nil )nil minmax_orders nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil ))nil 3315156935"" (skolem-typepred)"" (use "unique_greatest_lower_bound" )"" (rewrite "least_is_greatest_lower_bound" ) nil nil )) nil ))nil )nil bounded_orders nil )"(antisymmetric?[T])" minmax_orders nil )"(LAMBDA (S): has_least?(S, ale!1))" nil )"(LAMBDA (t): greatest_lower_bound?(t, S, <=))" nil )"bool" bounded_orders nil )"{t: (S) | least?(t, S, <=)}" minmax_orders nil )"bool" minmax_orders nil )"bool" bounded_orders nil )nil minmax_orders nil )"bool" minmax_orders nil )nil defined_types nil )set type-eq-decl nil sets nil )"bool" relations nil )nil defined_types nil )nil minmax_orders nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil 3315156954"" (skolem-typepred)"" (rewrite "least_iff_greatest_lower_bound" )"" (rewrite "least_iff_greatest_lower_bound" )"" (flatten)"" (use "unique_greatest_lower_bound" ) nil nil )) nil ))nil ))nil ))nil )nil minmax_orders nil )nil bounded_orders nil )"bool" bounded_orders nil )"(LAMBDA (t): least?(t, S!1, lesseqp!1))" nil )"(antisymmetric?[T])" minmax_ordersnil )"set[T]" minmax_orders nil )"(LAMBDA (t): least?(t, S!1, lesseqp!1))" nil )"bool" minmax_orders nil )nil defined_types nil )set type-eq-decl nil sets nil )"bool" relations nil )nil defined_types nil )nil minmax_orders nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil 3315156973"" (skosimp :preds? t)"" expand * "minimal?" "least?" "member" "lower_bound?" "antisymmetric?" )"" (prop)"" (skosimp)"" (inst - "r!1" )"" (inst - "t!1" "r!1" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"bool" minmax_orders nil )"bool" bounded_orders nil )"bool" minmax_orders nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil minmax_orders nil )nil defined_types nil )"bool" relations nil ))nil 3315157008"" (skosimp :preds? t)"" expand * "minimal?" "least?" "member" "lower_bound?" "dichotomous?" )"" (prop)"" (skolem!)"" (inst + "r!1" )"" (inst - "t!1" "r!1" ) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )"bool" minmax_orders nil )"bool" bounded_orders nil )"bool" minmax_orders nil )set type-eq-decl nil sets nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil minmax_orders nil )nil defined_types nil )"bool" orders nil ))nil 3315157031"" (skolem-typepred)"" (use "min_lem[T, le!1]" )"" (assert )"" (expand * "has_least?" "least?" "member" "lower_bound?" )"" (inst? +) (("" (ground) nil nil )) nil )) nil ))nil ))nil ))nil )nil finite_sets_minmax "finite_sets/" )min const-decl"{a: T | SS(a) AND (FORALL (x: T): SS(x) IMPLIES a <= x)}" "finite_sets/" )"[bool, bool -> bool]" booleans nil )AND const-decl "[bool, bool -> bool]" booleans nil )"bool" minmax_orders nil )"bool" bounded_orders nil )"bool" minmax_orders nil )"bool" orders nil )nil defined_types nil )nil finite_sets nil )"bool" sets nil )nil finite_sets nil )"bool" finite_sets nil )set type-eq-decl nil sets nil )nil minmax_orders nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil 3315157082"" (skolem!)"" (invoke (typepred "%1" ) (! 1 l))"" (expand * "least?" "lower_bound?" )"" (flatten) (("" (inst - "m!1" ) nil nil )) nil )) nil ))nil ))nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil minmax_orders nil )set type-eq-decl nil sets nil )nil defined_types nil )"bool" minmax_orders nil )"bool" minmax_orders nil )"{t: (S) | least?(t, S, <=)}" minmax_orders nil )"bool" bounded_orders nil ))nil 3315157107"" (skosimp)"" (invoke (typepred "%1" "%2" ) (! 1 l) (! 1 r))"" (expand * "least?" "lower_bound?" "subset?" "member" )"" (flatten)"" (inst?) (("" (inst? -4) (("" (assert ) nil nil )) nil ))nil ))nil ))nil ))nil ))nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )nil minmax_orders nil )set type-eq-decl nil sets nil )nil defined_types nil )"bool" minmax_orders nil )"bool" minmax_orders nil )"{t: (S) | least?(t, S, <=)}" minmax_orders nil )"pred[[T, T]]" minmax_orders nil )"(LAMBDA (S): has_least?(S, lesseqp!1))" nil )"(LAMBDA (S): has_least?(S, lesseqp!1))" nil )"bool" sets nil )"bool" sets nil )"bool" bounded_orders nil ))nil 3315157135"" (skolem-typepred)"" (rewrite "least_iff_greatest_lower_bound" )"" (prop)"1" (rewrite "least_equals_glb" )"1" (rewrite "glb_def" ) nil nil )) nil )"2" (use "least_member" ) (("2" (assert ) nil nil )) nil )"3" (rewrite "least_equals_glb" )"3" (rewrite "glb_def" ) nil nil )) nil ))nil ))nil ))nil )nil minmax_orders nil )nil minmax_orders nil )nil bounded_orders nil )"bool" bounded_orders nil )"bool" minmax_orders nil )nil defined_types nil )set type-eq-decl nil sets nil )"bool" relations nil )nil defined_types nil )nil minmax_orders nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil 3315157181"" (skolem-typepred)"" (invoke (typepred "%1" ) (! 1 l 2))"" (expand "least?" )"" (prop)"1" expand * "lower_bound?" "partial_order?" "preorder?" "transitive?" )"1" (skosimp :preds? t)"1" (inst?)"1" (inst - "t!1" "least(lesseqp!1)(S!1)" "r!1" )"1" (assert ) nil nil )) nil ))nil ))nil ))nil )"2" (expand "lower_bound?" ) (("2" (inst?) nil nil )) nil ))nil ))nil ))nil ))nil )"bool" minmax_orders nil )"{t: (S) | least?(t, S, <=)}" minmax_orders nil )"bool" bounded_orders nil )"bool" orders nil )"bool" relations nil )"bool" minmax_orders nil )set type-eq-decl nil sets nil )"bool" orders nil )nil defined_types nil )nil minmax_orders nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil 3315155075"" (judgement-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )set type-eq-decl nil sets nil )nil defined_types nil )"bool" minmax_orders nil )"bool" minmax_orders nil )"bool" minmax_orders nil )"bool" bounded_orders nil )nil minmax_orders nil )"bool" bounded_orders nil )"bool" minmax_orders nil )"bool" minmax_orders nil ))nil ))nil 3315155075 ("" (judgement-tcc) nil nil )nil booleans nil )nil booleans nil )NOT const-decl "[bool -> bool]" booleans nil )set type-eq-decl nil sets nil )nil defined_types nil )"bool" minmax_orders nil )"bool" minmax_orders nil )"bool" minmax_orders nil )"bool" bounded_orders nil )nil minmax_orders nil )"bool" bounded_orders nil )"bool" minmax_orders nil )"bool" minmax_orders nil ))nil ))nil 3315155075"" (skolem-typepred)"" expand * "lattice?" "upper_semilattice?" "lower_semilattice?" "total_order?" )"" (prop)"1" (skolem!)"1" (use "non_empty_finite_has_greatest" )"1" (rewrite "has_greatest_is_least_bounded_above" ) nil nil ))nil ))nil )"2" (skolem!)"2" (use "non_empty_finite_has_least" )"2" (rewrite "has_least_is_greatest_bounded_below" ) nil nil ))nil ))nil ))nil ))nil ))nil )"bool" bounded_orders nil )"bool" bounded_orders nil )"bool" bounded_orders nil )"bool" minmax_orders nil )nil nil )nil minmax_orders nil )"bool" minmax_orders nil )nil nil )nil finite_sets nil )"bool" sets nil )nil finite_sets nil )"bool" finite_sets nil )set type-eq-decl nil sets nil )nil minmax_orders nil )"bool" orders nil )nil defined_types nil )nil minmax_orders nil )NOT const-decl "[bool -> bool]" booleans nil )nil booleans nil )nil booleans nil ))nil )))quality 100%
¤ Dauer der Verarbeitung: 0.25 Sekunden
(vorverarbeitet)
¤ *© Formatika GbR, Deutschland
