proposition: Lemma New_RunsTo_characterization: forall (vlen vtup : StringMap.key) (env : GLabelMap.t (FuncSpec QsADTs.ADTValue)) (fnew : GLabelMap.key) (initial_state st' : State QsADTs.ADTValue) (w: W), StringMap.MapsTo vlen (wrap w) initial_state -> GLabelMap.MapsTo fnew (Axiomatic New) env -> RunsTo env (Call vtup fnew [[[vlen]]]) initial_state st' -> exists x1, M.Equal st' ([vtup |> ADT (TupleConstructor x1)]::initial_state) /\ Datatypes.length x1 = Word.wordToNat w.
proof: Proof. repeat QS_t. reflexivity. Qed.
imports: Fiat.Computation.Notations CertifiedExtraction.Extraction.QueryStructures.CallRules.Core