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