InputEncoding.lean`

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

def OAI.MaxCutGames.BinaryFormula.clauseNames line 11
Source documentation
An ordinary conjunction of three-slot clauses with sparse variable names. Repeated names and repeated literals are permitted in every clause.
```
def clauseNames (clause : Clause) : List Nat :=
…
```
Mentions: OAI.MaxCutGames.BinaryFormula.Clause
theorem OAI.MaxCutGames.BinaryEncoding.bitsValue_bits line 20
theorem OAI.MaxCutGames.BinaryEncoding.parseFrame_encoded line 29
Source documentation
Prefix-free framing on the two-symbol input alphabet.
```
@[simp] theorem parseFrame_encoded (bits trailing : List Bool) :
    parseFrame (frame bits ++ trailing) = some (bits, trailing) := by
…
```
Mentions: OAI.MaxCutGames.BinaryEncoding.parseFrame, OAI.MaxCutGames.BinaryEncoding.frame
theorem OAI.MaxCutGames.BinaryEncoding.frame_length line 35
theorem OAI.MaxCutGames.BinaryEncoding.parseName_encoded line 43
Source documentation
Equality with the canonical digits rejects alternate padded encodings.
```
@[simp] theorem parseName_encoded (name : Nat) (rest : List Bool) :
    parseName (nameBits name ++ rest) = some (name, rest) := by
…
```
Mentions: OAI.MaxCutGames.BinaryEncoding.parseName, OAI.MaxCutGames.BinaryEncoding.nameBits
theorem OAI.MaxCutGames.BinaryEncoding.nameBits_length line 47
theorem OAI.MaxCutGames.BinaryEncoding.nameBits_length_le_of_lt_pow line 51
def OAI.MaxCutGames.BinaryEncoding.literalBits line 57
theorem OAI.MaxCutGames.BinaryEncoding.parseLiteral_encoded line 60
theorem OAI.MaxCutGames.BinaryEncoding.literalBits_length line 65
def OAI.MaxCutGames.BinaryEncoding.clauseBits line 69
theorem OAI.MaxCutGames.BinaryEncoding.clause_three_entries line 72
theorem OAI.MaxCutGames.BinaryEncoding.parseClause_encoded line 78
def OAI.MaxCutGames.BinaryEncoding.clauseNameSize line 82
theorem OAI.MaxCutGames.BinaryEncoding.clauseBits_length line 85
def OAI.MaxCutGames.BinaryEncoding.clausesBits line 90
def OAI.MaxCutGames.BinaryEncoding.formulaBits line 94
def OAI.MaxCutGames.BinaryEncoding.namesBitSize line 96
theorem OAI.MaxCutGames.BinaryEncoding.namesBitSize_nil line 99
theorem OAI.MaxCutGames.BinaryEncoding.namesBitSize_cons line 101
theorem OAI.MaxCutGames.BinaryEncoding.clausesBits_length line 105
theorem OAI.MaxCutGames.BinaryEncoding.formulaBits_length line 114
theorem OAI.MaxCutGames.BinaryEncoding.clauses_length_lt_bits line 119
def OAI.MaxCutGames.BinaryEncoding.ordinarySize line 126
Source documentation
Binary digits, one sign per literal, and one terminal bit form a natural reference size. The concrete framing adds only a fixed multiplicative factor.
```
def ordinarySize (formula : Formula) : Nat :=
…
```
theorem OAI.MaxCutGames.BinaryEncoding.ordinarySize_le_bits line 129
theorem OAI.MaxCutGames.BinaryEncoding.bits_le_three_ordinarySize line 135
theorem OAI.MaxCutGames.BinaryEncoding.parseClauses_encoded line 143
Source documentation
Fuel bounds the number of clause iterations, not the size of any name.
```
@[simp] theorem parseClauses_encoded (clauses : List Clause) (rest : List Bool)
    (fuel : Nat) (enough : clauses.length < fuel) :
    parseClauses fuel (clausesBits clauses ++ rest) = some (clauses, rest) := by
…
```
Mentions: OAI.MaxCutGames.BinaryEncoding.parseClauses, OAI.MaxCutGames.BinaryEncoding.clausesBits
theorem OAI.MaxCutGames.BinaryEncoding.decodeFormula_encoded line 158
theorem OAI.MaxCutGames.BinaryEncoding.formulaBits_injective line 168
Source documentation
This preserves every literal and clause occurrence, including duplicates.
```
theorem formulaBits_injective {first second : Formula}
    (same : formulaBits first = formulaBits second) : first = second := by
…
```
Mentions: OAI.MaxCutGames.BinaryEncoding.formulaBits