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

import Definitions.Def_CK_CKLaneC_RSC2_S02_0251_part00

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

namespace CKLaneC.RSC2.S02_0251
open CKLaneC.TM3 CKLaneC.RSCell

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

noncomputable def c6 : Cell := { bc := 3166593487994880, bh := 70368744177664, tc := 16140901064495857664, th := 2305843009213693952, sc := 17870283321406128128, sh := 576460752303423488 }
noncomputable def q6 : Cert := { V0 := [[[36670623595751264]], [[(-37193351918308720), 5238630646701301], [84142780910769]], [[531041582066040, (-5313245110256975), (-6400023567)], [(-85205443696520), 12020191678863], [(-741771035870)]], [[(-8452933446338), 75769612331699, 19473654531, (-304752783)], [1079574256735, (-12171581003256), (-44055387)], [751455217963, (-105965950147)], [10002423836]], [[142130516696, (-1173747118371), (-20029015779), 927264925, 1096], [(-17208891476), 153582491374, 133977305, (-2097759)], [(-9838311217), 107346666650, 287288], [(-10134309780), 1428901206], [(-157185614)]]], r0 := 1232840214770, V1 := [[[41909247537677348]], [[(-42506576627651961), 0], [96162926436504]], [[606790211737138, 0, 0], [(-97376884343259), 0], [(-847736685047)]], [[(-9619090092259), 0, 0, 0], [1233012542022, 0, 0], [858800968987, 0], [11431321344]], [[160726333113, 0, 0, 0, 0], [(-19383572480), 0, 0, 0], [(-11238648954), 0, 0], [(-11582006911), 0], [(-179640401)]]], r1 := 224685425056, V2 := [[[18440509928525415775]], [[(-99133551332878), 4661476830], [(-138536433543913)]], [[93060406812, (-4586475780), (-3326)], [(-2203329367879), 208404797], [806251]], [[(-1324625153), (-75062907), 6598, 0], [2306364003, (-205047236), (-223)], [(-4034252), 2346009], [(-17817)]], [[24185285, 62810, (-3219), 0, 0], [(-32385622), (-3360467), 442, 0], [3266535, (-2308100), (-5)], [35570, 279], [175]]], r2 := 3977380347, V3 := [[[18440608789653193940]], [[(-197903219030170), 9173380685], [(-136339851958161)]], [[299329301, (-8873995260), (-13090)], [(-4397649798825), 410114814], [(-4616439)]], [[69344, (-299317072), 25749, 0], [13398229, (-396714007), (-878)], [4465160, 4616458], [(-547)]], [[(-569), (-68914), (-12229), (-1), 0], [3454, (-13397409), 1728, 0], [151231, (-4465199), (-20)], [524, 547], [2]]], r3 := 22834439894, Vm := [[[18440509933220972096]], [[(-99138205900726), 0], [(-138536223528225)]], [[93019290119, 0, 0], [(-2203537633539), 0], [3172568]], [[(-1324496559), 0, 0, 0], [2304607737, 0, 0], [(-6382920), 0], [(-17516)]], [[24184919, 0, 0, 0, 0], [(-32379363), 0, 0, 0], [3248803, 0, 0], [35251, 0], [174]]], rm := 440080463 }
noncomputable def w6 : Wit := { Z0 := { p := [[[36670728130699468]], [[(-37193669994236897), 5238675447242781], [84143500496173]], [[531368735398949, (-5313381427748129), 0], [(-85207632064043), 12020500070881], [(-741775728325)]], [[(-8571290910656), 75909819342707, 0, 0], [1081822727887, (-12172518866292), 0], [751469493795, (-105967961190)], [10002481529]], [[147018057809, (-1224470130094), 0, 0, 0], [(-18019976896), 154546103983, 0, 0], [(-9852989946), 107352784827, 0], [(-10134485306), 1428925932], [(-157186469)]]], r := 295895102996, ok := true }, Z1 := { p := [[[41909403577942249]], [[(-42507051421985025), 0], [96164000567055]], [[607278554741656, 0, 0], [(-97380150930335), 0], [(-847743689515)]], [[(-9795761040750), 0, 0, 0], [1236368831871, 0, 0], [858822278623, 0], [11431407462]], [[168020637496, 0, 0, 0, 0], [(-20594259309), 0, 0, 0], [(-11260559938), 0, 0], [(-11582268921), 0], [(-179641678)]]], r := 55872755233, ok := true }, Z2 := { p := [[[7809833538435919645648]], [[(-111408577223975033302), 5238675447242781], [(-155690447354046282031)]], [[1795209599124358463, (-5313381427748129), 0], [2249055389311029598, 12020500070881], [3301675458391571321]], [[(-30765621806910582), 75909819342707, 0, 0], [(-36126651903492947), (-12172518866292), 0], [(-47913931384334895), (-105967961190)], [(-71239129351579113)]], [[553660156155631, (-1224470130094), 0, 0, 0], [613678313493255, 154546103983, 0, 0], [768889744295124, 107352784827, 0], [1036631880370391, 1428925932], [1549599431624386]]], r := 761937261988890, ok := true }, Z3 := { p := [[[7922643603343458763352]], [[(-229298510745364146393), 10628642323246229], [(-157968754436903545374)]], [[7059198843237669674, (-10936158501138403), 0], [4630703512290213038, 24347573524195], [3350219824395013720]], [[(-221110033684466231), 316983575896237, 0, 0], [(-143225297842496247), (-24970988624916), 0], [(-98666094632856391), (-214731868026)], [(-72289494155894561)]], [[6981884565167299, (-9763939815186), 0, 0, 0], [4498512763849254, 641721891340, 0, 0], [3057064482492517, 220416378222, 0], [2134843782230852, 2895938400], [1572491927911026]]], r := 4484353809452152, ok := true }, iE := { p := [[[7812479069536777250137]], [[(-111409633015999534038), 0], [(-155684377001510486659)]], [[1795294595873687877, 0, 0], [2249062763319843774, 0], [3301621944571170742]], [[(-30767613737879538), 0, 0, 0], [(-36126439744230910), 0, 0], [(-47913973824125671), 0], [(-71238407743983037)]], [[553703237018002, 0, 0, 0, 0], [613672282864308, 0, 0, 0], [768887951152087, 0, 0], [1036632359722361, 0], [1549588091743475]]], r := 761863718063514, ok := true }, iHu := { p := [[[7925290135281947074434]], [[(-229300681777396574040), 0], [(-157962691891096020635)]], [[7059403612095436346, 0, 0], [4630718714944803143, 0], [3350166356159875319]], [[(-221117600809406964), 0, 0, 0], [(-143225103357336771), 0, 0], [(-98666182312893473), 0], [(-72288773067232846)]], [[6982140353684538, 0, 0, 0, 0], [4498502254146193, 0, 0, 0], [3057062292493517, 0, 0], [2134844773374636, 0], [1572480595297098]]], r := 4484092397925098, ok := true }, T := { p := [[[16140901064495857664]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[43556259657424556]], [[621132787786269, 0], [867974056496798]], [[(-1151509214668), 0, 0], [12216427032820, 0], [(-1110569691386)]], [[12379760111, 0, 0, 0], [(-25593349755), 0, 0], [(-17630974276), 0], [8225051477]], [[(-199673555), 0, 0, 0, 0], [275105766, 0, 0, 0], [(-94596), 0, 0], [130556366, 0], [(-91389462)]]], r := 177317600, ok := true }, de := { p := [[[(-115787543837470878966)]], [[429313751566287589, 0], [295749473301220340]], [[(-6923263647104349), 0, 0], [1586787684843, 0], [(-3285558698699891)]], [[148887394379796, 0, 0, 0], [8513609, 0, 0], [5864930, 0], [48674945031205]], [[(-3602114380139), 0, 0, 0, 0], [46, 0, 0, 0], [94643, 0, 0], [22, 0], [(-811249083849)]]], r := 554031837638, ok := true }, dde := { p := [[[(-80029883797754946574515)]], [[2581179769609276501974, 0], [1778146063508612695888]], [[(-83263865839567696234), 0, 0], [(-57359553609864911790), 0], [(-39514358060160271811)]], [[2685931156102733458, 0, 0, 0], [1850308129742631546, 0, 0], [1274656711600480098, 0], [878096845777304729]], [[(-86642940519439354), 0, 0, 0, 0], [(-59687359024501159), 0, 0, 0], [(-41117958439286182), 0, 0], [(-28325704702493134), 0], [(-19513263239491514)]]], r := 8305589616253883, ok := true }, nJu := { p := [[[(-231575087674941757931)]], [[858627503132575179, 0], [591498946602440680]], [[(-13846527294208698), 0, 0], [3173575369687, 0], [(-6571117397399781)]], [[297774788759593, 0, 0, 0], [17027218, 0, 0], [11729861, 0], [97349890062410]], [[(-7204228760278), 0, 0, 0, 0], [93, 0, 0, 0], [189286, 0, 0], [45, 0], [(-1622498167698)]]], r := 1108063675268, ok := true }, Jd1 := { p := [[[(-160059767595509893149030)]], [[5162359539218553003949, 0], [3556292127017225391776]], [[(-166527731679135392467), 0, 0], [(-114719107219729823580), 0], [(-79028716120320543621)]], [[5371862312205466917, 0, 0, 0], [3700616259485263092, 0, 0], [2549313423200960196, 0], [1756193691554609459]], [[(-173285881038878707), 0, 0, 0, 0], [(-119374718049002317), 0, 0, 0], [(-82235916878572363), 0, 0], [(-56651409404986268), 0], [(-39026526478983028)]]], r := 16611179232507758, ok := true }, term0 := { p := [[[481489510998674445397775027]], [[(-31056091585970694132014259), 0], [(-21392360920276978184068363)]], [[1502589213224013389414451, 0, 0], [1379980238811209066342660, 0], [712999031307877083371544]], [[(-64624807110736880353996), 0, 0, 0], [(-66770461899100279235612), 0, 0], [(-45996113533599048041112), 0], [(-21124716986241199015183)]], [[2605774014195248246269, 0, 0, 0, 0], [2871788136258150694593, 0, 0, 0], [2225556719849318320759, 0, 0], [1362799989740156770026, 0], [586778023433941108548]]], r := 451119609972082515841, ok := true }, r0 := { p := [[[35509590873673769104927]], [[(-1524031528647970643754), 10145504052930972478155], [(-707881514894277516931)]], [[48863936488011395669, (-435244236885780356589), 724652192752576156578], [30766226695803201072, (-202250429020673033543)], [15014095484693906314]], [[(-1383289562091703354), 13854155982687933212, (-31033634394955542143), (-3809661294054181)], [(-984762138502405770), 8787381751921938238, (-14446049967908378922)], [(-655443129699306758), 4289713925034707470], [(-323981045537803646)]], [[36951049410039763, (-387947060919513745), 959021812343740950, 7891063737442178, (-136045505462095)], [27688618292942543, (-279715532077190667), 626821927783747661, 58463146232767], [20968062511881729, (-187212166715315900), 306400239833915963], [14180698009555891, (-92565450247646200)], [7047664806769294]]], r := 165315148330060775, ok := true }, r1 := { p := [[[46379743173651587069515]], [[(-1990301227102918340609), 0], [(-924577933331902044162)]], [[63672593148268100648, 0, 0], [40180304881123232548, 0], [19610208481048027386]], [[(-1796561733554793266), 0, 0, 0], [(-1283917812780604561), 0, 0], [(-856008800979447179), 0], [(-423158129081980868)]], [[47809198616745528, 0, 0, 0, 0], [36005709180102255, 0, 0, 0], [27342406677601461, 0, 0], [18520095393032623, 0], [9205096786640631]]], r := 15467126829307822, ok := true }, r2 := { p := [[[261513791142123555332499998]], [[(-9933878785969735717675803), 19642055016188708663116], [(-11549209242536791199605572)]], [[301070751215700738267340, (-527045062029815334520), 457591185997171416], [435409273654094982533761, (-437540034382424684767)], [383534039246187253273574]], [[(-8610132267449908100635), 13391435041329493891, 199401995977405, (-422336486998)], [(-13087298820518435248433), 11588764983468897486, 89872000747064], [(-14392777795624073560457), 9731741518469339252], [(-11334337939888589863848)]], [[244356479985253078452, (-338990081468453034), (-6518982411515), (-237388132084), (-34138805928)], [371227018877266937125, (-289888047252598705), (-3086618877679), (-64213053900)], [430403215665830371757, (-256447901498502374), (-1778708554420)], [423948385052716202818, (-216372470224699765)], [314218970645011950544]]], r := 2211539056111537707648, ok := true }, r3 := { p := [[[962573473545708885740625368]], [[(-62092448176290634358731092), 80264727269504804825136], [(-42775706044676691012886402)]], [[3004327206571323514516768, (-3914863229378200658444), 1829558384276614649], [2759521747073657935652155, (-1788492893138226368707)], [1425797671643113893563717]], [[(-129215232899931883477578), 168993395802057479774, 1636149259384496, (-2936299958408)], [(-133522001351059456113123), 87171967053775741635, 350545518969175], [(-91982476121898943259596), 39784204660816149345], [(-42244980345278954285969)]], [[5210215634874914724965, (-6828891092628347849), (-45644981002027), (-138067088307), (-146334680107)], [5742811993843574270395, (-3761880140247362695), (-1290779735769), (-486373981816)], [4450692874694685052643, (-1938539922662822803), (-16271151035871)], [2725383267383618841893, (-884601804949211539)], [1173457062689684880188]]], r := 44169417197011009890774, ok := true }, eta := { p := [[[(-261625128797357717567625018)]], [[9938757402680474760112670, 0], [11551654930684578441019906]], [[(-301247269217488197629313), 0, 0], [(-435516499638935876685173), 0], [(-383588153205628476767072)]], [[8616110128027330533572, 0, 0, 0], [13091173702003655026104, 0, 0], [14395150178105853524683, 0], [11335537354009491835589]], [[(-244553453043835251153), 0, 0, 0, 0], [(-371358089669906108497), 0, 0, 0], [(-430488907889392138794), 0, 0], [(-424000968531830598344), 0], [(-314245576494818407879)]]], r := 241302822622591400756, ok := true } }
theorem sB_6 : stageB c6 w6 = true := by decide +kernel
theorem s0_6 : stageC0 w6 q6 = true := by decide +kernel
theorem s1_6 : stageC1 w6 q6 = true := by decide +kernel
theorem s2_6 : stageC2 w6 q6 = true := by decide +kernel
theorem s3_6 : stageC3 w6 q6 = true := by decide +kernel
theorem sE_6 : stageE w6 q6 = true := by decide +kernel
theorem sF_6 : stageF w6 = true := by decide +kernel
theorem ok_6 : (domOK c6 && cellCheck c6 q6) = true :=
  staged_check c6 q6 w6 (by decide +kernel) sB_6 s0_6 s1_6 s2_6 s3_6 sE_6 sF_6

