| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/sets_aux/ (Beweissystem der NASA Version 6.0.9©) Datei vom 7.10.2014 mit Größe 118 kB |
|
Quelle test_rr.prfSprache: Lisp |
|||||||||||||||
|
(singleton_example (relations_equality_TCC1 0 (relations_equality_TCC1-1 nil 3571493354 ("" (subtype-tcc) nil nil) ((== const-decl "bool" singleton_example nil) (reflexive? const-decl "bool" relations nil) (symmetric? const-decl "bool" relations nil) (transitive? const-decl "bool" relations nil) (equivalence? const-decl "bool" relations nil)) nil)) (relations_equality_TCC2 0 (relations_equality_TCC2-1 nil 3571493354 ("" (subtype-tcc) nil nil) ((== const-decl "bool" singleton_example nil) (reflexive? const-decl "bool" relations nil) (symmetric? const-decl "bool" relations nil) (transitive? const-decl "bool" relations nil) (equivalence? const-decl "bool" relations nil)) nil)) (relations_equality 0 (relations_equality-1 nil 3571493357 ("" (expand "ref0") (("" (grind) (("" (apply-extensionality :hide? t) nil nil)) nil)) nil) ((boolean nonempty-type-decl nil booleans nil) (U0 type-decl nil singleton_example nil) (T0 type-decl nil singleton_example nil) (rel_extension const-decl "set[[[T, U], [T, U]]]" relation_extension nil) (rel_extension_is_equivalence application-judgement "equivalence[[T0, U0]]" singleton_example nil) (TRUE const-decl "bool" booleans nil) (e0 const-decl "[U0 -> T0]" singleton_example nil) (g0 const-decl "[T0 -> U0]" singleton_example nil) (== const-decl "bool" singleton_example nil) (== const-decl "bool" singleton_example nil) (RR const-decl "set[[T, U]]" rr_rel nil) (set type-eq-decl nil sets nil) (equivalence type-eq-decl nil relations nil) (equivalence? const-decl "bool" relations nil) (PRED type-eq-decl nil defined_types nil) (bool nonempty-type-eq-decl nil booleans nil) (ref0 const-decl "predicate[[T0, U0]]" singleton_example nil)) shostak)) (relations_equality2 0 (relations_equality2-1 nil 3572415421 ("" (apply-extensionality :hide? t) (("" (iff) (("" (prop) (("1" (grind) nil nil) ("2" (grind) nil nil)) nil)) nil)) nil) ((rel_extension const-decl "set[[[T, U], [T, U]]]" relation_extension nil) (rel_inv_extension2 const-decl "set[[[T, U], [T, U]]]" relation_inverse_extension nil) (rel_extension_is_equivalence application-judgement "equivalence[[T0, U0]]" singleton_example nil) (rel_inv_extension2_is_equivalence application-judgement "equivalence[[T0, U0]]" singleton_example nil) (bool nonempty-type-eq-decl nil booleans nil) (PRED type-eq-decl nil defined_types nil) (equivalence? const-decl "bool" relations nil) (equivalence type-eq-decl nil relations nil) (set type-eq-decl nil sets nil) (RR2 const-decl "set[[T, U]]" rr_rel nil) (== const-decl "bool" singleton_example nil) (== const-decl "bool" singleton_example nil) (g0 const-decl "[T0 -> U0]" singleton_example nil) (e0 const-decl "[U0 -> T0]" singleton_example nil) (predicate type-eq-decl nil defined_types nil) (ref0 const-decl "predicate[[T0, U0]]" singleton_example nil) (boolean nonempty-type-decl nil booleans nil) (U0 type-decl nil singleton_example nil) (T0 type-decl nil singleton_example nil)) shostak))) (finite_nats_trivial (T1_TCC1 0 (T1_TCC1-1 nil 3571586796 ("" (existence-tcc) (("" (inst 1 "1") nil nil)) nil) ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil)) nil)) (U1_TCC1 0 (U1_TCC1-1 nil 3571586796 ("" (existence-tcc) (("" (inst 1 "1") nil nil)) nil) ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil)) nil)) (g1_TCC1 0 (g1_TCC1-1 nil 3571586483 ("" (subtype-tcc) nil nil) nil nil)) (e1_TCC1 0 (e1_TCC1-1 nil 3571586483 ("" (subtype-tcc) nil nil) ((boolean nonempty-type-decl nil booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (NOT const-decl "[bool -> bool]" booleans nil) (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) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (U1 nonempty-type-eq-decl nil finite_nats_trivial nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (sgn const-decl "int" real_defs nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (div const-decl "integer" div "ints/") (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}" real_defs nil) (nzint_abs_is_pos application-judgement "{j: posint | j >= i}" real_defs nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil)) nil)) (relations_equality_TCC1 0 (relations_equality_TCC1-1 nil 3571586483 ("" (subtype-tcc) nil nil) ((T1 nonempty-type-eq-decl nil finite_nats_trivial nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (< const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (== const-decl "bool" finite_nats_trivial nil) (reflexive? const-decl "bool" relations nil) (symmetric? const-decl "bool" relations nil) (transitive? const-decl "bool" relations nil) (equivalence? const-decl "bool" relations nil)) nil)) (relations_equality_TCC2 0 (relations_equality_TCC2-1 nil 3571586483 ("" (subtype-tcc) nil nil) ((U1 nonempty-type-eq-decl nil finite_nats_trivial nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (< const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (== const-decl "bool" finite_nats_trivial nil) (reflexive? const-decl "bool" relations nil) (sgn const-decl "int" real_defs nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (div const-decl "integer" div "ints/") (symmetric? const-decl "bool" relations nil) (transitive? const-decl "bool" relations nil) (equivalence? const-decl "bool" relations nil) (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}" real_defs nil) (nzint_abs_is_pos application-judgement "{j: posint | j >= i}" real_defs nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil)) nil)) (relations_equality 0 (relations_equality-1 nil 3571586500 ("" (apply-extensionality :hide? t) (("" (iff) (("" (prop) (("1" (expand "ref1") (("1" (expand "RR") (("1" (expand "rel_extension") (("1" (expand "e1") (("1" (expand "==") (("1" (prop) (("1" (expand "g1") (("1" (replace -1 1 lr) (("1" (assert) nil nil)) nil)) nil) ("2" (replace -1 1 rl) (("2" (assert) nil nil)) nil) ("3" (expand "g1") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "ref1") (("2" (expand "RR") (("2" (expand "rel_extension") (("2" (expand "e1") (("2" (expand "g1") (("2" (expand "==") (("2" (prop) (("1" (replace -1 1 rl) (("1" (assert) nil nil)) nil) ("2" (replace -1 1 rl) (("2" (propax) nil nil)) nil) ("3" (replace -1 1 rl) (("3" (assert) nil nil)) nil) ("4" (replace -1 1 rl) (("4" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (even_times_int_is_even application-judgement "even_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (rel_extension const-decl "set[[[T, U], [T, U]]]" relation_extension nil) (div_nat formula-decl nil div "ints/") (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nil application-judgement "nat" div "ints/") (PRED type-eq-decl nil defined_types nil) (equivalence? const-decl "bool" relations nil) (equivalence type-eq-decl nil relations nil) (set type-eq-decl nil sets nil) (RR const-decl "set[[T, U]]" rr_rel nil) (== const-decl "bool" finite_nats_trivial nil) (== const-decl "bool" finite_nats_trivial nil) (g1 const-decl "[T1 -> U1]" finite_nats_trivial nil) (e1 const-decl "[U1 -> T1]" finite_nats_trivial nil) (predicate type-eq-decl nil defined_types nil) (ref1 const-decl "predicate[[T1, U1]]" finite_nats_trivial nil) (U1 nonempty-type-eq-decl nil finite_nats_trivial nil) (T1 nonempty-type-eq-decl nil finite_nats_trivial nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) shostak)) (relations_equality2 0 (relations_equality2-1 nil 3572415483 ("" (apply-extensionality :hide? t) (("" (iff) (("" (prop) (("1" (expand "ref1") (("1" (expand "RR2") (("1" (expand "rel_inv_extension2") (("1" (expand "rel_extension") (("1" (expand "e1") (("1" (prop) (("1" (expand "g1") (("1" (expand "==") (("1" (assert) nil nil)) nil)) nil) ("2" (expand "g1") (("2" (expand "==") (("2" (assert) nil nil)) nil)) nil) ("3" (expand "g1") (("3" (expand "==") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "ref1") (("2" (expand "RR2") (("2" (expand "rel_inv_extension2") (("2" (expand "rel_extension") (("2" (expand "e1") (("2" (expand "g1") (("2" (prop) (("1" (assert) (("1" (replace -1 1 rl) (("1" (replace -1 3 rl) (("1" (expand "==") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "==") (("2" (propax) nil nil)) nil) ("3" (expand "==") (("3" (replace -1 1 rl) (("3" (propax) nil nil)) nil)) nil) ("4" (replace -1 1 rl) (("4" (expand "==") (("4" (propax) nil nil)) nil)) nil) ("5" (expand "==") (("5" (propax) nil nil)) nil) ("6" (expand "==") (("6" (propax) nil nil)) nil) ("7" (expand "==") (("7" (replace -1 1 rl) (("7" (propax) nil nil)) nil)) nil) ("8" (replace -1 1 rl) (("8" (expand "==") (("8" (propax) nil nil)) nil)) nil) ("9" (expand "==") (("9" (propax) nil nil)) nil) ("10" (expand "==") (("10" (propax) nil nil)) nil) ("11" (expand "==") (("11" (replace -1 1 rl) (("11" (assert) nil nil)) nil)) nil) ("12" (expand "==") (("12" (propax) nil nil)) nil) ("13" (expand "==") (("13" (propax) nil nil)) nil) ("14" (expand "==") (("14" (propax) nil nil)) nil) ("15" (expand "==") (("15" (replace -1 1 rl) (("15" (assert) nil nil)) nil)) nil) ("16" (replace -1 1 rl) (("16" (expand "==") (("16" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((posrat_div_posrat_is_posrat application-judgement "posrat" rationals nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (even_times_int_is_even application-judgement "even_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (rel_inv_extension2 const-decl "set[[[T, U], [T, U]]]" relation_inverse_extension nil) (div_nat formula-decl nil div "ints/") (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nil application-judgement "nat" div "ints/") (rel_extension const-decl "set[[[T, U], [T, U]]]" relation_extension nil) (PRED type-eq-decl nil defined_types nil) (equivalence? const-decl "bool" relations nil) (equivalence type-eq-decl nil relations nil) (set type-eq-decl nil sets nil) (RR2 const-decl "set[[T, U]]" rr_rel nil) (== const-decl "bool" finite_nats_trivial nil) (== const-decl "bool" finite_nats_trivial nil) (g1 const-decl "[T1 -> U1]" finite_nats_trivial nil) (e1 const-decl "[U1 -> T1]" finite_nats_trivial nil) (predicate type-eq-decl nil defined_types nil) (ref1 const-decl "predicate[[T1, U1]]" finite_nats_trivial nil) (U1 nonempty-type-eq-decl nil finite_nats_trivial nil) (T1 nonempty-type-eq-decl nil finite_nats_trivial nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) shostak))) (infinite_to_infinite_trivial (relations_equality_TCC1 0 (relations_equality_TCC1-1 nil 3571501270 ("" (subtype-tcc) nil nil) ((T4 type-eq-decl nil infinite_to_infinite_trivial nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (>= const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (equivT const-decl "bool" infinite_to_infinite_trivial nil) (reflexive? const-decl "bool" relations nil) (sgn const-decl "int" real_defs nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (div const-decl "integer" div "ints/") (symmetric? const-decl "bool" relations nil) (transitive? const-decl "bool" relations nil) (equivalence? const-decl "bool" relations nil) (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}" real_defs nil) (nzint_abs_is_pos application-judgement "{j: posint | j >= i}" real_defs nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil)) nil)) (relations_equality_TCC2 0 (relations_equality_TCC2-1 nil 3571501270 ("" (subtype-tcc) nil nil) ((T4 type-eq-decl nil infinite_to_infinite_trivial nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (>= const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (equivU const-decl "bool" infinite_to_infinite_trivial nil) (reflexive? const-decl "bool" relations nil) (symmetric? const-decl "bool" relations nil) (transitive? const-decl "bool" relations nil) (equivalence? const-decl "bool" relations nil)) nil)) (relations_equality 0 (relations_equality-1 nil 3571501278 ("" (apply-extensionality :hide? t) (("" (iff) (("" (prop) (("1" (expand "ref4") (("1" (expand "RR") (("1" (expand "rel_extension") (("1" (prop) (("1" (expand "equivT") (("1" (propax) nil nil)) nil) ("2" (replace -1 1 rl) (("2" (expand "equivU") (("2" (expand "g4") (("2" (propax) nil nil)) nil)) nil)) nil) ("3" (expand "e4") (("3" (expand "equivT") (("3" (propax) nil nil)) nil)) nil) ("4" (expand "equivU") (("4" (propax) nil nil)) nil) ("5" (expand "equivT") (("5" (propax) nil nil)) nil) ("6" (expand "equivU") (("6" (expand "g4") (("6" (propax) nil nil)) nil)) nil) ("7" (expand "equivT") (("7" (propax) nil nil)) nil) ("8" (expand "equivU") (("8" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "ref4") (("2" (expand "RR") (("2" (expand "rel_extension") (("2" (expand "equivT") (("2" (expand "e4") (("2" (expand "equivU") (("2" (expand "g4") (("2" (prop) (("2" (lemma "div_multiple") (("2" (inst -1 "10" "x!1") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((div_multiple formula-decl nil div "ints/") (div_nat formula-decl nil div "ints/") (nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (even_times_int_is_even application-judgement "even_int" integers nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (int_times_even_is_even application-judgement "even_int" integers nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (nil application-judgement "nat" div "ints/") (/= const-decl "boolean" notequal nil) (nonzero_integer nonempty-type-eq-decl nil integers nil) (rel_extension const-decl "set[[[T, U], [T, U]]]" relation_extension nil) (predicate type-eq-decl nil defined_types nil) (ref4 const-decl "predicate[[T4, U4]]" infinite_to_infinite_trivial nil) (PRED type-eq-decl nil defined_types nil) (equivalence? const-decl "bool" relations nil) (equivalence type-eq-decl nil relations nil) (set type-eq-decl nil sets nil) (RR const-decl "set[[T, U]]" rr_rel nil) (equivT const-decl "bool" infinite_to_infinite_trivial nil) (equivU const-decl "bool" infinite_to_infinite_trivial nil) (g4 const-decl "[T4 -> U4]" infinite_to_infinite_trivial nil) (e4 const-decl "[U4 -> T4]" infinite_to_infinite_trivial nil) (U4 type-eq-decl nil infinite_to_infinite_trivial nil) (T4 type-eq-decl nil infinite_to_infinite_trivial nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) shostak)) (relations_equality2 0 (relations_equality2-1 nil 3572415990 ("" (apply-extensionality :hide? t) (("" (iff) (("" (prop) (("1" (expand "ref4") (("1" (replace -1 1 rl) (("1" (expand "RR2") (("1" (expand "rel_inv_extension2") (("1" (expand "rel_extension") (("1" (expand "equivT") (("1" (expand "equivU") (("1" (expand "g4") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "ref4") (("2" (expand "RR2") (("2" (expand "rel_inv_extension2") (("2" (expand "rel_extension") (("2" (expand "equivT") (("2" (expand "equivU") (("2" (expand "e4") (("2" (expand "g4") (("2" (prop) (("1" (replace -2 1 rl) (("1" (assert) nil nil)) nil) ("2" (replace -1 1 lr) (("2" (assert) nil nil)) nil) ("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((div_nat formula-decl nil div "ints/") (nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (nil application-judgement "nat" div "ints/") (rel_extension const-decl "set[[[T, U], [T, U]]]" relation_extension nil) (rel_inv_extension2 const-decl "set[[[T, U], [T, U]]]" relation_inverse_extension nil) (predicate type-eq-decl nil defined_types nil) (ref4 const-decl "predicate[[T4, U4]]" infinite_to_infinite_trivial nil) (PRED type-eq-decl nil defined_types nil) (equivalence? const-decl "bool" relations nil) (equivalence type-eq-decl nil relations nil) (set type-eq-decl nil sets nil) (RR2 const-decl "set[[T, U]]" rr_rel nil) (equivT const-decl "bool" infinite_to_infinite_trivial nil) (equivU const-decl "bool" infinite_to_infinite_trivial nil) (g4 const-decl "[T4 -> U4]" infinite_to_infinite_trivial nil) (e4 const-decl "[U4 -> T4]" infinite_to_infinite_trivial nil) (U4 type-eq-decl nil infinite_to_infinite_trivial nil) (T4 type-eq-decl nil infinite_to_infinite_trivial nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) shostak))) (finite_to_infinite (relations_equality_TCC1 0 (relations_equality_TCC1-1 nil 3571502050 ("" (subtype-tcc) nil nil) ((equivT const-decl "bool" finite_to_infinite nil) (reflexive? const-decl "bool" relations nil) (symmetric? const-decl "bool" relations nil) (transitive? const-decl "bool" relations nil) (equivalence? const-decl "bool" relations nil)) nil)) (relations_equality_TCC2 0 (relations_equality_TCC2-1 nil 3571502050 ("" (subtype-tcc) nil nil) ((U6 type-eq-decl nil finite_to_infinite nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (>= const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (equivU const-decl "bool" finite_to_infinite nil) (reflexive? const-decl "bool" relations nil) (even? const-decl "bool" integers nil) (symmetric? const-decl "bool" relations nil) (transitive? const-decl "bool" relations nil) (equivalence? const-decl "bool" relations nil)) nil)) (relations_equality 0 (relations_equality-1 nil 3571502071 ("" (apply-extensionality :hide? t) (("" (iff) (("" (prop) (("1" (expand "RR") (("1" (expand "rel_extension") (("1" (expand "ref6") (("1" (prop) (("1" (expand "equivT") (("1" (propax) nil nil)) nil) ("2" (expand "equivU") (("2" (expand "g6") (("2" (smash) (("2" (expand "even?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("3" (expand "equivT") (("3" (propax) nil nil)) nil) ("4" (expand "equivU") (("4" (propax) nil nil)) nil) ("5" (expand "equivT") (("5" (propax) nil nil)) nil) ("6" (expand "g6") (("6" (expand "e6") (("6" (replace -1 2 rl) (("6" (expand "equivT") (("6" (propax) nil nil)) nil)) nil)) nil)) nil) ("7" (expand "equivT") (("7" (propax) nil nil)) nil) ("8" (expand "equivU") (("8" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "ref6") (("2" (expand "RR") (("2" (expand "rel_extension") (("2" (prop) (("1" (expand "g6") (("1" (expand "equivU") (("1" (expand "equivT") (("1" (expand "e6") (("1" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "equivU") (("2" (expand "e6") (("2" (expand "equivT") (("2" (replace -1 1 lr) (("2" (propax) nil nil)) nil)) nil)) nil)) nil) ("3" (expand "equivT") (("3" (expand "equivU") (("3" (replace -1 1 rl) (("3" (expand "g6") (("3" (smash) (("3" (expand "even?") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((even? const-decl "bool" integers nil) (rel_extension const-decl "set[[[T, U], [T, U]]]" relation_extension nil) (T6 type-eq-decl nil finite_to_infinite nil) (predicate type-eq-decl nil defined_types nil) (ref6 const-decl "predicate[[T6, U6]]" finite_to_infinite nil) (PRED type-eq-decl nil defined_types nil) (equivalence? const-decl "bool" relations nil) (equivalence type-eq-decl nil relations nil) (set type-eq-decl nil sets nil) (RR const-decl "set[[T, U]]" rr_rel nil) (equivT const-decl "bool" finite_to_infinite nil) (equivU const-decl "bool" finite_to_infinite nil) (g6 const-decl "[T6 -> U6]" finite_to_infinite nil) (e6 const-decl "[U6 -> T6]" finite_to_infinite nil) (U6 type-eq-decl nil finite_to_infinite nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil)) shostak)) (relations_equality2 0 (relations_equality2-1 nil 3572416182 ("" (apply-extensionality :hide? t) (("" (iff) (("" (prop) (("1" (expand "ref6") (("1" (replace -1 1 lr) (("1" (expand "RR2") (("1" (expand "rel_inv_extension2") (("1" (expand "rel_extension") (("1" (expand "equivT") (("1" (expand "equivU") (("1" (expand "e6") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "RR2") (("2" (prop) (("1" (expand "rel_inv_extension2") (("1" (expand "ref6") (("1" (expand "rel_extension") (("1" (expand "equivT") (("1" (expand "e6") (("1" (expand "equivU") (("1" (prop) (("1" (replace -1 1 lr) (("1" (assert) (("1" (expand "g6") (("1" (smash) (("1" (expand "even?") (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "rel_inv_extension2") (("2" (expand "ref6") (("2" (expand "rel_extension") (("2" (expand "equivT") (("2" (expand "e6") (("2" (expand "equivU") (("2" (expand "g6") (("2" (expand "even?") (("2" (assert) (("2" (smash) (("1" (inst 1 "0") (("1" (assert) nil nil)) nil) ("2" (inst 2 "0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "rel_inv_extension2") (("3" (expand "rel_extension") (("3" (expand "ref6") (("3" (expand "equivT") (("3" (expand "equivU") (("3" (expand "e6") (("3" (expand "g6") (("3" (expand "even?") (("3" (replace -1 1 lr) (("3" (smash) (("3" (inst 2 "0") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (even_times_int_is_even application-judgement "even_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (even? const-decl "bool" integers nil) (rel_extension const-decl "set[[[T, U], [T, U]]]" relation_extension nil) (rel_inv_extension2 const-decl "set[[[T, U], [T, U]]]" relation_inverse_extension nil) (T6 type-eq-decl nil finite_to_infinite nil) (predicate type-eq-decl nil defined_types nil) (ref6 const-decl "predicate[[T6, U6]]" finite_to_infinite nil) (PRED type-eq-decl nil defined_types nil) (equivalence? const-decl "bool" relations nil) (equivalence type-eq-decl nil relations nil) (set type-eq-decl nil sets nil) (RR2 const-decl "set[[T, U]]" rr_rel nil) (equivT const-decl "bool" finite_to_infinite nil) (equivU const-decl "bool" finite_to_infinite nil) (g6 const-decl "[T6 -> U6]" finite_to_infinite nil) (e6 const-decl "[U6 -> T6]" finite_to_infinite nil) (U6 type-eq-decl nil finite_to_infinite nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil)) shostak))) (infinite_to_finite_finite_equival_finite_equival_classes (relations_equality_TCC1 0 (relations_equality_TCC1-1 nil 3571502963 ("" (subtype-tcc) nil nil) ((T7 type-eq-decl nil infinite_to_finite_finite_equival_finite_equival_classes nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (>= const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (equivT const-decl "bool" infinite_to_finite_finite_equival_finite_equival_classes nil) (reflexive? const-decl "bool" relations nil) (even? const-decl "bool" integers nil) (symmetric? const-decl "bool" relations nil) (transitive? const-decl "bool" relations nil) (equivalence? const-decl "bool" relations nil)) nil)) (relations_equality_TCC2 0 (relations_equality_TCC2-1 nil 3571502963 ("" (subtype-tcc) nil nil) ((equivU const-decl "bool" infinite_to_finite_finite_equival_finite_equival_classes nil) (reflexive? const-decl "bool" relations nil) (symmetric? const-decl "bool" relations nil) (transitive? const-decl "bool" relations nil) (equivalence? const-decl "bool" relations nil)) nil)) (relations_equality 0 (relations_equality-1 nil 3571502988 ("" (grind) (("" (expand "ref7") (("" (expand "RR") (("" (grind) (("" (apply-extensionality :hide? t) (("" (lift-if) (("" (smash) (("" (inst 1 "0") (("" (assert) (("" (inst 2 "0") (("" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((ref7 const-decl "predicate[[T7, U7]]" infinite_to_finite_finite_equival_finite_equival_classes nil) (even? const-decl "bool" integers nil) (g7 const-decl "[T7 -> U7]" infinite_to_finite_finite_equival_finite_equival_classes nil) (e7 const-decl "[U7 -> T7]" infinite_to_finite_finite_equival_finite_equival_classes nil) (equivT const-decl "bool" infinite_to_finite_finite_equival_finite_equival_classes nil) (equivU const-decl "bool" infinite_to_finite_finite_equival_finite_equival_classes nil) (U7 type-decl nil infinite_to_finite_finite_equival_finite_equival_classes nil) (T7 type-eq-decl nil infinite_to_finite_finite_equival_finite_equival_classes nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil) (rel_extension const-decl "set[[[T, U], [T, U]]]" relation_extension nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (even_times_int_is_even application-judgement "even_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (IF const-decl "[boolean, T, T -> T]" if_def nil) (= const-decl "[T, T -> boolean]" equalities nil) (numfield nonempty-type-eq-decl nil number_fields nil) (* const-decl "[numfield, numfield -> numfield]" number_fields nil) (zero? adt-recognizer-decl "[U7 -> boolean]" infinite_to_finite_finite_equival_finite_equival_classes nil) (0 adt-constructor-decl "(zero?)" infinite_to_finite_finite_equival_finite_equival_classes nil) (one? adt-recognizer-decl "[U7 -> boolean]" infinite_to_finite_finite_equival_finite_equival_classes nil) (1 adt-constructor-decl "(one?)" infinite_to_finite_finite_equival_finite_equival_classes nil) (OR const-decl "[bool, bool -> bool]" booleans nil) (AND const-decl "[bool, bool -> bool]" booleans nil) (FALSE const-decl "bool" booleans nil) (RR const-decl "set[[T, U]]" rr_rel nil)) shostak)) (relations_equality2 0 (relations_equality2-1 nil 3572416486 ("" (apply-extensionality :hide? t) (("" (iff) (("" (prop) (("1" (expand "RR2") (("1" (expand "rel_inv_extension2") (("1" (expand "rel_extension") (("1" (expand "equivT") (("1" (expand "g7") (("1" (expand "equivU") (("1" (expand "e7") (("1" (expand "even?") (("1" (smash) (("1" (inst 1 "0") (("1" (assert) (("1" (expand "ref7") (("1" (expand "even?") (("1" (smash) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "ref7") (("2" (expand "even?") (("2" (smash) (("2" (inst 1 "0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (expand "ref7") (("3" (expand "even?") (("3" (smash) nil nil)) nil)) nil) ("4" (expand "ref7") (("4" (expand "even?") (("4" (smash) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "ref7") (("2" (expand "even?") (("2" (expand "RR2") (("2" (expand "rel_inv_extension2") (("2" (expand "rel_extension") (("2" (expand "equivT") (("2" (expand "equivU") (("2" (expand "e7") (("2" (expand "g7") (("2" (expand "even?") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((rel_extension const-decl "set[[[T, U], [T, U]]]" relation_extension nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (even? const-decl "bool" integers nil) (rel_inv_extension2 const-decl "set[[[T, U], [T, U]]]" relation_inverse_extension nil) (predicate type-eq-decl nil defined_types nil) (ref7 const-decl "predicate[[T7, U7]]" infinite_to_finite_finite_equival_finite_equival_classes nil) (PRED type-eq-decl nil defined_types nil) (equivalence? const-decl "bool" relations nil) (equivalence type-eq-decl nil relations nil) (set type-eq-decl nil sets nil) (RR2 const-decl "set[[T, U]]" rr_rel nil) (equivT const-decl "bool" infinite_to_finite_finite_equival_finite_equival_classes nil) (equivU const-decl "bool" infinite_to_finite_finite_equival_finite_equival_classes nil) (g7 const-decl "[T7 -> U7]" infinite_to_finite_finite_equival_finite_equival_classes nil) (e7 const-decl "[U7 -> T7]" infinite_to_finite_finite_equival_finite_equival_classes nil) (U7 type-decl nil infinite_to_finite_finite_equival_finite_equival_classes nil) (T7 type-eq-decl nil infinite_to_finite_finite_equival_finite_equival_classes nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) shostak))) (infinite_to_finite_infinite_equival_finite_equival_classes (U8_TCC1 0 (U8_TCC1-1 nil 3571503678 ("" (existence-tcc) (("" (inst 1 "1") nil nil)) nil) ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil)) nil)) (relations_equality_TCC1 0 (relations_equality_TCC1-1 nil 3571503678 ("" (subtype-tcc) nil nil) ((real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (T8 nonempty-type-eq-decl nil infinite_to_finite_infinite_equival_finite_equival_classes nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (>= const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (equivT const-decl "bool" infinite_to_finite_infinite_equival_finite_equival_classes nil) (reflexive? const-decl "bool" relations nil) (odd? const-decl "bool" integers nil) (even? const-decl "bool" integers nil) (symmetric? const-decl "bool" relations nil) (transitive? const-decl "bool" relations nil) (equivalence? const-decl "bool" relations nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (even_times_int_is_even application-judgement "even_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil)) nil)) (relations_equality_TCC2 0 (relations_equality_TCC2-1 nil 3571503678 ("" (subtype-tcc) nil nil) ((U8 nonempty-type-eq-decl nil infinite_to_finite_infinite_equival_finite_equival_classes nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (< const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (odd? const-decl "bool" integers nil) (even? const-decl "bool" integers nil) (equivU const-decl "bool" infinite_to_finite_infinite_equival_finite_equival_classes nil) (reflexive? const-decl "bool" relations nil) (symmetric? const-decl "bool" relations nil) (transitive? const-decl "bool" relations nil) (equivalence? const-decl "bool" relations nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (even_times_int_is_even application-judgement "even_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil)) nil)) (relations_equality 0 (relations_equality-1 nil 3571503732 ("" (apply-extensionality :hide? t) (("" (iff) (("" (prop) (("1" (expand "RR") (("1" (expand "ref8") (("1" (prop) (("1" (expand "rel_extension") (("1" (prop) (("1" (expand "equivT") (("1" (propax) nil nil)) nil) ("2" (expand "e8") (("2" (expand "equivU") (("2" (expand "g8") (("2" (expand "equivT") (("2" (expand "odd?") (("2" (expand "even?") (("2" (smash) (("2" (replace -3 1 lr) (("2" (inst 1 "0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "equivT") (("3" (propax) nil nil)) nil) ("4" (expand "equivU") (("4" (expand "equivT") (("4" (replace -2 3 lr) (("4" (expand "e8") (("4" (replace -2 1 lr) (("4" (expand "even?") (("4" (expand "odd?") (("4" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("5" (expand "equivT") (("5" (propax) nil nil)) nil) ("6" (replace -2 1 lr) (("6" (hide 3) (("6" (expand "equivU") (("6" (expand "e8") (("6" (replace -2 2 lr) (("6" (expand "even?") (("6" (expand "equivT") (("6" (expand "g8") (("6" (expand "odd?") (("6" (expand "even?") (("6" (smash) (("6" (inst 3 "0") (("6" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("7" (expand "equivT") (("7" (propax) nil nil)) nil) ("8" (expand "equivU") (("8" (replace -2 1 lr) (("8" (replace -2 3 lr) (("8" (expand "even?") (("8" (expand "g8") (("8" (expand "odd?") (("8" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "rel_extension") (("2" (prop) (("1" (expand "equivT") (("1" (propax) nil nil)) nil) ("2" (replace -1 1 lr) (("2" (replace -1 3 lr) (("2" (grind) nil nil)) nil)) nil) ("3" (expand "equivT") (("3" (propax) nil nil)) nil) ("4" (expand "equivU") (("4" (replace -1 1 lr) (("4" (replace -1 3 lr) (("4" (expand "equivT") (("4" (expand "odd?") (("4" (expand "g8") (("4" (expand "even?") (("4" (smash) (("4" (expand "e8") (("4" (expand "even?") (("4" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("5" (expand "equivT") (("5" (propax) nil nil)) nil) ("6" (replace -1 1 lr) (("6" (hide 3) (("6" (grind) nil nil)) nil)) nil) ("7" (grind) nil nil) ("8" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "ref8") (("2" (expand "RR") (("2" (expand "rel_extension") (("2" (prop) (("1" (expand "g8") (("1" (expand "equivT") (("1" (expand "odd?") (("1" (expand "equivU") (("1" (expand "odd?") (("1" (grind) nil nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "equivT") (("2" (expand "equivU") (("2" (expand "odd?") (("2" (expand "e8") (("2" (grind) nil nil)) nil)) nil)) nil)) nil) ("3" (grind) nil nil) ("4" (grind) nil nil) ("5" (expand "equivT") (("5" (expand "even?") (("5" (skolem!) (("5" (replace -1 -2 lr) (("5" (expand "g8") (("5" (expand "equivU") (("5" (expand "even?") (("5" (skolem!) (("5" (case "j!2=0") (("1" (replace -1 -3 lr) (("1" (assert) nil nil)) nil) ("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("6" (expand "equivT") (("6" (expand "equivU") (("6" (expand "even?") (("6" (expand "g8") (("6" (expand "odd?") (("6" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((= const-decl "[T, T -> boolean]" equalities nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (even? const-decl "bool" integers nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (odd? const-decl "bool" integers nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil) (rel_extension const-decl "set[[[T, U], [T, U]]]" relation_extension nil) (predicate type-eq-decl nil defined_types nil) (ref8 const-decl "predicate[[T8, U8]]" infinite_to_finite_infinite_equival_finite_equival_classes nil) (PRED type-eq-decl nil defined_types nil) (equivalence? const-decl "bool" relations nil) (equivalence type-eq-decl nil relations nil) (set type-eq-decl nil sets nil) (RR const-decl "set[[T, U]]" rr_rel nil) (equivT const-decl "bool" infinite_to_finite_infinite_equival_finite_equival_classes nil) (equivU const-decl "bool" infinite_to_finite_infinite_equival_finite_equival_classes nil) (g8 const-decl "[T8 -> U8]" infinite_to_finite_infinite_equival_finite_equival_classes nil) (e8 const-decl "[U8 -> T8]" infinite_to_finite_infinite_equival_finite_equival_classes nil) (U8 nonempty-type-eq-decl nil infinite_to_finite_infinite_equival_finite_equival_classes nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (T8 nonempty-type-eq-decl nil infinite_to_finite_infinite_equival_finite_equival_classes nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) shostak)) (relations_equality2 0 (relations_equality2-1 nil 3572417269 ("" (apply-extensionality :hide? t) (("" (iff) (("" (prop) (("1" (expand "RR2") (("1" (prop) (("1" (expand "ref8") (("1" (expand "rel_inv_extension2") (("1" (expand "rel_extension") (("1" (expand "equivT") (("1" (expand "equivU") (("1" (expand "odd?") (("1" (expand "even?") (("1" (expand "e8") (("1" (expand "g8") (("1" (smash) (("1" (inst 1 "0") (("1" (inst 2 "0") (("1" (expand "even?") (("1" (smash) nil nil)) nil)) nil)) nil) ("2" (grind) nil nil) ("3" (grind) nil nil) ("4" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "RR2") (("2" (prop) (("1" (expand "rel_inv_extension2") (("1" (expand "rel_extension") (("1" (expand "ref8") (("1" (expand "equivT") (("1" (expand "equivU") (("1" (expand "e8") (("1" (expand "g8") (("1" (expand "even?") (("1" (expand "odd?") (("1" (smash) (("1" (inst 1 "0") (("1" (lift-if) (("1" (split) (("1" (flatten) (("1" (inst?) (("1" (assert) nil nil)) nil)) nil) ("2" (prop) (("2" (inst?) (("2" (inst?) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (inst 1 "0") (("2" (smash) (("2" (inst 1 "0") (("2" (inst 3 "0") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "ref8") (("2" (expand "rel_inv_extension2") (("2" (expand "rel_extension") (("2" (expand "equivT") (("2" (expand "equivU") (("2" (expand "e8") (("2" (expand "g8") (("2" (expand "odd?") (("2" (expand "even?") (("2" (smash) (("1" (grind) nil nil) ("2" (inst 1 "0") (("2" (inst 2 "0") (("2" (lift-if) (("2" (split) (("1" (prop) (("1" (assert) nil nil)) nil) ("2" (prop) nil nil)) nil)) nil)) nil)) nil) ("3" (inst 1 "0") (("3" (inst 2 "0") (("3" (inst 3 "0") (("3" (smash) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "rel_inv_extension2") (("3" (expand "ref8") (("3" (expand "rel_extension") (("3" (expand "equivT") (("3" (expand "e8") (("3" (expand "equivU") (("3" (expand "g8") (("3" (expand "odd?") (("3" (expand "even?") (("3" (prop) (("1" (grind) nil nil) ("2" (grind) nil nil) ("3" (grind) nil nil) ("4" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nnint_plus_posint_is_posint application-judgement "posint" integers nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (rel_extension const-decl "set[[[T, U], [T, U]]]" relation_extension nil) (even? const-decl "bool" integers nil) (odd? const-decl "bool" integers nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (rel_inv_extension2 const-decl "set[[[T, U], [T, U]]]" relation_inverse_extension nil) (predicate type-eq-decl nil defined_types nil) (ref8 const-decl "predicate[[T8, U8]]" infinite_to_finite_infinite_equival_finite_equival_classes nil) (PRED type-eq-decl nil defined_types nil) (equivalence? const-decl "bool" relations nil) (equivalence type-eq-decl nil relations nil) (set type-eq-decl nil sets nil) (RR2 const-decl "set[[T, U]]" rr_rel nil) (equivT const-decl "bool" infinite_to_finite_infinite_equival_finite_equival_classes nil) (equivU const-decl "bool" infinite_to_finite_infinite_equival_finite_equival_classes nil) (g8 const-decl "[T8 -> U8]" infinite_to_finite_infinite_equival_finite_equival_classes nil) (e8 const-decl "[U8 -> T8]" infinite_to_finite_infinite_equival_finite_equival_classes nil) (U8 nonempty-type-eq-decl nil infinite_to_finite_infinite_equival_finite_equival_classes nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (T8 nonempty-type-eq-decl nil infinite_to_finite_infinite_equival_finite_equival_classes nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) shostak))) (infinite_to_infinite_infinite_equival_infinite_equival_classes (e9_TCC1 0 (e9_TCC1-1 nil 3571587486 ("" (subtype-tcc) nil nil) nil nil)) (relations_equality_TCC1 0 (relations_equality_TCC1-1 nil 3571587486 ("" (subtype-tcc) nil nil) ((T9 type-eq-decl nil infinite_to_infinite_infinite_equival_infinite_equival_classes nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (>= const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (equivT const-decl "bool" infinite_to_infinite_infinite_equival_infinite_equival_classes nil) (reflexive? const-decl "bool" relations nil) (symmetric? const-decl "bool" relations nil) (transitive? const-decl "bool" relations nil) (equivalence? const-decl "bool" relations nil)) nil)) (relations_equality_TCC2 0 (relations_equality_TCC2-1 nil 3571587486 ("" (subtype-tcc) nil nil) ((U9 type-eq-decl nil infinite_to_infinite_infinite_equival_infinite_equival_classes nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (> const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (equivU const-decl "bool" infinite_to_infinite_infinite_equival_infinite_equival_classes nil) (reflexive? const-decl "bool" relations nil) (symmetric? const-decl "bool" relations nil) (transitive? const-decl "bool" relations nil) (equivalence? const-decl "bool" relations nil)) nil)) (relations_equality 0 (relations_equality-1 nil 3571587491 ("" (apply-extensionality :hide? t) (("" (iff) (("" (prop) (("1" (expand "ref9") (("1" (expand "RR") (("1" (expand "rel_extension") (("1" (expand "e9") (("1" (expand "equivT") (("1" (expand "equivU") (("1" (expand "g9") (("1" (replace -1 1 rl) (("1" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "ref9") (("2" (expand "RR") (("2" (expand "rel_extension") (("2" (expand "e9") (("2" (expand "equivT") (("2" (expand "equivU") (("2" (expand "g9") (("2" (prop) (("2" (replace -1 1 rl) (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((int_minus_int_is_int application-judgement "int" integers nil) (int_plus_int_is_int application-judgement "int" integers nil) (rel_extension const-decl "set[[[T, U], [T, U]]]" relation_extension nil) (predicate type-eq-decl nil defined_types nil) (ref9 const-decl "predicate[[T9, U9]]" infinite_to_infinite_infinite_equival_infinite_equival_classes nil) (PRED type-eq-decl nil defined_types nil) (equivalence? const-decl "bool" relations nil) (equivalence type-eq-decl nil relations nil) (set type-eq-decl nil sets nil) (RR const-decl "set[[T, U]]" rr_rel nil) (equivT const-decl "bool" infinite_to_infinite_infinite_equival_infinite_equival_classes nil) (equivU const-decl "bool" infinite_to_infinite_infinite_equival_infinite_equival_classes nil) (g9 const-decl "[T9 -> U9]" infinite_to_infinite_infinite_equival_infinite_equival_classes nil) (e9 const-decl "[U9 -> T9]" infinite_to_infinite_infinite_equival_infinite_equival_classes nil) (U9 type-eq-decl nil infinite_to_infinite_infinite_equival_infinite_equival_classes nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (T9 type-eq-decl nil infinite_to_infinite_infinite_equival_infinite_equival_classes nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) shostak)) (relations_equality2 0 (relations_equality2-1 nil 3572418128 ("" (apply-extensionality :hide? t) (("" (iff) (("" (prop) (("1" (grind) nil nil) ("2" (grind) nil nil)) nil)) nil)) nil) ((rel_extension const-decl "set[[[T, U], [T, U]]]" relation_extension nil) (rel_inv_extension2 const-decl "set[[[T, U], [T, U]]]" relation_inverse_extension nil) (rel_extension_is_equivalence application-judgement "equivalence[[T9, U9]]" infinite_to_infinite_infinite_equival_infinite_equival_classes nil) (int_plus_int_is_int application-judgement "int" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (rel_inv_extension2_is_equivalence application-judgement "equivalence[[T9, U9]]" infinite_to_infinite_infinite_equival_infinite_equival_classes nil) (int_minus_int_is_int application-judgement "int" integers nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (predicate type-eq-decl nil defined_types nil) (ref9 const-decl "predicate[[T9, U9]]" infinite_to_infinite_infinite_equival_infinite_equival_classes nil) (PRED type-eq-decl nil defined_types nil) (equivalence? const-decl "bool" relations nil) (equivalence type-eq-decl nil relations nil) (set type-eq-decl nil sets nil) (RR2 const-decl "set[[T, U]]" rr_rel nil) (equivT const-decl "bool" infinite_to_infinite_infinite_equival_infinite_equival_classes nil) (equivU const-decl "bool" infinite_to_infinite_infinite_equival_infinite_equival_classes nil) (g9 const-decl "[T9 -> U9]" infinite_to_infinite_infinite_equival_infinite_equival_classes nil) (e9 const-decl "[U9 -> T9]" infinite_to_infinite_infinite_equival_infinite_equival_classes nil) (U9 type-eq-decl nil infinite_to_infinite_infinite_equival_infinite_equival_classes nil) (> const-decl "bool" reals nil) (nonneg_int nonempty-type-eq-decl nil integers nil) (T9 type-eq-decl nil infinite_to_infinite_infinite_equival_infinite_equival_classes nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) shostak))) (infinite_to_infinite_infinite_equival_finite_equival_classes (relations_equality_TCC1 0 (relations_equality_TCC1-1 nil 3571588100 ("" (subtype-tcc) nil nil) ((T10 nonempty-type-eq-decl nil infinite_to_infinite_infinite_equival_finite_equival_classes nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (>= const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (equivT const-decl "bool" infinite_to_infinite_infinite_equival_finite_equival_classes nil) (reflexive? const-decl "bool" relations nil) (symmetric? const-decl "bool" relations nil) (transitive? const-decl "bool" relations nil) (equivalence? const-decl "bool" relations nil)) nil)) (relations_equality_TCC2 0 (relations_equality_TCC2-1 nil 3571588100 ("" (subtype-tcc) nil nil) ((T10 nonempty-type-eq-decl nil infinite_to_infinite_infinite_equival_finite_equival_classes nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (>= const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (equivU const-decl "bool" infinite_to_infinite_infinite_equival_finite_equival_classes nil) (reflexive? const-decl "bool" relations nil) (sgn const-decl "int" real_defs nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (div const-decl "integer" div "ints/") (symmetric? const-decl "bool" relations nil) (transitive? const-decl "bool" relations nil) (equivalence? const-decl "bool" relations nil) (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}" real_defs nil) (nzint_abs_is_pos application-judgement "{j: posint | j >= i}" real_defs nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil)) nil)) (relations_equality 0 (relations_equality-1 nil 3571588128 ("" (apply-extensionality :hide? t) (("" (iff) (("" (prop) (("1" (expand "RR") (("1" (expand "rel_extension") (("1" (prop) (("1" (expand "ref10") (("1" (expand "e10") (("1" (expand "equivT") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (expand "ref10") (("2" (replace -1 1 lr) (("2" (expand "g10") (("2" (expand "equivU") (("2" (assert) nil nil)) nil)) nil)) nil)) nil) ("3" (expand "equivT") (("3" (propax) nil nil)) nil) ("4" (expand "equivU") (("4" (propax) nil nil)) nil) ("5" (expand "equivT") (("5" (propax) nil nil)) nil) ("6" (expand "ref10") (("6" (grind) nil nil)) nil) ("7" (expand "equivU") (("7" (propax) nil nil)) nil) ("8" (expand "equivU") (("8" (propax) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "ref10") (("2" (expand "RR") (("2" (expand "rel_extension") (("2" (expand "equivU") (("2" (expand "g10") (("2" (expand "equivT") (("2" (expand "e10") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nil application-judgement "nat" div "ints/") (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (even_times_int_is_even application-judgement "even_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (div_nat formula-decl nil div "ints/") (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}" real_defs nil) (nzint_abs_is_pos application-judgement "{j: posint | j >= i}" real_defs nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (minus_even_is_even application-judgement "even_int" integers nil) (minus_int_is_int application-judgement "int" integers nil) (div const-decl "integer" div "ints/") (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (sgn const-decl "int" real_defs nil) (rel_extension const-decl "set[[[T, U], [T, U]]]" relation_extension nil) (predicate type-eq-decl nil defined_types nil) (ref10 const-decl "predicate[[T10, U10]]" infinite_to_infinite_infinite_equival_finite_equival_classes nil) (PRED type-eq-decl nil defined_types nil) (equivalence? const-decl "bool" relations nil) (equivalence type-eq-decl nil relations nil) (set type-eq-decl nil sets nil) (RR const-decl "set[[T, U]]" rr_rel nil) (equivT const-decl "bool" infinite_to_infinite_infinite_equival_finite_equival_classes nil) (equivU const-decl "bool" infinite_to_infinite_infinite_equival_finite_equival_classes nil) (g10 const-decl "[T10 -> U10]" infinite_to_infinite_infinite_equival_finite_equival_classes nil) (e10 const-decl "[U10 -> T10]" infinite_to_infinite_infinite_equival_finite_equival_classes nil) (U10 nonempty-type-eq-decl nil infinite_to_infinite_infinite_equival_finite_equival_classes nil) (T10 nonempty-type-eq-decl nil infinite_to_infinite_infinite_equival_finite_equival_classes nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) shostak)) (relations_equality2 0 (relations_equality2-1 nil 3572418172 ("" (apply-extensionality :hide? t) (("" (iff) (("" (prop) (("1" (grind) nil nil) ("2" (expand "RR2") (("2" (prop) (("1" (expand "ref10") (("1" (expand "rel_inv_extension2") (("1" (expand "rel_extension") (("1" (expand "equivT") (("1" (prop) (("1" (expand "equivU") (("1" (expand "g10") (("1" (expand "e10") (("1" (replace -1 1 lr) (("1" (replace -2 1 rl) (("1" (replace -1 1 lr) (("1" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "rel_inv_extension2") (("2" (expand "ref10") (("2" (expand "rel_extension") (("2" (prop) (("2" (expand "equivU") (("2" (expand "equivT") (("2" (expand "e10") (("2" (expand "g10") (("2" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "ref10") (("3" (expand "rel_inv_extension2") (("3" (expand "rel_extension") (("3" (prop) (("3" (expand "equivT") (("3" (expand "g10") (("3" (expand "e10") (("3" (expand "equivU") (("3" (replace -1 1 lr) (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((div_nat formula-decl nil div "ints/") (sgn const-decl "int" real_defs nil) (abs const-decl "{n: nonneg_real | n >= m AND n >= -m}" real_defs nil) (div const-decl "integer" div "ints/") (rel_extension const-decl "set[[[T, U], [T, U]]]" relation_extension nil) (rel_inv_extension2 const-decl "set[[[T, U], [T, U]]]" relation_inverse_extension nil) (rel_extension_is_equivalence application-judgement "equivalence[[T10, U10]]" infinite_to_infinite_infinite_equival_finite_equival_classes nil) (minus_even_is_even application-judgement "even_int" integers nil) (rel_inv_extension2_is_equivalence application-judgement "equivalence[[T10, U10]]" infinite_to_infinite_infinite_equival_finite_equival_classes nil) (even_times_int_is_even application-judgement "even_int" integers nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (real_lt_is_strict_total_order name-judgement "(strict_total_order?[real])" real_props nil) (minus_int_is_int application-judgement "int" integers nil) (nnrat_div_posrat_is_nnrat application-judgement "nonneg_rat" rationals nil) (nonneg_floor_is_nat application-judgement "nat" floor_ceil nil) (real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (minus_odd_is_odd application-judgement "odd_int" integers nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (nzint_abs_is_pos application-judgement "{j: posint | j >= i}" real_defs nil) (int_abs_is_nonneg application-judgement "{j: nonneg_int | j >= i}" real_defs nil) (nil application-judgement "nat" div "ints/") (predicate type-eq-decl nil defined_types nil) (ref10 const-decl "predicate[[T10, U10]]" infinite_to_infinite_infinite_equival_finite_equival_classes nil) (PRED type-eq-decl nil defined_types nil) (equivalence? const-decl "bool" relations nil) (equivalence type-eq-decl nil relations nil) (set type-eq-decl nil sets nil) (RR2 const-decl "set[[T, U]]" rr_rel nil) (equivT const-decl "bool" infinite_to_infinite_infinite_equival_finite_equival_classes nil) (equivU const-decl "bool" infinite_to_infinite_infinite_equival_finite_equival_classes nil) (g10 const-decl "[T10 -> U10]" infinite_to_infinite_infinite_equival_finite_equival_classes nil) (e10 const-decl "[U10 -> T10]" infinite_to_infinite_infinite_equival_finite_equival_classes nil) (U10 nonempty-type-eq-decl nil infinite_to_infinite_infinite_equival_finite_equival_classes nil) (T10 nonempty-type-eq-decl nil infinite_to_infinite_infinite_equival_finite_equival_classes nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) shostak))) (finite_to_infinite_finite_equival_infinite_equival_classes (T11_TCC1 0 (T11_TCC1-1 nil 3571656715 ("" (existence-tcc) (("" (inst 1 "1") nil nil)) nil) ((number nonempty-type-decl nil numbers nil) (boolean nonempty-type-decl nil booleans nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number_field nonempty-type-from-decl nil number_fields nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (real nonempty-type-from-decl nil reals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (rational nonempty-type-from-decl nil rationals nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (int nonempty-type-eq-decl nil integers nil) (bool nonempty-type-eq-decl nil booleans nil) (>= const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (< const-decl "bool" reals nil)) nil)) (relations_equality_TCC1 0 (relations_equality_TCC1-1 nil 3571656715 ("" (subtype-tcc) nil nil) ((T11 nonempty-type-eq-decl nil finite_to_infinite_finite_equival_infinite_equival_classes nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (< const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (odd? const-decl "bool" integers nil) (even? const-decl "bool" integers nil) (equivT const-decl "bool" finite_to_infinite_finite_equival_infinite_equival_classes nil) (reflexive? const-decl "bool" relations nil) (symmetric? const-decl "bool" relations nil) (transitive? const-decl "bool" relations nil) (equivalence? const-decl "bool" relations nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (even_times_int_is_even application-judgement "even_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil)) nil)) (relations_equality_TCC2 0 (relations_equality_TCC2-1 nil 3571656715 ("" (subtype-tcc) nil nil) ((real_ge_is_total_order name-judgement "(total_order?[real])" real_props nil) (U11 nonempty-type-eq-decl nil finite_to_infinite_finite_equival_infinite_equival_classes nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (>= const-decl "bool" reals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (number nonempty-type-decl nil numbers nil) (NOT const-decl "[bool -> bool]" booleans nil) (bool nonempty-type-eq-decl nil booleans nil) (boolean nonempty-type-decl nil booleans nil) (equivU const-decl "bool" finite_to_infinite_finite_equival_infinite_equival_classes nil) (reflexive? const-decl "bool" relations nil) (odd? const-decl "bool" integers nil) (even? const-decl "bool" integers nil) (symmetric? const-decl "bool" relations nil) (transitive? const-decl "bool" relations nil) (equivalence? const-decl "bool" relations nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (even_times_int_is_even application-judgement "even_int" integers nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (mult_divides2 application-judgement "(divides(m))" divides nil)) nil)) (relations_equality 0 (relations_equality-1 nil 3571656768 ("" (apply-extensionality :hide? t) (("" (iff) (("" (prop) (("1" (expand "ref11") (("1" (expand "RR") (("1" (expand "rel_extension") (("1" (prop) (("1" (smash) (("1" (expand "e11") (("1" (expand "equivT") (("1" (propax) nil nil)) nil)) nil)) nil) ("2" (expand "even?") (("2" (replace -2 1 lr) (("2" (expand "g11") (("2" (expand "equivU") (("2" (prop) (("2" (expand "even?") (("2" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "equivT") (("3" (expand "odd?") (("3" (expand "e11") (("3" (smash) (("3" (expand "even?") (("3" (propax) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (expand "equivU") (("4" (propax) nil nil)) nil) ("5" (expand "equivT") (("5" (grind) nil nil)) nil) ("6" (grind) nil nil) ("7" (expand "equivT") (("7" (grind) nil nil)) nil) ("8" (grind) nil nil) ("9" (grind) nil nil) ("10" (grind) nil nil) ("11" (grind) nil nil) ("12" (grind) nil nil) ("13" (grind) nil nil) ("14" (grind) nil nil) ("15" (grind) nil nil) ("16" (grind) nil nil)) nil)) nil)) nil)) nil) ("2" (expand "ref11") (("2" (expand "RR") (("2" (expand "rel_extension") (("2" (expand "equivT") (("2" (expand "odd?") (("2" (expand "even?") (("2" (expand "e11") (("2" (expand "equivU") (("2" (expand "odd?") (("2" (expand "g11") (("2" (expand "even?") (("2" (smash) (("1" (inst?) (("1" (smash) (("1" (skolem!) (("1" (smash) nil nil)) nil)) nil)) nil) ("2" (inst 1 "0") (("2" (assert) (("2" (inst 2 "0") (("2" (assert) nil nil)) nil)) nil)) nil) ("3" (inst 2 "0") (("3" (assert) (("3" (inst 1 "0") (("3" (smash) (("3" (inst 1 "0") (("3" (assert) nil nil)) nil)) nil)) nil)) nil)) nil) ("4" (inst 1 "0") (("4" (smash) nil nil)) nil) ("5" (inst 1 "0") (("5" (smash) (("5" (inst 2 "0") (("5" (smash) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (rel_extension const-decl "set[[[T, U], [T, U]]]" relation_extension nil) (nnint_plus_posint_is_posint application-judgement "posint" integers nil) (odd? const-decl "bool" integers nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil) (even? const-decl "bool" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (predicate type-eq-decl nil defined_types nil) (ref11 const-decl "predicate[[T11, U11]]" finite_to_infinite_finite_equival_infinite_equival_classes nil) (PRED type-eq-decl nil defined_types nil) (equivalence? const-decl "bool" relations nil) (equivalence type-eq-decl nil relations nil) (set type-eq-decl nil sets nil) (RR const-decl "set[[T, U]]" rr_rel nil) (equivT const-decl "bool" finite_to_infinite_finite_equival_infinite_equival_classes nil) (equivU const-decl "bool" finite_to_infinite_finite_equival_infinite_equival_classes nil) (g11 const-decl "[T11 -> U11]" finite_to_infinite_finite_equival_infinite_equival_classes nil) (e11 const-decl "[U11 -> T11]" finite_to_infinite_finite_equival_infinite_equival_classes nil) (U11 nonempty-type-eq-decl nil finite_to_infinite_finite_equival_infinite_equival_classes nil) (T11 nonempty-type-eq-decl nil finite_to_infinite_finite_equival_infinite_equival_classes nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) shostak)) (relations_equality2 0 (relations_equality2-1 nil 3572418398 ("" (apply-extensionality :hide? t) (("" (iff) (("" (prop) (("1" (expand "RR2") (("1" (prop) (("1" (expand "ref11") (("1" (expand "rel_inv_extension2") (("1" (expand "rel_extension") (("1" (expand "equivT") (("1" (expand "equivU") (("1" (expand "e11") (("1" (expand "g11") (("1" (expand "even?") (("1" (smash) (("1" (expand "odd?") (("1" (propax) nil nil)) nil) ("2" (expand "odd?") (("2" (propax) nil nil)) nil) ("3" (expand "odd?") (("3" (propax) nil nil)) nil) ("4" (expand "odd?") (("4" (grind) nil nil)) nil) ("5" (expand "odd?") (("5" (propax) nil nil)) nil) ("6" (expand "odd?") (("6" (propax) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "ref11") (("2" (expand "RR2") (("2" (prop) (("1" (expand "rel_inv_extension2") (("1" (expand "rel_extension") (("1" (prop) (("1" (expand "equivT") (("1" (expand "equivU") (("1" (expand "g11") (("1" (expand "e11") (("1" (expand "even?") (("1" (smash) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("2" (expand "rel_inv_extension2") (("2" (expand "rel_extension") (("2" (prop) (("2" (expand "equivU") (("2" (expand "equivT") (("2" (expand "g11") (("2" (expand "e11") (("2" (expand "even?") (("2" (smash) (("1" (expand "odd?") (("1" (propax) nil nil)) nil) ("2" (expand "odd?") (("2" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("3" (expand "rel_inv_extension2") (("3" (expand "rel_extension") (("3" (prop) (("3" (expand "equivT") (("3" (expand "equivU") (("3" (expand "e11") (("3" (expand "g11") (("3" (expand "even?") (("3" (smash) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("4" (grind) nil nil) ("5" (expand "rel_inv_extension2") (("5" (expand "rel_extension") (("5" (prop) (("5" (expand "equivT") (("5" (expand "equivU") (("5" (expand "e11") (("5" (expand "g11") (("5" (expand "even?") (("5" (smash) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ("6" (expand "rel_inv_extension2") (("6" (expand "rel_extension") (("6" (prop) (("6" (expand "equivU") (("6" (expand "equivT") (("6" (expand "e11") (("6" (expand "g11") (("6" (expand "even?") (("6" (smash) (("1" (expand "odd?") (("1" (propax) nil nil)) nil) ("2" (expand "odd?") (("2" (grind) nil nil)) nil) ("3" (grind) nil nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil)) nil) ((nnint_plus_posint_is_posint application-judgement "posint" integers nil) (even_plus_odd_is_odd application-judgement "odd_int" integers nil) (nnint_times_nnint_is_nnint application-judgement "nonneg_int" integers nil) (int_times_even_is_even application-judgement "even_int" integers nil) (rel_inv_extension2_is_equivalence application-judgement "equivalence[[T11, U11]]" finite_to_infinite_finite_equival_infinite_equival_classes nil) (rel_extension_is_equivalence application-judgement "equivalence[[T11, U11]]" finite_to_infinite_finite_equival_infinite_equival_classes nil) (rel_extension const-decl "set[[[T, U], [T, U]]]" relation_extension nil) (odd_plus_even_is_odd application-judgement "odd_int" integers nil) (odd_plus_odd_is_even application-judgement "even_int" integers nil) (odd? const-decl "bool" integers nil) (mult_divides2 application-judgement "(divides(m))" divides nil) (mult_divides1 application-judgement "(divides(n))" divides nil) (even_times_int_is_even application-judgement "even_int" integers nil) (even? const-decl "bool" integers nil) (posint_plus_nnint_is_posint application-judgement "posint" integers nil) (rel_inv_extension2 const-decl "set[[[T, U], [T, U]]]" relation_inverse_extension nil) (predicate type-eq-decl nil defined_types nil) (ref11 const-decl "predicate[[T11, U11]]" finite_to_infinite_finite_equival_infinite_equival_classes nil) (PRED type-eq-decl nil defined_types nil) (equivalence? const-decl "bool" relations nil) (equivalence type-eq-decl nil relations nil) (set type-eq-decl nil sets nil) (RR2 const-decl "set[[T, U]]" rr_rel nil) (equivT const-decl "bool" finite_to_infinite_finite_equival_infinite_equival_classes nil) (equivU const-decl "bool" finite_to_infinite_finite_equival_infinite_equival_classes nil) (g11 const-decl "[T11 -> U11]" finite_to_infinite_finite_equival_infinite_equival_classes nil) (e11 const-decl "[U11 -> T11]" finite_to_infinite_finite_equival_infinite_equival_classes nil) (U11 nonempty-type-eq-decl nil finite_to_infinite_finite_equival_infinite_equival_classes nil) (T11 nonempty-type-eq-decl nil finite_to_infinite_finite_equival_infinite_equival_classes nil) (< const-decl "bool" reals nil) (nat nonempty-type-eq-decl nil naturalnumbers nil) (>= const-decl "bool" reals nil) (bool nonempty-type-eq-decl nil booleans nil) (int nonempty-type-eq-decl nil integers nil) (integer_pred const-decl "[rational -> boolean]" integers nil) (rational nonempty-type-from-decl nil rationals nil) (rational_pred const-decl "[real -> boolean]" rationals nil) (real nonempty-type-from-decl nil reals nil) (real_pred const-decl "[number_field -> boolean]" reals nil) (number_field nonempty-type-from-decl nil number_fields nil) (number_field_pred const-decl "[number -> boolean]" number_fields nil) (boolean nonempty-type-decl nil booleans nil) (number nonempty-type-decl nil numbers nil)) shostak))) (simplest_examples)
¤ Dauer der Verarbeitung: 0.62 Sekunden (vorverarbeitet am 2026-04-26) ¤*© Formatika GbR, Deutschland |
|
||||||||||||||
2026-05-26