Reading symbols commutes with taking prefix of tapes
Provedread_takeReading the symbols under the heads of the first k1 tapes equals taking the first k1 symbols from reading all tapes.
Formal statement
import Definitions.Def_CookLevin_Basic
open CookLevin
theorem read_take (tps : List Tape) (k1 : Nat) :
read (tps.take k1) = (read tps).take k1 := by sorry