OAI/Computability/Superstring/Model.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Superstring.Symbol line 7

   Also declared: ComparatorChallenges/Superstring.lean:7 (same declaration text).

2. abbrev OAI.Superstring.Word line 8

   Also declared: ComparatorChallenges/Superstring.lean:8 (same declaration text).

3. abbrev OAI.Superstring.Instance line 9

   Also declared: ComparatorChallenges/Superstring.lean:9 (same declaration text).

4. def OAI.Superstring.encodeList line 12

   Source documentation

   Prefix markers encode the list spine, including its final boundary.

   Also declared: ComparatorChallenges/Superstring.lean:12 (same declaration text).

   def encodeList {α : Type} (enc : α → List Bool) : List α → List Bool
     | [] => [true]
     | a :: as => false :: (enc a ++ encodeList enc as)

5. def OAI.Superstring.encodeSymbol line 16

   Also declared: ComparatorChallenges/Superstring.lean:16 (same declaration text).

6. def OAI.Superstring.encodeWord line 17

   Also declared: ComparatorChallenges/Superstring.lean:17 (same declaration text).

7. def OAI.Superstring.encodeInstance line 18

   Also declared: ComparatorChallenges/Superstring.lean:18 (same declaration text).

8. def OAI.Superstring.IsCommonSuperstring line 21

   Source documentation

   Ordinary contiguous substring containment, including the empty word.

   Also declared: ComparatorChallenges/Superstring.lean:21 (same declaration text).

   def IsCommonSuperstring (S : Instance) (T : Word) : Prop :=
   …

   Mentions: OAI.Superstring.Instance, OAI.Superstring.Word

9. def OAI.Superstring.opt line 25

   Source documentation

   The optimum in symbols, not in bits.

   Also declared: ComparatorChallenges/Superstring.lean:25 (same declaration text).

   noncomputable def opt (S : Instance) : ℕ :=
   …

   Mentions: OAI.Superstring.Instance

10. def OAI.Superstring.HasPolynomialImplementation line 30

    Source documentation

    A deterministic finite-stack-machine implementation, with a polynomial bound on bit-level running time in the explicitly encoded input length.

    Also declared: ComparatorChallenges/Superstring.lean:30 (same declaration text).

    def HasPolynomialImplementation (f : Instance → Word) : Prop :=
    …

    Mentions: OAI.Superstring.Instance, OAI.Superstring.Word