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

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:
mult-assocprovedall subs proved sum-multr, sum-multl, sum-red, sum-switch, multmx-get, multmx-colno, multmx-rowno,
sum-switchprovedall subs proved sum-add, sum-rec, sum-base,
multmx-columnprovedall subs proved sum-red, multmx-get, multmxvec-get, multmx-rowno, multmxvec-size,
distrmxvecvecprovedall subs proved sum-red, sum-add, addmvec-get, multmxvec-get, multmxvec-size, addvec-size,
distrmxmxvecprovedall subs proved addmx-get, sum-red, sum-add, addmvec-get, multmxvec-get, addmx-rowno, addmx-colno, multmxvec-size, addvec-size,
distrvecmxmxprovedall subs proved addmx-get, sum-red, sum-add, addmvec-get, multvecmx-get, addmx-colno, addmx-rowno, multvecmx-size, addvec-size,
singletonmxvec-getprovedall subs proved singletonmxvec-get-sum-aux, multmxvec-get,
distrvevecmxprovedall subs proved sum-red, sum-add, addmvec-get, multvecmx-get, multvecmx-size, addvec-size,
distrmxmx-lprovedall subs proved sum-red, sum-add, addmx-get, multmx-get, multmx-colno, addmx-colno, multmx-rowno, addmx-rowno,
distrmxmx-rprovedall subs proved sum-red, sum-add, addmx-get, multmx-get, multmx-colno, multmx-rowno, addmx-colno, addmx-rowno,
singletonmxvec-get-sum-auxprovedall subs proved sum-rec, sum-base,
sum-multlprovedall subs proved sum-rec, sum-base,
sum-multrprovedall subs proved sum-rec, sum-base,
sum-addprovedall subs proved sum-rec, sum-base,
sum-redprovedall subs proved sum-rec, sum-base,
addmx-assocprovedall subs proved addmx-get, addmx-colno, addmx-rowno,
addvec-comprovedall subs proved addmvec-get, addvec-size,
addvec-assocprovedall subs proved addmvec-get, addvec-size,
multmx-rowprovedall subs proved multvecmx-get, multmx-get, multvecmx-size, multmx-colno,
sum-unionprovedall subs proved sum-rec, sum-base,
addmx-comprovedall subs proved addmx-get, addmx-colno, addmx-rowno,
multvecmx-sizeaxiom
multvecmx-getaxiom
multmx-colnoaxiom
addvec-sizeaxiom
addmvec-getaxiom
addmx-rownoaxiom
addmx-colnoaxiom
addmx-getaxiom
sum-baseaxiom
sum-recaxiom
multmxvec-sizeaxiom
multmx-rownoaxiom
multmxvec-getaxiom
multmx-getaxiom