n:
, R:(n
nProp). (i,j:n. Dec(i R j)) 
(i,j:n. Dec(i (R^*) j))n:, R:(nnProp), x,y:n. (x (R^*) y) 
(
k:(n+1). x R^k y)| Rank | Theorem | Name |
| 4 | n:, R:(nnProp). (i,j:n. Dec(i R j)) (i,j:n. Dec(i (R^*) j)) | [decidable__rel_star] |
| cites the following: | ||
| 3 | n:, R:(nnProp), x,y:n. (x (R^*) y) (k:(n+1). x R^k y) | [rel_star_finite] |