fact: Definition add_link_back (F f : members) (v : compact_prod (map (fun it : member => reptype (field_type (name_member it) F)) (all_but_link f))) : compact_prod (map (fun it => reptype (field_type (name_member it) F)) f) := list_rect (fun f0 : list member => compact_prod (map (field_type' F) (all_but_link f0)) -> compact_prod (map (field_type' F) f0)) (fun _ : compact_prod (map (field_type' F) (all_but_link nil)) => tt) (fun (it0 : member) (f0 : list member) (IHf : compact_prod (map (field_type' F) (all_but_link f0)) -> compact_prod (map (field_type' F) f0)) (v0 : compact_prod (map (field_type' F) (all_but_link (it0 :: f0)))) => match f0 as l return (compact_prod (map (field_type' F) (all_but_link (it0 :: l))) -> (compact_prod (map (field_type' F) (all_but_link l)) -> compact_prod (map (field_type' F) l)) -> compact_prod (map (field_type' F) (it0 :: l))) with | nil => fun (_ : compact_prod (map (field_type' F) (all_but_link (it0 :: nil)))) (_ : compact_prod (map (field_type' F) (all_but_link nil)) -> compact_prod (map (field_type' F) nil)) => default_val (field_type (name_member it0) F) | it1 :: f1 => fun (v1 : compact_prod (map (field_type' F) (all_but_link (it0 :: it1 :: f1)))) (IHf0 : compact_prod (map (field_type' F) (all_but_link (it1 :: f1))) -> compact_prod (map (field_type' F) (it1 :: f1))) => (if ident_eq (name_member it0) list_link as s0 return (compact_prod (map (field_type' F) (if s0 then it1 :: f1 else it0 :: all_but_link (it1 :: f1))) -> reptype (field_type (name_member it0) F) * compact_prod (map (field_type' F) (it1 :: f1))) then fun v2 : compact_prod (map (field_type' F) (it1 :: f1)) => (default_val (field_type (name_member it0) F), v2) else fun v2 : compact_prod (map (field_type' F) (it0 :: all_but_link (it1 :: f1))) => match all_but_link (it1 :: f1) as l return (all_but_link (it1 :: f1) = l -> compact_prod (map (field_type' F) (it0 :: l)) -> (compact_prod (map (field_type' F) l) -> compact_prod (map (field_type' F) (it1 :: f1))) -> reptype (field_type (name_member it0) F) * compact_prod (map (field_type' F) (it1 :: f1))) with | nil => fun (Heqm0 : all_but_link (it1 :: f1) = nil) (v3 : compact_prod (map (field_type' F) (it0 :: nil))) (IHf1 : compact_prod (map (field_type' F) nil) -> compact_prod (map (field_type' F) (it1 :: f1))) => let s0 := ident_eq (name_member it1) list_link in (if s0 return ((if s0 then f1 else it1 :: all_but_link f1) = nil -> reptype (field_type (name_member it0) F) * compact_prod (map (field_type' F) (it1 :: f1))) then fun Heqm1 : f1 = nil => eq_rect_r (fun f2 : members => (compact_prod (map (field_type' F) nil) -> compact_prod (map (field_type' F) (it1 :: f2))) -> reptype (field_type (name_member it0) F) * compact_prod (map (field_type' F) (it1 :: f2))) (fun _ : compact_prod (map (field_type' F) nil) -> compact_prod (map (field_type' F) (it1 :: nil)) => (v3, default_val (field_type (name_member it1) F))) Heqm1 IHf1 else fun Heqm1 : it1 :: all_but_link f1 = nil => False_rect (reptype (field_type (name_member it0) F) * compact_prod (map (field_type' F) (it1 :: f1))) (eq_rect (it1 :: all_but_link f1) (fun e : members => match e with | nil => False | _ :: _ => True end) I nil Heqm1)) Heqm0 | p :: m0 => fun (_ : all_but_link (it1 :: f1) = p :: m0) (v3 : compact_prod (map (field_type' F) (it0 :: p :: m0))) (IHf1 : compact_prod (map (field_type' F) (p :: m0)) -> compact_prod (map (field_type' F) (it1 :: f1))) => (fst v3, IHf1 (snd v3)) end eq_refl v2 IHf0) v1 end v0 IHf) f v.
imports: VST.floyd.base2 VST.floyd.client_lemmas VST.floyd.closed_lemmas VST.floyd.nested_pred_lemmas VST.floyd.nested_field_lemmas VST.floyd.efield_lemmas VST.floyd.mapsto_memory_block VST.floyd.reptype_lemmas VST.floyd.data_at_rec_lemmas VST.floyd.field_at VST.floyd.nested_loadstore VST.floyd.entailer