The positions of the bits of an encoded structure

The encoding encStructure (n, tables) of an input is the framed cardinality in unary followed by the framed truth tables (Cslib.Logic.encStructure_eq). This file locates its bits: the markers of the unary cardinality, and for each table its start (Cslib.Logic.tableStart), its markers, its bits and its terminator. Past the last table there is nothing to read. These are the facts an algorithm with random access to the encoding needs, such as the logarithmic-space model checker Cslib.Logic.Vocabulary.modelChecker.

Main definitions

• Cslib.Logic.tableStart: the position of a truth table in the encoding of an input.

Main results

• Cslib.Logic.encStructure_eq: the encoding of an input as a concatenation of frames.
• Cslib.Logic.drop_tableStart: the encoding from the start of a table on.
• Cslib.Logic.getElem?_encStructure_two_mul, Cslib.Logic.getElem?_encStructure_two_mul_card: the markers of the cardinality.
• Cslib.Logic.getElem?_encStructure_tableStart_two_mul, Cslib.Logic.getElem?_encStructure_tableStart_two_mul_add_one, Cslib.Logic.getElem?_encStructure_tableStart_two_mul_length: the markers, bits and terminator of a table.
• Cslib.Logic.getElem?_encStructure_tableStart_length_add: nothing follows the last table.

References

• N. Immerman, Descriptive Complexity, Section 2.1

theorem Cslib.Logic.encStructure_eq (a : EncodedStructure) : encStructure a = Turing.MultiTapeTM.frame (List.replicate a.1 true) ++ List.flatMap Turing.MultiTapeTM.frame a.2

The encoding of an input: its framed cardinality in unary, then its framed tables.

def Cslib.Logic.tableStart (a : EncodedStructure) (i : ℕ) : ℕ

The position of the i-th truth table in the encoding of an input; past the last table, the length of the encoding.

theorem Cslib.Logic.drop_tableStart (a : EncodedStructure) (i : ℕ) : List.drop (tableStart a i) (encStructure a) = List.flatMap Turing.MultiTapeTM.frame (List.drop i a.2)

The encoding from the i-th table on.

theorem Cslib.Logic.getElem?_encStructure_tableStart_add (a : EncodedStructure) (i q : ℕ) : (encStructure a)[tableStart a i + q]? = (List.flatMap Turing.MultiTapeTM.frame (List.drop i a.2))[q]?

Indexing encStructure a at tableStart a i + q reads position q in the framed tables starting at index i.

theorem Cslib.Logic.length_encStructure (a : EncodedStructure) : (encStructure a).length = tableStart a a.2.length

The total length of encStructure a equals tableStart a a.2.length.

theorem Cslib.Logic.tableStart_succ {a : EncodedStructure} {i : ℕ} (hi : i < a.2.length) : tableStart a (i + 1) = tableStart a i + 2 * a.2[i].length + 1

For i < a.2.length, tableStart a (i + 1) advances past the framed i-th table of length 2 * a.2[i].length + 1.

theorem Cslib.Logic.tableStart_mono (a : EncodedStructure) {i j : ℕ} (h : i ≤ j) : tableStart a i ≤ tableStart a j

tableStart a is monotone in the table index.

theorem Cslib.Logic.tableStart_le_length (a : EncodedStructure) (i : ℕ) : tableStart a i ≤ (encStructure a).length

Every table start position is at most (encStructure a).length.

theorem Cslib.Logic.two_mul_card_add_one_le_length (a : EncodedStructure) : 2 * a.1 + 1 ≤ (encStructure a).length

The framed unary cardinality prefix of length 2 * a.1 + 1 fits within encStructure a.

The bits

theorem Cslib.Logic.getElem?_encStructure_two_mul {a : EncodedStructure} {k : ℕ} (hk : k < a.1) : (encStructure a)[2 * k]? = some true

The markers of the cardinality.

theorem Cslib.Logic.getElem?_encStructure_two_mul_card (a : EncodedStructure) : (encStructure a)[2 * a.1]? = some false

The terminator of the cardinality.

theorem Cslib.Logic.getElem?_encStructure_tableStart_two_mul {a : EncodedStructure} {i j : ℕ} (hi : i < a.2.length) (hj : j < a.2[i].length) : (encStructure a)[tableStart a i + 2 * j]? = some true

The markers of a table.

theorem Cslib.Logic.getElem?_encStructure_tableStart_two_mul_add_one {a : EncodedStructure} {i j : ℕ} (hi : i < a.2.length) (hj : j < a.2[i].length) : (encStructure a)[tableStart a i + 2 * j + 1]? = some a.2[i][j]

The bits of a table.

theorem Cslib.Logic.getElem?_encStructure_tableStart_two_mul_length {a : EncodedStructure} {i : ℕ} (hi : i < a.2.length) : (encStructure a)[tableStart a i + 2 * a.2[i].length]? = some false

The terminator of a table.

theorem Cslib.Logic.getElem?_encStructure_tableStart_length_add (a : EncodedStructure) (q : ℕ) : (encStructure a)[tableStart a a.2.length + q]? = none

Nothing follows the last table.

theorem Cslib.Logic.getElem?_encStructure_tableStart_isSome {a : EncodedStructure} {i : ℕ} (hi : i < a.2.length) : (encStructure a)[tableStart a i]?.isSome = true

There is a bit at the start of every table.