$$ \begin{array}{l} \text{CHOOSEDEF} (P : \iota^{n+1} \to o) & \forall c_1^\iota, \dots, c_n^\iota, x^\iota : \\ & P(x, c_1, \dots, c_n) \Rightarrow P(\text{choose}_P(c_1, \dots, c_n), c_1, \dots, c_n) \end{array} $$

$$ \begin{array}{l} \text{CHOOSEEXT} (P, Q : \iota^{n+1} \to o) & \forall c_1^\iota, \dots, c_n^\iota : \\ & (\forall x^\iota : P(x, c_1, \dots, c_n) \Leftrightarrow Q(x, c_1, \dots, c_n)) \\ & \Rightarrow \text{choose}_P(c_1, \dots, c_n) = \text{choose}_Q(c_1, \dots, c_n) \end{array} $$

Set Theory

<table><thead><tr><th>Operator</th><th>Type</th><th>Operator</th><th>Type</th><th></th></tr></thead><tbody><tr><td>in</td><td>ι × ι → o</td><td>setof<sub>F</sub><sup>**</sup></td><td>ι<sup>p</sup> × ι<sup>n</sup> → ι</td><td>(★) P : ι<sup>n+1</sup> → o</td></tr><tr><td>subseteq</td><td>ι × ι → o</td><td>cup</td><td>ι × ι → ι</td><td>(★★) F : ι<sup>p+n</sup> → ι</td></tr><tr><td>enum<sub>n</sub></td><td>ι<sup>n</sup> → ι</td><td>cap</td><td>ι × ι → ι</td><td></td></tr><tr><td>union</td><td>ι → ι</td><td>diff</td><td>ι × ι → ι</td><td></td></tr><tr><td>subset</td><td>ι → ι</td><td>boolean</td><td>ι</td><td></td></tr><tr><td>setst<sub>P</sub><sup>*</sup></td><td>ι × ι<sup>n</sup> → ι</td><td>cast<sub>o</sub></td><td>o → ι</td><td></td></tr></tbody></table>

SUBSETEQINTRO
∀a<sup>t</sup>, b<sup>t</sup> : {subseteq(a, b)}
(∀x<sup>t</sup> : in(x, a) ⇔ in(x, b)) ⇒subseteq(a, b)

SUBSETEQELIM
∀a<sup>t</sup>, b<sup>t</sup>, x<sup>t</sup> : {subseteq(a, b), in(x, a)}
subseteq(a, b) ∧ in(x, a) ⇒ in(x, b)

ENUMINTRO (p)
∀a<sub>1</sub><sup>t</sup>, ..., a<sub>p</sub><sup>t</sup> : {enum<sub>p</sub>(a<sub>1</sub>, ..., a<sub>p</sub>)}
in(a<sub>1</sub>, enum<sub>p</sub>(a<sub>1</sub>, ..., a<sub>p</sub>)) ∧ ... ∧ in(a<sub>p</sub>, enum<sub>p</sub>(a<sub>1</sub>, ..., a<sub>p</sub>))

ENUMELIM (p)
∀a<sub>1</sub><sup>t</sup>, ..., a<sub>p</sub><sup>t</sup>, x<sup>t</sup> : {in(x, enum<sub>p</sub>(a<sub>1</sub>, ..., a<sub>p</sub>))}
in(x, enum<sub>p</sub>(a<sub>1</sub>, ..., a<sub>p</sub>)) ⇒ x = a<sub>1</sub> ∨ ... ∨ x = a<sub>p</sub>

EMPTYELIM
∀x<sup>t</sup> : {in(x, enum<sub>0</sub>)} ¬in(x, enum<sub>0</sub>)

SUBSETDEF
∀a<sup>t</sup>, x<sup>t</sup> : {in(x,subset(a))}
{subseteq(x, a),subset(a)}
in(x,subset(a)) ⇔subseteq(x, a)

UNIONINTRO
∀a<sup>t</sup>, x<sup>t</sup>, y<sup>t</sup> : {in(y, a),in(x,union(a))}
{in(x, y),in(x,union(a))}
{in(x, y),in(y,a),union(a)}
in(x,y) ∧ in(y,a) ⇒in(x,union(a))

UNIONELIM
∀a<sup>t</sup>, x<sup>t</sup> : {in(x,union(a))}
in(x,union(a)) ⇒∃y<sup>t</sup> : in(x,y) ∧ in(y,a)
SETSTDEF (P : ι^{n+1} → o) ∀c_1^ι, ..., c_n^ι, a^ι, x^ι : {in(x, setstP(a, c_1, ..., c_n))} {in(x, a), setstP(a, c_1, ..., c_n)} in(x, setstP(a, c_1, ..., c_n)) ⇔ in(x, a) ∧ P(x, c_1, ..., c_n)

SETOFINTRO (F : ι^{p+n} → ι) ∀c_1^ι, ..., c_n^ι, a_1^ι, ..., a_p^ι, y_1^ι, ..., y_p^ι : 
{F(y_1, ..., y_p, c_1, ..., c_n), setofF(a_1, ..., a_p, c_1, ..., c_n)} 
{in(y_1, a_1), ..., in(y_p, a_p), setofF(a_1, ..., a_p, c_1, ..., c_n)} 
in(y_1, a_1) ∧ ... ∧ in(y_p, a_p) 
⇒ in(F(y_1, ..., y_p, c_1, ..., c_n), setofF(a_1, ..., a_p, c_1, ..., c_n))

