[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,
distrvecmxmxprovedall subs proved addmx-get, sum-red, sum-add, addmvec-get, multvecmx-get, addmx-colno, addmx-rowno, multvecmx-size, addvec-size,
distrmxmxvecprovedall subs proved addmx-get, sum-red, sum-add, addmvec-get, multmxvec-get, addmx-rowno, addmx-colno, multmxvec-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,
distrmxvecvecprovedall subs proved sum-red, sum-add, addmvec-get, multmxvec-get, multmxvec-size, addvec-size,
multmx-columnprovedall subs proved sum-red, multmx-get, multmxvec-get, multmx-rowno, multmxvec-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,
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,
addvec-comprovedall subs proved addmvec-get, addvec-size,
addmx-comprovedall subs proved addmx-get, addmx-colno, addmx-rowno,
addvec-assocprovedall subs proved addmvec-get, addvec-size,
sum-unionprovedall subs proved sum-rec, sum-base,
addmx-assocprovedall subs proved addmx-get, addmx-colno, addmx-rowno,
multmx-rowprovedall subs proved multvecmx-get, multmx-get, multvecmx-size, multmx-colno,
sum-baseaxiom
sum-recaxiom
multmxvec-sizeaxiom
multmxvec-getaxiom
multmx-rownoaxiom
multmx-colnoaxiom
multmx-getaxiom
multvecmx-sizeaxiom
multvecmx-getaxiom
addmx-rownoaxiom
addmx-colnoaxiom
addmx-getaxiom
addvec-sizeaxiom
addmvec-getaxiom