| products/sources/formale sprachen/Coq/dev/ci/nix/ |
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei: subgraph_paths.pvs Sprache: Unknown
|
(bounded_orders
(lub_TCC1 0 (lub_TCC1-1 nil 3315148143 ("" (inst + "LAMBDA <=: LAMBDA (S: {S | least_bounded_above?(S, <=)}): epsilon(least_upper_bound?(S, <=))") (("1" (skolem-typepred) (("1" (expand "least_bounded_above?") (("1" (use "epsilon_ax[T]") (("1" (assert) nil nil) ("2" (skolem!) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil) ("2" (skolem-typepred) (("2" (expand "least_bounded_above?") (("2" (skolem!) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil) ((NOT const-decl "[bool -> bool]" booleans nil) (epsilon_ax formula-decl nil epsilons nil) (epsilon const-decl "T" epsilons nil) (least_upper_bound? const-decl "bool" bounded_orders nil) (least_bounded_above? const-decl "bool" bounded_orders nil) (set type-eq-decl nil sets nil) (pred type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil bounded_orders nil)) nil)) (unique_least_upper_bound 0 (unique_least_upper_bound-1 nil 3315148346 ("" (grind) nil 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 bounded_orders nil) (PRED type-eq-decl nil defined_types nil) (antisymmetric? const-decl "bool" relations nil) (set type-eq-decl nil sets nil) (pred type-eq-decl nil defined_types nil) (least_upper_bound? const-decl "bool" bounded_orders nil) (t!1 skolem-const-decl "(LAMBDA (t): least_upper_bound?(t, S!1, lesseqp!1))" bounded_orders nil) (S!1 skolem-const-decl "set[T]" bounded_orders nil) (lesseqp!1 skolem-const-decl "(antisymmetric?[T])" bounded_orders nil) (r!1 skolem-const-decl "(LAMBDA (t): least_upper_bound?(t, S!1, lesseqp!1))" bounded_orders nil) (upper_bound? const-decl "bool" bounded_orders nil)) shostak)) (subset_upper_bound 0 (subset_upper_bound-1 nil 3315148417 ("" (grind) nil nil) ((set type-eq-decl nil sets nil) (T formal-type-decl nil bounded_orders nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (upper_bound? const-decl "bool" bounded_orders nil)) shostak)) (subset_least_upper_bound 0 (subset_least_upper_bound-1 nil 3315148426 ("" (expand "least_upper_bound?") (("" (skosimp) (("" (forward-chain "subset_upper_bound") (("" (inst -6 "t!1") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (set type-eq-decl nil sets nil) (pred type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil bounded_orders nil) (subset_upper_bound formula-decl nil bounded_orders nil) (least_upper_bound? const-decl "bool" bounded_orders nil)) shostak)) (lub_def 0 (lub_def-1 nil 3315148454 ("" (skolem-typepred) (("" (invoke (typepred "%1") (! 1 l l)) (("" (ground) (("" (use "unique_least_upper_bound") nil nil)) nil)) nil)) nil) ((least_upper_bound? const-decl "bool" bounded_orders nil) (lub const-decl "(LAMBDA (t): least_upper_bound?(t, S, <=))" bounded_orders nil) (unique_least_upper_bound formula-decl nil bounded_orders nil) (least_bounded_above? const-decl "bool" bounded_orders nil) (pred type-eq-decl nil defined_types nil) (set type-eq-decl nil sets nil) (antisymmetric? const-decl "bool" relations nil) (PRED type-eq-decl nil defined_types nil) (T formal-type-decl nil bounded_orders nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) shostak)) (lub_eq 0 (lub_eq-1 nil 3315149292 ("" (skolem-typepred) (("" (rewrite "unique_least_upper_bound") nil nil)) nil) ((unique_least_upper_bound formula-decl nil bounded_orders nil) (lub const-decl "(LAMBDA (t): least_upper_bound?(t, S, <=))" bounded_orders nil) (least_upper_bound? const-decl "bool" bounded_orders nil) (least_bounded_above? const-decl "bool" bounded_orders nil) (pred type-eq-decl nil defined_types nil) (set type-eq-decl nil sets nil) (antisymmetric? const-decl "bool" relations nil) (PRED type-eq-decl nil defined_types nil) (T formal-type-decl nil bounded_orders nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) shostak)) (lub_ge 0 (lub_ge-1 nil 3315149314 ("" (skolem-typepred) (("" (invoke (typepred "%1") (! 1 2)) (("" (expand* "least_upper_bound?" "upper_bound?") (("" (flatten) (("" (inst?) nil nil)) nil)) nil)) nil)) nil) ((least_upper_bound? const-decl "bool" bounded_orders nil) (lub const-decl "(LAMBDA (t): least_upper_bound?(t, S, <=))" bounded_orders nil) (upper_bound? const-decl "bool" bounded_orders nil) (least_bounded_above? const-decl "bool" bounded_orders nil) (pred type-eq-decl nil defined_types nil) (set type-eq-decl nil sets nil) (T formal-type-decl nil bounded_orders nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) shostak)) (lub_le 0 (lub_le-1 nil 3315149358 ("" (skolem-typepred) (("" (invoke (typepred "%1") (! 1 l l)) (("" (expand "least_upper_bound?") (("" (prop) (("1" (hide -3) (("1" (expand* "upper_bound?" "transitive?") (("1" (skolem-typepred) (("1" (inst?) (("1" (inst - "r!1" "lub(lesseqp!1)(S!1)" "t!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((least_upper_bound? const-decl "bool" bounded_orders nil) (lub const-decl "(LAMBDA (t): least_upper_bound?(t, S, <=))" bounded_orders nil) (upper_bound? const-decl "bool" bounded_orders nil) (least_bounded_above? const-decl "bool" bounded_orders nil) (pred type-eq-decl nil defined_types nil) (set type-eq-decl nil sets nil) (transitive? const-decl "bool" relations nil) (PRED type-eq-decl nil defined_types nil) (T formal-type-decl nil bounded_orders nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) shostak)) (all_least_bounded 0 (all_least_bounded-1 nil 3315149446 ("" (skolem-typepred) (("" (expand "complete_upper_semilattice?") (("" (flatten) (("" (inst?) nil nil)) nil)) nil)) nil) ((set type-eq-decl nil sets nil) (complete_upper_semilattice? const-decl "bool" bounded_orders nil) (pred type-eq-decl nil defined_types nil) (T formal-type-decl nil bounded_orders nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) shostak)) (all_finite_least_bounded 0 (all_finite_least_bounded-1 nil 3315149492 ("" (skolem-typepred) (("" (expand "upper_semilattice?") (("" (flatten) (("" (inst?) nil nil)) nil)) nil)) nil) ((upper_semilattice? const-decl "bool" bounded_orders nil) (pred type-eq-decl nil defined_types nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (empty? const-decl "bool" sets 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-type-decl nil bounded_orders nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) shostak)) (complete_upper_semilattice_upper 0 (complete_upper_semilattice_upper-1 nil 3315148143 ("" (judgement-tcc) nil nil) ((complete_upper_semilattice? const-decl "bool" bounded_orders nil) (pred type-eq-decl nil defined_types nil) (T formal-type-decl nil bounded_orders nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (injective? const-decl "bool" functions nil) (member const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (empty? const-decl "bool" sets nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (reflexive? const-decl "bool" relations nil) (transitive? const-decl "bool" relations nil) (preorder? const-decl "bool" orders nil) (antisymmetric? const-decl "bool" relations nil) (partial_order? const-decl "bool" orders nil) (upper_bound? const-decl "bool" bounded_orders nil) (least_upper_bound? const-decl "bool" bounded_orders nil) (least_bounded_above? const-decl "bool" bounded_orders nil) (upper_semilattice? const-decl "bool" bounded_orders nil)) nil)) (upper_semilattice_is_partial_order 0 (upper_semilattice_is_partial_order-1 nil 3315148143 ("" (judgement-tcc) nil 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 bounded_orders nil) (pred type-eq-decl nil defined_types nil) (upper_semilattice? const-decl "bool" bounded_orders nil) (least_bounded_above? const-decl "bool" bounded_orders nil) (least_upper_bound? const-decl "bool" bounded_orders nil) (upper_bound? const-decl "bool" bounded_orders nil) (reflexive? const-decl "bool" relations nil) (transitive? const-decl "bool" relations nil) (preorder? const-decl "bool" orders nil) (antisymmetric? const-decl "bool" relations nil) (partial_order? const-decl "bool" orders nil)) nil)) (glb_TCC1 0 (glb_TCC1-1 nil 3315148143 ("" (inst + "LAMBDA <=: LAMBDA (S: {S | greatest_bounded_below?(S, <=)}): epsilon(greatest_lower_bound?(S, <=))") (("1" (skolem-typepred) (("1" (expand "greatest_bounded_below?") (("1" (use "epsilon_ax[T]") (("1" (assert) nil nil) ("2" (skolem!) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil) ("2" (skolem-typepred) (("2" (expand "greatest_bounded_below?") (("2" (skolem!) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil) ((NOT const-decl "[bool -> bool]" booleans nil) (epsilon_ax formula-decl nil epsilons nil) (epsilon const-decl "T" epsilons nil) (greatest_lower_bound? const-decl "bool" bounded_orders nil) (greatest_bounded_below? const-decl "bool" bounded_orders nil) (set type-eq-decl nil sets nil) (pred type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil bounded_orders nil)) nil)) (unique_greatest_lower_bound 0 (unique_greatest_lower_bound-1 nil 3315149599 ("" (grind) nil 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 bounded_orders nil) (PRED type-eq-decl nil defined_types nil) (antisymmetric? const-decl "bool" relations nil) (set type-eq-decl nil sets nil) (pred type-eq-decl nil defined_types nil) (greatest_lower_bound? const-decl "bool" bounded_orders nil) (S!1 skolem-const-decl "set[T]" bounded_orders nil) (lesseqp!1 skolem-const-decl "(antisymmetric?[T])" bounded_orders nil) (r!1 skolem-const-decl "(LAMBDA (t): greatest_lower_bound?(t, S!1, lesseqp!1))" bounded_orders nil) (t!1 skolem-const-decl "(LAMBDA (t): greatest_lower_bound?(t, S!1, lesseqp!1))" bounded_orders nil) (lower_bound? const-decl "bool" bounded_orders nil)) shostak)) (subset_lower_bound 0 (subset_lower_bound-1 nil 3315149629 ("" (grind) nil nil) ((set type-eq-decl nil sets nil) (T formal-type-decl nil bounded_orders nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (member const-decl "bool" sets nil) (subset? const-decl "bool" sets nil) (lower_bound? const-decl "bool" bounded_orders nil)) shostak)) (subset_greatest_lower_bound 0 (subset_greatest_lower_bound-1 nil 3315149639 ("" (expand "greatest_lower_bound?") (("" (skosimp) (("" (forward-chain "subset_lower_bound") (("" (inst - "r!1") (("" (assert) nil nil)) nil)) nil)) nil)) nil) ((subset_is_partial_order name-judgement "(partial_order?[set[T]])" sets_lemmas nil) (set type-eq-decl nil sets nil) (pred type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil bounded_orders nil) (subset_lower_bound formula-decl nil bounded_orders nil) (greatest_lower_bound? const-decl "bool" bounded_orders nil)) shostak)) (glb_def 0 (glb_def-1 nil 3315149667 ("" (skolem-typepred) (("" (invoke (typepred "%1") (! 1 l l)) (("" (ground) (("" (use "unique_greatest_lower_bound") nil nil)) nil)) nil)) nil) ((greatest_lower_bound? const-decl "bool" bounded_orders nil) (glb const-decl "(LAMBDA (t): greatest_lower_bound?(t, S, <=))" bounded_orders nil) (unique_greatest_lower_bound formula-decl nil bounded_orders nil) (greatest_bounded_below? const-decl "bool" bounded_orders nil) (pred type-eq-decl nil defined_types nil) (set type-eq-decl nil sets nil) (antisymmetric? const-decl "bool" relations nil) (PRED type-eq-decl nil defined_types nil) (T formal-type-decl nil bounded_orders nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) shostak)) (glb_eq 0 (glb_eq-1 nil 3315149690 ("" (skolem-typepred) (("" (rewrite "unique_greatest_lower_bound") nil nil)) nil) ((unique_greatest_lower_bound formula-decl nil bounded_orders nil) (glb const-decl "(LAMBDA (t): greatest_lower_bound?(t, S, <=))" bounded_orders nil) (greatest_lower_bound? const-decl "bool" bounded_orders nil) (greatest_bounded_below? const-decl "bool" bounded_orders nil) (pred type-eq-decl nil defined_types nil) (set type-eq-decl nil sets nil) (antisymmetric? const-decl "bool" relations nil) (PRED type-eq-decl nil defined_types nil) (T formal-type-decl nil bounded_orders nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) shostak)) (glb_le 0 (glb_le-1 nil 3315149711 ("" (skolem-typepred) (("" (invoke (typepred "%1") (! 1 l)) (("" (expand* "greatest_lower_bound?" "lower_bound?") (("" (flatten) (("" (inst?) nil nil)) nil)) nil)) nil)) nil) ((greatest_lower_bound? const-decl "bool" bounded_orders nil) (glb const-decl "(LAMBDA (t): greatest_lower_bound?(t, S, <=))" bounded_orders nil) (lower_bound? const-decl "bool" bounded_orders nil) (greatest_bounded_below? const-decl "bool" bounded_orders nil) (pred type-eq-decl nil defined_types nil) (set type-eq-decl nil sets nil) (T formal-type-decl nil bounded_orders nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) shostak)) (glb_ge 0 (glb_ge-1 nil 3315149729 ("" (skolem-typepred) (("" (invoke (typepred "%1") (! 1 l r)) (("" (expand "greatest_lower_bound?") (("" (prop) (("1" (hide -3) (("1" (expand* "lower_bound?" "transitive?") (("1" (skolem-typepred) (("1" (inst?) (("1" (inst - "t!1" "glb(lesseqp!1)(S!1)" "r!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ((greatest_lower_bound? const-decl "bool" bounded_orders nil) (glb const-decl "(LAMBDA (t): greatest_lower_bound?(t, S, <=))" bounded_orders nil) (lower_bound? const-decl "bool" bounded_orders nil) (greatest_bounded_below? const-decl "bool" bounded_orders nil) (pred type-eq-decl nil defined_types nil) (set type-eq-decl nil sets nil) (transitive? const-decl "bool" relations nil) (PRED type-eq-decl nil defined_types nil) (T formal-type-decl nil bounded_orders nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) shostak)) (all_greatest_bounded 0 (all_greatest_bounded-1 nil 3315149785 ("" (skolem-typepred) (("" (expand "complete_lower_semilattice?") (("" (flatten) (("" (inst?) nil nil)) nil)) nil)) nil) ((set type-eq-decl nil sets nil) (complete_lower_semilattice? const-decl "bool" bounded_orders nil) (pred type-eq-decl nil defined_types nil) (T formal-type-decl nil bounded_orders nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) shostak)) (all_finite_greatest_bounded 0 (all_finite_greatest_bounded-1 nil 3315149803 ("" (skolem-typepred) (("" (expand "lower_semilattice?") (("" (flatten) (("" (inst?) nil nil)) nil)) nil)) nil) ((lower_semilattice? const-decl "bool" bounded_orders nil) (pred type-eq-decl nil defined_types nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (empty? const-decl "bool" sets 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-type-decl nil bounded_orders nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) shostak)) (complete_lower_semilattice_lower 0 (complete_lower_semilattice_lower-1 nil 3315148143 ("" (judgement-tcc) nil nil) ((complete_lower_semilattice? const-decl "bool" bounded_orders nil) (pred type-eq-decl nil defined_types nil) (T formal-type-decl nil bounded_orders nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (injective? const-decl "bool" functions nil) (member const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (empty? const-decl "bool" sets nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (reflexive? const-decl "bool" relations nil) (transitive? const-decl "bool" relations nil) (preorder? const-decl "bool" orders nil) (antisymmetric? const-decl "bool" relations nil) (partial_order? const-decl "bool" orders nil) (lower_bound? const-decl "bool" bounded_orders nil) (greatest_lower_bound? const-decl "bool" bounded_orders nil) (greatest_bounded_below? const-decl "bool" bounded_orders nil) (lower_semilattice? const-decl "bool" bounded_orders nil)) nil)) (lower_semilattice_is_partial_order 0 (lower_semilattice_is_partial_order-1 nil 3315148143 ("" (judgement-tcc) nil 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 bounded_orders nil) (pred type-eq-decl nil defined_types nil) (lower_semilattice? const-decl "bool" bounded_orders nil) (greatest_bounded_below? const-decl "bool" bounded_orders nil) (greatest_lower_bound? const-decl "bool" bounded_orders nil) (lower_bound? const-decl "bool" bounded_orders nil) (reflexive? const-decl "bool" relations nil) (transitive? const-decl "bool" relations nil) (preorder? const-decl "bool" orders nil) (antisymmetric? const-decl "bool" relations nil) (partial_order? const-decl "bool" orders nil)) nil)) (bounded_is_bounded_above 0 (bounded_is_bounded_above-1 nil 3315148143 ("" (judgement-tcc) nil 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 bounded_orders nil) (set type-eq-decl nil sets nil) (pred type-eq-decl nil defined_types nil) (bounded? const-decl "bool" bounded_orders nil) (bounded_below? const-decl "bool" bounded_orders nil) (lower_bound? const-decl "bool" bounded_orders nil) (upper_bound? const-decl "bool" bounded_orders nil) (bounded_above? const-decl "bool" bounded_orders nil)) nil)) (bounded_is_bounded_below 0 (bounded_is_bounded_below-1 nil 3315148143 ("" (judgement-tcc) nil 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 bounded_orders nil) (set type-eq-decl nil sets nil) (pred type-eq-decl nil defined_types nil) (bounded? const-decl "bool" bounded_orders nil) (bounded_above? const-decl "bool" bounded_orders nil) (upper_bound? const-decl "bool" bounded_orders nil) (lower_bound? const-decl "bool" bounded_orders nil) (bounded_below? const-decl "bool" bounded_orders nil)) nil)) (tightly_bounded_above 0 (tightly_bounded_above-1 nil 3315148143 ("" (judgement-tcc) nil 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 bounded_orders nil) (set type-eq-decl nil sets nil) (pred type-eq-decl nil defined_types nil) (tightly_bounded? const-decl "bool" bounded_orders nil) (greatest_bounded_below? const-decl "bool" bounded_orders nil) (greatest_lower_bound? const-decl "bool" bounded_orders nil) (lower_bound? const-decl "bool" bounded_orders nil) (upper_bound? const-decl "bool" bounded_orders nil) (least_upper_bound? const-decl "bool" bounded_orders nil) (least_bounded_above? const-decl "bool" bounded_orders nil)) nil)) (tightly_bounded_below 0 (tightly_bounded_below-1 nil 3315148143 ("" (judgement-tcc) nil 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 bounded_orders nil) (set type-eq-decl nil sets nil) (pred type-eq-decl nil defined_types nil) (tightly_bounded? const-decl "bool" bounded_orders nil) (least_bounded_above? const-decl "bool" bounded_orders nil) (least_upper_bound? const-decl "bool" bounded_orders nil) (upper_bound? const-decl "bool" bounded_orders nil) (lower_bound? const-decl "bool" bounded_orders nil) (greatest_lower_bound? const-decl "bool" bounded_orders nil) (greatest_bounded_below? const-decl "bool" bounded_orders nil)) nil)) (complete_lattice_upper 0 (complete_lattice_upper-1 nil 3315148143 ("" (judgement-tcc) nil nil) ((complete_lattice? const-decl "bool" bounded_orders nil) (pred type-eq-decl nil defined_types nil) (T formal-type-decl nil bounded_orders nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (complete_lower_semilattice? const-decl "bool" bounded_orders nil) (greatest_bounded_below? const-decl "bool" bounded_orders nil) (greatest_lower_bound? const-decl "bool" bounded_orders nil) (lower_bound? const-decl "bool" bounded_orders nil) (reflexive? const-decl "bool" relations nil) (transitive? const-decl "bool" relations nil) (preorder? const-decl "bool" orders nil) (antisymmetric? const-decl "bool" relations nil) (partial_order? const-decl "bool" orders nil) (upper_bound? const-decl "bool" bounded_orders nil) (least_upper_bound? const-decl "bool" bounded_orders nil) (least_bounded_above? const-decl "bool" bounded_orders nil) (complete_upper_semilattice? const-decl "bool" bounded_orders nil)) nil)) (complete_lattice_lower 0 (complete_lattice_lower-1 nil 3315148143 ("" (judgement-tcc) nil nil) ((complete_lattice? const-decl "bool" bounded_orders nil) (pred type-eq-decl nil defined_types nil) (T formal-type-decl nil bounded_orders nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (complete_upper_semilattice? const-decl "bool" bounded_orders nil) (least_bounded_above? const-decl "bool" bounded_orders nil) (least_upper_bound? const-decl "bool" bounded_orders nil) (upper_bound? const-decl "bool" bounded_orders nil) (reflexive? const-decl "bool" relations nil) (transitive? const-decl "bool" relations nil) (preorder? const-decl "bool" orders nil) (antisymmetric? const-decl "bool" relations nil) (partial_order? const-decl "bool" orders nil) (lower_bound? const-decl "bool" bounded_orders nil) (greatest_lower_bound? const-decl "bool" bounded_orders nil) (greatest_bounded_below? const-decl "bool" bounded_orders nil) (complete_lower_semilattice? const-decl "bool" bounded_orders nil)) nil)) (lattice_upper 0 (lattice_upper-1 nil 3315148143 ("" (judgement-tcc) nil nil) ((lattice? const-decl "bool" bounded_orders nil) (pred type-eq-decl nil defined_types nil) (T formal-type-decl nil bounded_orders nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (lower_semilattice? const-decl "bool" bounded_orders nil) (greatest_bounded_below? const-decl "bool" bounded_orders nil) (greatest_lower_bound? const-decl "bool" bounded_orders nil) (lower_bound? const-decl "bool" bounded_orders nil) (reflexive? const-decl "bool" relations nil) (transitive? const-decl "bool" relations nil) (preorder? const-decl "bool" orders nil) (antisymmetric? const-decl "bool" relations nil) (partial_order? const-decl "bool" orders nil) (upper_bound? const-decl "bool" bounded_orders nil) (least_upper_bound? const-decl "bool" bounded_orders nil) (least_bounded_above? const-decl "bool" bounded_orders nil) (upper_semilattice? const-decl "bool" bounded_orders nil)) nil)) (lattice_lower 0 (lattice_lower-1 nil 3315148143 ("" (judgement-tcc) nil nil) ((lattice? const-decl "bool" bounded_orders nil) (pred type-eq-decl nil defined_types nil) (T formal-type-decl nil bounded_orders nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (upper_semilattice? const-decl "bool" bounded_orders nil) (least_bounded_above? const-decl "bool" bounded_orders nil) (least_upper_bound? const-decl "bool" bounded_orders nil) (upper_bound? const-decl "bool" bounded_orders nil) (reflexive? const-decl "bool" relations nil) (transitive? const-decl "bool" relations nil) (preorder? const-decl "bool" orders nil) (antisymmetric? const-decl "bool" relations nil) (partial_order? const-decl "bool" orders nil) (lower_bound? const-decl "bool" bounded_orders nil) (greatest_lower_bound? const-decl "bool" bounded_orders nil) (greatest_bounded_below? const-decl "bool" bounded_orders nil) (lower_semilattice? const-decl "bool" bounded_orders nil)) nil)) (complete_lattice_is_lattice 0 (complete_lattice_is_lattice-1 nil 3315148143 ("" (judgement-tcc) nil nil) ((complete_lattice? const-decl "bool" bounded_orders nil) (pred type-eq-decl nil defined_types nil) (T formal-type-decl nil bounded_orders nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (injective? const-decl "bool" functions nil) (member const-decl "bool" sets nil) (nat nonempty-type-eq-decl nil naturalnumbers 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) (>= const-decl "bool" reals 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) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (set type-eq-decl nil sets nil) (is_finite const-decl "bool" finite_sets nil) (finite_set type-eq-decl nil finite_sets nil) (empty? const-decl "bool" sets nil) (non_empty_finite_set type-eq-decl nil finite_sets nil) (complete_lower_semilattice? const-decl "bool" bounded_orders nil) (complete_upper_semilattice? const-decl "bool" bounded_orders nil) (reflexive? const-decl "bool" relations nil) (transitive? const-decl "bool" relations nil) (preorder? const-decl "bool" orders nil) (antisymmetric? const-decl "bool" relations nil) (partial_order? const-decl "bool" orders nil) (upper_bound? const-decl "bool" bounded_orders nil) (least_upper_bound? const-decl "bool" bounded_orders nil) (least_bounded_above? const-decl "bool" bounded_orders nil) (upper_semilattice? const-decl "bool" bounded_orders nil) (lower_bound? const-decl "bool" bounded_orders nil) (greatest_lower_bound? const-decl "bool" bounded_orders nil) (greatest_bounded_below? const-decl "bool" bounded_orders nil) (lower_semilattice? const-decl "bool" bounded_orders nil) (lattice? const-decl "bool" bounded_orders nil)) nil)) (upper_bound_singleton 0 (upper_bound_singleton-1 nil 3315149840 ("" (skolem!) (("" (expand* "singleton" "upper_bound?") (("" (prop) (("1" (inst - "u!1") nil nil) ("2" (skolem-typepred) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ((upper_bound? const-decl "bool" bounded_orders nil) (singleton const-decl "(singleton?)" sets nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (T formal-type-decl nil bounded_orders nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil)) shostak)) (least_upper_bound_singleton 0 (least_upper_bound_singleton-1 nil 3318182228 ("" (grind) nil 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 bounded_orders nil) (PRED type-eq-decl nil defined_types nil) (reflexive? const-decl "bool" relations nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set[T]" bounded_orders nil) (singleton? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (upper_bound? const-decl "bool" bounded_orders nil) (least_upper_bound? const-decl "bool" bounded_orders nil) (singleton const-decl "(singleton?)" sets nil)) shostak)) (lub_singleton_TCC1 0 (lub_singleton_TCC1-1 nil 3318180939 ("" (grind :if-match nil) (("" (inst + "u!1") (("" (grind :if-match nil) (("1" (inst -4 "u!1") nil nil) ("2" (inst - "u!1") nil nil)) nil)) nil)) nil) ((nonempty_singleton_finite application-judgement "non_empty_finite_set[T]" bounded_orders nil) (singleton const-decl "(singleton?)" sets nil) (singleton? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (reflexive? const-decl "bool" relations nil) (transitive? const-decl "bool" relations nil) (preorder? const-decl "bool" orders nil) (antisymmetric? const-decl "bool" relations 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 bounded_orders nil) (pred type-eq-decl nil defined_types nil) (partial_order? const-decl "bool" orders nil) (least_bounded_above? const-decl "bool" bounded_orders nil) (least_upper_bound? const-decl "bool" bounded_orders nil) (upper_bound? const-decl "bool" bounded_orders nil)) nil)) (lub_singleton 0 (lub_singleton-1 nil 3318181433 ("" (skolem-typepred) (("" (rewrite "lub_def") (("" (grind :if-match nil) (("1" (inst -4 "u!1") nil nil) ("2" (inst - "u!1") nil nil)) nil)) nil)) nil) ((nonempty_singleton_finite application-judgement "non_empty_finite_set[T]" bounded_orders nil) (lub_def formula-decl nil bounded_orders nil) (PRED type-eq-decl nil defined_types nil) (antisymmetric? const-decl "bool" relations nil) (set type-eq-decl nil sets nil) (least_bounded_above? const-decl "bool" bounded_orders nil) (singleton? const-decl "bool" sets nil) (singleton const-decl "(singleton?)" sets nil) (reflexive? const-decl "bool" relations nil) (transitive? const-decl "bool" relations nil) (preorder? const-decl "bool" orders nil) (upper_bound? const-decl "bool" bounded_orders nil) (least_upper_bound? const-decl "bool" bounded_orders nil) (partial_order? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (T formal-type-decl nil bounded_orders nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) shostak)) (lower_bound_singleton 0 (lower_bound_singleton-1 nil 3315149913 ("" (skolem!) (("" (expand* "singleton" "lower_bound?") (("" (prop) (("1" (inst - "u!1") nil nil) ("2" (skolem-typepred) (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ((lower_bound? const-decl "bool" bounded_orders nil) (singleton const-decl "(singleton?)" sets nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (T formal-type-decl nil bounded_orders nil) (boolean nonempty-type-decl nil booleans nil) (= const-decl "[T, T -> boolean]" equalities nil)) shostak)) (greatest_lower_bound_singleton 0 (greatest_lower_bound_singleton-1 nil 3318182233 ("" (grind) nil 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 bounded_orders nil) (PRED type-eq-decl nil defined_types nil) (reflexive? const-decl "bool" relations nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set[T]" bounded_orders nil) (singleton? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (lower_bound? const-decl "bool" bounded_orders nil) (greatest_lower_bound? const-decl "bool" bounded_orders nil) (singleton const-decl "(singleton?)" sets nil)) shostak)) (glb_singleton_TCC1 0 (glb_singleton_TCC1-1 nil 3318180939 ("" (grind :if-match nil) (("" (inst + "u!1") (("" (grind :if-match nil) (("1" (inst -4 "u!1") nil nil) ("2" (inst - "u!1") nil nil)) nil)) nil)) nil) ((nonempty_singleton_finite application-judgement "non_empty_finite_set[T]" bounded_orders nil) (singleton const-decl "(singleton?)" sets nil) (singleton? const-decl "bool" sets nil) (set type-eq-decl nil sets nil) (reflexive? const-decl "bool" relations nil) (transitive? const-decl "bool" relations nil) (preorder? const-decl "bool" orders nil) (antisymmetric? const-decl "bool" relations 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 bounded_orders nil) (pred type-eq-decl nil defined_types nil) (partial_order? const-decl "bool" orders nil) (greatest_bounded_below? const-decl "bool" bounded_orders nil) (greatest_lower_bound? const-decl "bool" bounded_orders nil) (lower_bound? const-decl "bool" bounded_orders nil)) nil)) (glb_singleton 0 (glb_singleton-1 nil 3318181973 ("" (skolem-typepred) (("" (rewrite "glb_def") (("" (grind :if-match nil) (("1" (inst -4 "u!1") nil nil) ("2" (inst - "u!1") nil nil)) nil)) nil)) nil) ((nonempty_singleton_finite application-judgement "non_empty_finite_set[T]" bounded_orders nil) (glb_def formula-decl nil bounded_orders nil) (PRED type-eq-decl nil defined_types nil) (antisymmetric? const-decl "bool" relations nil) (set type-eq-decl nil sets nil) (greatest_bounded_below? const-decl "bool" bounded_orders nil) (singleton? const-decl "bool" sets nil) (singleton const-decl "(singleton?)" sets nil) (reflexive? const-decl "bool" relations nil) (transitive? const-decl "bool" relations nil) (preorder? const-decl "bool" orders nil) (lower_bound? const-decl "bool" bounded_orders nil) (greatest_lower_bound? const-decl "bool" bounded_orders nil) (partial_order? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (T formal-type-decl nil bounded_orders nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) shostak)) (upper_bound_emptyset 0 (upper_bound_emptyset-1 nil 3315149941 ("" (expand* "emptyset" "upper_bound?") (("" (skosimp* t) nil nil)) nil) ((emptyset const-decl "set" sets nil) (upper_bound? const-decl "bool" bounded_orders nil)) shostak)) (lower_bound_emptyset 0 (lower_bound_emptyset-1 nil 3315149963 ("" (expand* "emptyset" "lower_bound?") (("" (skosimp* t) nil nil)) nil) ((emptyset const-decl "set" sets nil) (lower_bound? const-decl "bool" bounded_orders nil)) shostak)) (lub_emptyset_is_glb_fullset 0 (lub_emptyset_is_glb_fullset-1 nil 3315149983 ("" (skolem!) (("" (expand* "emptyset" "fullset" "least_upper_bound?" "greatest_lower_bound?") (("" (prop) (("1" (hide -1) (("1" (expand* "lower_bound?" "upper_bound?") (("1" (skolem!) (("1" (inst?) (("1" (assert) (("1" (skolem-typepred) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -2 -1) (("2" (skosimp) (("2" (expand "lower_bound?") (("2" (inst?) nil nil)) nil)) nil)) nil) ("3" (hide -2 -1) (("3" (expand "upper_bound?") (("3" (skolem-typepred) nil nil)) nil)) nil) ("4" (skosimp) (("4" (hide -3 -1) (("4" (expand "lower_bound?") (("4" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((fullset const-decl "set" sets nil) (greatest_lower_bound? const-decl "bool" bounded_orders nil) (least_upper_bound? const-decl "bool" bounded_orders nil) (emptyset const-decl "set" sets nil) (T formal-type-decl nil bounded_orders nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (TRUE const-decl "bool" booleans nil) (lower_bound? const-decl "bool" bounded_orders nil) (upper_bound? const-decl "bool" bounded_orders nil)) shostak)) (glb_emptyset_is_lub_fullset 0 (glb_emptyset_is_lub_fullset-1 nil 3315150108 ("" (skolem!) (("" (expand* "emptyset" "fullset" "least_upper_bound?" "greatest_lower_bound?") (("" (prop) (("1" (hide -1) (("1" (expand* "lower_bound?" "upper_bound?") (("1" (skolem!) (("1" (inst?) (("1" (assert) (("1" (skolem-typepred) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (hide -2 -1) (("2" (skosimp) (("2" (expand "upper_bound?") (("2" (inst?) nil nil)) nil)) nil)) nil) ("3" (hide -2 -1) (("3" (expand "lower_bound?") (("3" (skolem-typepred) nil nil)) nil)) nil) ("4" (skosimp) (("4" (hide -3 -1) (("4" (expand "upper_bound?") (("4" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((fullset const-decl "set" sets nil) (greatest_lower_bound? const-decl "bool" bounded_orders nil) (least_upper_bound? const-decl "bool" bounded_orders nil) (emptyset const-decl "set" sets nil) (T formal-type-decl nil bounded_orders nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (TRUE const-decl "bool" booleans nil) (lower_bound? const-decl "bool" bounded_orders nil) (upper_bound? const-decl "bool" bounded_orders nil)) shostak)) (least_bounded_above_emptyset 0 (least_bounded_above_emptyset-1 nil 3315150181 ("" (skolem!) (("" (lemma "lub_emptyset_is_glb_fullset") (("" (expand* "least_bounded_above?" "greatest_bounded_below?") (("" (prop) (("1" (skolem!) (("1" (inst?) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (skolem!) (("2" (inst?) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((lub_emptyset_is_glb_fullset formula-decl nil bounded_orders nil) (T formal-type-decl nil bounded_orders nil) (finite_emptyset name-judgement "finite_set[T]" bounded_orders nil) (finite_emptyset name-judgement "finite_set" finite_sets nil) (pred type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (least_bounded_above? const-decl "bool" bounded_orders nil) (greatest_bounded_below? const-decl "bool" bounded_orders nil)) shostak)) (greatest_bounded_below_emptyset 0 (greatest_bounded_below_emptyset-1 nil 3315150225 ("" (skolem!) (("" (lemma "glb_emptyset_is_lub_fullset") (("" (expand* "least_bounded_above?" "greatest_bounded_below?") (("" (prop) (("1" (skolem!) (("1" (inst?) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil)) nil) ("2" (skolem!) (("2" (inst?) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((glb_emptyset_is_lub_fullset formula-decl nil bounded_orders nil) (T formal-type-decl nil bounded_orders nil) (finite_emptyset name-judgement "finite_set[T]" bounded_orders nil) (finite_emptyset name-judgement "finite_set" finite_sets nil) (pred type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (least_bounded_above? const-decl "bool" bounded_orders nil) (greatest_bounded_below? const-decl "bool" bounded_orders nil)) shostak)) (le_lub 0 (le_lub-1 nil 3406646721 ("" (skosimp) (("" (lemma "lub_le" ("<=" "lesseqp!1" "S" "S!1" "t" "lub(lesseqp!1)(R!1)")) (("" (replace -1 1) (("" (hide -1) (("" (expand "upper_bound?") (("" (skosimp) (("" (typepred "r!1") (("" (inst - "r!1") (("" (skosimp) (("" (typepred "r!2") (("" (typepred "lub(lesseqp!1)(R!1)") (("" (expand "least_upper_bound?") (("" (flatten) (("" (hide -2) (("" (expand "upper_bound?") (("" (inst - "r!2") (("" (typepred "lesseqp!1") (("" (expand "partial_order?") (("" (expand "preorder?") (("" (flatten) (("" (expand "transitive?") (("" (inst - "r!1" "r!2" "lub(lesseqp!1)(R!1)") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((transitive? const-decl "bool" relations nil) (PRED type-eq-decl nil defined_types nil) (partial_order? const-decl "bool" orders nil) (lub const-decl "(LAMBDA (t): least_upper_bound?(t, S, <=))" bounded_orders nil) (least_upper_bound? const-decl "bool" bounded_orders nil) (least_bounded_above? const-decl "bool" bounded_orders nil) (set type-eq-decl nil sets nil) (pred type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil bounded_orders nil) (lub_le formula-decl nil bounded_orders nil) (preorder? const-decl "bool" orders nil) (NOT const-decl "[bool -> bool]" booleans nil) (upper_bound? const-decl "bool" bounded_orders nil)) nil)) (eq_lub 0 (eq_lub-1 nil 3406646745 ("" (skosimp*) (("" (lemma "le_lub" ("<=" "lesseqp!1" "S" "S!1" "R" "R!1")) (("" (lemma "le_lub" ("<=" "lesseqp!1" "S" "R!1" "R" "S!1")) (("" (replace -3) (("" (replace -4) (("" (typepred "lesseqp!1") (("" (expand "partial_order?") (("" (flatten) (("" (expand "antisymmetric?") (("" (inst - " lub(lesseqp!1)(S!1)" "lub(lesseqp!1)(R!1)") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((least_bounded_above? const-decl "bool" bounded_orders nil) (set type-eq-decl nil sets nil) (partial_order? 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) (T formal-type-decl nil bounded_orders nil) (le_lub formula-decl nil bounded_orders nil) (NOT const-decl "[bool -> bool]" booleans nil) (lub const-decl "(LAMBDA (t): least_upper_bound?(t, S, <=))" bounded_orders nil) (least_upper_bound? const-decl "bool" bounded_orders nil) (antisymmetric? const-decl "bool" relations nil)) nil)) (lub_add_TCC1 0 (lub_add_TCC1-1 nil 3406646661 ("" (skosimp) (("" (typepred "S!1") (("" (expand "least_bounded_above?") (("" (skosimp) (("" (lemma "lub_def" ("<=" "lesseqp!1" "S" "S!1" "t" "t!1")) (("" (assert) (("" (replace -1) (("" (inst + "t!1") (("" (expand "least_upper_bound?") (("" (flatten) (("" (split 1) (("1" (expand "upper_bound?") (("1" (skosimp) (("1" (typepred "r!1") (("1" (expand "add") (("1" (split -1) (("1" (typepred "lesseqp!1") (("1" (expand "partial_order?") (("1" (expand "preorder?") (("1" (flatten) (("1" (expand "reflexive?") (("1" (inst - "t!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "member") (("2" (inst - "r!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (expand "upper_bound?") (("2" (inst - "t!1") (("2" (expand "add") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((partial_order? const-decl "bool" orders nil) (least_bounded_above? const-decl "bool" bounded_orders nil) (pred type-eq-decl nil defined_types nil) (set type-eq-decl nil sets nil) (T formal-type-decl nil bounded_orders nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (upper_bound? const-decl "bool" bounded_orders nil) (nonempty? const-decl "bool" sets nil) (add const-decl "(nonempty?)" sets nil) (reflexive? const-decl "bool" relations nil) (preorder? const-decl "bool" orders nil) (lesseqp!1 skolem-const-decl "(partial_order?[T])" bounded_orders nil) (S!1 skolem-const-decl "(LAMBDA (S): least_bounded_above?(S, lesseqp!1))" bounded_orders nil) (t!1 skolem-const-decl "T" bounded_orders nil) (r!1 skolem-const-decl "(add[T](t!1, S!1))" bounded_orders nil) (member const-decl "bool" sets nil) (least_upper_bound? const-decl "bool" bounded_orders nil) (lub_def formula-decl nil bounded_orders nil) (PRED type-eq-decl nil defined_types nil) (antisymmetric? const-decl "bool" relations nil)) nil)) (lub_add 0 (lub_add-1 nil 3406646847 ("" (skosimp) (("" (lemma "lub_eq" ("<=" "lesseqp!1" "S" "add(lub(lesseqp!1)(S!1), S!1)" "t" "lub(lesseqp!1)(S!1)")) (("1" (propax) nil nil) ("2" (hide 2) (("2" (expand "least_upper_bound?") (("2" (split) (("1" (expand "upper_bound?") (("1" (skosimp) (("1" (typepred "r!1") (("1" (expand "add") (("1" (expand "member") (("1" (split) (("1" (typepred "lesseqp!1") (("1" (expand "partial_order?") (("1" (expand "preorder?") (("1" (flatten) (("1" (expand "reflexive?") (("1" (inst - "r!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (typepred "S!1") (("2" (expand "least_bounded_above?") (("2" (skosimp) (("2" (lemma "lub_def" ("<=" "lesseqp!1" "S" "S!1" "t" "t!1")) (("2" (assert) (("2" (replace -1) (("2" (expand "least_upper_bound?") (("2" (flatten) (("2" (expand "upper_bound?") (("2" (inst - "r!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp*) (("2" (expand "upper_bound?") (("2" (inst - "lub(lesseqp!1)(S!1)") (("2" (expand "add") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((lub const-decl "(LAMBDA (t): least_upper_bound?(t, S, <=))" bounded_orders nil) (least_upper_bound? const-decl "bool" bounded_orders nil) (add const-decl "(nonempty?)" sets nil) (nonempty? const-decl "bool" sets nil) (least_bounded_above? const-decl "bool" bounded_orders nil) (set type-eq-decl nil sets nil) (partial_order? const-decl "bool" orders nil) (pred type-eq-decl nil defined_types nil) (antisymmetric? const-decl "bool" relations nil) (PRED type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil bounded_orders nil) (lub_eq formula-decl nil bounded_orders nil) (lesseqp!1 skolem-const-decl "(partial_order?)" bounded_orders nil) (S!1 skolem-const-decl "(LAMBDA (S): least_bounded_above?(S, lesseqp!1))" bounded_orders nil) (upper_bound? const-decl "bool" bounded_orders nil) (NOT const-decl "[bool -> bool]" booleans nil) (member const-decl "bool" sets nil) (lub_def formula-decl nil bounded_orders nil) (preorder? const-decl "bool" orders nil) (reflexive? const-decl "bool" relations nil)) nil)) (le_glb 0 (le_glb-1 nil 3406646869 ("" (skosimp*) (("" (lemma "glb_ge" ("<=" "lesseqp!1" "S" "R!1" "t" "glb(lesseqp!1)(S!1)")) (("" (replace -1 1) (("" (hide -1) (("" (expand "lower_bound?") (("" (skosimp) (("" (typepred "r!1") (("" (typepred "glb(lesseqp!1)(S!1)") (("" (expand "greatest_lower_bound?") (("" (flatten) (("" (hide -2) (("" (inst - "r!1") (("" (skosimp) (("" (expand "lower_bound?") (("" (inst - "s!1") (("" (typepred "lesseqp!1") (("" (expand "partial_order?") (("" (expand "preorder?") (("" (flatten) (("" (expand "transitive?") (("" (inst - "glb(lesseqp!1)(S!1)" "s!1" "r!1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((transitive? const-decl "bool" relations nil) (PRED type-eq-decl nil defined_types nil) (partial_order? const-decl "bool" orders nil) (glb const-decl "(LAMBDA (t): greatest_lower_bound?(t, S, <=))" bounded_orders nil) (greatest_lower_bound? const-decl "bool" bounded_orders nil) (greatest_bounded_below? const-decl "bool" bounded_orders nil) (set type-eq-decl nil sets nil) (pred type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil bounded_orders nil) (glb_ge formula-decl nil bounded_orders nil) (preorder? const-decl "bool" orders nil) (NOT const-decl "[bool -> bool]" booleans nil) (lower_bound? const-decl "bool" bounded_orders nil)) nil)) (eq_glb 0 (eq_glb-1 nil 3406646887 ("" (skosimp) (("" (lemma "le_glb" ("<=" "lesseqp!1" "S" "S!1" "R" "R!1")) (("" (lemma "le_glb" ("<=" "lesseqp!1" "S" "R!1" "R" "S!1")) (("" (replace -3) (("" (replace -4) (("" (typepred "lesseqp!1") (("" (expand "partial_order?") (("" (flatten) (("" (expand "antisymmetric?") (("" (inst - "glb(lesseqp!1)(S!1)" "glb(lesseqp!1)(R!1)") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((greatest_bounded_below? const-decl "bool" bounded_orders nil) (set type-eq-decl nil sets nil) (partial_order? 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) (T formal-type-decl nil bounded_orders nil) (le_glb formula-decl nil bounded_orders nil) (NOT const-decl "[bool -> bool]" booleans nil) (glb const-decl "(LAMBDA (t): greatest_lower_bound?(t, S, <=))" bounded_orders nil) (greatest_lower_bound? const-decl "bool" bounded_orders nil) (antisymmetric? const-decl "bool" relations nil)) nil)) (glb_add_TCC1 0 (glb_add_TCC1-1 nil 3406646687 ("" (skosimp) (("" (typepred "S!1") (("" (expand "greatest_bounded_below?") (("" (skosimp) (("" (inst + "t!1") (("" (lemma "glb_def" ("<=" "lesseqp!1" "S" "S!1" "t" "t!1")) (("" (assert) (("" (replace -1) (("" (expand "greatest_lower_bound?") (("" (flatten) (("" (split 1) (("1" (expand "lower_bound?") (("1" (skosimp) (("1" (typepred "r!1") (("1" (expand "add") (("1" (split -1) (("1" (typepred "lesseqp!1") (("1" (expand "partial_order?") (("1" (expand "preorder?") (("1" (flatten) (("1" (expand "reflexive?") (("1" (inst - "t!1") (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "member") (("2" (inst - "r!1") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (skosimp) (("2" (expand "lower_bound?") (("2" (inst - "t!1") (("2" (expand "add") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((partial_order? const-decl "bool" orders nil) (greatest_bounded_below? const-decl "bool" bounded_orders nil) (pred type-eq-decl nil defined_types nil) (set type-eq-decl nil sets nil) (T formal-type-decl nil bounded_orders nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (antisymmetric? const-decl "bool" relations nil) (PRED type-eq-decl nil defined_types nil) (glb_def formula-decl nil bounded_orders nil) (lower_bound? const-decl "bool" bounded_orders nil) (nonempty? const-decl "bool" sets nil) (add const-decl "(nonempty?)" sets nil) --> -------------------- --> maximum size reached --> -------------------- [ Verzeichnis aufwärts0.37unsichere Verbindung Übersetzung europäischer Sprachen durch Browser ] |