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

import Definitions.Def_CK_CKLaneC_RSC2_S07_0083_part00

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

namespace CKLaneC.RSC2.S07_0083
open CKLaneC.TM3 CKLaneC.RSCell

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 := 76561193665298432, bh := 4503599627370496, tc := 11529215046068469760, th := 2305843009213693952, sc := 17870283321406128128, sh := 576460752303423488 }
noncomputable def q5 : Cert := { V0 := [[[39041357222177437]], [[(-39566787900329995), 7808220985387124], [354138990441553]], [[533916890114146, (-7913204165818166), (-15137599147)], [(-358036489235940), 70826424967827], [(-7182159740812)]], [[(-8634248573676), 106625829346755, 46023689770, (-1009134824)], [3963126508008, (-71603126422082), (-411930914)], [7269432645877, (-1436416555782)], [248194525189]], [[150773722221, (-1670097113656), (-47263410044), 3068051127, 5767], [(-66880470231), 788348246800, 1251401031, (-27460318)], [(-88696630741), 1453839705876, 4617702], [(-251253158868), 49638410244], [(-10122583224)]]], r0 := 19812709308618, V1 := [[[62465856693829575]], [[(-63305903349847628), 0], [566613816562011]], [[853283949470767, 0, 0], [(-572832353729736), 0], [(-11491359537107)]], [[(-13460691490755), 0, 0, 0], [6314314905753, 0, 0], [11630800057407, 0], [397108152818]], [[227385322513, 0, 0, 0, 0], [(-97438837516), 0, 0, 0], [(-141614250570), 0, 0], [(-401995663810), 0], [(-16196014855)]]], r1 := 7602123142085, V2 := [[[18296009004286634881]], [[(-2390939739411218), 2885174475055], [(-8867255813646793)]], [[3667990559004, (-2838328374059), (-51704310)], [(-140201155502636), 343985848890], [(-29878982836)]], [[(-46989513543), (-46907094489), 102556816, 903], [260828979133, (-338396511016), (-9261010)], [27949768273, 10428627409], [(-41909426)]], [[847772560, 61837870, (-49999712), (-2693), 0], [(-3170315334), (-5597389310), 18369277, 216], [1944549715, (-10259249178), (-558195)], [59172744, 8172046], [667682]]], r2 := 2873042622688, V3 := [[[18298389731586004809]], [[(-4768607324718782), 5677075890068], [(-8727754491278163)]], [[561867679521, (-5490293112645), (-203425649)], [(-279511922071829), 676847042049], [(-61541440742)]], [[252238501, (-186719867330), 400060475, 7102], [67126715918, (-654566464473), (-36436010)], [59497674695, 20520400556], [(-47993261)]], [[(-2279641), (-63674576), (-189848141), (-21066), 0], [32201784, (-22273611208), 71654486, 1696], [2042726781, (-19845510578), (-2196116)], [46312704, 16134179], [452829]]], r3 := 7215287193188, Vm := [[[18296017692808668279]], [[(-2399520617136409), 0], [(-8866219582220013)]], [[3560058734719, 0, 0], [(-141224878090956), 0], [1560063121]], [[(-46699557085), 0, 0, 0], [248281279613, 0, 0], [(-3133692849), 0], [(-16632439)]], [[845300587, 0, 0, 0, 0], [(-3131131657), 0, 0, 0], [1587439111, 0, 0], [33466912, 0], [430499]]], rm := 515629336240 }
noncomputable def w5 : Wit := { Z0 := { p := [[[39041483370519370]], [[(-39567171439603237), 7808296674103874], [354142423275459]], [[534310769259304, (-7913434287920648), 0], [(-358046917964335), 70828484655091], [(-7182198221836)]], [[(-8776137782405), 106862153851860, 0, 0], [3973819482720, (-71609383592867), 0], [7269549704481, (-1436439644368)], [248195762174]], [[156334180398, (-1755227556481), 0, 0, 0], [(-70715463292), 794763896544, 0, 0], [(-88816968600), 1453909940896, 0], [(-251256921094), 49639152434], [(-10122630620)]]], r := 4920806293422, ok := true }, Z1 := { p := [[[62466373392830993]], [[(-63307474303365179), 0], [566627877240735]], [[854897230814887, 0, 0], [(-572875068742936), 0], [(-11491517154937)]], [[(-14041820451847), 0, 0, 0], [6358111172353, 0, 0], [11631279527170, 0], [397113219478]], [[250134688637, 0, 0, 0, 0], [(-113144741267), 0, 0, 0], [(-142107149759), 0, 0], [(-402011073750), 0], [(-16196208991)]]], r := 1898692954450, ok := true }, Z2 := { p := [[[477664281430061333204]], [[(-6470723686432280283), 7808296674103874], [(-23997912319257441203)]], [[106022598732017356, (-7913434287920648), 0], [333345013849388016, 70828484655091], [1321656871429431031]], [[(-1885899328719707), 106862153851860, 0, 0], [(-5405053830835777), (-71609383592867), 0], [(-18530163880803742), (-1436439644368)], [(-74665059557709366)]], [[35592400177610, (-1755227556481), 0, 0, 0], [94259376205990, 794763896544, 0, 0], [299743255372064, 1453909940896, 0], [1052210269497456, 49639152434], [4266733670191154]]], r := 1088061626473541, ok := true }, Z3 := { p := [[[484204110961836305884]], [[(-13296072462932291685), 15829110528904058], [(-24335167115392693404)]], [[401761247706386160, (-16261184921043784), 0], [685564943324064733, 143223786621916], [1340409731615382500]], [[(-12448617490211918), 445137739365465, 0, 0], [(-20909000735911771), (-146413272285655), 0], [(-38119172205966112), (-2908060458115)], [(-75730090741406340)]], [[390143408080523, (-13468169555646), 0, 0, 0], [651223122069333, 3280165957625, 0, 0], [1166060126717431, 2979610239210, 0], [2164863358497388, 100511836707], [4327814517665196]]], r := 2956754386464362, ok := true }, iE := { p := [[[481623087843831997406]], [[(-6484986973266864889), 0], [(-23962002277537309565)]], [[106371252460723038, 0, 0], [333303240511211595, 0], [1320928596529736958]], [[(-1892835201890495), 0, 0, 0], [(-5401928791428636), 0, 0], [(-18528488638685194), 0], [(-74639892507424902)]], [[35732675116834, 0, 0, 0, 0], [94187687118070, 0, 0, 0], [299682006579148, 0, 0], [1052148063745202, 0], [4265707235446365]]], r := 1088906724804590, ok := true }, iHu := { p := [[[488177217704591224469]], [[(-13325377582714842456), 0], [(-24299217944950592460)]], [[402879775899348345, 0, 0], [685480501355575989, 0], [1339679808440395795]], [[(-12484911158889316), 0, 0, 0], [(-20902187410464816), 0, 0], [(-38115753513201641), 0], [(-75704862270392749)]], [[391303985199090, 0, 0, 0, 0], [650997687539951, 0, 0, 0], [1165899927377082, 0, 0], [2164736255107551, 0], [4326785451756337]]], r := 2961099048908188, ok := true }, T := { p := [[[11529215046068469760]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[706532505416925182]], [[9513360570671070, 0], [35151831237467781]], [[(-27948677030581), 0, 0], [457678976163236, 0], [(-188883658004172)]], [[299310219330, 0, 0, 0], [(-1650676686089), 0, 0], [(-3010057486396), 0], [3688403975876]], [[(-4827663175), 0, 0, 0, 0], [17605907308, 0, 0, 0], [(-391979603), 0, 0], [58544210805, 0], [(-108484304438)]]], r := 123612602333, ok := true }, de := { p := [[[(-73349129218764604367)]], [[430975175970874223, 0], [785895909123358878]], [[(-6923151011995755), 0, 0], [102341954537495, 0], [(-23021273780373429)]], [[148887404174215, 0, 0, 0], [13327306501, 0, 0], [24302735384, 0], [902809822461642]], [[(-3602114379183), 0, 0, 0, 0], [1735526, 0, 0, 0], [396726776, 0, 0], [5771074, 0], [(-39829842477671)]]], r := 10437742836183, ok := true }, dde := { p := [[[(-3322869309697319182462)]], [[106756617581683252500, 0], [194673832060716519064]], [[(-3443818207045190587), 0, 0], [(-6280006544418739988), 0], [(-11451589262873454482)]], [[111090902566657225, 0, 0, 0], [202577501447570412, 0, 0], [369406032051451728, 0], [673622853320429596]], [[(-3583577503105432), 0, 0, 0, 0], [(-6534758981479158), 0, 0, 0], [(-11916325995000102), 0, 0], [(-21729769485126614), 0], [(-39624873735296992)]]], r := 5404520662819431, ok := true }, nJu := { p := [[[(-146698258437529208734)]], [[861950351941748447, 0], [1571791818246717756]], [[(-13846302023991510), 0, 0], [204683909074990, 0], [(-46042547560746858)]], [[297774808348431, 0, 0, 0], [26654613002, 0, 0], [48605470769, 0], [1805619644923285]], [[(-7204228758365), 0, 0, 0, 0], [3471053, 0, 0, 0], [793453553, 0, 0], [11542148, 0], [(-79659684955342)]]], r := 20875485672359, ok := true }, Jd1 := { p := [[[(-6645738619394638364924)]], [[213513235163366505000, 0], [389347664121433038128]], [[(-6887636414090381173), 0, 0], [(-12560013088837479975), 0], [(-22903178525746908963)]], [[222181805133314451, 0, 0, 0], [405155002895140825, 0, 0], [738812064102903457, 0], [1347245706640859192]], [[(-7167155006210864), 0, 0, 0, 0], [(-13069517962958316), 0, 0, 0], [(-23832651990000203), 0, 0], [(-43459538970253228), 0], [(-79249747470593983)]]], r := 10809041325638854, ok := true }, term0 := { p := [[[836531143342547545649891]], [[(-53645150799778842191930), 0], [(-97622556648854720128212)]], [[2590567968235460921913, 0, 0], [6279391697974638271471, 0], [8590668796371973636161]], [[(-111311187212938343606), 0, 0, 0], [(-303537632216819032516), 0, 0], [(-553128477569121544146), 0], [(-672872537340413077096)]], [[4485666639987996822, 0, 0, 0, 0], [13048847282312947780, 0, 0, 0], [26746406711060816376, 0, 0], [43345942133161010881, 0], [49435977434201430298]]], r := 11631885547188915243, ok := true }, r0 := { p := [[[1115145275553878276100]], [[(-45283044489459309527), 446053458757892409286], [(-55529889796749621609)]], [[1477151305010814558, (-18103601022127724035), 44603485311756699302], [2326944653254595688, (-22211808678200678906)], [3061843464582240493]], [[(-43439092115521820), 585567394662098012, (-1806513480496829649), (-372104234198168)], [(-75212295544542633), 930472935455235724, (-2221121971909998606)], [(-129352288897182814), 1224730145030228155], [(-173034957034272831)]], [[1218954431251154, (-17033334210395916), 56439625321154480, 769289245201290, (-18603068671420)], [2173629078847268, (-29916315311793179), 92925324395916619, 11779066173835], [4174359179645918, (-51725919110303654), 122470118196887696], [7345188445163084, (-69213602527476849)], [9889968304589779]]], r := 54553739841880602, ok := true }, r1 := { p := [[[2854725466037189886860]], [[(-115828583441298239303), 0], [(-142155047841710792502)]], [[3728666083553459321, 0, 0], [5953933978973615065, 0], [7838246977732567711]], [[(-107790354648401003), 0, 0, 0], [(-190860217683618950), 0, 0], [(-330992137418900414), 0], [(-442965693258963505)]], [[2971774944089254, 0, 0, 0, 0], [5450648698372014, 0, 0, 0], [10603557557915981, 0, 0], [18795818167061351, 0], [25318112983375743]]], r := 20988383011739353, ok := true }, r2 := { p := [[[475519977601260395665023]], [[(-19219505245273318516539), 802934588231899009936], [(-55121972083063076869925)]], [[621370338111489364816, (-22907678822123630564), 479561775999165877], [2200388772802660080653, (-47411066692063819137)], [4823965596047547688681]], [[(-18878479543646312297), 621814815844568034, 525885232675007, (-8002618509521)], [(-70231920899595790237), 1316158861434366340, 721910758160424], [(-191087893775564942121), 2796963051611091428], [(-376266224955473631009)]], [[564613599743064013, (-16815666789740397), (-5683019118352), 7993837431962, 124716620], [2108913559957513051, (-34706881680342795), 14763107262286, (-489694340554)], [6051305996191567407, (-76815820942976654), (-9659300491325)], [14823520567059327357, (-164766790856998783)], [27553463205553403903]]], r := 134566288823237921504, ok := true }, r3 := { p := [[[1649712133039470773123237]], [[(-106155728338392221230413), 3275973202649632368525], [(-193873092767045771906912)]], [[5132143512748241209755, (-160099447885729645908), 1916139924603533692], [12491865929412645956045, (-193596845455482292280)], [17100522138532229883198]], [[(-220642427967959532348), 6925331938788810787, 4260239061737032, (-63950758214208)], [(-604187526212822786121), 9475315838419191850, 2828848838319510], [(-1102317898584899873468), 11423543216473157451], [(-1340988011642446405426)]], [[8894575950206790389, (-280130348367042235), (-74165814812542), 63809452326995, 2085583536], [25981021403906954866, (-409301340324446435), 118186952275155, (-3910909472891)], [53322839400967801578, (-558316747797369295), (-38373298724613)], [86460077794800909611, (-673041555345355273)], [98592003782882857638]]], r := 1249154795329878302097, ok := true }, eta := { p := [[[(-482025966581881219689454)]], [[19477592534945249088108, 0], [55495385296016893991800]], [[(-630340676725438500384), 0, 0], [(-2215222611743753135467), 0], [(-4845802693131763423140)]], [[19175337039009258325, 0, 0, 0], [70744072944179322483, 0, 0], [191953241414584043873, 0], [377546305078088222705]], [[(-574249540335126035), 0, 0, 0, 0], [(-2125776238434775087), 0, 0, 0], [(-6081117038346991878), 0, 0], [(-14874176015300765153), 0], [(-27628581708696827564)]]], r := 17627652478561855597, 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

noncomputable def c6 : Cell := { bc := 85568392920039424, bh := 4503599627370496, tc := 11529215046068469760, th := 2305843009213693952, sc := 16717361816799281152, sh := 576460752303423488 }
noncomputable def q6 : Cert := { V0 := [[[122472720773122698]], [[(-42531980782022063), 24492986483534717], [1006534986076212]], [[598005793447281, (-8504773344050066), (-467266282097)], [(-347025881704298), 201268592763333], [(-18156961723903)]], [[(-10111629514846), 119014792084256, 486782855961, (-31139404800)], [4042177883955, (-69365262311629), (-11519895528)], [6281794136155, (-3631015179707)], [560917743690]], [[185317210629, (-1940864377883), (-175866863392), 32431909241, 1751770], [(-72148611654), 794079145461, 11971711959, (-767513076)], [(-80414470841), 1255965209573, 113147213], [(-194157710373), 112172669169], [(-20456402428)]]], r0 := 17065860187027, V1 := [[[195946634222157852]], [[(-68041044382780614), 0], [1610216368981842]], [[953151390993345, 0, 0], [(-554992407934307), 0], [(-29048785304369)]], [[(-15670673597647), 0, 0, 0], [6377943434860, 0, 0], [10048414543354, 0], [897400504884]], [[277017447086, 0, 0, 0, 0], [(-103147100543), 0, 0, 0], [(-127772879431), 0, 0], [(-310581536049), 0], [(-32727917553)]]], r1 := 6403549447135, V2 := [[[18283634064776400409]], [[(-2688692141222029), 10491589093855], [(-8586098000377851)]], [[4542442417225, (-3320106330363), (-631391332)], [(-141203042238588), 1119665034927], [(-79159251986)]], [[(-61962269785), (-59285876828), 410112880, 37006], [289285828272, (-354301224497), (-101233242)], [20700521811, 30403922418], [(-199204195)]], [[1190742108, 89044540, (-62930780), (-36365), (-2)], [(-3746121921), (-6337075899), 65752572, 7909], [1942880563, (-9620723846), (-5463699)], [111195410, 22227889], [3521207]]], r2 := 2066742556308, V3 := [[[18291591576294785588]], [[(-5330206087105049), 19935606190578], [(-8169153469691839)]], [[702305863808, (-5944026307016), (-2397662097)], [(-279574209011184), 2127534394925], [(-173149796582)]], [[346196423, (-233474460844), 1512870118, 280901], [75089762845, (-634316343651), (-384413571)], [51569184983, 57778797902], [(-124834652)]], [[(-3400962), (-86924991), (-209414943), (-270771), (-32)], [39503681, (-24929381739), 242543662, 60033], [2045817373, (-17228957206), (-20747532)], [36976765, 42766050], [1030480]]], r3 := 5918716537894, Vm := [[[18283665916575367050]], [[(-2698902590663793), 0], [(-8582695256092894)]], [[4405662968322, 0, 0], [(-142294956982703), 0], [13459179900]], [[(-61560537433), 0, 0, 0], [275032316877, 0, 0], [(-9093560894), 0], [(-126160918)]], [[1187113832, 0, 0, 0, 0], [(-3697414542), 0, 0, 0], [1578271136, 0, 0], [85720977, 0], [2927346]]], rm := 371640668336 }
noncomputable def w6 : Wit := { Z0 := { p := [[[122476615169892299]], [[(-42536038193258384), 24495323033978459], [1006631006207117]], [[599471979486649, (-8507207638651677), 0], [(-347125682384490), 201326201241423], [(-18157904651011)]], [[(-10315382593104), 119894395897329, 0, 0], [4078079998824, (-69425136476898), 0], [6282778205859, (-3631580930203)], [560944943506]], [[193176859116, (-2063076518621), 0, 0, 0], [(-77083128157), 815615999764, 0, 0], [(-80771198907), 1256555641171, 0], [(-194186079965), 112188988701], [(-20457334528)]]], r := 4207617403243, ok := true }, Z1 := { p := [[[195962584271827679]], [[(-68057661109213414), 0], [1610609609931387]], [[959155167178639, 0, 0], [(-555401091815184), 0], [(-29052647441617)]], [[(-16504612148966), 0, 0, 0], [6524927998119, 0, 0], [10052445129374, 0], [897511909611]], [[309082974587, 0, 0, 0, 0], [(-123333005051), 0, 0, 0], [(-129233918250), 0, 0], [(-310697727944), 0], [(-32731735244)]]], r := 1598592130981, ok := true }, Z2 := { p := [[[446559622987142789876]], [[(-6277445861535923907), 24495323033978459], [(-20046462193591431911)]], [[107419941201219889, (-8507207638651677), 0], [288661546368193441, 201326201241423], [987116348631817576]], [[(-2003894330017268), 119894395897329, 0, 0], [(-4878226176537042), (-69425136476898), 0], [(-14345001993026561), (-3631580930203)], [(-49876576662752696)]], [[39812102243580, (-2063076518621), 0, 0, 0], [89013963601203, 815615999764, 0, 0], [241704826812665, 1256555641171, 0], [728462404373746, 112188988701], [2549515680368749]]], r := 681651170932527, ok := true }, Z3 := { p := [[[466028215283177643673]], [[(-13665998991999070067), 51112465381860090], [(-20944714192641714132)]], [[441255688458836079, (-18526987888824411), 0], [630236574753472386, 416683261259634], [1031795815687686543]], [[(-14612281103581107), 544623031813375, 0, 0], [(-20541948537419752), (-148781365499755), 0], [(-31345174550730295), (-7545300192538)], [(-52146670942813503)]], [[489467516151495, (-17634905140377), 0, 0, 0], [683810060789522, 3595983621463, 0, 0], [1024734632182646, 2713323750689, 0], [1592516492268047, 233224335111], [2665993788491706]]], r := 2247951663858260, ok := true }, iE := { p := [[[450617681503105221408]], [[(-6293294883295110395), 0], [(-20013109152919102763)]], [[107820759470729263, 0, 0], [288613339318032771, 0], [986514716724380761]], [[(-2012247256936761), 0, 0, 0], [(-4874883370091042), 0, 0], [(-14343429212501706), 0], [(-49857990686957832)]], [[39989925671455, 0, 0, 0, 0], [88933571436566, 0, 0, 0], [241647127332483, 0, 0], [728410679170379, 0], [2548837860684748]]], r := 681778456071057, ok := true }, iHu := { p := [[[470134250002187070931]], [[(-13700468003761721801), 0], [(-20911240637320523475)]], [[442639088278919332, 0, 0], [630136795600821693, 0], [1031189676572219370]], [[(-14660113490141279), 0, 0, 0], [(-20534299846545351), 0, 0], [(-31341826081568201), 0], [(-52127935254559572)]], [[491100277898732, 0, 0, 0, 0], [683541671889588, 0, 0, 0], [1024574358102348, 0, 0], [1592405944761877, 0], [2665310238969098]]], r := 2250262724531652, ok := true }, T := { p := [[[11529215046068469760]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[755146504207011607]], [[10546323027565058, 0], [33538030209398396]], [[(-33397155651137), 0, 0], [453120421042058, 0], [(-163692822888242)]], [[382254806047, 0, 0, 0], [(-1765165430327), 0, 0], [(-2694199867342), 0], [2859019349206]], [[(-6590718056), 0, 0, 0, 0], [20117953876, 0, 0, 0], [(-392195873), 0, 0], [46867587838, 0], [(-75238852650)]]], r := 80595641780, ok := true }, de := { p := [[[(-72754086940474060882)]], [[460782314263777090, 0], [703299321771028190]], [[(-7910984516544055), 0, 0], [102379594959045, 0], [(-18429745092558312)]], [[181864967798944, 0, 0, 0], [14903443157, 0, 0], [22747360608, 0], [646669295764460]], [[(-4703403984279), 0, 0, 0, 0], [2169501, 0, 0, 0], [397162888, 0, 0], [5054156, 0], [(-25526417641090)]]], r := 6344452407407, ok := true }, dde := { p := [[[(-3178718920799041617117)]], [[109148269742364470730, 0], [166594727501503665596]], [[(-3763800798843650135), 0, 0], [(-5744851399503540444), 0], [(-8768300475976482515)]], [[129786224637339598, 0, 0, 0], [198094733987431990, 0, 0], [302355120296606608, 0], [461489463869378474]], [[(-4475387057886914), 0, 0, 0, 0], [(-6830853936995560), 0, 0, 0], [(-10426041013978664), 0, 0], [(-15913429808900978), 0], [(-24288919158766443)]]], r := 3658162280372695, ok := true }, nJu := { p := [[[(-145508173880948121763)]], [[921564628527554181, 0], [1406598643542056381]], [[(-15821969033088110), 0, 0], [204759189918091, 0], [(-36859490185116624)]], [[363729935597888, 0, 0, 0], [29806886315, 0, 0], [45494721216, 0], [1293338591528921]], [[(-9406807968558), 0, 0, 0, 0], [4339002, 0, 0, 0], [794325776, 0, 0], [10108313, 0], [(-51052835282179)]]], r := 12688904814805, ok := true }, Jd1 := { p := [[[(-6357437841598083234233)]], [[218296539484728941461, 0], [333189455003007331193]], [[(-7527601597687300270), 0, 0], [(-11489702799007080888), 0], [(-17536600951952965030)]], [[259572449274679197, 0, 0, 0], [396189467974863981, 0, 0], [604710240593213217, 0], [922978927738756949]], [[(-8950774115773828), 0, 0, 0, 0], [(-13661707873991120), 0, 0, 0], [(-20852082027957328), 0, 0], [(-31826859617801955), 0], [(-48577838317532885)]]], r := 7316324560745381, ok := true }, term0 := { p := [[[766031369829553461332527]], [[(-52497674056233214581674), 0], [(-79944200157842503026430)]], [[2709751940783907685164, 0, 0], [5496160803058286965083, 0], [6293395478993387110815]], [[(-124456509785543632138), 0, 0, 0], [(-283986999589962051804), 0, 0], [(-433120208243226369590), 0], [(-441010554968260618202)]], [[5361148191861521650, 0, 0, 0, 0], [13050042702943177108, 0, 0, 0], [22387130357582772679, 0, 0], [30366780743125024025, 0], [28988935219756794685]]], r := 7864576220417177294, ok := true }, r0 := { p := [[[1102980104456258296399]], [[(-46973214152881933996), 441146777051682368916], [(-49113064916897739953)]], [[1608211752919876796, (-18755926727544004806), 44096573864950305983], [2152646961261482693, (-19643954331770629883)], [2422573700884857843]], [[(-49791550984231156), 635985765316136035, (-1862252036815100329), (-3619947291151194)], [(-72839770964252107), 860117174180404930, (-1963886803104490217)], [(-106967395620504070), 968973549279486490], [(-122484388279896469)]], [[1476419215264457, (-19458726754391024), 60680650789050246, 2666952381221557, (-180792213142633)], [2210638193812098, (-28927622702711223), 85635107820730256, 101716444950396], [3611102447241657, (-42745535182818156), 96874983616459508], [5431727870036213, (-48991128414039782)], [6263363657725774]]], r := 46044423742834243, ok := true }, r1 := { p := [[[2823177224224334088189]], [[(-119918486987916325293), 0], [(-125716751115030159328)]], [[4044213677533914683, 0, 0], [5501376528096057515, 0], [6201230301956518948]], [[(-122912459124960372), 0, 0, 0], [(-184391053846630941), 0, 0], [(-273423027558682284), 0], [(-313533809010709877)]], [[3578183536020501, 0, 0, 0, 0], [5524192185122460, 0, 0, 0], [9152934864363656, 0, 0], [13885796537889497, 0], [16032939110810382]]], r := 16474115252185141, ok := true }, r2 := { p := [[[415044869679212759854780]], [[(-17686336314275858608604), 761588695216908652573], [(-42977547492282879724852)]], [[605769577188666455312, (-22985219508680525759), 479834865419634579], [1807239528451139967807, (-40158831618476136005)], [3362083860220339894649]], [[(-19574615234744211322), 661676118364286783, 580110994009493, (-26893248772713)], [(-61068930082818987108), 1176618848797222891, 657752816916423], [(-140217707162386158131), 2118724772283922342], [(-234485349332793814763)]], [[624527316902945127, (-19040881937883319), (-6668597150382), 8932033265081, 1482823768], [1949615547447698064, (-32833786382655359), 14838035248962, (-1474697271011)], [4698985848362384716, (-61355762887386689), (-7728279318232)], [9722300267075813780, (-111640904212954230)], [15356165761049868961]]], r := 76446508465733578964, ok := true }, r3 := { p := [[[1508947085045480719901020]], [[(-103781533377921732580463), 3242894667563842383515], [(-158673180049720993455054)]], [[5363171171831076131092, (-171268294755311559904), 1912341978412805740], [10928264580813108204707, (-171464675653667414294)], [12522745624617195053598]], [[(-246471581851965958613), 7962327391700694814, 4829597182695069, (-214368606597037)], [(-565003059081342955785), 9069868395634643099, 2455501379572202], [(-862866641400536256592), 9052757616781036580], [(-878648015554556695169)]], [[10620904709354219203, (-345398781976360549), (-92913801337510), 70926109676418, 23794669621], [25971359242074001965, (-421073520520912875), 118910821483306, (-11731713275493)], [44617796051778052238, (-478175823351881121), (-30225969069564)], [60555919333124782322, (-477221605114501828)], [57800260277658968855]]], r := 875234014895453294763, ok := true }, eta := { p := [[[(-421379744542844856068177)]], [[17953566744515600206053, 0], [43302433283310261074999]], [[(-615654711993671882959), 0, 0], [(-1820958592717934773489), 0], [(-3379077119090131552807)]], [[19923298019542139732, 0, 0, 0], [61572878510677887276, 0, 0], [140933386152435734569, 0], [235376439866636332809]], [[(-636605693287710430), 0, 0, 0, 0], [(-1967299774901732957), 0, 0, 0], [(-4725215269550042673), 0, 0], [(-9759772666344077697), 0], [(-15402946069282803581)]]], r := 10182250935870275571, 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 := 85568392920039424, bh := 4503599627370496, tc := 11529215046068469760, th := 2305843009213693952, sc := 17870283321406128128, sh := 576460752303423488 }
noncomputable def q7 : Cert := { V0 := [[[39722743335137569]], [[(-40255642538030924), 7944495519629080], [328097141662405]], [[541511344342282, (-8050966926612989), (-15944093743)], [(-331678627270575), 65618111392575], [(-5904374113579)]], [[(-8762585219097), 108136347124427, 48473660581, (-1062897655)], [3641958021378, (-66331724932053), (-395076778)], [5975923036203, (-1180862000786)], [182340128280]], [[153230450482, (-1692762133881), (-49775222783), 3231364915, 6288], [(-61629943312), 724290245476, 1200130309, (-26336722)], [(-72716127777), 1195145601791, 3846570], [(-184580447272), 36467655315], [(-6648246147)]]], r0 := 14437493769146, V1 := [[[63556057699515042]], [[(-64408019810962920), 0], [524947209081269]], [[865382830911375, 0, 0], [(-530660841015503), 0], [(-9446918573056)]], [[(-13647298420565), 0, 0, 0], [5801541660638, 0, 0], [9561233464882, 0], [291741894342]], [[230626613687, 0, 0, 0, 0], [(-89434083139), 0, 0, 0], [(-116095577251), 0, 0], [(-295321687212), 0], [(-10637114654)]]], r1 := 5084739696630, V2 := [[[18278274372818262704]], [[(-2671229794650341), 3614924871240], [(-8867375812494822)]], [[4197293701836, (-3556221738466), (-72551803)], [(-140088679279087), 385796069667], [(-30115758809)]], [[(-53391029430), (-58781461070), 143907938, 1418], [268410777633, (-379527967172), (-11632925)], [28280667335, 10475921325], [(-37219209)]], [[962587339, 79402698, (-70159039), (-4230), 0], [(-3230489952), (-6277394436), 23073966, 303], [1849378392, (-10305929987), (-627857)], [51482399, 7609872], [514703]]], r2 := 2038272892466, V3 := [[[18280933976060715216]], [[(-5327392814329752), 7112978326833], [(-8728001219136753)]], [[704305172372, (-6878931512338), (-285446849)], [(-279273388833377), 759117651118], [(-61819189612)]], [[320832045, (-233969514438), 561361954, 11156], [75317206296, (-734132581252), (-45767922)], [59765791662, 20613805446], [(-44691264)]], [[(-2956282), (-78293262), (-266389106), (-33089), 0], [36382371, (-24977668008), 90006376, 2385], [2052373378, (-19936499049), (-2470213)], [43156906, 15034627], [376496]]], r3 := 5535446478770, Vm := [[[18278285259757895674]], [[(-2681982653379614), 0], [(-8866213528800686)]], [[4062841359054, 0, 0], [(-141237036921931), 0], [1469601070]], [[(-53016455958), 0, 0, 0], [254439615836, 0, 0], [(-2951666483), 0], [(-13671664)]], [[959412203, 0, 0, 0, 0], [(-3185007765), 0, 0, 0], [1494753715, 0, 0], [27510500, 0], [317521]]], rm := 369893147769 }
noncomputable def w7 : Wit := { Z0 := { p := [[[39722876204419835]], [[(-40256046494497565), 7944575240883967], [328100434044634]], [[541926156830141, (-8051209298899513), 0], [(-331688628740169), 65620086808926], [(-5904406168456)]], [[(-8911980894588), 108385231366028, 0, 0], [3652211753628, (-66337725748034), 0], [5976020550069, (-1180881233692)], [182341054135]], [[159068086713, (-1782396178918), 0, 0, 0], [(-65306240390), 730442350725, 0, 0], [(-72816380348), 1195204110013, 0], [(-184583263186), 36468210827], [(-6648277868)]]], r := 3575924408101, ok := true }, Z1 := { p := [[[63556601927071736]], [[(-64409674391196103), 0], [524960694471415]], [[867081850928225, 0, 0], [(-530701805984270), 0], [(-9447049869529)]], [[(-14259169431341), 0, 0, 0], [5843538805805, 0, 0], [9561632880110, 0], [291745686617]], [[254508938741, 0, 0, 0, 0], [(-104489984624), 0, 0, 0], [(-116506208557), 0, 0], [(-295333221097), 0], [(-10637244588)]]], r := 1269424984367, ok := true }, Z2 := { p := [[[434418991288932178317]], [[(-5870602251827851779), 7944575240883967], [(-19487966372975437691)]], [[96289448935880699, (-8051209298899513), 0], [270164367498850224, 65620086808926], [959359405125716661]], [[(-1716057921638486), 108385231366028, 0, 0], [(-4382838576716653), (-66337725748034), 0], [(-13428199430427673), (-1180881233692)], [(-48466963472569767)]], [[32461166776383, (-1782396178918), 0, 0, 0], [76528332663951, 730442350725, 0, 0], [217305954443690, 1195204110013, 0], [681972219948988, 36468210827], [2477212512591187]]], r := 630373930121942, ok := true }, Z3 := { p := [[[440351678678123769918]], [[(-12061881488182533516), 16104669694244775], [(-19761282864437159680)]], [[364131404366923921, (-16542855409597853), 0], [555596390065297916, 132679606226284], [972948255638517594]], [[(-11276832555138106), 451422707724891, 0, 0], [(-16934387903238123), (-135610022208054), 0], [(-27622387633330200), (-2390602511444)], [(-49157211053844920)]], [[353294524008726, (-13646991436859), 0, 0, 0], [527230695896833, 3013629880001, 0, 0], [844475744234361, 2449256345880, 0], [1403057070311056, 73839848754], [2512622548890357]]], r := 1847301814264514, ok := true }, iE := { p := [[[438446890936060349616]], [[(-5884942843037313667), 0], [(-19454696988963311707)]], [[96644123534497557, 0, 0], [270128624990767773, 0], [958760698340235292]], [[(-1723132028902663), 0, 0, 0], [(-4379935441721359), 0, 0], [(-13426842138300467), 0], [(-48448474089680393)]], [[32604582610372, 0, 0, 0, 0], [76461626637353, 0, 0, 0], [217255686153725, 0, 0], [681927201005535, 0], [2476538377215448]]], r := 630678772624851, ok := true }, iHu := { p := [[[444393950771379208620]], [[(-12091342754264931806), 0], [(-19727980283274362233)]], [[365262960875484131, 0, 0], [555524253685005260, 0], [972348214408145318]], [[(-11313557358604933), 0, 0, 0], [(-16928153294690688), 0, 0], [(-27619618533443599), 0], [(-49138677251807539)]], [[354468828771267, 0, 0, 0, 0], [527024352207967, 0, 0, 0], [844345038437334, 0, 0], [1402965103798837, 0], [2511946710173110]]], r := 1849723038098289, ok := true }, T := { p := [[[11529215046068469760]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[776108518398782695]], [[10417120899227169, 0], [34437366002906582]], [[(-31251599066179), 0, 0], [446290618796003, 0], [(-169082791863289)]], [[334521821622, 0, 0, 0], [(-1652245722190), 0, 0], [(-2695769336204), 0], [2952754168165]], [[(-5395623690), 0, 0, 0, 0], [17605690908, 0, 0, 0], [(-392538625), 0, 0], [46867227044, 0], [(-77705700885)]]], r := 81377299887, ok := true }, de := { p := [[[(-71862782658079122626)]], [[431179957137081271, 0], [703504140592079968]], [[(-6923122768973246), 0, 0], [102439234775791, 0], [(-18429698008263959)]], [[148887408073480, 0, 0, 0], [14916467745, 0, 0], [24337394742, 0], [646669306592367]], [[(-3602114378644), 0, 0, 0, 0], [2172029, 0, 0, 0], [397854381, 0, 0], [5782050, 0], [(-25526417638599)]]], r := 6152819482569, ok := true }, dde := { p := [[[(-2974506281151132434455)]], [[95518689218406450993, 0], [155846282408978945994]], [[(-3081311108053764124), 0, 0], [(-5027505235838259568), 0], [(-8202603808420131124)]], [[99397123334243942, 0, 0, 0], [162174223893533194, 0, 0], [264600049510501486, 0], [431715950029224780]], [[(-3206358818570701), 0, 0, 0, 0], [(-5231427552634688), 0, 0, 0], [(-8535487855302780), 0, 0], [(-13926320991917255), 0], [(-22721892116277565)]]], r := 3135654958925864, ok := true }, nJu := { p := [[[(-143725565316158245252)]], [[862359914274162542, 0], [1407008281184159936]], [[(-13846245537946491), 0, 0], [204878469551583, 0], [(-36859396016527918)]], [[297774816146961, 0, 0, 0], [29832935491, 0, 0], [48674789484, 0], [1293338613184734]], [[(-7204228757287), 0, 0, 0, 0], [4344059, 0, 0, 0], [795708763, 0, 0], [11564101, 0], [(-51052835277197)]]], r := 12305638965129, ok := true }, Jd1 := { p := [[[(-5949012562302264868909)]], [[191037378436812901987, 0], [311692564817957891989]], [[(-6162622216107528248), 0, 0], [(-10055010471676519136), 0], [(-16405207616840262248)]], [[198794246668487885, 0, 0, 0], [324348447787066388, 0, 0], [529200099021002972, 0], [863431900058449561]], [[(-6412717637141401), 0, 0, 0, 0], [(-10462855105269376), 0, 0, 0], [(-17070975710605560), 0, 0], [(-27852641983834510), 0], [(-45443784232555130)]]], r := 6271309917851721, ok := true }, term0 := { p := [[[670958588867477175770845]], [[(-42996759779869729529917), 0], [(-69991734480051189785639)]], [[2075867072831633025846, 0, 0], [4500515517093477905995, 0], [5509127245852688842090]], [[(-89185208049382987782), 0, 0, 0], [(-217523583109960641855), 0, 0], [(-354633763223378237147), 0], [(-386025157018346817802)]], [[3593772974831123897, 0, 0, 0, 0], [9350621621165453061, 0, 0, 0], [17146895016141541777, 0, 0], [24863069877217873369, 0], [25373486776013775011]]], r := 6207222425919963836, ok := true }, r0 := { p := [[[1015090508985948812747]], [[(-41093845497186193152), 406031820393643887645], [(-45082413461993230574)]], [[1341724390507595546, (-16428476977148593806), 40601428779976236264], [1885904642826826248, (-18032843123638151764)], [2222259084342937409]], [[(-39523197453494577), 531703804868911224, (-1639223294615546224), (-350643515287736)], [(-60977206657963308), 754108665261846228, (-1803235408137942924)], [(-93736908882501925), 888898257670029139], [(-112311709170703544)]], [[1111369100925185, (-15487755977666997), 51176133369165021, 724846384048535, (-17530085218083)], [1764136525780475, (-24250890185606019), 75309590755131128, 9780750060377], [3025971172259328, (-37483629523250994), 88887675351364543], [4760652836628324, (-44924431283756505)], [5741585979879588]]], r := 37356965678474308, ok := true }, r1 := { p := [[[2598587941940897144100]], [[(-105109780567663111373), 0], [(-115409757816503945201)]], [[3385039896239245140, 0, 0], [4825388056038921842, 0], [5688929581698222312]], [[(-97973032839879948), 0, 0, 0], [(-154704023712726942), 0, 0], [(-239855326378076433), 0], [(-287515455689494212)]], [[2705565582281625, 0, 0, 0, 0], [4421699883287588, 0, 0, 0], [7685015820729258, 0, 0], [12182052166874889, 0], [14698337944792307]]], r := 12646026480225306, ok := true }, r2 := { p := [[[381948069815269460162383]], [[(-15479652942694163016621), 718121044915485076350], [(-39592673686489926910725)]], [[501852885418399974831, (-20550419904334429417), 480969590995677230], [1584533922584620038968, (-37929985383775756275)], [3099323545107982020271]], [[(-15285547235075993718), 559580819718522265, 555174981334010, (-8985683980033)], [(-50706475585447457175), 1055512498337434967, 687120135643067], [(-123069949825005904650), 2002428153182677364], [(-216259468481510146108)]], [[458120320941737303, (-15177135984355529), (-5827237744518), 8975180296279, 161004915], [1526205688581165557, (-27900975893855027), 14537731275372, (-493396677596)], [3906991501735206639, (-55108430017088295), (-7831353218755)], [8539755295596450686, (-105551387933339165)], [14167577740820694132]]], r := 66761853593768001396, ok := true }, r3 := { p := [[[1321021852264769198641793]], [[(-84978684201805896441012), 2929656667584275093823], [(-138885429665445841355784)]], [[4107908894149112954526, (-143146787377041244294), 1921654555286173943], [8947468350584308839592, (-154874420397012756599)], [10960380914625773014785]], [[(-176599240089176262306), 6193017833080160695, 4494641027979006, (-71801546757610)], [(-432735705296893086583), 7582600767553865868, 2690600888921430], [(-706446440405886042103), 8178080595835537003], [(-769002187987683619371)]], [[7118880853909773028, (-250525540371704015), (-75392024851629), 71632560265141, 2638953543], [18607852091298635512, (-327557949772792137), 116305512706049, (-3939930634099)], [34172054956283430945, (-399780095528668463), (-31128492559329)], [49577597131042960578, (-431139619206809987)], [50586471935782231342]]], r := 663751387974221372471, ok := true }, eta := { p := [[[(-387785415706620554584688)]], [[15711171226289547311633, 0], [39892004807885522597453]], [[(-509905684033706459215), 0, 0], [(-1596431419435173453757), 0], [(-3114983487313487741496)]], [[15552188917224683745, 0, 0, 0], [51117449403612626978, 0, 0], [123690803748217090271, 0], [217080740823323859564]], [[(-466778874175289298), 0, 0, 0, 0], [(-1539742262542826367), 0, 0, 0], [(-3928389423591842890), 0, 0], [(-8572269099342972691), 0], [(-14210696368619239464)]]], r := 8984736612626574075, 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 72057594037927936 90071992547409920 9223372036854775808 13835058055282163712 13835058055282163712 18446744073709551616 :=
  (RegionPosI.split_s 16140901064495857664 (RegionPosI.split_b 81064793292668928 (RegionPosI.split_s 14987979559889010688 (RegionPosI.of_check c0 q0 ok_0 72057594037927936 81064793292668928 9223372036854775808 13835058055282163712 13835058055282163712 14987979559889010688 (by decide +kernel)) (RegionPosI.of_check c1 q1 ok_1 72057594037927936 81064793292668928 9223372036854775808 13835058055282163712 14987979559889010688 16140901064495857664 (by decide +kernel))) (RegionPosI.split_s 14987979559889010688 (RegionPosI.of_check c2 q2 ok_2 81064793292668928 90071992547409920 9223372036854775808 13835058055282163712 13835058055282163712 14987979559889010688 (by decide +kernel)) (RegionPosI.of_check c3 q3 ok_3 81064793292668928 90071992547409920 9223372036854775808 13835058055282163712 14987979559889010688 16140901064495857664 (by decide +kernel)))) (RegionPosI.split_b 81064793292668928 (RegionPosI.split_s 17293822569102704640 (RegionPosI.of_check c4 q4 ok_4 72057594037927936 81064793292668928 9223372036854775808 13835058055282163712 16140901064495857664 17293822569102704640 (by decide +kernel)) (RegionPosI.of_check c5 q5 ok_5 72057594037927936 81064793292668928 9223372036854775808 13835058055282163712 17293822569102704640 18446744073709551616 (by decide +kernel))) (RegionPosI.split_s 17293822569102704640 (RegionPosI.of_check c6 q6 ok_6 81064793292668928 90071992547409920 9223372036854775808 13835058055282163712 16140901064495857664 17293822569102704640 (by decide +kernel)) (RegionPosI.of_check c7 q7 ok_7 81064793292668928 90071992547409920 9223372036854775808 13835058055282163712 17293822569102704640 18446744073709551616 (by decide +kernel)))))

end CKLaneC.RSC2.S07_0083