| products/Sources/formale Sprachen/PVS/sets_aux/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: cardinal.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(cardinal
(cardinal_member 0 (cardinal_member-1 nil 3319291475 ("" (skolem!) (("" (expand* "cardinal" "quotient_map" "EquivClass") (("" (lemma "card_eq_is_reflexive") (("" (expand "reflexive?") (("" (inst?) nil nil)) nil)) nil)) nil)) nil) ((quotient_map const-decl "Quotient(S)" QuotientDefinition nil) (EquivClass const-decl "set[T]" QuotientDefinition nil) (cardinal const-decl "cardinal_number" cardinal nil) (reflexive? const-decl "bool" relations nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil cardinal nil) (card_eq_is_reflexive judgement-tcc nil card_single nil)) shostak)) (cardinal_closed 0 (cardinal_closed-1 nil 3319330804 ("" (skosimp* t) (("" (replace -1) (("" (hide -1) (("" (decompose-equality) (("" (expand* "cardinal" "quotient_map" "EquivClass") (("" (iff) (("" (prop) (("1" (rewrite "card_eq_symmetric" -2) (("1" (forward-chain "card_eq_transitive") nil nil)) nil) ("2" (forward-chain "card_eq_transitive") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((card_eq_is_equivalence name-judgement "equivalence[set[T]]" cardinal nil) (cardinal const-decl "cardinal_number" cardinal nil) (card_eq_symmetric formula-decl nil card_comp_set_props nil) (card_eq_transitive formula-decl nil card_comp_set_transitive nil) (quotient_map const-decl "Quotient(S)" QuotientDefinition 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 cardinal nil) (set type-eq-decl nil sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (EquivClass const-decl "set[T]" QuotientDefinition nil) (card_eq const-decl "bool" card_comp_set nil) (cardinal_number type-eq-decl nil cardinal nil)) shostak)) (cardinal_empty 0 (cardinal_empty-1 nil 3319286580 ("" (grind-with-ext) (("" (lemma "fun_exists[(emptyset[T]), (x!1)]") (("" (prop) (("1" (skolem!) (("1" (inst + "f!1") (("1" (grind) nil nil)) nil)) nil) ("2" (skolem-typepred) (("2" (expand "emptyset") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ((fun_exists formula-decl nil function_image nil) (NOT const-decl "[bool -> bool]" booleans nil) (injective? const-decl "bool" functions nil) (surjective? const-decl "bool" functions nil) (bijective? const-decl "bool" functions nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (EquivClass const-decl "set[T]" QuotientDefinition nil) (card_eq const-decl "bool" card_comp_set nil) (singleton? const-decl "bool" sets nil) (singleton const-decl "(singleton?)" sets nil) (T formal-type-decl nil cardinal nil) (boolean nonempty-type-decl nil booleans nil) (nonempty_singleton_finite application-judgement "non_empty_finite_set" finite_sets nil) (card_eq_is_equivalence name-judgement "equivalence[set[T]]" cardinal nil) (finite_emptyset name-judgement "finite_set" cardinal nil) (finite_emptyset name-judgement "finite_set" finite_sets nil) (quotient_map const-decl "Quotient(S)" QuotientDefinition nil) (cardinal const-decl "cardinal_number" cardinal nil) (emptyset const-decl "set" sets nil)) shostak)) (cardinal_finite 0 (cardinal_finite-1 nil 3319286915 ("" (skolem-typepred) (("" (expand* "cardinal" "quotient_map" "EquivClass") (("" (rewrite "card_eq_symmetric") (("" (grind :if-match nil) (("" (inst + "N!1" "f!1 o f!2") (("" (skosimp) (("" (expand "o") (("" (inst - "f!2(x1!1)" "f!2(x2!1)") (("" (inst - "x1!1" "x2!1") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((quotient_map const-decl "Quotient(S)" QuotientDefinition nil) (bijective? const-decl "bool" functions nil) (surjective? const-decl "bool" functions nil) (injective? const-decl "bool" functions 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) (>= const-decl "bool" 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) (nat nonempty-type-eq-decl nil naturalnumbers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (< const-decl "bool" reals nil) (below type-eq-decl nil nat_types nil) (O const-decl "T3" function_props nil) (card_eq_is_equivalence name-judgement "equivalence[set[T]]" cardinal nil) (card_eq_symmetric formula-decl nil card_comp_set_props nil) (cardinal const-decl "cardinal_number" cardinal nil) (cardinal_number type-eq-decl nil cardinal nil) (card_eq const-decl "bool" card_comp_set nil) (EquivClass const-decl "set[T]" QuotientDefinition nil) (= const-decl "[T, T -> boolean]" equalities 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 cardinal nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) shostak)) (cardinal_finite_card_TCC1 0 (cardinal_finite_card_TCC1-1 nil 3319286566 ("" (skolem!) (("" (use "cardinal_finite") nil nil)) nil) ((cardinal const-decl "cardinal_number" cardinal nil) (cardinal_number type-eq-decl nil cardinal nil) (card_eq const-decl "bool" card_comp_set nil) (EquivClass const-decl "set[T]" QuotientDefinition nil) (= const-decl "[T, T -> boolean]" equalities 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) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil cardinal nil) (cardinal_finite formula-decl nil cardinal nil)) nil)) (cardinal_finite_card 0 (cardinal_finite_card-1 nil 3319287151 ("" (skolem-typepred) (("" (expand* "cardinal" "quotient_map" "EquivClass") (("" (rewrite "card_equal") (("" (rewrite "card_eq_symmetric") nil nil)) nil)) nil)) nil) ((quotient_map const-decl "Quotient(S)" QuotientDefinition nil) (card_eq_symmetric formula-decl nil card_comp_set_props nil) (card_eq_is_equivalence name-judgement "equivalence[set[T]]" cardinal nil) (card_equal formula-decl nil card_finite nil) (cardinal const-decl "cardinal_number" cardinal nil) (cardinal_number type-eq-decl nil cardinal nil) (card_eq const-decl "bool" card_comp_set nil) (EquivClass const-decl "set[T]" QuotientDefinition nil) (= const-decl "[T, T -> boolean]" equalities 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 cardinal nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil)) shostak)) (cardinal_equality 0 (cardinal_equality-1 nil 3319287441 ("" (skosimp* t) (("" (lemma "EquivClassEq") (("" (inst - "card_eq" "x!1" "x!2") (("" (lemma "rep_lemma") (("" (inst-cp - "card_eq" "x!2") (("" (inst - "card_eq" "x!1") (("" (expand "EquivClass" -1 1) (("" (expand "EquivClass" -2 1) (("" (ground) (("1" (rewrite "card_eq_symmetric" -4) (("1" (lemma "card_eq_transitive") (("1" (inst-cp - "rep(card_eq)(A!1)" "x!1" "x!2") (("1" (inst - "rep(card_eq)(A!1)" "x!2" "rep(card_eq)(B!1)") (("1" (assert) nil nil)) nil)) nil)) nil)) nil) ("2" (rewrite "card_eq_symmetric" -3) (("2" (lemma "card_eq_transitive") (("2" (inst-cp - "x!1" "rep(card_eq)(A!1)" "rep(card_eq)(B!1)") (("2" (inst - "x!1" "rep(card_eq)(B!1)" "x!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((EquivClassEq formula-decl nil QuotientDefinition nil) (rep_lemma formula-decl nil QuotientDefinition nil) (rep const-decl "T" QuotientDefinition nil) (Quotient type-eq-decl nil QuotientDefinition nil) (card_eq_symmetric formula-decl nil card_comp_set_props nil) (card_eq_transitive formula-decl nil card_comp_set_transitive nil) (PRED type-eq-decl nil defined_types nil) (equivalence? const-decl "bool" relations nil) (equivalence type-eq-decl nil relations nil) (card_eq_is_equivalence name-judgement "equivalence[set[T]]" cardinal 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 cardinal nil) (set type-eq-decl nil sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (EquivClass const-decl "set[T]" QuotientDefinition nil) (card_eq const-decl "bool" card_comp_set nil) (cardinal_number type-eq-decl nil cardinal nil)) shostak)) (cardinal_lt 0 (cardinal_lt-1 nil 3319289652 ("" (skosimp* t) (("" (expand "<") (("" (lemma "rep_lemma") (("" (inst-cp - "card_eq" "x!2") (("" (inst - "card_eq" "x!1") (("" (prop) (("1" (expand "EquivClass" -2 1) (("1" (expand "EquivClass" -3 1) (("1" (skolem-typepred) (("1" (replace -6 -1) (("1" (replace -7 -2) (("1" (expand "EquivClass" (-1 -2)) (("1" (rewrite "card_eq_symmetric" -1) (("1" (rewrite "card_eq_symmetric" -5) (("1" (lemma "card_eq_transitive") (("1" (inst-cp - "S!1" "x!1" "rep(card_eq)(A!1)") (("1" (inst - "rep(card_eq)(B!1)" "x!2" "R!1") (("1" (lemma "card_eq_lt_transitive") (("1" (inst - "S!1" "rep(card_eq)(A!1)" "rep(card_eq)(B!1)") (("1" (lemma "card_lt_eq_transitive") (("1" (inst - "S!1" "rep(card_eq)(B!1)" "R!1") (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (inst - "rep(card_eq)(A!1)" "rep(card_eq)(B!1)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((< const-decl "bool" cardinal nil) (card_eq_is_equivalence name-judgement "equivalence[set[T]]" cardinal nil) (equivalence type-eq-decl nil relations nil) (equivalence? const-decl "bool" relations nil) (PRED type-eq-decl nil defined_types nil) (rep const-decl "T" QuotientDefinition nil) (Quotient type-eq-decl nil QuotientDefinition nil) (card_eq_lt_transitive formula-decl nil card_comp_set_transitive nil) (card_lt_eq_transitive formula-decl nil card_comp_set_transitive nil) (card_lt_is_irreflexive name-judgement "(irreflexive?[set[T]])" cardinal nil) (card_lt_is_antisymmetric name-judgement "(antisymmetric?[set[T]])" cardinal nil) (card_lt_is_transitive name-judgement "(transitive?[set[T]])" cardinal nil) (card_eq_transitive formula-decl nil card_comp_set_transitive nil) (card_eq_symmetric formula-decl nil card_comp_set_props nil) (rep_lemma formula-decl nil QuotientDefinition 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 cardinal nil) (set type-eq-decl nil sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (EquivClass const-decl "set[T]" QuotientDefinition nil) (card_eq const-decl "bool" card_comp_set nil) (cardinal_number type-eq-decl nil cardinal nil)) shostak)) (cardinal_le 0 (cardinal_le-1 nil 3319290137 ("" (skosimp* t) (("" (expand "<=") (("" (lemma "rep_lemma") (("" (inst-cp - "card_eq" "x!2") (("" (inst - "card_eq" "x!1") (("" (prop) (("1" (expand "EquivClass" -2 1) (("1" (expand "EquivClass" -3 1) (("1" (skolem-typepred) (("1" (replace -6 -1) (("1" (replace -7 -2) (("1" (expand "EquivClass" (-1 -2)) (("1" (rewrite "card_eq_symmetric" -1) (("1" (rewrite "card_eq_symmetric" -5) (("1" (lemma "card_eq_transitive") (("1" (inst-cp - "S!1" "x!1" "rep(card_eq)(A!1)") (("1" (inst - "rep(card_eq)(B!1)" "x!2" "R!1") (("1" (lemma "card_eq_le_transitive") (("1" (inst - "S!1" "rep(card_eq)(A!1)" "rep(card_eq)(B!1)") (("1" (lemma "card_le_eq_transitive") (("1" (inst - "S!1" "rep(card_eq)(B!1)" "R!1") (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (inst - "rep(card_eq)(A!1)" "rep(card_eq)(B!1)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((<= const-decl "bool" cardinal nil) (card_eq_is_equivalence name-judgement "equivalence[set[T]]" cardinal nil) (equivalence type-eq-decl nil relations nil) (equivalence? const-decl "bool" relations nil) (PRED type-eq-decl nil defined_types nil) (rep const-decl "T" QuotientDefinition nil) (Quotient type-eq-decl nil QuotientDefinition nil) (card_eq_le_transitive formula-decl nil card_comp_set_transitive nil) (card_le_eq_transitive formula-decl nil card_comp_set_transitive nil) (card_le_is_reflexive name-judgement "(reflexive?[set[T]])" cardinal nil) (card_le_is_transitive name-judgement "(transitive?[set[T]])" cardinal nil) (card_le_is_dichotomous name-judgement "(dichotomous?[set[T]])" cardinal nil) (card_eq_transitive formula-decl nil card_comp_set_transitive nil) (card_eq_symmetric formula-decl nil card_comp_set_props nil) (rep_lemma formula-decl nil QuotientDefinition 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 cardinal nil) (set type-eq-decl nil sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (EquivClass const-decl "set[T]" QuotientDefinition nil) (card_eq const-decl "bool" card_comp_set nil) (cardinal_number type-eq-decl nil cardinal nil)) shostak)) (cardinal_eq 0 (cardinal_eq-1 nil 3319290289 ("" (skosimp* t) (("" (prop) (("1" (skolem-typepred) (("1" (replace -3 -2 :dir rl) (("1" (replace -4 -1) (("1" (replace -4 -2) (("1" (expand "EquivClass" (-1 -2)) (("1" (rewrite "card_eq_symmetric") (("1" (forward-chain "card_eq_transitive") nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (lemma "EquivClassEq") (("2" (inst - "card_eq" "x!1" "x!2") (("2" (assert) (("2" (lemma "card_eq_is_reflexive") (("2" (expand "reflexive?") (("2" (inst - "x!1" "x!2") (("1" (replace -3 1) (("1" (expand "EquivClass" 1) (("1" (inst?) nil nil)) nil)) nil) ("2" (replace -2 1) (("2" (expand "EquivClass" 1) (("2" (inst?) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((card_eq_symmetric formula-decl nil card_comp_set_props nil) (card_eq_is_equivalence name-judgement "equivalence[set[T]]" cardinal nil) (card_eq_transitive formula-decl nil card_comp_set_transitive nil) (equivalence type-eq-decl nil relations nil) (equivalence? const-decl "bool" relations nil) (PRED type-eq-decl nil defined_types nil) (card_eq_is_reflexive judgement-tcc nil card_single nil) (A!1 skolem-const-decl "cardinal_number" cardinal nil) (x!1 skolem-const-decl "set[T]" cardinal nil) (B!1 skolem-const-decl "cardinal_number" cardinal nil) (x!2 skolem-const-decl "set[T]" cardinal nil) (reflexive? const-decl "bool" relations nil) (EquivClassEq formula-decl nil QuotientDefinition 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 cardinal nil) (set type-eq-decl nil sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (EquivClass const-decl "set[T]" QuotientDefinition nil) (card_eq const-decl "bool" card_comp_set nil) (cardinal_number type-eq-decl nil cardinal nil)) shostak)) (cardinal_ge 0 (cardinal_ge-1 nil 3319290785 ("" (skosimp* t) (("" (expand ">=") (("" (lemma "rep_lemma") (("" (inst-cp - "card_eq" "x!2") (("" (inst - "card_eq" "x!1") (("" (prop) (("1" (expand "EquivClass" -2 1) (("1" (expand "EquivClass" -3 1) (("1" (skolem-typepred) (("1" (replace -6 -1) (("1" (replace -7 -2) (("1" (expand "EquivClass" (-1 -2)) (("1" (rewrite "card_eq_symmetric" -1) (("1" (rewrite "card_eq_symmetric" -5) (("1" (lemma "card_eq_transitive") (("1" (inst-cp - "S!1" "x!1" "rep(card_eq)(A!1)") (("1" (inst - "rep(card_eq)(B!1)" "x!2" "R!1") (("1" (lemma "card_eq_ge_transitive") (("1" (inst - "S!1" "rep(card_eq)(A!1)" "rep(card_eq)(B!1)") (("1" (lemma "card_ge_eq_transitive") (("1" (inst - "S!1" "rep(card_eq)(B!1)" "R!1") (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (inst - "rep(card_eq)(A!1)" "rep(card_eq)(B!1)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((>= const-decl "bool" cardinal nil) (card_eq_is_equivalence name-judgement "equivalence[set[T]]" cardinal nil) (equivalence type-eq-decl nil relations nil) (equivalence? const-decl "bool" relations nil) (PRED type-eq-decl nil defined_types nil) (rep const-decl "T" QuotientDefinition nil) (Quotient type-eq-decl nil QuotientDefinition nil) (card_eq_ge_transitive formula-decl nil card_comp_set_transitive nil) (card_ge_eq_transitive formula-decl nil card_comp_set_transitive nil) (card_ge_is_reflexive name-judgement "(reflexive?[set[T]])" cardinal nil) (card_ge_is_transitive name-judgement "(transitive?[set[T]])" cardinal nil) (card_ge_is_dichotomous name-judgement "(dichotomous?[set[T]])" cardinal nil) (card_eq_transitive formula-decl nil card_comp_set_transitive nil) (card_eq_symmetric formula-decl nil card_comp_set_props nil) (rep_lemma formula-decl nil QuotientDefinition 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 cardinal nil) (set type-eq-decl nil sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (EquivClass const-decl "set[T]" QuotientDefinition nil) (card_eq const-decl "bool" card_comp_set nil) (cardinal_number type-eq-decl nil cardinal nil)) shostak)) (cardinal_gt 0 (cardinal_gt-1 nil 3319290902 ("" (skosimp* t) (("" (expand ">") (("" (lemma "rep_lemma") (("" (inst-cp - "card_eq" "x!2") (("" (inst - "card_eq" "x!1") (("" (prop) (("1" (expand "EquivClass" -2 1) (("1" (expand "EquivClass" -3 1) (("1" (skolem-typepred) (("1" (replace -6 -1) (("1" (replace -7 -2) (("1" (expand "EquivClass" (-1 -2)) (("1" (rewrite "card_eq_symmetric" -1) (("1" (rewrite "card_eq_symmetric" -5) (("1" (lemma "card_eq_transitive") (("1" (inst-cp - "S!1" "x!1" "rep(card_eq)(A!1)") (("1" (inst - "rep(card_eq)(B!1)" "x!2" "R!1") (("1" (lemma "card_eq_gt_transitive") (("1" (inst - "S!1" "rep(card_eq)(A!1)" "rep(card_eq)(B!1)") (("1" (lemma "card_gt_eq_transitive") (("1" (inst - "S!1" "rep(card_eq)(B!1)" "R!1") (("1" (ground) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (assert) (("2" (inst - "rep(card_eq)(A!1)" "rep(card_eq)(B!1)") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((> const-decl "bool" cardinal nil) (card_eq_is_equivalence name-judgement "equivalence[set[T]]" cardinal nil) (equivalence type-eq-decl nil relations nil) (equivalence? const-decl "bool" relations nil) (PRED type-eq-decl nil defined_types nil) (rep const-decl "T" QuotientDefinition nil) (Quotient type-eq-decl nil QuotientDefinition nil) (card_eq_gt_transitive formula-decl nil card_comp_set_transitive nil) (card_gt_eq_transitive formula-decl nil card_comp_set_transitive nil) (card_gt_is_irreflexive name-judgement "(irreflexive?[set[T]])" cardinal nil) (card_gt_is_antisymmetric name-judgement "(antisymmetric?[set[T]])" cardinal nil) (card_gt_is_transitive name-judgement "(transitive?[set[T]])" cardinal nil) (card_eq_transitive formula-decl nil card_comp_set_transitive nil) (card_eq_symmetric formula-decl nil card_comp_set_props nil) (rep_lemma formula-decl nil QuotientDefinition 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 cardinal nil) (set type-eq-decl nil sets nil) (= const-decl "[T, T -> boolean]" equalities nil) (EquivClass const-decl "set[T]" QuotientDefinition nil) (card_eq const-decl "bool" card_comp_set nil) (cardinal_number type-eq-decl nil cardinal nil)) shostak)) (cardinal_card_lt 0 (cardinal_card_lt-1 nil 3319288643 ("" (skolem!) (("" (use "cardinal_lt") (("" (ground) (("1" (inst - "R!1" "S!1") (("1" (use "cardinal_member") nil nil) ("2" (use "cardinal_member") nil nil)) nil) ("2" (skolem-typepred) (("2" (hide 1 3) (("2" (expand* "cardinal" "quotient_map" "EquivClass") (("2" (rewrite "card_eq_symmetric") (("2" (lemma "card_lt_eq_transitive") (("2" (inst - "R!1" "S!1" "R!2") (("2" (lemma "card_eq_lt_transitive") (("2" (inst - "S!2" "R!1" "R!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((cardinal_lt formula-decl nil cardinal nil) (cardinal const-decl "cardinal_number" cardinal nil) (cardinal_number type-eq-decl nil cardinal nil) (card_eq const-decl "bool" card_comp_set nil) (EquivClass const-decl "set[T]" QuotientDefinition nil) (= const-decl "[T, T -> boolean]" equalities nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil cardinal nil) (NOT const-decl "[bool -> bool]" booleans nil) (quotient_map const-decl "Quotient(S)" QuotientDefinition nil) (card_lt_eq_transitive formula-decl nil card_comp_set_transitive nil) (card_eq_lt_transitive formula-decl nil card_comp_set_transitive nil) (card_eq_is_equivalence name-judgement "equivalence[set[T]]" cardinal nil) (card_eq_symmetric formula-decl nil card_comp_set_props nil) (R!1 skolem-const-decl "set[T]" cardinal nil) (S!1 skolem-const-decl "set[T]" cardinal nil) (cardinal_member formula-decl nil cardinal nil) (card_lt_is_transitive name-judgement "(transitive?[set[T]])" cardinal nil) (card_lt_is_antisymmetric name-judgement "(antisymmetric?[set[T]])" cardinal nil) (card_lt_is_irreflexive name-judgement "(irreflexive?[set[T]])" cardinal nil)) shostak)) (cardinal_card_le 0 (cardinal_card_le-1 nil 3319291621 ("" (skolem!) (("" (use "cardinal_le") (("" (ground) (("1" (inst - "R!1" "S!1") (("1" (use "cardinal_member") nil nil) ("2" (use "cardinal_member") nil nil)) nil) ("2" (skolem-typepred) (("2" (hide 1 3) (("2" (expand* "cardinal" "quotient_map" "EquivClass") (("2" (rewrite "card_eq_symmetric") (("2" (lemma "card_le_eq_transitive") (("2" (inst - "R!1" "S!1" "R!2") (("2" (lemma "card_eq_le_transitive") (("2" (inst - "S!2" "R!1" "R!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((cardinal_le formula-decl nil cardinal nil) (cardinal const-decl "cardinal_number" cardinal nil) (cardinal_number type-eq-decl nil cardinal nil) (card_eq const-decl "bool" card_comp_set nil) (EquivClass const-decl "set[T]" QuotientDefinition nil) (= const-decl "[T, T -> boolean]" equalities nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil cardinal nil) (NOT const-decl "[bool -> bool]" booleans nil) (quotient_map const-decl "Quotient(S)" QuotientDefinition nil) (card_le_eq_transitive formula-decl nil card_comp_set_transitive nil) (card_eq_le_transitive formula-decl nil card_comp_set_transitive nil) (card_eq_is_equivalence name-judgement "equivalence[set[T]]" cardinal nil) (card_eq_symmetric formula-decl nil card_comp_set_props nil) (R!1 skolem-const-decl "set[T]" cardinal nil) (S!1 skolem-const-decl "set[T]" cardinal nil) (cardinal_member formula-decl nil cardinal nil) (card_le_is_dichotomous name-judgement "(dichotomous?[set[T]])" cardinal nil) (card_le_is_transitive name-judgement "(transitive?[set[T]])" cardinal nil) (card_le_is_reflexive name-judgement "(reflexive?[set[T]])" cardinal nil)) shostak)) (cardinal_card_eq 0 (cardinal_card_eq-1 nil 3319291850 ("" (skolem!) (("" (use "cardinal_eq") (("" (ground) (("1" (inst - "R!1" "S!1") (("1" (use "cardinal_member") nil nil) ("2" (use "cardinal_member") nil nil)) nil) ("2" (skolem-typepred) (("2" (hide 1 3) (("2" (expand* "cardinal" "quotient_map" "EquivClass") (("2" (rewrite "card_eq_symmetric") (("2" (lemma "card_eq_transitive") (("2" (inst-cp - "S!2" "R!1" "S!1") (("2" (inst - "S!2" "S!1" "R!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((cardinal_eq formula-decl nil cardinal nil) (cardinal const-decl "cardinal_number" cardinal nil) (cardinal_number type-eq-decl nil cardinal nil) (card_eq const-decl "bool" card_comp_set nil) (EquivClass const-decl "set[T]" QuotientDefinition nil) (= const-decl "[T, T -> boolean]" equalities nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil cardinal nil) (NOT const-decl "[bool -> bool]" booleans nil) (quotient_map const-decl "Quotient(S)" QuotientDefinition nil) (card_eq_transitive formula-decl nil card_comp_set_transitive nil) (card_eq_symmetric formula-decl nil card_comp_set_props nil) (R!1 skolem-const-decl "set[T]" cardinal nil) (S!1 skolem-const-decl "set[T]" cardinal nil) (cardinal_member formula-decl nil cardinal nil) (card_eq_is_equivalence name-judgement "equivalence[set[T]]" cardinal nil)) shostak)) (cardinal_card_ge 0 (cardinal_card_ge-1 nil 3319291727 ("" (skolem!) (("" (use "cardinal_ge") (("" (ground) (("1" (inst - "R!1" "S!1") (("1" (use "cardinal_member") nil nil) ("2" (use "cardinal_member") nil nil)) nil) ("2" (skolem-typepred) (("2" (hide 1 3) (("2" (expand* "cardinal" "quotient_map" "EquivClass") (("2" (rewrite "card_eq_symmetric") (("2" (lemma "card_ge_eq_transitive") (("2" (inst - "R!1" "S!1" "R!2") (("2" (lemma "card_eq_ge_transitive") (("2" (inst - "S!2" "R!1" "R!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((cardinal_ge formula-decl nil cardinal nil) (cardinal const-decl "cardinal_number" cardinal nil) (cardinal_number type-eq-decl nil cardinal nil) (card_eq const-decl "bool" card_comp_set nil) (EquivClass const-decl "set[T]" QuotientDefinition nil) (= const-decl "[T, T -> boolean]" equalities nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil cardinal nil) (NOT const-decl "[bool -> bool]" booleans nil) (quotient_map const-decl "Quotient(S)" QuotientDefinition nil) (card_ge_eq_transitive formula-decl nil card_comp_set_transitive nil) (card_eq_ge_transitive formula-decl nil card_comp_set_transitive nil) (card_eq_is_equivalence name-judgement "equivalence[set[T]]" cardinal nil) (card_eq_symmetric formula-decl nil card_comp_set_props nil) (R!1 skolem-const-decl "set[T]" cardinal nil) (S!1 skolem-const-decl "set[T]" cardinal nil) (cardinal_member formula-decl nil cardinal nil) (card_ge_is_dichotomous name-judgement "(dichotomous?[set[T]])" cardinal nil) (card_ge_is_transitive name-judgement "(transitive?[set[T]])" cardinal nil) (card_ge_is_reflexive name-judgement "(reflexive?[set[T]])" cardinal nil)) shostak)) (cardinal_card_gt 0 (cardinal_card_gt-1 nil 3319291785 ("" (skolem!) (("" (use "cardinal_gt") (("" (ground) (("1" (inst - "R!1" "S!1") (("1" (use "cardinal_member") nil nil) ("2" (use "cardinal_member") nil nil)) nil) ("2" (skolem-typepred) (("2" (hide 1 3) (("2" (expand* "cardinal" "quotient_map" "EquivClass") (("2" (rewrite "card_eq_symmetric") (("2" (lemma "card_gt_eq_transitive") (("2" (inst - "R!1" "S!1" "R!2") (("2" (lemma "card_eq_gt_transitive") (("2" (inst - "S!2" "R!1" "R!2") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((cardinal_gt formula-decl nil cardinal nil) (cardinal const-decl "cardinal_number" cardinal nil) (cardinal_number type-eq-decl nil cardinal nil) (card_eq const-decl "bool" card_comp_set nil) (EquivClass const-decl "set[T]" QuotientDefinition nil) (= const-decl "[T, T -> boolean]" equalities nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil cardinal nil) (NOT const-decl "[bool -> bool]" booleans nil) (quotient_map const-decl "Quotient(S)" QuotientDefinition nil) (card_gt_eq_transitive formula-decl nil card_comp_set_transitive nil) (card_eq_gt_transitive formula-decl nil card_comp_set_transitive nil) (card_eq_is_equivalence name-judgement "equivalence[set[T]]" cardinal nil) (card_eq_symmetric formula-decl nil card_comp_set_props nil) (R!1 skolem-const-decl "set[T]" cardinal nil) (S!1 skolem-const-decl "set[T]" cardinal nil) (cardinal_member formula-decl nil cardinal nil) (card_gt_is_transitive name-judgement "(transitive?[set[T]])" cardinal nil) (card_gt_is_antisymmetric name-judgement "(antisymmetric?[set[T]])" cardinal nil) (card_gt_is_irreflexive name-judgement "(irreflexive?[set[T]])" cardinal nil)) shostak)) (cardinal_lt_gt 0 (cardinal_lt_gt-1 nil 3319292649 ("" (skolem!) (("" (expand* "<" ">") (("" (use "card_lt_gt") (("" (iff) (("" (propax) nil nil)) nil)) nil)) nil)) nil) ((> const-decl "bool" cardinal nil) (< const-decl "bool" cardinal nil) (card_eq_is_equivalence name-judgement "equivalence[set[T]]" cardinal nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (PRED type-eq-decl nil defined_types nil) (equivalence? const-decl "bool" relations nil) (equivalence type-eq-decl nil relations nil) (= const-decl "[T, T -> boolean]" equalities nil) (EquivClass const-decl "set[T]" QuotientDefinition nil) (Quotient type-eq-decl nil QuotientDefinition nil) (rep const-decl "T" QuotientDefinition nil) (card_eq const-decl "bool" card_comp_set nil) (cardinal_number type-eq-decl nil cardinal nil) (T formal-type-decl nil cardinal nil) (card_lt_gt formula-decl nil card_comp_set_props nil)) shostak)) (cardinal_le_ge 0 (cardinal_le_ge-1 nil 3319292703 ("" (skolem!) (("" (expand* "<=" ">=") (("" (use "card_le_ge") (("" (iff) (("" (propax) nil nil)) nil)) nil)) nil)) nil) ((>= const-decl "bool" cardinal nil) (<= const-decl "bool" cardinal nil) (card_eq_is_equivalence name-judgement "equivalence[set[T]]" cardinal nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (PRED type-eq-decl nil defined_types nil) (equivalence? const-decl "bool" relations nil) (equivalence type-eq-decl nil relations nil) (= const-decl "[T, T -> boolean]" equalities nil) (EquivClass const-decl "set[T]" QuotientDefinition nil) (Quotient type-eq-decl nil QuotientDefinition nil) (rep const-decl "T" QuotientDefinition nil) (card_eq const-decl "bool" card_comp_set nil) (cardinal_number type-eq-decl nil cardinal nil) (T formal-type-decl nil cardinal nil) (card_le_ge formula-decl nil card_comp_set_props nil)) shostak)) (cardinal_lt_le 0 (cardinal_lt_le-1 nil 3319292725 ("" (skolem!) (("" (expand* "<" "<=") (("" (use "card_le_lt_eq") (("" (use "cardinal_equality") (("" (use "card_lt_neq_ngt") (("" (prop) nil nil)) nil)) nil)) nil)) nil)) nil) ((<= const-decl "bool" cardinal nil) (< const-decl "bool" cardinal nil) (cardinal_equality formula-decl nil cardinal nil) (card_lt_neq_ngt formula-decl nil card_comp_set_props nil) (card_eq_is_equivalence name-judgement "equivalence[set[T]]" cardinal nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (PRED type-eq-decl nil defined_types nil) (equivalence? const-decl "bool" relations nil) (equivalence type-eq-decl nil relations nil) (= const-decl "[T, T -> boolean]" equalities nil) (EquivClass const-decl "set[T]" QuotientDefinition nil) (Quotient type-eq-decl nil QuotientDefinition nil) (rep const-decl "T" QuotientDefinition nil) (card_eq const-decl "bool" card_comp_set nil) (cardinal_number type-eq-decl nil cardinal nil) (T formal-type-decl nil cardinal nil) (card_le_lt_eq formula-decl nil card_comp_set_props nil)) shostak)) (cardinal_le_lt 0 (cardinal_le_lt-1 nil 3319296454 ("" (skolem!) (("" (expand* "<=" "<") (("" (use "card_le_lt_eq") (("" (use "cardinal_equality") (("" (prop) nil nil)) nil)) nil)) nil)) nil) ((< const-decl "bool" cardinal nil) (<= const-decl "bool" cardinal nil) (cardinal_equality formula-decl nil cardinal nil) (card_eq_is_equivalence name-judgement "equivalence[set[T]]" cardinal nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (PRED type-eq-decl nil defined_types nil) (equivalence? const-decl "bool" relations nil) (equivalence type-eq-decl nil relations nil) (= const-decl "[T, T -> boolean]" equalities nil) (EquivClass const-decl "set[T]" QuotientDefinition nil) (Quotient type-eq-decl nil QuotientDefinition nil) (rep const-decl "T" QuotientDefinition nil) (card_eq const-decl "bool" card_comp_set nil) (cardinal_number type-eq-decl nil cardinal nil) (T formal-type-decl nil cardinal nil) (card_le_lt_eq formula-decl nil card_comp_set_props nil)) shostak)) (cardinal_eq_lg 0 (cardinal_eq_lg-1 nil 3319299228 ("" (skolem!) (("" (lemma "cardinal_le_ge") (("" (inst - "B!1" "A!1") (("" (lemma "cardinal_lt_le") (("" (inst-cp - "B!1" "A!1") (("" (inst - "A!1" "B!1") (("" (lemma "cardinal_le_lt") (("" (inst-cp - "B!1" "A!1") (("" (inst - "A!1" "B!1") (("" (smash) (("" (expand "<") (("" (rewrite "card_lt_anticommutative") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((cardinal_le_ge formula-decl nil cardinal nil) (cardinal_lt_le formula-decl nil cardinal nil) (card_eq_is_equivalence name-judgement "equivalence[set[T]]" cardinal nil) (card_lt_anticommutative formula-decl nil card_comp_set_props nil) (PRED type-eq-decl nil defined_types nil) (equivalence? const-decl "bool" relations nil) (equivalence type-eq-decl nil relations nil) (Quotient type-eq-decl nil QuotientDefinition nil) (rep const-decl "T" QuotientDefinition nil) (< const-decl "bool" cardinal nil) (cardinal_le_lt formula-decl nil cardinal nil) (cardinal_number type-eq-decl nil cardinal nil) (card_eq const-decl "bool" card_comp_set nil) (EquivClass const-decl "set[T]" QuotientDefinition nil) (= const-decl "[T, T -> boolean]" equalities nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil cardinal nil)) shostak)) (cardinal_ge_gt 0 (cardinal_ge_gt-1 nil 3319299409 ("" (skolem!) (("" (expand* ">=" ">") (("" (use "card_ge_gt_eq") (("" (use "cardinal_equality") (("" (prop) nil nil)) nil)) nil)) nil)) nil) ((> const-decl "bool" cardinal nil) (>= const-decl "bool" cardinal nil) (cardinal_equality formula-decl nil cardinal nil) (card_eq_is_equivalence name-judgement "equivalence[set[T]]" cardinal nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (PRED type-eq-decl nil defined_types nil) (equivalence? const-decl "bool" relations nil) (equivalence type-eq-decl nil relations nil) (= const-decl "[T, T -> boolean]" equalities nil) (EquivClass const-decl "set[T]" QuotientDefinition nil) (Quotient type-eq-decl nil QuotientDefinition nil) (rep const-decl "T" QuotientDefinition nil) (card_eq const-decl "bool" card_comp_set nil) (cardinal_number type-eq-decl nil cardinal nil) (T formal-type-decl nil cardinal nil) (card_ge_gt_eq formula-decl nil card_comp_set_props nil)) shostak)) (cardinal_gt_ge 0 (cardinal_gt_ge-1 nil 3319299536 ("" (skolem!) (("" (expand* ">" ">=") (("" (use "card_ge_gt_eq") (("" (use "cardinal_equality") (("" (use "card_gt_neq_nlt") (("" (prop) nil nil)) nil)) nil)) nil)) nil)) nil) ((>= const-decl "bool" cardinal nil) (> const-decl "bool" cardinal nil) (cardinal_equality formula-decl nil cardinal nil) (card_gt_neq_nlt formula-decl nil card_comp_set_props nil) (card_eq_is_equivalence name-judgement "equivalence[set[T]]" cardinal nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (PRED type-eq-decl nil defined_types nil) (equivalence? const-decl "bool" relations nil) (equivalence type-eq-decl nil relations nil) (= const-decl "[T, T -> boolean]" equalities nil) (EquivClass const-decl "set[T]" QuotientDefinition nil) (Quotient type-eq-decl nil QuotientDefinition nil) (rep const-decl "T" QuotientDefinition nil) (card_eq const-decl "bool" card_comp_set nil) (cardinal_number type-eq-decl nil cardinal nil) (T formal-type-decl nil cardinal nil) (card_ge_gt_eq formula-decl nil card_comp_set_props nil)) shostak)) (cardinal_lt_not_ge 0 (cardinal_lt_not_ge-1 nil 3319299569 ("" (skolem!) (("" (expand* "<" ">=") (("" (use "card_lt_ge") (("" (expand* "XOR" "/=") (("" (iff) (("" (prop) nil nil)) nil)) nil)) nil)) nil)) nil) ((>= const-decl "bool" cardinal nil) (< const-decl "bool" cardinal nil) (/= const-decl "boolean" notequal nil) (XOR const-decl "bool" xor_def nil) (card_eq_is_equivalence name-judgement "equivalence[set[T]]" cardinal nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (PRED type-eq-decl nil defined_types nil) (equivalence? const-decl "bool" relations nil) (equivalence type-eq-decl nil relations nil) (= const-decl "[T, T -> boolean]" equalities nil) (EquivClass const-decl "set[T]" QuotientDefinition nil) (Quotient type-eq-decl nil QuotientDefinition nil) (rep const-decl "T" QuotientDefinition nil) (card_eq const-decl "bool" card_comp_set nil) (cardinal_number type-eq-decl nil cardinal nil) (T formal-type-decl nil cardinal nil) (card_lt_ge formula-decl nil card_comp_set_props nil)) shostak)) (cardinal_le_not_gt 0 (cardinal_le_not_gt-1 nil 3319299693 ("" (skolem!) (("" (expand* "<=" ">") (("" (use "card_le_gt") (("" (expand* "XOR" "/=") (("" (iff) (("" (prop) nil nil)) nil)) nil)) nil)) nil)) nil) ((> const-decl "bool" cardinal nil) (<= const-decl "bool" cardinal nil) (/= const-decl "boolean" notequal nil) (XOR const-decl "bool" xor_def nil) (card_eq_is_equivalence name-judgement "equivalence[set[T]]" cardinal nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (PRED type-eq-decl nil defined_types nil) (equivalence? const-decl "bool" relations nil) (equivalence type-eq-decl nil relations nil) (= const-decl "[T, T -> boolean]" equalities nil) (EquivClass const-decl "set[T]" QuotientDefinition nil) (Quotient type-eq-decl nil QuotientDefinition nil) (rep const-decl "T" QuotientDefinition nil) (card_eq const-decl "bool" card_comp_set nil) (cardinal_number type-eq-decl nil cardinal nil) (T formal-type-decl nil cardinal nil) (card_le_gt formula-decl nil card_comp_set_props nil)) shostak)) (cardinal_eq_not_lg 0 (cardinal_eq_not_lg-1 nil 3319299744 ("" (skolem!) (("" (use "cardinal_lt_le") (("" (use "cardinal_gt_ge") (("" (smash) (("" (expand* "<=" ">") (("" (use "card_le_gt") (("" (expand* "XOR" "/=") (("" (iff) (("" (prop) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((cardinal_lt_le formula-decl nil cardinal nil) (cardinal_number type-eq-decl nil cardinal nil) (card_eq const-decl "bool" card_comp_set nil) (EquivClass const-decl "set[T]" QuotientDefinition nil) (= const-decl "[T, T -> boolean]" equalities nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (T formal-type-decl nil cardinal nil) (card_le_gt formula-decl nil card_comp_set_props nil) (PRED type-eq-decl nil defined_types nil) (equivalence? const-decl "bool" relations nil) (equivalence type-eq-decl nil relations nil) (Quotient type-eq-decl nil QuotientDefinition nil) (rep const-decl "T" QuotientDefinition nil) (card_eq_is_equivalence name-judgement "equivalence[set[T]]" cardinal nil) (XOR const-decl "bool" xor_def nil) (/= const-decl "boolean" notequal nil) (<= const-decl "bool" cardinal nil) (> const-decl "bool" cardinal nil) (cardinal_gt_ge formula-decl nil cardinal nil)) shostak)) (cardinal_ge_not_lt 0 (cardinal_ge_not_lt-1 nil 3319299720 ("" (skolem!) (("" (expand* ">=" "<") (("" (use "card_lt_ge") (("" (expand* "XOR" "/=") (("" (iff) (("" (prop) nil nil)) nil)) nil)) nil)) nil)) nil) ((< const-decl "bool" cardinal nil) (>= const-decl "bool" cardinal nil) (/= const-decl "boolean" notequal nil) (XOR const-decl "bool" xor_def nil) (card_eq_is_equivalence name-judgement "equivalence[set[T]]" cardinal nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (PRED type-eq-decl nil defined_types nil) (equivalence? const-decl "bool" relations nil) (equivalence type-eq-decl nil relations nil) (= const-decl "[T, T -> boolean]" equalities nil) (EquivClass const-decl "set[T]" QuotientDefinition nil) (Quotient type-eq-decl nil QuotientDefinition nil) (rep const-decl "T" QuotientDefinition nil) (card_eq const-decl "bool" card_comp_set nil) (cardinal_number type-eq-decl nil cardinal nil) (T formal-type-decl nil cardinal nil) (card_lt_ge formula-decl nil card_comp_set_props nil)) shostak)) (cardinal_gt_not_le 0 (cardinal_gt_not_le-1 nil 3319299653 ("" (skolem!) (("" (expand* ">" "<=") (("" (use "card_le_gt") (("" (expand* "XOR" "/=") (("" (iff) (("" (prop) nil nil)) nil)) nil)) nil)) nil)) nil) ((<= const-decl "bool" cardinal nil) (> const-decl "bool" cardinal nil) (/= const-decl "boolean" notequal nil) (XOR const-decl "bool" xor_def nil) (card_eq_is_equivalence name-judgement "equivalence[set[T]]" cardinal nil) (boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (set type-eq-decl nil sets nil) (PRED type-eq-decl nil defined_types nil) (equivalence? const-decl "bool" relations nil) (equivalence type-eq-decl nil relations nil) (= const-decl "[T, T -> boolean]" equalities nil) (EquivClass const-decl "set[T]" QuotientDefinition nil) (Quotient type-eq-decl nil QuotientDefinition nil) (rep const-decl "T" QuotientDefinition nil) (card_eq const-decl "bool" card_comp_set nil) (cardinal_number type-eq-decl nil cardinal nil) (T formal-type-decl nil cardinal nil) (card_le_gt formula-decl nil card_comp_set_props nil)) shostak)) (cardinal_lt_strict_total_order 0 (cardinal_lt_strict_total_order-1 nil 3319292622 ("" (expand* "strict_total_order?" "strict_order?") (("" (split) (("1" (lemma "card_lt_is_irreflexive") (("1" (expand* "irreflexive?" "<") (("1" (skolem!) (("1" (inst?) nil nil)) nil)) nil)) nil) ("2" (expand* "transitive?" "<") (("2" (skosimp) (("2" (lemma "card_lt_transitive") (("2" (inst - "rep(card_eq)(x!1)" "rep(card_eq)(y!1)" "rep(card_eq)(z!1)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (expand "trichotomous?") (("3" (skosimp) (("3" (use "cardinal_eq_not_lg") (("3" (assert) (("3" (rewrite "cardinal_lt_gt" 2) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ((< const-decl "bool" cardinal nil) (irreflexive? const-decl "bool" relations nil) (cardinal_number type-eq-decl nil cardinal nil) (card_eq const-decl "bool" card_comp_set nil) (rep const-decl "T" QuotientDefinition nil) (Quotient type-eq-decl nil QuotientDefinition nil) (EquivClass const-decl "set[T]" QuotientDefinition nil) (= const-decl "[T, T -> boolean]" equalities nil) (equivalence type-eq-decl nil relations nil) (equivalence? const-decl "bool" relations nil) (PRED type-eq-decl nil defined_types nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (card_eq_is_equivalence name-judgement "equivalence[set[T]]" cardinal nil) (card_lt_is_irreflexive judgement-tcc nil card_single nil) (T formal-type-decl nil cardinal nil) (card_lt_is_irreflexive name-judgement "(irreflexive?[set[T]])" cardinal nil) (card_lt_is_antisymmetric name-judgement "(antisymmetric?[set[T]])" cardinal nil) (card_lt_is_transitive name-judgement "(transitive?[set[T]])" cardinal nil) (card_lt_transitive formula-decl nil card_comp_set_transitive nil) (transitive? const-decl "bool" relations nil) (cardinal_lt_gt formula-decl nil cardinal nil) (cardinal_eq_not_lg formula-decl nil cardinal nil) (trichotomous? const-decl "bool" orders nil) (strict_total_order? const-decl "bool" orders nil) (strict_order? const-decl "bool" orders nil)) nil)) (cardinal_le_total_order 0 (cardinal_le_total_order-1 nil 3319292622 ("" (expand* "total_order?" "partial_order?" "preorder?") (("" (split) (("1" (lemma "card_le_is_reflexive") (("1" (expand* "reflexive?" "<=") (("1" (skolem!) (("1" (inst?) nil nil)) nil)) nil)) nil) ("2" (expand* "transitive?" "<=") (("2" (skosimp) (("2" (lemma "card_le_transitive") (("2" (inst - "rep(card_eq)(x!1)" "rep(card_eq)(y!1)" "rep(card_eq)(z!1)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (expand "antisymmetric?") (("3" (skosimp) (("3" (use "cardinal_eq_lg") (("3" (assert) (("3" (rewrite "cardinal_le_ge" -2) nil nil)) nil)) nil)) nil)) nil) ("4" (expand "dichotomous?") (("4" (skosimp) (("4" (use "cardinal_le_not_gt") (("4" (assert) (("4" (rewrite "cardinal_lt_gt" :dir rl) (("4" (rewrite "cardinal_lt_le") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((<= const-decl "bool" cardinal nil) (reflexive? const-decl "bool" relations nil) (cardinal_number type-eq-decl nil cardinal nil) (card_eq const-decl "bool" card_comp_set nil) (rep const-decl "T" QuotientDefinition nil) (Quotient type-eq-decl nil QuotientDefinition nil) (EquivClass const-decl "set[T]" QuotientDefinition nil) (= const-decl "[T, T -> boolean]" equalities nil) (equivalence type-eq-decl nil relations nil) (equivalence? const-decl "bool" relations nil) (PRED type-eq-decl nil defined_types nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (card_eq_is_equivalence name-judgement "equivalence[set[T]]" cardinal nil) (T formal-type-decl nil cardinal nil) (card_le_is_reflexive judgement-tcc nil card_single nil) (card_le_is_reflexive name-judgement "(reflexive?[set[T]])" cardinal nil) (card_le_is_transitive name-judgement "(transitive?[set[T]])" cardinal nil) (card_le_is_dichotomous name-judgement "(dichotomous?[set[T]])" cardinal nil) (card_le_transitive formula-decl nil card_comp_set_transitive nil) (transitive? const-decl "bool" relations nil) (cardinal_le_ge formula-decl nil cardinal nil) (cardinal_eq_lg formula-decl nil cardinal nil) (antisymmetric? const-decl "bool" relations nil) (cardinal_lt_le formula-decl nil cardinal nil) (cardinal_lt_strict_total_order name-judgement "(strict_total_order?[cardinal_number])" cardinal nil) (cardinal_lt_gt formula-decl nil cardinal nil) (cardinal_le_not_gt formula-decl nil cardinal nil) (dichotomous? const-decl "bool" orders nil) (total_order? const-decl "bool" orders nil) (preorder? const-decl "bool" orders nil) (partial_order? const-decl "bool" orders nil)) nil)) (cardinal_ge_total_order 0 (cardinal_ge_total_order-1 nil 3319292622 ("" (expand* "total_order?" "partial_order?" "preorder?") (("" (split) (("1" (lemma "card_ge_is_reflexive") (("1" (expand* "reflexive?" ">=") (("1" (skolem!) (("1" (inst?) nil nil)) nil)) nil)) nil) ("2" (expand* "transitive?" ">=") (("2" (skosimp) (("2" (lemma "card_ge_transitive") (("2" (inst - "rep(card_eq)(x!1)" "rep(card_eq)(y!1)" "rep(card_eq)(z!1)") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (expand "antisymmetric?") (("3" (skosimp) (("3" (use "cardinal_eq_lg") (("3" (assert) (("3" (rewrite "cardinal_le_ge") nil nil)) nil)) nil)) nil)) nil) ("4" (expand "dichotomous?") (("4" (skosimp) (("4" (use "cardinal_ge_not_lt") (("4" (assert) (("4" (rewrite "cardinal_lt_gt") (("4" (rewrite "cardinal_gt_ge") nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((>= const-decl "bool" cardinal nil) (reflexive? const-decl "bool" relations nil) (cardinal_number type-eq-decl nil cardinal nil) (card_eq const-decl "bool" card_comp_set nil) (rep const-decl "T" QuotientDefinition nil) (Quotient type-eq-decl nil QuotientDefinition nil) (EquivClass const-decl "set[T]" QuotientDefinition nil) (= const-decl "[T, T -> boolean]" equalities nil) (equivalence type-eq-decl nil relations nil) (equivalence? const-decl "bool" relations nil) (PRED type-eq-decl nil defined_types nil) (set type-eq-decl nil sets nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (card_eq_is_equivalence name-judgement "equivalence[set[T]]" cardinal nil) (T formal-type-decl nil cardinal nil) (card_ge_is_reflexive judgement-tcc nil card_single nil) (card_ge_is_reflexive name-judgement "(reflexive?[set[T]])" cardinal nil) (card_ge_is_transitive name-judgement "(transitive?[set[T]])" cardinal nil) (card_ge_is_dichotomous name-judgement "(dichotomous?[set[T]])" cardinal nil) (card_ge_transitive formula-decl nil card_comp_set_transitive nil) (transitive? const-decl "bool" relations nil) (cardinal_le_total_order name-judgement "(total_order?[cardinal_number])" cardinal nil) (cardinal_le_ge formula-decl nil cardinal nil) (cardinal_eq_lg formula-decl nil cardinal nil) (antisymmetric? const-decl "bool" relations nil) (cardinal_lt_strict_total_order name-judgement "(strict_total_order?[cardinal_number])" cardinal nil) (cardinal_gt_ge formula-decl nil cardinal nil) (cardinal_lt_gt formula-decl nil cardinal nil) (cardinal_ge_not_lt formula-decl nil cardinal nil) (dichotomous? const-decl "bool" orders nil) (total_order? const-decl "bool" orders nil) (preorder? const-decl "bool" orders nil) --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.46 Sekunden (vorverarbeitet) ¤ |
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
