theory FieldAccessors

lemma field_access_take_drop_general:
  "\<forall>s m n f bs. field_lookup t f m = Some (s,n) \<longrightarrow> wf_fd t \<longrightarrow>
      length bs = size_td t \<longrightarrow>
      take (size_td s) (drop (n - m) (access_ti t v bs)) =
        access_ti s v (take (size_td s) (drop (n - m) bs))"
  "\<forall>s m n f bs. field_lookup_struct st f m = Some (s,n) \<longrightarrow> wf_fd_struct st \<longrightarrow>
      length bs = size_td_struct st \<longrightarrow>
      take (size_td s) (drop (n - m) (access_ti_struct st v bs)) =
        access_ti s v (take (size_td s) (drop (n - m) bs))"
  "\<forall>s m n f bs. field_lookup_list ts f m = Some (s,n) \<longrightarrow> wf_fd_list ts \<longrightarrow>
      length bs = size_td_list ts \<longrightarrow>
      take (size_td s) (drop (n - m) (access_ti_list ts v bs)) =
        access_ti s v (take (size_td s) (drop (n - m) bs))"
  "\<forall>s m n f bs. field_lookup_pair x f m = Some (s,n) \<longrightarrow> wf_fd_pair x \<longrightarrow>
      length bs = size_td_pair x \<longrightarrow>
      take (size_td s) (drop (n - m) (access_ti_pair x v bs)) =
        access_ti s v (take (size_td s) (drop (n - m) bs))" apply (induct t and st and ts and x) apply auto[4] apply(thin_tac "All P" for P)+ apply(drule wf_fd_cons_structD) apply(clarsimp simp: fd_cons_struct_def fd_cons_desc_def fd_cons_length_def) apply simp apply(clarsimp simp: min_def)? apply(frule wf_fd_cons_pairD) apply(clarsimp simp: fd_cons_pair_def fd_cons_desc_def fd_cons_length_def) apply(clarsimp split: option.splits) apply(subst drop_all) apply clarsimp apply(drule field_lookup_offset_le, clarsimp) apply(case_tac dt_pair) apply(clarsimp simp: fd_cons_length_def) apply arith apply simp apply(rotate_tac -3) apply(drule_tac x=s in spec) apply(drule_tac x="m + size_td (dt_fst dt_pair)" in spec) apply(drule_tac x=n in spec) apply(erule impE) apply fast apply(subgoal_tac "(size_td_pair dt_pair - (n - m)) = 0") apply simp apply(case_tac dt_pair, simp) apply(drule field_lookup_offset_le, clarsimp) apply(case_tac dt_pair, simp) apply(drule field_lookup_offset_le, clarsimp) apply simp apply(subgoal_tac "(size_td s - (size_td_pair dt_pair - (n - m))) = 0") prefer 2 apply clarsimp apply(drule td_set_pair_field_lookup_pairD) apply(drule td_set_pair_offset_size_m) apply simp apply simp apply(drule_tac x=s in spec) apply(drule_tac x=m in spec) apply(drule_tac x=n in spec) apply(drule mp, fast) apply(frule(1) wf_fd_field_lookup) apply (case_tac "size_td s = 0") apply (simp add: ex_with_length) apply(rule trans, drule spec, erule mp) apply simp apply(simp add: take_drop) apply auto done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<forall>s m n f bs. field_lookup t f m = Some (s, n) \<longrightarrow> wf_fd t \<longrightarrow> length bs = size_td t \<longrightarrow> take (size_td s) (drop (n - m) (access_ti t v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) &&& \<forall>s m n f bs. field_lookup_struct st f m = Some (s, n) \<longrightarrow> wf_fd_struct st \<longrightarrow> length bs = size_td_struct st \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_struct st v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))) &&& \<forall>s m n f bs. field_lookup_list ts f m = Some (s, n) \<longrightarrow> wf_fd_list ts \<longrightarrow> length bs = size_td_list ts \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list ts v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) &&& \<forall>s m n f bs. field_lookup_pair x f m = Some (s, n) \<longrightarrow> wf_fd_pair x \<longrightarrow> length bs = size_td_pair x \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair x v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) proof (prove)
goal (6 subgoals):
 1. \<And>typ_struct list. \<forall>s m n f bs. field_lookup_struct typ_struct f m = Some (s, n) \<longrightarrow> wf_fd_struct typ_struct \<longrightarrow> length bs = size_td_struct typ_struct \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_struct typ_struct v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) \<Longrightarrow> \<forall>s m n f bs. field_lookup (TypDesc typ_struct list) f m = Some (s, n) \<longrightarrow> wf_fd (TypDesc typ_struct list) \<longrightarrow> length bs = size_td (TypDesc typ_struct list) \<longrightarrow> take (size_td s) (drop (n - m) (access_ti (TypDesc typ_struct list) v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))
 2. \<And>nat1 nat2 a. \<forall>s m n f bs. field_lookup_struct (TypScalar nat1 nat2 a) f m = Some (s, n) \<longrightarrow> wf_fd_struct (TypScalar nat1 nat2 a) \<longrightarrow> length bs = size_td_struct (TypScalar nat1 nat2 a) \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_struct (TypScalar nat1 nat2 a) v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))
 3. \<And>list. \<forall>s m n f bs. field_lookup_list list f m = Some (s, n) \<longrightarrow> wf_fd_list list \<longrightarrow> length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) \<Longrightarrow> \<forall>s m n f bs. field_lookup_struct (TypAggregate list) f m = Some (s, n) \<longrightarrow> wf_fd_struct (TypAggregate list) \<longrightarrow> length bs = size_td_struct (TypAggregate list) \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_struct (TypAggregate list) v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))
 4. \<forall>s m n f bs. field_lookup_list [] f m = Some (s, n) \<longrightarrow> wf_fd_list [] \<longrightarrow> length bs = size_td_list [] \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list [] v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))
 5. \<And>dt_pair list. \<lbrakk>\<forall>s m n f bs. field_lookup_pair dt_pair f m = Some (s, n) \<longrightarrow> wf_fd_pair dt_pair \<longrightarrow> length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)); \<forall>s m n f bs. field_lookup_list list f m = Some (s, n) \<longrightarrow> wf_fd_list list \<longrightarrow> length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))\<rbrakk> \<Longrightarrow> \<forall>s m n f bs. field_lookup_list (dt_pair # list) f m = Some (s, n) \<longrightarrow> wf_fd_list (dt_pair # list) \<longrightarrow> length bs = size_td_list (dt_pair # list) \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list (dt_pair # list) v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))
 6. \<And>typ_desc list. \<forall>s m n f bs. field_lookup typ_desc f m = Some (s, n) \<longrightarrow> wf_fd typ_desc \<longrightarrow> length bs = size_td typ_desc \<longrightarrow> take (size_td s) (drop (n - m) (access_ti typ_desc v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) \<Longrightarrow> \<forall>s m n f bs. field_lookup_pair (DTPair typ_desc list) f m = Some (s, n) \<longrightarrow> wf_fd_pair (DTPair typ_desc list) \<longrightarrow> length bs = size_td_pair (DTPair typ_desc list) \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair (DTPair typ_desc list) v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) proof (prove)
goal (3 subgoals):
 1. \<And>typ_struct bs. \<lbrakk>\<forall>s m n. (\<exists>f. field_lookup_struct typ_struct f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_struct typ_struct \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_struct typ_struct v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); wf_fd_struct typ_struct; length bs = size_td_struct typ_struct; \<not> length (access_ti_struct typ_struct v bs) \<le> size_td_struct typ_struct\<rbrakk> \<Longrightarrow> False
 2. \<And>dt_pair list. \<lbrakk>\<forall>s m n f bs. field_lookup_pair dt_pair f m = Some (s, n) \<longrightarrow> wf_fd_pair dt_pair \<longrightarrow> length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)); \<forall>s m n f bs. field_lookup_list list f m = Some (s, n) \<longrightarrow> wf_fd_list list \<longrightarrow> length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))\<rbrakk> \<Longrightarrow> \<forall>s m n f bs. field_lookup_list (dt_pair # list) f m = Some (s, n) \<longrightarrow> wf_fd_list (dt_pair # list) \<longrightarrow> length bs = size_td_list (dt_pair # list) \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list (dt_pair # list) v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))
 3. \<And>typ_desc list. \<forall>s m n f bs. field_lookup typ_desc f m = Some (s, n) \<longrightarrow> wf_fd typ_desc \<longrightarrow> length bs = size_td typ_desc \<longrightarrow> take (size_td s) (drop (n - m) (access_ti typ_desc v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) \<Longrightarrow> \<forall>s m n f bs. field_lookup_pair (DTPair typ_desc list) f m = Some (s, n) \<longrightarrow> wf_fd_pair (DTPair typ_desc list) \<longrightarrow> length bs = size_td_pair (DTPair typ_desc list) \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair (DTPair typ_desc list) v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) proof (prove)
goal (3 subgoals):
 1. \<And>typ_struct bs. \<lbrakk>wf_fd_struct typ_struct; length bs = size_td_struct typ_struct; \<not> length (access_ti_struct typ_struct v bs) \<le> size_td_struct typ_struct\<rbrakk> \<Longrightarrow> False
 2. \<And>dt_pair list. \<lbrakk>\<forall>s m n f bs. field_lookup_pair dt_pair f m = Some (s, n) \<longrightarrow> wf_fd_pair dt_pair \<longrightarrow> length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)); \<forall>s m n f bs. field_lookup_list list f m = Some (s, n) \<longrightarrow> wf_fd_list list \<longrightarrow> length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))\<rbrakk> \<Longrightarrow> \<forall>s m n f bs. field_lookup_list (dt_pair # list) f m = Some (s, n) \<longrightarrow> wf_fd_list (dt_pair # list) \<longrightarrow> length bs = size_td_list (dt_pair # list) \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list (dt_pair # list) v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))
 3. \<And>typ_desc list. \<forall>s m n f bs. field_lookup typ_desc f m = Some (s, n) \<longrightarrow> wf_fd typ_desc \<longrightarrow> length bs = size_td typ_desc \<longrightarrow> take (size_td s) (drop (n - m) (access_ti typ_desc v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) \<Longrightarrow> \<forall>s m n f bs. field_lookup_pair (DTPair typ_desc list) f m = Some (s, n) \<longrightarrow> wf_fd_pair (DTPair typ_desc list) \<longrightarrow> length bs = size_td_pair (DTPair typ_desc list) \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair (DTPair typ_desc list) v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) proof (prove)
goal (3 subgoals):
 1. \<And>typ_struct bs. \<lbrakk>length bs = size_td_struct typ_struct; \<not> length (access_ti_struct typ_struct v bs) \<le> size_td_struct typ_struct; fd_cons_struct typ_struct\<rbrakk> \<Longrightarrow> False
 2. \<And>dt_pair list. \<lbrakk>\<forall>s m n f bs. field_lookup_pair dt_pair f m = Some (s, n) \<longrightarrow> wf_fd_pair dt_pair \<longrightarrow> length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)); \<forall>s m n f bs. field_lookup_list list f m = Some (s, n) \<longrightarrow> wf_fd_list list \<longrightarrow> length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))\<rbrakk> \<Longrightarrow> \<forall>s m n f bs. field_lookup_list (dt_pair # list) f m = Some (s, n) \<longrightarrow> wf_fd_list (dt_pair # list) \<longrightarrow> length bs = size_td_list (dt_pair # list) \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list (dt_pair # list) v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))
 3. \<And>typ_desc list. \<forall>s m n f bs. field_lookup typ_desc f m = Some (s, n) \<longrightarrow> wf_fd typ_desc \<longrightarrow> length bs = size_td typ_desc \<longrightarrow> take (size_td s) (drop (n - m) (access_ti typ_desc v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) \<Longrightarrow> \<forall>s m n f bs. field_lookup_pair (DTPair typ_desc list) f m = Some (s, n) \<longrightarrow> wf_fd_pair (DTPair typ_desc list) \<longrightarrow> length bs = size_td_pair (DTPair typ_desc list) \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair (DTPair typ_desc list) v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) proof (prove)
goal (2 subgoals):
 1. \<And>dt_pair list. \<lbrakk>\<forall>s m n f bs. field_lookup_pair dt_pair f m = Some (s, n) \<longrightarrow> wf_fd_pair dt_pair \<longrightarrow> length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)); \<forall>s m n f bs. field_lookup_list list f m = Some (s, n) \<longrightarrow> wf_fd_list list \<longrightarrow> length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))\<rbrakk> \<Longrightarrow> \<forall>s m n f bs. field_lookup_list (dt_pair # list) f m = Some (s, n) \<longrightarrow> wf_fd_list (dt_pair # list) \<longrightarrow> length bs = size_td_list (dt_pair # list) \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list (dt_pair # list) v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))
 2. \<And>typ_desc list. \<forall>s m n f bs. field_lookup typ_desc f m = Some (s, n) \<longrightarrow> wf_fd typ_desc \<longrightarrow> length bs = size_td typ_desc \<longrightarrow> take (size_td s) (drop (n - m) (access_ti typ_desc v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) \<Longrightarrow> \<forall>s m n f bs. field_lookup_pair (DTPair typ_desc list) f m = Some (s, n) \<longrightarrow> wf_fd_pair (DTPair typ_desc list) \<longrightarrow> length bs = size_td_pair (DTPair typ_desc list) \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair (DTPair typ_desc list) v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) proof (prove)
goal (2 subgoals):
 1. \<And>dt_pair list. \<lbrakk>\<forall>s m n. (\<exists>f. field_lookup_pair dt_pair f m = Some (s, n)) \<longrightarrow> wf_fd_pair dt_pair \<longrightarrow> (\<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); \<forall>s m n. (\<exists>f. field_lookup_list list f m = Some (s, n)) \<longrightarrow> wf_fd_list list \<longrightarrow> (\<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)))\<rbrakk> \<Longrightarrow> \<forall>s m n. (\<exists>f. (case field_lookup_pair dt_pair f m of None \<Rightarrow> field_lookup_list list f (m + size_td (dt_fst dt_pair)) | Some x \<Rightarrow> Some x) = Some (s, n)) \<longrightarrow> wf_fd_pair dt_pair \<and> wf_fd_list list \<and> fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list) \<and> fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair) \<and> fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list) \<longrightarrow> (\<forall>bs. length bs = size_td_pair dt_pair + size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v (take (size_td_pair dt_pair) bs))) @ take (size_td s - (length (access_ti_pair dt_pair v (take (size_td_pair dt_pair) bs)) - (n - m))) (drop (n - (m + length (access_ti_pair dt_pair v (take (size_td_pair dt_pair) bs)))) (access_ti_list list v (drop (size_td_pair dt_pair) bs))) = access_ti s v (take (size_td s) (drop (n - m) bs)))
 2. \<And>typ_desc list. \<forall>s m n f bs. field_lookup typ_desc f m = Some (s, n) \<longrightarrow> wf_fd typ_desc \<longrightarrow> length bs = size_td typ_desc \<longrightarrow> take (size_td s) (drop (n - m) (access_ti typ_desc v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) \<Longrightarrow> \<forall>s m n f bs. field_lookup_pair (DTPair typ_desc list) f m = Some (s, n) \<longrightarrow> wf_fd_pair (DTPair typ_desc list) \<longrightarrow> length bs = size_td_pair (DTPair typ_desc list) \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair (DTPair typ_desc list) v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) proof (prove)
