% Assuming the function *:U x U -> U to be injective, % where U is the domain of discourse, % the fork operator 'frk' has the following meaning: % frk^I(P,Q)={[x,y*z]: x P^I y, x Q^I z}, % where I is any interpretation. defAs(frk(P,Q),frk(P,Q)). % we take frk as primitive [defAs0B,defAs1,defFoAs0]. % we adopt all constructs of map algebra defAs(cross(P,Q),frk(circ(rev(frk(id,u)),P),circ(rev(frk(u,id)),Q))). defAs(left,rev(frk(id,u))). % first projection of non-urelements defAs(right,rev(frk(u,id))). % second projection of non-urelements defAs(idUr,diag(bros(frk(u,u)))). % identity map restricted to urelements