Commit ffff3722 authored by Heiko Becker's avatar Heiko Becker

Remove failing AA tests that cannot be handled (yet)

parent 7b77c32e
100 1
Ret + 1657#5 MTYPE 64 Var 0
GAMMA Var 0 MTYPE 64
PRE ? Var 0 ~100#1 100#1
ABS ? + 1657#5 MTYPE 64 Var 0 1157#5 2157#5 7771411516990528329#81129638414606681695789005144064 ? 1657#5 MTYPE 64 1657#5 1657#5 1657#45035996273704960 ? Var 0 ~100#1 100#1 25#2251799813685248
open preamble FloverTactics AbbrevsTheory MachineTypeTheory CertificateCheckerTheory FloverMapTheory;
open simpLib realTheory realLib RealArith;
val _ = new_theory "certificate_AdditionSimpleAA";
val C12_def = Define `C12:(real expr) = Const M64 ((1657)/(5))`;
val u0_def = Define `u0:(real expr) = Var 0`;
val PlusC12u0 = Define `PlusC12u0:(real expr) = Binop Plus C12 u0`;;
val RetPlusC12u0_def = Define `RetPlusC12u0 = Ret PlusC12u0`;
val defVars_additionSimple_def = Define `
defVars_additionSimple : typeMap =
(FloverMapTree_insert (Var 0) (M64) (FloverMapTree_empty))`;
val thePrecondition_additionSimple_def = Define `
thePreconditionadditionSimple (n:num):interval =
if n = 0 then ( (-100)/(1), (100)/(1)) else (0,1)`;
val absenv_additionSimple_def = RIGHT_CONV_RULE EVAL (Define `
absenv_additionSimple:analysisResult =
FloverMapTree_insert PlusC12u0 (( (1157)/(5), (2157)/(5)), (7771411516990528329)/(81129638414606681695789005144064)) (FloverMapTree_insert u0 (( (-100)/(1), (100)/(1)), (25)/(2251799813685248)) (FloverMapTree_insert C12 (( (1657)/(5), (1657)/(5)), (1657)/(45035996273704960)) (FloverMapTree_empty)))`);
val _ = store_thm ("ErrorBound_additionSimple_Sound",
``CertificateCheckerCmd RetPlusC12u0 absenv_additionSimple thePreconditionadditionSimple defVars_additionSimple``,
flover_eval_tac \\ fs[REAL_INV_1OVER]);
val _ = export_theory();
100 1
Let Var 5 MTYPE 32 Cast MTYPE 32 + 1657#5 MTYPE 64 * 3#5 MTYPE 64 Var 2 Ret / * ~ Var 5 Var 1 * + Var 5 Var 0 + Var 5 Var 0
GAMMA Var 2 MTYPE 64 Var 5 MTYPE 32 Var 1 MTYPE 32 Var 0 MTYPE 64
PRE ? Var 0 ~100#1 100#1 ? Var 1 20#1 20000#1 ? Var 2 ~30#1 50#1
ABS ? Var 5 1567#5 1807#5 5946853494151590254223768460713179402300517371078900237055784124491#276069853871622551497390234491081018098044358886815462206500968951971840 ? Cast MTYPE 32 + 1657#5 MTYPE 64 * 3#5 MTYPE 64 Var 2 1567#5 1807#5 5946853494151590254223768460713179402300517371078900237055784124491#276069853871622551497390234491081018098044358886815462206500968951971840 ? + 1657#5 MTYPE 64 * 3#5 MTYPE 64 Var 2 1567#5 1807#5 286015870425657721837309664377505636991869898457103#3291009114642412084309938365114701009965471731267159726697218048 ? 1657#5 MTYPE 64 1657#5 1657#5 1657#45035996273704960 ? * 3#5 MTYPE 64 Var 2 ~18#1 30#1 3650833728657301081634471694827535#365375409332725729550921208179070754913983135744 ? 3#5 MTYPE 64 3#5 3#5 3#45035996273704960 ? Var 2 ~30#1 50#1 25#4503599627370496 ? / * ~ Var 5 Var 1 * + Var 5 Var 0 + Var 5 Var 0 ~1697764138654329772000#3490644748218790563 845148567992740137100#3490644748218790563 86789720644057150247866605447704701639542420366828894132198862668669714230796996017035083608214420357613914531567484222212219331055483511822890139010872023483027505740246147962523569787278664172305316497757644071254699998665282042562758048408625758851595888688321139287912787500084300448747342010732963228878699239161772886561738720968290627692004030895987294913860908138447593680198320054472132697520066221100165663039771347855801540617277134187668140137009343975368944377522556200084375#116581075971445025849972765325192688960688023193987481443423359259469524004578990495359777413108258534013101183101133893535361165723138789382125100532000290607255302844371142602120272808586051005748656571844135028373285214957706768877222323723316372017777470087619528348277265902992869293242456576370752686840418222478699145317598793362601803894470311876274014967799666442159459249464411902617752130127840333947718959260993021328099576810901846581180134891356519631659292569462696113720000512 ? * ~ Var 5 Var 1 ~7228000#1 473252#1 627708954014028785690670388543358359225843737736535036700014937775757601384955913375#485667223056432267729865476705879726660601709763034880312953102434726071301302124544 ? ~ Var 5 ~1807#5 ~1567#5 5946853494151590254223768460713179402300517371078900237055784124491#276069853871622551497390234491081018098044358886815462206500968951971840 ? Var 5 1567#5 1807#5 5946853494151590254223768460713179402300517371078900237055784124491#276069853871622551497390234491081018098044358886815462206500968951971840 ? Var 1 20#1 20000#1 625#524288 ? * + Var 5 Var 0 + Var 5 Var 0 369689#25 5322249#25 221418104607549167303687710004535513986647169788185712517024989429754271464351432210081914542156799340890022745270932056774650467829092329282443134010319379819395881176728139368810835608677#11138771039116687545510672865479226867415108660274804518015606733152527263693060025649201199505301268990825951107408220973361095511170502925421536425103061983037096372949865600788267070914560 ? + Var 5 Var 0 1067#5 2307#5 53564494515561689875478770421278470058449227170380936038373717166064943312314302539#2486616182048933210776911240734104200502280753986738587202319884465797485062666877665280 ? Var 5 1567#5 1807#5 5946853494151590254223768460713179402300517371078900237055784124491#276069853871622551497390234491081018098044358886815462206500968951971840 ? Var 0 ~100#1 100#1 25#2251799813685248 ? + Var 5 Var 0 1067#5 2307#5 53564494515561689875478770421278470058449227170380936038373717166064943312314302539#2486616182048933210776911240734104200502280753986738587202319884465797485062666877665280 ? Var 5 1567#5 1807#5 5946853494151590254223768460713179402300517371078900237055784124491#276069853871622551497390234491081018098044358886815462206500968951971840 ? Var 0 ~100#1 100#1 25#2251799813685248
open preamble FloverTactics AbbrevsTheory MachineTypeTheory CertificateCheckerTheory FloverMapTheory;
open simpLib realTheory realLib RealArith;
val _ = new_theory "certificate_DopplerAA";
val C12_def = Define `C12:(real expr) = Const M64 ((1657)/(5))`;
val C34_def = Define `C34:(real expr) = Const M64 ((3)/(5))`;
val T2_def = Define `T2:(real expr) = Var 2`;
val MultC34T2 = Define `MultC34T2:(real expr) = Binop Mult C34 T2`;;
val PlusC12MultC34T2 = Define `PlusC12MultC34T2:(real expr) = Binop Plus C12 MultC34T2`;;
val CastM32PlusC12MultC34T2 = Define `CastM32PlusC12MultC34T2 : real expr = Downcast M32 PlusC12MultC34T2`;;
val t15_def = Define `t15:(real expr) = Var 5`;
val UMint15 = Define `UMint15:(real expr) = Unop Neg t15`;
val v1_def = Define `v1:(real expr) = Var 1`;
val MultUMint15v1 = Define `MultUMint15v1:(real expr) = Binop Mult UMint15 v1`;;
val u0_def = Define `u0:(real expr) = Var 0`;
val Plust15u0 = Define `Plust15u0:(real expr) = Binop Plus t15 u0`;;
val MultPlust15u0Plust15u0 = Define `MultPlust15u0Plust15u0:(real expr) = Binop Mult Plust15u0 Plust15u0`;;
val DivMultUMint15v1MultPlust15u0Plust15u0 = Define `DivMultUMint15v1MultPlust15u0Plust15u0:(real expr) = Binop Div MultUMint15v1 MultPlust15u0Plust15u0`;;
val RetDivMultUMint15v1MultPlust15u0Plust15u0_def = Define `RetDivMultUMint15v1MultPlust15u0Plust15u0 = Ret DivMultUMint15v1MultPlust15u0Plust15u0`;
val Lett15CastM32PlusC12MultC34T2RetDivMultUMint15v1MultPlust15u0Plust15u0_def = Define `Lett15CastM32PlusC12MultC34T2RetDivMultUMint15v1MultPlust15u0Plust15u0 = Let M32 5 CastM32PlusC12MultC34T2 RetDivMultUMint15v1MultPlust15u0Plust15u0`;
val defVars_doppler_def = Define `
defVars_doppler : typeMap =
(FloverMapTree_insert (Var 0) (M64) (FloverMapTree_insert (Var 1) (M32) (FloverMapTree_insert (Var 5) (M32) (FloverMapTree_insert (Var 2) (M64) (FloverMapTree_empty)))))`;
val thePrecondition_doppler_def = Define `
thePreconditiondoppler (n:num):interval =
if n = 0 then ( (-100)/(1), (100)/(1)) else if n = 1 then ( (20)/(1), (20000)/(1)) else if n = 2 then ( (-30)/(1), (50)/(1)) else (0,1)`;
val absenv_doppler_def = RIGHT_CONV_RULE EVAL (Define `
absenv_doppler:analysisResult =
FloverMapTree_insert (Var 5) (( (1567)/(5), (1807)/(5)) , (5946853494151590254223768460713179402300517371078900237055784124491)/(276069853871622551497390234491081018098044358886815462206500968951971840)) (FloverMapTree_insert DivMultUMint15v1MultPlust15u0Plust15u0 (( (-1697764138654329772000)/(3490644748218790563), (845148567992740137100)/(3490644748218790563)), (86789720644057150247866605447704701639542420366828894132198862668669714230796996017035083608214420357613914531567484222212219331055483511822890139010872023483027505740246147962523569787278664172305316497757644071254699998665282042562758048408625758851595888688321139287912787500084300448747342010732963228878699239161772886561738720968290627692004030895987294913860908138447593680198320054472132697520066221100165663039771347855801540617277134187668140137009343975368944377522556200084375)/(116581075971445025849972765325192688960688023193987481443423359259469524004578990495359777413108258534013101183101133893535361165723138789382125100532000290607255302844371142602120272808586051005748656571844135028373285214957706768877222323723316372017777470087619528348277265902992869293242456576370752686840418222478699145317598793362601803894470311876274014967799666442159459249464411902617752130127840333947718959260993021328099576810901846581180134891356519631659292569462696113720000512)) (FloverMapTree_insert MultPlust15u0Plust15u0 (( (369689)/(25), (5322249)/(25)), (221418104607549167303687710004535513986647169788185712517024989429754271464351432210081914542156799340890022745270932056774650467829092329282443134010319379819395881176728139368810835608677)/(11138771039116687545510672865479226867415108660274804518015606733152527263693060025649201199505301268990825951107408220973361095511170502925421536425103061983037096372949865600788267070914560)) (FloverMapTree_insert Plust15u0 (( (1067)/(5), (2307)/(5)), (53564494515561689875478770421278470058449227170380936038373717166064943312314302539)/(2486616182048933210776911240734104200502280753986738587202319884465797485062666877665280)) (FloverMapTree_insert u0 (( (-100)/(1), (100)/(1)), (25)/(2251799813685248)) (FloverMapTree_insert t15 (( (1567)/(5), (1807)/(5)), (5946853494151590254223768460713179402300517371078900237055784124491)/(276069853871622551497390234491081018098044358886815462206500968951971840)) (FloverMapTree_insert Plust15u0 (( (1067)/(5), (2307)/(5)), (53564494515561689875478770421278470058449227170380936038373717166064943312314302539)/(2486616182048933210776911240734104200502280753986738587202319884465797485062666877665280)) (FloverMapTree_insert u0 (( (-100)/(1), (100)/(1)), (25)/(2251799813685248)) (FloverMapTree_insert t15 (( (1567)/(5), (1807)/(5)), (5946853494151590254223768460713179402300517371078900237055784124491)/(276069853871622551497390234491081018098044358886815462206500968951971840)) (FloverMapTree_insert MultUMint15v1 (( (-7228000)/(1), (473252)/(1)), (627708954014028785690670388543358359225843737736535036700014937775757601384955913375)/(485667223056432267729865476705879726660601709763034880312953102434726071301302124544)) (FloverMapTree_insert v1 (( (20)/(1), (20000)/(1)), (625)/(524288)) (FloverMapTree_insert UMint15 (( (-1807)/(5), (-1567)/(5)), (5946853494151590254223768460713179402300517371078900237055784124491)/(276069853871622551497390234491081018098044358886815462206500968951971840)) (FloverMapTree_insert t15 (( (1567)/(5), (1807)/(5)), (5946853494151590254223768460713179402300517371078900237055784124491)/(276069853871622551497390234491081018098044358886815462206500968951971840)) (FloverMapTree_insert CastM32PlusC12MultC34T2 (( (1567)/(5), (1807)/(5)), (5946853494151590254223768460713179402300517371078900237055784124491)/(276069853871622551497390234491081018098044358886815462206500968951971840)) (FloverMapTree_insert PlusC12MultC34T2 (( (1567)/(5), (1807)/(5)), (286015870425657721837309664377505636991869898457103)/(3291009114642412084309938365114701009965471731267159726697218048)) (FloverMapTree_insert MultC34T2 (( (-18)/(1), (30)/(1)), (3650833728657301081634471694827535)/(365375409332725729550921208179070754913983135744)) (FloverMapTree_insert T2 (( (-30)/(1), (50)/(1)), (25)/(4503599627370496)) (FloverMapTree_insert C34 (( (3)/(5), (3)/(5)), (3)/(45035996273704960)) (FloverMapTree_insert C12 (( (1657)/(5), (1657)/(5)), (1657)/(45035996273704960)) (FloverMapTree_empty)))))))))))))))))))`);
val _ = store_thm ("ErrorBound_doppler_Sound",
``CertificateCheckerCmd Lett15CastM32PlusC12MultC34T2RetDivMultUMint15v1MultPlust15u0Plust15u0 absenv_doppler thePreconditiondoppler defVars_doppler``,
flover_eval_tac \\ fs[REAL_INV_1OVER]);
val _ = export_theory();
100 1
Let Var 4 MTYPE 64 + * Var 0 Var 0 Var 1 Let Var 5 MTYPE 32 Cast MTYPE 32 + Var 0 * Var 1 Var 1 Ret + * - Var 4 11#1 MTYPE 64 - Var 4 11#1 MTYPE 64 * - Var 5 7#1 MTYPE 64 - Var 5 7#1 MTYPE 64
GAMMA Var 0 MTYPE 64 Var 1 MTYPE 32 Var 4 MTYPE 64 Var 5 MTYPE 32
PRE ? Var 0 ~5#1 5#1 ? Var 1 ~5#1 5#1
ABS ? Var 4 ~30#1 30#1 1961594369037173916351814399292228280199748452939370332185#6582018229284824168619876730229402019930943462534319453394436096 ? + * Var 0 Var 0 Var 1 ~30#1 30#1 1961594369037173916351814399292228280199748452939370332185#6582018229284824168619876730229402019930943462534319453394436096 ? * Var 0 Var 0 ~25#1 25#1 6084722881095501802724119491379225#730750818665451459101842416358141509827966271488 ? Var 0 ~5#1 5#1 5#9007199254740992 ? Var 0 ~5#1 5#1 5#9007199254740992 ? Var 1 ~5#1 5#1 5#16777216 ? Var 5 ~30#1 30#1 4466206448905498720458189731062635560985#713623846352979940529142984724747568191373312 ? Cast MTYPE 32 + Var 0 * Var 1 Var 1 ~30#1 30#1 4466206448905498720458189731062635560985#713623846352979940529142984724747568191373312 ? + Var 0 * Var 1 Var 1 ~30#1 30#1 190147601533197042302697458892825#42535295865117307932921825928971026432 ? Var 0 ~5#1 5#1 5#9007199254740992 ? * Var 1 Var 1 ~25#1 25#1 21110624511590425#4722366482869645213696 ? Var 1 ~5#1 5#1 5#16777216 ? Var 1 ~5#1 5#1 5#16777216 ? + * - Var 4 11#1 MTYPE 64 - Var 4 11#1 MTYPE 64 * - Var 5 7#1 MTYPE 64 - Var 5 7#1 MTYPE 64 ~2710#1 3050#1 139030704224875129848631128264048621058694569279811803247481731950009496854900927199310534682209129985511707022154285854387010824157493138914819710540399882149220846561084929737220738253425#285152538601387201165073225356268207805826781703034995661199532368704697950542336656619550707335712486165144348349650456918044045085964874890791332482638386765749667147516559380179637015412736 ? * - Var 4 11#1 MTYPE 64 - Var 4 11#1 MTYPE 64 ~1439#1 1681#1 773662351057808216309562571440580964132485471675311443368294135882643818858939959011276491221639706451414523198800188781950039677633553108167639838248029929043321394561649#31658291388557380359744322690514840324496812684955115509000071179890844813636078997800499335839109758668501942530065835436974724391264154875845907853042325493325666835033489408 ? - Var 4 11#1 MTYPE 64 ~41#1 19#1 17668471681160709216739148477143291992482578503008842760016586714686423065#59285549689505892056868344324448208820874232148807968788202283012051522375647232 ? Var 4 ~30#1 30#1 1961594369037173916351814399292228280199748452939370332185#6582018229284824168619876730229402019930943462534319453394436096 ? 11#1 MTYPE 64 11#1 11#1 11#9007199254740992 ? - Var 4 11#1 MTYPE 64 ~41#1 19#1 17668471681160709216739148477143291992482578503008842760016586714686423065#59285549689505892056868344324448208820874232148807968788202283012051522375647232 ? Var 4 ~30#1 30#1 1961594369037173916351814399292228280199748452939370332185#6582018229284824168619876730229402019930943462534319453394436096 ? 11#1 MTYPE 64 11#1 11#1 11#9007199254740992 ? * - Var 5 7#1 MTYPE 64 - Var 5 7#1 MTYPE 64 ~1271#1 1369#1 172349177736374561212483578428963824900652162571585970864206741278453079284487093344235995612234246229019482224189617435933207648273009#372141426839350727961253789638658321589064376671906846864122981980487315514059736743009817965446945567110411062408283101969716033850703872 ? - Var 5 7#1 MTYPE 64 ~37#1 23#1 40228011429500474146133911235065735963306515172659036185#6427752177035961102167848369364650410088811975131171341205504 ? Var 5 ~30#1 30#1 4466206448905498720458189731062635560985#713623846352979940529142984724747568191373312 ? 7#1 MTYPE 64 7#1 7#1 7#9007199254740992 ? - Var 5 7#1 MTYPE 64 ~37#1 23#1 40228011429500474146133911235065735963306515172659036185#6427752177035961102167848369364650410088811975131171341205504 ? Var 5 ~30#1 30#1 4466206448905498720458189731062635560985#713623846352979940529142984724747568191373312 ? 7#1 MTYPE 64 7#1 7#1 7#9007199254740992
open preamble FloverTactics AbbrevsTheory MachineTypeTheory CertificateCheckerTheory FloverMapTheory;
open simpLib realTheory realLib RealArith;
val _ = new_theory "certificate_HimmilbeauAA";
val x10_def = Define `x10:(real expr) = Var 0`;
val Multx10x10 = Define `Multx10x10:(real expr) = Binop Mult x10 x10`;;
val x21_def = Define `x21:(real expr) = Var 1`;
val PlusMultx10x10x21 = Define `PlusMultx10x10x21:(real expr) = Binop Plus Multx10x10 x21`;;
val t14_def = Define `t14:(real expr) = Var 4`;
val Multx21x21 = Define `Multx21x21:(real expr) = Binop Mult x21 x21`;;
val Plusx10Multx21x21 = Define `Plusx10Multx21x21:(real expr) = Binop Plus x10 Multx21x21`;;
val CastM32Plusx10Multx21x21 = Define `CastM32Plusx10Multx21x21 : real expr = Downcast M32 Plusx10Multx21x21`;;
val t25_def = Define `t25:(real expr) = Var 5`;
val C12_def = Define `C12:(real expr) = Const M64 ((11)/(1))`;
val Subt14C12 = Define `Subt14C12:(real expr) = Binop Sub t14 C12`;;
val MultSubt14C12Subt14C12 = Define `MultSubt14C12Subt14C12:(real expr) = Binop Mult Subt14C12 Subt14C12`;;
val C34_def = Define `C34:(real expr) = Const M64 ((7)/(1))`;
val Subt25C34 = Define `Subt25C34:(real expr) = Binop Sub t25 C34`;;
val MultSubt25C34Subt25C34 = Define `MultSubt25C34Subt25C34:(real expr) = Binop Mult Subt25C34 Subt25C34`;;
val PlusMultSubt14C12Subt14C12MultSubt25C34Subt25C34 = Define `PlusMultSubt14C12Subt14C12MultSubt25C34Subt25C34:(real expr) = Binop Plus MultSubt14C12Subt14C12 MultSubt25C34Subt25C34`;;
val RetPlusMultSubt14C12Subt14C12MultSubt25C34Subt25C34_def = Define `RetPlusMultSubt14C12Subt14C12MultSubt25C34Subt25C34 = Ret PlusMultSubt14C12Subt14C12MultSubt25C34Subt25C34`;
val Lett25CastM32Plusx10Multx21x21RetPlusMultSubt14C12Subt14C12MultSubt25C34Subt25C34_def = Define `Lett25CastM32Plusx10Multx21x21RetPlusMultSubt14C12Subt14C12MultSubt25C34Subt25C34 = Let M32 5 CastM32Plusx10Multx21x21 RetPlusMultSubt14C12Subt14C12MultSubt25C34Subt25C34`;
val Lett14PlusMultx10x10x21Lett25CastM32Plusx10Multx21x21RetPlusMultSubt14C12Subt14C12MultSubt25C34Subt25C34_def = Define `Lett14PlusMultx10x10x21Lett25CastM32Plusx10Multx21x21RetPlusMultSubt14C12Subt14C12MultSubt25C34Subt25C34 = Let M64 4 PlusMultx10x10x21 Lett25CastM32Plusx10Multx21x21RetPlusMultSubt14C12Subt14C12MultSubt25C34Subt25C34`;
val defVars_himmilbeau_def = Define `
defVars_himmilbeau : typeMap =
(FloverMapTree_insert (Var 5) (M32) (FloverMapTree_insert (Var 4) (M64) (FloverMapTree_insert (Var 1) (M32) (FloverMapTree_insert (Var 0) (M64) (FloverMapTree_empty)))))`;
val thePrecondition_himmilbeau_def = Define `
thePreconditionhimmilbeau (n:num):interval =
if n = 0 then ( (-5)/(1), (5)/(1)) else if n = 1 then ( (-5)/(1), (5)/(1)) else (0,1)`;
val absenv_himmilbeau_def = RIGHT_CONV_RULE EVAL (Define `
absenv_himmilbeau:analysisResult =
FloverMapTree_insert (Var 4) (( (-30)/(1), (30)/(1)) , (1961594369037173916351814399292228280199748452939370332185)/(6582018229284824168619876730229402019930943462534319453394436096)) (FloverMapTree_insert (Var 5) (( (-30)/(1), (30)/(1)) , (4466206448905498720458189731062635560985)/(713623846352979940529142984724747568191373312)) (FloverMapTree_insert PlusMultSubt14C12Subt14C12MultSubt25C34Subt25C34 (( (-2710)/(1), (3050)/(1)), (139030704224875129848631128264048621058694569279811803247481731950009496854900927199310534682209129985511707022154285854387010824157493138914819710540399882149220846561084929737220738253425)/(285152538601387201165073225356268207805826781703034995661199532368704697950542336656619550707335712486165144348349650456918044045085964874890791332482638386765749667147516559380179637015412736)) (FloverMapTree_insert MultSubt25C34Subt25C34 (( (-1271)/(1), (1369)/(1)), (172349177736374561212483578428963824900652162571585970864206741278453079284487093344235995612234246229019482224189617435933207648273009)/(372141426839350727961253789638658321589064376671906846864122981980487315514059736743009817965446945567110411062408283101969716033850703872)) (FloverMapTree_insert Subt25C34 (( (-37)/(1), (23)/(1)), (40228011429500474146133911235065735963306515172659036185)/(6427752177035961102167848369364650410088811975131171341205504)) (FloverMapTree_insert C34 (( (7)/(1), (7)/(1)), (7)/(9007199254740992)) (FloverMapTree_insert t25 (( (-30)/(1), (30)/(1)), (4466206448905498720458189731062635560985)/(713623846352979940529142984724747568191373312)) (FloverMapTree_insert Subt25C34 (( (-37)/(1), (23)/(1)), (40228011429500474146133911235065735963306515172659036185)/(6427752177035961102167848369364650410088811975131171341205504)) (FloverMapTree_insert C34 (( (7)/(1), (7)/(1)), (7)/(9007199254740992)) (FloverMapTree_insert t25 (( (-30)/(1), (30)/(1)), (4466206448905498720458189731062635560985)/(713623846352979940529142984724747568191373312)) (FloverMapTree_insert MultSubt14C12Subt14C12 (( (-1439)/(1), (1681)/(1)), (773662351057808216309562571440580964132485471675311443368294135882643818858939959011276491221639706451414523198800188781950039677633553108167639838248029929043321394561649)/(31658291388557380359744322690514840324496812684955115509000071179890844813636078997800499335839109758668501942530065835436974724391264154875845907853042325493325666835033489408)) (FloverMapTree_insert Subt14C12 (( (-41)/(1), (19)/(1)), (17668471681160709216739148477143291992482578503008842760016586714686423065)/(59285549689505892056868344324448208820874232148807968788202283012051522375647232)) (FloverMapTree_insert C12 (( (11)/(1), (11)/(1)), (11)/(9007199254740992)) (FloverMapTree_insert t14 (( (-30)/(1), (30)/(1)), (1961594369037173916351814399292228280199748452939370332185)/(6582018229284824168619876730229402019930943462534319453394436096)) (FloverMapTree_insert Subt14C12 (( (-41)/(1), (19)/(1)), (17668471681160709216739148477143291992482578503008842760016586714686423065)/(59285549689505892056868344324448208820874232148807968788202283012051522375647232)) (FloverMapTree_insert C12 (( (11)/(1), (11)/(1)), (11)/(9007199254740992)) (FloverMapTree_insert t14 (( (-30)/(1), (30)/(1)), (1961594369037173916351814399292228280199748452939370332185)/(6582018229284824168619876730229402019930943462534319453394436096)) (FloverMapTree_insert CastM32Plusx10Multx21x21 (( (-30)/(1), (30)/(1)), (4466206448905498720458189731062635560985)/(713623846352979940529142984724747568191373312)) (FloverMapTree_insert Plusx10Multx21x21 (( (-30)/(1), (30)/(1)), (190147601533197042302697458892825)/(42535295865117307932921825928971026432)) (FloverMapTree_insert Multx21x21 (( (-25)/(1), (25)/(1)), (21110624511590425)/(4722366482869645213696)) (FloverMapTree_insert x21 (( (-5)/(1), (5)/(1)), (5)/(16777216)) (FloverMapTree_insert x21 (( (-5)/(1), (5)/(1)), (5)/(16777216)) (FloverMapTree_insert x10 (( (-5)/(1), (5)/(1)), (5)/(9007199254740992)) (FloverMapTree_insert PlusMultx10x10x21 (( (-30)/(1), (30)/(1)), (1961594369037173916351814399292228280199748452939370332185)/(6582018229284824168619876730229402019930943462534319453394436096)) (FloverMapTree_insert x21 (( (-5)/(1), (5)/(1)), (5)/(16777216)) (FloverMapTree_insert Multx10x10 (( (-25)/(1), (25)/(1)), (6084722881095501802724119491379225)/(730750818665451459101842416358141509827966271488)) (FloverMapTree_insert x10 (( (-5)/(1), (5)/(1)), (5)/(9007199254740992)) (FloverMapTree_insert x10 (( (-5)/(1), (5)/(1)), (5)/(9007199254740992)) (FloverMapTree_empty))))))))))))))))))))))))))))`);
val _ = store_thm ("ErrorBound_himmilbeau_Sound",
``CertificateCheckerCmd Lett14PlusMultx10x10x21Lett25CastM32Plusx10Multx21x21RetPlusMultSubt14C12Subt14C12MultSubt25C34Subt25C34 absenv_himmilbeau thePreconditionhimmilbeau defVars_himmilbeau``,
flover_eval_tac \\ fs[REAL_INV_1OVER]);
val _ = export_theory();
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment