[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 list
Status:
Proved!
Axioms: 7, User Theorems: 130 (Proved: 130, Partially proved: 0, Unproved: 0, Invalid: 0, Siginvalid: 0)
Proof steps: 466, Interactions: 80
Cons(0,0)
app-07(2,0)
constrrew(2,0)
first-01(3,0)
in-08(3,0)
in-last-rest(2,0)
inapp-12(3,1)
k-Two(2,0)
len-06(6,3)
one(3,0)
Last(0,0)
app-08(2,0)
e(2,0)
first-02(6,0)
in-09(3,0)
in-rec(0,0)
inapp-13(5,1)
last(2,0)
len-last-rest(5,2)
one-01(3,1)
Nil(0,0)
app-09(2,0)
e-01(2,0)
first-app(5,1)
in-10(2,0)
inapp(9,3)
inapp-14(3,1)
last-01(2,0)
less-append(2,1)
onein(3,0)
Noassoc(2,0)
append-size-less(7,2)
e-02(2,0)
firsteq(3,0)
in-11(2,0)
inapp-01(2,0)
inex(3,1)
lastdiv(9,0)
longest-common-prefix(13,7)
rest(2,0)
One(0,0)
c(2,0)
e-03(2,0)
firsteq-01(3,0)
in-12(2,0)
inapp-02(3,0)
inex-01(3,0)
lastdiv-rew(2,1)
neq(2,0)
rest-01(3,0)
Two(0,0)
c-01(2,0)
e-04(2,0)
firstoc(13,5)
in-13(2,0)
inapp-03(6,3)
inex-02(2,0)
lastoc(11,3)
neq-01(7,2)
rewlem(2,0)
a(4,0)
c-02(3,0)
elim-first(2,1)
firstoc-rew(2,1)
in-14(2,0)
inapp-04(2,0)
inex-03(2,0)
lastoc-rew(2,1)
neq-02(3,0)
some-element(4,2)
app(2,0)
c-03(2,0)
eq(2,0)
firstrest(2,0)
in-15(2,0)
inapp-05(3,0)
ins(2,0)
lasttwo(8,3)
neq-03(3,1)
split-first(11,4)
app-01(5,0)
c-04(2,0)
eq-01(3,0)
fr(2,0)
in-16(2,0)
inapp-06(7,3)
ins-01(2,0)
len(4,0)
neq-04(2,0)
split-rest(5,1)
app-02(2,1)
c-05(3,0)
eq-02(2,0)
if-in(2,0)
in-17(2,1)
inapp-07(3,0)
isin(3,0)
len-01(7,3)
neq-05(2,0)
two(9,0)
app-03(5,0)
c-06(2,0)
eq-03(2,0)
in(2,0)
in-append(12,0)
inapp-08(3,0)
isin-01(5,1)
len-02(3,1)
neq-06(4,1)
unequal(13,5)
app-04(5,0)
c-07(2,0)
eq-04(5,0)
in-01(2,0)
in-append0-not-left(3,0)
inapp-09(2,0)
k-In(2,0)
len-03(3,0)
neq-07(9,4)
app-05(3,0)
c-08(2,0)
eq-05(2,0)
in-06(2,0)
in-def(10,2)
inapp-10(2,0)
k-Last-base(2,0)
len-04(3,1)
neq-09(2,0)
app-06(7,2)
c-09(2,0)
first(2,0)
in-07(3,0)
in-empty(0,0)
inapp-11(3,1)
k-Last-rec(2,0)
len-05(2,1)
ni(3,1)