Quellcode-Bibliothek
© Kompilation durch diese Firma
[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]
Datei:
scott_continuity.prf
Sprache: Lisp
Untersuchungsergebnis.summary Download desMT940 {MT940[368] Hlasm[1524] Haskell[1884]}zum Wurzelverzeichnis wechseln
***
*** top (18:56:40 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 digraphs
empty_digraph_TCC1....................proved - complete [shostak](0.02 s)
edges_vert............................proved - complete [shostak](0.02 s)
other_vert............................proved - complete [shostak](0.02 s)
edges_to_pair.........................proved - complete [shostak](0.02 s)
empty?_rew............................proved - complete [shostak](0.01 s)
empty_size............................proved - complete [shostak](0.01 s)
edges_of_empty........................proved - complete [shostak](0.03 s)
singleton_edges.......................proved - complete [shostak](0.03 s)
edge_in_card_gt_1.....................proved - complete [shostak](0.10 s)
not_singleton_2_vert..................proved - complete [shostak](0.02 s)
proj_rew..............................proved - complete [shostak](0.01 s)
singleton_digraph_TCC1................proved - complete [shostak](0.00 s)
is_sing...............................proved - complete [shostak](0.01 s)
Theory totals: 13 formulas, 13 attempted, 13 succeeded (0.30 s)
Proof summary for theory pairs
mk_pair_eq............................proved - complete [shostak](0.01 s)
apair_irreflexive.....................proved - complete [shostak](0.00 s)
Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.01 s)
Proof summary for theory digraph_deg
incoming_edges_TCC1...................proved - complete [shostak](0.05 s)
outgoing_edges_TCC1...................proved - complete [shostak](0.05 s)
incident_edges_TCC1...................proved - complete [shostak](0.02 s)
incoming_edges_subset.................proved - complete [shostak](0.02 s)
outgoing_edges_subset.................proved - complete [shostak](0.01 s)
incident_edges_subset.................proved - complete [shostak](0.02 s)
incoming_edges_emptyset...............proved - complete [shostak](0.01 s)
outgoing_edges_emptyset...............proved - complete [shostak](0.01 s)
incident_edges_emptyset...............proved - complete [shostak](0.00 s)
deg_del_edge_incoming.................proved - complete [shostak](0.12 s)
deg_del_edge_outgoing.................proved - complete [shostak](0.10 s)
deg_del_non_edge......................proved - complete [shostak](0.12 s)
deg_del_non_edge_incoming.............proved - complete [shostak](0.05 s)
deg_del_non_edge_outgoing.............proved - complete [shostak](0.04 s)
deg_del_edge..........................proved - complete [shostak](0.07 s)
deg_del_self_loop.....................proved - complete [shostak](0.06 s)
deg_del_edge_ge_incoming..............proved - complete [shostak](0.03 s)
deg_del_edge_ge_outgoing..............proved - complete [shostak](0.03 s)
deg_del_edge_ge.......................proved - complete [shostak](0.05 s)
deg_del_edge_le_incoming..............proved - complete [shostak](0.04 s)
deg_del_edge_le_outgoing..............proved - complete [shostak](0.03 s)
deg_del_edge_le.......................proved - complete [shostak](0.05 s)
in_deg_edge_exists....................proved - complete [shostak](0.02 s)
out_deg_edge_exists...................proved - complete [shostak](0.02 s)
deg_edge_exists.......................proved - complete [shostak](0.05 s)
deg_to_card...........................proved - complete [shostak](0.13 s)
del_vert_deg_0........................proved - complete [shostak](0.08 s)
singleton_loops.......................proved - complete [shostak](0.03 s)
singleton_edges.......................proved - complete [shostak](0.04 s)
singleton_deg.........................proved - complete [shostak](0.01 s)
in_deg_1_sing.........................proved - complete [shostak](0.03 s)
out_deg_1_sing........................proved - complete [shostak](0.04 s)
deg_1_sing............................proved - complete [shostak](0.27 s)
deg_1_in_out..........................proved - complete [shostak](0.04 s)
deg_1_edge............................proved - complete [shostak](0.11 s)
Theory totals: 35 formulas, 35 attempted, 35 succeeded (1.85 s)
Proof summary for theory digraph_ops
union_TCC1............................proved - complete [shostak](0.03 s)
del_vert_TCC1.........................proved - complete [shostak](0.02 s)
del_vert_TCC2.........................proved - complete [shostak](0.04 s)
del_edge_TCC1.........................proved - complete [shostak](0.01 s)
del_vert_still_in.....................proved - complete [shostak](0.02 s)
size_del_vert.........................proved - complete [shostak](0.03 s)
del_vert_le...........................proved - complete [shostak](0.03 s)
del_vert_ge...........................proved - complete [shostak](0.03 s)
edge_in_del_vert......................proved - complete [shostak](0.01 s)
edges_del_vert........................proved - complete [shostak](0.01 s)
del_vert_comm.........................proved - complete [shostak](0.06 s)
del_vert_empty?.......................proved - complete [shostak](0.03 s)
del_edge_lem..........................proved - complete [shostak](0.01 s)
del_edge_lem2.........................proved - complete [shostak](0.02 s)
del_edge_lem3.........................proved - complete [shostak](0.02 s)
del_edge_lem5.........................proved - complete [shostak](0.03 s)
vert_del_edge.........................proved - complete [shostak](0.00 s)
del_edge_num..........................proved - complete [shostak](0.06 s)
del_edge_singleton....................proved - complete [shostak](0.02 s)
del_vert_edge_comm....................proved - complete [shostak](0.05 s)
del_vert_edge.........................proved - complete [shostak](0.06 s)
Theory totals: 21 formulas, 21 attempted, 21 succeeded (0.57 s)
Proof summary for theory walks
walk?_TCC1............................proved - complete [shostak](0.03 s)
walk?_TCC2............................proved - complete [shostak](0.05 s)
from?_TCC1............................proved - complete [shostak](0.01 s)
from?_TCC2............................proved - complete [shostak](0.00 s)
verts_of_TCC1.........................proved - complete [shostak](0.27 s)
edges_of_TCC1.........................proved - complete [shostak](0.00 s)
edges_of_TCC2.........................proved - complete [shostak](0.01 s)
edges_of_TCC3.........................proved - complete [shostak](0.10 s)
walk_from_l...........................proved - complete [shostak](0.03 s)
verts_in?_concat_TCC1.................proved - complete [shostak](0.05 s)
verts_in?_concat......................proved - complete [shostak](0.09 s)
verts_in?_caret_TCC1..................proved - complete [shostak](0.11 s)
verts_in?_caret.......................proved - complete [shostak](0.34 s)
vert_seq_lem..........................proved - complete [shostak](0.02 s)
verts_of_subset.......................proved - complete [shostak](0.03 s)
edges_of_subset.......................proved - complete [shostak](0.06 s)
walk_verts_in.........................proved - complete [shostak](0.02 s)
walk_from_vert........................proved - complete [shostak](0.03 s)
walk_edge_in..........................proved - complete [shostak](0.20 s)
prewalk_across_TCC1...................proved - complete [shostak](0.01 s)
prewalk_across_TCC2...................proved - complete [shostak](0.01 s)
prewalk_across_TCC3...................proved - complete [shostak](0.02 s)
prewalk_across_TCC4...................proved - complete [shostak](0.02 s)
prewalk_across........................proved - complete [shostak](0.08 s)
gen_seq1_TCC1.........................proved - complete [shostak](0.01 s)
gen_seq2_TCC1.........................proved - complete [shostak](0.01 s)
trunc1_TCC1...........................proved - complete [shostak](0.01 s)
trunc1_TCC2...........................proved - complete [shostak](0.09 s)
add1_TCC1.............................proved - complete [shostak](0.01 s)
gen_seq1_is_walk......................proved - complete [shostak](0.01 s)
edge_to_walk_TCC1.....................proved - complete [shostak](0.03 s)
edge_to_walk_TCC2.....................proved - complete [shostak](0.01 s)
edge_to_walk..........................proved - complete [shostak](0.04 s)
walk?_caret_TCC1......................proved - complete [shostak](0.17 s)
walk?_caret...........................proved - complete [shostak](0.19 s)
l_trunc1_TCC1.........................proved - complete [shostak](0.01 s)
l_trunc1..............................proved - complete [shostak](0.08 s)
walk?_add1............................proved - complete [shostak](0.09 s)
walk_concat_edge_TCC1.................proved - complete [shostak](0.08 s)
walk_concat_edge......................proved - complete [shostak](0.25 s)
walk_concat_TCC1......................proved - complete [shostak](0.11 s)
walk_concat_TCC2......................proved - complete [shostak](0.15 s)
walk_concat...........................proved - complete [shostak](0.44 s)
walk?_cut_TCC1........................proved - complete [shostak](0.04 s)
walk?_cut_TCC2........................proved - complete [shostak](0.24 s)
walk?_cut.............................proved - complete [shostak](1.02 s)
walk_merge............................proved - complete [shostak](0.07 s)
reord_prewalk_TCC1....................proved - complete [shostak](0.01 s)
reord_prewalk_TCC2....................proved - complete [shostak](0.01 s)
reord_prewalk_TCC3....................proved - complete [shostak](0.23 s)
eq_relation_eq_prewalk................proved - complete [shostak](6.44 s)
eq_prewalk_length.....................proved - complete [shostak](0.22 s)
subwalk_is_walk.......................proved - complete [shostak](0.11 s)
walk_o_TCC1...........................proved - complete [shostak](0.05 s)
walk_o_TCC2...........................proved - complete [shostak](0.04 s)
walk_o_TCC3...........................proved - complete [shostak](0.21 s)
walk_o................................proved - complete [shostak](0.62 s)
edges_o_walk_TCC1.....................proved - complete [shostak](0.04 s)
edges_o_walk_TCC2.....................proved - complete [shostak](0.04 s)
edges_o_walk_TCC3.....................proved - complete [shostak](0.22 s)
edges_o_walk..........................proved - complete [shostak](0.65 s)
Theory totals: 61 formulas, 61 attempted, 61 succeeded (13.66 s)
Proof summary for theory paths
path?_verts...........................proved - complete [shostak](0.03 s)
path_from_l...........................proved - complete [shostak](0.03 s)
path_from_in..........................proved - complete [shostak](0.05 s)
path?_caret_TCC1......................proved - complete [shostak](0.19 s)
path?_caret...........................proved - complete [shostak](0.35 s)
path_from?_caret_TCC1.................proved - complete [shostak](0.21 s)
path_from?_caret_TCC2.................proved - complete [shostak](0.13 s)
path_from?_caret......................proved - complete [shostak](0.14 s)
path?_gen_seq2........................proved - complete [shostak](0.08 s)
path?_add1_TCC1.......................proved - complete [shostak](0.06 s)
path?_add1............................proved - complete [shostak](0.15 s)
path?_trunc1_TCC1.....................proved - complete [shostak](0.08 s)
path?_trunc1_TCC2.....................proved - complete [shostak](0.05 s)
path?_trunc1_TCC3.....................proved - complete [shostak](0.09 s)
path?_trunc1..........................proved - complete [shostak](0.14 s)
Theory totals: 15 formulas, 15 attempted, 15 succeeded (1.80 s)
Proof summary for theory path_ops
walk?_del_vert........................proved - complete [shostak](0.13 s)
walk?_del_vert_not....................proved - complete [shostak](0.11 s)
path?_del_vert........................proved - complete [shostak](0.04 s)
path?_del_verts.......................proved - complete [shostak](0.11 s)
walk_to_path..........................proved - complete [shostak](0.51 s)
walk_to_path_from.....................proved - complete [shostak](0.30 s)
Theory totals: 6 formulas, 6 attempted, 6 succeeded (1.21 s)
Proof summary for theory di_subgraphs
finite_vert_subset....................proved - complete [shostak](0.02 s)
finite_edge_subset....................proved - complete [shostak](0.02 s)
di_subgraph_TCC1......................proved - complete [shostak](0.02 s)
di_subgraph_TCC2......................proved - complete [shostak](0.00 s)
di_subgraph_TCC3......................proved - complete [shostak](0.03 s)
di_subgraph_vert_sub..................proved - complete [shostak](0.03 s)
di_subgraph_lem.......................proved - complete [shostak](0.00 s)
di_subgraph_smaller...................proved - complete [shostak](0.03 s)
Theory totals: 8 formulas, 8 attempted, 8 succeeded (0.16 s)
Proof summary for theory sep_sets
del_verts_TCC1........................proved - complete [shostak](0.05 s)
del_verts_TCC2........................proved - complete [shostak](0.02 s)
sep_set_exists........................proved - complete [shostak](0.43 s)
min_sep_set_TCC1......................proved - complete [shostak](0.02 s)
min_sep_set_edge......................proved - complete [shostak](0.06 s)
min_sep_set_card......................proved - complete [shostak](0.16 s)
min_sep_set_seps......................proved - complete [shostak](0.05 s)
min_sep_set_vert......................proved - complete [shostak](0.23 s)
ends_not_in_min_sep_set...............proved - complete [shostak](0.02 s)
walk?_del_verts_not...................proved - complete [shostak](0.23 s)
adj_verts_TCC1........................proved - complete [shostak](0.20 s)
Theory totals: 11 formulas, 11 attempted, 11 succeeded (1.46 s)
Proof summary for theory abstract_min
prep0.................................proved - complete [shostak](0.01 s)
min_f_TCC1............................proved - complete [shostak](0.00 s)
prep1.................................proved - complete [shostak](0.03 s)
min_TCC1..............................proved - complete [shostak](0.04 s)
min_def...............................proved - complete [shostak](0.00 s)
min_in................................proved - complete [shostak](0.00 s)
min_is_min............................proved - complete [shostak](0.01 s)
Theory totals: 7 formulas, 7 attempted, 7 succeeded (0.08 s)
Proof summary for theory walk_inductions
walk_prep.............................proved - complete [shostak](0.14 s)
digraph_induction_walk................proved - complete [shostak](0.02 s)
Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.16 s)
Proof summary for theory dags
dag_no_self_loops.....................proved - complete [shostak](0.15 s)
Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.15 s)
Proof summary for theory circuits
pre_circuit?_TCC1.....................proved - complete [shostak](0.05 s)
pre_circuit?_TCC2.....................proved - complete [shostak](0.05 s)
eq_circuit?_TCC1......................proved - complete [shostak](0.20 s)
eq_circuit?_TCC2......................proved - complete [shostak](0.20 s)
eq_circuit_length.....................proved - complete [shostak](0.12 s)
eq_circuit_reflexive..................proved - complete [shostak](0.01 s)
eq_circuit_symmetric..................proved - complete [shostak](0.01 s)
loop_is_circuit.......................proved - complete [shostak](0.02 s)
equal_rest_equal_circuit..............proved - complete [shostak](0.41 s)
equal_eq_circuit......................proved - complete [shostak](0.02 s)
circuit_equal_fisrt_TCC1..............proved - complete [shostak](0.26 s)
circuit_equal_fisrt_TCC2..............proved - complete [shostak](0.26 s)
circuit_equal_fisrt_TCC3..............proved - complete [shostak](0.26 s)
circuit_equal_fisrt...................proved - complete [shostak](0.21 s)
comp_circuit_inter_TCC1...............proved - complete [shostak](0.15 s)
comp_circuit_inter....................proved - complete [shostak](0.23 s)
eq_circuit_position_TCC1..............proved - complete [shostak](0.30 s)
eq_circuit_position...................proved - complete [shostak](2.95 s)
eq_circuit_edges......................proved - complete [shostak](5.07 s)
commuted_circuit_TCC1.................proved - complete [shostak](0.05 s)
commuted_circuit_TCC2.................proved - complete [shostak](0.25 s)
commuted_circuit......................proved - complete [shostak](1.21 s)
commuted_circuit_is_eq................proved - complete [shostak](3.62 s)
Theory totals: 23 formulas, 23 attempted, 23 succeeded (15.93 s)
Proof summary for theory cycles
cycle?_TCC1...........................proved - complete [shostak](0.08 s)
cycle?_TCC2...........................proved - complete [shostak](0.07 s)
cycle_is_circuit......................proved - complete [shostak](0.04 s)
circuit_subwalk_cycle_TCC1............proved - complete [shostak](0.10 s)
circuit_subwalk_cycle.................proved - complete [shostak](1.75 s)
cycle_prefix_TCC1.....................proved - complete [shostak](0.12 s)
cycle_prefix..........................proved - complete [shostak](0.94 s)
cycle_o_circuit_TCC1..................proved - complete [shostak](0.26 s)
cycle_o_circuit.......................proved - complete [shostak](0.53 s)
Pigeon_hole...........................proved - incomplete [shostak](0.22 s)
Theory totals: 10 formulas, 10 attempted, 10 succeeded (4.13 s)
Proof summary for theory di_subgraphs_from_walk
G_from_TCC1...........................proved - complete [shostak](0.15 s)
G_from_vert...........................proved - complete [shostak](0.01 s)
vert_G_from...........................proved - complete [shostak](0.02 s)
edge?_G_from_TCC1.....................proved - complete [shostak](0.01 s)
edge?_G_from_TCC2.....................proved - complete [shostak](0.05 s)
edge?_G_from..........................proved - complete [shostak](0.07 s)
vert_G_from_not.......................proved - complete [shostak](0.03 s)
del_vert_di_subgraph..................proved - complete [shostak](0.32 s)
Theory totals: 8 formulas, 8 attempted, 8 succeeded (0.66 s)
Proof summary for theory max_di_subgraphs
prep0.................................proved - complete [shostak](0.02 s)
max_size_TCC1.........................proved - complete [shostak](0.05 s)
prep..................................proved - complete [shostak](0.07 s)
max_di_subgraph_TCC1..................proved - complete [shostak](0.12 s)
max_di_subgraph_def...................proved - complete [shostak](0.01 s)
max_di_subgraph_in....................proved - complete [shostak](0.01 s)
max_di_subgraph_is_max................proved - complete [shostak](0.02 s)
Theory totals: 7 formulas, 7 attempted, 7 succeeded (0.30 s)
Proof summary for theory max_upto
max_TCC1..............................proved - complete [shostak](0.12 s)
max_def...............................proved - complete [shostak](0.03 s)
max_lem...............................proved - complete [shostak](0.02 s)
Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.17 s)
Proof summary for theory min_lem
min_lem...............................proved - complete [shostak](0.01 s)
Theory totals: 1 formulas, 1 attempted, 1 succeeded (0.01 s)
Proof summary for theory max_subtrees
sing_is_tree..........................proved - complete [shostak](0.03 s)
tree_in...............................proved - complete [shostak](0.12 s)
max_subtree_TCC1......................proved - complete [shostak](0.02 s)
max_subtree_TCC2......................proved - complete [shostak](0.07 s)
max_subtree_tree......................proved - complete [shostak](0.06 s)
max_subtree_di_subgraph...............proved - complete [shostak](0.01 s)
max_subtree_max.......................proved - complete [shostak](0.07 s)
Theory totals: 7 formulas, 7 attempted, 7 succeeded (0.38 s)
Proof summary for theory trees
tree?_TCC1............................proved - complete [shostak](0.04 s)
tree_nonempty.........................proved - complete [shostak](0.06 s)
Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.10 s)
Proof summary for theory doubletons
dbl_comm..............................proved - complete [shostak](0.01 s)
doubleton_irreflexive.................proved - complete [shostak](0.01 s)
doubleton_nonempty....................proved - complete [shostak](0.02 s)
doubleton_rest_nonempty...............proved - complete [shostak](0.02 s)
dbl_choose_TCC1.......................proved - complete [shostak](0.01 s)
dbl_choose............................proved - complete [shostak](0.02 s)
dbl_rest_choose_TCC1..................proved - complete [shostak](0.01 s)
dbl_rest_choose.......................proved - complete [shostak](0.10 s)
dbl_to_pair_TCC1......................proved - complete [shostak](0.03 s)
dbl_def...............................proved - complete [shostak](0.01 s)
dbl_in................................proved - complete [shostak](0.00 s)
dbl_not_in............................proved - complete [shostak](0.01 s)
dbl_to_pair_lem_TCC1..................proved - complete [shostak](0.01 s)
dbl_to_pair_lem.......................proved - complete [shostak](0.08 s)
dbl_to_pair_inverse_l.................proved - complete [shostak](0.01 s)
dbl_proj..............................proved - complete [shostak](0.01 s)
proj_dbl..............................proved - complete [shostak](0.02 s)
dbl_eq................................proved - complete [shostak](0.03 s)
finite_dbl............................proved - complete [shostak](0.04 s)
Theory totals: 19 formulas, 19 attempted, 19 succeeded (0.48 s)
Proof summary for theory subtrees
walk_acr_TCC1.........................proved - complete [shostak](0.05 s)
walk_acr_TCC2.........................proved - complete [shostak](0.09 s)
walk_acr_TCC3.........................proved - complete [shostak](0.10 s)
walk_acr..............................proved - complete [shostak](0.13 s)
walk_acr2.............................proved - complete [shostak](0.14 s)
add_pair..............................proved - complete [shostak](0.02 s)
max_tree_all_verts....................proved - complete [shostak](1.06 s)
Theory totals: 7 formulas, 7 attempted, 7 succeeded (1.59 s)
Proof summary for theory digraph_conn_defs
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory min_walk_reduced
reduced?_TCC1.........................proved - complete [shostak](0.01 s)
reduced?_TCC2.........................proved - complete [shostak](0.02 s)
min_walk_vert.........................proved - complete [shostak](0.12 s)
min_walk_is_reduced_TCC1..............proved - complete [shostak](0.18 s)
min_walk_is_reduced...................proved - complete [shostak](1.09 s)
Theory totals: 5 formulas, 5 attempted, 5 succeeded (1.42 s)
Proof summary for theory min_walks
min_walk_from_TCC1....................proved - complete [shostak](0.01 s)
min_walk_from_TCC2....................proved - complete [shostak](0.08 s)
min_walk_def_TCC1.....................proved - complete [shostak](0.09 s)
min_walk_def..........................proved - complete [shostak](0.12 s)
min_walk_in...........................proved - complete [shostak](0.02 s)
min_walk_is_min.......................proved - complete [shostak](0.02 s)
Theory totals: 6 formulas, 6 attempted, 6 succeeded (0.34 s)
Proof summary for theory reduce_walks
reduce_TCC1...........................proved - complete [shostak](0.05 s)
reduce_TCC2...........................proved - complete [shostak](0.04 s)
reduce_TCC3...........................proved - complete [shostak](0.06 s)
reduce_TCC4...........................proved - complete [shostak](0.04 s)
reduce_TCC5...........................proved - complete [shostak](0.08 s)
reduce_TCC6...........................proved - complete [shostak](0.18 s)
reduce_lem_TCC1.......................proved - complete [shostak](0.04 s)
reduce_lem_TCC2.......................proved - complete [shostak](0.05 s)
reduce_lem_TCC3.......................proved - complete [shostak](0.05 s)
reduce_lem_TCC4.......................proved - complete [shostak](0.05 s)
reduce_lem............................proved - complete [shostak](0.47 s)
Theory totals: 11 formulas, 11 attempted, 11 succeeded (1.13 s)
Proof summary for theory abstract_max
prep0.................................proved - complete [shostak](0.01 s)
max_f_TCC1............................proved - complete [shostak](0.00 s)
prep1.................................proved - complete [shostak](0.04 s)
max_TCC1..............................proved - complete [shostak](0.05 s)
max_def...............................proved - complete [shostak](0.01 s)
max_in................................proved - complete [shostak](-.00 s)
max_is_max............................proved - complete [shostak](0.00 s)
Theory totals: 7 formulas, 7 attempted, 7 succeeded (0.11 s)
Proof summary for theory digraph_inductions
size_prep.............................proved - complete [shostak](0.08 s)
digraph_induction_vert................proved - complete [shostak](0.03 s)
digraph_induction_vert_not............proved - complete [shostak](0.03 s)
num_edges_prep........................proved - complete [shostak](0.02 s)
digraph_induction_edge................proved - complete [shostak](0.03 s)
Theory totals: 5 formulas, 5 attempted, 5 succeeded (0.17 s)
Proof summary for theory ind_paths
independent?_TCC1.....................proved - complete [shostak](0.03 s)
independent?_TCC2.....................proved - complete [shostak](0.04 s)
independent?_comm.....................proved - complete [shostak](0.03 s)
independent_ne........................proved - complete [shostak](0.01 s)
ind_path_set_2........................proved - complete [shostak](0.05 s)
internal_verts_TCC1...................proved - complete [shostak](0.03 s)
internal_verts_TCC2...................proved - complete [shostak](0.09 s)
indep?_lem............................proved - complete [shostak](0.08 s)
Theory totals: 8 formulas, 8 attempted, 8 succeeded (0.34 s)
Proof summary for theory weighted_digraphs
wgt_aux_TCC1..........................proved - complete [shostak](0.07 s)
wgt_aux_TCC2..........................proved - complete [shostak](0.05 s)
wgt_aux_TCC3..........................proved - complete [shostak](0.09 s)
wgt_walk_TCC1.........................proved - complete [shostak](0.05 s)
wgt_aux_shift_walk....................proved - complete [shostak](1.47 s)
wgt_aux_first_TCC1....................proved - complete [shostak](0.07 s)
wgt_aux_first_TCC2....................proved - complete [shostak](0.08 s)
wgt_aux_first_TCC3....................proved - complete [shostak](0.11 s)
wgt_aux_first.........................proved - complete [shostak](0.22 s)
wgt_aux_split_TCC1....................proved - complete [shostak](0.08 s)
wgt_aux_split.........................proved - complete [shostak](0.17 s)
wgt_aux_sub_walk_TCC1.................proved - complete [shostak](0.16 s)
wgt_aux_sub_walk_TCC2.................proved - complete [shostak](0.12 s)
wgt_aux_sub_walk......................proved - complete [shostak](0.81 s)
wgt_walk_to_aux.......................proved - complete [shostak](0.15 s)
wgt_walk_decomposed_TCC1..............proved - complete [shostak](0.09 s)
wgt_walk_decomposed_TCC2..............proved - complete [shostak](0.05 s)
wgt_walk_decomposed_TCC3..............proved - complete [shostak](0.10 s)
wgt_walk_decomposed...................proved - complete [shostak](0.25 s)
wgt_walk_edge_TCC1....................proved - complete [shostak](0.05 s)
wgt_walk_edge_TCC2....................proved - complete [shostak](0.06 s)
wgt_walk_edge_TCC3....................proved - complete [shostak](0.08 s)
wgt_walk_edge.........................proved - complete [shostak](0.03 s)
wgt_comp_rest_TCC1....................proved - complete [shostak](0.04 s)
wgt_comp_rest_TCC2....................proved - complete [shostak](0.05 s)
wgt_comp_rest_TCC3....................proved - complete [shostak](0.09 s)
wgt_comp_rest.........................proved - complete [shostak](1.17 s)
Theory totals: 27 formulas, 27 attempted, 27 succeeded (5.78 s)
Proof summary for theory wgt_digraphs_props
min_wgt_TCC1.........................proved - complete [shostak]( 0.09 s)
walk_member_set_min..................proved - complete [shostak]( 0.06 s)
wgt_min_walk_choose_TCC1.............proved - complete [shostak]( 0.26 s)
wgt_min_walk_choose..................proved - complete [shostak]( 0.08 s)
min_walk_min_wgt.....................proved - complete [shostak]( 0.03 s)
sub_min_walk_nonempty................proved - complete [shostak](62.32 s)
sub_min_walk_is_min_TCC1.............proved - complete [shostak]( 0.12 s)
sub_min_walk_is_min_TCC2.............proved - complete [shostak]( 0.03 s)
sub_min_walk_is_min..................proved - complete [shostak](60.37 s)
Theory totals: 9 formulas, 9 attempted, 9 succeeded (123.36 s)
Proof summary for theory Eulerian
no_repeat_subseq?_TCC1................proved - complete [shostak](0.01 s)
no_repeat_subseq?_TCC2................proved - complete [shostak](0.01 s)
no_repeat_subseq?_TCC3................proved - complete [shostak](0.01 s)
no_repeat_subseq?_TCC4................proved - complete [shostak](0.01 s)
cycle_is_pre_Eulerian_circuit.........proved - complete [shostak](0.09 s)
pre_Eulerian_circuit_is_a_circuit.....proved - complete [shostak](0.04 s)
Eulerian_circuit_is_circuit...........proved - complete [shostak](0.04 s)
Eulerian_walk_is_Eulerian_circuit.....proved - complete [shostak](0.02 s)
circuit_subwalk_pre_Eulerian_TCC1.....proved - complete [shostak](0.08 s)
circuit_subwalk_pre_Eulerian..........proved - complete [shostak](0.03 s)
pre_Eulerian_circuit_prefix_TCC1......proved - complete [shostak](0.10 s)
pre_Eulerian_circuit_prefix...........proved - complete [shostak](0.02 s)
pre_Eulerian_circuit_o_circuit_TCC1...proved - complete [shostak](0.25 s)
pre_Eulerian_circuit_o_circuit........proved - complete [shostak](0.03 s)
Theory totals: 14 formulas, 14 attempted, 14 succeeded (0.75 s)
Grand Totals: 361 proofs, 361 attempted, 361 succeeded (178.58 s)
[ zur Elbe Produktseite wechseln0.188Quellennavigators
]
|
|
