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

import Definitions.Def_CK_CKLaneC_RSCell_Staged
import Definitions.Def_CK_CKLaneC_RSCell_RegionI

-- ===== source module CKLaneC.RSC2.S01_0277 =====
section

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

namespace CKLaneC.RSC2.S01_0277
open CKLaneC.TM3 CKLaneC.RSCell

noncomputable def c0 : Cell := { bc := 2040693581152256, bh := 70368744177664, tc := 16140901064495857664, th := 2305843009213693952, sc := 12970366926827028480, sh := 288230376151711744 }
noncomputable def q0 : Cert := { V0 := [[[380236249643049327]], [[(-23216768011603161), 54286173298179986], [1277869979960773]], [[198995952473513, (-3310583701056225), (-7128616526197)], [(-77022339053774), 182217245984146], [(-17737916720341)]], [[(-1905299448693), 28003530424727, 1305021315928, (-338231363138)], [608900617566, (-10941990420185), (-71829445082)], [1072671253127, (-2530457153513)], [372847238451]], [[19556818064, (-257737785066), (-90750700316), 61769587084, 131179376], [(-6033783490), 82755642722, 13088102857, (-3399848808)], [(-8666646558), 152593001992, 756011709], [(-22570559821), 53196011651], [(-9116349768)]]], r0 := 2555422559527, V1 := [[[434514956228230853]], [[(-26525984962883735), 0], [1460011998914718]], [[226904464976140, 0, 0], [(-87950625085136), 0], [(-20267582025431)]], [[(-2159813697831), 0, 0, 0], [690711134184, 0, 0], [1225119539828, 0], [426028026356]], [[21999208946, 0, 0, 0, 0], [(-6721856490), 0, 0, 0], [(-9849860502), 0, 0], [(-25779720326), 0], [(-10416761446)]]], r1 := 743123553079, V2 := [[[18443274225729973579]], [[(-32538134692862), 15780862529], [(-119629212340774)]], [[21762643411, (-681040843), (-68654)], [(-1124385745521), 1093947608], [426337474]], [[(-209611162), (-7961246), 6572, 0], [829016270, (-47187940), (-7142)], [(-49464241), 19075453], [(-3929291)]], [[2581246, 5730, (-121), 0, 0], [(-7914488), (-553373), 683, 0], [1640396, (-821949), (-248)], [444628, 3017], [60948]]], r2 := 4589509736, V3 := [[[18443874322308863940]], [[(-63770888009956), 26052418713], [(-98957852274609)]], [[30698933, (-786419771), (-226400)], [(-2198968787048), 1805798318], [(-31479856)]], [[4569, (-30698844), 18718, 2], [2129377, (-54470451), (-23550)], [947962, 31480674], [(-4853)]], [[(-29), (-4555), (-90), 0, 0], [350, (-2129368), 1946, 0], [37181, (-948030), (-819)], [122, 4862], [32]]], r3 := 13346171022, Vm := [[[18443274242703820647]], [[(-32538940518417), 0], [(-119628031255400)]], [[21757919522, 0, 0], [(-1124442041723), 0], [447102683]], [[(-209605292), 0, 0, 0], [828698649, 0, 0], [(-50462563), 0], [(-3923589)]], [[2581275, 0, 0, 0, 0], [(-7914038), 0, 0, 0], [1635232, 0, 0], [444235, 0], [60912]]], rm := 459557581 }
noncomputable def w0 : Wit := { Z0 := { p := [[[380352831117881025]], [[(-23238128359174063), 54336118731125860], [1279045671034947]], [[200484094314585, (-3319732622739152), 0], [(-77236865553303), 182720810147849], [(-17750282645589)]], [[(-1956052853624), 28640584902083, 0, 0], [623748311970, (-11033837936187), 0], [1074933696410, (-2535754663656)], [373084952563]], [[20572671466, (-279436121947), 0, 0, 0], [(-6534871835), 89106901710, 0, 0], [(-8823904527), 153561956630, 0], [(-22614075463), 53297850366], [(-9121853121)]]], r := 627725917458, ok := true }, Z1 := { p := [[[434688949849006885]], [[(-26557860981913214), 0], [1461766481182797]], [[229124679216669, 0, 0], [(-88270703489489), 0], [(-20286037309244)]], [[(-2235488975570), 0, 0, 0], [712855213680, 0, 0], [1228495653041, 0], [426382802929]], [[23511624533, 0, 0, 0, 0], [(-7468424954), 0, 0, 0], [(-10084462316), 0, 0], [(-25844657672), 0], [(-10424974996)]]], r := 185918188086, ok := true }, Z2 := { p := [[[13233151385586320053347]], [[(-112034177260236407482), 54336118731125860], [(-411903156324100168852)]], [[1079885581217883073, (-3319732622739152), 0], [3518145374167907687, 182720810147849], [13585697745117199623]], [[(-11229025847934268), 28640584902083, 0, 0], [(-33699464161143145), (-11033837936187), 0], [(-116418961749601429), (-2535754663656)], [(-455487946605329505)]], [[124861414961593, (-279436121947), 0, 0, 0], [346112086919113, 89106901710, 0, 0], [1112695718811479, 153561956630, 0], [3910816233628570, 53297850366], [15389029239913896]]], r := 2465325863108360, ok := true }, Z3 := { p := [[[15710427990127151726494]], [[(-315795020037127509552), 129012224017295758], [(-490041740315937935833)]], [[6717661401307274266, (-9382999044882826), 0], [9958732413751373977, 425259807136310], [16175573560011611821]], [[(-145211902574411373), 191624289854775, 0, 0], [(-212705856417184317), (-30025215330186), 0], [(-330060367798398661), (-5930007065493)], [(-542572916047666345)]], [[3162754058072072, (-4095286883768), 0, 0, 0], [4609104794619853, 557801128377, 0, 0], [7060737364612825, 421669905252, 0], [11098004155964467, 124832175012], [18337314780985981]]], r := 11285998152940294, ok := true }, iE := { p := [[[13235699463575237587133]], [[(-112035727310069311133), 0], [(-411894587679792709163)]], [[1079924032952392488, 0, 0], [3518146244714084152, 0], [13585578831569551360]], [[(-11229554361399008), 0, 0, 0], [(-33699304796403840), 0, 0], [(-116418953335229660), 0], [(-455485447216662330)]], [[124868469743912, 0, 0, 0, 0], [346109524667642, 0, 0, 0], [1112693623605045, 0, 0], [3910815919148126, 0], [15388968130356523]]], r := 2465111687199798, ok := true }, iHu := { p := [[[15713001444490444099781]], [[(-315799210390106306783), 0], [(-490033257501890322066)]], [[6717806362336852308, 0, 0], [9958736628282291231, 0], [16175455271975936998]], [[(-145215364820221176), 0, 0, 0], [(-212705569856591629), 0, 0], [(-330060367018979845), 0], [(-542570425974280576)]], [[3162832795453118, 0, 0, 0, 0], [4609096857876259, 0, 0, 0], [7060732864549045, 0, 0], [11098003733820074, 0], [18337253843664072]]], r := 11285345802567478, ok := true }, T := { p := [[[16140901064495857664]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[25709435897770160]], [[217621694831097, 0], [800076907739913]], [[(-255583987088), 0, 0], [6711004689420, 0], [(-1490682085445)]], [[1893067447, 0, 0, 0], [(-8813926517), 0, 0], [(-13676782526), 0], [17132613493]], [[(-21034082), 0, 0, 0, 0], [65278188, 0, 0, 0], [(-23642), 0, 0], [157179940, 0], [(-295389889)]]], r := 194564710, ok := true }, de := { p := [[[(-125899523464392661499)]], [[295723293622045103, 0], [458880972861794126]], [[(-3285558769709283), 0, 0], [793253386537, 0], [(-7911125456196551)]], [[48674945031004, 0, 0, 0], [1371273, 0, 0], [2127837, 0], [181864954116618]], [[(-811249083849), 0, 0, 0, 0], [3, 0, 0, 0], [23649, 0, 0], [6, 0], [(-4703403985772)]]], r := 745664775665, ok := true }, dde := { p := [[[(-171083226666499070747148)]], [[3801553735179786888214, 0], [5898962692520358939801]], [[(-84478972404131643359), 0, 0], [(-131088061420415930735), 0], [(-203412507869639227963)]], [[1877310497868724694, 0, 0, 0], [2913068013931475875, 0, 0], [4520277952652274201, 0], [7014224409294609686]], [[(-41718011063737119), 0, 0, 0, 0], [(-64734844754086350), 0, 0, 0], [(-100450621170184689), 0, 0], [(-155871653539873671), 0], [(-241869807217052306)]]], r := 22581995047789259, ok := true }, nJu := { p := [[[(-251799046928785322998)]], [[591446587244090207, 0], [917761945723588252]], [[(-6571117539418566), 0, 0], [1586506773075, 0], [(-15822250912393102)]], [[97349890062008, 0, 0, 0], [2742546, 0, 0], [4255675, 0], [363729908233236]], [[(-1622498167698), 0, 0, 0, 0], [6, 0, 0, 0], [47298, 0, 0], [12, 0], [(-9406807971544)]]], r := 1491329551326, ok := true }, Jd1 := { p := [[[(-342166453332998141494296)]], [[7603107470359573776428, 0], [11797925385040717879602]], [[(-168957944808263286717), 0, 0], [(-262176122840831861469), 0], [(-406825015739278455926)]], [[3754620995737449388, 0, 0, 0], [5826136027862951751, 0, 0], [9040555905304548403, 0], [14028448818589219372]], [[(-83436022127474238), 0, 0, 0, 0], [(-129469689508172700), 0, 0, 0], [(-200901242340369378), 0, 0], [(-311743307079747342), 0], [(-483739614434104612)]]], r := 45163990095578514, ok := true }, term0 := { p := [[[2200049283897148926426002593]], [[(-97768560554511515408995489), 0], [(-151701445707378160987914503)]], [[3258825300030478779200287, 0, 0], [6741893211715995537457699, 0], [7846176734459776508023568]], [[(-96555909357072278406955), 0, 0, 0], [(-224725404121660857728090), 0, 0], [(-348705405142132253284842), 0], [(-360733418419845292905987)]], [[2682077304743400071372, 0, 0, 0, 0], [6658465757648731583235, 0, 0, 0], [11623362828805805097405, 0, 0], [16032128759254565243289, 0], [15548586841725543011209]]], r := 2585058546674342459143, ok := true }, r0 := { p := [[[78933215843634834882820]], [[(-2071110535619399071508), 22530082129793032722243], [(-2462369725328474327134)]], [[40474360947111649878, (-588447758019073702513), 1602937023909632474792], [64978129431040549707, (-702989094892914373026)], [81287678991624221662]], [[(-708448051134453787), 11375974958489218739, (-41091541729240583536), (-905811854254278554)], [(-1261966947190083015), 18484189377555155151, (-50057883765515285455)], [(-2149410290426809202), 23208609086375535094], [(-2726764607895849805)]], [[11953020960830677, (-196458470523321613), 759035960176337461, 133813562570348120, (-31997109381675753)], [21836398246402648, (-355922187033967915), 1297192553879893667, 22196633568615889], [41647896351344254, (-611672398620268898), 1653063479017656105], [72188202918440310, (-778553955028126709)], [92159870222699691]]], r := 451767552887366366, ok := true }, r1 := { p := [[[103065297219237652733666]], [[(-2700511346382965292188), 0], [(-3215393721449744952990)]], [[52601527166144666686, 0, 0], [84756104253695900436, 0], [106148658190063208467]], [[(-917007605825842303), 0, 0, 0], [(-1641796177929259631), 0, 0], [(-2803973088909779221), 0], [(-3560758619725257074)]], [[15411525752466306, 0, 0, 0, 0], [28315004986344939, 0, 0, 0], [54201192136702358, 0, 0], [94178077249162099, 0], [120348377009200134]]], r := 74221121066356545, ok := true }, r2 := { p := [[[895074465940138835231767006]], [[(-21061717838667426151617613), 39321820293849637890634], [(-61198094247693772467026297)]], [[407734460405375538324477, (-660362832776041910543), 454017581849158133], [1426825023153527649518890, (-1354028470888601500933)], [3149067048273709664065623]], [[(-7680926817144195611944), 10679672473082193471, 114425208682812, (-46588969854533)], [(-27355007041540057904924), 22368439541726076560, 112563021109498], [(-73004874591896455181699), 46661617455650909178], [(-144258557267694366975379)]], [[147411129075739313933, (-176801115447287837), (-42495642710663), 1711664740344, (-5015835385445)], [510767651122208232126, (-354787642022858931), (-39802563749972), 4962342471691], [1391206280311727978753, (-765759656462743327), (-25784037235009)], [3330840333980783221870, (-1608408529452519909)], [6200774665960571608473]]], r := 16010738267079488048937, ok := true }, r3 := { p := [[[4399064791475925603723883853]], [[(-195500647049799054215961230), 204982563177167529529729], [(-303367230862310731999134299)]], [[6516540049189732623439472, (-7244336586531453045706), 1805635275185742484], [13482528302002486507930175, (-7083356131714623987011)], [15691123604793323480972064]], [[(-193080472756797604658659), 220705493993829965667, 1224966673844560, (-354167826446943)], [(-449412503195384929800613), 250199502749539657795, 269701795490547], [(-697367421993110736993125), 244443227973546288016], [(-721424424103894820791313)]], [[5363309808809370219740, (-6231887105386290057), (-122501779419610), 27121587892094, (-38680541943568)], [13315850166383315620014, (-7621315123770030850), (-270030255661344), (-303710094901236)], [23245404628331843273586, (-8632763234751244540), (-236103616641409)], [32062760967591574266025, (-8433157175070999549)], [31095710912766729639242]]], r := 254084801078160697107402, ok := true }, eta := { p := [[[(-895337999971656604787265974)]], [[21069366133799569873271908, 0], [61207087027270870216757453]], [[(-407919516951853377513113), 0, 0], [(-1427085880268763171796425), 0], [(-3149375886443199070766194)]], [[7685163749814508887406, 0, 0, 0], [27361310504874819311344, 0, 0], [73013830176563040912978, 0], [144269180714013742245640]], [[(-147506265559048554361), 0, 0, 0, 0], [(-510911858655102032784), 0, 0, 0], [(-1391422603668021084647), 0, 0], [(-3331148340714985648575), 0], [(-6201140377603220461509)]]], r := 1645761526833774498140, ok := true } }
theorem sB_0 : stageB c0 w0 = true := by decide +kernel
theorem s0_0 : stageC0 w0 q0 = true := by decide +kernel
theorem s1_0 : stageC1 w0 q0 = true := by decide +kernel
theorem s2_0 : stageC2 w0 q0 = true := by decide +kernel
theorem s3_0 : stageC3 w0 q0 = true := by decide +kernel
theorem sE_0 : stageE w0 q0 = true := by decide +kernel
theorem sF_0 : stageF w0 = true := by decide +kernel
theorem ok_0 : (domOK c0 && cellCheck c0 q0) = true :=
  staged_check c0 q0 w0 (by decide +kernel) sB_0 s0_0 s1_0 s2_0 s3_0 sE_0 sF_0

