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

import Definitions.Def_CK_CKLaneC_RSCell_Staged
import Definitions.Def_CK_CKLaneC_RSCell_RegionI

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

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

namespace CKLaneC.RSC2.BA_0131
open CKLaneC.TM3 CKLaneC.RSCell

noncomputable def c0 : Cell := { bc := 3026418949592973312, bh := 144115188075855872, tc := 14411518807585587200, th := 576460752303423488, sc := 2431943798780067840, sh := 126100789566373888 }
noncomputable def q0 : Cert := { V0 := [[[4901301966022311857]], [[(-69047423158089748), 176619715787356838], [76775001361569997]], [[616711309107490, (-1955400278290925), (-1031488231159982)], [(-1008334965042835), 2174242747400934], [(-530656486046641)]], [[(-9877871311769), 6614865218006, 39174096255470, (-5895413812005)], [10252165087512, (-4426680205854), (-43558342307228)], [9196263726388, (-28442757942289)], [20006649963871]], [[225518890593, (-44290876619), (-753512965902), 13451696797, 168260229236], [(-209492502940), (-380930292322), 1469666494265, (-14957169909)], [(-94914617601), 600420628981, (-197952868872)], [(-278442497363), 694798815008], [(-613410972683)]]], r0 := 22797936143160, V1 := [[[6085464683778680752]], [[(-80831141278273469), 0], [89877517477922215]], [[628840169529305, 0, 0], [(-973335567913793), 0], [(-736348570512975)]], [[(-9681228110755), 0, 0, 0], [6702008407023, 0, 0], [13170718626481, 0], [24711493367834]], [[225812804485, 0, 0, 0, 0], [(-148798733955), 0, 0, 0], [(-134718036882), 0, 0], [(-329449530453), 0], [(-774688437396)]]], r1 := 17176550363532, V2 := [[[15298976687350436768]], [[(-31069901727184288), 19880590108119026], [(-151869766097416029)]], [[162610843388010, 31299806094582, (-109475795182763)], [(-1628410627668836), 2018269091501442], [(-224585855317317)]], [[(-2928317082891), (-2523959116743), 815680525812, 556296237892], [10749466197610, 2670101272965, (-16555855047158)], [(-5281548171185), 57074301888469], [(-4535378276535)]], [[77971242373, 26228159509, 13785102357, (-9582829268), (-2641765072)], [(-185589652679), (-274434348185), 139203279000, 109740840130], [140090350382, (-13294729274), (-867328431851)], [50537112064, 305655773548], [15926134948]]], r2 := 96776943893368, V3 := [[[17581786910034854584]], [[(-44441261689196338), 10300381240636517], [(-44768255632018520)]], [[25083644510947, 466080518202711, (-112332302771533)], [(-2280271673670653), 1079272417779741], [(-188347080155982)]], [[99558509633, (-4127223125500), (-4280979311248), 1178755176795], [2593591463058, 48593596079634, (-17612185852977)], [(-8578386642965), 32977858416998], [(-867402639123)]], [[(-1975065686), (-13937763589), 86002387337, 35730263563, (-12081273940)], [11770537003, (-456331514947), (-664396436680), 245333202545], [79270162101, 1455013227345, (-993069942096)], [(-34754168565), 255638531368], [(-1538839445)]]], r3 := 1550665245270400, Vm := [[[15547018987377265170]], [[(-32036935011649474), 0], [(-124752918015739582)]], [[144685114065620, 0, 0], [(-1724195601603594), 0], [672185813943543]], [[(-2796640708110), 0, 0, 0], [8256109598138, 0, 0], [(-7519011548953), 0], [4081184073611]], [[77401920415, 0, 0, 0, 0], [(-162065323040), 0, 0, 0], [17408567935, 0, 0], [71437961395, 0], [55919123916]]], rm := 17099454323439 }
noncomputable def w0 : Wit := { Z0 := { p := [[[5167649981898464770]], [[(-80809305675166361), 206705999275938590], [89853238100335009]], [[906264307915552, (-3232372227006655), 0], [(-1590395617185998), 3594129524013400], [(-392943703913912)]], [[(-16111024636821), 36250572316622, 0, 0], [25237321852222, (-63615824687440), 0], [2953085029649, (-15717748156557)], [21986298154630]], [[369977541339, (-644440985473), 0, 0, 0], [(-558390947563), 1009492874088, 0, 0], [86052104168, 118123401185, 0], [(-367388528009), 879451926185], [(-616374338739)]]], r := 5379718162841, ok := true }, Z1 := { p := [[[6614591976830034906]], [[(-103435911264212942), 0], [115012144768428811]], [[1160018314131907, 0, 0], [(-2035706389998077), 0], [(-502967941009807)]], [[(-20622111535130), 0, 0, 0], [32303771970844, 0, 0], [3779948837951, 0], [28142461637927]], [[473571252914, 0, 0, 0, 0], [(-714740412880), 0, 0, 0], [110146693335, 0, 0], [(-470257315851), 0], [(-788959153586)]]], r := 4554745331496, ok := true }, Z2 := { p := [[[36369504813306691993]], [[(-323045495581140923), 206705999275938590], [(-1579047281305252360)]], [[4470843712250764, (-3232372227006655), 0], [10247243197638853, 3594129524013400], [64089048931403317]], [[(-85320540829032), 36250572316622, 0, 0], [(-116995772931554), (-63615824687440), 0], [(-437622603204610), (-15717748156557)], [(-2860657408949473)]], [[2058915349279, (-644440985473), 0, 0, 0], [1844642717664, 1009492874088, 0, 0], [4804349827759, 118123401185, 0], [19459224298600, 879451926185], [129843510779893]]], r := 20230813231896, ok := true }, Z3 := { p := [[[109634334815670953808]], [[(-4707886660411325090), 1091171258347338069], [(-4742526775541587018)]], [[224175961437879352, (-53310826185537720), 0], [204736608380098722, 10892134211614440], [204837983719117523]], [[(-11056504802017712), 2495687363785017, 0, 0], [(-9934735315888193), (-407541139032113), 0], [(-9061963186134970), (-147754424718454)], [(-9257953294454208)]], [[553355367355969, (-122722231715612), 0, 0, 0], [493872228640086, 17147659364305, 0, 0], [440987340524973, 6923089228575, 0], [413095789362469, 4108472174221], [425090246081494]]], r := 853505218988271, ok := true }, iE := { p := [[[46439969981630849820]], [[(-360537584976334232), 0], [(-1403945657216900972)]], [[5305420508777989, 0, 0], [9234216259824563, 0], [63323299335893062]], [[(-103009512472128), 0, 0, 0], [(-88313896683340), 0, 0], [(-440991343887628), 0], [(-2817811579506268)]], [[2513767900190, 0, 0, 0, 0], [1181038188427, 0, 0, 0], [4968771107593, 0, 0], [19253764581752, 0], [128642350420609]]], r := 20777036160611, ok := true }, iHu := { p := [[[122574963135981398429]], [[(-5023428473708475705), 0], [(-4613352679936355244)]], [[240794459301587212, 0, 0], [203064657792307487, 0], [203085705991550980]], [[(-11889784571724530), 0, 0, 0], [(-9824764090654546), 0, 0], [(-9022742532233757), 0], [(-9209229310052842)]], [[595375691022743, 0, 0, 0, 0], [488553722082190, 0, 0, 0], [439084723839145, 0, 0], [412045517374563, 0], [423503333939888]]], r := 867243208413220, ok := true }, T := { p := [[[14411518807585587200]], [[0, 576460752303423488], [0]]], r := 0, ok := true }, E := { p := [[[7327359751858923147]], [[56886095969333250, 0], [221516398622938651]], [[(-395459968007206), 0, 0], [1982506669546853, 0], [(-3294481222107850)]], [[6684003323635, 0, 0, 0], [(-19247742898153), 0, 0], [(-17676498579936), 0], [42952166730834]], [[(-173375583304), 0, 0, 0, 0], [317967719811, 0, 0, 0], [(-20262835930), 0, 0], [268173524623, 0], [(-1065835728404)]]], r := 1079115185671, ok := true }, de := { p := [[[(-50722274631921411694)]], [[705220801722999416, 0], [647651756684387218]], [[(-17879299666031356), 0, 0], [742412940357346, 0], [(-15079376019872343)]], [[618358760675248, 0, 0, 0], [851039109091, 0, 0], [781566528758, 0], [478949604897041]], [[(-24047019568555), 0, 0, 0, 0], [975558919, 0, 0, 0], [21606718115, 0, 0], [822785011, 0], [(-17105154127315)]]], r := 8681415135468, ok := true }, dde := { p := [[[(-628807489275081492074)]], [[31884021303755944082, 0], [29281244054469744557]], [[(-1654071826106654848), 0, 0], [(-1519804380425205536), 0], [(-1395041835845887558)]], [[85765740105837179, 0, 0, 0], [78762715492318884, 0, 0], [72333106064374521, 0], [66429829978532880]], [[(-4447113535691748), 0, 0, 0, 0], [(-4084086850687052), 0, 0, 0], [(-3750735258782430), 0, 0], [(-3444513066489507), 0], [(-3163326009396679)]]], r := 1292694475368835, ok := true }, nJu := { p := [[[(-101444549263842823387)]], [[1410441603445998832, 0], [1295303513368774437]], [[(-35758599332062711), 0, 0], [1484825880714693, 0], [(-30158752039744686)]], [[1236717521350496, 0, 0, 0], [1702078218183, 0, 0], [1563133057516, 0], [957899209794083]], [[(-48094039137109), 0, 0, 0, 0], [1951117838, 0, 0, 0], [43213436230, 0, 0], [1645570022, 0], [(-34210308254630)]]], r := 17362830270928, ok := true }, Jd1 := { p := [[[(-1257614978550162984147)]], [[63768042607511888165, 0], [58562488108939489115]], [[(-3308143652213309695), 0, 0], [(-3039608760850411071), 0], [(-2790083671691775115)]], [[171531480211674358, 0, 0, 0], [157525430984637768, 0, 0], [144666212128749042, 0], [132859659957065760]], [[(-8894227071383496), 0, 0, 0, 0], [(-8168173701374104), 0, 0, 0], [(-7501470517564859), 0, 0], [(-6889026132979014), 0], [(-6326652018793357)]]], r := 2585388950737661, ok := true }, term0 := { p := [[[35021571692476493157475]], [[(-3529184519067298443912), 0], [(-3018984165027477571909)]], [[272019391357934190974, 0, 0], [308526564172140915786, 0], [208257468139033858253]], [[(-18720502270312890956), 0, 0, 0], [(-23877956373200742231), 0, 0], [(-21380075440258273609), 0], [(-12988312103790074602)]], [[1210030566997749427, 0, 0, 0, 0], [1646738649387916582, 0, 0, 0], [1657269195865276816, 0, 0], [1336602506021419083, 0], [764742705973461045]]], r := 680027846650871715, ok := true }, r0 := { p := [[[677999766554831350806]], [[(-28159572090128632628), 46906370698064129627], [(-18761623308574656206)]], [[1178896955301315262, (-1789557706345550881), 446928269869365260], [602905755453845445, (-1496125438039129607)], [851835617087901103]], [[(-52653461824226277), 74140427218937317, (-7109749343053210), (-13264662882161688)], [(-20370125443146869), 48897636830774133, (-26880599854992536)], [(-28656185734732894), 65061831405473587], [(-37556381208311436)]], [[2479211306356944, (-3365768723483444), 304815477398039, 619351989804201, 102469187049155], [807892120562855, (-1728380413759489), 795597183569087, 262978113108795], [1018006159804860, (-2114769722881131), 1087549424763548], [1228140241915797, (-2896898804709720)], [1706900012716559]]], r := 20627610786341890, ok := true }, r1 := { p := [[[1023968076647039999752]], [[(-40849459740576822031), 0], [(-30450098565125188259)]], [[1706791683179089543, 0, 0], [977463248135646280, 0], [1357855364883665391]], [[(-76885987513389077), 0, 0, 0], [(-33654892133279314), 0, 0], [(-44821764708061806), 0], [(-60119904143899083)]], [[3648424404327303, 0, 0, 0, 0], [1366672460693387, 0, 0, 0], [1589653801286372, 0, 0], [1934320371258780, 0], [2734270625830480]]], r := 18369864991641608, ok := true }, r2 := { p := [[[3872100996739192721646]], [[(-194918107427572895355), 36476762417719733715], [(-338335732354666193952)]], [[9341185398681208010, (-1494878756200378690), 17072149999584459], [16797103045916363227, (-1116097331323229907)], [22583765764662368913]], [[(-457239945993331273), 67394848575012272, 607514866151361, (-131712799860215)], [(-803145487245342919), 41071115312410523, (-989338640559228)], [(-1105312307623465386), 55581305193436070], [(-1368050834579095015)]], [[22817437867066477, (-3202963480183774), (-18070953864512), (-2457659690515), 958198985633], [39446893144201446, (-1687620906505629), 41776899898993, (-5152809885052)], [52556111470502214, (-1966679967182180), (-22275188755804)], [66178977162355743, (-2531391859792419)], [78555578231703728]]], r := 1155955286638381812, ok := true }, r3 := { p := [[[54954992653062386946154]], [[(-5589539680164943077253), 639342956882481614853], [(-5320227858050100647399)]], [[431985440986426388320, (-62511203738988977420), (-19677646392140361)], [546858609771325621609, (-30628478889051509219)], [382318691910445034686]], [[(-29770332785410537983), 4784155291358927688, 6760480104499963, (-189864903249958)], [(-42407302422436229875), 3009144179975432860, (-3988367985008088)], [(-39415967134659779320), 1463292275591865449], [(-24347142077532982370)]], [[1925828550230345137, (-328027672704456853), (-459417524004019), (-27789205474498), 2909414474919], [2927455783379172453, (-229466637800324553), 10864311254216, 29861629501969], [3059664894324893082, (-143512797535074614), (-7230295818995)], [2513881952114111780, (-69832869758134462)], [1451859207405158011]]], r := 1143615516620385197338, ok := true }, eta := { p := [[[(-5790390728831102978630)]], [[303284991376580335131, 0], [413619781291745474791]], [[(-15041995854499215846), 0, 0], [(-21025933799240770977), 0], [(-26126065929499159040)]], [[752357552162287537, 0, 0, 0], [1022754775579699670, 0, 0], [1303678005394290790, 0], [1533256942357827454]], [[(-38067850275031257), 0, 0, 0, 0], [(-50793760442997230), 0, 0, 0], [(-62874002805033293), 0, 0], [(-75406949248467079), 0], [(-86337433968526239)]]], r := 129738858311920166, 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 := 3026418949592973312, bh := 144115188075855872, tc := 14411518807585587200, th := 576460752303423488, sc := 2684145377912815616, sh := 126100789566373888 }
noncomputable def q1 : Cert := { V0 := [[[4765598356073585288]], [[(-66692375351793398), 172735040890660263], [74797745896879797]], [[562385644566384, (-1929432077414577), (-956060403298443)], [(-969679053367929), 2163923079519817], [(-512631640436880)]], [[(-8302145842984), 6378297297198, 36298866829603, (-5843402127395)], [9113243258406, (-5865375727697), (-40710402098348)], [8834314225494, (-27272756763906)], [19459608834971]], [[171762725612, (-35198616581), (-685769417316), 37660408939, 150916696514], [(-171969307920), (-339488631458), 1379413645587, (-42237417447)], [(-86309803062), 570115715395, (-198561767691)], [(-268748644919), 679685263251], [(-595702719611)]]], r0 := 21440815508196, V1 := [[[5926243725927524411]], [[(-78425221037754617), 0], [87956527626225274]], [[575689649952849, 0, 0], [(-948187751627927), 0], [(-710529463539330)]], [[(-8108744566750), 0, 0, 0], [5900911926594, 0, 0], [12656284643935, 0], [24063597363695]], [[170795445233, 0, 0, 0, 0], [(-119726731970), 0, 0, 0], [(-122863571715), 0, 0], [(-318617745209), 0], [(-753102004193)]]], r1 := 16138015937904, V2 := [[[15237465074693156606]], [[(-30452284653157632), 19933294474988955], [(-155085000939133529)]], [[146734157348022, 21500497552770, (-107791240132671)], [(-1587495444756544), 2022535324258914], [(-234604591022864)]], [[(-2390785144494), (-2379932910277), 867932506393, 537076816443], [9741619599972, 1607519028160, (-16269755736389)], [(-4744842349994), 57013836897856], [(-4431953329607)]], [[57749820707, 21982582010, 12371289569, (-9630163982), (-2496129928)], [(-152029111088), (-257339473149), 146741966946, 105589359160], [128598544568, (-46727850475), (-848079029428)], [52844955169, 293455660738], [15625537520]]], r2 := 93125969402488, V3 := [[[17493005487559413437]], [[(-44339792007774487), 11215927007706047], [(-49318334200600641)]], [[25637136644270, 449414507805657, (-120551062013513)], [(-2269763481746093), 1174621740886916], [(-205183430222390)]], [[85480186348, (-4203389148396), (-3938246945676), 1245095807850], [2658750120987, 46749782149972, (-18885059298988)], [(-8256367498058), 35822300463828], [(-933842929467)]], [[(-1568016509), (-11541729099), 85303180780, 30642191349, (-12546648716)], [10013936598, (-465255816222), (-608554391453), 258796334562], [81665555741, 1389214272256, (-1062630108216)], [(-31668360802), 273940878285], [(-1389030553)]]], r3 := 1203450186702312, Vm := [[[15483502649004510959]], [[(-31489460245167240), 0], [(-128169512023923267)]], [[129583591170985, 0, 0], [(-1692979470389858), 0], [657212539781923]], [[(-2264233585679), 0, 0, 0], [7383541014632, 0, 0], [(-7456526217855), 0], [4216742378652]], [[57059155958, 0, 0, 0, 0], [(-130414669933), 0, 0, 0], [14007357167, 0, 0], [64200948091, 0], [57187099607]]], rm := 16734738697234 }
noncomputable def w1 : Wit := { Z0 := { p := [[[5009533149680022532]], [[(-77366506166445456), 200381325987200901], [86769143228777794]], [[817726342418623, (-3094660246657819), 0], [(-1495724409216568), 3470765729151111], [(-386719201746416)]], [[(-13515985667541), 32709053696744, 0, 0], [22196865256486, (-59828976368663), 0], [3259247925512, (-15468768069857)], [21270812444987]], [[283970666398, (-540639426702), 0, 0, 0], [(-459640680038), 887874610259, 0, 0], [67775408088, 130369917020, 0], [(-348482219259), 850832497799], [(-598469148717)]]], r := 5086447149200, ok := true }, Z1 := { p := [[[6412202431590428841]], [[(-99029127893050183), 0], [111064503332835577]], [[1046689718295838, 0, 0], [(-1914527243797207), 0], [(-495000578235412)]], [[(-17300461654453), 0, 0, 0], [28411987528302, 0, 0], [4171837344656, 0], [27226639929584]], [[363482452989, 0, 0, 0, 0], [(-588340070449), 0, 0, 0], [86752522352, 0, 0], [(-446057240652), 0], [(-766040510357)]]], r := 4269354706100, ok := true }, Z2 := { p := [[[35740645799235370857]], [[(-306124468576727637), 200381325987200901], [(-1559006624213687282)]], [[4004026362973358, (-3094660246657819), 0], [9800204546922293, 3470765729151111], [63232435234432437]], [[(-70939754490188), 32709053696744, 0, 0], [(-106802534562963), (-59828976368663), 0], [(-419272018870895), (-15468768069857)], [(-2822555697958903)]], [[1566606025481, (-540639426702), 0, 0, 0], [1565216549600, 887874610259, 0, 0], [4382654591022, 130369917020, 0], [18654561848669, 850832497799], [128115949709707]]], r := 19095418376648, ok := true }, Z3 := { p := [[[101034855765687827533]], [[(-3928144223183994102), 993639728288504666], [(-4369202488662524734)]], [[169181015109246526, (-44626521367813700), 0], [170218788904432694, 10139761702960469], [188318239701712841]], [[(-7554585860180071), 1885109062579104, 0, 0], [(-7480541019225038), (-347513188694811), 0], [(-7530357358494196), (-135009759066660)], [(-8505071661260093)]], [[342401693060365, (-83899289496992), 0, 0, 0], [336775754845709, 13113384987104, 0, 0], [331786430664686, 5868979956919, 0], [343107127115305, 3761031052698], [390329582078088]]], r := 596684391655180, ok := true }, iE := { p := [[[45739330455152146345]], [[(-340476967308326967), 0], [(-1385821364213153919)]], [[4742400030593093, 0, 0], [8894476415920003, 0], [62460570225634713]], [[(-85467934991846), 0, 0, 0], [(-81710733903527), 0, 0], [(-422035457187210), 0], [(-2780100614888703)]], [[1909038673984, 0, 0, 0, 0], [1026114597791, 0, 0, 0], [4521896134983, 0, 0], [18468822399074, 0], [126921446326754]]], r := 19518025484001, ok := true }, iHu := { p := [[[113404818691684034774]], [[(-4186018513843574510), 0], [(-4242971146684983710)]], [[181660708531749073, 0, 0], [168930350650042185, 0], [186637483923983561]], [[(-8122200740845064), 0, 0, 0], [(-7397100759953952), 0, 0], [(-7497741586619958), 0], [(-8458250048394895)]], [[368347075588419, 0, 0, 0, 0], [333120010156497, 0, 0, 0], [330356936123419, 0, 0], [342246163426501, 0], [388806002324483]]], r := 604182016840863, ok := true }, T := { p := [[[14411518807585587200]], [[0, 576460752303423488], [0]]], r := 0, ok := true }, E := { p := [[[7439600963433179214]], [[55379314668750557, 0], [225406840322148476]], [[(-359125998633981), 0, 0], [1909086089036242, 0], [(-3329915456859190)]], [[5486357901068, 0, 0, 0], [(-17519469381622), 0, 0], [(-17757829509264), 0], [43488425229540]], [[(-128953191638), 0, 0, 0, 0], [260934787112, 0, 0, 0], [(-20402842968), 0, 0], [268083354560, 0], [(-1078625582940)]]], r := 1023267760112, ok := true }, de := { p := [[[(-49378758722873965008)]], [[640426706026575135, 0], [649139994543943504]], [[(-14675671485892041), 0, 0], [745828839389102, 0], [(-15077726070539553)]], [[459922523389202, 0, 0, 0], [856919404659, 0, 0], [868578172069, 0], [478951435680708]], [[(-16205080975372), 0, 0, 0, 0], [984556814, 0, 0, 0], [21899771186, 0, 0], [1011529726, 0], [(-17105152094159)]]], r := 6616504078665, ok := true }, dde := { p := [[[(-571034076274253442207)]], [[26171015142841381909, 0], [26527083376077319102]], [[(-1230264591544275451), 0, 0], [(-1247766954287785173), 0], [(-1263968910957215000)]], [[57796799281739449, 0, 0, 0], [58581394539575942, 0, 0], [59378420315624600, 0], [60188093833172531]], [[(-2715286867393049), 0, 0, 0, 0], [(-2752232571766986), 0, 0, 0], [(-2789721761234107), 0, 0], [(-2827632714415261), 0], [(-2866100756708292)]]], r := 910395216879370, ok := true }, nJu := { p := [[[(-98757517445747930015)]], [[1280853412053150270, 0], [1298279989087887008]], [[(-29351342971784082), 0, 0], [1491657678778204, 0], [(-30155452141079105)]], [[919845046778405, 0, 0, 0], [1713838809319, 0, 0], [1737156344138, 0], [957902871361416]], [[(-32410161950743), 0, 0, 0, 0], [1969113629, 0, 0, 0], [43799542373, 0, 0], [2023059452, 0], [(-34210304188318)]]], r := 13233008157323, ok := true }, Jd1 := { p := [[[(-1142068152548506884414)]], [[52342030285682763818, 0], [53054166752154638205]], [[(-2460529183088550902), 0, 0], [(-2495533908575570346), 0], [(-2527937821914430000)]], [[115593598563478898, 0, 0, 0], [117162789079151885, 0, 0], [118756840631249201, 0], [120376187666345063]], [[(-5430573734786097), 0, 0, 0, 0], [(-5504465143533972), 0, 0, 0], [(-5579443522468213), 0, 0], [(-5655265428830521), 0], [(-5732201513416584)]]], r := 1820790433758732, ok := true }, term0 := { p := [[[28918731582055824292495]], [[(-2632278681845208657354), 0], [(-2485785061827663368782)]], [[183658397391449346466, 0, 0], [229827685484712716757, 0], [171316691186480085020]], [[(-11446522363515862700), 0, 0, 0], [(-16107660990597245269), 0, 0], [(-15918735643472543374), 0], [(-10679187721281024022)]], [[670158653179164496, 0, 0, 0, 0], [1006229745932710937, 0, 0, 0], [1117606159990728691, 0, 0], [994930691642940950, 0], [628592039629483801]]], r := 432340382276177483, ok := true }, r0 := { p := [[[626011138956628545739]], [[(-24005110287420868542), 43599239233810679906], [(-17631355558941757848)]], [[914087934547387568, (-1528793449471322506), 433793782244299715], [530089897023755972, (-1404718855334759697)], [798287362785034218]], [[(-36830898925908138), 57263149933673037, (-6084886314127966), (-12104502727479875)], [(-16267918516905814), 42749568796812252, (-25397518503560995)], [(-25033266403005084), 61108345413045162], [(-35257264292811957)]], [[1562462123420255, (-2339774913413261), 214249116498023, 543653088095844, 82247302604944], [576810521734714, (-1366496740355989), 692020728939492, 229396739216111], [805653990726324, (-1849162644112624), 1029922500728130], [1076780156350719, (-2724071584248823)], [1603331227930948]]], r := 16847595156295824, ok := true }, r1 := { p := [[[948534417706239808566]], [[(-34840923332888699888), 0], [(-28619761895854576786)]], [[1320631155569088303, 0, 0], [857475796761044581, 0], [1274086687113261329]], [[(-53629598313849349), 0, 0, 0], [(-26733425318881215), 0, 0], [(-39168644036696551), 0], [(-56498738984059673)]], [[2293335009086697, 0, 0, 0, 0], [970401949735665, 0, 0, 0], [1256177079562215, 0, 0], [1696054356302479, 0], [2571035169421306]]], r := 15131661942864907, ok := true }, r2 := { p := [[[3516303200971236119302]], [[(-162392246370430340083), 33733248857744682740], [(-307667258496169505016)]], [[7065451872914970809, (-1259262297156902500), 18221391920861159], [14001754252587372714, (-1040139904156430530)], [20564613683760528727]], [[(-312864534313791928), 51406421677085704, 544679307382117, (-136257340602698)], [(-606970840437241774), 35144175984333428, (-910171196202500)], [(-922362918324475394), 51946588477041172], [(-1247108040720358475)]], [[14115428290073100, (-2205376898662442), (-13628976198611), (-2100149613429), 968599567110], [26946643897343985, (-1299693450246294), 37588149393198, (-5941958707599)], [39732169287224121, (-1680600726933160), (-20357968500584)], [55271457442828074, (-2371012652195189)], [71673955927529391]]], r := 984696407207740302, ok := true }, r3 := { p := [[[45293090179756223674801]], [[(-4165569910969271074517), 531134026471594784731], [(-4375416947855745535381)]], [[291496438744096893403, (-46725494344647633624), (-7776552459087750)], [407115531389869504781, (-25416750074042910084)], [314229560034600421466]], [[(-18195154610664126038), 3235080040911409995, 5237166067723198, (-238605518089495)], [(-28595726922368998551), 2251833857277289541, (-3979190112018170)], [(-29334582292937482064), 1214763769814268517], [(-20004858777063088950)]], [[1066235609759440417, (-200791684356527458), (-313599219261487), (-21393065823183), 3144407080879], [1788266687254601961, (-155240229391845641), (-496898351813), 27741030199041], [2062727099377027408, (-107366351416735576), (-16132025732027)], [1870616192217464474, (-57976026013231548)], [1192703005463735740]]], r := 644851979850697782708, ok := true }, eta := { p := [[[(-5238522608853627145863)]], [[251065374511065781098, 0], [375289816441886520039]], [[(-11307036046158507399), 0, 0], [(-17471692749869628958), 0], [(-23747587864047017429)]], [[512002566509378725, 0, 0, 0], [770481923795867662, 0, 0], [1085075143496351680, 0], [1395597225849405359]], [[(-23440718037499366), 0, 0, 0, 0], [(-34601416888022778), 0, 0, 0], [(-47413659890154756), 0, 0], [(-62841845963801395), 0], [(-78669466239396995)]]], r := 111368537196501149, 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 := 3026418949592973312, bh := 144115188075855872, tc := 14411518807585587200, th := 576460752303423488, sc := 3062447746611937280, sh := 252201579132747776 }
noncomputable def q2 : Cert := { V0 := [[[4570371463008386947]], [[(-127050593600603837), 167003265103043020], [71966387735382577]], [[1983528987334343, (-3784053819307201), (-853066519762612)], [(-1838492875032450), 2143434962829822], [(-486872078211952)]], [[(-52642208303154), 24409774283526, 64898164883320, (-5686964948240)], [31030092891747, (-15483530840360), (-36760839638341)], [16698431549175, (-25624029895919)], [18673312150004]], [[1912701906394, (-215285501279), (-2401274599655), 130071043532, 127865564985], [(-1055236327630), (-1151317884033), 2511633676396, (-73677287818)], [(-303228281557), 1059985617089, (-196671463767)], [(-511450422491), 657568266260], [(-570297472808)]]], r0 := 44511116286188, V1 := [[[5695943156990806174]], [[(-150346461407972153), 0], [85162071499974740]], [[2043423232511655, 0, 0], [(-1831424741311543), 0], [(-673620728634360)]], [[(-51234166479766), 0, 0, 0], [19878614671432, 0, 0], [23927664208934, 0], [23129996498596]], [[1884172655946, 0, 0, 0, 0], [(-714570860125), 0, 0, 0], [(-434192677021), 0, 0], [(-608191298910), 0], [(-722015072659)]]], r1 := 36649129026528, V2 := [[[15147368587797444947]], [[(-59261589888309840), 19976935652459045], [(-159763648029407520)]], [[511780207122544, 15538694823341, (-105081817225258)], [(-3065596396002630), 2025108591704431], [(-247726384191763)]], [[(-14580496301987), (-8815786506069), 1873045228905, 508160832904], [34175660098281, 258060699424, (-15814520207117)], [(-8034121569822), 56803968852724], [(-4268785004801)]], [[618286051770, 139317242334, 42171013643, (-19269790096), (-2285627154)], [(-931929222357), (-945090121090), 312899901417, 99394034970], [458147755905, (-184703321265), (-818126435526)], [111690306649, 274503240797], [15381470742]]], r2 := 192302135536148, V3 := [[[17360219034395733935]], [[(-88367635939358844), 12526048762194903], [(-56103440516257627)]], [[105319995030065, 847818588368431, (-131602529431609)], [(-4507120633366932), 1310650527255479], [(-229208368085713)]], [[554419076204, (-17176853531124), (-6862092422339), 1326025412628], [10957000876217, 87851701721732, (-20586412912274)], [(-15514803718029), 39839398684013], [(-1021698666083)]], [[(-18552546155), (-70228986002), 334632225829, 46781010852, (-13013606051)], [63784325766, (-1901985330737), (-1051931994406), 274996947856], [338099561992, 2577042165453, (-1154294807793)], [(-53750173764), 297790954248], [(-1036618706)]]], r3 := 5695498389915772, Vm := [[[15390143640076419896]], [[(-61535066695863164), 0], [(-133185267515345458)]], [[447580550136505, 0, 0], [(-3303739608077863), 0], [634957290877147]], [[(-13636569116101), 0, 0, 0], [25476868031270, 0, 0], [(-14767611760767), 0], [4394048214076]], [[606826393044, 0, 0, 0, 0], [(-778140171555), 0, 0, 0], [41984179310, 0, 0], [108292606458, 0], [59075938274]]], rm := 48239980072147 }
noncomputable def w2 : Wit := { Z0 := { p := [[[4784449635905845647]], [[(-145594079473588554), 191377985436233825], [82470137906719556]], [[2838819645500242, (-5823763178943543), 0], [(-2747795506091574), 3298805516268782], [(-376398195090326)]], [[(-85258658545543), 113552785820009, 0, 0], [74289110755117, (-109911820243663), 0], [7202016255948, (-15055927803614)], [20263189914234]], [[3188375057162, (-3410346341822), 0, 0, 0], [(-2819798302409), 2971564430204, 0, 0], [189244786461, 288080650237, 0], [(-647902727153), 810527596569], [(-572739097542)]]], r := 9974395551789, ok := true }, Z1 := { p := [[[6124095533959482428]], [[(-186360421726193349), 0], [105561776520601032]], [[3633689146240309, 0, 0], [(-3517178247797215), 0], [(-481789689715618)]], [[(-109131082938294), 0, 0, 0], [95090061766550, 0, 0], [9218580807613, 0], [25936883090220]], [[4081120073167, 0, 0, 0, 0], [(-3609341827084), 0, 0, 0], [242233326670, 0, 0], [(-829315490756), 0], [(-733106044853)]]], r := 9356479856904, ok := true }, Z2 := { p := [[[34856511033397083552]], [[(-567722892233322419), 191377985436233825], [(-1530527285952783501)]], [[13761721955255170, (-5823763178943543), 0], [18397235247127241, 3298805516268782], [62012413805952865]], [[(-442077349791776), 113552785820009, 0, 0], [(-376759572294470), (-109911820243663), 0], [(-789190496136426), (-15055927803614)], [(-2768252171516350)]], [[17379022034803, (-3410346341822), 0, 0, 0], [10043080087334, 2971564430204, 0, 0], [15449320419787, 288080650237, 0], [35140352233548, 810527596569], [125651925302984]]], r := 44051003613584, ok := true }, Z3 := { p := [[[90593470860000019970]], [[(-6170975768072607272), 874731371497200002], [(-3917870702899791851)]], [[464741073943187447, (-70462644721499130), 0], [266031264577406674, 9201923645097960], [168357488715737312]], [[(-36341064368461071), 5185295399422761, 0, 0], [(-20484335242156282), (-563276739636091), 0], [(-11762262928139691), (-119238674315815)], [(-7595898934496719)]], [[2885370946320094, (-403937280772489), 0, 0, 0], [1615568226065034, 36668420610856, 0, 0], [907559087703001, 9428440346648, 0], [535559579212391, 3333187978639], [348368373134524]]], r := 2718558921022410, ok := true }, iE := { p := [[[44758416963707888975]], [[(-628284744572627147), 0], [(-1359846934030239690)]], [[16257342972658498, 0, 0], [16860400549613419, 0], [61233419396198245]], [[(-531078982319976), 0, 0, 0], [(-293250528895699), 0, 0], [(-793226052174384), 0], [(-2726315435706027)]], [[21120962943467, 0, 0, 0, 0], [6794075223804, 0, 0, 0], [15892890968307, 0, 0], [34819122449081, 0], [124466583393665]]], r := 48678442080581, ok := true }, iHu := { p := [[[102288649782429797058]], [[(-6562842269819726924), 0], [(-3794840768263107406)]], [[498766420774129739, 0, 0], [264288405733768487, 0], [166763264847660071]], [[(-39058801635942474), 0, 0, 0], [(-20253500179098675), 0, 0], [(-11711207586553718), 0], [(-7551334133161700)]], [[3103294898492658, 0, 0, 0, 0], [1597860075732792, 0, 0, 0], [903672850538031, 0, 0], [534246797499641, 0], [346920058816035]]], r := 2807336225431722, ok := true }, T := { p := [[[14411518807585587200]], [[0, 576460752303423488], [0]]], r := 0, ok := true }, E := { p := [[[7602645267746053432]], [[106720173861269984, 0], [230983009659319330]], [[(-1263408276657418), 0, 0], [3620828639436250, 0], [(-3383373206092233)]], [[33710720779127, 0, 0, 0], [(-61846816833514), 0, 0], [(-35761764835704), 0], [44292450343164]], [[(-1389208077519), 0, 0, 0, 0], [1602682925205, 0, 0, 0], [(-82461128937), 0, 0], [535859324106, 0], [(-1097810794958)]]], r := 3462392917906, ok := true }, de := { p := [[[(-47578321865116935840)]], [[1126513262843817654, 0], [651385220011731296]], [[(-45087057081241635), 0, 0], [1501994123099630, 0], [(-15074921903464798)]], [[2477364369205642, 0, 0, 0], [3463367415345, 0, 0], [2002627417037, 0], [478954943262937]], [[(-153010228860047), 0, 0, 0, 0], [7985992535, 0, 0, 0], [89387755115, 0, 0], [2670128005, 0], [(-17105147700070)]]], r := 58348487487895, ok := true }, dde := { p := [[[(-502225667984574378766)]], [[40201705753418391923, 0], [23245884279187505541]], [[(-3313399006127773798), 0, 0], [(-1917455039236685802), 0], [(-1107839688059288492)]], [[272861996151619875, 0, 0, 0], [157770224033158044, 0, 0], [91227680563390731, 0], [52753080455143459]], [[(-22471002116141973), 0, 0, 0, 0], [(-12993461226559598), 0, 0, 0], [(-7513404913403376), 0, 0], [(-4344382311161694), 0], [(-2512053037426401)]]], r := 5028824308909907, ok := true }, nJu := { p := [[[(-95156643730233871680)]], [[2253026525687635308, 0], [1302770440023462592]], [[(-90174114162483270), 0, 0], [3003988246199261, 0], [(-30149843806929595)]], [[4954728738411284, 0, 0, 0], [6926734830690, 0, 0], [4005254834074, 0], [957909886525875]], [[(-306020457720093), 0, 0, 0, 0], [15971985070, 0, 0, 0], [178775510230, 0, 0], [5340256011, 0], [(-34210295400140)]]], r := 116696974975784, ok := true }, Jd1 := { p := [[[(-1004451335969148757531)]], [[80403411506836783847, 0], [46491768558375011082]], [[(-6626798012255547595), 0, 0], [(-3834910078473371603), 0], [(-2215679376118576983)]], [[545723992303239751, 0, 0, 0], [315540448066316089, 0, 0], [182455361126781462, 0], [105506160910286918]], [[(-44942004232283945), 0, 0, 0, 0], [(-25986922453119195), 0, 0, 0], [(-15026809826806751), 0, 0], [(-8688764622323387), 0], [(-5024106074852801)]]], r := 10057648617819801, ok := true }, term0 := { p := [[[22412181179385179559061]], [[(-3559493334116294566672), 0], [(-1918188163633570214955)]], [[434759154869917998066, 0, 0], [310201921134674545262, 0], [132016134223786202140]], [[(-47465327033547808782), 0, 0, 0], [(-38081048974741163551), 0, 0], [(-21470141552027362333), 0], [(-8223309157838725042)]], [[4869283542029503791, 0, 0, 0, 0], [4168462069739245439, 0, 0, 0], [2640926967742598553, 0, 0], [1341394214850585356, 0], [483815776927883482]]], r := 1914764430192938486, ok := true }, r0 := { p := [[[561340041790131608126]], [[(-38740329446341115888), 39472272821483013030], [(-16173573219725535593)]], [[2606433858472317227, (-2478089087865925433), 417187007915272695], [891836351800444498, (-1287550066476753538)], [729722837100617732]], [[(-183319035551743704), 162613026506193415, (-10133455738278986), (-10611414473273602)], [(-48386064090868492), 71450424944930596, (-23503345967518242)], [(-41778465343003854), 56039067292263324], [(-32300971455285185)]], [[13536875710234750, (-11550451176742790), 532990448594110, 911985236103265, 58233219739303], [2964078280316642, (-4010307343442547), 1154676879595425, 187724735229529], [2367460019212312, (-3092084892865125), 955942793964208], [1805713015841228, (-2501758521498084)], [1469990993734195]]], r := 43106835209907928, ok := true }, r1 := { p := [[[854613422705789965457]], [[(-56305420275975994774), 0], [(-26264554871497724717)]], [[3756493607197176688, 0, 0], [1439244616688624548, 0], [1166764502542053723]], [[(-265910003848211122), 0, 0, 0], [(-78967674418042037), 0, 0], [(-65425739503660118), 0], [(-51841242650953676)]], [[19794770005098144, 0, 0, 0, 0], [4946718442685110, 0, 0, 0], [3684980910131810, 0, 0], [2845656601603590, 0], [2360790831224089]]], r := 41341568192842545, ok := true }, r2 := { p := [[[3085273833544452921709]], [[(-254292699526866959302), 30365550187067673200], [(-270484112036896852715)]], [[19471805900394176074, (-2002690271874202358), 19747266612338366], [21950141708963297728, (-945124421728233847)], [18113240291700982059]], [[(-1509309865197913145), 143400869355613463, 953650613814712, (-141903254570558)], [(-1671540991314224392), 57153945407596819, (-804611869371966)], [(-1448356830328168296), 47406362076271011], [(-1100122553078315832)]], [[119047904041573811, (-10737987715882274), (-37403672356892), (-3366213835619), 976623472694], [129734328326403127, (-3681013603794608), 66136444274413, (-6971821838479)], [109490946232391614, (-2729149510530015), (-17760165755236)], [86902014187623180, (-2170421000127326)], [63303646022168882]]], r := 2004946829858669374, ok := true }, r3 := { p := [[[35002416923597600509435]], [[(-5625970525288814253553), 415464119892474784264], [(-3370412195300988264785)]], [[689446441706731235566, (-63384791686784441352), 5550661827215723], [548980926009289512226, (-19837461066549549589)], [241829838943177519684]], [[(-75401713176948327383), 7676026746891662920, 7553107670744961, (-293151728468039)], [(-67563853553094329997), 3060415033509482975, (-3993444927657375)], [(-39538338389475135910), 948804308828940242], [(-15388550815431849834)]], [[7743192615563244318, (-834035167722395488), (-747013943734351), (-31042441225768), 3412818140611], [7404806770634826312, (-368608258261851306), (-15647094843366), 25184513364164], [4872101190752037386, (-145844230155419548), (-27686766833948)], [2520699682666051651, (-45285235738487563)], [917223043849171713]]], r := 2709969022950619253713, ok := true }, eta := { p := [[[(-4574933682107842732604)]], [[389781670655457154445, 0], [328987239860512705354]], [[(-30894720945063146447), 0, 0], [(-27275431540790710435), 0], [(-20868694472778104421)]], [[2450963124525874866, 0, 0, 0], [2112508541115940683, 0, 0], [1697937431669418787, 0], [1228718889053034316]], [[(-196376641904293131), 0, 0, 0, 0], [(-165929825167620975), 0, 0, 0], [(-130202654401339107), 0, 0], [(-98516443080672469), 0], [(-69363316537731312)]]], r := 308004128881572787, 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 := 3026418949592973312, bh := 144115188075855872, tc := 14411518807585587200, th := 576460752303423488, sc := 3566850904877432832, sh := 252201579132747776 }
noncomputable def q3 : Cert := { V0 := [[[4323811349565859184]], [[(-119693131257277634), 159531187419212600], [68405720253940206]], [[1707594964852755, (-3688779398053840), (-732356714521871)], [(-1725783719754066), 2108171195215734], [(-454626483285769)]], [[(-40199884112373), 23273184487660, 56056136232776, (-5375013270468)], [25603783181341, (-19635782481456), (-32036595027445)], [15575855025996, (-23598184938158)], [17681376131666]], [[1260096348599, (-169088809509), (-2034012926690), 177765427303, 102017404954], [(-774667911312), (-934297895974), 2219057570849, (-101594569073)], [(-260108894709), 968420652742, (-190231421978)], [(-481251007955), 628986184858], [(-538324560731)]]], r0 := 35706949333132, V1 := [[[5403041671024689184]], [[(-142733489726009674), 0], [81573496043637042]], [[1775206091253912, 0, 0], [(-1759555046678889), 0], [(-627418752128088)]], [[(-39039883900046), 0, 0, 0], [16262128308249, 0, 0], [22313066942965, 0], [21948089238102]], [[1228199432692, 0, 0, 0, 0], [(-507630229825), 0, 0, 0], [(-375939019736), 0, 0], [(-574575781507), 0], [(-682697228324)]]], r1 := 28518211033300, V2 := [[[15030784882178925258]], [[(-57371843955531889), 19973790886843824], [(-165765029984526773)]], [[437005848575990, (-18196623458636), (-101178459535164)], [(-2938974788005219), 2021969985042762], [(-262045338286279)]], [[(-10648682330823), (-8084121394262), 2024864617800, 469778419936], [29380472597685, (-3337735434773), (-15167014806080)], [(-6323814357377), 56324395870027], [(-4038685078286)]], [[388191228737, 106928060167, 33989662126, (-19077409999), (-2020854605)], [(-685437100575), (-856532916410), 333719375092, 91257792832], [399563125595, (-292485167157), (-776657544612)], [118127269525, 248375067629], [15364303977]]], r2 := 164463153320728, V3 := [[[17183909201188311670]], [[(-87940247023998428), 14152464061658500], [(-65073378769071703)]], [[108249586246530, 778361596122015, (-144003244623995)], [(-4462596626145323), 1478690988122062], [(-258869477869116)]], [[429171510155, (-17530244934861), (-5546717270769), 1401501715084], [11289004439805, 80164280147419, (-22475111785324)], [(-14138985476259), 44721063613650], [(-1116104286801)]], [[(-13225248710), (-48769423237), 322509442838, 29003398816, (-13254056305)], [47741716800, (-1938798052182), (-838191902867), 289648983978], [349100919350, 2304035399189, (-1253457747101)], [(-40611862395), 322850298751], [(-330224479)]]], r3 := 3435038765106840, Vm := [[[15268763552771337715]], [[(-59891152407234408), 0], [(-139696543932800895)]], [[378201754526950, 0, 0], [(-3210152891061675), 0], [605572948724202]], [[(-9792566459568), 0, 0, 0], [21541955864673, 0, 0], [(-14624044788821), 0], [4585747180130]], [[377847492303, 0, 0, 0, 0], [(-551542757071), 0, 0, 0], [30952846667, 0, 0], [83790351507, 0], [61523716154]]], rm := 39913891439658 }
noncomputable def w3 : Wit := { Z0 := { p := [[[4503981587714754495]], [[(-135169973490407219), 180159263508590179], [77250877274171957]], [[2393960066832721, (-5406798939616289), 0], [(-2481085118786503), 3090035090966878], [(-361347348229103)]], [[(-64452592865632), 95758402673308, 0, 0], [59825902238658, (-99243404751461), 0], [7799229152010, (-14453893929165)], [19023622245855]], [[2112760183166, (-2578103714626), 0, 0, 0], [(-2056800811564), 2393036089546, 0, 0], [114578282161, 311969166080, 0], [(-593480444947), 760944889834], [(-540321235689)]]], r := 8054064483204, ok := true }, Z1 := { p := [[[5765096432274885754]], [[(-173017566067721241), 0], [98881122910940105]], [[3064268885545883, 0, 0], [(-3175788952046723), 0], [(-462524605733252)]], [[(-82499318868009), 0, 0, 0], [76577154865483, 0, 0], [9983013314573, 0], [24350236474694]], [[2704333034452, 0, 0, 0, 0], [(-2632705038802), 0, 0, 0], [146660201167, 0, 0], [(-759654969532), 0], [(-691611181682)]]], r := 7268260991380, ok := true }, Z2 := { p := [[[33772830441159672004]], [[(-517481594341035465), 180159263508590179], [(-1495164632827029385)]], [[11471105149654578, (-5406798939616289), 0], [17000663978108752, 3090035090966878], [60492734557841111]], [[(-329443908583529), 95758402673308, 0, 0], [(-323800432787083), (-99243404751461), 0], [(-731937998839538), (-14453893929165)], [(-2700556801884478)]], [[11351024770102, (-2578103714626), 0, 0, 0], [7760378016384, 2393036089546, 0, 0], [13271649990300, 311969166080, 0], [32617633691260, 760944889834], [122577290832099]]], r := 34231821738991, ok := true }, Z3 := { p := [[[79859552588793936888]], [[(-4671252327691964881), 751757391272259569], [(-3456599024140268081)]], [[301094741879330229, (-53715868629719165), 0], [200047637537109768, 8203089549776001], [147968048822656016]], [[(-20190231545256769), 3365395041419081, 0, 0], [(-13220539177212254), (-443780520059178), 0], [(-8840662528282974), (-102618249293085)], [(-6667901700670650)]], [[1375244978890401, (-224676723577864), 0, 0, 0], [894560279385080, 24249448163516, 0, 0], [584970543470036, 7336132838580, 0], [402196872928455, 2885294676512], [305558089639836]]], r := 1405930242669891, ok := true }, iE := { p := [[[43562937828383133036]], [[(-569021947312562970), 0], [(-1327247786467296578)]], [[13510169425595323, 0, 0], [15763023136947287, 0], [59707289663283654]], [[(-394405679208033), 0, 0, 0], [(-256788744559351), 0, 0], [(-734422312895623), 0], [(-2659205987931574)]], [[13749975199161, 0, 0, 0, 0], [5439389901876, 0, 0, 0], [13610787087477, 0, 0], [32350906786549, 0], [121402818242021]]], r := 37039279748519, ok := true }, iHu := { p := [[[90888361387144108146]], [[(-4953831608482211361), 0], [(-3336253940406387230)]], [[322917009628060577, 0, 0], [199052698278779035, 0], [146462567049128663]], [[(-21690513050508162), 0, 0, 0], [(-13069688715701172), 0, 0], [(-8802035257513044), 0], [(-6625572401772377)]], [[1478651398483252, 0, 0, 0, 0], [884661086657944, 0, 0, 0], [582505175943905, 0, 0], [401247781495414, 0], [304184610213030]]], r := 1448600555838640, ok := true }, T := { p := [[[14411518807585587200]], [[0, 576460752303423488], [0]]], r := 0, ok := true }, E := { p := [[[7811281421411157071]], [[102031469570030895, 0], [237989136932959534]], [[(-1089770164707239), 0, 0], [3390787716858387, 0], [(-3455228108468363)]], [[24843323856666, 0, 0, 0], [(-53593980411372), 0, 0], [(-36093905175005), 0], [45363702116351]], [[(-879274001993), 0, 0, 0, 0], [1180389770071, 0, 0, 0], [(-83612589009), 0, 0], [535378783677, 0], [(-1123392138839)]]], r := 2352254299959, ok := true }, de := { p := [[[(-45487989045860847898)]], [[971689489989845766, 0], [654403125911528781]], [[(-33227185148375928), 0, 0], [1515944017350250, 0], [(-15070555862799411)]], [[1568002748154218, 0, 0, 0], [3511728738366, 0, 0], [2365041803390, 0], [478961272602557]], [[(-83148641067997), 0, 0, 0, 0], [8135022528, 0, 0, 0], [91830621971, 0, 0], [3689729085, 0], [(-17105138505909)]]], r := 28727905306847, ok := true }, dde := { p := [[[(-433201649088262122896)]], [[29626895318149181460, 0], [19952807050998428318]], [[(-2097155675572139577), 0, 0], [(-1413935758749927675), 0], [(-951188059432761297)]], [[148278349415844516, 0, 0, 0], [99853675636026239, 0, 0], [67248393795691133, 0], [45293024530231519]], [[(-10484340211495076), 0, 0, 0, 0], [(-7060907387886560), 0, 0, 0], [(-4755488995748731), 0, 0], [(-3202552330449160), 0], [(-2156813258247119)]]], r := 2469178524040970, ok := true }, nJu := { p := [[[(-90975978091721695796)]], [[1943378979979691533, 0], [1308806251823057562]], [[(-66454370296751855), 0, 0], [3031888034700500, 0], [(-30141111725598822)]], [[3136005496308436, 0, 0, 0], [7023457476733, 0, 0], [4730083606780, 0], [957922545205114]], [[(-166297282135993), 0, 0, 0, 0], [16270045056, 0, 0, 0], [183661243942, 0, 0], [7379458171, 0], [(-34210277011817)]]], r := 57455810613687, ok := true }, Jd1 := { p := [[[(-866403298176524245791)]], [[59253790636298362920, 0], [39905614101996856637]], [[(-4194311351144279154), 0, 0], [(-2827871517499855349), 0], [(-1902376118865522594)]], [[296556698831689033, 0, 0, 0], [199707351272052479, 0, 0], [134496787591382267, 0], [90586049060463039]], [[(-20968680422990151), 0, 0, 0, 0], [(-14121814775773119), 0, 0, 0], [(-9510977991497461), 0, 0], [(-6405104660898319), 0], [(-4313626516494237)]]], r := 4938357048081928, ok := true }, term0 := { p := [[[16717534002908268718525]], [[(-2265388346700131075525), 0], [(-1422479428030072077914)]], [[237146412085015077993, 0, 0], [196937304449974130027, 0], [97721816422714215165]], [[(-22208896769276952298), 0, 0, 0], [(-20736306303280992748), 0, 0], [(-13617477837409338419), 0], [(-6081189474372179172)]], [[1955044452630466040, 0, 0, 0, 0], [1947883281181681445, 0, 0, 0], [1437148423946254290, 0, 0], [850358530774550080, 0], [357569331148477305]]], r := 828424637573251657, ok := true }, r0 := { p := [[[493006530110328691609]], [[(-30150881433630488006), 35086164810855402244], [(-14562564170296433894)]], [[1764523293500852451, (-1943001897553325422), 398698849573768914], [728376819898682051, (-1158889503482976462)], [654576396923258704]], [[(-106310654081955356), 109791610386987113, (-8502282091695613), (-8968525695138411)], [(-34501815561507078), 58000591716632407, (-21419785874205439)], [(-33833173033729899), 50468964017322304], [(-29044289839428411)]], [[6692645000877752, (-6638676208856706), 309393480198633, 740178386105795, 34962508082114], [1794911536911423, (-2817545242413736), 942536980365699, 144470885272672], [1665520012066348, (-2512143747619442), 874160728452655], [1470239548298553, (-2256537081346686)], [1322864898878867]]], r := 26690761506432177, ok := true }, r1 := { p := [[[755175894991040995529]], [[(-43939333704756913533), 0], [(-23667171371565599119)]], [[2537779709150670993, 0, 0], [1173425798173187315, 0], [1048997184287714224]], [[(-153535893773943959), 0, 0, 0], [(-55903375544825679), 0, 0], [(-53068074866168964), 0], [(-46706213034185203)]], [[9741301638014138, 0, 0, 0, 0], [2965977127094077, 0, 0, 0], [2588693453690325, 0, 0], [2319754852949738, 0], [2128584604997910]]], r := 25014420566097356, ok := true }, r2 := { p := [[[2644143816592404563173]], [[(-191344822638757404292), 26859349290405078287], [(-232373754507384107657)]], [[12661912933343791635, (-1535762663952632341), 21525210284439342], [16547285482839462061, (-843713488903999522)], [15595907610529269080]], [[(-842256879333072603), 94686329649481123, 833037963288473, (-147758916311592)], [(-1086730527581744699), 45050936423932927, (-680964355290714)], [(-1094277684044091141), 42566589512281638], [(-948958335276028481)]], [[56888206760242611, (-6064702746112140), (-24190917075728), (-2529686368690), 976115450522], [72259788920719211, (-2482025138170620), 58089284866401, (-8121479915786)], [71263234781075669, (-2149113632642961), (-14684547613220)], [65769363245637335, (-1956264039050802)], [54685444861492315]]], r := 1384500589895043044, ok := true }, r3 := { p := [[[26008441160345397630071]], [[(-3574811520719184738177), 313866192046979375378], [(-2493632767001013770639)]], [[375642943973332892943, (-40504093648762356723), 18215922477002549], [348098391741805168030, (-14925758313358112830)], [178700868628100166852]], [[(-35250212149735572614), 4200174944692730179, 5338242464873990, (-346039048346698)], [(-36760998452880724996), 1961184085722942117, (-4027623672743107)], [(-25055241062796428009), 714828213337865691], [(-11364451975716249113)]], [[3106828922348675457, (-391150830213825441), (-401722994992872), (-22839037660868), 3694276346398], [3458114951709215040, (-201896262657167045), (-15904213519397), 22103843519403], [2649759352224509944, (-93378650593666109), (-40252859674141)], [1596857891036246073, (-34117920476319882)], [677122232299169333]]], r := 964154724332170838078, ok := true }, eta := { p := [[[(-3902046917918741515372)]], [[290391391024923988698, 0], [281741442161137816681]], [[(-19884455650065405434), 0, 0], [(-20464266019634294574), 0], [(-17923357685858025622)]], [[1354740717900066503, 0, 0, 0], [1366215513952298938, 0, 0], [1277721828296803164, 0], [1057634639332282644]], [[(-93050105706906050), 0, 0, 0, 0], [(-91968305483864786), 0, 0, 0], [(-84385835943078175), 0, 0], [(-74308334324500397), 0], [(-59807830559192133)]]], r := 205608748855698273, 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

noncomputable def c4 : Cell := { bc := 3026418949592973312, bh := 144115188075855872, tc := 14411518807585587200, th := 576460752303423488, sc := 4071254063142928384, sh := 252201579132747776 }
noncomputable def q4 : Cert := { V0 := [[[4090952597415583570]], [[(-113308349438536455), 152245424411296451], [65050782370241556]], [[1493199059478335, (-3597607589452247), (-627967031415786)], [(-1631856806426444), 2065401089281017], [(-424468520910755)]], [[(-31771694135561), 22335725006578, 48529758735862, (-4989691395797)], [21542609479666, (-23021986373242), (-27861131060950)], [14603995106528, (-21741482288313)], [16745610598731]], [[878403699570, (-145892267594), (-1739378804333), 204684616372, 80935225522], [(-591102631761), (-765576488350), 1961771510540, (-117510267339)], [(-227227593020), 890206460978, (-180704624228)], [(-455110849409), 601310917495], [(-508236801129)]]], r0 := 30209612956484, V1 := [[[5124381420301661423]], [[(-136065352586938876), 0], [78115670055404088]], [[1567017585221279, 0, 0], [(-1700017010140476), 0], [(-584233509232660)]], [[(-30859319608705), 0, 0, 0], [13637467217856, 0, 0], [20901642619765, 0], [20828674938223]], [[848876656807, 0, 0, 0, 0], [(-376544859442), 0, 0, 0], [(-331667878949), 0, 0], [(-545503399723), 0], [(-645505008925)]]], r1 := 23724717914408, V2 := [[[14917709748876549411]], [[(-55740387500489843), 19905868484433399], [(-171530581806879029)]], [[381256156013132, (-49344397463722), (-97002347334353)], [(-2828973410697262), 2011966968610462], [(-273159489597232)]], [[(-8105753701518), (-7511240280930), 2146642099848, 431976719886], [25779510574175, (-6618584118093), (-14482881996660)], [(-4820958355914), 55642588893374], [(-3797339432277)]], [[259023817964, 85383684311, 27075762507, (-18696340881), (-1775177155)], [(-525573082014), (-786395666459), 349670383283, 83336200030], [353566789897, (-387392329475), (-734002573354)], [122967727470, 221694189183], [15611951392]]], r2 := 146533528336452, V3 := [[[17008464939335459912]], [[(-87502492066992548), 15638710338267618], [(-73953059942218658)]], [[110536324476218, 707722861002359, (-153825728979285)], [(-4416918766511018), 1631231109468043], [(-285740252684430)]], [[337408601897, (-17773420722202), (-4285714786895), 1443304551612], [11537993755229, 72361452920485, (-23945607585167)], [(-12726951007351), 49054263563744], [(-1184073294691)]], [[(-9960152078), (-33034819812), 307600415023, 13121494743, (-13126141892)], [35786675723, (-1960439922268), (-634069035804), 297124681834], [356371401116, 2029085257148, (-1327409474843)], [(-27362299288), 340322627113], [637870523]]], r3 := 2271678741489468, Vm := [[[15150421274369432164]], [[(-58484958022398415), 0], [(-146034767649081519)]], [[327352462787822, 0, 0], [(-3129963563348964), 0], [576439832557841]], [[(-7326386593372), 0, 0, 0], [18696846944354, 0, 0], [(-14512745649758), 0], [4730547170879]], [[250185289448, 0, 0, 0, 0], [(-406856176597), 0, 0, 0], [25409838998, 0, 0], [61303092658, 0], [63832950833]]], rm := 35626690430555 }
noncomputable def w4 : Wit := { Z0 := { p := [[[4242733278798421357]], [[(-126305826736669754), 169709331151936854], [72512686733623530]], [[2052216081232070, (-5052233069466791), 0], [(-2264244395182979), 2900507469344941], [(-345363546980039)]], [[(-50308897561071), 82088643249282, 0, 0], [49098007465577, (-90569775807320), 0], [8151452002041, (-13814541879202)], [17883024406876]], [[1474487330463, (-2012355902443), 0, 0, 0], [(-1551627640338), 1963920298623, 0, 0], [64750304024, 326058080081, 0], [(-548463252232), 715320976275], [(-509809893389)]]], r := 6879768739247, ok := true }, Z1 := { p := [[[5430698596861979337]], [[(-161671458222937285), 0], [92816239019038118]], [[2626836583977050, 0, 0], [(-2898232825834213), 0], [(-442065340134450)]], [[(-64395388878170), 0, 0, 0], [62845449555939, 0, 0], [10433858562612, 0], [22890271240801]], [[1887343782993, 0, 0, 0, 0], [(-1986083379632), 0, 0, 0], [82880389151, 0, 0], [(-702032962856), 0], [(-652556663538)]]], r := 6041029569513, ok := true }, Z2 := { p := [[[32781284492192224221]], [[(-475219852289060910), 169709331151936854], [(-1462399911529236924)]], [[9735054929480787, (-5052233069466791), 0], [15791727460369707, 2900507469344941], [59079541202344011]], [[(-253922747947872), 82088643249282, 0, 0], [(-282241393858820), (-90569775807320), 0], [(-682389887796468), (-13814541879202)], [(-2637560067060798)]], [[7820386058939, (-2012355902443), 0, 0, 0], [6182536470737, 1963920298623, 0, 0], [11567590274994, 326058080081, 0], [30428265091310, 715320976275], [119713221582460]]], r := 28648201630214, ok := true }, Z3 := { p := [[[71579252155851611989]], [[(-3671629196388648226), 656204687609211790], [(-3103091210685129277)]], [[206710231685773127, (-42533623428436966), 0], [156228828357295688, 7401567198156574], [132347300374419079]], [[(-12130365177442115), 2314522479055739, 0, 0], [(-9044635424411511), (-362587724378523), 0], [(-6902904219011092), (-89452824879483)], [(-5957518910334148)]], [[723356127964326, (-135145099185291), 0, 0, 0], [535809684105454, 16943380386021, 0, 0], [399722501602457, 5913830050018, 0], [313796929811087, 2533098113048], [272802170215568]]], r := 813654232146380, ok := true }, iE := { p := [[[42475983201330311239]], [[(-519313898496582185), 0], [(-1296707513662622275)]], [[11434922936928323, 0, 0], [14796937215320691, 0], [58290381169630626]], [[(-303053172668728), 0, 0, 0], [(-227227877856583), 0, 0], [(-683667640274043), 0], [(-2596697132193035)]], [[9445058572615, 0, 0, 0, 0], [4463565824187, 0, 0, 0], [11836136750825, 0, 0], [30205650551457, 0], [118548299587472]]], r := 30534326664206, ok := true }, iHu := { p := [[[82119642739529402381]], [[(-3882103978683124211), 0], [(-2984202378171381186)]], [[221539973520937127, 0, 0], [155736776632312451, 0], [130910450362758419]], [[(-13025842154879773), 0, 0, 0], [(-8940141913000772), 0, 0], [(-6872353987544832), 0], [(-5916830625104756)]], [[777498919915862, 0, 0, 0, 0], [529842357479726, 0, 0, 0], [398080155764036, 0, 0], [313089780307202, 0], [271483993710702]]], r := 836251957186224, ok := true }, T := { p := [[[14411518807585587200]], [[0, 576460752303423488], [0]]], r := 0, ok := true }, E := { p := [[[8011171049485703549]], [[97945054020576009, 0], [244565161537667224]], [[(-959198414558666), 0, 0], [3189364193563084, 0], [(-3527751925914982)]], [[19062338984030, 0, 0, 0], [(-47392142096840), 0, 0], [(-36430694264917), 0], [46433909836629]], [[(-591292325983), 0, 0, 0, 0], [905067940951, 0, 0, 0], [(-84785587400), 0, 0], [534814778010, 0], [(-1148975118081)]]], r := 1816648296270, ok := true }, de := { p := [[[(-43666170478180062705)]], [[855265677503629622, 0], [657449126244286716]], [[(-25495294850149578), 0, 0], [1530089159126548, 0], [(-15065455131730297)]], [[1054447180291154, 0, 0, 0], [3560994670798, 0, 0], [2737363250341, 0], [478969827418396]], [[(-48987107338433), 0, 0, 0, 0], [8287545187, 0, 0, 0], [94341634401, 0, 0], [4897203225, 0], [(-17105124135751)]]], r := 16361851937545, ok := true }, dde := { p := [[[(-381297220686244019551)]], [[22732784262576908775, 0], [17474861371912861863]], [[(-1410290824644104095), 0, 0], [(-1085688683887953543), 0], [(-833356635655540038)]], [[87358341946437147, 0, 0, 0], [67145621597447117, 0, 0], [51615341772187244, 0], [39681466030464235]], [[(-5411589890831135), 0, 0, 0, 0], [(-4159955440683662), 0, 0, 0], [(-3197978038127983), 0, 0], [(-2458164238145653), 0], [(-1889597526445909)]]], r := 1395292824779743, ok := true }, nJu := { p := [[[(-87332340956360125409)]], [[1710531355007259245, 0], [1314898252488573433]], [[(-50990589700299156), 0, 0], [3060178318253097, 0], [(-30130910263460593)]], [[2108894360582309, 0, 0, 0], [7121989341596, 0, 0], [5474726500683, 0], [957939654836793]], [[(-97974214676866), 0, 0, 0, 0], [16575090374, 0, 0, 0], [188683268803, 0, 0], [9794406450, 0], [(-34210248271502)]]], r := 32723703875080, ok := true }, Jd1 := { p := [[[(-762594441372488039101)]], [[45465568525153817551, 0], [34949722743825723726]], [[(-2820581649288208189), 0, 0], [(-2171377367775907086), 0], [(-1666713271311080076)]], [[174716683892874294, 0, 0, 0], [134291243194894234, 0, 0], [103230683544374488, 0], [79362932060928471]], [[(-10823179781662270), 0, 0, 0, 0], [(-8319910881367323), 0, 0, 0], [(-6395956076255966), 0, 0], [(-4916328476291305), 0], [(-3779195052891817)]]], r := 2790585649559479, ok := true }, term0 := { p := [[[12984408866009860056952]], [[(-1531784256319764136645), 0], [(-1098315887222407961130)]], [[140239595081302901147, 0, 0], [132840278161228193928, 0], [75317313049744927447]], [[(-11495797201547572238), 0, 0, 0], [(-12241758550725567464), 0, 0], [(-9176463659687729448), 0], [(-4682439277219462712)]], [[886102743804046391, 0, 0, 0, 0], [1006964373268762261, 0, 0, 0], [847887486823608902, 0, 0], [572750766732214361, 0], [275158981925880194]]], r := 415490263781751193, ok := true }, r0 := { p := [[[439007152459260981738]], [[(-24184393424513536980), 31592217835801236163], [(-13230930111039971883)]], [[1258279110415166544, (-1571848666935401901), 382757666180939876], [609045658661755471, (-1053065910241321535)], [592928092106867665]], [[(-66453515597024322), 78282507285659474, (-7512938482909472), (-7621460598886332)], [(-25783571917233222), 48311796402706595, (-19691401575259700)], [(-28103401278246489), 45883492542662063], [(-26359287672096166)]], [[3647470629351333, (-4121789166718738), 197433043266784, 612686315129137, 18799289650489], [1170794944172682, (-2081153884565435), 793863997097116, 111535470156489], [1231243335357726, (-2094374375283302), 806076326882174], [1226770487690976, (-2053910149830195)], [1201362945444362]]], r := 18216664380513708, ok := true }, r1 := { p := [[[676357899384454587313]], [[(-35362915253858969561), 0], [(-21522682474381148560)]], [[1807891801235583843, 0, 0], [980587148098958249, 0], [952212451253922057]], [[(-95634328656842789), 0, 0, 0], [(-41556602159558889), 0, 0], [(-44165442203605117), 0], [(-42466660625996502)]], [[5286754446558431, 0, 0, 0, 0], [1917909612727229, 0, 0, 0], [1912567621169085, 0, 0], [1938658742598946, 0], [1936534143854632]]], r := 16927877637936641, ok := true }, r2 := { p := [[[2306164563662389710522]], [[(-149250745283694979907), 24123701359019931648], [(-203116891165324294042)]], [[8716308052227690392, (-1218829160994868979), 23106009514446460], [12933901228980455131, (-762474675141946531)], [13659112332524907282]], [[(-508342367822695801), 66123171620446555, 752818833399092, (-152145272370566)], [(-748423221612507089), 36660024505274069, (-570504844923805)], [(-857185420360991538), 38691547153748257], [(-832456858109592639)]], [[30028796572764270, (-3703092557591904), (-16563244195063), (-1880315188490), 965539134466], [43561761640794029, (-1770267324496227), 52701192508668, (-9071146270103)], [49142418298390324, (-1748726755190318), (-11940724168746)], [51606080500890486, (-1784548352970224)], [48034718768692200]]], r := 1027521742883215834, ok := true }, r3 := { p := [[[20121871991232068084943]], [[(-2413374236828434937077), 246998997380312119851], [(-1920988398646018721419)]], [[221889823268197620539, (-27492386963089197924), 27555840075300831], [234509974792943354850, (-11683343202953985049)], [137495002397157372821]], [[(-18230692688796059278), 2491624679750014054, 4116749531949863, (-387228355461296)], [(-21684521635609404458), 1335433911964391020, (-4050559156216716)], [(-16869271297821073246), 560522349327400997], [(-8738639974940574955)]], [[1407177828352759236, (-202947471588078991), (-227279509110851), (-18817242432481), 3940454139930], [1786604428485824943, (-119894964606711792), (-5875242656503), 18842407874652], [1562382684866969600, (-63514993994894472), (-50158832538332)], [1074803799358886393, (-26750789568175424)], [520479904642899986]]], r := 410740935539088517348, ok := true }, eta := { p := [[[(-3391271919884974981177)]], [[224574096994757973812, 0], [245630363598119746996]], [[(-13563858792648754070), 0, 0], [(-15931699503535252593), 0], [(-15665670659185254067)]], [[810524720459900813, 0, 0, 0], [936535479572206560, 0, 0], [997478813538625906, 0], [926194527721311806]], [[(-48728572309194239), 0, 0, 0, 0], [(-55194335047014400), 0, 0, 0], [(-57971547278570975), 0, 0], [(-58138027582268211), 0], [(-52454041730984334)]]], r := 152272199262154914, ok := true } }
theorem sB_4 : stageB c4 w4 = true := by decide +kernel
theorem s0_4 : stageC0 w4 q4 = true := by decide +kernel
theorem s1_4 : stageC1 w4 q4 = true := by decide +kernel
theorem s2_4 : stageC2 w4 q4 = true := by decide +kernel
theorem s3_4 : stageC3 w4 q4 = true := by decide +kernel
theorem sE_4 : stageE w4 q4 = true := by decide +kernel
theorem sF_4 : stageF w4 = true := by decide +kernel
theorem ok_4 : (domOK c4 && cellCheck c4 q4) = true :=
  staged_check c4 q4 w4 (by decide +kernel) sB_4 s0_4 s1_4 s2_4 s3_4 sE_4 sF_4

theorem region : RegionPosI 2882303761517117440 3170534137668829184 13835058055282163712 14987979559889010688 2305843009213693952 4323455642275676160 :=
  (RegionPosI.split_s 3314649325744685056 (RegionPosI.split_s 2810246167479189504 (RegionPosI.split_s 2558044588346441728 (RegionPosI.of_check c0 q0 ok_0 2882303761517117440 3170534137668829184 13835058055282163712 14987979559889010688 2305843009213693952 2558044588346441728 (by decide +kernel)) (RegionPosI.of_check c1 q1 ok_1 2882303761517117440 3170534137668829184 13835058055282163712 14987979559889010688 2558044588346441728 2810246167479189504 (by decide +kernel))) (RegionPosI.of_check c2 q2 ok_2 2882303761517117440 3170534137668829184 13835058055282163712 14987979559889010688 2810246167479189504 3314649325744685056 (by decide +kernel))) (RegionPosI.split_s 3819052484010180608 (RegionPosI.of_check c3 q3 ok_3 2882303761517117440 3170534137668829184 13835058055282163712 14987979559889010688 3314649325744685056 3819052484010180608 (by decide +kernel)) (RegionPosI.of_check c4 q4 ok_4 2882303761517117440 3170534137668829184 13835058055282163712 14987979559889010688 3819052484010180608 4323455642275676160 (by decide +kernel))))

end CKLaneC.RSC2.BA_0131

end