+++ title = "Appending predicated expressions to existing expressions" author = "Yann Herklotz" tags = [] categories = [] backlinks = ["3c3g3"] forwardlinks = ["3c3g5"] zettelid = "3c3g4" +++ In addition to that, another primitive that is needed is the following append operation, which will negate the combination of all predicates in the second predicated type, and it to the first predicated type and append the first predicated type to the second: $$ \mu(p, P) \equiv \texttt{map } (\lambda (p', e') . (p \land p', e'))\ P $$ $$ P_{1} \oplus_{p} P_{2} \equiv \mu(\neg p, P_{1}) \mathbin{++} \mu(p, P_{2})$$ The append operation, denoted by $\oplus$, will take two predicated expressions $P_1$ and $P_2$ and negates all the predicates in the second and anding them to the predicates in the first, while then appending the whole expression to the previous one.