SETOFELIM (F : ι^{p+n} → ι) ∀c_1^ι, ..., c_n^ι, a_1^ι, ..., a_p^ι, x^ι : 
{in(x, setofF(a_1, ..., a_p, c_1, ..., c_n))} 
in(x, setofF(a_1, ..., a_p, c_1, ..., c_n)) ⇒ 
∃y_1^ι, ..., y_p^ι : in(y_1, a_1) ∧ ... ∧ in(y_p, a_p) ∧ x = F(y_1, ..., y_p)

CUPDEF
∀a^ι, b^ι, x^ι : {in(x, cup(a, b))}
{in(x, a), cup(a, b)}
{in(x, b), cup(a, b)}
in(x, cup(a, b)) ⇔ in(x, a) ∨ in(x, b)

CAPDEF
∀a^ι, b^ι, x^ι : {in(x, cap(a, b))}
{in(x, a), cap(a, b)}
{in(x, b), cap(a, b)}
in(x, cap(a, b)) ⇔ in(x, a) ∧ in(x, b)

SETMINUSDEF
∀a^ι, b^ι, x^ι : {in(x, diff(a, b))}
{in(x, a), diff(a, b)}
{in(x, b), diff(a, b)}
in(x, diff(a, b)) ⇔ in(x, a) ∧ ¬in(x, b)

BOOLCASTINJ
    cast_o(TRUE) ≠ cast_o(FALSE)

BOOLEANINTRO
    in(cast_o(TRUE), boolean) ∧ in(cast_o(FALSE), boolean)

BOOLEANELIM
    ∀x^ι : {in(x, boolean)}
    in(x, boolean) ⇒ x = cast_o(TRUE) ∨ x = cast_o(FALSE)
Function Theory

<table><thead><tr><th>Operator</th><th>Type</th></tr></thead><tbody><tr><td>isafcn</td><td>ι → o</td></tr><tr><td>fn<sub>F</sub><sup>*</sup></td><td>ι × ι<sup>n</sup> → ι</td></tr><tr><td>except</td><td>ι × ι × ι → ι</td></tr><tr><td>domain</td><td>ι → ι</td></tr><tr><td>fnapp</td><td>ι × ι → ι</td></tr><tr><td>arrow</td><td>ι × ι → ι</td></tr></tbody></table>

**FCNEXTENSIONALITY**
$$ \begin{array}{l} \forall f^t, g^t : \{\text{isafcn}(f), \text{isafcn}(g)\} \\ \quad \wedge \text{isafcn}(f) \wedge \text{isafcn}(g) \\ \quad \wedge \text{domain}(f) = \text{domain}(g) \\ \quad \wedge (\forall x^t : \text{in}(x, \text{domain}(f)) \Rightarrow \text{fnapp}(f, x) = \text{fnapp}(g, x)) \\ \quad \Rightarrow f = g \end{array} $$

**FCNISAFCN** ($F : \iota^{n+1} \to \iota$)
$$ \begin{array}{l} \forall c_1^t, \dots, c_n^t, a^t : \{\text{fnn}_F(a, c_1, \dots, c_n)\} \\ \quad \text{isafcn}(\text{fnn}_F(a, c_1, \dots, c_n)) \end{array} $$

**FCNDOM** ($F : \iota^{n+1} \to \iota$)
$$ \begin{array}{l} \forall c_1^t, \dots, c_n^t, a^t : \{\text{fnn}_F(a, c_1, \dots, c_n)\} \\ \quad \text{domain}(\text{fnn}_F(a, c_1, \dots, c_n)) = a \end{array} $$

**FCNAPP** ($F : \iota^{n+1} \to \iota$)
$$ \begin{array}{l} \forall c_1^t, \dots, c_n^t, a^t, x^t : \{\text{fnapp}(\text{fnn}_F(a, c_1, \dots, c_n), x)\} \\ \quad \{\text{in}(x, a), \text{fnn}_F(a, c_1, \dots, c_n)\} \\ \quad \text{in}(x, a) \Rightarrow \text{fnapp}(\text{fnn}_F(a, c_1, \dots, c_n), x) = F(x, c_1, \dots, c_n) \end{array} $$

**FCNTYPING** ($F : \iota^{n+1} \to \iota$)
$$ \begin{array}{l} \forall c_1^t, \dots, c_n^t, a^t, b^t : \{\text{fnn}_F(a, c_1, \dots, c_n), \text{arrow}(a, b)\} \\ \quad (\forall x^t : \text{in}(x, a) \Rightarrow \text{in}(F(x, c_1, \dots, c_n), b)) \\ \quad \Rightarrow \text{in}(\text{fnn}_F(a, c_1, \dots, c_n), \text{arrow}(a, b)) \end{array} $$

