Project Statistics

theorems contains the number of theorems (not axioms) that were invented by the user.
proofs shows how many proofs were done, for a completed project this is equal to the number of user defined theorems + the number of (generated) proof obligations.
proof steps shows the number of rule applications of the calculus.
interactions is the number rule applications that were done by the user.

Proofs spec-name data? lib? theorems proofs proof steps interactions nonlib specs 460 460 2602 805 lib specs 2227 2227 8841 2313 total 2687 2687 11443 3118 address No No 0 0 0 0 address-data Yes No 0 0 0 0 address-list-set No No 0 0 0 0 align No No 77 77 377 89 alink Yes No 0 0 0 0 alink-set No No 0 0 0 0 array-indices No No 24 24 148 51 array-splice No No 84 84 752 300 branch Yes No 0 0 0 0 branch-array No No 0 0 0 0 buffer No No 2 2 9 5 buffer-inf No No 0 0 0 0 buffer-inf-conv No No 14 14 64 32 checksum No No 2 2 4 2 constants No No 2 2 4 0 dataarray No No 0 0 0 0 dataset No No 0 0 0 0 datasize No No 35 35 345 71 datastream No No 0 0 0 0 datastream-conv No No 9 9 25 13 debug No No 0 0 0 0 default-volid No No 0 0 0 0 dentry Yes No 0 0 0 0 encoding No No 3 3 31 17 encoding-aligned No No 3 3 50 16 encoding-elem-alignment No No 0 0 0 0 encoding-elem-size No No 0 0 0 0 encoding-fixed-size No No 1 1 2 1 encoding-fixed-size-nonempty No No 6 6 50 11 encoding-nat No No 0 0 0 0 encoding-page-size-nonempty No No 5 5 47 14 eraseblock No No 54 54 214 77 error Yes No 0 0 0 0 error-class No No 19 19 36 9 file Yes No 0 0 0 0 file-mode Yes No 0 0 0 0 groupnode Yes No 0 0 0 0 indexnode Yes No 0 0 0 0 inode Yes No 0 0 0 0 key Yes No 7 7 18 0 key-list-set No No 0 0 0 0 key-set No No 0 0 0 0 laddress Yes No 0 0 0 0 laddress-list No No 0 0 0 0 list+set No No 5 5 19 10 list-prefixn No No 49 49 229 43 lp-array No No 0 0 0 0 lprops Yes No 0 0 0 0 metadata No No 0 0 0 0 min-max No No 30 30 65 7 nat-list-less No No 4 4 27 5 nat-list-set No No 0 0 0 0 nat-set No No 6 6 36 18 node Yes No 0 0 0 0 node-index No No 0 0 0 0 node-list No No 0 0 0 0 node-store No No 1 1 1 0 page No No 3 3 6 1 path No No 3 3 8 3 path-permission No No 12 12 35 10 permission No No 0 0 0 0 permission-param No No 0 0 0 0 root-ino No No 0 0 0 0 seekflag Yes No 0 0 0 0 stringset No No 0 0 0 0 user No No 0 0 0 0 volid No No 0 0 0 0 array No Yes 14 14 46 11 array-copy No Yes 53 53 277 85 char No Yes 0 0 0 0 data No Yes 0 0 0 0 elem No Yes 0 0 0 0 elemdata No Yes 0 0 0 0 gelem No Yes 0 0 0 0 list No Yes 130 130 440 87 list-data Yes Yes 29 29 68 0 list-del No Yes 311 311 1700 334 list-dup No Yes 104 104 600 147 list-last No Yes 163 163 579 153 nat No Yes 120 120 302 69 nat-basic No Yes 129 129 356 39 nat-div No Yes 139 139 488 165 nat-inf No Yes 72 72 203 76 nat-mult No Yes 213 213 648 238 oelem No Yes 8 8 18 3 oset No Yes 111 111 328 76 set-basic No Yes 96 96 444 86 set-union No Yes 197 197 770 140 store No Yes 76 76 444 141 store+set No Yes 40 40 163 52 stream No Yes 218 218 957 408 stream-basic Yes Yes 4 4 10 3 string No Yes 0 0 0 0

