| | Who Cites spanner-root? |
|
| spanner-root | Def spanner-root(f;T;to;from;i) ==  l:Edge(T). (l  to(i))    (f(l)) |
|
| bi-graph-edge | Def Edge(G) == {l:IdLnk|  i:|G|. (l from(i)) } |
|
| rset | Def |R| == {i:Id| (R(i)) } |
| | | Thm* R:(Id   ). |R| Type |
|
| assert | Def b == if b True else False fi |
| | | Thm* b:. b Prop |
|
| bi-graph-to | Def to(i) == to(i) |
|
| l_member | Def (x l) == i: . i<||l|| & x = l[i] T |
| | | Thm* T:Type, x:T, l:T List. (x l) Prop |
|
| IdLnk | Def IdLnk == Id Id |
| | | Thm* IdLnk Type |
|
| select | Def l[i] == hd(nth_tl(i;l)) |
| | | Thm* A:Type, l:A List, n: . 0 n n<||l|| l[n] A |
|
| length | Def ||as|| == Case of as; nil 0 ; a.as' ||as'||+1 (recursive) |
| | | Thm* A:Type, l:A List. ||l|| |
| | | Thm* ||nil|| |
|
| Id | Def Id == Atom |
| | | Thm* Id Type |
|
| nat | Def == {i:| 0i } |
| | | Thm* Type |
|
| nth_tl | Def nth_tl(n;as) == if n 0 as else nth_tl(n-1;tl(as)) fi (recursive) |
| | | Thm* A:Type, as:A List, i:. nth_tl(i;as) A List |
|
| hd | Def hd(l) == Case of l; nil "?" ; h.t h |
| | | Thm* A:Type, l:A List. ||l|| 1 hd(l) A |
|
| le | Def AB ==  B<A |
| | | Thm* i,j:. (ij) Prop |
|
| tl | Def tl(l) == Case of l; nil nil ; h.t t |
| | | Thm* A:Type, l:A List. tl(l) A List |
|
| le_int | Def ij == j<i |
| | | Thm* i,j:. (ij) |
|
| not | Def A == A False |
| | | Thm* A:Prop. (A) Prop |
|
| lt_int | Def i<j == if i<j true ; false fi |
| | | Thm* i,j:. (i<j) |
|
| bnot | Def b == if b false else true fi |
| | | Thm* b:. b |
