tm: comparison thys/UF

equal deleted inserted replaced

-:aea02b5a58d2
+:6e7244ae43b8
 fun Scan :: "nat \<Rightarrow> nat"
 where
 "Scan r = r mod 2"
 definition
-"rec_scan = CN rec_rem [Id 1 0, constn 2]"
+"rec_scan = CN rec_mod [Id 1 0, constn 2]"
 lemma scan_lemma [simp]:
 "rec_eval rec_scan [r] = r mod 2"
 by(simp add: rec_scan_def)
 "rec_newleft =
 (let cond1 = CN rec_disj [CN rec_eq [Id 3 2, Z], CN rec_eq [Id 3 2, constn 1]] in
 let cond2 = CN rec_eq [Id 3 2, constn 2] in
 let cond3 = CN rec_eq [Id 3 2, constn 3] in
 let case3 = CN rec_add [CN rec_mult [constn 2, Id 3 0],
-CN rec_rem [Id 3 1, constn 2]] in
+CN rec_mod [Id 3 1, constn 2]] in
 CN rec_if [cond1, Id 3 0,
 CN rec_if [cond2, CN rec_quo [Id 3 0, constn 2],
 CN rec_if [cond3, case3, Id 3 0]]])"
 definition
 "rec_newright =
 (let condn = \<lambda>n. CN rec_eq [Id 3 2, constn n] in
 let case0 = CN rec_minus [Id 3 1, CN rec_scan [Id 3 1]] in
 let case1 = CN rec_minus [CN rec_add [Id 3 1, constn 1], CN rec_scan [Id 3 1]] in
 let case2 = CN rec_add [CN rec_mult [constn 2, Id 3 1],
-CN rec_rem [Id 3 0, constn 2]] in
+CN rec_mod [Id 3 0, constn 2]] in
 let case3 = CN rec_quo [Id 2 1, constn 2] in
 CN rec_if [condn 0, case0,
 CN rec_if [condn 1, case1,
 CN rec_if [condn 2, case2,
 CN rec_if [condn 3, case3, Id 3 1]]]])"