Lines et. al. of Specifications spec-name data? lib? lines axioms operations sorts all specs No No 3495 761 268 50 all lib specs No No 1162 200 75 11 all nonlib specs No No 2333 561 193 39 all data specs No No 76 44 14 4 all nondata specs No No 3178 264 144 32 all data lib specs No No 38 22 7 2 all nondata lib specs No No 1124 178 68 9 all data nonlib specs No No 279 475 117 16 all nondata nonlib specs No No 2054 86 76 23 address No No 26 0 0 1 address-data Yes No 14 18 7 1 address-list-set No No 72 0 0 1 align No No 30 3 3 0 alink Yes No 14 5 3 1 alink-set No No 27 0 0 1 array-indices No No 83 14 10 0 array-splice No No 68 10 8 0 branch Yes No 16 24 8 1 branch-array No No 32 0 0 1 buffer No No 40 0 0 1 buffer-inf No No 80 0 0 1 buffer-inf-conv No No 32 5 3 0 checksum No No 25 1 1 0 constants No No 26 2 3 0 dataarray No No 40 0 0 1 dataset No No 25 0 0 0 datasize No No 30 3 2 0 datastream No No 80 0 0 1 datastream-conv No No 32 5 3 0 debug No No 23 1 1 0 default-volid No No 22 0 1 0 dentry Yes No 18 20 6 1 encoding No No 59 5 3 0 encoding-aligned No No 46 2 2 0 encoding-elem-alignment No No 35 1 1 0 encoding-elem-size No No 34 0 1 0 encoding-fixed-size No No 26 2 0 0 encoding-fixed-size-nonempty No No 51 2 2 0 encoding-nat No No 21 0 0 0 encoding-page-size-nonempty No No 50 2 2 0 eraseblock No No 56 11 10 0 error Yes No 32 121 16 1 error-class No No 39 1 1 0 file Yes No 14 18 7 1 file-mode Yes No 16 4 3 1 groupnode Yes No 16 27 9 1 indexnode Yes No 16 18 7 1 inode Yes No 21 51 13 1 key Yes No 19 35 8 1 key-list-set No No 72 0 0 1 key-set No No 27 0 0 1 laddress Yes No 14 11 5 1 laddress-list No No 56 0 0 1 list+set No No 24 1 1 0 list-prefixn No No 31 3 3 0 lp-array No No 42 0 0 1 lprops Yes No 24 31 12 2 metadata No No 20 0 0 1 min-max No No 26 2 2 0 nat-list-less No No 25 2 1 0 nat-list-set No No 72 0 0 1 nat-set No No 34 0 0 1 node Yes No 29 88 10 1 node-index No No 50 0 0 1 node-list No No 56 0 0 1 node-store No No 50 0 0 1 page No No 26 2 2 0 path No No 53 0 0 1 path-permission No No 39 5 5 0 permission No No 25 0 3 0 permission-param No No 23 0 1 1 root-ino No No 23 1 1 0 seekflag Yes No 16 4 3 1 stringset No No 27 0 0 1 user No No 20 0 0 1 volid No No 23 0 0 1 array No Yes 48 5 2 1 array-copy No Yes 100 14 4 0 char No Yes 34 0 0 1 data No Yes 23 0 0 1 elem No Yes 22 0 0 1 elemdata No Yes 23 0 0 0 gelem No Yes 26 0 0 0 list No Yes 38 7 5 0 list-data Yes Yes 21 12 4 1 list-del No Yes 101 26 5 0 list-dup No Yes 39 7 4 0 list-last No Yes 62 14 5 0 nat No Yes 31 5 3 0 nat-basic No Yes 42 12 3 1 nat-div No Yes 32 2 0 0 nat-inf No Yes 48 13 5 1 nat-mult No Yes 23 2 1 0 oelem No Yes 27 3 1 0 oset No Yes 61 8 2 0 set-basic No Yes 42 6 5 1 set-union No Yes 35 5 5 0 store No Yes 58 11 6 1 store+set No Yes 42 8 5 0 stream No Yes 114 30 7 0 stream-basic Yes Yes 17 10 3 1 string No Yes 53 0 0 1