[DeriveMode False False, Mark [[0, 0, 1]], CreateInvariant True, Mark [[0]], Narrow 3 True, Mark [], Simplify 100 True, Mark [[0, 1]], ShiftSubs, Mark [], Induction False, Mark [[0, 0, 0], [1, 0, 0, 1, 0, 0], [1, 0, 0, 2], [2, 0, 0, 1, 0, 0], [2, 0, 0, 2]], Narrow 0 False, Mark [[0, 0, 1]], Theorem False (F "<===" [F "lgOk" [V "n", F "++" [V "p", F "[]" [V "s"]]], F "&" [F "lgOk" [V "n", V "p"], F "<=" [F "length" [V "s"], V "n"]]]), Mark [[0, 0, 1]], Theorem False (F "===>" [F "<" [V "k", V "n"], F "<=" [F "+" [V "k", F "1" []], V "n"]]), Mark []]