| products/sources/formale sprachen/PVS/sets_aux/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: test_rr.prf Sprache: LispOriginal von: PVS© |
|
||||||
|
(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) --> -------------------- --> maximum size reached --> -------------------- ¤ Dauer der Verarbeitung: 0.71 Sekunden (vorverarbeitet) ¤ |
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
