69   shows "tshift p n == (map (\<lambda> (a, s). (a, (if s = 0 then 0 else s + n))) p)"

    69   shows "tshift p n == (map (\<lambda> (a, s). (a, (if s = 0 then 0 else s + n))) p)"

    70 apply(rule eq_reflection)

    70 apply(rule eq_reflection)

    71 apply(auto simp add: tshift.simps)

    71 apply(auto simp add: tshift.simps)

    72 done

    72 done

    73 

    73 

    74 

    82 

    75 consts DUMMY::'a

    83 consts DUMMY::'a

    76 

    84 

    77 notation (latex output)

    85 notation (latex output)

    78   Cons ("_::_" [78,77] 73) and

    86   Cons ("_::_" [78,77] 73) and

    83   tstep ("step") and

    91   tstep ("step") and

    84   steps ("nsteps") and

    92   steps ("nsteps") and

    85   abc_lm_v ("lookup") and

    93   abc_lm_v ("lookup") and

    86   abc_lm_s ("set") and

    94   abc_lm_s ("set") and

    87   haltP ("stdhalt") and 

    95   haltP ("stdhalt") and 

    89   tape_of_nat_list ("\<ulcorner>_\<urcorner>") and 

    97   tape_of_nat_list ("\<ulcorner>_\<urcorner>") and 

    90   DUMMY  ("\<^raw:\mbox{$\_$}>")

    98   DUMMY  ("\<^raw:\mbox{$\_$}>")

    91 

    99 

    92 declare [[show_question_marks = false]]

   100 declare [[show_question_marks = false]]

    93 (*>*)

   101 (*>*)