goal (2 subgoals):
 1. \<And>dt_pair list s m n f bs. \<lbrakk>\<forall>s m n. (\<exists>f. field_lookup_pair dt_pair f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); \<forall>s m n. (\<exists>f. field_lookup_list list f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); (case field_lookup_pair dt_pair f m of None \<Rightarrow> field_lookup_list list f (m + size_td (dt_fst dt_pair)) | Some x \<Rightarrow> Some x) = Some (s, n); wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list\<rbrakk> \<Longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v (take (size_td_pair dt_pair) bs))) @ take (size_td s - (length (access_ti_pair dt_pair v (take (size_td_pair dt_pair) bs)) - (n - m))) (drop (n - (m + length (access_ti_pair dt_pair v (take (size_td_pair dt_pair) bs)))) (access_ti_list list v (drop (size_td_pair dt_pair) bs))) = access_ti s v (take (size_td s) (drop (n - m) bs))
 2. \<And>typ_desc list. \<forall>s m n f bs. field_lookup typ_desc f m = Some (s, n) \<longrightarrow> wf_fd typ_desc \<longrightarrow> length bs = size_td typ_desc \<longrightarrow> take (size_td s) (drop (n - m) (access_ti typ_desc v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) \<Longrightarrow> \<forall>s m n f bs. field_lookup_pair (DTPair typ_desc list) f m = Some (s, n) \<longrightarrow> wf_fd_pair (DTPair typ_desc list) \<longrightarrow> length bs = size_td_pair (DTPair typ_desc list) \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair (DTPair typ_desc list) v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) proof (prove)
goal (2 subgoals):
 1. \<And>dt_pair list s m n f bs. \<lbrakk>\<forall>s m n. (\<exists>f. field_lookup_pair dt_pair f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); \<forall>s m n. (\<exists>f. field_lookup_list list f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); (case field_lookup_pair dt_pair f m of None \<Rightarrow> field_lookup_list list f (m + size_td (dt_fst dt_pair)) | Some x \<Rightarrow> Some x) = Some (s, n); wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_pair dt_pair\<rbrakk> \<Longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v (take (size_td_pair dt_pair) bs))) @ take (size_td s - (length (access_ti_pair dt_pair v (take (size_td_pair dt_pair) bs)) - (n - m))) (drop (n - (m + length (access_ti_pair dt_pair v (take (size_td_pair dt_pair) bs)))) (access_ti_list list v (drop (size_td_pair dt_pair) bs))) = access_ti s v (take (size_td s) (drop (n - m) bs))
 2. \<And>typ_desc list. \<forall>s m n f bs. field_lookup typ_desc f m = Some (s, n) \<longrightarrow> wf_fd typ_desc \<longrightarrow> length bs = size_td typ_desc \<longrightarrow> take (size_td s) (drop (n - m) (access_ti typ_desc v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) \<Longrightarrow> \<forall>s m n f bs. field_lookup_pair (DTPair typ_desc list) f m = Some (s, n) \<longrightarrow> wf_fd_pair (DTPair typ_desc list) \<longrightarrow> length bs = size_td_pair (DTPair typ_desc list) \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair (DTPair typ_desc list) v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) proof (prove)
goal (2 subgoals):
 1. \<And>dt_pair list s m n f bs. \<lbrakk>\<forall>s m n. (\<exists>f. field_lookup_pair dt_pair f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); \<forall>s m n. (\<exists>f. field_lookup_list list f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); (case field_lookup_pair dt_pair f m of None \<Rightarrow> field_lookup_list list f (m + size_td (dt_fst dt_pair)) | Some x \<Rightarrow> Some x) = Some (s, n); wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair\<rbrakk> \<Longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v (take (size_td_pair dt_pair) bs))) @ take (size_td s - (size_td_pair dt_pair - (n - m))) (drop (n - (m + size_td_pair dt_pair)) (access_ti_list list v (drop (size_td_pair dt_pair) bs))) = access_ti s v (take (size_td s) (drop (n - m) bs))
 2. \<And>typ_desc list. \<forall>s m n f bs. field_lookup typ_desc f m = Some (s, n) \<longrightarrow> wf_fd typ_desc \<longrightarrow> length bs = size_td typ_desc \<longrightarrow> take (size_td s) (drop (n - m) (access_ti typ_desc v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) \<Longrightarrow> \<forall>s m n f bs. field_lookup_pair (DTPair typ_desc list) f m = Some (s, n) \<longrightarrow> wf_fd_pair (DTPair typ_desc list) \<longrightarrow> length bs = size_td_pair (DTPair typ_desc list) \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair (DTPair typ_desc list) v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) proof (prove)
goal (3 subgoals):
 1. \<And>dt_pair list s m n f bs. \<lbrakk>wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_pair dt_pair f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); \<forall>s m n. (\<exists>f. field_lookup_list list f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); field_lookup_pair dt_pair f m = None; field_lookup_list list f (m + size_td (dt_fst dt_pair)) = Some (s, n)\<rbrakk> \<Longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v (take (size_td_pair dt_pair) bs))) @ take (size_td s - (size_td_pair dt_pair - (n - m))) (drop (n - (m + size_td_pair dt_pair)) (access_ti_list list v (drop (size_td_pair dt_pair) bs))) = access_ti s v (take (size_td s) (drop (n - m) bs))
 2. \<And>dt_pair list s m n f bs. \<lbrakk>wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_pair dt_pair f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); \<forall>s m n. (\<exists>f. field_lookup_list list f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); field_lookup_pair dt_pair f m = Some (s, n)\<rbrakk> \<Longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v (take (size_td_pair dt_pair) bs))) @ take (size_td s - (size_td_pair dt_pair - (n - m))) (drop (n - (m + size_td_pair dt_pair)) (access_ti_list list v (drop (size_td_pair dt_pair) bs))) = access_ti s v (take (size_td s) (drop (n - m) bs))
 3. \<And>typ_desc list. \<forall>s m n f bs. field_lookup typ_desc f m = Some (s, n) \<longrightarrow> wf_fd typ_desc \<longrightarrow> length bs = size_td typ_desc \<longrightarrow> take (size_td s) (drop (n - m) (access_ti typ_desc v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) \<Longrightarrow> \<forall>s m n f bs. field_lookup_pair (DTPair typ_desc list) f m = Some (s, n) \<longrightarrow> wf_fd_pair (DTPair typ_desc list) \<longrightarrow> length bs = size_td_pair (DTPair typ_desc list) \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair (DTPair typ_desc list) v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) proof (prove)
