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

import Definitions.Def_CK_CKLaneC_RSC2_BD_0234_part00

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

namespace CKLaneC.RSC2.BD_0234
open CKLaneC.TM3 CKLaneC.RSCell

theorem ok_3 : (domOK c3 && cellCheck c3 q3) = true :=
  staged_check c3 q3 w3 (by decide +kernel) sB_3 s0_3 s1_3 s2_3 s3_3 sE_3 sF_3

noncomputable def c4 : Cell := { bc := 8718968878589280256, bh := 72057594037927936, tc := 15852670688344145920, th := 288230376151711744, sc := 16176929861514821632, sh := 252201579132747776 }
noncomputable def q4 : Cert := { V0 := [[[931152486143647771]], [[(-104592805463835990), 16867871665234419], [6576440846352219]], [[163733977270346, (-1880750024650291), (-1688302019034)], [(-682216917756895), 118255182362084], [29107875610215]], [[(-4358151378366), 596266020944, 566900322006, (-10010747889)], [(-4788851415356), (-11972117136395), (-35644769419)], [(-2514606650037), 514124796629], [206465389791]], [[17375738504, 16316664091, (-63998582295), 3311777822, 2986091], [(-62613872622), (-133676405548), 11634091337, (-208233358)], [(-69637181821), (-40948234469), (-407274558)], [(-16408236143), 3608706653], [1125193590]]], r0 := 100928859236, V1 := [[[1082819301027180277]], [[(-121471233725185737), 0], [7637699166634540]], [[163656583308170, 0, 0], [(-788975725979984), 0], [33700328137392]], [[(-4000382173480), 0, 0, 0], [(-6097047416332), 0, 0], [(-2872309610509), 0], [238612742885]], [[14493658914, 0, 0, 0, 0], [(-55044897293), 0, 0, 0], [(-86360392146), 0, 0], [(-18597954265), 0], [1294928705]]], r1 := 44925070024, V2 := [[[1938011435886842545]], [[(-104301954123102807), 16559149852480763], [(-137076917230665074)]], [[154408979202945, (-1823929540189701), (-3409602426998)], [(-744641456714958), 173832699594756], [3787383822928]], [[(-4215607998303), (-1945669512323), 937886106514, (-8948204721)], [(-3368568207015), (-21021466480403), 173880714459], [392242703842, (-1013035651874)], [85694884513]], [[14335911591, 21832558114, (-82255194612), 2882708762, 5705839], [(-86527433937), 191620600638, (-32983839416), (-379226145)], [(-84255448436), 81226704759, 4724405950], [(-6260504542), (-12395440846)], [(-176796070)]]], r2 := 244730835988, V3 := [[[2863664598430869305]], [[(-207679014864706528), 32495302078690506], [(-129734914213155574)]], [[232916510787958, (-3466847307001510), (-19609274914154)], [(-1556304469357841), 368461730854685], [12226261247236]], [[(-6282565489413), (-21087303113041), 5662658572351, (-61336707956)], [(-3048875312174), (-45566092064892), 478922265453], [(-218081085897), (-1515611208115)], [199491095443]], [[(-5898852538), 580537877693, (-521242200887), 17915385241, 122654236], [(-175585110395), 393254465971, (-57971720472), (-3158582522)], [(-115725655671), 55993237516, 17686266525], [(-17647450290), (-22814897278)], [(-127447102)]]], r3 := 1287290078484, Vm := [[[2343962267191685313]], [[(-161140918734095880), 0], [(-116297492413130613)]], [[611675477610571, 0, 0], [(-2829027114270515), 0], [1038632490539155]], [[37294413026053, 0, 0, 0], [(-69141101270142), 0, 0], [(-16658021344989), 0], [51642671717446]], [[2585684972358, 0, 0, 0, 0], [(-2068856432162), 0, 0, 0], [(-6139871510633), 0, 0], [3956028535035, 0], [2332870160274]]], rm := 61484492121851 }
noncomputable def w4 : Wit := { Z0 := { p := [[[932867830864325434]], [[(-105171713952575190), 16961233288442280], [6612840648563864]], [[229912737039745, (-1912212980955913), 0], [(-694201133959272), 120233466337524], [29527036948532]], [[(-7067526655094), 4180231582540, 0, 0], [(-3483044423342), (-12621838799260), 0], [(-2647818366335), 536855217246], [210509178843]], [[37856513440, (-128500484639), 0, 0, 0], [(-109457320721), (-63328080425), 0, 0], [(-56129595769), (-48142152116), 0], [(-17646567102), 3827439615], [1160917397]]], r := 12653981820, ok := true }, Z1 := { p := [[[1085518930460305960]], [[(-122381630781178403), 0], [7694941845601587]], [[267534821282612, 0, 0], [(-807797683152607), 0], [34358733903746]], [[(-8224031016837), 0, 0, 0], [(-4052997147161), 0, 0], [(-3081097735372), 0], [244956135381]], [[44051215639, 0, 0, 0, 0], [(-127368518658), 0, 0, 0], [(-65314438713), 0, 0], [(-20534187173), 0], [1350885698]]], r := 8202030063, ok := true }, Z2 := { p := [[[1953594538661711387]], [[(-106834577383652310), 16961233288442280], [(-140405370584981517)]], [[296716393452108, (-1912212980955913), 0], [(-398527703155728), 120233466337524], [243197542319040]], [[(-7378054970379), 4180231582540, 0, 0], [(-12458620840127), (-12621838799260), 0], [(-10738657635060), 536855217246], [(-5940447108361)]], [[44775263362, (-128500484639), 0, 0, 0], [(-57862689574), (-63328080425), 0, 0], [(-126399876331), (-48142152116), 0], [(-43435434526), 3827439615], [20360486090]]], r := 19511537938, ok := true }, Z3 := { p := [[[2914536353008667832]], [[(-218908707272460339), 34252399430478608], [(-136749985919409374)]], [[1089770496263381, (-3918508603476285), 0], [(-585657125928202), 223341891874246], [342348762251764]], [[(-31905515227906), 17234914628965, 0, 0], [(-35576873355302), (-21680299303323), 0], [(-19807196635672), 831065195251], [(-5553647910631)]], [[297165720448, (-560191006932), 0, 0, 0], [(-138930234874), (-289377760218), 0, 0], [(-275318140328), (-48103911211), 0], [(-51646787320), 5527275358], [26743575452]]], r := 74423210410, ok := true }, iE := { p := [[[18664716942580771719]], [[(-30406645596838770), 0], [(-21944870759005290)]], [[1221552574397506, 0, 0], [1062793363716419, 0], [772136275488548]], [[(-5678232050912), 0, 0, 0], [10382684721275, 0, 0], [3880848188516, 0], [(-2169447039094)]], [[126514284292, 0, 0, 0, 0], [132268676569, 0, 0, 0], [198298401336, 0, 0], [82839022608, 0], [41156821952]]], r := 45366534029, ok := true }, iHu := { p := [[[18846251599220011569]], [[(-62001994628839756), 0], [(-32867645322726151)]], [[2593832076256337, 0, 0], [2237600049676875, 0], [728899610132228]], [[(-20023037196328), 0, 0, 0], [11030245530266, 0, 0], [5847202176021, 0], [(-2982762992847)]], [[483518898974, 0, 0, 0, 0], [528826636878, 0, 0, 0], [466080990901, 0, 0], [148606971504, 0], [38182571737]]], r := 109170156013, ok := true }, T := { p := [[[15852670688344145920]], [[0, 288230376151711744], [0]]], r := 0, ok := true }, E := { p := [[[18231316765626106343]], [[29700594408234697, 0], [21435304452724885]], [[(-1144802599860155), 0, 0], [(-968274585379902), 0], [(-729004681969000)]], [[1737567346768, 0, 0, 0], [(-16159071053064), 0, 0], [(-8566024678661), 0], [375199180620]], [[(-36786251288), 0, 0, 0, 0], [(-34922305822), 0, 0, 0], [(-94541820138), 0, 0], [(-9813609497), 0], [(-7110509269)]]], r := 34061517840, ok := true }, de := { p := [[[(-4596123152628262186)]], [[354313025664392692, 0], [187823551975575347]], [[(-806657947847219), 0, 0], [2072977972236066, 0], [(-226681082818793)]], [[22770472391063, 0, 0, 0], [22879120473320, 0, 0], [12128364926234, 0], [3392038965502]], [[(-147161080260), 0, 0, 0, 0], [252513128767, 0, 0, 0], [295330004582, 0, 0], [70959381988, 0], [(-11621031807)]]], r := 39832492291, ok := true }, dde := { p := [[[(-54829417827489113180)]], [[249658253932067509, 0], [132345402615700488]], [[(-10571090993771457), 0, 0], [(-9144311611431286), 0], [(-2970610231312010)]], [[91091839961615, 0, 0, 0], [(-29863713677110), 0, 0], [(-15830941488808), 0], [13569638138491]], [[(-2233704911899), 0, 0, 0, 0], [(-2477928432803), 0, 0, 0], [(-2093751826874), 0, 0], [(-696329220820), 0], [(-176391446588)]]], r := 997045196049, ok := true }, nJu := { p := [[[(-9192246305256524372)]], [[708626051328785385, 0], [375647103951150694]], [[(-1613315895694437), 0, 0], [4145955944472132, 0], [(-453362165637585)]], [[45540944782127, 0, 0, 0], [45758240946640, 0, 0], [24256729852469, 0], [6784077931005]], [[(-294322160520), 0, 0, 0, 0], [505026257534, 0, 0, 0], [590660009164, 0, 0], [141918763977, 0], [(-23242063614)]]], r := 79664984574, ok := true }, Jd1 := { p := [[[(-109658835654978226359)]], [[499316507864135019, 0], [264690805231400977]], [[(-21142181987542913), 0, 0], [(-18288623222862571), 0], [(-5941220462624019)]], [[182183679923230, 0, 0, 0], [(-59727427354220), 0, 0], [(-31661882977616), 0], [27139276276983]], [[(-4467409823798), 0, 0, 0, 0], [(-4955856865606), 0, 0, 0], [(-4187503653748), 0, 0], [(-1392658441640), 0], [(-352782893176)]]], r := 1994090392090, ok := true }, term0 := { p := [[[337830090168426428463]], [[(-2996685466450976883), 0], [(-1437646692353329480)]], [[136544209741999488, 0, 0], [107219722438650233, 0], [31595805594081700]], [[(-1683231410233463), 0, 0, 0], [(-254754081482180), 0, 0], [(-153098942134821), 0], [(-204324338991750)]], [[44789321137488, 0, 0, 0, 0], [47838410257960, 0, 0, 0], [34739646974204, 0, 0], [11855133296737, 0], [2732362871280]]], r := 8473866494002, ok := true }, r0 := { p := [[[81815238110998412289]], [[(-563273131821684716), 2957556203262526664], [(-177284140274934719)]], [[26883983687703411, (-16444131320935539), 26253099685204469], [12557097361988393, (-6655020574430390)], [3003867407601533]], [[(-235883024053723), 723920673740350, (-4528094111017), (-11372678212466)], [148260666135474, 499703952843020, (-67967519470046)], [17576910088016, 107182342964604], [(-15482045007219)]], [[6022793032126, (-5461791640599), (-2315537201004), 2567587252236, (-48308766669)], [4356579444706, 3440703828609, 6062006516518, (-131877620271)], [3653890985065, 1023627517071, 901515254939], [788143635834, (-579594026295)], [155190762966]]], r := 9380165215575, ok := true }, r1 := { p := [[[110551139557276358283]], [[(-709699714403268810), 0], [(-242784139985060658)]], [[33099741756079858, 0, 0], [17564858140790682, 0], [4040580069482758]], [[(-281695361020288), 0, 0, 0], [176023011578539, 0, 0], [28780379531660, 0], [(-21179901629507)]], [[7116597506417, 0, 0, 0, 0], [5564009895410, 0, 0, 0], [4807504390170, 0, 0], [1101837572866, 0], [208385997820]]], r := 4370009267205, ok := true }, r2 := { p := [[[84113406299564072273]], [[(-749942242346059165), 2942189250619336280], [(-603218318238568624)]], [[28312078813082349, (-15203293331059070), 25074591206619776], [39207461284222960, (-3651272658202245)], [17415359589840957]], [[(-279489474065819), 701533749651860, 107649973574467, (-16499878382107)], [(-100237185415662), 315518342728304, 117561029244087], [(-7378807778193), (-9589305144652)], [(-90745607950403)]], [[6473730534234, (-4791603121811), (-2515347934080), 2987650180128, (-39380640603)], [10471671528767, 7129350725454, (-8983358035067), 504921298675], [9820748385170, 2066937742150, (-1514254391599)], [4712054556079, (-411613037405)], [1473356586272]]], r := 26671363897312, ok := true }, r3 := { p := [[[339879141893794989533]], [[(-3970469671999817416), 11644657123857567663], [(-2161442463899660139)]], [[173657244674179826, (-39916398227677988), 90303019248850714], [156538157230564148, (-7958340130308431)], [51095618479839233]], [[(-2022544980897317), 2011112910806389, 2331923261312829, (-198349878419819)], [(-397731332247168), 702627171655662, 629553487957595], [(-198834254960788), 65611343857426], [(-318532032663807)]], [[52935446908257, (-19092584045701), (-92363293579144), 35491922247264, (-376875670530)], [64084118074178, 5243601009812, (-31972334631510), 1304210855083], [50396641278884, (-5466756018773), (-1910426012552)], [18833313970836, (-2229438641502)], [4539504428528]]], r := 520510040207020, ok := true }, eta := { p := [[[(-222680304499146461493)]], [[1511745788722449008, 0], [834684421554036294]], [[(-64939322361259919), 0, 0], [(-56811111805667815), 0], [(-20883694090297616)]], [[627671450094556, 0, 0, 0], [(-54915784666856), 0, 0], [10648296798461, 0], [118731616760776]], [[(-15550298862068), 0, 0, 0, 0], [(-17658677047503), 0, 0, 0], [(-15672917722014), 0, 0], [(-6235979119505), 0], [(-1772506165383)]]], r := 36090757125225288, ok := true } }
theorem sB_4 : stageB c4 w4 = true := by decide +kernel
theorem s0_4 : stageC0 w4 q4 = true := by decide +kernel
theorem s1_4 : stageC1 w4 q4 = true := by decide +kernel
theorem s2_4 : stageC2 w4 q4 = true := by decide +kernel
theorem s3_4 : stageC3 w4 q4 = true := by decide +kernel
theorem sE_4 : stageE w4 q4 = true := by decide +kernel
theorem sF_4 : stageF w4 = true := by decide +kernel
theorem ok_4 : (domOK c4 && cellCheck c4 q4) = true :=
  staged_check c4 q4 w4 (by decide +kernel) sB_4 s0_4 s1_4 s2_4 s3_4 sE_4 sF_4

