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

import Definitions.Def_CK_CKLaneC_RSCell_Staged
import Definitions.Def_CK_CKLaneC_RSCell_RegionI

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

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

namespace CKLaneC.RSC2.S02_0051
open CKLaneC.TM3 CKLaneC.RSCell

noncomputable def c0 : Cell := { bc := 3448068464705536, bh := 70368744177664, tc := 2305843009213693952, th := 2305843009213693952, sc := 3602879701896396800, sh := 144115188075855872 }
noncomputable def q0 : Cert := { V0 := [[[218413842047697794]], [[(-3600420745206411), 218369669551121931], [452402073087331]], [[27286835199148, (-3598236353352393), (-66242942296005)], [(-7564646110868), 452127598665276], [(-3679004190489)]], [[(-271135792354), 27234275029799, 3275285372830, (-22054649912405)], [64987426035, (-7551008334251), (-411547982163)], [61296905298, (-3677340590888)], [45622452031]], [[3606510845, (-270227773303), (-78787448606), 1089591890612, 19736312770], [(-812083630), 64653575547, 20443138787, (-136910007197)], [(-510946348), 61214512532, 2494746442], [(-759281000), 45603626091], [(-658952538)]]], r0 := 836523247645, V1 := [[[1736303042273711118]], [[(-28263046328428707), 0], [3551324041160484]], [[205457831983869, 0, 0], [(-57185053804312), 0], [(-29017942519684)]], [[(-1951414322368), 0, 0, 0], [439997024662, 0, 0], [470033380921, 0], [360289590771]], [[25523211950, 0, 0, 0, 0], [(-5102195052), 0, 0, 0], [(-3602141363), 0, 0], [(-5843868622), 0], [(-5207532492)]]], r1 := 223969513829, V2 := [[[18442734061064391106]], [[(-30155990767145), 83665082580], [(-81598692708825)]], [[46647913847, (-176432845), (-1668828)], [(-622389298863), 3428552449], [2863469282]], [[(-717582019), (-7126676), 19638, 32], [1050309722, (-7019464), (-102683)], [(-85837349), 35296774], [(-16177092)]], [[14859724, 24233, 109, (-1), 0], [(-16129086), (-296123), 1204, 2], [1214451, (-67488), (-2112)], [452705, 2661], [148268]]], r2 := 604540203, V3 := [[[18445396782628962724]], [[(-53887998007223), 55634939813], [(-27503753472295)]], [[149303497, 1704361424, (-2204999)], [(-1100001180807), 2281346210], [(-164505562)]], [[65275, (-21339562), (-46615), 86], [6113730, 69956252, (-135674)], [(-5056528), 23520322], [(-13647)]], [[(-953), (-9272), 1499, 1, 0], [2920, (-874035), (-2873), 7], [62828, 722775, (-2791)], [(-517), 2085], [50]]], r3 := 8868019727, Vm := [[[18442734673677008224]], [[(-30157795744571), 0], [(-81573529473103)]], [[46603060281, 0, 0], [(-622462926114), 0], [3123841869]], [[(-717486386), 0, 0, 0], [1048450521, 0, 0], [(-86587208), 0], [(-16146674)]], [[14858427, 0, 0, 0, 0], [(-16124898), 0, 0, 0], [1194824, 0, 0], [452723, 0], [148155]]], rm := 101428853 }
noncomputable def w0 : Wit := { Z0 := { p := [[[218435932247472880]], [[(-3601513266832997), 218435932247472880], [452539351223344]], [[27313128490741, (-3601513266832997), 0], [(-7571468382127), 452539351223344], [(-3679836153550)]], [[(-271590166213), 27313128490741, 0, 0], [65154489472, (-7571468382127), 0], [61338115118, (-3679836153550)], [45631866724]], [[3613606226, (-271590166213), 0, 0, 0], [(-815085819), 65154489472, 0, 0], [(-511943611), 61338115118, 0], [(-759747043), 45631866724], [(-659081116)]]], r := 161854565739, ok := true }, Z1 := { p := [[[1747487457979783045]], [[(-28812106134663975), 0], [3620314809786757]], [[218505027925932, 0, 0], [(-60571747057009), 0], [(-29438689228399)]], [[(-2172721329698), 0, 0, 0], [521235915777, 0, 0], [490704920950, 0], [365054933796]], [[28908849809, 0, 0, 0, 0], [(-6520686545), 0, 0, 0], [(-4095548886), 0, 0], [(-6077976338), 0], [(-5272648922)]]], r := 56933585872, ok := true }, Z2 := { p := [[[11613855962574329732542]], [[(-78732390537944842274), 218435932247472880], [(-213040924151508408587)]], [[687834032351650707, (-3601513266832997), 0], [1438344019922892171, 452539351223344], [4151949120164143802]], [[(-7762238353391920), 27313128490741, 0, 0], [(-12218352460937669), (-7571468382127), 0], [(-27991067557730637), (-3679836153550)], [(-82306070950727778)]], [[116770213790692, (-271590166213), 0, 0, 0], [132835902086518, 65154489472, 0, 0], [235342743748395, 61338115118, 0], [554397286953297, 45631866724], [1644655959575035]]], r := 263437870481101, ok := true }, Z3 := { p := [[[31210365160005258405727]], [[(-1137136890958894167990), 1174000609189559927], [(-580380304887061833893)]], [[43656525200661016314, (-54171867502394780), 0], [21348193053778864359, 2135827057181803], [11368026036831126716]], [[(-1701365200998043795), 2057436003928151, 0, 0], [(-822522955900229981), (-90935953925422), 0], [(-419648338013807314), (-17908104312424)], [(-226034726133388003)]], [[66776151247545969, (-79940756680918), 0, 0, 0], [32124004850485051, 3266393009154, 0, 0], [16191376762348129, 776337782517, 0], [8361985949965516, 224285180868], [4526285078643065]]], r := 31594766779673984, ok := true }, iE := { p := [[[11617980796440556283541]], [[(-78758232028289659311), 0], [(-213032378626866375523)]], [[688063945276921022, 0, 0], [1438288403981047717, 0], [4151879631996001528]], [[(-7764869584649412), 0, 0, 0], [(-12217735586454205), 0, 0], [(-27990619648705294), 0], [(-82305209261593999)]], [[116810268574055, 0, 0, 0, 0], [132827132057943, 0, 0, 0], [235338020610703, 0, 0], [554391749215468, 0], [1644643513819996]]], r := 263354243580096, ok := true }, iHu := { p := [[[31220862777102963111489]], [[(-1137507965446882627464), 0], [(-580361206860657324761)]], [[43670793668662249068, 0, 0], [21347586081350673848, 0], [11367865907082857374]], [[(-1701921507142684223), 0, 0, 0], [(-822500524448003615), 0, 0], [(-419643124720165403), 0], [(-226032720631916352)]], [[66797989885223403, 0, 0, 0, 0], [32123152387120232, 0, 0, 0], [16191182704333806, 0, 0], [8361920131822312, 0], [4526255941424162]]], r := 31593845594552934, ok := true }, T := { p := [[[2305843009213693952]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[29289286398647864]], [[198551921762039, 0], [537061169157649]], [[(-388647882030), 0, 0], [3655500564501, 0], [(-619227508335)]], [[5181782572, 0, 0, 0], [(-7931879004), 0, 0], [(-4046877043), 0], [4211748035]], [[(-103635651), 0, 0, 0, 0], [105750666, 0, 0, 0], [(-5910), 0, 0], [27527766, 0], [(-42977021)]]], r := 98135626, ok := true }, de := { p := [[[(-135965244025176290546)]], [[532279956307874434, 0], [271571406279527773]], [[(-10645210464086243), 0, 0], [396593950251, 0], [(-2771035626844608)]], [[283872279420693, 0, 0, 0], [579173, 0, 0], [295496, 0], [37701165041338]], [[(-8516168382620), 0, 0, 0, 0], [1, 0, 0, 0], [5911, 0, 0], [1, 0], [(-577058648592)]]], r := 1467449621829, ok := true }, dde := { p := [[[(-364496971406031505405203)]], [[14579346556851848789130, 0], [7438442120842780012126]], [[(-583173863051426443580), 0, 0], [(-297537685626928060383), 0], [(-151804941444040581791)]], [[23326954522055948016, 0, 0, 0], [11901507409211062994, 0, 0], [6072197657760768294, 0], [3098060029470093373]], [[(-933078180882226343), 0, 0, 0, 0], [(-476060296368479147), 0, 0, 0], [(-242887906310439160), 0, 0], [(-123922401178786286), 0], [(-63225714887134276)]]], r := 78012813736996496, ok := true }, nJu := { p := [[[(-271930488050352581092)]], [[1064559912615748869, 0], [543142812559055547]], [[(-21290420928172486), 0, 0], [793187900502, 0], [(-5542071253689215)]], [[567744558841387, 0, 0, 0], [1158346, 0, 0], [590993, 0], [75402330082676]], [[(-17032336765240), 0, 0, 0, 0], [3, 0, 0, 0], [11822, 0, 0], [2, 0], [(-1154117297183)]]], r := 2934899243651, ok := true }, Jd1 := { p := [[[(-728993942812063010810406)]], [[29158693113703697578261, 0], [14876884241685560024253]], [[(-1166347726102852887159), 0, 0], [(-595075371253856120765), 0], [(-303609882888081163581)]], [[46653909044111896033, 0, 0, 0], [23803014818422125988, 0, 0], [12144395315521536588, 0], [6196120058940186746]], [[(-1866156361764452685), 0, 0, 0, 0], [(-952120592736958294), 0, 0, 0], [(-485775812620878320), 0, 0], [(-247844802357572571), 0], [(-126451429774268552)]]], r := 156025627473992984, ok := true }, term0 := { p := [[[9986667700386143092316656494]], [[(-798889672668348265245271964), 0], [(-407558686945906727386393060)]], [[47932505599314479080871978, 0, 0], [32603802342621114520018352, 0], [12475670007017082629213956]], [[(-2556376971675584834758660), 0, 0, 0], [(-1956210288295987279923529), 0, 0], [(-998035383968395054155956), 0], [(-339465628380571612489108)]], [[127818148775142986196254, 0, 0, 0, 0], [104330739315489138294953, 0, 0, 0], [59881758706242807608462, 0, 0], [27156878503241271768204, 0], [8659709110486278990860]]], r := 17972524732843972659331, ok := true }, r0 := { p := [[[3167675559780139387264]], [[(-81871542241486108899), 6333331913952564107197], [(-57597794173567137520)]], [[1906182839092520577, (-163626605220052319242), 3162628989848219514468], [1450263549738638171, (-115167144066288702196)], [1119157399570488698]], [[(-50476681110582584), 3808589035666075156, (-81580474432532603105), (-4034079975810520294)], [(-32487613593271544), 2898908765137917983, (-57526697855390469180)], [(-27910278231009163), 2237810766120060892], [(-22145578013240755)]], [[1564767483734667, (-100852469093877555), 1896747362294196875, 232567606599467773, (-1004913097887053670)], [832923110904298, (-64924081650699051), 1446218995757982689, 56845415836851136], [616118195670561, (-55791982408812296), 1117897551192869726], [549087572319741, (-44281732959169508)], [441954556804300]]], r := 365401948827695137, ok := true }, r1 := { p := [[[198750221308557332862477]], [[(-5012989336245514789598), 0], [(-3629816755557717711463)]], [[114756002337104731616, 0, 0], [89634278969498925137, 0], [70624628348069724504]], [[(-3039735381432268965), 0, 0, 0], [(-1979755484766512415), 0, 0], [(-1729953386143551418), 0], [(-1398580676730279286)]], [[95130738649875384, 0, 0, 0, 0], [50772029252897725, 0, 0, 0], [37682604305956331, 0, 0], [34090007861838549, 0], [27925945820082995]]], r := 55126506030422793, ok := true }, r2 := { p := [[[995820749213669921992218315]], [[(-30555635929330312473135851), 52399363271812752214107], [(-39613040294899834412838767)]], [[984584759289302545568871, (-1108842149742958906636), 448826314424465932], [1193509274346929182915535, (-1042622945545138844746)], [1193814499023990244431727]], [[(-35146917755461750148008), 29368880436465709002, 181032979112008, (-22692311988926)], [(-38057420098916273779724), 21109124579089902634, 41914252434819], [(-35560315198116548176386), 21061265188707540263], [(-32126427484657873981635)]], [[1327222496799432463608, (-950437118438025296), (-18943748974313), (-3331779548827), (-3527704230178)], [1353270164605124866979, (-541405639932969379), (-5555071043300), (-29528650622608)], [1126399030204860305390, (-418618860103928449), (-11079929159999)], [949086466886253250492, (-427163732549325504)], [812597693633649561104]]], r := 4784515675287240927550, ok := true }, r3 := { p := [[[19961131623938500550428292813]], [[(-1596882189607748953018263458), 1106052030936258051355553], [(-814868081294774615323706736)]], [[95812762576202912302867567, (-81344670669878426127244), 1617198779938009745], [65189281321464872119372673, (-22606579770514921684116)], [24946250618741948224539634]], [[(-5110009413709360458311159), 4738171445745769138083, 12205847796479701, (-2453401816440405)], [(-3911353541276743527488226), 1662101286055620620114, (-6209848476822292)], [(-1995696717798497728357357), 461613312746880738939], [(-678827372553534227679103)]], [[255500329679784950746746, (-248921420533982401981), (-2061226532931111), (-5861629431140569), (-640397469243446)], [208605429205381087968844, (-96804136114685095039), (-3115730254372320), (-5833327631255585)], [119741735633544629160421, (-33940443899631757875), (-2971438024085481)], [54306118042825084889092, (-9425463022419459730)], [17317296974034489668277]]], r := 1671898506291953200016369, ok := true }, eta := { p := [[[(-996871413754017177521341502)]], [[30595316608013907855537018, 0], [39634116218360022598076424]], [[(-986099842020289249027624), 0, 0], [(-1194299756651794318790887), 0], [(-1194241703410769680530238)]], [[35206187869994293102862, 0, 0, 0], [38087563111904898624232, 0, 0], [35576294248132645317581, 0], [32135109986599110109565]], [[(-1329568200277006362826), 0, 0, 0, 0], [(-1354449822964509419554), 0, 0, 0], [(-1127008099157560963386), 0, 0], [(-949410713290556961357), 0], [(-812774378777361609155)]]], r := 375327651262919826879, 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 := 3588805953060864, bh := 70368744177664, tc := 2305843009213693952, th := 2305843009213693952, sc := 3602879701896396800, sh := 144115188075855872 }
noncomputable def q1 : Cert := { V0 := [[[219304284933104217]], [[(-3615310754016087), 219259569995469004], [438213233231412]], [[27414815018649, (-3613099408923063), (-67056279141353)], [(-7328232356239), 437945195226124], [(-3420297916017)]], [[(-272736214963), 27361594946910, 3315688389570, (-22325221150010)], [63016092883, (-7314913361361), (-401895889025)], [56991173883, (-3418741396569)], [40737856357]], [[3632322472, (-271816339050), (-79776205811), 1103014849156, 20141754280], [(-788616554), 62689955704, 19965174532, (-133696862108)], [(-475387012), 56914081242, 2334165455], [(-678038955), 40720941963], [(-565219233)]]], r0 := 764559010478, V1 := [[[1743292420109199720]], [[(-28375581742050605), 0], [3439415382534757]], [[206323764733461, 0, 0], [(-55372443746486), 0], [(-26974967983906)]], [[(-1961461334194), 0, 0, 0], [426104507139, 0, 0], [436897870279, 0], [321689282695]], [[25685211124, 0, 0, 0, 0], [(-4946681708), 0, 0, 0], [(-3348894610), 0, 0], [(-5217335731), 0], [(-4466452561)]]], r1 := 197069366906, V2 := [[[18442570875005753149]], [[(-31401109157775), 90663395713], [(-81587428344033)]], [[48753341281, (-190741450), (-1882762)], [(-622727345371), 3569771178], [2769834340]], [[(-749912190), (-7731494), 22145, 38], [1055093252, (-7289003), (-111309)], [(-83217400), 35312516], [(-15055544)]], [[15529985, 26371, 123, (-1), 0], [(-16200713), (-308699), 1304, 3], [1177756, (-67283), (-2200)], [421201, 2587], [132519]]], r2 := 551903755, V3 := [[[18445341774463887513]], [[(-56088020599051), 60291730086], [(-27504411656713)]], [[161782298, 1847165641, (-2487665)], [(-1100021413058), 2375452289], [(-164586259)]], [[71260, (-23123592), (-52601), 101], [6365085, 72848267, (-147071)], [(-5059584), 23532662], [(-13258)]], [[(-1039), (-10121), 1691, 1, 0], [3063, (-909998), (-3115), 8], [62849, 723229, (-2907)], [(-503), 2029], [47]]], r3 := 8630666999, Vm := [[[18442571538986573612]], [[(-31403064388994), 0], [(-81561223256518)]], [[48704690758, 0, 0], [(-622803971842), 0], [3030386773]], [[(-749807984), 0, 0, 0], [1053155474, 0, 0], [(-83967151), 0], [(-15026003)]], [[15528572, 0, 0, 0, 0], [(-16196327), 0, 0, 0], [1158095, 0, 0], [421219, 0], [132413]]], rm := 98039431 }
noncomputable def w1 : Wit := { Z0 := { p := [[[219326646434619313]], [[(-3616416758975442), 219326646434619313], [438347292525948]], [[27441438535693, (-3616416758975442), 0], [(-7334895184529), 438347292525948], [(-3421076329191)]], [[(-273196524929), 27441438535693, 0, 0], [63179297560, (-7334895184529), 0], [57029732831, (-3421076329191)], [40746315109]], [[3639516528, (-273196524929), 0, 0, 0], [(-791551212), 63179297560, 0, 0], [(-476320266), 57029732831, 0], [(-678457695), 40746315109], [(-565330188)]]], r := 143638103929, ok := true }, Z1 := { p := [[[1754613171476954511]], [[(-28931334071803536), 0], [3506778340207591]], [[219531508285545, 0, 0], [(-58679161476226), 0], [(-27368610633528)]], [[(-2185572199425), 0, 0, 0], [505434380487, 0, 0], [456237862655, 0], [325970520874]], [[29116132229, 0, 0, 0, 0], [(-6332409695), 0, 0, 0], [(-3810562124), 0, 0], [(-5427661556), 0], [(-4522641503)]]], r := 50090737303, ok := true }, Z2 := { p := [[[11203748761076475855902]], [[(-75963401897063804999), 219326646434619313], [(-197370690885647435001)]], [[664303056088649202, (-3616416758975442), 0], [1332695187683358879, 438347292525948], [3695094183317539664]], [[(-7506277873638774), 27441438535693, 0, 0], [(-11329763701462129), (-7334895184529), 0], [(-24913638700769544), (-3421076329191)], [(-70370137643688921)]], [[113041694009882, (-273196524929), 0, 0, 0], [123306784578276, 63179297560, 0, 0], [209619801786824, 57029732831, 0], [474044844636170, 40746315109], [1350913066224200]]], r := 224675841125314, ok := true }, Z3 := { p := [[[30093337997658963158890]], [[(-1096054781690261538254), 1178202374618058788], [(-537482720765294122144)]], [[42073761188085349813, (-54350710101296108), 0], [19764834689518652086, 2066785730111118], [10113584401700397127]], [[(-1639551677637231392), 2063858740105345, 0, 0], [(-761434957358785877), (-87943593582325), 0], [(-373246641150482548), (-16636694291259)], [(-193190785032436104)]], [[64346433477725232, (-80183057522922), 0, 0, 0], [29736209987567096, 3157690777269, 0, 0], [14399598587912487, 720898560631, 0], [7145239893494087, 200138076319], [3716674562221008]]], r := 28362601859523892, ok := true }, iE := { p := [[[11207890414739731531298]], [[(-75989352870719309268), 0], [(-197362413356676920723)]], [[664534184317168071, 0, 0], [1332641299383641723, 0], [3695029581439284555]], [[(-7508926393774021), 0, 0, 0], [(-11329165055453834), 0, 0], [(-24913222197121253), 0], [(-70369368210845352)]], [[113082054621418, 0, 0, 0, 0], [123298262813217, 0, 0, 0], [209615404606872, 0, 0], [474039898800665, 0], [1350902390814342]]], r := 224602471284873, ok := true }, iHu := { p := [[[30103873185882489684559]], [[(-1096427049781573665737), 0], [(-537464240089008371272)]], [[42088073761854510978, 0, 0], [19764247810026676755, 0], [10113435640579598596]], [[(-1640109659806836679), 0, 0, 0], [(-761413273765384833), 0, 0], [(-373241800861557772), 0], [(-193188995448277946)]], [[64368336691211850, 0, 0, 0, 0], [29735386071215814, 0, 0, 0], [14399418450567813, 0, 0], [7145181193380445, 0], [3716649585512069]]], r := 28361518244102927, ok := true }, T := { p := [[[2305843009213693952]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[30360964849676438]], [[205846951217817, 0], [534633465606429]], [[(-404511663680), 0, 0], [3639634667329, 0], [(-594948019700)]], [[5393283900, 0, 0, 0], [(-7931902644), 0, 0], [(-3888187571), 0], [3887891967]], [[(-107865678), 0, 0, 0, 0], [105750666, 0, 0, 0], [(-5910), 0, 0], [25411060, 0], [(-38116587)]]], r := 98581967, ok := true }, de := { p := [[[(-135432892687167110532)]], [[532280749496956922, 0], [260921936027920061]], [[(-10645210462904256), 0, 0], [396595132239, 0], [(-2557960991662883)]], [[283872279420695, 0, 0, 0], [602816, 0, 0], [295498, 0], [33437398632112]], [[(-8516168382620), 0, 0, 0, 0], [1, 0, 0, 0], [5911, 0, 0], [1, 0], [(-491726450472)]]], r := 1458699517144, ok := true }, dde := { p := [[[(-350203494390287749781974)]], [[14007607474635661292832, 0], [6866474252272383007092]], [[(-560304299794511227851), 0, 0], [(-274658970884115719067), 0], [(-134636750238973272944)]], [[22412171991779250019, 0, 0, 0], [10986358819498426286, 0, 0], [5385470009558064956, 0], [2639936279195426700]], [[(-896486879671158876), 0, 0, 0, 0], [(-439454352779970490), 0, 0, 0], [(-215418800382327891), 0, 0], [(-105597451167800088), 0], [(-51763456454802236)]]], r := 72283179916837726, ok := true }, nJu := { p := [[[(-270865785374334221063)]], [[1064561498993913845, 0], [521843872055840122]], [[(-21290420925808511), 0, 0], [793190264478, 0], [(-5115921983325765)]], [[567744558841390, 0, 0, 0], [1205632, 0, 0], [590996, 0], [66874797264225]], [[(-17032336765240), 0, 0, 0, 0], [3, 0, 0, 0], [11822, 0, 0], [2, 0], [(-983452900944)]]], r := 2917399034281, ok := true }, Jd1 := { p := [[[(-700406988780575499563948)]], [[28015214949271322585664, 0], [13732948504544766014184]], [[(-1120608599589022455702), 0, 0], [(-549317941768231438134), 0], [(-269273500477946545888)]], [[44824343983558500038, 0, 0, 0], [21972717638996852573, 0, 0], [10770940019116129912, 0], [5279872558390853400]], [[(-1792973759342317752), 0, 0, 0, 0], [(-878908705559940980), 0, 0, 0], [(-430837600764655782), 0, 0], [(-211194902335600175), 0], [(-103526912909604471)]]], r := 144566359833675449, ok := true }, term0 := { p := [[[9218869359267478232266986194]], [[(-737467520596090810479416746), 0], [(-361468530218539548081082185)]], [[44247210779324250009029853, 0, 0], [28916658440575968236685921, 0], [10630880734163387013945651]], [[(-2359828829391969770180988), 0, 0, 0], [(-1734983026896162961946212), 0, 0], [(-850454302323043359606159), 0], [(-277924377034259763085092)]], [[117990769104438196327970, 0, 0, 0, 0], [92531988646775183541794, 0, 0, 0], [51026935011180475393530, 0, 0], [22233633370386404751612, 0], [6811766906316698347784]]], r := 15833763271037589242060, ok := true }, r0 := { p := [[[3056786235023047778752]], [[(-79078431452104835578), 6111608209472001012829], [(-53373445335792617874)]], [[1843579636414410476, (-158043510121210831796), 3051876999811956102106], [1344878918771730466, (-106720354955101852482)], [996222277179692713]], [[(-48870901522486899), 3683481461895198551, (-78795177359723347033), (-3924273486684046544)], [(-30160057957005752), 2688247713835527875, (-53307119539322814539)], [(-24861208473989728), 1991992991904890313], [(-18937835200826885)]], [[1515832522330748, (-97643455630843820), 1834391124338945775, 226322095051848217, (-977531096117243306)], [773973828474683, (-60272368004683392), 1341104812238661160, 53030954351854470], [549381326286685, (-49696811494954271), 995093582027072507], [469855321858004, (-37867561589635089)], [363089276286740]]], r := 342382995036777882, ok := true }, r1 := { p := [[[191762327245442070622926]], [[(-4840378307154941242028), 0], [(-3363250334416402612432)]], [[110941555913331218423, 0, 0], [83102875495374110666, 0], [62861106202304879081]], [[(-2941865220661985240), 0, 0, 0], [(-1837416146522097348), 0, 0], [(-1540668843596755816), 0], [(-1195899573340118794)]], [[92122885836375378, 0, 0, 0, 0], [47166607650657837, 0, 0, 0], [33592731013765685, 0, 0], [29165716405105978, 0], [22940857543646982]]], r := 48441639360174305, ok := true }, r2 := { p := [[[921125312934198521435182258]], [[(-28303629945040453304918862), 50395078896833199906786], [(-35198792203446328148538738)]], [[912747608279304618607802, (-1068233794354747902462), 448924597926077035], [1061937479956967273119100, (-963239223991203222823)], [1019082581410756817688399]], [[(-32592124909960032554728), 28326843816777849623, 204634993626660, (-18443555926779)], [(-33888232165752590872311), 19530244182249838292, 38608928010645], [(-30395140278926644519913), 18693412457451323813], [(-26347005913323928748270)]], [[1230848396276216699451, (-917165375543332316), (-27335709196434), (-3069550783136), (-3045378986043)], [1205364850887953680208, (-501444339290575968), (-23860241150243), (-22375789737719)], [963521341091098467004, (-372076764938895074), (-6966060884792)], [779342444018704668470, (-364254998428044431)], [640247723925274533391]]], r := 4055414034337174186480, ok := true }, r3 := { p := [[[18426013967832788875683553916]], [[(-1474073094643800676698195410), 1062612892662346252302338], [(-722706943315593980816929774)]], [[88444223303029142273151327, (-78150884731005744814238), 1618190480845937230], [57816402862128010529274178, (-20867355858571180067095)], [21257247767268681430145185]], [[(-4717020823932745307932295), 4552156485691142829613, 9389848402948896, (-1520183773224824)], [(-3468981085571849021580665), 1534239751140799346511, (-2236881005901158)], [(-1700576863232289014483444), 409390270773952330177], [(-555760232979328333836828)]], [[235850901866944503202819, (-239148676670904957858), (-5020762790389394), (-5118885429792557), (-547064313418393)], [185012240049867847952440, (-89358874248322693802), (-94212157472227), (-5043496507601393)], [102034549299566015301946, (-30099641974044597404), (-3759963148295313)], [44460756725191024018627, (-8034070687811939565)], [13621795479471243489977]]], r := 1440818040348041067867405, ok := true }, eta := { p := [[[(-922135467701168170896043206)]], [[28341791082931777350980104, 0], [35218258120314186519810709]], [[(-914204746135108495506684), 0, 0], [(-1062667736016175037682105), 0], [(-1019461659795958483412083)]], [[32649127394113293351429, 0, 0, 0], [33916079620051954252704, 0, 0], [30409322051380202542557, 0], [26354407960383513636532]], [[(-1233104312227716109640), 0, 0, 0, 0], [(-1206454652454717062809), 0, 0, 0], [(-964061910191761681330), 0, 0], [(-779618922512805693541), 0], [(-640392441992149292948)]]], r := 318556746739960097173, 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 := 3518437208883200, bh := 140737488355328, tc := 2305843009213693952, th := 2305843009213693952, sc := 3891110078048108544, sh := 144115188075855872 }
noncomputable def q2 : Cert := { V0 := [[[211754046080470590]], [[(-3501671939595387), 211713792173269498], [861079011981618]], [[25801706115727, (-3499675030794098), (-60367324843394)], [(-14395118749763), 860587961909740], [(-13718994929783)]], [[(-245350280222), 25753973021170, 2994244071963, (-20099887126791)], [118947362550, (-14370670482387), (-736299908044)], [228720303712, (-13713167999345)], [333403629084]], [[3052500202, (-244541823588), (-71554385961), 996216770692, 16906343368], [(-1412559939), 118354172359, 36649598661, (-244974791308)], [(-1838126877), 228430907743, 8738249033], [(-5553709591), 333274414842], [(-9437753437)]]], r0 := 6415808553686, V1 := [[[1683994490143386016]], [[(-27518883387656422), 0], [6767033956076029]], [[194735377633052, 0, 0], [(-109176602246454), 0], [(-108300468034728)]], [[(-1768548628319), 0, 0, 0], [809210712031, 0, 0], [1758225091731, 0], [2635015908067]], [[21552978817, 0, 0, 0, 0], [(-8871822180), 0, 0, 0], [(-13009264623), 0, 0], [(-42841951707), 0], [(-74639411042)]]], r1 := 2895696310731, V2 := [[[18442591093448004915]], [[(-30596014000542), 86732386194], [(-165668092616053)]], [[43634395882, (-212934468), (-1731456)], [(-1237065245757), 6967287758], [10605796092]], [[(-625498204), (-7284821), 21308, 34], [1926337457, (-16703509), (-208835)], [(-319696762), 140629791], [(-118010364)]], [[12026589, 21877, 105, (-1), 0], [(-27556465), (-592891), 2561, 5], [4386730, (-319296), (-8423)], [3304932, 21503], [2119009]]], r2 := 8310662505, V3 := [[[18445259303324931937]], [[(-54987381536314), 61400923789], [(-59408160268215)]], [[155867128, 1686038213, (-2436267)], [(-2199972606462), 4935251581], [(-697642801)]], [[61033, (-22277543), (-43270), 95], [12512752, 135658149, (-293837)], [(-19225185), 99746163], [(-115617)]], [[(-814), (-8662), 1545, 1, 0], [5356, (-1788840), (-5228), 15], [252170, 2747935, (-11850)], [(-3953), 17642], [836]]], r3 := 33537230019, Vm := [[[18442591727539400062]], [[(-30598079127675), 0], [(-165617040101318)]], [[43588232059, 0, 0], [(-1237230588079), 0], [11641337553]], [[(-625408257), 0, 0, 0], [1922589299, 0, 0], [(-323008001), 0], [(-117770479)]], [[12025453, 0, 0, 0, 0], [(-27548751), 0, 0, 0], [4309277, 0, 0], [3304902, 0], [2117256]]], rm := 936413354 }
noncomputable def w2 : Wit := { Z0 := { p := [[[211774176418741189]], [[(-3502670673857294), 211774176418741189], [861324605836872]], [[25825583981464, (-3502670673857294), 0], [(-14407348586296), 861324605836872], [(-13721908931729)]], [[(-245754817639), 25825583981464, 0, 0], [119244189732, (-14407348586296), 0], [228865046023, (-13721908931729)], [333468247293]], [[3058597743, (-245754817639), 0, 0, 0], [(-1417770409), 119244189732, 0, 0], [(-1841603886), 228865046023, 0], [(-5556917708), 333468247293], [(-9439482926)]]], r := 1549082921219, ok := true }, Z1 := { p := [[[1694193411349929518]], [[(-28021365390858350), 0], [6890596846694978]], [[206604671851713, 0, 0], [(-115258788690366), 0], [(-109775271453829)]], [[(-1966038541108), 0, 0, 0], [953953517856, 0, 0], [1830920368191, 0], [2667745978347]], [[24468781946, 0, 0, 0, 0], [(-11342163265), 0, 0, 0], [(-14732831086), 0, 0], [(-44455341662), 0], [(-75515863401)]]], r := 736566347886, ok := true }, Z2 := { p := [[[11252887405923737380741]], [[(-74706184747969101143), 211774176418741189], [(-404511225991704292647)]], [[632644393676294020, (-3502670673857294), 0], [2676830689949411001, 861324605836872], [15450653979973192849]], [[(-6794941366503908), 25825583981464, 0, 0], [(-22071303289529439), (-14407348586296), 0], [(-102126984893708136), (-13721908931729)], [(-600296323356701331)]], [[95248226710111, (-245754817639), 0, 0, 0], [228665209653972, 119244189732, 0, 0], [833880383280871, 228865046023, 0], [3965174165874880, 333468247293], [23510016994649641]]], r := 3013613688717988, ok := true }, Z3 := { p := [[[28567743609001657926350]], [[(-962930458562012738693), 1075243411279387148], [(-1040346446968365377669)]], [[34219030237876448910, (-46888710170925196), 0], [35408747759961492311, 3867581785207232], [39926966521176989996]], [[(-1234547801778658764), 1646774111830660, 0, 0], [(-1262869484422607250), (-155771843157199), 0], [(-1363878199385233575), (-63438635265142)], [(-1555707755245232144)]], [[44858869090822796, (-59217724726846), 0, 0, 0], [45661066761172607, 5165886323858, 0, 0], [48712828281894292, 2601472846238, 0], [53258045603956819, 1556260786980], [61050766907843761]]], r := 101436487047658176, ok := true }, iE := { p := [[[11256969824948364005460]], [[(-74731189763820138616), 0], [(-404494622041134348188)]], [[632859985017749625, 0, 0], [2676725879726423513, 0], [15450389459609924776]], [[(-6797288571499005), 0, 0, 0], [(-22070184964125136), 0, 0], [(-102125327884080325), 0], [(-600289895013359941)]], [[95281515125890, 0, 0, 0, 0], [228650132135255, 0, 0, 0], [833863554289865, 0, 0], [3965133992536383, 0], [23509835027587711]]], r := 3012778644067822, ok := true }, iHu := { p := [[[28577569843344339850486]], [[(-963251020955416725272), 0], [(-1040311102631853038303)]], [[34230441340863030967, 0, 0], [35407712458051229466, 0], [39926386779985408553]], [[(-1234959683786821789), 0, 0, 0], [(-1262834068191681490), 0, 0], [(-1363860793646518408), 0], [(-1555693533178832316)]], [[44873838645882752, 0, 0, 0, 0], [45659820907404903, 0, 0, 0], [48712228510462532, 0, 0], [53257615109477968, 0], [61050362072704600]]], r := 101440352660169316, ok := true }, T := { p := [[[2305843009213693952]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[30228593681292856]], [[200677340866948, 0], [1086198485568532]], [[(-367204582308), 0, 0], [7233931736893, 0], [(-2459107534359)]], [[4533207506, 0, 0, 0], [(-14688774267), 0, 0], [(-15863876209), 0], [32782705110]], [[(-83948287), 0, 0, 0, 0], [181328300, 0, 0, 0], [(-23640), 0, 0], [211501329, 0], [(-655654121)]]], r := 526930054, ok := true }, de := { p := [[[(-134672283761215903474)]], [[492853647486123261, 0], [532281939285013122]], [[(-9126552178534476), 0, 0], [793193810460, 0], [(-10645210461042614)]], [[225346967736036, 0, 0, 0], [1181999, 0, 0], [1276559, 0], [283872279420698]], [[(-6259637992667), 0, 0, 0, 0], [2, 0, 0, 0], [23643, 0, 0], [2, 0], [(-8516168382620)]]], r := 2382382630740, ok := true }, dde := { p := [[[(-330748484010501877526184)]], [[12249450978763478899331, 0], [13229407057064557199267]], [[(-453683370318300793265), 0, 0], [(-489978040736990582843), 0], [(-529176283139266042228)]], [[16803087789565609091, 0, 0, 0], [18147334812728508542, 0, 0], [19599121597746777657, 0], [21167051325569291983]], [[(-622336584798711134), 0, 0, 0, 0], [(-672123511582619379), 0, 0, 0], [(-725893392509269519), 0, 0], [(-783964863909964550), 0], [(-846682053022763070)]]], r := 177082106424126037, ok := true }, nJu := { p := [[[(-269344567522431806947)]], [[985707294972246522, 0], [1064563878570026244]], [[(-18253104357068952), 0, 0], [1586387620921, 0], [(-21290420922085228)]], [[450693935472073, 0, 0, 0], [2363998, 0, 0], [2553118, 0], [567744558841396]], [[(-12519275985333), 0, 0, 0, 0], [5, 0, 0, 0], [47286, 0, 0], [5, 0], [(-17032336765240)]]], r := 4764765261473, ok := true }, Jd1 := { p := [[[(-661496968021003755052368)]], [[24498901957526957798662, 0], [26458814114129114398535]], [[(-907366740636601586529), 0, 0], [(-979956081473981165686), 0], [(-1058352566278532084455)]], [[33606175579131218182, 0, 0, 0], [36294669625457017085, 0, 0], [39198243195493555314, 0], [42334102651138583967]], [[(-1244673169597422268), 0, 0, 0, 0], [(-1344247023165238758), 0, 0, 0], [(-1451786785018539038), 0, 0], [(-1567929727819929100), 0], [(-1693364106045526140)]]], r := 354164212848252069, ok := true }, term0 := { p := [[[8223027613185116828488347486]], [[(-609076403250668514002206227), 0], [(-657739798321710725513325475)]], [[33836897433322706138194137, 0, 0], [48719996608238246537001948, 0], [39462339791098580112371713]], [[(-1670941094854072800412555), 0, 0, 0], [(-2706639257232931628446437), 0, 0], [(-2923077483457324408081932), 0], [(-2104603505973073284769825)]], [[77357917268582547284385, 0, 0, 0, 0], [133660525764534190826090, 0, 0, 0], [162392104685317594895029, 0, 0], [155894204103413264246743, 0], [105228536812087706439239]]], r := 41560046130349428419129, ok := true }, r0 := { p := [[[2957400887019251388099]], [[(-73501996681028762833), 5913026147263498560556], [(-105502407213392847845)]], [[1609469726901374117, (-146902893438294620321), 2952963014560581606167], [2559592162031105743, (-210955762027055994923)], [4019393226127234438]], [[(-39192522815156112), 3215752925886543780, (-73249353979190864386), (-3547670908733509431)], [(-54002716125833117), 5116425432728352763, (-105379799532755286324)], [(-96656479326930105), 8037082551920845658], [(-155921700714915293)]], [[1107089794993513, (-78303854930935394), 1601508367679189372, 201878622289089222, (-883934114113721036)], [1272353686135814, (-107920479968920615), 2552697001483539514, 98034852468757763], [2010787040261190, (-193217429471117815), 4015134219382305681], [3729587571214099, (-311780960215464127)], [6099856825168547]]], r := 778907777378955525, ok := true }, r1 := { p := [[[185768288804084722862645]], [[(-4506922111472585894964), 0], [(-6654727222313815441544)]], [[96885322751495714480, 0, 0], [158381111376167693200, 0], [253852801583106151899]], [[(-2354614914627376990), 0, 0, 0], [(-3290742111331797055), 0, 0], [(-5997545682426916655), 0], [(-9854731462964105294)]], [[67089793414305182, 0, 0, 0, 0], [77401630985809488, 0, 0, 0], [122981968104371268, 0, 0], [231792455550610688, 0], [385722325157479661]]], r := 469590487420414911, ok := true }, r2 := { p := [[[902115478819717881292582608]], [[(-25974988491265507433122794), 49309480095076126388659], [(-70404838208876419067467643)]], [[771751415474186861084488, (-983010926364907422757), 449282392731555326], [1990980435803279872872091, (-1926228465837467790087)], [4161231514921213104231816]], [[(-25319105872844236071382), 23952693538775272910, 170752860822917, (-19940272966870)], [(-58510082327624877750548), 36790406846270056015, 81116535282348], [(-116357093657318165059419), 76315784605870287956], [(-219580357392227385987405)]], [[880586097209631155200, (-708521656655787838), (-11426479290819), (-3030311126387), (-3051244566433)], [1911146422432105825426, (-867539700325032562), (-19839305452704), (-20850002131341)], [3395779144882933710147, (-1431879059876256003), (-11582320701483)], [6090174123729522674976, (-3034847391099147438)], [10889552694026473397930]]], r := 32777899548390953660826, ok := true }, r3 := { p := [[[16435668911714800356026448968]], [[(-1217449950581663567089839204), 941264443316977003586779], [(-1315063737585123550868824823)]], [[67635977370279095031112446, (-63724526692493987132861), 1639427814747311822], [97411856808206628264369188, (-37709407676919598385425)], [78908039198781665555259253]], [[(-3340044969217714738614368), 3429337096656938768048, 9747908274414351, (-1311025132496523)], [(-5411764740163416268728118), 2552145158068474429738, (-2864986973365159)], [(-5845029178298596615399437), 1509236458050323716023], [(-4208541258946558715607010)]], [[154631614828909114275873, (-166621484751692935670), (-2563356823415518), (-4154910516726862), (-443750138444901)], [267247512590794963262468, (-137329297413275102599), (-2988144437666589), (-3286637370296270)], [324723639316110124369948, (-102136694808803436697), (-543624073809136)], [311743366347986604491255, (-60391487087780437825)], [210430438094848766254522]]], r := 5055479442563433198591031, ok := true }, eta := { p := [[[(-903073185739271786230521703)]], [[26008582649251658403943829, 0], [70442508955202333375574313]], [[(-772936935667101063789575), 0, 0], [(-1992292279215674124505410), 0], [(-4162728395211540481953859)]], [[25361968153548142697804, 0, 0, 0], [58556303134843850426421, 0, 0], [116409071135695752909843, 0], [219639992234099534125680]], [[(-882155011001085927058), 0, 0, 0, 0], [(-1912817992725978574968), 0, 0, 0], [(-3397609453365553496976), 0, 0], [(-6092241263845321468632), 0], [(-10891931321378298501081)]]], r := 2816711153077550217946, 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 := 3799912185593856, bh := 140737488355328, tc := 2305843009213693952, th := 2305843009213693952, sc := 3602879701896396800, sh := 144115188075855872 }
noncomputable def q3 : Cert := { V0 := [[[220589198063216346]], [[(-3636800108861704), 220543692580778760], [837467163319114]], [[27599730067871, (-3634549478865084), (-68241618349896)], [(-14007262376591), 836948897628801], [(-12328146465955)]], [[(-275052805486), 27545547848819, 3374576232822, (-22719537851465)], [120614228660, (-13981506537848), (-777083342641)], [205443483777, (-12322484619615)], [277227889570]], [[3669733571, (-274115629113), (-81217812518), 1122578310239, 20738522467], [(-1512645062), 119983302935, 38607702271, (-258502652041)], [(-1715408321), 205163042269, 8490522660], [(-4614665510), 277111762173], [(-7263452801)]]], r0 := 5134269918820, V1 := [[[1753376230965610443]], [[(-28537902241749513), 0], [6571589122877752]], [[207572972068124, 0, 0], [(-105769026959390), 0], [(-97216061134659)]], [[(-1975975259729), 0, 0, 0], [814062655957, 0, 0], [1574325838015, 0], [2188896844105]], [[25919566768, 0, 0, 0, 0], [(-9465858104), 0, 0, 0], [(-12071015032), 0, 0], [(-35496421892), 0], [(-57390848753)]]], r1 := 2203581504695, V2 := [[[18442326137253122741]], [[(-33270029069910), 101690591034], [(-163142404182159)]], [[51929065695, (-213213101), (-2236886)], [(-1246431326781), 7563430376], [10564470137]], [[(-798670631), (-8685940), 26292, 48], [2124011927, (-15383601), (-249813)], [(-318468313), 141341342], [(-108699433)]], [[16540905, 29756, 147, (-1), 0], [(-32608291), (-655214), 2925, 7], [4509398, (-267942), (-9329)], [3039791, 19886], [1806078]]], r2 := 6507800655, V3 := [[[18445259259747286816]], [[(-59388130387892), 67629935168], [(-55010799054561)]], [[181443299, 2072221505, (-2955563)], [(-2200103567856), 5033404691], [(-658812516)]], [[80778, (-25934532), (-62511), 127], [13484559, 154379266, (-330073)], [(-20256037), 94202304], [(-101784)]], [[(-1177), (-11469), 2009, 1, 0], [6563, (-1927935), (-6993), 19], [251526, 2895551, (-12326)], [(-3854), 15624], [676]]], r3 := 33541125074, Vm := [[[18442326882194966865]], [[(-33272220927820), 0], [(-163086865804977)]], [[51874424738, 0, 0], [(-1246593575776), 0], [11607721272]], [[(-798552819), 0, 0, 0], [2119900140, 0, 0], [(-321466682), 0], [(-108472751)]], [[16539305, 0, 0, 0, 0], [(-32598920), 0, 0, 0], [4430558, 0, 0], [3039931, 0], [1804550]]], rm := 751102078 }
noncomputable def w3 : Wit := { Z0 := { p := [[[220611954956667684]], [[(-3637925766155090), 220611954956667684], [837726374986555]], [[27626835062378, (-3637925766155090), 0], [(-14020146812707), 837726374986555], [(-12330977950916)]], [[(-275521776991), 27626835062378, 0, 0], [120929957845, (-14020146812707), 0], [205583750765, (-12330977950916)], [277285964014]], [[3677071773, (-275521776991), 0, 0, 0], [(-1518327394), 120929957845, 0, 0], [(-1718803992), 205583750765, 0], [(-4617540590), 277285964014], [(-7264891055)]]], r := 1222831713245, ok := true }, Z1 := { p := [[[1764895639653341473]], [[(-29103406129240716), 0], [6701810999892441]], [[221014680499027, 0, 0], [(-112161174501656), 0], [(-98647823607321)]], [[(-2204174215928), 0, 0, 0], [967439662766, 0, 0], [1644670006120, 0], [2218287712117]], [[29416574191, 0, 0, 0, 0], [(-12146619148), 0, 0, 0], [(-13750431935), 0, 0], [(-36940324719), 0], [(-58119128439)]]], r := 561283322115, ok := true }, Z2 := { p := [[[10643095982419174977835]], [[(-72177436278983051870), 220611954956667684], [(-353928169329657207492)]], [[632099120864083940, (-3637925766155090), 0], [2390193419231812595, 837726374986555], [12512975109626940283]], [[(-7155522314755965), 27626835062378, 0, 0], [(-20342879388969816), (-14020146812707), 0], [(-84379292141061262), (-12330977950916)], [(-450057649088642169)]], [[107926448885761, (-275521776991), 0, 0, 0], [221739825802323, 120929957845, 0, 0], [710693515081911, 205583750765, 0], [3032210478914024, 277285964014], [16318124012635027]]], r := 2124174022465865, ok := true }, Z3 := { p := [[[28566980505558880634560]], [[(-1039937115943546468365), 1184258188819000260], [(-963286288706151140763)]], [[39912010719912527016, (-54608278903208383), 0], [35408831135124231754, 3944167563132242], [34230976975104681933]], [[(-1555133138971496332), 2073104402515284, 0, 0], [(-1363902111183982522), (-167682580691405), 0], [(-1262851481380129898), (-59902635059772)], [(-1234971850495800919)]], [[61028365937763825, (-80531778318137), 0, 0, 0], [53259184715600026, 6017444096088, 0, 0], [48712876377366699, 2594023112808, 0], [45660219675597752, 1360663436319], [44874159320706878]]], r := 101435476551891235, ok := true }, iE := { p := [[[10647261907199667391871]], [[(-72203545297232785531), 0], [(-353912350127721781765)]], [[632332006788165856, 0, 0], [2390090387608120335, 0], [12512742257664663295]], [[(-7158195878805508), 0, 0, 0], [(-20341732233654231), 0, 0], [(-84377790418197085), 0], [(-450052412960486745)]], [[107967252951526, 0, 0, 0, 0], [221723465981870, 0, 0, 0], [710677633847455, 0, 0], [3032176811901134, 0], [16317986826100060]]], r := 2123517070705306, ok := true }, iHu := { p := [[[28577569843344339850486]], [[(-1040311102631853038303), 0], [(-963251020955416725272)]], [[39926386779985408553, 0, 0], [35407712458051229466, 0], [34230441340863030967]], [[(-1555693533178832316), 0, 0, 0], [(-1363860793646518408), 0, 0], [(-1262834068191681490), 0], [(-1234959683786821789)]], [[61050362072704600, 0, 0, 0, 0], [53257615109477968, 0, 0, 0], [48712228510462532, 0, 0], [45659820907404903, 0], [44873838645882752]]], r := 101440352660169316, ok := true }, T := { p := [[[2305843009213693952]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[31959612704825067]], [[216731528136305, 0], [1062329614892634]], [[(-428307424804), 0, 0], [7233931736893, 0], [(-2247603752205)]], [[5710535893, 0, 0, 0], [(-15863876209), 0, 0], [(-14688774267), 0], [27743228985]], [[(-114210718), 0, 0, 0, 0], [211501329, 0, 0, 0], [(-23640), 0, 0], [181328300, 0], [(-513763517)]]], r := 433887053, ok := true }, de := { p := [[[(-134672283761215903474)]], [[532281939285013122, 0], [492853647486123261]], [[(-10645210461042614), 0, 0], [793193810460, 0], [(-9126552178534476)]], [[283872279420698, 0, 0, 0], [1276559, 0, 0], [1181999, 0], [225346967736036]], [[(-8516168382620), 0, 0, 0, 0], [2, 0, 0, 0], [23643, 0, 0], [2, 0], [(-6259637992667)]]], r := 2382382630740, ok := true }, dde := { p := [[[(-330748484010501877527302)]], [[13229407057064557200155, 0], [12249450978763478895554]], [[(-529176283139266039295), 0, 0], [(-489978040736990582723), 0], [(-453683370318300795357)]], [[21167051325569293943, 0, 0, 0], [19599121597746777542, 0, 0], [18147334812728508628, 0], [16803087789565606431]], [[(-846682053022761251), 0, 0, 0, 0], [(-783964863909964622), 0, 0, 0], [(-725893392509269519), 0, 0], [(-672123511582619272), 0], [(-622336584798711551)]]], r := 177082106424119657, ok := true }, nJu := { p := [[[(-269344567522431806947)]], [[1064563878570026244, 0], [985707294972246522]], [[(-21290420922085228), 0, 0], [1586387620921, 0], [(-18253104357068952)]], [[567744558841396, 0, 0, 0], [2553118, 0, 0], [2363998, 0], [450693935472073]], [[(-17032336765240), 0, 0, 0, 0], [5, 0, 0, 0], [47286, 0, 0], [5, 0], [(-12519275985333)]]], r := 4764765261473, ok := true }, Jd1 := { p := [[[(-661496968021003755054604)]], [[26458814114129114400311, 0], [24498901957526957791108]], [[(-1058352566278532078589), 0, 0], [(-979956081473981165446), 0], [(-907366740636601590714)]], [[42334102651138587886, 0, 0, 0], [39198243195493555084, 0, 0], [36294669625457017256, 0], [33606175579131212862]], [[(-1693364106045522502), 0, 0, 0, 0], [(-1567929727819929244), 0, 0, 0], [(-1451786785018539038), 0, 0], [(-1344247023165238544), 0], [(-1244673169597423102)]]], r := 354164212848239312, ok := true }, term0 := { p := [[[8223153047563139366567828103]], [[(-657812550260980042876386203), 0], [(-609022977497081363605229744)]], [[39467959251243086979819345, 0, 0], [48720368265655211204644615, 0], [33832767906467542290299264]], [[(-2104936659681640558480996), 0, 0, 0], [(-2923192697256583450040109), 0, 0], [(-2706566990512966284782560), 0], [(-1670708490332138299956743)]], [[105246197972541783528243, 0, 0, 0, 0], [155902826555486852652835, 0, 0, 0], [162392930590688627526503, 0, 0], [133654662856036108677006, 0], [77346351949886688838477]]], r := 41561163652114683086962, ok := true }, r0 := { p := [[[2905148381386787571617]], [[(-75255546570900909790), 5808408252777538555944], [(-95741736480928035156)]], [[1757781037287957904, (-150402052022218116172), 2900428483943328466495], [2414988221517525960, (-191435412524172476310)], [3374606479471440708]], [[(-46667653865546448), 3512020637360139210, (-74983068189645186404), (-3772888347028805878)], [(-54243825679140525), 4827240386693586885, (-95621610025596654672)], [(-84296677844755653), 6747669164044580832], [(-121153221371009512)]], [[1448649157953164, (-93240475926738087), 1748933300879240414, 217709108513474047, (-939781452739131122)], [1393886598259696, (-108401083420593752), 2408150276926681176, 96046968990106418], [1865565887983689, (-168505786683669325), 3370747719377064291], [3008640311900483, (-242254099186551514)], [4387088075968488]]], r := 726363720645948945, ok := true }, r1 := { p := [[[182207793558312398773699]], [[(-4604190923080407997559), 0], [(-6032125570571686381433)]], [[105715536374052502004, 0, 0], [149180365871838142166, 0], [212908119286701451872]], [[(-2807622030875099027), 0, 0, 0], [(-3303352343919323943), 0, 0], [(-5222488133359420015), 0], [(-7649748656585714658)]], [[87994480534439196, 0, 0, 0, 0], [84913237496515785, 0, 0, 0], [114032835378101017, 0, 0], [186710031395964424, 0], [277155440508153813]]], r := 363862295235482293, ok := true }, r2 := { p := [[[824037767493414560799861303]], [[(-25371756146226952022226380), 47664311848873792966904], [(-59464236217267354232703295)]], [[819135584471076414751440, (-1012808702441701697072), 449072872159384099], [1797480881667392704051115, (-1720395266648146747052)], [3251485407254894263466569]], [[(-29261784109800617762404), 26902734665647255528, 209551027835062, (-11138376438216)], [(-57424340982315188479748), 34954827450681419986, 87594243564383], [(-97160242839769221296516), 63059171230735279394], [(-158769603080050926309133)]], [[1105206430972096714110, (-871667751545937803), (-22188820613057), (-2701883883269), (-2498958041518)], [2043354748521404337665, (-898855202153653931), (-16062721726135), (-17244719644291)], [3083323314479342160740, (-1257541689053027709), (-2929329886083)], [4704990360550655070356, (-2320725103185091736)], [7287161109789821807263]]], r := 23944054491087895631877, ok := true }, r3 := { p := [[[16435233329759393502865320868]], [[(-1314811076224657215324718314), 1003490611230670486608987], [(-1217635454166589645537872106)]], [[78888510953046474484609596, (-73803982371483984269636), 1614896933983039093], [97410563772268885073706025, (-37223930672962826642101)], [67650326611939493705174408]], [[(-4207383069578650472471533), 4298988753532945806449, 11029390903169898, (-3908554222030192)], [(-5844628313353031062141308), 2736861883801463240257, (-3086937495020315)], [(-5412016144644040890086598), 1379441227119800618113], [(-3340853561131161625851482)]], [[210369021830383860974460, (-225846693613441741144), (-1955139118402794), (-3268695779420927), (-444021412683099)], [311713359781558892485905, (-159403151689327816695), (-912166833046764), (-2815265685482923)], [324720767099405790138967, (-101415216412537062410), (-2390753286177355)], [267267917469527874679775, (-51109003694034943753)], [154671832626350457810452]]], r := 5056079135949585318696980, ok := true }, eta := { p := [[[(-824992747431277242447432133)]], [[25407847100769904587017823, 0], [59498989706037365677402803]], [[(-820513776237968661536605), 0, 0], [(-1798785054773596554646123), 0], [(-3252763695558492615737957)]], [[29315697151754393025492, 0, 0, 0], [57474076712979539648687, 0, 0], [97208078896961319834399, 0], [158816748686155074895532]], [[(-1107340011867314715438), 0, 0, 0, 0], [(-2045301073018742858646), 0, 0, 0], [(-3085146742949182437710), 0, 0], [(-4706751680809177991599), 0], [(-7288902065740853377442)]]], r := 2006003411663446393203, 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 := 3799912185593856, bh := 140737488355328, tc := 2305843009213693952, th := 2305843009213693952, sc := 3891110078048108544, sh := 144115188075855872 }
noncomputable def q4 : Cert := { V0 := [[[213423853055961496]], [[(-3529589356360788), 213382639374888458], [809923370605023]], [[26032583485650, (-3527544659887134), (-61806443500648)], [(-13542211737653), 809454180766601], [(-11923962303025)]], [[(-248095922210), 25983690644590, 3065880656888, (-20578690069052)], [112088731948, (-13518849197074), (-703517646049)], [198817730911, (-11918835110564)], [268147716564]], [[3093988551, (-247267105652), (-73292177503), 1020020795294, 17583262833], [(-1334851855), 111521621015, 35021676378, (-234060848786)], [(-1599787313), 198563072090, 7688883325], [(-4467194780), 268042549454], [(-7025687173)]]], r0 := 4933388365795, V1 := [[[1697115310964083316]], [[(-27730528116359219), 0], [6363233943966849]], [[196304157664012, 0, 0], [(-102621710087556), 0], [(-94114642923199)]], [[(-1785765662076), 0, 0, 0], [760703520737, 0, 0], [1527602094929, 0], [2118966282925]], [[21811227956, 0, 0, 0, 0], [(-8357098844), 0, 0, 0], [(-11306138255), 0, 0], [(-34445458453), 0], [(-55555896554)]]], r1 := 2100916351537, V2 := [[[18442259798774329202]], [[(-33071397752003), 101229650545], [(-165627021335998)]], [[47504271916, (-247616754), (-2183731)], [(-1238306178906), 7530060283], [9945053170]], [[(-680849906), (-8519898), 26853, 46], [1943371618, (-17977832), (-243898)], [(-301197316), 140755341], [(-102785061)]], [[13092086, 25740, 133, (-1), 0], [(-27792868), (-642216), 2989, 7], [4136167, (-317880), (-9109)], [2876976, 20373], [1707425]]], r2 := 6467806011, V3 := [[[18445140484212912376]], [[(-59387403681153), 71670550883], [(-59410952200989)]], [[181901564, 1968350867, (-3072629)], [(-2200049553751), 5334444253], [(-698317351)]], [[72263, (-25999571), (-54596), 129], [13521806, 146656781, (-343170)], [(-19248246), 99849284], [(-109378)]], [[(-962), (-10252), 1948, 1, 0], [5875, (-1933209), (-6109), 19], [252354, 2751351, (-12817)], [(-3739), 16752], [727]]], r3 := 29539152996, Vm := [[[18442260539114811474]], [[(-33073806808967), 0], [(-165571823830968)]], [[47450301634, 0, 0], [(-1238484766527), 0], [10981993772]], [[(-680743816), 0, 0, 0], [1939313153, 0, 0], [(-304508721), 0], [(-102558267)]], [[13090744, 0, 0, 0, 0], [(-27784437), 0, 0, 0], [4058467, 0, 0], [2876950, 0], [1705898]]], rm := 736450038 }
noncomputable def w4 : Wit := { Z0 := { p := [[[213444463416744198]], [[(-3530611995694242), 213444463416744198], [810158032321230]], [[26057041681946, (-3530611995694242), 0], [(-13553898543778), 810158032321230], [(-11926526375658)]], [[(-248510652240), 26057041681946, 0, 0], [112372512771, (-13553898543778), 0], [198945099666, (-11926526375658)], [268200309232]], [[3100249048, (-248510652240), 0, 0, 0], [(-1339838728), 112372512771, 0, 0], [(-1602847751), 198945099666, 0], [(-4469806021), 268200309232], [(-7026989712)]]], r := 1179043503070, ok := true }, Z1 := { p := [[[1707555707333953589]], [[(-28244895965553933), 0], [6481264258569844]], [[208456333455568, 0, 0], [(-108431188350222), 0], [(-95412211005264)]], [[(-1988085217914), 0, 0, 0], [898980102171, 0, 0], [1591560797331, 0], [2145602473858]], [[24801992385, 0, 0, 0, 0], [(-10718709822), 0, 0, 0], [(-12822782004), 0, 0], [(-35758448161), 0], [(-56215917691)]]], r := 534505059216, ok := true }, Z2 := { p := [[[10501213924450740254786]], [[(-69731612324887240763), 213444463416744198], [(-349227429966370414700)]], [[591598435672843359, (-3530611995694242), 0], [2311383934654154270, 810158032321230], [12346999905172953566]], [[(-6369276475181730), 26057041681946, 0, 0], [(-19085459677984945), (-13553898543778), 0], [(-81624791968871109), (-11926526375658)], [(-444092641123435912)]], [[89468885750963, (-248510652240), 0, 0, 0], [198123590600104, 112372512771, 0, 0], [667359387155644, 198945099666, 0], [2933820200703086, 268200309232], [16101964567492795]]], r := 2044602180784302, ok := true }, Z3 := { p := [[[26635218384438030597440]], [[(-897173454192186140875), 1082736602622814068], [(-897529204832431847294)]], [[31874022205374029494, (-47190333938385936), 0], [30531380823844847204, 3631186096714981], [31886005070031953852]], [[(-1149765711652130810), 1656773032530715, 0, 0], [(-1088684170447005476), (-146081889079570), 0], [(-1088666078023438645), (-55064775744193)], [(-1150191429030709308)]], [[41773599603970020, (-59566638209513), 0, 0, 0], [39358009246663374, 4840782075768, 0, 0], [38875579773099229, 2256150137649, 0], [39357187745656790, 1250130158843], [41788956163784506]]], r := 77165419287313261, ok := true }, iE := { p := [[[10505328541978189769190]], [[(-69756820637409522246), 0], [(-349211812365489925234)]], [[591816199392019332, 0, 0], [2311285304143739177, 0], [12346769994808068359]], [[(-6371653004677291), 0, 0, 0], [(-19084404184188834), 0, 0], [(-81623351283546459), 0], [(-444087470964999522)]], [[89502659461349, 0, 0, 0, 0], [198109325256600, 0, 0, 0], [667344722659151, 0, 0], [2933787880370655, 0], [16101829106611925]]], r := 2043962165767249, ok := true }, iHu := { p := [[[26645113096162989581448]], [[(-897496020824835135137), 0], [(-897496020824835135137)]], [[31885501854309063853, 0, 0], [30530410344736658931, 0], [31885501854309063853]], [[(-1150180004573911159), 0, 0, 0], [(-1088650987468206801), 0, 0], [(-1088650987468206801), 0], [(-1150180004573911159)]], [[41788655144393562, 0, 0, 0, 0], [39356842301682324, 0, 0, 0], [38875059980990041, 0, 0], [39356842301682324, 0], [41788655144393562]]], r := 77168207188531371, ok := true }, T := { p := [[[2305843009213693952]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[32391406471602088]], [[215083376250839, 0], [1076735650276525]], [[(-396582225403), 0, 0], [7172886521447, 0], [(-2276981395301)]], [[4895864105, 0, 0, 0], [(-14688868828), 0, 0], [(-14688868828), 0], [28105885584]], [[(-90664150), 0, 0, 0, 0], [181328300, 0, 0, 0], [(-23640), 0, 0], [181328300, 0], [(-520479380)]]], r := 411389869, ok := true }, de := { p := [[[(-133648157828502864251)]], [[492855233878850430, 0], [492855233878850430]], [[(-9126552176075908), 0, 0], [793198916719, 0], [(-9126552176075908)]], [[225346967736040, 0, 0, 0], [1276571, 0, 0], [1276571, 0], [225346967736040]], [[(-6259637992667), 0, 0, 0, 0], [2, 0, 0, 0], [23644, 0, 0], [2, 0], [(-6259637992667)]]], r := 1926042463261, ok := true }, dde := { p := [[[(-306249582056147832853269)]], [[11342084236540410878330, 0], [11342084236540410874796]], [[(-420077194739174505486), 0, 0], [(-420077195532407913306), 0], [(-420077194739174507423)]], [[15558414619968170672, 0, 0, 0], [15558414619965613912, 0, 0], [15558414619965613989, 0], [15558414619968168209]], [[(-576237578517325647), 0, 0, 0, 0], [(-576237578517331270), 0, 0, 0], [(-576237578517360328), 0, 0], [(-576237578517331179), 0], [(-576237578517326033)]]], r := 133849736479990842, ok := true }, nJu := { p := [[[(-267296315657005728502)]], [[985710467757700860, 0], [985710467757700860]], [[(-18253104352151815), 0, 0], [1586397833439, 0], [(-18253104352151815)]], [[450693935472080, 0, 0, 0], [2553142, 0, 0], [2553142, 0], [450693935472080]], [[(-12519275985333), 0, 0, 0, 0], [5, 0, 0, 0], [47288, 0, 0], [5, 0], [(-12519275985333)]]], r := 3852084926514, ok := true }, Jd1 := { p := [[[(-612499164112295665706537)]], [[22684168473080821756661, 0], [22684168473080821749592]], [[(-840154389478349010972), 0, 0], [(-840154391064815826611), 0], [(-840154389478349014845)]], [[31116829239936341345, 0, 0, 0], [31116829239931227825, 0, 0], [31116829239931227978, 0], [31116829239936336419]], [[(-1152475157034651293), 0, 0, 0, 0], [(-1152475157034662539), 0, 0, 0], [(-1152475157034720655), 0, 0], [(-1152475157034662357), 0], [(-1152475157034652065)]]], r := 267699472959981671, ok := true }, term0 := { p := [[[7050096394956401174959468808]], [[(-522195331408004324997555577), 0], [(-522141561527179244368463740)]], [[29010221629105348049642415, 0, 0], [38675892474141899925429078, 0], [29006238674962635959478345]], [[(-1432587978825151239875058), 0, 0, 0], [(-2148637355385645618036882), 0, 0], [(-2148563596975595417576004), 0], [(-1432366703595000471452678)]], [[66323085360016939701607, 0, 0, 0, 0], [106104972176527114101700, 0, 0, 0], [119363779920053015290391, 0, 0], [106099508590597460092264, 0], [66312158188157661616664]]], r := 29129602088123625774000, ok := true }, r0 := { p := [[[2761316756946037411061]], [[(-68741758250413550138), 5520949640980611493447], [(-91118221023422675500)]], [[1508936292089654314, (-137387578247834287511), 2757108225292200531617], [2213486294020679618, (-182193524450283403320)], [3213118211618340364]], [[(-36821710471861712), 3014845059533956246, (-68502015836439820162), (-3364294726619071751)], [(-46795781977107692), 4424557711663156357, (-91010947657362760121)], [(-77360121484410215), 6424857294214309421], [(-115387328485349515)]], [[1041365514287270, (-73566146672188802), 1501372264396182349, 191566945867717478, (-838199648091938663)], [1104579739914675, (-93517143961914682), 2207450932314216149, 85773325142878555], [1612450532776720, (-154642891149300171), 3209670997910242707], [2763168888758674, (-230727885865685066)], [4179109241148968]]], r := 632119161225449071, ok := true }, r1 := { p := [[[173401129346390611151755]], [[(-4212429907915549168367), 0], [(-5746338045513760365170)]], [[90760763598050159259, 0, 0], [136908964359212047363, 0], [202897448698335978008]], [[(-2210426863622382214), 0, 0, 0], [(-2850059593286078759), 0, 0], [(-4798476134873250045), 0], [(-7291728036458699624)]], [[63061562994267202, 0, 0, 0, 0], [67160829077263483, 0, 0, 0], [98572581369276575, 0, 0], [171672699743440454, 0], [264226743317437260]]], r := 321728544423983867, ok := true }, r2 := { p := [[[776353115741351235496153802]], [[(-22414119503050177273693031), 45739799149081058244231], [(-56083769840841260973703211)]], [[667026521674212562434414, (-914740013476260190128), 449484804213528140], [1590055145518921103605583, (-1653866567297394849838)], [3068683946170840340134869]], [[(-21897380592424976761088), 22341148121816973873, 179373391112923, (-11367803011939)], [(-46800810861801373133885), 31673940649340574693, 77260034688177], [(-86019912693118049784505), 60664058960780948182], [(-149914786521960030016584)]], [[761727725782131391712, (-661554745207322018), (-5402342515646), (-2539596020951), (-2364060519253)], [1529633060615855952914, (-748478677652911766), (-15295181650749), (-15990139389385)], [2514261968753366761496, (-1141098449979059029), (-17953716955087)], [4168043503642606652234, (-2233554457895204077)], [6883280573105134541084]]], r := 20739349924869085359905, ok := true }, r3 := { p := [[[14090576563325860226851508504]], [[(-1043739910174935685130640368), 871435255625640806856253], [(-1043926610989503512537549917)]], [[57985428994878421596224930, (-58998498840227910988317), 1640286310147182016], [77327663622207335058125031, (-32326872778787205433320)], [57999268330669887983407120]], [[(-2863474916663466800593516), 3175036392517406705978, 8560146204926009, (-2748905681834356)], [(-4295976947544882903522875), 2187891634498953073154, (-2159389168351326)], [(-4296233544492145737338264), 1197986859801210745530], [(-2864244081245909907311329)]], [[132568193918936600644359, (-154266285233264679481), (-1001822532053156), (-2523450418373050), (-334171835149373)], [212146898181499224092654, (-117729762811641143049), (-377771148935753), (-2108481209934463)], [238679481010953209984315, (-81072344719113495649), (-1179377478857503)], [212165911816170678216451, (-44386178228334362427)], [132606189670000359337540]]], r := 3481074335823313249512336, ok := true }, eta := { p := [[[(-777241026854934908185719047)]], [[22445282567340804366583896, 0], [56116099498031365551048699]], [[(-668126382254273710309753), 0, 0], [(-1591181489181640484934370), 0], [(-3069873326948062934575246)]], [[21937145049626645679350, 0, 0, 0], [46840499359386860266311, 0, 0], [86061229275514562367402, 0], [149958658523997936090817]], [[(-763183181167427808472), 0, 0, 0, 0], [(-1531068360361322992840), 0, 0, 0], [(-2515716981678585629985), 0, 0], [(-4169564843630835873301), 0], [(-6884900798668213286161)]]], r := 1784042648815091854749, 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 3377699720527872 3940649673949184 0 4611686018427387904 3458764513820540928 4035225266123964416 :=
  (RegionPosI.split_b 3659174697238528 (RegionPosI.split_s 3746994889972252672 (RegionPosI.split_b 3518437208883200 (RegionPosI.of_check c0 q0 ok_0 3377699720527872 3518437208883200 0 4611686018427387904 3458764513820540928 3746994889972252672 (by decide +kernel)) (RegionPosI.of_check c1 q1 ok_1 3518437208883200 3659174697238528 0 4611686018427387904 3458764513820540928 3746994889972252672 (by decide +kernel))) (RegionPosI.of_check c2 q2 ok_2 3377699720527872 3659174697238528 0 4611686018427387904 3746994889972252672 4035225266123964416 (by decide +kernel))) (RegionPosI.split_s 3746994889972252672 (RegionPosI.of_check c3 q3 ok_3 3659174697238528 3940649673949184 0 4611686018427387904 3458764513820540928 3746994889972252672 (by decide +kernel)) (RegionPosI.of_check c4 q4 ok_4 3659174697238528 3940649673949184 0 4611686018427387904 3746994889972252672 4035225266123964416 (by decide +kernel))))

end CKLaneC.RSC2.S02_0051

end