goal (4 subgoals):
 1. \<And>dt_pair list s m n f bs. \<lbrakk>wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_pair dt_pair f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); \<forall>s m n. (\<exists>f. field_lookup_list list f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); field_lookup_pair dt_pair f m = None; field_lookup_list list f (m + size_td (dt_fst dt_pair)) = Some (s, n)\<rbrakk> \<Longrightarrow> length (access_ti_pair dt_pair v (take (size_td_pair dt_pair) bs)) \<le> n - m
 2. \<And>dt_pair list s m n f bs. \<lbrakk>wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_pair dt_pair f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); \<forall>s m n. (\<exists>f. field_lookup_list list f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); field_lookup_pair dt_pair f m = None; field_lookup_list list f (m + size_td (dt_fst dt_pair)) = Some (s, n)\<rbrakk> \<Longrightarrow> take (size_td s) [] @ take (size_td s - (size_td_pair dt_pair - (n - m))) (drop (n - (m + size_td_pair dt_pair)) (access_ti_list list v (drop (size_td_pair dt_pair) bs))) = access_ti s v (take (size_td s) (drop (n - m) bs))
 3. \<And>dt_pair list s m n f bs. \<lbrakk>wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_pair dt_pair f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); \<forall>s m n. (\<exists>f. field_lookup_list list f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); field_lookup_pair dt_pair f m = Some (s, n)\<rbrakk> \<Longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v (take (size_td_pair dt_pair) bs))) @ take (size_td s - (size_td_pair dt_pair - (n - m))) (drop (n - (m + size_td_pair dt_pair)) (access_ti_list list v (drop (size_td_pair dt_pair) bs))) = access_ti s v (take (size_td s) (drop (n - m) bs))
 4. \<And>typ_desc list. \<forall>s m n f bs. field_lookup typ_desc f m = Some (s, n) \<longrightarrow> wf_fd typ_desc \<longrightarrow> length bs = size_td typ_desc \<longrightarrow> take (size_td s) (drop (n - m) (access_ti typ_desc v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) \<Longrightarrow> \<forall>s m n f bs. field_lookup_pair (DTPair typ_desc list) f m = Some (s, n) \<longrightarrow> wf_fd_pair (DTPair typ_desc list) \<longrightarrow> length bs = size_td_pair (DTPair typ_desc list) \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair (DTPair typ_desc list) v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) proof (prove)
goal (4 subgoals):
 1. \<And>dt_pair list s m n f bs. \<lbrakk>wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_pair dt_pair f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); \<forall>s m n. (\<exists>f. field_lookup_list list f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); field_lookup_pair dt_pair f m = None; field_lookup_list list f (m + size_td (dt_fst dt_pair)) = Some (s, n)\<rbrakk> \<Longrightarrow> size_td_pair dt_pair \<le> n - m
 2. \<And>dt_pair list s m n f bs. \<lbrakk>wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_pair dt_pair f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); \<forall>s m n. (\<exists>f. field_lookup_list list f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); field_lookup_pair dt_pair f m = None; field_lookup_list list f (m + size_td (dt_fst dt_pair)) = Some (s, n)\<rbrakk> \<Longrightarrow> take (size_td s) [] @ take (size_td s - (size_td_pair dt_pair - (n - m))) (drop (n - (m + size_td_pair dt_pair)) (access_ti_list list v (drop (size_td_pair dt_pair) bs))) = access_ti s v (take (size_td s) (drop (n - m) bs))
 3. \<And>dt_pair list s m n f bs. \<lbrakk>wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_pair dt_pair f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); \<forall>s m n. (\<exists>f. field_lookup_list list f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); field_lookup_pair dt_pair f m = Some (s, n)\<rbrakk> \<Longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v (take (size_td_pair dt_pair) bs))) @ take (size_td s - (size_td_pair dt_pair - (n - m))) (drop (n - (m + size_td_pair dt_pair)) (access_ti_list list v (drop (size_td_pair dt_pair) bs))) = access_ti s v (take (size_td s) (drop (n - m) bs))
 4. \<And>typ_desc list. \<forall>s m n f bs. field_lookup typ_desc f m = Some (s, n) \<longrightarrow> wf_fd typ_desc \<longrightarrow> length bs = size_td typ_desc \<longrightarrow> take (size_td s) (drop (n - m) (access_ti typ_desc v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) \<Longrightarrow> \<forall>s m n f bs. field_lookup_pair (DTPair typ_desc list) f m = Some (s, n) \<longrightarrow> wf_fd_pair (DTPair typ_desc list) \<longrightarrow> length bs = size_td_pair (DTPair typ_desc list) \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair (DTPair typ_desc list) v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) proof (prove)
goal (4 subgoals):
 1. \<And>dt_pair list m n f bs. \<lbrakk>wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_pair dt_pair f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); \<forall>s m n. (\<exists>f. field_lookup_list list f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); field_lookup_pair dt_pair f m = None; m + size_td (dt_fst dt_pair) \<le> n\<rbrakk> \<Longrightarrow> size_td_pair dt_pair \<le> n - m
 2. \<And>dt_pair list s m n f bs. \<lbrakk>wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_pair dt_pair f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); \<forall>s m n. (\<exists>f. field_lookup_list list f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); field_lookup_pair dt_pair f m = None; field_lookup_list list f (m + size_td (dt_fst dt_pair)) = Some (s, n)\<rbrakk> \<Longrightarrow> take (size_td s) [] @ take (size_td s - (size_td_pair dt_pair - (n - m))) (drop (n - (m + size_td_pair dt_pair)) (access_ti_list list v (drop (size_td_pair dt_pair) bs))) = access_ti s v (take (size_td s) (drop (n - m) bs))
 3. \<And>dt_pair list s m n f bs. \<lbrakk>wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_pair dt_pair f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); \<forall>s m n. (\<exists>f. field_lookup_list list f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); field_lookup_pair dt_pair f m = Some (s, n)\<rbrakk> \<Longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v (take (size_td_pair dt_pair) bs))) @ take (size_td s - (size_td_pair dt_pair - (n - m))) (drop (n - (m + size_td_pair dt_pair)) (access_ti_list list v (drop (size_td_pair dt_pair) bs))) = access_ti s v (take (size_td s) (drop (n - m) bs))
 4. \<And>typ_desc list. \<forall>s m n f bs. field_lookup typ_desc f m = Some (s, n) \<longrightarrow> wf_fd typ_desc \<longrightarrow> length bs = size_td typ_desc \<longrightarrow> take (size_td s) (drop (n - m) (access_ti typ_desc v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) \<Longrightarrow> \<forall>s m n f bs. field_lookup_pair (DTPair typ_desc list) f m = Some (s, n) \<longrightarrow> wf_fd_pair (DTPair typ_desc list) \<longrightarrow> length bs = size_td_pair (DTPair typ_desc list) \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair (DTPair typ_desc list) v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) proof (prove)
goal (4 subgoals):
 1. \<And>dt_pair list m n f bs x1 x2. \<lbrakk>wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_pair dt_pair f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); \<forall>s m n. (\<exists>f. field_lookup_list list f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); field_lookup_pair dt_pair f m = None; m + size_td (dt_fst dt_pair) \<le> n; dt_pair = DTPair x1 x2\<rbrakk> \<Longrightarrow> size_td_pair dt_pair \<le> n - m
 2. \<And>dt_pair list s m n f bs. \<lbrakk>wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_pair dt_pair f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); \<forall>s m n. (\<exists>f. field_lookup_list list f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); field_lookup_pair dt_pair f m = None; field_lookup_list list f (m + size_td (dt_fst dt_pair)) = Some (s, n)\<rbrakk> \<Longrightarrow> take (size_td s) [] @ take (size_td s - (size_td_pair dt_pair - (n - m))) (drop (n - (m + size_td_pair dt_pair)) (access_ti_list list v (drop (size_td_pair dt_pair) bs))) = access_ti s v (take (size_td s) (drop (n - m) bs))
 3. \<And>dt_pair list s m n f bs. \<lbrakk>wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_pair dt_pair f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); \<forall>s m n. (\<exists>f. field_lookup_list list f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); field_lookup_pair dt_pair f m = Some (s, n)\<rbrakk> \<Longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v (take (size_td_pair dt_pair) bs))) @ take (size_td s - (size_td_pair dt_pair - (n - m))) (drop (n - (m + size_td_pair dt_pair)) (access_ti_list list v (drop (size_td_pair dt_pair) bs))) = access_ti s v (take (size_td s) (drop (n - m) bs))
 4. \<And>typ_desc list. \<forall>s m n f bs. field_lookup typ_desc f m = Some (s, n) \<longrightarrow> wf_fd typ_desc \<longrightarrow> length bs = size_td typ_desc \<longrightarrow> take (size_td s) (drop (n - m) (access_ti typ_desc v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) \<Longrightarrow> \<forall>s m n f bs. field_lookup_pair (DTPair typ_desc list) f m = Some (s, n) \<longrightarrow> wf_fd_pair (DTPair typ_desc list) \<longrightarrow> length bs = size_td_pair (DTPair typ_desc list) \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair (DTPair typ_desc list) v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) proof (prove)
goal (4 subgoals):
 1. \<And>list m n f bs x1 x2. \<lbrakk>wf_fd x1; wf_fd_list list; fu_commutes (update_ti_t x1) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti x1, field_update = update_ti_t x1\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td x1); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti x1, field_update = update_ti_t x1\<rparr> (size_td x1) (size_td_list list); length bs = size_td x1 + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti x1, field_update = update_ti_t x1\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti x1, field_update = update_ti_t x1\<rparr> (size_td x1); fd_cons_access_update \<lparr>field_access = access_ti x1, field_update = update_ti_t x1\<rparr> (size_td x1); \<forall>v bs. length bs = size_td x1 \<longrightarrow> length (access_ti x1 v bs) = size_td x1; \<forall>s m n. (\<exists>f. (if x2 = hd f \<and> f \<noteq> [] then field_lookup x1 (tl f) m else None) = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td x1 \<longrightarrow> take (size_td s) (drop (n - m) (access_ti x1 v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); \<forall>s m n. (\<exists>f. field_lookup_list list f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); (if x2 = hd f \<and> f \<noteq> [] then field_lookup x1 (tl f) m else None) = None; m + size_td x1 \<le> n\<rbrakk> \<Longrightarrow> size_td x1 \<le> n - m
 2. \<And>dt_pair list s m n f bs. \<lbrakk>wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_pair dt_pair f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); \<forall>s m n. (\<exists>f. field_lookup_list list f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); field_lookup_pair dt_pair f m = None; field_lookup_list list f (m + size_td (dt_fst dt_pair)) = Some (s, n)\<rbrakk> \<Longrightarrow> take (size_td s) [] @ take (size_td s - (size_td_pair dt_pair - (n - m))) (drop (n - (m + size_td_pair dt_pair)) (access_ti_list list v (drop (size_td_pair dt_pair) bs))) = access_ti s v (take (size_td s) (drop (n - m) bs))
 3. \<And>dt_pair list s m n f bs. \<lbrakk>wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_pair dt_pair f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); \<forall>s m n. (\<exists>f. field_lookup_list list f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); field_lookup_pair dt_pair f m = Some (s, n)\<rbrakk> \<Longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v (take (size_td_pair dt_pair) bs))) @ take (size_td s - (size_td_pair dt_pair - (n - m))) (drop (n - (m + size_td_pair dt_pair)) (access_ti_list list v (drop (size_td_pair dt_pair) bs))) = access_ti s v (take (size_td s) (drop (n - m) bs))
 4. \<And>typ_desc list. \<forall>s m n f bs. field_lookup typ_desc f m = Some (s, n) \<longrightarrow> wf_fd typ_desc \<longrightarrow> length bs = size_td typ_desc \<longrightarrow> take (size_td s) (drop (n - m) (access_ti typ_desc v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) \<Longrightarrow> \<forall>s m n f bs. field_lookup_pair (DTPair typ_desc list) f m = Some (s, n) \<longrightarrow> wf_fd_pair (DTPair typ_desc list) \<longrightarrow> length bs = size_td_pair (DTPair typ_desc list) \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair (DTPair typ_desc list) v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) proof (prove)
