Courtade–Kumar proof module `CKLaneC.RSC2.BB_0047` (transplant)

import Definitions.Def_CK_CKLaneC_RSCell_Staged
import Definitions.Def_CK_CKLaneC_RSCell_RegionI

-- ===== source module CKLaneC.RSC2.BB_0047 =====
section

/-! RA-stat cover batch BB_0047 (generated by tools/emit_cover2.py; compact format). -/

namespace CKLaneC.RSC2.BB_0047
open CKLaneC.TM3 CKLaneC.RSCell

noncomputable def c0 : Cell := { bc := 6052837899185946624, bh := 288230376151711744, tc := 8070450532247928832, th := 1152921504606846976, sc := 4575657221408423936, sh := 252201579132747776 }
noncomputable def q0 : Cert := { V0 := [[[2960624824337056949]], [[(-85734389431053657), 407384632275270479], [71619506058332093]], [[1296885150095846, (-10904803269433761), (-3190691496194738)], [(-2043351207297792), 9109490707322256], [328423838953897]], [[(-30871261392003), 126708987016324, 267139561525783, (-119247525556792)], [39459762020588, (-196001706170113), (-223159033056415)], [(-8596947662074), 15084094437201], [21225634618050]], [[843679962189, (-2424972952618), (-11061902468651), 8125187039128, 3124395129529], [(-1188339705317), 1365859726793, 18096969785823, (-6787496665407)], [375855538951, 1443811364089, (-5922791105198)], [(-593938072676), 2254110250710], [(-156716437361)]]], r0 := 62080663330396, V1 := [[[6303185242674377988]], [[(-158977419724821235), 0], [132804168206927052]], [[1546069050933552, 0, 0], [(-2354254811287827), 0], [9733307003060]], [[(-29539935817552), 0, 0, 0], [6211618607847, 0, 0], [28442978042583, 0], [32857359736389]], [[757098582609, 0, 0, 0, 0], [(-310060983321), 0, 0, 0], [(-643901730189), 0, 0], [(-456498036489), 0], [(-630425451052)]]], r1 := 25560313411108, V2 := [[[9873689158114783943]], [[(-100777728725211340), 212017700577454857], [(-498731932119494799)]], [[1264590561235794, (-2812969337743867), (-3746066947006127)], [(-3403512324081082), 22948610641789036], [(-5064831706190772)]], [[(-24323164450994), (-45842159971947), 164463156253582, 42625585023049], [89849441998327, (-499673836731355), (-488969090803779)], [166441308694361, 628449578156274], [(-2244375645879)]], [[629507884728, 1175068851974, (-2220624458259), (-3866714477853), 11664609235], [(-2239118039505), 234459019735, 29835979562148, 3101835872480], [(-589556034032), (-34124479829376), (-8759485542115)], [6323750391729, (-10347660899834)], [2499239980385]]], r2 := 591187236954184, V3 := [[[13818145498190437332]], [[(-215125861054405226), 260286259431381534], [(-334205717121190674)]], [[2155417152597333, 5533296347712195, (-12278132496833105)], [(-12370682067696306), 35259357935491765], [(-7434454824857535)]], [[(-13101514591616), (-405271746012457), 125423662162964, 511116366583808], [295922817752358, 324825360787605, (-2320642677576172)], [(-19594719497084), 1739881664777420], [(-100173721370488)]], [[(-168678163287), 6172269254649, 24667860210110, (-25407826982425), (-18620013158120)], [(-3706919335596), (-62535831634413), 63760849552196, 117601131741616], [15058234946654, (-35735750062434), (-164702484974965)], [9763240412391, 33782495066198], [872824526852]]], r3 := 13834310633504824, Vm := [[[12137275977009092666]], [[(-127064580794556958), 0], [(-240646648434152342)]], [[595066093855899, 0, 0], [(-7036681818977407), 0], [4137837561398334]], [[(-11969263070037), 0, 0, 0], [20180797067890, 0, 0], [(-14922199347726), 0], [86466895718068]], [[397962150248, 0, 0, 0, 0], [(-594095314580), 0, 0, 0], [(-1276980635208), 0, 0], [3177426712325, 0], [1189148934517]]], rm := 83667226764190 }
noncomputable def w0 : Wit := { Z0 := { p := [[[3016925860243858640]], [[(-90702031619939666), 430989408606265520], [75769300349789209]], [[1521531782267514, (-12957433088562810), 0], [(-2411525359537910), 10824185764255601], [451781269549778]], [[(-38851706356030), 217361683181073, 0, 0], [56832780801893, (-344503622791130), 0], [(-19687030344173), 64540181364254], [24385097957606]], [[1115404337452, (-5550243765148), 0, 0, 0], [(-1855888107564), 8118968685984, 0, 0], [938122161604, (-2812432906311), 0], [(-882238552920), 3483585422515], [(-85831278849)]]], r := 7374328550977, ok := true }, Z1 := { p := [[[6895830537700248321]], [[(-207318929417004949), 0], [173186972228089620]], [[3477786930897175, 0, 0], [(-5512057964658080), 0], [1032642901828065]], [[(-88803900242354), 0, 0, 0], [129903498975757, 0, 0], [(-44998926500967), 0], [55737366760244]], [[2549495628463, 0, 0, 0, 0], [(-4242029960146), 0, 0, 0], [2144279226524, 0, 0], [(-2016545263817), 0], [(-196185780225)]]], r := 6329475964179, ok := true }, Z2 := { p := [[[12624178201203116166]], [[(-204860884660401371), 430989408606265520], [(-1013821864362290809)]], [[4291159561201084, (-12957433088562810), 0], [10110278772029344, 10824185764255601], [31840875703535971]], [[(-112216189822528), 217361683181073, 0, 0], [(-205719385383394), (-344503622791130), 0], [(-353188132896924), 64540181364254], [(-1523469198810388)]], [[3333455010233, (-5550243765148), 0, 0, 0], [4599340158979, 8118968685984, 0, 0], [4752906216453, (-2812432906311), 0], [16922528148524, 3483585422515], [66288813627118]]], r := 15363705790428, ok := true }, Z3 := { p := [[[25361375860768468076]], [[(-1155163286758804467), 1397661487415822451], [(-1794587469637892272)]], [[56610587319205543, (-79269726423599540), 0], [73505048631874628, 20025187691782104], [68773832753277726]], [[(-2935020971232239), 3721274739033837, 0, 0], [(-3778423034846269), (-755445720615581), 0], [(-3152827615983636), (-169053155327366)], [(-3059136474043338)]], [[154959020151424, (-192371251418611), 0, 0, 0], [197442066696713, 29458060888623, 0, 0], [159539333728564, 13058577263655, 0], [140036808123412, 5558848742984], [138708860768527]]], r := 234114958690522, ok := true }, iE := { p := [[[27948370446426930983]], [[(-332098481572252233), 0], [(-628958802214511780)]], [[8057098993261294, 0, 0], [6236295512536356, 0], [34135656333913307]], [[(-213423951902539), 0, 0, 0], [(-31324574969810), 0, 0], [(-403249069922880), 0], [(-1399607378423864)]], [[6452511048090, 0, 0, 0, 0], [(-623331579380), 0, 0, 0], [8249864980486, 0, 0], [15136678593030, 0], [65852841687916]]], r := 16367941295840, ok := true }, iHu := { p := [[[45317077669404249936]], [[(-1746255132490495101), 0], [(-1508669400178863107)]], [[88906659333727078, 0, 0], [70466024104307560, 0], [66360104974486737]], [[(-4620864614696632), 0, 0, 0], [(-3509225765491382), 0, 0], [(-3031780083111596), 0], [(-2979767664848052)]], [[244478502662124, 0, 0, 0, 0], [184740969005009, 0, 0, 0], [155856220518611, 0, 0], [137891021753977, 0], [136202858375096]]], r := 237285218973441, ok := true }, T := { p := [[[8070450532247928832]], [[0, 1152921504606846976], [0]]], r := 0, ok := true }, E := { p := [[[12175392034866990949]], [[144674953950424526, 0], [273998800946946318]], [[(-1790873871310656), 0, 0], [3794848396871191, 0], [(-8704659223242248)]], [[29987915269578, 0, 0, 0], [(-92835635922722), 0, 0], [(-80204937157727), 0], [79173402530903]], [[(-833557078360), 0, 0, 0, 0], [1403396087441, 0, 0, 0], [(-391685517497), 0, 0], [1047497593334, 0], [(-2553184867828)]]], r := 3166878411045, ok := true }, de := { p := [[[(-32249720347261978210)]], [[798412993402824485, 0], [689785375252780337]], [[(-20053959337826641), 0, 0], [3368607360624522, 0], [(-14968314598537919)]], [[743238050169557, 0, 0, 0], [16450791734887, 0, 0], [14212588777759, 0], [479277558173030]], [[(-30701160054629), 0, 0, 0, 0], [80338406865, 0, 0, 0], [495797534557, 0, 0], [59964744520, 0], [(-17104104080067)]]], r := 10595060534846, ok := true }, dde := { p := [[[(-177975489577032331292)]], [[8940518905876236319, 0], [7724121775825047706]], [[(-497029069958286597), 0, 0], [(-433073138967830921), 0], [(-370983473060169579)]], [[27374574494424197, 0, 0, 0], [23614325870473467, 0, 0], [20401492418708377, 0], [17652512834508718]], [[(-1508936043861582), 0, 0, 0, 0], [(-1303900992508734), 0, 0, 0], [(-1127503391335076), 0, 0], [(-973234259251851), 0], [(-840652245662690)]]], r := 517553705314653, ok := true }, nJu := { p := [[[(-64499440694523956419)]], [[1596825986805648971, 0], [1379570750505560675]], [[(-40107918675653281), 0, 0], [6737214721249045, 0], [(-29936629197075837)]], [[1486476100339114, 0, 0, 0], [32901583469774, 0, 0], [28425177555518, 0], [958555116346061]], [[(-61402320109257), 0, 0, 0, 0], [160676813730, 0, 0, 0], [991595069114, 0, 0], [119929489040, 0], [(-34208208160134)]]], r := 21190121069683, ok := true }, Jd1 := { p := [[[(-355950979154064662583)]], [[17881037811752472638, 0], [15448243551650095413]], [[(-994058139916573194), 0, 0], [(-866146277935661841), 0], [(-741966946120339158)]], [[54749148988848395, 0, 0, 0], [47228651740946935, 0, 0], [40802984837416755, 0], [35305025669017436]], [[(-3017872087723163), 0, 0, 0, 0], [(-2607801985017467), 0, 0, 0], [(-2255006782670151), 0, 0], [(-1946468518503702), 0], [(-1681304491325379)]]], r := 1035107410629296, ok := true }, term0 := { p := [[[3228113420576602407091]], [[(-320654813497762075424), 0], [(-245888541730660888416)]], [[25807563359243363960, 0, 0], [25861085926028534322, 0], [16271579107376600364]], [[(-1869010436244122530), 0, 0, 0], [(-2100270358885495555), 0, 0], [(-1732270753284187460), 0], [(-991734532997700047)]], [[127640002837394156, 0, 0, 0, 0], [153072117431573762, 0, 0, 0], [141550313961692778, 0, 0], [106406148631592095, 0], [57553928789841413]]], r := 73726917753228268, ok := true }, r0 := { p := [[[92815991422213154764]], [[(-5559844765198998724), 25092616870715747186], [(-1714458889812884053)]], [[295371524410166409, (-1428630226037109163), 1410442655666293705], [47401724738963861, (-527534044214701079)], [108468731775106324]], [[(-14861206366174918), 73635151285833019, (-60639505170930902), (-47698675096917304)], [(-423987487663554), 18413699972406032, (-46583752440917430)], [(-5591103650181460), 29636199433545349], [(-4165999943206762)]], [[747424117877030, (-3643309316958466), 2574664975827244, 4795018218667806, (-602458288320849)], [(-44163527738615), (-510459020645422), 2386317016946410, (-793940665819435)], [263105747813549, (-1427072520224667), 1803144638268608], [174387423690365, (-1205822391119290)], [201611101329495]]], r := 14014860478493999, ok := true }, r1 := { p := [[[397840893597523992293]], [[(-20284346166949194396), 0], [(-10413768924327696329)]], [[1013006629218612659, 0, 0], [399489991542635989, 0], [510412349294919511]], [[(-50110681968913255), 0, 0, 0], [(-13130450186388419), 0, 0], [(-23435594553549526), 0], [(-21673870672336618)]], [[2531787817592903, 0, 0, 0, 0], [454905984062818, 0, 0, 0], [997184568583579, 0, 0], [910243266015237, 0], [1005280840343907]]], r := 11404611892922566, ok := true }, r2 := { p := [[[384028540170510688858]], [[(-24855270810364030724), 29360449342386753769], [(-48739259224127715262)]], [[1339220006245409507, (-1499606115445213916), 190827045446294546], [2959859782400522922, (-571987398287808239)], [3209506304988606439]], [[(-69965698736238616), 73717229177342039, 9945455980784640, (-11695631902479186)], [(-155906855098749853), 10941888827806587, 23652172747942691], [(-185550781177854375), 20847118832545790], [(-193923068603169916)]], [[3661760249090066, (-3723383157812898), (-409477038199321), 187177392826268, 395106878210201], [8157545456971398, (-406770768345665), 389782357736189, (-2357853949209984)], [9818243516267699, (-1948023827298379), 3079594330376185], [11609472209944314, (-3058625917162619)], [11572340647851629]]], r := 488828812968632285, ok := true }, r3 := { p := [[[2905630866111993768564]], [[(-307072309573757781859), 210482734326529046734], [(-333052629770979023781)]], [[24645653243107966781, (-19250675560829814673), (-670498510572236519)], [35238389167948497545, (-7965750644874487659)], [24578556401307215535]], [[(-1783589672089588758), 1540836915395314912, 54244837338340434, 24523040135978043], [(-2889182085812061569), 937455425943236244, (-159577095089357664)], [(-2685424327588172838), 521978586961342974], [(-1618522604623099063)]], [[121889296162881475, (-112990570681318965), 1784699845891423, (-5937145360797741), (-56988097229437)], [212228315084672813, (-79954990325540368), 11428279623418946, 7091949664462277], [222140796971756679, (-49869100016504440), (-9896238922308826)], [176505157713600101, (-19341485457554319)], [97354208151253195]]], r := 193345459471748641117, ok := true }, eta := { p := [[[(-1113073923742324316291)]], [[66950886306931562537, 0], [69381964606815807109]], [[(-3749472393159108432), 0, 0], [(-4200438153012520846), 0], [(-4327437898454649829)]], [[203056543041411280, 0, 0, 0], [224033779687926489, 0, 0], [258422594973878709, 0], [248564089560878027]], [[(-10954407679896270), 0, 0, 0, 0], [(-11873037202856140), 0, 0, 0], [(-13803542121643332), 0, 0], [(-14637250063582225), 0], [(-13870168996832670)]]], r := 69373470376763520, ok := true } }
theorem sB_0 : stageB c0 w0 = true := by decide +kernel
theorem s0_0 : stageC0 w0 q0 = true := by decide +kernel
theorem s1_0 : stageC1 w0 q0 = true := by decide +kernel
theorem s2_0 : stageC2 w0 q0 = true := by decide +kernel
theorem s3_0 : stageC3 w0 q0 = true := by decide +kernel
theorem sE_0 : stageE w0 q0 = true := by decide +kernel
theorem sF_0 : stageF w0 = true := by decide +kernel
theorem ok_0 : (domOK c0 && cellCheck c0 q0) = true :=
  staged_check c0 q0 w0 (by decide +kernel) sB_0 s0_0 s1_0 s2_0 s3_0 sE_0 sF_0

