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

import Definitions.Def_CK_CKLaneC_RSC2_S00_0091_part00

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

namespace CKLaneC.RSC2.S00_0091
open CKLaneC.TM3 CKLaneC.RSCell

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 := 1073123348709376, bh := 17592186044416, tc := 6917529027641081856, th := 2305843009213693952, sc := 8935141660703064064, sh := 288230376151711744 }
noncomputable def q6 : Cert := { V0 := [[[303089022165714636]], [[(-12221612678415444), 100990330013819039], [452001345841224]], [[127051610590445, (-4069111755816868), (-19662986697182)], [(-17990522482419), 150491104439583], [(-3030894106610)]], [[(-1507309118868), 42109190941562, 2377747269703, (-2179759884323)], [184303047820, (-5975642986468), (-87938064662)], [120997675574, (-1009380237068)], [30446705324]], [[19813173461, (-495282983985), (-120507178775), 263183049768, 1252657677], [(-2435705356), 60364222222, 10585377526, (-9733502104)], [(-1244100036), 40221741945, 458648440], [(-1216679286), 10140434961], [(-355014541)]]], r0 := 487661984320, V1 := [[[807277668414387208]], [[(-32475039339087069), 0], [1201049474709520]], [[332941687430230, 0, 0], [(-47459576890418), 0], [(-8060005288300)]], [[(-3846675815998), 0, 0, 0], [465589673113, 0, 0], [319962920372, 0], [80984726829]], [[49098918759, 0, 0, 0, 0], [(-5736001962), 0, 0, 0], [(-3181513588), 0, 0], [(-3219570369), 0], [(-944419805)]]], r1 := 111829396804, V2 := [[[18445160884826447723]], [[(-17468180414497), 6526550596], [(-25938550965349)]], [[17319996802, (-125120080), (-25809)], [(-287478525725), 214884975], [147333343]], [[(-234940187), (-2269444), 1275, 0], [310982410, (-4112263), (-1275)], [(-10854388), 1777581], [(-671144)]], [[4097721, 3011, (-6), 0, 0], [(-4196005), (-75042), 63, 0], [264759, (-33886), (-21)], [47541, 107], [4986]]], r2 := 208161010, V3 := [[[18445704442764075396]], [[(-33535199528824), 8540619771], [(-17043836123355)]], [[41868610, 18966924, (-67397)], [(-549758971099), 281195212], [(-11628870)]], [[8490, (-8374078), 1881, 0], [1378801, 630978, (-3330)], [(-26733), 2326049], [(-692)]], [[(-85), (-1688), 71, (-1), 0], [305, (-275778), 93, 0], [11411, 5339, (-55)], [(-6), 140], [2]]], r3 := 2273463614, Vm := [[[18445160918379678725]], [[(-17468861901091), 0], [(-25937444742938)]], [[17309536420, 0, 0], [(-287501015010), 0], [156511180]], [[(-234928301), 0, 0, 0], [310637642, 0, 0], [(-11041346), 0], [(-670413)]], [[4097602, 0, 0, 0, 0], [(-4195592), 0, 0, 0], [261900, 0, 0], [47524, 0], [4984]]], rm := 26670893 }
noncomputable def w6 : Wit := { Z0 := { p := [[[303148058562746490]], [[(-12228755484016871), 101049352854248830], [452265513740330]], [[127414002793794, (-4076251828005624), 0], [(-18022349740258), 150755171246776], [(-3032271368793)]], [[(-1518059921287), 42471334264598, 0, 0], [185911007934, (-6007449913420), 0], [121164014321, (-1010757122931)], [30459410367]], [[20048129812, (-506019973763), 0, 0, 0], [(-2483372823), 61970335978, 0, 0], [(-1252524255), 40388004773, 0], [(-1218214615), 10153136789], [(-355155156)]]], r := 100021062056, ok := true }, Z1 := { p := [[[808394822833990640]], [[(-32610014624044989), 0], [1206041369974214]], [[339770674116784, 0, 0], [(-48059599307353), 0], [(-8086056983447)]], [[(-4048159790097), 0, 0, 0], [495762687824, 0, 0], [323104038191, 0], [81225094313]], [[53461679498, 0, 0, 0, 0], [(-6622327528), 0, 0, 0], [(-3340064678), 0, 0], [(-3248572305), 0], [(-947080415)]]], r := 27930750144, ok := true }, Z2 := { p := [[[26947221318497551668528]], [[(-270456545224477268497), 101049352854248830], [(-401601696098546334293)]], [[3130712474340359507, (-4076251828005624), 0], [4050242176914923179, 150755171246776], [6314022581366596587]], [[(-40076087404974425), 42471334264598, 0, 0], [(-46430535436646415), (-6007449913420), 0], [(-63794413718581597), (-1010757122931)], [(-100800526238367867)]], [[567723187647060, (-506019973763), 0, 0, 0], [584659633218088, 61970335978, 0, 0], [728673387963935, 40388004773, 0], [1019565258063129, 10153136789], [1620892778628053]]], r := 566337086618137, ok := true }, Z3 := { p := [[[39533588114454961549091]], [[(-1164186067806692423209), 296490573739342588], [(-591682674788802364778)]], [[36074435806598435144, (-17715422348442877), 0], [17582190411187499791, 423507032717705], [9317430088525606872]], [[(-1134345446867776454), 535113471024768, 0, 0], [(-546686530856841536), (-24114150166308), 0], [(-277823405948410885), (-2866382912579)], [(-148892666491355204)]], [[35917202254205501, (-16705322638808), 0, 0, 0], [17225889058989060, 677367133440, 0, 0], [8650146708594545, 164911703144, 0], [4448807346697668, 28885152793], [2395863720695474]]], r := 13455084737789965, ok := true }, iE := { p := [[[26950053762479072279676]], [[(-270475785857835506199), 0], [(-401597470385412901914)]], [[3130949340866192799, 0, 0], [4050215543202112879, 0], [6313994249538150801]], [[(-40079232494280569), 0, 0, 0], [(-46430151603366742), 0, 0], [(-63794232057836103), 0], [(-100800241642866958)]], [[567769198479321, 0, 0, 0, 0], [584653694965581, 0, 0, 0], [728670861593677, 0, 0], [1019563422873389, 0], [1620889460259178]]], r := 566295125139314, ok := true }, iHu := { p := [[[39537298738908123624516]], [[(-1164268382147768993055), 0], [(-591677374534120170464)]], [[36077027965853323966, 0, 0], [17582087733362095621, 0], [9317394215309155510]], [[(-1134427319552075372), 0, 0, 0], [(-546683357149259486), 0, 0], [(-277822689700889383), 0], [(-148892304989291454)]], [[35919800000912796, 0, 0, 0, 0], [17225790856222601, 0, 0, 0], [8650124532208957, 0, 0], [4448800055335161, 0], [2395859497581081]]], r := 13454515458722456, ok := true }, T := { p := [[[6917529027641081856]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[12626407721482656]], [[126720992140808, 0], [188152997604107]], [[(-195089889076), 0, 0], [1879105229805, 0], [(-154407775925)]], [[2097681632, 0, 0, 0], [(-3198285024), 0, 0], [(-1625357963), 0], [843717511]], [[(-33833574), 0, 0, 0, 0], [34388224, 0, 0, 0], [(-1477), 0, 0], [8881237, 0], [(-6915717)]]], r := 23683545, ok := true }, de := { p := [[[(-139411505369220806718)]], [[429254453568100904, 0], [218145705911657837]], [[(-6923263833131264), 0, 0], [198293671519, 0], [(-1788029170556072)]], [[148887394379115, 0, 0, 0], [180249, 0, 0], [91602, 0], [19541302425966]], [[(-3602114380139), 0, 0, 0, 0], [1, 0, 0, 0], [1478, 0, 0], [1, 0], [(-240261915074)]]], r := 496299382525, ok := true }, dde := { p := [[[(-472242274522885217644124)]], [[15233192492253266912868, 0], [7741458479669693014882]], [[(-491393306591920005405), 0, 0], [(-249724467482717663921), 0], [(-126909155505196173340)]], [[15851396986835823613, 0, 0, 0], [8055627976916190595, 0, 0], [4093843725973800778, 0], [2080477959101555631]], [[(-511335386672101741), 0, 0, 0, 0], [(-259858966997291460), 0, 0, 0], [(-132059475031395339), 0, 0], [(-67112192229078024), 0], [(-34106196050840138)]]], r := 34072639451646948, ok := true }, nJu := { p := [[[(-278823010738441613435)]], [[858508907136201808, 0], [436291411823315675]], [[(-13846527666262527), 0, 0], [396587343038, 0], [(-3576058341112144)]], [[297774788758230, 0, 0, 0], [360498, 0, 0], [183204, 0], [39082604851932]], [[(-7204228760278), 0, 0, 0, 0], [2, 0, 0, 0], [2957, 0, 0], [2, 0], [(-480523830148)]]], r := 992598765046, ok := true }, Jd1 := { p := [[[(-944484549045770435288247)]], [[30466384984506533825737, 0], [15482916959339386029764]], [[(-982786613183840010810), 0, 0], [(-499448934965435327842), 0], [(-253818311010392346680)]], [[31702793973671647227, 0, 0, 0], [16111255953832381190, 0, 0], [8187687451947601557, 0], [4160955918203111262]], [[(-1022670773344203482), 0, 0, 0, 0], [(-519717933994582920), 0, 0, 0], [(-264118950062790678), 0, 0], [(-134224384458156047), 0], [(-68212392101680275)]]], r := 68145278903293890, ok := true }, term0 := { p := [[[16761116990219706910534605686]], [[(-1081316682595646850226954052), 0], [(-549505610428615542953979346)]], [[52321037874349698446561531, 0, 0], [35451225692963786494669519, 0], [13512111676594864763821271]], [[(-2250351369005154136350219), 0, 0, 0], [(-1715369804927183502009267), 0, 0], [(-871736858894297630088301), 0], [(-295343191108824071888835)]], [[90739591055117986100094, 0, 0, 0, 0], [73779086589512901971329, 0, 0, 0], [42180617663735476222246, 0, 0], [19054198089798752574601, 0], [6052071389056797029653]]], r := 10138766939022019536191, ok := true }, r0 := { p := [[[39099578142624870610836]], [[(-1265070620846842773023), 26050086008470653757445], [(-583572399117263856478)]], [[30993079688910683962, (-841545236193277203027), 4330822250925830298751], [18837940691616624298, (-388853473033680110145)], [9180462467153453031]], [[(-703597713763227560), 20567413917907495147, (-139035541419128546968), (-3614567275984691324)], [(-455295887490158434), 12536677209686516288, (-64679117693426727897)], [(-296089466486960088), 6117494095266231150], [(-146614253162992134)]], [[16061480435076583, (-465787311713319834), 3364939901003439581, 406364350387553966, (-299126135186018612)], [10141691999289851, (-302400132008022025), 2074825988104457482, 43219812975283214], [7119274159317881, (-197075790487041214), 1017707103260297331], [4726117966217400, (-97700201431641417)], [2358179212263784]]], r := 366363751903449268, ok := true }, r1 := { p := [[[276983444232722566244650]], [[(-8877294956019355767431), 0], [(-4137190802109543470002)]], [[214303409499575233486, 0, 0], [132535655918684064003, 0], [65100378729890545030]], [[(-4794081565613727186), 0, 0, 0], [(-3164667132728281321), 0, 0], [(-2084952636290977295), 0], [(-1039818848761650861)]], [[108317675051568230, 0, 0, 0, 0], [69620848224281179, 0, 0, 0], [49570800566843567, 0, 0], [33296168783731566, 0], [16726357466289710]]], r := 36420312194810948, ok := true }, r2 := { p := [[[4625790764795494134949805389]], [[(-138529200736703981188412266), 97172752019000368608159], [(-149984788513984927874022150)]], [[3603071577263693588576669, (-2079253206230432373308), 450032350136061138], [4442293896200949918789223, (-1583743411592113056783)], [3663246143291466890669282]], [[(-95800391105258043532063), 44636654168592846210, (-626134781001640), (-9581396860822)], [(-114299674567207817745527), 33194860459222973140, (-823595180512106)], [(-107758271480890762151947), 25899104937087229367], [(-79687535786537952185210)]], [[2682730629968226410251, (-1033436661390746340), (-795513993816410), (-95274043519279), (-2012580971743)], [3013343469620830717633, (-696009241967378569), (-424942877891557), (-7847379719139)], [2753822182954117290307, (-538624142499369668), (-223449502731827)], [2332593423787974204579, (-424247663813972189)], [1626933693529294685274]]], r := 10612435166385556572558, ok := true }, r3 := { p := [[[33515752405765977127484383074]], [[(-2162283162822471662435152389), 717434096297736979934604], [(-1098904875284528357452331673)]], [[104626227100244156266306966, (-38787882372757543489018), 1765712298180611038], [70896706585381693902176200, (-11779594474470290424784)], [27022479425388895624590023]], [[(-4500044651237593482674334), 1755783027555258663174, (-4181331714180628), (-16654618686181434)], [(-3430479652760941243280875), 636614658418268774614, (-6803551840585478)], [(-1743379532182992733015550), 193208704673693179533], [(-590657789030344632142762)]], [[181453214173015660723003, (-72930739866806422120), (-5851721669771163), 1922728711849214, (-1673338066478937)], [147547367806309002642863, (-28819365328399341392), (-15358248871451940), 924011339932944], [84356966954963199694439, (-10446503361221351181), (-7501783141816632)], [38106838587528479311125, (-3172851656992408763)], [12103658560923099450438]]], r := 879110237225384307530564, ok := true }, eta := { p := [[[(-4626980180748103163855732213)]], [[138569631798335173986910559, 0], [150004125427211778774639301]], [[(-3604344541775430541759645), 0, 0], [(-4442947586564862472299670), 0], [(-3663562077011566476326332)]], [[95840332779824401941247, 0, 0, 0], [114320191011993365732230, 0, 0], [107768926644789534681910, 0], [79692704143609586739078]], [[(-2683994552847943833046), 0, 0, 0, 0], [(-3013987139035229761606), 0, 0, 0], [(-2754156698584085777044), 0, 0], [(-2332768115644029232206), 0], [(-1627018549683060768365)]]], r := 980226516406163027411, 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 := 1108307720798208, bh := 17592186044416, tc := 6917529027641081856, th := 2305843009213693952, sc := 8935141660703064064, sh := 288230376151711744 }
noncomputable def q7 : Cert := { V0 := [[[303981139314050919]], [[(-12257119244578642), 101287353979839352], [440232116787618]], [[127415338200715, (-4080905317449241), (-19837061351289)], [(-17520691585757), 146571600590826], [(-2856389526740)]], [[(-1512117489721), 42228315255635, 2398700593727, (-2199027272378)], [179472406806, (-5819464030766), (-86152791603)], [114024492501, (-951260683356)], [27776734216]], [[19886280679, (-496823074884), (-121563849299), 265496274188, 1271187669], [(-2373279037), 58775841592, 10369903238, (-9535681629)], [(-1172319801), 37903223810, 434340986], [(-1109924921), 9251150945], [(-313559401)]]], r0 := 459938619066, V1 := [[[809648160481338018]], [[(-32568703811301584), 0], [1169751973019268]], [[333860391984691, 0, 0], [(-46217194363982), 0], [(-7595845951271)]], [[(-3857995444757), 0, 0, 0], [453237650825, 0, 0], [301510850456, 0], [73882032098]], [[49261272479, 0, 0, 0, 0], [(-5585121075), 0, 0, 0], [(-2997324102), 0, 0], [(-2936971076), 0], [(-834130449)]]], r1 := 102604885369, V2 := [[[18445109008308559579]], [[(-18043180508724), 6963431722], [(-25937969529750)]], [[17943011682, (-133480156), (-28445)], [(-287521383845), 221996575], [143422565]], [[(-243345376), (-2422035), 1405, 0], [312028045, (-4247818), (-1361)], [(-10577377), 1778217], [(-633027)]], [[4244337, 3222, (-7), 0, 0], [(-4209127), (-77550), 67, 0], [258123, (-33892), (-22)], [44837, 105], [4552]]], r2 := 196636090, V3 := [[[18445670355045307707]], [[(-34634717577998), 9112315504], [(-17043882647068)]], [[44671862, 20250244, (-74278)], [(-549759078100), 290501073], [(-11632969)]], [[9113, (-8934764), 2073, 0], [1424453, 652347, (-3553)], [(-26768), 2326878], [(-675)]], [[(-91), (-1812), 78, (-1), 0], [317, (-284910), 99, 0], [11415, 5345, (-57)], [(-6), 136], [2]]], r3 := 2224880855, Vm := [[[18445109044110952568]], [[(-18043907721856), 0], [(-25936826587284)]], [[17931850326, 0, 0], [(-287544621166), 0], [152604738]], [[(-243332647), 0, 0, 0], [311671838, 0, 0], [(-10764437), 0], [(-632313)]], [[4244210, 0, 0, 0, 0], [(-4208698), 0, 0, 0], [255262, 0, 0], [44820, 0], [4550]]], rm := 26095809 }
noncomputable def w7 : Wit := { Z0 := { p := [[[304040698637276050]], [[(-12264325051357880), 101346899545758683], [440490923731428]], [[127780913236361, (-4088108350452627), 0], [(-17551871384664), 146830307910476], [(-2857693801795)]], [[(-1522962645751), 42593637745453, 0, 0], [181047576897, (-5850623794888), 0], [114182011310, (-952564600599)], [27788379344]], [[20123320638, (-507654215251), 0, 0, 0], [(-2419974014), 60349192299, 0, 0], [(-1180297084), 38060670436, 0], [(-1111332124), 9262793114], [(-313684164)]]], r := 92964980333, ok := true }, Z1 := { p := [[[810775196366069467]], [[(-32704866803621012), 0], [1174642463283809]], [[340749101963630, 0, 0], [(-46804990359104), 0], [(-7620516804786)]], [[(-4061233722001), 0, 0, 0], [482793538393, 0, 0], [304485363494, 0], [74102344917]], [[53662188369, 0, 0, 0, 0], [(-6453264036), 0, 0, 0], [(-3147458889), 0, 0], [(-2963552330), 0], [(-836491102)]]], r := 25616306126, ok := true }, Z2 := { p := [[[26168492735417422315671]], [[(-262603336306354537919), 101346899545758683], [(-377505359004285756054)]], [[3040676028252868162, (-4088108350452627), 0], [3806794678896461729, 146830307910476], [5746124249132573835]], [[(-38942115627781197), 42593637745453, 0, 0], [(-43649543256966729), (-5850623794888), 0], [(-58050579835755659), (-952564600599)], [(-88816178307475311)]], [[551977040790416, (-507654215251), 0, 0, 0], [549856085377843, 60349192299, 0, 0], [663202572827400, 38060670436, 0], [898259263397499, 9262793114], [1382777990283750]]], r := 504243476213044, ok := true }, Z3 := { p := [[[38386338477936287454951]], [[(-1130098501270125580727), 297326348088236337], [(-556125979427971002009)]], [[35014588933579982450, (-17763004039126943), 0], [16522077639685138916, 412377655420909], [8478622122565430463]], [[(-1100950925131742079), 536449762625772, 0, 0], [(-513680762301257083), (-23473910513921), 0], [(-252762704868137365), (-2700842505541)], [(-131179163530059269)]], [[34858293464349766, (-16745665642000), 0, 0, 0], [16185052452896251, 659107109280, 0, 0], [7869253576414815, 155354881742, 0], [3918813293293068, 26347559522], [2043731934354197]]], r := 12335476087019556, ok := true }, iE := { p := [[[26171333519722871612100]], [[(-262622629494841874494), 0], [(-377501243306260992706)]], [[3040913652536984840, 0, 0], [3806768750470347290, 0], [5746097548458163127]], [[(-38945272444500993), 0, 0, 0], [(-43649169235591648), 0, 0], [(-58050408691757429), 0], [(-88815918668577399)]], [[552023250219648, 0, 0, 0, 0], [549850294780809, 0, 0, 0], [663200191041812, 0, 0], [898257589656260, 0], [1382775059396368]]], r := 504204097034450, ok := true }, iHu := { p := [[[38390059562232058412749]], [[(-1130181018158856603766), 0], [(-556120818459131946388)]], [[35017187353310771550, 0, 0], [16521977742011292524, 0], [8478588321112255061]], [[(-1101032991522392967), 0, 0, 0], [(-513677674670022401), 0, 0], [(-252762030395850463), 0], [(-131178833786359792)]], [[34860897257681561, 0, 0, 0, 0], [16184956922483960, 0, 0, 0], [7869232694655160, 0, 0], [3918806646171725, 0], [2043728204987730]]], r := 12334903625079067, ok := true }, T := { p := [[[6917529027641081856]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[13002102726806017]], [[130472771076130, 0], [187545275110497]], [[(-201486465035), 0, 0], [1872708099110, 0], [(-149506178962)]], [[2166458079, 0, 0, 0], [(-3198290934), 0, 0], [(-1573762205), 0], [790998453]], [[(-34942871), 0, 0, 0, 0], [34388224, 0, 0, 0], [(-1477), 0, 0], [8326300, 0], [(-6277765)]]], r := 23987027, ok := true }, de := { p := [[[(-138982213489699406216)]], [[429254850155810346, 0], [211220640552859060]], [[(-6923263832764857), 0, 0], [198294037925, 0], [(-1676305503473678)]], [[148887394379115, 0, 0, 0], [186159, 0, 0], [91602, 0], [17738682591465]], [[(-3602114380139), 0, 0, 0, 0], [1, 0, 0, 0], [1478, 0, 0], [1, 0], [(-211174792756)]]], r := 493906101695, ok := true }, dde := { p := [[[(-457250878737248496760530)]], [[14749599079020174554088, 0], [7257739229359133502371]], [[(-475793519081066510274), 0, 0], [(-234120620698507142489), 0], [(-115202210087403581735)]], [[15348178034872767769, 0, 0, 0], [7552278080651305315, 0, 0], [3716200325399871835, 0], [1828606509323854969]], [[(-495102517253939335), 0, 0, 0, 0], [(-243621873569391461), 0, 0, 0], [(-119877429851591266), 0, 0], [(-58987306752378549), 0], [(-29025500147981172)]]], r := 32040321108619339, ok := true }, nJu := { p := [[[(-277964426979398812431)]], [[858509700311620693, 0], [422441281105718121]], [[(-13846527665529713), 0, 0], [396588075850, 0], [(-3352611006947355)]], [[297774788758231, 0, 0, 0], [372318, 0, 0], [183205, 0], [35477365182931]], [[(-7204228760278), 0, 0, 0, 0], [2, 0, 0, 0], [2957, 0, 0], [2, 0], [(-422349585511)]]], r := 987812203380, ok := true }, Jd1 := { p := [[[(-914501757474496993521059)]], [[29499198158040349108176, 0], [14515478458718267004742]], [[(-951587038162133020547), 0, 0], [(-468241241397014284978), 0], [(-230404420174807163470)]], [[30696356069745535539, 0, 0, 0], [15104556161302610631, 0, 0], [7432400650799743670, 0], [3657213018647709938]], [[(-990205034507878670), 0, 0, 0, 0], [(-487243747138782922), 0, 0, 0], [(-239754859703182531), 0, 0], [(-117974613504757098), 0], [(-58051000295962343)]]], r := 64080642217238672, ok := true }, term0 := { p := [[[15713884634335483433597936527]], [[(-1013754755576896508810562737), 0], [(-498816721405440229297026441)]], [[49051935773123826514643919, 0, 0], [32181021599783149505525396, 0], [11876296883166610397496031]], [[(-2109745330235895371164030), 0, 0, 0], [(-1557134878023932941369811), 0, 0], [(-766201553538807243812586), 0], [(-251347111583152311303010)]], [[85070004892300005422553, 0, 0, 0, 0], [66973299518939604716814, 0, 0, 0], [37074088903473165418598, 0, 0], [16215765720863530837453, 0], [4987009114715563846246]]], r := 9154379547679607735316, ok := true }, r0 := { p := [[[37968018830572920500610]], [[(-1228542466156844915162), 25296091793824404557071], [(-548537391356579783817)]], [[30110086939827172755, (-817235801446454846549), 4205408856912033514900], [17707959117609446239, (-365507566776850727758)], [8354467927089325711]], [[(-683924634355228352), 19980949607242912073, (-135012389093116125751), (-3530552166410333255)], [(-428122252471684906), 11784569530145160222, (-60795306929660667898)], [(-269462867240986944), 5567071819453975297], [(-129178913201547328)]], [[15621655388471541, (-452747598510112893), 3268658579275653801, 396907931958254251, (-292161390771870993)], [9540752006021568, (-284346841673967287), 1950282955198956263, 40830903451414839], [6480974850042590, (-179351862540873110), 926130484688631780], [4164286986241450, (-86081533432156077)], [2011692834473824]]], r := 347091643895077996, ok := true }, r1 := { p := [[[268961404840360440237357]], [[(-8620305385723650342918), 0], [(-3888752673569732717131)]], [[208166238457302592342, 0, 0], [124578928541995475952, 0], [59242289539993478194]], [[(-4659039802406994399), 0, 0, 0], [(-2975468734154663972), 0, 0], [(-1897368506683099443), 0], [(-916152238254553057)]], [[105325625573056777, 0, 0, 0, 0], [65485452485403492, 0, 0, 0], [45122077342464393, 0, 0], [29336709950261385, 0], [14268590109910895]]], r := 32962493011931474, ok := true }, r2 := { p := [[[4339861719434663868322131464]], [[(-130057715751516533694436502), 94105579884486915143981], [(-136238433298586813153267105)]], [[3385031483999444220845278, (-2014946637243268575434), 450108451769256120], [4037804761003772617669786, (-1485019154710839507168)], [3221753349800423145416794]], [[(-90050629194194176258323), 43288315159571311415, (-657099421881238), (-8908476067391)], [(-103959531779389448503002), 31142911357124979706, 37938991258020], [(-94831129830448176435669), 23513614724666705464], [(-67857083132793933317133)]], [[2522575568648282862330, (-1002954451528841038), (-699968316242455), (-84121812139785), (-1831399735678)], [2742141840906116863017, (-653990939396669730), (-377809904317677), (-7132435896486)], [2424986452574304668231, (-489219309603708941), (-252982143891242)], [1987512918923859831199, (-373395209105796322)], [1341392421300545142398]]], r := 9239165419713645594051, ok := true }, r3 := { p := [[[31421493630945784284241982996]], [[(-2027170433537916655180555404), 694623248190294911532305], [(-997533744214633434497143860)]], [[98088526322800903359307986, (-37555076512261435638823), 1769674853644245293], [64356657447059706411484134, (-11043143600388458260982)], [23751010742363251670287674]], [[(-4218853479534171547477147), 1699976626886217819914, (-2159778530255356), (-14776152911038402)], [(-3114026046115912043556425), 596813450831234837736, (-5297067551522046)], [(-1532317597861557423060909), 175374880143029466091], [(-502669095490125043917753)]], [[170114855956632838281273, (-70611823503576793027), (-4480596836796390), 1713530974980827, (-1489693934701866)], [133936476754781386122751, (-27020714535468237353), (-13668935033116415), 783687921105001], [74144302593453577511228, (-9488342026025365424), (-7028459755000164)], [32430166946224880668604, (-2797269662725527801)], [9973609597957750741232]]], r := 780571775722884767310489, ok := true }, eta := { p := [[[(-4341013685253964651987358103)]], [[130096880707681709624476277, 0], [136256565902080474807830728]], [[(-3386264708450163369363283), 0, 0], [(-4038417829064724289524689), 0], [(-3222040196502068843956518)]], [[90089325338232632156756, 0, 0, 0], [103978775123049949035620, 0, 0], [94840805498445462230355, 0], [67861626597225210921636]], [[(-2523800023414709511295), 0, 0, 0, 0], [(-2742745223238337436616), 0, 0, 0], [(-2425289927673545383242), 0, 0], [(-1987666274176560280452), 0], [(-1341464779576206649204)]]], r := 855491415064606062289, 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 985162418487296 1125899906842624 4611686018427387904 9223372036854775808 8070450532247928832 9223372036854775808 :=
  (RegionPosI.split_b 1055531162664960 (RegionPosI.split_s 8646911284551352320 (RegionPosI.split_b 1020346790576128 (RegionPosI.of_check c0 q0 ok_0 985162418487296 1020346790576128 4611686018427387904 9223372036854775808 8070450532247928832 8646911284551352320 (by decide +kernel)) (RegionPosI.of_check c1 q1 ok_1 1020346790576128 1055531162664960 4611686018427387904 9223372036854775808 8070450532247928832 8646911284551352320 (by decide +kernel))) (RegionPosI.split_b 1020346790576128 (RegionPosI.of_check c2 q2 ok_2 985162418487296 1020346790576128 4611686018427387904 9223372036854775808 8646911284551352320 9223372036854775808 (by decide +kernel)) (RegionPosI.of_check c3 q3 ok_3 1020346790576128 1055531162664960 4611686018427387904 9223372036854775808 8646911284551352320 9223372036854775808 (by decide +kernel)))) (RegionPosI.split_s 8646911284551352320 (RegionPosI.split_s 8358680908399640576 (RegionPosI.of_check c4 q4 ok_4 1055531162664960 1125899906842624 4611686018427387904 9223372036854775808 8070450532247928832 8358680908399640576 (by decide +kernel)) (RegionPosI.of_check c5 q5 ok_5 1055531162664960 1125899906842624 4611686018427387904 9223372036854775808 8358680908399640576 8646911284551352320 (by decide +kernel))) (RegionPosI.split_b 1090715534753792 (RegionPosI.of_check c6 q6 ok_6 1055531162664960 1090715534753792 4611686018427387904 9223372036854775808 8646911284551352320 9223372036854775808 (by decide +kernel)) (RegionPosI.of_check c7 q7 ok_7 1090715534753792 1125899906842624 4611686018427387904 9223372036854775808 8646911284551352320 9223372036854775808 (by decide +kernel)))))

end CKLaneC.RSC2.S00_0091