Captured plain polynomial-time rules

Plain Turing.MultiTapeTM.ComputableInPolyTime composition rules for operations that combine multiple arguments computed from a shared input. Rules whose head and encoding disambiguate search are registered with fun_prop, and rules whose result hides an element or index encoding additionally carry program_certificate; binary_mod' stays explicit alongside Turing.MultiTapeTM.ComputableInPolyTime.binary_div' so HMod.hMod automation on Turing.MultiTapeTM.encUnary remains unambiguous.

Main results

• Turing.MultiTapeTM.ComputableInPolyTime.cond': Boolean _root_.cond case distinction.
• Turing.MultiTapeTM.ComputableInPolyTime.listHead?WithInput: optional head of a computed framed list, fixing the element encoding without typeclass synthesis.
• Turing.MultiTapeTM.ComputableInPolyTime.listHeadDWithInput: head of a computed framed list with a computed fallback.
• Turing.MultiTapeTM.ComputableInPolyTime.listTakeWithInput: prefix of a computed framed list of computed unary length.
• Turing.MultiTapeTM.ComputableInPolyTime.listDropWithInput: suffix of a computed framed list after dropping a computed unary prefix.
• Turing.MultiTapeTM.ComputableInPolyTime.countWithInput: unary occurrence count of a computed value in a computed framed list.
• Turing.MultiTapeTM.ComputableInPolyTime.anyConst: existential Boolean scan over a fixed list with input-dependent predicates.
• Turing.MultiTapeTM.ComputableInPolyTime.binary_mod': explicit remainder of computed binary naturals on Turing.MultiTapeTM.encNat.

theorem Turing.MultiTapeTM.ComputableInPolyTime.cond' {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encOut : β ↪ List Bool} {encC : Bool ↪ List Bool} {c : α → Bool} {t e : α → β} (hc : ComputableInPolyTime c encIn encC) (ht : ComputableInPolyTime t encIn encOut) (he : ComputableInPolyTime e encIn encOut) : ComputableInPolyTime (fun (a : α) => bif c a then t a else e a) encIn encOut

Case distinction on a computed Boolean guard in any encoding of Bool, for _root_.cond.

theorem Turing.MultiTapeTM.ComputableInPolyTime.listHead?WithInput {α γ : Type} {encA : α ↪ List Bool} {encIn : γ ↪ List Bool} {list : γ → List α} (hlist : ComputableInPolyTime list encIn (encList encA)) : ComputableInPolyTime (fun (a : γ) => (list a).head?) encIn (encOption encA)

Read the optional head of a computed framed list, inferring the element encoding directly from the list certificate without waiting on ListEncoding synthesis.

theorem Turing.MultiTapeTM.ComputableInPolyTime.listHeadDWithInput {α γ : Type} {encA : α ↪ List Bool} {encIn : γ ↪ List Bool} {list : γ → List α} {fallback : γ → α} (hlist : ComputableInPolyTime list encIn (encList encA)) (hfallback : ComputableInPolyTime fallback encIn encA) : ComputableInPolyTime (fun (a : γ) => (list a).headD (fallback a)) encIn encA

Read the head of a computed framed list with a computed fallback, inferring the element encoding from the list before checking the fallback or composing with an outer projection.

theorem Turing.MultiTapeTM.ComputableInPolyTime.listDropWithInput {α γ : Type} {encA : α ↪ List Bool} {encIn : γ ↪ List Bool} {list : γ → List α} {count : γ → ℕ} (hlist : ComputableInPolyTime list encIn (encList encA)) (hcount : ComputableInPolyTime count encIn encUnary) : ComputableInPolyTime (fun (a : γ) => List.drop (count a) (list a)) encIn (encList encA)

Drop a computed unary number of elements from a computed framed list.

theorem Turing.MultiTapeTM.ComputableInPolyTime.listTakeWithInput {α γ : Type} {encA : α ↪ List Bool} {encIn : γ ↪ List Bool} {list : γ → List α} {count : γ → ℕ} (hlist : ComputableInPolyTime list encIn (encList encA)) (hcount : ComputableInPolyTime count encIn encUnary) : ComputableInPolyTime (fun (a : γ) => List.take (count a) (list a)) encIn (encList encA)

Take a computed unary number of elements from a computed framed list.

theorem Turing.MultiTapeTM.ComputableInPolyTime.countWithInput {α γ : Type} {encA : α ↪ List Bool} {encIn : γ ↪ List Bool} [BEq α] [LawfulBEq α] {list : γ → List α} {value : γ → α} (hlist : ComputableInPolyTime list encIn (encList encA)) (hvalue : ComputableInPolyTime value encIn encA) : ComputableInPolyTime (fun (a : γ) => List.count (value a) (list a)) encIn encUnary

Count occurrences of a computed value in a computed framed list using lawful Boolean equality, returning the count in unary.

theorem Turing.MultiTapeTM.ComputableInPolyTime.anyConst {γ : Type} {encIn : γ ↪ List Bool} {ι : Type u_1} (l : List ι) {test : γ → ι → Bool} (htest : ∀ i ∈ l, ComputableInPolyTime (fun (a : γ) => test a i) encIn encBool) : ComputableInPolyTime (fun (a : γ) => l.any (test a)) encIn encBool

Test whether any element of a fixed list satisfies an input-dependent predicate. Only the list's members need certificates; the index type may live in any universe and requires no encoding.

theorem Turing.MultiTapeTM.ComputableInPolyTime.binary_mod' {α : Type} {input : α ↪ List Bool} {left right : α → ℕ} (hleft : ComputableInPolyTime left input encNat) (hright : ComputableInPolyTime right input encNat) : ComputableInPolyTime (fun (a : α) => left a % right a) input encNat

Remainder of computed binary naturals on encNat. Like Turing.MultiTapeTM.ComputableInPolyTime.binary_div', this rule is kept out of fun_prop and program_certificate so HMod.hMod dispatch on encUnary stays unambiguous.