|
|
|
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
vectors_3D_rew.prf
Sprache: Lisp
Untersuchungsergebnis.summary Download desMT940 {MT940[457] Hlasm[1381] Haskell[1763]}zum Wurzelverzeichnis wechseln
***
*** top (17:29:56 11/7/2014)
*** Generated by proveit - ProofLite-6.0.9 (3/14/14)
***
Proof summary for theory top
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory fun_below_props
cartesian_bijection...................proved - complete [shostak](-.37 s)
empty_domain1.........................proved - complete [shostak](0.02 s)
empty_domain2.........................proved - complete [shostak](0.01 s)
empty_range...........................proved - complete [shostak](0.02 s)
funset_bijection_TCC1.................proved - complete [shostak](0.01 s)
funset_bijection......................proved - complete [shostak](0.80 s)
Theory totals: 6 formulas, 6 attempted, 6 succeeded (0.49 s)
Proof summary for theory power_sets
B_TCC1................................proved - complete [shostak](0.03 s)
card_B................................proved - complete [shostak](0.19 s)
powerset_bijection....................proved - complete [shostak](0.84 s)
finite_powerset_bijection.............proved - incomplete [shostak](0.06 s)
card_powerset.........................proved - incomplete [shostak](0.13 s)
elem_finite_powerset..................proved - complete [shostak](0.01 s)
finite_subset_of_powerset.............proved - complete [shostak](0.03 s)
Theory totals: 7 formulas, 7 attempted, 7 succeeded (1.28 s)
Proof summary for theory set_of_functions
empty_finite_domain1..................proved - complete [shostak](0.03 s)
empty_finite_domain2..................proved - complete [shostak](0.04 s)
empty_finite_range....................proved - complete [shostak](0.04 s)
finite_funset_bijection1..............proved - incomplete [shostak](0.34 s)
finite_funset_bijection2_TCC1.........proved - complete [shostak](0.02 s)
finite_funset_bijection2..............proved - incomplete [shostak](0.04 s)
finite_funset.........................proved - incomplete [shostak](0.04 s)
funset_TCC1...........................proved - incomplete [shostak](0.01 s)
card_funset_TCC1......................proved - complete [shostak](0.04 s)
card_funset...........................proved - incomplete [shostak](0.13 s)
Theory totals: 10 formulas, 10 attempted, 10 succeeded (0.73 s)
Proof summary for theory bits
bounding_bits_has_least...............proved - complete [shostak](0.35 s)
bit_decoding_TCC1.....................proved - complete [shostak](0.31 s)
bit_decoding_TCC2.....................proved - complete [shostak](0.24 s)
bit_decoding_TCC3.....................proved - complete [shostak](0.33 s)
bit_decoding_TCC4.....................proved - complete [shostak](0.24 s)
bit_decoding_has_greatest.............proved - incomplete [shostak](0.24 s)
bit_decoding_max1_TCC1................proved - incomplete [shostak](0.02 s)
bit_decoding_max1.....................proved - incomplete [shostak](1.03 s)
bit_decoding_max2_TCC1................proved - complete [shostak](0.01 s)
bit_decoding_max2.....................proved - incomplete [shostak](1.10 s)
bit_decoding_max3.....................proved - incomplete [shostak](0.56 s)
bit_encoding_TCC1.....................proved - incomplete [shostak](0.21 s)
bit_encoding_TCC2.....................proved - incomplete [shostak](0.25 s)
bit_encoding_member1..................proved - incomplete [shostak](0.32 s)
bit_encoding_member2..................proved - incomplete [shostak](0.87 s)
bit_encoding_member3_TCC1.............proved - incomplete [shostak](0.37 s)
bit_encoding_member3..................proved - incomplete [shostak](0.63 s)
decoding_encoding_max_TCC1............proved - incomplete [shostak](0.37 s)
decoding_encoding_max.................proved - incomplete [shostak](0.52 s)
decoding_encoding_empty...............proved - incomplete [shostak](0.27 s)
decoding_encoding_remove..............proved - incomplete [shostak](0.74 s)
encoding_decoding.....................proved - incomplete [shostak](1.22 s)
decoding_encoding.....................proved - incomplete [shostak](1.46 s)
encoding_bijection....................proved - incomplete [shostak](0.37 s)
decoding_bijection....................proved - incomplete [shostak](0.37 s)
encoding_decoding_inverse.............proved - incomplete [shostak](0.27 s)
decoding_encoding_inverse.............proved - incomplete [shostak](0.27 s)
Theory totals: 27 formulas, 27 attempted, 27 succeeded (12.93 s)
Proof summary for theory card_comp
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory card_comp_props
card_lt_surj..........................proved - complete [shostak](0.72 s)
card_ge_surj..........................proved - complete [shostak](1.30 s)
card_lt_le............................proved - complete [shostak](0.01 s)
card_gt_ge............................proved - complete [shostak](0.01 s)
card_lt_gt............................proved - complete [shostak](0.01 s)
card_le_ge............................proved - complete [shostak](0.01 s)
card_gt_lt............................proved - complete [shostak](0.01 s)
card_ge_le............................proved - complete [shostak](0.00 s)
card_lt_ge............................proved - complete [shostak](0.01 s)
card_le_gt............................proved - complete [shostak](0.01 s)
card_eq_le_ge.........................proved - complete [shostak](0.91 s)
card_le_lt_eq.........................proved - complete [shostak](0.22 s)
card_ge_gt_eq.........................proved - complete [shostak](0.02 s)
card_lt_neq_ngt.......................proved - complete [shostak](0.01 s)
card_gt_neq_nlt.......................proved - complete [shostak](0.12 s)
card_lt_anticommutative...............proved - complete [shostak](0.01 s)
card_le_antisymmetric.................proved - complete [shostak](0.01 s)
card_eq_symmetric.....................proved - complete [shostak](0.82 s)
card_ge_antisymmetric.................proved - complete [shostak](0.01 s)
card_gt_anticommutative...............proved - complete [shostak](0.01 s)
card_lt_trichotomous..................proved - complete [shostak](0.01 s)
card_le_dichotomous...................proved - complete [shostak](0.01 s)
card_ge_dichotomous...................proved - complete [shostak](0.01 s)
card_gt_trichotomous..................proved - complete [shostak](0.01 s)
Theory totals: 24 formulas, 24 attempted, 24 succeeded (4.27 s)
Proof summary for theory card_comp_set
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory card_comp_set_props
card_lt_surj..........................proved - complete [shostak](0.73 s)
card_ge_surj..........................proved - complete [shostak](1.32 s)
card_lt_le............................proved - complete [shostak](0.02 s)
card_gt_ge............................proved - complete [shostak](0.02 s)
card_lt_gt............................proved - complete [shostak](0.01 s)
card_le_ge............................proved - complete [shostak](0.02 s)
card_gt_lt............................proved - complete [shostak](0.01 s)
card_ge_le............................proved - complete [shostak](0.02 s)
card_lt_ge............................proved - complete [shostak](0.02 s)
card_le_gt............................proved - complete [shostak](0.03 s)
card_eq_le_ge.........................proved - complete [shostak](0.43 s)
card_le_lt_eq.........................proved - complete [shostak](0.03 s)
card_ge_gt_eq.........................proved - complete [shostak](0.04 s)
card_lt_neq_ngt.......................proved - complete [shostak](0.02 s)
card_gt_neq_nlt.......................proved - complete [shostak](0.03 s)
card_lt_anticommutative...............proved - complete [shostak](0.02 s)
card_le_antisymmetric.................proved - complete [shostak](0.02 s)
card_eq_symmetric.....................proved - complete [shostak](0.83 s)
card_ge_antisymmetric.................proved - complete [shostak](0.03 s)
card_gt_anticommutative...............proved - complete [shostak](0.02 s)
card_lt_trichotomous..................proved - complete [shostak](0.02 s)
card_le_dichotomous...................proved - complete [shostak](0.02 s)
card_ge_dichotomous...................proved - complete [shostak](0.31 s)
card_gt_trichotomous..................proved - complete [shostak](0.02 s)
Theory totals: 24 formulas, 24 attempted, 24 succeeded (4.05 s)
Proof summary for theory card_comp_set_transitive
card_lt_transitive....................proved - complete [shostak](0.32 s)
card_lt_le_transitive.................proved - complete [shostak](0.32 s)
card_lt_eq_transitive.................proved - complete [shostak](0.32 s)
card_le_lt_transitive.................proved - complete [shostak](0.32 s)
card_eq_lt_transitive.................proved - complete [shostak](0.33 s)
card_le_transitive....................proved - complete [shostak](0.32 s)
card_le_eq_transitive.................proved - complete [shostak](0.32 s)
card_eq_le_transitive.................proved - complete [shostak](0.33 s)
card_eq_transitive....................proved - complete [shostak](0.32 s)
card_eq_ge_transitive.................proved - complete [shostak](0.73 s)
card_ge_eq_transitive.................proved - complete [shostak](0.73 s)
card_ge_transitive....................proved - complete [shostak](0.32 s)
card_eq_gt_transitive.................proved - complete [shostak](0.73 s)
card_ge_gt_transitive.................proved - complete [shostak](0.32 s)
card_gt_eq_transitive.................proved - complete [shostak](0.73 s)
card_gt_ge_transitive.................proved - complete [shostak](0.32 s)
card_gt_transitive....................proved - complete [shostak](0.43 s)
Theory totals: 17 formulas, 17 attempted, 17 succeeded (7.22 s)
Proof summary for theory card_comp_transitive
card_lt_transitive....................proved - complete [shostak](0.31 s)
card_lt_le_transitive.................proved - complete [shostak](0.30 s)
card_lt_eq_transitive.................proved - complete [shostak](0.31 s)
card_le_lt_transitive.................proved - complete [shostak](0.31 s)
card_eq_lt_transitive.................proved - complete [shostak](0.30 s)
card_le_transitive....................proved - complete [shostak](0.31 s)
card_le_eq_transitive.................proved - complete [shostak](0.31 s)
card_eq_le_transitive.................proved - complete [shostak](0.31 s)
card_eq_transitive....................proved - complete [shostak](0.30 s)
card_eq_ge_transitive.................proved - complete [shostak](0.71 s)
card_ge_eq_transitive.................proved - complete [shostak](0.71 s)
card_ge_transitive....................proved - complete [shostak](0.31 s)
card_eq_gt_transitive.................proved - complete [shostak](0.71 s)
card_ge_gt_transitive.................proved - complete [shostak](0.30 s)
card_gt_eq_transitive.................proved - complete [shostak](0.71 s)
card_gt_ge_transitive.................proved - complete [shostak](0.30 s)
card_gt_transitive....................proved - complete [shostak](0.31 s)
Theory totals: 17 formulas, 17 attempted, 17 succeeded (6.83 s)
Proof summary for theory card_finite
card_less_than........................proved - complete [shostak](1.92 s)
card_less_than_equal..................proved - complete [shostak](1.93 s)
card_equal............................proved - complete [shostak](0.63 s)
card_greater_than_equal...............proved - complete [shostak](0.32 s)
card_greater_than.....................proved - complete [shostak](0.33 s)
Theory totals: 5 formulas, 5 attempted, 5 succeeded (5.13 s)
Proof summary for theory card_power
card_power............................proved - complete [shostak](0.02 s)
Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.02 s)
Proof summary for theory card_power_set
card_power............................proved - complete [shostak](0.07 s)
Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.07 s)
Proof summary for theory card_sets_lemmas
empty_card_le.........................proved - complete [shostak](0.24 s)
nonempty_card_lt......................proved - complete [shostak](1.58 s)
full_card_le..........................proved - complete [shostak](0.24 s)
add_card_le...........................proved - complete [shostak](0.25 s)
remove_card_ge........................proved - complete [shostak](0.26 s)
subset_card_le........................proved - complete [shostak](0.56 s)
strict_subset_card_lt.................proved - complete [shostak](0.02 s)
union_card_le1........................proved - complete [shostak](0.24 s)
union_card_le2........................proved - complete [shostak](0.25 s)
intersection_card_le1.................proved - complete [shostak](0.26 s)
intersection_card_le2.................proved - complete [shostak](0.26 s)
difference_card_le....................proved - complete [shostak](0.25 s)
Theory totals: 12 formulas, 12 attempted, 12 succeeded (4.41 s)
Proof summary for theory card_single
card_lt_is_irreflexive................proved - complete [shostak](0.02 s)
card_le_is_reflexive..................proved - complete [shostak](0.03 s)
card_eq_is_reflexive..................proved - complete [shostak](0.02 s)
card_ge_is_reflexive..................proved - complete [shostak](0.03 s)
card_gt_is_irreflexive................proved - complete [shostak](0.03 s)
card_lt_is_antisymmetric..............proved - complete [shostak](0.01 s)
card_eq_is_symmetric..................proved - complete [shostak](0.02 s)
card_gt_is_antisymmetric..............proved - complete [shostak](0.02 s)
card_lt_is_transitive.................proved - complete [shostak](0.02 s)
card_le_is_transitive.................proved - complete [shostak](0.03 s)
card_eq_is_transitive.................proved - complete [shostak](0.03 s)
card_ge_is_transitive.................proved - complete [shostak](0.03 s)
card_gt_is_transitive.................proved - complete [shostak](0.03 s)
card_le_is_dichotomous................proved - complete [shostak](0.03 s)
card_ge_is_dichotomous................proved - complete [shostak](0.04 s)
card_eq_is_equivalence................proved - complete [shostak](0.04 s)
Theory totals: 16 formulas, 16 attempted, 16 succeeded (0.44 s)
Proof summary for theory card_function
infinite_bijection....................proved - complete [shostak](0.05 s)
finite_bijection......................proved - complete [shostak](0.05 s)
infinite_injection....................proved - complete [shostak](0.04 s)
finite_injection......................proved - complete [shostak](0.01 s)
infinite_surjection...................proved - complete [shostak](0.05 s)
finite_surjection.....................proved - complete [shostak](0.01 s)
Theory totals: 6 formulas, 6 attempted, 6 succeeded (0.22 s)
Proof summary for theory cardinal
cardinal_member.......................proved - complete [shostak](0.02 s)
cardinal_closed.......................proved - complete [shostak](0.05 s)
cardinal_empty........................proved - complete [shostak](0.79 s)
cardinal_finite.......................proved - complete [shostak](0.11 s)
cardinal_finite_card_TCC1.............proved - complete [shostak](0.02 s)
cardinal_finite_card..................proved - complete [shostak](0.04 s)
cardinal_equality.....................proved - complete [shostak](0.08 s)
cardinal_lt...........................proved - complete [shostak](0.08 s)
cardinal_le...........................proved - complete [shostak](0.08 s)
cardinal_eq...........................proved - complete [shostak](0.05 s)
cardinal_ge...........................proved - complete [shostak](0.09 s)
cardinal_gt...........................proved - complete [shostak](0.09 s)
cardinal_card_lt......................proved - complete [shostak](0.32 s)
cardinal_card_le......................proved - complete [shostak](0.32 s)
cardinal_card_eq......................proved - complete [shostak](0.32 s)
cardinal_card_ge......................proved - complete [shostak](0.32 s)
cardinal_card_gt......................proved - complete [shostak](0.32 s)
cardinal_lt_gt........................proved - complete [shostak](0.03 s)
cardinal_le_ge........................proved - complete [shostak](0.02 s)
cardinal_lt_le........................proved - complete [shostak](0.05 s)
cardinal_le_lt........................proved - complete [shostak](0.03 s)
cardinal_eq_lg........................proved - complete [shostak](0.04 s)
cardinal_ge_gt........................proved - complete [shostak](0.03 s)
cardinal_gt_ge........................proved - complete [shostak](0.04 s)
cardinal_lt_not_ge....................proved - complete [shostak](0.02 s)
cardinal_le_not_gt....................proved - complete [shostak](0.02 s)
cardinal_eq_not_lg....................proved - complete [shostak](0.04 s)
cardinal_ge_not_lt....................proved - complete [shostak](0.03 s)
cardinal_gt_not_le....................proved - complete [shostak](0.03 s)
cardinal_lt_strict_total_order........proved - complete [shostak](0.06 s)
cardinal_le_total_order...............proved - complete [shostak](0.08 s)
cardinal_ge_total_order...............proved - complete [shostak](0.08 s)
cardinal_gt_strict_total_order........proved - complete [shostak](0.06 s)
cardinal_lt_le_transitive.............proved - complete [shostak](0.03 s)
cardinal_le_lt_transitive.............proved - complete [shostak](0.03 s)
cardinal_ge_gt_transitive.............proved - complete [shostak](0.03 s)
cardinal_gt_ge_transitive.............proved - complete [shostak](0.03 s)
cardinal_empty_least..................proved - complete [shostak](0.05 s)
cardinal_full_greatest................proved - complete [shostak](0.05 s)
Theory totals: 39 formulas, 39 attempted, 39 succeeded (3.99 s)
Proof summary for theory countability
countable_set_TCC1....................proved - complete [shostak](0.08 s)
countably_infinite_countable..........proved - complete [shostak](0.80 s)
countably_infinite_subset.............proved - complete [shostak](0.60 s)
countable_subset......................proved - complete [shostak](0.69 s)
countable_type_is_countably_infinite...proved - complete [shostak](0.22 s)
countable_full........................proved - complete [shostak](1.27 s)
countably_infinite_full...............proved - complete [shostak](4.55 s)
uncountable_full......................proved - complete [shostak](0.06 s)
countable_type_set....................proved - complete [shostak](0.38 s)
countably_infinite_type_set...........proved - complete [shostak](0.53 s)
uncountably_infinite_type_set.........proved - complete [shostak](0.07 s)
countable_complement..................proved - complete [shostak](0.06 s)
countably_infinite_complement.........proved - complete [shostak](0.06 s)
Theory totals: 13 formulas, 13 attempted, 13 succeeded (9.35 s)
Proof summary for theory countable_image
countable_image.......................proved - complete [shostak](0.08 s)
Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.08 s)
Proof summary for theory infinite_image
infinite_image........................proved - complete [shostak](0.07 s)
infinite_injective_image..............proved - complete [shostak](0.05 s)
Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.12 s)
Proof summary for theory countable_props
infinite_countably_infinite...........proved - complete [shostak](0.03 s)
countably_infinite_add................proved - complete [shostak](0.19 s)
countable_add.........................proved - complete [shostak](0.13 s)
countably_infinite_remove.............proved - complete [shostak](0.35 s)
countable_remove......................proved - complete [shostak](0.12 s)
countably_infinite_rest...............proved - complete [shostak](0.08 s)
countable_rest........................proved - complete [shostak](0.08 s)
countable_intersection1...............proved - complete [shostak](0.42 s)
countable_intersection2...............proved - complete [shostak](0.08 s)
countably_infinite_difference.........proved - complete [shostak](0.21 s)
countable_difference..................proved - complete [shostak](0.74 s)
finite_countable......................proved - complete [shostak](0.71 s)
infinite_uncountable..................proved - complete [shostak](0.26 s)
countably_infinite_subset_exists......proved - complete [shostak](0.16 s)
countably_infinite_strict_subset_exists...proved - complete [shostak](0.42 s)
countable_card........................proved - complete [shostak](1.37 s)
countably_infinite_union1.............proved - complete [shostak](0.63 s)
countably_infinite_union2.............proved - complete [shostak](0.13 s)
countable_union.......................proved - complete [shostak](0.15 s)
countably_infinite_def................proved - complete [shostak](0.12 s)
countable_emptyset....................proved - complete [shostak](0.12 s)
countable_singleton...................proved - complete [shostak](0.13 s)
card_le_finite........................proved - complete [shostak](0.09 s)
card_ge_infinite......................proved - complete [shostak](0.09 s)
card_eq_countably_infinite............proved - complete [shostak](0.50 s)
card_le_countable.....................proved - complete [shostak](0.50 s)
card_ge_uncountable...................proved - complete [shostak](0.49 s)
countably_infinite_subset_union.......proved - complete [shostak](1.94 s)
countable_finite_subset_union.........proved - complete [shostak](0.79 s)
infinite_countable_union..............proved - complete [shostak](0.23 s)
infinite_countable_difference.........proved - complete [shostak](0.10 s)
Theory totals: 31 formulas, 31 attempted, 31 succeeded (11.34 s)
Proof summary for theory infinite_nat_def
infinite_def..........................proved - complete [shostak](0.38 s)
infinite_def2.........................proved - complete [shostak](0.05 s)
Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.43 s)
Proof summary for theory countable_set
int_to_nat_TCC1.......................proved - complete [shostak](0.05 s)
int_to_nat_TCC2.......................proved - complete [shostak](0.03 s)
nat_to_int_TCC1.......................proved - complete [shostak](0.05 s)
nat_to_int_TCC2.......................proved - complete [shostak](0.10 s)
int_to_nat_bijective..................proved - complete [shostak](0.16 s)
nat_to_int_bijective..................proved - complete [shostak](0.18 s)
countable_family_nat..................proved - incomplete [shostak](0.01 s)
intset_to_natset_bijective............proved - complete [shostak](0.38 s)
countable_family_int..................proved - incomplete [shostak](0.02 s)
tuple_to_natset_TCC1..................proved - complete [shostak](0.14 s)
countable_nat_tuple...................proved - incomplete [shostak](0.11 s)
tuple_to_intset_TCC1..................proved - complete [shostak](0.12 s)
countable_int_tuple...................proved - incomplete [shostak](0.11 s)
countable_rat.........................proved - incomplete [shostak](0.12 s)
Theory totals: 14 formulas, 14 attempted, 14 succeeded (1.57 s)
Proof summary for theory countable_setofsets
countable_union1......................proved - incomplete [shostak](0.80 s)
countable_union2......................proved - complete [shostak](0.74 s)
countable_intersection................proved - complete [shostak](1.08 s)
countable_finite_subsets..............proved - incomplete [shostak](0.18 s)
countably_infinite_finite_subsets.....proved - incomplete [shostak](0.86 s)
Theory totals: 5 formulas, 5 attempted, 5 succeeded (3.65 s)
Proof summary for theory countable_types
nat_rational..........................proved - incomplete [shostak](0.17 s)
nat_nonzero_rational..................proved - incomplete [shostak](0.07 s)
nat_nonneg_rat........................proved - incomplete [shostak](0.29 s)
nat_nonpos_rat........................proved - incomplete [shostak](0.09 s)
nat_negrat............................proved - incomplete [shostak](0.08 s)
nat_posrat............................proved - incomplete [shostak](0.12 s)
nat_integer...........................proved - complete [shostak](0.01 s)
nat_nonzero_integer...................proved - complete [shostak](0.23 s)
nat_upfrom............................proved - complete [shostak](0.08 s)
nat_above.............................proved - complete [shostak](0.10 s)
nat_nonpos_int........................proved - complete [shostak](0.07 s)
nat_negint............................proved - complete [shostak](0.07 s)
nat_posint............................proved - complete [shostak](0.07 s)
nat_even_int..........................proved - complete [shostak](0.17 s)
nat_odd_int...........................proved - complete [shostak](0.21 s)
Theory totals: 15 formulas, 15 attempted, 15 succeeded (1.82 s)
Proof summary for theory infinite_card
finite_card_eq........................proved - complete [shostak](0.82 s)
infinite_card_eq......................proved - complete [shostak](0.01 s)
infinite_card_le......................proved - complete [shostak](0.42 s)
infinite_card_ge......................proved - complete [shostak](0.41 s)
finite_card_le........................proved - complete [shostak](0.41 s)
finite_card_ge........................proved - complete [shostak](0.42 s)
Theory totals: 6 formulas, 6 attempted, 6 succeeded (2.49 s)
Proof summary for theory infinite_sets
infinite_add_card.....................proved - complete [shostak](0.05 s)
infinite_remove_card..................proved - complete [shostak](0.06 s)
finite_infinite_lt....................proved - complete [shostak](0.69 s)
Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.79 s)
Proof summary for theory sets_lemmas_extra
disjoint_commutative..................proved - complete [shostak](0.01 s)
Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.01 s)
Proof summary for theory indexed_sets_aux
disjoint_indexed_set_TCC1.............proved - complete [shostak](0.02 s)
IComplement_IComplement...............proved - complete [shostak](0.02 s)
IDemorgan1............................proved - complete [shostak](0.07 s)
IDemorgan2............................proved - complete [shostak](0.08 s)
Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.18 s)
Proof summary for theory countable_indexed_sets
Union_IUnion..........................proved - complete [shostak](0.15 s)
Intersection_IIntersection............proved - complete [shostak](0.08 s)
Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.23 s)
Proof summary for theory nat_indexed_sets
IUnion_0_def..........................proved - complete [shostak](0.03 s)
IUnion_n_def..........................proved - complete [shostak](-.70 s)
increasing_indexed_TCC1...............proved - complete [shostak](0.04 s)
increasing_IUnion.....................proved - complete [shostak](0.17 s)
decreasing_IIntersection..............proved - complete [shostak](0.17 s)
disjoint_IUnion.......................proved - complete [shostak](0.52 s)
Theory totals: 6 formulas, 6 attempted, 6 succeeded (0.23 s)
Proof summary for theory inverse_image_Union
inverse_image_Union...................proved - complete [shostak](0.05 s)
Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.05 s)
Proof summary for theory countability_aux
countable_emptyset....................proved - complete [shostak](0.02 s)
countable_singleton...................proved - complete [shostak](0.03 s)
countable_add.........................proved - complete [shostak](0.11 s)
countable_remove......................proved - complete [shostak](0.06 s)
countable_intersection1...............proved - complete [shostak](0.02 s)
countable_intersection2...............proved - complete [shostak](0.02 s)
countable_difference..................proved - complete [shostak](0.03 s)
Theory totals: 7 formulas, 7 attempted, 7 succeeded (0.30 s)
Proof summary for theory cantor_bernstein_schroeder
Afun_TCC1.............................proved - complete [shostak](0.02 s)
Afun_TCC2.............................proved - complete [shostak](0.01 s)
Afundef...............................proved - complete [shostak](0.03 s)
Afundef2..............................proved - complete [shostak](0.01 s)
Afuncomp..............................proved - complete [shostak](0.13 s)
Afuneq_TCC1...........................proved - complete [shostak](0.05 s)
Afuneq_TCC2...........................proved - complete [shostak](0.04 s)
Afuneq................................proved - complete [shostak](0.23 s)
Bfun_TCC1.............................proved - complete [shostak](0.02 s)
Bfun_TCC2.............................proved - complete [shostak](0.02 s)
Bfun_TCC3.............................proved - complete [shostak](0.01 s)
Bfundef...............................proved - complete [shostak](0.01 s)
Bfundef2..............................proved - complete [shostak](0.02 s)
Bfuneq_TCC1...........................proved - complete [shostak](0.04 s)
Bfuneq_TCC2...........................proved - complete [shostak](0.05 s)
Bfuneq................................proved - complete [shostak](0.23 s)
ABfun.................................proved - complete [shostak](0.09 s)
BAfun.................................proved - complete [shostak](0.08 s)
ABfuneq_TCC1..........................proved - complete [shostak](0.04 s)
ABfuneq_TCC2..........................proved - complete [shostak](0.05 s)
ABfuneq...............................proved - complete [shostak](0.23 s)
ABrel_Arel_equiv......................proved - complete [shostak](0.24 s)
ABrel_Brel_equiv......................proved - complete [shostak](0.33 s)
Brel_Arel.............................proved - complete [shostak](0.14 s)
Arel_Brel.............................proved - complete [shostak](0.12 s)
ABrel_Brel............................proved - complete [shostak](0.11 s)
Afununique............................proved - complete [shostak](0.31 s)
af_fun_TCC1...........................proved - complete [shostak](0.03 s)
ag_fun_TCC1...........................proved - complete [shostak](0.06 s)
aginj.................................proved - complete [shostak](0.28 s)
Arel_union............................proved - complete [shostak](0.02 s)
Arel_disjoint.........................proved - complete [shostak](0.73 s)
Brel_disjoint.........................proved - complete [shostak](0.04 s)
ABrel_union...........................proved - complete [shostak](0.02 s)
ABrel_disjoint........................proved - complete [shostak](0.07 s)
Cantor_Bernstein_Schroeder............proved - complete [shostak](0.62 s)
Theory totals: 36 formulas, 36 attempted, 36 succeeded (4.57 s)
Proof summary for theory top_choice_facts
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory relational_choice
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory relation_implication
rel_impl_extensionality...............proved - complete [shostak](0.02 s)
lemma_double_impl.....................proved - complete [shostak](0.01 s)
rel_impl_is_partial_order.............proved - complete [shostak](0.04 s)
double_impl_is_equivalence............proved - complete [shostak](0.05 s)
turnstile_TCC1........................proved - complete [shostak](0.07 s)
models_TCC1...........................proved - complete [shostak](0.12 s)
Theory totals: 6 formulas, 6 attempted, 6 succeeded (0.31 s)
Proof summary for theory relational_choice_properties
fun_choice_impl_description...........proved - complete [shostak](0.06 s)
fun_choice_impl_rel_unique_choice.....proved - complete [shostak](0.04 s)
fun_choice_impl_rel_choice............proved - complete [shostak](0.04 s)
fun_choice_impl_rel_choice_impl_description_rel_choice...proved - complete [shostak](0.07 s)
fun_choice_impl_rel_choice_and_description_rel_choice...proved - complete [shostak](0.03 s)
fun_choice_impl_rel_unique_choice_impl_description_rel_choice...proved - complete [shostak](0.08 s)
fun_choice_impl_rel_unique_choice_and_description_rel_choice...proved - complete [shostak](0.03 s)
description_rel_unique_choice_imp_funct_choice...proved - complete [shostak](0.05 s)
description_rel_and_rel_unique_choice_imp_funct_choice...proved - complete [shostak](0.03 s)
rel_choice_and_proof_irrel_imp_guarded_rel_choice...proved - complete [shostak](0.05 s)
relx_choice_indep_of_premises_imp_guarded_rel_choice...proved - complete [shostak](0.06 s)
fun_choice_equiv_rel_unique_param_desc...proved - complete [shostak](0.03 s)
Theory totals: 12 formulas, 12 attempted, 12 succeeded (0.58 s)
Proof summary for theory top_refinement_relations
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory relation_extension
rel_extension_is_equivalence..........proved - complete [shostak](0.05 s)
Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.05 s)
Proof summary for theory relation_extension_props
extended_equiv_class_non_empty........proved - complete [shostak](0.03 s)
nonempty_equivClass_impl_extended_equiv_class_non_empty...proved - complete [shostak](0.04 s)
nonempty_equivClass_iff_extended_equiv_classT_non_empty...proved - complete [shostak](0.16 s)
nonempty_equivClass_iff_extended_equiv_classU_non_empty...proved - complete [shostak](0.16 s)
proj_tuple_1_equiv_class_representative...proved - complete [shostak](0.02 s)
proj_tuple_2_equiv_class_representative...proved - complete [shostak](0.02 s)
Theory totals: 6 formulas, 6 attempted, 6 succeeded (0.44 s)
Proof summary for theory relation_inverse_image
equivClass_is_nonempty................proved - complete [shostak](0.02 s)
equivClass_equal_is_nonempty..........proved - complete [shostak](0.01 s)
inverse_image_of_equivalence..........proved - complete [shostak](0.03 s)
preserves_eqv_of_inv_image............proved - complete [shostak](0.02 s)
inverse_image_of_equality.............proved - complete [shostak](0.02 s)
image_inverse_eq_is_eq_kernel.........proved - complete [shostak](0.02 s)
inv_img_surj_impl_codom_eq............proved - complete [shostak](0.05 s)
right_inv_inv_finv_image_impl_codom_eq...proved - complete [shostak](0.06 s)
surjective_eqv_image_inv_rel_codomain...proved - complete [shostak](0.03 s)
right_inv_inv_finv_image_eq_codom_eq...proved - complete [shostak](0.05 s)
Theory totals: 10 formulas, 10 attempted, 10 succeeded (0.32 s)
Proof summary for theory relation_inverse_extension
le_U_induces_equivalence..............proved - complete [shostak](0.03 s)
le_T_induces_equivalence..............proved - complete [shostak](0.04 s)
rel_inv_extension_is_equivalence......proved - complete [shostak](0.06 s)
rel_extension_IFF_rel_ext.............proved - complete [shostak](0.05 s)
rel_inv_extension2_is_equivalence.....proved - complete [shostak](0.08 s)
Theory totals: 5 formulas, 5 attempted, 5 succeeded (0.27 s)
Proof summary for theory rr_rel
g_conistent_with_RR...................proved - complete [shostak](0.04 s)
f_conistent_with_RR...................proved - complete [shostak](0.04 s)
RR_functional_conditional_equal_RR2...proved - complete [shostak](0.14 s)
Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.22 s)
Proof summary for theory simplest_examples
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory singleton_example
relations_equality_TCC1...............proved - complete [shostak](0.03 s)
relations_equality_TCC2...............proved - complete [shostak](0.02 s)
relations_equality....................proved - complete [shostak](0.06 s)
relations_equality2...................proved - complete [shostak](0.08 s)
Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.19 s)
Proof summary for theory finite_nats_trivial
T1_TCC1...............................proved - complete [shostak](0.02 s)
U1_TCC1...............................proved - complete [shostak](0.01 s)
g1_TCC1...............................proved - complete [shostak](0.02 s)
e1_TCC1...............................proved - complete [shostak](0.06 s)
relations_equality_TCC1...............proved - complete [shostak](0.05 s)
relations_equality_TCC2...............proved - complete [shostak](0.14 s)
relations_equality....................proved - complete [shostak](0.20 s)
relations_equality2...................proved - complete [shostak](0.27 s)
Theory totals: 8 formulas, 8 attempted, 8 succeeded (0.76 s)
Proof summary for theory infinite_to_infinite_trivial
relations_equality_TCC1...............proved - complete [shostak](0.12 s)
relations_equality_TCC2...............proved - complete [shostak](0.04 s)
relations_equality....................proved - complete [shostak](0.14 s)
relations_equality2...................proved - complete [shostak](0.19 s)
Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.48 s)
Proof summary for theory finite_to_infinite
relations_equality_TCC1...............proved - complete [shostak](0.04 s)
relations_equality_TCC2...............proved - complete [shostak](0.05 s)
relations_equality....................proved - complete [shostak](0.07 s)
relations_equality2...................proved - complete [shostak](0.15 s)
Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.31 s)
Proof summary for theory infinite_to_finite_finite_equival_finite_equival_classes
relations_equality_TCC1...............proved - complete [shostak](0.06 s)
relations_equality_TCC2...............proved - complete [shostak](0.04 s)
relations_equality....................proved - complete [shostak](0.15 s)
relations_equality2...................proved - complete [shostak](0.25 s)
Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.50 s)
Proof summary for theory infinite_to_finite_infinite_equival_finite_equival_classes
U8_TCC1...............................proved - complete [shostak](0.01 s)
relations_equality_TCC1...............proved - complete [shostak](0.12 s)
relations_equality_TCC2...............proved - complete [shostak](0.10 s)
relations_equality....................proved - complete [shostak](0.62 s)
relations_equality2...................proved - complete [shostak](0.54 s)
Theory totals: 5 formulas, 5 attempted, 5 succeeded (1.39 s)
Proof summary for theory infinite_to_infinite_infinite_equival_infinite_equival_classes
e9_TCC1...............................proved - complete [shostak](0.01 s)
relations_equality_TCC1...............proved - complete [shostak](0.05 s)
relations_equality_TCC2...............proved - complete [shostak](0.05 s)
relations_equality....................proved - complete [shostak](0.07 s)
relations_equality2...................proved - complete [shostak](0.13 s)
Theory totals: 5 formulas, 5 attempted, 5 succeeded (0.30 s)
Proof summary for theory infinite_to_infinite_infinite_equival_finite_equival_classes
relations_equality_TCC1...............proved - complete [shostak](0.04 s)
relations_equality_TCC2...............proved - complete [shostak](0.11 s)
relations_equality....................proved - complete [shostak](0.28 s)
relations_equality2...................proved - complete [shostak](0.42 s)
Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.85 s)
Proof summary for theory finite_to_infinite_finite_equival_infinite_equival_classes
T11_TCC1..............................proved - complete [shostak](0.01 s)
relations_equality_TCC1...............proved - complete [shostak](0.10 s)
relations_equality_TCC2...............proved - complete [shostak](0.12 s)
relations_equality....................proved - complete [shostak](0.54 s)
relations_equality2...................proved - complete [shostak](0.77 s)
Theory totals: 5 formulas, 5 attempted, 5 succeeded (1.54 s)
Grand Totals: 447 proofs, 447 attempted, 447 succeeded (97.82 s)
[ Seitenstruktur0.223Drucken
]
|
|
|
|
|
|
