[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 list-last
- list-last/lapp
is used by
orderedCombined-Two-Lists,
- list-last/postfix-is-lessOrEqual
is used by
ordered-postfix,
- list-last/prefix-rec-01
is used by
ordered-prefix,
- list-last/l-02
is used by
orderedle-append,
- list-last/lapp-04
is used by
ole-last,
- list-last/last-def
is used by
orderedle-append2-split,
ordered-append-split2,
ordered-last1,
ordered-append,
orderedls-twolast,
- list-last/last-elim
is used by
ordle-append,
ordered-last3,
ordered-append-split2,
ordered-last1,
ordered-sublist2,
ordered-append,
ordered-last2,
ordered-append-split1,
ole-last,
ole-last-01,
- list-last/last-one
is used by
orderedle-append,
orderedCombined-Two-Lists,
- 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 nat
- nat/add-num-01
is used by
len,
- nat/elim-pred-c
is used by
orderedle-all,
orderedls-all,
- nat/fle
is used by
orderedls-all,
- nat/l-num-06
is used by
orderedls-all,
- nat/le-def
is used by
ordered-postfix,
- nat/le-ls-simp
is used by
orderedle-all,
orderedls-all,
- nat/le-num-06
is used by
orderedle-append,
- nat/le-sum
is used by
orderedle-all,
- nat/lels
is used by
orderedle-all,
orderedls-all,
- nat/lels-03
is used by
ordered-shorter-sublist,
- nat/lep-02
is used by
orderedle-all,
orderedls-all,
- nat/let
is used by
orderedle-all,
- nat/lez
is used by
orderedle-all,
orderedls-all,
- nat/lez-01
is used by
orderedle-all,
- nat/ls-add-not-01
is used by
orderedle-all,
orderedls-all,
- nat/one-01
is used by
szle1-orderedle,
k-ls-r,
k-le-r,
szle1-orderedls,
ordered-prefix,
- nat/pred-03
is used by
orderedle-all,
- nat/succ-01
is used by
orderedle-all,
orderedls-all,
ordered-prefix,
Used from specification weakord
- weakord/irreflexivity
is used by
orderedle-all,
ins-one-02,
del1-02,
ins-y-01,
orderedls-all,
ordered-nodup,
orderedls-eq,
ole-01,
orderedls-ls,
ole-last,
orderedls-ls-attach,
eq,
orderedls-eq-attach,
- weakord/lel
is used by
orderedls-le-attach,
ole-01,
orderedls-ls-attach,
eq,
- weakord/leq-trans
is used by
orderedle-all,
ordered-ex-divide-lsle,
del1-01-02,
ole-last,
ole-in,
del1-01,
- weakord/nen
is used by
ordered-sublist2,
ordered-postfix,
ole-01,
ole-last,
eq,
- weakord/nll
is used by
orderedle-all,
ordered-append-split2,
ordered-last1,
orderedls-all,
ordered-ex-divide-lels,
orderedls-le-attach,
ordered-ex-divide-lsle,
ole-01,
ordered-last2,
ole-in,
del1,
orderedls-le,
del1-01,
- weakord/transitivity
is used by
ins-one-02,
ins-y-01,
ordered-sublist2,
ordered-ordered-subset-ordered,
ole-01,
orderedls-ls,
orderedls-ls-attach,
Used from specification list-perm
- list-perm/cons
is used by
insperm-01,
- list-perm/del-01
is used by
insperm,
sort-possible,
- list-perm/perm-del
is used by
perm-ins,
- list-perm/trans
is used by
insperm-01,
- list-perm/a
is used by
insperm-01,
- list-perm/app-beg-beg
is used by
perm-ins,
insperm-03,
insperm-01,
insperm-02,
- list-perm/app-beg-end
is used by
perm-ins,
- list-perm/empty-01
is used by
sort-possible,
- list-perm/ref
is used by
insperm,
perm-ins,
insperm-03,
insperm-01,
insperm-02,
- 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-01,
insperm-02,
- list-perm/trans
is used by
perm-ins,
insperm-03,
insperm-01,
Used from specification list-data
- list-data/elim-add
is used by
ins-yes,
ordered-last3,
ins-rec,
ordered-append-first,
app,
ordered-sublist2,
ordered-append,
ins-less-first,
orderedCombined-Two-Lists,
ordered-append-split1,
eq,
- list-data/elim-list-c
is used by
ordle-append,
orderedle-all,
k-ls-r,
rest,
k-le-r,
ole-rec,
rest-01,
ordered-append-split2,
ordered-sublist2,
orderedls-all,
ols-rec,
orderedls-le-attach,
ordered-postfix,
ole-01,
del1-01-02,
orderedle-append,
ole-last,
orderedls-ls-attach,
del1,
ordered-prefix,
del1-01,
- list-data/l
is used by
szle1-orderedle,
orderedle-all,
k-ls-r,
k-le-r,
ordered-shorter-sublist,
orderedls-all,
ordered-postfix,
szle1-orderedls,
ordered-prefix,
- list-data/size-nil
is used by
szle1-orderedle,
orderedle-all,
k-ls-r,
k-le-r,
orderedls-all,
len,
szle1-orderedls,
Used from specification nat-basic
- nat-basic/a
is used by
szle1-orderedle,
orderedle-all,
k-ls-r,
k-le-r,
orderedls-all,
len,
szle1-orderedls,
sort-possible,
orderedle-append,
ordered-prefix,
- nat-basic/c
is used by
szle1-orderedle,
orderedle-all,
k-ls-r,
k-le-r,
orderedls-all,
len,
szle1-orderedls,
sort-possible,
orderedle-append,
ordered-prefix,
- nat-basic/eq-01
is used by
len,
sort-possible,
- nat-basic/f
is used by
orderedle-all,
ordered-shorter-sublist,
orderedls-all,
- nat-basic/l
is used by
orderedls-all,
- nat-basic/less-zero
is used by
orderedle-all,
orderedls-all,
- nat-basic/lf-02
is used by
orderedls-all,
- nat-basic/nls-fst
is used by
orderedle-all,
orderedls-all,
- nat-basic/one
is used by
ordered-postfix,
- nat-basic/one-01
is used by
ordered-prefix,
- nat-basic/oz
is used by
orderedle-all,
orderedls-all,
- nat-basic/s-04
is used by
orderedle-all,
orderedls-all,
- nat-basic/succ
is used by
szle1-orderedle,
orderedle-all,
k-ls-r,
k-le-r,
orderedls-all,
len,
szle1-orderedls,
sort-possible,
orderedle-append,
ordered-prefix,
- nat-basic/zero
is used by
orderedle-all,
orderedls-all,
Used from specification list
- list/Nil
is used by
ordle-append,
app-02,
ordered-append-second,
ex,
ins-less-last,
ordered-sublist,
ordered-append-split2,
ordered-append-first,
app,
ordered-sublist2,
ordls-append,
ordered-ordered-subset-ordered,
ordered-nodup,
ordered-ex-divide-lels,
ordered-ex-divide-lsle,
orderedle-append,
app-01,
ordered-last2,
orderedCombined-Two-Lists,
ordered-append-split1,
ole-last,
insperm-02,
- list/a
is used by
ordle-append,
cons-02,
szle1-orderedle,
orderedle-all,
ins-one-02,
k-ls-r,
rest,
same,
app-02,
ordered-append-second,
perm-ins,
ex,
k-le-r,
ins-yes,
del1-02,
ins-less-last,
ordered-last3,
ole-rec,
rest-01,
ordered-sublist,
orderedle-append2-split,
ordered-append-split2,
insperm-03,
ins-one,
ins-rec,
ordered-append-first,
app,
ins-y-01,
in-01-02,
ordered-last1,
ordered-sublist2,
orderedls-all,
ole-two,
ordls-append,
ordered-ordered-subset-ordered,
one-02,
ordered-nodup,
cons-03,
ordered-ex-divide-lels,
in-04,
ols-rec,
orderedls-le-attach,
len,
insperm-01,
empty,
ordered-ex-divide-lsle,
orderedle-ls,
ordered-postfix,
ole-01,
orderedls-ls,
szle1-orderedls,
sort-possible,
del1-01-02,
orderedle-append,
ordered-append,
ins-less-first,
app-01,
ordered-last2,
cons,
orderedCombined-Two-Lists,
ols-two,
ordered-append-split1,
ole-last,
orderedle-twolast,
ins-one-01,
orderedls-ls-attach,
orderedls-append2-split,
ole-in,
insperm-02,
eq,
ole-last-01,
del1,
ordered-prefix,
orderedls-le,
orderedls-twolast,
del1-01,
- list/app
is used by
ordle-append,
cons-02,
szle1-orderedle,
orderedle-all,
ins-one-02,
k-ls-r,
ordered-append-second,
ex,
k-le-r,
ordered-last3,
ins-one,
ordered-append-first,
app,
ordered-sublist2,
orderedls-all,
ole-two,
ordls-append,
cons-03,
ordered-postfix,
ole-01,
szle1-orderedls,
del1-01-02,
orderedle-append,
cons,
orderedCombined-Two-Lists,
ole-last,
ins-one-01,
del1,
del1-01,
- list/app-01
is used by
ordered-ex-divide-lels,
ordered-ex-divide-lsle,
- list/app-02
is used by
ordle-append,
orderedle-all,
k-ls-r,
rest,
ex,
k-le-r,
ordered-last3,
ole-rec,
rest-01,
orderedle-append2-split,
ordered-append-split2,
ordered-append-first,
app,
ordered-last1,
ordered-sublist2,
orderedls-all,
ordered-ordered-subset-ordered,
ols-rec,
orderedls-le-attach,
empty,
ordered-postfix,
ole-01,
del1-01-02,
orderedle-append,
ordered-append,
ordered-last2,
orderedCombined-Two-Lists,
ols-two,
ordered-append-split1,
ole-last,
orderedls-ls-attach,
orderedls-append2-split,
eq,
del1,
ordered-prefix,
orderedls-twolast,
del1-01,
- list/c
is used by
ordle-append,
cons-02,
szle1-orderedle,
orderedle-all,
ins-one-02,
k-ls-r,
rest,
same,
app-02,
ex,
k-le-r,
ins-yes,
del1-02,
ins-less-last,
ordered-last3,
ole-rec,
rest-01,
ordered-append-split2,
insperm-03,
ins-one,
ins-rec,
ordered-append-first,
app,
ins-y-01,
in-01-02,
ordered-sublist2,
orderedls-all,
cons-03,
ordered-ex-divide-lels,
in-04,
ols-rec,
orderedls-le-attach,
len,
empty,
ordered-ex-divide-lsle,
ordered-postfix,
ole-01,
orderedls-ls,
szle1-orderedls,
sort-possible,
del1-01-02,
orderedle-append,
ordered-append,
ins-less-first,
app-01,
cons,
orderedCombined-Two-Lists,
ordered-append-split1,
ole-last,
ins-one-01,
orderedls-ls-attach,
ole-in,
insperm-02,
eq,
del1,
ordered-prefix,
orderedls-le,
del1-01,
- list/c-03
is used by
ole-01,
eq,
- list/c-04
is used by
ex,
cons-03,
del1-01-02,
- list/c-05
is used by
ole-last,
- list/c-06
is used by
ordered-sublist2,
ordered-postfix,
ole-01,
ins-less-first,
eq,
del1-01,
- list/c-07
is used by
orderedle-all,
ordered-append-split2,
ordered-append-first,
app,
orderedls-all,
orderedls-le-attach,
ordered-postfix,
ole-01,
del1-01-02,
orderedle-append,
orderedCombined-Two-Lists,
ols-two,
ole-last,
orderedls-ls-attach,
del1,
ordered-prefix,
del1-01,
- list/c-08
is used by
ordle-append,
orderedle-all,
orderedle-append2-split,
ordered-append-split2,
ordered-append-first,
app,
orderedls-all,
ordered-ordered-subset-ordered,
orderedls-le-attach,
ordered-postfix,
ole-01,
del1-01-02,
orderedle-append,
orderedCombined-Two-Lists,
ols-two,
ole-last,
orderedls-ls-attach,
orderedls-append2-split,
del1,
ordered-prefix,
del1-01,
- list/e
is used by
ordle-append,
orderedle-all,
k-ls-r,
rest,
k-le-r,
ordered-last3,
ole-rec,
rest-01,
orderedle-append2-split,
ordered-append-split2,
ordered-append-first,
app,
ordered-last1,
ordered-sublist2,
orderedls-all,
ordered-ordered-subset-ordered,
ols-rec,
orderedls-le-attach,
empty,
ordered-attach,
ordered-postfix,
ole-01,
del1-01-02,
orderedle-append,
ordered-append,
ordered-last2,
orderedCombined-Two-Lists,
ols-two,
ordered-append-split1,
ole-last,
orderedls-ls-attach,
orderedls-append2-split,
eq,
del1,
ordered-prefix,
orderedls-twolast,
del1-01,
- list/e-01
is used by
ins-less-first,
- list/first
is used by
ordered-attach,
ols-two,
- list/first-01
is used by
ordered-append-first,
orderedle-append,
orderedCombined-Two-Lists,
- list/first-02
is used by
ordered-append-split2,
ole-last,
- list/in-01
is used by
in-01-02,
ole-last,
- 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-append-split2,
ordered-sublist2,
orderedls-le-attach,
ordered-postfix,
ole-01,
ole-last,
orderedls-ls-attach,
eq,
del1,
del1-01,
- list/in-15
is used by
ordered-append-split2,
orderedls-le-attach,
ole-last,
orderedls-ls-attach,
- list/in-17
is used by
ordered-append-split2,
in-01-02,
ordered-ex-divide-lels,
in-04,
orderedls-le-attach,
ordered-ex-divide-lsle,
ole-01,
ole-last,
orderedls-ls-attach,
- list/in-append
is used by
ordered-last3,
ordered-append-split2,
ordered-sublist2,
ordered-ordered-subset-ordered,
ordered-nodup,
ordered-ex-divide-lels,
orderedls-le-attach,
ordered-ex-divide-lsle,
ole-last,
orderedls-ls-attach,
- list/in-empty
is used by
in-01-02,
ordered-ex-divide-lels,
orderedls-le-attach,
ordered-ex-divide-lsle,
orderedls-ls,
ole-last,
orderedls-ls-attach,
ole-in,
orderedls-le,
- list/in-rec
is used by
ordered-last3,
ordered-append-split2,
in-01-02,
ordered-sublist2,
ordered-ordered-subset-ordered,
ordered-nodup,
orderedls-le-attach,
ordered-postfix,
ole-01,
orderedls-ls,
ole-last,
orderedls-ls-attach,
ole-in,
eq,
del1,
orderedls-le,
del1-01,
- list/inapp-02
is used by
ordered-sublist2,
- list/inapp-07
is used by
ole-last,
- list/inapp-10
is used by
ole-last,
- list/len
is used by
orderedle-append,
- list/len-01
is used by
same,
ex,
ins-yes,
del1-02,
ins-less-last,
ins-rec,
one-02,
cons-03,
del1-01-02,
eq,
- list/len-02
is used by
len,
ordered-postfix,
- list/len-05
is used by
szle1-orderedle,
orderedle-all,
k-ls-r,
k-le-r,
orderedls-all,
len,
szle1-orderedls,
sort-possible,
orderedle-append,
ordered-prefix,
- list/len-06
is used by
ex,
ole-last,
- 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 list-del
- list-del/app
is used by
perm-ins,
- list-del/del1-n
is used by
del1-02,
del1-01-02,
del1,
del1-01,
- list-del/get-numrec
is used by
orderedle-all,
- list-del/sublist-prefix
is used by
ordered-shorter-sublist,
- list-del/del1-e
is used by
del1-01-02,
del1,
del1-01,
- list-del/del1-empty
is used by
del1,
- list-del/del1-n
is used by
del1-01-02,
- list-del/del1-y
is used by
del1-02,
del1-01-02,
del1,
del1-01,
- list-del/get-in
is used by
orderedle-all,
orderedls-all,
- list-del/get-numrec
is used by
orderedle-all,
orderedls-all,
- list-del/get-succ
is used by
orderedle-all,
orderedls-all,
- list-del/get-zero
is used by
orderedle-all,
orderedls-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,
Used from specification list-getput