noncomputable def c1 : Cell := { bc := 6052837899185946624, bh := 288230376151711744, tc := 8070450532247928832, th := 1152921504606846976, sc := 5080060379673919488, sh := 252201579132747776 }
noncomputable def q1 : Cert := { V0 := [[[2794109325877348063]], [[(-80892253463004796), 386063308151506889], [67681673042719289]], [[1129995599760893, (-10425397071677196), (-2698022783357744)], [(-1898714717813434), 8722816904445385], [312625330262942]], [[(-25047153932522), 113384077173857, 226772603713752, (-103807565228323)], [33102636137168, (-190740309961518), (-189738183355466)], [(-7252436476744), 17714730028145], [20085709205858]], [[626553953291, (-2034327870896), (-9194519043229), 7319962784114, 2388494777228], [(-943657430608), 1263652080682, 15407788331416, (-6124533643583)], [299439532659, 1196088349434, (-5095394774288)], [(-547247238919), 2208615330110], [(-146239865507)]]], r0 := 52568092518952, V1 := [[[5991189752945437154]], [[(-153125173082720327), 0], [128118175171547619]], [[1385257384753189, 0, 0], [(-2332833344659650), 0], [64108824070809]], [[(-24326094634124), 0, 0, 0], [4566402803193, 0, 0], [25963045365511, 0], [31958761370238]], [[559800519176, 0, 0, 0, 0], [(-242576996841), 0, 0, 0], [(-598081979351), 0, 0], [(-442591896879), 0], [(-582145215239)]]], r1 := 22263786675016, V2 := [[[9677006951888237288]], [[(-95992574901984462), 206217342108171087], [(-505196602954177525)]], [[1132314170844298, (-2983128931031047), (-3426025322347798)], [(-3069270185835969), 21950967527660007], [(-4734690618429052)]], [[(-19986443062176), (-39446385342717), 155581851513593, 35461125410638], [77670592310510, (-497613354271127), (-432227792077840)], [163521182684193, 563173847099919], [9574212863389]], [[465824196199, 965990249321, (-2215695897076), (-3309979529592), 67458182673], [(-1839419299597), 769095373347, 26946154307595, 2003288434248], [(-857809597835), (-31184118837216), (-5612079973919)], [5505293273353, (-11880636798705)], [2556188382722]]], r2 := 510769494656504, V3 := [[[13396408190342682555]], [[(-206666173712231883), 269780828826205404], [(-357793142777905708)]], [[2073384175610929, 3985618625642764, (-11936522443342718)], [(-11231644548895697), 35671839710729307], [(-7416805360694081)]], [[(-14147055839833), (-368766794639842), 212360826334076, 458308235448048], [273582689373143, 94003795343628, (-2178369859276370)], [35577364416149, 1656274957316571], [(-79706318461381)]], [[(-96710463200), 5973657938069, 18929746839170, (-27102508490617), (-14943126895523)], [(-3720918572042), (-53016969119515), 77482888017177, 99711990583509], [12558819453773, (-47166653377481), (-142591737503627)], [10603973912089, 24845155177371], [1715766731973]]], r3 := 10085087008459884, Vm := [[[11885437285997278685]], [[(-124816216107918678), 0], [(-254643722577169758)]], [[531819352238088, 0, 0], [(-6962459512232071), 0], [4102854803974699]], [[(-9259739402780), 0, 0, 0], [17075440037668, 0, 0], [(-20077020745409), 0], [92720287156196]], [[287464577655, 0, 0, 0, 0], [(-448661737959), 0, 0, 0], [(-1301640307858), 0, 0], [3073051047106, 0], [1455852338449]]], rm := 82302421266621 }
noncomputable def w1 : Wit := { Z0 := { p := [[[2841313887078494697]], [[(-85049072177897952), 405901983868356385], [71159638275668614]], [[1312601715326137, (-12149867453985422), 0], [(-2204684891885006), 10165662610809802], [415873555145839]], [[(-31182395392720), 187514530760876, 0, 0], [46996876622548, (-314954984555001), 0], [(-16353891449657), 59410507877977], [22724965381944]], [[821382333751, (-4454627913246), 0, 0, 0], [(-1445511720167), 6713839517506, 0, 0], [737960440490, (-2336270207094), 0], [(-781531425891), 3246423625992], [(-87154303689)]]], r := 6658203840133, ok := true }, Z1 := { p := [[[6494431741893702166]], [[(-194397879263766746), 0], [162650601772956832]], [[3000232492174027, 0, 0], [(-5039279752880014), 0], [950568126047632]], [[(-71274046611932), 0, 0, 0], [107421432280110, 0, 0], [(-37380323313501), 0], [51942778015872]], [[1877445334289, 0, 0, 0, 0], [(-3304026788952), 0, 0, 0], [1686766721120, 0, 0], [(-1786357544892), 0], [(-199209837002)]]], r := 5531872632877, ok := true }, Z2 := { p := [[[12230773409693134821]], [[(-188944228409795849), 405901983868356385], [(-994389226853146268)]], [[3689964162477883, (-12149867453985422), 0], [9338970309765294, 10165662610809802], [31152828005034564]], [[(-89372432782720), 187514530760876, 0, 0], [(-180777902694231), (-314954984555001), 0], [(-335187844271432), 59410507877977], [(-1490778873715823)]], [[2437812669923, (-4454627913246), 0, 0, 0], [3754746837406, 6713839517506, 0, 0], [4260182512772, (-2336270207094), 0], [15791043723140, 3246423625992], [64869413532665]]], r := 13863350252409, ok := true }, Z3 := { p := [[[23256251940468806335]], [[(-959568110714330605), 1252614666317724078], [(-1661263107914294081)]], [[42150662005859872, (-66407121336361304), 0], [60464826996513577, 18621267027088525], [63045531171885837]], [[(-1966390632782179), 2773053336749960, 0, 0], [(-2806845142588132), (-653408112890921), 0], [(-2602952067404372), (-144867165756281)], [(-2805121166707195)]], [[93435959981900, (-129021457814100), 0, 0, 0], [131946290941372, 22034993883485, 0, 0], [118180562141727, 11210276675478, 0], [115216711044761, 5009791028956], [127070633523330]]], r := 159892658353330, ok := true }, iE := { p := [[[27314791338515316724]], [[(-302240454492793884), 0], [(-616615667782432680)]], [[6915963482623262, 0, 0], [6105137450910521, 0], [33360624964909685]], [[(-169280108770907), 0, 0, 0], [(-33893586864879), 0, 0], [(-372504458126027), 0], [(-1370136171474442)]], [[4702342796135, 0, 0, 0, 0], [(-261075902597), 0, 0, 0], [7165229040740, 0, 0], [14347086058449, 0], [64406727208079]]], r := 14422127240133, ok := true }, iHu := { p := [[[42146761530893782661]], [[(-1439180396683058850), 0], [(-1380438339675587065)]], [[66150657886865882, 0, 0], [58368862226631067, 0], [60860809359469691]], [[(-3093063063515588), 0, 0, 0], [(-2600384118714095), 0, 0], [(-2494245991419645), 0], [(-2729569196876978)]], [[147328459934999, 0, 0, 0, 0], [123394061697385, 0, 0, 0], [115622446486389, 0, 0], [113526648183898, 0], [124707841034595]]], r := 156534839063073, ok := true }, T := { p := [[[8070450532247928832]], [[0, 1152921504606846976], [0]]], r := 0, ok := true }, E := { p := [[[12457805835079623180]], [[137846665234020550, 0], [281227784935333957]], [[(-1628966918580671), 0, 0], [3439169970057106, 0], [(-8866651293117427)]], [[24279025741214, 0, 0, 0], [(-85275571235346), 0, 0], [(-81794935674719), 0], [81261452569788]], [[(-609274123148), 0, 0, 0, 0], [1130809082378, 0, 0, 0], [(-403390329257), 0, 0], [1040382033724, 0], [(-2604523946765)]]], r := 2859756625675, ok := true }, de := { p := [[[(-30727615825771328862)]], [[726231129089135214, 0], [696589042187537858]], [[(-16236226846695832), 0, 0], [3435387298338245, 0], [(-14937869681112492)]], [[543256992308696, 0, 0, 0], [16942393828823, 0, 0], [16250867550096, 0], [479413940725938]], [[(-20205876265940), 0, 0, 0, 0], [83555268657, 0, 0, 0], [523607603549, 0, 0], [76873631180, 0], [(-17103492471511)]]], r := 7654913951141, ok := true }, dde := { p := [[[(-161885317265257024903)]], [[7238485460034408282, 0], [6943037073910554868]], [[(-363294798448395193), 0, 0], [(-352243094844942780), 0], [(-334243319355478953)]], [[18016493972308081, 0, 0, 0], [17243876000059754, 0, 0], [16540044326587926, 0], [15899212519332445]], [[(-894531635285689), 0, 0, 0, 0], [(-858295706684784), 0, 0, 0], [(-824326367099484), 0, 0], [(-789660648091077), 0], [(-757186418855132)]]], r := 362392930731722, ok := true }, nJu := { p := [[[(-61455231651542657723)]], [[1452462258178270428, 0], [1393178084375075717]], [[(-32472453693391663), 0, 0], [6870774596676491, 0], [(-29875739362224983)]], [[1086513984617392, 0, 0, 0], [33884787657647, 0, 0], [32501735100192, 0], [958827881451876]], [[(-40411752531880), 0, 0, 0, 0], [167110537314, 0, 0, 0], [1047215207099, 0, 0], [153747262360, 0], [(-34206984943021)]]], r := 15309827902273, ok := true }, Jd1 := { p := [[[(-323770634530514049806)]], [[14476970920068816565, 0], [13886074147821109736]], [[(-726589596896790385), 0, 0], [(-704486189689885559), 0], [(-668486638710957906)]], [[36032987944616163, 0, 0, 0], [34487752000119508, 0, 0], [33080088653175852, 0], [31798425038664891]], [[(-1789063270571377), 0, 0, 0, 0], [(-1716591413369568), 0, 0, 0], [(-1648652734198968), 0, 0], [(-1579321296182153), 0], [(-1514372837710263)]]], r := 724785861463435, ok := true }, term0 := { p := [[[2676886195286860512027]], [[(-236349660757412597331), 0], [(-201491140212636456655)]], [[17094992718499818308, 0, 0], [19009023453768054049, 0], [13300550421459659872]], [[(-1113346518466002282), 0, 0, 0], [(-1387362887827593599), 0, 0], [(-1270675528378640160), 0], [(-809307148994581940)]], [[68420993185184326, 0, 0, 0, 0], [91001105303353202, 0, 0, 0], [93413554840331576, 0, 0], [77989208534498812, 0], [46917724966713888]]], r := 45178124760791620, ok := true }, r0 := { p := [[[82769754583073532268]], [[(-4535480535937429365), 22503396281931770295], [(-1621643376691943164)]], [[221512164988271667, (-1172639671657653764), 1298627416628631400], [45294807121800150, (-492651278613433415)], [98246988609314163]], [[(-10137452105120157), 55505973101726958, (-51556416870564119), (-39142923842910936)], [(-604091020812390), 16515903860880283, (-42237166731771340)], [(-4672478190627466), 27009827136981954], [(-3840746856575567)]], [[461348274410940, (-2492043348037555), 2001922848458489, 3808213045211219, (-591155300798736)], [(-18600083110194), (-440196946718547), 1979791960736466, (-661958069503389)], [200157123546702, (-1208577453298143), 1678181472025160], [151654714803452, (-1108692392575242)], [184469226277629]]], r := 10187141030933808, ok := true }, r1 := { p := [[[360960076781590486757]], [[(-16761887993820741830), 0], [(-9663920245851487850)]], [[764106598559676917, 0, 0], [351938788792484492, 0], [467202579335640110]], [[(-34149848465660487), 0, 0, 0], [(-10756051496637171), 0, 0], [(-19923583237037623), 0], [(-19981496056883285)]], [[1554672954810303, 0, 0, 0, 0], [343652434422848, 0, 0, 0], [772428329600400, 0, 0], [786826110927600, 0], [924419567041339]]], r := 8457206232172348, ok := true }, r2 := { p := [[[339168153193622367779]], [[(-20234504365876591253), 26629108033284184749], [(-43384135922815683203)]], [[993996002681670868, (-1243971953060830055), 209191062799608312], [2421964176815557073, (-551548756397141928)], [2873941367475319685]], [[(-47017574493589568), 55302267747471016, 8470043269338433, (-11287395505514545)], [(-115720533726819240), 9578622100771770, 24229986984929567], [(-151703733865194495), 17392264770750599], [(-172927330522212986)]], [[2220039650805554, (-2514937976125604), (-332087241535637), 219246032864682, 345567805744676], [5464152556485302, (-283530085034073), 196009372104647, (-2143486472892442)], [7275279980095822, (-1524901813988613), 2817406440118861], [9490642592551717, (-2797288758480227)], [10346459521308962]]], r := 367627232251639532, ok := true }, r3 := { p := [[[2377522592805196338484]], [[(-226547955368306808651), 177350471533741277923], [(-272641064961631975067)]], [[16332513886139235904, (-14230246186226024057), (-555556237650939723)], [25827814869988174755, (-6370943360177147949)], [19982016949806322122]], [[(-1062146469884328519), 1014961437237418666, 60344885979964169, 12701955794644555], [(-1901805574711028377), 674878206815197826, (-135370439538429834)], [(-1961283104556854875), 433840745749141366], [(-1315883974261036793)]], [[65303188549374252, (-67059833224502679), 1258153336327932, (-5825416214626362), 790478146825101], [125871452200634561, (-53529523698480230), 12616071603668501, 3566162690125426], [146476068088032794, (-38980884133211584), (-6648778544354413)], [129399057509593501, (-16620254051375428)], [79201306713797473]]], r := 102082994779425732702, ok := true }, eta := { p := [[[(-992703767933529819513)]], [[54081026200272313257, 0], [61791380513491422919]], [[(-2753359050052326355), 0, 0], [(-3428939760841389052), 0], [(-3860534436355478562)]], [[134796856150576281, 0, 0, 0], [165643117179809625, 0, 0], [210863637217351568, 0], [222080557698580805]], [[(-6560296471583135), 0, 0, 0, 0], [(-7924794442506144), 0, 0, 0], [(-10217116195724674), 0, 0], [(-11978537427011369), 0], [(-12405080161982905)]]], r := 59541993092510197, ok := true } }
theorem sB_1 : stageB c1 w1 = true := by decide +kernel
theorem s0_1 : stageC0 w1 q1 = true := by decide +kernel
theorem s1_1 : stageC1 w1 q1 = true := by decide +kernel
theorem s2_1 : stageC2 w1 q1 = true := by decide +kernel
theorem s3_1 : stageC3 w1 q1 = true := by decide +kernel
theorem sE_1 : stageE w1 q1 = true := by decide +kernel
theorem sF_1 : stageF w1 = true := by decide +kernel
theorem ok_1 : (domOK c1 && cellCheck c1 q1) = true :=
  staged_check c1 q1 w1 (by decide +kernel) sB_1 s0_1 s1_1 s2_1 s3_1 sE_1 sF_1

