a,y. InjCase(a; j. f(j,y), g(j,y));x;as)
k ; a.as' f(a,reduce(f;k;as')) (recursive)
A,B:Type, f:(A
BB), k:B, as:A List. reduce(f;k;as) 
B| No other cites to report in Graphs | |
| union-reduce | Def union-reduce(f;g;x;as) == reduce(a,y. InjCase(a; j. f(j,y), g(j,y));x;as) |
| reduce | Def reduce(f;k;as) == Case of as; nil k ; a.as' f(a,reduce(f;k;as')) (recursive) |
| Thm* A,B:Type, f:(ABB), k:B, as:A List. reduce(f;k;as) B |
| Syntax: | union-reduce(f;g;x;as) | has structure: | union-reduce(f; g; x; as) |
About:
 |  |  |
 |  |  |  |  |  |  |  |