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

import Definitions.Def_CK_CKLaneC_RSC2_S01_0272_part01

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

namespace CKLaneC.RSC2.S01_0272
open CKLaneC.TM3 CKLaneC.RSCell

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 := 2146246697418752, bh := 35184372088832, tc := 16140901064495857664, th := 2305843009213693952, sc := 10088063165309911040, sh := 288230376151711744 }
noncomputable def q6 : Cert := { V0 := [[[637538249766781016]], [[(-27993235814976080), 90920017535633990], [1015742393535268]], [[271733669263883, (-3978375678213767), (-33547865118753)], [(-43836434338984), 144356474559808], [(-6708438373693)]], [[(-2981839329966), 37712207756543, 4411735619614, (-1581298606622)], [403144101389, (-6164223123414), (-160081061281)], [290854872212, (-954591081422)], [67053639858]], [[35833923276, (-392955737504), (-235730344314), 206526719292, 1728866365], [(-4716809822), 52377801717, 20907855835, (-7493879793)], [(-2718128283), 41056883653, 803267273], [(-2911318569), 9544739049], [(-779545125)]]], r0 := 513375777266, V1 := [[[728423139915600755]], [[(-31966993619516935), 0], [1159931307256862]], [[309199305160494, 0, 0], [(-49978785240848), 0], [(-7662188427495)]], [[(-3367493105837), 0, 0, 0], [454366470043, 0, 0], [331801435891, 0], [76590687845]], [[40114137386, 0, 0, 0, 0], [(-5202905335), 0, 0, 0], [(-3074170491), 0, 0], [(-3321692999), 0], [(-890445841)]]], r1 := 92819238701, V2 := [[[18443439585370115699]], [[(-34764721588691), 24112977179], [(-54145083034387)]], [[31785772946, (-575176261), (-168342)], [(-572035125699), 794497707], [264542642]], [[(-384842876), (-9055706), 9809, 1], [574489677, (-18925106), (-8325)], [(-20989672), 6583175], [(-1138599)]], [[5991574, 10264, (-75), 0, 0], [(-6909018), (-299626), 485, 0], [527830, (-156327), (-138)], [89179, 474], [8402]]], r2 := 380923776, V3 := [[[18444396582242382796]], [[(-67070016912249), 34142342746], [(-38484031812250)]], [[33800412, (-192401088), (-475693)], [(-1099505319710), 1124863607], [(-9318322)]], [[6808, (-33800796), 19001, 6], [1114069, (-6309005), (-23518)], [51689, 9318710], [(-654)]], [[(-58), (-6793), 382, (-1), 0], [247, (-1114088), 939, 0], [9238, (-51705), (-389)], [(-1), 656], [2]]], r3 := 3372508979, Vm := [[[18443439612560200138]], [[(-34765508097006), 0], [(-54144181735214)]], [[31780398855, 0, 0], [(-572061376269), 0], [272109454]], [[(-384839387), 0, 0, 0], [574317069, 0, 0], [(-21213283), 0], [(-1137388)]], [[5991722, 0, 0, 0, 0], [(-6908878), 0, 0, 0], [526480, 0, 0], [89122, 0], [8398]]], rm := 46464606 }
noncomputable def w6 : Wit := { Z0 := { p := [[[638088151085271101]], [[(-28065722831720783), 91155450155038728], [1018372605218376]], [[275625726981555, (-4009388975960112), 0], [(-44181331739000), 145481800745482], [(-6721611583917)]], [[(-3098457736730), 39375103854507, 0, 0], [421535840119, (-6311618819858), 0], [292588231554, (-960230226274)], [67174066636]], [[38285924578, (-442636819533), 0, 0, 0], [(-5264129233), 60219405731, 0, 0], [(-2810983116), 41798318793, 0], [(-2927175638), 9596295233], [(-780870822)]]], r := 102275409418, ok := true }, Z1 := { p := [[[729243601240309830]], [[(-32075111807680895), 0], [1163854405963859]], [[315000830836063, 0, 0], [(-50492950558857), 0], [(-7681841810191)]], [[(-3541094556262), 0, 0, 0], [481755245850, 0, 0], [334386550348, 0], [76770361870]], [[43755342375, 0, 0, 0, 0], [(-6016147695), 0, 0, 0], [(-3212552132), 0, 0], [(-3345343586), 0], [(-892423797)]]], r := 23167636983, ok := true }, Z2 := { p := [[[13829728475496821584947]], [[(-131422753084132659156), 91155450155038728], [(-204687267815281819203)]], [[1442976870896951188, (-4009388975960112), 0], [1958004688439421448, 145481800745482], [3209779297184805022]], [[(-17406711613189276), 39375103854507, 0, 0], [(-21294717202965583), (-6311618819858), 0], [(-30780234993344292), (-960230226274)], [(-51162976808601361)]], [[229672890890172, (-442636819533), 0, 0, 0], [252699302903153, 60219405731, 0, 0], [333611529096703, 41798318793, 0], [491352556617583, 9596295233], [821808514403060]]], r := 248963135883316, ok := true }, Z3 := { p := [[[18844307398372505027214]], [[(-487971236191733654041), 248404308859546892], [(-279992483103663068889)]], [[13355823930937295245, (-14997277283396806), 0], [7327059555330501661, 381932913715771], [4397038726668854626]], [[(-371356247971076222), 397814754504199, 0, 0], [(-201330273215298979), (-22035174141761), 0], [(-115517209515928145), (-2543258839433)], [(-70148492753360153)]], [[10402395868553221, (-10964805417994), 0, 0, 0], [5611106225894711, 537968568237, 0, 0], [3178978424971393, 148307371016, 0], [1847243525494089, 25489434421], [1127454693179908]]], r := 4192593445390407, ok := true }, iE := { p := [[[13832309117723624577927]], [[(-131425269565904210456), 0], [(-204683149175336576408)]], [[1443037034885271152, 0, 0], [1958003142698020018, 0], [3209752112735985339]], [[(-17407663858483581), 0, 0, 0], [(-21294589166449547), 0, 0], [(-30780220843022709), 0], [(-51162705134174225)]], [[229688052579147, 0, 0, 0, 0], [252696963772085, 0, 0, 0], [333610737730862, 0, 0], [491352402569594, 0], [821805356299884]]], r := 248913306882122, ok := true }, iHu := { p := [[[18846954189111732613067]], [[(-487979806459986247103), 0], [(-279988413542616924977)]], [[13356147156796103075, 0, 0], [7327057287145410291, 0], [4397011627807427570]], [[(-371365909892932177), 0, 0, 0], [(-201329938115867887), 0, 0], [(-115517177608881904), 0], [(-70148221159041660)]], [[10402675315866653, 0, 0, 0, 0], [5611095322835060, 0, 0, 0], [3178975989627843, 0, 0], [1847243150500574, 0], [1127451530658511]]], r := 4191930348429431, ok := true }, T := { p := [[[16140901064495857664]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[24600546736258779]], [[233737798856646, 0], [364025798914560]], [[(-345600055326), 0, 0], [3435176966947, 0], [(-321834186930)]], [[3291219658, 0, 0, 0], [(-5665935190), 0, 0], [(-3250946420), 0], [1758484903]], [[(-47017423), 0, 0, 0, 0], [53954421, 0, 0, 0], [(-5910), 0, 0], [17762475, 0], [(-14413810)]]], r := 31534915, ok := true }, de := { p := [[[(-128572771763359578714)]], [[380210280513710681, 0], [218153439639014325]], [[(-5431229813863600), 0, 0], [396615463257, 0], [(-1788029164736068)]], [[103451996873451, 0, 0, 0], [721070, 0, 0], [413729, 0], [19541302425970]], [[(-2216828504430), 0, 0, 0, 0], [1, 0, 0, 0], [5912, 0, 0], [1, 0], [(-240261915073)]]], r := 276820818352, ok := true }, dde := { p := [[[(-209143278740954591323596)]], [[5975142015267502792135, 0], [3428360172694468816682]], [[(-170718343984645273317), 0, 0], [(-97953148584551933172), 0], [(-56202626009457255840)]], [[4877666970988622670, 0, 0, 0], [2798661376795304735, 0, 0], [1605789314554696528, 0], [921354524744976222]], [[(-139361913456807692), 0, 0, 0, 0], [(-79961753622759312), 0, 0, 0], [(-45879694701593935), 0, 0], [(-26324414992704859), 0], [(-15104172536800657)]]], r := 9279534957573825, ok := true }, nJu := { p := [[[(-257145543526719157428)]], [[760420561027421362, 0], [436306879278028651]], [[(-10862459627727200), 0, 0], [793230926514, 0], [(-3576058329472135)]], [[206903993746903, 0, 0, 0], [1442140, 0, 0], [827458, 0], [39082604851941]], [[(-4433657008859), 0, 0, 0, 0], [3, 0, 0, 0], [11825, 0, 0], [2, 0], [(-480523830146)]]], r := 553641636697, ok := true }, Jd1 := { p := [[[(-418286557481909182647191)]], [[11950284030535005584270, 0], [6856720345388937633364]], [[(-341436687969290546633), 0, 0], [(-195906297169103866343), 0], [(-112405252018914511680)]], [[9755333941977245341, 0, 0, 0], [5597322753590609471, 0, 0], [3211578629109393056, 0], [1842709049489952444]], [[(-278723826913615384), 0, 0, 0, 0], [(-159923507245518623), 0, 0, 0], [(-91759389403187870), 0, 0], [(-52648829985409718), 0], [(-30208345073601314)]]], r := 18559069915147643, ok := true }, term0 := { p := [[[3287772115597957201744997480]], [[(-187854763091484430430637162), 0], [(-107779250805130786029728064)]], [[8050662340697756303823568, 0, 0], [6158520472284074198298644, 0], [2650173756832491245282030]], [[(-306687021026277295433086), 0, 0, 0], [(-263932393677133375278519), 0, 0], [(-151433683022484900478801), 0], [(-57925812289267088151083)]], [[10953003372360217003021, 0, 0, 0, 0], [10054487416422743198564, 0, 0, 0], [6489946167135746583920, 0, 0], [3309967443284303041226, 0], [1186986117295843201083]]], r := 1260504286037232706414, ok := true }, r0 := { p := [[[99878348288492483398197]], [[(-3012785371314077628637), 28457731549789570007330], [(-1481993355822826990561)]], [[68453434742985983539, (-851518456762239462926), 2010210107836897666562], [44759253375923585032, (-422506029638507802601)], [23262489538498672544]], [[(-1424959335393194261), 19080840954548388619, (-58186247814644530011), (-3192457682944946364)], [(-1006164830339518109), 12679850746442852772, (-29916547314306860184)], [(-702843461278743417), 6633217438409040113], [(-371012175147728311)]], [[29430274841005680, (-391320993407463450), 1227870324364027260, 372609860219342959, (-110518070501504991)], [20601231142563484, (-281880419987481864), 874822236289148764, 37326378529057901], [15735596564536028, (-199254590841340641), 470035212106859999], [11212041750090033, (-105804203130025730)], [5961819183259160]]], r := 227592482817930955, ok := true }, r1 := { p := [[[130342987273464711442661]], [[(-3922104935339319664586), 0], [(-1934377305663610608500)]], [[88742624563706987976, 0, 0], [58309399445014007359, 0], [30365187677035335228]], [[(-1839159826133682869), 0, 0, 0], [(-1306361290136518292), 0, 0], [(-915821957506988064), 0], [(-484308627017236713)]], [[37853981192524903, 0, 0, 0, 0], [26649527035254352, 0, 0, 0], [20440364544687674, 0, 0], [14611428836111274, 0], [7782562699084830]]], r := 13484527081556036, ok := true }, r2 := { p := [[[1046261027398337579042975280]], [[(-29269081939432358941297454), 44896910271672695779127], [(-33917379840760417432453334)]], [[696859466169168667603593, (-897675738227874326321), 452793275600273241], [938338338257254594298997, (-732498014867891802212)], [828369862110327389227300]], [[(-16637335627162455851644), 17734861689118933147, 130233024929760, (-57453649080702)], [(-22095400688869471711705), 14343204351028776424, 44633541561550], [(-22760250860293565481563), 11984449338900686719], [(-18019722034827175109145)]], [[412976637535534753904, (-370244188129586339), (-45836511269626), 2281985701337, (-6133169428411)], [522756164825602261417, (-276740665597940702), (-28211502861549), 2541870761063], [532255055324018708666, (-232704619645425186), (-48351565273992)], [492680354765761260552, (-196233355182036355)], [367902745134111881605]]], r := 1875511620933963966919, ok := true }, r3 := { p := [[[6574068277578939370351425813]], [[(-375640072876296076266428127), 292820474533404761605759], [(-215534297226476760103194615)]], [[16098560790428211643439232, (-13799129594160308438154), 1788735566598875724], [12315902032664185689495646, (-4809661593534093429267)], [5299950663698397759370061]], [[(-613272801754107325749335), 549429524554999380761, 1537225525053646, (-705870723030226)], [(-527819466058000200019003), 226547935033546992281, (-192903938484842)], [(-302848693653488712781414), 78902874598700377941], [(-115845118897132165892588)]], [[21902477390943748096621, (-20132518754419587062), (-62094634588811), 65066010923121, (-81278837443037)], [20107314446395617189942, (-9019095666591288062), (-98196801725491), (-684802402603376)], [12979149179365357205850, (-3716109165217269882), (-248648162483926)], [6619628506963112447823, (-1294542504796715978)], [2373865432534337234396]]], r := 111203104794391287857864, ok := true }, eta := { p := [[[(-1046607296853559969475117383)]], [[29281587881886290687541864, 0], [33922995290052805319139125]], [[(-697240623355374663335654), 0, 0], [(-938540951152517328759694), 0], [(-828461529805597144154541)]], [[16648433366176841215183, 0, 0, 0], [22101567908243533226117, 0, 0], [22763556742118974342347, 0], [18021220917819853515846]], [[(-413295269553804114972), 0, 0, 0, 0], [(-522935609089638796445), 0, 0, 0], [(-532355638006648314713), 0, 0], [(-492734440070894835687), 0], [(-367927298424716745807)]]], r := 186786747455765623343, 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 := 2216615441596416, bh := 35184372088832, tc := 16140901064495857664, th := 2305843009213693952, sc := 10088063165309911040, sh := 288230376151711744 }
noncomputable def q7 : Cert := { V0 := [[[639543425062818108]], [[(-28079768026035753), 91204986746154542], [989689099495336]], [[272529298656865, (-3990543113251806), (-33864871672317)], [(-42706899799366), 140649203960287], [(-6324070254486)]], [[(-2991149622954), 37815544340157, 4453137250385, (-1596137839563)], [392589715822, (-6004783620448), (-156953625515)], [274167096608, (-899878740507)], [61190139836]], [[35959177826, (-393980806834), (-237919886946), 208442253541, 1756132252], [(-4594686434), 50972773838, 20497469927, (-7346678436)], [(-2561462156), 38698878308, 761060165], [(-2656537281), 8709947484], [(-688695500)]]], r0 := 483985862916, V1 := [[[730712952604386849]], [[(-32065649954546889), 0], [1130174017065356]], [[310095983337438, 0, 0], [(-48690240706167), 0], [(-7223152160382)]], [[(-3377761735982), 0, 0, 0], [442429916947, 0, 0], [312761457097, 0], [69893034704]], [[40249605885, 0, 0, 0, 0], [(-5067066307), 0, 0, 0], [(-2896821681), 0, 0], [(-3030973459), 0], [(-786669697)]]], r1 := 84862721197, V2 := [[[18443331296253240716]], [[(-35908875095698), 25728309063], [(-54144038264172)]], [[32936845973, (-613651844), (-185548)], [(-572118034854), 820836050], [257906698]], [[(-398684069), (-9664984), 10810, 1], [576574651, (-19550510), (-8885)], [(-20469945), 6585984], [(-1074354)]], [[6207034, 10985, (-82), 0, 0], [(-6932077), (-309653), 517, 0], [514784, (-156375), (-142)], [84139, 462], [7674]]], r2 := 358408604, V3 := [[[18444319614141479815]], [[(-69269027344913), 36429350015], [(-38484069093316)]], [[36065508, (-205225917), (-524302)], [(-1099505112956), 1162146254], [(-9322196)]], [[7313, (-36065930), 20941, 7], [1151029, (-6515822), (-25100)], [51687, 9322598], [(-638)]], [[(-62), (-7295), 422, (-1), 0], [257, (-1151050), 1002, 0], [9242, (-51703), (-402)], [(-1), 640], [2]]], r3 := 3285670766, Vm := [[[18443331325276200373]], [[(-35909715000051), 0], [(-54143106683343)]], [[32931121266, 0, 0], [(-572145180548), 0], [265480685]], [[(-398680293), 0, 0, 0], [576396647, 0, 0], [(-20693894), 0], [(-1073173)]], [[6207192, 0, 0, 0, 0], [(-6931930), 0, 0, 0], [513436, 0, 0], [84084, 0], [7670]]], rm := 44969684 }
noncomputable def w7 : Wit := { Z0 := { p := [[[640098535054537473]], [[(-28152938028271562), 91442647864933924], [992268022282580]], [[276457775088114, (-4021848289753081), 0], [(-43045048622791), 141752574611797], [(-6336551484051)]], [[(-3108851762562), 39493967869730, 0, 0], [410619946952, (-6149292660399), 0], [275809341758, (-905221640579)], [61300571745]], [[38433971654, (-444121680366), 0, 0, 0], [(-5131197312), 58659992421, 0, 0], [(-2649431729), 39401334536, 0], [(-2671077759), 8757224535], [(-689872279)]]], r := 94770673841, ok := true }, Z1 := { p := [[[731541182919471397]], [[(-32174786318024642), 0], [1134020596894377]], [[315951742957845, 0, 0], [(-49194341283190), 0], [(-7241773124630)]], [[(-3552973442928), 0, 0, 0], [469279939374, 0, 0], [315210676294, 0], [70057796281]], [[43924539033, 0, 0, 0, 0], [(-5864225499), 0, 0, 0], [(-3027921976), 0, 0], [(-3052660296), 0], [(-788425462)]]], r := 21172799941, ok := true }, Z2 := { p := [[[13432796491185247134868]], [[(-127626056281683189856), 91442647864933924], [(-192436829513735154108)]], [[1401680688128144392, (-4021848289753081), 0], [1840536984404418859, 141752574611797], [2921513362859156539]], [[(-16916567033709805), 39493967869730, 0, 0], [(-20021422138776708), (-6149292660399), 0], [(-28012001887878414), (-905221640579)], [(-45086397221944050)]], [[223333937636878, (-444121680366), 0, 0, 0], [237679799184765, 58659992421, 0, 0], [303666661918182, 39401334536, 0], [432938135207895, 8757224535], [701175839457361]]], r := 220783880977566, ok := true }, Z3 := { p := [[[18301366874300151392963]], [[(-473764868892869660662), 249158200934856947], [(-263211432978173802284)]], [[12965484943759271051, (-15040766063142727), 0], [6886243010720606554, 372056543919520], [4001818390976281829]], [[(-360477751251768392), 398876217588729, 0, 0], [(-189199738037590572), (-21459303607168), 0], [(-105110814426193048), (-2397157669438)], [(-61812222205164209)]], [[10097170863264799, (-10993007566483), 0, 0, 0], [5272722166905970, 523637225282, 0, 0], [2892345956706684, 139758741176, 0], [1627380450179034, 23257102025], [961884646450483]]], r := 3828498636467970, ok := true }, iE := { p := [[[13435385264078250953910]], [[(-127628575799539359592), 0], [(-192432816449467695988)]], [[1401741105084579137, 0, 0], [1840535493473920700, 0], [2921487735722366364]], [[(-16917523901573857), 0, 0, 0], [(-20021297177581627), 0, 0], [(-28011988618658395), 0], [(-45086149301897727)]], [[223349180264180, 0, 0, 0, 0], [237677515219255, 0, 0, 0], [303665914955046, 0, 0], [432937995254627, 0], [701173049382776]]], r := 220737279525747, ok := true }, iHu := { p := [[[18304021697889422799745]], [[(-473773443572790201944), 0], [(-263207468651550659810)]], [[12965808830272111641, 0, 0], [6886240865810812217, 0], [4001792848848010928]], [[(-360487434675978100), 0, 0, 0], [(-189199412386984791), 0, 0], [(-105110784660018343), 0], [(-61811974396732279)]], [[10097450946376332, 0, 0, 0, 0], [5272711564578251, 0, 0, 0], [2892343665397837, 0, 0], [1627380110770737, 0], [961881852884655]]], r := 3827849948793650, ok := true }, T := { p := [[[16140901064495857664]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[25327324839038317]], [[240595288819991, 0], [362759113796137]], [[(-356931949347), 0, 0], [3422381783584, 0], [(-311618227026)]], [[3399128499, 0, 0, 0], [(-5665958831), 0, 0], [(-3147754906), 0], [1648607287]], [[(-48558978), 0, 0, 0, 0], [53954421, 0, 0, 0], [(-5910), 0, 0], [16652600, 0], [(-13084184)]]], r := 31684961, ok := true }, de := { p := [[[(-128143464416360185184)]], [[380211073746292111, 0], [211228374303495618]], [[(-5431229812397815), 0, 0], [396617118177, 0], [(-1676305497653646)]], [[103451996873454, 0, 0, 0], [744716, 0, 0], [413732, 0], [17738682591470]], [[(-2216828504430), 0, 0, 0, 0], [1, 0, 0, 0], [5912, 0, 0], [1, 0], [(-211174792755)]]], r := 274427537521, ok := true }, dde := { p := [[[(-202504232058205458297490)]], [[5785454965602388367913, 0], [3214141647556882435017]], [[(-165298714016883098285), 0, 0], [(-91832619294911581076), 0], [(-51018121610149099899)]], [[4722820400481039668, 0, 0, 0], [2623789111376879844, 0, 0], [1457660617431603440, 0], [809811454129137177]], [[(-134937725728019927), 0, 0, 0, 0], [(-74965403182230268), 0, 0, 0], [(-41647446212359665), 0, 0], [(-23137470117966832), 0], [(-12854150065534540)]]], r := 8672276782773718, ok := true }, nJu := { p := [[[(-256286928832720370367)]], [[760422147492584223, 0], [422456748606991236]], [[(-10862459624795629), 0, 0], [793234236354, 0], [(-3352610995307292)]], [[206903993746909, 0, 0, 0], [1489433, 0, 0], [827464, 0], [35477365182940]], [[(-4433657008859), 0, 0, 0, 0], [3, 0, 0, 0], [11825, 0, 0], [2, 0], [(-422349585510)]]], r := 548855075033, ok := true }, Jd1 := { p := [[[(-405008464116410916594979)]], [[11570909931204776735827, 0], [6428283295113764870034]], [[(-330597428033766196570), 0, 0], [(-183665238589823162151), 0], [(-102036243220298199797)]], [[9445640800962079337, 0, 0, 0], [5247578222753759688, 0, 0], [2915321234863206880, 0], [1619622908258274354]], [[(-269875451456039853), 0, 0, 0, 0], [(-149930806364460535), 0, 0, 0], [(-83294892424719329), 0, 0], [(-46274940235933664), 0], [(-25708300131069079)]]], r := 17344553565547426, ok := true }, term0 := { p := [[[3082369174633484601213417407]], [[(-176118021240361710924009932), 0], [(-97837467845950180088713556)]], [[7547667247951972746932351, 0, 0], [5590436950490194510054057, 0], [2329340347821206966459769]], [[(-287525458053960544571687), 0, 0, 0], [(-239586219337222767338654), 0, 0], [(-133100789750788496072331), 0], [(-49296905008680287989207)]], [[10268665155775429500741, 0, 0, 0, 0], [9127019104585999958109, 0, 0, 0], [5704257089578551013248, 0, 0], [2816896588085409731832, 0], [978097677821019167313]]], r := 1131324155171706416613, ok := true }, r0 := { p := [[[97004535844267303219029]], [[(-2925991335018707055215), 27638432280811615760649], [(-1393212174904511850071)]], [[66502106507848651792, (-826931126564561701308), 1952199017942182014463], [42076881804121230429, (-397190513963225473891)], [21172160191821497315]], [[(-1384998036046175938), 18534197021385880278, (-56490050668508990669), (-3119885382298079436)], [(-946103722326789834), 11919419199801440514, (-28122705444609511599)], [(-639673987152107188), 6037105969720846732], [(-326930618451678182)]], [[28620925936768985, (-380263563674674056), 1191910458326766715, 364099644001007749, (-107984198762862260)], [19379126357050841, (-265027607863694622), 822202548080765708, 35276359526513777], [14324649389022651, (-181338967373232189), 427776763499039653], [9879705518436542, (-93232276240629926)], [5086438241015101]]], r := 214585906652403353, ok := true }, r1 := { p := [[[126591939571490253315356]], [[(-3809036172900918901268), 0], [(-1818488888799565685981)]], [[86209141462634583808, 0, 0], [54814225566262598141, 0], [27636535679943162934]], [[(-1787467482830129464), 0, 0, 0], [(-1228343601030931658), 0, 0], [(-833500535371690849), 0], [(-426764609663642339)]], [[36810156693526010, 0, 0, 0, 0], [25067497805539606, 0, 0, 0], [18607067359336861, 0, 0], [12874997194257337, 0], [6639821931651930]]], r := 12137076884669597, ok := true }, r2 := { p := [[[981601253412875669715527797]], [[(-27479659114150221550766872), 43478332167449994878130], [(-30808916126226546100532526)]], [[654709548681429285320298, (-869890677947613062776), 452894352806191462], [852903826448729040652323, (-686816046548792200087)], [728535304263784397202087]], [[(-15639840835451739098024), 17198661549928307728, 108184954580184, (-51373169177808)], [(-20096863960628406207958), 13456014208081806888, 39935574668810], [(-20029840482748065535201), 10880220991581959134], [(-15344475711908438819214)]], [[388367835389715755551, (-359297875072153452), (-40026682634238), 2041763618495, (-5433525667296)], [475730835431929822455, (-259803348853993271), (-43595405533371), 2175026142582], [468702019277904800527, (-211371546455937217), (-4958483127264)], [419792544514779384163, (-172527288378019863)], [303331572855536585918]]], r := 1619697107169468121535, ok := true }, r3 := { p := [[[6163309267419656905033099596]], [[(-352168794677680756378573408), 283506740793778432859550], [(-195652243908268427970283271)]], [[15092658369975346878492117, (-13360425356252837057078), 1789099328425436901], [11179806160905916267246829, (-4508925773425705446878)], [4658320456550767816681204]], [[(-574952890710873029301422), 531964853795971917699, 1663494140283009, (-624638228652660)], [(-479129949790547603875875), 212384510227272351635, (-319589811300942)], [(-266184629483482731254200), 71621026144402319181], [(-98588091858654222570843)]], [[20533913136852432428130, (-19492592348860016044), (-52290135657636), 57454027470221, (-72449832873583)], [18252481557201122988691, (-8455531495814296061), (-425440547087337), (-609911117882811)], [11407839234214121318334, (-3373333712890531866), (-462560504429102)], [5633523672342963546817, (-1137654287467328996)], [1956104466104682876348]]], r := 98276034773813143629254, ok := true }, eta := { p := [[[(-981936647028922569167004984)]], [[27491772635988238856612184, 0], [30814182137662150696782304]], [[(-655078760922533444826542), 0, 0], [(-853093836910435492022367), 0], [(-728618536602412945688702)]], [[15650591073117694979159, 0, 0, 0], [20102647789980567588852, 0, 0], [20032842256852215078518, 0], [15345793430244147798836]], [[(-388676522412622297858), 0, 0, 0, 0], [(-475899132549884272376), 0, 0, 0], [(-468793354217410301577), 0, 0], [(-419840079415477149746), 0], [(-303352457464070983073)]]], r := 161748340883137885679, 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 1970324836974592 2251799813685248 13835058055282163712 18446744073709551616 9223372036854775808 10376293541461622784 :=
  (RegionPosI.split_b 2111062325329920 (RegionPosI.split_s 9799832789158199296 (RegionPosI.split_b 2040693581152256 (RegionPosI.of_check c0 q0 ok_0 1970324836974592 2040693581152256 13835058055282163712 18446744073709551616 9223372036854775808 9799832789158199296 (by decide +kernel)) (RegionPosI.of_check c1 q1 ok_1 2040693581152256 2111062325329920 13835058055282163712 18446744073709551616 9223372036854775808 9799832789158199296 (by decide +kernel))) (RegionPosI.split_b 2040693581152256 (RegionPosI.of_check c2 q2 ok_2 1970324836974592 2040693581152256 13835058055282163712 18446744073709551616 9799832789158199296 10376293541461622784 (by decide +kernel)) (RegionPosI.of_check c3 q3 ok_3 2040693581152256 2111062325329920 13835058055282163712 18446744073709551616 9799832789158199296 10376293541461622784 (by decide +kernel)))) (RegionPosI.split_s 9799832789158199296 (RegionPosI.split_b 2181431069507584 (RegionPosI.of_check c4 q4 ok_4 2111062325329920 2181431069507584 13835058055282163712 18446744073709551616 9223372036854775808 9799832789158199296 (by decide +kernel)) (RegionPosI.of_check c5 q5 ok_5 2181431069507584 2251799813685248 13835058055282163712 18446744073709551616 9223372036854775808 9799832789158199296 (by decide +kernel))) (RegionPosI.split_b 2181431069507584 (RegionPosI.of_check c6 q6 ok_6 2111062325329920 2181431069507584 13835058055282163712 18446744073709551616 9799832789158199296 10376293541461622784 (by decide +kernel)) (RegionPosI.of_check c7 q7 ok_7 2181431069507584 2251799813685248 13835058055282163712 18446744073709551616 9799832789158199296 10376293541461622784 (by decide +kernel)))))

end CKLaneC.RSC2.S01_0272