3099 |
3099 |
3100 lemma save_paras_prog_ex: |
3100 lemma save_paras_prog_ex: |
3101 "\<lbrakk>rec_ci (Cn n f gs) = (aprog, rs_pos, a_md); |
3101 "\<lbrakk>rec_ci (Cn n f gs) = (aprog, rs_pos, a_md); |
3102 rec_ci f = (a, aa, ba); |
3102 rec_ci f = (a, aa, ba); |
3103 pstr = Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n) |
3103 pstr = Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n) |
3104 (map rec_ci (f # gs))))\<rbrakk> |
3104 (map rec_ci (gs))))\<rbrakk> |
3105 \<Longrightarrow> \<exists>ap bp cp. |
3105 \<Longrightarrow> \<exists>ap bp cp. |
3106 aprog = ap [+] bp [+] cp \<and> |
3106 aprog = ap [+] bp [+] cp \<and> |
3107 length ap = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + |
3107 length ap = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + |
3108 3 * length gs \<and> bp = mv_boxes 0 (pstr + Suc (length gs)) n" |
3108 3 * length gs \<and> bp = mv_boxes 0 (pstr + Suc (length gs)) n" |
3109 apply(simp add: rec_ci.simps) |
3109 apply(simp add: rec_ci.simps) |
3128 \<forall>k<length gs. rec_calc_rel (gs ! k) lm (ys ! k); |
3128 \<forall>k<length gs. rec_calc_rel (gs ! k) lm (ys ! k); |
3129 length ys = length gs; |
3129 length ys = length gs; |
3130 length lm = n; |
3130 length lm = n; |
3131 rec_ci f = (a, aa, ba); |
3131 rec_ci f = (a, aa, ba); |
3132 pstr = Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n) |
3132 pstr = Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n) |
3133 (map rec_ci (f # gs))))\<rbrakk> |
3133 (map rec_ci (gs))))\<rbrakk> |
3134 \<Longrightarrow> \<exists>stp. abc_steps_l ((\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + |
3134 \<Longrightarrow> \<exists>stp. abc_steps_l ((\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + |
3135 3 * length gs, lm @ 0\<up>(pstr - n) @ ys @ |
3135 3 * length gs, lm @ 0\<up>(pstr - n) @ ys @ |
3136 0\<up>(a_md - pstr - length ys) @ suf_lm) aprog stp = |
3136 0\<up>(a_md - pstr - length ys) @ suf_lm) aprog stp = |
3137 ((\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + |
3137 ((\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + |
3138 3 * length gs + 3 * n, |
3138 3 * length gs + 3 * n, |
3144 "\<forall>k<length gs. rec_calc_rel (gs ! k) lm (ys ! k)" |
3144 "\<forall>k<length gs. rec_calc_rel (gs ! k) lm (ys ! k)" |
3145 "length ys = length gs" |
3145 "length ys = length gs" |
3146 "length lm = n" |
3146 "length lm = n" |
3147 "rec_ci f = (a, aa, ba)" |
3147 "rec_ci f = (a, aa, ba)" |
3148 and g: "pstr = Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n) |
3148 and g: "pstr = Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n) |
3149 (map rec_ci (f # gs))))" |
3149 (map rec_ci (gs))))" |
3150 from h and g have k1: |
3150 from h and g have k1: |
3151 "\<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and> |
3151 "\<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and> |
3152 length ap = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + |
3152 length ap = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + |
3153 3 *length gs \<and> bp = mv_boxes 0 (pstr + Suc (length ys)) n" |
3153 3 *length gs \<and> bp = mv_boxes 0 (pstr + Suc (length ys)) n" |
3154 apply(drule_tac save_paras_prog_ex, auto) |
3154 apply(drule_tac save_paras_prog_ex, auto) |
3188 |
3188 |
3189 lemma calc_gs_prog_ex: |
3189 lemma calc_gs_prog_ex: |
3190 "\<lbrakk>rec_ci (Cn n f gs) = (aprog, rs_pos, a_md); |
3190 "\<lbrakk>rec_ci (Cn n f gs) = (aprog, rs_pos, a_md); |
3191 rec_ci f = (a, aa, ba); |
3191 rec_ci f = (a, aa, ba); |
3192 Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n) |
3192 Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n) |
3193 (map rec_ci (f # gs)))) = pstr\<rbrakk> |
3193 (map rec_ci (gs)))) = pstr\<rbrakk> |
3194 \<Longrightarrow> \<exists>ap bp. aprog = ap [+] bp \<and> |
3194 \<Longrightarrow> \<exists>ap bp. aprog = ap [+] bp \<and> |
3195 ap = cn_merge_gs (map rec_ci gs) pstr" |
3195 ap = cn_merge_gs (map rec_ci gs) pstr" |
3196 apply(simp add: rec_ci.simps) |
3196 apply(simp add: rec_ci.simps) |
3197 apply(rule_tac x = "mv_boxes 0 (Suc (max (Suc n) |
3197 apply(rule_tac x = "mv_boxes 0 (Suc (max (Suc n) |
3198 (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) + length gs)) n [+] |
3198 (Max (insert ba (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) + length gs)) n [+] |
3220 "\<forall>k<length gs. rec_calc_rel (gs ! k) lm (ys ! k)" |
3220 "\<forall>k<length gs. rec_calc_rel (gs ! k) lm (ys ! k)" |
3221 "length ys = length gs" |
3221 "length ys = length gs" |
3222 "length lm = n" |
3222 "length lm = n" |
3223 "rec_ci f = (a, aa, ba)" |
3223 "rec_ci f = (a, aa, ba)" |
3224 "Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n) |
3224 "Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n) |
3225 (map rec_ci (f # gs)))) = pstr" |
3225 (map rec_ci (gs)))) = pstr" |
3226 shows |
3226 shows |
3227 "\<exists>stp. abc_steps_l (0, lm @ 0\<up>(a_md - rs_pos) @ suf_lm) aprog stp = |
3227 "\<exists>stp. abc_steps_l (0, lm @ 0\<up>(a_md - rs_pos) @ suf_lm) aprog stp = |
3228 ((\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 3 * length gs, |
3228 ((\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 3 * length gs, |
3229 lm @ 0\<up>(pstr - n) @ ys @ 0\<up>(a_md -pstr - length ys) @ suf_lm) " |
3229 lm @ 0\<up>(pstr - n) @ ys @ 0\<up>(a_md -pstr - length ys) @ suf_lm) " |
3230 proof - |
3230 proof - |
3285 |
3285 |
3286 lemma [simp]: |
3286 lemma [simp]: |
3287 "\<lbrakk>rec_ci (Cn n f gs) = (aprog, rs_pos, a_md); |
3287 "\<lbrakk>rec_ci (Cn n f gs) = (aprog, rs_pos, a_md); |
3288 rec_calc_rel f ys rs; rec_ci f = (a, aa, ba); |
3288 rec_calc_rel f ys rs; rec_ci f = (a, aa, ba); |
3289 pstr = Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n) |
3289 pstr = Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n) |
3290 (map rec_ci (f # gs))))\<rbrakk> |
3290 (map rec_ci (gs))))\<rbrakk> |
3291 \<Longrightarrow> length ys < pstr" |
3291 \<Longrightarrow> length ys < pstr" |
3292 apply(subgoal_tac "length ys = aa", simp) |
3292 apply(subgoal_tac "length ys = aa", simp) |
3293 apply(subgoal_tac "aa < ba \<and> ba \<le> pstr", |
3293 apply(subgoal_tac "aa < ba \<and> ba \<le> pstr", |
3294 rule basic_trans_rules(22), auto) |
3294 rule basic_trans_rules(22), auto) |
3295 apply(rule min_max.le_supI2) |
3295 apply(rule min_max.le_supI2) |
3299 |
3299 |
3300 lemma reset_new_paras_prog_ex: |
3300 lemma reset_new_paras_prog_ex: |
3301 "\<lbrakk>rec_ci (Cn n f gs) = (aprog, rs_pos, a_md); |
3301 "\<lbrakk>rec_ci (Cn n f gs) = (aprog, rs_pos, a_md); |
3302 rec_ci f = (a, aa, ba); |
3302 rec_ci f = (a, aa, ba); |
3303 Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n) |
3303 Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n) |
3304 (map rec_ci (f # gs)))) = pstr\<rbrakk> |
3304 (map rec_ci (gs)))) = pstr\<rbrakk> |
3305 \<Longrightarrow> \<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and> |
3305 \<Longrightarrow> \<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and> |
3306 length ap = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + |
3306 length ap = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + |
3307 3 *length gs + 3 * n \<and> bp = mv_boxes pstr 0 (length gs)" |
3307 3 *length gs + 3 * n \<and> bp = mv_boxes pstr 0 (length gs)" |
3308 apply(simp add: rec_ci.simps) |
3308 apply(simp add: rec_ci.simps) |
3309 apply(rule_tac x = "cn_merge_gs (map rec_ci gs) (max (Suc n) |
3309 apply(rule_tac x = "cn_merge_gs (map rec_ci gs) (max (Suc n) |
3328 length ys = length gs; |
3328 length ys = length gs; |
3329 length lm = n; |
3329 length lm = n; |
3330 length ys = aa; |
3330 length ys = aa; |
3331 rec_ci f = (a, aa, ba); |
3331 rec_ci f = (a, aa, ba); |
3332 pstr = Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n) |
3332 pstr = Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n) |
3333 (map rec_ci (f # gs))))\<rbrakk> |
3333 (map rec_ci (gs))))\<rbrakk> |
3334 \<Longrightarrow> \<exists>stp. abc_steps_l ((\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + |
3334 \<Longrightarrow> \<exists>stp. abc_steps_l ((\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + |
3335 3 * length gs + 3 * n, |
3335 3 * length gs + 3 * n, |
3336 0\<up>pstr @ ys @ 0 # lm @ 0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm) aprog stp = |
3336 0\<up>pstr @ ys @ 0 # lm @ 0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm) aprog stp = |
3337 ((\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 6 * length gs + 3 * n, |
3337 ((\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 6 * length gs + 3 * n, |
3338 ys @ 0\<up>pstr @ 0 # lm @ 0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm)" |
3338 ys @ 0\<up>pstr @ 0 # lm @ 0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm)" |
3343 "length ys = aa" |
3343 "length ys = aa" |
3344 "\<forall>k<length gs. rec_calc_rel (gs ! k) lm (ys ! k)" |
3344 "\<forall>k<length gs. rec_calc_rel (gs ! k) lm (ys ! k)" |
3345 "length ys = length gs" "length lm = n" |
3345 "length ys = length gs" "length lm = n" |
3346 "rec_ci f = (a, aa, ba)" |
3346 "rec_ci f = (a, aa, ba)" |
3347 and g: "pstr = Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n) |
3347 and g: "pstr = Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n) |
3348 (map rec_ci (f # gs))))" |
3348 (map rec_ci (gs))))" |
3349 from h and g have k1: |
3349 from h and g have k1: |
3350 "\<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and> length ap = |
3350 "\<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and> length ap = |
3351 (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + |
3351 (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + |
3352 3 *length gs + 3 * n \<and> bp = mv_boxes pstr 0 (length ys)" |
3352 3 *length gs + 3 * n \<and> bp = mv_boxes pstr 0 (length ys)" |
3353 by(drule_tac reset_new_paras_prog_ex, auto) |
3353 by(drule_tac reset_new_paras_prog_ex, auto) |
3389 |
3389 |
3390 lemma calc_f_prog_ex: |
3390 lemma calc_f_prog_ex: |
3391 "\<lbrakk>rec_ci (Cn n f gs) = (aprog, rs_pos, a_md); |
3391 "\<lbrakk>rec_ci (Cn n f gs) = (aprog, rs_pos, a_md); |
3392 rec_ci f = (a, aa, ba); |
3392 rec_ci f = (a, aa, ba); |
3393 Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n) |
3393 Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n) |
3394 (map rec_ci (f # gs)))) = pstr\<rbrakk> |
3394 (map rec_ci (gs)))) = pstr\<rbrakk> |
3395 \<Longrightarrow> \<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and> |
3395 \<Longrightarrow> \<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and> |
3396 length ap = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + |
3396 length ap = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + |
3397 6 *length gs + 3 * n \<and> bp = a" |
3397 6 *length gs + 3 * n \<and> bp = a" |
3398 apply(simp add: rec_ci.simps) |
3398 apply(simp add: rec_ci.simps) |
3399 apply(rule_tac x = "cn_merge_gs (map rec_ci gs) (max (Suc n) (Max (insert ba |
3399 apply(rule_tac x = "cn_merge_gs (map rec_ci gs) (max (Suc n) (Max (insert ba |
3411 (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) + length gs)) 0 n" in exI, |
3411 (((\<lambda>(aprog, p, n). n) \<circ> rec_ci) ` set gs))) + length gs)) 0 n" in exI, |
3412 auto simp: abc_append_commute) |
3412 auto simp: abc_append_commute) |
3413 done |
3413 done |
3414 |
3414 |
3415 lemma calc_cn_f: |
3415 lemma calc_cn_f: |
3416 assumes ind: |
3416 assumes ind: |
3417 "\<And>x aprog a_md rs_pos rs suf_lm lm. |
3417 "\<And>x ap fp arity r anything args. |
3418 \<lbrakk>x \<in> set (f # gs); |
3418 \<lbrakk>x = map rec_ci gs; rec_ci f = (ap, arity, fp); rec_calc_rel f args r\<rbrakk> |
3419 rec_ci x = (aprog, rs_pos, a_md); |
3419 \<Longrightarrow> \<exists>stp. abc_steps_l (0, args @ 0 \<up> (fp - arity) @ anything) ap stp = |
3420 rec_calc_rel x lm rs\<rbrakk> |
3420 (length ap, args @ [r] @ 0 \<up> (fp - arity - 1) @ anything)" |
3421 \<Longrightarrow> \<exists>stp. abc_steps_l (0, lm @ 0\<up>(a_md - rs_pos) @ suf_lm) aprog stp = |
|
3422 (length aprog, lm @ [rs] @ 0\<up>(a_md - rs_pos - 1) @ suf_lm)" |
|
3423 and h: "rec_ci (Cn n f gs) = (aprog, rs_pos, a_md)" |
3421 and h: "rec_ci (Cn n f gs) = (aprog, rs_pos, a_md)" |
3424 "rec_calc_rel (Cn n f gs) lm rs" |
3422 "rec_calc_rel (Cn n f gs) lm rs" |
3425 "length ys = length gs" |
3423 "length ys = length gs" |
3426 "rec_calc_rel f ys rs" |
3424 "rec_calc_rel f ys rs" |
3427 "length lm = n" |
3425 "length lm = n" |
3428 "rec_ci f = (a, aa, ba)" |
3426 "rec_ci f = (a, aa, ba)" |
3429 and p: "pstr = Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n) |
3427 and p: "pstr = Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n) |
3430 (map rec_ci (f # gs))))" |
3428 (map rec_ci (gs))))" |
3431 shows "\<exists>stp. abc_steps_l |
3429 shows "\<exists>stp. abc_steps_l |
3432 ((\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 6 * length gs + 3 * n, |
3430 ((\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 6 * length gs + 3 * n, |
3433 ys @ 0\<up>pstr @ 0 # lm @ 0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm) aprog stp = |
3431 ys @ 0\<up>pstr @ 0 # lm @ 0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm) aprog stp = |
3434 ((\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 6 * length gs + |
3432 ((\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 6 * length gs + |
3435 3 * n + length a, |
3433 3 * n + length a, |
3447 "aprog = ap [+] bp [+] cp \<and> |
3445 "aprog = ap [+] bp [+] cp \<and> |
3448 length ap = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + |
3446 length ap = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + |
3449 6 * length gs + 3 * n \<and> bp = a" |
3447 6 * length gs + 3 * n \<and> bp = a" |
3450 from h and this show "?thesis" |
3448 from h and this show "?thesis" |
3451 apply(simp, rule_tac abc_append_exc1, simp_all) |
3449 apply(simp, rule_tac abc_append_exc1, simp_all) |
3452 apply(insert ind[of f "a" aa ba ys rs |
3450 thm ind |
|
3451 apply(insert ind[of "map rec_ci gs" a aa ba ys rs |
3453 "0\<up>(pstr - ba + length gs) @ 0 # lm @ |
3452 "0\<up>(pstr - ba + length gs) @ 0 # lm @ |
3454 0\<up>(a_md - Suc (pstr + length gs + n)) @ suf_lm"], simp) |
3453 0\<up>(a_md - Suc (pstr + length gs + n)) @ suf_lm"], simp) |
3455 apply(subgoal_tac "ba > aa \<and> aa = length gs\<and> pstr \<ge> ba", simp) |
3454 apply(subgoal_tac "ba > aa \<and> aa = length gs\<and> pstr \<ge> ba", simp) |
3456 apply(simp add: exponent_add_iff) |
3455 apply(simp add: exponent_add_iff) |
3457 apply(case_tac pstr, simp add: p) |
3456 apply(case_tac pstr, simp add: p) |
3462 apply(insert p, simp) |
3461 apply(insert p, simp) |
3463 apply(auto intro: min_max.le_supI2) |
3462 apply(auto intro: min_max.le_supI2) |
3464 done |
3463 done |
3465 qed |
3464 qed |
3466 qed |
3465 qed |
3467 (* |
3466 |
3468 lemma [simp]: |
3467 lemma [simp]: |
3469 "\<lbrakk>pstr + length ys + n \<le> a_md; ys \<noteq> []\<rbrakk> \<Longrightarrow> |
3468 "\<lbrakk>pstr + length ys + n \<le> a_md; ys \<noteq> []\<rbrakk> \<Longrightarrow> |
3470 pstr < a_md + length suf_lm" |
3469 pstr < a_md + length suf_lm" |
3471 apply(case_tac "length ys", simp) |
3470 apply(case_tac "length ys", simp) |
3472 apply(arith) |
3471 apply(arith) |
3473 done |
3472 done |
3474 *) |
|
3475 |
3473 |
3476 lemma [simp]: |
3474 lemma [simp]: |
3477 "pstr > length ys |
3475 "pstr > length ys |
3478 \<Longrightarrow> (ys @ rs # 0\<up>pstr @ lm @ |
3476 \<Longrightarrow> (ys @ rs # 0\<up>pstr @ lm @ |
3479 0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm) ! pstr = (0::nat)" |
3477 0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm) ! pstr = (0::nat)" |
3514 |
3512 |
3515 lemma save_rs_prog_ex: |
3513 lemma save_rs_prog_ex: |
3516 "\<lbrakk>rec_ci (Cn n f gs) = (aprog, rs_pos, a_md); |
3514 "\<lbrakk>rec_ci (Cn n f gs) = (aprog, rs_pos, a_md); |
3517 rec_ci f = (a, aa, ba); |
3515 rec_ci f = (a, aa, ba); |
3518 Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n) |
3516 Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n) |
3519 (map rec_ci (f # gs)))) = pstr\<rbrakk> |
3517 (map rec_ci (gs)))) = pstr\<rbrakk> |
3520 \<Longrightarrow> \<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and> |
3518 \<Longrightarrow> \<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and> |
3521 length ap = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + |
3519 length ap = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + |
3522 6 *length gs + 3 * n + length a |
3520 6 *length gs + 3 * n + length a |
3523 \<and> bp = mv_box aa pstr" |
3521 \<and> bp = mv_box aa pstr" |
3524 apply(simp add: rec_ci.simps) |
3522 apply(simp add: rec_ci.simps) |
3547 "length ys = length gs" |
3545 "length ys = length gs" |
3548 "rec_calc_rel f ys rs" |
3546 "rec_calc_rel f ys rs" |
3549 "rec_ci f = (a, aa, ba)" |
3547 "rec_ci f = (a, aa, ba)" |
3550 "length lm = n" |
3548 "length lm = n" |
3551 and pdef: "pstr = Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n) |
3549 and pdef: "pstr = Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n) |
3552 (map rec_ci (f # gs))))" |
3550 (map rec_ci (gs))))" |
3553 shows "\<exists>stp. abc_steps_l |
3551 shows "\<exists>stp. abc_steps_l |
3554 ((\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 6 * length gs |
3552 ((\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 6 * length gs |
3555 + 3 * n + length a, ys @ rs # 0\<up>pstr @ lm @ |
3553 + 3 * n + length a, ys @ rs # 0\<up>pstr @ lm @ |
3556 0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm) aprog stp = |
3554 0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm) aprog stp = |
3557 ((\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 6 * length gs |
3555 ((\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + 6 * length gs |
3641 |
3639 |
3642 lemma mv_box_paras_prog_ex: |
3640 lemma mv_box_paras_prog_ex: |
3643 "\<lbrakk>rec_ci (Cn n f gs) = (aprog, rs_pos, a_md); |
3641 "\<lbrakk>rec_ci (Cn n f gs) = (aprog, rs_pos, a_md); |
3644 rec_ci f = (a, aa, ba); |
3642 rec_ci f = (a, aa, ba); |
3645 Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n) |
3643 Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n) |
3646 (map rec_ci (f # gs)))) = pstr\<rbrakk> |
3644 (map rec_ci (gs)))) = pstr\<rbrakk> |
3647 \<Longrightarrow> \<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and> |
3645 \<Longrightarrow> \<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and> |
3648 length ap = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + |
3646 length ap = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + |
3649 6 *length gs + 3 * n + length a + 3 \<and> bp = empty_boxes (length gs)" |
3647 6 *length gs + 3 * n + length a + 3 \<and> bp = empty_boxes (length gs)" |
3650 apply(simp add: rec_ci.simps) |
3648 apply(simp add: rec_ci.simps) |
3651 apply(rule_tac x = "cn_merge_gs (map rec_ci gs) (max (Suc n) |
3649 apply(rule_tac x = "cn_merge_gs (map rec_ci gs) (max (Suc n) |
3671 "\<forall>k<length gs. rec_calc_rel (gs ! k) lm (ys ! k)" |
3669 "\<forall>k<length gs. rec_calc_rel (gs ! k) lm (ys ! k)" |
3672 "length ys = length gs" |
3670 "length ys = length gs" |
3673 "rec_calc_rel f ys rs" |
3671 "rec_calc_rel f ys rs" |
3674 "rec_ci f = (a, aa, ba)" |
3672 "rec_ci f = (a, aa, ba)" |
3675 and pdef: "pstr = Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n) |
3673 and pdef: "pstr = Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n) |
3676 (map rec_ci (f # gs))))" |
3674 (map rec_ci (gs))))" |
3677 and starts: "ss = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + |
3675 and starts: "ss = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + |
3678 6 * length gs + 3 * n + length a + 3" |
3676 6 * length gs + 3 * n + length a + 3" |
3679 shows "\<exists>stp. abc_steps_l |
3677 shows "\<exists>stp. abc_steps_l |
3680 (ss, ys @ 0\<up>(pstr - length ys) @ rs # 0\<up>length ys |
3678 (ss, ys @ 0\<up>(pstr - length ys) @ rs # 0\<up>length ys |
3681 @ lm @ 0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm) aprog stp = |
3679 @ lm @ 0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm) aprog stp = |
3721 |
3719 |
3722 lemma restore_rs_prog_ex: |
3720 lemma restore_rs_prog_ex: |
3723 "\<lbrakk>rec_ci (Cn n f gs) = (aprog, rs_pos, a_md); |
3721 "\<lbrakk>rec_ci (Cn n f gs) = (aprog, rs_pos, a_md); |
3724 rec_ci f = (a, aa, ba); |
3722 rec_ci f = (a, aa, ba); |
3725 Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n) |
3723 Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n) |
3726 (map rec_ci (f # gs)))) = pstr; |
3724 (map rec_ci (gs)))) = pstr; |
3727 ss = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + |
3725 ss = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + |
3728 8 * length gs + 3 * n + length a + 3\<rbrakk> |
3726 8 * length gs + 3 * n + length a + 3\<rbrakk> |
3729 \<Longrightarrow> \<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and> length ap = ss \<and> |
3727 \<Longrightarrow> \<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and> length ap = ss \<and> |
3730 bp = mv_box pstr n" |
3728 bp = mv_box pstr n" |
3731 apply(simp add: rec_ci.simps) |
3729 apply(simp add: rec_ci.simps) |
3759 "\<forall>k<length gs. rec_calc_rel (gs ! k) lm (ys ! k)" |
3757 "\<forall>k<length gs. rec_calc_rel (gs ! k) lm (ys ! k)" |
3760 "length ys = length gs" |
3758 "length ys = length gs" |
3761 "rec_calc_rel f ys rs" |
3759 "rec_calc_rel f ys rs" |
3762 "rec_ci f = (a, aa, ba)" |
3760 "rec_ci f = (a, aa, ba)" |
3763 and pdef: "pstr = Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n) |
3761 and pdef: "pstr = Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n) |
3764 (map rec_ci (f # gs))))" |
3762 (map rec_ci (gs))))" |
3765 and starts: "ss = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + |
3763 and starts: "ss = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + |
3766 8 * length gs + 3 * n + length a + 3" |
3764 8 * length gs + 3 * n + length a + 3" |
3767 shows "\<exists>stp. abc_steps_l |
3765 shows "\<exists>stp. abc_steps_l |
3768 (ss, 0\<up>pstr @ rs # 0\<up>length ys @ lm @ |
3766 (ss, 0\<up>pstr @ rs # 0\<up>length ys @ lm @ |
3769 0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm) aprog stp = |
3767 0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm) aprog stp = |
3800 |
3798 |
3801 lemma restore_paras_prog_ex: |
3799 lemma restore_paras_prog_ex: |
3802 "\<lbrakk>rec_ci (Cn n f gs) = (aprog, rs_pos, a_md); |
3800 "\<lbrakk>rec_ci (Cn n f gs) = (aprog, rs_pos, a_md); |
3803 rec_ci f = (a, aa, ba); |
3801 rec_ci f = (a, aa, ba); |
3804 Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n) |
3802 Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n) |
3805 (map rec_ci (f # gs)))) = pstr; |
3803 (map rec_ci (gs)))) = pstr; |
3806 ss = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + |
3804 ss = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + |
3807 8 * length gs + 3 * n + length a + 6\<rbrakk> |
3805 8 * length gs + 3 * n + length a + 6\<rbrakk> |
3808 \<Longrightarrow> \<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and> length ap = ss \<and> |
3806 \<Longrightarrow> \<exists> ap bp cp. aprog = ap [+] bp [+] cp \<and> length ap = ss \<and> |
3809 bp = mv_boxes (pstr + Suc (length gs)) (0::nat) n" |
3807 bp = mv_boxes (pstr + Suc (length gs)) (0::nat) n" |
3810 apply(simp add: rec_ci.simps) |
3808 apply(simp add: rec_ci.simps) |
3829 "length ys = length gs" |
3827 "length ys = length gs" |
3830 "rec_calc_rel f ys rs" |
3828 "rec_calc_rel f ys rs" |
3831 "rec_ci f = (a, aa, ba)" |
3829 "rec_ci f = (a, aa, ba)" |
3832 and pdef: |
3830 and pdef: |
3833 "pstr = Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n) |
3831 "pstr = Max (set (Suc n # ba # map (\<lambda>(aprog, p, n). n) |
3834 (map rec_ci (f # gs))))" |
3832 (map rec_ci (gs))))" |
3835 and starts: "ss = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + |
3833 and starts: "ss = (\<Sum>(ap, pos, n)\<leftarrow>map rec_ci gs. length ap) + |
3836 8 * length gs + 3 * n + length a + 6" |
3834 8 * length gs + 3 * n + length a + 6" |
3837 shows "\<exists>stp. abc_steps_l (ss, 0\<up>n @ rs # 0\<up>(pstr - n+ length ys) @ |
3835 shows "\<exists>stp. abc_steps_l (ss, 0\<up>n @ rs # 0\<up>(pstr - n+ length ys) @ |
3838 lm @ 0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm) |
3836 lm @ 0\<up>(a_md - Suc (pstr + length ys + n)) @ suf_lm) |
3839 aprog stp = (ss + 3 * n, lm @ rs # 0\<up>(a_md - Suc n) @ suf_lm)" |
3837 aprog stp = (ss + 3 * n, lm @ rs # 0\<up>(a_md - Suc n) @ suf_lm)" |
3872 8 * length gs + 6 * n + length a + 6" |
3870 8 * length gs + 6 * n + length a + 6" |
3873 apply(simp add: rec_ci.simps, auto simp: cn_merge_gs_len) |
3871 apply(simp add: rec_ci.simps, auto simp: cn_merge_gs_len) |
3874 done |
3872 done |
3875 |
3873 |
3876 lemma cn_case: |
3874 lemma cn_case: |
3877 assumes ind: |
3875 assumes ind1: |
3878 "\<And>x aprog a_md rs_pos rs suf_lm lm. |
3876 "\<And>x aprog a_md rs_pos rs suf_lm lm. |
3879 \<lbrakk>x \<in> set (f # gs); |
3877 \<lbrakk>x \<in> set gs; |
3880 rec_ci x = (aprog, rs_pos, a_md); |
3878 rec_ci x = (aprog, rs_pos, a_md); |
3881 rec_calc_rel x lm rs\<rbrakk> |
3879 rec_calc_rel x lm rs\<rbrakk> |
3882 \<Longrightarrow> \<exists>stp. abc_steps_l (0, lm @ 0\<up>(a_md - rs_pos) @ suf_lm) aprog stp = |
3880 \<Longrightarrow> \<exists>stp. abc_steps_l (0, lm @ 0\<up>(a_md - rs_pos) @ suf_lm) aprog stp = |
3883 (length aprog, lm @ [rs] @ 0\<up>(a_md - rs_pos - 1) @ suf_lm)" |
3881 (length aprog, lm @ [rs] @ 0\<up>(a_md - rs_pos - 1) @ suf_lm)" |
|
3882 and ind2: |
|
3883 "\<And>x ap fp arity r anything args. |
|
3884 \<lbrakk>x = map rec_ci gs; rec_ci f = (ap, arity, fp); rec_calc_rel f args r\<rbrakk> |
|
3885 \<Longrightarrow> \<exists>stp. abc_steps_l (0, args @ 0 \<up> (fp - arity) @ anything) ap stp = |
|
3886 (length ap, args @ [r] @ 0 \<up> (fp - arity - 1) @ anything)" |
3884 and h: "rec_ci (Cn n f gs) = (aprog, rs_pos, a_md)" |
3887 and h: "rec_ci (Cn n f gs) = (aprog, rs_pos, a_md)" |
3885 "rec_calc_rel (Cn n f gs) lm rs" |
3888 "rec_calc_rel (Cn n f gs) lm rs" |
3886 shows "\<exists>stp. abc_steps_l (0, lm @ 0\<up>(a_md - rs_pos) @ suf_lm) aprog stp |
3889 shows "\<exists>stp. abc_steps_l (0, lm @ 0\<up>(a_md - rs_pos) @ suf_lm) aprog stp |
3887 = (length aprog, lm @ [rs] @ 0\<up>(a_md - rs_pos - 1) @ suf_lm)" |
3890 = (length aprog, lm @ [rs] @ 0\<up>(a_md - rs_pos - 1) @ suf_lm)" |
3888 apply(insert h, case_tac "rec_ci f", rule_tac calc_cn_reverse, simp) |
3891 apply(insert h, case_tac "rec_ci f", rule_tac calc_cn_reverse, simp) |
3889 proof - |
3892 proof - |
3890 fix a b c ys |
3893 fix a b c ys |
3891 let ?pstr = "Max (set (Suc n # c # (map (\<lambda>(aprog, p, n). n) |
3894 let ?pstr = "Max (set (Suc n # c # (map (\<lambda>(aprog, p, n). n) |
3892 (map rec_ci (f # gs)))))" |
3895 (map rec_ci (gs)))))" |
3893 let ?gs_len = "listsum (map (\<lambda> (ap, pos, n). length ap) |
3896 let ?gs_len = "listsum (map (\<lambda> (ap, pos, n). length ap) |
3894 (map rec_ci (gs)))" |
3897 (map rec_ci (gs)))" |
3895 assume g: "rec_ci (Cn n f gs) = (aprog, rs_pos, a_md)" |
3898 assume g: "rec_ci (Cn n f gs) = (aprog, rs_pos, a_md)" |
3896 "rec_calc_rel (Cn n f gs) lm rs" |
3899 "rec_calc_rel (Cn n f gs) lm rs" |
3897 "\<forall>k<length gs. rec_calc_rel (gs ! k) lm (ys ! k)" |
3900 "\<forall>k<length gs. rec_calc_rel (gs ! k) lm (ys ! k)" |
3902 hence k1: |
3905 hence k1: |
3903 "\<exists> stp. abc_steps_l (0, lm @ 0\<up>(a_md - rs_pos) @ suf_lm) aprog stp = |
3906 "\<exists> stp. abc_steps_l (0, lm @ 0\<up>(a_md - rs_pos) @ suf_lm) aprog stp = |
3904 (?gs_len + 3 * length gs, lm @ 0\<up>(?pstr - n) @ ys @ |
3907 (?gs_len + 3 * length gs, lm @ 0\<up>(?pstr - n) @ ys @ |
3905 0\<up>(a_md - ?pstr - length ys) @ suf_lm)" |
3908 0\<up>(a_md - ?pstr - length ys) @ suf_lm)" |
3906 apply(rule_tac a = a and aa = b and ba = c in cn_calc_gs) |
3909 apply(rule_tac a = a and aa = b and ba = c in cn_calc_gs) |
3907 apply(rule_tac ind, auto) |
3910 apply(rule_tac ind1, auto) |
3908 done |
3911 done |
3909 from g have k2: |
3912 from g have k2: |
3910 "\<exists> stp. abc_steps_l (?gs_len + 3 * length gs, lm @ |
3913 "\<exists> stp. abc_steps_l (?gs_len + 3 * length gs, lm @ |
3911 0\<up>(?pstr - n) @ ys @ 0\<up>(a_md - ?pstr - length ys) @ suf_lm) aprog stp = |
3914 0\<up>(?pstr - n) @ ys @ 0\<up>(a_md - ?pstr - length ys) @ suf_lm) aprog stp = |
3912 (?gs_len + 3 * length gs + 3 * n, 0\<up>?pstr @ ys @ 0 # lm @ |
3915 (?gs_len + 3 * length gs + 3 * n, 0\<up>?pstr @ ys @ 0 # lm @ |
3926 from g have k4: |
3929 from g have k4: |
3927 "\<exists>stp. abc_steps_l (?gs_len + 6 * length gs + 3 * n, |
3930 "\<exists>stp. abc_steps_l (?gs_len + 6 * length gs + 3 * n, |
3928 ys @ 0\<up>?pstr @ 0 # lm @ 0\<up>(a_md - Suc (?pstr + length ys + n)) @ suf_lm) aprog stp = |
3931 ys @ 0\<up>?pstr @ 0 # lm @ 0\<up>(a_md - Suc (?pstr + length ys + n)) @ suf_lm) aprog stp = |
3929 (?gs_len + 6 * length gs + 3 * n + length a, |
3932 (?gs_len + 6 * length gs + 3 * n + length a, |
3930 ys @ rs # 0\<up>?pstr @ lm @ 0\<up>(a_md - Suc (?pstr + length ys + n)) @ suf_lm)" |
3933 ys @ rs # 0\<up>?pstr @ lm @ 0\<up>(a_md - Suc (?pstr + length ys + n)) @ suf_lm)" |
3931 apply(rule_tac ba = c in calc_cn_f, rule_tac ind, auto) |
3934 apply(rule_tac ba = c in calc_cn_f, rule_tac ind2, auto) |
3932 done |
3935 done |
3933 from g h have k5: |
3936 from g h have k5: |
3934 "\<exists> stp. abc_steps_l (?gs_len + 6 * length gs + 3 * n + length a, |
3937 "\<exists> stp. abc_steps_l (?gs_len + 6 * length gs + 3 * n + length a, |
3935 ys @ rs # 0\<up>?pstr @ lm @ 0\<up>(a_md - Suc (?pstr + length ys + n)) @ suf_lm) |
3938 ys @ rs # 0\<up>?pstr @ lm @ 0\<up>(a_md - Suc (?pstr + length ys + n)) @ suf_lm) |
3936 aprog stp = |
3939 aprog stp = |
4059 thus "\<exists>stp. abc_steps_l (0, args @ 0\<up>(fp - arity) @ anything) ap stp |
4062 thus "\<exists>stp. abc_steps_l (0, args @ 0\<up>(fp - arity) @ anything) ap stp |
4060 = (length ap, args @ [r] @ 0\<up>(fp - arity - 1) @ anything)" |
4063 = (length ap, args @ [r] @ 0\<up>(fp - arity - 1) @ anything)" |
4061 by(erule_tac id_case) |
4064 by(erule_tac id_case) |
4062 next |
4065 next |
4063 fix n f gs ap fp arity r anything args |
4066 fix n f gs ap fp arity r anything args |
4064 assume ind: "\<And>x ap fp arity r anything args. |
4067 assume ind1: "\<And>x ap fp arity r anything args. |
4065 \<lbrakk>x \<in> set (f # gs); |
4068 \<lbrakk>x \<in> set gs; |
4066 rec_ci x = (ap, arity, fp); |
4069 rec_ci x = (ap, arity, fp); |
4067 rec_calc_rel x args r\<rbrakk> |
4070 rec_calc_rel x args r\<rbrakk> |
4068 \<Longrightarrow> \<exists>stp. abc_steps_l (0, args @ 0\<up>(fp - arity) @ anything) ap stp = |
4071 \<Longrightarrow> \<exists>stp. abc_steps_l (0, args @ 0\<up>(fp - arity) @ anything) ap stp = |
4069 (length ap, args @ [r] @ 0\<up>(fp - arity - 1) @ anything)" |
4072 (length ap, args @ [r] @ 0\<up>(fp - arity - 1) @ anything)" |
|
4073 and ind2: |
|
4074 "\<And>x ap fp arity r anything args. |
|
4075 \<lbrakk>x = map rec_ci gs; rec_ci f = (ap, arity, fp); rec_calc_rel f args r\<rbrakk> |
|
4076 \<Longrightarrow> \<exists>stp. abc_steps_l (0, args @ 0 \<up> (fp - arity) @ anything) ap stp = |
|
4077 (length ap, args @ [r] @ 0 \<up> (fp - arity - 1) @ anything)" |
4070 and h: "rec_ci (Cn n f gs) = (ap, arity, fp)" |
4078 and h: "rec_ci (Cn n f gs) = (ap, arity, fp)" |
4071 "rec_calc_rel (Cn n f gs) args r" |
4079 "rec_calc_rel (Cn n f gs) args r" |
4072 from h show |
4080 from h show |
4073 "\<exists>stp. abc_steps_l (0, args @ 0\<up>(fp - arity) @ anything) |
4081 "\<exists>stp. abc_steps_l (0, args @ 0\<up>(fp - arity) @ anything) |
4074 ap stp = (length ap, args @ [r] @ 0\<up>(fp - arity - 1) @ anything)" |
4082 ap stp = (length ap, args @ [r] @ 0\<up>(fp - arity - 1) @ anything)" |
4075 apply(rule_tac cn_case, rule_tac ind, auto) |
4083 apply(rule_tac cn_case) |
|
4084 apply(rule_tac ind1, simp, simp, simp) |
|
4085 apply(rule_tac ind2, auto) |
4076 done |
4086 done |
4077 next |
4087 next |
4078 fix n f ap fp arity r anything args |
4088 fix n f ap fp arity r anything args |
4079 assume ind: |
4089 assume ind: |
4080 "\<And>ap fp arity r anything args. |
4090 "\<And>ap fp arity r anything args. |
4323 done |
4333 done |
4324 from this obtain ys where g1: |
4334 from this obtain ys where g1: |
4325 "(length ys = i \<and> (\<forall> k < i. rec_calc_rel (?ggs ! k) |
4335 "(length ys = i \<and> (\<forall> k < i. rec_calc_rel (?ggs ! k) |
4326 lm (ys ! k)))" .. |
4336 lm (ys ! k)))" .. |
4327 let ?pstr = "Max (set (Suc n # c # map (\<lambda>(aprog, p, n). n) |
4337 let ?pstr = "Max (set (Suc n # c # map (\<lambda>(aprog, p, n). n) |
4328 (map rec_ci (f # gs))))" |
4338 (map rec_ci (gs))))" |
4329 have "\<exists>stp. abc_steps_l (0, lm @ 0\<up>(a_md - n) @ suflm) |
4339 have "\<exists>stp. abc_steps_l (0, lm @ 0\<up>(a_md - n) @ suflm) |
4330 (cn_merge_gs (map rec_ci ?ggs) ?pstr) stp = |
4340 (cn_merge_gs (map rec_ci ?ggs) ?pstr) stp = |
4331 (listsum (map ((\<lambda>(ap, pos, n). length ap) \<circ> rec_ci) ?ggs) + |
4341 (listsum (map ((\<lambda>(ap, pos, n). length ap) \<circ> rec_ci) ?ggs) + |
4332 3 * length ?ggs, lm @ 0\<up>(?pstr - n) @ ys @ 0\<up>(a_md -(?pstr + length ?ggs)) @ |
4342 3 * length ?ggs, lm @ 0\<up>(?pstr - n) @ ys @ 0\<up>(a_md -(?pstr + length ?ggs)) @ |
4333 suflm) " |
4343 suflm) " |