Direct plain list lookup and first occurrence

Unary dropping uses the existing full-prefix fold and the codec's bare tail machine. Fixed-default lookup uses the bare head machine, without an inhabitedness assumption. First occurrence uses the original credited Boolean/counter fold.

theorem Turing.MultiTapeTM.ComputableInPolyTime.dropUnary {α : Type} {encA : α ↪ List Bool} {encL : List α ↪ List Bool} [ListEncoding encA encL] [SizedListEncoding encA encL] : ComputableInPolyTime (fun (p : List α × ℕ) => List.drop p.2 p.1) (encPair encL encUnary) encL

Drop a unary number of elements, retaining arbitrary sized list encodings.

theorem Turing.MultiTapeTM.ComputableInPolyTime.head? {α : Type} (enc : α ↪ List Bool) {encL : List α ↪ List Bool} [_inst3 : ListEncoding enc encL] : ComputableInPolyTime List.head? encL (encOption enc)

Read an optional head in any list encoding, without an inhabitant of the element type.

theorem Turing.MultiTapeTM.ComputableInPolyTime.getElem? {α γ : Type} {encA : α ↪ List Bool} {encIn : γ ↪ List Bool} {encL : List α ↪ List Bool} {list : γ → List α} {index : γ → ℕ} (hlist : ComputableInPolyTime list encIn encL) (hindex : ComputableInPolyTime index encIn encUnary) [ListEncoding encA encL] [SizedListEncoding encA encL] : ComputableInPolyTime (fun (x : γ) => (list x)[index x]?) encIn (encOption encA)

Look up a computed unary index, returning none outside a computed list. The list certificate determines its encoding before proof search checks the corresponding operation and size rules.

theorem Turing.MultiTapeTM.ComputableInPolyTime.listGetD {α : Type} {encA : α ↪ List Bool} {encL : List α ↪ List Bool} [ListEncoding encA encL] [SizedListEncoding encA encL] (d : α) : ComputableInPolyTime (fun (p : List α × ℕ) => p.1.getD p.2 d) (encPair encL encUnary) encA

Lookup with an explicit default and unary index, in any sized list encoding.

theorem Turing.MultiTapeTM.ComputableInPolyTime.idxOf {α : Type} [DecidableEq α] (enc : α ↪ List Bool) : ComputableInPolyTime (fun (p : List α × α) => List.idxOf p.2 p.1) (encPair (encList enc) enc) encUnary

The first occurrence, or the list length when absent; the returned index is unary.

theorem Turing.MultiTapeTM.ComputableInPolyTime.idxOfWithInput {α γ : Type} {encA : α ↪ List Bool} {encIn : γ ↪ List Bool} [DecidableEq α] {list : γ → List α} {value : γ → α} (hlist : ComputableInPolyTime list encIn (encList encA)) (hvalue : ComputableInPolyTime value encIn encA) : ComputableInPolyTime (fun (x : γ) => List.idxOf (value x) (list x)) encIn encUnary

Find a computed value's first occurrence in a computed list.