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

import Definitions.Def_CK_CKLaneC_RSC2_BD_0143_part00

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

namespace CKLaneC.RSC2.BD_0143
open CKLaneC.TM3 CKLaneC.RSCell

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 := 8791026472627208192, bh := 144115188075855872, tc := 11240984669916758016, th := 288230376151711744, sc := 15798627492815699968, sh := 126100789566373888 }
noncomputable def q6 : Cert := { V0 := [[[778181906802612640]], [[(-37647998104119721), 19902188816845755], [10897973586736008]], [[38749461522484, (-957906579708378), (-1963021845676)], [(-482980246035971), 277285410378304], [95738943422294]], [[(-526306868497), 627045527770, 284202896821, (-16524287757)], [(-1377241103401), (-12081058993031), (-82268269732)], [(-3468987277671), 2405886406696], [1349618376548]], [[1316950674, (-6891521384), (-13956715666), 2367843344, 4841356], [(-15104899383), (-49467091408), 11556750477, (-685420091)], [(-42023075716), (-82325102275), (-1867692701)], [(-44737553635), 33671260262], [14642809522]]], r0 := 71192611444, V1 := [[[1274253667810947829]], [[(-61381547572354088), 0], [17768128926974604]], [[43981194143894, 0, 0], [(-776340771043220), 0], [154484906801970]], [[(-518298881000), 0, 0, 0], [(-3010197516119), 0, 0], [(-5340171441125), 0], [2164881834393]], [[994803976, 0, 0, 0, 0], [(-13660064016), 0, 0, 0], [(-83797834762), 0, 0], [(-67025146069), 0], [23161570894]]], r1 := 54343066288, V2 := [[[1645775338728116572]], [[(-37907826778608368), 19636760947448924], [(-278307067153065829)]], [[44526340067862, (-936777325880519), (-4061659547752)], [(-400943706831509), 390838337989841], [94665594658511]], [[(-525690389137), 202339445775, 482277816494, (-15240878747)], [(-3055199740478), (-20113902522511), 533961008198], [(-1764556404051), (-5507366964677)], [2592676963120]], [[1315829797, (-5648393805), (-18520791527), 2143416781, 9623167], [(-16046975705), 82896595393, (-46179080932), (-1187512687)], [(-124979552562), 228182255920, 25865809279], [(-107126557105), (-115877491742)], [(-11151922528)]]], r2 := 403434929292, V3 := [[[2432069905907042836]], [[(-76533864753657083), 38924252952283819], [(-268315497127976835)]], [[122197374687245, (-1829774759743626), (-23764300861988)], [(-820535748278086), 822594566418426], [182455130002418]], [[(-1575339517682), (-1458591292698), 3003282394359, (-111028179432)], [(-4766256817318), (-43961158667375), 1691661410934], [(-2951744694891), (-9748538455892)], [5262201933172]], [[3297138476, 20088623923, (-125289665043), 14753773137, 216627910], [(-63269380834), 245087741878, (-119030186339), (-10208656792)], [(-258244564319), 339719372384, 100797047059], [(-218993983538), (-223806929150)], [(-17407880595)]]], r3 := 1005795873928, Vm := [[[2475832852407978295]], [[(-82694455334831497), 0], [(-219908786142140170)]], [[102621280217251, 0, 0], [(-2626731657471411), 0], [4800603298584003]], [[2801315074519, 0, 0, 0], [(-33461740316502), 0, 0], [23617009939906, 0], [427515093005544]], [[97833166215, 0, 0, 0, 0], [(-738618462534), 0, 0, 0], [(-3394148938820), 0, 0], [21379943033847, 0], [33332562098214]]], rm := 221243656832652 }
noncomputable def w6 : Wit := { Z0 := { p := [[[779182448983395358]], [[(-37793368347377477), 19979037153420393], [10940053940303257]], [[45950575533367, (-969060726855833), 0], [(-488927570877100), 280514203597519], [96699485816877]], [[(-657770469711), 1178219885470, 0, 0], [(-1097638201712), (-12536604381465), 0], [(-3599505783153), 2479473995304], [1367998541610]], [[1925241524, (-16865909480), 0, 0, 0], [(-19569387277), (-28144569275), 0, 0], [(-36348848304), (-92295020081), 0], [(-47134512065), 35076885682], [14965065758]]], r := 14543226773, ok := true }, Z1 := { p := [[[1278658377818905204]], [[(-62019886518773296), 0], [17952909030241243]], [[75406072670141, 0, 0], [(-802342680413702), 0], [158686335699492]], [[(-1079418206705), 0, 0, 0], [(-1801252433579), 0, 0], [(-5906881285173), 0], [2244920683667]], [[3159370707, 0, 0, 0, 0], [(-32113866300), 0, 0, 0], [(-59649392088), 0, 0], [(-77348942876), 0], [24558056629]]], r := 12087758223, ok := true }, Z2 := { p := [[[1655292304377546532]], [[(-38568574605662364), 19979037153420393], [(-283158065099984005)]], [[60702648489506, (-969060726855833), 0], [(-181805719699425), 280514203597519], [926389978905518]], [[(-694885481390), 1178219885470, 0, 0], [(-5776181734671), (-12536604381465), 0], [(-19507833427305), 2479473995304], [(-46938160186631)]], [[2322594445, (-16865909480), 0, 0, 0], [(-5704859382), (-28144569275), 0, 0], [(-106916254068), (-92295020081), 0], [(-142853391806), 35076885682], [310971809690]]], r := 35854969232, ok := true }, Z3 := { p := [[[2463043706562055964]], [[(-79488582416779722), 40426988742409601], [(-278674264991136157)]], [[222335767285923, (-1997476095017242), 0], [(-183154042858796), 514075970814641], [1362307577423428]], [[(-3046522302087), 4889689590727, 0, 0], [(-15601246443166), (-20925694882611), 0], [(-37116182152554), 3649832929151], [(-43772457434756)]], [[15477946105, (-74731773737), 0, 0, 0], [(-5485267119), (-135368455674), 0, 0], [(-193133185704), (-75094776784), 0], [(-155558635081), 47632338361], [424315336355]]], r := 71818772173, ok := true }, iE := { p := [[[18690343581741891703]], [[(-16537733510077574), 0], [(-43978678945497698)]], [[314710889730975, 0, 0], [1039354988431193, 0], [3040504204058435]], [[(-791786915812), 0, 0, 0], [5094701207218, 0, 0], [7074006401801, 0], [(-17029984849657)]], [[8476862309, 0, 0, 0, 0], [31847623136, 0, 0, 0], [192795746111, 0, 0], [315999366121, 0], [638148920653]]], r := 71704051113, ok := true }, iHu := { p := [[[18909677772972405566]], [[(-33856313836955529), 0], [(-69536269871217791)]], [[674941295947986, 0, 0], [2217453949025954, 0], [2847144030906658]], [[(-2815640029043), 0, 0, 0], [4780396315836, 0, 0], [9818284704891, 0], [(-24394520489075)]], [[33003230446, 0, 0, 0, 0], [132662510078, 0, 0, 0], [447889740324, 0, 0], [559617963772, 0], [587277449938]]], r := 116127170666, ok := true }, T := { p := [[[11240984669916758016]], [[0, 288230376151711744], [0]]], r := 0, ok := true }, E := { p := [[[18206319505723341367]], [[16109455605680146, 0], [42839762512634180]], [[(-292306725271248), 0, 0], [(-936627182402833), 0], [(-2860961576339033)]], [[241387415779, 0, 0, 0], [(-8096496166006), 0, 0], [(-16629103366715), 0], [2887991676164]], [[(-2439393203), 0, 0, 0, 0], [(-8169216925), 0, 0, 0], [(-91532415567), 0, 0], [(-34460681761), 0], [(-110378221077)]]], r := 51404793019, ok := true }, de := { p := [[[(-4944961510884561868)]], [[179453054307977344, 0], [368572198192262600]], [[(-222288979116413), 0, 0], [2028750610739235, 0], [(-937694498509987)]], [[2995186379385, 0, 0, 0], [11166954699139, 0, 0], [22935408129144, 0], [25950098289148]], [[(-10448282725), 0, 0, 0, 0], [61466834116, 0, 0, 0], [280899207790, 0, 0], [259289112849, 0], [(-185922430974)]]], r := 42683930978, ok := true }, dde := { p := [[[(-55084943171557860137)]], [[136467733352442482, 0], [280286187705133619]], [[(-2758208916525137), 0, 0], [(-9092796969831394), 0], [(-11635112712503589)]], [[12828827291286, 0, 0, 0], [(-11387073133477), 0, 0], [(-23387501494291), 0], [111148118005122]], [[(-152962413991), 0, 0, 0, 0], [(-625730152657), 0, 0, 0], [(-2021083774678), 0, 0], [(-2639553809781), 0], [(-2721896469132)]]], r := 1052929510695, ok := true }, nJu := { p := [[[(-9889923021769123735)]], [[358906108615954688, 0], [737144396384525200]], [[(-444577958232826), 0, 0], [4057501221478471, 0], [(-1875388997019974)]], [[5990372758770, 0, 0, 0], [22333909398278, 0, 0], [45870816258288, 0], [51900196578297]], [[(-20896565449), 0, 0, 0, 0], [122933668233, 0, 0, 0], [561798415581, 0, 0], [518578225699, 0], [(-371844861948)]]], r := 85367861949, ok := true }, Jd1 := { p := [[[(-110169886343115720273)]], [[272935466704884965, 0], [560572375410267239]], [[(-5516417833050274), 0, 0], [(-18185593939662787), 0], [(-23270225425007177)]], [[25657654582573, 0, 0, 0], [(-22774146266954), 0, 0], [(-46775002988582), 0], [222296236010245]], [[(-305924827981), 0, 0, 0, 0], [(-1251460305313), 0, 0, 0], [(-4042167549355), 0, 0], [(-5279107619562), 0], [(-5443792938264)]]], r := 2105859021380, ok := true }, term0 := { p := [[[341070727527313113321]], [[(-1655118329195745363), 0], [(-3072121348364795256)]], [[36076928060411654, 0, 0], [107832064760066520, 0], [125014691025789855]], [[(-239782694807498), 0, 0, 0], [(-202297704341551), 0, 0], [(-442799647766292), 0], [(-1688126281797255)]], [[3118047587797, 0, 0, 0, 0], [12356300467093, 0, 0, 0], [34158196217298, 0, 0], [45959324066346, 0], [42771707273220]]], r := 9182513675632, ok := true }, r0 := { p := [[[41665150413250406876]], [[(-176145302950493567), 2127873559322540850], [(-187021059674082706)]], [[4016661544994684, (-8149254236261247), 26831165382568633], [5764161788016680, (-9796396981706832)], [5981997731003843]], [[(-20478800116518), 180674500905426, (-59558056095062), (-11414483283787)], [41242461569369, 314061878348069, (-136031448986298)], [3179589762599, 302778035994561], [(-63165841189675)]], [[256664876613, (-845167144063), 1049313521778, 1131129604178, (-69824533124)], [537406970880, 1723597975088, 4953263235837, (-262227302210)], [1817866026864, 487856336649, 3680279197637], [1363780661215, (-3303090493297)], [1222083472632]]], r := 3322813678000, ok := true }, r1 := { p := [[[111426382435278581993]], [[(-396954495181209177), 0], [(-521610817440758063)]], [[8655597251843922, 0, 0], [17106400579405950, 0], [15763673352115727]], [[(-40116192847557), 0, 0, 0], [80360545239435, 0, 0], [35784391860809, 0], [(-175558338166410)]], [[487841769961, 0, 0, 0, 0], [1350305535624, 0, 0, 0], [4563917625416, 0, 0], [4035520824622, 0], [3204472040128]]], r := 4304004724999, ok := true }, r2 := { p := [[[43749330540344470835]], [[(-255254940945215560), 2146273697423415003], [(-1062239580924207789)]], [[4410396532940749, (-9009417787946801), 25945949327164115], [32471879934663019, (-15542816179193749)], [67899324334780530]], [[(-26250892456890), 180282817932729, (-20348463102175), (-17075642574276)], [(-112796221080963), 575356988720569, 195277522635817], [(-157760116620233), 165157763759770], [(-705374731308993)]], [[289548422418, (-840636730147), 818483049418, 1373542491922, (-60380867831)], [2443523257966, 2099996178004, (-7826049143559), 1440772401920], [9182167486931, 9242384783696, (-8309415652703)], [17491767663895, (-461428257140)], [21269485786550]]], r := 29850377402926, ok := true }, r3 := { p := [[[180029954865003846631]], [[(-1559787437456374528), 8721243405702059123], [(-3974722323573559316)]], [[32425453449089657, (-49174109316219811), 98622945758714784], [137850903198717627, (-58269142078527061)], [195210171879360050]], [[(-236643639926970), 1056642870957749, 373517462682857, (-216748209633672)], [(-532905896665868), 1890009815834269, 1150148837611290], [(-782856130205047), 689674584637386], [(-2430747265378564)]], [[2972563713285, (-4571619790086), (-8651224806901), 18281161689880, (-715018116226)], [14887200757581, 19941359523131, (-45964691097638), 6736471597024], [42712856784376, 33119256664366, (-24223849596874)], [65338545183441, (-5208070451963)], [64422140684228]]], r := 268171793465989, ok := true }, eta := { p := [[[(-224197206467753357775)]], [[827150324392892695, 0], [1756689670457396442]], [[(-16992756961332632), 0, 0], [(-56669956236217181), 0], [(-82245066124869688)]], [[88455612096646, 0, 0, 0], [(-2959072378646), 0, 0], [77471927860695, 0], [967403995969881]], [[(-1066638680824), 0, 0, 0, 0], [(-4472598078768), 0, 0, 0], [(-15297482236541), 0, 0], [(-24019411076579), 0], [(-27520735612063)]]], r := 87501273661499860, 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

noncomputable def c7 : Cell := { bc := 9079256848778919936, bh := 144115188075855872, tc := 11240984669916758016, th := 288230376151711744, sc := 15798627492815699968, sh := 126100789566373888 }
noncomputable def q7 : Cert := { V0 := [[[800371847847914821]], [[(-38628198467306014), 20466658466354538], [11297610596637440]], [[35821212262102, (-982406327634112), (-2135323524155)], [(-497405169236562), 287324922664372], [104205448609917]], [[(-558227686703), 522478684859, 308358853110, (-17958745475)], [(-1553936689792), (-12422915695368), (-90185884529)], [(-3746606154143), 2616955416197], [1475547428833]], [[1238979290, (-7256209022), (-15070451192), 2565258963, 5568050], [(-16856685860), (-55194977584), 12618717660, (-750262711)], [(-46417178209), (-88666008904), (-2096496665)], [(-47869991960), 36757938348], [16891931427]]], r0 := 72563389528, V1 := [[[1310425565725044449]], [[(-62956134135113536), 0], [18412815413335291]], [[37614302444105, 0, 0], [(-798522129508316), 0], [168057370275385]], [[(-547788518639), 0, 0, 0], [(-3362526398460), 0, 0], [(-5754730404971), 0], [2363980512876]], [[878725969, 0, 0, 0, 0], [(-15890865255), 0, 0, 0], [(-92548714547), 0, 0], [(-71248308255), 0], [26694097180]]], r1 := 55806176396, V2 := [[[1089560420541563741]], [[(-38717623171391902), 20395492109780694], [(-277897672599322838)]], [[37911234807193, (-976048729548178), (-2890380415396)], [(-409274715110055), 367440487445854], [109930958635460]], [[(-558531579373), 374725827057, 379927803705, (-17589517970)], [(-3562210641082), (-19135958217176), 637174962958], [(-2397491432593), (-6185774412053)], [2491965904220]], [[1241931147, (-6852819034), (-16743074211), 2497049888, 7459092], [(-16816954136), 89440640483, (-56173217018), (-1153412905)], [(-128437207471), 260491279892, 25650732102], [(-103670622049), (-110095184510)], [(-14010199597)]]], r2 := 373333140020, V3 := [[[1896210534166840994]], [[(-78188489451750607), 40528683426612075], [(-267523129894629098)]], [[111621797644274, (-1916252823848574), (-19976417241070)], [(-834958794817062), 780967080744448], [213568011192459]], [[(-1704029692226), (-944140247124), 2726795710034, (-131623131364)], [(-5814121705155), (-42474921695225), 2096571706145], [(-4256312699816), (-11051558924669)], [5101767346521]], [[3406372297, 18048881681, (-125028144993), 17873996525, 200463047], [(-65437701067), 269153896185, (-157596885609), (-10332391930)], [(-265447164726), 402680934006, 101319980092], [(-215529576193), (-210166153194)], [(-22649662100)]]], r3 := 957097237632, Vm := [[[2059244389955808087]], [[(-87614264477653671), 0], [(-194324392400755306)]], [[30369330378495, 0, 0], [(-2131824625845603), 0], [8353486742143180]], [[597136732509, 0, 0, 0], [(-31691400643627), 0, 0], [269682952084398, 0], [789775188796991]], [[33447530484, 0, 0, 0, 0], [(-1228072633560), 0, 0, 0], [7724073015196, 0, 0], [67580195601289, 0], [57604193603584]]], rm := 612043973199979 }
noncomputable def w7 : Wit := { Z0 := { p := [[[801460545280572928]], [[(-38786005275682657), 20550270391809562], [11343764441271083]], [[43605018044053, (-994512955786735), 0], [(-503904674060161), 290865754904386], [105284457928186]], [[(-698913503547), 1118077385744, 0, 0], [(-1250440888271), (-12920632668210), 0], [(-3892527134723), 2699601485338], [1496735322077]], [[1866887824, (-17920859066), 0, 0, 0], [(-21618013748), (-32062586879), 0, 0], [(-40132368982), (-99808388070), 0], [(-50616621807), 38377828771], [17273543673]]], r := 14543069831, ok := true }, Z1 := { p := [[[1315217305075811985]], [[(-63648829170351027), 0], [18615408313880753]], [[71556952687677, 0, 0], [(-826920490765392), 0], [172774495061638]], [[(-1146934980179), 0, 0, 0], [(-2052005560239), 0, 0], [(-6387736836468), 0], [2456181041358]], [[3063610788, 0, 0, 0, 0], [(-35475714868), 0, 0, 0], [(-65858246535), 0, 0], [(-83063174247), 0], [28346328079]]], r := 12244208546, ok := true }, Z2 := { p := [[[1092310889821687597]], [[(-39011445314366097), 20550270391809562], [(-280006595694349154)]], [[48694056165742, (-994512955786735), 0], [(-261722160999247), 290865754904386], [651444578756890]], [[(-710214337986), 1118077385744, 0, 0], [(-6247182828293), (-12920632668210), 0], [(-20493937029702), 2699601485338], [(-44837077967563)]], [[2006247170, (-17920859066), 0, 0, 0], [(-9741340676), (-32062586879), 0, 0], [(-129085333955), (-99808388070), 0], [(-186423975240), 38377828771], [215833640939]]], r := 33635920120, ok := true }, Z3 := { p := [[[1910800726323104596]], [[(-80004736530662050), 41470127664783922], [(-273737447457474506)]], [[190291276171303, (-2039633618720532), 0], [(-333759546012693), 529260163347662], [1109140213564022]], [[(-3072552825529), 4604285554222, 0, 0], [(-16478932473647), (-21234672040092), 0], [(-38255627712648), 3945697456728], [(-40731777463338)]], [[13818238976, (-77766793438), 0, 0, 0], [(-20905351302), (-150223155653), 0, 0], [(-246687611352), (-79359151546), 0], [(-224645035214), 51067258734], [337925289499]]], r := 69436001235, ok := true }, iE := { p := [[[18614422050631338797]], [[(-14428162475740129), 0], [(-32000998048356412)]], [[325698439788128, 0, 0], [1071518360158359, 0], [2953249684680652]], [[(-723253404100), 0, 0, 0], [5906955626733, 0, 0], [9028126879696, 0], [(-12114365856297)]], [[8918998171, 0, 0, 0, 0], [36853672513, 0, 0, 0], [213965868503, 0, 0], [336456260009, 0], [593480368736]]], r := 71287263035, ok := true }, iHu := { p := [[[18781807833378022575]], [[(-29377625635924091), 0], [(-58422171616112079)]], [[686344931624492, 0, 0], [2263504831333092, 0], [2714341199990823]], [[(-2537464413759), 0, 0, 0], [6650249818931, 0, 0], [13225099980055, 0], [(-19956435462862)]], [[33549428920, 0, 0, 0, 0], [146042276573, 0, 0, 0], [488422878006, 0, 0], [577564647137, 0], [524721848218]]], r := 117859726280, ok := true }, T := { p := [[[11240984669916758016]], [[0, 288230376151711744], [0]]], r := 0, ok := true }, E := { p := [[[18280576533365817086]], [[14169396592394259, 0], [31427067269447046]], [[(-308874317101425), 0, 0], [(-1003582258614832), 0], [(-2846255941789557)]], [[222948099101, 0, 0, 0], [(-8475428550308), 0, 0], [(-16854763806396), 0], [2017929148957]], [[(-2631279642), 0, 0, 0, 0], [(-10314328580), 0, 0, 0], [(-98032877944), 0, 0], [(-40790870195), 0], [(-107344944487)]]], r := 53094250377, ok := true }, de := { p := [[[(-4211363152286394841)]], [[183604419460853094, 0], [365127156161379054]], [[(-198790838403487), 0, 0], [2123700239606023, 0], [(-786173450107905)]], [[3128227530789, 0, 0, 0], [12352142620993, 0, 0], [24564238273493, 0], [24602619249708]], [[(-9694843310), 0, 0, 0, 0], [71844144708, 0, 0, 0], [312343472871, 0, 0], [284127576343, 0], [(-151629886503)]]], r := 44610747513, ok := true }, dde := { p := [[[(-54570064552319584160)]], [[118167404858148952, 0], [234995043221307549]], [[(-2789272373575526), 0, 0], [(-9218167594658599), 0], [(-11030950434313765)]], [[11525827685234, 0, 0, 0], [(-19785398163772), 0, 0], [(-39346472085329), 0], [90647354543888]], [[(-154448982922), 0, 0, 0, 0], [(-679738437030), 0, 0, 0], [(-2184682103150), 0, 0], [(-2688213986643), 0], [(-2415622512304)]]], r := 1072662570583, ok := true }, nJu := { p := [[[(-8422726304572789681)]], [[367208838921706188, 0], [730254312322758109]], [[(-397581676806974), 0, 0], [4247400479212046, 0], [(-1572346900215810)]], [[6256455061579, 0, 0, 0], [24704285241986, 0, 0], [49128476546987, 0], [49205238499417]], [[(-19389686619), 0, 0, 0, 0], [143688289416, 0, 0, 0], [624686945743, 0, 0], [568255152687, 0], [(-303259773005)]]], r := 89221495017, ok := true }, Jd1 := { p := [[[(-109140129104639168319)]], [[236334809716297905, 0], [469990086442615099]], [[(-5578544747151052), 0, 0], [(-18436335189317198), 0], [(-22061900868627530)]], [[23051655370468, 0, 0, 0], [(-39570796327544), 0, 0], [(-78692944170658), 0], [181294709087776]], [[(-308897965844), 0, 0, 0, 0], [(-1359476874059), 0, 0, 0], [(-4369364206300), 0, 0], [(-5376427973286), 0], [(-4831245024607)]]], r := 2145325141160, ok := true }, term0 := { p := [[[335413702176328936441]], [[(-1440861674000581957), 0], [(-2591002869668403266)]], [[35810227433096894, 0, 0], [106604710608991529, 0], [115861618678950075]], [[(-214677597680373), 0, 0, 0], [(-63642251212201), 0, 0], [(-172504539756900), 0], [(-1370854066732813)]], [[3074173718480, 0, 0, 0, 0], [12796709340684, 0, 0, 0], [35299875326907, 0, 0], [44330524682115, 0], [36798795025652]]], r := 8784735787714, ok := true }, r0 := { p := [[[41314549965095591550]], [[(-164593376788018356), 2109466410613636419], [(-163813309414075966)]], [[4106600953069275, (-7518583805213251), 26573470691582229], [5793197739876295, (-8623020072258679)], [5630988211476410]], [[(-19339147675814), 184483945777007, (-49552775680913), (-11959602779514)], [48792911368784, 316906267226599, (-121834165983734)], [11331747281622, 284368819351682], [(-54050930624340)]], [[265356936284, (-786053478380), 1060016533549, 1178198765984, (-72956593048)], [604532254044, 2090652255237, 5056755074963, (-283225094809)], [1961863114524, 934542805069, 3423801006123], [1357121629542, (-2844483583755)], [1061768755301]]], r := 3408278506708, ok := true }, r1 := { p := [[[110444860787153354387]], [[(-362566261170837188), 0], [(-460564037178181752)]], [[8835064978544978, 0, 0], [17297999002050171, 0], [14783507917039154]], [[(-37262345232135), 0, 0, 0], [99365025607233, 0, 0], [60038887729316, 0], [(-151756480002314)]], [[502515572765, 0, 0, 0, 0], [1509208025206, 0, 0, 0], [4950831059308, 0, 0], [4059545425227, 0], [2759398073726]]], r := 4433908027703, ok := true }, r2 := { p := [[[41891136705581991704]], [[(-190802510256960593), 2115846167707872782], [(-798449138207573465)]], [[4222301026725608, (-7821863035666885), 26302663237187733], [32050394726850817, (-14885422364466383)], [64154902502909945]], [[(-21283289297759), 184522146998020, (-36300680641959), (-13966532392695)], [(-74873319935416), 612112786657754, 161152418371175], [(-52944664589656), 164081797076850], [(-546259580719520)]], [[275397483221, (-785974218461), 984368221759, 1266795470634, (-70056532162)], [2534374360424, 2139196480448, (-8109995594633), 1665305688274], [9821443846763, 9115272332433, (-8735234866441)], [17529234065537, 81563268656], [18646458492422]]], r := 25643877489965, ok := true }, r3 := { p := [[[172842903329194762465]], [[(-1286699727433858378), 8607427896344500356], [(-3221069261046072965)]], [[31532481285973092, (-45259663520632275), 100822771224383048], [135493174862052684, (-55561577958519949)], [182092713589558487]], [[(-206411135055982), 1097363057198299, 278031800438997, (-201324498662381)], [(-358874239063510), 2025287092901996, 1047947068445458], [(-398110392290893), 666800021993377], [(-1954052798798546)]], [[2899777506759, (-4473193821961), (-8252086708277), 18475569578059, (-894781979365)], [15407582927122, 20739857204377, (-49418961110581), 8680533108271], [44501328439999, 34397261197329, (-26817188715468)], [63232952784819, (-2514363788189)], [55177017096915]]], r := 238438345068653, ok := true }, eta := { p := [[[(-221005496604074757668)]], [[713928822474109368, 0], [1438467024935411353]], [[(-17060989864136460), 0, 0], [(-56647066669689810), 0], [(-77072098980080658)]], [[79234639824049, 0, 0, 0], [(-65896284716652), 0, 0], [(-65870408398786), 0], [761431843618847]], [[(-1071437603147), 0, 0, 0, 0], [(-4767577133560), 0, 0, 0], [(-16231711545065), 0, 0], [(-23862413528504), 0], [(-24132290079993)]]], r := 270552677097799615, ok := true } }
theorem sB_7 : stageB c7 w7 = true := by decide +kernel
theorem s0_7 : stageC0 w7 q7 = true := by decide +kernel
theorem s1_7 : stageC1 w7 q7 = true := by decide +kernel
theorem s2_7 : stageC2 w7 q7 = true := by decide +kernel
theorem s3_7 : stageC3 w7 q7 = true := by decide +kernel
theorem sE_7 : stageE w7 q7 = true := by decide +kernel
theorem sF_7 : stageF w7 = true := by decide +kernel
theorem ok_7 : (domOK c7 && cellCheck c7 q7) = true :=
  staged_check c7 q7 w7 (by decide +kernel) sB_7 s0_7 s1_7 s2_7 s3_7 sE_7 sF_7

theorem region : RegionPosI 8646911284551352320 9223372036854775808 10376293541461622784 11529215046068469760 15420325124116578304 15924728282382073856 :=
  (RegionPosI.split_t 10952754293765046272 (RegionPosI.split_s 15672526703249326080 (RegionPosI.split_b 8935141660703064064 (RegionPosI.of_check c0 q0 ok_0 8646911284551352320 8935141660703064064 10376293541461622784 10952754293765046272 15420325124116578304 15672526703249326080 (by decide +kernel)) (RegionPosI.of_check c1 q1 ok_1 8935141660703064064 9223372036854775808 10376293541461622784 10952754293765046272 15420325124116578304 15672526703249326080 (by decide +kernel))) (RegionPosI.split_b 8935141660703064064 (RegionPosI.of_check c2 q2 ok_2 8646911284551352320 8935141660703064064 10376293541461622784 10952754293765046272 15672526703249326080 15924728282382073856 (by decide +kernel)) (RegionPosI.of_check c3 q3 ok_3 8935141660703064064 9223372036854775808 10376293541461622784 10952754293765046272 15672526703249326080 15924728282382073856 (by decide +kernel)))) (RegionPosI.split_s 15672526703249326080 (RegionPosI.split_b 8935141660703064064 (RegionPosI.of_check c4 q4 ok_4 8646911284551352320 8935141660703064064 10952754293765046272 11529215046068469760 15420325124116578304 15672526703249326080 (by decide +kernel)) (RegionPosI.of_check c5 q5 ok_5 8935141660703064064 9223372036854775808 10952754293765046272 11529215046068469760 15420325124116578304 15672526703249326080 (by decide +kernel))) (RegionPosI.split_b 8935141660703064064 (RegionPosI.of_check c6 q6 ok_6 8646911284551352320 8935141660703064064 10952754293765046272 11529215046068469760 15672526703249326080 15924728282382073856 (by decide +kernel)) (RegionPosI.of_check c7 q7 ok_7 8935141660703064064 9223372036854775808 10952754293765046272 11529215046068469760 15672526703249326080 15924728282382073856 (by decide +kernel)))))

end CKLaneC.RSC2.BD_0143