Def | i![]() | [ge] | core |
Def | {...i} | [int_lower] | int 1 |
Def | Rem(a;n;r) | [rem_nrel] | |
Def | {i...} | [int_upper] | int 1 |
Def | {i..j![]() | [int_seg] | int 1 |
Def | Div(a;n;q) | [div_nrel] | |
Def | i ![]() | [lelt] | int 1 |
Def | ![]() | [nat] | int 1 |
Def | A![]() | [le] | core |
Def | P ![]() ![]() | [iff] | core |
Def | {T} | [guard] | core |
Def | ![]() | [all] | core |
Def | P ![]() ![]() | [implies] | core |
Def | i > j | [gt] | core |
Def | ![]() ![]() ![]() | [int_nzero] | int 1 |
Def | a ![]() | [nequal] | core |
Def | Dec(P) | [decidable] | core |
Def | ![]() | [not] | core |
Def | ![]() ![]() | [nat_plus] | int 1 |
Def | |i| | [absval] | |
Def | i = ![]() | [pm_equal] | |
Def | Prop | [prop] | core |
Def | imin(a;b) | [imin] | |
Def | a -- b | [ndiff] | |
Def | a mod n | [modulus] | |
Def | a ![]() ![]() | [div_floor] | |
Def | WellFnd{i}(A;x,y.R(x;y)) | [wellfounded] | well fnd |
Def | imax(a;b) | [imax] | |
Def | i![]() ![]() | [le_int] | bool 1 |
Def | if b![]() | [ifthenelse] | bool 1 |
Def | P ![]() | [or] | core |
Def | P & Q | [and] | core |
Def | ![]() | [exists] | core |
Def | i=![]() | [eq_int] | bool 1 |
Def | P ![]() ![]() | [rev_implies] | core |
Def | i < ![]() | [lt_int] | bool 1 |
Def | ![]() ![]() | [bnot] | bool 1 |
About:
![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() |
![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() |
![]() | ![]() | ![]() | ![]() | ![]() |
![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() | ![]() |