| Who Cites double sum? |
|
double_sum | Def sum(f(x;y) | x < n; y < m) == sum(sum(f(x;y) | y < m) | x < n) |
| | Thm* n,m: , f:( n  m  ). sum(f(x,y) | x < n; y < m)  |
|
sum | Def sum(f(x) | x < k) == primrec(k;0; x,n. n+f(x)) |
| | Thm* n: , f:( n  ). sum(f(x) | x < n)  |
|
primrec | Def primrec(n;b;c) == if n= 0 b else c(n-1,primrec(n-1;b;c)) fi (recursive) |
| | Thm* T:Type, n: , b:T, c:( n T T). primrec(n;b;c) T |
|
eq_int | Def i= j == if i=j true ; false fi |
| | Thm* i,j: . (i= j)  |