|
***
*** top (21:1:1 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 list_props_aux
length_is_0...........................proved - complete [shostak](0.06 s)
append_is_null........................proved - complete [shostak](0.05 s)
append_eq1............................proved - complete [shostak](0.08 s)
append_eq2............................proved - complete [shostak](-.82 s)
Theory totals: 4 formulas, 4 attempted, 4 succeeded (-0.63 s)
Proof summary for theory State
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory AExp
A_TCC1................................proved - complete [shostak](0.05 s)
A_TCC2................................proved - complete [shostak](0.04 s)
A_TCC3................................proved - complete [shostak](0.05 s)
A_TCC4................................proved - complete [shostak](0.05 s)
A_TCC5................................proved - complete [shostak](0.04 s)
A_TCC6................................proved - complete [shostak](0.04 s)
Theory totals: 6 formulas, 6 attempted, 6 succeeded (0.27 s)
Proof summary for theory BExp
B_TCC1................................proved - complete [shostak](0.05 s)
B_TCC2................................proved - complete [shostak](0.05 s)
B_TCC3................................proved - complete [shostak](0.05 s)
Theory totals: 3 formulas, 3 attempted, 3 succeeded (0.15 s)
Proof summary for theory Stm
Stm_measure_TCC1......................proved - complete [shostak](0.06 s)
Stm_measure_TCC2......................proved - complete [shostak](0.04 s)
Stm_measure_TCC3......................proved - complete [shostak](0.06 s)
Stm_measure_TCC4......................proved - complete [shostak](0.06 s)
Stm_measure_TCC5......................proved - complete [shostak](0.06 s)
IMP_measure_induction_TCC1............proved - complete [shostak](0.04 s)
structural_induction..................proved - complete [shostak](0.29 s)
Theory totals: 7 formulas, 7 attempted, 7 succeeded (0.61 s)
Proof summary for theory Cont
sq_le_def.............................proved - complete [shostak](0.13 s)
partial_order_sq_le...................proved - complete [shostak](0.08 s)
lub_graph_TCC1........................proved - complete [shostak](0.04 s)
lub_graph_TCC2........................proved - complete [shostak](0.14 s)
lub_graph.............................proved - complete [shostak](0.48 s)
sq_le_dcpo............................proved - complete [shostak](0.55 s)
sq_le_pdcpo...........................proved - complete [shostak](0.05 s)
sq_le_bottom..........................proved - complete [shostak](0.05 s)
sq_le_least...........................proved - complete [shostak](0.06 s)
sq_le_conditional.....................proved - complete [shostak](0.09 s)
apply_continuous......................proved - complete [shostak](3.72 s)
Theory totals: 11 formulas, 11 attempted, 11 succeeded (5.38 s)
Proof summary for theory direct
SS_TCC1...............................proved - complete [shostak](0.14 s)
SS_TCC2...............................proved - complete [shostak](0.14 s)
SS_TCC3...............................proved - complete [shostak](0.17 s)
SS_TCC4...............................proved - complete [shostak](0.15 s)
SS_TCC5...............................proved - complete [shostak](0.15 s)
SS_TCC6...............................proved - complete [shostak](0.15 s)
Theory totals: 6 formulas, 6 attempted, 6 succeeded (0.90 s)
Proof summary for theory continuation
IMP_fixpoints_TCC1....................proved - complete [shostak](3.81 s)
identity_continuous...................proved - complete [shostak](4.75 s)
composition_continuous................proved - complete [shostak](4.91 s)
assign_continuous.....................proved - complete [shostak](4.75 s)
conditional_continuous................proved - complete [shostak](5.81 s)
composition_conditional...............proved - complete [shostak](4.75 s)
SS_TCC1...............................proved - complete [shostak](3.82 s)
SS_TCC2...............................proved - complete [shostak](4.83 s)
SS_TCC3...............................proved - complete [shostak](4.88 s)
SS_TCC4...............................proved - complete [shostak](4.80 s)
SS_TCC5...............................proved - complete [shostak](4.81 s)
SS_TCC6...............................proved - complete [shostak](4.82 s)
SS_TCC7...............................proved - complete [shostak](4.89 s)
SS_TCC8...............................proved - complete [shostak](4.84 s)
SS_TCC9...............................proved - complete [shostak](4.87 s)
Theory totals: 15 formulas, 15 attempted, 15 succeeded (71.36 s)
Proof summary for theory congruence
IMP_admissible_TCC1..................proved - complete [shostak](10.36 s)
P_bottom_TCC1........................proved - complete [shostak]( 5.36 s)
P_bottom.............................proved - complete [shostak]( 4.09 s)
IMP_scott_continuity_TCC1............proved - complete [shostak]( 2.55 s)
admissible_P.........................proved - complete [shostak](11.78 s)
continuation_direct..................proved - complete [shostak]( 7.07 s)
Theory totals: 6 formulas, 6 attempted, 6 succeeded (41.21 s)
Proof summary for theory sos
step_TCC1.............................proved - complete [shostak](4.11 s)
tr_TCC1...............................proved - complete [shostak](4.08 s)
tr_TCC2...............................proved - complete [shostak](4.04 s)
tr_TCC3...............................proved - complete [shostak](4.01 s)
tr_add................................proved - complete [shostak](4.22 s)
tr_eq.................................proved - complete [shostak](4.04 s)
tr_split..............................proved - complete [shostak](4.27 s)
tr_partial............................proved - complete [shostak](4.10 s)
tr_deterministic......................proved - complete [shostak](3.12 s)
SS_TCC1...............................proved - complete [shostak](4.06 s)
SS_deterministic......................proved - complete [shostak](4.09 s)
Theory totals: 11 formulas, 11 attempted, 11 succeeded (44.14 s)
Proof summary for theory direct_sos
sos_le_direct........................proved - complete [shostak](19.98 s)
direct_le_sos........................proved - complete [shostak](19.28 s)
direct_eq_sos........................proved - complete [shostak](16.55 s)
Theory totals: 3 formulas, 3 attempted, 3 succeeded (55.81 s)
Proof summary for theory compiler
CA_TCC1...............................proved - complete [shostak](0.07 s)
CA_TCC2...............................proved - complete [shostak](0.07 s)
CA_TCC3...............................proved - complete [shostak](0.07 s)
CA_TCC4...............................proved - complete [shostak](0.07 s)
CA_TCC5...............................proved - complete [shostak](0.08 s)
CA_TCC6...............................proved - complete [shostak](0.07 s)
CB_TCC1...............................proved - complete [shostak](0.06 s)
CB_TCC2...............................proved - complete [shostak](0.07 s)
CB_TCC3...............................proved - complete [shostak](0.07 s)
CS_TCC1...............................proved - complete [shostak](0.08 s)
CS_TCC2...............................proved - complete [shostak](0.07 s)
CS_TCC3...............................proved - complete [shostak](0.09 s)
CS_TCC4...............................proved - complete [shostak](0.08 s)
CS_TCC5...............................proved - complete [shostak](0.08 s)
nonnull_CA............................proved - complete [shostak](0.17 s)
nonnull_CB............................proved - complete [shostak](0.21 s)
nonnull_CS............................proved - complete [shostak](0.13 s)
Theory totals: 17 formulas, 17 attempted, 17 succeeded (1.54 s)
Proof summary for theory Instruction
Theory totals: 0 formulas, 0 attempted, 0 succeeded (0.00 s)
Proof summary for theory am
check2_TCC1...........................proved - complete [shostak](0.06 s)
step_TCC1.............................proved - complete [shostak](0.05 s)
step_TCC2.............................proved - complete [shostak](0.07 s)
step_TCC3.............................proved - complete [shostak](0.05 s)
step_TCC4.............................proved - complete [shostak](0.07 s)
step_TCC5.............................proved - complete [shostak](0.06 s)
step_TCC6.............................proved - complete [shostak](0.06 s)
tr_TCC1...............................proved - complete [shostak](0.08 s)
tr_TCC2...............................proved - complete [shostak](0.07 s)
step_append...........................proved - complete [shostak](0.95 s)
tr_add................................proved - complete [shostak](0.18 s)
tr_eq.................................proved - complete [shostak](0.08 s)
code_partial..........................proved - complete [shostak](2.12 s)
code_split............................proved - complete [shostak](1.28 s)
M_TCC1................................proved - complete [shostak](0.05 s)
M_deterministic.......................proved - complete [shostak](0.27 s)
Theory totals: 16 formulas, 16 attempted, 16 succeeded (5.51 s)
Proof summary for theory bisimulation
correct_AExp..........................proved - complete [shostak](0.97 s)
correct_BExp..........................proved - complete [shostak](1.26 s)
eq_AExp...............................proved - complete [shostak](0.18 s)
AExp_steps............................proved - complete [shostak](-.54 s)
AExp_e................................proved - complete [shostak](1.43 s)
eq_BExp...............................proved - complete [shostak](0.20 s)
BExp_steps............................proved - complete [shostak](0.09 s)
BExp_e................................proved - complete [shostak](3.82 s)
tilde_TCC1............................proved - complete [shostak](0.06 s)
tilde_TCC2............................proved - complete [shostak](0.06 s)
sos_step..............................proved - complete [shostak](1.51 s)
sos_steps.............................proved - complete [shostak](0.28 s)
am_step1..............................proved - complete [shostak](1.97 s)
am_steps..............................proved - complete [shostak](0.66 s)
bisimulation..........................proved - complete [shostak](0.47 s)
Theory totals: 15 formulas, 15 attempted, 15 succeeded (12.43 s)
Proof summary for theory axiomatic
inference_tree?_TCC1..................proved - complete [shostak](0.05 s)
inference_tree?_TCC2..................proved - complete [shostak](0.06 s)
inference_tree?_TCC3..................proved - complete [shostak](0.08 s)
inference_tree?_TCC4..................proved - complete [shostak](0.08 s)
inference_tree?_TCC5..................proved - complete [shostak](0.05 s)
inference_tree?_TCC6..................proved - complete [shostak](0.06 s)
inference_tree?_TCC7..................proved - complete [shostak](0.08 s)
inference_tree?_TCC8..................proved - complete [shostak](0.08 s)
inference_tree?_TCC9..................proved - complete [shostak](0.06 s)
inference_tree?_TCC10.................proved - complete [shostak](0.05 s)
inference_tree?_TCC11.................proved - complete [shostak](0.06 s)
inference_tree?_TCC12.................proved - complete [shostak](0.05 s)
inference_tree_TCC1...................proved - complete [shostak](0.04 s)
wlp_is_precondition...................proved - complete [shostak](5.22 s)
wlp_is_weakest........................proved - complete [shostak](5.21 s)
soundness.............................proved - complete [shostak](4.99 s)
completeness..........................proved - complete [shostak](6.18 s)
sound_and_complete....................proved - complete [shostak](5.21 s)
Theory totals: 18 formulas, 18 attempted, 18 succeeded (27.61 s)
Proof summary for theory natural
depth_TCC1............................proved - complete [shostak](4.03 s)
depth_TCC2............................proved - complete [shostak](4.02 s)
depth_TCC3............................proved - complete [shostak](4.03 s)
derivation_tree?_TCC1.................proved - complete [shostak](4.04 s)
derivation_tree?_TCC2.................proved - complete [shostak](4.03 s)
derivation_tree?_TCC3.................proved - complete [shostak](4.04 s)
derivation_tree?_TCC4.................proved - complete [shostak](4.04 s)
derivation_tree?_TCC5.................proved - complete [shostak](4.03 s)
derivation_tree?_TCC6.................proved - complete [shostak](4.04 s)
derivation_tree_TCC1..................proved - complete [shostak](3.98 s)
dt_eq.................................proved - complete [shostak](6.65 s)
SS_TCC1...............................proved - complete [shostak](4.00 s)
SS_deterministic......................proved - complete [shostak](4.09 s)
natural_le_sos........................proved - complete [shostak](1.34 s)
sos_le_natural........................proved - complete [shostak](1.02 s)
natural_eq_sos........................proved - complete [shostak](0.07 s)
Theory totals: 16 formulas, 16 attempted, 16 succeeded (57.44 s)
Grand Totals: 154 proofs, 154 attempted, 154 succeeded (323.72 s)
[ Dauer der Verarbeitung: 0.14 Sekunden
(vorverarbeitet)
]
|
