Comp.lean`

23 declarations, 0 contain sorry, 0 declared as axioms

Uniform deterministic computation of binary register values. Inputs in the main work ports are charged (only public input x here besides the port). All pullbacks are mathematical indices; no index or bound parameter is available to a program unless it is in a port or provided in the inputs.

def OAI.Fifths.files line 18
Source documentation
Throughout, binary order LSB to MSB, ordinary canonical bits, also on any supplied argument tapes.
Distinct definitions of this name: ComparatorChallenges/OneTapeSpace.lean:216 (different declaration text). Qualify references as OAI.Fifths.files@path.
```
def files (x : List X) : Inputs X Empty :=
…
```
Mentions: OAI.Fifths.Inputs
def OAI.Fifths.file line 21
theorem OAI.Fifths.file_ok line 23
def OAI.Fifths.Comp line 26
theorem OAI.Fifths.Comp.source line 34
theorem OAI.Fifths.Comp.target line 37
theorem OAI.Fifths.Comp.pull line 40
theorem OAI.Fifths.Comp.up line 43
theorem OAI.Fifths.Comp.trans line 46
theorem OAI.Fifths.Comp.congr line 48
theorem OAI.Fifths.Comp.refl line 50
theorem OAI.Fifths.Comp.constant line 54

theorem OAI.Fifths.Comp.onPort line 76

Source documentation

Use one charged port of a larger file. Itself restores readers.

theorem onPort [DecidableEq L] (h : Comp x S a b) (k : L)
    (v : I → Store Empty L) (p : FitsStore S v) (o : ∀ i, (v i).ro = .home)
    (q : ∀ i, (v i).st k = (a i).bits) :
    Works (fun i => files (x i)) S v (fun i => (v i).set k (b i).bits) (fun _ => ()) := by
…

Mentions: OAI.Fifths.Comp, OAI.Fifths.Store, OAI.Fifths.FitsStore, OAI.Fifths.Works

def OAI.Fifths.Comp.singleton line 92
Source documentation
For programs with dedicated scratch Sq.
```
def singleton (K : Type) (a : ℕ) := (file a).extra K
```
Mentions: OAI.Fifths.file, OAI.Fifths.Comp.extra
theorem OAI.Fifths.Comp.singleton_set line 94
theorem OAI.Fifths.Comp.extra line 101
theorem OAI.Fifths.Comp.checked line 107
theorem OAI.Fifths.Comp.checkSized line 112
theorem OAI.Fifths.Comp.pair line 120
theorem OAI.Fifths.Comp.projectF line 177
theorem OAI.Fifths.Comp.projectS line 189
theorem OAI.Fifths.Comp.left line 201
theorem OAI.Fifths.Comp.right line 204