Stay action with current symbol leaves tape unchanged
Provedact_stay_noopApplying a Stay action that writes the symbol already under the head leaves the tape unchanged: the head does not move and every cell keeps its value.
Formal statement
import Definitions.Def_CookLevin_Basic
open CookLevin
theorem act_stay_noop (tp : Tape) :
act (tp.1 tp.2, Direction.Stay) tp = tp := by sorry