[Imprint]
[Data Privacy Statement]
[E-Mail]
Back to
main index
. View
the specification
. View
theorem base summary
, View
theorem base listing
, the
used properties by spec
, the
dependency list
, the
symbol table
,
Theorem base summary for Specification datasize
Status:
Proved!
Axioms: 3, User Theorems: 35 (Proved: 35, Partially proved: 0, Unproved: 0, Invalid: 0, Siginvalid: 0)
Proof steps: 345, Interactions: 71
datasize(0,0)
datasize-at(3,1)
datasize-further(64,12)
datasize-ls(5,1)
datasize-mkempbuffer(2,1)
datasize-subarray(3,1)
datsize-write-higher(3,1)
datasize-add-empty-h(20,9)
datasize-at-h(9,3)
datasize-is-smaller(2,0)
datasize-ls-add(3,1)
datasize-mkempbuffer-h(5,0)
datasize-subarray-h(12,2)
datsize-write-higher-h(22,2)
datasize-append(4,1)
datasize-base(0,0)
datasize-is-smaller-help(6,1)
datasize-ls-datasize-h(2,0)
datasize-rec(0,0)
datasize-subarray0(2,1)
datasize-append-empty-h(32,7)
datasize-datasize-elim-h(5,1)
datasize-le(3,1)
datasize-ls-h(5,1)
datasize-samebuf-h(11,5)
datasize-subarray0-h(9,0)
datasize-append-h-new(13,3)
datasize-empbuf(2,1)
datasize-le-fwd(2,0)
datasize-ls-samedata(3,1)
datasize-split-empty(3,1)
datasize-zero(2,1)
datasize-append-lower-h(6,0)
datasize-empbuf-h(20,5)
datasize-le-h(19,1)
datasize-ls-samedata-h(15,3)
datasize-split-empty-h(11,3)
datasize-zero-h(17,0)