noncomputable def c7 : Cell := { bc := 3307330976350208, bh := 70368744177664, tc := 16140901064495857664, th := 2305843009213693952, sc := 17870283321406128128, sh := 576460752303423488 }
noncomputable def q7 : Cert := { V0 := [[[36836019660588879]], [[(-37360835594824995), 5262258250010318], [81290901332728]], [[533162416449973, (-5337170115206517), (-6487012623)], [(-82316346049162), 11612785483076], [(-685325644531)]], [[(-8486740520938), 76071320242055, 19738196592, (-308894886)], [1041763842398, (-11758868504103), (-42947001)], [694265834669, (-97902416141)], [8844856378]], [[142725933023, (-1178119178785), (-20300812116), 939860984, 1121], [(-16606212075), 148197183685, 130605306, (-2044981)], [(-9082477654), 99177038703, 267289], [(-8961395716), 1263536234], [(-133051818)]]], r0 := 1132240008908, V1 := [[[42098271114692848]], [[(-42697985031979790), 0], [92903641823840]], [[609212469295088, 0, 0], [(-94075077729307), 0], [(-783227780651)]], [[(-9657166532086), 0, 0, 0], [1189820452148, 0, 0], [793442021489, 0], [10108389321]], [[161384519017, 0, 0, 0, 0], [(-18701957128), 0, 0, 0], [(-10375196718), 0, 0], [(-10241540434), 0], [(-152058965)]]], r1 := 200719747265, V2 := [[[18440232855661413162]], [[(-103540225926578), 5087672673], [(-138536430527262)]], [[97686059923, (-5005804822), (-3793)], [(-2203345088970), 217792145], [703394]], [[(-1389551466), (-81935665), 7524, 0], [2319219953, (-214282882), (-244)], [(-3828943), 2347656], [(-16496)]], [[25368002, 68857, (-3670), 0, 0], [(-32539811), (-3512314), 483, 0], [3162785, (-2309714), (-5)], [32920, 270], [155]]], r2 := 3668526880, V3 := [[[18440336109930807527]], [[(-206698500763016), 10012080487], [(-136339870430406)]], [[326730857, (-9685288235), (-14927)], [(-4397631931956), 428587141], [(-4619668)]], [[76447, (-326716913), 29363, 0], [14003414, (-414581035), (-959)], [4468258, 4619688], [(-530)]], [[(-626), (-75957), (-13945), 0, 0], [3648, (-14002518), 1886, 0], [151360, (-4468299), (-20)], [508, 530], [2]]], r3 := 21823334642, Vm := [[[18440232860786468518]], [[(-103545306422945), 0], [(-138536211042728)]], [[97641359902, 0, 0], [(-2203562753082), 0], [3071491]], [[(-1389410018), 0, 0, 0], [2317392956, 0, 0], [(-6179491), 0], [(-16204)]], [[25367596, 0, 0, 0, 0], [(-32533216), 0, 0, 0], [3145152, 0, 0], [32611, 0], [154]]], rm := 414838646 }
noncomputable def w7 : Wit := { Z0 := { p := [[[36836125616386326]], [[(-37361157991748723), 5262303659483760], [81291602814270]], [[533494009412768, (-5337308284535532), 0], [(-82318479339542), 11613086116324], [(-685330010332)]], [[(-8606699439595), 76213429916109, 0, 0], [1043955682271, (-11759782762792), 0], [694279116660, (-97904287191)], [8844907741]], [[147677275829, (-1229528491371), 0, 0, 0], [(-17396827292), 149136526038, 0, 0], [(-9096134360), 99182730951, 0], [(-8961551982), 1263558248], [(-133052547)]]], r := 270608808955, ok := true }, Z1 := { p := [[[42098429275870087]], [[(-42698466276284255), 0], [92904688930594]], [[609707439328877, 0, 0], [(-94078262102333), 0], [(-783234297522)]], [[(-9836227930965), 0, 0, 0], [1193092208309, 0, 0], [793461847612, 0], [10108465990]], [[168774029519, 0, 0, 0, 0], [(-19882088334), 0, 0, 0], [(-10395582126), 0, 0], [(-10241773694), 0], [(-152060053)]]], r := 49880679350, ok := true }, Z2 := { p := [[[7511113187949791008660]], [[(-107094175427630764784), 5262303659483760], [(-143291601512683117514)]], [[1725904399609483193, (-5337308284535532), 0], [2069153882557581246, 11613086116324], [2908889684433833698]], [[(-29588189139725153), 76213429916109, 0, 0], [(-33239615206413297), (-11759782762792), 0], [(-42199240791284623), (-97904287191)], [(-60086686694677249)]], [[532724852625315, (-1229528491371), 0, 0, 0], [564786562376347, 149136526038, 0, 0], [677232617074486, 99182730951, 0], [874063707283122, 1263558248], [1251296331165129]]], r := 648073311815976, ok := true }, Z3 := { p := [[[7619552764157925852163]], [[(-220415402584437869245), 10676501006087564], [(-145387641024463205195)]], [[6784468914332393245, (-10985241876654106), 0], [4260245740681527843, 23522000394144], [2951643683846365925]], [[(-212481519847602106), 318244225622333, 0, 0], [(-131747821797739622), (-24123569068059), 0], [(-86897294694352796), (-198389669058)], [(-60972320246537808)]], [[6708908748309870, (-9800990493536), 0, 0, 0], [4137652119254378, 619227598537, 0, 0], [2692055959748038, 203637378128, 0], [1800032597335389, 2560770569], [1269776006720199]]], r := 3932873221704959, ok := true }, iE := { p := [[[7513770651297830307945]], [[(-107095216637665522711), 0], [(-143285736904194373749)]], [[1725989813690611950, 0, 0], [2069161092353929525, 0], [2908840242768802673]], [[(-29590192937325768), 0, 0, 0], [(-33239409943755006), 0, 0], [(-42199280507195444), 0], [(-60086048597761610)]], [[532768216198496, 0, 0, 0, 0], [564780723890876, 0, 0, 0], [677230959158680, 0, 0], [874064137142130, 0], [1251286732374291]]], r := 648001313638165, ok := true }, iHu := { p := [[[7622211212908441655641]], [[(-220417543554166325122), 0], [(-145381784046365063297)]], [[6784674063647319627, 0, 0], [4260260604084482132, 0], [2951594284818770679]], [[(-212489107586209674), 0, 0, 0], [(-131747635706225903), 0, 0], [(-86897376742477447), 0], [(-60971682614666094)]], [[6709165299966285, 0, 0, 0, 0], [4137642009798492, 0, 0, 0], [2692053949085352, 0, 0], [1800033486085117, 0], [1269766414168431]]], r := 3932589505067291, ok := true }, T := { p := [[[16140901064495857664]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[45287829867705976]], [[645496139796863, 0], [863627648025854]], [[(-1202696292564), 0, 0], [12147424886338, 0], [(-1063319395735)]], [[12929971640, 0, 0, 0], [(-25593728142), 0, 0], [(-16880969625), 0], [7539940786]], [[(-208547935), 0, 0, 0, 0], [275105764, 0, 0, 0], [(-94597), 0, 0], [119681594, 0], [(-80212137)]]], r := 175437231, ok := true }, de := { p := [[[(-115208810261043924362)]], [[429316925165117169, 0], [283166482555715580]], [[(-6923263629698556), 0, 0], [1586811144824, 0], [(-3011886078832193)]], [[148887394379892, 0, 0, 0], [8892189, 0, 0], [5865060, 0], [42721789641711]], [[(-3602114380139), 0, 0, 0, 0], [50, 0, 0, 0], [94647, 0, 0], [22, 0], [(-681730685768)]]], r := 539562850009, ok := true }, dde := { p := [[[(-76624923254797940433613)]], [[2471342326391418837386, 0], [1630034300385829444188]], [[(-79720722612403171364), 0, 0], [(-52581754799522939470), 0], [(-34681581906074895200)]], [[2571636213289851482, 0, 0, 0], [1696185587471261196, 0, 0], [1118760706629983557, 0], [737905997997727576]], [[(-82956006880314284), 0, 0, 0, 0], [(-54715664112549127), 0, 0, 0], [(-36089055053143622), 0, 0], [(-23803419290248723), 0], [(-15700127616970540)]]], r := 7465600081204247, ok := true }, nJu := { p := [[[(-230417620522087848724)]], [[858633850330234339, 0], [566332965111431161]], [[(-13846527259397112), 0, 0], [3173622289649, 0], [(-6023772157664385)]], [[297774788759785, 0, 0, 0], [17784378, 0, 0], [11730121, 0], [85443579283422]], [[(-7204228760278), 0, 0, 0, 0], [101, 0, 0, 0], [189295, 0, 0], [45, 0], [(-1363461371536)]]], r := 1079125700009, ok := true }, Jd1 := { p := [[[(-153249846509595880867226)]], [[4942684652782837674773, 0], [3260068600771658888377]], [[(-159441445224806342728), 0, 0], [(-105163509599045878940), 0], [(-69363163812149790399)]], [[5143272426579702965, 0, 0, 0], [3392371174942522393, 0, 0], [2237521413259967115, 0], [1475811995995455153]], [[(-165912013760628568), 0, 0, 0, 0], [(-109431328225098254), 0, 0, 0], [(-72178110106287244), 0, 0], [(-47606838580497445), 0], [(-31400255233941079)]]], r := 14931200162408485, ok := true }, term0 := { p := [[[441396699996037361054123240]], [[(-28469788130318648313353940), 0], [(-18776262746498586624802295)]], [[1377450812343863155949825, 0, 0], [1211214044867099526761754, 0], [599172505544947684842997]], [[(-59242624593630208405116), 0, 0, 0], [(-58604586924327677230229), 0, 0], [(-38652934398199156996585), 0], [(-16996809766606102949832)]], [[2388753290802470238794, 0, 0, 0, 0], [2520572678930623676674, 0, 0, 0], [1870249143749595090333, 0, 0], [1096496961781226386217, 0], [452026986200075219323]]], r := 384587632500793897702, ok := true }, r0 := { p := [[[34151400418255351675068]], [[(-1465012139593033041115), 9757452395606314299945], [(-651499085687776016923)]], [[46974807869728982822, (-418387271527712008082), 696935005369233533254], [28305247060091203494, (-186141267704832785401)], [13227794336494242040]], [[(-1330167241946626743), 13317573018912149903, (-29831198911722242036), (-3697071496278757)], [(-906032213512646276), 8084460648763356516, (-13295425351362210077)], [(-577268510156841043), 3779345281874702872], [(-273259340731226299)]], [[35546080222659746, (-372988080465285739), 921599584523641148, 7657717350115129, (-132024728575038)], [25480351946448950, (-257340971086047131), 576674972647725614, 54211322474542], [18467941204129188, (-164883015536498148), 269946226307942056], [11956832632301443, (-78073619368923946)], [5690912998242693]]], r := 150917309073241870, ok := true }, r1 := { p := [[[44605783990135745381170]], [[(-1913222678885585090839), 0], [(-850935722596678577624)]], [[61209593247507239801, 0, 0], [36966266315190366856, 0], [17277084807778614184]], [[(-1727483667332271188), 0, 0, 0], [(-1181254403277710480), 0, 0], [(-753912207823724915), 0], [(-356909490426358436)]], [[45987869355353843, 0, 0, 0, 0], [33133055927304471, 0, 0, 0], [24081950320490296, 0, 0], [15615700868100226, 0], [7433015863694358]]], r := 13472363274264057, ok := true }, r2 := { p := [[[239863607098954020158098674]], [[(-9117417859999717597288851), 18804244643159861327164], [(-10141660144015264390032593)]], [[276522006600434655607073, (-504849768552344400586), 457773674742428917], [382573853891693457179294, (-401063701143812050609)], [322448521024579370374461]], [[(-7913571245842967353087), 12836085552136303276, 203823710612446, (-422890150239)], [(-11506813300594871318933), 10627369788564134712, 88359439533943], [(-12107333821202985912049), 8540943820122976576], [(-9123412383431643283649)]], [[224727981944938030483, (-325165488565344707), (-3486453966094), (-158022524060), (-30060974193)], [326610019363446278796, (-265986179568393674), (-1036283050424), (-57554917677)], [362288465872852750421, (-225156735930615396), (-1649919804048)], [341438296297728314043, (-181814848624985589)], [242159131297007255006]]], r := 1795317406257244204162, ok := true }, r3 := { p := [[[882405115681246915165622808]], [[(-56920681382138661077633903), 76840102814709876775139], [(-37544260817513544206378507)]], [[2754086639115107167706269, (-3747943335863254242618), 1830273688763793347], [2422025908501924414292151, (-1639375138263779855518)], [1198169131428773138590647]], [[(-118452331346440644915976), 161790004824357613841, 1659716823706922, (-2993531414129)], [(-117191827733019073560140), 79905942365115831498, 344637974325299], [(-77297310532326177357875), 34915796641840039771], [(-33989876996121468557837)]], [[4776230896215558302210, (-6537850155943208179), (-49354198821191), 593863895141, (-128866030972)], [5040444747256765438776, (-3448337483552734558), 5663849402480, (-435803304874)], [3740129167316910593937, (-1701363725611559211), (-14940387577626)], [2192811803575557715493, (-743324866999900060)], [903974327948039321295]]], r := 36944448719157533587037, ok := true }, eta := { p := [[[(-239970260645991604592332580)]], [[9122091111514983173875869, 0], [10143902962787770431805371]], [[(-276691103051438211348591), 0, 0], [(-382672185937129959612844), 0], [(-322496032747284867172693)]], [[7919298066283928801710, 0, 0, 0], [11510366925901362341073, 0, 0], [12109416774539332665412, 0], [9124420626125550946375]], [[(-224916688828555524025), 0, 0, 0, 0], [(-326730226766457372688), 0, 0, 0], [(-362363707974366671591), 0, 0], [(-341482497221680195736), 0], [(-242180545687700903433)]]], r := 197043549639778008557, ok := true } }
theorem sB_7 : stageB c7 w7 = true := by decide +kernel
theorem s0_7 : stageC0 w7 q7 = true := by decide +kernel
theorem s1_7 : stageC1 w7 q7 = true := by decide +kernel
theorem s2_7 : stageC2 w7 q7 = true := by decide +kernel
theorem s3_7 : stageC3 w7 q7 = true := by decide +kernel
theorem sE_7 : stageE w7 q7 = true := by decide +kernel
theorem sF_7 : stageF w7 = true := by decide +kernel
theorem ok_7 : (domOK c7 && cellCheck c7 q7) = true :=
  staged_check c7 q7 w7 (by decide +kernel) sB_7 s0_7 s1_7 s2_7 s3_7 sE_7 sF_7