goal (3 subgoals):
 1. \<And>dt_pair list s m n f bs. \<lbrakk>wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_pair dt_pair f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); \<forall>s m n. (\<exists>f. field_lookup_list list f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); field_lookup_pair dt_pair f m = None; field_lookup_list list f (m + size_td (dt_fst dt_pair)) = Some (s, n)\<rbrakk> \<Longrightarrow> take (size_td s) [] @ take (size_td s - (size_td_pair dt_pair - (n - m))) (drop (n - (m + size_td_pair dt_pair)) (access_ti_list list v (drop (size_td_pair dt_pair) bs))) = access_ti s v (take (size_td s) (drop (n - m) bs))
 2. \<And>dt_pair list s m n f bs. \<lbrakk>wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_pair dt_pair f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); \<forall>s m n. (\<exists>f. field_lookup_list list f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); field_lookup_pair dt_pair f m = Some (s, n)\<rbrakk> \<Longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v (take (size_td_pair dt_pair) bs))) @ take (size_td s - (size_td_pair dt_pair - (n - m))) (drop (n - (m + size_td_pair dt_pair)) (access_ti_list list v (drop (size_td_pair dt_pair) bs))) = access_ti s v (take (size_td s) (drop (n - m) bs))
 3. \<And>typ_desc list. \<forall>s m n f bs. field_lookup typ_desc f m = Some (s, n) \<longrightarrow> wf_fd typ_desc \<longrightarrow> length bs = size_td typ_desc \<longrightarrow> take (size_td s) (drop (n - m) (access_ti typ_desc v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) \<Longrightarrow> \<forall>s m n f bs. field_lookup_pair (DTPair typ_desc list) f m = Some (s, n) \<longrightarrow> wf_fd_pair (DTPair typ_desc list) \<longrightarrow> length bs = size_td_pair (DTPair typ_desc list) \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair (DTPair typ_desc list) v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) proof (prove)
goal (3 subgoals):
 1. \<And>dt_pair list s m n f bs. \<lbrakk>wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_pair dt_pair f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); \<forall>s m n. (\<exists>f. field_lookup_list list f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); field_lookup_pair dt_pair f m = None; field_lookup_list list f (m + size_td (dt_fst dt_pair)) = Some (s, n)\<rbrakk> \<Longrightarrow> take (size_td s - (size_td_pair dt_pair - (n - m))) (drop (n - (m + size_td_pair dt_pair)) (access_ti_list list v (drop (size_td_pair dt_pair) bs))) = access_ti s v (take (size_td s) (drop (n - m) bs))
 2. \<And>dt_pair list s m n f bs. \<lbrakk>wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_pair dt_pair f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); \<forall>s m n. (\<exists>f. field_lookup_list list f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); field_lookup_pair dt_pair f m = Some (s, n)\<rbrakk> \<Longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v (take (size_td_pair dt_pair) bs))) @ take (size_td s - (size_td_pair dt_pair - (n - m))) (drop (n - (m + size_td_pair dt_pair)) (access_ti_list list v (drop (size_td_pair dt_pair) bs))) = access_ti s v (take (size_td s) (drop (n - m) bs))
 3. \<And>typ_desc list. \<forall>s m n f bs. field_lookup typ_desc f m = Some (s, n) \<longrightarrow> wf_fd typ_desc \<longrightarrow> length bs = size_td typ_desc \<longrightarrow> take (size_td s) (drop (n - m) (access_ti typ_desc v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) \<Longrightarrow> \<forall>s m n f bs. field_lookup_pair (DTPair typ_desc list) f m = Some (s, n) \<longrightarrow> wf_fd_pair (DTPair typ_desc list) \<longrightarrow> length bs = size_td_pair (DTPair typ_desc list) \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair (DTPair typ_desc list) v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) proof (prove)
goal (3 subgoals):
 1. \<And>dt_pair list s m n f bs. \<lbrakk>\<forall>s m n. (\<exists>f. field_lookup_list list f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); field_lookup_pair dt_pair f m = None; field_lookup_list list f (m + size_td (dt_fst dt_pair)) = Some (s, n); wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_pair dt_pair f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)))\<rbrakk> \<Longrightarrow> take (size_td s - (size_td_pair dt_pair - (n - m))) (drop (n - (m + size_td_pair dt_pair)) (access_ti_list list v (drop (size_td_pair dt_pair) bs))) = access_ti s v (take (size_td s) (drop (n - m) bs))
 2. \<And>dt_pair list s m n f bs. \<lbrakk>wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_pair dt_pair f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); \<forall>s m n. (\<exists>f. field_lookup_list list f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); field_lookup_pair dt_pair f m = Some (s, n)\<rbrakk> \<Longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v (take (size_td_pair dt_pair) bs))) @ take (size_td s - (size_td_pair dt_pair - (n - m))) (drop (n - (m + size_td_pair dt_pair)) (access_ti_list list v (drop (size_td_pair dt_pair) bs))) = access_ti s v (take (size_td s) (drop (n - m) bs))
 3. \<And>typ_desc list. \<forall>s m n f bs. field_lookup typ_desc f m = Some (s, n) \<longrightarrow> wf_fd typ_desc \<longrightarrow> length bs = size_td typ_desc \<longrightarrow> take (size_td s) (drop (n - m) (access_ti typ_desc v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) \<Longrightarrow> \<forall>s m n f bs. field_lookup_pair (DTPair typ_desc list) f m = Some (s, n) \<longrightarrow> wf_fd_pair (DTPair typ_desc list) \<longrightarrow> length bs = size_td_pair (DTPair typ_desc list) \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair (DTPair typ_desc list) v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) proof (prove)
goal (3 subgoals):
 1. \<And>dt_pair list s m n f bs. \<lbrakk>field_lookup_pair dt_pair f m = None; field_lookup_list list f (m + size_td (dt_fst dt_pair)) = Some (s, n); wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_pair dt_pair f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); \<forall>m n. (\<exists>f. field_lookup_list list f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)))\<rbrakk> \<Longrightarrow> take (size_td s - (size_td_pair dt_pair - (n - m))) (drop (n - (m + size_td_pair dt_pair)) (access_ti_list list v (drop (size_td_pair dt_pair) bs))) = access_ti s v (take (size_td s) (drop (n - m) bs))
 2. \<And>dt_pair list s m n f bs. \<lbrakk>wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_pair dt_pair f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); \<forall>s m n. (\<exists>f. field_lookup_list list f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); field_lookup_pair dt_pair f m = Some (s, n)\<rbrakk> \<Longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v (take (size_td_pair dt_pair) bs))) @ take (size_td s - (size_td_pair dt_pair - (n - m))) (drop (n - (m + size_td_pair dt_pair)) (access_ti_list list v (drop (size_td_pair dt_pair) bs))) = access_ti s v (take (size_td s) (drop (n - m) bs))
 3. \<And>typ_desc list. \<forall>s m n f bs. field_lookup typ_desc f m = Some (s, n) \<longrightarrow> wf_fd typ_desc \<longrightarrow> length bs = size_td typ_desc \<longrightarrow> take (size_td s) (drop (n - m) (access_ti typ_desc v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) \<Longrightarrow> \<forall>s m n f bs. field_lookup_pair (DTPair typ_desc list) f m = Some (s, n) \<longrightarrow> wf_fd_pair (DTPair typ_desc list) \<longrightarrow> length bs = size_td_pair (DTPair typ_desc list) \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair (DTPair typ_desc list) v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) proof (prove)
goal (3 subgoals):
 1. \<And>dt_pair list s m n f bs. \<lbrakk>field_lookup_pair dt_pair f m = None; field_lookup_list list f (m + size_td (dt_fst dt_pair)) = Some (s, n); wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_pair dt_pair f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); \<forall>n. (\<exists>f. field_lookup_list list f (m + size_td (dt_fst dt_pair)) = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - (m + size_td (dt_fst dt_pair))) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - (m + size_td (dt_fst dt_pair))) bs)))\<rbrakk> \<Longrightarrow> take (size_td s - (size_td_pair dt_pair - (n - m))) (drop (n - (m + size_td_pair dt_pair)) (access_ti_list list v (drop (size_td_pair dt_pair) bs))) = access_ti s v (take (size_td s) (drop (n - m) bs))
 2. \<And>dt_pair list s m n f bs. \<lbrakk>wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_pair dt_pair f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); \<forall>s m n. (\<exists>f. field_lookup_list list f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); field_lookup_pair dt_pair f m = Some (s, n)\<rbrakk> \<Longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v (take (size_td_pair dt_pair) bs))) @ take (size_td s - (size_td_pair dt_pair - (n - m))) (drop (n - (m + size_td_pair dt_pair)) (access_ti_list list v (drop (size_td_pair dt_pair) bs))) = access_ti s v (take (size_td s) (drop (n - m) bs))
 3. \<And>typ_desc list. \<forall>s m n f bs. field_lookup typ_desc f m = Some (s, n) \<longrightarrow> wf_fd typ_desc \<longrightarrow> length bs = size_td typ_desc \<longrightarrow> take (size_td s) (drop (n - m) (access_ti typ_desc v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) \<Longrightarrow> \<forall>s m n f bs. field_lookup_pair (DTPair typ_desc list) f m = Some (s, n) \<longrightarrow> wf_fd_pair (DTPair typ_desc list) \<longrightarrow> length bs = size_td_pair (DTPair typ_desc list) \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair (DTPair typ_desc list) v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) proof (prove)