noncomputable def c1 : Cell := { bc := 2040693581152256, bh := 70368744177664, tc := 16140901064495857664, th := 2305843009213693952, sc := 13546827679130451968, sh := 288230376151711744 }
noncomputable def q1 : Cert := { V0 := [[[334583761230581737]], [[(-22443038681468871), 47774997400233314], [1126213683341366]], [[188016929535852, (-3201584260566139), (-4857874722469)], [(-74657055870706), 160658636907180], [(-15626572440213)]], [[(-1757045378541), 26515240600076, 977114099020, (-230680128893)], [574247091215, (-10619391818144), (-49032543416)], [1039000053587, (-2229960359210)], [328426281380]], [[17553121765, (-238682726614), (-73653036645), 46312247067, 69249572], [(-5527508807), 78595367450, 9820803851, (-2323993962)], [(-8176023311), 147944888328, 515487016], [(-21857310457), 46871774930], [(-8029639782)]]], r0 := 2366286855879, V1 := [[[382353670147176910]], [[(-25643599539548690), 0], [1286820964908479]], [[214455044117089, 0, 0], [(-85266163269314), 0], [(-17855992851801)]], [[(-1992975085614), 0, 0, 0], [652073081445, 0, 0], [1186836502288, 0], [375287677888]], [[19761940906, 0, 0, 0, 0], [(-6168380890), 0, 0, 0], [(-9299466905), 0, 0], [(-24968396361), 0], [(-9175419937)]]], r1 := 675693532471, V2 := [[[18443209234874450509]], [[(-32453519640887), 14386980757], [(-121874729566923)]], [[20564163210, (-712818941), (-56008)], [(-1121161643411), 997361497], [333860853]], [[(-190322667), (-7928258), 6066, 0], [783762127, (-49396575), (-5827)], [(-43065949), 17392790], [(-3097100)]], [[2250709, 5275, (-132), 0, 0], [(-7186848), (-550978), 631, 0], [1560027, (-860684), (-203)], [388054, 2773], [48027]]], r2 := 4571386305, V3 := [[[18443746780655675875]], [[(-63770765160271), 24356747800], [(-103355781328429)]], [[30725695, (-909268927), (-189436)], [(-2198960265404), 1688337190], [(-29435147)]], [[4355, (-30725521), 18189, 1], [2131428, (-62992039), (-19706)], [1096775, 29435833], [(-4581)]], [[(-26), (-4341), (-175), 0, 0], [333, (-2131410), 1891, 0], [37225, (-1096841), (-686)], [149, 4589], [30]]], r3 := 12800362076, Vm := [[[18443209250217798298]], [[(-32454344290723), 0], [(-121873662340812)]], [[20559475147, 0, 0], [(-1121219204645), 0], [352608838]], [[(-190316607), 0, 0, 0], [783447245, 0, 0], [(-44084811), 0], [(-3092167)]], [[2250728, 0, 0, 0, 0], [(-7186386), 0, 0, 0], [1554921, 0, 0], [387678, 0], [47996]]], rm := 459493941 }
noncomputable def w1 : Wit := { Z0 := { p := [[[334663184282293067]], [[(-22459024291929760), 47809026326041866], [1127015856945982]], [[189223646152117, (-3208432041704252), 0], [(-74817900209061), 161002265277997], [(-15635001410771)]], [[(-1800305197548), 27031949450302, 0, 0], [586313533315, (-10688271458438), 0], [1040694316795, (-2233571630111)], [328588281320]], [[18415270837, (-257186456793), 0, 0, 0], [(-5955504785), 83759076187, 0, 0], [(-8303640690), 148670616685, 0], [(-21889889706), 46941183045], [(-8033389808)]]], r := 582447530198, ok := true }, Z1 := { p := [[[382472210608334934]], [[(-25667456333634011), 0], [1288018122223979]], [[216255595602420, 0, 0], [(-85506171667498), 0], [(-17868573040881)]], [[(-2057491654340), 0, 0, 0], [670072609503, 0, 0], [1189364933480, 0], [375529464366]], [[21046023813, 0, 0, 0, 0], [(-6806291183), 0, 0, 0], [(-9489875074), 0, 0], [(-25017016806), 0], [(-9181016924)]]], r := 169009943075, ok := true }, Z2 := { p := [[[13013314692652331911071]], [[(-107845502893383145431), 47809026326041866], [(-404998953752334323107)]], [[1015393738161226174, (-3208432041704252), 0], [3387383102761652871, 161002265277997], [13357221536122552456]], [[(-10286614855084199), 27031949450302, 0, 0], [(-31710277859082138), (-10688271458438), 0], [(-112100835974406989), (-2233571630111)], [(-447812652667473512)]], [[111085236117659, (-257186456793), 0, 0, 0], [317497710649723, 83759076187, 0, 0], [1047301962887565, 148670616685, 0], [3765936219444232, 46941183045], [15129352594387529]]], r := 2363462572426563, ok := true }, Z3 := { p := [[[15104595383560018674637]], [[(-290570966923086485215), 110981321010152129], [(-470939767497140142893)]], [[5917104203846928141, (-8662953306540725), 0], [9160167742464711622, 367352642441587], [15542521869281458623]], [[(-122451958978470618), 169036661752742, 0, 0], [(-187299360633821058), (-27924138561242), 0], [(-303553726289143302), (-5117456912452)], [(-521287926534668834)]], [[2553370526184795, (-3456621145559), 0, 0, 0], [3885557546494761, 494480830391, 0, 0], [6216617079209683, 391491027338, 0], [10205924035136240, 107692781243], [17616739687713053]]], r := 9928397431778892, ok := true }, iE := { p := [[[13015859820230277081042]], [[(-107846905260178138630), 0], [(-404990382749388641476)]], [[1015429180700379164, 0, 0], [3387384581181225926, 0], [13357102631279890718]], [[(-10287090593795496), 0, 0, 0], [(-31710133007122488), 0, 0], [(-112100835558875961), 0], [(-447810153739787837)]], [[111091400090312, 0, 0, 0, 0], [317495428520485, 0, 0, 0], [1047300055106983, 0, 0], [3765936070381928, 0], [15129291500120505]]], r := 2363269868015272, ok := true }, iHu := { p := [[[15107161010569253367995]], [[(-290574616593272646761), 0], [(-470931275168406052076)]], [[5917230148831450569, 0, 0], [9160173013686865396, 0], [15542403565718717830]], [[(-122454856066318432), 0, 0, 0], [(-187299117503317001), 0, 0], [(-303553742158989422), 0], [(-521285436930961262)]], [[2553433754027740, 0, 0, 0, 0], [3885550956545725, 0, 0, 0], [6216613234550547, 0, 0], [10205923978156787, 0], [17616678773424098]]], r := 9927855712164975, ok := true }, T := { p := [[[16140901064495857664]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[26143671768195040]], [[216621424268523, 0], [813464172333747]], [[(-244708918785), 0, 0], [6676509858714, 0], [(-1518035745069)]], [[1735383240, 0, 0, 0], [(-8438924166), 0, 0], [(-13676877097), 0], [17446973371]], [[(-18461523), 0, 0, 0, 0], [59840802, 0, 0, 0], [(-23643), 0, 0], [157179940, 0], [(-300809887)]]], r := 195697662, ok := true }, de := { p := [[[(-125320842247608096546)]], [[283140302592500361, 0], [458882559374052309]], [[(-3011886149842791), 0, 0], [793258871657, 0], [(-7911125451846284)]], [[42721789641510, 0, 0, 0], [1371287, 0, 0], [2222431, 0], [181864954116630]], [[(-681730685768), 0, 0, 0, 0], [3, 0, 0, 0], [23649, 0, 0], [6, 0], [(-4703403985772)]]], r := 731195788038, ok := true }, dde := { p := [[[(-163803655686197880337974)]], [[3484901000229025339086, 0], [5647943000371178994341]], [[(-74146830281604276665), 0, 0], [(-120169001594544064270), 0], [(-194756656470943958652)]], [[1577592133650314223, 0, 0, 0], [2556787251085696521, 0, 0], [4143758648311303043, 0], [6715746774856546904]], [[(-33565790077655992), 0, 0, 0, 0], [(-54399728746555106), 0, 0, 0], [(-88165077623778613), 0, 0], [(-142888229252259500), 0], [(-231577474995050277)]]], r := 20425079715087229, ok := true }, nJu := { p := [[[(-250641684495216193092)]], [[566280605185000723, 0], [917765118748104618]], [[(-6023772299685581), 0, 0], [1586517743314, 0], [(-15822250903692567)]], [[85443579283020, 0, 0, 0], [2742575, 0, 0], [4444862, 0], [363729908233261]], [[(-1363461371536), 0, 0, 0, 0], [6, 0, 0, 0], [47298, 0, 0], [13, 0], [(-9406807971544)]]], r := 1462391576070, ok := true }, Jd1 := { p := [[[(-327607311372395760675948)]], [[6969802000458050678173, 0], [11295886000742357988682]], [[(-148293660563208553329), 0, 0], [(-240338003189088128540), 0], [(-389513312941887917303)]], [[3155184267300628447, 0, 0, 0], [5113574502171393042, 0, 0], [8287517296622606087, 0], [13431493549713093809]], [[(-67131580155311983), 0, 0, 0, 0], [(-108799457493110212), 0, 0, 0], [(-176330155247557225), 0, 0], [(-285776458504519000), 0], [(-463154949990100554)]]], r := 40850159430174450, ok := true }, term0 := { p := [[[2016815754193596363570111913]], [[(-85811489452298419565993635), 0], [(-139066102434276243430681200)]], [[2738553336747964470986548, 0, 0], [5917345979577042233076626, 0], [7192649528591295988023916]], [[(-77687878769510854107308), 0, 0, 0], [(-188847632252256125439841), 0, 0], [(-306057761430067933966697), 0], [(-330686766021175895915872)]], [[2066141814208011624935, 0, 0, 0, 0], [5357325238632954055759, 0, 0, 0], [9767668649087673912650, 0, 0], [14071348612808917676847, 0], [14253487396714438732884]]], r := 2215770182023601280694, ok := true }, r0 := { p := [[[74947409629863069251917]], [[(-1917347493012902793881), 21397169490940590020218], [(-2337292263390737100383)]], [[36495178673793427187, (-545200888050583237608), 1523694314140251379130], [60181148061059298729, (-667397224063421448775)], [77149893881166022909]], [[(-620380211781868599), 10271568475285694072, (-38197601551100942778), (-666718679050567057)], [(-1139199955360273011), 17130521028840715273, (-47556853149675281781)], [(-1991063997293961306), 22030747593751862460], [(-2587789518641737540)]], [[10125872550705850, (-172336686058517306), 689363429141375822, 106142729079853821, (-23610006044408374)], [19158724600317273, (-321650876865851212), 1205317104856014598, 16319562302613304], [37612712938498959, (-566941206160376459), 1570175561763952321], [66876853950283310, (-738985257368410962)], [87458611394432328]]], r := 403799729359328662, ok := true }, r1 := { p := [[[97867583123867665264751]], [[(-2500636113297323642553), 0], [(-3052229442086597998395)]], [[47449603634880193710, 0, 0], [78514287046787340283, 0], [100750307368074960959]], [[(-803429794325698260), 0, 0, 0], [(-1482571983491838097), 0, 0], [(-2597867459689908330), 0], [(-3379433847461128275)]], [[13062409246094362, 0, 0, 0, 0], [24853572845363400, 0, 0, 0], [48964773042784353, 0, 0], [87263483250943791, 0], [114214248933069521]]], r := 65237867731340097, ok := true }, r2 := { p := [[[854522789619509047800332041]], [[(-19518456334451067709498139), 38042446399693898529043], [(-58449927927498773299328756)]], [[364966984537038398147076, (-619671789352250140809), 454258478130847938], [1323237358563178111633074, (-1310666073770107143938)], [3008423013963325166431707]], [[(-6609410615881244391489), 9688251279795357529, 111493760544122, (-2253440493799)], [(-24509554544327294720718), 21015463360344711104, 101659084724613], [(-67735084543427211093333), 45176788275305834603], [(-137840658985283017956339)]], [[121497729522586190222, (-154382496020686987), (-10142189343906), (-4494792004231), (-184468496595)], [439984512892829061603, (-322474152972687109), (-18879020185901), (-608182638779)], [1247250850345130108860, (-719805797246252408), (-25067976333442)], [3091398965097222037506, (-1557425906370720046)], [5925735749942454142913]]], r := 14860206579552092088506, ok := true }, r3 := { p := [[[4032666475908223306407625918]], [[(-171590596265338910946535858), 191329413144873915258413], [(-278098915543463428546179206)]], [[5476165563497512225006143, (-6431250184367594135326), 1808184184724985522], [11833574960167334404374559, (-6611807752915530437594)], [14384150969177356604039776]], [[(-155350369829677699811514), 187020706152129255174, 1052728818520742, (-303660833599365)], [(-377662803406301153062737), 222123211211124015342, 175010113904565], [(-612077001321764103531729), 228173511057048930546], [(-661333939338828527575228)]], [[4131629118050632519364, (-5047173621001530663), (-153605123478001), 22660848296077, (-33249664822951)], [10713774753473957950285, (-6458139922853720041), (-176553081447033), (-258236506078530)], [19534217786775286825472, (-7663971179974714126), (-146189798514546)], [28141368776316848085240, (-7871788917668671940)], [28505609374321942489598]]], r := 213308980951803295238184, ok := true }, eta := { p := [[[(-854771734848144951956310322)]], [[19525412364093191225218990, 0], [58458423102939485695477593]], [[(-365128743280616144277818), 0, 0], [(-1323474633851964277646987), 0], [(-3008714768244129022812080)]], [[6612964402538930316056, 0, 0, 0], [24515065150296710496634, 0, 0], [67743230925169775118117, 0], [137850694880517067108969]], [[(-121574223922784809440), 0, 0, 0, 0], [(-440105470165689302225), 0, 0, 0], [(-1247439956481097937834), 0, 0], [(-3091679142680080959136), 0], [(-5926081218336852891707)]]], r := 1537991679903427582786, ok := true } }
theorem sB_1 : stageB c1 w1 = true := by decide +kernel
theorem s0_1 : stageC0 w1 q1 = true := by decide +kernel
theorem s1_1 : stageC1 w1 q1 = true := by decide +kernel
theorem s2_1 : stageC2 w1 q1 = true := by decide +kernel
theorem s3_1 : stageC3 w1 q1 = true := by decide +kernel
theorem sE_1 : stageE w1 q1 = true := by decide +kernel
theorem sF_1 : stageF w1 = true := by decide +kernel
theorem ok_1 : (domOK c1 && cellCheck c1 q1) = true :=
  staged_check c1 q1 w1 (by decide +kernel) sB_1 s0_1 s1_1 s2_1 s3_1 sE_1 sF_1

