Supply.lean`

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

def OAI.Fifths.Entry.Tells line 14
Source documentation
Computes a value from a fixed finite type.
```
def Tells [Fintype A] (x : I → List X) (S a : I → ℕ) (v : I → A) : Prop :=
…
```
theorem OAI.Fifths.Entry.finite_map line 20
theorem OAI.Fifths.Entry.tell_both line 25
theorem OAI.Fifths.Entry.tell_all line 30
inductive OAI.Fifths.Single.Arg line 57
Also declared: ComparatorChallenges/OneTapeSpace.lean:223 (same declaration text).
instance OAI.Fifths.Single.(instance at line 61) line 61
abbrev OAI.Fifths.Single.Sym line 63
Also declared: ComparatorChallenges/OneTapeSpace.lean:229 (same declaration text).
def OAI.Fifths.Single.arg line 65
Also declared: ComparatorChallenges/OneTapeSpace.lean:231 (same declaration text).
def OAI.Fifths.Single.Gives line 73
Source documentation
Access condition with a numeric allowance of cells (bits accounting of TM.Within).
```
def Gives (A : M.Sym) (x : List X) (T s : ℕ) : Prop :=
…
```
theorem OAI.Fifths.Single.Gives.mono line 77
structure OAI.Fifths.Single.Kit line 82
Source documentation
Sufficient resources and access for a family of offset trials.
```
structure Kit (A : M.Sym) (x : I → List X) (S a : I → ℕ) (W : I → Site) : Prop where
…
```
Mentions: OAI.Fifths.Site
theorem OAI.Fifths.Single.Kit.changeInput line 95
theorem OAI.Fifths.Single.Kit.read line 104
theorem OAI.Fifths.Single.Kit.ofBlock line 123
Source comment
Common sizes. radix itself and its b-th power included in S.
```
theorem ofBlock : Comp x S a (fun i => (W i).b) := p.ofK.mul p.ofK
```
Mentions: OAI.Fifths.Comp
theorem OAI.Fifths.Single.Kit.double line 124
theorem OAI.Fifths.Single.Kit.ofBlocks line 126
theorem OAI.Fifths.Single.Kit.ofW line 128
theorem OAI.Fifths.Single.Kit.ofC line 131
theorem OAI.Fifths.Single.Kit.granted line 134
theorem OAI.Fifths.Single.Kit.subGranted line 138
theorem OAI.Fifths.Single.Kit.ofRadix line 141
theorem OAI.Fifths.Single.Kit.ofQ line 144
theorem OAI.Fifths.Single.Kit.neighbors line 148