goal (3 subgoals):
 1. \<And>dt_pair list s m n f bs. \<lbrakk>field_lookup_pair dt_pair f m = None; field_lookup_list list f (m + size_td (dt_fst dt_pair)) = Some (s, n); wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_pair dt_pair f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); (\<exists>f. field_lookup_list list f (m + size_td (dt_fst dt_pair)) = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - (m + size_td (dt_fst dt_pair))) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - (m + size_td (dt_fst dt_pair))) bs)))\<rbrakk> \<Longrightarrow> take (size_td s - (size_td_pair dt_pair - (n - m))) (drop (n - (m + size_td_pair dt_pair)) (access_ti_list list v (drop (size_td_pair dt_pair) bs))) = access_ti s v (take (size_td s) (drop (n - m) bs))
 2. \<And>dt_pair list s m n f bs. \<lbrakk>wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_pair dt_pair f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); \<forall>s m n. (\<exists>f. field_lookup_list list f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); field_lookup_pair dt_pair f m = Some (s, n)\<rbrakk> \<Longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v (take (size_td_pair dt_pair) bs))) @ take (size_td s - (size_td_pair dt_pair - (n - m))) (drop (n - (m + size_td_pair dt_pair)) (access_ti_list list v (drop (size_td_pair dt_pair) bs))) = access_ti s v (take (size_td s) (drop (n - m) bs))
 3. \<And>typ_desc list. \<forall>s m n f bs. field_lookup typ_desc f m = Some (s, n) \<longrightarrow> wf_fd typ_desc \<longrightarrow> length bs = size_td typ_desc \<longrightarrow> take (size_td s) (drop (n - m) (access_ti typ_desc v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) \<Longrightarrow> \<forall>s m n f bs. field_lookup_pair (DTPair typ_desc list) f m = Some (s, n) \<longrightarrow> wf_fd_pair (DTPair typ_desc list) \<longrightarrow> length bs = size_td_pair (DTPair typ_desc list) \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair (DTPair typ_desc list) v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) proof (prove)
goal (4 subgoals):
 1. \<And>dt_pair list s m n f bs. \<lbrakk>field_lookup_pair dt_pair f m = None; field_lookup_list list f (m + size_td (dt_fst dt_pair)) = Some (s, n); wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_pair dt_pair f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)))\<rbrakk> \<Longrightarrow> \<exists>f. field_lookup_list list f (m + size_td (dt_fst dt_pair)) = Some (s, n)
 2. \<And>dt_pair list s m n f bs. \<lbrakk>field_lookup_pair dt_pair f m = None; field_lookup_list list f (m + size_td (dt_fst dt_pair)) = Some (s, n); wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_pair dt_pair f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); \<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - (m + size_td (dt_fst dt_pair))) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - (m + size_td (dt_fst dt_pair))) bs))\<rbrakk> \<Longrightarrow> take (size_td s - (size_td_pair dt_pair - (n - m))) (drop (n - (m + size_td_pair dt_pair)) (access_ti_list list v (drop (size_td_pair dt_pair) bs))) = access_ti s v (take (size_td s) (drop (n - m) bs))
 3. \<And>dt_pair list s m n f bs. \<lbrakk>wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_pair dt_pair f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); \<forall>s m n. (\<exists>f. field_lookup_list list f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); field_lookup_pair dt_pair f m = Some (s, n)\<rbrakk> \<Longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v (take (size_td_pair dt_pair) bs))) @ take (size_td s - (size_td_pair dt_pair - (n - m))) (drop (n - (m + size_td_pair dt_pair)) (access_ti_list list v (drop (size_td_pair dt_pair) bs))) = access_ti s v (take (size_td s) (drop (n - m) bs))
 4. \<And>typ_desc list. \<forall>s m n f bs. field_lookup typ_desc f m = Some (s, n) \<longrightarrow> wf_fd typ_desc \<longrightarrow> length bs = size_td typ_desc \<longrightarrow> take (size_td s) (drop (n - m) (access_ti typ_desc v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) \<Longrightarrow> \<forall>s m n f bs. field_lookup_pair (DTPair typ_desc list) f m = Some (s, n) \<longrightarrow> wf_fd_pair (DTPair typ_desc list) \<longrightarrow> length bs = size_td_pair (DTPair typ_desc list) \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair (DTPair typ_desc list) v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) proof (prove)
goal (3 subgoals):
 1. \<And>dt_pair list s m n f bs. \<lbrakk>field_lookup_pair dt_pair f m = None; field_lookup_list list f (m + size_td (dt_fst dt_pair)) = Some (s, n); wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_pair dt_pair f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); \<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - (m + size_td (dt_fst dt_pair))) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - (m + size_td (dt_fst dt_pair))) bs))\<rbrakk> \<Longrightarrow> take (size_td s - (size_td_pair dt_pair - (n - m))) (drop (n - (m + size_td_pair dt_pair)) (access_ti_list list v (drop (size_td_pair dt_pair) bs))) = access_ti s v (take (size_td s) (drop (n - m) bs))
 2. \<And>dt_pair list s m n f bs. \<lbrakk>wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_pair dt_pair f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); \<forall>s m n. (\<exists>f. field_lookup_list list f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); field_lookup_pair dt_pair f m = Some (s, n)\<rbrakk> \<Longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v (take (size_td_pair dt_pair) bs))) @ take (size_td s - (size_td_pair dt_pair - (n - m))) (drop (n - (m + size_td_pair dt_pair)) (access_ti_list list v (drop (size_td_pair dt_pair) bs))) = access_ti s v (take (size_td s) (drop (n - m) bs))
 3. \<And>typ_desc list. \<forall>s m n f bs. field_lookup typ_desc f m = Some (s, n) \<longrightarrow> wf_fd typ_desc \<longrightarrow> length bs = size_td typ_desc \<longrightarrow> take (size_td s) (drop (n - m) (access_ti typ_desc v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) \<Longrightarrow> \<forall>s m n f bs. field_lookup_pair (DTPair typ_desc list) f m = Some (s, n) \<longrightarrow> wf_fd_pair (DTPair typ_desc list) \<longrightarrow> length bs = size_td_pair (DTPair typ_desc list) \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair (DTPair typ_desc list) v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) proof (prove)
goal (4 subgoals):
 1. \<And>dt_pair list s m n f bs. \<lbrakk>field_lookup_pair dt_pair f m = None; field_lookup_list list f (m + size_td (dt_fst dt_pair)) = Some (s, n); wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_pair dt_pair f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); \<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - (m + size_td (dt_fst dt_pair))) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - (m + size_td (dt_fst dt_pair))) bs)); size_td_pair dt_pair - (n - m) = 0\<rbrakk> \<Longrightarrow> take (size_td s - (size_td_pair dt_pair - (n - m))) (drop (n - (m + size_td_pair dt_pair)) (access_ti_list list v (drop (size_td_pair dt_pair) bs))) = access_ti s v (take (size_td s) (drop (n - m) bs))
 2. \<And>dt_pair list s m n f bs. \<lbrakk>field_lookup_pair dt_pair f m = None; field_lookup_list list f (m + size_td (dt_fst dt_pair)) = Some (s, n); wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_pair dt_pair f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); \<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - (m + size_td (dt_fst dt_pair))) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - (m + size_td (dt_fst dt_pair))) bs))\<rbrakk> \<Longrightarrow> size_td_pair dt_pair - (n - m) = 0
 3. \<And>dt_pair list s m n f bs. \<lbrakk>wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_pair dt_pair f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); \<forall>s m n. (\<exists>f. field_lookup_list list f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); field_lookup_pair dt_pair f m = Some (s, n)\<rbrakk> \<Longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v (take (size_td_pair dt_pair) bs))) @ take (size_td s - (size_td_pair dt_pair - (n - m))) (drop (n - (m + size_td_pair dt_pair)) (access_ti_list list v (drop (size_td_pair dt_pair) bs))) = access_ti s v (take (size_td s) (drop (n - m) bs))
 4. \<And>typ_desc list. \<forall>s m n f bs. field_lookup typ_desc f m = Some (s, n) \<longrightarrow> wf_fd typ_desc \<longrightarrow> length bs = size_td typ_desc \<longrightarrow> take (size_td s) (drop (n - m) (access_ti typ_desc v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) \<Longrightarrow> \<forall>s m n f bs. field_lookup_pair (DTPair typ_desc list) f m = Some (s, n) \<longrightarrow> wf_fd_pair (DTPair typ_desc list) \<longrightarrow> length bs = size_td_pair (DTPair typ_desc list) \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair (DTPair typ_desc list) v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) proof (prove)
goal (4 subgoals):
 1. \<And>dt_pair list s m n f bs. \<lbrakk>field_lookup_pair dt_pair f m = None; field_lookup_list list f (m + size_td (dt_fst dt_pair)) = Some (s, n); wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_pair dt_pair f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); \<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - (m + size_td (dt_fst dt_pair))) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - (m + size_td (dt_fst dt_pair))) bs)); size_td_pair dt_pair \<le> n - m\<rbrakk> \<Longrightarrow> take (size_td s) (drop (n - (m + size_td_pair dt_pair)) (access_ti_list list v (drop (size_td_pair dt_pair) bs))) = access_ti s v (take (size_td s) (drop (n - m) bs))
 2. \<And>dt_pair list s m n f bs. \<lbrakk>field_lookup_pair dt_pair f m = None; field_lookup_list list f (m + size_td (dt_fst dt_pair)) = Some (s, n); wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_pair dt_pair f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); \<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - (m + size_td (dt_fst dt_pair))) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - (m + size_td (dt_fst dt_pair))) bs))\<rbrakk> \<Longrightarrow> size_td_pair dt_pair - (n - m) = 0
 3. \<And>dt_pair list s m n f bs. \<lbrakk>wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_pair dt_pair f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); \<forall>s m n. (\<exists>f. field_lookup_list list f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); field_lookup_pair dt_pair f m = Some (s, n)\<rbrakk> \<Longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v (take (size_td_pair dt_pair) bs))) @ take (size_td s - (size_td_pair dt_pair - (n - m))) (drop (n - (m + size_td_pair dt_pair)) (access_ti_list list v (drop (size_td_pair dt_pair) bs))) = access_ti s v (take (size_td s) (drop (n - m) bs))
 4. \<And>typ_desc list. \<forall>s m n f bs. field_lookup typ_desc f m = Some (s, n) \<longrightarrow> wf_fd typ_desc \<longrightarrow> length bs = size_td typ_desc \<longrightarrow> take (size_td s) (drop (n - m) (access_ti typ_desc v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) \<Longrightarrow> \<forall>s m n f bs. field_lookup_pair (DTPair typ_desc list) f m = Some (s, n) \<longrightarrow> wf_fd_pair (DTPair typ_desc list) \<longrightarrow> length bs = size_td_pair (DTPair typ_desc list) \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair (DTPair typ_desc list) v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) proof (prove)