noncomputable def c2 : Cell := { bc := 2181431069507584, bh := 70368744177664, tc := 16140901064495857664, th := 2305843009213693952, sc := 12970366926827028480, sh := 288230376151711744 }
noncomputable def q2 : Cert := { V0 := [[[382723882172705227]], [[(-23366694177582001), 54640891761943369], [1211118865147480]], [[200180487195617, (-3331881811025566), (-7269362521986)], [(-72985927703693), 172694728963682], [(-15701800609220)]], [[(-1917039274016), 28164462124354, 1330665110140, (-344892921732)], [576301607880, (-10367802821683), (-68969688475)], [949420531940, (-2239955945852)], [308598816552]], [[19687575516, (-259136191042), (-92519832572), 62978356386, 135521637], [(-5712603890), 78268258197, 12565409674, (-3264230489)], [(-7664576796), 135053921420, 676246459], [(-18679085460), 44028794107], [(-7056520274)]]], r0 := 2073861587496, V1 := [[[437357159818560377]], [[(-26697182387625331), 0], [1383741362394208]], [[228248079805800, 0, 0], [(-83340573529791), 0], [(-17941048254133)]], [[(-2172890011742), 0, 0, 0], [653662693681, 0, 0], [1084345016028, 0], [352614882856]], [[22141984639, 0, 0, 0, 0], [(-6361825845), 0, 0, 0], [(-8710436319), 0, 0], [(-21334814683), 0], [(-8063090596)]]], r1 := 576424923461, V2 := [[[18443034968980146570]], [[(-34787100590209), 18045083384], [(-119627552281785)]], [[23427124870, (-778705444), (-83956)], [(-1124578477714), 1170285009], [404135837]], [[(-225495329), (-9106838), 8036, 0], [835410531, (-50477118), (-8172)], [(-46952131), 19093099], [(-3485121)]], [[2776674, 6594, (-148), 0, 0], [(-7969194), (-592229), 782, 0], [1558380, (-822635), (-266)], [394313, 2868], [50535]]], r2 := 3755077532, V3 := [[[18443676406478356979]], [[(-68168821791235), 29789976446], [(-98957978251271)]], [[35106464, (-899153765), (-276852)], [(-2198964993755), 1931778372], [(-31508236)]], [[5299, (-35106355), 22888, 2], [2278180, (-58264024), (-26942)], [948678, 31509113], [(-4613)]], [[(-33), (-5282), (-110), (-1), 0], [380, (-2278170), 2226, 0], [37220, (-948750), (-877)], [116, 4622], [28]]], r3 := 11585368727, Vm := [[[18443034988399270267]], [[(-34788023004564), 0], [(-119626288068282)]], [[23421745116, 0, 0], [(-1124638771850), 0], [424934418]], [[(-225488520), 0, 0, 0], [835072305, 0, 0], [(-47952757), 0], [(-3479694)]], [[2776706, 0, 0, 0, 0], [(-7968706), 0, 0, 0], [1553241, 0, 0], [393938, 0], [50503]]], rm := 375835852 }
noncomputable def w2 : Wit := { Z0 := { p := [[[382842767383899840]], [[(-23388474861159249), 54691823911985691], [1212247779514903]], [[201697718544316, (-3341210694451322), 0], [(-73191896298247), 173178254216414], [(-15712861958105)]], [[(-1968774268603), 28813959792045, 0, 0], [590554488179, (-10455985185464), 0], [951444168087, (-2244694565444)], [308797559830]], [[20722838341, (-281253466944), 0, 0, 0], [(-6193481761), 84364926882, 0, 0], [(-7805221931), 135920595441, 0], [(-18715464989), 44113937118], [(-7060822295)]]], r := 507228031501, ok := true }, Z1 := { p := [[[437534591295885532]], [[(-26729685555610570), 0], [1385426033731318]], [[230511678336362, 0, 0], [(-83647881483711), 0], [(-17957556523549)]], [[(-2250027735546), 0, 0, 0], [674919415062, 0, 0], [1087364763528, 0], [352911496948]], [[23683243819, 0, 0, 0, 0], [(-7078264870), 0, 0, 0], [(-8920253636), 0, 0], [(-21389102845), 0], [(-8069511194)]]], r := 144202178920, ok := true }, Z2 := { p := [[[12460274537817518724519]], [[(-105434258151804617777), 54691823911985691], [(-362572390781433832076)]], [[1016657703910022704, (-3341210694451322), 0], [3095497714651546752, 173178254216414], [11184219557051860057]], [[(-10579450986904913), 28813959792045, 0, 0], [(-29659427200287785), (-10455985185464), 0], [(-95803481683733807), (-2244694565444)], [(-350727534157886100)]], [[117750728659827, (-281253466944), 0, 0, 0], [304798779892708, 84364926882, 0, 0], [915893384581009, 135920595441, 0], [3010257105470115, 44113937118], [11083918119136631]]], r := 1789996273361560, ok := true }, Z3 := { p := [[[14790980968274176988991]], [[(-297114641567229777920), 129839975836718020], [(-431309555684948916850)]], [[6318712144910712053, (-9441430658007297), 0], [8760588240876094529, 402946079717683], [13315075310198326658]], [[(-136567630512303733), 192709128425026, 0, 0], [(-187077181915720752), (-28438755392559), 0], [(-271563258308930587), (-5248355070751)], [(-417747092103758899)]], [[2974166386153092, (-4117562923281), 0, 0, 0], [4053261150798814, 527656848437, 0, 0], [5808267390233312, 373094162732, 0], [8540935452662783, 103304061852], [13206314707308550]]], r := 8661094500324859, ok := true }, iE := { p := [[[12462839296507286053528]], [[(-105435806429257507163), 0], [(-362564269632775578096)]], [[1016696466323741846, 0, 0], [3095498615369310996, 0], [11184114292690922678]], [[(-10579984497788223), 0, 0, 0], [(-29659275728113121), 0, 0], [(-95803474945436831), 0], [(-350725465446413855)]], [[117757856877113, 0, 0, 0, 0], [304796342256551, 0, 0, 0], [915891526118718, 0, 0], [3010256857980789, 0], [11083870816936149]]], r := 1789815092570413, ok := true }, iHu := { p := [[[14793570934107972574770]], [[(-297118823491163049158), 0], [(-431301517971042969376)]], [[6318857661812489031, 0, 0], [8760592453937683570, 0], [13314970619326125892]], [[(-136571108172681168), 0, 0, 0], [(-187076912246278698), 0, 0], [(-271563259712615868), 0], [(-417745031459577736)]], [[2974245488665882, 0, 0, 0, 0], [4053253663575832, 0, 0, 0], [5808263427375095, 0, 0], [8540935141139863, 0], [13206267546183560]]], r := 8660511191657088, ok := true }, T := { p := [[[16140901064495857664]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[27303759506575896]], [[230990212874936, 0], [794310781693618]], [[(-273211934692), 0, 0], [6658101250083, 0], [(-1394518383975)]], [[2023623820, 0, 0, 0], [(-8814021088), 0, 0], [(-12794546741), 0], [14993265273]], [[(-22484709), 0, 0, 0, 0], [65278188, 0, 0, 0], [(-23643), 0, 0], [137552892, 0], [(-241826861)]]], r := 153010035, ok := true }, de := { p := [[[(-125012022428669781667)]], [[295724880137329571, 0], [429278051812252602]], [[(-3285558766872144), 0, 0], [793261897954, 0], [(-6923263790755560)]], [[48674945031009, 0, 0, 0], [1465867, 0, 0], [2127871, 0], [148887394379197]], [[(-811249083849), 0, 0, 0, 0], [3, 0, 0, 0], [23649, 0, 0], [6, 0], [(-3602114380139)]]], r := 554031837894, ok := true }, dde := { p := [[[(-160046457762518963143923)]], [[3556292200806943023385, 0], [5162359646332659218218]], [[(-79028716120002355623), 0, 0], [(-114719104838492595223), 0], [(-166527731678464929307)]], [[1756193691554614298, 0, 0, 0], [2549313423221498946, 0, 0], [3700616259515071069, 0], [5371862312205464098]], [[(-39026526478979905), 0, 0, 0, 0], [(-56651409404985576), 0, 0, 0], [(-82235916878245843), 0, 0], [(-119374718049004305), 0], [(-173285881038880060)]]], r := 16606762040315304, ok := true }, nJu := { p := [[[(-250024044857339563333)]], [[591449760274659143, 0], [858556103624505205]], [[(-6571117533744288), 0, 0], [1586523795909, 0], [(-13846527581511119)]], [[97349890062018, 0, 0, 0], [2931734, 0, 0], [4255743, 0], [297774788758394]], [[(-1622498167698), 0, 0, 0, 0], [6, 0, 0, 0], [47299, 0, 0], [12, 0], [(-7204228760278)]]], r := 1108063675780, ok := true }, Jd1 := { p := [[[(-320092915525037926287846)]], [[7112584401613886046770, 0], [10324719292665318436436]], [[(-158057432240004711246), 0, 0], [(-229438209676985190446), 0], [(-333055463356929858613)]], [[3512387383109228597, 0, 0, 0], [5098626846442997893, 0, 0], [7401232519030142138, 0], [10743724624410928196]], [[(-78053052957959810), 0, 0, 0, 0], [(-113302818809971152), 0, 0, 0], [(-164471833756491686), 0, 0], [(-238749436098008610), 0], [(-346571762077760120)]]], r := 33213524080630604, ok := true }, term0 := { p := [[[1925374956582687410009688288]], [[(-85561548458438332936625697), 0], [(-124194905739641075189620795)]], [[2851933072212835850794359, 0, 0], [5519429431130760274784998, 0], [6009062711577671201849644]], [[(-84499964464466918786926), 0, 0, 0], [(-183977157067372338654955), 0, 0], [(-267058351999118178328901), 0], [(-258446391652419931926832)]], [[2347191965228951033910, 0, 0, 0, 0], [5451118372809009865139, 0, 0, 0], [8901821712761760262528, 0, 0], [11486148171508825564968, 0], [10421033892687022987944]]], r := 1803722847589772164259, ok := true }, r0 := { p := [[[74313193820278668029179]], [[(-1949210997674668152112), 21211104212772271827530], [(-2167222406472935081869)]], [[38106551520833674495, (-553772103190526431341), 1509017903234446410189], [57174739231052628204, (-618721298677844624469)], [66911975200396061040]], [[(-667465270021072507), 10708210163684517978, (-38658298588409453083), (-863937526024637466)], [(-1110744889978064161), 16263571921722043371, (-44055888413910326882)], [(-1768869653464155749), 19104029046240578920], [(-2099416484159422354)]], [[11271601918366062, (-185027294202317132), 713831725784739881, 127604607164455039, (-30513507956780594)], [19230629851704853, (-313227587870485879), 1141122938267714978, 19752646590069366], [34283760255895698, (-503357651019774608), 1360668328681878369], [55567461692367391, (-599427491970486810)], [66371810282509677]]], r := 360008921796773515, ok := true }, r1 := { p := [[[97032421515073437496971]], [[(-2541509337664690587201), 0], [(-2829979141605786829752)]], [[49521115024054040387, 0, 0], [74576402481492016073, 0], [87376095776358402733]], [[(-863867641605574681), 0, 0, 0], [(-1444997147279944262), 0, 0], [(-2307515565978656369), 0], [(-2741527252508822483)]], [[14530885188237931, 0, 0, 0, 0], [24934297382687247, 0, 0, 0], [44615721322200526, 0, 0], [72493471338435078, 0], [86672470918835801]]], r := 54326092916590588, ok := true }, r2 := { p := [[[784212107110384975490444583]], [[(-18475550059825936620375919), 36788372892087626416285], [(-50153177466257048283934606)]], [[358123585689258924197621, (-618492148697732431900), 454244406560026613], [1170637204948793708861868, (-1185049358017175121724)], [2414074409216465136361955]], [[(-6754104979376286342097), 10015266984746797755, 94870498014192, (-37045336050664)], [(-22470281722294356987473), 19594255746345499274, 94262234104462], [(-56025912607128798876885), 38203575890818473988], [(-103449308954444856627967)]], [[129742187397839456823, (-166044538610615562), (-6149966423892), 1377530079345, (-3902017884397)], [420021353063021146664, (-311119058692688976), (-23386477561274), 3554002475692], [1068881727114420561780, (-627483681074454468), (-8477166554042)], [2391070041934861867869, (-1231894458200741666)], [4159624121832815522601]]], r := 10649245804301674340607, ok := true }, r3 := { p := [[[3849782855908053095865618756]], [[(-171088976743903811003601332), 191730515463800773010112], [(-248358604505168864247208430)]], [[5702827261126889198316387, (-6776238915375394105657), 1806422754731616941], [11037757859314892632897991, (-6198210276544921771814)], [12017118588443666876639298]], [[(-168970605791987157079808), 206447305456597753439, 1152216388897430, (-279797818655653)], [(-367920792430981254259306), 218940087901045453477, 347359598393330], [(-534081183660842039835809), 200100195538640450801], [(-516860301940213257853815)]], [[4693593484830320192120, (-5829379204071276370), (-139898460578043), 19190707539453, (-30310433989974)], [10901290541680758842246, (-6669175286953492330), (-100668867706518), (-239928994633565)], [17802561737215055396105, (-7066956623647109511), (-181910159269348)], [22971150348632550863432, (-6457829653209107784)], [20841019829630522883781]]], r := 178287798278051809274051, ok := true }, eta := { p := [[[(-784458811421762521753166494)]], [[18482710158016275169072984, 0], [50161051602913352881071414]], [[(-358296844805654148497633), 0, 0], [(-1170865623239011658291137), 0], [(-2414327370707250562996819)]], [[6758072060309060329678, 0, 0, 0], [22475801694649586379050, 0, 0], [56033248222190427026743, 0], [103457448707943770735117]], [[(-129831266317128191947), 0, 0, 0, 0], [(-420147634233161825092), 0, 0, 0], [(-1069058935589821430252), 0, 0], [(-2391306046408422067108), 0], [(-4159886258392003441337)]]], r := 1102632055161488997237, ok := true } }
theorem sB_2 : stageB c2 w2 = true := by decide +kernel
theorem s0_2 : stageC0 w2 q2 = true := by decide +kernel
theorem s1_2 : stageC1 w2 q2 = true := by decide +kernel
theorem s2_2 : stageC2 w2 q2 = true := by decide +kernel
theorem s3_2 : stageC3 w2 q2 = true := by decide +kernel
theorem sE_2 : stageE w2 q2 = true := by decide +kernel
theorem sF_2 : stageF w2 = true := by decide +kernel
theorem ok_2 : (domOK c2 && cellCheck c2 q2) = true :=
  staged_check c2 q2 w2 (by decide +kernel) sB_2 s0_2 s1_2 s2_2 s3_2 sE_2 sF_2

