1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
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)
|