goal (4 subgoals):
 1. \<And>dt_pair list s m n f bs x1 x2. \<lbrakk>(if x2 = hd f \<and> f \<noteq> [] then field_lookup x1 (tl f) m else None) = None; field_lookup_list list f (m + size_td x1) = Some (s, n); wf_fd x1; wf_fd_list list; fu_commutes (update_ti_t x1) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti x1, field_update = update_ti_t x1\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td x1); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti x1, field_update = update_ti_t x1\<rparr> (size_td x1) (size_td_list list); length bs = size_td x1 + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti x1, field_update = update_ti_t x1\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti x1, field_update = update_ti_t x1\<rparr> (size_td x1); fd_cons_access_update \<lparr>field_access = access_ti x1, field_update = update_ti_t x1\<rparr> (size_td x1); \<forall>v bs. length bs = size_td x1 \<longrightarrow> length (access_ti x1 v bs) = size_td x1; \<forall>s m n. (\<exists>f. (if x2 = hd f \<and> f \<noteq> [] then field_lookup x1 (tl f) m else None) = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td x1 \<longrightarrow> take (size_td s) (drop (n - m) (access_ti x1 v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); \<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - (m + size_td x1)) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - (m + size_td x1)) bs)); size_td x1 \<le> n - m; dt_pair = DTPair x1 x2\<rbrakk> \<Longrightarrow> access_ti s v (take (size_td s) (drop (n - (m + size_td x1) + size_td x1) bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))
 2. \<And>dt_pair list s m n f bs. \<lbrakk>field_lookup_pair dt_pair f m = None; field_lookup_list list f (m + size_td (dt_fst dt_pair)) = Some (s, n); wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_pair dt_pair f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); \<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - (m + size_td (dt_fst dt_pair))) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - (m + size_td (dt_fst dt_pair))) bs))\<rbrakk> \<Longrightarrow> size_td_pair dt_pair - (n - m) = 0
 3. \<And>dt_pair list s m n f bs. \<lbrakk>wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_pair dt_pair f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); \<forall>s m n. (\<exists>f. field_lookup_list list f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); field_lookup_pair dt_pair f m = Some (s, n)\<rbrakk> \<Longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v (take (size_td_pair dt_pair) bs))) @ take (size_td s - (size_td_pair dt_pair - (n - m))) (drop (n - (m + size_td_pair dt_pair)) (access_ti_list list v (drop (size_td_pair dt_pair) bs))) = access_ti s v (take (size_td s) (drop (n - m) bs))
 4. \<And>typ_desc list. \<forall>s m n f bs. field_lookup typ_desc f m = Some (s, n) \<longrightarrow> wf_fd typ_desc \<longrightarrow> length bs = size_td typ_desc \<longrightarrow> take (size_td s) (drop (n - m) (access_ti typ_desc v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) \<Longrightarrow> \<forall>s m n f bs. field_lookup_pair (DTPair typ_desc list) f m = Some (s, n) \<longrightarrow> wf_fd_pair (DTPair typ_desc list) \<longrightarrow> length bs = size_td_pair (DTPair typ_desc list) \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair (DTPair typ_desc list) v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) proof (prove)
goal (3 subgoals):
 1. \<And>dt_pair list s m n f bs. \<lbrakk>field_lookup_pair dt_pair f m = None; field_lookup_list list f (m + size_td (dt_fst dt_pair)) = Some (s, n); wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_pair dt_pair f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); \<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - (m + size_td (dt_fst dt_pair))) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - (m + size_td (dt_fst dt_pair))) bs))\<rbrakk> \<Longrightarrow> size_td_pair dt_pair - (n - m) = 0
 2. \<And>dt_pair list s m n f bs. \<lbrakk>wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_pair dt_pair f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); \<forall>s m n. (\<exists>f. field_lookup_list list f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); field_lookup_pair dt_pair f m = Some (s, n)\<rbrakk> \<Longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v (take (size_td_pair dt_pair) bs))) @ take (size_td s - (size_td_pair dt_pair - (n - m))) (drop (n - (m + size_td_pair dt_pair)) (access_ti_list list v (drop (size_td_pair dt_pair) bs))) = access_ti s v (take (size_td s) (drop (n - m) bs))
 3. \<And>typ_desc list. \<forall>s m n f bs. field_lookup typ_desc f m = Some (s, n) \<longrightarrow> wf_fd typ_desc \<longrightarrow> length bs = size_td typ_desc \<longrightarrow> take (size_td s) (drop (n - m) (access_ti typ_desc v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) \<Longrightarrow> \<forall>s m n f bs. field_lookup_pair (DTPair typ_desc list) f m = Some (s, n) \<longrightarrow> wf_fd_pair (DTPair typ_desc list) \<longrightarrow> length bs = size_td_pair (DTPair typ_desc list) \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair (DTPair typ_desc list) v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) proof (prove)
goal (3 subgoals):
 1. \<And>dt_pair list s m n f bs x1 x2. \<lbrakk>(if x2 = hd f \<and> f \<noteq> [] then field_lookup x1 (tl f) m else None) = None; field_lookup_list list f (m + size_td x1) = Some (s, n); wf_fd x1; wf_fd_list list; fu_commutes (update_ti_t x1) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti x1, field_update = update_ti_t x1\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td x1); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti x1, field_update = update_ti_t x1\<rparr> (size_td x1) (size_td_list list); length bs = size_td x1 + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti x1, field_update = update_ti_t x1\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti x1, field_update = update_ti_t x1\<rparr> (size_td x1); fd_cons_access_update \<lparr>field_access = access_ti x1, field_update = update_ti_t x1\<rparr> (size_td x1); \<forall>v bs. length bs = size_td x1 \<longrightarrow> length (access_ti x1 v bs) = size_td x1; \<forall>s m n. (\<exists>f. (if x2 = hd f \<and> f \<noteq> [] then field_lookup x1 (tl f) m else None) = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td x1 \<longrightarrow> take (size_td s) (drop (n - m) (access_ti x1 v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); \<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - (m + size_td x1)) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - (m + size_td x1)) bs)); dt_pair = DTPair x1 x2\<rbrakk> \<Longrightarrow> size_td x1 \<le> n - m
 2. \<And>dt_pair list s m n f bs. \<lbrakk>wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_pair dt_pair f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); \<forall>s m n. (\<exists>f. field_lookup_list list f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); field_lookup_pair dt_pair f m = Some (s, n)\<rbrakk> \<Longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v (take (size_td_pair dt_pair) bs))) @ take (size_td s - (size_td_pair dt_pair - (n - m))) (drop (n - (m + size_td_pair dt_pair)) (access_ti_list list v (drop (size_td_pair dt_pair) bs))) = access_ti s v (take (size_td s) (drop (n - m) bs))
 3. \<And>typ_desc list. \<forall>s m n f bs. field_lookup typ_desc f m = Some (s, n) \<longrightarrow> wf_fd typ_desc \<longrightarrow> length bs = size_td typ_desc \<longrightarrow> take (size_td s) (drop (n - m) (access_ti typ_desc v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) \<Longrightarrow> \<forall>s m n f bs. field_lookup_pair (DTPair typ_desc list) f m = Some (s, n) \<longrightarrow> wf_fd_pair (DTPair typ_desc list) \<longrightarrow> length bs = size_td_pair (DTPair typ_desc list) \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair (DTPair typ_desc list) v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) proof (prove)
goal (3 subgoals):
 1. \<And>list s m n f bs x1 x2. \<lbrakk>(if x2 = hd f \<and> f \<noteq> [] then field_lookup x1 (tl f) m else None) = None; wf_fd x1; wf_fd_list list; fu_commutes (update_ti_t x1) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti x1, field_update = update_ti_t x1\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td x1); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti x1, field_update = update_ti_t x1\<rparr> (size_td x1) (size_td_list list); length bs = size_td x1 + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti x1, field_update = update_ti_t x1\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti x1, field_update = update_ti_t x1\<rparr> (size_td x1); fd_cons_access_update \<lparr>field_access = access_ti x1, field_update = update_ti_t x1\<rparr> (size_td x1); \<forall>v bs. length bs = size_td x1 \<longrightarrow> length (access_ti x1 v bs) = size_td x1; \<forall>s m n. (\<exists>f. (if x2 = hd f \<and> f \<noteq> [] then field_lookup x1 (tl f) m else None) = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td x1 \<longrightarrow> take (size_td s) (drop (n - m) (access_ti x1 v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); \<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - (m + size_td x1)) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - (m + size_td x1)) bs)); m + size_td x1 \<le> n\<rbrakk> \<Longrightarrow> size_td x1 \<le> n - m
 2. \<And>dt_pair list s m n f bs. \<lbrakk>wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_pair dt_pair f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); \<forall>s m n. (\<exists>f. field_lookup_list list f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); field_lookup_pair dt_pair f m = Some (s, n)\<rbrakk> \<Longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v (take (size_td_pair dt_pair) bs))) @ take (size_td s - (size_td_pair dt_pair - (n - m))) (drop (n - (m + size_td_pair dt_pair)) (access_ti_list list v (drop (size_td_pair dt_pair) bs))) = access_ti s v (take (size_td s) (drop (n - m) bs))
 3. \<And>typ_desc list. \<forall>s m n f bs. field_lookup typ_desc f m = Some (s, n) \<longrightarrow> wf_fd typ_desc \<longrightarrow> length bs = size_td typ_desc \<longrightarrow> take (size_td s) (drop (n - m) (access_ti typ_desc v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) \<Longrightarrow> \<forall>s m n f bs. field_lookup_pair (DTPair typ_desc list) f m = Some (s, n) \<longrightarrow> wf_fd_pair (DTPair typ_desc list) \<longrightarrow> length bs = size_td_pair (DTPair typ_desc list) \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair (DTPair typ_desc list) v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) proof (prove)
goal (2 subgoals):
 1. \<And>dt_pair list s m n f bs. \<lbrakk>wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_pair dt_pair f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); \<forall>s m n. (\<exists>f. field_lookup_list list f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); field_lookup_pair dt_pair f m = Some (s, n)\<rbrakk> \<Longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v (take (size_td_pair dt_pair) bs))) @ take (size_td s - (size_td_pair dt_pair - (n - m))) (drop (n - (m + size_td_pair dt_pair)) (access_ti_list list v (drop (size_td_pair dt_pair) bs))) = access_ti s v (take (size_td s) (drop (n - m) bs))
 2. \<And>typ_desc list. \<forall>s m n f bs. field_lookup typ_desc f m = Some (s, n) \<longrightarrow> wf_fd typ_desc \<longrightarrow> length bs = size_td typ_desc \<longrightarrow> take (size_td s) (drop (n - m) (access_ti typ_desc v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) \<Longrightarrow> \<forall>s m n f bs. field_lookup_pair (DTPair typ_desc list) f m = Some (s, n) \<longrightarrow> wf_fd_pair (DTPair typ_desc list) \<longrightarrow> length bs = size_td_pair (DTPair typ_desc list) \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair (DTPair typ_desc list) v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) proof (prove)
goal (3 subgoals):
 1. \<And>dt_pair list s m n f bs. \<lbrakk>wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_pair dt_pair f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); \<forall>s m n. (\<exists>f. field_lookup_list list f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); field_lookup_pair dt_pair f m = Some (s, n); size_td s - (size_td_pair dt_pair - (n - m)) = 0\<rbrakk> \<Longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v (take (size_td_pair dt_pair) bs))) @ take (size_td s - (size_td_pair dt_pair - (n - m))) (drop (n - (m + size_td_pair dt_pair)) (access_ti_list list v (drop (size_td_pair dt_pair) bs))) = access_ti s v (take (size_td s) (drop (n - m) bs))
 2. \<And>dt_pair list s m n f bs. \<lbrakk>wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_pair dt_pair f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); \<forall>s m n. (\<exists>f. field_lookup_list list f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); field_lookup_pair dt_pair f m = Some (s, n)\<rbrakk> \<Longrightarrow> size_td s - (size_td_pair dt_pair - (n - m)) = 0
 3. \<And>typ_desc list. \<forall>s m n f bs. field_lookup typ_desc f m = Some (s, n) \<longrightarrow> wf_fd typ_desc \<longrightarrow> length bs = size_td typ_desc \<longrightarrow> take (size_td s) (drop (n - m) (access_ti typ_desc v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) \<Longrightarrow> \<forall>s m n f bs. field_lookup_pair (DTPair typ_desc list) f m = Some (s, n) \<longrightarrow> wf_fd_pair (DTPair typ_desc list) \<longrightarrow> length bs = size_td_pair (DTPair typ_desc list) \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair (DTPair typ_desc list) v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) proof (prove)
