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