x,s'. f(s';x))
t:AdjMatrix. t.size 
0
b else c(n-1,primrec(n-1;b;c)) fi (recursive)T:Type, n:, b:T, c:(n
TT). primrec(n;b;c) TA:Type, B:(AType), p:(a:A
B(a)). 1of(p) Aj == if i=j true ; false fii,j:
. (i=j) 
| Who Cites adjm-vertex-accum? | |
| adjm-vertex-accum | Def adjm-vertex-accum(M;s',x.f(s';x);s) == primrec(M.size;s;x,s'. f(s';x)) |
| adjm_size | Def t.size == 1of(t) |
| Thm* t:AdjMatrix. t.size | |
| primrec | Def primrec(n;b;c) == if n=0 b else c(n-1,primrec(n-1;b;c)) fi (recursive) |
| Thm* T:Type, n:, b:T, c:(nTT). primrec(n;b;c) T | |
| pi1 | Def 1of(t) == t.1 |
| Thm* A:Type, B:(AType), p:(a:AB(a)). 1of(p) A | |
| eq_int | Def i=j == if i=j true ; false fi |
| Thm* i,j:. (i=j) |
| Syntax: | adjm-vertex-accum(M;s',x.f(s';x);s) | has structure: | adjm-vertex-accum(M; s',x.f(s';x); s) |
About:
 |  |  |  |  |  |  |
 |  |  |  |  |  |
 |  |  |  |  |