fact: Definition size_of_kind (k : kind_of_rewrite) (arg : Z) : Q := let x := inject_Z arg in match k with | kind_rewrite_strat bottomup => -9.07 + 0.926*x + -0.0169*x^2 + 9.36E-05*x^3 | kind_rewrite_strat topdown => -9.31 + 0.947*x + -0.0172*x^2 + 9.45E-05*x^3 | kind_setoid_rewrite => -0.074 + 7.79E-03*x + -7.08E-05*x^2 + 1.42E-06*x^3 end%Q.
imports: Coq.micromega.Lia Coq.ZArith.ZArith Coq.QArith.QArith Coq.Classes.Morphisms Coq.Setoids.Setoid Coq.Lists.List PerformanceExperiments.Harness PerformanceExperiments.LetIn PerformanceExperiments.ListRectInstances