[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
,
Theorem base summary for Specification matrixops
Status:
Proved!
Axioms: 19, User Theorems: 21 (Proved: 21, Partially proved: 0, Unproved: 0, Invalid: 0, Siginvalid: 0)
Proof steps: 237, Interactions: 123
addinvmx-colno(0,0)
addmx-assoc(4,2)
addvec-com(2,1)
distrvecmxmx(20,10)
multmx-row(6,3)
singletonmxvec-get(4,2)
sum-rec(0,0)
addinvmx-get(0,0)
addmx-colno(0,0)
addvec-size(0,0)
distrvevecmx(19,10)
multmx-rowno(0,0)
singletonmxvec-get-sum-aux(14,7)
sum-red(11,5)
addinvmx-rowno(0,0)
addmx-com(2,1)
distrmxmx-l(18,9)
mult-assoc(25,14)
multmxvec-get(0,0)
sum-add(7,3)
sum-switch(12,7)
addinvvec-get(0,0)
addmx-get(0,0)
distrmxmx-r(21,11)
multmx-colno(0,0)
multmxvec-size(0,0)
sum-base(0,0)
sum-union(11,6)
addinvvec-size(0,0)
addmx-rowno(0,0)
distrmxmxvec(16,8)
multmx-column(7,5)
multvecmx-get(0,0)
sum-multl(8,4)
addmvec-get(0,0)
addvec-assoc(4,2)
distrmxvecvec(18,9)
multmx-get(0,0)
multvecmx-size(0,0)
sum-multr(8,4)