| Who Cites rel star? |
|
rel_star | Def (R^*)(x,y) == n: . x R^n y |
| | Thm* T:Type, R:(T T Prop). (R^*) T T Prop |
|
rel_exp | Def R^n == if n= 0 x,y. x = y T else x,y. z:T. (x R z) & (z R^n-1 y) fi
Def (recursive) |
| | Thm* n: , T:Type, R:(T T Prop). R^n T T Prop |
|
nat | Def == {i: | 0 i } |
| | Thm* Type |
|
eq_int | Def i= j == if i=j true ; false fi |
| | Thm* i,j: . (i= j)  |
|
le | Def A B == B<A |
| | Thm* i,j: . (i j) Prop |
|
not | Def A == A  False |
| | Thm* A:Prop. ( A) Prop |