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

import Definitions.Def_CK_CKLaneC_RSC2_BA_0135_part00

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

namespace CKLaneC.RSC2.BA_0135
open CKLaneC.TM3 CKLaneC.RSCell

noncomputable def w5 : Wit := { Z0 := { p := [[[3698284533373109319]], [[(-55379782249959919), 284483425644085332], [122675924722975680]], [[356970870123555, (-4259983249996917), 0], [(-1833599675104590), 9436609594075052], [(-1037485070139432)]], [[(-3477190623739), 27459297701811, 0, 0], [14682243339163, (-141046128854200), 0], [14823934209004, (-79806543856880)], [109355694720728]], [[38733174054, (-267476201827), 0, 0, 0], [(-190117753199), 1129403333781, 0, 0], [4183037290, 1140302631461, 0], [(-1654237533467), 8411976516979], [(-5866231904101)]]], r := 78112791926792, ok := true }, Z1 := { p := [[[4551734810305365315]], [[(-68159731999950670), 0], [150985753505200837]], [[439348763228991, 0, 0], [(-2256738061667187), 0], [(-1276904701710070)]], [[(-4279619229217), 0, 0, 0], [18070453340508, 0, 0], [18244842103389, 0], [134591624271666]], [[47671598836, 0, 0, 0, 0], [(-233991080861), 0, 0, 0], [5148353588, 0, 0], [(-2035984656575), 0], [(-7219977728124)]]], r := 60240045721908, ok := true }, Z2 := { p := [[[28870074519436263684]], [[(-183087886265263441), 284483425644085332], [(-2529350965453231174)]], [[1522200084444513, (-4259983249996917), 0], [11644531928008480, 9436609594075052], [193233708290382652]], [[(-15607216894466), 27459297701811, 0, 0], [(-88515629750295), (-141046128854200), 0], [(-978858934043175), (-79806543856880)], [(-16471088731164711)]], [[182265140098, (-267476201827), 0, 0, 0], [772653060941, 1129403333781, 0, 0], [6948682020237, 1140302631461, 0], [83315398038999, 8411976516979], [1426075874365859]]], r := 305079709773081, ok := true }, Z3 := { p := [[[52232383108711512850]], [[(-967448466592582197), 912495913731873429], [(-4343318117767650575)]], [[19186764528623321, (-23884024607540335), 0], [75895153192878319, 21820882062725925], [349339544769282505]], [[(-399926006452463), 448824797624666, 0, 0], [(-1570057892470195), (-430983127830043), 0], [(-6421294034318429), (-442430705275194)], [(-29925744300455758)]], [[8480929239069, (-9296175122624), 0, 0, 0], [33080996154907, 6528930130092, 0, 0], [132050429528102, 12728576983490, 0], [555909596691807, 24863007343780], [2610090075221421]]], r := 912899533522202, ok := true }, iE := { p := [[[38357013312096235223]], [[(-194602825166176795), 0], [(-2214659389216304005)]], [[1775587374203365, 0, 0], [11271304101592449, 0], [190572323729542985]], [[(-18483849555393), 0, 0, 0], [(-72702122126632), 0, 0], [(-977454651546537), 0], [(-16190566566609099)]], [[218715376828, 0, 0, 0, 0], [586896023671, 0, 0, 0], [7120087872746, 0, 0], [82932080322495, 0], [1411027658763315]]], r := 308016550462136, ok := true }, iHu := { p := [[[61516093303157574493]], [[(-1001076033058373867), 0], [(-4121313019214344234)]], [[20345969004956436, 0, 0], [76517040490049051, 0], [344838266037960775]], [[(-425258255022267), 0, 0, 0], [(-1552948499438488), 0, 0], [(-6393307458727267), 0], [(-29672788696744570)]], [[9032080050354, 0, 0, 0, 0], [32756547381762, 0, 0, 0], [131693747168751, 0, 0], [555181765870502, 0], [2594549293547347]]], r := 835398557052914, ok := true }, T := { p := [[[14987979559889010688]], [[0, 1152921504606846976], [0]]], r := 0, ok := true }, E := { p := [[[8871451073424095419]], [[45008964284176987, 0], [512220340407364146]], [[(-182317764222924), 0, 0], [2590562174959798, 0], [(-14502157797286485)]], [[1266565409543, 0, 0, 0], [(-17505779151248), 0, 0], [(-72069246635657), 0], [362422865694779]], [[(-14030954613), 0, 0, 0, 0], [114371729234, 0, 0, 0], [(-89434672451), 0, 0], [1938455169330, 0], [(-17164324072220)]]], r := 27781024074239, ok := true }, de := { p := [[[(-38307889393867830551)]], [[310347454444509620, 0], [1277664195570253889]], [[(-3233985610900258), 0, 0], [1585523425984457, 0], [(-54811937941264314)]], [[47767929429797, 0, 0, 0], [1967562793934, 0, 0], [8100226047754, 0], [3333051527423543]], [[(-790960970415), 0, 0, 0, 0], [2441656354, 0, 0, 0], [104512693186, 0, 0], [41382965997, 0], [(-227210921024914)]]], r := 90958344656536, ok := true }, dde := { p := [[[(-264141958110069901589)]], [[5504999506388555096, 0], [22663439526300934571]], [[(-121968273627707046), 0, 0], [(-503803752405797228), 0], [(-2067206923355482215)]], [[2692800943227491, 0, 0, 0], [11081790470408165, 0, 0], [45622436092459531, 0], [187892680382192324]], [[(-59463107809719), 0, 0, 0, 0], [(-244810401233486), 0, 0, 0], [(-1008065962858505), 0, 0], [(-4149224558872334), 0], [(-17081332705157674)]]], r := 2599137483947510, ok := true }, nJu := { p := [[[(-76615778787735661102)]], [[620694908889019240, 0], [2555328391140507778]], [[(-6467971221800516), 0, 0], [3171046851968915, 0], [(-109623875882528628)]], [[95535858859594, 0, 0, 0], [3935125587868, 0, 0], [16200452095509, 0], [6666103054847086]], [[(-1581921940829), 0, 0, 0, 0], [4883312709, 0, 0, 0], [209025386372, 0, 0], [82765931994, 0], [(-454421842049827)]]], r := 181916689313067, ok := true }, Jd1 := { p := [[[(-528283916220139803177)]], [[11009999012777110193, 0], [45326879052601869143]], [[(-243936547255414091), 0, 0], [(-1007607504811594456), 0], [(-4134413846710964430)]], [[5385601886454983, 0, 0, 0], [22163580940816330, 0, 0], [91244872184919063, 0], [375785360764384648]], [[(-118926215619438), 0, 0, 0, 0], [(-489620802466971), 0, 0, 0], [(-2016131925717009), 0, 0], [(-8298449117744667), 0], [(-34162665410315348)]]], r := 5198274967895010, ok := true }, term0 := { p := [[[6327659050664450003307]], [[(-259707419042911496755), 0], [(-995975744702091739208)]], [[8423530521432508640, 0, 0], [42503576531146573596, 0], [129412785265094607383]], [[(-245312695134942733), 0, 0, 0], [(-1390787808775063845), 0, 0], [(-5578337427792170379), 0], [(-15296080449189455133)]], [[6726660537170608, 0, 0, 0, 0], [40704910048196489, 0, 0, 0], [183264917154681374, 0, 0], [663090044929346105, 0], [1711585804309401932]]], r := 369817857656969481, ok := true }, r0 := { p := [[[335197825901817991148]], [[(-7016276799306179754), 47424445114543782973], [(-20057160562692682745)]], [[136968629628148771, (-886637445850456201), 1245425248228714355], [373367462519855625, (-3077390001997881150)], [1706099966583397411]], [[(-2616900404278858), 16171234104700191, (-8765759576196977), (-36265572597325294)], [(-6016684799594685), 56709043568183912, (-113676185405299183)], [(-32501495256370013), 255805319439276480], [(-145299942713847061)]], [[51080140865033, (-301836103500829), 28020244304450, 1367709318388978, (-22108900040704)], [98920461818944, (-911162963576573), 1834727838392540, 785286250878567], [539540099458448, (-4691743247025143), 8905360735317618], [2734225501873362, (-21911816237219177)], [12658905009288273]]], r := 105801297934582868, ok := true }, r1 := { p := [[[487703719008304902268]], [[(-9719847684840853072), 0], [(-30287735321118012934)]], [[185131467403017135, 0, 0], [558394751613097296, 0], [2551930219982471955]], [[(-3517224670197749), 0, 0, 0], [(-8924627536567790), 0, 0], [(-47750075302431809), 0], [(-217843479593346396)]], [[68869000915538, 0, 0, 0, 0], [147334613234262, 0, 0, 0], [781214782094418, 0, 0], [4034100784901224, 0], [18984312852013887]]], r := 89386233797987876, ok := true }, r2 := { p := [[[1488081908803138616963]], [[(-36251667545016251733), 35512788832694103548], [(-249963735454934433595)]], [[774384165640427181, (-648560723428490470), 106885034715334488], [6014467955444332590, (-2099016042489415676)], [32193048218559599693]], [[(-16223473566646878), 12841456053901193, 1322754143068490, (-1332557637774349)], [(-126966133928327676), 39422440122465417, (-2443862555525708)], [(-764824166968453002), 209185795619121248], [(-3756945629371355428)]], [[341262590510234, (-257222492124987), (-6387092136154), (-2724675999712), 15799566734832], [2644704272024178, (-688819576671967), 178586776024300, (-179322151889811)], [15976581922366331, (-3619524081924154), (-74738990063726)], [88279923978400140, (-18595054830234850)], [414957726943181217]]], r := 8049270208623799757, ok := true }, r3 := { p := [[[9701362870939096608374]], [[(-407880138302368596256), 261306325770543802663], [(-1730469816689821348392)]], [[13298329658353915412, (-9759045028809484076), 172641870731530220], [74747235729350842688, (-22924846839642368181)], [234995486770422390686]], [[(-388471009273296219), 313803268934531725, 5487129945472876, (-3735087991062797)], [(-2457770365772535801), 919721140453320303, (-32222557352378256)], [(-10226489847552920071), 2117580387687648449], [(-28423810796841489194)]], [[10672120912894861, (-9066066877215870), (-29565814742523), (-68096046249573), 74672002691546], [72094567790362087, (-28958421210944892), 152982066219047, 168559259221276], [337068657099624150, (-83015530519245767), (-1009128415822926)], [1241545916767383923, (-192832698742983330)], [3225909439116633317]]], r := 311456956800142184893, ok := true }, eta := { p := [[[(-2184099967170348870344)]], [[53708997687982273352, 0], [301222834342044996242]], [[(-1186001647955138051), 0, 0], [(-7367804236977345545), 0], [(-36833701666729517957)]], [[25480358306818037, 0, 0, 0], [157707836471243168, 0, 0], [885546543788194646, 0], [4171150479167783754]], [[(-546643269457689), 0, 0, 0, 0], [(-3326886560588367), 0, 0, 0], [(-18732953936364158), 0, 0], [(-99011851751755238), 0], [(-452259470249356405)]]], r := 1036634347121974485, ok := true } }
theorem sB_5 : stageB c5 w5 = true := by decide +kernel
theorem s0_5 : stageC0 w5 q5 = true := by decide +kernel
theorem s1_5 : stageC1 w5 q5 = true := by decide +kernel
theorem s2_5 : stageC2 w5 q5 = true := by decide +kernel
theorem s3_5 : stageC3 w5 q5 = true := by decide +kernel
theorem sE_5 : stageE w5 q5 = true := by decide +kernel
theorem sF_5 : stageF w5 = true := by decide +kernel
theorem ok_5 : (domOK c5 && cellCheck c5 q5) = true :=
  staged_check c5 q5 w5 (by decide +kernel) sB_5 s0_5 s1_5 s2_5 s3_5 sE_5 sF_5

