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

import Definitions.Def_CK_CKLaneC_RSC2_S10_0052_part00

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

namespace CKLaneC.RSC2.S10_0052
open CKLaneC.TM3 CKLaneC.RSCell

theorem sF_5 : stageF w5 = true := by decide +kernel
theorem ok_5 : (domOK c5 && cellCheck c5 q5) = true :=
  staged_check c5 q5 w5 (by decide +kernel) sB_5 s0_5 s1_5 s2_5 s3_5 sE_5 sF_5

noncomputable def c6 : Cell := { bc := 756604737398243328, bh := 36028797018963968, tc := 2305843009213693952, th := 2305843009213693952, sc := 17293822569102704640, sh := 1152921504606846976 }
noncomputable def q6 : Cert := { V0 := [[[24522797110771879]], [[(-25128344182078762), 24522734587051635], [283387478330213]], [[626988878967634, (-25128151979268065), (-93785298377)], [(-288065500400649), 283385310743306], [(-3333666386917)]], [[(-22269810856406), 626787134533022, 288302771274, (-31261296143)], [4898274032017, (-288058854814094), (-3251364069)], [3419819726233, (-3333665937005)], [95022902272]], [[862154030979, (-22192541846206), (-302613654981), 96098515818, 352483], [(-230217235628), 4891334232853, 9968296487, (-1083760868)], [(-88747140326), 3419817903697, 675052], [(-97252210532), 95022668298], [(-3074584626)]]], r0 := 41657559281174, V1 := [[[196166623146737858]], [[(-200978329814194784), 0], [2266553724048495]], [[4965095215465681, 0, 0], [(-2302849976773271), 0], [(-26669216250390)]], [[(-158711948465089), 0, 0, 0], [37438731351055, 0, 0], [27358091066310, 0], [760124264277]], [[5522002306406, 0, 0, 0, 0], [(-1182383314086), 0, 0, 0], [(-709258060632), 0, 0], [(-777836248401), 0], [(-24594999283)]]], r1 := 19447287643254, V2 := [[[16976802053465526441]], [[(-43630910512605546), 607906485034929], [(-70207510804374903)]], [[370032861350608, (-590294521216109), (-227279040442)], [(-1876351716084451), 59522240711843], [(-10382698447117)]], [[(-6800764006474), (-17785372452256), 448339824774, 81015125], [26706551149915, (-57942839026095), (-33322390665)], [10015525256768, 1506788014750], [(-11933204477)]], [[233195433750, 176394767137, (-214766385827), (-241015331), (-27978)], [(-451846726719), (-1601375723097), 65817775637, 15733542], [373483387896, (-1477902680848), (-1648509057)], [14096516797, 1751356538], [174040183]]], r2 := 39428342780377, V3 := [[[17019886487858182409]], [[(-86884793661066132), 1180975087554422], [(-68359100701051772)]], [[534625352175328, (-1110627663693264), (-884450968583)], [(-3748806884202661), 115919212496884], [(-20379865753312)]], [[(-1703687000712), (-70974766256064), 1718979995413, 631954271], [50611768454678, (-109583160552682), (-130003223736)], [19255124664041, 2956226220954], [(-23979925071)]], [[(-17676329322), 627922927673, (-783922161184), (-1863028085), (-437744)], [(-296983830054), (-6431734142361), 253327848578, 123071100], [1141997673719, (-2838093074477), (-6465097538)], [28157034005, 4189727380], [298164510]]], r3 := 203258071974256, Vm := [[[16981071806110165739]], [[(-47791772045953803), 0], [(-69789543151090392)]], [[259914736053012, 0, 0], [(-2284574458149951), 0], [188743910706]], [[(-5554362828228), 0, 0, 0], [16807080589397, 0, 0], [(-377434655579), 0], [30238957]], [[213187953145, 0, 0, 0, 0], [(-294988950945), 0, 0, 0], [188688990641, 0, 0], [(-14106825), 0], [16492270]]], rm := 13149362246939 }
noncomputable def w6 : Wit := { Z0 := { p := [[[24522828372702501]], [[(-25128440283845304), 24522828372702501], [283388562127742]], [[627089751934180, (-25128440283845304), 0], [(-288068823214763), 283388562127742], [(-3333666611825)]], [[(-22308446157272), 627089751934180, 0, 0], [4901743974721, (-288068823214763), 0], [3419820637266, (-3333666611825)], [95023019261]], [[864911249719, (-22308446157272), 0, 0, 0], [(-231528396598), 4901743974721, 0, 0], [(-88748536145), 3419820637266, 0], [(-97252570601), 95023019261], [(-3074587953)]]], r := 10084201206862, ok := true }, Z1 := { p := [[[196182626981620010]], [[(-201027522270762427), 0], [2267108497021939]], [[5016718015473445, 0, 0], [(-2304550585718099), 0], [(-26669332894596)]], [[(-178467569258169), 0, 0, 0], [39213951797770, 0, 0], [27358565098128, 0], [760184154091]], [[6919289997757, 0, 0, 0, 0], [(-1852227172777), 0, 0, 0], [(-709988289157), 0, 0], [(-778020564804), 0], [(-24596703621)]]], r := 4707035372635, ok := true }, Z2 := { p := [[[70276587347505201672]], [[(-1760062372395796017), 24522828372702501], [(-2832157215482603394)]], [[62155989847617201, (-25128440283845304), 0], [76302696622946874, 283388562127742], [121869987703515223]], [[(-2401795056256390), 627089751934180, 0, 0], [(-2552375247175397), (-288068823214763), 0], [(-3339894104949431), (-3333666611825)], [(-5490539161682253)]], [[99143100347617, (-22308446157272), 0, 0, 0], [94424841537474, 4901743974721, 0, 0], [111553708988058, 3419820637266, 0], [151670780120755, 95023019261], [251489357818911]]], r := 186803590008998, ok := true }, Z3 := { p := [[[72061972447848929041]], [[(-3698686770970697063), 50274124494363227], [(-2910047786091863712)]], [[226549358989632286, (-52819444104210177), 0], [161089037858149035, 575920492698047], [125282863304331349]], [[(-14324682066281278), 2701596305869522, 0, 0], [(-9953093569424776), (-595079461222652), 0], [(-7058261966856860), (-6842488758788)], [(-5645607894770337)]], [[919766270370449, (-166161301609612), 0, 0, 0], [634238373768223, 20302913127033, 0, 0], [439512177492246, 7203426128983, 0], [320685750891455, 194548401773], [258634768174803]]], r := 966284732542909, ok := true }, iE := { p := [[[76529908582544339523]], [[(-1889970581364508011), 0], [(-2759893132140029069)]], [[67027227338275972, 0, 0], [75392618607884557, 0], [121019902717499980]], [[(-2592121583767550), 0, 0, 0], [(-2500577371898528), 0, 0], [(-3321258495073658), 0], [(-5466308291770585)]], [[107060495357710, 0, 0, 0, 0], [92084719656829, 0, 0, 0], [110978262784244, 0, 0], [151197267548568, 0], [250705337891007]]], r := 188708366262689, ok := true }, iHu := { p := [[[78446786258633058929]], [[(-3971668236926896353), 0], [(-2836905883519211708)]], [[243851179774652202, 0, 0], [159231769348222364, 0], [124413867231965376]], [[(-15423750279812538), 0, 0, 0], [(-9826971573440897), 0, 0], [(-7019265409600654), 0], [(-5620900247745084)]], [[990498733983018, 0, 0, 0, 0], [626603485692613, 0, 0, 0], [437385363874474, 0, 0], [319695655965624, 0], [257834947413320]]], r := 980998233619829, ok := true }, T := { p := [[[2305843009213693952]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[4446397143594043994]], [[109807524275191490, 0], [160350131950520350]], [[(-1182500846577507), 0, 0], [3539642803707919, 0], [(-1248574885596128)]], [[25226951608253, 0, 0, 0], [(-58561374799222), 0, 0], [(-41829553428015), 0], [18997630865526]], [[(-842299157833), 0, 0, 0, 0], [1197281207370, 0, 0, 0], [(-111517153991), 0, 0], [610857758862, 0], [(-453135263245)]]], r := 1729858893729, ok := true }, de := { p := [[[(-42835392326779460602)]], [[922575898586946722, 0], [658982784704961944]], [[(-29522741082114558), 0, 0], [1756841243976667, 0], [(-15062623001078856)]], [[1314307562089985, 0, 0, 0], [4683720467629, 0, 0], [3345514619735, 0], [478975059070694]], [[(-65711007741996), 0, 0, 0, 0], [12486750010, 0, 0, 0], [124895814715, 0, 0], [6370790821, 0], [(-17105114468450)]]], r := 22196841181913, ok := true }, dde := { p := [[[(-359892464820203216082)]], [[23033361423303091052, 0], [16452401016645065029]], [[(-1538115364091593588), 0, 0], [(-1100480928544986518), 0], [(-784752736781425271)]], [[102534204842368067, 0, 0, 0], [73228975701113105, 0, 0], [52306411215080790, 0], [37366692726810550]], [[(-6835631836688297), 0, 0, 0, 0], [(-4882633127342660), 0, 0, 0], [(-3487845595935875), 0, 0], [(-2491139350685021), 0], [(-1779371052865543)]]], r := 1695661238241840, ok := true }, nJu := { p := [[[(-85670784653558921204)]], [[1845151797173893445, 0], [1317965569409923888]], [[(-59045482164229115), 0, 0], [3513682487953335, 0], [(-30125246002157711)]], [[2628615124179971, 0, 0, 0], [9367440935259, 0, 0], [6691029239471, 0], [957950118141389]], [[(-131422015483992), 0, 0, 0, 0], [24973500020, 0, 0, 0], [249791629431, 0, 0], [12741581642, 0], [(-34210228936899)]]], r := 44393682363815, ok := true }, Jd1 := { p := [[[(-719784929640406432163)]], [[46066722846606182105, 0], [32904802033290130059]], [[(-3076230728183187176), 0, 0], [(-2200961857089973035), 0], [(-1569505473562850541)]], [[205068409684736135, 0, 0, 0], [146457951402226210, 0, 0], [104612822430161581, 0], [74733385453621101]], [[(-13671263673376593), 0, 0, 0, 0], [(-9765266254685320), 0, 0, 0], [(-6975691191871750), 0, 0], [(-4982278701370041), 0], [(-3558742105731085)]]], r := 3391322476483669, ok := true }, term0 := { p := [[[10476591916202521165966]], [[(-1318112520038923465812), 0], [(-923959715133857262931)]], [[129531223700481529006, 0, 0], [119933547586885305858, 0], [64413219859057547407]], [[(-11411269495036982458), 0, 0, 0], [(-11882049430631783505), 0, 0], [(-8431384659440902023), 0], [(-4039052492544245197)]], [[945812654084028070, 0, 0, 0, 0], [1051308110589657094, 0, 0, 0], [837915456090246256, 0, 0], [531067258461560490, 0], [238610811011251389]]], r := 424712946247181588, ok := true }, r0 := { p := [[[7247427798566715057]], [[(-548147373989743955), 14494795968168386047], [(-262676409656828348)]], [[39087502897974073, (-1096168050928850643), 7247278726696051251], [21771007230221132, (-525352036164404617)], [11521109678437977]], [[(-2530118153997357), 78099823881676497, (-547830633625264025), (-119256304253852)], [(-1453904785907786), 43540323296659397, (-262674451778290634)], [(-959513325594986), 23042182762529528], [(-520608376849248)]], [[157277960702618, (-5051395367208701), 38899551751999268, 253387314965055, (-29812721213278)], [89592110052397, (-2906765351562038), 21766779298543088, 1566314726416], [64477623156187, (-1918948269527815), 11521018192665030], [43672668028817, (-1041215234804241)], [23883623263842]]], r := 9392074655065741, ok := true }, r1 := { p := [[[463715201519456826342]], [[(-34826154273952757689), 0], [(-16809711046022686341)]], [[2350264423093787509, 0, 0], [1389933667417332525, 0], [737277251125987384]], [[(-144280385717725546), 0, 0, 0], [(-90942549447719425), 0, 0], [(-61250860071863532), 0], [(-33315874194872356)]], [[8549291154663440, 0, 0, 0, 0], [5433138238352538, 0, 0, 0], [4030924472330737, 0, 0], [2788487948729722, 0], [1528418982118876]]], r := 8686683530892015, ok := true }, r2 := { p := [[[5301075781340223650097]], [[(-473938584236023336881), 81432043255183464702], [(-503599985150173429455)]], [[33787912648604809059, (-5407242377098172717), 552861969799847336], [44150900218202833604, (-3901370762520920881)], [35631744049058008949]], [[(-2245394733331504435), 325870644838425469, 3404438662105809, (-205768492335877)], [(-3090805273389798098), 236706713167497533, 3738867071125331], [(-3087601316006962259), 187576524280438903], [(-2246062605121034966)]], [[145485054852250786, (-19548983471504184), (-60402721167320), 204207329056051, 76177544816], [202255427903382493, (-13781983751798745), 146464598727624, (-12521524451175)], [213718692046065719, (-11254821982346069), 10477350824400], [192965961375144964, (-8976393923975924)], [132925761052826744]]], r := 2303451002558702680, ok := true }, r3 := { p := [[[17000535627762372414842]], [[(-2251084289023105412289), 337123391351869307185], [(-1666911320036458877293)]], [[224351990099830540477, (-34666914359785883222), 2198069640928444379], [221216650692178450865, (-16238406357265326828)], [120111916350040061071]], [[(-19911475514536011831), 3114698948104153272, 27226427527098571, (-1633864865891478)], [(-22095723755476150919), 1666488116775440595, 14386035286670992], [(-15973813398645759501), 781335836564749292], [(-7661900274488206898)]], [[1657836267405601267, (-261770036076398157), (-488251662956207), 1609002537580006, 1207892335673], [1963064698889708397, (-150538546068332976), 1158604307896685, (-98964516674588)], [1596323920962527544, (-80255781424144725), 39377632889179], [1019779804702993151, (-37401704509175260)], [457368633133520893]]], r := 45101464645272427617, ok := true }, eta := { p := [[[(-6410020847984742901183)]], [[555879617587806411202, 0], [551964386913083627398]], [[(-39530808143117076798), 0, 0], [(-47854773983402892370), 0], [(-37939323495918312639)]], [[2631835198826658273, 0, 0, 0], [3343813175326533472, 0, 0], [3261364037312072161, 0], [2355657791228755558]], [[(-171096646926517588), 0, 0, 0, 0], [(-218990180031361940), 0, 0, 0], [(-225517777563532013), 0, 0], [(-201166174636979092), 0], [(-138133726205840473)]]], r := 456248552856989502, 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 := 828662331436171264, bh := 36028797018963968, tc := 2305843009213693952, th := 2305843009213693952, sc := 17293822569102704640, sh := 1152921504606846976 }
noncomputable def q7 : Cert := { V0 := [[[25076951644979257]], [[(-25691526883897824), 25076884786112658], [271102720810464]], [[636447770348957, (-25691321391750472), (-100287984575)], [(-275460722323322), 271100552411501], [(-2829464770553)]], [[(-22720053246051), 636232151749698, 308236605762, (-33428802652)], [4568753043999, (-275454075990133), (-3252581401)], [2903817233513, (-2829465581418)], [74219884706]], [[882602289593, (-22637545335270), (-323424549177), 102742843158, 394151], [(-220316013222), 4561815962179, 9969412615, (-1084165394)], [(-76526090915), 2903819290247, (-1216107)], [(-75952446002), 74219695912], [(-2189589663)]]], r0 := 35334193710523, V1 := [[[200598767228059278]], [[(-205480443868835134), 0], [2168275465211732]], [[5037272855920658, 0, 0], [(-2202011594321392), 0], [(-22635920989647)]], [[(-160996644438003), 0, 0, 0], [34803310457797, 0, 0], [23231048470215, 0], [593711509304]], [[5602077856544, 0, 0, 0, 0], [(-1104376300735), 0, 0, 0], [(-612517205057), 0, 0], [(-607473271923), 0], [(-17515515429)]]], r1 := 15663703516441, V2 := [[[16836345408327008206]], [[(-47343441859895570), 732991770662142], [(-70249179363560150)]], [[424922925600340, (-712108304821689), (-300741022639)], [(-1836126003038725), 65569694486732], [(-10450255111037)]], [[(-7730546682948), (-21104390592963), 593480169976, 117379483], [28175052636314, (-63879027558310), (-40251126498)], [10095981978232, 1516763735868], [(-10606595831)]], [[262466485309, 224731370261, (-284630282345), (-349326779), (-44290)], [(-478077149157), (-1716241366384), 79545463397, 20785818], [360790684016, (-1490028356890), (-1815804003)], [12746527529, 1576158734], [158330515]]], r2 := 34060078024319, V3 := [[[16883086579843861442]], [[(-94305165702791016), 1424671266308936], [(-68440898581237654)]], [[640385481973993, (-1341190026765292), (-1171207817194)], [(-3671456524889541), 127793061326746], [(-20516786102195)]], [[(-2369579089864), (-84319665924096), 2278070674307, 916616720], [55132333022378, (-121000758773169), (-157198837108)], [19418089231974, 2980371256869], [(-21690870801)]], [[(-20136253619), 840205434898, (-1041511904481), (-2704237516), (-694021)], [(-370268112376), (-6907979250178), 306650676310, 162824406], [1117957782281, (-2870429318025), (-7132887085)], [26190537479, 3862674392], [275121117]]], r3 := 186001717806571, Vm := [[[16841493475279020585]], [[(-52362431322048351), 0], [(-69788787310514768)]], [[294283405555721, 0, 0], [(-2286085372750116), 0], [189295913581]], [[(-6144170591799), 0, 0, 0], [17561588117801, 0, 0], [(-378262180065), 0], [149912616]], [[237347069309, 0, 0, 0, 0], [(-294630861859), 0, 0, 0], [188685349469, 0, 0], [(-253919878), 0], [13597898]]], rm := 11796644692386 }
noncomputable def w7 : Wit := { Z0 := { p := [[[25076985074491390]], [[(-25691629630375317), 25076985074491390], [271103805014208]], [[636555580486021, (-25691629630375317), 0], [(-275464045511708), 271103805014208], [(-2829464365072)]], [[(-22761308090503), 636555580486021, 0, 0], [4572221629994, (-275464045511708), 0], [2903816204904, (-2829464365072)], [74219979104]], [[885528529462, (-22761308090503), 0, 0, 0], [(-221624918775), 4572221629994, 0, 0], [(-76525447017), 2903816204904, 0], [(-75952736349), 74219979104], [(-2189592046)]]], r := 8483774550910, ok := true }, Z1 := { p := [[[200615880595931121]], [[(-205533037043002534), 0], [2168830440113664]], [[5092444643888170, 0, 0], [(-2203712364093658), 0], [(-22635714920569)]], [[(-182090464724022), 0, 0, 0], [36577773039958, 0, 0], [23230529639237, 0], [593759832837]], [[7084228235701, 0, 0, 0, 0], [(-1772999350198), 0, 0, 0], [(-612203576131), 0, 0], [(-607621890787), 0], [(-17516736363)]]], r := 3758102100399, ok := true }, Z2 := { p := [[[65059512016520684626]], [[(-1619705476124481561), 25076985074491390], [(-2403352524413616442)]], [[57460416252910223, (-25691629630375317), 0], [64562937154730319, 271103805014208], [94147134174210315]], [[(-2227879113157861), 636555580486021, 0, 0], [(-2160159620955025), (-275464045511708), 0], [(-2574802318163993), (-2829464365072)], [(-3869427842955000)]], [[92289711522451, (-22761308090503), 0, 0, 0], [80106975695520, 4572221629994, 0, 0], [86045794180678, 2903816204904, 0], [106676941146126, 74219979104], [161732460928127]]], r := 135471143432495, ok := true }, Z3 := { p := [[[66701631543943102866]], [[(-3402392596601796296), 51400057811863549], [(-2469247627128507021)]], [[208254523317084046, (-53982321637111262), 0], [136280723971237750, 550700018832516], [96777827925822407]], [[(-13159172655532004), 2740754191727164, 0, 0], [(-8408897561324779), (-568518134315640), 0], [(-5440680389252907), (-5810255048845)], [(-3978479900361867)]], [[844559684784285, (-168508649477685), 0, 0, 0], [535570035489741, 18889783505642, 0, 0], [338515809069414, 6121818639985, 0], [225525500567047, 151937810376], [166318534508976]]], r := 733319087504847, ok := true }, iE := { p := [[[71454143210515989135]], [[(-1751362852800391410), 0], [(-2334221054134993378)]], [[62433082970560497, 0, 0], [63722179632882264, 0], [93425620761117191]], [[(-2422790378099758), 0, 0, 0], [(-2110464672666113), 0, 0], [(-2558672063371483), 0], [(-3850501748283320)]], [[100426913503026, 0, 0, 0, 0], [77859791326866, 0, 0, 0], [85565876188943, 0, 0], [106309308028078, 0], [161174114956570]]], r := 136677988414523, ok := true }, iHu := { p := [[[73229438886049773670]], [[(-3678940044596392141), 0], [(-2399308724736777458)]], [[225800536034726874, 0, 0], [134568523323713629, 0], [96039925534619155]], [[(-14273004229827922), 0, 0, 0], [(-8290613837947901), 0, 0], [(-5406922068226895), 0], [(-3959183798444099)]], [[916214448813128, 0, 0, 0, 0], [528428445187176, 0, 0, 0], [336710134684279, 0, 0], [224756900126867, 0], [165748966274257]]], r := 742548696400442, ok := true }, T := { p := [[[2305843009213693952]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[4762248228467439140]], [[116724157178402419, 0], [155570266193742497]], [[(-1300071370164476), 0, 0], [3379218090150789, 0], [(-1144518743655529)]], [[27620280698849, 0, 0, 0], [(-59010004733946), 0, 0], [(-38484785696052), 0], [15831645853267]], [[(-922537528739), 0, 0, 0, 0], [1196025668355, 0, 0, 0], [(-112801079522), 0, 0], [508706569716, 0], [(-344915286762)]]], r := 1683288528237, ok := true }, de := { p := [[[(-41574099808933591388)]], [[926103014294555796, 0], [603980226713840736]], [[(-29512870367604425), 0, 0], [1770300142018395, 0], [(-12552733143120975)]], [[1314335206163181, 0, 0, 0], [5188849658013, 0, 0], [3384032385660, 0], [364582996696041]], [[(-65710930263834), 0, 0, 0, 0], [15208811283, 0, 0, 0], [127679264472, 0, 0], [6468776066, 0], [(-11887521287469)]]], r := 20937293778174, ok := true }, dde := { p := [[[(-329853734482652220424)]], [[21023429047949169205, 0], [13710931987792936431]], [[(-1404395740289840401), 0, 0], [(-917758398293306245), 0], [(-597332781786794112)]], [[93618076647187597, 0, 0, 0], [61044433414946105, 0, 0], [39811587009747471, 0], [25968686503185529]], [[(-6241229455281096), 0, 0, 0, 0], [(-4070414668491556), 0, 0, 0], [(-2654874492764643), 0, 0], [(-1731272779604150), 0], [(-1129077730474097)]]], r := 1366554827725818, ok := true }, nJu := { p := [[[(-83148199617867182775)]], [[1852206028589111592, 0], [1207960453427681473]], [[(-59025740735208850), 0, 0], [3540600284036790, 0], [(-25105466286241949)]], [[2628670412326363, 0, 0, 0], [10377699316026, 0, 0], [6768064771321, 0], [729165993392083]], [[(-131421860527668), 0, 0, 0, 0], [30417622567, 0, 0, 0], [255358528945, 0, 0], [12937552132, 0], [(-23775042574938)]]], r := 41874587556340, ok := true }, Jd1 := { p := [[[(-659707468965304440847)]], [[42046858095898338411, 0], [27421863975585872862]], [[(-2808791480579680802), 0, 0], [(-1835516796586612489), 0], [(-1194665563573588223)]], [[187236153294375195, 0, 0, 0], [122088866829892211, 0, 0], [79623174019494943, 0], [51937373006371058]], [[(-12482458910562192), 0, 0, 0, 0], [(-8140829336983112), 0, 0, 0], [(-5309748985529286), 0, 0], [(-3462545559208299), 0], [(-2258155460948194)]]], r := 2733109655451628, ok := true }, term0 := { p := [[[8857439954105369759530]], [[(-1108174161055981590359), 0], [(-708097284829240745239)]], [[108740926288271977880, 0, 0], [91700563647952299552, 0], [44976556634257223753]], [[(-9572141002054012678), 0, 0, 0], [(-9076992384209634015), 0, 0], [(-5877311949065451484), 0], [(-2572113146555656751)]], [[792997834491620883, 0, 0, 0, 0], [802782972965102344, 0, 0, 0], [583757858589833933, 0, 0], [337754952507130203, 0], [138640906117393148]]], r := 306923065481289112, ok := true }, r0 := { p := [[[6764344336263301417]], [[(-508123506391203169), 13528630474664618588], [(-222154501024681929)]], [[36416169653272132, (-1016123408500935556), 6764198842161455269], [18399327623484506, (-444308348949878471)], [8893166335076256]], [[(-2365362326937613), 72759070524092403, (-507814497995554562), (-116394064630224)], [(-1227243345520223), 36797242611907156, (-222152868270216624)], [(-739240062889065), 17786303812365634], [(-366684199964964)]], [[147561940558861, (-4722157631272992), 36233001408943993, 247201638888906, (-29097133388206)], [75759816729816, (-2453611089035030), 18395796012172942, 1306216226143], [49717048969791, (-1478418327309465), 8893094190688932], [30708000487106, (-733367309832620)], [15352925359310]]], r := 8074158947087516, ok := true }, r1 := { p := [[[432800745744786215454]], [[(-32270864682059602806), 0], [(-14216571052053658040)]], [[2183160537056775850, 0, 0], [1174707595361235169, 0], [569104473215602053]], [[(-134291557744789125), 0, 0, 0], [(-76776005289803774), 0, 0], [(-47186799425861541), 0], [(-23465591277754063)]], [[7977120566471249, 0, 0, 0, 0], [4592069667508470, 0, 0, 0], [3106521087683045, 0, 0], [1960601889079043, 0], [982500118981976]]], r := 6749921490791952, ok := true }, r2 := { p := [[[4420343333220493911745]], [[(-396606478414786469722), 74314054700895839406], [(-384305659735583105859)]], [[28366319582529301461, (-4974971367847956164), 560383751492779638], [33798378551547419008, (-3246537851131445818)], [24827862038311451769]], [[(-1890169251597126414), 300636852311295967, 3699762301155969, (-231407671244562)], [(-2373218025629750257), 197335152581651202, 3783918526161644], [(-2158094233256090602), 142572042735924788], [(-1428951114010121832)]], [[122735493731286487, (-18102398877228790), (-66057483699366), 229523670920341, 95020997175], [155703479080527085, (-11551198444648621), 148790237004494, (-13121341140544)], [149818595193612292, (-8591281496385752), 11985383217501], [123136203399352379, (-6232936739002464)], [77211941976115967]]], r := 1503055695214855018, ok := true }, r3 := { p := [[[14092429472895072785895]], [[(-1865261987649193895187), 307498791090151560397], [(-1265617464460018163178)]], [[185817803331385318214, (-31627054586268883666), 2227008252917844233], [167855940061407580245, (-13510854016722823353)], [83325521432445050474]], [[(-16488022698731649904), 2839819797218049186, 29565429368825105, (-1836437530378548)], [(-16763313640296799209), 1386110397529975707, 14556837040085555], [(-11078076350069466032), 593827094295959592], [(-4855159692263281991)]], [[1372646639011782182, (-238775113916560575), (-518135692321966), 1806409906817353, 1505850639872], [1489255568815402920, (-125480946484606840), 1179948002880163, (-103638133282846)], [1107018416610808875, (-61094811443323897), 45776633322275], [646083416995207380, (-25967636254647869)], [264691347906031933]]], r := 30652846452454675767, ok := true }, eta := { p := [[[(-5440989244978335461792)]], [[471774886434527512010, 0], [424606004642807141614]], [[(-33646340437798181610), 0, 0], [(-36894503581762825592), 0], [(-26585545586218016567)]], [[2245981049361273695, 0, 0, 0], [2584937461733519250, 0, 0], [2290684590908852769, 0], [1505174516306972528]], [[(-146341466260770047), 0, 0, 0, 0], [(-169719098171112372), 0, 0, 0], [(-158831075973837757), 0, 0], [(-128847522870395591), 0], [(-80519011585931671)]]], r := 306009188374650753, 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 576460752303423488 864691128455135232 0 4611686018427387904 13835058055282163712 18446744073709551616 :=
  (RegionPosI.split_b 720575940379279360 (RegionPosI.split_s 16140901064495857664 (RegionPosI.split_b 648518346341351424 (RegionPosI.of_check c0 q0 ok_0 576460752303423488 648518346341351424 0 4611686018427387904 13835058055282163712 16140901064495857664 (by decide +kernel)) (RegionPosI.of_check c1 q1 ok_1 648518346341351424 720575940379279360 0 4611686018427387904 13835058055282163712 16140901064495857664 (by decide +kernel))) (RegionPosI.split_b 648518346341351424 (RegionPosI.of_check c2 q2 ok_2 576460752303423488 648518346341351424 0 4611686018427387904 16140901064495857664 18446744073709551616 (by decide +kernel)) (RegionPosI.of_check c3 q3 ok_3 648518346341351424 720575940379279360 0 4611686018427387904 16140901064495857664 18446744073709551616 (by decide +kernel)))) (RegionPosI.split_s 16140901064495857664 (RegionPosI.split_b 792633534417207296 (RegionPosI.of_check c4 q4 ok_4 720575940379279360 792633534417207296 0 4611686018427387904 13835058055282163712 16140901064495857664 (by decide +kernel)) (RegionPosI.of_check c5 q5 ok_5 792633534417207296 864691128455135232 0 4611686018427387904 13835058055282163712 16140901064495857664 (by decide +kernel))) (RegionPosI.split_b 792633534417207296 (RegionPosI.of_check c6 q6 ok_6 720575940379279360 792633534417207296 0 4611686018427387904 16140901064495857664 18446744073709551616 (by decide +kernel)) (RegionPosI.of_check c7 q7 ok_7 792633534417207296 864691128455135232 0 4611686018427387904 16140901064495857664 18446744073709551616 (by decide +kernel)))))

end CKLaneC.RSC2.S10_0052