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]
Thm* x:, n:. ((-x) mod n) = if (x mod n)=0 0 else n-(x mod n) fi	[mod_minus]
Thm* i:. f91(i) ~ if 101 < i i-10 else 91 fi	[f91-val]
Thm* k:, f,g:(k), p:(k). sum(if p(i) f(i)+g(i) else f(i) fi | i < k) = sum(f(i) | i < k)+sum(if p(i) g(i) else 0 fi | i < k)	[sum-ite]
Thm* f:(TAT), P:(A), L:A List, s:T. list_accum(s',x'.f(s',x');s;filter(P;L)) ~ list_accum(i,y.if P(y) f(i,y) else i fi;s;L)	[list_accum_filter]
Thm* P:(T), L2,L1:T List. list_accum(l,x.if P(x) [x / l] else l fi;L1;L2) ~ (rev(filter(P;L2)) @ L1)	[filter_list_accum]
Def f91(i) == if 100 < i i-10 else f91(f91(i+11)) fi (recursive)	[f91]
Def process u j where process s i == if P(i;s) then F(i;s) else G(i;s) where xs := N(i;s); s:= H(i;s); while not null xs { s := process s (hd xs); xs := tl xs; } == if P(j;u) F(j;u) else G(j;list_accum(s',i'.process s' i' where process s i == if P(i;s) then F(i;s) else G(i;s) where xs := N(i;s); s:= H(i;s); while not null xs { s := process s (hd xs); xs := tl xs; } ;H(j;u);N(j;u))) fi (recursive)	[accumulate]
Def upto(i;j) == if i < j [i / upto(i+1;j)] else nil fi (recursive)	[upto]

In prior sections: bool 1 mb nat mb list 2 int 2 list 1 prog 1 mb list 1 num thy 1

Try larger context: Graphs