goal (3 subgoals):
 1. \<And>dt_pair list s m n f bs. \<lbrakk>wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_pair dt_pair f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); \<forall>s m n. (\<exists>f. field_lookup_list list f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); field_lookup_pair dt_pair f m = Some (s, n)\<rbrakk> \<Longrightarrow> size_td s - (size_td_pair dt_pair - (n - m)) = 0
 2. \<And>dt_pair list s m n f bs. \<lbrakk>wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_pair dt_pair f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); \<forall>s m n. (\<exists>f. field_lookup_list list f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); field_lookup_pair dt_pair f m = Some (s, n); size_td s - (size_td_pair dt_pair - (n - m)) = 0\<rbrakk> \<Longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v (take (size_td_pair dt_pair) bs))) @ take (size_td s - (size_td_pair dt_pair - (n - m))) (drop (n - (m + size_td_pair dt_pair)) (access_ti_list list v (drop (size_td_pair dt_pair) bs))) = access_ti s v (take (size_td s) (drop (n - m) bs))
 3. \<And>typ_desc list. \<forall>s m n f bs. field_lookup typ_desc f m = Some (s, n) \<longrightarrow> wf_fd typ_desc \<longrightarrow> length bs = size_td typ_desc \<longrightarrow> take (size_td s) (drop (n - m) (access_ti typ_desc v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) \<Longrightarrow> \<forall>s m n f bs. field_lookup_pair (DTPair typ_desc list) f m = Some (s, n) \<longrightarrow> wf_fd_pair (DTPair typ_desc list) \<longrightarrow> length bs = size_td_pair (DTPair typ_desc list) \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair (DTPair typ_desc list) v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) proof (prove)
goal (3 subgoals):
 1. \<And>dt_pair list s m n f bs. \<lbrakk>wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_pair dt_pair f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); \<forall>s m n. (\<exists>f. field_lookup_list list f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); field_lookup_pair dt_pair f m = Some (s, n)\<rbrakk> \<Longrightarrow> size_td s \<le> size_td_pair dt_pair - (n - m)
 2. \<And>dt_pair list s m n f bs. \<lbrakk>wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_pair dt_pair f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); \<forall>s m n. (\<exists>f. field_lookup_list list f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); field_lookup_pair dt_pair f m = Some (s, n); size_td s - (size_td_pair dt_pair - (n - m)) = 0\<rbrakk> \<Longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v (take (size_td_pair dt_pair) bs))) @ take (size_td s - (size_td_pair dt_pair - (n - m))) (drop (n - (m + size_td_pair dt_pair)) (access_ti_list list v (drop (size_td_pair dt_pair) bs))) = access_ti s v (take (size_td s) (drop (n - m) bs))
 3. \<And>typ_desc list. \<forall>s m n f bs. field_lookup typ_desc f m = Some (s, n) \<longrightarrow> wf_fd typ_desc \<longrightarrow> length bs = size_td typ_desc \<longrightarrow> take (size_td s) (drop (n - m) (access_ti typ_desc v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) \<Longrightarrow> \<forall>s m n f bs. field_lookup_pair (DTPair typ_desc list) f m = Some (s, n) \<longrightarrow> wf_fd_pair (DTPair typ_desc list) \<longrightarrow> length bs = size_td_pair (DTPair typ_desc list) \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair (DTPair typ_desc list) v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) proof (prove)
goal (3 subgoals):
 1. \<And>dt_pair list s m n f bs. \<lbrakk>wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_pair dt_pair f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); \<forall>s m n. (\<exists>f. field_lookup_list list f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); (s, n) \<in> td_set_pair dt_pair m\<rbrakk> \<Longrightarrow> size_td s \<le> size_td_pair dt_pair - (n - m)
 2. \<And>dt_pair list s m n f bs. \<lbrakk>wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_pair dt_pair f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); \<forall>s m n. (\<exists>f. field_lookup_list list f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); field_lookup_pair dt_pair f m = Some (s, n); size_td s - (size_td_pair dt_pair - (n - m)) = 0\<rbrakk> \<Longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v (take (size_td_pair dt_pair) bs))) @ take (size_td s - (size_td_pair dt_pair - (n - m))) (drop (n - (m + size_td_pair dt_pair)) (access_ti_list list v (drop (size_td_pair dt_pair) bs))) = access_ti s v (take (size_td s) (drop (n - m) bs))
 3. \<And>typ_desc list. \<forall>s m n f bs. field_lookup typ_desc f m = Some (s, n) \<longrightarrow> wf_fd typ_desc \<longrightarrow> length bs = size_td typ_desc \<longrightarrow> take (size_td s) (drop (n - m) (access_ti typ_desc v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) \<Longrightarrow> \<forall>s m n f bs. field_lookup_pair (DTPair typ_desc list) f m = Some (s, n) \<longrightarrow> wf_fd_pair (DTPair typ_desc list) \<longrightarrow> length bs = size_td_pair (DTPair typ_desc list) \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair (DTPair typ_desc list) v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) proof (prove)
goal (3 subgoals):
 1. \<And>dt_pair list s m n f bs. \<lbrakk>wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_pair dt_pair f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); \<forall>s m n. (\<exists>f. field_lookup_list list f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); size_td s + (n - m) \<le> size_td_pair dt_pair\<rbrakk> \<Longrightarrow> size_td s \<le> size_td_pair dt_pair - (n - m)
 2. \<And>dt_pair list s m n f bs. \<lbrakk>wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_pair dt_pair f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); \<forall>s m n. (\<exists>f. field_lookup_list list f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); field_lookup_pair dt_pair f m = Some (s, n); size_td s - (size_td_pair dt_pair - (n - m)) = 0\<rbrakk> \<Longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v (take (size_td_pair dt_pair) bs))) @ take (size_td s - (size_td_pair dt_pair - (n - m))) (drop (n - (m + size_td_pair dt_pair)) (access_ti_list list v (drop (size_td_pair dt_pair) bs))) = access_ti s v (take (size_td s) (drop (n - m) bs))
 3. \<And>typ_desc list. \<forall>s m n f bs. field_lookup typ_desc f m = Some (s, n) \<longrightarrow> wf_fd typ_desc \<longrightarrow> length bs = size_td typ_desc \<longrightarrow> take (size_td s) (drop (n - m) (access_ti typ_desc v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) \<Longrightarrow> \<forall>s m n f bs. field_lookup_pair (DTPair typ_desc list) f m = Some (s, n) \<longrightarrow> wf_fd_pair (DTPair typ_desc list) \<longrightarrow> length bs = size_td_pair (DTPair typ_desc list) \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair (DTPair typ_desc list) v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) proof (prove)
goal (2 subgoals):
 1. \<And>dt_pair list s m n f bs. \<lbrakk>wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_pair dt_pair f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); \<forall>s m n. (\<exists>f. field_lookup_list list f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); field_lookup_pair dt_pair f m = Some (s, n); size_td s - (size_td_pair dt_pair - (n - m)) = 0\<rbrakk> \<Longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v (take (size_td_pair dt_pair) bs))) @ take (size_td s - (size_td_pair dt_pair - (n - m))) (drop (n - (m + size_td_pair dt_pair)) (access_ti_list list v (drop (size_td_pair dt_pair) bs))) = access_ti s v (take (size_td s) (drop (n - m) bs))
 2. \<And>typ_desc list. \<forall>s m n f bs. field_lookup typ_desc f m = Some (s, n) \<longrightarrow> wf_fd typ_desc \<longrightarrow> length bs = size_td typ_desc \<longrightarrow> take (size_td s) (drop (n - m) (access_ti typ_desc v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) \<Longrightarrow> \<forall>s m n f bs. field_lookup_pair (DTPair typ_desc list) f m = Some (s, n) \<longrightarrow> wf_fd_pair (DTPair typ_desc list) \<longrightarrow> length bs = size_td_pair (DTPair typ_desc list) \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair (DTPair typ_desc list) v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) proof (prove)
goal (2 subgoals):
 1. \<And>dt_pair list s m n f bs. \<lbrakk>wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_pair dt_pair f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); \<forall>s m n. (\<exists>f. field_lookup_list list f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); field_lookup_pair dt_pair f m = Some (s, n); size_td s \<le> size_td_pair dt_pair - (n - m)\<rbrakk> \<Longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v (take (size_td_pair dt_pair) bs))) = access_ti s v (take (size_td s) (drop (n - m) bs))
 2. \<And>typ_desc list. \<forall>s m n f bs. field_lookup typ_desc f m = Some (s, n) \<longrightarrow> wf_fd typ_desc \<longrightarrow> length bs = size_td typ_desc \<longrightarrow> take (size_td s) (drop (n - m) (access_ti typ_desc v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) \<Longrightarrow> \<forall>s m n f bs. field_lookup_pair (DTPair typ_desc list) f m = Some (s, n) \<longrightarrow> wf_fd_pair (DTPair typ_desc list) \<longrightarrow> length bs = size_td_pair (DTPair typ_desc list) \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair (DTPair typ_desc list) v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) proof (prove)
goal (2 subgoals):
 1. \<And>dt_pair list s m n f bs. \<lbrakk>wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_list list f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); field_lookup_pair dt_pair f m = Some (s, n); size_td s \<le> size_td_pair dt_pair - (n - m); \<forall>m n. (\<exists>f. field_lookup_pair dt_pair f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)))\<rbrakk> \<Longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v (take (size_td_pair dt_pair) bs))) = access_ti s v (take (size_td s) (drop (n - m) bs))
 2. \<And>typ_desc list. \<forall>s m n f bs. field_lookup typ_desc f m = Some (s, n) \<longrightarrow> wf_fd typ_desc \<longrightarrow> length bs = size_td typ_desc \<longrightarrow> take (size_td s) (drop (n - m) (access_ti typ_desc v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) \<Longrightarrow> \<forall>s m n f bs. field_lookup_pair (DTPair typ_desc list) f m = Some (s, n) \<longrightarrow> wf_fd_pair (DTPair typ_desc list) \<longrightarrow> length bs = size_td_pair (DTPair typ_desc list) \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair (DTPair typ_desc list) v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) proof (prove)
