配列

定義 3.1（「基本的なデータ構造」§3）

長さ $n$ の配列とは、同じ大きさ $s$ （語数）の $n$ 個の区画を、先頭番地 $b$ から連続した番地に並べたものをいう。 $i$ 番目の要素（ $0 \le i \le n-1$ ）を $A[i]$ と書き、その区画の先頭番地は

\mathrm{addr}(A[i]) = b + s \cdot i

で与えられる。

閉包の状態

定義

定義は閉包の起点です（証明を要しません）。

印の意味: ✓公理まで証明済み・ △証明あり（閉包未完）・ ※主張のみ。テーマごとの集計は閉包の状況。