x,y:
, n:
. ((x+y) rem n) = (((x rem n)+(y rem n)) rem n)+if (x+y < 
0)
(0 < (((x rem n)+(y rem n)) rem n))
-|n| ;((((x rem n)+(y rem n)) rem n) < 0)(0 < x+y)|n| else 0 fix
L.P(x)) == reduce(
x,b. P(x)b;true;L)q == if p q else false fi
is mentioned by
| Thm* x,y:, n:. ((x+y) rem n) = (((x rem n)+(y rem n)) rem n)+if (x+y < 0)(0 < (((x rem n)+(y rem n)) rem n))-|n| ;((((x rem n)+(y rem n)) rem n) < 0)(0 < x+y)|n| else 0 fi | [rem_add] |
| Def (xL.P(x)) == reduce(x,b. P(x)b;true;L) | [l_ball] |
In prior sections: bool 1 mb list 1 mb list 2 mb basic
Try larger context:
Graphs