noncomputable def c5 : Cell := { bc := 8863084066665136128, bh := 72057594037927936, tc := 15852670688344145920, th := 288230376151711744, sc := 16176929861514821632, sh := 252201579132747776 }
noncomputable def q5 : Cert := { V0 := [[[944423469327070915]], [[(-105967430113727314), 17106467710105864], [6695386596329307]], [[153872956224743, (-1904860100441071), (-1761252363179)], [(-692474494485779), 120355610876736], [30374331533156]], [[(-4487567260626), 321826742495, 590688176846, (-10436687594)], [(-5074593005006), (-12138990210172), (-37321710055)], [(-2614753964843), 536248476789], [215798315751]], [[16512807677, 17225337770, (-66528160963), 3447039894, 3203370], [(-66857144997), (-140823489879), 12158588784, (-217795834)], [(-73272525424), (-42495612071), (-431479924)], [(-16980515300), 3767735312], [1209001873]]], r0 := 105387988440, V1 := [[[1098231430594839229]], [[(-123060824436960495), 0], [7775406024135750]], [[151111134006853, 0, 0], [(-800690623550419), 0], [35163839800240]], [[(-4114808649600), 0, 0, 0], [(-6451406067999), 0, 0], [(-2985770372845), 0], [249352810876]], [[13614946131, 0, 0, 0, 0], [(-59443070613), 0, 0, 0], [(-90867014112), 0, 0], [(-19229181510), 0], [1391189563]]], r1 := 47580045476, V2 := [[[1663873433602058686]], [[(-105789717972418958), 16902664242167465], [(-137060745237025351)]], [[147332118574922, (-1865637049741616), (-3042884104012)], [(-743147252782072), 169632409526582], [4297087111741]], [[(-4391085720129), (-1548293676174), 867720619131, (-9708418630)], [(-3709634088250), (-20680792695787), 192863610455], [354954696226, (-1086954222315)], [84168959817]], [[14273487266, 21174338988, (-80298218597), 3146666351, 5339540], [(-88955581397), 205775025798, (-37192707212), (-380452891)], [(-86267905834), 89102034145, 4763393869], [(-6165058497), (-12240286727)], [(-204734497)]]], r2 := 243510796216, V3 := [[[2604245268807662253]], [[(-210792637574722732), 33225981006210098], [(-129683619682032611)]], [[226351506095559, (-3557738170179310), (-18580181590612)], [(-1557389093036073), 362126375406380], [13419820437260]], [[(-6638917331962), (-20253327173920), 5531992860883, (-67741728865)], [(-3518282615140), (-45316097127787), 550411519144], [(-324357255053), (-1651838849940)], [198307238686]], [[(-5453874829), 608108547034, (-530753278829), 20089202743, 122691097], [(-180748066077), 440882018691, (-72776535682), (-3243291982)], [(-118955372096), 69003809337, 18046893635], [(-17773943842), (-22587240260)], [(-168491809)]]], r3 := 1292028775680, Vm := [[[2115975450363305776]], [[(-166826107021141266), 0], [(-111440569289580087)]], [[449299218989371, 0, 0], [(-2831917014217060), 0], [1412661485025134]], [[30379641146719, 0, 0, 0], [(-92530978249893), 0, 0], [20022855782279, 0], [74527956197427]], [[2464358903067, 0, 0, 0, 0], [(-4974474486662), 0, 0, 0], [(-5026123786196), 0, 0], [8796251578273, 0], [3454368671874]]], rm := 96015832402491 }
noncomputable def w5 : Wit := { Z0 := { p := [[[946213323229179688]], [[(-106570849959580738), 17203878604166903], [6733512737008101]], [[222718302801763, (-1937651817446923), 0], [(-705006761322166), 122427504309238], [30818637581756]], [[(-7292180845642), 4049423687304, 0, 0], [(-3713334505917), (-12818304751313), 0], [(-2755655281092), 560338865122], [220140299282]], [[37104021214, (-132585106285), 0, 0, 0], [(-115261595022), (-67515172835), 0, 0], [(-59046858757), (-50102823293), 0], [(-18306572977), 4002550896], [1247878118]]], r := 13243067929, ok := true }, Z1 := { p := [[[1101048230666681819]], [[(-124009716316603041), 0], [7835360275791245]], [[259163115987507, 0, 0], [(-820371504083975), 0], [35861687367861]], [[(-8485446802202), 0, 0, 0], [(-4320971061430), 0, 0], [(-3206580690725), 0], [256163257346]], [[43175588322, 0, 0, 0, 0], [(-134122583298), 0, 0, 0], [(-68709072008), 0, 0], [(-21302194009), 0], [1452076356]]], r := 8680724010, ok := true }, Z2 := { p := [[[1673709379625283819]], [[(-107674946357046464), 17203878604166903], [(-139503239765712968)]], [[271277878958435, (-1937651817446923), 0], [(-442026509643008), 122427504309238], [208018060034284]], [[(-7503265186380), 4049423687304, 0, 0], [(-12987864637560), (-12818304751313), 0], [(-11016539730405), 560338865122], [(-5790232084456)]], [[42177630046, (-132585106285), 0, 0, 0], [(-67483197526), (-67515172835), 0, 0], [(-138357793405), (-50102823293), 0], [(-49230247121), 4002550896], [17221154102]]], r := 19672712270, ok := true }, Z3 := { p := [[[2642361765421669340]], [[(-220159681830590873), 34702452092253028], [(-135446402570463244)]], [[1017475625226063, (-3962063666909021), 0], [(-665542398550389), 226733280843231], [309645087835298]], [[(-32219772055369), 16640334437006, 0, 0], [(-36738207862334), (-21875788399101), 0], [(-20144664007747), 864833022186], [(-5351444009498)]], [[282493582822, (-572363486425), 0, 0, 0], [(-175775256722), (-305311348923), 0, 0], [(-305636636837), (-49640312365), 0], [(-60872087341), 5731020961], [23842762558]]], r := 75783197782, ok := true }, iE := { p := [[[18623899043740265761]], [[(-28264867775122581), 0], [(-18881055321606216)]], [[1243125149610786, 0, 0], [1079320887961929, 0], [760094150463486]], [[(-5403759122884), 0, 0, 0], [11197058552095, 0, 0], [4385535689968, 0], [(-1846702930989)]], [[129884386087, 0, 0, 0, 0], [142375151301, 0, 0, 0], [209051783435, 0, 0], [85461079895, 0], [39575278984]]], r := 47633499125, ok := true }, iHu := { p := [[[18783408648902470875]], [[(-57502211855225725), 0], [(-29986635450634556)]], [[2617785118482745, 0, 0], [2262782291998753, 0], [711902263218281]], [[(-18938375732236), 0, 0, 0], [12937281704341, 0, 0], [6746619611207, 0], [(-2685791513600)]], [[488169653673, 0, 0, 0, 0], [556384213265, 0, 0, 0], [487810979790, 0, 0], [151307751673, 0], [36103020407]]], r := 113834742956, ok := true }, T := { p := [[[15852670688344145920]], [[0, 288230376151711744], [0]]], r := 0, ok := true }, E := { p := [[[18271274244010240404]], [[27729700927665454, 0], [18523561526357645]], [[(-1177503386723504), 0, 0], [(-1002659854569163), 0], [(-726923199736972)]], [[1663459336047, 0, 0, 0], [(-16543981055138), 0, 0], [(-8627465149544), 0], [318777919417]], [[(-38257675270), 0, 0, 0, 0], [(-39231287722), 0, 0, 0], [(-97939844337), 0, 0], [(-10668882759), 0], [(-6998229772)]]], r := 36293464547, ok := true }, de := { p := [[[(-4221355818804838776)]], [[358508069464862395, 0], [186957169790619298]], [[(-759696662349346), 0, 0], [2122356426787834, 0], [(-206598230491636)]], [[23296213765837, 0, 0, 0], [24093201706959, 0, 0], [12564282887834, 0], [3303808843794]], [[(-141274907107), 0, 0, 0, 0], [273508427315, 0, 0, 0], [311886331906, 0, 0], [74380157119, 0], [(-10448111258)]]], r := 42643955389, ok := true }, dde := { p := [[[(-54576503694423279670)]], [[231300722247278563, 0], [120620237269486734]], [[(-10639307772528978), 0, 0], [(-9216020120789864), 0], [(-2893341867085392)]], [[86026409404674, 0, 0, 0], [(-38412003887707), 0, 0], [(-20031346975122), 0], [12200043107774]], [[(-2247549340788), 0, 0, 0, 0], [(-2590062739325), 0, 0, 0], [(-2182171043602), 0, 0], [(-704363208797), 0], [(-166219508130)]]], r := 1038224619626, ok := true }, nJu := { p := [[[(-8442711637609677551)]], [[717016138929724791, 0], [373914339581238597]], [[(-1519393324698692), 0, 0], [4244712853575668, 0], [(-413196460983272)]], [[46592427531675, 0, 0, 0], [48186403413919, 0, 0], [25128565775668, 0], [6607617687589]], [[(-282549814213), 0, 0, 0, 0], [547016854631, 0, 0, 0], [623772663813, 0, 0], [148760314238, 0], [(-20896222516)]]], r := 85287910769, ok := true }, Jd1 := { p := [[[(-109153007388846559340)]], [[462601444494557126, 0], [241240474538973468]], [[(-21278615545057955), 0, 0], [(-18432040241579728), 0], [(-5786683734170784)]], [[172052818809349, 0, 0, 0], [(-76824007775414), 0, 0], [(-40062693950243), 0], [24400086215548]], [[(-4495098681575), 0, 0, 0, 0], [(-5180125478650), 0, 0, 0], [(-4364342087204), 0, 0], [(-1408726417594), 0], [(-332439016260)]]], r := 2076449239248, ok := true }, term0 := { p := [[[335079588470823709306]], [[(-2782763976609548029), 0], [(-1313629565281161977)]], [[136174519596418178, 0, 0], [106748803254642296, 0], [30433807965422789]], [[(-1586592341535613), 0, 0, 0], [(-114471596809529), 0, 0], [(-82537390195112), 0], [(-183270866962787)]], [[44533096544721, 0, 0, 0, 0], [48850198806212, 0, 0, 0], [35436457750684, 0, 0], [11678342099415, 0], [2535316447696]]], r := 8579621618319, ok := true }, r0 := { p := [[[81472563891848361678]], [[(-538082316335918681), 2944670341567934697], [(-165449576102310666)]], [[27195325869886595, (-15440377376690379), 26120724595528581], [12636879319533668, (-6233073302383945)], [2914613118567648]], [[(-226907386820407), 731294303939210, 7689312085751, (-11641577492871)], [163186677860638, 504176083121594, (-64430275821133)], [22319027507114, 103833754233105], [(-14283466202309)]], [[6125154907667, (-5177310078985), (-2376123336448), 2620317164749, (-49351570311)], [4623724025236, 3936670506324, 6156917571728, (-137062566770)], [3811649385204, 1212777819656, 867453684426], [793101844073, (-537127922727)], [144627640116]]], r := 9706812445305, ok := true }, r1 := { p := [[[110081567444849499139]], [[(-674446047134816738), 0], [(-226869429036320177)]], [[33471294772119442, 0, 0], [17693232147849303, 0], [3918383632606728]], [[(-270239418818358), 0, 0, 0], [195671937214717, 0, 0], [35415359949745, 0], [(-19571487357113)]], [[7232931203950, 0, 0, 0, 0], [5897933222081, 0, 0, 0], [5020425431944, 0, 0], [1110572837151, 0], [193950784758]]], r := 4585340841936, ok := true }, r2 := { p := [[[82975928387942870061]], [[(-671519205690381836), 2934845174124545736], [(-534599481641639243)]], [[28151259567824458, (-14563794348128737), 25303567064276419], [39234363492155527, (-3694331854704892)], [16905450571261695]], [[(-258259236700783), 716030801958526, 89208826377651, (-15440030140253)], [(-60384096075919), 324077252612064, 111370679667703], [20806874887699, (-11881584828922)], [(-79351795878677)]], [[6431500058693, (-4685383903783), (-2527220520150), 2938927662144, (-43089141720)], [10771058073917, 7366307231173, (-9454915184033), 554818645772], [10117750952406, 2211863240684, (-1580472866347)], [4689009560529, (-352901073121)], [1377533533767]]], r := 25906743081074, ok := true }, r3 := { p := [[[335758162695280410375]], [[(-3658038847486699526), 11628985482947807376], [(-1960739898913586543)]], [[173064167333080054, (-38531809129834004), 91554131730350058], [155967208431456550, (-7721791242190805)], [49290604247698433]], [[(-1893566655494493), 2023746222412710, 2264313510026842, (-195382035567327)], [(-194891446625182), 682562076498241, 621382128796432], [(-87008956696025), 52874569809984], [(-283585734227796)]], [[52381136912415, (-17663523457348), (-97665367797201), 36396200932600, (-437216240897)], [64966076460970, 7390402985999, (-35638670558135), 1665076709534], [51078642283937, (-4566505195937), (-2175707943869)], [18464412427137, (-2017952768051)], [4204651088751]]], r := 510811504618564, ok := true }, eta := { p := [[[(-221093548556742990876)]], [[1398116319229415582, 0], [752518656485056831]], [[(-65112486321547552), 0, 0], [(-56843261029790998), 0], [(-20212899117809781)]], [[591754840260966, 0, 0, 0], [(-118584475439535), 0, 0], [(-26710787875859), 0], [105018726738985]], [[(-15601947674539), 0, 0, 0, 0], [(-18277675339070), 0, 0, 0], [(-16177445275165), 0, 0], [(-6223849192344), 0], [(-1658463061589)]]], r := 61455643211470693, ok := true } }
theorem sB_5 : stageB c5 w5 = true := by decide +kernel
theorem s0_5 : stageC0 w5 q5 = true := by decide +kernel
theorem s1_5 : stageC1 w5 q5 = true := by decide +kernel
theorem s2_5 : stageC2 w5 q5 = true := by decide +kernel
theorem s3_5 : stageC3 w5 q5 = true := by decide +kernel
theorem sE_5 : stageE w5 q5 = true := by decide +kernel
theorem sF_5 : stageF w5 = true := by decide +kernel
theorem ok_5 : (domOK c5 && cellCheck c5 q5) = true :=
  staged_check c5 q5 w5 (by decide +kernel) sB_5 s0_5 s1_5 s2_5 s3_5 sE_5 sF_5

