proposition: Lemma CompileWordList_push : forall vret vhd vlst fpointer (env: Env QsADTs.ADTValue) ext tenv h (t: list W), GLabelMap.MapsTo fpointer (Axiomatic QsADTs.WordListADTSpec.Push) env -> Lifted_MapsTo ext tenv vhd (wrap h) -> Lifted_MapsTo ext tenv vlst (wrap (FacadeWrapper := WrapInstance (H := QS_WrapWordList)) t) -> Lifted_not_mapsto_adt ext tenv vret -> vret <> vlst -> vret <> vhd -> vhd <> vlst -> vhd ∉ ext -> vlst ∉ ext -> vret ∉ ext -> {{ tenv }} Call vret fpointer (vlst :: vhd :: nil) {{ [[ `vret ->> (Word.natToWord 32 0) as _ ]] :: [[ NTSome (H := WrapInstance (H := QS_WrapWordList)) vlst ->> h :: t as _ ]] :: DropName vlst (DropName vret tenv) }} ∪ {{ ext }} // env.
proof: Proof. repeat (SameValues_Facade_t_step || facade_cleanup_call || LiftPropertyToTelescope_t). facade_eauto. facade_eauto. repeat apply DropName_remove; congruence. Qed.
imports: CertifiedExtraction.Extraction.QueryStructures.CallRules.Core