a,y. InjCase(a; j. f(j,y), g(j,y));x;as)
x
L.P(x)) == reduce(x,b. P(x) 
b;false;L)
xL.P(x)) == reduce(x,b. P(x)
b;true;L)
k ; a.as' f(a,reduce(f;k;as')) (recursive)
is mentioned by
| Def union-reduce(f;g;x;as) == reduce(a,y. InjCase(a; j. f(j,y), g(j,y));x;as) | [union-reduce] |
| Def (xL.P(x)) == reduce(x,b. P(x) b;false;L) | [l_bexists] |
| Def (xL.P(x)) == reduce(x,b. P(x)b;true;L) | [l_ball] |
In prior sections: mb list 2 list 1 mb list 1
Try larger context:
Graphs