theorem region : RegionPosI 2814749767106560 3377699720527872 13835058055282163712 18446744073709551616 16140901064495857664 18446744073709551616 :=
  (RegionPosI.split_b 3096224743817216 (RegionPosI.split_s 17293822569102704640 (RegionPosI.split_b 2955487255461888 (RegionPosI.of_check c0 q0 ok_0 2814749767106560 2955487255461888 13835058055282163712 18446744073709551616 16140901064495857664 17293822569102704640 (by decide +kernel)) (RegionPosI.of_check c1 q1 ok_1 2955487255461888 3096224743817216 13835058055282163712 18446744073709551616 16140901064495857664 17293822569102704640 (by decide +kernel))) (RegionPosI.split_b 2955487255461888 (RegionPosI.of_check c2 q2 ok_2 2814749767106560 2955487255461888 13835058055282163712 18446744073709551616 17293822569102704640 18446744073709551616 (by decide +kernel)) (RegionPosI.of_check c3 q3 ok_3 2955487255461888 3096224743817216 13835058055282163712 18446744073709551616 17293822569102704640 18446744073709551616 (by decide +kernel)))) (RegionPosI.split_s 17293822569102704640 (RegionPosI.split_b 3236962232172544 (RegionPosI.of_check c4 q4 ok_4 3096224743817216 3236962232172544 13835058055282163712 18446744073709551616 16140901064495857664 17293822569102704640 (by decide +kernel)) (RegionPosI.of_check c5 q5 ok_5 3236962232172544 3377699720527872 13835058055282163712 18446744073709551616 16140901064495857664 17293822569102704640 (by decide +kernel))) (RegionPosI.split_b 3236962232172544 (RegionPosI.of_check c6 q6 ok_6 3096224743817216 3236962232172544 13835058055282163712 18446744073709551616 17293822569102704640 18446744073709551616 (by decide +kernel)) (RegionPosI.of_check c7 q7 ok_7 3236962232172544 3377699720527872 13835058055282163712 18446744073709551616 17293822569102704640 18446744073709551616 (by decide +kernel)))))

end CKLaneC.RSC2.S02_0251