| | Some definitions of interest. |
|
| IdLnk | Def IdLnk == Id Id |
| | | Thm* IdLnk  Type |
|
| rset | Def |R| == {i:Id|  (R(i)) } |
| | | Thm*  R:(Id   ). |R| Type |
|
| Id | Def Id == Atom |
| | | Thm* Id Type |
|
| assert | Def b == if b True else False fi |
| | | Thm* b:. b Prop |
|
| l_all | Def (xL.P(x)) == x:T. (x L)   P(x) |
| | | Thm* T:Type, L:T List, P:(TProp). (xL.P(x)) Prop |
|
| l_member | Def (x l) ==  i:. i<||l|| & x = l[i] T |
| | | Thm* T:Type, x:T, l:T List. (x l) Prop |
|
| ldst | Def destination(l) == 1of(2of(l)) |
| | | Thm* l:IdLnk. destination(l) Id |
|
| lnk-inv | Def lnk-inv(l) == <1of(2of(l)),1of(l),2of(2of(l))> |
|
| lsrc | Def source(l) == 1of(l) |
| | | Thm* l:IdLnk. source(l) Id |