noncomputable def c6 : Cell := { bc := 3170534137668829184, bh := 288230376151711744, tc := 14987979559889010688, th := 1152921504606846976, sc := 6088866696204910592, sh := 252201579132747776 }
noncomputable def q6 : Cert := { V0 := [[[3445761164523268056]], [[(-98792459066746261), 251894475221618695], [108654165745027822]], [[993907157160318, (-6477289799972932), (-1430566575896190)], [(-2758650751597901), 7123868827167721], [(-1185973408356496)]], [[(-15640658029279), 33713574869756, 116979142898098, (-26059504251488)], [22938115561469, (-111687599992664), (-128656289166505)], [44939340055224, (-115802006707814)], [99209001556185]], [[298876125720, (-119199098901), (-4106140880587), 1536865511832, 523783439925], [(-479280092611), (-1850758499475), 9709834332796, (-1690279213900)], [(-604585676400), 5115368125469, (-2138968290288)], [(-2749870449207), 6971347904649], [(-5617507292327)]]], r0 := 371771619113992, V1 := [[[4187908679474858659]], [[(-117135418341140301), 0], [128828164409316220]], [[1058047836230927, 0, 0], [(-3006017395238600), 0], [(-1551811675886636)]], [[(-15236245355299), 0, 0, 0], [14885782562582, 0, 0], [61002441136586, 0], [119630070539824]], [[282380542329, 0, 0, 0, 0], [(-292011728050), 0, 0, 0], [(-860558264040), 0, 0], [(-3227144435284), 0], [(-6897832603966)]]], r1 := 274411157486388, V2 := [[[14320772022700113528]], [[(-53475315836659570), 41702499943978739], [(-382637465950313119)]], [[263609617123029, (-338506675152777), (-358580351905346)], [(-5023240247681246), 7963956759614607], [(-996831870650114)]], [[(-3726102682915), (-13299725412547), 10985312025664, 2768648399038], [34340683205575, (-72573560075095), (-100006269642879)], [(-2058576381769), 403878654693046], [(-20866042173252)]], [[79326259920, 97154997625, 30558607120, (-151909512921), (-19237442420)], [(-475694083913), (-2527252545935), 3283660437858, 981641900478], [881349046894, (-5357809175787), (-9154054761145)], [946701380442, 1468399627895], [219004521310]]], r2 := 2095819968262820, V3 := [[[16228857643330179974]], [[(-89458324745538845), 43814587295449158], [(-214180650226243593)]], [[108302898440845, 923563206781466, (-770434496803796)], [(-8397174411551435), 8600018654865771], [(-1230144040329936)]], [[133829781622, (-39118336455395), 55851796288, 12751329234025], [21395640139689, 171671436836550, (-224548248373288)], [(-23710176680326), 472412740540489], [(-6899119259089)]], [[(-4299003865), (-4528992391), 1057225437677, (-292046223223), (-201836130198)], [17397081068, (-8017047830697), 432603239497, 4878793562918], [1219452974406, 7650104974621, (-22769208912517)], [156366840529, 4514330967404], [96743649489]]], r3 := 8118686086651784, Vm := [[[14530954591246720955]], [[(-57184330902690951), 0], [(-338202936327551033)]], [[227419472698620, 0, 0], [(-5831081086375387), 0], [1908076238909036]], [[(-3111663247057), 0, 0, 0], [25336079527562, 0, 0], [(-56625516937503), 0], [41502799264223]], [[74970896363, 0, 0, 0, 0], [(-301951710986), 0, 0, 0], [64566340561, 0, 0], [(-100083632127), 0], [1149981633302]]], rm := 548000922004296 }
noncomputable def w6 : Wit := { Z0 := { p := [[[3535267064699649473]], [[(-106655689686685326), 271943620361511497], [117302323419623259]], [[1310578533743860, (-8204283822052718), 0], [(-3500775247842237), 9023255647663327], [(-993010772991715)]], [[(-24421102556087), 100813733364912, 0, 0], [52380043417120, (-269290403680173), 0], [29629004265074, (-76385444076286)], [104498106877764]], [[516512617241, (-1878546350469), 0, 0, 0], [(-1307940719599), 4029234109009, 0, 0], [(-27690198537), 2279154174236, 0], [(-3170576979745), 8038315913674], [(-5608966622724)]]], r := 90510142433423, ok := true }, Z1 := { p := [[[4351097925784183967]], [[(-131268541152843478), 0], [144372090362613241]], [[1613019733838597, 0, 0], [(-4308646458882754), 0], [(-1222167105220572)]], [[(-30056741607491), 0, 0, 0], [64467745744148, 0, 0], [36466466787784, 0], [128613054618787]], [[635707836605, 0, 0, 0, 0], [(-1609773193353), 0, 0, 0], [(-34080244353), 0, 0], [(-3902248590455), 0], [(-6903343535660)]]], r := 70451574233381, ok := true }, Z2 := { p := [[[28334103480300787038]], [[(-348714609630883191), 271943620361511497], [(-2495193763353914885)]], [[5563915273940509, (-8204283822052718), 0], [22266974144472205, 9023255647663327], [190358077433036500]], [[(-108925009932799), 100813733364912, 0, 0], [(-327850023176352), (-269290403680173), 0], [(-1877486813761429), (-76385444076286)], [(-16226333860363000)]], [[2415123921338, (-1878546350469), 0, 0, 0], [5488248768901, 4029234109009, 0, 0], [25733615760422, 2279154174236, 0], [159794879120951, 8038315913674], [1404761056553298]]], r := 353357469713205, ok := true }, Z3 := { p := [[[49492566096264707072]], [[(-1724556361251409679), 844647219259939749], [(-4128923762604344240)]], [[64002915423782386, (-42844870766527886), 0], [134594770783936188, 20583355802669423], [331193229912823414]], [[(-2500817245990596), 1498935340771007, 0, 0], [(-5226997370519307), (-790165872033702), 0], [(-11396907085242240), (-406145832979055)], [(-28355199513528758)]], [[99433474894788, (-58183985420014), 0, 0, 0], [206482588961107, 21916503178577, 0, 0], [439269087026119, 22991156092758, 0], [986105730397249, 23063798793399], [2472039216664053]]], r := 1567482479282974, ok := true }, iE := { p := [[[37788703109487447718]], [[(-368851687534015795), 0], [(-2181484365107893946)]], [[6481275032680608, 0, 0], [21700775858097446, 0], [187702402737381378]], [[(-128767858859752), 0, 0, 0], [(-270766052300500), 0, 0], [(-1872710967559555), 0], [(-15946867629253480)]], [[2893121987195, 0, 0, 0, 0], [4224295465346, 0, 0, 0], [26361701827914, 0, 0], [159151601317272, 0], [1389760624399010]]], r := 358414831573741, ok := true }, iHu := { p := [[[58685184374682651928]], [[(-1779158920055690919), 0], [(-3904907240122230660)]], [[67835056752395110, 0, 0], [136027749895061278, 0], [326772989695590730]], [[(-2658172092236832), 0, 0, 0], [(-5168863067929101), 0, 0], [(-11344647512727528), 0], [(-28104187382637325)]], [[105866440709470, 0, 0, 0, 0], [204468830943281, 0, 0, 0], [438205557225660, 0, 0], [984961086282962, 0], [2456644021484418]]], r := 1498816670177036, ok := true }, T := { p := [[[14987979559889010688]], [[0, 1152921504606846976], [0]]], r := 0, ok := true }, E := { p := [[[9004870210417600390]], [[87895622231698517, 0], [519837463512207583]], [[(-686517126696029), 0, 0], [4976968399982226, 0], [(-14719173457021315)]], [[8908460096527, 0, 0, 0], [(-66164292270199), 0, 0], [(-145217732385242), 0], [368234007022419]], [[(-185204822899), 0, 0, 0, 0], [803625996721, 0, 0, 0], [(-361764062042), 0, 0], [3871202916565, 0], [(-17431502525657)]]], r := 29218191356983, ok := true }, de := { p := [[[(-37404724016731129465)]], [[584306317079883727, 0], [1282438540084420129]], [[(-11373211186090487), 0, 0], [3194790112475343, 0], [(-54786689945341610)]], [[315261903207823, 0, 0, 0], [7958809364930, 0, 0], [17468036138612, 0], [3333185096719514]], [[(-9791380620385), 0, 0, 0, 0], [19826856939, 0, 0, 0], [427038194949, 0, 0], [95509337327, 0], [(-227210214133447)]]], r := 92585196006083, ok := true }, dde := { p := [[[(-248656485689267921702)]], [[9679932055735404982, 0], [21245565161289395341]], [[(-402487092635608493), 0, 0], [(-886767700268673297), 0], [(-1938848684898906187)]], [[16667218710065778, 0, 0, 0], [36564423235127507, 0, 0], [80251786061513605, 0], [176218326549699093]], [[(-690367748276984), 0, 0, 0, 0], [(-1515285778232108), 0, 0, 0], [(-3326616408557069), 0, 0], [(-7299388954644516), 0], [(-16020070100255199)]]], r := 3485956470799737, ok := true }, nJu := { p := [[[(-74809448033462258930)]], [[1168612634159767455, 0], [2564877080168840259]], [[(-22746422372180973), 0, 0], [6389580224950686, 0], [(-109573379890683220)]], [[630523806415647, 0, 0, 0], [15917618729860, 0, 0], [34936072277224, 0], [6666370193439029]], [[(-19582761240769), 0, 0, 0, 0], [39653713878, 0, 0, 0], [854076389899, 0, 0], [191018674655, 0], [(-454420428266893)]]], r := 185170392012156, ok := true }, Jd1 := { p := [[[(-497312971378535843404)]], [[19359864111470809965, 0], [42491130322578790683]], [[(-804974185271216986), 0, 0], [(-1773535400537346594), 0], [(-3877697369797812373)]], [[33334437420131556, 0, 0, 0], [73128846470255015, 0, 0], [160503572123027210, 0], [352436653099398186]], [[(-1380735496553967), 0, 0, 0, 0], [(-3030571556464216), 0, 0, 0], [(-6653232817114137), 0, 0], [(-14598777909289032), 0], [(-32040140200510397)]]], r := 6971912941599466, ok := true }, term0 := { p := [[[5618229951348636070159]], [[(-430257929841321981292), 0], [(-879967077021388148851)]], [[26144187438399568433, 0, 0], [70295883927674512347, 0], [114193174418111355967]], [[(-1427148052167665216), 0, 0, 0], [(-4310968706139621272), 0, 0], [(-9218606839496242627), 0], [(-13487273087726966243)]], [[73373154422921080, 0, 0, 0, 0], [236574936959777283, 0, 0, 0], [567787228183540581, 0, 0], [1095393401732242081, 0], [1508496534383886685]]], r := 540530174880132669, ok := true }, r0 := { p := [[[315314960298981719053]], [[(-12519980606813312670), 44902375558350088765], [(-18988668856845284495)]], [[463688729904073236, (-1594333114317265243), 1219373297399882367], [679530642648444021, (-2915071671746511492)], [1613218337885659442]], [[(-16686220085414540), 54976950462903797, (-17208127915345610), (-32380303411964136)], [(-20843955950855588), 103254238531183819, (-108383590196161878)], [(-58986661666016339), 242376664529093267], [(-137478763879178369)]], [[611250188497799, (-1923997136120953), 104596233459814, 2450949473922114, (-68782652274946)], [647363074189455, (-3148409442079710), 3393572574065312, 639730987682057], [1862920548152944, (-8541724317838715), 8505237664505880], [4971730988954452, (-20767576144682156)], [11979616743082150]]], r := 124176567152851068, ok := true }, r1 := { p := [[[460120655262895130292]], [[(-17394217392364513721), 0], [(-28689092846953608222)]], [[627411923245023238, 0, 0], [1017128564039925803, 0], [2415375417932245217]], [[(-22413430965981349), 0, 0, 0], [(-30904589202676414), 0, 0], [(-86785262026762086), 0], [(-206296672718234107)]], [[822836623492092, 0, 0, 0, 0], [961714486658439, 0, 0, 0], [2699768648867193, 0, 0], [7344850231481739, 0], [17980550206355733]]], r := 103254523310648162, ok := true }, r2 := { p := [[[1385884320031456843181]], [[(-64018524073802110005), 33676135642824342673], [(-232995850508619642198)]], [[2580075571109326867, (-1155860828955032108), 110799364999801261], [10637042722892141703, (-1986624346376775247)], [30033963435997230635]], [[(-101638598659568870), 43133473251389624, 2575823564107912, (-1338832192439704)], [(-423494231879181195), 71214716561068899, (-1915869335043218)], [(-1354401520127167482), 198860288582805501], [(-3507600031763034329)]], [[4012597230827681, (-1622906026660293), (-21091959856722), (-2940622853652), 15344631702857], [16575523100077888, (-2346820728836750), 347082294171136, (-184933607274834)], [53352648808908766, (-6546939683548175), (-51873025633700)], [156501368978307194, (-17722453296209904)], [387666604404530250]]], r := 9700090836677364960, ok := true }, r3 := { p := [[[8587719887348737512479]], [[(-675061486971237724367), 234627199613771162704], [(-1526550422277509189231)]], [[41240912653902515407, (-16193415186259209822), 188886656013225926], [123504376714755316718, (-20405512886620118270)], [207102792981715821141]], [[(-2258604485761111882), 975962850320484141, 10717597658521065, (-3938170889272774)], [(-7613741309932665013), 1532465292594189577, (-31677407777537247)], [(-16889138214116331337), 1890349539520539732], [(-25037897586697465177)]], [[116351758724656497, (-52833262011651218), (-56335640665645), (-134539247612151), 77717954579662], [418823096484865127, (-90167947764456864), 420518412712134, 105764179460824], [1043843279525006568, (-138108348430701128), (-1035698381431094)], [2049923885529032263, (-172098775639807236)], [2840801281865351238]]], r := 544176177307659643922, ok := true }, eta := { p := [[[(-2033000607313655751572)]], [[94452686775463954572, 0], [280454338480480292880]], [[(-3933206449895094059), 0, 0], [(-13008653571735762855), 0], [(-34335706499315871650)]], [[158855703725670582, 0, 0, 0], [524824853562596847, 0, 0], [1565806559518350808, 0], [3891675703796941491]], [[(-6396829922640585), 0, 0, 0, 0], [(-20799816005882801), 0, 0, 0], [(-62436578011693146), 0, 0], [(-175295788396136357), 0], [(-422257528244986478)]]], r := 1344528025535156830, ok := true } }
theorem sB_6 : stageB c6 w6 = true := by decide +kernel
theorem s0_6 : stageC0 w6 q6 = true := by decide +kernel
theorem s1_6 : stageC1 w6 q6 = true := by decide +kernel
theorem s2_6 : stageC2 w6 q6 = true := by decide +kernel
theorem s3_6 : stageC3 w6 q6 = true := by decide +kernel
theorem sE_6 : stageE w6 q6 = true := by decide +kernel
theorem sF_6 : stageF w6 = true := by decide +kernel
theorem ok_6 : (domOK c6 && cellCheck c6 q6) = true :=
  staged_check c6 q6 w6 (by decide +kernel) sB_6 s0_6 s1_6 s2_6 s3_6 sE_6 sF_6

