Minimum conditional time-bounded Kolmogorov complexity -- proof internals

theorem Complexity.MINCKT.Instance.length_unaryClock_internal (inst : Instance) : inst.unaryClock.length = inst.time

theorem Complexity.MINCKT.Instance.decode?_encode_internal (inst : Instance) : decode? inst.encode = some inst

theorem Complexity.MINCKT.Instance.decode?_eq_some_iff_internal (bits : List Bool) (inst : Instance) : decode? bits = some inst ↔ bits = inst.encode

theorem Complexity.MINCKT.Instance.decode?_eq_none_iff_internal (bits : List Bool) : decode? bits = none ↔ ¬∃ (inst : Instance), bits = inst.encode

theorem Complexity.MINCKT.Instance.encode_injective_internal : Function.Injective encode

theorem Complexity.MINCKT.Instance.length_encode_internal (inst : Instance) : inst.encode.length = 2 * inst.output.length + 2 * inst.condition.length + inst.time + 4

theorem Complexity.MINCKT.Instance.isAtMost_iff_hasProgramAtMost_internal {tapes : ℕ} (inst : Instance) (machine : OracleTM tapes) (threshold : ℕ) : inst.IsAtMost machine threshold ↔ inst.HasProgramAtMost machine threshold

theorem Complexity.MINCKT.Instance.isAtMost_withTime_mono_internal {tapes : ℕ} (inst : Instance) (machine : OracleTM tapes) (threshold : ℕ) {first second : ℕ} (hclock : first ≤ second) (hsmall : (inst.withTime first).IsAtMost machine threshold) : (inst.withTime second).IsAtMost machine threshold

theorem Complexity.MINCKT.Instance.isAtMost_threshold_mono_internal {tapes : ℕ} (inst : Instance) (machine : OracleTM tapes) {first second : ℕ} (hthreshold : first ≤ second) (hsmall : inst.IsAtMost machine first) : inst.IsAtMost machine second