34.5. Length — CLRS-Lean

CLRS-Lean
Chapter 34. NP-Completeness
34.5. NP-Complete Problems
34.5. SUBSET-SUM
34.5. Encoding
34.5. Length

Imports
                import CLRSLean.Chapter_34.Section_34_5_NP_Complete_Problems.SubsetSum.Encoding.RoundTrip
import CLRSLean.Chapter_34.Section_34_5_NP_Complete_Problems.TravelingSalesperson.Encoding.Length

              
                
                  Physical lengths of serialized SUBSET-SUM records 
                
              

              namespace CLRS.Chapter34@[simp] theorem encodeSubsetSumData_length (data : SubsetSumData) :
    (encodeSubsetSumData data).length =
      (encodeTSPFields (data.target :: data.values)).length + 2 := by
  simp [encodeSubsetSumData]@[simp] theorem encodeSubsetSumCertificate_length (indices : List Nat) :
    (encodeSubsetSumCertificate indices).length =
      (encodeTSPFields indices).length + 2 := by
  exact encodeTSPCertificate_length indicesend CLRS.Chapter34