|
(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.103 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.
|