noncomputable def c2 : Cell := { bc := 6052837899185946624, bh := 288230376151711744, tc := 8070450532247928832, th := 1152921504606846976, sc := 5836665117072162816, sh := 504403158265495552 }
noncomputable def q2 : Cert := { V0 := [[[2560973049928277192]], [[(-149454726634259590), 355755854344104461], [62259907754781434]], [[3736777461954396, (-19591634766063334), (-2093573613894378)], [(-3446104975833421), 8161490778979903], [293281594473197]], [[(-150996768255528), 388463779142044, 356616571683953, (-83570486218573)], [103317561188929, (-367274557328674), (-148559469190986)], [(-11459975823388), 20851993047392], [18533687791106]], [[6723060075829, (-12850384645314), (-28299993485185), 12379116896687, 1587296107706], [(-5525621374065), 4414730663122, 24372469438789, (-5156897298803)], [850508042520, 1818777543491, (-4063619645566)], [(-979289026616), 2128318410492], [(-130652201608)]]], r0 := 131868604613208, V1 := [[[5543666538124762937]], [[(-290831580654229403), 0], [121154732215467371]], [[4771099937281845, 0, 0], [(-4622644671365873), 0], [136779229417751]], [[(-150513230286393), 0, 0, 0], [10804232957776, 0, 0], [45067116108713, 0], [30655888679034]], [[6007602966368, 0, 0, 0, 0], [(-1419861415351), 0, 0, 0], [(-2193158276525), 0, 0], [(-854009179115), 0], [(-513436537112)]]], r1 := 80586207433528, V2 := [[[9398715206058340912]], [[(-179385679734388949), 196937292361209198], [(-513751795363442899)]], [[3897828171905411, (-6391978096107859), (-2979110111489827)], [(-5297322129363841), 20466894447208514], [(-4252787872962294)]], [[(-123175670256343), (-127409605544367), 284817332018679, 26628196611401], [252706341913657, (-982440879095094), (-357357335979053)], [314931033415860, 475795670986982], [24386935319185]], [[5005799728124, 5880559853647, (-8675937969844), (-5204918816323), 112706728248], [(-11268845210114), 5276195481423, 46104834886938, 821123658459], [(-4561680186981), (-54281374704341), (-2036658484494)], [8784373601000, (-13431161735893)], [2547891827013]]], r2 := 908451251653692, V3 := [[[12794681684852503425]], [[(-389232097055331269), 278577152726810198], [(-389125648005337828)]], [[7769178106768076, 3860663506720299, (-11151850359794082)], [(-19379342793757460), 35516005757034871], [(-7207490887160963)]], [[(-118723779130623), (-1268224716123712), 607177754323087, 376637836286912], [962506002859285, (-370639488050500), (-1927492015272231)], [201217360745594, 1497705402638368], [(-47222338472801)]], [[(-394683148095), 43928184783811, 47050357530061, (-53786475382624), (-10190360885719)], [(-28617057967549), (-161780883860207), 176036587405774, 74627105181313], [36811566171079, (-114600497433137), (-110056227301126)], [21758260411898, 12180388231608], [2774734050795]]], r3 := 21713360550984800, Vm := [[[11515546337726156985]], [[(-243694898015830625), 0], [(-275388378234069023)]], [[1847768334772376, 0, 0], [(-13741213783099680), 0], [4030772729146880]], [[(-51732319032692), 0, 0, 0], [55082053575507, 0, 0], [(-56052115085283), 0], [101660251871651]], [[3004407113981, 0, 0, 0, 0], [(-2366038462584), 0, 0, 0], [(-5399637135571), 0, 0], [5756767943265, 0], [1898681524240]]], rm := 360273936166383 }
noncomputable def w2 : Wit := { Z0 := { p := [[[2597199359454058215]], [[(-155870829286853500), 371028479922008316], [64932730276301712]], [[4282550493866736, (-22267261326693358), 0], [(-3915107436862787), 9276104325185958], [372746035434516]], [[(-185116417519766), 611792927695248, 0, 0], [144008537273433, (-559301062408970), 0], [(-25223634201280), 53249433633502], [20564290945581]], [[8698969819833, (-26445202502824), 0, 0, 0], [(-8232864933505), 20572648181919, 0, 0], [2092932057628, (-3603376314469), 0], [(-1329478274037), 2937755849368], [(-85206787805)]]], r := 16912446071380, ok := true }, Z1 := { p := [[[5936455678752133063]], [[(-356276181227093714), 0], [148417669202975342]], [[9788686843123968, 0, 0], [(-8948816998543512), 0], [851990938136038]], [[(-423123240045178), 0, 0, 0], [329162370910704, 0, 0], [(-57654021031497), 0], [47004093589899]], [[19883359588190, 0, 0, 0, 0], [(-18817976990867), 0, 0, 0], [4783844703151, 0, 0], [(-3038807483513), 0], [(-194758372126)]]], r := 18051186934710, ok := true }, Z2 := { p := [[[11694918647272293157]], [[(-337961364623373571), 371028479922008316], [(-967904785353120361)]], [[12000258141759454, (-22267261326693358), 0], [16693445312407564, 9276104325185958], [30183666189667891]], [[(-524851672946762), 611792927695248, 0, 0], [(-605308611652964), (-559301062408970), 0], [(-623065054895449), 53249433633502], [(-1445667908297461)]], [[25581146324030, (-26445202502824), 0, 0, 0], [22783258830676, 20572648181919, 0, 0], [14587941833638, (-3603376314469), 0], [28647896265656, 2937755849368], [62888306082315]]], r := 40604273848652, ok := true }, Z3 := { p := [[[20710427044124717892]], [[(-1502425182169839025), 1075300142512232636], [(-1502014291766560010)]], [[114023279351001879, (-105386494586335381), 0], [93219237247571463, 16835152366204737], [56167791215475440]], [[(-9247998336861962), 7508361713801149, 0, 0], [(-7571231188153476), (-1088881841221942), 0], [(-4041663971689207), (-114467807729504)], [(-2501529491072861)]], [[764070049856021, (-607814409927292), 0, 0, 0], [618269218432277, 59559154303166, 0, 0], [317290611882852, 18347317524482, 0], [177831773855334, 4345876817564], [113156423447795]]], r := 707074101459723, ok := true }, iE := { p := [[[26466092473653047105]], [[(-529717920978967479), 0], [(-598609820589859929)]], [[22451513157506090, 0, 0], [11795978817971250, 0], [32303602213237098]], [[(-988320743060353), 0, 0, 0], [(-138785055285328), 0, 0], [(-666813331294741), 0], [(-1328711651140021)]], [[49111786194027, 0, 0, 0, 0], [381383399402, 0, 0, 0], [23732296140636, 0, 0], [26587513997766, 0], [62403705518531]]], r := 55075659796537, ok := true }, iHu := { p := [[[38351493953568260177]], [[(-2224639185645065778), 0], [(-1225821592090138295)]], [[178806537758236613, 0, 0], [91116903519175985, 0], [54289865066953135]], [[(-14525956268715412), 0, 0, 0], [(-6983100984234910), 0, 0], [(-3847831154578423), 0], [(-2430232277682988)]], [[1203726714432125, 0, 0, 0, 0], [577975332197192, 0, 0, 0], [311449996034942, 0, 0], [175486887618382, 0], [110968224027940]]], r := 774501183286438, ok := true }, T := { p := [[[8070450532247928832]], [[0, 1152921504606846976], [0]]], r := 0, ok := true }, E := { p := [[[12857295320784094503]], [[257338318964858067, 0], [290806179752725835]], [[(-5756384925576066), 0, 0], [5910434522521659, 0], [(-9115721133850559)]], [[146611622389881, 0, 0, 0], [(-305869147736897), 0, 0], [(-168540142630535), 0], [84364201203180]], [[(-6431232139011), 0, 0, 0, 0], [6769556851346, 0, 0, 0], [(-1687352786671), 0, 0], [2055396478398, 0], [(-2681674411572)]]], r := 14731180945188, ok := true }, de := { p := [[[(-28681843659321323473)]], [[1283164770348820008, 0], [707049975498329392]], [[(-49022139208893913), 0, 0], [7078685990482492, 0], [(-14884273004283075)]], [[2867192037158111, 0, 0, 0], [70868817040178, 0, 0], [39050164491527, 0], [479689082502895]], [[(-185514614206154), 0, 0, 0, 0], [709508690657, 0, 0, 0], [2273783439153, 0, 0], [215423504993, 0], [(-17102077259619)]]], r := 73714909645227, ok := true }, dde := { p := [[[(-143016133315612700659)]], [[10927601752360787243, 0], [6021331577831454190]], [[(-958695394628540463), 0, 0], [(-536159467097265626), 0], [(-291082441767682620)]], [[82706705827309529, 0, 0, 0], [45414925110453381, 0, 0], [25024550571066151, 0], [13837058460326346]], [[(-7148929892404067), 0, 0, 0, 0], [(-3941581379356597), 0, 0, 0], [(-2176529929967615), 0, 0], [(-1196756695356494), 0], [(-659039999984226)]]], r := 2127226059098044, ok := true }, nJu := { p := [[[(-57363687318642646946)]], [[2566329540697640016, 0], [1414099950996658785]], [[(-98044278417787825), 0, 0], [14157371980964985, 0], [(-29768546008566149)]], [[5734384074316222, 0, 0, 0], [141737634080357, 0, 0], [78100328983054, 0], [959378165005791]], [[(-371029228412307), 0, 0, 0, 0], [1419017381314, 0, 0, 0], [4547566878306, 0, 0], [430847009987, 0], [(-34204154519238)]]], r := 147429819290445, ok := true }, Jd1 := { p := [[[(-286032266631225401318)]], [[21855203504721574486, 0], [12042663155662908381]], [[(-1917390789257080926), 0, 0], [(-1072318934194531252), 0], [(-582164883535365239)]], [[165413411654619058, 0, 0, 0], [90829850220906763, 0, 0], [50049101142132303, 0], [27674116920652692]], [[(-14297859784808133), 0, 0, 0, 0], [(-7883162758713194), 0, 0, 0], [(-4353059859935229), 0, 0], [(-2393513390712988), 0], [(-1318079999968451)]]], r := 4254452118196081, ok := true }, term0 := { p := [[[2096335319547238333464]], [[(-315613574796112374580), 0], [(-154879139522998236685)]], [[39619561040960743296, 0, 0], [25294026006891436242, 0], [10189500883137054005]], [[(-4480865219185825292), 0, 0, 0], [(-3201752677641710134), 0, 0], [(-1685141129664642592), 0], [(-618465212971795814)]], [[478701175025165185, 0, 0, 0, 0], [365173516295438532, 0, 0, 0], [215298507540658854, 0, 0], [103310573254185385, 0], [35798564952356052]]], r := 209202271939231119, ok := true }, r0 := { p := [[[70916068489770551194]], [[(-6875259848705417848), 19425757384211162257], [(-1491543733893275067)]], [[601889538374388557, (-1793056607905156013), 1160078768520379213], [82730100169229698, (-446789513257274993)], [85824589004962988]], [[(-48648339781715585), 152012786720758927, (-82740153411087551), (-29400863790045711)], [(-2719208903495010), 28290308890498817, (-36992956571878455)], [(-7339636245681250), 23770156776904292], [(-3427684244422206)]], [[3885451534248227, (-12020129096598308), 5753332456261379, 5511989335858414, (-539288419014668)], [(-7929767785554), (-1414309797017748), 3088847809551524, (-510874787591335)], [556546491753153, (-1929934188251167), 1514916561650902], [249961462419719, (-986650430895164)], [163158036334712]]], r := 26838482807926031, ok := true }, r1 := { p := [[[316739926816524017188]], [[(-25912614797660704311), 0], [(-8696467333880489285)]], [[2098805131631648227, 0, 0], [591182502583472435, 0], [413638099545866501]], [[(-164114974004564312), 0, 0, 0], [(-32746223353462371), 0, 0], [(-32012849409717944), 0], [(-17844568946170001)]], [[13028008024129646, 0, 0, 0, 0], [1890718027776948, 0, 0, 0], [2203881794993199, 0, 0], [1290001406384091, 0], [822951656669529]]], r := 33236678195896524, ok := true }, r2 := { p := [[[286298536578591592113]], [[(-30673325074058685066), 23335316262262335524], [(-37030599805377749165)]], [[2669338964312591336, (-1938657233985761546), 231884033087150013], [3702810590630809916, (-524977360540054182)], [2476144159444553467]], [[(-221620520779501330), 151051457125640700, 13481549562944157, (-10579030509074453)], [(-311269752288219618), 16494790879088849, 24477413072806987], [(-231750986328250958), 13561163529803519], [(-148056238131513819)]], [[18275674973080525, (-11955582693039066), (-998487714592106), 500045045159468, 279832908656158], [25675523504648894, (-684191250899379), (-35408514047694), (-1840749288503048)], [19519800037906246, (-2113805061966213), 2433830309420659], [14476062217811113, (-2446008330409698)], [8882683372163366]]], r := 620039336295949516, ok := true }, r3 := { p := [[[1820682974459441993957]], [[(-302947098140272112756), 142269474761306744556], [(-209411655111210833581)]], [[37894625140640166797, (-19169555676650400120), (-365579501433041567)], [34255709866904776305, (-4749858193295466379)], [15196737858044681619]], [[(-4274338876045543898), 2332894948966499964, 131072231495191570, (-3860031622900385)], [(-4365686629174099255), 855967492365755361, (-96781347572315565)], [(-2581147942157600570), 333988139333987038], [(-999171975966400130)]], [[456548833384334035, (-267896925162545221), 1961670851197004, (-10267424774893799), 1725634681084779], [503008990563437810, (-124791470313704830), 25694913375841200, (-932168622695100)], [336880438306057705, (-56850295399579950), (-2228221074798857)], [171485441562418732, (-14024172507297777)], [60274539666883467]]], r := 190610616344310713114, ok := true }, eta := { p := [[[(-852065081066670005641)]], [[81203682004644448547, 0], [52808274176534082457]], [[(-7295563280812333962), 0, 0], [(-5228650112646557917), 0], [(-3308406355396979558)]], [[625190363614100704, 0, 0, 0], [443143791539920765, 0, 0], [321142340175516471, 0], [190652270358041049]], [[(-53117494667565788), 0, 0, 0, 0], [(-37074003607814227), 0, 0, 0], [(-27389759515755935), 0, 0], [(-18320069854574697), 0], [(-10664134158458633)]]], r := 246620329823189434, ok := true } }
theorem sB_2 : stageB c2 w2 = true := by decide +kernel
theorem s0_2 : stageC0 w2 q2 = true := by decide +kernel
theorem s1_2 : stageC1 w2 q2 = true := by decide +kernel
theorem s2_2 : stageC2 w2 q2 = true := by decide +kernel
theorem s3_2 : stageC3 w2 q2 = true := by decide +kernel
theorem sE_2 : stageE w2 q2 = true := by decide +kernel
theorem sF_2 : stageF w2 = true := by decide +kernel
theorem ok_2 : (domOK c2 && cellCheck c2 q2) = true :=
  staged_check c2 q2 w2 (by decide +kernel) sB_2 s0_2 s1_2 s2_2 s3_2 sE_2 sF_2

theorem region : RegionPosI 5764607523034234880 6341068275337658368 6917529027641081856 9223372036854775808 4323455642275676160 6341068275337658368 :=
  (RegionPosI.split_s 5332261958806667264 (RegionPosI.split_s 4827858800541171712 (RegionPosI.of_check c0 q0 ok_0 5764607523034234880 6341068275337658368 6917529027641081856 9223372036854775808 4323455642275676160 4827858800541171712 (by decide +kernel)) (RegionPosI.of_check c1 q1 ok_1 5764607523034234880 6341068275337658368 6917529027641081856 9223372036854775808 4827858800541171712 5332261958806667264 (by decide +kernel))) (RegionPosI.of_check c2 q2 ok_2 5764607523034234880 6341068275337658368 6917529027641081856 9223372036854775808 5332261958806667264 6341068275337658368 (by decide +kernel)))

end CKLaneC.RSC2.BB_0047

end