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

import Definitions.Def_CK_CKLaneC_RSC2_S09_0016_part00

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

namespace CKLaneC.RSC2.S09_0016
open CKLaneC.TM3 CKLaneC.RSCell

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 := 378302368699121664, bh := 18014398509481984, tc := 11529215046068469760, th := 2305843009213693952, sc := 4323455642275676160, sh := 288230376151711744 }
noncomputable def q6 : Cert := { V0 := [[[1908710809361971343]], [[(-62971295306278518), 375870196082343009], [17519319285096510]], [[930908995036535, (-12014689275877381), (-1729700872548450)], [(-568613352863139), 3342621054744827], [(-253848666431969)]], [[(-19425961762283), 158625170501703, 168632430834851, (-104890664720862)], [9258294911892, (-97923517793260), (-46915430010588)], [8385331393058, (-49903144452825)], [7037125723214]], [[523194018323, (-2941936075295), (-7846403427222), 9543535343608, 1492466174691], [(-244964691371), 1097862369562, 4501510611720, (-2655118367506)], [(-131013342045), 1589348363907, 265419136559], [(-232244521901), 1380877849165], [(-229982213883)]]], r0 := 48408493500201, V1 := [[[3018053168145261793]], [[(-97260684232079951), 0], [27059011136124271]], [[1327248877918601, 0, 0], [(-816717577621411), 0], [(-400633088226235)]], [[(-25716926982196), 0, 0, 0], [10543831162196, 0, 0], [12851847014691, 0], [11095084164751]], [[675054346909, 0, 0, 0, 0], [(-249649818279), 0, 0, 0], [(-182230649345), 0, 0], [(-355340344706), 0], [(-362904779910)]]], r1 := 17962980021980, V2 := [[[17998226301768569324]], [[(-7115232125441702), 1083353965990533], [(-21299832376866778)]], [[32730130297243, (-4488686856981), (-2421760415576)], [(-349918323926586), 105327539116195], [(-673962814585)]], [[(-812067252131), (-436242992319), 58996365482, 5242520277], [1903025499385, (-407664614437), (-354371044934)], [(-354114260580), 2640773019093], [(-76397434778)]], [[28436572615, 3509570683, 787520782, (-234324184), (-11139918)], [(-45926449650), (-43864651642), 8582137490, 1022700584], [12279213239, (-8895031139), (-17587506672)], [3585861693, 3494165849], [1355666337]]], r2 := 4223479421094, V3 := [[[18266905831366430479]], [[(-11942068041798352), 847390940428227], [(-8688162362763856)]], [[3334148900016, 40354546069153, (-3732502348459)], [(-574663359573798), 82922150097223], [(-6112082764810)]], [[6432860618, (-1136899073430), (-105374395208), 16004574022], [323934592528, 3950760735311, (-548521978346)], [(-295083408865), 2117722950241], [(-7938127960)]], [[(-150006715), (-1895610768), 8643248623, 136715183, (-67606379)], [693311905, (-111718248334), (-15512911602), 3134388310], [8134067307, 100672946085, (-27473583082)], [(-392308433), 4062808866], [23930711]]], r3 := 30708184432676, Vm := [[[18002113294135289161]], [[(-7153881567955727), 0], [(-20915889392244128)]], [[31710745468250, 0, 0], [(-353777504349696), 0], [9293962911546]], [[(-806403557420), 0, 0, 0], [1799323667994, 0, 0], [(-456821573965), 0], [(-55699986407)]], [[28387110027, 0, 0, 0, 0], [(-45227510653), 0, 0, 0], [9388066782, 0, 0], [3305661786, 0], [1276169862]]], rm := 993212304471 }
noncomputable def w6 : Wit := { Z0 := { p := [[[1923593320504473753]], [[(-64453720618027138), 384718664100894750], [17931746601805104]], [[1002515717953132, (-12890744123605428), 0], [(-609648943761169), 3586349320361020], [(-255978362478484)]], [[(-21933937387894), 200503143590626, 0, 0], [11267713516503, (-121929788752234), 0], [8598679250721, (-51195672495697)], [7103849021387]], [[603706994627, (-4386787477579), 0, 0, 0], [(-318230334204), 2253542703300, 0, 0], [(-140995462069), 1719735850144, 0], [(-238901775229), 1420769804277], [(-232037836885)]]], r := 9463115117226, ok := true }, Z1 := { p := [[[3077749312807158006]], [[(-103125952988843421), 0], [28690794562888166]], [[1604025148725012, 0, 0], [(-975438310017870), 0], [(-409565379965575)]], [[(-35094299820630), 0, 0, 0], [18028341626405, 0, 0], [13757886801154, 0], [11366158434220]], [[965931191403, 0, 0, 0, 0], [(-509168534726), 0, 0, 0], [(-225592739311), 0, 0], [(-382242840366), 0], [(-371260539015)]]], r := 4712587472112, ok := true }, Z2 := { p := [[[189902591193492098993]], [[(-2526748121113742553), 384718664100894750], [(-7563957224367402251)]], [[48720290389148049, (-12890744123605428), 0], [97842761339517011, 3586349320361020], [332202498676748995]], [[(-1191548404862938), 200503143590626, 0, 0], [(-1743090642106356), (-121929788752234), 0], [(-4301330653756860), (-51195672495697)], [(-15079097007161959)]], [[35729984643173, (-4386787477579), 0, 0, 0], [39214524200310, 2253542703300, 0, 0], [75098823301089, 1719735850144, 0], [195145538297551, 1420769804277], [694069217087711]]], r := 196239120979434, ok := true }, Z3 := { p := [[[410915302431227748120]], [[(-23228084776249718047), 1648229480354620786], [(-16899030486658533248)]], [[1448352789713376885, (-126133292625935080), 0], [980234859524318133, 12418577903433862], [751283162604072555]], [[(-92669041422305005), 7659327134840532, 0, 0], [(-61715083206316716), (-817358263512096), 0], [(-44029591874074149), (-201399249334251)], [(-34320969001222927)]], [[5998738899877203, (-487132939335747), 0, 0, 0], [3969735022504153, 44579027848219, 0, 0], [2780795486707728, 14305357364519, 0], [2022436635865416, 5624234577347], [1586635937195631]]], r := 8036721000689055, ok := true }, iE := { p := [[[196018832812565507378]], [[(-2567606380964982265), 0], [(-7506941589253907654)]], [[49758657090940524, 0, 0], [97433864937013128, 0], [331388591965031694]], [[(-1219638711501472), 0, 0, 0], [(-1728050551910312), 0, 0], [(-4295824752673867), 0], [(-15056509666804158)]], [[36628623535755, 0, 0, 0, 0], [38739575580794, 0, 0, 0], [74938363859118, 0, 0], [194991870803645, 0], [693331431475741]]], r := 193455807687066, ok := true }, iHu := { p := [[[419896471232343743021]], [[(-23563906672744321461), 0], [(-16831361909103087509)]], [[1470364054721094098, 0, 0], [978429284232785187, 0], [750185742204638986]], [[(-94092645383952444), 0, 0, 0], [(-61592425373125265), 0, 0], [(-43994589552232888), 0], [(-34290322661791259)]], [[6091338412798523, 0, 0, 0, 0], [3962017553145320, 0, 0, 0], [2778532488534074, 0, 0], [2021437527114579, 0], [1585625367761817]]], r := 7989943030512568, ok := true }, T := { p := [[[11529215046068469760]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[1735967723296866546]], [[22739048792053411, 0], [66482429839181665]], [[(-142815338134819), 0, 0], [878789935619470, 0], [(-388739086506783)]], [[3158346182631, 0, 0, 0], [(-6833576097680), 0, 0], [(-4881125784057), 0], [6059899242071]], [[(-105280673759), 0, 0, 0, 0], [150390386780, 0, 0, 0], [(-1571635538), 0, 0], [76729789174, 0], [(-144336288869)]]], r := 283539972864, ok := true }, de := { p := [[[(-70963157220762488449)]], [[891385333333666068, 0], [636703809524047191]], [[(-29569339346404241), 0, 0], [205007282930422, 0], [(-15086397625716449)]], [[1314223663896746, 0, 0, 0], [66008692623, 0, 0], [47149066160, 0], [478944483927386]], [[(-65711175756069), 0, 0, 0, 0], [21253623, 0, 0, 0], [1594407278, 0, 0], [10843685, 0], [(-17105158203891)]]], r := 22195655078951, ok := true }, dde := { p := [[[(-2781801390731197113142)]], [[184557735562471269557, 0], [131826953973193763895]], [[(-12304137433876731992), 0, 0], [(-8788875593039557117), 0], [(-6277621139733026328)]], [[820275736066619985, 0, 0, 0], [585911107392591719, 0, 0], [418507933851851301, 0], [298934306146727604]], [[(-54685049101006475), 0, 0, 0, 0], [(-39060749421930691), 0, 0, 0], [(-27900538490340295), 0, 0], [(-19928953786699331), 0], [(-14234966967150767)]]], r := 12078939959540411, ok := true }, nJu := { p := [[[(-141926314441524976897)]], [[1782770666667332136, 0], [1273407619048094383]], [[(-59138678692808482), 0, 0], [410014565860844, 0], [(-30172795251432898)]], [[2628447327793492, 0, 0, 0], [132017385246, 0, 0], [94298132320, 0], [957888967854772]], [[(-131422351512138), 0, 0, 0, 0], [42507247, 0, 0, 0], [3188814557, 0, 0], [21687371, 0], [(-34210316407782)]]], r := 44391310157896, ok := true }, Jd1 := { p := [[[(-5563602781462394226283)]], [[369115471124942539114, 0], [263653907946387527790]], [[(-24608274867753463984), 0, 0], [(-17577751186079114233), 0], [(-12555242279466052656)]], [[1640551472133239971, 0, 0, 0], [1171822214785183439, 0, 0], [837015867703702602, 0], [597868612293455208]], [[(-109370098202012949), 0, 0, 0, 0], [(-78121498843861381), 0, 0, 0], [(-55801076980680590), 0, 0], [(-39857907573398662), 0], [(-28469933934301533)]]], r := 24157879919080814, ok := true }, term0 := { p := [[[596158155692555903757533]], [[(-78925143591744369460262), 0], [(-55812640895246065714582)]], [[7874061171714030954238, 0, 0], [7415321998482873394893, 0], [3963809115107967349300]], [[(-699096271750500526854), 0, 0, 0], [(-740653187810460341140), 0, 0], [(-527252357442084751489), 0], [(-250946334667947529171)]], [[58217008859458636990, 0, 0, 0, 0], [65796778273626924307, 0, 0, 0], [52683385014612897746, 0, 0], [33399724427836629754, 0], [14911421635464762487]]], r := 23610044160915579924, ok := true }, r0 := { p := [[[1247978692594959234089]], [[(-66575127905333340340), 487351698097603554911], [(-47204762914108364572)]], [[3241209398207444685, (-25261898471804636960), 44126684508330825701], [2366620001681524398, (-18644528029296108116)], [2077512749699098104]], [[(-165842873578347724), 1206975505850854938, (-2001842947034655670), (-872088285332964824)], [(-105855043366197401), 920092124355957485, (-1769757339695331018)], [(-102763449674003576), 821447749643443351], [(-94208829497547217)]], [[9146447588124103, (-61514994475284091), 87042840498876982, 96036843035082675, (-31732552766844281)], [5063932194894706, (-40728033696376212), 81427300933899285, 18814995116362475], [4506399518387990, (-40033565074695681), 78355163372164874], [4619601944040347, (-37281862007969187)], [4332310789005965]]], r := 180106745670735528, ok := true }, r1 := { p := [[[3081380157985737488319]], [[(-157616835691677199509), 0], [(-118487221746987047013)]], [[7481596805226825622, 0, 0], [5795722777151372802, 0], [5224302255899011039]], [[(-381616008080091021), 0, 0, 0], [(-255060196095634177), 0, 0], [(-252600011219772752), 0], [(-237217348718529585)]], [[21218573045211157, 0, 0, 0, 0], [12197120241363072, 0, 0, 0], [10901197755982100, 0, 0], [11386456603519659, 0], [10918459801484685]]], r := 54489001156495890, ok := true }, r2 := { p := [[[101949114499674516991074]], [[(-6572388645696845392801), 520655364031958894079], [(-9150583227785366366757)]], [[393686710654860583450, (-24873504873001339903), 467856711994937079], [574266207559642866244, (-22859301764020994566)], [630924079488102690795]], [[(-24214968308054662582), 1292714385904095104, 1746738353073934, (-992320676305858)], [(-33869145395216738150), 1001218934490994936, 237148667475081], [(-38921954249206345511), 1067669842353573192], [(-39092598235440589369)]], [[1530934156742784264, (-73575600850626389), (-52366388653498), 17146405589765, 2068802744992], [2069188215626870371, (-49131803409874758), 50481053009418, (-50062831769502)], [2273162049818807935, (-45246777576965477), (-7710196074157)], [2381947273892020668, (-50218769860011027)], [2284517486245101389]]], r := 17530994411371263292, ok := true }, r3 := { p := [[[1141739869906778977873025]], [[(-151745390711251213190405), 7116388526222270897677], [(-109214458738911054093712)]], [[15158403018636598169364, (-862102878952152875607), 1510408376909981279], [14539245604228621929010, (-340717139202336603312)], [7812699776264898410465]], [[(-1346694242172165463887), 83384247908438677243, 40949383456969236, (-6814534131811810)], [(-1453170231369168293078), 41273998373128786389, (-5064090519394961)], [(-1040619098346556816574), 16264666786360268926], [(-496417334954012842872)]], [[112188378856117926231, (-7287074548422797358), (-3089698201060744), 41126447545331, 28603241260154], [129137024833707985198, (-3988246801877298374), 506060040496600, (-318499987982203)], [104026118283814025567, (-1968665966764106482), 18973811746172], [66137964152443705897, (-775517213587112268)], [29562017361396876897]]], r := 3622037184165135952195, ok := true }, eta := { p := [[[(-109189369486537825822021)]], [[7099024067716664562058, 0], [9475379782825739472104]], [[(-428973707400173093533), 0, 0], [(-597699300345877024670), 0], [(-646150720924150655501)]], [[26552002539076125698, 0, 0, 0], [35429441266574723203, 0, 0], [40015795092980027815, 0], [39811019057886282623]], [[(-1685763425448511403), 0, 0, 0, 0], [(-2172348554349990598), 0, 0, 0], [(-2345901148870691628), 0, 0], [(-2433433909127104375), 0], [(-2318512174404591831)]]], r := 2296155056032267724, 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 := 414331165718085632, bh := 18014398509481984, tc := 11529215046068469760, th := 2305843009213693952, sc := 4323455642275676160, sh := 288230376151711744 }
noncomputable def q7 : Cert := { V0 := [[[1942786915214363280]], [[(-64076725215694753), 382366197881187237], [16581613792148045]], [[948928654594355, (-12204507927104173), (-1822529668898557)], [(-537635866120841), 3158251865856631], [(-216554904647322)]], [[(-19904178401281), 160737317722874, 177532688023881, (-110127381049681)], [8774106651456, (-92049617566611), (-45941462494918)], [7154618867308, (-42586058756867)], [5482478798207]], [[538553417074, (-2985055660867), (-8255464062005), 9983114922805, 1626001731124], [(-233548668871), 1016387824841, 4401526960881, (-2583405371224)], [(-111873369244), 1357290605309, 223220727771], [(-180911339004), 1075517305166], [(-163468439839)]]], r0 := 39386892041111, V1 := [[[3070651998536129841]], [[(-98845380745557948), 0], [25578959023630208]], [[1347645248297275, 0, 0], [(-769232095601102), 0], [(-341839881175697)]], [[(-26200970867246), 0, 0, 0], [9870208637302, 0, 0], [10969421578940, 0], [8642133800097]], [[690791267457, 0, 0, 0, 0], [(-234778931114), 0, 0, 0], [(-155688604711), 0, 0], [(-276618449506), 0], [(-257896745098)]]], r1 := 13180245248987, V2 := [[[17955623350633844597]], [[(-7816457624712120), 1304599931185673], [(-21303404189837856)]], [[36584695578601, (-5339594367440), (-3203329594592)], [(-351293886831061), 115932247071404], [(-1102343387620)]], [[(-904866749557), (-528718950150), 77912820122, 7611506126], [1951251140193, (-443245755950), (-428441183497)], [(-334169047681), 2661505835769], [(-66784157905)]], [[31687933492, 4308494618, 1052250686, (-340071139), (-17743930)], [(-46865673643), (-48623957287), 10364236886, 1357042174], [11845943016, (-8899286297), (-19452068590)], [3083303723, 3418987696], [1063920544]]], r2 := 3405140296196, V3 := [[[18249504995173836966]], [[(-13092578203615982), 1021738558624004], [(-8712705219976536)]], [[4014653586819, 48660123804580, (-4943425558359)], [(-575848342484703), 91441645219798], [(-6159171175513)]], [[7903033968, (-1371986726929), (-139618315218), 23273394630], [356619708821, 4355495046462, (-664404089141)], [(-297393981249), 2141989666228], [(-7763329469)]], [[(-185731820), (-2306455764), 11456736297, 198995182, (-107912335)], [777146009, (-123399385438), (-18786761300), 4168260782], [8208491697, 101690082914, (-30477866374)], [(-378234371), 4027821053], [19934678]]], r3 := 28187270629680, Vm := [[[17960318265024861513]], [[(-7863238487690901), 0], [(-20879343566458155)]], [[35346249801637, 0, 0], [(-355567236696072), 0], [8987968143230]], [[(-897694314604), 0, 0, 0], [1835845836273, 0, 0], [(-438541219740), 0], [(-46669249936)]], [[31620846410, 0, 0, 0, 0], [(-46054668506), 0, 0, 0], [8885511734, 0, 0], [2808344565, 0], [997257810]]], rm := 840627098898 }
noncomputable def w7 : Wit := { Z0 := { p := [[[1958486265204642197]], [[(-65640418504370375), 391697253040928439], [16986262408551467]], [[1024516684462317, (-13128083700874075), 0], [(-577891907449214), 3397252481710293], [(-218328515740392)]], [[(-22557513170604), 204903336892463, 0, 0], [10747125454535, (-115578381489843), 0], [7332438195799, (-43665703148079)], [5535213227428]], [[624050894512, (-4511502634121), 0, 0, 0], [(-305680378701), 2149425090907, 0, 0], [(-120157628795), 1466487639159, 0], [(-186173011127), 1107042645485], [(-164949973599)]]], r := 7115327575851, ok := true }, Z1 := { p := [[[3133578024327427515]], [[(-105024669606992600), 0], [27178019853682347]], [[1639226695139708, 0, 0], [(-924627051918742), 0], [(-349325625184627)]], [[(-36092021072966), 0, 0, 0], [17195400727256, 0, 0], [11731901113279, 0], [8856341163886]], [[998481431220, 0, 0, 0, 0], [(-489088605921), 0, 0, 0], [(-192252206072), 0, 0], [(-297876817804), 0], [(-263919957758)]]], r := 3456933268267, ok := true }, Z2 := { p := [[[175993016610104680389]], [[(-2346838219842595652), 391697253040928439], [(-6396202162908508956)]], [[45509812045070510, (-13128083700874075), 0], [82721833118440672, 3397252481710293], [256128128243539562]], [[(-1119194593654252), 204903336892463, 0, 0], [(-1478702824030820), (-115578381489843), 0], [(-3316741234381147), (-43665703148079)], [(-10608419174573034)]], [[33697961180072, (-4511502634121), 0, 0, 0], [33385453731073, 2149425090907, 0, 0], [58082696591162, 1466487639159, 0], [137310478873258, 1107042645485], [445647716696603]]], r := 134015186777519, ok := true }, Z3 := { p := [[[379871031531232027640]], [[(-21428927274420937861), 1672303264163695328], [(-14260287287860531651)]], [[1335109056893740250, (-127713815416662730), 0], [825697631981094547, 11675026242439568], [578260972303780571]], [[(-85385976515154626), 7745401990047033, 0, 0], [(-51957237550349630), (-764585077096449), 0], [(-33840322052269396), (-171625837635005)], [(-24108033077008118)]], [[5525629705743145, (-492364474683031), 0, 0, 0], [3340977047058974, 41577422052859, 0, 0], [2136215259924857, 12171419410471, 0], [1418736407335520, 4371863870534], [1017261030134560]]], r := 6098536552728884, ok := true }, iE := { p := [[[182220203551306379457]], [[(-2388493403446158163), 0], [(-6342192781617645311)]], [[46577650766117372, 0, 0], [82333263414743279, 0], [255433932677165012]], [[(-1148217147663861), 0, 0, 0], [(-1464255058017146), 0, 0], [(-3312050014201745), 0], [(-10590819455780515)]], [[34629533877723, 0, 0, 0, 0], [32927696352843, 0, 0, 0], [57946025158693, 0, 0], [137190666156654, 0], [445123243107081]]], r := 131972986644324, ok := true }, iHu := { p := [[[388983377889021959328]], [[(-21768227805801357051), 0], [(-14196670308131320125)]], [[1357357071646369332, 0, 0], [824021058416944703, 0], [577325786617075549]], [[(-86824472230205746), 0, 0, 0], [(-51842917698543887), 0, 0], [(-33810598499050703), 0], [(-24084210879999284)]], [[5619175788080052, 0, 0, 0, 0], [3333788286706258, 0, 0, 0], [2134294678331600, 0, 0], [1417962881869359, 0], [1016544302912991]]], r := 6052817143803797, ok := true }, T := { p := [[[11529215046068469760]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[1867423920559542692]], [[24477690337110004, 0], [64995880140470546]], [[(-156488779765314), 0, 0], [860131606267416, 0], [(-355542540725536)]], [[3459124866474, 0, 0, 0], [(-6839866979970), 0, 0], [(-4460782813024), 0], [5051454035673]], [[(-115307408692), 0, 0, 0, 0], [150388264255, 0, 0, 0], [(-1573806272), 0, 0], [63964762679, 0], [(-109862873131)]]], r := 256737275776, ok := true }, de := { p := [[[(-69746517997080051920)]], [[891795536582580948, 0], [581605784727770184]], [[(-29569200945546698), 0, 0], [205196009399131, 0], [(-12576692273625722)]], [[1314223710625101, 0, 0, 0], [72395088528, 0, 0], [47214188170, 0], [364552068986580]], [[(-65711175740281), 0, 0, 0, 0], [25541671, 0, 0, 0], [1598792689, 0, 0], [10863660, 0], [(-11887565695705)]]], r := 20935999123905, ok := true }, dde := { p := [[[(-2541074447194609782355)]], [[168508448101508558111, 0], [109896813979244711840]], [[(-11234212839068685118), 0, 0], [(-7326866829154434777), 0], [(-4778256878620896293)]], [[748947411011318381, 0, 0, 0], [488443818146606485, 0, 0], [318550316182569607, 0], [207750268115657303]], [[(-49929827440125498), 0, 0, 0, 0], [(-32562931016242892), 0, 0, 0], [(-21236697338789564), 0, 0], [(-13850017918061638), 0], [(-9032620359976927)]]], r := 9644041763433096, ok := true }, nJu := { p := [[[(-139493035994160103839)]], [[1783591073165161897, 0], [1163211569455540368]], [[(-59138401891093396), 0, 0], [410392018798263, 0], [(-25153384547251444)]], [[2628447421250202, 0, 0, 0], [144790177056, 0, 0], [94428376341, 0], [729104137973160]], [[(-131422351480562), 0, 0, 0, 0], [51083342, 0, 0, 0], [3197585379, 0, 0], [21727320, 0], [(-23775131391409)]]], r := 41871998247803, ok := true }, Jd1 := { p := [[[(-5082148894389219564709)]], [[337016896203017116222, 0], [219793627958489423681]], [[(-22468425678137370235), 0, 0], [(-14653733658308869554), 0], [(-9556513757241792585)]], [[1497894822022636763, 0, 0, 0], [976887636293212971, 0, 0], [637100632365139214, 0], [415500536231314607]], [[(-99859654880250996), 0, 0, 0, 0], [(-65125862032485784), 0, 0, 0], [(-42473394677579128), 0, 0], [(-27700035836123275), 0], [(-18065240719953854)]]], r := 19288083526866183, ok := true }, term0 := { p := [[[498594613926681749579470]], [[(-65964812870468218557816), 0], [(-42551637059935944822502)]], [[6579633277544871348183, 0, 0], [5651574183151179647795, 0], [2757746311524733786134]], [[(-584107342592546000810), 0, 0, 0], [(-564424606898289190013), 0, 0], [(-366743856483172019243), 0], [(-159366134058860435090)]], [[48638164512670984638, 0, 0, 0, 0], [50138513354693619817, 0, 0, 0], [36642530680604427811, 0, 0], [21207267820897666421, 0], [8644793677644382892]]], r := 16904848206722971810, ok := true }, r0 := { p := [[[1161188985658104132513]], [[(-62219077936703094439), 453075296646849477941], [(-39901029647836926732)]], [[3046057937554894259, (-23568634055422019386), 40874449362937872657], [2004945844498472889, (-15756947444802885645)], [1602154382182059374]], [[(-156495306991323329), 1131900557225800845, (-1852119535937462164), (-837206400453773247)], [(-89969100224383007), 779226304181826270, (-1494445751242011305)], [(-79429910282854614), 633349539160792670], [(-66298729088463284)]], [[8651633861896631, (-57919319794624213), 80726684550060198, 92150749926192656, (-30054885598548001)], [4315004686608446, (-34606683783724177), 68841391490089698, 16172930178632135], [3494828146671388, (-30929193694983094), 60356430229022801], [3258018601595701, (-26231437290510940)], [2782654879913825]]], r := 148798107424741651, ok := true }, r1 := { p := [[[2863565055840969040190]], [[(-146952335715358740227), 0], [(-100123659072633407272)]], [[7011521487861505722, 0, 0], [4907008545833584898, 0], [4027532902205184860]], [[(-359105917120731242), 0, 0, 0], [(-216647112862922364), 0, 0], [(-195105344568364757), 0], [(-166887014091375075)]], [[20016677846359930, 0, 0, 0, 0], [10388941215702650, 0, 0, 0], [8447006046278147, 0, 0], [8025094220481641, 0], [7010873204913906]]], r := 38919244377469105, ok := true }, r2 := { p := [[[85891747061507297476279]], [[(-5562472067901202709985), 478840345692535396414], [(-7031981447320256813502)]], [[334050460289061216923, (-23036782666428876841), 468301245928379634], [443294705083243853788, (-19123433195136881022)], [442376107229980163553]], [[(-20569638642297217905), 1202434333302317303, 1847686436131916, (-1092913512782550)], [(-26210937048306472757), 842489125198982101, 207890311394308], [(-27410327988076252943), 815410940267698807], [(-25014314000602976427)]], [[1300969098945973026, (-68574053596425938), (-54990070821305), 18641309546317, 2506687059274], [1603072562586193434, (-41480749429294531), 50488519822274, (-50528862283541)], [1604820237134868596, (-34740207045754491), (-6951495013009)], [1530708731137804813, (-35010290738611849)], [1334200734006817727]]], r := 11139501788934835428, ok := true }, r3 := { p := [[[951014751131558578104640]], [[(-126356815193783433449239), 6494348704119776782393], [(-83093875642519714877265)]], [[12620923381510543661194, (-786744183492640950483), 1500349765620671167], [11060255167646347746599, (-283908315105009446139)], [5428035026419216092864]], [[(-1121201992310987225216), 76102335935756195138, 41935332351716504, (-7450088486737471)], [(-1105396259936173427105), 34397562058332664944, (-4997499960918099)], [(-722919747048235636997), 12375496459799808101], [(-314927592968876610149)]], [[93400444942383502509, (-6650995634652399553), (-3146491715754218), 41213840366582, 34356467932513], [98229359310969496180, (-3323888761835097687), 480527412717960, (-317041664578813)], [72264714309574059228, (-1498071764589118327), 14503341872591], [41954869698401268181, (-538788739923766711)], [17124104107921765167]]], r := 2484163486978104800107, ok := true }, eta := { p := [[[(-92538064964005253139504)]], [[6046240326301391918787, 0], [7303520337515478064164]], [[(-366482813784917591610), 0, 0], [(-462900707799567100900), 0], [(-453995386860804800337)]], [[22717932228301289420, 0, 0, 0], [27516709846525269986, 0, 0], [28245569026830667977, 0], [25514754963545621778]], [[(-1443295686517991712), 0, 0, 0, 0], [(-1689408047730412377), 0, 0, 0], [(-1660374600035940628), 0, 0], [(-1566594876114526813), 0], [(-1355818697363285964)]]], r := 1486766645617891058, 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 288230376151711744 432345564227567616 9223372036854775808 13835058055282163712 3458764513820540928 4611686018427387904 :=
  (RegionPosI.split_b 360287970189639680 (RegionPosI.split_s 4035225266123964416 (RegionPosI.split_b 324259173170675712 (RegionPosI.of_check c0 q0 ok_0 288230376151711744 324259173170675712 9223372036854775808 13835058055282163712 3458764513820540928 4035225266123964416 (by decide +kernel)) (RegionPosI.of_check c1 q1 ok_1 324259173170675712 360287970189639680 9223372036854775808 13835058055282163712 3458764513820540928 4035225266123964416 (by decide +kernel))) (RegionPosI.split_b 324259173170675712 (RegionPosI.of_check c2 q2 ok_2 288230376151711744 324259173170675712 9223372036854775808 13835058055282163712 4035225266123964416 4611686018427387904 (by decide +kernel)) (RegionPosI.of_check c3 q3 ok_3 324259173170675712 360287970189639680 9223372036854775808 13835058055282163712 4035225266123964416 4611686018427387904 (by decide +kernel)))) (RegionPosI.split_s 4035225266123964416 (RegionPosI.split_b 396316767208603648 (RegionPosI.of_check c4 q4 ok_4 360287970189639680 396316767208603648 9223372036854775808 13835058055282163712 3458764513820540928 4035225266123964416 (by decide +kernel)) (RegionPosI.of_check c5 q5 ok_5 396316767208603648 432345564227567616 9223372036854775808 13835058055282163712 3458764513820540928 4035225266123964416 (by decide +kernel))) (RegionPosI.split_b 396316767208603648 (RegionPosI.of_check c6 q6 ok_6 360287970189639680 396316767208603648 9223372036854775808 13835058055282163712 4035225266123964416 4611686018427387904 (by decide +kernel)) (RegionPosI.of_check c7 q7 ok_7 396316767208603648 432345564227567616 9223372036854775808 13835058055282163712 4035225266123964416 4611686018427387904 (by decide +kernel)))))

end CKLaneC.RSC2.S09_0016