# Associative

## Definition

An operation $$\circ: S \times S$$ is associative if and only if:

$$\forall x,y,z \in S : (x \circ y) \circ z = x \circ (y \circ z)$$
THEOREM

Append is associative.

append_assoc: (?xs @ ?ys) @ ?zs = ?xs @ ?ys @ ?zs

Proof unavailable

THEOREM

Conjunction is associative.

$$P \wedge Q \wedge R \dashv\vdash P \wedge (Q \wedge R)$$

Proof available

THEOREM

Natural number multiplication is associative.

$$\forall x,y \in \mathbb{N} : x * y * z = x * (y * z)$$

Proof available

LEMMA    $$P \vee Q \vee R \vdash P \vee (Q \vee R)$$

Proof available

LEMMA    $$P \vee (Q \vee R) \vdash P \vee Q \vee R$$

Proof available

THEOREM

Disjunction is associative.

$$P \vee Q \vee R \dashv\vdash P \vee (Q \vee R)$$

Proof available

THEOREM

Union is associative.

$$A \cup B \cup C = A \cup (B \cup C)$$

Proof available

THEOREM

$$\forall x,y,z \in \mathbb{N} : x + y + z = x + (y + z)$$

Proof available

THEOREM

Intersection is associative.

$$A \cap B \cap C = A \cap (B \cap C)$$

Proof available

THEOREM

$$\forall x,y,z \in \mathbb{Z} : x + y + z = x + (y + z)$$

Proof available

THEOREM

The left operation is associative.

$$(x \leftarrow y) \leftarrow z = x \leftarrow (y \leftarrow z)$$

Proof available