| | 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 |
|
| eq_id | Def a = b == eqof(IdDeq)(a,b) |
| | | Thm* a,b:Id. a = b |
|
| assert | Def b == if b True else False fi |
| | | Thm* b:. b Prop |
|
| fun_exp | Def f^n == primrec(n; x.x;i,g. f o g) |
| | | Thm* T:Type, n:, f:(TT). f^n TT |
|
| rnext | Def n(i) == destination(out(i)) |
| | | Thm* R:(Id), in,out:(|R|IdLnk), i:|R|. ring(R;in;out)   n(i) |R| |
|
| ldst | Def destination(l) == 1of(2of(l)) |
| | | Thm* l:IdLnk. destination(l) Id |
|
| lsrc | Def source(l) == 1of(l) |
| | | Thm* l:IdLnk. source(l) Id |
|
| nat | Def == {i: | 0 i } |
| | | Thm* Type |
|
| nat_plus | Def  == {i:| 0<i } |
| | | Thm* Type |
