diff options
Diffstat (limited to 'assignment8/qs.status')
| -rw-r--r-- | assignment8/qs.status | 46 |
1 files changed, 46 insertions, 0 deletions
diff --git a/assignment8/qs.status b/assignment8/qs.status new file mode 100644 index 0000000..763c95b --- /dev/null +++ b/assignment8/qs.status @@ -0,0 +1,46 @@ + Proof summary for theory my_list_induction + less_wf...............................proved - complete [shostak](0.04 s) + list_length_induction.................proved - complete [shostak](0.00 s) + Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.05 s) + + Proof summary for theory my_list_props + occ_TCC1..............................proved - complete [shostak](0.01 s) + occ_TCC2..............................proved - complete [shostak](0.03 s) + occ_nth...............................proved - complete [shostak](0.11 s) + nth_occ...............................proved - complete [shostak](0.10 s) + perm_null.............................proved - complete [shostak](0.03 s) + perm_commutative......................proved - complete [shostak](0.01 s) + append_occ............................proved - complete [shostak](0.07 s) + length_append.........................proved - complete [shostak](0.11 s) + nth_append_TCC1.......................proved - complete [shostak](0.04 s) + nth_append_TCC2.......................proved - complete [shostak](0.05 s) + nth_append............................proved - complete [shostak](0.30 s) + Theory totals: 11 formulas, 11 attempted, 11 succeeded (0.86 s) + + Proof summary for theory SPLIT + split_TCC1............................proved - complete [shostak](0.04 s) + split_length..........................proved - complete [shostak](0.13 s) + split_occ.............................proved - complete [shostak](0.14 s) + split_lwb_upb.........................proved - complete [shostak](0.18 s) + Theory totals: 4 formulas, 4 attempted, 4 succeeded (0.50 s) + + Proof summary for theory QS + qs_TCC1...............................proved - complete [shostak](0.07 s) + qs_TCC2...............................proved - complete [shostak](0.06 s) + Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.12 s) + + Proof summary for theory SORTED + sorted?_TCC1..........................proved - complete [shostak](0.03 s) + sorted_append.........................proved - complete [shostak](0.53 s) + Theory totals: 2 formulas, 2 attempted, 2 succeeded (0.56 s) + + Proof summary for theory QS_props + qs_perm...............................proved - complete [shostak](1.35 s) + occ_upb...............................proved - complete [shostak](0.12 s) + occ_lwb...............................proved - complete [shostak](0.10 s) + upb_perm..............................proved - complete [shostak](0.08 s) + lwb_perm..............................proved - complete [shostak](0.08 s) + qs_sorted.............................proved - complete [shostak](0.74 s) + Theory totals: 6 formulas, 6 attempted, 6 succeeded (2.48 s) + +Grand Totals: 27 proofs, 27 attempted, 27 succeeded (4.56 s) |