noncomputable def c3 : Cell := { bc := 2181431069507584, bh := 70368744177664, tc := 16140901064495857664, th := 2305843009213693952, sc := 13546827679130451968, sh := 288230376151711744 }
noncomputable def q3 : Cert := { V0 := [[[336776187690891880]], [[(-22588363526068022), 48087752390708850], [1067407509501745]], [[189134040592120, (-3222255012527020), (-4953953633923)], [(-70747296009730), 152266860497957], [(-13833026618316)]], [[(-1767799808614), 26668088301460, 996356781427, (-235233837716)], [543493751322, (-10062684320330), (-47082592302)], [919642744210, (-1973993433800)], [271836199717]], [[17669096650, (-239980711519), (-75092945506), 47221383003, 71546169], [(-5232942213), 74339741678, 9429158244, (-2231434730)], [(-7230575089), 130944889819, 461110683], [(-18089249743), 38795061572], [(-6215433340)]]], r0 := 1921345074342, V1 := [[[384858750967703828]], [[(-25809574985079372), 0], [1219625057137446]], [[215723495530142, 0, 0], [(-80800106095800), 0], [(-15806537061681)]], [[(-2004974435317), 0, 0, 0], [617094951893, 0, 0], [1050490639476, 0], [310622584202]], [[19888815087, 0, 0, 0, 0], [(-5837738009), 0, 0, 0], [(-8223661292), 0, 0], [(-20663908436), 0], [(-7102327361)]]], r1 := 523989421688, V2 := [[[18442965486726723185]], [[(-34696012179875), 16451296810], [(-121873429822564)]], [[22137820632, (-815055826), (-68492)], [(-1121329434452), 1066965369], [316361059]], [[(-204746536), (-9068877), 7418, 0], [789843415, (-52840804), (-6667)], [(-40873437), 17409010], [(-2747089)]], [[2421101, 6070, (-161), 0, 0], [(-7236580), (-589650), 722, 0], [1482178, (-861424), (-217)], [344154, 2637], [39822]]], r2 := 3735248395, V3 := [[[18443540068975242252]], [[(-68168681302802), 27851201752], [(-103355899123056)]], [[35137504, (-1039641553), (-231654)], [(-2198955876546), 1806134655], [(-29461941)]], [[5051, (-35137292), 22242, 2], [2280407, (-67381171), (-22544)], [1097646, 29462674], [(-4355)]], [[(-30), (-5034), (-213), 0, 0], [362, (-2280387), 2164, 0], [37264, (-1097717), (-734)], [141, 4363], [26]]], r3 := 11071000780, Vm := [[[18442965504279554107]], [[(-34696956030597), 0], [(-121872287546298)]], [[22132482416, 0, 0], [(-1121391075569), 0], [335137914]], [[(-204739513), 0, 0, 0], [789508163, 0, 0], [(-41894498), 0], [(-2742395)]], [[2421123, 0, 0, 0, 0], [(-7236079), 0, 0, 0], [1477099, 0, 0], [343796, 0], [39794]]], rm := 375082234 }
noncomputable def w3 : Wit := { Z0 := { p := [[[336857182612829337]], [[(-22604664297300164), 48122454658975619], [1068177798398672]], [[190364398404833, (-3229237756757167), 0], [(-70901731549863), 152596828342667], [(-13840566522780)]], [[(-1811898059342), 27194914057833, 0, 0], [555077484274, (-10128818792838), 0], [921158215182, (-1977223788969)], [271971644361]], [[18547715071, (-258842579906), 0, 0, 0], [(-5643699065), 79296783467, 0, 0], [(-7344714654), 131594030740, 0], [(-18116487060), 38853092051], [(-6218364831)]]], r := 471126157829, ok := true }, Z1 := { p := [[[384979637271804956]], [[(-25833902054057331), 0], [1220774626741340]], [[217559312462667, 0, 0], [(-81030550342700), 0], [(-15817790311749)]], [[(-2070740639248), 0, 0, 0], [634374267742, 0, 0], [1052752245922, 0], [310824736413]], [[21197388653, 0, 0, 0, 0], [(-6449941788), 0, 0, 0], [(-8393959605), 0, 0], [(-20704556640), 0], [(-7106702664)]]], r := 131055399127, ok := true }, Z2 := { p := [[[12253389857011887868079]], [[(-101490921487267847754), 48122454658975619], [(-356497646858688390452)]], [[955899057251761817, (-3229237756757167), 0], [2980413809230536966, 152596828342667], [10996202813621532466]], [[(-9690762196578606), 27194914057833, 0, 0], [(-27907735692892367), (-10128818792838), 0], [(-92249159352507255), (-1977223788969)], [(-344819686388210834)]], [[104746436863287, (-258842579906), 0, 0, 0], [279581482785476, 79296783467, 0, 0], [862038181237000, 131594030740, 0], [2898714138132967, 38853092051], [10896952074441718]]], r := 1713743385745182, ok := true }, Z3 := { p := [[[14220979585017141237746]], [[(-273388375127450296356), 111696377966952395], [(-414505617258106097973)]], [[5565804428986074806, (-8717298590576766), 0], [8058236249437477287, 348096045567596], [12794216298426411259]], [[(-115164629690284220), 169998377553614, 0, 0], [(-164734467063758177), (-26451171416175), 0], [(-249758345325562888), (-4529385028318)], [(-401366212638748022)]], [[2401160535270088, (-3475504362093), 0, 0, 0], [3417022465518824, 467783360448, 0, 0], [5113955851696224, 346415625925, 0], [7854514991815420, 89123677582], [12687584733291472]]], r := 7594422090704601, ok := true }, iE := { p := [[[12255951670039321570181]], [[(-101492320896668947991), 0], [(-356489523321650148446)]], [[955934782164934689, 0, 0], [2980415287691073602, 0], [10996097555531590320]], [[(-9691242386180791), 0, 0, 0], [(-27907598027126183), 0, 0], [(-92249159708898132), 0], [(-344817618032428084)]], [[104752664329751, 0, 0, 0, 0], [279579311819931, 0, 0, 0], [862036489186652, 0, 0], [2898714027806925, 0], [10896904783515904]]], r := 1713579417145529, ok := true }, iHu := { p := [[[14223561742460730196069]], [[(-273392014319023181287), 0], [(-414497570096582094119)]], [[5565930845496171771, 0, 0], [8058241456700796131, 0], [12794111589701933102]], [[(-115167539576244809), 0, 0, 0], [(-164734238362342780), 0, 0], [(-249758361389015097), 0], [(-401364152309025080)]], [[2401224055292981, 0, 0, 0, 0], [3417016249530850, 0, 0, 0], [5113952466942220, 0, 0], [7854514981087561, 0], [12687537588380508]]], r := 7593935611503492, ok := true }, T := { p := [[[16140901064495857664]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[27764662923140159]], [[229920952272664, 0], [807592239030490]], [[(-261586861690), 0, 0], [6623606041089, 0], [(-1420107572030)]], [[1855064840, 0, 0, 0], [(-8439018739), 0, 0], [(-12794641313), 0], [15268371056]], [[(-19734732), 0, 0, 0, 0], [59840801, 0, 0, 0], [(-23643), 0, 0], [137552892, 0], [(-246264050)]]], r := 153360229, ok := true }, de := { p := [[[(-124433338038843299183)]], [[283141889119133445, 0], [429279638341911997]], [[(-3011886147005621), 0, 0], [793267761453, 0], [(-6923263786405222)]], [[42721789641515, 0, 0, 0], [1465883, 0, 0], [2222468, 0], [148887394379209]], [[(-681730685768), 0, 0, 0, 0], [3, 0, 0, 0], [23650, 0, 0], [6, 0], [(-3602114380139)]]], r := 539562850266, ok := true }, dde := { p := [[[(-153236536529024242876759)]], [[3260068674562649262267, 0], [4942684764659500491620]], [[(-69363163811831596372), 0, 0], [(-105163507217726510210), 0], [(-159441445224074934542)]], [[1475811995995456146, 0, 0, 0], [2237521413280494255, 0, 0], [3392371174973658020, 0], [5143272426579704539]], [[(-31400255233936270), 0, 0, 0, 0], [(-47606838580496423), 0, 0, 0], [(-72178110105954162), 0, 0], [(-109431328225092922), 0], [(-165912013760630002)]]], r := 14927092109233231, ok := true }, nJu := { p := [[[(-248866676077686598365)]], [[566283778238266891, 0], [858559276683823994]], [[(-6023772294011242), 0, 0], [1586535522907, 0], [(-13846527572810443)]], [[85443579283030, 0, 0, 0], [2931767, 0, 0], [4444937, 0], [297774788758419]], [[(-1363461371536), 0, 0, 0, 0], [6, 0, 0, 0], [47301, 0, 0], [13, 0], [(-7204228760278)]]], r := 1079125700522, ok := true }, Jd1 := { p := [[[(-306473073058048485753517)]], [[6520137349125298524534, 0], [9885369529319000983240]], [[(-138726327623663192744), 0, 0], [(-210327014435453020420), 0], [(-318882890448149869084)]], [[2951623991990912292, 0, 0, 0], [4475042826560988510, 0, 0], [6784742349947316041, 0], [10286544853159409078]], [[(-62800510467872540), 0, 0, 0, 0], [(-95213677160992845), 0, 0, 0], [(-144356220211908323), 0, 0], [(-218862656450185843), 0], [(-331824027521260004)]]], r := 29854184218466457, ok := true }, term0 := { p := [[[1765019243220628697452481870]], [[(-75097418801455801309399128), 0], [(-113850646428169375806489243)]], [[2396622087221131671308724, 0, 0], [4844392868140731767473868, 0], [5508554528489061646977648]], [[(-67987803258107156233961), 0, 0, 0], [(-154604926743470857753142), 0, 0], [(-234396398566860790177960), 0], [(-236919598686724714462254)]], [[1808162706672907497667, 0, 0, 0, 0], [4385907761770481081069, 0, 0, 0], [7480627857308890184132, 0, 0], [10081356756514088855220, 0], [9553028709768726882273]]], r := 1537677802078597425585, ok := true }, r0 := { p := [[[70562032754906132148486]], [[(-1804448333895068106230), 20144960362206484444182], [(-2057167015737844914512)]], [[34357774245908009717, (-513064895113919509750), 1434466584190834302992], [52952700449335789733, (-587405525591485482426)], [63506794938742763006]], [[(-584424607372545849), 9668115328909066021, (-35936679941742091576), (-635931038229181081)], [(-1002632963646735857), 15072309486599103778, (-41855749444213252032)], [(-1638525355403937505), 18134749574684080868], [(-1992440280059142256)]], [[9547075735724550, (-162293249131625242), 648321553001272209, 101224415821153651, (-22517221410758575)], [16870881727967158, (-283054573714576327), 1060316811662445468, 14523161171849376], [30960470277384683, (-466541112854430325), 1292469749305808086], [51478045628714245, (-568970571158141987)], [62986804077775454]]], r := 321235639479803640, ok := true }, r1 := { p := [[[92140801270059902988957]], [[(-2353345131432210071296), 0], [(-2686413252420018965750)]], [[44668007548873929764, 0, 0], [69082924973565651265, 0], [82933590265715496995]], [[(-756788152987210767), 0, 0, 0], [(-1304790102627596739), 0, 0], [(-2137863824377269594), 0], [(-2601953908255588384)]], [[12314065199902059, 0, 0, 0, 0], [21884147214883486, 0, 0, 0], [40303393219842148, 0, 0], [67169831120271962, 0], [82255815141454011]]], r := 47708862536859189, ok := true }, r2 := { p := [[[748641465415541755354776788]], [[(-17120149068219097367643483), 35590166144749328447762], [(-47898547335906196285368914)]], [[320519208572975353406636, (-580334968867739180105), 454493149966516036], [1085552018100964232036700, (-1147066081455387416175)], [2306144973676354846615048]], [[(-5811081099062707947532), 9084375860956830571, 113946136651862, (-34342869264424)], [(-20130522481458351357469), 18407874566269935134, 87713499860628], [(-51977297110787652422411), 36986937131937721625], [(-98842360027642761527668)]], [[106921102868697707361, (-144924183604672284), (-16923943679663), 1162642357259, (-3676761125477)], [361766181414390967815, (-282743985198000946), (-13195808439750), 3306547839911], [958167925040578496218, (-589766966979200901), (-6145776498807)], [2219001658574112510196, (-1192802453395923639)], [3974941850010718608305]]], r := 9864412995874903464270, ok := true }, r3 := { p := [[[3529135736567477377531825184]], [[(-150164544816347718062309274), 178959583195680695565939], [(-227672160982403745419588698)]], [[4792363797811177738410600, (-6015680741291122180498), 1808948811456203744], [9687808232247581186453660, (-5785576181862317868281)], [11016169168878431095854527]], [[(-135951857165805323217364), 174938472485681351276, 1115001689292508, (-240152531520543)], [(-309181446420715860636093), 194371466689451004281, 280199348456718], [(-468761261031420841905414), 186781529799344577458], [(-473808875674602915313281)]], [[3615713260687783553109, (-4720997014752549970), (-225535563535665), 17304112863818, (-26023300829200)], [8771049042884652756289, (-5651306241000336624), (-2821688904357), (-204297522153883)], [14960339145285255754715, (-6273870434036948498), (-71838156142556)], [20161695941631213669647, (-6028059781961566623)], [19105079066748942040301]]], r := 149104044872771849638938, ok := true }, eta := { p := [[[(-748874512194322312347824933)]], [[17126661035907263170373809, 0], [47905985749217522827831371]], [[(-320670653801698646810249), 0, 0], [(-1085759785782467077566708), 0], [(-2306383941618141245190447)]], [[5814408512755863662933, 0, 0, 0], [20135348116900298018513, 0, 0], [51983969850552538210320, 0], [98850049586844308156296]], [[(-106992724593825001610), 0, 0, 0, 0], [(-361872107945862940005), 0, 0, 0], [(-958322857723291923625), 0, 0], [(-2219216357321654099507), 0], [(-3975189467643021583830)]]], r := 1028528063053550821174, ok := true } }
theorem sB_3 : stageB c3 w3 = true := by decide +kernel
theorem s0_3 : stageC0 w3 q3 = true := by decide +kernel
theorem s1_3 : stageC1 w3 q3 = true := by decide +kernel
theorem s2_3 : stageC2 w3 q3 = true := by decide +kernel
theorem s3_3 : stageC3 w3 q3 = true := by decide +kernel
theorem sE_3 : stageE w3 q3 = true := by decide +kernel
theorem sF_3 : stageF w3 = true := by decide +kernel
theorem ok_3 : (domOK c3 && cellCheck c3 q3) = true :=
  staged_check c3 q3 w3 (by decide +kernel) sB_3 s0_3 s1_3 s2_3 s3_3 sE_3 sF_3

theorem region : RegionPosI 1970324836974592 2251799813685248 13835058055282163712 18446744073709551616 12682136550675316736 13835058055282163712 :=
  (RegionPosI.split_b 2111062325329920 (RegionPosI.split_s 13258597302978740224 (RegionPosI.of_check c0 q0 ok_0 1970324836974592 2111062325329920 13835058055282163712 18446744073709551616 12682136550675316736 13258597302978740224 (by decide +kernel)) (RegionPosI.of_check c1 q1 ok_1 1970324836974592 2111062325329920 13835058055282163712 18446744073709551616 13258597302978740224 13835058055282163712 (by decide +kernel))) (RegionPosI.split_s 13258597302978740224 (RegionPosI.of_check c2 q2 ok_2 2111062325329920 2251799813685248 13835058055282163712 18446744073709551616 12682136550675316736 13258597302978740224 (by decide +kernel)) (RegionPosI.of_check c3 q3 ok_3 2111062325329920 2251799813685248 13835058055282163712 18446744073709551616 13258597302978740224 13835058055282163712 (by decide +kernel))))

end CKLaneC.RSC2.S01_0277

end