Output.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Fifths.binaryIn line 11
Source documentation
Arguments individually binary.
Distinct definitions of this name: ComparatorChallenges/OneTapeSpace.lean:213 (different declaration text). Qualify references as OAI.Fifths.binaryIn@path.
```
def binaryIn (pub : List X) (f : J → ℕ) : Inputs X J :=
…
```
Mentions: OAI.Fifths.Inputs
def OAI.Fifths.SM.decode line 18
Source comment
From an injective natural coding on a fixed finite alphabet.
```
noncomputable def decode (base : Y) (e : Y ↪ ℕ) (l : List Bool) : Y := by
…
```
theorem OAI.Fifths.SM.decode_code line 21
def OAI.Fifths.SM.charLength line 29
theorem OAI.Fifths.SM.char_le line 31
def OAI.Fifths.SM.emit line 34
theorem OAI.Fifths.SM.exec_emit line 38

theorem OAI.Fifths.SM.scaledTM line 46

Source documentation

Uniform conversion with new constant.

theorem scaledTM [Fintype K] (M : SM X J K Y) {x : I → Inputs X J} {y : I → Y}
    {S : I → ℕ} (c : ℕ)
    (r : ∀ i, ∃ t, M.Exec (x i) (c*(S i+1)) (.init (fun _ => [])) t (y i)) :
    ∃ d, ∀ i, M.toTM.Within (x i) (y i) (d*(S i+1)) := by
…

Mentions: OAI.Fifths.SM, OAI.Fifths.Inputs

theorem OAI.Fifths.Comp.withBinary line 66

Source documentation

Binary result of a uniform register computation can also be returned directly in finite control.

theorem withBinary (base : Y) (d : Y ↪ ℕ) (h : Comp x S a (fun i => d (y i))) :
    ∃ (M : TM X Unit Y) (c : ℕ), ∀ i,
      M.Within (binaryIn (x i) (fun _ => a i)) (y i) (c*(S i+1)) := by
…

Mentions: OAI.Fifths.Comp, OAI.Fifths.TM

theorem OAI.Fifths.Comp.withoutBinary line 92