proposition: Theorem SharpenedWheelSensor : FullySharpened WheelSensorSpec.
proof: Proof. start sharpening ADT. start_honing_QueryStructure'. hone method "AddSpeedSubscriber". { dropDuplicateFree. } hone method "AddTirePressureSubscriber". { dropDuplicateFree. } decompose_EnumField "subscribers" "topic". chooseIndexes. initializer. insertOne. insertOne. rewrite refine_encode_SensorData_Impl; planOne. rewrite refine_encode_SensorData_Impl; planOne. final_optimizations. determinize. choose_data_structures. final_simplification. use_this_one. Defined.
imports: Coq.Strings.Ascii Coq.Bool.Bool Coq.Lists.List Coq.Structures.OrderedType Fiat.Narcissus.BinLib.Core Fiat.Narcissus.Common.Specs Fiat.Narcissus.Common.Compose Fiat.Narcissus.Common.ComposeOpt Fiat.Narcissus.Automation.Solver Fiat.Narcissus.Lib2.WordOpt Fiat.Narcissus.Lib2.NatOpt Fiat.Narcissus.Lib2.StringOpt Fiat.Narcissus.Lib2.EnumOpt Fiat.Narcissus.Lib2.FixListOpt Fiat.Narcissus.Lib2.SumTypeOpt Fiat.Common.SumType Fiat.Examples.Tutorial.Tutorial Fiat.Examples.DnsServer.DecomposeEnumField Fiat.QueryStructure.Automation.AutoDB Fiat.QueryStructure.Implementation.DataStructures.BagADT.BagADT Fiat.QueryStructure.Automation.IndexSelection Fiat.QueryStructure.Specification.SearchTerms.ListPrefix Fiat.QueryStructure.Automation.SearchTerms.FindPrefixSearchTerms Fiat.QueryStructure.Automation.MasterPlan Fiat.Examples.HACMSDemo.DuplicateFree Fiat.Examples.HACMSDemo.HACMSDemo Fiat.Examples.HACMSDemo.WheelSensor