| products/sources/formale sprachen/PVS/summaries/ |
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei: sets_aux.summary Sprache: Unknown
|
Spracherkennung für: .summary vermutete Sprache: MT940 {MT940[457] Hlasm[1381] Haskell[1763]} [Methode: Schwerpunktbildung, einfache Gewichte, sechs Dimensionen] *** *** 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 fun_choice_impl_rel_choice_and_description_rel_choice...proved - complete [shostak] fun_choice_impl_rel_unique_choice_impl_description_rel_choice...proved - complete [ fun_choice_impl_rel_unique_choice_and_description_rel_choice...proved - complete [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 rel_choice_and_proof_irrel_imp_guarded_rel_choice...proved - complete [shostak](0.0 relx_choice_indep_of_premises_imp_guarded_rel_choice...proved - complete [shostak]( 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 [shosta nonempty_equivClass_iff_extended_equiv_classT_non_empty...proved - complete [shosta nonempty_equivClass_iff_extended_equiv_classU_non_empty...proved - complete [shosta 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_clas 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_classe 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) [ Dauer der Verarbeitung: 0.150 Sekunden ] |