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   

Natural number addition is associative.

$$\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   

Integer addition is associative.

$$\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

Proper supersets