| Who Cites rel star? |
|
rel_star | Def (R^*)(x,y) == n: . x R^n y |
| | Thm* T:Type, R:(T![](FONT/dash.png) T![](FONT/dash.png) Prop). (R^*) T![](FONT/dash.png) T![](FONT/dash.png) 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![](FONT/dash.png) T![](FONT/dash.png) Prop). R^n T![](FONT/dash.png) T![](FONT/dash.png) Prop |
|
nat | Def == {i: | 0 i } |
| | Thm* Type |
|
eq_int | Def i= j == if i=j true ; false fi |
| | Thm* i,j: . (i= j) ![](FONT/bool.png) |
|
le | Def A B == B<A |
| | Thm* i,j: . (i j) Prop |
|
not | Def A == A ![](FONT/eq.png) False |
| | Thm* A:Prop. ( A) Prop |