[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/add-num-01
is used by
len,
- nat/elim-pred-c
is used by
orderedls-all,
orderedle-all,
- nat/fle
is used by
orderedls-all,
- nat/l-num-06
is used by
orderedls-all,
- nat/le-ls-simp
is used by
orderedls-all,
orderedle-all,
- nat/le-num-06
is used by
ordered-append,
- nat/le-sum
is used by
orderedle-all,
- nat/lels
is used by
orderedls-all,
orderedle-all,
- nat/lels-01
is used by
ordered-postfix,
- nat/lels-03
is used by
ordered-shorter-sublist,
- nat/lep-02
is used by
orderedls-all,
orderedle-all,
- nat/let
is used by
orderedle-all,
- nat/lez
is used by
orderedls-all,
orderedle-all,
- nat/lez-01
is used by
orderedls-all,
orderedle-all,
- nat/pred-03
is used by
orderedle-all,
- nat/succ-01
is used by
orderedls-all,
orderedle-all,
ordered-prefix,
k-ls-r,
k-le-r,
Used from specification list-last
- list-last/postfix-is-lessOrEqual
is used by
ordered-postfix,
- list-last/prefix-rec-01
is used by
ordered-prefix,
- list-last/l
is used by
ordered-append,
- list-last/l-02
is used by
ordered-append,
- list-last/lapp-04
is used by
ole-last,
- list-last/last-elim
is used by
ole-last-01,
ole-last,
- list-last/lin-01
is used by
ole-last,
- list-last/postfix-empty
is used by
ordered-postfix,
- list-last/postfix-empty-03
is used by
ordered-postfix,
- list-last/postfix-one
is used by
ordered-postfix,
- list-last/prefix-empty
is used by
ordered-prefix,
- list-last/prefix-nil
is used by
ordered-prefix,
- list-last/prefix-rec-03
is used by
ordered-prefix,
Used from specification list-data
- list-data/elim-list-c
is used by
rest-01,
rest,
orderedls-all,
orderedle-all,
ordered-prefix,
ordered-postfix,
ordered-append,
ols-rec,
ole-rec,
ole-last,
ole-01,
k-ls-r,
k-le-r,
ins-yes,
ins-rec,
ins-less-first,
eq,
del1-01-02,
del1-01,
del1,
app,
- list-data/l
is used by
orderedls-all,
orderedle-all,
ordered-shorter-sublist,
ordered-prefix,
ordered-postfix,
k-ls-r,
k-le-r,
- list-data/size-01
is used by
orderedls-all,
orderedle-all,
len,
k-ls-r,
k-le-r,
Used from specification list
- list/Nil
is used by
ordered-ex-divide-lsle,
ordered-ex-divide-lels,
ordered-append,
ole-last,
insperm-02,
ins-less-last,
ex,
app-02,
app-01,
app,
- list/a
is used by
sw,
same,
rest-01,
rest,
perm-ins,
orderedls-ls,
orderedls-all,
orderedle-ls,
orderedle-all,
ordered-prefix,
ordered-postfix,
ordered-ex-divide-lsle,
ordered-ex-divide-lels,
ordered-append,
one-02,
ols-rec,
ole-two,
ole-rec,
ole-last-01,
ole-last,
ole-in,
ole-01,
len,
k-ls-r,
k-le-r,
insperm-03,
insperm-02,
insperm-01,
ins-yes,
ins-y-01,
ins-rec,
ins-one-02,
ins-one-01,
ins-one,
ins-less-last,
ins-less-first,
in-04,
in-01-02,
ex,
eqdef,
eq,
empty,
del1-02,
del1-01-02,
del1-01-01,
del1-01,
del1,
cons-03,
cons-02,
cons,
app-02,
app-01,
app,
- list/app
is used by
orderedls-ls,
orderedls-all,
orderedle-all,
ordered-postfix,
ordered-append,
ole-two,
ole-last,
ole-01,
k-ls-r,
k-le-r,
ins-one-02,
ins-one-01,
ins-one,
ex,
del1-01-02,
del1-01-01,
del1-01,
del1,
cons-03,
cons-02,
cons,
app,
- list/app-02-ant
is used by
orderedls-all,
orderedle-all,
ole-last,
empty,
del1,
- list/app-03
is used by
sw,
ex,
- list/app-06
is used by
ole-last,
- list/app-08
is used by
sw,
same,
ordered-ex-divide-lsle,
ordered-ex-divide-lels,
one-02,
ins-yes,
ins-rec,
ins-less-last,
ins-less-first,
ex,
eq,
del1-02,
del1-01-02,
del1-01-01,
cons-03,
- list/c
is used by
sw,
same,
rest-01,
rest,
orderedls-ls,
orderedls-all,
orderedle-all,
ordered-prefix,
ordered-postfix,
ordered-ex-divide-lsle,
ordered-ex-divide-lels,
ordered-append,
ols-rec,
ole-two,
ole-rec,
ole-last,
ole-in,
ole-01,
len,
k-ls-r,
k-le-r,
insperm-03,
insperm-02,
ins-yes,
ins-y-01,
ins-rec,
ins-one-02,
ins-one-01,
ins-one,
ins-less-last,
ins-less-first,
in-04,
in-01-02,
ex,
eqdef,
eq,
empty,
del1-02,
del1-01-02,
del1-01-01,
del1-01,
del1,
cons-03,
cons-02,
cons,
app-02,
app-01,
app,
- list/c-03
is used by
ole-01,
eq,
- list/c-04
is used by
ex,
del1-01-02,
cons-03,
- list/c-05
is used by
ole-last,
- list/c-06
is used by
ordered-postfix,
ole-01,
ins-less-first,
eq,
del1-01,
- list/c-07
is used by
orderedls-all,
orderedle-all,
ordered-prefix,
ordered-postfix,
ordered-append,
ole-last,
ole-01,
del1-01-02,
del1-01,
del1,
app,
- list/c-08
is used by
orderedls-all,
orderedle-all,
ordered-prefix,
ordered-postfix,
ordered-append,
ole-last,
ole-01,
del1-01-02,
del1-01,
del1,
app,
- list/e
is used by
orderedls-all,
orderedle-all,
ole-last,
eq,
empty,
del1-01-01,
del1,
- list/e-01
is used by
rest-01,
rest,
orderedls-all,
orderedle-all,
ordered-prefix,
ordered-postfix,
ordered-append,
ols-rec,
ole-rec,
ole-last,
ole-01,
k-ls-r,
k-le-r,
ins-yes,
ins-rec,
ins-less-first,
eq,
del1-01-02,
del1-01,
del1,
app,
- list/e-02
is used by
ole-last,
- list/first-01
is used by
ordered-append,
- list/first-02
is used by
ole-last,
- list/in-01
is used by
ole-last,
in-01-02,
- list/in-06
is used by
in-04,
- list/in-11
is used by
ordered-ex-divide-lels,
ole-last,
- list/in-12
is used by
ole-last,
- list/in-14
is used by
ordered-postfix,
ole-last,
ole-01,
eq,
del1-01,
del1,
- list/in-15
is used by
ole-last,
- list/in-17
is used by
ole-last,
ole-01,
in-04,
in-01-02,
- list/in-append
is used by
ordered-ex-divide-lsle,
ordered-ex-divide-lels,
ole-last,
- list/in-empty
is used by
orderedls-ls,
ordered-ex-divide-lsle,
ordered-ex-divide-lels,
ole-last,
ole-in,
in-01-02,
del1-01-01,
- list/in-rec
is used by
orderedls-ls,
ordered-postfix,
ordered-ex-divide-lsle,
ordered-ex-divide-lels,
ole-last,
ole-in,
ole-01,
in-01-02,
eq,
del1-01-01,
del1-01,
del1,
- list/inapp-10
is used by
ole-last,
- list/len
is used by
orderedls-all,
orderedle-all,
ordered-append,
- list/len-02
is used by
orderedls-all,
orderedle-all,
ordered-postfix,
len,
- list/len-05
is used by
ordered-prefix,
ordered-append,
len,
k-ls-r,
k-le-r,
- list/less-append
is used by
ordered-postfix,
- list/ni
is used by
ole-last,
- list/one-01
is used by
eq,
Used from specification nat-basic2
- nat-basic2/a
is used by
orderedls-all,
orderedle-all,
ordered-prefix,
ordered-append,
len,
k-ls-r,
k-le-r,
- nat-basic2/c
is used by
orderedls-all,
orderedle-all,
ordered-prefix,
ordered-append,
len,
k-ls-r,
k-le-r,
- nat-basic2/eq-01
is used by
len,
- nat-basic2/l
is used by
orderedls-all,
orderedle-all,
- nat-basic2/l-02
is used by
orderedls-all,
orderedle-all,
- nat-basic2/oz
is used by
orderedls-all,
orderedle-all,
- nat-basic2/s
is used by
orderedls-all,
orderedle-all,
- nat-basic2/succ
is used by
orderedls-all,
orderedle-all,
ordered-prefix,
ordered-append,
len,
k-ls-r,
k-le-r,
Used from specification list-perm
- list-perm/cons
is used by
insperm-01,
- list-perm/del-01
is used by
insperm,
eqdef,
- list-perm/perm-del
is used by
perm-ins,
- list-perm/trans
is used by
insperm-01,
- list-perm/app
is used by
perm-ins,
insperm-03,
insperm-02,
insperm-01,
- list-perm/app-02
is used by
perm-ins,
- list-perm/perm-r
is used by
eqdef,
- list-perm/ref
is used by
perm-ins,
insperm-03,
insperm-02,
insperm-01,
insperm,
- list-perm/sym-01
is used by
perm-ins,
insperm-03,
insperm-01,
- list-perm/sym-02
is used by
perm-ins,
insperm-03,
insperm-02,
insperm-01,
- list-perm/trans
is used by
perm-ins,
insperm-03,
insperm-01,
Used from specification oelem
- oelem/irreflexivity
is used by
orderedls-ls,
orderedls-all,
orderedle-all,
ordered-ex-divide-lels,
ole-last,
ole-01,
ins-y-01,
ins-one-02,
eq,
del1-02,
- oelem/lel
is used by
ole-01,
eq,
- oelem/ls-le
is used by
orderedls-ls,
ole-last,
- oelem/nen
is used by
ordered-postfix,
ole-last,
ole-01,
ins-less-first,
eq,
- oelem/nll
is used by
sw,
orderedls-all,
orderedle-all,
ordered-ex-divide-lsle,
ordered-ex-divide-lels,
ole-last,
ole-in,
ole-01,
del1-01-02,
del1,
- oelem/nnn
is used by
sw,
orderedle-all,
ordered-ex-divide-lsle,
ole-last,
ole-in,
- oelem/seq
is used by
sw,
ins-less-first,
- oelem/sls
is used by
ordered-ex-divide-lsle,
ordered-ex-divide-lels,
ole-last,
del1-01-02,
del1-01-01,
del1-01,
- oelem/transitivity
is used by
orderedls-ls,
ordered-ex-divide-lels,
ole-01,
ins-y-01,
ins-one-02,
del1-01-02,
del1-01,
Used from specification nat-basic1
- nat-basic1/f
is used by
orderedls-all,
orderedle-all,
ordered-shorter-sublist,
- nat-basic1/less-1
is used by
orderedls-all,
orderedle-all,
- nat-basic1/lf-02
is used by
orderedls-all,
- nat-basic1/one
is used by
ordered-postfix,
- nat-basic1/one-01
is used by
ordered-prefix,
k-ls-r,
k-le-r,
- nat-basic1/z
is used by
orderedls-all,
orderedle-all,
Used from specification list-del
- list-del/app
is used by
perm-ins,
- list-del/del1-n
is used by
del1-02,
del1-01-02,
del1-01,
del1,
- list-del/get-numrec
is used by
orderedle-all,
- list-del/get-rec
is used by
orderedls-all,
- list-del/sublist-prefix
is used by
ordered-shorter-sublist,
- list-del/app-01
is used by
perm-ins,
- list-del/del1-e
is used by
del1-01-02,
del1-01-01,
del1-01,
del1,
- list-del/del1-empty
is used by
del1,
- list-del/del1-n
is used by
del1-01-02,
del1-01-01,
- list-del/del1-y
is used by
del1-02,
del1-01-02,
del1-01-01,
del1-01,
del1,
- list-del/get-in
is used by
orderedls-all,
orderedle-all,
- list-del/get-numrec
is used by
orderedls-all,
orderedle-all,
- list-del/get-succ
is used by
orderedls-all,
orderedle-all,
- list-del/get-zero-01
is used by
orderedls-all,
orderedle-all,
- list-del/in-01-01
is used by
del1,
- list-del/one-01
is used by
del1-02,
- list-del/one-01-01
is used by
del1-01-02,
- list-del/one-03
is used by
orderedle-all,