x:A. B(x)
Q
b < c
j
t else f fiBj
bA
| Def | a = b = c | [rc_loop_sqrt_eqeq] | ||
| Def | | [nat] | int 1 | |
| Def | x:A. B(x) | [all] | core | |
| Def | P Q | [implies] | core | |
| Def | Prop | [prop] | core | |
| Def | a b < c | [rc_loop_sqrt_lelt] | ||
| Def | wrt(n,r) | [rc_loop_sqrt_wrt] | ||
| Def | (a)sqr | [rc_loop_sqrt_sqr] | ||
| Def | ij | [le_int] | bool 1 | |
| Def | if b t else f fi | [ifthenelse] | bool 1 | |
| Def | Y | [ycomb] | core | |
| Def | P & Q | [and] | core | |
| Def | AB | [le] | core | |
| Def | i < j | [lt_int] | bool 1 | |
| Def | b | [bnot] | bool 1 | |
| Def | A | [not] | core |
About:
 |  |  |  |  |  |  |  |
 |  |  |  |
 |  |  |  |  |  |  |  |  |  |
 |