theorem region : RegionPosI 8646911284551352320 8935141660703064064 14987979559889010688 16140901064495857664 15420325124116578304 16429131440647569408 :=
  (RegionPosI.split_s 15924728282382073856 (RegionPosI.split_t 15564440312192434176 (RegionPosI.of_check c0 q0 ok_0 8646911284551352320 8935141660703064064 14987979559889010688 15564440312192434176 15420325124116578304 15924728282382073856 (by decide +kernel)) (RegionPosI.of_check c1 q1 ok_1 8646911284551352320 8935141660703064064 15564440312192434176 16140901064495857664 15420325124116578304 15924728282382073856 (by decide +kernel))) (RegionPosI.split_t 15564440312192434176 (RegionPosI.split_b 8791026472627208192 (RegionPosI.of_check c2 q2 ok_2 8646911284551352320 8791026472627208192 14987979559889010688 15564440312192434176 15924728282382073856 16429131440647569408 (by decide +kernel)) (RegionPosI.of_check c3 q3 ok_3 8791026472627208192 8935141660703064064 14987979559889010688 15564440312192434176 15924728282382073856 16429131440647569408 (by decide +kernel))) (RegionPosI.split_b 8791026472627208192 (RegionPosI.of_check c4 q4 ok_4 8646911284551352320 8791026472627208192 15564440312192434176 16140901064495857664 15924728282382073856 16429131440647569408 (by decide +kernel)) (RegionPosI.of_check c5 q5 ok_5 8791026472627208192 8935141660703064064 15564440312192434176 16140901064495857664 15924728282382073856 16429131440647569408 (by decide +kernel)))))

end CKLaneC.RSC2.BD_0234