[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 erasequeue
Status:
Proved!
Axioms: 11, User Theorems: 30 (Proved: 30, Partially proved: 0, Unproved: 0, Invalid: 0, Siginvalid: 0)
Proof steps: 348, Interactions: 23
eq-entry-in-lref-in(3,0)
in-prepend(14,2)
in-single(2,1)
lebrefs-append-none(9,0)
queue-in(0,0)
queue-rm-v-rec(0,0)
rm-vl-in-before-h(11,0)
in-append(14,2)
in-prepend-other(11,0)
in-vl-append(7,1)
lebrefs-base(0,0)
queue-in-v(0,0)
queue-rm-vl-base(0,0)
rm-vl-lebrefs-subseteq(3,2)
in-append-other(11,0)
in-prepend-vl(9,0)
in-vl-append0(20,0)
lebrefs-lref(3,3)
queue-in-vl(0,0)
queue-rm-vl-rec(0,0)
rm-vl-notin(2,0)
in-concat(16,0)
in-rm-v(45,0)
in-vl-in-lebrefs(33,2)
lebrefs-none(4,3)
queue-rm-base(0,0)
rm-v-subseteq(13,1)
rm-vl-notin-before(19,0)
in-empty(2,0)
in-rm-v-in(19,0)
in-vl-subset(3,0)
lebrefs-none-notin(2,0)
queue-rm-rec(0,0)
rm-vl-append-same(13,3)
subseteq-lebrefs-subseteq(13,1)
in-empty-vl(2,1)
in-rm-v-same(17,0)
lebrefs-append-lref(9,1)
lebrefs-rec(0,0)
queue-rm-v-base(0,0)
rm-vl-in-before(19,0)