[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: 350, Interactions: 85
datasize(0,0)
datasize-at(2,1)
datasize-further(63,14)
datasize-ls(4,1)
datasize-mkempbuffer(2,1)
datasize-subarray(2,1)
datsize-write-higher(2,1)
datasize-add-empty-h(21,10)
datasize-at-h(9,4)
datasize-is-smaller(1,0)
datasize-ls-add(2,1)
datasize-mkempbuffer-h(4,0)
datasize-subarray-h(26,6)
datsize-write-higher-h(21,4)
datasize-append(7,2)
datasize-base(0,0)
datasize-is-smaller-help(5,1)
datasize-ls-datasize-h(1,0)
datasize-rec(0,0)
datasize-subarray0(2,1)
datasize-append-empty-h(31,7)
datasize-datasize-elim-h(5,1)
datasize-le(2,1)
datasize-ls-h(4,1)
datasize-samebuf-h(7,1)
datasize-subarray0-h(14,2)
datasize-append-h-new(14,4)
datasize-empbuf(4,2)
datasize-le-fwd(1,0)
datasize-ls-samedata(2,1)
datasize-split-empty(2,1)
datasize-zero(2,1)
datasize-append-lower-h(6,0)
datasize-empbuf-h(21,6)
datasize-le-h(18,1)
datasize-ls-samedata-h(14,3)
datasize-split-empty-h(12,5)
datasize-zero-h(17,0)