[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,

Used simplifier rules/spec theorems by specification

Used from specification nat

nat/lels is used by lenle,
nat/lels-01 is used by lenle,
nat/lez-01 is used by lenle,
nat/succ-01 is used by lenle,

Used from specification list-data

list-data/assoclista/elim-list-c is used by uniquelen, k-unique-r,
list-data/assoclista/l is used by uniquelen, lenle, lenequal,
list-data/assoclista/size-01 is used by uniquelen, lenle, lenequal,

Used from specification pair

pair/elim is used by uniquelen, k-unique-r,
pair/inj is used by unique-02, inone,
pair/sel-02 is used by unique, one, lenle,

Used from specification list

list/assoclista/In is used by ex,
list/assoclista/c is used by cons,
list/assoclista/Nil is used by nuni-01, insnotin, insfirst, firstoc, app,
list/assoclista/a is used by uniquelen, unique-04, unique-03, unique-02, unique-01, unique, put-one, one-01, nuni-01, nuni, not, lenle, lenequal, k-unique-r, insnotin, insfirst, inrec, inkeys-nc, inkeys-n, infirst, incons, inapp, in-put, in-03, in-02, in, firstoc, ex, app,
list/assoclista/app is used by put-one, one-01,
list/assoclista/app-08 is used by insnotin, insfirst, firstoc,
list/assoclista/c is used by uniquelen, unique-02, unique-01, unique, nuni-01, nuni, lenle, lenequal, k-unique-r, insnotin, insfirst, in-put, firstoc, ex, app,
list/assoclista/c-04 is used by insnotin,
list/assoclista/c-07 is used by unique, lenle, app,
list/assoclista/c-08 is used by unique, lenle, app,
list/assoclista/e is used by one,
list/assoclista/e-01 is used by uniquelen, unique, lenle, k-unique-r, app,
list/assoclista/first is used by one,
list/assoclista/in-17 is used by inone,
list/assoclista/in-append is used by inapp,
list/assoclista/in-empty is used by unique-02, empty,
list/assoclista/in-rec is used by unique-02,
list/assoclista/len is used by uniquelen, lenle, lenequal,
list/assoclista/len-05 is used by uniquelen, lenle, lenequal,
list/assoclista/rest is used by one,

Used from specification nat-basic2

nat-basic2/a is used by uniquelen, lenle, lenequal,
nat-basic2/c is used by uniquelen, lenle, lenequal,
nat-basic2/eq-01 is used by uniquelen, lenequal,
nat-basic2/s is used by lenle,
nat-basic2/succ is used by uniquelen, lenle, lenequal,

Used from specification nat-basic1

nat-basic1/f is used by lenle,
nat-basic1/zero-01 is used by lenle,