Direct linear capabilities used by codecs

The witnesses normalize only realizing machines. No higher tidy computability rule is used.

theorem Turing.MultiTapeTM.ComputableInLinearTimeAndSpace.restrict {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {f : α → β} (h : ComputableInLinearTimeAndSpace f encIn encMid) (p : α → Prop) : ComputableInLinearTimeAndSpace (f ∘ Subtype.val) ((Function.Embedding.subtype p).trans encIn) encMid

Restrict a certificate to the inputs satisfying a proposition, using the same machine.

theorem Turing.MultiTapeTM.ComputableInLinearTimeAndSpace.of_cons_true {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {f : α → β} (h : ∀ (a : α), encMid (f a) = true :: encIn a) : ComputableInLinearTimeAndSpace f encIn encMid

Prepend the marker of the existing option encoding.

theorem Turing.MultiTapeTM.ComputableInLinearTimeAndSpace.of_tail {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {f : α → β} (h : ∀ (a : α), encMid (f a) = (encIn a).tail) : ComputableInLinearTimeAndSpace f encIn encMid

Drop the input word's first symbol using the existing head machine.

theorem Turing.MultiTapeTM.ComputableInLinearTimeAndSpace.of_take_one {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {f : α → β} (h : ∀ (a : α), encMid (f a) = List.take 1 (encIn a)) : ComputableInLinearTimeAndSpace f encIn encMid

Keep the input word's first symbol using the existing head machine.

theorem Turing.MultiTapeTM.ComputableInLinearTimeAndSpace.of_isEmpty {α : Type u_1} {encIn : α ↪ List Bool} {f : α → Bool} (h : ∀ (a : α), f a = (encIn a).isEmpty) : ComputableInLinearTimeAndSpace f encIn encBool

Test the encoded input for emptiness using the existing finite transducer.

theorem Turing.MultiTapeTM.ComputableInLinearTimeAndSpace.append {α : Type u_1} {β : Type u_2} {γ : Type u_3} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {encOut : γ ↪ List Bool} {δ : Type u_4} {enc₂ : δ ↪ List Bool} {f₁ : α → β} {f₂ : α → δ} {g : α → γ} (h₁ : ComputableInLinearTimeAndSpace f₁ encIn encMid) (h₂ : ComputableInLinearTimeAndSpace f₂ encIn enc₂) (hg : ∀ (a : α), encOut (g a) = encMid (f₁ a) ++ enc₂ (f₂ a)) : ComputableInLinearTimeAndSpace g encIn encOut

Concatenate two encoded outputs within a common linear bound.

theorem Turing.MultiTapeTM.ComputableInLinearTimeAndSpace.ite {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {encC : Bool ↪ List Bool} {c : α → Bool} {f g : α → β} (hc : ComputableInLinearTimeAndSpace c encIn encC) (hf : ComputableInLinearTimeAndSpace (f ∘ Subtype.val) ((Function.Embedding.subtype fun (x : α) => c x = true).trans encIn) encMid) (hg : ComputableInLinearTimeAndSpace (g ∘ Subtype.val) ((Function.Embedding.subtype fun (x : α) => c x = false).trans encIn) encMid) : ComputableInLinearTimeAndSpace (fun (a : α) => if c a = true then f a else g a) encIn encMid

Choose branches on their actual domains; normalize only their realizing machines.

theorem Turing.MultiTapeTM.ComputableInLinearTimeAndSpace.of_isEmpty_ite {α : Type u_1} {β : Type u_2} {encIn : α ↪ List Bool} {encMid : β ↪ List Bool} {f : α → β} (d : β) (hd : ∀ (a : α), encIn a = [] → f a = d) (h : ComputableInLinearTimeAndSpace (f ∘ Subtype.val) ((Function.Embedding.subtype fun (a : α) => (encIn a).isEmpty = false).trans encIn) encMid) : ComputableInLinearTimeAndSpace f encIn encMid

A fixed default on the empty word and a linear certificate on nonempty encoded inputs.

theorem Turing.MultiTapeTM.ComputableInLinearTimeAndSpace.pair {α β₁ β₂ : Type u} {encIn : α ↪ List Bool} {enc₁ : β₁ ↪ List Bool} {enc₂ : β₂ ↪ List Bool} {enc : β₁ × β₂ ↪ List Bool} [hP : PairEncoding enc₁ enc₂ enc] {f : α → β₁} {g : α → β₂} (hf : ComputableInLinearTimeAndSpace f encIn enc₁) (hg : ComputableInLinearTimeAndSpace g encIn enc₂) : ComputableInLinearTimeAndSpace (fun (x : α) => (f x, g x)) encIn enc

Pairing functions computable in linear time and space.