**ARROWINTRO**
$$ \begin{array}{l} \forall a^t, b^t, f^t : \{\text{in}(f, \text{arrow}(a, b))\} \\ \quad \wedge \text{isafcn}(f) \\ \quad \wedge \text{domain}(f) = a \\ \quad \wedge (\forall x^t : \text{in}(x, a) \Rightarrow \text{in}(\text{fnapp}(f, x), b)) \\ \quad \Rightarrow \text{in}(f, \text{arrow}(a, b)) \end{array} $$

**ARROWELIM<sub>1</sub>**
$$ \begin{array}{l} \forall a^t, b^t, f^t : \{\text{in}(f, \text{arrow}(a, b))\} \\ \quad \text{in}(f, \text{arrow}(a, b)) \Rightarrow \wedge \text{isafcn}(f) \\ \quad \wedge \text{domain}(f) = a \end{array} $$

**ARROWELIM<sub>2</sub>**
$$ \begin{array}{l} \forall a^t, b^t, f^t, x^t : \{\text{in}(f, \text{arrow}(a, b)), \text{in}(x, a)\} \\ \quad \{\text{in}(f, \text{arrow}(a, b)), \text{fnapp}(f, x)\} \\ \quad \text{in}(f, \text{arrow}(a, b)) \wedge \text{in}(x, a) \Rightarrow \text{in}(\text{fnapp}(f, x), b) \end{array} $$
EXCEPTISAFCN $\forall f^t, x^t, y^t : \{except(f, x, y)\}$
isafcn(except(f, x, y))

EXCEPTDOM $\forall f^t, x^t, y^t : \{except(f, x, y)\}$
domain(except(f, x, y)) = domain(f)

EXCEPTAPP₁ $\forall f^t, x^t, y^t : \{except(f, x, y)\}$
in(x, domain(f)) ⇒ fcnapp(except(f, x, y), x) = y

EXCEPTAPP₂ $\forall f^t, x^t, y^t, z^t : \{fnapp(except(f, x, y), z)\}$
$\{except(f, x, y), fnapp(f, z)\}$
in(z, domain(f)) ∧ z ≠ x ⇒ fnapp(except(f, x, y), z) = fnapp(f, z)

EXCEPTTYPING $\forall f^t, x^t, y^t, a^t, b^t : \{except(f, x, y), in(f, arrow(a, b))\}$
in(f, arrow(a, b)) ∧ (in(x, a) ⇒ in(y, b)) ⇒ in(except(f, x, y), arrow(a, b))

## Arithmetic

<table><thead><tr><th>Operator</th><th>Type</th></tr></thead><tbody><tr><td>cast<sub>int</sub></td><td>int → ι</td></tr><tr><td>proj<sub>int</sub></td><td>ι → int</td></tr><tr><td>Int</td><td>ι</td></tr><tr><td>Nat</td><td>ι</td></tr><tr><td>plus</td><td>ι × ι → ι</td></tr><tr><td>uminus</td><td>ι → ι</td></tr></tbody></table>

<table><thead><tr><th>Operator</th><th>Type</th></tr></thead><tbody><tr><td>minus</td><td>ι × ι → ι</td></tr><tr><td>mult</td><td>ι × ι → ι</td></tr><tr><td>quotient</td><td>ι × ι → ι</td></tr><tr><td>remainder</td><td>ι × ι → ι</td></tr><tr><td>lteq</td><td>ι × ι → o</td></tr><tr><td>range</td><td>ι × ι → ι</td></tr></tbody></table>