theorem region : RegionPosI 2882303761517117440 3458764513820540928 13835058055282163712 16140901064495857664 4323455642275676160 6341068275337658368 :=
  (RegionPosI.split_s 5332261958806667264 (RegionPosI.split_s 4827858800541171712 (RegionPosI.split_s 4575657221408423936 (RegionPosI.of_check c0 q0 ok_0 2882303761517117440 3458764513820540928 13835058055282163712 16140901064495857664 4323455642275676160 4575657221408423936 (by decide +kernel)) (RegionPosI.of_check c1 q1 ok_1 2882303761517117440 3458764513820540928 13835058055282163712 16140901064495857664 4575657221408423936 4827858800541171712 (by decide +kernel))) (RegionPosI.split_s 5080060379673919488 (RegionPosI.of_check c2 q2 ok_2 2882303761517117440 3458764513820540928 13835058055282163712 16140901064495857664 4827858800541171712 5080060379673919488 (by decide +kernel)) (RegionPosI.of_check c3 q3 ok_3 2882303761517117440 3458764513820540928 13835058055282163712 16140901064495857664 5080060379673919488 5332261958806667264 (by decide +kernel)))) (RegionPosI.split_s 5836665117072162816 (RegionPosI.split_s 5584463537939415040 (RegionPosI.of_check c4 q4 ok_4 2882303761517117440 3458764513820540928 13835058055282163712 16140901064495857664 5332261958806667264 5584463537939415040 (by decide +kernel)) (RegionPosI.of_check c5 q5 ok_5 2882303761517117440 3458764513820540928 13835058055282163712 16140901064495857664 5584463537939415040 5836665117072162816 (by decide +kernel))) (RegionPosI.of_check c6 q6 ok_6 2882303761517117440 3458764513820540928 13835058055282163712 16140901064495857664 5836665117072162816 6341068275337658368 (by decide +kernel))))

end CKLaneC.RSC2.BA_0135