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

import Definitions.Def_CK_CKLaneC_RSCell_Staged
import Definitions.Def_CK_CKLaneC_RSCell_RegionI

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

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

namespace CKLaneC.RSC2.S07_0027
open CKLaneC.TM3 CKLaneC.RSCell

noncomputable def c0 : Cell := { bc := 112589990684262400, bh := 4503599627370496, tc := 16140901064495857664, th := 2305843009213693952, sc := 3602879701896396800, sh := 144115188075855872 }
noncomputable def q0 : Cert := { V0 := [[[2339793700795028689]], [[(-37995944190648174), 326546080096086551], [14407498235852806]], [[287944796145388, (-5053933247040649), (-1607374563259323)], [(-228564240920715), 1916376494699073], [(-199700991303292)]], [[(-3089791643620), 32288879032940, 76540284732665, (-66185110729459)], [1848135358630, (-25843049683107), (-29022940230790)], [3231950778123, (-27427037929133)], [4692949894968]], [[45964161346, (-288683766619), (-1752059698450), 2819096147915, 1034268044365], [(-24898964314), 103479359746, 1349248136458, (-1068959428250)], [(-26098551454), 407575200422, 233770445862], [(-76054293011), 646481078654], [(-130163269635)]]], r0 := 14500604843945, V1 := [[[2664667274220772019]], [[(-42970599197035419), 0], [16293813598062994]], [[318433412361873, 0, 0], [(-253020751977394), 0], [(-226883815882760)]], [[(-3349206263238), 0, 0, 0], [1921153235405, 0, 0], [3627648519714, 0], [5334167002420]], [[49618175418, 0, 0, 0, 0], [(-25147912949), 0, 0, 0], [(-28251477587), 0, 0], [(-85495274891), 0], [(-147997632972)]]], r1 := 4173610910766, V2 := [[[18317964816916805932]], [[(-1045802931637972), 93040397441474], [(-5114318247781690)]], [[2360645271835, (-129851592618), (-63019019576)], [(-42922690171802), 7514590690533], [924673511769]], [[(-35972509705), (-9154877170), 691897167, 41611021], [109267260114, (-9296202803), (-7656338102)], [(-28598539555), 153656766131], [(-9323048606)]], [[749647010, 41921628, 5471443, (-856961), (-27091)], [(-1655841206), (-761397319), 83181568, 6743574], [388959904, (-135055385), (-312595543)], [251655360, 62249397], [158247512]]], r2 := 278270465992, V3 := [[[18402701518418914058]], [[(-1761145623846273), 62172988716165], [(-1764236164644591)]], [[23387559929, 1928826426132, (-82917161743)], [(-70524934611664), 5027610639365], [(-102702102618)]], [[22560748, (-23443422753), (-1808371558), 108182432], [1881847686, 156410806099, (-10067919309)], [(-3218829530), 103111743502], [(-42738650)]], [[(-302341), (-22314696), 55958701, 1350531, (-139474)], [2055325, (-1888619336), (-220592379), 17511099], [38139245, 3227882119, (-410707047)], [(-1728314), 48442908], [248072]]], r3 := 1147252685739, Vm := [[[18318106533118807040]], [[(-1046897818145591), 0], [(-5102525875172614)]], [[2358542862025, 0, 0], [(-43015568277045), 0], [1182261243466]], [[(-36027092611), 0, 0, 0], [109087726222, 0, 0], [(-30700756574), 0], [(-8910945606)]], [[751541934, 0, 0, 0, 0], [(-1660004911), 0, 0, 0], [384571202, 0, 0], [247296937, 0], [156129058]]], rm := 50222199397 }
noncomputable def w0 : Wit := { Z0 := { p := [[[2367341804289074237]], [[(-39350992777623258), 338191686327010605], [14921312553201538]], [[320752061472005, (-5621570396803323), 0], [(-253807897553687), 2131616079028791], [(-203582336266047)]], [[(-3675387961131), 45821723067429, 0, 0], [2466940500996, (-36258271079099), 0], [3423594269241, (-29083190895150)], [4777774312620]], [[55755166713, (-525055423019), 0, 0, 0], [(-36373189197), 352420071570, 0, 0], [(-30723872441), 489084895605, 0], [(-80234976147), 682539187517], [(-132371811265)]]], r := 3092724653271, ok := true }, Z1 := { p := [[[2705533490616084842]], [[(-44972563174426580), 0], [17052928632230329]], [[366573784539434, 0, 0], [(-290066168632785), 0], [(-232665527161197)]], [[(-4200443384150), 0, 0, 0], [2819360572566, 0, 0], [3912679164847, 0], [5460313500137]], [[63720190530, 0, 0, 0, 0], [(-41569359082), 0, 0, 0], [(-35112997075), 0, 0], [(-91697115596), 0], [(-151282070017)]]], r := 1088843998537, ok := true }, Z2 := { p := [[[546508440207466917676]], [[(-3801379473242860671), 338191686327010605], [(-18589988437208559551)]], [[37522092689016740, (-5621570396803323), 0], [127046571278683602, 2131616079028791], [695503396290977758]], [[(-487297021996782), 45821723067429, 0, 0], [(-1180052269725401), (-36258271079099), 0], [(-4743600799027319), (-29083190895150)], [(-26702183618189701)]], [[8175903198690, (-525055423019), 0, 0, 0], [14331949120590, 352420071570, 0, 0], [43277195297044, 489084895605, 0], [181856065861327, 682539187517], [1037177148380961]]], r := 139213020001329, ok := true }, Z3 := { p := [[[1382301206231855142364]], [[(-48251971670362409241), 1703419211661990437], [(-48336646489427548960)]], [[1823492190939879110, (-75856624974786158), 0], [1719854166529405429, 8818194090353561], [1826440842404012755]], [[(-70405748034002027), 2818042490924556, 0, 0], [(-65449322478158422), (-346831481275967), 0], [(-65442830070946476), (-130608973209089)], [(-70517201685355426)]], [[2745376817238664, (-108341998655776), 0, 0, 0], [2537120974644192, 11871054660048, 0, 0], [2496462997911104, 5378647448102, 0], [2536811621987651, 3111652697622], [2749680286964530]]], r := 4912920292503268, ok := true }, iE := { p := [[[550865531156553743630]], [[(-3808519193273754930), 0], [(-18562525771802042989)]], [[37661070491948402, 0, 0], [126990932950894816, 0], [695128703142260638]], [[(-489598174248647), 0, 0, 0], [(-1178516199728973), 0, 0], [(-4742914001245902), 0], [(-26693390127880619)]], [[8220495882100, 0, 0, 0, 0], [14303868470685, 0, 0, 0], [43260554750063, 0, 0], [181840153294068, 0], [1036933518154127]]], r := 137594439947212, ok := true }, iHu := { p := [[[1387312235563249153068]], [[(-48310705588365635084), 0], [(-48310705588365635084)]], [[1826056623774086990, 0, 0], [1719685024013558546, 0], [1826056623774086990]], [[(-70508047988584748), 0, 0, 0], [(-65439614063816518), 0, 0], [(-65439614063816518), 0], [(-70508047988584748)]], [[2749424201466468, 0, 0, 0, 0], [2536731047279773, 0, 0, 0], [2496304289643722, 0, 0], [2536731047279773, 0], [2749424201466468]]], r := 4883066354459980, ok := true }, T := { p := [[[16140901064495857664]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[617723106048237385]], [[4270752429497697, 0], [20815426682776563]], [[(-12705225591500), 0, 0], [145419645996907, 0], [(-78077434374817)]], [[169200822741, 0, 0, 0], [(-508815579097), 0, 0], [(-508815579097), 0], [1035477599087]], [[(-3384021280), 0, 0, 0, 0], [6768013605, 0, 0, 0], [(-24291175), 0, 0], [6768013605, 0], [(-20710214221)]]], r := 17488633889, ok := true }, de := { p := [[[(-89564169990259515701)]], [[532895785193347947, 0], [532895785193347947]], [[(-10645195314389534), 0, 0], [25440778954851, 0], [(-10645195314389534)]], [[283872279903301, 0, 0, 0], [1214558741, 0, 0], [1214558741, 0], [283872279903301]], [[(-8516168382604), 0, 0, 0, 0], [57984, 0, 0, 0], [24378151, 0, 0], [57984, 0], [(-8516168382604)]]], r := 2838722801619, ok := true }, dde := { p := [[[(-11175634617098000335034)]], [[446491852879252794414, 0], [446491852879252794388]], [[(-17859699586313034268), 0, 0], [(-17859725057455958082), 0], [(-17859699586313034363)]], [[714387982236514288, 0, 0, 0], [714387979804496876, 0, 0], [714387979804496880, 0], [714387982236514226]], [[(-28575519289517702), 0, 0, 0, 0], [(-28575519289691847), 0, 0, 0], [(-28575519338448833), 0, 0], [(-28575519289691845), 0], [(-28575519289517761)]]], r := 7222223697937091, ok := true }, nJu := { p := [[[(-179128339980519031402)]], [[1065791570386695895, 0], [1065791570386695895]], [[(-21290390628779067), 0, 0], [50881557909702, 0], [(-21290390628779067)]], [[567744559806603, 0, 0, 0], [2429117483, 0, 0], [2429117483, 0], [567744559806603]], [[(-17032336765207), 0, 0, 0, 0], [115969, 0, 0, 0], [48756302, 0, 0], [115969, 0], [(-17032336765207)]]], r := 5677445603226, ok := true }, Jd1 := { p := [[[(-22351269234196000670068)]], [[892983705758505588829, 0], [892983705758505588776]], [[(-35719399172626068535), 0, 0], [(-35719450114911916164), 0], [(-35719399172626068726)]], [[1428775964473028577, 0, 0, 0], [1428775959608993752, 0, 0], [1428775959608993760, 0], [1428775964473028452]], [[(-57151038579035403), 0, 0, 0, 0], [(-57151038579383694), 0, 0, 0], [(-57151038676897665), 0, 0], [(-57151038579383690), 0], [(-57151038579035521)]]], r := 14444447395874176, ok := true }, term0 := { p := [[[9454330698399495959690941]], [[(-755001648968773542606899), 0], [(-752715610682031768255362)]], [[45273309655909396274433, 0, 0], [60163670029304007594526, 0], [45090426332145550954473]], [[(-2413862126985026041058), 0, 0, 0], [(-3608748609075168194625), 0, 0], [(-3605090942618569185440), 0], [(-2402889127577873101219)]], [[120671674709783466735, 0, 0, 0, 0], [192438016965885830248, 0, 0, 0], [216262593279182117544, 0, 0], [192145403648359369569, 0], [120086448074734221585]]], r := 57742397202312351469, ok := true }, r0 := { p := [[[7393188125890003376863]], [[(-206004248256374940794), 2037656489062728508748], [(-247095103027554143727)]], [[5427424300171516984, (-54525758590896172032), 125066673188822516377], [6581641436596073892, (-68986372944943824500)], [9224320732845600943]], [[(-160094788416734256), 1405285369799951779, (-2733481498206677768), (-2690455564702056893)], [(-162679974412454735), 1788420233142601123, (-4475153850399169831)], [(-242345730652856926), 2581793178433494414], [(-353551338551385965)]], [[5294294266627639, (-41574223171142681), 62446578346248446, 145167481136438277, (-56758028983062852)], [4567981254592361, (-43516075073779005), 102172098176342376, 62269352334505712], [5871323686278255, (-66183727255938231), 169343359405795484], [9212162127874556, (-99098419450540270)], [13715717482151626]]], r := 216959871397385801, ok := true }, r1 := { p := [[[9553166950146229884034]], [[(-263116743471388470382), 0], [(-320492602693554914118)]], [[6890698098362315981, 0, 0], [8468710081674128529, 0], [11973324674050546462]], [[(-203456071342314528), 0, 0, 0], [(-208382125508820468), 0, 0], [(-312290968355558464), 0], [(-459114022171754328)]], [[6751639308379487, 0, 0, 0, 0], [5856807958513538, 0, 0, 0], [7533349896659054, 0, 0], [11881153279350875, 0], [17816125986404431]]], r := 34311335902423208, ok := true }, r2 := { p := [[[1200953722539725390491677]], [[(-42489784123167399299234), 1829554541184327465595], [(-91224465884826615900830)]], [[1477009761194708577208, (-46641026870014324701), 457316398092893597], [3148424505017935452914, (-68982416577518484489)], [5310897206851990898729]], [[(-54209849453509650649), 1388662777909344107, 588846882287103, (-292664182574784)], [(-108047224040428412230), 1633540192188619636, 73824532525106], [(-180470228046880869100), 2707163331075490409], [(-277403063776810739465)]], [[2063138597675480460, (-47128748217430097), (-11529520474998), 2574477670232, 184377522505], [3946835788620647904, (-46502122182993310), 9872240969661, (-11950620389423)], [6143695664594739576, (-62289980815418549), (-2797981537826)], [9321535490333236243, (-107052350937946602)], [13653317910066298886]]], r := 43559563031883890324, ok := true }, r3 := { p := [[[18738398880769638625111356]], [[(-1497492540287417147781571), 33581171555735352291767], [(-1498617745059542766915026)]], [[89818048082028884311936, (-2473634279062566892982), 1486295357454734640], [119826582835992636216147, (-1348402342237794036955)], [89908235977334320110143]], [[(-4789454945188082070860), 144203037256526287016, 23983973814326718, (-2068806955702426)], [(-7188337911160736633133), 99270826706759736752, (-3095527164033973)], [(-7190147273701719904228), 54013937922926116630], [(-4794871839075670001938)]], [[239447490945475625843, (-7579258350921765546), (-1179234594962851), 4464530204798, 2657058072700], [383344473304268361838, (-5784523585782805570), 195928229577105, (-80974656530293)], [431358589159244002027, (-3975166818964571195), 25541446086231], [383489323279351081921, (-2162306495733620760)], [239736592256577555643]]], r := 7083220845268838523337, ok := true }, eta := { p := [[[(-1225283425583762794967479)]], [[43589641840536231727173, 0], [92163816382225396989598]], [[(-1521773954945568839589), 0, 0], [(-3190754575226695847643), 0], [(-5348047213846363812255)]], [[56002383813998729606, 0, 0, 0], [109766179850271489138, 0, 0], [182142139503986870186, 0], [278879270765497550826]], [[(-2134754476351739267), 0, 0, 0, 0], [(-4015627661484648387), 0, 0, 0], [(-6211551758764835845), 0, 0], [(-9387921657607377462), 0], [(-13712097429743057288)]]], r := 4945181083991484198, 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 := 112589990684262400, bh := 4503599627370496, tc := 16140901064495857664, th := 2305843009213693952, sc := 3891110078048108544, sh := 144115188075855872 }
noncomputable def q1 : Cert := { V0 := [[[2264929581168662426]], [[(-36879839846191561), 316565122617658408], [13957569996649070]], [[270441898508603, (-4928117235151893), (-1461078480885533)], [(-221456844474168), 1865098697505007], [(-193338945310166)]], [[(-2754984687704), 30648783680738, 69864357756257, (-60747671225641)], [1708797806067, (-25437440014974), (-26440913727412)], [3131323464112, (-26621427967764)], [4543225232068]], [[38093638107, (-258998295088), (-1589165958859), 2620370066673, 885567795579], [(-21660748543), 99437201323, 1234611343227, (-991707089166)], [(-24255363608), 398125697960, 212017590494], [(-73698605118), 627324659701], [(-126005779765)]]], r0 := 13744138792361, V1 := [[[2579973779823376008]], [[(-41735542302892265), 0], [15795262546425683]], [[299455940291939, 0, 0], [(-245624017150713), 0], [(-219738834524590)]], [[(-2987989510393), 0, 0, 0], [1780506271552, 0, 0], [3518634263832, 0], [5165770442131]], [[41075414887, 0, 0, 0, 0], [(-21852378543), 0, 0, 0], [(-26298462012), 0, 0], [(-82931377988), 0], [(-143316953304)]]], r1 := 3975720127965, V2 := [[[18315882377293273052]], [[(-1036769406923620), 92744397948012], [(-5199739278203219)]], [[2161447530560, (-165992118103), (-61614036983)], [(-42504448186962), 7492980822947], [868989488570]], [[(-30635580201), (-8921075285), 712742639, 39900732], [100099570587, (-12300107665), (-7487308130)], [(-27106016187), 153320967725], [(-8832880581)]], [[592701104, 36225466, 4957137, (-852967), (-25477)], [(-1409703048), (-741050502), 85805551, 6467527], [358141089, (-200420718), (-305803825)], [238701413, 63955072], [149806959]]], r2 := 276269928457, V3 := [[[18399179320897297876]], [[(-1761051812086497), 65936694026920], [(-1905278490453593)]], [[23516127885, 1834794202867, (-86312064178)], [(-70517383387019), 5332861986176], [(-108986791053)]], [[20366683, (-23570488362), (-1587536510), 110507413], [1893567005, 148832849287, (-10482192214)], [(-3065657192), 109413444523], [(-46156603)]], [[(-248667), (-20112183), 54450389, 978437, (-139791)], [1857516, (-1900160329), (-193800060), 17890937], [38441911, 3073621856, (-427743104)], [(-1688795), 52102197], [268418]]], r3 := 1018049297825, Vm := [[[18316021894904617184]], [[(-1037873301526887), 0], [(-5188133410923206)]], [[2159059070039, 0, 0], [(-42598089803393), 0], [1122354723095]], [[(-30676964556), 0, 0, 0], [99898417365, 0, 0], [(-29226528373), 0], [(-8429588232)]], [[594132179, 0, 0, 0, 0], [(-1412796529), 0, 0, 0], [353403704, 0, 0], [234250787, 0], [147742393]]], rm := 49550238495 }
noncomputable def w1 : Wit := { Z0 := { p := [[[2289894283044914064]], [[(-38110386588338448), 327127754720702009], [14423283577816840]], [[299957350809177, (-5444340941191207), 0], [(-244356728390354), 2060469082545262], [(-196854876332148)]], [[(-3268737177674), 42851050115596, 0, 0], [2263368677806, (-34908104055765), 0], [3305398276113, (-28122125190307)], [4620078120819]], [[46324410744, (-466962453954), 0, 0, 0], [(-31644170813), 323338382543, 0, 0], [(-28423983062), 472199753730, 0], [(-77496113193), 660011160117], [(-128006814895)]]], r := 2967517601110, ok := true }, Z1 := { p := [[[2617022037765616073]], [[(-43554727529529655), 0], [16483752660362102]], [[342808400924774, 0, 0], [(-279264832446119), 0], [(-224977001522455)]], [[(-3735699631627), 0, 0, 0], [2586707060350, 0, 0], [3777598029844, 0], [5280089280936]], [[52942183707, 0, 0, 0, 0], [(-36164766643), 0, 0, 0], [(-32484552071), 0, 0], [(-88566986506), 0], [(-146293502737)]]], r := 1034469172673, ok := true }, Z2 := { p := [[[539051996894672390114]], [[(-3656889858082345027), 327127754720702009], [(-18340504363025258025)]], [[34781886202602935, (-5444340941191207), 0], [122491382982163829, 2060469082545262], [686185308395508272]], [[(-428071030060512), 42851050115596, 0, 0], [(-1099200075808172), (-34908104055765), 0], [(-4576424815580069), (-28122125190307)], [(-26344888634964521)]], [[6699023148937, (-466962453954), 0, 0, 0], [12672282466602, 323338382543, 0, 0], [40369491085101, 472199753730, 0], [175511554358587, 660011160117], [1023311608084371]]], r := 133585498226470, ok := true }, Z3 := { p := [[[1292568717953711038560]], [[(-41722887703766614218), 1562173958518208108], [(-45139910112816581454)]], [[1459249338036168815, (-65761704667856959), 0], [1485612651464397128, 8168751707360291], [1704821984498882350]], [[(-52154191101656263), 2257374843814777, 0, 0], [(-52328821925889514), (-304127981012795), 0], [(-56509469085084051), (-120554595667950)], [(-65803291363115281)]], [[1882676714488094, (-80305072347294), 0, 0, 0], [1877848317692456, 9591352539516, 0, 0], [1995350754297286, 4700065859832, 0], [2190052879885728, 2869718769523], [2565376649740734]]], r := 3763364871889804, ok := true }, iE := { p := [[[543395346588538344514]], [[(-3663499929619241460), 0], [(-18313147045800572901)]], [[34908052540026504, 0, 0], [122441569450121466, 0], [685811924535308259]], [[(-430051950481489), 0, 0, 0], [(-1097819615307591), 0, 0], [(-4575801240003628), 0], [(-26336125516492075)]], [[6734912019684, 0, 0, 0, 0], [12648339002938, 0, 0, 0], [40354478716901, 0, 0], [175497070749482, 0], [1023068811565598]]], r := 132019387837458, ok := true }, iHu := { p := [[[1297471778793812741238]], [[(-41772473662479302302), 0], [(-45114271555477638758)]], [[1461285674017372754, 0, 0], [1485478109378351673, 0], [1704443610173865122]], [[(-52229624250628387), 0, 0, 0], [(-52321128650623260), 0, 0], [(-56506818942679358), 0], [(-65794284424006976)]], [[1885443301708372, 0, 0, 0, 0], [1877560153330482, 0, 0, 0], [1995224875393863, 0, 0], [2189986162848892, 0], [2565124796680624]]], r := 3739367972506536, ok := true }, T := { p := [[[16140901064495857664]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[626215091934900138]], [[4221859755761116, 0], [21104282789500871]], [[(-11765221127977), 0, 0], [143461512594015, 0], [(-79095162706989)]], [[145062399333, 0, 0, 0], [(-471215516402), 0, 0], [(-508912757713), 0], [1049013621534]], [[(-2686345198), 0, 0, 0, 0], [5802476664, 0, 0, 0], [(-24298134), 0, 0], [6768008780, 0], [(-20980935925)]]], r := 16861767439, ok := true }, de := { p := [[[(-88538816305139333400)]], [[493469140379589375, 0], [532946671609956525]], [[(-9126537026526790), 0, 0], [25445637885708, 0], [(-10645192787740849)]], [[225346968218782, 0, 0, 0], [1214906710, 0, 0], [1312099247, 0], [283872280028819]], [[(-6259637992650), 0, 0, 0, 0], [58006, 0, 0, 0], [24392105, 0, 0], [67659, 0], [(-8516168382597)]]], r := 2382382634327, ok := true }, dde := { p := [[[(-10348797946853366169136)]], [[382794707565094237809, 0], [413418284170301776639]], [[(-14177605352818643720), 0, 0], [(-15311839259484502623), 0], [(-16536758883527666501)]], [[525096493422475613, 0, 0, 0], [567104210463327885, 0, 0], [612472547300393909, 0], [661470353922213394]], [[(-19448018274959257), 0, 0, 0, 0], [(-21003859737131038), 0, 0, 0], [(-22684168564885751), 0, 0], [(-24498901997389500), 0], [(-26458814156961100)]]], r := 5556902057185466, ok := true }, nJu := { p := [[[(-177077632610278666800)]], [[986938280759178750, 0], [1065893343219913051]], [[(-18253074053053580), 0, 0], [50891275771417, 0], [(-21290385575481697)]], [[450693936437565, 0, 0, 0], [2429813421, 0, 0], [2624198495, 0], [567744560057638]], [[(-12519275985300), 0, 0, 0, 0], [116013, 0, 0, 0], [48784210, 0, 0], [135318, 0], [(-17032336765194)]]], r := 4764765268646, ok := true }, Jd1 := { p := [[[(-20697595893706732338272)]], [[765589415130188475619, 0], [826836568340603553278]], [[(-28355210705637287439), 0, 0], [(-30623678518969005245), 0], [(-33073517767055333001)]], [[1050192986844951227, 0, 0, 0], [1134208420926655770, 0, 0], [1224945094600787818, 0], [1322940707844426788]], [[(-38896036549918514), 0, 0, 0, 0], [(-42007719474262075), 0, 0, 0], [(-45368337129771501), 0, 0], [(-48997803994778999), 0], [(-52917628313922200)]]], r := 11113804114370924, ok := true }, term0 := { p := [[[8107871004532204723709492]], [[(-599429715688737332632021), 0], [(-645424184041103036443692)]], [[33280384711024295202575, 0, 0], [47763263669450124051765, 0], [38661447753820846682335]], [[(-1642950691691808797069), 0, 0, 0], [(-2652663982060545265919), 0, 0], [(-2861973527067816356167), 0], [(-2060237123365577858942)]], [[76047946009061874161, 0, 0, 0, 0], [130974748341865395502, 0, 0, 0], [158964503029829848095, 0, 0], [152536660580346668135, 0], [102960653463103570736]]], r := 41021585376649607227, ok := true }, r0 := { p := [[[7001687660938007164142]], [[(-186060117740823183325), 1933914298163548579729], [(-234548195107134428747)]], [[4580355368907156210, (-49362644762410374665), 119835277646981224502], [5981411335208517078, (-65574387106781817799)], [8761893729077538610]], [[(-124293623944498303), 1185643660763372693, (-2504548164273742344), (-2417056696168484099)], [(-138429239681538535), 1627892081638490444, (-4279494294237061648)], [(-220655464519173929), 2455415150629005896], [(-335963444782469235)]], [[3764672764092650, (-32178909502459875), 52478631368558914, 128658747769665187, (-53182181296941751)], [3571446032448250, (-37017215129459126), 93718533013538777, 55789898711924813], [5008861175021241, (-60348962888364423), 161912119604601633], [8397094419969059, (-94277818342443515)], [13037098781379927]]], r := 188254569785091037, ok := true }, r1 := { p := [[[9052969450758052901218]], [[(-237797079809900561612), 0], [(-304344684137244847591)]], [[5814655800752511015, 0, 0], [7699900741590201062, 0], [11377308828655242273]], [[(-157822849924093566), 0, 0, 0], [(-177300597442086672), 0, 0], [(-284461897171601143), 0], [(-436425961298056967)]], [[4795908433059434, 0, 0, 0, 0], [4575692358680007, 0, 0, 0], [6426302964354896, 0, 0], [10834353501016883, 0], [16940214805855013]]], r := 30118588965749148, ok := true }, r2 := { p := [[[1121479148965425903670589]], [[(-37172096007770761404510), 1741475708604815091949], [(-85330458509925322074151)]], [[1195539139793949221247, (-41601620056345454160), 458450675378283198], [2759222863317372445153, (-65889785666486205802)], [4972867640883816202627]], [[(-40466462854460805179), 1142523740115436760, 546692190137662, (-287490820470081)], [(-87550104301037531360), 1464481130642506595, 92876713797545], [(-158332732281561564515), 2589123835703663876], [(-259936667670166162883)]], [[1420998542281458148, (-35614623672082987), (-9633574963889), 2598254208652, 177576967784], [2947526339000625288, (-38402874985005533), 9201719958735, (-11749728400519)], [4981501270016320076, (-55950181081293538), (-2914614298160)], [8184494006601776583, (-102463130015220337)], [12800849789109699495]]], r := 38087332604032175013, ok := true }, r3 := { p := [[[16067865191773542925785880]], [[(-1188857888290021337100751), 29155566614825482745542], [(-1284930913501903435657741)]], [[66022654947156655802798, (-1977042158456273083516), 1529966086927478586], [95126196118665916461591, (-1170787090467443584347)], [77086127514601781163960]], [[(-3259760047818707505991), 106486046668021194439, 19878483271748196, (-2056855856492769)], [(-5283790898049637478946), 79349916198200154699, (-2734711480602370)], [(-5707930266567971656377), 46901481500735804716], [(-4111001958628603564809)]], [[150897633614758568860, (-5176411799501865599), (-890860867380361), 7351260693689, 2579975547383], [260903290927264948198, (-4271886877533266479), 166256604766405, (-80818378689234)], [317067353311687443383, (-3177545861078877197), 20657123474381], [304432568147252877895, (-1877627952843685545)], [205542373072839554005]]], r := 4918683560381612649942, ok := true }, eta := { p := [[[(-1143774914147983267872366)]], [[38112324469504958961048, 0], [86191515073746050125818]], [[(-1231062682913507138626), 0, 0], [(-2795422682083337871389), 0], [(-5006925134334889276594)]], [[41784489454251586384, 0, 0, 0], [88914429522300026013, 0, 0], [159762647716335265960, 0], [261290077980400230546]], [[(-1469762127182082706), 0, 0, 0, 0], [(-2998109215323031552), 0, 0, 0], [(-5035359808397202503), 0, 0], [(-8241274186470696694), 0], [(-12854742212898958778)]]], r := 4395216638880244717, 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 := 121597189939003392, bh := 4503599627370496, tc := 16140901064495857664, th := 2305843009213693952, sc := 3746994889972252672, sh := 288230376151711744 }
noncomputable def q2 : Cert := { V0 := [[[2329693200212101344]], [[(-75733741885373810), 325202163654578845], [13446378085756386]], [[1129593869218131, (-10079886929765186), (-1587110512073312)], [(-426108955732471), 1789664254599212], [(-171580696632995)]], [[(-23677988562608), 126561332809943, 151320600092573, (-65437819875253)], [6728133181493, (-48268123647817), (-26866677261081)], [5553753901411, (-23586505040051)], [3730195796247]], [[680804790377, (-2194892464184), (-6897899414939), 5587339509869, 1013158799432], [(-176367704776), 370284303610, 2499357847569, (-992021226906)], [(-87879257950), 702301867951, 196532010819], [(-120911855370), 514226448870], [(-95739048073)]]], r0 := 25112866971216, V1 := [[[2653243847137413243]], [[(-85656880080421924), 0], [15208211908384342]], [[1249066655945383, 0, 0], [(-471808232185270), 0], [(-194961829410298)]], [[(-25645219601002), 0, 0, 0], [6986197187057, 0, 0], [6236020115403, 0], [4240316811526]], [[733699472822, 0, 0, 0, 0], [(-177561824263), 0, 0, 0], [(-95144741089), 0, 0], [(-135961752075), 0], [(-108867494712)]]], r1 := 8110839446112, V2 := [[[18306610588401422037]], [[(-2253428156934978), 108525025815646], [(-5153651682121399)]], [[9870058503397, (-340641019493), (-78738249940)], [(-85635048146925), 8119304127457], [845455385910]], [[(-289749753011), (-42403835406), 1771160750, 55671368], [423814612146, (-22940383739), (-8861374902)], [(-52922090570), 153875888962], [(-7965079970)]], [[11629608323, 368085125, 26552905, (-2333462), (-38804)], [(-12364094471), (-3265960900), 197322292, 8357398], [1419061131, (-325999199), (-335242229)], [429284229, 60492627], [124836561]]], r2 := 583414690910, V3 := [[[18397270453891531804]], [[(-3804307390060626), 74868214318795], [(-1835183271842119)]], [[109529817334, 4399494185718, (-106958250003)], [(-141067509260815), 5607931022175], [(-106143558966)]], [[204133463, (-109808228674), (-4292899694), 149436882], [8164600021, 330505682266, (-12030167305)], [(-6304832125), 106597034149], [(-42525023)]], [[(-5208011), (-201615928), 278918699, 3181226, (-206272)], [17245864, (-8195866706), (-485258146), 22406565], [153410152, 6323295008, (-454738959)], [(-3265894), 48381477], [225967]]], r3 := 8274461650144, Vm := [[[18306775631337114027]], [[(-2256016607915909), 0], [(-5140925618977568)]], [[9859434083513, 0, 0], [(-85838539883000), 0], [1103334779752]], [[(-290189196534), 0, 0, 0], [422975657504, 0, 0], [(-57196104127), 0], [(-7573007131)]], [[11660334967, 0, 0, 0, 0], [(-12394631634), 0, 0, 0], [1400188779, 0, 0], [420875953, 0], [123006950]]], rm := 160123118138 }
noncomputable def w2 : Wit := { Z0 := { p := [[[2356882679940164055]], [[(-78410805200936807), 336697525705737722], [13921685453442660]], [[1258641199784211, (-11201543600133830), 0], [(-472816676547468), 1988812207634665], [(-174836496607004)]], [[(-28231695116012), 179805885683458, 0, 0], [9004479013468, (-67545239506782), 0], [5875746096193, (-24976642372430)], [3796279888856]], [[830127769005, (-4033099302288), 0, 0, 0], [(-259636900125), 1286354144781, 0, 0], [(-103358562882), 839392299456, 0], [(-127433740725), 542325698408], [(-97331572402)]]], r := 4677644518181, ok := true }, Z1 := { p := [[[2693580205645901777]], [[(-89612348801070637), 0], [15910497661077325]], [[1438447085467669, 0, 0], [(-540361916054249), 0], [(-199813138979433)]], [[(-32264794418299), 0, 0, 0], [10290833158249, 0, 0], [6715138395649, 0], [4338605587264]], [[948717450292, 0, 0, 0, 0], [(-296727885857), 0, 0, 0], [(-118124071865), 0, 0], [(-145638560829), 0], [(-111236082745)]]], r := 2099223169350, ok := true }, Z2 := { p := [[[508382210376473961399]], [[(-6991232474659868033), 336697525705737722], [(-15989139432845125090)]], [[135944781047329211, (-11201543600133830), 0], [216071714878407838, 1988812207634665], [553514569484727569]], [[(-3448703272891691), 179805885683458, 0, 0], [(-3954044633984697), (-67545239506782), 0], [(-7467563774278958), (-24976642372430)], [(-19669579479806446)]], [[111991411124992, (-4033099302288), 0, 0, 0], [93783801452951, 1286354144781, 0, 0], [134248611459544, 839392299456, 0], [265028114749098, 542325698408], [707245720320378]]], r := 284196347435632, ok := true }, Z3 := { p := [[[1248993757131682879409]], [[(-83677599571276478326), 1646762949479962317], [(-40365752610401617438)]], [[6076819877182478470, (-142318009112249566), 0], [2757696009831374497, 8014516140374815], [1411217468633141107]], [[(-451018375975457281), 10149626007484287, 0, 0], [(-201707642249145835), (-611213440621037), 0], [(-97107942408929389), (-109312200910281)], [(-50428407561569121)]], [[33811009405360778, (-749918527722584), 0, 0, 0], [15031917772332850, 40068943807595, 0, 0], [7120334092396971, 8740447098189, 0], [3484300618939744, 2408322454778], [1820167671494083]]], r := 26983948502426634, ok := true }, iE := { p := [[[512785685859723511609]], [[(-7005175051485349406), 0], [(-15963128888874687402)]], [[136485509355651737, 0, 0], [215971313989640335, 0], [553187914181543057]], [[(-3466168130274414), 0, 0, 0], [(-3948460699685596), 0, 0], [(-7466419012240806), 0], [(-19662486710378246)]], [[112646367299882, 0, 0, 0, 0], [93584756861368, 0, 0, 0], [134193158785870, 0, 0], [265003535029647, 0], [707063871136088]]], r := 283013997604185, ok := true }, iHu := { p := [[[1253998624919318059003]], [[(-83785973747323611007), 0], [(-40341394767229890057)]], [[6086007951522227195, 0, 0], [2757416036750160584, 0], [1410885245277433391]], [[(-451724295885356531), 0, 0, 0], [(-201675245795721988), 0, 0], [(-97102896123867825), 0], [(-50421088150186951)]], [[33864747117040698, 0, 0, 0, 0], [15029406015931509, 0, 0, 0], [7119844237513297, 0, 0], [3484183287641045, 0], [1819978214712020]]], r := 26863734340279359, ok := true }, T := { p := [[[16140901064495857664]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[663595681986383168]], [[9065393289851072, 0], [20657876562777432]], [[(-52783313775181), 0, 0], [284926930803569, 0], [(-72796035586020)]], [[1351603700988, 0, 0, 0], [(-1957558637475), 0, 0], [(-942528232858), 0], [893552891423]], [[(-51984851304), 0, 0, 0, 0], [50059216116, 0, 0, 0], [(-97207573), 0, 0], [11604948592, 0], [(-16547890409)]]], r := 95365707807, ok := true }, de := { p := [[[(-88016239206471074334)]], [[1024950296761564136, 0], [493494587329641991]], [[(-39368311176848304), 0, 0], [50896524574379, 0], [(-9126535787225464)]], [[2018891386726635, 0, 0, 0], [5249208969, 0, 0], [2527396911, 0], [225346968279145]], [[(-116474502799284), 0, 0, 0, 0], [541377, 0, 0, 0], [97598568, 0, 0], [125504, 0], [(-6259637992647)]]], r := 39787855529003, ok := true }, dde := { p := [[[(-9951280392380128464777)]], [[764456782603238656220, 0], [368071784216374167834]], [[(-58804473742451884912), 0, 0], [(-28313316100018902407), 0], [(-13632312842900367720)]], [[4523421046194863339, 0, 0, 0], [2177943456173922089, 0, 0], [1048639441861518431, 0], [504900474444450670]], [[(-347955465093037590), 0, 0, 0, 0], [(-167534112824200100), 0, 0, 0], [(-80664573036479130), 0, 0], [(-38838498034690685), 0], [(-18700017572076587)]]], r := 55470747432794013, ok := true }, nJu := { p := [[[(-176032478412942148667)]], [[2049900593523128272, 0], [986989174659283982]], [[(-78736622353696608), 0, 0], [101793049148759, 0], [(-18253071574450927)]], [[4037782773453270, 0, 0, 0], [10498417938, 0, 0], [5054793822, 0], [450693936558291]], [[(-232949005598567), 0, 0, 0, 0], [1082755, 0, 0, 0], [195197137, 0, 0], [251009, 0], [(-12519275985293)]]], r := 79575711057997, ok := true }, Jd1 := { p := [[[(-19902560784760256929554)]], [[1528913565206477312440, 0], [736143568432748335668]], [[(-117608947484903769824), 0, 0], [(-56626632200037804814), 0], [(-27264625685800735439)]], [[9046842092389726678, 0, 0, 0], [4355886912347844179, 0, 0], [2097278883723036862, 0], [1009800948888901340]], [[(-695910930186075180), 0, 0, 0, 0], [(-335068225648400199), 0, 0, 0], [(-161329146072958260), 0, 0], [(-77676996069381370), 0], [(-37400035144153174)]]], r := 110941494865588023, ok := true }, term0 := { p := [[[7500958317428376336711323]], [[(-1151689961748426341667648), 0], [(-552705343283071672914817)]], [[132799097678230279762688, 0, 0], [84946652046167670783613, 0], [30651847549126854072330]], [[(-13615896853513259932037), 0, 0, 0], [(-9798269818136561471485), 0, 0], [(-4712522935354821547709), 0], [(-1512338028809719662420)]], [[1308959884700546299052, 0, 0, 0, 0], [1004783216474995061032, 0, 0, 0], [543631649531962743538, 0, 0], [232550873553544967673, 0], [69978609062508662619]]], r := 348868016435950555766, ok := true }, r0 := { p := [[[6744505615585086440486]], [[(-367859142084392859550), 1859366436572290530025], [(-208465986903214528506)]], [[18790578923155665150, (-97318941688878081180), 114258116948256612810], [10881436079612127487, (-58221924695493431983)], [7203860215149690962]], [[(-1065193365852675594), 4854908968258839208, (-4864570381434263389), (-2439098459082898993)], [(-521473702531370429), 2957004710791629843, (-3782480264977447115)], [(-371066340580799825), 2016924536524475310], [(-255617202470111174)]], [[67466997563339779, (-275659797290613560), 212775770657426541, 261039215139861227, (-51747577136820036)], [28103169530142235, (-139348757129418945), 168956995887355407, 51846038312028225], [17433657612814385, (-101345532644041168), 132470462819210848], [13061884038130846, (-71669668389713370)], [9180886671626199]]], r := 495970193899814551, ok := true }, r1 := { p := [[[8715641912907493731781]], [[(-469778750862579982664), 0], [(-270417070329169917011)]], [[23842526947518686474, 0, 0], [14001563130573903278, 0], [9351612636615353144]], [[(-1352420800400854913), 0, 0, 0], [(-667771896537833899), 0, 0], [(-478173569774831868), 0], [(-331968780636583908)]], [[85952581138586630, 0, 0, 0, 0], [36010991328898017, 0, 0, 0], [22362724748801753, 0, 0], [16846718514333797, 0], [11926616599611312]]], r := 91176896583183159, ok := true }, r2 := { p := [[[1002119548609046742806322]], [[(-68830104666034251433558), 1659279197588927489748], [(-70477765768134153790177)]], [[4607654860419260785356, (-82254891767306243058), 458050159643430618], [4721621305125182543000, (-57943090784957947094)], [3799199505466443280785]], [[(-324775979011751221709), 4714076383592449978, 1171285829571413, (-313812294791328)], [(-311915551411563415592), 2667971341967251497, 72808302410189], [(-250584994022348913209), 2106312400603221741], [(-183749782180161988261)]], [[23732839791842275728, (-306775706206770916), (-43386218419118), 5574347184811, 211675708695], [21874408090124413933, (-146023780278840974), 18608030291694, (-11878263914139)], [16417004810416057197, (-94235329555836460), (-2509995790172)], [11984116163256257560, (-77139771204504062)], [8374267040174203587]]], r := 110878910385044163753, ok := true }, r3 := { p := [[[14855214018835944755855706]], [[(-2282711977488626970797272), 28921398654282896695543], [(-1099975044151889400941966)]], [[263286100931876307201896, (-4085136145199647012101), 1503427376116914331], [169127303008560397581807, (-1075393741615307874021)], [61102315194648838562145]], [[(-26998377420551063602667), 457495786390124301881, 44276670163055951, (-2225154473264927)], [(-19510856249653092153048), 151820265243031162709, (-2821768273059374)], [(-9396669125738188378923), 39889374109390394422], [(-3017216297261525251255)]], [[2595690272529233632165, (-46216610789619662032), (-4145583152934136), 12296737428898, 3055785643017], [2000916764817311210235, (-16994351462980274181), 341884949119429, (-80685230014871)], [1084089206389109835374, (-5629320914644560577), 20076183364948], [464050621264672989909, (-1478628731122646617)], [139680899553064407111]]], r := 44127449468574870227792, ok := true }, eta := { p := [[[(-1023726795476701762982306)]], [[70716063516887248487550, 0], [71249578518904432439894]], [[(-4755481931888066759411), 0, 0], [(-4788775367494589270302), 0], [(-3827458097208489708379)]], [[336164132963096122096, 0, 0, 0], [317166408512282213469, 0, 0], [253040416472135635545, 0], [184789407492098875994]], [[(-24607861996078809370), 0, 0, 0, 0], [(-22278632583637589874), 0, 0, 0], [(-16608882292790195700), 0, 0], [(-12074380995497268279), 0], [(-8412594191096749433)]]], r := 12936955203562228436, 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 := 112589990684262400, bh := 4503599627370496, tc := 16140901064495857664, th := 2305843009213693952, sc := 4323455642275676160, sh := 288230376151711744 }
noncomputable def q3 : Cert := { V0 := [[[2156652583062118798]], [[(-70655433742359126), 302049874610599112], [13308021609695678]], [[990140824342241, (-9501757078454123), (-1265126804490433)], [(-423504694717540), 1789665448679250], [(-184155852949533)]], [[(-18820011553922), 113934418667050, 121962410902557, (-53306957462898)], [6126800623685, (-49712814865922), (-22971742071252)], [5986203362456, (-25447164309341)], [4327072250826]], [[472210291550, (-1789766432303), (-5511665006057), 4688832306752, 700305117294], [(-143012201225), 377659508901, 2163454956679, (-883146254400)], [(-87559282640), 769782271228, 182983229621], [(-140915713220), 599423423023], [(-120003154027)]]], r0 := 25184172348235, V1 := [[[2457384737996973785]], [[(-80030651506093467), 0], [15073853251892226]], [[1098396467168462, 0, 0], [(-470987831282404), 0], [(-209411757851339)]], [[(-20434200025109), 0, 0, 0], [6407737282160, 0, 0], [6737174095490, 0], [4922364140592]], [[508551601583, 0, 0, 0, 0], [(-144145252221), 0, 0, 0], [(-95171265177), 0, 0], [(-158795072380), 0], [(-136551201294)]]], r1 := 8359840917785, V2 := [[[18312790739915487886]], [[(-2049137711687666), 92167061603177], [(-5326387714973427)]], [[7657910914446, (-437208096246), (-59433382790)], [(-83878382728329), 7449491948403], [790773982269]], [[(-196574522521), (-34504175209), 1480626616, 37355467], [354950822206, (-33333655442), (-7224546676)], [(-50151385737), 152576680712], [(-8143572699)]], [[6871692780, 237377721, 16973306, (-1686302), (-23148)], [(-9041387568), (-2861506450), 178559413, 6056432], [1280225559, (-590321710), (-295218407)], [442373716, 66165691], [137948108]]], r2 := 611904266538, V3 := [[[18393896377637010252]], [[(-3521820381051886), 71228418366246], [(-2116813550080471)]], [[94748577771, 3385706900745, (-90591593683)], [(-141011948195999), 5762211486921], [(-117836532767)]], [[142020880, (-94956662387), (-2535663292), 112659031], [7636703572, 274769660929, (-11004952689)], [(-5667533807), 118284696747], [(-51123192)]], [[(-3050876), (-139901130), 208408985, 929633, (-138399)], [12971967, (-7661961759), (-309974329), 18244281], [155383436, 5680307200, (-449275631)], [(-3241130), 57375070], [298138]]], r3 := 6145300552706, Vm := [[[18312926923336662436]], [[(-2051376116802387), 0], [(-5315064657784859)]], [[7647138892135, 0, 0], [(-84068224194743), 0], [1037733923829]], [[(-196792260246), 0, 0, 0], [354056782150, 0, 0], [(-54451392636), 0], [(-7753818534)]], [[6887157907, 0, 0, 0, 0], [(-9056991786), 0, 0, 0], [1259989070, 0, 0], [433230887, 0], [135963954]]], rm := 134191924452 }
noncomputable def w3 : Wit := { Z0 := { p := [[[2178178047244339212]], [[(-72788411844964676), 311168292463477030], [13709770168567870]], [[1091347243435290, (-10398344549280668), 0], [(-463154375116344), 1958538595509695], [(-187185233551670)]], [[(-22229600646921), 155906749062184, 0, 0], [8019301959962, (-66164910730907), 0], [6287962282513, (-26740747650239)], [4393310410997]], [[575514233271, (-3175657235275), 0, 0, 0], [(-208556390228), 1145614565708, 0, 0], [(-101882818777), 898280326073, 0], [(-147499347348), 627615772999], [(-121727851501)]]], r := 5070418225499, ok := true }, Z1 := { p := [[[2489346339707816242]], [[(-83186756394245344), 0], [15668308764077566]], [[1247253992497475, 0, 0], [(-529319285847250), 0], [(-213925981201908)]], [[(-25405257882195), 0, 0, 0], [9164916525671, 0, 0], [7186242608586, 0], [5020926183997]], [[657730552309, 0, 0, 0, 0], [(-238350160261), 0, 0, 0], [(-116437507174), 0, 0], [(-168570682683), 0], [(-139117544573)]]], r := 2155599357977, ok := true }, Z2 := { p := [[[528383319752795987498]], [[(-6918162211936944378), 311168292463477030], [(-17982595315912517741)]], [[125037953636061203, (-10398344549280668), 0], [232438627193916053, 1958538595509695], [672807554700998980]], [[(-2862943018795025), 155906749062184, 0, 0], [(-3977826690138840), (-66164910730907), 0], [(-8691701107083668), (-26740747650239)], [(-25831705482576876)]], [[81634734383142, (-3175657235275), 0, 0, 0], [85528540091322, 1145614565708, 0, 0], [146375345977089, 898280326073, 0], [333504360732936, 627615772999], [1003390524265314]]], r := 309273572314693, ok := true }, Z3 := { p := [[[1179262659818405464257]], [[(-68393377395106912842), 1383248312375385951], [(-41108294103996419378)]], [[4302771757745397708, (-108221647080148736), 0], [2431770192053322861, 7334678684175812], [1551505339926215696]], [[(-276701939811776870), 6666141029095351, 0, 0], [(-154104733540975073), (-508675211412255), 0], [(-92453462481710304), (-107696367398111)], [(-59862292699140585)]], [[17974419581277453, (-426449149311841), 0, 0, 0], [9951287020168338, 28665312981902, 0, 0], [5873506219625972, 7821544913658, 0], [3582017385085600, 2560683538242], [2333137943074045]]], r := 18027970565589389, ok := true }, iE := { p := [[[532707923980706760104]], [[(-6929968137710516277), 0], [(-17955375626452474825)]], [[125478324217547142, 0, 0], [232354365059647965, 0], [672435912881615055]], [[(-2875818625984833), 0, 0, 0], [(-3973076751162036), 0, 0], [(-8690621477509783), 0], [(-25822982904180697)]], [[82060940616380, 0, 0, 0, 0], [85375064245294, 0, 0, 0], [146323424529299, 0, 0], [333479183374647, 0], [1003148843020789]]], r := 307642983963630, ok := true }, iHu := { p := [[[1184033455018230774988]], [[(-68471661578170017412), 0], [(-41082996946902017084)]], [[4308705270424846047, 0, 0], [2431579861383015961, 0], [1551133897352944661]], [[(-277099356267911262), 0, 0, 0], [(-154082419648245505), 0, 0], [(-92449451788948047), 0], [(-59853460953876034)]], [[18000703402889165, 0, 0, 0, 0], [9949765414793771, 0, 0, 0], [5873140480352473, 0, 0], [3581915549317929, 0], [2332891161013496]]], r := 17955942699396785, ok := true }, T := { p := [[[16140901064495857664]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[638778496813316729]], [[8309834396477322, 0], [21530574891165260]], [[(-42360863642639), 0, 0], [281560339487926, 0], [(-80622119694667)]], [[940003980695, 0, 0, 0], [(-1696861926161), 0, 0], [(-1018117155697), 0], [1069317636176]], [[(-31333530418), 0, 0, 0, 0], [37600004679, 0, 0, 0], [(-97234313), 0, 0], [13536001685, 0], [(-21387018483)]]], r := 60840552354, ok := true }, de := { p := [[[(-87134929121206029018)]], [[888371699098900704, 0], [533023019459340423]], [[(-29569968421809312), 0, 0], [50905857784855, 0], [(-10645188631851352)]], [[1314223519700221, 0, 0, 0], [4861715653, 0, 0], [2917029392, 0], [283872280255248]], [[(-65711175791547), 0, 0, 0, 0], [464314, 0, 0, 0], [97652196, 0, 0], [167154, 0], [(-8516168382585)]]], r := 20193983084711, ok := true }, dde := { p := [[[(-9315252427543289041081)]], [[620127184157342414564, 0], [372076310494405448503]], [[(-41341897241795360090), 0, 0], [(-24805189323860735592), 0], [(-14883083007046328910)]], [[2756126474671891136, 0, 0, 0], [1653675875065773639, 0, 0], [992205525039464338, 0], [595323318529128754]], [[(-183741764978900119), 0, 0, 0, 0], [(-110245058988735002), 0, 0, 0], [(-66147035588545916), 0, 0], [(-39688221235944283), 0], [(-23812932741264748)]]], r := 31462166658616724, ok := true }, nJu := { p := [[[(-174269858242412058036)]], [[1776743398197801409, 0], [1066046038918680846]], [[(-59139936843618623), 0, 0], [101811715569710, 0], [(-21290377263702704)]], [[2628447039400443, 0, 0, 0], [9723431306, 0, 0], [5834058784, 0], [567744560510497]], [[(-131422351583094), 0, 0, 0, 0], [928629, 0, 0, 0], [195304392, 0, 0], [334308, 0], [(-17032336765169)]]], r := 40387966169416, ok := true }, Jd1 := { p := [[[(-18630504855086578082161)]], [[1240254368314684829128, 0], [744152620988810897006]], [[(-82683794483590720180), 0, 0], [(-49610378647721471183), 0], [(-29766166014092657819)]], [[5512252949343782273, 0, 0, 0], [3307351750131547278, 0, 0], [1984411050078928676, 0], [1190646637058257509]], [[(-367483529957800238), 0, 0, 0, 0], [(-220490117977470003), 0, 0, 0], [(-132294071177091831), 0, 0], [(-79376442471888566), 0], [(-47625865482529496)]]], r := 62924333317233440, ok := true }, term0 := { p := [[[6570178753613944032089519]], [[(-874154561596860541482959), 0], [(-522905211366673527978786)]], [[87353444205124396670814, 0, 0], [69646280068396862171487, 0], [31320237605517986426470]], [[(-7761994469439118846870), 0, 0, 0], [(-6962147457254979833407), 0, 0], [(-4173055064112819669394), 0], [(-1668970666921677166126)]], [[646695066129535150847, 0, 0, 0, 0], [618747306704808325732, 0, 0, 0], [417206285862710958121, 0, 0], [222410357592517187327, 0], [83405273184935843474]]], r := 195493619442274531452, ok := true }, r0 := { p := [[[6481652404247639879339]], [[(-323143360349299442411), 1795701014772510943092], [(-217761156463199018564)]], [[14544988000344658454, (-86045729053982098714), 112758411676647653440], [10474285104303671992, (-61000154522611930939)], [8141847757021766382]], [[(-706188015951182931), 3766669986586120346, (-4448301106738504220), (-2063038977379403861)], [(-444664162038175340), 2857725674238049909, (-4014613624025325048)], [(-387356526161995312), 2285644577047840522], [(-312349826499991480)]], [[37963790416310844, (-182150537884249893), 166628830117131676, 216193587431773180, (-48000360604014026)], [20506148118626319, (-118928194199394614), 166500954130391606, 47416081107630661], [16146839695080647, (-106183891728408366), 151841354068607836], [14762914139785894, (-87794171812438248)], [12125141747415462]]], r := 398996172876743914, ok := true }, r1 := { p := [[[8388002724152219140074]], [[(-413418137031926163359), 0], [(-282727113964978648826)]], [[18465957128640840438, 0, 0], [13493276103130625841, 0], [10577706848938342692]], [[(-895743793924153407), 0, 0, 0], [(-569548622714345014), 0, 0], [(-499699777783431998), 0], [(-405949096032438599)]], [[48290913110922227, 0, 0, 0, 0], [26248128312711624, 0, 0, 0], [20717610576705956, 0, 0], [19059906691287022, 0], [15762541007231917]]], r := 74368327607880011, ok := true }, r2 := { p := [[[1019734055982249677038082]], [[(-61912458609197274115726), 1626079693033860443410], [(-77768715899083016424434)]], [[3585065834098958691698, (-71187735533774463576), 460010835138086377], [4607343550955243133048, (-61813166705960532945)], [4538618070225362448553]], [[(-217309456749231770618), 3507522668327566542, 990954205323689, (-279648552029627)], [(-262975345162459396478), 2523997803948737308, 119230556651296], [(-264799403802915126799), 2433171024349099471], [(-237477155538906600430)]], [[13667800535775261341, (-194758594337500182), (-30258080407600), 5257945036150, 167565776571], [15840755184232672808, (-118566568950915935), 16805618340084, (-11443541201658)], [14978502071835962237, (-96687540832691267), (-3070922180219)], [13703405664515709097, (-96391233512621550)], [11703877304907967343]]], r := 98750733377449614835, ok := true }, r3 := { p := [[[13018262428037846956254366]], [[(-1733573529048134278018762), 24060023735767640253731], [(-1040924946867175767493911)]], [[173284449599436000921767, (-2911849803365425404496), 1582538896607691403], [138702721769271731659218, (-966259522225186539778)], [62444995624558446610136]], [[(-15399819548992648011412), 281404831072501828399, 30903036690371541, (-2029756672921038)], [(-13867363088473555651103), 116886445135716316893, (-2287163463619524)], [(-8322511203704174498406), 38711080730546135941], [(-3330120794850198693392)]], [[1283156016082086632378, (-24581542237197682927), (-2431983423772314), 21044328485554, 2458585602701], [1232525119275608747310, (-11290346697314767901), 268246930336877, (-80134249487935)], [832134834200027037252, (-4680864486115325467), 14758735415781], [443876633917914571021, (-1549798344562499085)], [166497688271417443085]]], r := 25606305553951434702450, ok := true }, eta := { p := [[[(-1039496816262078679941691)]], [[63428562365775511046279, 0], [78532222625547470535331]], [[(-3688576323381383247717), 0, 0], [(-4665748034332135638789), 0], [(-4568822022657393124883)]], [[224230295421628043463, 0, 0, 0], [266951852075458998661, 0, 0], [267106743944575460466, 0], [238677540675160724053]], [[(-14128811397821295221), 0, 0, 0, 0], [(-16106378237490263685), 0, 0, 0], [(-15135488391603283155), 0, 0], [(-13795034559370846390), 0], [(-11751679329857822189)]]], r := 11471443477020633549, 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 := 121597189939003392, bh := 4503599627370496, tc := 16140901064495857664, th := 2305843009213693952, sc := 4323455642275676160, sh := 288230376151711744 }
noncomputable def q4 : Cert := { V0 := [[[2182564808595785558]], [[(-71479566593313473), 305531960923285685], [12619752698905205]], [[1002059766359872, (-9598242129212901), (-1310368458741310)], [(-401134443989810), 1694574376815134], [(-160808551584992)]], [[(-19098687827386), 114657366411004, 126220131544650, (-55041271641373)], [5799524888910, (-46837876746476), (-22284226410878)], [5225983886449, (-22213540942060)], [3495640320742]], [[480723239637, (-1797286182867), (-5698456842350), 4824691305356, 741619012918], [(-135823589688), 346029780103, 2095664932466, (-851801627011)], [(-76472584001), 671217744657, 161491960240], [(-113805398077), 484047859301], [(-89711402442)]]], r0 := 21166004884300, V1 := [[[2486732115843317124]], [[(-80946882233144896), 0], [14291211939514623]], [[1110848260777747, 0, 0], [(-445813367314282), 0], [(-182853267935430)]], [[(-20714709482958), 0, 0, 0], [6052114562314, 0, 0], [5880577713293, 0], [3976306739492]], [[517144682433, 0, 0, 0, 0], [(-136534123881), 0, 0, 0], [(-83071347974), 0, 0], [(-128220570186), 0], [(-102076415711)]]], r1 := 6563481660791, V2 := [[[18302141064548362108]], [[(-2217091660320483), 107676875736639], [(-5323318154658877)]], [[8372848385802, (-506226118091), (-75096470600)], [(-84073910613346), 8060581112399], [744999402169]], [[(-214776173026), (-40475791371), 1867343479, 51033018], [359945521776, (-35679151396), (-8455123488)], [(-47667296286), 152965108553], [(-7149347220)]], [[7509281354, 280666599, 21636409, (-2301255), (-34185)], [(-9159223455), (-3110447643), 208550257, 7663638], [1218505265, (-582498340), (-320091846)], [387578777, 63371669], [111857597]]], r2 := 515334776955, V3 := [[[18389662278786375361]], [[(-3803866973204928), 83226434547039], [(-2117285500466087)]], [[110643905302, 3957994538853, (-114448927802)], [(-141034656622256), 6236029674849], [(-118136429974)]], [[169320377, (-110906740257), (-3208208187), 153853192], [8258815398, 297531374527, (-12877577920)], [(-5686533517), 118622197798], [(-48892078)]], [[(-3630625), (-166653195), 263278029, 1278058, (-204282)], [14333070, (-8288365098), (-363303866), 23077462], [155670623, 5700405106, (-487070246)], [(-3095259), 55174608], [260949]]], r3 := 5759017563855, Vm := [[[18302300885010818374]], [[(-2219727020706184), 0], [(-5311002642033007)]], [[8360206745485, 0, 0], [(-84281060168230), 0], [994252341276]], [[(-215025901836), 0, 0, 0], [358969646991, 0, 0], [(-52020934010), 0], [(-6774437954)]], [[7527330680, 0, 0, 0, 0], [(-9175598598), 0, 0, 0], [1197823531, 0, 0], [378835748, 0], [110121876]]], rm := 121483784938 }
noncomputable def w4 : Wit := { Z0 := { p := [[[2204882156184870095]], [[(-73690687096864536), 314983165169267156], [13010127113191364]], [[1106996268767070, (-10527241013837791), 0], [(-439650976128839), 1858589587598766], [(-163478249391721)]], [[(-22637536767536), 158142324109581, 0, 0], [7638236139224, (-62807282304120), 0], [5491992289925, (-23354035627389)], [3549852625246]], [[588162038593, (-3233933823934), 0, 0, 0], [(-199576941023), 1091176591317, 0, 0], [(-89100642107), 784570327132, 0], [(-119193876868), 507121803606], [(-91017882502)]]], r := 4031006567241, ok := true }, Z1 := { p := [[[2519865321354137252]], [[(-84217928110702327), 0], [14868716700790130]], [[1265138592876652, 0, 0], [(-502458258432959), 0], [(-186832285019109)]], [[(-25871470591470), 0, 0, 0], [8729412730542, 0, 0], [6276562617058, 0], [4056974428853]], [[672185186964, 0, 0, 0, 0], [(-228087932598), 0, 0, 0], [(-101829305265), 0, 0], [(-136221573563), 0], [(-104020437145)]]], r := 1691513680904, ok := true }, Z2 := { p := [[[494917595875352714020]], [[(-6485575884892655608), 314983165169267156], [(-15572104874760245249)]], [[117626476218569838, (-10527241013837791), 0], [201296521511583569, 1858589587598766], [539092885474776117]], [[(-2703373005944686), 158142324109581, 0, 0], [(-3452835291916346), (-62807282304120), 0], [(-6965240846604892), (-23354035627389)], [(-19157566314381935)]], [[77312564138110, (-3233933823934), 0, 0, 0], [74441896838269, 1091176591317, 0, 0], [117545218755097, 784570327132, 0], [247371244433091, 507121803606], [688848181371108]]], r := 228630345716895, ok := true }, Z3 := { p := [[[1102807811567372674189]], [[(-63873071718470301703), 1397506290346608756], [(-35552644078350611051)]], [[4016365374629096371, (-109209134471486239), 0], [2100862174427428201, 6932493382948276], [1241787444620871867]], [[(-258209305755104581), 6721739863984339, 0, 0], [(-133085800936129195), (-479486210740040), 0], [(-73928380553238608), (-93890764984774)], [(-44350345243266973)]], [[16769807168957394, (-429862815687828), 0, 0, 0], [8592099573232727, 26972910231136, 0, 0], [4695045549912987, 6809427735171, 0], [2651522911297218, 2065310001214], [1600196128254463]]], r := 14488167748709846, ok := true }, iE := { p := [[[499295219048419467767]], [[(-6497546207365551764), 0], [(-15546274272532597088)]], [[118076147915485437, 0, 0], [201216296411414874, 0], [538768312040852615]], [[(-2716549352238893), 0, 0, 0], [(-3448279880030837), 0, 0], [(-6964297158656690), 0], [(-19150518356254258)]], [[77749418851959, 0, 0, 0, 0], [74294502200767, 0, 0, 0], [117499656727087, 0, 0], [247350876051528, 0], [688667472397396]]], r := 227365892355705, ok := true }, iHu := { p := [[[1107627782242241590106]], [[(-63951721290274097561), 0], [(-35528734050152279238)]], [[4022342120014997469, 0, 0], [2100686752228732345, 0], [1241463617288577445]], [[(-258609670886072976), 0, 0, 0], [(-133064849994186624), 0, 0], [(-73924916663441543), 0], [(-44343222031221967)]], [[16796285193957548, 0, 0, 0, 0], [8590670332566297, 0, 0, 0], [4694728055026857, 0, 0], [2651441460668966, 0], [1600011925959998]]], r := 14420983538216044, ok := true }, T := { p := [[[16140901064495857664]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[681525386062107210]], [[8868986760719927, 0], [21220272438434282]], [[(-45754976476795), 0, 0], [277642128385781, 0], [(-74681480962253)]], [[1015203951909, 0, 0, 0], [(-1697250930285), 0, 0], [(-942917183491), 0], [916762768303]], [[(-33840212878), 0, 0, 0, 0], [37599966039, 0, 0, 0], [(-97267751), 0, 0], [11604927790, 0], [(-16977705646)]]], r := 59521297902, ok := true }, de := { p := [[[(-86109320940820893171)]], [[888473522483925355, 0], [493596401379958530]], [[(-29569958307679807), 0, 0], [50917527908562, 0], [(-9126530341876483)]], [[1314223520705355, 0, 0, 0], [5252458570, 0, 0], [2918032539, 0], [225346968570877]], [[(-65711175791447), 0, 0, 0, 0], [541824, 0, 0, 0], [97719271, 0, 0], [167230, 0], [(-6259637992632)]]], r := 19737642918754, ok := true }, dde := { p := [[[(-8626222336223189926891)]], [[574191640785808538859, 0], [318995355992115854894]], [[(-38279534512420518849), 0, 0], [(-21266459058770631325), 0], [(-11814671145808801406)]], [[2551968958025647556, 0, 0, 0], [1417760521715298654, 0, 0], [787644734286277191, 0], [437580411184096407]], [[(-170131263869352343), 0, 0, 0, 0], [(-94517368817934807), 0, 0, 0], [(-52509649538736741), 0, 0], [(-29172027412942632), 0], [(-16206681895799338)]]], r := 26688614258125221, ok := true }, nJu := { p := [[[(-172218641881641786341)]], [[1776947044967850711, 0], [987192802759917061]], [[(-59139916615359613), 0, 0], [101835055817124, 0], [(-18253060683752966)]], [[2628447041410711, 0, 0, 0], [10504917140, 0, 0], [5836065078, 0], [450693937141754]], [[(-131422351582894), 0, 0, 0, 0], [1083649, 0, 0, 0], [195438543, 0, 0], [334460, 0], [(-12519275985263)]]], r := 39475285837500, ok := true }, Jd1 := { p := [[[(-17252444672446379853781)]], [[1148383281571617077719, 0], [637990711984231709789]], [[(-76559069024841037698), 0, 0], [(-42532918117541262649), 0], [(-23629342291617602812)]], [[5103937916051295113, 0, 0, 0], [2835521043430597309, 0, 0], [1575289468572554383, 0], [875160822368192814]], [[(-340262527738704686), 0, 0, 0, 0], [(-189034737635869614), 0, 0, 0], [(-105019299077473482), 0, 0], [(-58344054825885263), 0], [(-32413363791598676)]]], r := 53377228516250434, ok := true }, term0 := { p := [[[5637514881938750744900068]], [[(-749937183761800896056683), 0], [(-415270721904323025681815)]], [[74936300037275964049811, 0, 0], [55305630997736600881610, 0], [23027669138715012128599]], [[(-6658452478686343235473), 0, 0, 0], [(-5528436423199723877636), 0, 0], [(-3067992950911336409490), 0], [(-1136108929359330976868)]], [[554743441442638824428, 0, 0, 0, 0], [491322053590696168235, 0, 0, 0], [306720530621640371603, 0, 0], [151393674499006907868, 0], [52568193479708704314]]], r := 150620873818364350263, ok := true }, r0 := { p := [[[6076378625859182873034]], [[(-303634580707324641968), 1682191548140544595831], [(-188588597692186617110)]], [[13715724918167699017, (-80724881020004598896), 105293035369290569801], [9085384140632813191, (-52811706073203990604)], [6524861893685364135]], [[(-667902372002083849), 3544970608110382726, (-4138813488170131604), (-1974106532843236935)], [(-386699177822234029), 2477106933933764824, (-3470947276985621886)], [(-310880349597444221), 1831203013980110761], [(-231691124052869573)]], [[35970898419293459, (-171940254692243128), 154990970163617177, 206615077976937360, (-45339144824978372)], [17873896341484175, (-103338086997784860), 143830672217729227, 41712413572940050], [12990683733471819, (-85167943484977780), 121507331262942393], [10965834836417337, (-65106479014368237)], [8325737404849584]]], r := 337837064738466547, ok := true }, r1 := { p := [[[7861845650277124615119]], [[(-388288842804420919624), 0], [(-244828312346915585440)]], [[17403922459167922522, 0, 0], [11701714695401277524, 0], [8476248753614583993]], [[(-846743092271302088), 0, 0, 0], [(-495183320157649614), 0, 0], [(-400971722427249560), 0], [(-301097247307792349)]], [[45733697209662157, 0, 0, 0, 0], [22873709338130026, 0, 0, 0], [16664281869174816, 0, 0], [14155298135618671, 0], [10822594748123270]]], r := 57396101536978462, ok := true }, r2 := { p := [[[880622275695051291105347]], [[(-53657130968313503448819), 1511471671573126550603], [(-62129418961564835395902)]], [[3113415869563054135525, (-66498543212336071673), 460237543034918754], [3693431888839099012422, (-53125753809742297486)], [3355681372988224710164]], [[(-188886981040803561121), 3286950807018770561, 1024193517271497, (-302565394322040)], [(-211231077329072200971), 2178151068577612687, 107728282524290], [(-196433964452338819555), 1935853689880012799], [(-162523020761414682901)]], [[11883831792575268607, (-182782311180294040), (-31175140537304), 5668841933758, 196069736878], [12734742934685022659, (-102596648182269610), 16442617562934, (-11473195539514)], [11133017873893107809, (-77215563975764294), (-2693983008803)], [9408719549621894159, (-70998647167927652)], [7414744271755557738]]], r := 69201669062769155758, ok := true }, r3 := { p := [[[11161981647588407460488698]], [[(-1486231047589342793656806), 22270869537626591903922], [(-826353137967271365479719)]], [[148555588930430000931566, (-2695412575845715225320), 1578020981436026250], [110105588637097773857190, (-828209008093229057579)], [45900166565363925058968]], [[(-13201938202356228887621), 260498427010448995532, 31426264211064946, (-2189842498204403)], [(-11008064531056520068889), 100193257997876191159, (-2232014708579613)], [(-6117252890457954661413), 30723820797139232515], [(-2266469738211690265121)]], [[1100011225765456896690, (-22755803848668950808), (-2466325338155378), 22208690321326, 2870642189641], [978383691835079260563, (-9678103669758291069), 255262517469237, (-79955223226557)], [611632969313540779775, (-3715246117648776963), 12874605934778], [302093440501532650246, (-1138939192980360260)], [104923468172263352582]]], r := 18812193377267525032282, ok := true }, eta := { p := [[[(-898969943607273171867455)]], [[55064976131361372612775, 0], [62785123937969161540096]], [[(-3209555110827216754000), 0, 0], [(-3743600465205287861392), 0], [(-3379694212836684455542)]], [[195315427025603750607, 0, 0, 0], [214647206429460413389, 0, 0], [198268681699405665625, 0], [163406558266559020525]], [[(-12312050030119897358), 0, 0, 0, 0], [(-12962940827636419086), 0, 0, 0], [(-11257859414294729744), 0, 0], [(-9476173626077585844), 0], [(-7447319873274535383)]]], r := 8175061966811252989, 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 108086391056891904 126100789566373888 13835058055282163712 18446744073709551616 3458764513820540928 4611686018427387904 :=
  (RegionPosI.split_s 4035225266123964416 (RegionPosI.split_b 117093590311632896 (RegionPosI.split_s 3746994889972252672 (RegionPosI.of_check c0 q0 ok_0 108086391056891904 117093590311632896 13835058055282163712 18446744073709551616 3458764513820540928 3746994889972252672 (by decide +kernel)) (RegionPosI.of_check c1 q1 ok_1 108086391056891904 117093590311632896 13835058055282163712 18446744073709551616 3746994889972252672 4035225266123964416 (by decide +kernel))) (RegionPosI.of_check c2 q2 ok_2 117093590311632896 126100789566373888 13835058055282163712 18446744073709551616 3458764513820540928 4035225266123964416 (by decide +kernel))) (RegionPosI.split_b 117093590311632896 (RegionPosI.of_check c3 q3 ok_3 108086391056891904 117093590311632896 13835058055282163712 18446744073709551616 4035225266123964416 4611686018427387904 (by decide +kernel)) (RegionPosI.of_check c4 q4 ok_4 117093590311632896 126100789566373888 13835058055282163712 18446744073709551616 4035225266123964416 4611686018427387904 (by decide +kernel))))

end CKLaneC.RSC2.S07_0027

end