| products/sources/formale Sprachen/PVS/summaries/ |
|
Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei: find2.thy Sprache: SML
|
Untersuchungsergebnis.summary Download desMT940 {MT940[840] Hlasm[998] BAT[1110]}zum Wurzelverzeichnis wechseln *** *** top (16:21:58 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 bounded_integers non_empty_bounded_above_has_greatest_lem...proved - complete [shostak](0.37 s) non_empty_bounded_above_has_greatest...proved - complete [shostak](0.30 s) non_empty_bounded_below_has_least_lem...proved - complete [shostak](0.34 s) non_empty_bounded_below_has_least.....proved - complete [shostak](0.30 s) remove_least_TCC1.....................proved - complete [shostak](0.29 s) remove_least..........................proved - complete [shostak](0.17 s) remove_least_monotone.................proved - complete [shostak](0.69 s) remove_greatest_TCC1..................proved - complete [shostak](0.28 s) remove_greatest.......................proved - complete [shostak](0.19 s) remove_greatest_monotone..............proved - complete [shostak](0.68 s) intersection_greatest.................proved - complete [shostak](0.56 s) intersection_least....................proved - complete [shostak](0.53 s) Theory totals: 12 formulas, 12 attempted, 12 succeeded (4.71 s) Proof summary for theory non_empty_bounded_sets non_empty_bounded_above_is_nonempty...proved - complete [shostak](0.28 s) non_empty_bounded_above_is_bounded_above...proved - complete [shostak](0.29 s) non_empty_bounded_below_is_nonempty...proved - complete [shostak](0.28 s) non_empty_bounded_below_is_bounded_below...proved - complete [shostak](0.29 s) non_empty_finite_bounded_above........proved - complete [shostak](0.31 s) non_empty_finite_bounded_below........proved - complete [shostak](0.29 s) Theory totals: 6 formulas, 6 attempted, 6 succeeded (1.74 s) Proof summary for theory total_lattices singleton_has_greatest................proved - incomplete [shostak](0.04 s) union_preserves_has_greatest..........proved - complete [shostak](0.10 s) add_preserves_has_greatest............proved - incomplete [shostak](0.08 s) greatest_singleton....................proved - incomplete [shostak](0.15 s) greatest_union........................proved - complete [shostak](0.33 s) greatest_add..........................proved - incomplete [shostak](0.09 s) singleton_has_least...................proved - incomplete [shostak](0.07 s) union_preserves_has_least.............proved - complete [shostak](0.12 s) add_preserves_has_least...............proved - incomplete [shostak](0.11 s) least_singleton.......................proved - incomplete [shostak](0.19 s) least_union...........................proved - complete [shostak](0.35 s) least_add.............................proved - incomplete [shostak](0.13 s) Theory totals: 12 formulas, 12 attempted, 12 succeeded (1.76 s) Proof summary for theory minmax_orders greatest_TCC1.........................proved - complete [shostak](0.08 s) greatest_iff_least_upper_bound........proved - complete [shostak](0.14 s) greatest_is_least_upper_bound.........proved - complete [shostak](0.16 s) has_greatest_is_least_bounded_above...proved - complete [shostak](0.13 s) greatest_equals_lub_TCC1..............proved - complete [shostak](0.03 s) greatest_equals_lub...................proved - complete [shostak](0.04 s) greatest_unique.......................proved - complete [shostak](0.77 s) greatest_is_maximal...................proved - complete [shostak](0.04 s) maximal_is_greatest...................proved - complete [shostak](0.03 s) non_empty_finite_has_greatest.........proved - incomplete [shostak](0.37 s) greatest_ge...........................proved - complete [shostak](0.03 s) greatest_monotone.....................proved - complete [shostak](0.04 s) greatest_def..........................proved - complete [shostak](0.07 s) greatest_upper_bound..................proved - complete [shostak](0.16 s) least_TCC1............................proved - complete [shostak](0.08 s) least_iff_greatest_lower_bound........proved - complete [shostak](0.15 s) least_is_greatest_lower_bound.........proved - complete [shostak](0.15 s) has_least_is_greatest_bounded_below...proved - complete [shostak](0.14 s) least_equals_glb_TCC1.................proved - complete [shostak](0.02 s) least_equals_glb......................proved - complete [shostak](0.05 s) least_unique..........................proved - complete [shostak](0.78 s) least_is_minimal......................proved - complete [shostak](0.04 s) minimal_is_least......................proved - complete [shostak](0.04 s) non_empty_finite_has_least............proved - incomplete [shostak](0.37 s) least_le..............................proved - complete [shostak](0.03 s) least_monotone........................proved - complete [shostak](0.05 s) least_def.............................proved - complete [shostak](0.06 s) least_lower_bound.....................proved - complete [shostak](0.16 s) has_extrema_has_greatest..............proved - complete [shostak](0.05 s) has_extrema_has_least.................proved - complete [shostak](0.04 s) total_order_is_lattice................proved - incomplete [shostak](0.68 s) Theory totals: 31 formulas, 31 attempted, 31 succeeded (4.96 s) Proof summary for theory bounded_orders lub_TCC1..............................proved - complete [shostak](0.12 s) unique_least_upper_bound..............proved - complete [shostak](0.17 s) subset_upper_bound....................proved - complete [shostak](0.05 s) subset_least_upper_bound..............proved - complete [shostak](0.03 s) lub_def...............................proved - complete [shostak](0.03 s) lub_eq................................proved - complete [shostak](0.03 s) lub_ge................................proved - complete [shostak](0.03 s) lub_le................................proved - complete [shostak](0.14 s) all_least_bounded.....................proved - complete [shostak](0.03 s) all_finite_least_bounded..............proved - complete [shostak](0.02 s) complete_upper_semilattice_upper......proved - complete [shostak](1.33 s) upper_semilattice_is_partial_order....proved - complete [shostak](0.06 s) glb_TCC1..............................proved - complete [shostak](0.13 s) unique_greatest_lower_bound...........proved - complete [shostak](0.18 s) subset_lower_bound....................proved - complete [shostak](0.04 s) subset_greatest_lower_bound...........proved - complete [shostak](0.03 s) glb_def...............................proved - complete [shostak](0.04 s) glb_eq................................proved - complete [shostak](0.02 s) glb_le................................proved - complete [shostak](0.03 s) glb_ge................................proved - complete [shostak](0.14 s) all_greatest_bounded..................proved - complete [shostak](0.02 s) all_finite_greatest_bounded...........proved - complete [shostak](0.03 s) complete_lower_semilattice_lower......proved - complete [shostak](1.34 s) lower_semilattice_is_partial_order....proved - complete [shostak](0.06 s) bounded_is_bounded_above..............proved - complete [shostak](0.03 s) bounded_is_bounded_below..............proved - complete [shostak](0.03 s) tightly_bounded_above.................proved - complete [shostak](0.04 s) tightly_bounded_below.................proved - complete [shostak](0.03 s) complete_lattice_upper................proved - complete [shostak](0.06 s) complete_lattice_lower................proved - complete [shostak](0.05 s) lattice_upper.........................proved - complete [shostak](0.07 s) lattice_lower.........................proved - complete [shostak](0.07 s) complete_lattice_is_lattice...........proved - complete [shostak](3.56 s) upper_bound_singleton.................proved - complete [shostak](0.03 s) least_upper_bound_singleton...........proved - complete [shostak](0.25 s) lub_singleton_TCC1....................proved - complete [shostak](0.10 s) lub_singleton.........................proved - complete [shostak](0.10 s) lower_bound_singleton.................proved - complete [shostak](0.03 s) greatest_lower_bound_singleton........proved - complete [shostak](0.25 s) glb_singleton_TCC1....................proved - complete [shostak](0.10 s) glb_singleton.........................proved - complete [shostak](0.10 s) upper_bound_emptyset..................proved - complete [shostak](0.02 s) lower_bound_emptyset..................proved - complete [shostak](0.03 s) lub_emptyset_is_glb_fullset...........proved - complete [shostak](0.04 s) glb_emptyset_is_lub_fullset...........proved - complete [shostak](0.04 s) least_bounded_above_emptyset..........proved - complete [shostak](0.24 s) greatest_bounded_below_emptyset.......proved - complete [shostak](0.23 s) le_lub................................proved - complete [shostak](0.06 s) eq_lub................................proved - complete [shostak](0.05 s) lub_add_TCC1..........................proved - complete [shostak](0.06 s) lub_add...............................proved - complete [shostak](0.08 s) le_glb................................proved - complete [shostak](0.06 s) eq_glb................................proved - complete [shostak](0.04 s) glb_add_TCC1..........................proved - complete [shostak](0.06 s) glb_add...............................proved - complete [shostak](0.07 s) Theory totals: 55 formulas, 55 attempted, 55 succeeded (10.06 s) Proof summary for theory relations_extra strict_order_is_asymmetric............proved - complete [shostak](0.04 s) asymmetric_is_antisymmetric...........proved - complete [shostak](0.04 s) asymmetric_is_irreflexive.............proved - complete [shostak](0.03 s) dichotomous_is_trichotomous...........proved - complete [shostak](0.04 s) order_is_transitive...................proved - complete [shostak](0.02 s) order_is_antisymmetric................proved - complete [shostak](0.06 s) partial_order_is_order................proved - complete [shostak](0.04 s) strict_order_is_order.................proved - complete [shostak](0.06 s) total_order_is_linear.................proved - complete [shostak](0.20 s) strict_total_order_is_linear..........proved - complete [shostak](0.19 s) reflexive.............................proved - complete [shostak](0.03 s) irreflexive...........................proved - complete [shostak](0.02 s) symmetric.............................proved - complete [shostak](0.02 s) antisymmetric.........................proved - complete [shostak](0.02 s) asymmetric............................proved - complete [shostak](0.03 s) transitive............................proved - complete [shostak](0.02 s) dichotomous...........................proved - complete [shostak](0.02 s) trichotomous..........................proved - complete [shostak](0.02 s) well_founded..........................proved - complete [shostak](0.02 s) Theory totals: 19 formulas, 19 attempted, 19 succeeded (0.91 s) Proof summary for theory lattices finite_set_is_tightly_bounded.........proved - complete [shostak](0.04 s) add_preserves_tightly_bounded.........proved - complete [shostak](0.04 s) union_preserves_tightly_bounded.......proved - complete [shostak](0.07 s) Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.15 s) Proof summary for theory lower_semilattices finite_set_is_greatest_bounded_below...proved - complete [shostak](0.03 s) greatest_lower_bound_singleton........proved - complete [shostak](0.04 s) glb_singleton.........................proved - complete [shostak](0.05 s) le_glb................................proved - complete [shostak](0.10 s) glb_le_1..............................proved - complete [shostak](0.09 s) glb_le_2..............................proved - complete [shostak](0.08 s) union_preserves_bounded_below.........proved - complete [shostak](0.26 s) add_preserves_bounded_below...........proved - complete [shostak](0.05 s) greatest_lower_bound_union............proved - complete [shostak](0.09 s) greatest_lower_bound_add..............proved - complete [shostak](0.06 s) union_preserves_greatest_bounded_below...proved - complete [shostak](0.04 s) add_preserves_greatest_bounded_below...proved - complete [shostak](0.05 s) glb_union.............................proved - complete [shostak](0.12 s) glb_add...............................proved - complete [shostak](0.06 s) Theory totals: 14 formulas, 14 attempted, 14 succeeded (1.12 s) Proof summary for theory bounded_sets least_bounded_above_is_bounded_above...proved - complete [shostak](0.03 s) greatest_bounded_below_is_bounded_below...proved - complete [shostak](0.03 s) bounded_is_bounded_above..............proved - complete [shostak](0.06 s) bounded_is_bounded_below..............proved - complete [shostak](0.05 s) tightly_bounded_is_bounded............proved - complete [shostak](0.04 s) tightly_bounded_above.................proved - complete [shostak](0.07 s) tightly_bounded_below.................proved - complete [shostak](0.07 s) intersection1_preserves_bounded_above...proved - complete [shostak](0.14 s) intersection2_preserves_bounded_above...proved - complete [shostak](0.14 s) difference_preserves_bounded_above....proved - complete [shostak](0.04 s) remove_preserves_bounded_above........proved - complete [shostak](0.04 s) intersection1_preserves_bounded_below...proved - complete [shostak](0.15 s) intersection2_preserves_bounded_below...proved - complete [shostak](0.14 s) difference_preserves_bounded_below....proved - complete [shostak](0.04 s) remove_preserves_bounded_below........proved - complete [shostak](0.05 s) intersection1_preserves_bounded.......proved - complete [shostak](0.04 s) intersection2_preserves_bounded.......proved - complete [shostak](0.05 s) difference_preserves_bounded..........proved - complete [shostak](0.05 s) remove_preserves_bounded..............proved - complete [shostak](0.06 s) Theory totals: 19 formulas, 19 attempted, 19 succeeded (1.27 s) Proof summary for theory upper_semilattices finite_set_is_least_bounded_above.....proved - complete [shostak](0.03 s) least_upper_bound_singleton...........proved - complete [shostak](0.16 s) lub_singleton.........................proved - complete [shostak](0.06 s) lub_le................................proved - complete [shostak](0.11 s) le_lub_1..............................proved - complete [shostak](0.08 s) le_lub_2..............................proved - complete [shostak](0.08 s) union_preserves_bounded_above.........proved - complete [shostak](0.26 s) add_preserves_bounded_above...........proved - complete [shostak](0.05 s) least_upper_bound_union...............proved - complete [shostak](0.09 s) least_upper_bound_add.................proved - complete [shostak](0.06 s) union_preserves_least_bounded_above...proved - complete [shostak](0.05 s) add_preserves_least_bounded_above.....proved - complete [shostak](0.06 s) lub_union.............................proved - complete [shostak](0.11 s) lub_add...............................proved - complete [shostak](0.07 s) Theory totals: 14 formulas, 14 attempted, 14 succeeded (1.26 s) Proof summary for theory closure_ops reflexive_closure_TCC1................proved - complete [shostak](0.04 s) irreflexive_kernel_TCC1...............proved - complete [shostak](0.03 s) symmetric_closure_TCC1................proved - complete [shostak](0.05 s) symmetric_kernel_TCC1.................proved - complete [shostak](0.04 s) asymmetric_kernel_TCC1................proved - complete [shostak](0.05 s) transitive_closure_TCC1...............proved - complete [shostak](0.07 s) preorder_closure_TCC1.................proved - complete [shostak](0.06 s) reflexive_irreflexive.................proved - complete [shostak](0.10 s) irreflexive_reflexive.................proved - complete [shostak](0.10 s) reflexive_closure_preserves_transitive...proved - complete [shostak](0.04 s) reflexive_closure_preserves_antisymmetric...proved - complete [shostak](0.06 s) order_to_partial_order................proved - complete [shostak](0.03 s) reflexive_closure_dichotomous.........proved - complete [shostak](0.08 s) linear_order_to_total_order...........proved - complete [shostak](0.08 s) order_to_strict_order.................proved - complete [shostak](0.11 s) irreflexive_kernel_of_antisymmetric...proved - complete [shostak](0.12 s) irreflexive_kernel_trichotomous.......proved - complete [shostak](0.13 s) linear_order_to_strict_total_order....proved - complete [shostak](0.12 s) symmetric_kernel_of_preorder..........proved - complete [shostak](0.18 s) asymmetric_kernel_of_preorder.........proved - complete [shostak](0.17 s) preorder_closure_converse.............proved - complete [shostak](0.21 s) symmetry_char.........................proved - complete [shostak](0.15 s) transitive_closure_of_reflexive.......proved - complete [shostak](0.19 s) transitive_closure_is_monotone........proved - complete [shostak](0.16 s) preorder_closure_is_monotone..........proved - complete [shostak](0.16 s) preorder_closure_preserves_symmetry...proved - complete [shostak](0.22 s) transitive_closure_step_r.............proved - complete [shostak](0.21 s) transitive_closure_step_l.............proved - complete [shostak](0.20 s) preorder_closure_reflexive_transitive...proved - complete [shostak](0.17 s) preorder_closure_transitive_reflexive...proved - complete [shostak](0.29 s) reflexive_closure_identity............proved - complete [shostak](0.20 s) irreflexive_kernel_identity...........proved - complete [shostak](0.20 s) symmetric_closure_identity............proved - complete [shostak](0.19 s) symmetric_kernel_identity.............proved - complete [shostak](0.18 s) asymmetric_kernel_identity............proved - complete [shostak](0.20 s) transitive_closure_identity...........proved - complete [shostak](0.25 s) preorder_closure_identity.............proved - complete [shostak](0.24 s) preorder_closure_reflexive............proved - complete [shostak](0.15 s) equivalence_closure_identity..........proved - complete [shostak](0.23 s) Theory totals: 39 formulas, 39 attempted, 39 succeeded (5.42 s) Proof summary for theory relation_iterate comp_equal_r..........................proved - complete [shostak](0.04 s) comp_equal_l..........................proved - complete [shostak](0.04 s) iterate_TCC1..........................proved - complete [shostak](0.03 s) iterate_TCC2..........................proved - complete [shostak](0.02 s) iterate_add...........................proved - complete [shostak](0.09 s) iterate_add_applied...................proved - complete [shostak](0.04 s) iterate_1.............................proved - complete [shostak](0.03 s) iterate_add_one.......................proved - complete [shostak](0.07 s) iterate_mult..........................proved - complete [shostak](0.09 s) converse_equal........................proved - complete [shostak](0.04 s) converse_comp.........................proved - complete [shostak](0.06 s) iterate_converse......................proved - complete [shostak](0.05 s) comp_is_monotone......................proved - complete [shostak](0.04 s) iterate_is_monotone...................proved - complete [shostak](0.05 s) Theory totals: 14 formulas, 14 attempted, 14 succeeded (0.66 s) Proof summary for theory indexed_sets_extra IUnion_is_monotone....................proved - complete [shostak](0.03 s) IIntersection_is_monotone.............proved - complete [shostak](0.03 s) Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.06 s) Proof summary for theory complementary_lattices dual_dual.............................proved - complete [shostak](0.04 s) dual_inclusion1.......................proved - complete [shostak](0.05 s) dual_inclusion2.......................proved - complete [shostak](0.04 s) dual_inclusion3.......................proved - complete [shostak](0.04 s) dual_inclusion4.......................proved - complete [shostak](0.04 s) Theory totals: 5 formulas, 5 attempted, 5 succeeded (0.19 s) Proof summary for theory function_image_extra image_singleton.......................proved - complete [shostak](0.06 s) image_add.............................proved - complete [shostak](0.05 s) Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.11 s) Proof summary for theory complementary_orders complement_complement.................proved - complete [shostak](0.05 s) image_complement......................proved - complete [shostak](0.05 s) inverse_complement....................proved - complete [shostak](0.07 s) le_complement.........................proved - complete [shostak](0.05 s) upper_bound_complement................proved - complete [shostak](0.06 s) bounded_above_complement..............proved - complete [shostak](0.15 s) least_upper_bound_complement..........proved - complete [shostak](0.18 s) least_bounded_above_complement........proved - complete [shostak](0.25 s) lub_complement_TCC1...................proved - complete [shostak](0.03 s) lub_complement........................proved - complete [shostak](0.18 s) glb_complement_TCC1...................proved - complete [shostak](0.35 s) glb_complement........................proved - complete [shostak](0.17 s) Theory totals: 12 formulas, 12 attempted, 12 succeeded (1.59 s) Proof summary for theory complete_lattices every_set_is_tightly_bounded..........proved - complete [shostak](0.04 s) Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.04 s) Proof summary for theory complete_lower_semilattices every_set_is_greatest_bounded_below...proved - complete [shostak](0.03 s) Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.03 s) Proof summary for theory complete_upper_semilattices every_set_is_least_bounded_above......proved - complete [shostak](0.03 s) Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.03 s) Proof summary for theory finite_orders IMP_finite_types_TCC1.................proved - complete [shostak](0.02 s) finite_lower_semilattice_is_complete...proved - complete [shostak](0.04 s) finite_upper_semilattice_is_complete...proved - complete [shostak](0.03 s) finite_lattice_is_complete............proved - complete [shostak](0.06 s) finite_strict_order_is_well_founded...proved - complete [shostak](0.74 s) finite_strict_total_order_is_well_ordered...proved - complete [shostak](0.03 s) Theory totals: 6 formulas, 6 attempted, 6 succeeded (0.92 s) Proof summary for theory finite_types every_set_is_finite...................proved - complete [shostak](0.02 s) every_non_empty_set_is_non_empty_finite...proved - complete [shostak](0.03 s) fullset_is_nonempty_finite............proved - complete [shostak](0.03 s) Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.08 s) Proof summary for theory finite_pointwise_orders IMP_infinite_pigeonhole_TCC1..........proved - complete [shostak](0.02 s) IMP_infinite_pigeonhole_TCC2..........proved - complete [shostak](0.02 s) infinite_pigeonhole...................proved - complete [shostak](2.89 s) descending_exists.....................proved - complete [shostak](0.50 s) descending_reflexive_closure..........proved - complete [shostak](0.12 s) pointwise_pigeonhole..................proved - complete [shostak](1.38 s) strictly_pointwise_well_founded_order...proved - complete [shostak](1.87 s) Theory totals: 7 formulas, 7 attempted, 7 succeeded (6.80 s) Proof summary for theory numbers_infinite nat_infinite..........................proved - complete [shostak](0.07 s) int_infinite..........................proved - complete [shostak](0.05 s) rat_infinite..........................proved - complete [shostak](0.05 s) real_infinite.........................proved - complete [shostak](0.05 s) Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.22 s) Proof summary for theory pointwise_orders pointwise_preserves_reflexive.........proved - complete [shostak](0.03 s) pointwise_preserves_transitive........proved - complete [shostak](0.04 s) pointwise_preserves_preorder..........proved - complete [shostak](0.05 s) pointwise_preserves_antisymmetric.....proved - complete [shostak](0.08 s) pointwise_preserves_partial_order.....proved - complete [shostak](0.12 s) finiteness_lemma......................proved - complete [shostak](0.21 s) least_upper_bound_pointwise...........proved - complete [shostak](0.59 s) least_bounded_above_pointwise.........proved - complete [shostak](0.32 s) pointwise_preserves_upper_semilattices...proved - complete [shostak](0.21 s) pointwise_preserves_complete_upper_semilattices...proved - complete [shostak](0.31 s greatest_lower_bound_pointwise........proved - complete [shostak](0.72 s) greatest_bounded_below_pointwise......proved - complete [shostak](0.58 s) pointwise_preserves_lower_semilattices...proved - complete [shostak](0.46 s) pointwise_preserves_complete_lower_semilattices...proved - complete [shostak](0.59 s pointwise_preserves_lattices..........proved - complete [shostak](0.74 s) pointwise_preserves_complete_lattices...proved - complete [shostak](0.88 s) lub_pointwise_def_TCC1................proved - complete [shostak](0.20 s) lub_pointwise_def_TCC2................proved - complete [shostak](1.08 s) lub_pointwise_def.....................proved - complete [shostak](1.16 s) glb_pointwise_def_TCC1................proved - complete [shostak](1.06 s) glb_pointwise_def_TCC2................proved - complete [shostak](1.08 s) glb_pointwise_def.....................proved - complete [shostak](1.17 s) Theory totals: 22 formulas, 22 attempted, 22 succeeded (11.68 s) Proof summary for theory skolemization skolemize_exists......................proved - complete [shostak](0.04 s) skolemize_forall......................proved - complete [shostak](0.04 s) Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.08 s) Proof summary for theory well_foundedness no_infinite_descending_sequence.......proved - complete [shostak](0.08 s) well_founded_is_irreflexive...........proved - complete [shostak](0.03 s) well_order_is_well_founded_order......proved - complete [shostak](0.05 s) well_founded_order_is_well_founded....proved - complete [shostak](0.04 s) well_founded_order_is_strict_order....proved - complete [shostak](0.02 s) transitive_closure_preserves_well_foundedness...proved - complete [shostak](0.15 s) Theory totals: 6 formulas, 6 attempted, 6 succeeded (0.37 s) Proof summary for theory monotone_sequences reflexive_closure_ascending...........proved - complete [shostak](0.09 s) reflexive_closure_descending..........proved - complete [shostak](0.09 s) ascending_lem.........................proved - complete [shostak](0.14 s) descending_lem........................proved - complete [shostak](0.22 s) ascending_subsequence.................proved - complete [shostak](0.26 s) descending_subsequence................proved - complete [shostak](0.11 s) Theory totals: 6 formulas, 6 attempted, 6 succeeded (0.93 s) Proof summary for theory infinite_pigeonhole Union_inverse_image...................proved - complete [shostak](0.04 s) infinite_pigeonhole...................proved - complete [shostak](0.06 s) Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.11 s) Proof summary for theory integer_enumerations enumerable_below_bounded..............proved - complete [shostak](0.21 s) enumerable_infinite...................proved - complete [shostak](0.33 s) remove_enumerable.....................proved - complete [shostak](0.10 s) enum_TCC1.............................proved - complete [shostak](0.33 s) enum_TCC2.............................proved - complete [shostak](0.11 s) enum_member...........................proved - complete [shostak](0.12 s) enum_surjective_lem...................proved - complete [shostak](0.89 s) enum_surjective.......................proved - complete [shostak](0.52 s) enum_def..............................proved - complete [shostak](0.55 s) enum_subset_monotone..................proved - complete [shostak](0.40 s) enum_strictly_ascending...............proved - complete [shostak](0.56 s) enum_strictly_monotone................proved - complete [shostak](0.14 s) enumerable............................proved - complete [shostak](0.09 s) enum_bijective........................proved - complete [shostak](0.70 s) Theory totals: 14 formulas, 14 attempted, 14 succeeded (5.06 s) Proof summary for theory finite_total_orders IMP_finite_orders_TCC1................proved - complete [shostak](0.02 s) Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.02 s) Proof summary for theory fixed_points prefixed_points_closed................proved - complete [shostak](0.03 s) prefixed_points_lower_bounds..........proved - complete [shostak](0.16 s) least_prefixed_point_is_fixed_point...proved - complete [shostak](0.05 s) least_fixed_point_le_prefixed_points...proved - complete [shostak](0.16 s) least_prefixed_point..................proved - complete [shostak](0.08 s) least_fixed_point_exists..............proved - complete [shostak](0.04 s) least_fixed_point_unique..............proved - complete [shostak](0.80 s) Theory totals: 7 formulas, 7 attempted, 7 succeeded (1.33 s) Proof summary for theory new_mucalculus_prop leq_equals_subset.....................proved - complete [shostak](1.12 s) monotonic_is_monotone.................proved - complete [shostak](1.14 s) leq_is_complete_lattice...............proved - complete [shostak](1.12 s) fixpoint_equals_fixed_point...........proved - complete [shostak](0.09 s) fixpoint2_equals_fixed_point..........proved - complete [shostak](0.09 s) antisymmetry..........................proved - complete [shostak](0.11 s) reflexivity...........................proved - complete [shostak](0.09 s) glb_equals_glb........................proved - complete [shostak](0.22 s) glb_lower_bound.......................proved - complete [shostak](0.12 s) glb_greatest_lower_bound..............proved - complete [shostak](0.13 s) lub_equals_lub........................proved - complete [shostak](0.31 s) lub_upper_bound.......................proved - complete [shostak](0.12 s) lub_least_upper_bound.................proved - complete [shostak](0.13 s) mu_equals_least_prefixed_point_TCC1...proved - complete [shostak](0.19 s) mu_equals_least_prefixed_point........proved - complete [shostak](0.10 s) smallest_closed.......................proved - complete [shostak](0.11 s) fixpoint_mu2..........................proved - complete [shostak](0.46 s) fixpoint_mu1..........................proved - complete [shostak](0.08 s) closure_mu............................proved - complete [shostak](0.21 s) least_fixpoint2.......................proved - complete [shostak](0.24 s) least_fixpoint1.......................proved - complete [shostak](0.09 s) lfp_equals_lfp........................proved - complete [shostak](0.10 s) mu_lfp................................proved - complete [shostak](0.20 s) monotonic_dual_monotonic..............proved - complete [shostak](0.11 s) least_fixpoint_dual...................proved - complete [shostak](0.47 s) greatest_fixpoint_dual................proved - complete [shostak](0.11 s) complement_is_complement..............proved - complete [shostak](1.18 s) closure_nu............................proved - complete [shostak](0.24 s) largest_closed........................proved - complete [shostak](0.51 s) fixpoint_nu1..........................proved - complete [shostak](0.25 s) fixpoint_nu2..........................proved - complete [shostak](0.21 s) greatest_fixpoint1....................proved - complete [shostak](0.12 s) greatest_fixpoint2....................proved - complete [shostak](0.10 s) nu_gfp................................proved - complete [shostak](0.09 s) Theory totals: 34 formulas, 34 attempted, 34 succeeded (9.99 s) Proof summary for theory sets_complete_lattices subset_equals_pointwise_implies.......proved - complete [shostak](0.44 s) subset_is_a_complete_lattice..........proved - complete [shostak](1.37 s) Theory totals: 2 formulas, 2 attempted, 2 succeeded (1.81 s) Proof summary for theory booleans_are_finite bool_is_finite_type...................proved - complete [shostak](0.04 s) implies_is_total_order................proved - complete [shostak](0.04 s) IMP_finite_types_TCC1.................proved - complete [shostak](0.01 s) Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.09 s) Proof summary for theory bounded_nats every_nonempty_set_has_least..........proved - complete [shostak](0.50 s) Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.50 s) Proof summary for theory chain chain_TCC1............................proved - complete [shostak](0.20 s) subset_chain..........................proved - complete [shostak](1.19 s) intersection_chain....................proved - complete [shostak](1.53 s) chain_order_partial...................proved - complete [shostak](1.25 s) Theory totals: 4 formulas, 4 attempted, 4 succeeded (4.17 s) Proof summary for theory chain_chain chain_incl_partial_order..............proved - complete [shostak](2.12 s) chain_union_TCC1......................proved - complete [shostak](2.00 s) chain_union_upper_bound...............proved - complete [shostak](0.92 s) Theory totals: 3 formulas, 3 attempted, 3 succeeded (5.05 s) Proof summary for theory converse_zorn converse_zorn.........................proved - complete [shostak](0.73 s) Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.73 s) Proof summary for theory zorn maximal_upto_subset...................proved - complete [shostak](0.17 s) bounded_chain_upto....................proved - complete [shostak](0.29 s) succ_TCC1.............................proved - complete [shostak](1.43 s) succ_TCC2.............................proved - complete [shostak](0.03 s) empty_succ............................proved - complete [shostak](0.06 s) maximal_chain_add_set.................proved - complete [shostak](0.10 s) tower?_TCC1...........................proved - complete [shostak](0.02 s) tower_intersection....................proved - complete [shostak](0.06 s) T0_TCC1...............................proved - complete [shostak](0.15 s) T0_smallest...........................proved - complete [shostak](0.03 s) make_tower_TCC1.......................proved - complete [shostak](0.25 s) T0_construct..........................proved - complete [shostak](0.04 s) T0_comparable.........................proved - complete [shostak](0.20 s) T0_all_comparable.....................proved - complete [shostak](0.13 s) T0_chain..............................proved - complete [shostak](0.29 s) zorn..................................proved - complete [shostak](0.89 s) Theory totals: 16 formulas, 16 attempted, 16 succeeded (4.13 s) Proof summary for theory subset_chain subset_chain_min......................proved - complete [shostak](0.30 s) subset_chain_intersection.............proved - complete [shostak](0.53 s) Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.83 s) Proof summary for theory ordered_subset emptyset_is_prefix....................proved - complete [shostak](0.09 s) fullset_is_prefix.....................proved - complete [shostak](0.08 s) emptyset_is_suffix....................proved - complete [shostak](0.09 s) fullset_is_suffix.....................proved - complete [shostak](0.08 s) upto_TCC1.............................proved - complete [shostak](0.13 s) below_TCC1............................proved - complete [shostak](0.14 s) upfrom_TCC1...........................proved - complete [shostak](0.13 s) above_TCC1............................proved - complete [shostak](0.13 s) add_below_is_upto.....................proved - complete [shostak](0.22 s) remove_upto_is_below..................proved - complete [shostak](0.22 s) add_above_is_upfrom...................proved - complete [shostak](0.17 s) remove_upfrom_is_above................proved - complete [shostak](0.17 s) upto_above_related....................proved - complete [shostak](0.18 s) below_upfrom_related..................proved - complete [shostak](0.18 s) down_TCC1.............................proved - complete [shostak](0.10 s) up_TCC1...............................proved - complete [shostak](0.09 s) down_subset...........................proved - complete [shostak](0.10 s) up_subset.............................proved - complete [shostak](0.10 s) complement_lower_set..................proved - complete [shostak](0.09 s) complement_upper_set..................proved - complete [shostak](0.09 s) lower_set_def.........................proved - complete [shostak](0.19 s) upper_set_def.........................proved - complete [shostak](0.20 s) Union_lower_set.......................proved - complete [shostak](0.10 s) Union_upper_set.......................proved - complete [shostak](0.10 s) union_lower_set.......................proved - complete [shostak](0.17 s) union_upper_set.......................proved - complete [shostak](0.17 s) Intersection_lower_set................proved - complete [shostak](0.10 s) Intersection_upper_set................proved - complete [shostak](0.11 s) intersection_lower_set................proved - complete [shostak](0.16 s) intersection_upper_set................proved - complete [shostak](0.17 s) Theory totals: 30 formulas, 30 attempted, 30 succeeded (4.06 s) Proof summary for theory finite_below nth_TCC1..............................proved - incomplete [shostak](0.23 s) nth_TCC2..............................proved - incomplete [shostak](0.23 s) nth_TCC3..............................proved - incomplete [shostak](0.27 s) nth_TCC4..............................proved - complete [shostak](0.06 s) nth_TCC5..............................proved - complete [shostak](0.04 s) nth_one_step..........................proved - incomplete [shostak](0.37 s) nth_monotonic.........................proved - incomplete [shostak](0.36 s) nth_surjective........................proved - incomplete [shostak](0.40 s) nth_bijective.........................proved - incomplete [shostak](0.09 s) index_TCC1............................proved - complete [shostak](0.21 s) index_TCC2............................proved - complete [shostak](0.11 s) index_TCC3............................proved - incomplete [shostak](0.10 s) index_TCC4............................proved - complete [shostak](0.12 s) index_TCC5............................proved - complete [shostak](0.14 s) index_monotonic.......................proved - incomplete [shostak](0.33 s) index_nth_left_inverse................proved - incomplete [shostak](0.28 s) index_nth_right_inverse...............proved - incomplete [shostak](0.33 s) index_bijective.......................proved - incomplete [shostak](0.06 s) Theory totals: 18 formulas, 18 attempted, 18 succeeded (3.71 s) Proof summary for theory isomorphism isomorphism_implication...............proved - complete [shostak](0.10 s) isomorphism_preserves_reflexive.......proved - complete [shostak](0.33 s) isomorphism_preserves_irreflexive.....proved - complete [shostak](0.34 s) isomorphism_preserves_symmetric.......proved - complete [shostak](0.08 s) isomorphism_preserves_antisymmetric...proved - complete [shostak](0.09 s) isomorphism_preserves_asymmetric......proved - complete [shostak](0.09 s) isomorphism_preserves_transitive......proved - complete [shostak](0.09 s) isomorphism_preserves_dichotomous.....proved - complete [shostak](0.08 s) isomorphism_preserves_trichotomous....proved - complete [shostak](0.09 s) isomorphism_preserves_well_founded....proved - complete [shostak](0.45 s) isomorphism_inverse_TCC1..............proved - complete [shostak](0.06 s) isomorphism_inverse...................proved - complete [shostak](0.14 s) Theory totals: 12 formulas, 12 attempted, 12 succeeded (1.93 s) Proof summary for theory isomorphism_equivalence isomorphism_reflexive.................proved - complete [shostak](0.10 s) isomorphism_symmetric.................proved - complete [shostak](0.09 s) isomorphism_transitive................proved - complete [shostak](0.04 s) isomorphism_equivalence...............proved - complete [shostak](0.03 s) Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.26 s) Proof summary for theory isomorphism_symmetric isomorphism_symmetric.................proved - complete [shostak](0.34 s) Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.34 s) Proof summary for theory isomorphism_transitive isomorphism_transitive................proved - complete [shostak](0.06 s) Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.06 s) Proof summary for theory kuratowski kuratowski............................proved - complete [shostak](0.07 s) Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.07 s) Proof summary for theory monotone_functions increasing_is_nondecreasing...........proved - complete [shostak](0.13 s) decreasing_is_nonincreasing...........proved - complete [shostak](0.14 s) not_increasing_and_nonincreasing......proved - complete [shostak](0.35 s) not_decreasing_and_nondecreasing......proved - complete [shostak](0.35 s) increasing_converse_decreasing1.......proved - complete [shostak](0.20 s) increasing_converse_decreasing2.......proved - complete [shostak](-.59 s) nonincreasing_converse_nondecreasing1...proved - complete [shostak](0.17 s) nonincreasing_converse_nondecreasing2...proved - complete [shostak](0.17 s) increasing_total_order_injective......proved - complete [shostak](0.17 s) increasing_strict_total_order_injective...proved - complete [shostak](0.15 s) decreasing_total_order_injective......proved - complete [shostak](0.17 s) decreasing_strict_total_order_injective...proved - complete [shostak](0.15 s) Theory totals: 12 formulas, 12 attempted, 12 succeeded (1.56 s) Proof summary for theory order_strength stronger_reflexive....................proved - complete [shostak](0.03 s) weaker_irreflexive....................proved - complete [shostak](0.04 s) weaker_antisymmetric..................proved - complete [shostak](0.04 s) Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.12 s) Proof summary for theory ordered_int upto_has_greatest.....................proved - complete [shostak](0.10 s) below_has_greatest....................proved - complete [shostak](0.11 s) above_has_least.......................proved - complete [shostak](0.12 s) upfrom_has_least......................proved - complete [shostak](0.11 s) prefix_empty..........................proved - incomplete [shostak](0.44 s) prefix_below..........................proved - incomplete [shostak](0.71 s) prefix_upto...........................proved - incomplete [shostak](0.76 s) suffix_empty..........................proved - incomplete [shostak](0.46 s) suffix_upfrom.........................proved - incomplete [shostak](0.67 s) suffix_above..........................proved - incomplete [shostak](0.76 s) unrelated_empty.......................proved - complete [shostak](0.10 s) Theory totals: 11 formulas, 11 attempted, 11 succeeded (4.35 s) Proof summary for theory ordered_nat upto_has_greatest.....................proved - complete [shostak](0.09 s) above_has_least.......................proved - complete [shostak](0.09 s) upfrom_has_least......................proved - complete [shostak](0.09 s) nonzero_below_greatest................proved - complete [shostak](0.49 s) upto_greatest.........................proved - complete [shostak](0.65 s) above_least...........................proved - complete [shostak](0.57 s) upfrom_least..........................proved - complete [shostak](0.65 s) below_prelude.........................proved - complete [shostak](0.52 s) upto_prelude..........................proved - complete [shostak](0.61 s) prefix_finite.........................proved - complete [shostak](0.08 s) prefix_below..........................proved - incomplete [shostak](1.26 s) prefix_upto_TCC1......................proved - complete [shostak](0.05 s) prefix_upto...........................proved - incomplete [shostak](0.48 s) below_is_finite.......................proved - complete [shostak](0.53 s) upto_is_finite........................proved - complete [shostak](0.64 s) below_card............................proved - complete [shostak](0.78 s) upto_card.............................proved - complete [shostak](0.79 s) suffix_empty..........................proved - incomplete [shostak](0.46 s) suffix_upfrom.........................proved - complete [shostak](0.65 s) suffix_above..........................proved - complete [shostak](0.65 s) unrelated_empty.......................proved - complete [shostak](0.08 s) prefix_finite_full....................proved - incomplete [shostak](0.53 s) prefix_bijective......................proved - incomplete [shostak](0.95 s) Theory totals: 23 formulas, 23 attempted, 23 succeeded (11.72 s) Proof summary for theory range range_TCC1............................proved - complete [shostak](0.05 s) min_range_TCC1........................proved - complete [shostak](0.40 s) max_range_TCC1........................proved - complete [shostak](0.40 s) c_range_TCC1..........................proved - complete [shostak](0.53 s) o_range_TCC1..........................proved - complete [shostak](0.30 s) c_range_is_nonempty...................proved - complete [shostak](1.09 s) oc_range_is_nonempty..................proved - complete [shostak](2.25 s) co_range_is_nonempty..................proved - complete [shostak](3.39 s) closed_range_TCC1.....................proved - complete [shostak](0.34 s) nontrivial_closed_range_TCC1..........proved - complete [shostak](0.64 s) open_closed_range_TCC1................proved - complete [shostak](0.15 s) closed_open_range_TCC1................proved - complete [shostak](0.15 s) open_range_TCC1.......................proved - complete [shostak](0.17 s) nontrivial_open_range_TCC1............proved - complete [shostak](0.22 s) open_closed_range_TCC2................proved - complete [shostak](0.65 s) closed_open_range_TCC2................proved - complete [shostak](0.65 s) left_open_range_TCC1..................proved - complete [shostak](0.38 s) right_open_range_TCC1.................proved - complete [shostak](0.38 s) c_range_construction..................proved - complete [shostak](0.08 s) ntc_range_construction................proved - complete [shostak](0.31 s) c_range_endpoints.....................proved - complete [shostak](0.54 s) ntc_range_endpoints...................proved - complete [shostak](0.03 s) c_range_min...........................proved - complete [shostak](0.25 s) c_range_max...........................proved - complete [shostak](0.25 s) ntc_range_min.........................proved - complete [shostak](0.26 s) ntc_range_max.........................proved - complete [shostak](0.25 s) oc_range_max1.........................proved - complete [shostak](0.25 s) oc_range_max2.........................proved - complete [shostak](0.25 s) co_range_min1.........................proved - complete [shostak](0.25 s) co_range_min2.........................proved - complete [shostak](0.25 s) Theory totals: 30 formulas, 30 attempted, 30 succeeded (15.12 s) Proof summary for theory range_real real_no_minimum.......................proved - complete [shostak](0.06 s) real_no_maximum.......................proved - complete [shostak](0.06 s) ntc_range_infinite....................proved - complete [shostak](1.07 s) nto_range_infinite....................proved - complete [shostak](0.53 s) Theory totals: 4 formulas, 4 attempted, 4 succeeded (1.72 s) Proof summary for theory set_antisymmetric inj_inj_bij...........................proved - complete [shostak](0.17 s) surj_surj_bij.........................proved - complete [shostak](0.06 s) inj_surj_bij..........................proved - complete [shostak](0.04 s) Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.26 s) Proof summary for theory set_dichotomous injection_order_TCC1..................proved - complete [shostak](0.03 s) partial_injection_order...............proved - complete [shostak](0.64 s) injective_or_surjective...............proved - complete [shostak](0.75 s) injective_dichotomous.................proved - complete [shostak](0.59 s) surjective_dichotomous................proved - complete [shostak](0.26 s) Theory totals: 5 formulas, 5 attempted, 5 succeeded (2.27 s) Proof summary for theory similarity similarity_is_isomorphism.............proved - complete [shostak](0.07 s) similar_is_isomorphic.................proved - complete [shostak](0.04 s) Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.11 s) Proof summary for theory similarity_props similarity_greatest...................proved - complete [shostak](0.11 s) similar_has_greatest..................proved - complete [shostak](0.10 s) similarity_least......................proved - complete [shostak](0.12 s) similar_has_least.....................proved - complete [shostak](0.10 s) similar_finite_TCC1...................proved - complete [shostak](0.08 s) similar_finite_TCC2...................proved - complete [shostak](0.09 s) similar_finite........................proved - incomplete [shostak](2.01 s) Theory totals: 7 formulas, 7 attempted, 7 succeeded (2.62 s) Proof summary for theory well_nat well_lt_nat...........................proved - complete [shostak](0.26 s) well_gt_nat...........................proved - incomplete [shostak](2.13 s) Theory totals: 2 formulas, 2 attempted, 2 succeeded (2.39 s) Proof summary for theory well_ordered_finite nonempty_has_least....................proved - incomplete [shostak](0.49 s) finite_well_ordered...................proved - incomplete [shostak](0.23 s) nonlast_has_next......................proved - incomplete [shostak](0.35 s) nonfirst_has_prev.....................proved - incomplete [shostak](0.93 s) finite_last...........................proved - incomplete [shostak](0.28 s) Theory totals: 5 formulas, 5 attempted, 5 succeeded (2.28 s) Proof summary for theory well_ordered_traversal well_ordering_has_first...............proved - complete [shostak](0.10 s) first_TCC1............................proved - complete [shostak](0.02 s) last_TCC1.............................proved - complete [shostak](0.21 s) well_ordering_has_next................proved - complete [shostak](0.26 s) next_TCC1.............................proved - complete [shostak](0.03 s) last_no_next..........................proved - complete [shostak](0.13 s) last_is_last..........................proved - complete [shostak](0.29 s) well_ordering_has_prev................proved - complete [shostak](0.37 s) prev_TCC1.............................proved - complete [shostak](0.03 s) Theory totals: 9 formulas, 9 attempted, 9 succeeded (1.43 s) Proof summary for theory well_ordered_props induced_prefixes......................proved - complete [shostak](0.09 s) increasing_well_ordered...............proved - complete [shostak](0.06 s) initial_segment_isomorphism...........proved - complete [shostak](0.55 s) Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.70 s) Proof summary for theory well_ordering ordered_set_order_TCC1................proved - complete [shostak](0.04 s) ordered_set_order_TCC2................proved - complete [shostak](0.03 s) ordered_set_order_TCC3................proved - complete [shostak](0.05 s) partial_ordered_set...................proved - complete [shostak](4.19 s) ordered_set_union_TCC1................proved - complete [shostak](-.49 s) chain_upper_bound.....................proved - complete [shostak](0.73 s) well_ordering.........................proved - complete [shostak](0.41 s) Theory totals: 7 formulas, 7 attempted, 7 succeeded (4.96 s) Proof summary for theory directed_orders directed_def..........................proved - complete [shostak](0.25 s) directed_least_bounded_above..........proved - complete [shostak](0.10 s) dcpo_is_po............................proved - complete [shostak](0.14 s) complete_upper_semilattice_is_dcpo....proved - complete [shostak](0.11 s) pdcpo_is_dcpo.........................proved - complete [shostak](0.09 s) pdcpo_is_ccpo.........................proved - complete [shostak](0.48 s) Theory totals: 6 formulas, 6 attempted, 6 succeeded (1.17 s) Proof summary for theory bounded_order_props singleton_is_lub_set..................proved - complete [shostak](0.05 s) lub_TCC1..............................proved - complete [shostak](0.13 s) lub_rew_TCC1..........................proved - complete [shostak](0.06 s) lub_rew...............................proved - complete [shostak](0.06 s) lub_singleton.........................proved - complete [shostak](0.06 s) lub_lem...............................proved - complete [shostak](0.04 s) above_lub.............................proved - complete [shostak](0.06 s) singleton_is_glb_set..................proved - complete [shostak](0.04 s) glb_TCC1..............................proved - complete [shostak](0.14 s) glb_rew_TCC1..........................proved - complete [shostak](0.05 s) glb_rew...............................proved - complete [shostak](0.05 s) glb_singleton.........................proved - complete [shostak](0.06 s) glb_lem...............................proved - complete [shostak](0.04 s) below_glb.............................proved - complete [shostak](0.05 s) Theory totals: 14 formulas, 14 attempted, 14 succeeded (0.90 s) Proof summary for theory directed_order_props directed_is_lub_set...................proved - complete [shostak](0.03 s) directed_singleton....................proved - complete [shostak](0.03 s) intersection_directed_upper...........proved - complete [shostak](0.06 s) split_directed_lower..................proved - complete [shostak](0.05 s) directed_union_lower..................proved - complete [shostak](0.12 s) Theory totals: 5 formulas, 5 attempted, 5 succeeded (0.30 s) Proof summary for theory partial_order_props partial_order_reflexive...............proved - complete [shostak](0.02 s) partial_order_antisymmetric...........proved - complete [shostak](0.03 s) partial_order_transitive..............proved - complete [shostak](0.02 s) lower_set_TCC1........................proved - complete [shostak](0.03 s) upper_set_TCC1........................proved - complete [shostak](0.02 s) lower_sets_TCC1.......................proved - complete [shostak](0.02 s) upper_sets_TCC1.......................proved - complete [shostak](0.03 s) complement_lower_set..................proved - complete [shostak](0.03 s) complement_upper_set..................proved - complete [shostak](0.03 s) Complement_lower_sets.................proved - complete [shostak](0.03 s) Complement_upper_sets.................proved - complete [shostak](0.03 s) down_TCC1.............................proved - complete [shostak](0.03 s) up_TCC1...............................proved - complete [shostak](0.03 s) down_subset...........................proved - complete [shostak](0.04 s) up_subset.............................proved - complete [shostak](0.03 s) lower_set_def.........................proved - complete [shostak](0.08 s) upper_set_def.........................proved - complete [shostak](0.07 s) Union_lower_set.......................proved - complete [shostak](0.04 s) Union_upper_set.......................proved - complete [shostak](0.05 s) Intersection_lower_set................proved - complete [shostak](0.04 s) Intersection_upper_set................proved - complete [shostak](0.04 s) union_lower_set.......................proved - complete [shostak](0.03 s) union_upper_set.......................proved - complete [shostak](0.04 s) intersection_lower_set................proved - complete [shostak](0.03 s) intersection_upper_set................proved - complete [shostak](0.04 s) Theory totals: 25 formulas, 25 attempted, 25 succeeded (0.90 s) Proof summary for theory lift_props down_up...............................proved - complete [shostak](0.02 s) up_down...............................proved - complete [shostak](0.04 s) down_equal............................proved - complete [shostak](0.04 s) up_equal..............................proved - complete [shostak](0.03 s) Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.13 s) Proof summary for theory lifted_orders lift_preserves_reflexive..............proved - complete [shostak](0.03 s) lift_preserves_transitive.............proved - complete [shostak](0.06 s) lift_preserves_antisymmetric..........proved - complete [shostak](0.05 s) lift_preserves_preorder...............proved - complete [shostak](0.04 s) lift_preserves_partial_order..........proved - complete [shostak](0.04 s) lift_lub_emptyset_TCC1................proved - complete [shostak](0.16 s) lift_lub_emptyset.....................proved - complete [shostak](0.17 s) lift_lub_bounded_TCC1.................proved - complete [shostak](0.25 s) lift_lub_bounded_TCC2.................proved - complete [shostak](0.20 s) lift_lub_bounded......................proved - complete [shostak](0.27 s) lift_preserves_directed_complete......proved - complete [shostak](0.34 s) lift_preserves_directed_complete_partial_order...proved - complete [shostak](0.21 s) Theory totals: 12 formulas, 12 attempted, 12 succeeded (1.84 s) Proof summary for theory partial_order_lift lift_TCC1.............................proved - complete [shostak](0.25 s) lift_TCC2.............................proved - complete [shostak](0.25 s) lift_TCC3.............................proved - complete [shostak](0.42 s) Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.92 s) Proof summary for theory sum_orders sum_preserves_reflexive...............proved - complete [shostak](0.05 s) sum_preserves_transitive..............proved - complete [shostak](0.09 s) sum_preserves_antisymmetric...........proved - complete [shostak](0.10 s) sum_preserves_preorder................proved - complete [shostak](0.04 s) sum_preserves_partial_order...........proved - complete [shostak](0.04 s) sum_preserves_directed_complete.......proved - complete [shostak](0.79 s) sum_preserves_directed_complete_partial_order...proved - complete [shostak](0.21 s) Theory totals: 7 formulas, 7 attempted, 7 succeeded (1.32 s) Proof summary for theory product_orders product_preserves_reflexive...........proved - complete [shostak](0.04 s) product_preserves_transitive..........proved - complete [shostak](0.04 s) product_preserves_antisymmetric.......proved - complete [shostak](0.05 s) product_preserves_preorder............proved - complete [shostak](0.03 s) product_preserves_partial_order.......proved - complete [shostak](0.04 s) product_preserves_directed_complete...proved - complete [shostak](0.29 s) product_preserves_directed_complete_partial_order...proved - complete [shostak](0.1 product_lub_TCC1......................proved - complete [shostak](0.25 s) product_lub_TCC2......................proved - complete [shostak](0.31 s) product_lub_TCC3......................proved - complete [shostak](0.31 s) product_lub...........................proved - complete [shostak](0.47 s) product_preserves_has_least...........proved - complete [shostak](0.27 s) product_preserves_pointed_directed_complete_partial_order...proved - complete [shos product_least_TCC1....................proved - complete [shostak](0.33 s) product_least_TCC2....................proved - complete [shostak](0.53 s) product_least_TCC3....................proved - complete [shostak](0.52 s) product_least.........................proved - complete [shostak](0.41 s) Theory totals: 17 formulas, 17 attempted, 17 succeeded (4.33 s) Proof summary for theory mucalculus_prop antisymmetry..........................proved - complete [shostak](0.05 s) reflexivity...........................proved - complete [shostak](0.02 s) glb_lower_bound.......................proved - complete [shostak](0.04 s) glb_greatest_lower_bound..............proved - complete [shostak](0.06 s) lub_upper_bound.......................proved - complete [shostak](0.03 s) lub_least_upper_bound.................proved - complete [shostak](0.06 s) closure_mu............................proved - complete [shostak](0.07 s) smallest_closed.......................proved - complete [shostak](0.02 s) fixpoint_mu1..........................proved - complete [shostak](0.04 s) fixpoint_mu2..........................proved - complete [shostak](0.02 s) least_fixpoint1.......................proved - complete [shostak](0.03 s) least_fixpoint2.......................proved - complete [shostak](0.02 s) mu_lfp................................proved - complete [shostak](0.04 s) closure_nu............................proved - complete [shostak](0.07 s) largest_closed........................proved - complete [shostak](0.02 s) fixpoint_nu1..........................proved - complete [shostak](0.04 s) fixpoint_nu2..........................proved - complete [shostak](0.02 s) greatest_fixpoint1....................proved - complete [shostak](0.03 s) greatest_fixpoint2....................proved - complete [shostak](0.02 s) nu_gfp................................proved - complete [shostak](0.04 s) dual_dual.............................proved - complete [shostak](0.04 s) dual_inclusion1.......................proved - complete [shostak](0.05 s) --> -------------------- --> maximum size reached --> -------------------- [ zur Elbe Produktseite wechseln0.212Quellennavigators ] |