summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy

changeset 41807 | ab5d2d81f9fb |

parent 41763 | 8ce56536fda7 |

child 41816 | 7a55699805dc |

1.1 --- a/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Mon Feb 21 18:29:47 2011 +0100 1.2 +++ b/src/HOL/Decision_Procs/Reflected_Multivariate_Polynomial.thy Mon Feb 21 23:47:19 2011 +0100 1.3 @@ -253,53 +253,53 @@ 1.4 \<Longrightarrow> isnpolyh (polyadd(p,q)) (min n0 n1)" 1.5 proof(induct p q arbitrary: n0 n1 rule: polyadd.induct) 1.6 case (2 a b c' n' p' n0 n1) 1.7 - from prems have th1: "isnpolyh (C (a,b)) (Suc n')" by simp 1.8 - from prems(3) have th2: "isnpolyh c' (Suc n')" and nplen1: "n' \<ge> n1" by simp_all 1.9 + from 2 have th1: "isnpolyh (C (a,b)) (Suc n')" by simp 1.10 + from 2(3) have th2: "isnpolyh c' (Suc n')" and nplen1: "n' \<ge> n1" by simp_all 1.11 with isnpolyh_mono have cp: "isnpolyh c' (Suc n')" by simp 1.12 - with prems(1)[OF th1 th2] have th3:"isnpolyh (C (a,b) +\<^sub>p c') (Suc n')" by simp 1.13 + with 2(1)[OF th1 th2] have th3:"isnpolyh (C (a,b) +\<^sub>p c') (Suc n')" by simp 1.14 from nplen1 have n01len1: "min n0 n1 \<le> n'" by simp 1.15 - thus ?case using prems th3 by simp 1.16 + thus ?case using 2 th3 by simp 1.17 next 1.18 case (3 c' n' p' a b n1 n0) 1.19 - from prems have th1: "isnpolyh (C (a,b)) (Suc n')" by simp 1.20 - from prems(2) have th2: "isnpolyh c' (Suc n')" and nplen1: "n' \<ge> n1" by simp_all 1.21 + from 3 have th1: "isnpolyh (C (a,b)) (Suc n')" by simp 1.22 + from 3(2) have th2: "isnpolyh c' (Suc n')" and nplen1: "n' \<ge> n1" by simp_all 1.23 with isnpolyh_mono have cp: "isnpolyh c' (Suc n')" by simp 1.24 - with prems(1)[OF th2 th1] have th3:"isnpolyh (c' +\<^sub>p C (a,b)) (Suc n')" by simp 1.25 + with 3(1)[OF th2 th1] have th3:"isnpolyh (c' +\<^sub>p C (a,b)) (Suc n')" by simp 1.26 from nplen1 have n01len1: "min n0 n1 \<le> n'" by simp 1.27 - thus ?case using prems th3 by simp 1.28 + thus ?case using 3 th3 by simp 1.29 next 1.30 case (4 c n p c' n' p' n0 n1) 1.31 hence nc: "isnpolyh c (Suc n)" and np: "isnpolyh p n" by simp_all 1.32 - from prems have nc': "isnpolyh c' (Suc n')" and np': "isnpolyh p' n'" by simp_all 1.33 - from prems have ngen0: "n \<ge> n0" by simp 1.34 - from prems have n'gen1: "n' \<ge> n1" by simp 1.35 + from 4 have nc': "isnpolyh c' (Suc n')" and np': "isnpolyh p' n'" by simp_all 1.36 + from 4 have ngen0: "n \<ge> n0" by simp 1.37 + from 4 have n'gen1: "n' \<ge> n1" by simp 1.38 have "n < n' \<or> n' < n \<or> n = n'" by auto 1.39 moreover {assume eq: "n = n'" 1.40 - with prems(2)[OF nc nc'] 1.41 + with 4(2)[OF nc nc'] 1.42 have ncc':"isnpolyh (c +\<^sub>p c') (Suc n)" by auto 1.43 hence ncc'n01: "isnpolyh (c +\<^sub>p c') (min n0 n1)" 1.44 using isnpolyh_mono[where n'="min n0 n1" and n="Suc n"] ngen0 n'gen1 by auto 1.45 - from eq prems(1)[OF np np'] have npp': "isnpolyh (p +\<^sub>p p') n" by simp 1.46 + from eq 4(1)[OF np np'] have npp': "isnpolyh (p +\<^sub>p p') n" by simp 1.47 have minle: "min n0 n1 \<le> n'" using ngen0 n'gen1 eq by simp 1.48 - from minle npp' ncc'n01 prems ngen0 n'gen1 ncc' have ?case by (simp add: Let_def)} 1.49 + from minle npp' ncc'n01 eq ngen0 n'gen1 ncc' have ?case by (simp add: Let_def)} 1.50 moreover {assume lt: "n < n'" 1.51 have "min n0 n1 \<le> n0" by simp 1.52 - with prems have th1:"min n0 n1 \<le> n" by auto 1.53 - from prems have th21: "isnpolyh c (Suc n)" by simp 1.54 - from prems have th22: "isnpolyh (CN c' n' p') n'" by simp 1.55 + with 4 have th1:"min n0 n1 \<le> n" by auto 1.56 + from 4 have th21: "isnpolyh c (Suc n)" by simp 1.57 + from 4 have th22: "isnpolyh (CN c' n' p') n'" by simp 1.58 from lt have th23: "min (Suc n) n' = Suc n" by arith 1.59 - from prems(4)[OF th21 th22] 1.60 + from 4(4)[OF th21 th22] 1.61 have "isnpolyh (polyadd (c, CN c' n' p')) (Suc n)" using th23 by simp 1.62 - with prems th1 have ?case by simp } 1.63 + with 4 lt th1 have ?case by simp } 1.64 moreover {assume gt: "n' < n" hence gt': "n' < n \<and> \<not> n < n'" by simp 1.65 have "min n0 n1 \<le> n1" by simp 1.66 - with prems have th1:"min n0 n1 \<le> n'" by auto 1.67 - from prems have th21: "isnpolyh c' (Suc n')" by simp_all 1.68 - from prems have th22: "isnpolyh (CN c n p) n" by simp 1.69 + with 4 have th1:"min n0 n1 \<le> n'" by auto 1.70 + from 4 have th21: "isnpolyh c' (Suc n')" by simp_all 1.71 + from 4 have th22: "isnpolyh (CN c n p) n" by simp 1.72 from gt have th23: "min n (Suc n') = Suc n'" by arith 1.73 - from prems(3)[OF th22 th21] 1.74 + from 4(3)[OF th22 th21] 1.75 have "isnpolyh (polyadd (CN c n p,c')) (Suc n')" using th23 by simp 1.76 - with prems th1 have ?case by simp} 1.77 + with 4 gt th1 have ?case by simp} 1.78 ultimately show ?case by blast 1.79 qed auto 1.80 1.81 @@ -370,14 +370,15 @@ 1.82 \<Longrightarrow> degreen p m = degreen q m" 1.83 proof (induct p q arbitrary: m n0 n1 c rule: polyadd.induct) 1.84 case (4 c n p c' n' p' m n0 n1 x) 1.85 - {assume nn': "n' < n" hence ?case using prems by simp} 1.86 + {assume nn': "n' < n" hence ?case using 4 by simp} 1.87 moreover 1.88 {assume nn':"\<not> n' < n" hence "n < n' \<or> n = n'" by arith 1.89 - moreover {assume "n < n'" with prems have ?case by simp } 1.90 - moreover {assume eq: "n = n'" hence ?case using prems 1.91 + moreover {assume "n < n'" with 4 have ?case by simp } 1.92 + moreover {assume eq: "n = n'" hence ?case using 4 1.93 apply (cases "p +\<^sub>p p' = 0\<^sub>p") 1.94 apply (auto simp add: Let_def) 1.95 - by blast 1.96 + apply blast 1.97 + done 1.98 } 1.99 ultimately have ?case by blast} 1.100 ultimately show ?case by blast 1.101 @@ -664,13 +665,13 @@ 1.102 qed 1.103 1.104 lemma polypow_normh: 1.105 - assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 1.106 + assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 1.107 shows "isnpolyh p n \<Longrightarrow> isnpolyh (polypow k p) n" 1.108 proof (induct k arbitrary: n rule: polypow.induct) 1.109 case (2 k n) 1.110 let ?q = "polypow (Suc k div 2) p" 1.111 let ?d = "polymul (?q,?q)" 1.112 - from prems have th1:"isnpolyh ?q n" and th2: "isnpolyh p n" by blast+ 1.113 + from 2 have th1:"isnpolyh ?q n" and th2: "isnpolyh p n" by blast+ 1.114 from polymul_normh[OF th1 th1] have dn: "isnpolyh ?d n" by simp 1.115 from polymul_normh[OF th2 dn] have on: "isnpolyh (polymul(p,?d)) n" by simp 1.116 from dn on show ?case by (simp add: Let_def) 1.117 @@ -695,7 +696,7 @@ 1.118 1.119 1.120 lemma shift1: "Ipoly bs (shift1 p) = Ipoly bs (Mul (Bound 0) p)" 1.121 -by (simp add: shift1_def polymul) 1.122 + by (simp add: shift1_def) 1.123 1.124 lemma shift1_isnpoly: 1.125 assumes pn: "isnpoly p" and pnz: "p \<noteq> 0\<^sub>p" shows "isnpoly (shift1 p) " 1.126 @@ -713,7 +714,7 @@ 1.127 using f np by (induct k arbitrary: p, auto) 1.128 1.129 lemma funpow_shift1: "(Ipoly bs (funpow n shift1 p) :: 'a :: {field_char_0, field_inverse_zero}) = Ipoly bs (Mul (Pw (Bound 0) n) p)" 1.130 - by (induct n arbitrary: p, simp_all add: shift1_isnpoly shift1 power_Suc ) 1.131 + by (induct n arbitrary: p) (simp_all add: shift1_isnpoly shift1) 1.132 1.133 lemma shift1_isnpolyh: "isnpolyh p n0 \<Longrightarrow> p\<noteq> 0\<^sub>p \<Longrightarrow> isnpolyh (shift1 p) 0" 1.134 using isnpolyh_mono[where n="n0" and n'="0" and p="p"] by (simp add: shift1_def) 1.135 @@ -731,10 +732,10 @@ 1.136 using np 1.137 proof (induct p arbitrary: n rule: behead.induct) 1.138 case (1 c p n) hence pn: "isnpolyh p n" by simp 1.139 - from prems(2)[OF pn] 1.140 + from 1(1)[OF pn] 1.141 have th:"Ipoly bs (Add (Mul (head p) (Pw (Bound 0) (degree p))) (behead p)) = Ipoly bs p" . 1.142 then show ?case using "1.hyps" apply (simp add: Let_def,cases "behead p = 0\<^sub>p") 1.143 - by (simp_all add: th[symmetric] field_simps power_Suc) 1.144 + by (simp_all add: th[symmetric] field_simps) 1.145 qed (auto simp add: Let_def) 1.146 1.147 lemma behead_isnpolyh: 1.148 @@ -747,7 +748,7 @@ 1.149 case (goal1 c n p n') 1.150 hence "n = Suc (n - 1)" by simp 1.151 hence "isnpolyh p (Suc (n - 1))" using `isnpolyh p n` by simp 1.152 - with prems(2) show ?case by simp 1.153 + with goal1(2) show ?case by simp 1.154 qed 1.155 1.156 lemma isconstant_polybound0: "isnpolyh p n0 \<Longrightarrow> isconstant p \<longleftrightarrow> polybound0 p" 1.157 @@ -838,7 +839,7 @@ 1.158 qed 1.159 1.160 lemma decr_maxindex: "polybound0 p \<Longrightarrow> maxindex (decrpoly p) = maxindex p - 1" 1.161 - by (induct p, auto) 1.162 + by (induct p) auto 1.163 1.164 lemma wf_bs_insensitive: "length bs = length bs' \<Longrightarrow> wf_bs bs p = wf_bs bs' p" 1.165 unfolding wf_bs_def by simp 1.166 @@ -1033,7 +1034,7 @@ 1.167 isnpolyh_unique[OF polyadd_normh[OF zero_normh np] np] by simp_all 1.168 1.169 lemma polymul_1[simp]: 1.170 - assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 1.171 + assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 1.172 and np: "isnpolyh p n0" shows "p *\<^sub>p 1\<^sub>p = p" and "1\<^sub>p *\<^sub>p p = p" 1.173 using isnpolyh_unique[OF polymul_normh[OF np one_normh] np] 1.174 isnpolyh_unique[OF polymul_normh[OF one_normh np] np] by simp_all 1.175 @@ -1101,17 +1102,17 @@ 1.176 next 1.177 case (2 a b c' n' p') 1.178 let ?c = "(a,b)" 1.179 - from prems have "degree (C ?c) = degree (CN c' n' p')" by simp 1.180 + from 2 have "degree (C ?c) = degree (CN c' n' p')" by simp 1.181 hence nz:"n' > 0" by (cases n', auto) 1.182 hence "head (CN c' n' p') = CN c' n' p'" by (cases n', auto) 1.183 - with prems show ?case by simp 1.184 + with 2 show ?case by simp 1.185 next 1.186 case (3 c n p a' b') 1.187 let ?c' = "(a',b')" 1.188 - from prems have "degree (C ?c') = degree (CN c n p)" by simp 1.189 + from 3 have "degree (C ?c') = degree (CN c n p)" by simp 1.190 hence nz:"n > 0" by (cases n, auto) 1.191 hence "head (CN c n p) = CN c n p" by (cases n, auto) 1.192 - with prems show ?case by simp 1.193 + with 3 show ?case by simp 1.194 next 1.195 case (4 c n p c' n' p') 1.196 hence H: "isnpolyh (CN c n p) n0" "isnpolyh (CN c' n' p') n1" 1.197 @@ -1126,36 +1127,40 @@ 1.198 moreover 1.199 {assume nn': "n = n'" 1.200 have "n = 0 \<or> n >0" by arith 1.201 - moreover {assume nz: "n = 0" hence ?case using prems by (auto simp add: Let_def degcmc')} 1.202 + moreover {assume nz: "n = 0" hence ?case using 4 nn' by (auto simp add: Let_def degcmc')} 1.203 moreover {assume nz: "n > 0" 1.204 - with nn' H(3) have cc':"c = c'" and pp': "p = p'" by (cases n, auto)+ 1.205 - hence ?case using polysub_same_0[OF p'nh, simplified polysub_def split_def fst_conv snd_conv] polysub_same_0[OF c'nh, simplified polysub_def split_def fst_conv snd_conv] using nn' prems by (simp add: Let_def)} 1.206 + with nn' H(3) have cc': "c = c'" and pp': "p = p'" by (cases n, auto)+ 1.207 + hence ?case 1.208 + using polysub_same_0 [OF p'nh, simplified polysub_def split_def fst_conv snd_conv] 1.209 + polysub_same_0 [OF c'nh, simplified polysub_def split_def fst_conv snd_conv] 1.210 + using 4 nn' by (simp add: Let_def) } 1.211 ultimately have ?case by blast} 1.212 moreover 1.213 {assume nn': "n < n'" hence n'p: "n' > 0" by simp 1.214 hence headcnp':"head (CN c' n' p') = CN c' n' p'" by (cases n', simp_all) 1.215 - have degcnp': "degree (CN c' n' p') = 0" and degcnpeq: "degree (CN c n p) = degree (CN c' n' p')" using prems by (cases n', simp_all) 1.216 - hence "n > 0" by (cases n, simp_all) 1.217 - hence headcnp: "head (CN c n p) = CN c n p" by (cases n, auto) 1.218 - from H(3) headcnp headcnp' nn' have ?case by auto} 1.219 + have degcnp': "degree (CN c' n' p') = 0" and degcnpeq: "degree (CN c n p) = degree (CN c' n' p')" 1.220 + using 4 nn' by (cases n', simp_all) 1.221 + hence "n > 0" by (cases n) simp_all 1.222 + hence headcnp: "head (CN c n p) = CN c n p" by (cases n) auto 1.223 + from H(3) headcnp headcnp' nn' have ?case by auto } 1.224 moreover 1.225 {assume nn': "n > n'" hence np: "n > 0" by simp 1.226 - hence headcnp:"head (CN c n p) = CN c n p" by (cases n, simp_all) 1.227 - from prems have degcnpeq: "degree (CN c' n' p') = degree (CN c n p)" by simp 1.228 - from np have degcnp: "degree (CN c n p) = 0" by (cases n, simp_all) 1.229 + hence headcnp: "head (CN c n p) = CN c n p" by (cases n) simp_all 1.230 + from 4 have degcnpeq: "degree (CN c' n' p') = degree (CN c n p)" by simp 1.231 + from np have degcnp: "degree (CN c n p) = 0" by (cases n) simp_all 1.232 with degcnpeq have "n' > 0" by (cases n', simp_all) 1.233 - hence headcnp': "head (CN c' n' p') = CN c' n' p'" by (cases n', auto) 1.234 - from H(3) headcnp headcnp' nn' have ?case by auto} 1.235 + hence headcnp': "head (CN c' n' p') = CN c' n' p'" by (cases n') auto 1.236 + from H(3) headcnp headcnp' nn' have ?case by auto } 1.237 ultimately show ?case by blast 1.238 qed auto 1.239 1.240 lemma shift1_head : "isnpolyh p n0 \<Longrightarrow> head (shift1 p) = head p" 1.241 -by (induct p arbitrary: n0 rule: head.induct, simp_all add: shift1_def) 1.242 + by (induct p arbitrary: n0 rule: head.induct) (simp_all add: shift1_def) 1.243 1.244 lemma funpow_shift1_head: "isnpolyh p n0 \<Longrightarrow> p\<noteq> 0\<^sub>p \<Longrightarrow> head (funpow k shift1 p) = head p" 1.245 proof(induct k arbitrary: n0 p) 1.246 case (Suc k n0 p) hence "isnpolyh (shift1 p) 0" by (simp add: shift1_isnpolyh) 1.247 - with prems have "head (funpow k shift1 (shift1 p)) = head (shift1 p)" 1.248 + with Suc have "head (funpow k shift1 (shift1 p)) = head (shift1 p)" 1.249 and "head (shift1 p) = head p" by (simp_all add: shift1_head) 1.250 thus ?case by (simp add: funpow_swap1) 1.251 qed auto 1.252 @@ -1194,19 +1199,20 @@ 1.253 apply (metis head_nz) 1.254 apply (metis head_nz) 1.255 apply (metis degree.simps(9) gr0_conv_Suc head.simps(1) less_Suc0 not_less_eq) 1.256 -by (metis degree.simps(9) gr0_conv_Suc nat_less_le order_le_less_trans) 1.257 +apply (metis degree.simps(9) gr0_conv_Suc nat_less_le order_le_less_trans) 1.258 +done 1.259 1.260 lemma polymul_head_polyeq: 1.261 - assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 1.262 + assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 1.263 shows "\<lbrakk>isnpolyh p n0; isnpolyh q n1 ; p \<noteq> 0\<^sub>p ; q \<noteq> 0\<^sub>p \<rbrakk> \<Longrightarrow> head (p *\<^sub>p q) = head p *\<^sub>p head q" 1.264 proof (induct p q arbitrary: n0 n1 rule: polymul.induct) 1.265 case (2 a b c' n' p' n0 n1) 1.266 hence "isnpolyh (head (CN c' n' p')) n1" "isnormNum (a,b)" by (simp_all add: head_isnpolyh) 1.267 - thus ?case using prems by (cases n', auto) 1.268 + thus ?case using 2 by (cases n') auto 1.269 next 1.270 case (3 c n p a' b' n0 n1) 1.271 hence "isnpolyh (head (CN c n p)) n0" "isnormNum (a',b')" by (simp_all add: head_isnpolyh) 1.272 - thus ?case using prems by (cases n, auto) 1.273 + thus ?case using 3 by (cases n) auto 1.274 next 1.275 case (4 c n p c' n' p' n0 n1) 1.276 hence norm: "isnpolyh p n" "isnpolyh c (Suc n)" "isnpolyh p' n'" "isnpolyh c' (Suc n')" 1.277 @@ -1215,15 +1221,14 @@ 1.278 have "n < n' \<or> n' < n \<or> n = n'" by arith 1.279 moreover 1.280 {assume nn': "n < n'" hence ?case 1.281 - thm prems 1.282 - using norm 1.283 - prems(6)[rule_format, OF nn' norm(1,6)] 1.284 - prems(7)[rule_format, OF nn' norm(2,6)] by (simp, cases n, simp,cases n', simp_all)} 1.285 + using norm 1.286 + 4(5)[rule_format, OF nn' norm(1,6)] 1.287 + 4(6)[rule_format, OF nn' norm(2,6)] by (simp, cases n, simp,cases n', simp_all) } 1.288 moreover {assume nn': "n'< n" 1.289 hence stupid: "n' < n \<and> \<not> n < n'" by simp 1.290 - hence ?case using norm prems(4) [rule_format, OF stupid norm(5,3)] 1.291 - prems(5)[rule_format, OF stupid norm(5,4)] 1.292 - by (simp,cases n',simp,cases n,auto)} 1.293 + hence ?case using norm 4(3) [rule_format, OF stupid norm(5,3)] 1.294 + 4(4)[rule_format, OF stupid norm(5,4)] 1.295 + by (simp,cases n',simp,cases n,auto) } 1.296 moreover {assume nn': "n' = n" 1.297 hence stupid: "\<not> n' < n \<and> \<not> n < n'" by simp 1.298 from nn' polymul_normh[OF norm(5,4)] 1.299 @@ -1247,8 +1252,8 @@ 1.300 have dth:"degree (CN c 0 p *\<^sub>p c') < degree (CN 0\<^sub>p 0 (CN c 0 p *\<^sub>p p'))" by simp 1.301 hence dth':"degree (CN c 0 p *\<^sub>p c') \<noteq> degree (CN 0\<^sub>p 0 (CN c 0 p *\<^sub>p p'))" by simp 1.302 from polyadd_head[OF ncnpc'[simplified nz] ncnpp0'[simplified nz] dth'] dth 1.303 - have ?case using norm prems(2)[rule_format, OF stupid norm(5,3)] 1.304 - prems(3)[rule_format, OF stupid norm(5,4)] nn' nz by simp } 1.305 + have ?case using norm 4(1)[rule_format, OF stupid norm(5,3)] 1.306 + 4(2)[rule_format, OF stupid norm(5,4)] nn' nz by simp } 1.307 ultimately have ?case by (cases n) auto} 1.308 ultimately show ?case by blast 1.309 qed simp_all 1.310 @@ -1603,12 +1608,13 @@ 1.311 1.312 definition "swapnorm n m t = polynate (swap n m t)" 1.313 1.314 -lemma swapnorm: assumes nbs: "n < length bs" and mbs: "m < length bs" 1.315 +lemma swapnorm: 1.316 + assumes nbs: "n < length bs" and mbs: "m < length bs" 1.317 shows "((Ipoly bs (swapnorm n m t) :: 'a\<Colon>{field_char_0, field_inverse_zero})) = Ipoly ((bs[n:= bs!m])[m:= bs!n]) t" 1.318 - using swap[OF prems] swapnorm_def by simp 1.319 + using swap[OF assms] swapnorm_def by simp 1.320 1.321 lemma swapnorm_isnpoly[simp]: 1.322 - assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 1.323 + assumes "SORT_CONSTRAINT('a::{field_char_0, field_inverse_zero})" 1.324 shows "isnpoly (swapnorm n m p)" 1.325 unfolding swapnorm_def by simp 1.326 1.327 @@ -1625,9 +1631,9 @@ 1.328 "isweaknpoly p = False" 1.329 1.330 lemma isnpolyh_isweaknpoly: "isnpolyh p n0 \<Longrightarrow> isweaknpoly p" 1.331 - by (induct p arbitrary: n0, auto) 1.332 + by (induct p arbitrary: n0) auto 1.333 1.334 lemma swap_isweanpoly: "isweaknpoly p \<Longrightarrow> isweaknpoly (swap n m p)" 1.335 - by (induct p, auto) 1.336 + by (induct p) auto 1.337 1.338 end 1.339 \ No newline at end of file