n,m:
, f:(n
m
). sum(f(x,y) | x < n; y < m) 
x,n. n+f(x))n:, f:(n). sum(f(x) | x < n) 
0
b else c(n-1,primrec(n-1;b;c)) fi (recursive)T:Type, n:, b:T, c:(nTT). primrec(n;b;c) Tj == if i=j true ; false fii,j:. (i=j) 
| 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:(nm). 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:(nTT). primrec(n;b;c) T | |
| eq_int | Def i=j == if i=j true ; false fi |
| Thm* i,j:. (i=j) |
| Syntax: | sum(f(x;y) | x < n; y < m) | has structure: | double_sum(n; m; x,y.f(x;y)) |
About:
 |  |  |  |  |  |  |  |  |
 |  |  |  |  |  |  |  |