The symbols +, -, ×, ÷, % and ≤ as used below are not TLA⁺'s operators, but the builtin integer operators of SMT-LIB.
<table>
  <tr>
    <td>INTCASTINJECTIVE</td>
    <td>∀z<sup>int</sup> : {cast<sub>int</sub>(z)} z = proj<sub>int</sub>(cast<sub>int</sub>(z))</td>
  </tr>
  <tr>
    <td>INTINTINTRO</td>
    <td>∀z<sup>int</sup> : {cast<sub>int</sub>(z)} in(cast<sub>int</sub>(z), Int)</td>
  </tr>
  <tr>
    <td>INTINTELIM</td>
    <td>∀x<sup>l</sup> : {in(x, Int)} in(x, Int) ⇒ x = cast<sub>int</sub>(proj<sub>int</sub>(x))</td>
  </tr>
  <tr>
    <td>INTNATINTRO</td>
    <td>∀z<sup>int</sup> : {cast<sub>int</sub>(z)}<br/>z ≥ 0 ⇒ in(cast<sub>int</sub>(z), Nat)</td>
  </tr>
  <tr>
    <td>INTNATELIM</td>
    <td>∀x<sup>l</sup> : {in(x, Nat)}<br/>in(x, Nat) ⇒ x = cast<sub>int</sub>(proj<sub>int</sub>(x)) ∧ proj<sub>int</sub>(x) ≥ 0</td>
  </tr>
  <tr>
    <td>INTPLUSTYPING</td>
    <td>∀z<sub>1</sub><sup>int</sup>, z<sub>2</sub><sup>int</sup> : {plus(cast<sub>int</sub>(z<sub>1</sub>), cast<sub>int</sub>(z<sub>2</sub>))}<br/>plus(cast<sub>int</sub>(z<sub>1</sub>), cast<sub>int</sub>(z<sub>2</sub>)) = cast<sub>int</sub>(z<sub>1</sub> + z<sub>2</sub>)</td>
  </tr>
  <tr>
    <td>INTUMINUSTYPING</td>
    <td>∀z<sup>int</sup> : {uminus(cast<sub>int</sub>(z))}<br/>uminus(cast<sub>int</sub>(z)) = cast<sub>int</sub>(-z)</td>
  </tr>
  <tr>
    <td>INTMINUSTYPING</td>
    <td>∀z<sub>1</sub><sup>int</sup>, z<sub>2</sub><sup>int</sup> : {minus(cast<sub>int</sub>(z<sub>1</sub>), cast<sub>int</sub>(z<sub>2</sub>))}<br/>minus(cast<sub>int</sub>(z<sub>1</sub>), cast<sub>int</sub>(z<sub>2</sub>)) = cast<sub>int</sub>(z<sub>1</sub> - z<sub>2</sub>)</td>
  </tr>
  <tr>
    <td>INTMULTTYPING</td>
    <td>∀z<sub>1</sub><sup>int</sup>, z<sub>2</sub><sup>int</sup> : {mult(cast<sub>int</sub>(z<sub>1</sub>), cast<sub>int</sub>(z<sub>2</sub>))}<br/>mult(cast<sub>int</sub>(z<sub>1</sub>), cast<sub>int</sub>(z<sub>2</sub>)) = cast<sub>int</sub>(z<sub>1</sub> × z<sub>2</sub>)</td>
  </tr>
  <tr>
    <td>INTQUOTIENTTYPING</td>
    <td>∀z<sub>1</sub><sup>int</sup>, z<sub>2</sub><sup>int</sup> : {quotient(cast<sub>int</sub>(z<sub>1</sub>), cast<sub>int</sub>(z<sub>2</sub>))}<br/>z<sub>2</sub> > 0 ⇒ quotient(cast<sub>int</sub>(z<sub>1</sub>), cast<sub>int</sub>(z<sub>2</sub>)) = cast<sub>int</sub>(z<sub>1</sub> ÷ z<sub>2</sub>)</td>
  </tr>
  <tr>
    <td>INTREMAINDERTYPING</td>
    <td>∀z<sub>1</sub><sup>int</sup>, z<sub>2</sub><sup>int</sup> : {remainder(cast<sub>int</sub>(z<sub>1</sub>), cast<sub>int</sub>(z<sub>2</sub>))}<br/>z<sub>2</sub> > 0 ⇒ remainder(cast<sub>int</sub>(z<sub>1</sub>), cast<sub>int</sub>(z<sub>2</sub>)) = cast<sub>int</sub>(z<sub>1</sub> % z<sub>2</sub>)</td>
  </tr>
  <tr>
    <td>INTLTEQTYPING</td>
    <td>∀z<sub>1</sub><sup>int</sup>, z<sub>2</sub><sup>int</sup> : {lteq(cast<sub>int</sub>(z<sub>1</sub>), cast<sub>int</sub>(z<sub>2</sub>))}<br/>lteq(cast<sub>int</sub>(z<sub>1</sub>), cast<sub>int</sub>(z<sub>2</sub>)) ⇔ z<sub>1</sub> ≤ z<sub>2</sub></td>
  </tr>
  <tr>
    <td>INTRANGEINTRO</td>
    <td>∀a<sup>l</sup>, b<sup>l</sup>, z<sup>int</sup> : {in(cast<sub>int</sub>(z), range(a, b))}<br/>lteq(a, cast<sub>int</sub>(z)) ∧ lteq(cast<sub>int</sub>(z), b) ⇒ in(cast<sub>int</sub>(z), range(a, b))</td>
  </tr>
  <tr>
    <td>INTRANGEELIM</td>
    <td>∀a<sup>l</sup>, b<sup>l</sup>, x<sup>l</sup> : {in(x, range(a, b))}<br/>in(x, range(a, b)) ⇒ x = cast<sub>int</sub>(proj<sub>int</sub>(x)) ∧ lteq(a, x) ∧ lteq(x, b)</td>
  </tr>
</table>

Tuples

<table>
  <thead>
    <tr>
      <th>Operator</th>
      <th>Type</th>
    </tr>
  </thead>
  <tbody>
    <tr>
      <td>tup<sub>n</sub></td>
      <td>ι<sup>n</sup> → ι</td>
    </tr>
    <tr>
      <td>prod<sub>p+1</sub></td>
      <td>ι<sup>p+1</sup> → ι</td>
    </tr>
  </tbody>
</table>
TUPISAFCN (n)
$\forall x_1^t, \dots, x_n^t : \{\mathbf{tup}_n(x_1, \dots, x_n)\}$
isafcn($\mathbf{tup}_n(x_1, \dots, x_n)$)

TUPDOM (n)
$\forall x_1^t, \dots, x_n^t : \{\mathbf{tup}_n(x_1, \dots, x_n)\}$
domain($\mathbf{tup}_n(x_1, \dots, x_n)$) = enum_n($\mathbf{cast}_{\text{int}}(1), \dots, \mathbf{cast}_{\text{int}}(n)$)

