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

Lemma dependency for Specification rowcol-upd

A lemma (entry) may depend on lemmas (entries) below its position, but never on lemmas above its position. This means the list is a topological order of the dependency graph. An entry 'all subs proved' means that all used lemmas are (transitively) proved.

Name: Status: Subs proved? Used:
perm-updcolprovedall subs proved perm-toArr-toArc, perm-updcol-aux,
perm-toArr-toArcprovedall subs proved oc-toArr-toArc,
oc-toArr-toArcprovedall subs proved oc-put-toArc, oc-put-toAr, put-outside-id, init-toArc, init-toArr,
perm-updcol-auxprovedall subs proved perm-updcol-ind, colno-updcol, toArc-def,
perm-updrowprovedall subs proved perm-updrow-ind, rowno-updrow, toArr-def,
perm-updcol-indprovedall subs proved overwrite-col, toArc-rec, toArc-base, toArc-outside-gen,
perm-updrow-indprovedall subs proved overwrite-row, toArr-rec, toArr-base, toArr-outside-gen,
oc-put-toArprovedall subs proved oc-put-toArr-rec, toArr-def,
oc-put-toArcprovedall subs proved oc-put-toArc-rec, toArc-def,
toArc-outsideprovedall subs proved toArc-outside-gen,
getmx-inmxprovedall subs proved in-toArr,
toArr-outsideprovedall subs proved toArr-outside-gen,
in-toArrprovedall subs proved in-toArr-ind, toArr-def,
oc-put-toArr-recprovedall subs proved oc-toArr-positive, getrow-putsame, put-selrow, toArr-rec, toArr-base,
toArr-outside-genprovedall subs proved overwrite-row, toArr-rec, toArr-base,
oc-put-toArc-recprovedall subs proved oc-toArc-positive, getcol-putsame, put-selcol, toArc-rec, toArc-base,
init-toArrprovedall subs proved init-toArr-rec, toArr-def,
init-toArcprovedall subs proved init-toArc-rec, toArc-def,
toArc-outside-genprovedall subs proved overwrite-col, toArc-rec, toArc-base,
in-toArr-indprovedall subs proved toArr-rec, toArr-base,
oc-toArc-positiveprovedall subs proved toArc-rec,
oc-toArr-positiveprovedall subs proved toArr-rec,
overwrite-rowprovedall subs proved updrow-sel, colno-updrow,
init-toArc-recprovedall subs proved selcol-mkmatrix, toArc-rec, toArc-base,
init-toArr-recprovedall subs proved selrow-mkmatrix, toArr-rec, toArr-base,
overwrite-colprovedall subs proved updcol-sel, rowno-updcol,
size-toArprovedall subs proved toArr-rec, toArr-base,
size-toArcprovedall subs proved toArc-rec, toArc-base,
rowno-updcolaxiom
updcol-selaxiom
put-selcolprovedall subs proved
getcol-putsameprovedall subs proved
put-selrowprovedall subs proved
getrow-putsameprovedall subs proved
colno-updcolaxiom
rowno-updrowaxiom
selcol-mkmatrixprovedall subs proved
selrow-mkmatrixprovedall subs proved
toArc-defaxiom
put-outside-idprovedall subs proved
toArr-defaxiom
toArr-baseaxiom
toArr-recaxiom
colno-updrowaxiom
updrow-selaxiom
toArc-baseaxiom
toArc-recaxiom