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

import Definitions.Def_CK_CKLaneC_RSC2_S00_0001_part00

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

namespace CKLaneC.RSC2.S00_0001
open CKLaneC.TM3 CKLaneC.RSCell

noncomputable def w5 : Wit := { Z0 := { p := [[[215250797900193581]], [[(-1763193582478407), 215250797900193581], [352594329350808]], [[7286215007645, (-1763193582478407), 0], [(-2963049353507), 352594329350808], [(-2627756345115)]], [[(-41797450142), 7286215007645, 0, 0], [14284682273, (-2963049353507), 0], [21959776019, (-2627756345115)], [29297502075]], [[356685753, (-41797450142), 0, 0, 0], [(-105028453), 14284682273, 0, 0], [(-102580862), 21959776019, 0], [(-244374989), 29297502075], [(-379042105)]]], r := 67979825268, ok := true }, Z1 := { p := [[[1722006383201548652]], [[(-14105548659827253), 0], [2820754634806467]], [[58289720061161, 0, 0], [(-23704394828054), 0], [(-21022050760920)]], [[(-334379601131), 0, 0, 0], [114277458190, 0, 0], [175678208152, 0], [234380016602]], [[2853486030, 0, 0, 0, 0], [(-840227622), 0, 0, 0], [(-820646895), 0, 0], [(-1954999911), 0], [(-3032336840)]]], r := 16774656500, ok := true }, Z2 := { p := [[[38372907406038041069434]], [[(-139107957119896217033), 215250797900193581], [(-634901276717245463459)]], [[663730447714886786, (-1763193582478407), 0], [2288261755486616694, 352594329350808], [11075094158607194446]], [[(-4420560742618687), 7286215007645, 0, 0], [(-10623808676323219), (-2963049353507), 0], [(-39828606512992521), (-2627756345115)], [(-196141616732457979)]], [[43401595998665, (-41797450142), 0, 0, 0], [68256808707594, 14284682273, 0, 0], [182978831171689, 21959776019, 0], [704437256947454, 29297502075], [3498629687081260]]], r := 244776967978387, ok := true }, Z3 := { p := [[[131860269526216001498856]], [[(-3285154987473159359973), 1479318140495209818], [(-2210233441395030888633)]], [[85611347891273500842, (-43610401706693734), 0], [55461569677793800770, 2102977080733104], [38748130104888313251]], [[(-2260644168015049428), 1128747460842265, 0, 0], [(-1449393926371994746), (-57551752401944), 0], [(-975043256387607394), (-16128339466975)], [(-688319568102281471)]], [[60069690700896633, (-29747386924028), 0, 0, 0], [38337986231913002, 1422935019935, 0, 0], [25510115457115651, 447700742719, 0], [17350234687808931, 181626591060], [12304163238842487]]], r := 32725220149206075, ok := true }, iE := { p := [[[38376718033177123491881]], [[(-139120788277806199527), 0], [(-634895034670602116042)]], [[663792796135399022, 0, 0], [2288239412557982688, 0], [11075047638920664719]], [[(-4420982724713107), 0, 0, 0], [(-10623671344199072), 0, 0], [(-39828442172313292), 0], [(-196141098073026261)]], [[43405792761783, 0, 0, 0, 0], [68255641682458, 0, 0, 0], [182977865849562, 0, 0], [704435432815502, 0], [3498622976824454]]], r := 244726582800016, ok := true }, iHu := { p := [[[131872624196896210351632]], [[(-3285456035125674605523), 0], [(-2210215878175484492062)]], [[85619200955436325336, 0, 0], [55461178828668156820, 0], [38747995407477879024]], [[(-2260851593398886774), 0, 0, 0], [(-1449384090083075039), 0, 0], [(-975040206072956559), 0], [(-688318051229975305)]], [[60075203123052713, 0, 0, 0, 0], [38337732343783557, 0, 0, 0], [25510038243735036, 0, 0], [17350200122094711, 0], [12304143496293379]]], r := 32724272569289267, ok := true }, T := { p := [[[2305843009213693952]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[8866895981744983]], [[32143696016195, 0], [146691757926871]], [[(-36843310770), 0, 0], [534859836713, 0], [(-132044294875)]], [[331919203, 0, 0, 0], [(-669883455), 0, 0], [(-450648870), 0], [800231012]], [[(-4485395), 0, 0, 0, 0], [6034895, 0, 0, 0], [(-92), 0, 0], [2731165, 0], [(-7274827)]]], r := 4728432, ok := true }, de := { p := [[[(-156881958138768069860)]], [[359638215535924655, 0], [241938435905985678]], [[(-4859939042030523), 0, 0], [49571375745, 0], [(-2199423652409847)]], [[87566469230808, 0, 0, 0], [10157, 0, 0], [6833, 0], [26659680636804]], [[(-1774995997922), 0, 0, 0, 0], [1, 0, 0, 0], [93, 0, 0], [1, 0], [(-363541099593)]]], r := 224150752558, ok := true }, dde := { p := [[[(-1755266334225676708237738)]], [[47439271013806057583841, 0], [31913691409287711450648]], [[(-1282142459906283654134), 0, 0], [(-862532200350162585086), 0], [(-580248934747670149598)]], [[34652498916386068867, 0, 0, 0], [23311681089205214321, 0, 0], [15682403641828961297, 0], [10549980631775858968]], [[(-936554024767153881), 0, 0, 0, 0], [(-630045434843384610), 0, 0, 0], [(-423848747076458889), 0, 0], [(-285134611669618507), 0], [(-191817829668639867)]]], r := 72191501487758510, ok := true }, nJu := { p := [[[(-313763916277536139719)]], [[719276431071849311, 0], [483876871811971356]], [[(-9719878084061045), 0, 0], [99142751490, 0], [(-4398847304819693)]], [[175132938461617, 0, 0, 0], [20315, 0, 0], [13667, 0], [53319361273608]], [[(-3549991995844), 0, 0, 0, 0], [2, 0, 0, 0], [187, 0, 0], [2, 0], [(-727082199185)]]], r := 448301505107, ok := true }, Jd1 := { p := [[[(-3510532668451353416475475)]], [[94878542027612115167682, 0], [63827382818575422901297]], [[(-2564284919812567308268), 0, 0], [(-1725064400700325170171), 0], [(-1160497869495340299196)]], [[69304997832772137735, 0, 0, 0], [46623362178410428642, 0, 0], [31364807283657922595, 0], [21099961263551717937]], [[(-1873108049534307761), 0, 0, 0, 0], [(-1260090869686769219), 0, 0, 0], [(-847697494152917777), 0, 0], [(-570269223339237013), 0], [(-383635659337279734)]]], r := 144383002975517010, ok := true }, term0 := { p := [[[231551634781368016960294371469]], [[(-12516162261367225558648053539), 0], [(-8419742894858323838251609382)]], [[507410060355252428957056321, 0, 0], [455118649963308811451288224, 0], [229626473956885976440272398]], [[(-18285012567510189392741496), 0, 0, 0], [(-18450721112071973926172188), 0, 0], [(-12412194788296439413764531), 0], [(-5566667517487328089546793)]], [[617736208649005230802373, 0, 0, 0, 0], [664890220840042238194368, 0, 0, 0], [503196450238897776279186, 0, 0], [300900091487372368201841, 0], [126514695195606758805767]]], r := 85431368379920474170697, ok := true }, r0 := { p := [[[11821753604484196243627]], [[(-173526636059794112440), 23636233730243462751081], [(-193513713126019147439)]], [[2531021623741669277, (-346833670061576129061), 11803574948405176326327], [2761795691695947423, (-386931864663516872610)], [3362131887151924030]], [[(-46428481980399229), 5058099976587596159, (-172977864149823094403), (-14531838712062055292)], [(-38814895476602758), 5520751355548288967, (-193274858949995554997)], [(-47465603860034832), 6722736510291480266], [(-59399754084264328)]], [[1029092785945060, (-92793505433746450), 2521169243704796585, 438504627213370569, (-3620369094285070972)], [694633037954045, (-77580194549337771), 2754697893441242794, 190973814091679637], [657247613904532, (-94886030338946269), 3358314460476251587], [833040278194841, (-118773885794047738)], [1057712078219989]]], r := 600562281379631786, ok := true }, r1 := { p := [[[742242223479270661383479]], [[(-10677376854661609700841), 0], [(-12195342383860725992250)]], [[154390297185511503826, 0, 0], [171170892669403372621, 0], [212143420793668660569]], [[(-2850135742417255498), 0, 0, 0], [(-2387580614026112812), 0, 0], [(-2948801413948203514), 0], [(-3750663252744183506)]], [[63727181688560399, 0, 0, 0, 0], [42967465935751986, 0, 0, 0], [40536599544577318, 0, 0], [51824007556852414, 0], [66819585016191676]]], r := 53215744882613212, ok := true }, r2 := { p := [[[14816135335445670790023547742]], [[(-283530753487612603431237647), 210253067977777025940488], [(-525648911449042033672392245)]], [[6211917376317839074819711, (-2706936919349846351104), 443073362957853926], [9890394995917085487137774, (-3724232098550987703543)], [14120224490415067848679921]], [[(-153355178025506675896432), 48955628906122896776, (-2743147364303433), (-4703979391904059)], [(-214992738127625627095368), 45946177394358010792, (-2195203609557355)], [(-262852046226548271567365), 66982635308963316972], [(-338625980407975486700224)]], [[3978012823313945444567, (-1118002455459412554), (-4629249225382577), 82120985442580, (-473208483875796)], [5296344162323213590523, (-812091514250895528), (-4330503270799891), 286844973510535], [5685024008217652180051, (-812317620001058385), (-1599147561327659)], [6254722840661579932732, (-1211084991510438546)], [7632051416318714817304]]], r := 19922460452570974024358, ok := true }, r3 := { p := [[[463027126609673406319262737403]], [[(-25028466918304659577630666274), 6906199303793031233744276], [(-16838100502536231672186866104)]], [[1014667212369545347021077031, (-349973662449619156464612), 321818325031114514], [910167122821293070514620013, (-125693352223147539749962)], [459227753753557433026655850]], [[(-36564577752363946016538019), 13872724084076613693472, (-1577738586182976602), (-2493962404517441555)], [(-36898661064042794539239874), 6366355364935715315531, (-1514457500500181191)], [(-24823113843352763510524680), 2284480343413678708954], [(-11132877948319521780251172)]], [[1235287259961848546832237, (-495682110864470686847), (-69709294528911248), 248453732527578744, (-227044363048294808)], [1329680346495036433880596, (-252799997847427866936), (-333946813058603161), 165576980461938396], [1006339961237864922891002, (-117460258454314986371), (-369891789586883425)], [601775377705577428639339, (-41645116577817994284)], [253020545843651302198969]]], r := 8139760371421916019407814, ok := true }, eta := { p := [[[(-14821000703991528169207560805)]], [[283653269283631801204662103, 0], [525736065462288653630388767]], [[(-6215102789779081667777615), 0, 0], [(-9892580002990378449106542), 0], [(-14121799533449710399992746)]], [[153439969179766907857662, 0, 0, 0], [215049533791358773318727, 0, 0], [262891459299438741159101, 0], [338654510382285669913468]], [[(-3980290748206956071854), 0, 0, 0, 0], [(-5297859750371726842799), 0, 0, 0], [(-5686049355317596490780), 0, 0], [(-6255438030317206608705), 0], [(-7632569370230323949654)]]], r := 1354791921788703136610, 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 := 949978046398464, bh := 35184372088832, tc := 2305843009213693952, th := 2305843009213693952, sc := 2810246167479189504, sh := 72057594037927936 }
noncomputable def q6 : Cert := { V0 := [[[211383863866733376]], [[(-1731118260267674), 211343820695635873], [703761949299019]], [[7023849451229, (-1730134498656518), (-60051338584891)], [(-5897018692568), 703362014756704], [(-10689512492667)]], [[(-38957074696), 7011802145507, 1475093011822, (-19994754802506)], [27696888174, (-5887117594711), (-599678460581)], [89128663545, (-10684769237979)], [242815367881]], [[315104548, (-38847581591), (-18059731578), 490782303947, 16759137858], [(-195988310), 27572878003, 14842459349, (-199520690665)], [(-406299284), 89011737682, 7112976589], [(-2021194031), 242716348789], [(-6399936735)]]], r0 := 3812441300135, V1 := [[[1681085218342206917]], [[(-13605323615670886), 0], [5531054283447988]], [[53241838108208, 0, 0], [(-44752241261432), 0], [(-84335763237005)]], [[(-285285193074), 0, 0, 0], [191779417511, 0, 0], [684173607293, 0], [1917859530551]], [[2297565846, 0, 0, 0, 0], [(-1290931253), 0, 0, 0], [(-2898315679), 0, 0], [(-15566868342), 0], [(-50581852443)]]], r1 := 1413403165117, V2 := [[[18445681055912669907]], [[(-4172541660823), 6355533005], [(-39260326260057)]], [[3768117007, (-4134600), (-36498)], [(-156130613564), 472086830], [2415918978]], [[(-36455486), (-138149), 191, 0], [152219710, (-293544), (-4070)], [(-34933069), 8795412], [(-24301319)]], [[479534, 321, 0, 0, 0], [(-1472203), (-10400), 21, 0], [277007, (-4915), (-152)], [345540, 789], [409436]]], r2 := 1034358450, V3 := [[[18446454603279116124]], [[(-7422212249450), 3428048742], [(-10722021732453)]], [[2792771, 72684855, (-39141)], [(-274915744665), 254796498], [(-33267322)]], [[712, (-399026), (-654), 0], [207291, 5405899, (-4365)], [(-706852), 4753612], [(-3559)]], [[(-7), (-102), 8, 0, 0], [57, (-29620), (-73), 0], [3855, 100998, (-163)], [(-92), 522], [26]]], r3 := 2332409034, Vm := [[[18445681102402896130]], [[(-4172591816524), 0], [(-39256865955535)]], [[3767265452, 0, 0], [(-156134311916), 0], [2480672302]], [[(-36454430), 0, 0, 0], [152155775, 0, 0], [(-35000823), 0], [(-24291317)]], [[479526, 0, 0, 0, 0], [(-1472119), 0, 0, 0], [275788, 0, 0], [345552, 0], [409364]]], rm := 106047299 }
noncomputable def w6 : Wit := { Z0 := { p := [[[211403888807469678]], [[(-1731610278463015), 211403888807469678], [703961972424067]], [[7029875911947, (-1731610278463015), 0], [(-5901971539256), 703961972424067], [(-10691884596452)]], [[(-39011861033), 7029875911947, 0, 0], [27758940695, (-5901971539256), 0], [89187145972, (-10691884596452)], [242864886639]], [[315575913, (-39011861033), 0, 0, 0], [(-196579688), 27758940695, 0, 0], [(-407022779), 89187145972, 0], [(-2022413590), 242864886639], [(-6401176142)]]], r := 931206924005, ok := true }, Z1 := { p := [[[1691231110459757424]], [[(-13852882227704115), 0], [5631695779392539]], [[56239007295580, 0, 0], [(-47215772314041), 0], [(-85535076771609)]], [[(-312094888261), 0, 0, 0], [222071525562, 0, 0], [713497167777, 0], [1942919093115]], [[2524607310, 0, 0, 0, 0], [(-1572637500), 0, 0, 0], [(-3256182226), 0, 0], [(-16179308714), 0], [(-51209409135)]]], r := 359651015573, ok := true }, Z2 := { p := [[[38738872880242226365921]], [[(-138791118322783467462), 211403888807469678], [(-1305914962698284576681)]], [[648612746707069784, (-1731610278463015), 0], [4653823607146283123, 703961972424067], [46407511923808720726]], [[(-4159792906481868), 7029875911947, 0, 0], [(-21182658568534357), (-5901971539256), 0], [(-165047748264814993), (-10691884596452)], [(-1674285690945314781)]], [[38658585253897, (-39011861033), 0, 0, 0], [131156226301915, 27758940695, 0, 0], [743654613201566, 89187145972, 0], [5947342477663335, 242864886639], [60837431768284672]]], r := 4886133258923000, ok := true }, Z3 := { p := [[[127757611135923957853493]], [[(-3019025495572834821965), 1394377606904378162], [(-4361241081021314281700)]], [[74634634325183360210, (-39376010862895900), 0], [103805484724577947689, 4048726307362909], [155733732419137020238]], [[(-1869625536217301555), 966423609896423, 0, 0], [(-2573468367585572960), (-106193391888848), 0], [(-3717218699827973859), (-63220203923535)], [(-5635042864975510150)]], [[47130064061521560, (-24159326059078), 0, 0, 0], [64577107281763093, 2488293094622, 0, 0], [92259925417173704, 1681832922809, 0], [134734338206850626, 1449994214310], [205182924207577293]]], r := 166613927628256436, ok := true }, iE := { p := [[[38742651846531093531274]], [[(-138803683051320257312), 0], [(-1305902378972519447844)]], [[648672528042771129, 0, 0], [4653779339589309771, 0], [46407320800212639465]], [[(-4160182380202292), 0, 0, 0], [(-21182393557463183), 0, 0], [(-165047084018462236), 0], [(-1674281349595566973)]], [[38662251767208, 0, 0, 0, 0], [131154061497326, 0, 0, 0], [743650809478718, 0, 0], [5947327451268506, 0], [60837317343573824]]], r := 4885457692134309, ok := true }, iHu := { p := [[[127769376598588667145730]], [[(-3019297097580292650177), 0], [(-4361206918726988099731)]], [[74641355724314234067, 0, 0], [103804764774900920339, 0], [155733198980457831336]], [[(-1869793959734690493), 0, 0, 0], [(-2573451179006829470), 0, 0], [(-3717207258458395279), 0], [(-5635030630231701840)]], [[47134310323353945, 0, 0, 0, 0], [64576686404200968, 0, 0, 0], [92259650661013631, 0, 0], [134734074138353104, 0], [205182599867236952]]], r := 166611787848339892, ok := true }, T := { p := [[[2305843009213693952]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[8783145982595055]], [[31467464230143, 0], [296054366101963]], [[(-34318393654), 0, 0], [1066319612039, 0], [(-541629734969)]], [[293317303, 0, 0, 0], [(-1271061588), 0, 0], [(-1835977851), 0], [6686481066]], [[(-3760478), 0, 0, 0, 0], [10863604, 0, 0, 0], [(-369), 0, 0], [22666038, 0], [(-123823723)]]], r := 78748184, ok := true }, de := { p := [[[(-156425613144105933812)]], [[341195320369174898, 0], [492837684977697074]], [[(-4374264660429085), 0, 0], [99142803936, 0], [(-9126552192747103)]], [[74773754883732, 0, 0, 0], [19945, 0, 0], [28808, 0], [225346967736022]], [[(-1437956824687), 0, 0, 0, 0], [1, 0, 0, 0], [370, 0, 0], [1, 0], [(-6259637992668)]]], r := 1114385110589, ok := true }, dde := { p := [[[(-1696091137191954665460269)]], [[43489175140258023038035, 0], [62817697424817144337605]], [[(-1115107054947048526120), 0, 0], [(-1610710190578213840095), 0], [(-2326581386247545936170)]], [[28592488588385936505, 0, 0, 0], [41300261294335155687, 0, 0], [59655932980706291264, 0], [86169680972131351404]], [[(-733140733035463923), 0, 0, 0, 0], [(-1058981058829109402), 0, 0, 0], [(-1529639307197595767), 0, 0], [(-2209478999285418718), 0], [(-3191469665634419577)]]], r := 355532988018134939, ok := true }, nJu := { p := [[[(-312851226288211867623)]], [[682390640738349797, 0], [985675369955394149]], [[(-8748529320858170), 0, 0], [198285607872, 0], [(-18253104385494206)]], [[149547509767465, 0, 0, 0], [39890, 0, 0], [57617, 0], [450693935472044]], [[(-2875913649374), 0, 0, 0, 0], [2, 0, 0, 0], [741, 0, 0], [2, 0], [(-12519275985335)]]], r := 2228770221171, ok := true }, Jd1 := { p := [[[(-3392182274383909330920538)]], [[86978350280516046076070, 0], [125635394849634288675211]], [[(-2230214109894097052239), 0, 0], [(-3221420381156427680190), 0], [(-4653162772495091872339)]], [[57184977176771873011, 0, 0, 0], [82600522588670311375, 0, 0], [119311865961412582528, 0], [172339361944262702809]], [[(-1466281466070927845), 0, 0, 0, 0], [(-2117962117658218804), 0, 0, 0], [(-3059278614395191534), 0, 0], [(-4418957998570837435), 0], [(-6382939331268839153)]]], r := 711065976036269868, ok := true }, term0 := { p := [[[216202083761408876292861488139]], [[(-11087155875801540443876942800), 0], [(-16014368367682376700317412405)]], [[426427399485631347155129662, 0, 0], [821244827750576841289567284, 0], [889676005706408973525441104]], [[(-14578685919840710751835389), 0, 0, 0], [(-31586277578476390355324370), 0, 0], [(-45624231581247689243982673), 0], [(-43934342853859695084486143)]], [[467265024498300999280391, 0, 0, 0, 0], [1079871678744631367185813, 0, 0, 0], [1754775843281334929821825, 0, 0], [2253036594837858803987157, 0], [2033989723459534481898618]]], r := 410227326582271217321533, ok := true }, r0 := { p := [[[11675937314598032479559]], [[(-166588838139265035557), 23344933533520610415423], [(-389714162618862353432)]], [[2310871726102020246, (-332970426404232641389), 11658589218160009240893], [5413549854175218976, (-779242269166749727834)], [13797747543172558322]], [[(-39702769150693877), 4618109852367992914, (-166070926849745220589), (-13868266175829506068)], [(-72406808729358877), 10821625679574799645, (-389249116116594627641)], [(-189696087344152005), 27589435122993777322], [(-496676737693615336)]], [[824341072318896, (-79349489104798170), 2301792959449741747, 413859751305168354, (-3455469664882800679)], [1212494520913851, (-144720134964420265), 5399869031197747549, 371831158080546477], [2500497829849844, (-379214660726530472), 13782600446410263965], [6785519889876259, (-993146322965483735)], [18018726691256523]]], r := 1831222966718626187, ok := true }, r1 := { p := [[[733555541970088623586115]], [[(-10257048278197928600491), 0], [(-24572483691942384305199)]], [[140890833944626222964, 0, 0], [335696340539639842640, 0], [871015181996610070113]], [[(-2433842311001361066), 0, 0, 0], [(-4451889484366376210), 0, 0], [(-11790618636527516225), 0], [(-31375426130604518602)]], [[50984930529222497, 0, 0, 0, 0], [74906191349728887, 0, 0, 0], [154157139157896824, 0, 0], [422329597115311957, 0], [1138795366107722523]]], r := 902065565913703822, ok := true }, r2 := { p := [[[14793393271546524534289603976]], [[(-269741381850787740842787991), 208728582806186857431881], [(-1069860730679316573113129853)]], [[5570757187403494844663621, (-2567339377819413751334), 442586661318991763], [19182019315934959367372663, (-7539788293319940294971)], [58567663545571900119624683]], [[(-129774166101606365990283), 43603277434287133723, (-2844862706549071), (-26787470629112)], [(-392908914086470061698246), 88948498015458171219, (-1666778245591141)], [(-1038967656371563759632439), 276366462140533297177], [(-2861996067683034374936104)]], [[3184540671641179968494, (-936786598079633403), (-4778563568888126), (-485487944077148), (-7070582309338)], [9131542215874873037088, (-1474291950549075391), (-4145666059063942), (-29275272923096)], [21169610443452333052101, (-3205864828244338076), (-1457250955569965)], [50379208480121181334401, (-10174312064487652741)], [131429428220546717578863]]], r := 266925364580059861940134, ok := true }, r3 := { p := [[[432333890415799656658094432972]], [[(-22170944556983603162687177294), 6374049815439927653614979], [(-32026132224763408409339957923)]], [[852728319481455128480503841, (-305478178828232694831345), 1479373620166113157], [1642364877753602914352694577, (-236314699814160864723684)], [1779255522633398927127259448]], [[(-29153100297558284798115974), 11474922773940744063881, (-1186081872489929590), (-2192473962187357808)], [(-63167868774354191709498865), 11322894239825072595773, (-1011339346647319711)], [(-91243841867021447924781978), 8753865415927825863339], [(-87865112794218669729015070)]], [[934392424056173569516317, (-388850408582582486454), (-89985503913665027), 206950015684731849, (-199950263733188181)], [2159584908345799497269674, (-426969276541445501725), (-569283912274000117), 301010050272059493], [3509376278810757301543942, (-419741443513873427553), (-969964395715996935)], [4505900857942574881128706, (-324882859808102283118)], [4067846761365364866970628]]], r := 43853377943382760305797593, ok := true }, eta := { p := [[[(-14798110233832731272376583241)]], [[269854116325800990972688219, 0], [1070032897590623180345342831]], [[(-5573533443453571452006650), 0, 0], [(-19186115272704970570293487), 0], [(-58574002236858111746900489)]], [[129844206139414494727407, 0, 0, 0], [393009748178996997833114, 0, 0], [1039118179067830201028133, 0], [2862229974211233464275434]], [[(-3186328199668403950149), 0, 0, 0, 0], [(-9134087710795612056222), 0, 0, 0], [(-21173316917887403656128), 0, 0], [(-50384758851165232102660), 0], [(-131438071902514960236616)]]], r := 20659555174786958926813, 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 844424930131968 985162418487296 0 4611686018427387904 2594073385365405696 2882303761517117440 :=
  (RegionPosI.split_b 914793674309632 (RegionPosI.split_s 2738188573441261568 (RegionPosI.split_b 879609302220800 (RegionPosI.of_check c0 q0 ok_0 844424930131968 879609302220800 0 4611686018427387904 2594073385365405696 2738188573441261568 (by decide +kernel)) (RegionPosI.of_check c1 q1 ok_1 879609302220800 914793674309632 0 4611686018427387904 2594073385365405696 2738188573441261568 (by decide +kernel))) (RegionPosI.split_b 879609302220800 (RegionPosI.of_check c2 q2 ok_2 844424930131968 879609302220800 0 4611686018427387904 2738188573441261568 2882303761517117440 (by decide +kernel)) (RegionPosI.of_check c3 q3 ok_3 879609302220800 914793674309632 0 4611686018427387904 2738188573441261568 2882303761517117440 (by decide +kernel)))) (RegionPosI.split_s 2738188573441261568 (RegionPosI.split_b 949978046398464 (RegionPosI.of_check c4 q4 ok_4 914793674309632 949978046398464 0 4611686018427387904 2594073385365405696 2738188573441261568 (by decide +kernel)) (RegionPosI.of_check c5 q5 ok_5 949978046398464 985162418487296 0 4611686018427387904 2594073385365405696 2738188573441261568 (by decide +kernel))) (RegionPosI.of_check c6 q6 ok_6 914793674309632 985162418487296 0 4611686018427387904 2738188573441261568 2882303761517117440 (by decide +kernel))))

end CKLaneC.RSC2.S00_0001