TUPAPP (p)
$\forall x_1^t, \dots, x_p^t : \{\mathbf{tup}_p(x_1, \dots, x_p)\}$
$\land \mathbf{fnapp}(\mathbf{tup}_p(x_1, \dots, x_p), \mathbf{cast}_{\text{int}}(1)) = x_1$
$\land \dots$
$\land \mathbf{fnapp}(\mathbf{tup}_p(x_1, \dots, x_p), \mathbf{cast}_{\text{int}}(p)) = x_p$

TUPEXCEPT (p, p' ≤ p)
$\forall x_1^t, \dots, x_p^t, x^t : \{\text{except}(\mathbf{tup}_p(x_1, \dots, x_p), \mathbf{cast}_{\text{int}}(p'), x)\}$
$\text{except}(\mathbf{tup}_p(x_1, \dots, x_p', \dots, x_p), \mathbf{cast}_{\text{int}}(p'), x) = \mathbf{tup}_p(x_1, \dots, x, \dots, x_p)$

PRODUCTINTRO (p)
$\forall a_1^t, \dots, a_p^t, x_1^t, \dots, x_p^t : \{\mathbf{tup}_p(x_1, \dots, x_p), \mathbf{prod}_p(a_1, \dots, a_p)\}$
$\mathbf{in}(x_1, a_1) \land \dots \land \mathbf{in}(x_p, a_p) \Rightarrow \mathbf{in}(\mathbf{tup}_p(x_1, \dots, x_p), \mathbf{prod}_p(a_1, \dots, a_p))$

PRODUCTELIM (p)
$\forall a_1^t, \dots, a_p^t, x^t : \{\mathbf{in}(x, \mathbf{prod}_p(a_1, \dots, a_p))\}$
$\mathbf{in}(x, \mathbf{prod}_p(a_1, \dots, a_p)) \Rightarrow x = \mathbf{tup}_p(\mathbf{fnapp}(x, \mathbf{cast}_{\text{int}}(1)), \dots, \mathbf{fnapp}(x, \mathbf{cast}_{\text{int}}(p)))$

## Strings

<table><thead><tr><td>Operator</td><td>Type</td></tr></thead><tbody><tr><td>str<sub>s</sub></td><td>ι</td></tr><tr><td>string</td><td>ι</td></tr></tbody></table>

<table><tr><td>STRINGINTRO (s)</td><td>in(str<sub>s</sub>, string)</td></tr><tr><td>STRINGSDISTINCT (s<sub>1</sub>, s<sub>2</sub> distincts)</td><td>str<sub>s<sub>1</sub></sub> ≠ str<sub>s<sub>2</sub></sub></td></tr></table>

## Records

<table><thead><tr><td>Operator</td><td>Type</td></tr></thead><tbody><tr><td>record<sub>s<sub>1</sub>,...,s<sub>p</sub></sub> *</td><td>ι<sup>p</sup> → ι</td></tr><tr><td>recset<sub>s<sub>1</sub>,...,s<sub>p</sub></sub> *</td><td>ι<sup>p</sup> → ι</td></tr></tbody></table>

<footnote>(*) Fields s<sub>1</sub>, ..., s<sub>p</sub>
are assumed distinct</footnote>
RECORDISAFCN $(s_1, \dots, s_p)$
$$ \forall x_1^t, \dots, x_p^t : \{ \mathit{record}_{s_1, \dots, s_p}(x_1, \dots, x_p) \} \\ \phantom{\forall x_1^t, \dots, x_p^t : \{ \mathit{record}_{s_1, \dots, s_p}(} } \mathit{isafcn}(\mathit{record}_{s_1, \dots, s_p}(x_1, \dots, x_p)) $$

RECORDDOM $(s_1, \dots, s_p)$
$$ \forall x_1^t, \dots, x_p^t : \{ \mathit{record}_{s_1, \dots, s_p}(x_1, \dots, x_p) \} \\ \phantom{\forall x_1^t, \dots, x_p^t : \{ \mathit{record}_{s_1, \dots, s_p}(} } \mathit{domain}(\mathit{record}_{s_1, \dots, s_p}(x_1, \dots, x_p)) = \mathit{enum}_p(\mathit{str}_{s_1}, \dots, \mathit{str}_{s_p}) $$

RECORDAPP $(s_1, \dots, s_p)$
$$ \forall x_1^t, \dots, x_p^t : \{ \mathit{record}_{s_1, \dots, s_p}(x_1, \dots, x_p) \} \\ \phantom{\forall x_1^t, \dots, x_p^t : \{ \mathit{record}_{s_1, \dots, s_p}(} } \mathit{fcnapp}(\mathit{record}_{s_1, \dots, s_p}(x_1, \dots, x_p), \mathit{str}_{s_1}) = x_1 \\ \phantom{\forall x_1^t, \dots, x_p^t : \{ \mathit{record}_{s_1, \dots, s_p}(} } \dots \\ \phantom{\forall x_1^t, \dots, x_p^t : \{ \mathit{record}_{s_1, \dots, s_p}(} } \mathit{fcnapp}(\mathit{record}_{s_1, \dots, s_p}(x_1, \dots, x_p), \mathit{str}_{s_p}) = x_p $$

RECORDEXCEPT $(s_1, \dots, s_p, p' \le p)$
$$ \forall x_1^t, \dots, x_p^t, x^t : \{ \mathit{except}(\mathit{record}_{s_1, \dots, s_p}(x_1, \dots, x_p), \mathit{str}_{s_{p'}}(x)) \} \\ \phantom{\forall x_1^t, \dots, x_p^t, x^t : \{ \mathit{except}(\mathit{record}_{s_1, \dots, s_p}(} } \mathit{except}(\mathit{record}_{s_1, \dots, s_p}(x_1, \dots, x_{p'}, \dots, x_p), \mathit{str}_{s_{p'}}, x) \\ \phantom{\forall x_1^t, \dots, x_p^t, x^t : \{ \mathit{except}(\mathit{record}_{s_1, \dots, s_p}(} } = \mathit{record}_{s_1, \dots, s_p}(x_1, \dots, x, \dots, x_p) $$

RECSETINTRO $(s_1, \dots, s_p)$
$$ \forall a_1^t, \dots, a_p^t, x_1^t, \dots, x_p^t : \{ \mathit{record}_{s_1, \dots, s_p}(x_1, \dots, x_p), \mathit{recset}_{s_1, \dots, s_p}(a_1, \dots, a_p) \} \\ \phantom{\forall a_1^t, \dots, a_p^t, x_1^t, \dots, x_p^t : \{ \mathit{record}_{s_1, \dots, s_p}(} } \mathit{in}(x_1, a_1) \wedge \dots \wedge \mathit{in}(x_p, a_p) \\ \phantom{\forall a_1^t, \dots, a_p^t, x_1^t, \dots, x_p^t : \{ \mathit{record}_{s_1, \dots, s_p}(} } \Rightarrow \mathit{in}(\mathit{record}_{s_1, \dots, s_p}(x_1, \dots, x_p), \mathit{recset}_{s_1, \dots, s_p}(a_1, \dots, a_p)) $$

RECSETELIM $(s_1, \dots, s_p)$
$$ \forall a_1^t, \dots, a_p^t, x^t : \{ \mathit{in}(x, \mathit{recset}_{s_1, \dots, s_p}(a_1, \dots, a_p)) \} \\ \phantom{\forall a_1^t, \dots, a_p^t, x^t : \{ \mathit{in}(x, \mathit{recset}_{s_1, \dots, s_p}(} } \mathit{in}(x, \mathit{recset}_{s_1, \dots, s_p}(a_1, \dots, a_p)) \\ \phantom{\forall a_1^t, \dots, a_p^t, x^t : \{ \mathit{in}(x, \mathit{recset}_{s_1, \dots, s_p}(} } \Rightarrow x = \mathit{record}_{s_1, \dots, s_p}(\mathit{fcnapp}(x, \mathit{str}_{s_1}), \dots, \mathit{fcnapp}(x, \mathit{str}_{s_p})) $$

Sequences

<table><thead><tr><th>Operator</th><th>Type</th></tr></thead><tbody><tr><td>Seq</td><td>ι → ι</td></tr><tr><td>Len</td><td>ι → ι</td></tr><tr><td>Cat</td><td>ι × ι → ι</td></tr><tr><td>Append</td><td>ι × ι → ι</td></tr></tbody></table>

<table><thead><tr><th>Operator</th><th>Type</th></tr></thead><tbody><tr><td>Head</td><td>ι → ι</td></tr><tr><td>Tail</td><td>ι → ι</td></tr><tr><td>Subseq</td><td>ι × ι × ι → ι</td></tr><tr><td>Selectseq<sub>T</sub><sup>*</sup></td><td>ι × ι<sup>n</sup> → ι</td></tr></tbody></table>

$$ (\star) \ T : \iota^{n+1} \to o $$
SEQINTRO
∀a<sup>t</sup>, s<sup>t</sup> : {in(s, Seq(a))}

& isafcn(s)

& in(Len(s), Nat)

& ∀i<sup>t</sup> : in(i, domain(s)) ⇔ & in(i, Int)

& 1 ≤ proj<sub>int</sub>(i)

& proj<sub>int</sub>(i) ≤ proj<sub>int</sub>(Len(s))

& ∀i<sup>int</sup> : 1 ≤ i & i ≤ proj<sub>int</sub>(Len(s)) ⇒ in(fcnapp(s, cast<sub>int</sub>(i)), a)

⇒ in(s, Seq(a))

SEQELIM<sub>1</sub>
∀a<sup>t</sup>, s<sup>t</sup> : {in(s, Seq(a))}

in(s, Seq(a)) ⇒ & isafcn(s)

& in(Len(s), Nat)

& domain(s) = range(cast<sub>int</sub>(1), Len(s))

SEQELIM<sub>2</sub>
∀a<sup>t</sup>, s<sup>t</sup>, i<sup>int</sup> : {in(s, Seq(a)), fcnapp(s, cast<sub>int</sub>(i))}

in(s, Seq(a)) & 1 ≤ i & i ≤ proj<sub>int</sub>(Len(s)) ⇒ in(fcnapp(s, cast<sub>int</sub>(i)), a)

CATTYPING
∀a<sup>t</sup>, s<sup>t</sup>, t<sup>t</sup> : {in(s, Seq(a)), Cat(s, t)}

{in(t, Seq(a)), Cat(s, t)}

in(s, Seq(a)) & in(t, Seq(a)) ⇒ in(Cat(s, t), Seq(a))

CATLEN
∀s<sup>t</sup>, t<sup>t</sup> : {Cat(s, t)}

in(Len(s), Nat) & in(Len(t), Nat)

⇒ Len(Cat(s, t)) = cast<sub>int</sub>(proj<sub>int</sub>(Len(s)) + proj<sub>int</sub>(Len(t))))

CATAPP<sub>1</sub>
∀s<sup>t</sup>, t<sup>t</sup>, i<sup>int</sup> : {fnapp(Cat(s, t), cast<sub>int</sub>(i))}

{Cat(s, t), fnapp(s, cast<sub>int</sub>(i))}

& in(Len(s), Nat) & in(Len(t), Nat)

& 1 ≤ i & i ≤ proj<sub>int</sub>(Len(s))

⇒ fnapp(Cat(s, t), cast<sub>int</sub>(i)) = fnapp(s, cast<sub>int</sub>(i))

CATAPP<sub>2</sub>
∀s<sup>t</sup>, t<sup>t</sup>, i<sup>int</sup> : {fnapp(Cat(s, t), cast<sub>int</sub>(i))}

& in(Len(s), Nat) & in(Len(t), Nat)

& i ≤ proj<sub>int</sub>(Len(s)) + proj<sub>int</sub>(Len(t)) & proj<sub>int</sub>(Len(s)) < i

⇒ fnapp(Cat(s, t), cast<sub>int</sub>(i)) = fnapp(t, cast<sub>int</sub>(i - proj<sub>int</sub>(Len(s))))
APPENDTYPING $\forall a^t, s^t, x^t : \{\text{in}(s, \text{Seq}(a)), \text{Append}(s, x)\}$
$\text{in}(s, \text{Seq}(a)) \wedge \text{in}(x, a) \Rightarrow \text{in}(\text{Append}(s, x), \text{Seq}(a))$

APPENDLEN $\forall s^t, x^t : \{\text{Append}(s, x)\}$
$\text{in}(\text{Len}(s), \text{Nat}) \Rightarrow \text{Len}(\text{Append}(s, x)) = \text{cast}_{\text{int}}(\text{proj}_{\text{int}}(\text{Len}(s)) + 1)$

APPENDAPP₁ $\forall s^t, x^t, i^{\text{int}} : \{\text{fnapp}(\text{Append}(s, x), \text{cast}_{\text{int}}(i))\}$
$\{\text{Append}(s, x), \text{fnapp}(s, \text{cast}_{\text{int}}(i))\}$
$\wedge \text{in}(\text{Len}(s), \text{Nat})$
$\wedge 1 \le i \wedge i \le \text{proj}_{\text{int}}(\text{Len}(s))$
$\Rightarrow \text{fnapp}(\text{Append}(s, x), \text{cast}_{\text{int}}(i)) = \text{fnapp}(s, \text{cast}_{\text{int}}(i))$

APPENDAPP₂ $\forall s^t, x^t : \{\text{Append}(s, x)\}$
$\text{in}(\text{Len}(s), \text{Nat}) \Rightarrow \text{fnapp}(\text{Append}(s, x), \text{cast}_{\text{int}}(\text{proj}_{\text{int}}(\text{Len}(s)) + 1)) = x$

HEADDEF $\forall s^t : \{\text{Head}(s)\}$
$\text{Head}(s) = \text{fnapp}(s, \text{cast}_{\text{int}}(1))$

TAILTYPING $\forall a^t, s^t : \{\text{in}(s, \text{Seq}(a)), \text{Tail}(s)\}$
$\wedge \text{in}(s, \text{Seq}(a))$
$\wedge \text{proj}_{\text{int}}(\text{Len}(s)) \neq 0$
$\Rightarrow \text{in}(\text{Tail}(s), \text{Seq}(a))$

TAILLEN $\forall s^t : \{\text{Tail}(s)\}$
$\wedge \text{in}(\text{Len}(s), \text{Nat})$
$\wedge \text{proj}_{\text{int}}(\text{Len}(s)) \neq 0$
$\Rightarrow \text{Len}(\text{Tail}(s)) = \text{cast}_{\text{int}}(\text{proj}_{\text{int}}(\text{Len}(s)) - 1)$

TAILAPP $\forall s^t, i^{\text{int}} : \{\text{fnapp}(\text{Tail}(s), \text{cast}_{\text{int}}(i))\}$
$\wedge \text{in}(\text{Len}(s), \text{Nat})$
$\wedge \text{proj}_{\text{int}}(\text{Len}(s)) \neq 0$
$\wedge 1 \le i \wedge i \le \text{proj}_{\text{int}}(\text{Len}(s)) - 1$
$\Rightarrow \text{fnapp}(\text{Tail}(s), \text{cast}_{\text{int}}(i)) = \text{fnapp}(s, \text{cast}_{\text{int}}(i + 1))$
SUBSEQTYPING
$\forall a^t, s^t, x^{\text{int}}, y^{\text{int}} : \{\text{in}(s, \text{Seq}(a)), \text{Subseq}(s, \text{cast}_{\text{int}}(x), \text{cast}_{\text{int}}(y))\}$
$\quad \land \text{in}(s, \text{Seq}(a))$
$\quad \land 1 \le x$
$\quad \land y \le \text{proj}_{\text{int}}(\text{Len}(s))$
$\quad \Rightarrow \text{in}(\text{Subseq}(s, \text{cast}_{\text{int}}(x), \text{cast}_{\text{int}}(y)), \text{Seq}(a))$

SUBSEQLEN
$\forall s^t, x^{\text{int}}, y^{\text{int}} : \{\text{Subseq}(s, \text{cast}_{\text{int}}(x), \text{cast}_{\text{int}}(y))\}$
$\quad \land x \le y + 1$
$\quad \Rightarrow \text{Len}(\text{Subseq}(s, \text{cast}_{\text{int}}(x), \text{cast}_{\text{int}}(y))) = \text{cast}_{\text{int}}((y + 1) - x)$
$\quad \land x > y + 1 \Rightarrow \text{Len}(\text{Subseq}(s, \text{cast}_{\text{int}}(x), \text{cast}_{\text{int}}(y))) = \text{cast}_{\text{int}}(0)$

SUBSEQAPP
$\forall s^t, x^{\text{int}}, y^{\text{int}}, z^{\text{int}} : \{\text{fnapp}(\text{Subseq}(s, \text{cast}_{\text{int}}(x), \text{cast}_{\text{int}}(y)), \text{cast}_{\text{int}}(z))\}$
$\quad \land 1 \le x$
$\quad \land 1 \le z \land z \le (y + 1) - x$
$\quad \Rightarrow \text{fnapp}(\text{Subseq}(s, \text{cast}_{\text{int}}(x), \text{cast}_{\text{int}}(y)), \text{cast}_{\text{int}}(z))$
$\quad = \text{fnapp}(s, \text{cast}_{\text{int}}((z + x) - 1))$

SELECTSEQTYPING ($T: \iota^{n+1} \to o$)
$\forall c_1^t, \dots, c_n^t, s^t : \{\text{in}(s, \text{Seq}(a)), \text{Selectseq}_T(s, c_1, \dots, c_n)\}$
$\quad \text{in}(s, \text{Seq}(a)) \Rightarrow \text{in}(\text{Selectseq}_T(s, c_1, \dots, c_n), \text{Seq}(a))$

SELECTSEQLEN ($T: \iota^{n+1} \to o$)
$\forall c_1^t, \dots, c_n^t, s^t : \{\text{Selectseq}_T(s, c_1, \dots, c_n)\}$
$\quad \text{in}(\text{Len}(s), \text{Nat})$
$\quad \Rightarrow \text{proj}_{\text{int}}(\text{Len}(\text{Selectseq}_T(s, c_1, \dots, c_n))) \le \text{proj}_{\text{int}}(\text{Len}(s))$

SELECTSEQAPP ($T: \iota^{n+1} \to o$)
$\forall c_1^t, \dots, c_n^t, s^t, x^t : \{\text{fnapp}(\text{Selectseq}_T(s, c_1, \dots, c_n), x)\}$
$\quad \text{in}(x, \text{domain}(\text{Selectseq}_T(s, c_1, \dots, c_n)))$
$\quad \Rightarrow T(\text{fnapp}(\text{Selectseq}_T(s, c_1, \dots, c_n), x))$

SELECTSEQNIL ($T: \iota^{n+1} \to o$)
$\text{Selectseq}_T(\text{tup}_0, c_1, \dots, c_n) = \text{tup}_0$

SELECTSEQAPPEND ($T: \iota^{n+1} \to o$)
$\forall c_1^t, \dots, c_n^t, s^t, x^t : \{\text{Selectseq}_T(\text{Append}(s, x), c_1, \dots, c_n)\}$
$\quad \land T(x, c_1, \dots, c_n) \Rightarrow$
$\quad \quad \text{Selectseq}_T(\text{Append}(s, x), c_1, \dots, c_n)$
$\quad = \text{Append}(\text{Selectseq}_T(s, c_1, \dots, c_n), x)$
$\quad \land \neg T(x, c_1, \dots, c_n) \Rightarrow$
$\quad \quad \text{Selectseq}_T(\text{Append}(s, x), c_1, \dots, c_n)$
$\quad = \text{Selectseq}_T(s, c_1, \dots, c_n)$

TUPSEQTYPING ($n$)
$\forall a^t, x_1^t, \dots, x_n^t : \{\text{in}(x_1, a), \dots, \text{in}(x_n, a), \text{tup}_n(x_1, \dots, x_n)\}$
$\quad \text{in}(x_1, a) \land \dots \land \text{in}(x_n, a) \Rightarrow \text{in}(\text{tup}_n(x_1, \dots, x_n), \text{Seq}(a))$

TUPSEQLEN ($n$)
$\forall x_1^t, \dots, x_n^t : \{\text{tup}_n(x_1, \dots, x_n)\}$
$\quad \text{Len}(\text{tup}_n(x_1, \dots, x_n)) = \text{cast}_{\text{int}}(n)$