[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/list-as-arrayinstance/mk-plus
is used by
init-toArc-rec,
init-toArr-rec,
- list-last/list-as-arrayinstance/mk-inj-01
is used by
init-toArc,
init-toArr,
- list-last/list-as-arrayinstance/mk-len
is used by
selcol-mkmatrix,
selrow-mkmatrix,
- list-last/list-as-arrayinstance/mk-zero
is used by
init-toArc-rec,
init-toArr-rec,
init-toArc,
init-toArr,
Used from specification nat
- nat/prop-05
is used by
oc-put-toArc-rec,
oc-put-toArr-rec,
- nat/add-01
is used by
oc-put-toArc-rec,
oc-put-toArr-rec,
oc-toArr-toArc,
- nat/anti
is used by
oc-toArc-positive,
oc-toArr-positive,
in-toArr-ind,
- nat/elim-pred-c
is used by
oc-put-toArc-rec,
oc-put-toArr-rec,
- nat/eq-01
is used by
oc-put-toArc-rec,
oc-put-toArr-rec,
- nat/eq-02
is used by
oc-put-toArc-rec,
oc-put-toArr-rec,
- nat/fle
is used by
putcol-outside-id,
putrow-outside-id,
- nat/fle-01
is used by
toArc-outside-gen,
toArr-outside-gen,
in-toArr-ind,
- nat/le-def
is used by
in-toArr,
toArr-outside,
oc-put-toArc-rec,
oc-put-toArr-rec,
perm-updrow-ind,
init-toArc,
toArc-outside,
init-toArr,
perm-updcol-ind,
- nat/lels
is used by
oc-toArc-positive,
put-selrow,
oc-toArr-positive,
in-toArr-ind,
put-selcol,
- nat/lels-03
is used by
oc-put-toArc-rec,
toArc-outside-gen,
oc-put-toArr-rec,
toArr-outside-gen,
perm-updrow-ind,
init-toArc-rec,
init-toArr-rec,
in-toArr-ind,
perm-updcol-ind,
- nat/ler
is used by
in-toArr,
oc-put-toAr,
oc-toArc-positive,
perm-updcol-aux,
perm-updrow,
oc-put-toArc,
oc-toArr-positive,
in-toArr-ind,
- nat/lez
is used by
perm-updrow-ind,
init-toArc,
init-toArr,
in-toArr-ind,
perm-updcol-ind,
- nat/ls-le-simp
is used by
putcol-outside-id,
putrow-outside-id,
put-selrow,
put-selcol,
- nat/pred-03
is used by
oc-put-toArc-rec,
oc-put-toArr-rec,
- nat/sub-base
is used by
oc-put-toArc-rec,
oc-put-toArr-rec,
oc-toArr-toArc,
- nat/succ-01
is used by
oc-put-toArc-rec,
toArc-outside-gen,
oc-put-toArr-rec,
toArr-outside-gen,
perm-updrow-ind,
init-toArc-rec,
init-toArr-rec,
in-toArr-ind,
perm-updcol-ind,
Used from specification nat-mult
- nat-mult/mult-a
is used by
size-toArc,
init-toArc-rec,
init-toArr-rec,
init-toArc,
size-toAr,
init-toArr,
- nat-mult/mult-c
is used by
size-toArc,
init-toArc-rec,
init-toArr-rec,
init-toArc,
size-toAr,
init-toArr,
- nat-mult/rsucc-02
is used by
size-toArc,
init-toArc-rec,
init-toArr-rec,
size-toAr,
- nat-mult/zero
is used by
size-toArc,
init-toArc-rec,
init-toArr-rec,
init-toArc,
size-toAr,
init-toArr,
- nat-mult/zero-02
is used by
init-toArc,
Used from specification nat-basic
- nat-basic/a
is used by
size-toArc,
oc-put-toArc-rec,
toArc-outside-gen,
oc-put-toArr-rec,
oc-toArc-positive,
toArr-outside-gen,
perm-updrow-ind,
init-toArc-rec,
init-toArr-rec,
size-toAr,
oc-toArr-positive,
oc-toArr-toArc,
in-toArr-ind,
perm-updcol-ind,
- nat-basic/add-base
is used by
oc-put-toArc-rec,
oc-put-toArr-rec,
oc-toArr-toArc,
- nat-basic/c
is used by
size-toArc,
oc-put-toArc-rec,
toArc-outside-gen,
oc-put-toArr-rec,
oc-toArc-positive,
toArr-outside-gen,
perm-updrow-ind,
init-toArc-rec,
init-toArr-rec,
size-toAr,
oc-toArr-positive,
oc-toArr-toArc,
in-toArr-ind,
perm-updcol-ind,
- nat-basic/eq-01
is used by
size-toArc,
oc-put-toArc-rec,
oc-put-toArr-rec,
size-toAr,
oc-toArr-toArc,
- nat-basic/eq-02
is used by
oc-put-toArc-rec,
oc-put-toArr-rec,
- nat-basic/f
is used by
putcol-getcol,
putcol-outside-id,
size-toArc,
putrow-id,
getmx-inmx,
oc-put-toArc-rec,
putcol-id,
toArc-outside-gen,
oc-put-toArr-rec,
oc-put-toAr,
oc-toArc-positive,
toArr-outside-gen,
perm-updrow-ind,
putrow-getrow-gr,
putcol-getcol-gr,
perm-updcol-aux,
putrow-outside-id,
selcol-mkmatrix,
init-toArc-rec,
perm-updrow,
putrow-getrow-ls,
putcol-getcol-ls,
init-toArr-rec,
oc-put-toArc,
put-selrow,
init-toArc,
putrow-getrow,
size-toAr,
oc-toArr-positive,
oc-toArr-toArc,
in-toArr-ind,
put-selcol,
perm-updcol-ind,
perm-updcol,
selrow-mkmatrix,
- nat-basic/less-zero
is used by
oc-put-toArc-rec,
oc-put-toArr-rec,
oc-toArc-positive,
oc-toArr-positive,
in-toArr-ind,
- nat-basic/lf
is used by
oc-put-toArc-rec,
toArc-outside-gen,
oc-put-toArr-rec,
oc-toArc-positive,
toArr-outside-gen,
putrow-getrow-ls,
putcol-getcol-ls,
oc-toArr-positive,
in-toArr-ind,
- nat-basic/lf-01
is used by
putcol-outside-id,
putrow-outside-id,
- nat-basic/lf-02
is used by
oc-toArc-positive,
oc-toArr-positive,
in-toArr-ind,
- nat-basic/ls-02
is used by
oc-put-toArc-rec,
oc-put-toArr-rec,
in-toArr-ind,
- nat-basic/neq-01
is used by
oc-put-toArc-rec,
oc-put-toArr-rec,
- nat-basic/nls-fst
is used by
size-toArc,
oc-toArc-positive,
size-toAr,
oc-toArr-positive,
- nat-basic/one-01
is used by
oc-put-toArc-rec,
oc-put-toArr-rec,
- nat-basic/oz
is used by
oc-put-toArc-rec,
oc-put-toArr-rec,
- nat-basic/refl-nat
is used by
in-toArr,
toArr-outside,
oc-put-toArc-rec,
toArc-outside-gen,
oc-put-toArr-rec,
toArr-outside-gen,
perm-updrow-ind,
putrow-getrow-gr,
putcol-getcol-gr,
putrow-getrow-ls,
putcol-getcol-ls,
init-toArc,
toArc-outside,
init-toArr,
in-toArr-ind,
perm-updcol-ind,
- nat-basic/s-04
is used by
oc-put-toArc-rec,
oc-put-toArr-rec,
oc-toArc-positive,
oc-toArr-positive,
in-toArr-ind,
- nat-basic/succ
is used by
size-toArc,
oc-put-toArc-rec,
toArc-outside-gen,
oc-put-toArr-rec,
oc-toArc-positive,
toArr-outside-gen,
perm-updrow-ind,
init-toArc-rec,
putrow-getrow-ls,
putcol-getcol-ls,
init-toArr-rec,
size-toAr,
oc-toArr-positive,
in-toArr-ind,
perm-updcol-ind,
- nat-basic/trans-nat
is used by
oc-put-toArc-rec,
toArc-outside-gen,
oc-put-toArr-rec,
oc-toArc-positive,
toArr-outside-gen,
putrow-getrow-ls,
putcol-getcol-ls,
oc-toArr-positive,
in-toArr-ind,
- nat-basic/z-01
is used by
oc-put-toArc-rec,
oc-put-toArr-rec,
- nat-basic/zero
is used by
oc-toArc-positive,
oc-toArr-positive,
Used from specification matrix
- matrix/cngetput-c
is used by
put-selcol,
- matrix/cngetput-num-r
is used by
put-selcol,
- matrix/extension
is used by
putcol-outside-id,
putrow-id,
putcol-id,
putrow-outside-id,
- matrix/colno-mkmatrix
is used by
init-toArc,
selrow-mkmatrix,
- matrix/colno-put
is used by
oc-put-toArc,
put-selrow,
- matrix/eq-write-left
is used by
put-outside-id,
- matrix/get-mkmatrix
is used by
selcol-mkmatrix,
selrow-mkmatrix,
- matrix/put-othercol
is used by
put-selrow,
- matrix/put-otherrow
is used by
put-selrow,
- matrix/put-same
is used by
put-selrow,
put-selcol,
- matrix/put-same-content
is used by
oc-put-toArc-rec,
oc-put-toArr-rec,
- matrix/rowno-mkmatrix
is used by
selcol-mkmatrix,
init-toArr,
- matrix/rowno-put
is used by
oc-put-toAr,
put-selcol,
Used from specification list
- list/list-as-arrayinstance/a
is used by
size-toArc,
oc-put-toArc-rec,
toArc-outside-gen,
oc-put-toArr-rec,
oc-toArc-positive,
toArr-outside-gen,
perm-updrow-ind,
init-toArc-rec,
init-toArr-rec,
size-toAr,
oc-toArr-positive,
in-toArr-ind,
perm-updcol-ind,
- list/list-as-arrayinstance/in-append
is used by
oc-toArc-positive,
oc-toArr-positive,
in-toArr-ind,
- list/list-as-arrayinstance/in-empty
is used by
in-toArr-ind,
- list/list-as-arrayinstance/len
is used by
size-toArc,
size-toAr,
- list/list-as-arrayinstance/len-06
is used by
toArc-outside-gen,
toArr-outside-gen,
init-toArc-rec,
init-toArr-rec,
- matrix+array/selcol-get
is used by
putcol-getcol,
oc-put-toArc-rec,
putcol-id,
oc-toArc-positive,
getcol-putsame,
selcol-mkmatrix,
put-selcol,
- matrix+array/selcol-size
is used by
putcol-getcol,
size-toArc,
oc-put-toArc-rec,
putcol-id,
oc-toArc-positive,
getcol-putsame,
selcol-mkmatrix,
put-selcol,
- matrix+array/selrow-get
is used by
putrow-id,
oc-put-toArr-rec,
getrow-putsame,
put-selrow,
putrow-getrow,
oc-toArr-positive,
in-toArr-ind,
selrow-mkmatrix,
- matrix+array/selrow-size
is used by
putrow-id,
oc-put-toArr-rec,
getrow-putsame,
put-selrow,
putrow-getrow,
size-toAr,
oc-toArr-positive,
in-toArr-ind,
selrow-mkmatrix,
Used from specification array
- array/Extension
is used by
putcol-getcol,
put-selrow,
putrow-getrow,
put-selcol,
- array/Put-other
is used by
put-selrow,
- array/Put-other
is used by
put-selcol,
- array/Size-put
is used by
put-selrow,
put-selcol,
- array/cgetput
is used by
put-selrow,
put-selcol,
- array/eq-write-left
is used by
getcol-putsame,
getrow-putsame,
Used from specification list-perm
- list-perm/list-as-arrayinstance/ocs-put
is used by
oc-put-toArc-rec,
oc-put-toArr-rec,
- list-perm/list-as-arrayinstance/ocs-put-01
is used by
oc-put-toArc-rec,
oc-put-toArr-rec,
- list-perm/list-as-arrayinstance/ocs-put-02
is used by
oc-put-toArc-rec,
oc-put-toArr-rec,
- list-perm/list-as-arrayinstance/perm-all
is used by
perm-toArr-toArc,
- list-perm/list-as-arrayinstance/sym
is used by
perm-updcol,
- list-perm/list-as-arrayinstance/trans
is used by
perm-updcol,
- list-perm/list-as-arrayinstance/a
is used by
perm-updrow-ind,
perm-updcol-ind,
- list-perm/list-as-arrayinstance/app-end-end
is used by
perm-updrow-ind,
perm-updcol-ind,
- list-perm/list-as-arrayinstance/notin
is used by
oc-put-toArc-rec,
oc-put-toArr-rec,
- list-perm/list-as-arrayinstance/oc-e
is used by
oc-put-toArc-rec,
oc-put-toArr-rec,
- list-perm/list-as-arrayinstance/oc-zero
is used by
oc-put-toArc-rec,
oc-put-toArr-rec,
oc-toArc-positive,
oc-toArr-positive,
- list-perm/list-as-arrayinstance/ocappend
is used by
oc-put-toArc-rec,
oc-put-toArr-rec,
- list-perm/list-as-arrayinstance/perm-e
is used by
perm-updrow-ind,
perm-updcol-ind,
Used from specification list-data
Used from specification list-del
Used from specification list-getput