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

import Definitions.Def_CK_CKLaneC_RSCell_Staged
import Definitions.Def_CK_CKLaneC_RSCell_RegionI

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

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

namespace CKLaneC.RSC2.BD_0045
open CKLaneC.TM3 CKLaneC.RSCell

noncomputable def c0 : Cell := { bc := 8214565720323784704, bh := 144115188075855872, tc := 5764607523034234880, th := 1152921504606846976, sc := 18068441705010429952, sh := 126100789566373888 }
noncomputable def q0 : Cert := { V0 := [[[53187637749958359]], [[(-17759287460404678), 10637399966114662], [790458761241171]], [[10736700568499, (-3551729692052375), (-38274621732)], [(-260705401133444), 158086063920225], [7283632372251]], [[(-238404124998), 2104590805408, 38339104753, (-2551460996)], [(-900302515976), (-52135405497863), (-1706458175)], [(-2340792796804), 1456589521934], [108586862689]], [[400209436, (-42878233978), (-12824188380), 2555639050, 27066], [(-8806304384), (-181943333174), 1702351651, (-113750471)], [(-28180124798), (-468022722059), (-41084189)], [(-34527447448), 21714614401], [1225666549]]], r0 := 126192311852, V1 := [[[170191010723991197]], [[(-56820274438241114), 0], [2529047623446266]], [[31198444242903, 0, 0], [(-833837922045859), 0], [23297502735466]], [[(-408230913653), 0, 0, 0], [(-3020070683927), 0, 0], [(-7480500295718), 0], [347274156623]], [[617828655, 0, 0, 0, 0], [(-12943618090), 0, 0, 0], [(-93466582239), 0, 0], [(-110286945901), 0], [3918379684]]], r1 := 34817188916, V2 := [[[2072538334568243786]], [[(-18408000164416002), 10349504719160111], [(-287868695078985678)]], [[33912498304585, (-3450655205317563), (-1426166438759)], [(-110282040709019), 233149961074301], [28490033036797]], [[(-258359931995), 384912704444, 963929762716, (-2160432157)], [(-3410686115256), (-77796949618347), 137884494731], [(-9082788081272), (-2729818883603)], [789273410761]], [[784258074, (-37165060740), (-167291139190), 2157513476, 929008], [(-4978218971), 35150055974, (-91377929913), (-199684797)], [(-136997434771), 918479990798, 8256442508], [(-258992393148), (-72710766653)], [(-1931749591)]]], r2 := 882116503612, V3 := [[[2127557820743529648]], [[(-36882442451502660), 20701105070915387], [(-287515887097211730)]], [[80870450407852, (-6903099451163345), (-5860517376172)], [(-214778509568505), 466609088986832], [56675152632464]], [[(-960500396781), 1262695508434, 4012344917648, (-17205433496)], [(-7721413573170), (-155843237408643), 544872413922], [(-17966095862559), (-5513062176126)], [1575826647417]], [[3038474894, (-117025923544), (-721903465690), 17155630073, 15250182], [(-23930714995), 133633180769, (-358875800007), (-1604772827)], [(-305432442788), 1872635975435, 32927144586], [(-516420292659), (-145042639969)], [(-4057110028)]]], r3 := 2287830824492, Vm := [[[2192618160010095535]], [[(-60345215216336239), 0], [(-284210611014761910)]], [[616722375236648, 0, 0], [(-1639948208801772), 0], [140763482882549]], [[16589407160278, 0, 0, 0], [83527749796977, 0, 0], [(-82207384813447), 0], [18272939613372]], [[374748121439, 0, 0, 0, 0], [4939030592218, 0, 0, 0], [8405936098276, 0, 0], [(-10065260356744), 0], [2364402884578]]], rm := 116520183701027 }
noncomputable def w0 : Wit := { Z0 := { p := [[[53187956713034501]], [[(-17759606966125024), 10637591342606900], [790472982312625]], [[10843577615004, (-3551921393225005), 0], [(-260719588374251), 158094596462525], [7283974763328]], [[(-250411866786), 2168715523000, 0, 0], [(-895595162167), (-52143917674851), 0], [(-2341132406315), 1456794952665], [108593758312]], [[424803028, (-50082373358), 0, 0, 0], [(-9322559783), (-179119032434), 0, 0], [(-28068739385), (-468226481263), 0], [(-34534246278), 21718751662], [1225793559]]], r := 27656644877, ok := true }, Z1 := { p := [[[170201461481710406]], [[(-56830742291600077), 0], [2529513543400400]], [[34699448368014, 0, 0], [(-834302682797603), 0], [23308719242651]], [[(-801317973714), 0, 0, 0], [(-2865904518932), 0, 0], [(-7491623700206), 0], [347500026599]], [[1359369691, 0, 0, 0, 0], [(-29832191303), 0, 0, 0], [(-89819966030), 0, 0], [(-110509588090), 0], [3922539390]]], r := 8067960449, ok := true }, Z2 := { p := [[[2091624173757145097]], [[(-18920401361930009), 10637591342606900], [(-295881747163285612)]], [[39493809760093, (-3551921393225005), 0], [31687526193432, 158094596462525], [1163363076882116]], [[(-297405889565), 2168715523000, 0, 0], [(-4410093386286), (-52143917674851), 0], [(-19315695210300), 1456794952665], [(-55891538047960)]], [[1040766944, (-50082373358), 0, 0, 0], [1269439987, (-179119032434), 0, 0], [(-86951673664), (-468226481263), 0], [(-148530214379), 21718751662], [436109868873]]], r := 62909482036, ok := true }, Z3 := { p := [[[2148216993019682261]], [[(-37965430791359337), 21308956772803855], [(-295958287669225458)]], [[102394546000406, (-7127293032495809), 0], [77473143656758, 312737678004395], [1222039901952970]], [[(-1192162121771), 8716312327411, 0, 0], [(-11174000012882), (-102012703638019), 0], [(-38596396538312), 2806877941358], [(-55438291895646)]], [[5121888152, (-206288057981), 0, 0, 0], [4541096487, (-724739691947), 0, 0], [(-173380970730), (-866624018085), 0], [(-281292246911), 41404196044], [455268829203]]], r := 129971917609, ok := true }, iE := { p := [[[18637131127260439735]], [[(-10612977333074143), 0], [(-49984423151121058)]], [[261944979612240, 0, 0], [1157296857036795, 0], [3429234197783051]], [[(-429659636836), 0, 0, 0], [5288156181225, 0, 0], [10132119654536, 0], [(-22110605402624)]], [[5631670092, 0, 0, 0, 0], [35461192629, 0, 0, 0], [217092626766, 0, 0], [405196813728, 0], [817425059638]]], r := 98186687623, ok := true }, iHu := { p := [[[18666717340851775849]], [[(-21293400035476992), 0], [(-53527018134294289)]], [[537718714179191, 0, 0], [2329849474674487, 0], [3397904949923022]], [[(-1469456748486), 0, 0, 0], [7785630682505, 0, 0], [19571397429959, 0], [(-23342153447515)]], [[20212663798, 0, 0, 0, 0], [125901291838, 0, 0, 0], [543028072587, 0, 0], [795584404011, 0], [807115526077]]], r := 161031000396, ok := true }, T := { p := [[[5764607523034234880]], [[0, 1152921504606846976], [0]]], r := 0, ok := true }, E := { p := [[[18258301913388865119]], [[10397251756402927, 0], [48968410568558584]], [[(-250699782779637), 0, 0], [(-1078002511180783), 0], [(-3228197255742977)]], [[132030855025, 0, 0, 0], [(-7800792271047), 0, 0], [(-19609510395640), 0], [3993017092686]], [[(-1678727442), 0, 0, 0, 0], [(-9930843463), 0, 0, 0], [(-105874002353), 0, 0], [(-62754115246), 0], [(-138016909739)]]], r := 71851419984, ok := true }, de := { p := [[[(-3415510231115900672)]], [[164710385606479533, 0], [414046407928067597]], [[(-130116903982676), 0, 0], [2235484185103031, 0], [(-822223330624230)]], [[2205856273437, 0, 0, 0], [12069636268199, 0, 0], [30340464102764, 0], [35039776210369]], [[(-5065305397), 0, 0, 0, 0], [65165354610, 0, 0, 0], [351591486088, 0, 0], [411787194965, 0], [(-202263623978)]]], r := 67847915020, ok := true }, dde := { p := [[[(-54107568075720514472)]], [[85487132024146903, 0], [214896224110825413]], [[(-2173879650163793), 0, 0], [(-9429555523958783), 0], [(-13736989673316330)]], [[6655836681707, 0, 0, 0], [(-26082462473827), 0, 0], [(-65565688875319), 0], [105727209260222]], [[(-92429318129), 0, 0, 0, 0], [(-579082340967), 0, 0, 0], [(-2412325816153), 0, 0], [(-3659286353448), 0], [(-3690811783817)]]], r := 1449404459266, ok := true }, nJu := { p := [[[(-6831020462231801343)]], [[329420771212959067, 0], [828092815856135195]], [[(-260233807965352), 0, 0], [4470968370206062, 0], [(-1644446661248459)]], [[4411712546874, 0, 0, 0], [24139272536398, 0, 0], [60680928205528, 0], [70079552420738]], [[(-10130610793), 0, 0, 0, 0], [130330709220, 0, 0, 0], [703182972177, 0, 0], [823574389930, 0], [(-404527247955)]]], r := 135695830033, ok := true }, Jd1 := { p := [[[(-108215136151441028944)]], [[170974264048293807, 0], [429792448221650826]], [[(-4347759300327586), 0, 0], [(-18859111047917565), 0], [(-27473979346632660)]], [[13311673363414, 0, 0, 0], [(-52164924947654), 0, 0], [(-131131377750638), 0], [211454418520444]], [[(-184858636257), 0, 0, 0, 0], [(-1158164681933), 0, 0, 0], [(-4824651632306), 0, 0], [(-7318572706896), 0], [(-7381623567633)]]], r := 2898808918526, ok := true }, term0 := { p := [[[328486330298425546643]], [[(-964728250816251647), 0], [(-2205723339288155262)]], [[26983692525219907, 0, 0], [107579157710130314, 0], [142463776568601460]], [[(-116448882418297), 0, 0, 0], [119858993590804, 0, 0], [234361225559890, 0], [(-1525954743635918)]], [[1752875350150, 0, 0, 0, 0], [10547666383755, 0, 0, 0], [38593985153420, 0, 0], [59180085519934, 0], [54922033939161]]], r := 11029882428721, ok := true }, r0 := { p := [[[10540016933370707947]], [[(-20470001721032319), 4215925180814506616], [(-32060667070220740)]], [[871507217154394, (-8133358905223061), 421559881765637866], [1907074382906101, (-12826443674913973)], [1899276324974003]], [[(-2529166220096), 339364084200147, (-791480110395706), (-6526984089309)], [16590921407151, 764263269155197, (-1283515066870085)], [15026533742555, 759662843773394], [(-13811430096331)]], [[45920841061, (-978576366874), 30241356425958, 4370782777382, (-326279438512)], [189324987432, 6405941849084, 76999680973941, (-174124135614)], [694046186860, 6041577207643, 75947211197039], [644514642046, (-5525444371473)], [449664469248]]], r := 7274062393567, ok := true }, r1 := { p := [[[107910476985001020429]], [[(-196692729055069581), 0], [(-328815935894929673)]], [[6741412401532231, 0, 0], [19867245428504102, 0], [19437316813636423]], [[(-18646805672314), 0, 0, 0], [115527307098758, 0, 0], [161186557226407, 0], [(-141635201032305)]], [[292132798151, 0, 0, 0, 0], [1498866394997, 0, 0, 0], [5984994052277, 0, 0], [6731237712826, 0], [4600833635731]]], r := 2955661180557, ok := true }, r2 := { p := [[[13592867009139660061]], [[(-122682363844482356), 4377396658635045227], [(-879670013414678069)]], [[1358401850728031, (-24396373683425414), 408101907332662027], [17595260623019791, (-50902901562930404)], [64577530340539080]], [[(-9629179968585), 367455955687619, (-135320562084090), (-123103883955566)], [(-104618098249205), 2806166650683256, 2264321664284333], [(-286744460470609), 2847187539033434], [(-747508398527357)]], [[80906354178, (-1866459557953), 25959667823671, 43235761083416, (-264620662066)], [1217613630545, 716591961581, (-15906661369482), 13214991428904], [7320613107280, 47360612305348, (-154120500022403)], [20750368051809, 4690149091641], [27769634206030]]], r := 59814493496412, ok := true }, r3 := { p := [[[50788058991534599362]], [[(-551345127845312850), 17556931048986459228], [(-2449491498268866088)]], [[9274718956946988, (-117063647678733097), 1632685844283734302], [75019302180544301, (-208215147725961360)], [175703650754976085]], [[(-73662701242809), 2721799632569729, (-805507266498273), (-1036473448381628)], [(-467588633713427), 12703199750654929, 9187066815127529], [(-1019487137241049), 11349006633423420], [(-2269756035578855)]], [[842198238450, (-14427391369695), 159945991807240, 380687220104325, (-4186836018316)], [8411011299725, 20153204382863, (-123251257187545), 103979107289379], [36744056369035, 200099657066380, (-626186155831426)], [79395329384185, 17851998205229], [81756341500715]]], r := 437379529436899, ok := true }, eta := { p := [[[(-218654624835506386302)]], [[517412188568274447, 0], [1429836039254514167]], [[(-13270189537195559), 0, 0], [(-58262503553419890), 0], [(-94881822020976994)]], [[45912621472175, 0, 0, 0], [(-103056765250021), 0, 0], [(-183073723951342), 0], [981578550738621]], [[(-641884217836), 0, 0, 0, 0], [(-4110177395691), 0, 0, 0], [(-17448171170282), 0, 0], [(-30889939401587), 0], [(-36179015874364)]]], r := 87453039748280792, 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 := 8214565720323784704, bh := 144115188075855872, tc := 5188146770730811392, th := 576460752303423488, sc := 18320643284143177728, sh := 126100789566373888 }
noncomputable def q1 : Cert := { V0 := [[[15939099795005231]], [[(-15947276224628136), 1771009180749223], [238838395515089]], [[8389993353817, (-1771913854825622), (-317930379)], [(-237972060205606), 26537513749459], [2238373796260]], [[(-213879576498), 926489848413, 954279415, (-11775126)], [(-858107852748), (-26441082989349), (-14292007)], [(-2211214926482), 248706110972], [33604111992]], [[320185666, (-21847775978), (-955268515), 35343307, 5], [(-8202535011), (-95601909080), 42838764, (-529329)], [(-26892104790), (-245684299148), (-348102)], [(-33076393760), 3733747651], [386333215]]], r0 := 59759153408, V1 := [[[56671999501764597]], [[(-56700360062962285), 0], [849187211145933]], [[28763486025589, 0, 0], [(-846075004164896), 0], [7958273349481]], [[(-403488080493), 0, 0, 0], [(-3098843016237), 0, 0], [(-7860933704821), 0], [119473358203]], [[568134740, 0, 0, 0, 0], [(-13316270539), 0, 0, 0], [(-96773614125), 0, 0], [(-117581284028), 0], [1373481398]]], r1 := 32052178760, V2 := [[[2034131172509727681]], [[(-16550566976785043), 1724796090719621], [(-288141775871098342)]], [[32260171054491, (-1724936929678927), (-38861536605)], [(-85149005709336), 38829418526661], [10226248506731]], [[(-233367731132), 160111149223, 78051838815, (-10032708)], [(-3447213886363), (-38829527861207), 3863508183], [(-10088626729986), (-452546570216)], [278052081741]], [[730601998, (-19274097255), (-39520694964), 30086579, 703], [(-4005082713), 1528840645, (-7714302069), (-921313)], [(-137279164632), 454465261448, 229796433], [(-276585958942), (-12142103781)], [(-643627420)]]], r2 := 528322401356, V3 := [[[2050659115150557980]], [[(-33120346395484465), 3449823016286143], [(-288054195397942284)]], [[74736964066594, (-3450361715153626), (-156755346164)], [(-168270687042769), 77655910254231], [20421153828825]], [[(-875443225894), 603379088699, 316142085024, (-80165417)], [(-7889745251787), (-77655738163646), 15402804850], [(-20115031227651), (-908970806475)], [555720569714]], [[2813152281, (-64634056830), (-162031896994), 240307673, 11351], [(-20119468781), 5210213102, (-30703894972), (-7380272)], [(-304983374122), 916687146934, 918200444], [(-552436269771), (-24261152744)], [(-1315256239)]]], r3 := 1124629673376, Vm := [[[2074533509227742015]], [[(-57666814691712089), 0], [(-287113985335182144)]], [[725697113971267, 0, 0], [(-1240711315187340), 0], [18469519053449]], [[19807778829942, 0, 0, 0], [117629484332119, 0, 0], [(-35397056261210), 0], [2559422420594]], [[428767753548, 0, 0, 0, 0], [6477353894528, 0, 0, 0], [15451976902801, 0, 0], [(-4823199222518), 0], [354183272553]]], rm := 127486476422418 }
noncomputable def w1 : Wit := { Z0 := { p := [[[15939108379144511]], [[(-15947301990267821), 1771012042127167], [238838781400677]], [[8415785794746, (-1771922443363092), 0], [(-237973216859404), 26537642377853], [2238383195033]], [[(-222504454842), 935087310527, 0, 0], [(-856953182147), (-26441468539934), 0], [(-2211243043679), 248709243892], [33604303551]], [[334482811, (-24722717205), 0, 0, 0], [(-8585479840), (-95217020239), 0, 0], [(-26864144796), (-245693671520), 0], [(-33076965668), 3733811505], [386336788]]], r := 14326498436, ok := true }, Z1 := { p := [[[56672385348069375]], [[(-56701518187618919), 0], [849204556091297]], [[29922793936876, 0, 0], [(-846126993277880), 0], [7958695804563]], [[(-791126950547), 0, 0, 0], [(-3046944647631), 0, 0], [(-7862197488634), 0], [119481968182]], [[1189272217, 0, 0, 0, 0], [(-30526150542), 0, 0, 0], [(-95516959274), 0, 0], [(-117606989041), 0], [1373641913]]], r := 7444760792, ok := true }, Z2 := { p := [[[2052167971411531908]], [[(-16994039804258395), 1771012042127167], [(-295862541464082927)]], [[36798708343177, (-1771922443363092), 0], [40500869828692, 26537642377853], [1124129595971057]], [[(-264634445334), 935087310527, 0, 0], [(-4309497087849), (-26441468539934), 0], [(-19426198912157), 248709243892], [(-56206380662134)]], [[934834444, (-24722717205), 0, 0, 0], [1478304519, (-95217020239), 0, 0], [(-88191130178), (-245693671520), 0], [(-159002176082), 3733811505], [423126573350]]], r := 50665253788, ok := true }, Z3 := { p := [[[2069142455398686615]], [[(-34022555819234145), 3543797360587877], [(-295900888984277709)]], [[91614759589866, (-3547442612705145), 0], [85312050468728, 52880601806652], [1143639905346304]], [[(-1052093050390), 3745971054812, 0, 0], [(-10775593181858), (-52495065993805), 0], [(-38844230571563), 491340753968], [(-56046448290391)]], [[4404928672, (-100968343782), 0, 0, 0], [4258925891, (-382141929979), 0, 0], [(-178405888133), (-479308287243), 0], [(-312745713276), 7349735490], [429706800385]]], r := 97050561842, ok := true }, iE := { p := [[[18616949604867541915]], [[(-9570174299342388), 0], [(-47648390120486965)]], [[259501006157087, 0, 0], [1178881035527965, 0], [3450378213882654]], [[(-385188484504), 0, 0, 0], [5505456598873, 0, 0], [11017694277905, 0], [(-21282974845882)]], [[5488929217, 0, 0, 0, 0], [36984816352, 0, 0, 0], [225789933492, 0, 0], [422640115920, 0], [824628613449]]], r := 101657144344, ok := true }, iHu := { p := [[[18626269980831046596]], [[(-19159518216117460), 0], [(-48835162971908408)]], [[529380755168454, 0, 0], [2362515860901789, 0], [3439254099424158]], [[(-1310884172440), 0, 0, 0], [8550934742470, 0, 0], [21795239681939, 0], [(-21707434114794)]], [[19446616523, 0, 0, 0, 0], [129273855644, 0, 0, 0], [569262000964, 0, 0], [839859843099, 0], [820797980477]]], r := 168039253377, ok := true }, T := { p := [[[5188146770730811392]], [[0, 576460752303423488], [0]]], r := 0, ok := true }, E := { p := [[[18278094647254621759]], [[9395983517534392, 0], [46781121660439136]], [[(-249947647191560), 0, 0], [(-1109327392894468), 0], [(-3267844395470436)]], [[118719870748, 0, 0, 0], [(-7862287556464), 0, 0], [(-20039966027378), 0], [3861649868933]], [[(-1649577829), 0, 0, 0, 0], [(-10569837911), 0, 0, 0], [(-109379183411), 0, 0], [(-68669588026), 0], [(-140608314333)]]], r := 75236186394, ok := true }, de := { p := [[[(-3086592359925482859)]], [[164216230640061156, 0], [418566181856997982]], [[(-116998878937592), 0, 0], [2284556127121215, 0], [(-760112395634976)]], [[2167553537128, 0, 0, 0], [12469226908901, 0, 0], [31782465579830, 0], [35893350905244]], [[(-4514160458), 0, 0, 0, 0], [68057693072, 0, 0, 0], [369584724218, 0, 0], [442153776106, 0], [(-190532568114)]]], r := 72340275588, ok := true }, dde := { p := [[[(-53945237550010264949)]], [[76868556692271325, 0], [195928125704360742]], [[(-2136132159537189), 0, 0], [(-9540884500382837), 0], [(-13877915309298081)]], [[5931629469436, 0, 0, 0], [(-29595109579665), 0, 0], [(-75434151485016), 0], [98224128880467]], [[(-88701801987), 0, 0, 0, 0], [(-592167197127), 0, 0, 0], [(-2523643966791), 0, 0], [(-3847161878076), 0], [(-3743903719604)]]], r := 1513847518432, ok := true }, nJu := { p := [[[(-6173184719850965718)]], [[328432461280122313, 0], [837132363713995965]], [[(-233997757875184), 0, 0], [4569112254242431, 0], [(-1520224791269951)]], [[4335107074256, 0, 0, 0], [24938453817803, 0, 0], [63564931159660, 0], [71786701810488]], [[(-9028320915), 0, 0, 0, 0], [136115386145, 0, 0, 0], [739169448436, 0, 0], [884307552213, 0], [(-381065136227)]]], r := 144680551167, ok := true }, Jd1 := { p := [[[(-107890475100020529898)]], [[153737113384542650, 0], [391856251408721484]], [[(-4272264319074377), 0, 0], [(-19081769000765674), 0], [(-27755830618596162)]], [[11863258938873, 0, 0, 0], [(-59190219159330), 0, 0], [(-150868302970031), 0], [196448257760935]], [[(-177403603974), 0, 0, 0, 0], [(-1184334394254), 0, 0, 0], [(-5047287933581), 0, 0], [(-7694323756151), 0], [(-7487807439208)]]], r := 3027695036857, ok := true }, term0 := { p := [[[326663904726380011923]], [[(-858135510651951878), 0], [(-1990001033283581993)]], [[26326337798270872, 0, 0], [108185523419516735, 0], [143088745391280143]], [[(-102787024401172), 0, 0, 0], [183427276837117, 0, 0], [391579319132281, 0], [(-1405389172131240)]], [[1664610183588, 0, 0, 0, 0], [10651088054190, 0, 0, 0], [40051783159966, 0, 0], [61450166139893, 0], [55180763042509]]], r := 11359894200184, ok := true }, r0 := { p := [[[8507063666659318664]], [[(-13787368452587377), 1890455306718154301], [(-22824585067694908)]], [[697997647174990, (-3057279265588898), 105024564625120366], [1600174170902944, (-5072219672134013)], [1565056206742285]], [[(-1766408809917), 151807087599820, (-168386544691691), (-81132194568)], [14480109749266, 355772797271380, (-281809905502897)], [14489484585265, 347788267222928], [(-10099161981889)]], [[36208021924, (-383213189054), 7699624262774, 162476907921, (-2253628806)], [163697306948, 3129683910701, 19804829987824, (-2213728576)], [601556107284, 3223851185645, 19321125750193], [566809952844, (-2244295661106)], [372988144325]]], r := 1923507274413, ok := true }, r1 := { p := [[[107543912641188833798]], [[(-169941579948354854), 0], [(-288607217876036507)]], [[6636456254040995, 0, 0], [20347596160286867, 0], [19784076794268932]], [[(-16352512087549), 0, 0, 0], [124713218869835, 0, 0], [185801825664709, 0], [(-127698152291284)]], [[281679825298, 0, 0, 0, 0], [1564032445436, 0, 0, 0], [6327634637530, 0, 0], [7214453928624, 0], [4714849933877]]], r := 2820335669332, ok := true }, r2 := { p := [[[11289819300225698126]], [[(-105900495383432931), 1961047165761083894], [(-821686009050219554)]], [[1130749705104195, (-11443330846470794), 101998609646446877], [15783836473356145, (-23760850270164917)], [62523291205244664]], [[(-8144404145603), 165110058366539, (-22960973397490), (-4941136116238)], [(-97911415505097), 1408711624739011, 557976965377346], [(-281901215255143), 1548137515814703], [(-708451960230090)]], [[66769130066, (-858792236024), 6750128047814, 5022864769356, (-1851185339)], [1088784893286, 65247323108, (-796545131620), 557135334300], [7038365730738, 24098316212302, (-38198457329352)], [20976828586302, 3028270442741], [27981421273409]]], r := 24736916994236, ok := true }, r3 := { p := [[[41463071818489220921]], [[(-462014229705110450), 7850809914453758043], [(-2207654532643325412)]], [[7574359213714180, (-52965872032130851), 408050064026042346], [66835349347704549, (-95839904736182852)], [167778583767652270]], [[(-60669570455002), 1234808989037887, (-165183550182443), (-40177729511482)], [(-428492296582483), 6423816960375045, 2233423344328990], [(-975885824058822), 6186796922300341], [(-2120178748939801)]], [[686785415622, (-6567120383142), 44650473156917, 41485388488158, (-29530018216)], [7546219475959, 7530662082869, (-6120269361346), 4437577871498], [35407021890280, 101608256290738, (-153823765713017)], [80482632527657, 11881426688290], [82519529727475]]], r := 148101403180269, ok := true }, eta := { p := [[[(-217672524095301589314)]], [[464862065576539096, 0], [1312865790197579459]], [[(-13009896451713555), 0, 0], [(-58724322926735714), 0], [(-95318619097335850)]], [[40887677437874, 0, 0, 0], [(-127924567467731), 0, 0], [(-254164518870168), 0], [918698506341406]], [[(-614927131900), 0, 0, 0, 0], [(-4181827910127), 0, 0, 0], [(-18109997690241), 0, 0], [(-32015038029757), 0], [(-36372973514186)]]], r := 103740759120881690, 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 := 8142508126285856768, bh := 72057594037927936, tc := 6341068275337658368, th := 576460752303423488, sc := 18320643284143177728, sh := 126100789566373888 }
noncomputable def q2 : Cert := { V0 := [[[19335838951247536]], [[(-19346343433374598), 1757800754700629], [144604073453898]], [[10755474259456, (-1758750130438773), (-379952274)], [(-144090777406190), 13145762346504], [668719133942]], [[(-251384206297), 969397695560, 1140474315, (-11513599)], [(-508541092825), (-13098974197630), (-8524467)], [(-660655371914), 60791891942], [5018118857]], [[397040459, (-20052841909), (-1141723570), 34559289, 6], [(-4741038816), (-46418088471), 25552333, (-258315)], [(-7986774128), (-60057315716), (-103173)], [(-4940347244), 456184962], [28409174]]], r0 := 12646174220, V1 := [[[56249380615553004]], [[(-56279273179700695), 0], [420658931277430]], [[30288946345759, 0, 0], [(-419150796618193), 0], [1945274414527]], [[(-396968557527), 0, 0, 0], [(-1501729252644), 0, 0], [(-1921636270192), 0], [14597249499]], [[591150787, 0, 0, 0, 0], [(-6383025398), 0, 0, 0], [(-23503024973), 0, 0], [(-14369188968), 0], [82636408]]], r1 := 3986587304, V2 := [[[2181614958719841738]], [[(-19920972745215580), 1705106705644706], [(-144036616524222986)]], [[34101614512638, (-1705082545765931), (-40793401639)], [(-76923451449072), 19643685532883], [2235142701515]], [[(-267200251636), (-7005964391), 81966600618, (-9567781)], [(-1644851685812), (-19651936011855), 1814524492], [(-2200542571319), (-108344400001)], [31859911048]], [[754285228, (-17148911481), (-41554576667), 28685376, 719], [(-3223853769), 8924688618, (-3620050293), (-457635)], [(-34517739991), 108599245396, 57012592], [(-31683185020), (-1524278970)], [(-32700909)]]], r2 := 70275957504, V3 := [[[2201512132780011639]], [[(-39862460104383531), 3410113026729785], [(-143958523960752684)]], [[79124233607334, (-3409980810992241), (-164686376846)], [(-152897214656858), 39302258264909], [4461086403676]], [[(-978497073826), (-81513837087), 332410899371, (-76394503)], [(-3752147875151), (-39334730936964), 7221930424], [(-4382791680304), (-217209539323)], [63682926706]], [[2752990352, (-50597000141), (-170775297114), 228890770, 11603], [(-14671365751), 34910010530, (-14371801778), (-3666473)], [(-78027748854), 218240589333, 227793297], [(-63295659021), (-3045886861)], [(-66458806)]]], r3 := 221066812840, Vm := [[[2218094820051642109]], [[(-57054743785430761), 0], [(-143565349121626077)]], [[670512165077548, 0, 0], [(-604314722742834), 0], [3776551177143]], [[16891423006227, 0, 0, 0], [51774376958894, 0, 0], [(-7261273829970), 0], [244806315543]], [[337789906963, 0, 0, 0, 0], [2621899910830, 0, 0, 0], [3204497770936, 0, 0], [(-463393162550), 0], [15844228692]]], rm := 16579780260377 }
noncomputable def w2 : Wit := { Z0 := { p := [[[19335854276039320]], [[(-19346389432756132), 1757804934185392], [144604417275871]], [[10801524278740, (-1758762675705103), 0], [(-144091808026344), 13145856115988], [668723295237]], [[(-266785894398), 981956752612, 0, 0], [(-507512144627), (-13099255275123), 0], [(-660667821513), 60793026839], [5018160982]], [[423927684, (-24253263128), 0, 0, 0], [(-5082382163), (-46137467694), 0, 0], [(-7974392649), (-60060711047), 0], [(-4940473015), 456196452], [28409565]]], r := 2569896668, ok := true }, Z1 := { p := [[[56249757893932567]], [[(-56280405622563291), 0], [420667395711625]], [[31422616083608, 0, 0], [(-419176168803909), 0], [1945376858873]], [[(-776104420067), 0, 0, 0], [(-1476398966186), 0, 0], [(-1921942753492), 0], [14598286493]], [[1233244172, 0, 0, 0, 0], [(-14785111745), 0, 0, 0], [(-23198233160), 0, 0], [(-14372285134), 0], [82646009]]], r := 838931562, ok := true }, Z2 := { p := [[[2203902937084646754]], [[(-20536652673635781), 1757804934185392], [(-148488229148050308)]], [[40895762651249, (-1758762675705103), 0], [3707030819342, 13145856115988], [302394368863472]], [[(-314049145694), 981956752612, 0, 0], [(-2204243887064), (-13099255275123), 0], [(-4919490655354), 60793026839], [(-7134996965267)]], [[1056075842, (-24253263128), 0, 0, 0], [150136922, (-46137467694), 0, 0], [(-22189951891), (-60060711047), 0], [(-19148470730), 456196452], [28627272451]]], r := 5036122180, ok := true }, Z3 := { p := [[[2224420800921683991]], [[(-41117512663933372), 3517478981348348], [(-148490996705606975)]], [[104827346093036, (-3521314022061272), 0], [9943045254626, 26197365947402], [307333057288410]], [[(-1253526926799), 3934096413336, 0, 0], [(-5672593666304), (-26010528115975), 0], [(-9833006475534), 120110034489], [(-7115750766675)]], [[5145012763, (-99314898148), 0, 0, 0], [227098024, (-185207796762), 0, 0], [(-46818928616), (-117187559564), 0], [(-37607904038), 898182367], [29035718729]]], r := 13153074330, ok := true }, iE := { p := [[[18641639106633450105]], [[(-10156912988839679), 0], [(-25557572648553390)]], [[256804167445409, 0, 0], [584089225560541, 0], [870887332278708]], [[(-403313077724), 0, 0, 0], [2641500294226, 0, 0], [2597326855263, 0], [(-2868973592078)]], [[5394330955, 0, 0, 0, 0], [17763291012, 0, 0, 0], [54793914086, 0, 0], [51913543184, 0], [52778723822]]], r := 8342615787, ok := true }, iHu := { p := [[[18651550140815805120]], [[(-20335431861413407), 0], [(-26145555250388667)]], [[525246169995357, 0, 0], [1170673434564687, 0], [868264076931101]], [[(-1374404669232), 0, 0, 0], [3995117236553, 0, 0], [5136579304138, 0], [(-2921110798452)]], [[19233603923, 0, 0, 0, 0], [62427057792, 0, 0, 0], [138072549929, 0, 0], [103195748599, 0], [52557965578]]], r := 16944226425, ok := true }, T := { p := [[[6341068275337658368]], [[0, 576460752303423488], [0]]], r := 0, ok := true }, E := { p := [[[18253886633812807655]], [[9945645722848821, 0], [25025966391341629]], [[(-246043659314392), 0, 0], [(-544669131460851), 0], [(-818462131619263)]], [[123857343060, 0, 0, 0], [(-3877019566026), 0, 0], [(-4984739442033), 0], [518045444006]], [[(-1610011396), 0, 0, 0, 0], [(-4991810565), 0, 0, 0], [(-26782017067), 0, 0], [(-8251768487), 0], [(-8882787466)]]], r := 6068836065, ok := true }, de := { p := [[[(-3296069977712365700)]], [[163081843305467090, 0], [209676655678457686]], [[(-123142070817887), 0, 0], [1126551113899731, 0], [(-203561382372426)]], [[2134284842492, 0, 0, 0], [6052735857133, 0, 0], [7782088959172, 0], [4536133090894]], [[(-4694332089), 0, 0, 0, 0], [32520150133, 0, 0, 0], [89499449466, 0, 0], [53757799199, 0], [(-12827785437)]]], r := 6320884128, ok := true }, dde := { p := [[[(-54046683604890473531)]], [[81620619500592286, 0], [104940796500761511]], [[(-2121959414981715), 0, 0], [(-4734160699833975), 0], [(-3507728828847333)]], [[6222963292508, 0, 0, 0], [(-13553945391043), 0, 0], [(-17426501217056), 0], [13226064840340]], [[(-87869887438), 0, 0, 0, 0], [(-286690863435), 0, 0, 0], [(-612877017753), 0, 0], [(-473917549765), 0], [(-240114257190)]]], r := 155696369608, ok := true }, nJu := { p := [[[(-6592139955424731400)]], [[326163686610934180, 0], [419353311356915373]], [[(-246284141635774), 0, 0], [2253102227799463, 0], [(-407122764744851)]], [[4268569684984, 0, 0, 0], [12105471714267, 0, 0], [15564177918344, 0], [9072266181789]], [[(-9388664177), 0, 0, 0, 0], [65040300266, 0, 0, 0], [178998898932, 0, 0], [107515598399, 0], [(-25655570874)]]], r := 12641768248, ok := true }, Jd1 := { p := [[[(-108093367209780947062)]], [[163241239001184573, 0], [209881593001523022]], [[(-4243918829963429), 0, 0], [(-9468321399667950), 0], [(-7015457657694665)]], [[12445926585017, 0, 0, 0], [(-27107890782086), 0, 0], [(-34853002434112), 0], [26452129680680]], [[(-175739774876), 0, 0, 0, 0], [(-573381726869), 0, 0, 0], [(-1225754035506), 0, 0], [(-947835099530), 0], [(-480228514380)]]], r := 311392739211, ok := true }, term0 := { p := [[[327694856573885319592]], [[(-912138048122246128), 0], [(-1067085816146293064)]], [[26244561744276685, 0, 0], [53919973917977963, 0], [36320122396319613]], [[(-108049269540262), 0, 0, 0], [71912119199989, 0, 0], [74911991334969, 0], [(-189692775224249)]], [[1657556624434, 0, 0, 0, 0], [5200999530992, 0, 0, 0], [9791984874227, 0, 0], [7643211615035, 0], [3562390303787]]], r := 1161126528436, ok := true }, r0 := { p := [[[12725706394860048399]], [[(-21764280222709421), 2313758880709507958], [(-18222897368799646)]], [[1021273288275773, (-3945288691937289), 105169782152389641], [1184974984147230, (-3313334112869119)], [590347301897494]], [[(-2726451619542), 179734194576527, (-177176195126829), (-97823236220)], [10229553270480, 215609410967291, (-150620649737402)], [5099567966535, 107334984923339], [(-2026827812052)]], [[52086754156, (-478077009638), 7087598435600, 195916791516, (-2223192561)], [116307408617, 1781215405377, 9829411761468, (-1323047706)], [216578298787, 928954694162, 4878701470886], [104100892766, (-368522384488)], [35693982250]]], r := 727512526887, ok := true }, r1 := { p := [[[107693178527706860718]], [[(-180069825488539960), 0], [(-154244720045609039)]], [[6575665830773588, 0, 0], [10083587089607652, 0], [4995688514573040]], [[(-17119898504470), 0, 0, 0], [59239760629389, 0, 0], [43768125301213, 0], [(-17155519379421)]], [[277589841885, 0, 0, 0, 0], [753032063171, 0, 0, 0], [1535336349062, 0, 0], [886623913447, 0], [302045162933]]], r := 371840906660, ok := true }, r2 := { p := [[[16069810605485151356]], [[(-138196432987949001), 2380092033620707814], [(-466489963224860507)]], [[1537274558352442, (-12168015953660521), 101678776505918006], [9421164761552178, (-11458182433109142)], [16641094808177939]], [[(-10483507584127), 190330986970309, 9355914153728, (-5228428103032)], [(-51843937703293), 687040456403914, 299592053907414], [(-66122707913023), 348148294020927], [(-95013024853864)]], [[88002420104, (-891466826356), 6027241903904, 5323076527433, (-1770075581)], [625150891341, 678272751387, (-2123630354700), 267013249242], [1840072112070, 6181254294945, (-9415818299375)], [2627370294848, 252963025902], [1799008624947]]], r := 4108194029656, ok := true }, r3 := { p := [[[60036904901730158721]], [[(-608287196508429056), 9527346031492723767], [(-1285760119933165000)]], [[10422003610557032, (-56273355475968185), 406640230778892964], [40225098697029479, (-46210372527307096)], [45703388107859589]], [[(-77792176449531), 1387550825739465, 101600126519935, (-42578774751317)], [(-219864266029143), 3119626033299314, 1205989644595223], [(-221934779079472), 1390446751383861], [(-283424238622144)]], [[897826810959, (-6456792878582), 34694600066471, 44091299716293, (-28192123667)], [4303843371477, 8788021011984, (-16724918018948), 2121232225975], [9368246283919, 26763968642616, (-37795001642189)], [10132461632833, 991706129682], [5296994196969]]], r := 35250095901583, ok := true }, eta := { p := [[[(-218352903772704405466)]], [[494164680554915196, 0], [704445881600895376]], [[(-12950424887032398), 0, 0], [(-29247056738034879), 0], [(-24187950670242730)]], [[42950201988020, 0, 0, 0], [(-55016900247977), 0, 0], [(-51576685298425), 0], [124075700310607]], [[(-610337383962), 0, 0, 0, 0], [(-2034924497186), 0, 0, 0], [(-4419353333257), 0, 0], [(-3975720182368), 0], [(-2346941293621)]]], r := 6529928151561548, 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 := 8286623314361712640, bh := 72057594037927936, tc := 6341068275337658368, th := 576460752303423488, sc := 18320643284143177728, sh := 126100789566373888 }
noncomputable def q3 : Cert := { V0 := [[[19627762581201888]], [[(-19637207582537206), 1784339138399973], [147340094084002]], [[9705819674226, (-1785191941807111), (-397422403)], [(-146793586681591), 13394488374087], [699527304535]], [[(-261180513441), 873591202188, 1192839050, (-12042989)], [(-541431883551), (-13344674796240), (-8950002)], [(-690979505810), 63592587019], [5254263611]], [[367405511, (-20816281127), (-1193997917), 36146057, 6], [(-5059496300), (-49417443582), 26825347, (-271209)], [(-8464408987), (-62813912736), (-109678)], [(-5170607782), 477652075], [30653669]]], r0 := 12895738176, V1 := [[[57098597696343861]], [[(-57125377580455935), 0], [428617891414127]], [[27189634637670, 0, 0], [(-427012399856529), 0], [2034892487545]], [[(-410289160658), 0, 0, 0], [(-1598519910101), 0, 0], [(-2009834927227), 0], [15284145253]], [[543615167, 0, 0, 0, 0], [(-6946244037), 0, 0, 0], [(-24909348842), 0, 0], [(-15038826865), 0], [89165063]]], r1 := 4146812512, V2 := [[[1893550920573954099]], [[(-20083874723145072), 1743948532741281], [(-144027294741709286)]], [[30672434109773, (-1743939866988686), (-36935159557)], [(-86104686250791), 19192072898533], [2425456562747]], [[(-273993440080), 9845816467, 74268371570, (-10489023)], [(-1785038218984), (-19199324041343), 2044242587], [(-2389776114342), (-117447103960)], [31567923230]], [[700189395, (-18507572891), (-37732760826), 31450642, 685], [(-3579940585), 7934038717, (-4079221425), (-462941)], [(-35582033170), 117690699400, 57799848], [(-31384475351), (-1509466074)], [(-40290090)]]], r2 := 68954143748, V3 := [[[1913613437555365359]], [[(-40186290910473944), 3487824398595192], [(-143939917668749110)]], [[71304752382684, (-3487753052180237), (-149326830826)], [(-171185594203952), 38396991843830], [4841466935446]], [[(-1008954807163), (-15756606081), 301837979348, (-83776218)], [(-4068891718497), (-38425417451955), 8139685411], [(-4760783526932), (-235391573698)], [63090276103]], [[2572607114, (-55496221998), (-155707501548), 251060214, 11092], [(-15820096265), 30873477417, (-16205199256), (-3709915)], [(-80365426767), 236379161324, 230897067], [(-62681108778), (-3013790253)], [(-81688772)]]], r3 := 219032368380, Vm := [[[1930981477649055618]], [[(-58296666496170231), 0], [(-143546701232226067)]], [[788639785965516, 0, 0], [(-640042022351368), 0], [5727050772497]], [[23435062012177, 0, 0, 0], [67353544741492, 0, 0], [(-10934915855342), 0], [426190425116]], [[552067388725, 0, 0, 0, 0], [4055252782599, 0, 0, 0], [4713035767861, 0, 0], [(-799013944071), 0], [31676956350]]], rm := 28858896677035 }
noncomputable def w3 : Wit := { Z0 := { p := [[[19627778610626126]], [[(-19637255693982540), 1784343510056920], [147340455069385]], [[9753978131143, (-1785205063089322), 0], [(-146794668647412), 13394586824489], [699531728208]], [[(-277281456100), 886725284649, 0, 0], [(-540351876950), (-13344969877038), 0], [(-690992738759), 63593793473], [5254308996]], [[392581804, (-25207405100), 0, 0, 0], [(-5417574942), (-49122897905), 0, 0], [(-8451251679), (-62817521706), 0], [(-5170743269), 477664454], [30654096]]], r := 2605367055, ok := true }, Z1 := { p := [[[57098992321821458]], [[(-57126562018858297), 0], [428626778383668]], [[28375209108779, 0, 0], [(-427039036065198), 0], [2035001391150]], [[(-806636963199), 0, 0, 0], [(-1571932732945), 0, 0], [(-2010160694570), 0], [15285262534]], [[1142056158, 0, 0, 0, 0], [(-15760218013), 0, 0, 0], [(-24585459428), 0, 0], [(-15042162235), 0], [89175552]]], r := 868280082, ok := true }, Z2 := { p := [[[1908079420320159677]], [[(-20549076332378531), 1784343510056920], [(-147363390500670122)]], [[36394914035966, (-1785205063089322), 0], [(-16213879222348), 13394586824489], [260236614459174]], [[(-314485313012), 886725284649, 0, 0], [(-2298439913739), (-13344969877038), 0], [(-5044288500767), 63593793473], [(-6923301713964)]], [[960281601, (-25207405100), 0, 0, 0], [(-599481806), (-49122897905), 0, 0], [(-24943153416), (-62817521706), 0], [(-22473071085), 477664454], [24341069515]]], r := 5008881795, ok := true }, Z3 := { p := [[[1928611664350254076]], [[(-41137272496945843), 3570361420668234], [(-147346159154588375)]], [[93284934617248, (-3573810867429046), 0], [(-29866394189643), 26688748557680], [265300709445268]], [[(-1256039141434), 3551897371956, 0, 0], [(-5874887301795), (-26489876149708), 0], [(-10078306231622), 125623129757], [(-6900723458423)]], [[4669277209, (-102689576251), 0, 0, 0], [(-2786952388), (-197105475925), 0, 0], [(-54424415921), (-122526206376), 0], [(-44201804867), 940045205], [24766218939]]], r := 13353478764, ok := true }, iE := { p := [[[18593985395293868814]], [[(-8977926285745142), 0], [(-22106782080060625)]], [[262310753524413, 0, 0], [595108827743308, 0], [854920346884847]], [[(-366314898826), 0, 0, 0], [2867344985798, 0, 0], [2914382323558, 0], [(-2456524927231)]], [[5589659544, 0, 0, 0, 0], [19261617122, 0, 0, 0], [58183197183, 0, 0], [53821874084, 0], [50400634344]]], r := 8632372558, ok := true }, iHu := { p := [[[18602709550502434401]], [[(-17972706020690137), 0], [(-22705890711853252)]], [[533800010099493, 0, 0], [1192472395524895, 0], [851978671572538]], [[(-1245083595629), 0, 0, 0], [4564534274702, 0, 0], [5766622804189, 0], [(-2510578058037)]], [[19683498573, 0, 0, 0, 0], [66988467940, 0, 0, 0], [146791028330, 0, 0], [106917843474, 0], [50142107463]]], r := 17674762255, ok := true }, T := { p := [[[6341068275337658368]], [[0, 576460752303423488], [0]]], r := 0, ok := true }, E := { p := [[[18300668720922186551]], [[8836301162087930, 0], [21758051688865197]], [[(-253906327306722), 0, 0], [(-564709765971748), 0], [(-815565529473913)]], [[113283863567, 0, 0, 0], [(-3986409334848), 0, 0], [(-5036246327380), 0], [447731790226]], [[(-1690773868), 0, 0, 0, 0], [(-5588952746), 0, 0, 0], [(-27923453523), 0, 0], [(-8920323053), 0], [(-8700374783)]]], r := 6408801714, ok := true }, de := { p := [[[(-2877494822154506944)]], [[165366509976381002, 0], [208916448007427925]], [[(-110670876263633), 0, 0], [1158336655297437, 0], [(-176637737648760)]], [[2202366334796, 0, 0, 0], [6422394310274, 0, 0], [8113757780807, 0], [4440836434850]], [[(-4322637812), 0, 0, 0, 0], [35608947096, 0, 0, 0], [95403514136, 0, 0], [56834138008, 0], [(-11011567322)]]], r := 6813538822, ok := true }, dde := { p := [[[(-53850730920805492264)]], [[72078773136034718, 0], [91061009042667461]], [[(-2151566908578977), 0, 0], [(-4809609540493675), 0], [(-3434037245950768)]], [[5630576728415, 0, 0, 0], [(-16078319405879), 0, 0], [(-20312609733887), 0], [11353456457124]], [[(-89646114697), 0, 0, 0, 0], [(-306134513429), 0, 0, 0], [(-650040146784), 0, 0], [(-488610099553), 0], [(-228366166717)]]], r := 161510737284, ok := true }, nJu := { p := [[[(-5754989644309013887)]], [[330733019952762005, 0], [417832896014855851]], [[(-221341752527266), 0, 0], [2316673310594874, 0], [(-353275475297519)]], [[4404732669593, 0, 0, 0], [12844788620549, 0, 0], [16227515561614, 0], [8881672869700]], [[(-8645275624), 0, 0, 0, 0], [71217894192, 0, 0, 0], [190807028273, 0, 0], [113668276016, 0], [(-22023134644)]]], r := 13627077636, ok := true }, Jd1 := { p := [[[(-107701461841610984527)]], [[144157546272069436, 0], [182122018085334923]], [[(-4303133817157953), 0, 0], [(-9619219080987350), 0], [(-6868074491901535)]], [[11261153456830, 0, 0, 0], [(-32156638811758), 0, 0], [(-40625219467773), 0], [22706912914248]], [[(-179292229394), 0, 0, 0, 0], [(-612269026858), 0, 0, 0], [(-1300080293567), 0, 0], [(-977220199105), 0], [(-456732333434)]]], r := 323021474560, ok := true }, term0 := { p := [[[325704504149798558658]], [[(-803937160604995978), 0], [(-923969476576374349)]], [[26428143217045482, 0, 0], [54311644907411005, 0], [35265645364848486]], [[(-97393972788787), 0, 0, 0], [111977795987385, 0, 0], [121015179437945, 0], [(-162089734984278)]], [[1674029146130, 0, 0, 0, 0], [5462716338128, 0, 0, 0], [10254749623803, 0, 0], [7734895344978, 0], [3344700701388]]], r := 1204680875749, ok := true }, r0 := { p := [[[12691606340166352519]], [[(-19373092157355436), 2307558707053851331], [(-15884701925804142)]], [[1042615978042176, (-3510201223456360), 104887926311611982], [1206636621507285, (-2888211322593588)], [579029062844657]], [[(-2484309441341), 183453786107102, (-157340219629422), (-100529160058)], [11121984947452, 219555132206460, (-131297550883463)], [5734938207681, 105277071992384], [(-1748148242955)]], [[53909960014, (-435417029206), 7227417755874, 201305059952, (-2284687123)], [126008523583, 1939952741382, 10010079378993, (-1383441189)], [229852852668, 1044577614751, 4785150649598], [107788845922, (-317854002108)], [34021320842]]], r := 741053077456, ok := true }, r1 := { p := [[[107404539382462596859]], [[(-159720425587388584), 0], [(-134458285595882372)]], [[6700410899585608, 0, 0], [10269420548053887, 0], [4899886596259721]], [[(-15555300694630), 0, 0, 0], [65569015175159, 0, 0], [49180239662174, 0], [(-14797326032699)]], [[286093935400, 0, 0, 0, 0], [812696658116, 0, 0, 0], [1630911055659, 0, 0], [918263599294, 0], [287887437418]]], r := 387581424855, ok := true }, r2 := { p := [[[15202663378068290984]], [[(-119597496752478479), 2358570268150046020], [(-401009067112694644)]], [[1441039493789729, (-10769113651558679), 102240027212191885], [9188363804793306, (-10062590894812918)], [16113305600401782]], [[(-9236400554976), 191907830889827, 5237719711496, (-4672613322097)], [(-44341726807197), 711909350756551, 261528061953946], [(-50232080217191), 349635422356767], [(-81058109076513)]], [[82296340256, (-813673243417), 6394880024793, 4770912805436, (-1927238454)], [623023328083, 903271677536, (-1996013626535), 288675322382], [1914196508603, 6252533105006, (-9611687743349)], [2673058322973, 240936753279], [1692924916078]]], r := 3933322334606, ok := true }, r3 := { p := [[[57646014523571728177]], [[(-528643393693852191), 9440494933552852227], [(-1106180761017743784)]], [[10020240897549725, (-49926516158208741), 408899960988636676], [39459535401206568, (-40636841094460760)], [44127386950832130]], [[(-69128522247946), 1406441092237230, 69200447154057, (-38161903633157)], [(-181636596097513), 3227477946418612, 1053224561076904], [(-160679574026787), 1396268852744582], [(-242321155380498)]], [[867252569149, (-5925497003823), 37375848280877, 39733123306319, (-30717691675)], [4366857529390, 10130479809331, (-15685845589864), 2294624592487], [9761138439583, 27161081640954, (-38568943872924)], [10299741016962, 941701157554], [4988130939081]]], r := 33961644445935, ok := true }, eta := { p := [[[(-217039808279518619805)]], [[435432353067426613, 0], [609109073537214436]], [[(-13078424520471135), 0, 0], [(-29501281409157805), 0], [(-23498644801336659)]], [[38766754975139, 0, 0, 0], [(-73132886217967), 0, 0], [(-75595805445661), 0], [105880956852672]], [[(-620339939016), 0, 0, 0, 0], [(-2151761331376), 0, 0, 0], [(-4644628725884), 0, 0], [(-4035881743623), 0], [(-2205873957048)]]], r := 13085387389433701, 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 8070450532247928832 8358680908399640576 4611686018427387904 6917529027641081856 17942340915444056064 18446744073709551616 :=
  (RegionPosI.split_s 18194542494576803840 (RegionPosI.of_check c0 q0 ok_0 8070450532247928832 8358680908399640576 4611686018427387904 6917529027641081856 17942340915444056064 18194542494576803840 (by decide +kernel)) (RegionPosI.split_t 5764607523034234880 (RegionPosI.of_check c1 q1 ok_1 8070450532247928832 8358680908399640576 4611686018427387904 5764607523034234880 18194542494576803840 18446744073709551616 (by decide +kernel)) (RegionPosI.split_b 8214565720323784704 (RegionPosI.of_check c2 q2 ok_2 8070450532247928832 8214565720323784704 5764607523034234880 6917529027641081856 18194542494576803840 18446744073709551616 (by decide +kernel)) (RegionPosI.of_check c3 q3 ok_3 8214565720323784704 8358680908399640576 5764607523034234880 6917529027641081856 18194542494576803840 18446744073709551616 (by decide +kernel)))))

end CKLaneC.RSC2.BD_0045

end