456   "rec_entry = CN rec_lo [Id 2 0, CN rec_pi [CN S [Id 2 1]]]"

   455   "rec_read = CN rec_ldec [Id 1 0, constn 0]"

   457 

   456 

   458 fun rec_listsum2 :: "nat \<Rightarrow> nat \<Rightarrow> recf"

   457 definition 

   459   where

   458   "rec_write = CN rec_penc [S, CN rec_pdec2 [Id 2 1]]"

   460   "rec_listsum2 vl 0 = CN Z [Id vl 0]"

   459 

   461 | "rec_listsum2 vl (Suc n) = CN rec_add [rec_listsum2 vl n, Id vl n]"

   460 lemma read_lemma [simp]:

   462 

   461   "rec_eval rec_read [x] = Read x"

   463 fun rec_strt' :: "nat \<Rightarrow> nat \<Rightarrow> recf"

   462 by (simp add: rec_read_def)

   464   where

   463 

   465   "rec_strt' xs 0 = Z"

   464 lemma write_lemma [simp]:

   466 | "rec_strt' xs (Suc n) = 

   465   "rec_eval rec_write [x, y] = Write x y"

   467       (let dbound = CN rec_add [rec_listsum2 xs n, constn n] in

   466 by (simp add: rec_write_def)

   468        let t1 = CN rec_power [constn 2, dbound] in

   467 

   469        let t2 = CN rec_power [constn 2, CN rec_add [Id xs n, dbound]] in

   468 

   470        CN rec_add [rec_strt' xs n, CN rec_minus [t2, t1]])"

   469 

   471 

   472 fun rec_map :: "recf \<Rightarrow> nat \<Rightarrow> recf list"

   473   where

   474   "rec_map rf vl = map (\<lambda>i. CN rf [Id vl i]) [0..<vl]"

   475 

   476 fun rec_strt :: "nat \<Rightarrow> recf"

   477   where

   478   "rec_strt xs = CN (rec_strt' xs xs) (rec_map S xs)"

   479 

   480 definition 

   481   "rec_scan = CN rec_mod [Id 1 0, constn 2]"