[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 remtau
Status:
Proved!
Axioms: 5, User Theorems: 43 (Proved: 43, Partially proved: 0, Unproved: 0, Invalid: 0, Siginvalid: 0)
Proof steps: 319, Interactions: 136
addopt(0,0)
finremtau-nontau-lem(2,0)
one-eq-empty(2,1)
remtau-equiv(29,15)
remtau-one(5,1)
remtau-split-list-fin(2,1)
remtau-toempty-from(9,5)
ex-first-nontau(8,5)
finremtau-one(2,0)
remtau-alltau(0,0)
remtau-fin(2,0)
remtau-one-02(2,1)
remtau-split-list-inf(10,3)
remtau-toempty-from-inf(5,1)
finremtau-append(4,1)
finremtau-split-fin(5,1)
remtau-append(2,1)
remtau-fromempty-to(8,4)
remtau-one-03(2,1)
remtau-split-list-weak(7,3)
remtau_of_to-to_of_rmtau(10,3)
finremtau-cons(7,6)
finremtau-split-weak(6,2)
remtau-append-fin(5,1)
remtau-inf(41,18)
remtau-split(13,7)
remtau-split-one(21,10)
size-to-less(3,1)
finremtau-def(0,0)
not-lessto(4,2)
remtau-cons(0,0)
remtau-nontau-lem(2,0)
remtau-split-fin(6,2)
remtau-split-one-fin(6,3)
to-addone(8,3)
finremtau-empty(4,3)
not-lessto-fin(2,1)
remtau-empty(0,0)
remtau-notless(2,1)
remtau-split-inf(10,3)
remtau-split-one-inf(8,3)
to_of_remtau-remtau_of_to(4,1)
finremtau-empty-equiv(1,1)
not-lessto-inf(2,1)
remtau-empty-equiv(32,14)
remtau-notless-fin(8,2)
remtau-split-list(2,1)
remtau-split-weak(6,3)