goal (2 subgoals):
 1. \<And>dt_pair list s m n f bs. \<lbrakk>wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_list list f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); field_lookup_pair dt_pair f m = Some (s, n); size_td s \<le> size_td_pair dt_pair - (n - m); \<forall>n. (\<exists>f. field_lookup_pair dt_pair f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)))\<rbrakk> \<Longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v (take (size_td_pair dt_pair) bs))) = access_ti s v (take (size_td s) (drop (n - m) bs))
 2. \<And>typ_desc list. \<forall>s m n f bs. field_lookup typ_desc f m = Some (s, n) \<longrightarrow> wf_fd typ_desc \<longrightarrow> length bs = size_td typ_desc \<longrightarrow> take (size_td s) (drop (n - m) (access_ti typ_desc v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) \<Longrightarrow> \<forall>s m n f bs. field_lookup_pair (DTPair typ_desc list) f m = Some (s, n) \<longrightarrow> wf_fd_pair (DTPair typ_desc list) \<longrightarrow> length bs = size_td_pair (DTPair typ_desc list) \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair (DTPair typ_desc list) v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) proof (prove)
goal (2 subgoals):
 1. \<And>dt_pair list s m n f bs. \<lbrakk>wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_list list f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); field_lookup_pair dt_pair f m = Some (s, n); size_td s \<le> size_td_pair dt_pair - (n - m); (\<exists>f. field_lookup_pair dt_pair f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)))\<rbrakk> \<Longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v (take (size_td_pair dt_pair) bs))) = access_ti s v (take (size_td s) (drop (n - m) bs))
 2. \<And>typ_desc list. \<forall>s m n f bs. field_lookup typ_desc f m = Some (s, n) \<longrightarrow> wf_fd typ_desc \<longrightarrow> length bs = size_td typ_desc \<longrightarrow> take (size_td s) (drop (n - m) (access_ti typ_desc v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) \<Longrightarrow> \<forall>s m n f bs. field_lookup_pair (DTPair typ_desc list) f m = Some (s, n) \<longrightarrow> wf_fd_pair (DTPair typ_desc list) \<longrightarrow> length bs = size_td_pair (DTPair typ_desc list) \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair (DTPair typ_desc list) v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) proof (prove)
goal (2 subgoals):
 1. \<And>dt_pair list s m n f bs. \<lbrakk>wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_list list f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); field_lookup_pair dt_pair f m = Some (s, n); size_td s \<le> size_td_pair dt_pair - (n - m); \<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))\<rbrakk> \<Longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v (take (size_td_pair dt_pair) bs))) = access_ti s v (take (size_td s) (drop (n - m) bs))
 2. \<And>typ_desc list. \<forall>s m n f bs. field_lookup typ_desc f m = Some (s, n) \<longrightarrow> wf_fd typ_desc \<longrightarrow> length bs = size_td typ_desc \<longrightarrow> take (size_td s) (drop (n - m) (access_ti typ_desc v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) \<Longrightarrow> \<forall>s m n f bs. field_lookup_pair (DTPair typ_desc list) f m = Some (s, n) \<longrightarrow> wf_fd_pair (DTPair typ_desc list) \<longrightarrow> length bs = size_td_pair (DTPair typ_desc list) \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair (DTPair typ_desc list) v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) proof (prove)
goal (2 subgoals):
 1. \<And>dt_pair list s m n f bs. \<lbrakk>wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_list list f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); field_lookup_pair dt_pair f m = Some (s, n); size_td s \<le> size_td_pair dt_pair - (n - m); \<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)); wf_fd s\<rbrakk> \<Longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v (take (size_td_pair dt_pair) bs))) = access_ti s v (take (size_td s) (drop (n - m) bs))
 2. \<And>typ_desc list. \<forall>s m n f bs. field_lookup typ_desc f m = Some (s, n) \<longrightarrow> wf_fd typ_desc \<longrightarrow> length bs = size_td typ_desc \<longrightarrow> take (size_td s) (drop (n - m) (access_ti typ_desc v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) \<Longrightarrow> \<forall>s m n f bs. field_lookup_pair (DTPair typ_desc list) f m = Some (s, n) \<longrightarrow> wf_fd_pair (DTPair typ_desc list) \<longrightarrow> length bs = size_td_pair (DTPair typ_desc list) \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair (DTPair typ_desc list) v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) proof (prove)
goal (3 subgoals):
 1. \<And>dt_pair list s m n f bs. \<lbrakk>wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_list list f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); field_lookup_pair dt_pair f m = Some (s, n); size_td s \<le> size_td_pair dt_pair - (n - m); \<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)); wf_fd s; size_td s = 0\<rbrakk> \<Longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v (take (size_td_pair dt_pair) bs))) = access_ti s v (take (size_td s) (drop (n - m) bs))
 2. \<And>dt_pair list s m n f bs. \<lbrakk>wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_list list f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); field_lookup_pair dt_pair f m = Some (s, n); size_td s \<le> size_td_pair dt_pair - (n - m); \<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)); wf_fd s; size_td s \<noteq> 0\<rbrakk> \<Longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v (take (size_td_pair dt_pair) bs))) = access_ti s v (take (size_td s) (drop (n - m) bs))
 3. \<And>typ_desc list. \<forall>s m n f bs. field_lookup typ_desc f m = Some (s, n) \<longrightarrow> wf_fd typ_desc \<longrightarrow> length bs = size_td typ_desc \<longrightarrow> take (size_td s) (drop (n - m) (access_ti typ_desc v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) \<Longrightarrow> \<forall>s m n f bs. field_lookup_pair (DTPair typ_desc list) f m = Some (s, n) \<longrightarrow> wf_fd_pair (DTPair typ_desc list) \<longrightarrow> length bs = size_td_pair (DTPair typ_desc list) \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair (DTPair typ_desc list) v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) proof (prove)
goal (2 subgoals):
 1. \<And>dt_pair list s m n f bs. \<lbrakk>wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_list list f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); field_lookup_pair dt_pair f m = Some (s, n); size_td s \<le> size_td_pair dt_pair - (n - m); \<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)); wf_fd s; size_td s \<noteq> 0\<rbrakk> \<Longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v (take (size_td_pair dt_pair) bs))) = access_ti s v (take (size_td s) (drop (n - m) bs))
 2. \<And>typ_desc list. \<forall>s m n f bs. field_lookup typ_desc f m = Some (s, n) \<longrightarrow> wf_fd typ_desc \<longrightarrow> length bs = size_td typ_desc \<longrightarrow> take (size_td s) (drop (n - m) (access_ti typ_desc v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) \<Longrightarrow> \<forall>s m n f bs. field_lookup_pair (DTPair typ_desc list) f m = Some (s, n) \<longrightarrow> wf_fd_pair (DTPair typ_desc list) \<longrightarrow> length bs = size_td_pair (DTPair typ_desc list) \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair (DTPair typ_desc list) v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) proof (prove)
goal (3 subgoals):
 1. \<And>dt_pair list s m n f bs. \<lbrakk>wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_list list f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); field_lookup_pair dt_pair f m = Some (s, n); size_td s \<le> size_td_pair dt_pair - (n - m); wf_fd s; size_td s \<noteq> 0\<rbrakk> \<Longrightarrow> length (take (size_td_pair dt_pair) bs) = size_td_pair dt_pair
 2. \<And>dt_pair list s m n f bs. \<lbrakk>wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_list list f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); field_lookup_pair dt_pair f m = Some (s, n); size_td s \<le> size_td_pair dt_pair - (n - m); \<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)); wf_fd s; size_td s \<noteq> 0\<rbrakk> \<Longrightarrow> access_ti s v (take (size_td s) (drop (n - m) (take (size_td_pair dt_pair) bs))) = access_ti s v (take (size_td s) (drop (n - m) bs))
 3. \<And>typ_desc list. \<forall>s m n f bs. field_lookup typ_desc f m = Some (s, n) \<longrightarrow> wf_fd typ_desc \<longrightarrow> length bs = size_td typ_desc \<longrightarrow> take (size_td s) (drop (n - m) (access_ti typ_desc v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) \<Longrightarrow> \<forall>s m n f bs. field_lookup_pair (DTPair typ_desc list) f m = Some (s, n) \<longrightarrow> wf_fd_pair (DTPair typ_desc list) \<longrightarrow> length bs = size_td_pair (DTPair typ_desc list) \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair (DTPair typ_desc list) v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) proof (prove)
goal (2 subgoals):
 1. \<And>dt_pair list s m n f bs. \<lbrakk>wf_fd_pair dt_pair; wf_fd_list list; fu_commutes (update_ti_pair_t dt_pair) (update_ti_list_t list); fa_fu_ind \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> (size_td_list list) (size_td_pair dt_pair); fa_fu_ind \<lparr>field_access = access_ti_list list, field_update = update_ti_list_t list\<rparr> \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair) (size_td_list list); length bs = size_td_pair dt_pair + size_td_list list; fd_cons_double_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr>; fd_cons_update_access \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); fd_cons_access_update \<lparr>field_access = access_ti_pair dt_pair, field_update = update_ti_pair_t dt_pair\<rparr> (size_td_pair dt_pair); \<forall>v bs. length bs = size_td_pair dt_pair \<longrightarrow> length (access_ti_pair dt_pair v bs) = size_td_pair dt_pair; \<forall>s m n. (\<exists>f. field_lookup_list list f m = Some (s, n)) \<longrightarrow> (\<forall>bs. length bs = size_td_list list \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_list list v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs))); field_lookup_pair dt_pair f m = Some (s, n); size_td s \<le> size_td_pair dt_pair - (n - m); \<forall>bs. length bs = size_td_pair dt_pair \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair dt_pair v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)); wf_fd s; size_td s \<noteq> 0\<rbrakk> \<Longrightarrow> access_ti s v (take (size_td s) (drop (n - m) (take (size_td_pair dt_pair) bs))) = access_ti s v (take (size_td s) (drop (n - m) bs))
 2. \<And>typ_desc list. \<forall>s m n f bs. field_lookup typ_desc f m = Some (s, n) \<longrightarrow> wf_fd typ_desc \<longrightarrow> length bs = size_td typ_desc \<longrightarrow> take (size_td s) (drop (n - m) (access_ti typ_desc v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) \<Longrightarrow> \<forall>s m n f bs. field_lookup_pair (DTPair typ_desc list) f m = Some (s, n) \<longrightarrow> wf_fd_pair (DTPair typ_desc list) \<longrightarrow> length bs = size_td_pair (DTPair typ_desc list) \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair (DTPair typ_desc list) v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) proof (prove)
goal (1 subgoal):
 1. \<And>typ_desc list. \<forall>s m n f bs. field_lookup typ_desc f m = Some (s, n) \<longrightarrow> wf_fd typ_desc \<longrightarrow> length bs = size_td typ_desc \<longrightarrow> take (size_td s) (drop (n - m) (access_ti typ_desc v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) \<Longrightarrow> \<forall>s m n f bs. field_lookup_pair (DTPair typ_desc list) f m = Some (s, n) \<longrightarrow> wf_fd_pair (DTPair typ_desc list) \<longrightarrow> length bs = size_td_pair (DTPair typ_desc list) \<longrightarrow> take (size_td s) (drop (n - m) (access_ti_pair (DTPair typ_desc list) v bs)) = access_ti s v (take (size_td s) (drop (n - m) bs)) proof (prove)
goal:
No subgoals!