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

import Definitions.Def_CK_CKLaneC_RSCell_Staged
import Definitions.Def_CK_CKLaneC_RSCell_RegionI

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

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

namespace CKLaneC.RSC2.BD_0170
open CKLaneC.TM3 CKLaneC.RSCell

noncomputable def c0 : Cell := { bc := 8791026472627208192, bh := 144115188075855872, tc := 13258597302978740224, th := 576460752303423488, sc := 14663720386718334976, sh := 252201579132747776 }
noncomputable def q0 : Cert := { V0 := [[[1320297514541224540]], [[(-90485728407855648), 56980830917888738], [17806722863338563]], [[233257583085175, (-3847223183374954), (-27373664680423)], [(-1078350480277211), 757096596614470], [144865121686313]], [[(-4953807477753), 3978934734402, 5587866987623, (-379494230092)], [(-5361218179351), (-43511408577238), (-1099638590491)], [(-6392752911395), 5929316387574], [1986878117429]], [[30254395421, (-46138000774), (-390494517937), 75114800543, 549456005], [(-117243673652), (-454546764434), 214614355576, (-14781871792)], [(-164745436673), (-209381313755), (-23510650173)], [(-77417137927), 79714828149], [19911745070]]], r0 := 607462676032, V1 := [[[1830634924846842087]], [[(-124604656169032132), 0], [24521000371268677]], [[234078904012062, 0, 0], [(-1450664440848824), 0], [196114266417259]], [[(-4488090070492), 0, 0, 0], [(-10660398575557), 0, 0], [(-7896625459404), 0], [2666794959788]], [[22278469192, 0, 0, 0, 0], [(-95618042575), 0, 0, 0], [(-285136143080), 0, 0], [(-91024905625), 0], [26100874975]]], r1 := 218588969124, V2 := [[[2187053599649284314]], [[(-90778539751836022), 55881452027997369], [(-270833416962278940)]], [[242451972170570, (-3715540712392409), (-43926651318764)], [(-1009512689919949), 1185055206297125], [51197530928024]], [[(-4853085738099), (-192693603572), 7706217085442, (-336621331253)], [(-7652102834129), (-89999467966160), 3700704108589], [3300009253135, (-13347403232080)], [2347201642450]], [[28332611084, (-21754947461), (-449506272140), 64321379934, 831536663], [(-157223121808), 834661548752, (-390441736419), (-29841547919)], [(-422742132810), 582188511706, 212622977109], [(-113579766059), (-329814176949)], [(-7830076589)]]], r2 := 1986781097604, V3 := [[[3515599886758569459]], [[(-182847877290815711), 108689718461451165], [(-252479080957189209)]], [[571205981912384, (-6858396537286247), (-272070213171115)], [(-2187446111464201), 2542704773882193], [112346712877967]], [[(-11251426018594), (-37202833749932), 49346797662153, (-2066291077943)], [(-5269628609745), (-197276349995862), 7997924949524], [4963961664272, (-18985179554216)], [4902205758095]], [[29589178116, 899967649758, (-2909161781009), 319003734263, 18480353153], [(-542967430251), 1637498438231, (-138527884939), (-244642492956)], [(-742751861266), 167221096543, 771765660708], [(-235676495168), (-615416693212)], [(-5743938116)]]], r3 := 8853152041396, Vm := [[[3226851196011610981]], [[(-168139758310734339), 0], [(-198513402469262780)]], [[234699276490440, 0, 0], [(-4343765438813103), 0], [4426501772928367]], [[6861600776993, 0, 0, 0], [(-74744790213985), 0, 0], [101572487187562, 0], [273851413650306]], [[440676143854, 0, 0, 0, 0], [(-3074492375532), 0, 0, 0], [(-1482955382206), 0, 0], [26315368276377, 0], [13829408329024]]], rm := 169731476966887 }
noncomputable def w0 : Wit := { Z0 := { p := [[[1325198699722383213]], [[(-91496498412673698), 57617334770538400], [18005632698856978]], [[305663912053267, (-3978108626637987), 0], [(-1117868410840039), 782853595602477], [149186471440866]], [[(-7012193080898), 13289735306663, 0, 0], [(-2716521011854), (-48602974384350), 0], [(-7205960926027), 6486368323515], [2065577449648]], [[53937947553, (-304877960040), 0, 0, 0], [(-181815930067), (-118109609212), 0, 0], [(-115767130085), (-313302648958), 0], [(-91410075419), 89807715202], [21225736727]]], r := 73835705894, ok := true }, Z1 := { p := [[[1843754712657228818]], [[(-127299476052415580), 0], [25051315059279274]], [[425271529813241, 0, 0], [(-1555295180299184), 0], [207563786352509]], [[(-9756094721249), 0, 0, 0], [(-3779507494753), 0, 0], [(-10025684766645), 0], [2873846886467]], [[75044100943, 0, 0, 0, 0], [(-252961294006), 0, 0, 0], [(-161067311422), 0, 0], [(-127179235365), 0], [29531459794]]], r := 43488353934, ok := true }, Z2 := { p := [[[2209510093521447526]], [[(-93598453960030482), 57617334770538400], [(-279246495677067789)]], [[369504524210165, (-3978108626637987), 0], [(-327700892285707), 782853595602477], [1116643584703166]], [[(-7435422057116), 13289735306663, 0, 0], [(-23185547746891), (-48602974384350), 0], [(-36683703266924), 6486368323515], [(-45600286169756)]], [[61715731355, (-304877960040), 0, 0, 0], [(-31278410768), (-118109609212), 0, 0], [(-354823905817), (-313302648958), 0], [(-186703508182), 89807715202], [357340820689]]], r := 114255761020, ok := true }, Z3 := { p := [[[3610784186599217205]], [[(-198030694863337575), 117714795437238753], [(-273443742313110393)]], [[1452560267304598, (-8419299130583870), 0], [(-66091625519214), 1384879636479581], [1711676674799678]], [[(-35074032255615), 56889037127186, 0, 0], [(-66179273278527), (-75268394898187), 0], [(-69215237109016), 8128997751269], [(-42647387244150)]], [[446459580528, (-1456657744610), 0, 0, 0], [124512355200, (-798905342024), 0, 0], [(-486097434433), (-79741932512), 0], [(-41500237427), 102426896846], [496041564860]]], r := 347333975004, ok := true }, iE := { p := [[[18865309734380038694]], [[(-44841718343611383), 0], [(-52942160559715463)]], [[1361933059347160, 0, 0], [1909667614621959, 0], [2991698229690583]], [[(-9028884825992), 0, 0, 0], [17305116101595, 0, 0], [7697368268184, 0], [(-19639013983758)]], [[165926054446, 0, 0, 0, 0], [201838803056, 0, 0, 0], [668494151582, 0, 0], [532862857107, 0], [624117129956]]], r := 186089323421, ok := true }, iHu := { p := [[[19271336352911485288]], [[(-93585383678049563), 0], [(-89201993341841151)]], [[3074398152092017, 0, 0], [4326609859617227, 0], [2793143051823300]], [[(-33512621431423), 0, 0, 0], [4971108574998, 0, 0], [4738269765863, 0], [(-29020707986589)]], [[707596420945, 0, 0, 0, 0], [1049653216024, 0, 0, 0], [1541480488048, 0, 0], [953627813356, 0], [584052334748]]], r := 408406954105, ok := true }, T := { p := [[[13258597302978740224]], [[0, 576460752303423488], [0]]], r := 0, ok := true }, E := { p := [[[18037465152284762841]], [[42873981046674765, 0], [50618960919695402]], [[(-1200260024042419), 0, 0], [(-1585231363568632), 0], [(-2718363818557507)]], [[2684556045746, 0, 0, 0], [(-31676340526320), 0, 0], [(-30192671180824), 0], [3121354574736]], [[(-45094795017), 0, 0, 0, 0], [(-39903160019), 0, 0, 0], [(-316693374787), 0, 0], [(-36252700087), 0], [(-104191717506)]]], r := 123430483254, ok := true }, de := { p := [[[(-6580302627341633076)]], [[368432041853133470, 0], [351175271742916446]], [[(-1236077740145004), 0, 0], [3683505884060659, 0], [(-1122997666730360)]], [[27684613454705, 0, 0, 0], [38636591724039, 0, 0], [36826915296684, 0], [23973865620589]], [[(-250816868959), 0, 0, 0, 0], [405262341649, 0, 0, 0], [896114123210, 0, 0], [368187735532, 0], [(-207025040792)]]], r := 115527559488, ok := true }, dde := { p := [[[(-56546984297159145261)]], [[379426654698562021, 0], [361654914431650453]], [[(-12747111199303556), 0, 0], [(-18080004527735748), 0], [(-11580967498606556)]], [[153981586174100, 0, 0, 0], [22369929574516, 0, 0], [21322157697488, 0], [133342438066646]], [[(-3332809504115), 0, 0, 0, 0], [(-5133959164055), 0, 0, 0], [(-7156878960533), 0, 0], [(-4664289287863), 0], [(-2750911557116)]]], r := 3853027955407, ok := true }, nJu := { p := [[[(-13160605254683266151)]], [[736864083706266940, 0], [702350543485832892]], [[(-2472155480290008), 0, 0], [7367011768121318, 0], [(-2245995333460719)]], [[55369226909410, 0, 0, 0], [77273183448079, 0, 0], [73653830593369, 0], [47947731241179]], [[(-501633737917), 0, 0, 0, 0], [810524683298, 0, 0, 0], [1792228246421, 0, 0], [736375471064, 0], [(-414050081583)]]], r := 231055118968, ok := true }, Jd1 := { p := [[[(-113093968594318290521)]], [[758853309397124042, 0], [723309828863300907]], [[(-25494222398607112), 0, 0], [(-36160009055471496), 0], [(-23161934997213111)]], [[307963172348201, 0, 0, 0], [44739859149032, 0, 0], [42644315394977, 0], [266684876133293]], [[(-6665619008230), 0, 0, 0, 0], [(-10267918328109), 0, 0, 0], [(-14313757921065), 0, 0], [(-9328578575725), 0], [(-5501823114232)]]], r := 7706055910804, ok := true }, term0 := { p := [[[359085844549387779548]], [[(-4745495008441055752), 0], [(-4068267028641325398)]], [[177076254375684811, 0, 0], [229200384390241746, 0], [131739418418169714]], [[(-3005539487396987), 0, 0, 0], [(-2234614605359884), 0, 0], [(-2103125855829789), 0], [(-2099459122900873)]], [[73076095386197, 0, 0, 0, 0], [114814895056220, 0, 0, 0], [136605296662958, 0, 0], [92576072145857, 0], [46474816644530]]], r := 40413321057534, ok := true }, r0 := { p := [[[60444849097073155693]], [[(-677883407241755341), 5194257977061901455], [(-332471197577957931)]], [[24841654969325771, (-49896662945825640), 107613635952968923], [14844772341810866, (-30215001713293832)], [8397236201782605]], [[(-320832969205589), 1748764940182223, (-317626452453600), (-224620792829829)], [140784632639902, 1454277525481654, (-766915039793677)], [(-65218211626296), 706820872228033], [(-104083095550981)]], [[7088118541347, (-20032316537916), 4454260804433, 31658537152619, (-2120475404425)], [4831161045940, 7145655885619, 44923864104328, (-4498869172427)], [8223517416937, (-3114960488962), 13427060362832], [3111952075448, (-9386206816476)], [1762160193750]]], r := 47765780281926, ok := true }, r1 := { p := [[[115732707008732454840]], [[(-1128061649816834028), 0], [(-670005710215951110)]], [[39998978853402873, 0, 0], [31943133483690926, 0], [15788369429391714]], [[(-483653806654166), 0, 0, 0], [186186445097417, 0, 0], [(-78088657568087), 0], [(-208015627704780)]], [[10499730484920, 0, 0, 0, 0], [9351405754607, 0, 0, 0], [15278047647863, 0, 0], [6528631996881, 0], [3315660100969]]], r := 20557577548640, ok := true }, r2 := { p := [[[63395809169755297237]], [[(-860753513444314563), 5209022919967105745], [(-1495493709897175700)]], [[27036391948446336, (-50719771439560125), 101963782644019105], [76910347995914320, (-33009782859743568)], [70294312655733323]], [[(-376720147807479), 1710694091525558, 63812616396975, (-279791555778899)], [(-674627901996006), 1632320112215332, 1225290510762696], [(-524167933506118), (-18249144271061)], [(-866437756062374)]], [[7863238546817, (-19012802399984), 539151703915, 33657604343395, (-1666761465401)], [23611341925036, 21843632846656, (-77437887615948), 11445943842971], [35999050218366, 29146993328955, (-22075221113401)], [33500434485189, (-4299730438662)], [22700412280464]]], r := 208174892034947, ok := true }, r3 := { p := [[[266145305157517432247]], [[(-5321343543268926303), 21028059325308832162], [(-5707826789787941605)]], [[192730817065634800, (-231843394007669446), 342430278721058538], [319823717803033687, (-102899745375829286)], [208113242614150382]], [[(-3247825652750870), 7893211762433326, 8615630378605733, (-3438146803434965)], [(-3359856459162643), 3933380515891045, 6336897656652580], [(-2836210712661509), 630769094779776], [(-3105975606072789)]], [[76543780555121, (-77039085537468), (-295833432060704), 379861218773708, (-7379065095327)], [143997674484649, 120077233125241, (-240187320913164), (-15882594545165)], [183982436223709, 27016264493340, (-557258982228)], [139851258920254, (-34649831483111)], [73598942877428]]], r := 3477113061311439, ok := true }, eta := { p := [[[(-233089893643841098182)]], [[2315746140788842496, 0], [2269759409590409956]], [[(-79824349967916243), 0, 0], [(-115427695492523428), 0], [(-84146950954436346)]], [[1067500532945422, 0, 0, 0], [480029498061962, 0, 0], [684639913288737, 0], [1176435844632958]], [[(-23458287725103), 0, 0, 0, 0], [(-37674598528998), 0, 0, 0], [(-57381579445151), 0, 0], [(-45503256265648), 0], [(-28580645015490)]]], r := 64273992990842422, 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 := 9079256848778919936, bh := 144115188075855872, tc := 13258597302978740224, th := 576460752303423488, sc := 14663720386718334976, sh := 252201579132747776 }
noncomputable def q1 : Cert := { V0 := [[[1356506643566938038]], [[(-92668626915402022), 58519391522455600], [18410686160659539]], [[221856320391014, (-3935101169778510), (-29670461233217)], [(-1104864987356830), 781795469068237], [157287519179269]], [[(-5200354416372), 3023926397890, 6034838090932, (-410301676309)], [(-6050258126336), (-44375407607870), (-1198954962655)], [(-6868239776515), 6426597127564], [2157921903045]], [[29264909298, (-46567414737), (-418902399784), 80771607546, 627769374], [(-129574255454), (-501152053893), 232659658232, (-16047078357)], [(-180069500207), (-222625711123), (-26207089585)], [(-81156375707), 86193887530], [22913693077]]], r0 := 645142755764, V1 := [[[1880483146601014522]], [[(-127538305579419206), 0], [25338324259714688]], [[211583482024007, 0, 0], [(-1483354964408646), 0], [212771701082611]], [[(-4693396062240), 0, 0, 0], [(-11852549951554), 0, 0], [(-8451650822732), 0], [2890883281193]], [[20723334223, 0, 0, 0, 0], [(-110062689936), 0, 0, 0], [(-311431923948), 0, 0], [(-94038636374), 0], [30002530496]]], r1 := 234288408592, V2 := [[[1645610199181155286]], [[(-92785273485310564), 58195556403995162], [(-270600733480476071)]], [[225436370279609, (-3893033234975801), (-35669688986511)], [(-997674851942534), 1127752558175367], [65070318522961]], [[(-5171343075493), 1565596612356, 6809243600592, (-396711339303)], [(-9373356936350), (-87404676420275), 4558122870560], [2619429317691, (-15292045719809)], [2273310362291]], [[28634735688, (-38208500739), (-441221445900), 77207201424, 742258797], [(-161016516351), 923177458837, (-507181083887), (-30084967640)], [(-437527113721), 714734556073, 215415392465], [(-113059149979), (-317942047465)], [(-10642534506)]]], r2 := 1914030078736, V3 := [[[3011130222759837762]], [[(-187204814330156067), 113694304781195537], [(-251971088120536937)]], [[557643963280798, (-7251963144748765), (-252939630302274)], [(-2170448521661192), 2459461932297301], [141585445494242]], [[(-12359710814572), (-33615170705776), 48685103100460, (-2573336609934)], [(-8317528120900), (-196131926340965), 11154373135977], [3527754544311, (-22613991435206)], [4837957695774]], [[34050837386, 931460905234, (-3089922720065), 422187876128, 19250766082], [(-565048796916), 1949900600045, (-528277947104), (-261529579673)], [(-780453797031), 404666417345, 804317230105], [(-242753326841), (-593173319637)], [(-10303215331)]]], r3 := 8719768611112, Vm := [[[2849957306615935488]], [[(-176164211276278732), 0], [(-177041940943922849)]], [[96458832075737, 0, 0], [(-3526523798875560), 0], [6437551924062775]], [[103616322093, 0, 0, 0], [(-51838341740341), 0, 0], [334125058360127, 0], [401822423312309]], [[114913706931, 0, 0, 0, 0], [(-2952115471760), 0, 0, 0], [16254395409645, 0, 0], [53360257900128, 0], [17714265056514]]], rm := 363210204743245 }
noncomputable def w1 : Wit := { Z0 := { p := [[[1361823585127004887]], [[(-93761801189925563), 59209721092478473], [18627869571670182]], [[299754120196678, (-4076600051735895), 0], [(-1147810987295468), 809907372681312], [162114354048762]], [[(-7391565622118), 13032787834638, 0, 0], [(-3200315748484), (-49904825534586), 0], [(-7770967829436), 7048450176033], [2248023835702]], [[54065531862, (-321372418353), 0, 0, 0], [(-197865167571), (-139144162978), 0, 0], [(-126336980377), (-337868166498), 0], [(-97051536916), 97740166769], [24457507278]]], r := 76702134540, ok := true }, Z1 := { p := [[[1894711074959311148]], [[(-130451201655548609), 0], [25917035925801993]], [[417049210708422, 0, 0], [(-1596954417106738), 0], [225550405633061]], [[(-10283917387294), 0, 0, 0], [(-4452613215282), 0, 0], [(-10811781327910), 0], [3127685336629]], [[75221609547, 0, 0, 0, 0], [(-275290667925), 0, 0, 0], [(-175773190089), 0, 0], [(-135028225274), 0], [34027836213]]], r := 46099030892, ok := true }, Z2 := { p := [[[1655124286677773537]], [[(-94402227661791444), 59209721092478473], [(-275316449344904887)]], [[321618113797974, (-4076600051735895), 0], [(-476963788450999), 809907372681312], [850863003117151]], [[(-7525913350979), 13032787834638, 0, 0], [(-24750271551759), (-49904825534586), 0], [(-38020548331025), 7048450176033], [(-43115464257378)]], [[56753299019, (-321372418353), 0, 0, 0], [(-59927492873), (-139144162978), 0, 0], [(-428968131420), (-337868166498), 0], [(-259539303478), 97740166769], [265615628117]]], r := 112410568594, ok := true }, Z3 := { p := [[[3070409877700369340]], [[(-198440294149438018), 120517901019930950], [(-267093648326857283)]], [[1318031631171349, (-8570158440501254), 0], [(-343896261312444), 1418646718510127], [1466985814067488]], [[(-34934952174398), 55206118223548, 0, 0], [(-68464208506185), (-75592345598302), 0], [(-69797938720322), 8760237683748], [(-39030013206775)]], [[416753402003, (-1497611691987), 0, 0, 0], [12701532269, (-884782515592), 0, 0], [(-658424166673), (-81884666407), 0], [(-152400906178), 108122241979], [410650768589]]], r := 348656431660, ok := true }, iE := { p := [[[18771244899249193562]], [[(-40987294199416364), 0], [(-41191511411610870)]], [[1399295590482924, 0, 0], [1946926526629705, 0], [2888402128766051]], [[(-8598254647119), 0, 0, 0], [20098419073373, 0, 0], [10953374527974, 0], [(-14861109191091)]], [[172017098096, 0, 0, 0, 0], [229756533571, 0, 0, 0], [730025406632, 0, 0], [554157468043, 0], [573010542578]]], r := 193967523450, ok := true }, iHu := { p := [[[19103881871485278390]], [[(-84905601146188135), 0], [(-78359591080495627)]], [[3090618369902764, 0, 0], [4356970850515955, 0], [2632431149346328]], [[(-31352528557679), 0, 0, 0], [11308888457403, 0, 0], [10437001365449, 0], [(-24645636080962)]], [[706044171022, 0, 0, 0, 0], [1113462155809, 0, 0, 0], [1631178584407, 0, 0], [948390293383, 0], [512218371374]]], r := 425600778493, ok := true }, T := { p := [[[13258597302978740224]], [[0, 576460752303423488], [0]]], r := 0, ok := true }, E := { p := [[[18127852933960121748]], [[39582438213125404, 0], [39779655798273067]], [[(-1264905325282472), 0, 0], [(-1706475889542075), 0], [(-2702108737640122)]], [[2590947912022, 0, 0, 0], [(-32982147740084), 0, 0], [(-30439306417719), 0], [2301201475567]], [[(-48040947182), 0, 0, 0, 0], [(-53969967935), 0, 0, 0], [(-336476604342), 0, 0], [(-45968866976), 0], [(-101043614871)]]], r := 133442348935, ok := true }, de := { p := [[[(-5882255489195887616)]], [[375949366883048262, 0], [346964608438550211]], [[(-1155104505865267), 0, 0], [3835352608632677, 0], [(-983859123986794)]], [[28557020539695, 0, 0, 0], [42396052147061, 0, 0], [39127422276313, 0], [22448139533087]], [[(-241415386234), 0, 0, 0, 0], [468646672437, 0, 0, 0], [985249378769, 0, 0], [399169341182, 0], [(-175141161187)]]], r := 126909721931, ok := true }, dde := { p := [[[(-55868974394665421456)]], [[343314870278395190, 0], [316846150120877193]], [[(-12731380259111975), 0, 0], [(-18050202809452115), 0], [(-10843940583098806)]], [[143504750587195, 0, 0, 0], [(-6848125080745), 0, 0], [(-6320151718513), 0], [112806399405863]], [[(-3302304166610), 0, 0, 0, 0], [(-5357259457869), 0, 0, 0], [(-7470692373724), 0, 0], [(-4563040461209), 0], [(-2395743682099)]]], r := 3998034174951, ok := true }, nJu := { p := [[[(-11764510978391775232)]], [[751898733766096524, 0], [693929216877100422]], [[(-2310209011730533), 0, 0], [7670705217265355, 0], [(-1967718247973588)]], [[57114041079390, 0, 0, 0], [84792104294123, 0, 0], [78254844552627, 0], [44896279066174]], [[(-482830772468), 0, 0, 0, 0], [937293344874, 0, 0, 0], [1970498757539, 0, 0], [798338682365, 0], [(-350282322373)]]], r := 253819443855, ok := true }, Jd1 := { p := [[[(-111737948789330842911)]], [[686629740556790380, 0], [633692300241754386]], [[(-25462760518223950), 0, 0], [(-36100405618904230), 0], [(-21687881166197611)]], [[287009501174391, 0, 0, 0], [(-13696250161490), 0, 0], [(-12640303437026), 0], [225612798811726]], [[(-6604608333219), 0, 0, 0, 0], [(-10714518915738), 0, 0, 0], [(-14941384747448), 0, 0], [(-9126080922418), 0], [(-4791487364197)]]], r := 7996068349896, ok := true }, term0 := { p := [[[351460191102323207083]], [[(-4294782470271578898), 0], [(-3565077668521528967)]], [[173149356578758901, 0, 0], [221866588611968336, 0], [120196758964038888]], [[(-2777657749992758), 0, 0, 0], [(-1693890756772263), 0, 0], [(-1571246662239566), 0], [(-1757738423815557)]], [[70698319812329, 0, 0, 0, 0], [113385335536201, 0, 0, 0], [134192186921782, 0, 0], [85095372486240, 0], [39234720400112]]], r := 38913950173208, ok := true }, r0 := { p := [[[59812690316253767338]], [[(-648430237297496925), 5136582462363422685], [(-300076998682802375)]], [[25156602774759796, (-46998197775519206), 106131708403610122], [14620457118534188, (-27495800284693280)], [7812910545334016]], [[(-310783707983236), 1765747078269787, (-227186926307957), (-233932240201770)], [174420853547756, 1445359162982795, (-715894544532359)], [(-47124455700353), 653871762330069], [(-91029715258392)]], [[7211989461084, (-19066999252703), 4113352900884, 32690849050542, (-2189819841233)], [5234138104623, 9858716989113, 45549698499663, (-4816823511778)], [8610118411447, (-1357267772514), 12103571448367], [2926771373578, (-8293773205150)], [1508788825852]]], r := 49867368019348, ok := true }, r1 := { p := [[[114454236287820983427]], [[(-1064436184710305382), 0], [(-609246554041946341)]], [[40433461336151180, 0, 0], [31707788251005108, 0], [14615652273749779]], [[(-464246487139571), 0, 0, 0], [248826258213120, 0, 0], [(-39894764268331), 0], [(-183560516776056)]], [[10649467583019, 0, 0, 0, 0], [10086100594777, 0, 0, 0], [16073571787784, 0, 0], [6217587595647, 0], [2812491851880]]], r := 21829100244631, ok := true }, r2 := { p := [[[60679419259657100120]], [[(-708765339419314377), 5142899786370604834], [(-1224015668016304015)]], [[25831933933158571, (-47336512554520348), 104322101022407886], [75208169380047138, (-33126771811092061)], [65612490546095409]], [[(-329371124746583), 1754473677268247, (-96961169405129), (-253951041546788)], [(-529280498156223), 1751871993116945, 1131076409771634], [(-328556894512877), (-38404741914195)], [(-698538772544566)]], [[7456543288018, (-18731416249828), 2752867076262, 33505005655004, (-2039548248656)], [23812381099383, 21879608450063, (-83194047970511), 14390037682112], [36823630954874, 30547198386221, (-25001405526447)], [31863321621478, (-2458785238641)], [19420308682089]]], r := 189876564456190, ok := true }, r3 := { p := [[[255538393019192403701]], [[(-4691949817746141092), 20824522125313868956], [(-4910392819634614176)]], [[186738914893501325, (-223845489470337520), 355085005455776871], [310102564256538014, (-100759827365535185)], [191142504699568995]], [[(-2963125469889896), 8152174060484324, 8080992514491621, (-3450689889248324)], [(-2635356500077778), 4075743356076273, 6309319063842763], [(-2036972107728174), 447118208064683], [(-2566829129373064)]], [[73459379076213, (-73307016423236), (-316396707781325), 411386431049325, (-12904015856142)], [141197914113043, 138483272406265, (-294245202525424), 3625326661620], [179012700628833, 43844361825977, (-13317783988159)], [127234852765405, (-26720113503943)], [61668222483340]]], r := 3231510084977595, ok := true }, eta := { p := [[[(-228877994446500796665)]], [[2087270383864278462, 0], [1946408930168489474]], [[(-79094801150572826), 0, 0], [(-113225195499557311), 0], [(-77740012758758447)]], [[991544416917214, 0, 0, 0], [248839782439110, 0, 0], [418829194295757, 0], [964577479098743]], [[(-23131025259875), 0, 0, 0, 0], [(-38400063816637), 0, 0, 0], [(-58401344162339), 0, 0], [(-43282247288592), 0], [(-24551390873267)]]], r := 134865442031792766, 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 := 8791026472627208192, bh := 144115188075855872, tc := 13258597302978740224, th := 576460752303423488, sc := 15168123544983830528, sh := 252201579132747776 }
noncomputable def q2 : Cert := { V0 := [[[1140219927340791105]], [[(-89611211317333238), 49301925912114802], [15627632045175261]], [[204225338538074, (-3831871515984322), (-17679380621082)], [(-1101216516201015), 668254308985194], [131396976918349]], [[(-4729370560279), 3694458763153, 4146112356163, (-247917838812)], [(-6075570095231), (-45331856371478), (-723055936503)], [(-7087519156296), 5465440881230], [1821883124475]], [[25930546651, (-48579950977), (-330943014505), 56839046407, 266409437], [(-121014386761), (-456009139628), 163083902339, (-9912372460)], [(-182939834059), (-254774639112), (-15857096988)], [(-87848484610), 74635733597], [18887270840]]], r0 := 562129252556, V1 := [[[1582326369936122333]], [[(-123721509447237465), 0], [21576253655005730]], [[207660448326908, 0, 0], [(-1494476130646143), 0], [179153145893665]], [[(-4322057984267), 0, 0, 0], [(-11251225662212), 0, 0], [(-9078476561043), 0], [2467466015602]], [[19280370900, 0, 0, 0, 0], [(-101398057283), 0, 0, 0], [(-306111196988), 0, 0], [(-108671421636), 0], [25144141799]]], r1 := 212367009680, V2 := [[[2006427943143748798]], [[(-89866095950086957), 48449413956783211], [(-272884305362034612)]], [[213979908829361, (-3716596043897312), (-30237821230477)], [(-1042001729591380), 1008333530151085], [56098221266788]], [[(-4643050744024), (-340639841690), 6019392447580, (-222882633807)], [(-8591282878195), (-86752336883716), 2932607840689], [1596168005055, (-12094842787171)], [2109501878307]], [[24244739958, (-27424810731), (-394330637754), 49632372859, 432418144], [(-156087614041), 789467424110, (-375496567738), (-18957206675)], [(-429514558285), 669613877453, 159253534039], [(-124117476024), (-285541454164)], [(-7693084787)]]], r2 := 1875124662212, V3 := [[[3152099409004505333]], [[(-180697146497291376), 94831131370101592], [(-256879361580454664)]], [[504384573781312, (-6996770629526135), (-184598969303646)], [(-2214973238205967), 2154832950314877], [119258073866794]], [[(-11026304516934), (-32071718867019), 38334530468722, (-1461719312190)], [(-8478072284793), (-190532634175361), 7382876681694], [1924697924201, (-18342733404585)], [4404744960289]], [[26644393057, 812450800290, (-2594117089943), 282031896360, 9714413622], [(-527103884291), 1731865753381, (-457100002418), (-158655443459)], [(-776817848550), 472915039950, 592665148726], [(-261550152121), (-536049962201)], [(-7378901590)]]], r3 := 7943651326976, Vm := [[[2891573194605783670]], [[(-167102540581438919), 0], [(-207526483364484185)]], [[288492629587347, 0, 0], [(-4683651553651015), 0], [4620103866803325]], [[11470149927423, 0, 0, 0], [(-96281190986803), 0, 0], [89881926946153, 0], [332945088743994]], [[743482991741, 0, 0, 0, 0], [(-4157932798669), 0, 0, 0], [(-4729169056832), 0, 0], [33003996122957, 0], [20220896533676]]], rm := 259108287261671 }
noncomputable def w2 : Wit := { Z0 := { p := [[[1143373096021507511]], [[(-90356332745349269), 49711873740065543], [15757576539115584]], [[264816012978782, (-3928536206319534), 0], [(-1130914157807565), 685112023439808], [134280657382432]], [[(-6614964243796), 11513739694729, 0, 0], [(-3806342100282), (-49170180774242), 0], [(-7715545831133), 5838289451410], [1875520035533]], [[45541145158, (-287607141035), 0, 0, 0], [(-181804045235), (-165493134795), 0, 0], [(-139312531968), (-335458514398), 0], [(-98954829248), 81544349371], [19801577064]]], r := 72580685604, ok := true }, Z1 := { p := [[[1590779959682097406]], [[(-125713158602225069), 0], [21923584750073857]], [[368439670231349, 0, 0], [(-1573445784775742), 0], [186825262445123]], [[(-9203428513107), 0, 0, 0], [(-5295780313436), 0, 0], [(-10734672460707), 0], [2609419179872]], [[63361593263, 0, 0, 0, 0], [(-252944758587), 0, 0, 0], [(-193826131434), 0, 0], [(-137676284170), 0], [27550020263]]], r := 42429435477, ok := true }, Z2 := { p := [[[2023732677384037367]], [[(-92207761674233283), 49711873740065543], [(-279994927201873620)]], [[326298000785886, (-3928536206319534), 0], [(-420893087277723), 685112023439808], [1041802592634785]], [[(-6978884906493), 11513739694729, 0, 0], [(-23429243508347), (-49170180774242), 0], [(-38185012132938), 5838289451410], [(-46021692922709)]], [[52612428086, (-287607141035), 0, 0, 0], [(-49976213717), (-165493134795), 0, 0], [(-396416733704), (-335458514398), 0], [(-235393650747), 81544349371], [338885490099]]], r := 115626288251, ok := true }, Z3 := { p := [[[3220259324294044421]], [[(-192627713468778499), 101092376695355524], [(-273839875270549988)]], [[1252178837992594, (-8208674889940110), 0], [(-329770823692484), 1230988866038517], [1571085951796576]], [[(-31823791168277), 48553554569565, 0, 0], [(-65772975528527), (-78702823969048), 0], [(-71485010319845), 7881981356477], [(-42844849264286)]], [[368393046641, (-1326112083531), 0, 0, 0], [11813012432, (-919607634838), 0, 0], [(-650439953051), (-169325167665), 0], [(-157820732129), 100542677296], [467014516538]]], r := 343418365083, ok := true }, iE := { p := [[[18781004402400636939]], [[(-39497150482858968), 0], [(-49051945674224041)]], [[1311615739884876, 0, 0], [1981399343683649, 0], [3009819393975506]], [[(-7763640804201), 0, 0, 0], [18583349922914, 0, 0], [10451166789388, 0], [(-18534078450661)]], [[150854035799, 0, 0, 0, 0], [224446804307, 0, 0, 0], [709560337280, 0, 0], [573027404468, 0], [629097327867]]], r := 196290689368, ok := true }, iHu := { p := [[[19096206086418503740]], [[(-81668074669994386), 0], [(-80520513901797745)]], [[2889537768374991, 0, 0], [4359049832041647, 0], [2808903485482572]], [[(-28228549271067), 0, 0, 0], [11243257676567, 0, 0], [11085272791182, 0], [(-27055229470470)]], [[616742682790, 0, 0, 0, 0], [1044016728637, 0, 0, 0], [1636177906331, 0, 0], [1014882816231, 0], [582801805919]]], r := 424323962443, ok := true }, T := { p := [[[13258597302978740224]], [[0, 576460752303423488], [0]]], r := 0, ok := true }, E := { p := [[[18118432839376933660]], [[38103737853283884, 0], [47321451201278274]], [[(-1185209914725221), 0, 0], [(-1712460382261475), 0], [(-2780043078429554)]], [[2336143844461, 0, 0, 0], [(-31949389064634), 0, 0], [(-31500451513375), 0], [3035668955434]], [[(-42095936993), 0, 0, 0, 0], [(-51125379774), 0, 0, 0], [(-337490723779), 0, 0], [(-49698695416), 0], [(-106749623729)]]], r := 133636450838, ok := true }, de := { p := [[[(-5848165255158811552)]], [[363812257477434002, 0], [358700141447306124]], [[(-1075654728271100), 0, 0], [3843055084631784, 0], [(-1045637938525951)]], [[25843553412777, 0, 0, 0], [41173868301036, 0, 0], [40595312774558, 0], [24769365977714]], [[(-210422833442), 0, 0, 0, 0], [441130140874, 0, 0, 0], [989888110107, 0, 0], [428820139960, 0], [(-198842743916)]]], r := 126551103287, ok := true }, dde := { p := [[[(-55837939358410104757)]], [[330183176917914963, 0], [325543600661457138]], [[(-11899412996204437), 0, 0], [(-18051577293627014), 0], [(-11567352746191061)]], [[129182864753208, 0, 0, 0], [(-8041741835052), 0, 0], [(-7928743120741), 0], [123813378292621]], [[(-2883648649196), 0, 0, 0, 0], [(-5019260340595), 0, 0, 0], [(-7489014055055), 0, 0], [(-4879194873154), 0], [(-2724954324202)]]], r := 3987459333374, ok := true }, nJu := { p := [[[(-11696330510317623104)]], [[727624514954868005, 0], [717400282894612249]], [[(-2151309456542199), 0, 0], [7686110169263568, 0], [(-2091275877051902)]], [[51687106825555, 0, 0, 0], [82347736602072, 0, 0], [81190625549116, 0], [49538731955429]], [[(-420845666883), 0, 0, 0, 0], [882260281749, 0, 0, 0], [1979776220215, 0, 0], [857640279920, 0], [(-397685487832)]]], r := 253102206566, ok := true }, Jd1 := { p := [[[(-111675878716820209513)]], [[660366353835829927, 0], [651087201322914277]], [[(-23798825992408873), 0, 0], [(-36103154587254027), 0], [(-23134705492382121)]], [[258365729506417, 0, 0, 0], [(-16083483670104), 0, 0], [(-15857486241481), 0], [247626756585243]], [[(-5767297298392), 0, 0, 0, 0], [(-10038520681190), 0, 0, 0], [(-14978028110110), 0, 0], [(-9758389746308), 0], [(-5449908648404)]]], r := 7974918666738, ok := true }, term0 := { p := [[[350280243093565716469]], [[(-4071020589217359260), 0], [(-3617906045617179813)]], [[160695522750169235, 0, 0], [221600672419221685, 0], [128075899102430341]], [[(-2470576410225198), 0, 0, 0], [(-1574182218620818), 0, 0], [(-1561705119107534), 0], [(-1916159218623069)]], [[61159407841917, 0, 0, 0, 0], [105865634092583, 0, 0, 0], [134636342441953, 0, 0], [91043704744333, 0], [44537819387209]]], r := 38342064745404, ok := true }, r0 := { p := [[[59185992431626485118]], [[(-582147947703000485), 5101306041225749906], [(-302178974797337193)]], [[23078873556223875, (-43128900648112060), 106997138297508703], [15467678405136954, (-27274114457231079)], [8300466679888936]], [[(-268006535647601), 1638281187953595, (-298429432897586), (-166286596207245)], [171133318701638, 1488500034685457, (-677773922693406)], [(-31133666689804), 703308774163450], [(-97600577986579)]], [[6153101156491, (-16865816302151), 5117350807368, 26728251544609, (-1630121695058)], [5296296487787, 9981816763897, 44253238762162, (-3527049121873)], [8850307583198, (-360631380120), 13737788838530], [3387157970881, (-8764312522747)], [1718152371434]]], r := 43006253635511, ok := true }, r1 := { p := [[[113632873694084955595]], [[(-973545243557887853), 0], [(-605298843492482644)]], [[37337519874148542, 0, 0], [32802206676613974, 0], [15694695442394981]], [[(-405317950953289), 0, 0, 0], [243909374872206, 0, 0], [(-14839243622934), 0], [(-194431691154521)]], [[9134576728712, 0, 0, 0, 0], [9910864784302, 0, 0, 0], [16397676216607, 0, 0], [7086127111286, 0], [3242734568209]]], r := 19362346108653, ok := true }, r2 := { p := [[[61779556072048370689]], [[(-756886121865773046), 5114280376170966279], [(-1344186045355666357)]], [[24955727271479748, (-44092581081293301), 102095189999333630], [74488442045371715, (-29656688319005203)], [69390098948538047]], [[(-318265681964459), 1605941164398828, 68377651330660, (-216795064644102)], [(-537895297386117), 1721373411770067, 1074393933069515], [(-379899095388871), 40330130155980], [(-799038023824779)]], [[6789188405550, (-15971262039990), 1713970557653, 29370893164190, (-1327023737338)], [22040139676383, 22742109419374, (-73516385168749), 11284088334387], [36219086667510, 29472835749545, (-25003650112885)], [33973608935410, (-3805724453248)], [22244377773771]]], r := 188437715931706, ok := true }, r3 := { p := [[[256248741445842610962]], [[(-4587048914096148136), 20595359664882448739], [(-5080492827881505185)]], [[174978025719110407, (-201134412137643330), 358503569550597775], [308061044038202905, (-94536741436981956)], [203169702372578888]], [[(-2685900031982996), 7475715598954091, 7470189798591224, (-2704915058287512)], [(-2533249563905415), 4437229326681553, 5815683796694847], [(-2110103854356732), 703544131610699], [(-2830101132824722)]], [[64434682840333, (-62589224447993), (-277050267030363), 351941590575894, (-9716651272406)], [132216575121317, 131500622714687, (-279864874376198), 11799281686323], [179816091650848, 45351267263175, (-26846663755505)], [136517009827821, (-29108103415128)], [70309261518133]]], r := 2927130260618104, ok := true }, eta := { p := [[[(-228769522915120417173)]], [[2008535812261163812, 0], [2040525731037942165]], [[(-73954918558851595), 0, 0], [(-113953836723943120), 0], [(-83008275260561305)]], [[893298882588139, 0, 0, 0], [258175761180246, 0, 0], [453331879259086, 0], [1084892032171495]], [[(-20213855710725), 0, 0, 0, 0], [(-36397680266626), 0, 0, 0], [(-58437888110143), 0, 0], [(-46159136924685), 0], [(-27981914559780)]]], r := 110818363549427705, 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 := 9079256848778919936, bh := 144115188075855872, tc := 12970366926827028480, th := 288230376151711744, sc := 15168123544983830528, sh := 252201579132747776 }
noncomputable def q3 : Cert := { V0 := [[[1146680448320604284]], [[(-89879804231905736), 25339947668470220], [15829994596861596]], [[189863453539708, (-1964008907638939), (-4696989337216)], [(-1107403308873795), 345909191300572], [139833348172450]], [[(-4957345864034), 1543608559597, 1098532972045, (-33651987526)], [(-6593484120580), (-23280753488865), (-193478069525)], [(-7492314102768), 2974756711389], [1943594651223]], [[24870071268, (-29932050894), (-87262796579), 7692231690, 18695860], [(-134231725470), (-245818264545), 43455695628, (-1354786954)], [(-194597746813), (-138034538952), (-4343958393)], [(-91387409111), 40674609743], [21323777511]]], r0 := 316891134112, V1 := [[[1626215643460900281]], [[(-126747654961377849), 0], [22323309561584999]], [[183894882820599, 0, 0], [(-1532114164915200), 0], [194590710951751]], [[(-4540301212102), 0, 0, 0], [(-12534253914367), 0, 0], [(-9745708851455), 0], [2683435516530]], [[17599173674, 0, 0, 0, 0], [(-117267259370), 0, 0, 0], [(-335989935727), 0, 0], [(-113839605688), 0], [28930685559]]], r1 := 229261680060, V2 := [[[1435686850958220650]], [[(-89999796158835674), 25219487300197155], [(-273112253046885582)]], [[194303028787048, (-1946185892831477), (-5835275880012)], [(-995313540805152), 476490615757306], [75479346819135]], [[(-4936693471325), 849649310928, 1269972355319, (-32699816804)], [(-10774116119048), (-41666545921844), 900344983980], [450295753631, (-6968644781109)], [2175418047293]], [[24389734973, (-26254778517), (-93284726573), 7405467690, 22898211], [(-157296434999), 432004516575, (-120699726371), (-2353746304)], [(-454463256086), 412550640160, 40078514859], [(-132903296027), (-137337551539)], [(-10928125103)]]], r2 := 1045835045636, V3 := [[[2589279602175742915]], [[(-181424459114005198), 49614632164100369], [(-257384825819521863)]], [[497750476081202, (-3706214092269245), (-41184119392651)], [(-2116554906333052), 1032593784743277], [156379017027130]], [[(-12506554201755), (-12804123900252), 9131600293817, (-225948714851)], [(-12686448673536), (-93663956261975), 2511564180037], [(-34953149884), (-11055803412846)], [4587393215413]], [[35494942522, 387779843675, (-671803702833), 45875840258, 606716651], [(-554161679400), 1041387470298, (-217595228677), (-20859464618)], [(-848831645691), 399971906703, 153597881458], [(-285244166931), (-258606271442)], [(-12985254878)]]], r3 := 3911114619752, Vm := [[[2498017617523564546]], [[(-175772862339485470), 0], [(-184329038184837546)]], [[100457359466338, 0, 0], [(-3775663095176349), 0], [7177385984619459]], [[1355400912014, 0, 0, 0], [(-74586860833074), 0, 0], [409273246389639, 0], [531360974925172]], [[210694790379, 0, 0, 0, 0], [(-4821634702877), 0, 0, 0], [21608156827852, 0, 0], [78221180327288, 0], [28919662709650]]], rm := 614474187739691 }
noncomputable def w3 : Wit := { Z0 := { p := [[[1149887643232936834]], [[(-90635700870107328), 25553058738509707], [15963126169641207]], [[251049696408539, (-2014126686002386), 0], [(-1137706941700462), 354736137103137], [142857804667044]], [[(-6843466621848), 5578882142411, 0, 0], [(-4294675098908), (-25282376482233), 0], [(-8147574066269), 3174617881489], [2001298006143]], [[44134401533, (-152077036042), 0, 0, 0], [(-194797833976), (-95437224421), 0, 0], [(-149523337955), (-181057201473), 0], [(-103258357473), 44473289025], [22333876777]]], r := 53516891424, ok := true }, Z1 := { p := [[[1635395759264621275]], [[(-128904107904152643), 0], [22703112774600827]], [[357048457114367, 0, 0], [(-1618072094862879), 0], [203175544415352]], [[(-9732930306628), 0, 0, 0], [(-6107982362891), 0, 0], [(-11587660894249), 0], [2846290497627]], [[62768926625, 0, 0, 0, 0], [(-277045808322), 0, 0, 0], [(-212655413981), 0, 0], [(-146856330628), 0], [31763735861]]], r := 45344348371, ok := true }, Z2 := { p := [[[1441993915252293573]], [[(-91190199480488626), 25553058738509707], [(-276724636042035473)]], [[272170180083222, (-2014126686002386), 0], [(-551486671153890), 354736137103137], [769868207170559]], [[(-6957261726235), 5578882142411, 0, 0], [(-25078297809660), (-25282376482233), 0], [(-39650928717158), 3174617881489], [(-43733064917207)]], [[46592406038, (-152077036042), 0, 0, 0], [(-76980486855), (-95437224421), 0, 0], [(-474189838017), (-181057201473), 0], [(-312152842960), 44473289025], [245559347208]]], r := 92077224725, ok := true }, Z3 := { p := [[[2626734994368811034]], [[(-189391314489648290), 51793349415883563], [(-268687313329768078)]], [[1094473435411968, (-4183384244797440), 0], [(-578388843438843), 631873875659514], [1320264635483372]], [[(-31232664579256), 23308187902262, 0, 0], [(-68242441573504), (-39697911845304), 0], [(-72705089896804), 4251895179078], [(-39511922609760)]], [[332555575737, (-685009826655), 0, 0, 0], [(-96480836994), (-509310581470), 0, 0], [(-829004115938), (-88447141560), 0], [(-277889874339), 53436490687], [381389909680]]], r := 273716783733, ok := true }, iE := { p := [[[18694801409238831315]], [[(-35487911064403105), 0], [(-37215372308476156)]], [[1351710955179734, 0, 0], [2030186250577517, 0], [2913293451748802]], [[(-7282886680770), 0, 0, 0], [21559101691626, 0, 0], [13971552920615, 0], [(-13705775345658)]], [[157312288348, 0, 0, 0, 0], [257423534987, 0, 0, 0], [780445687681, 0, 0], [602305849468, 0], [580654761885]]], r := 206350987546, ok := true }, iHu := { p := [[[18946193321859244096]], [[(-72897502320864067), 0], [(-69591493145314676)]], [[2918718707850077, 0, 0], [4415597813523168, 0], [2659985409875800]], [[(-26062232308628), 0, 0, 0], [18016921778016, 0, 0], [17199827819830, 0], [(-22674730329641)]], [[619820227491, 0, 0, 0, 0], [1125783185070, 0, 0, 0], [1755082330151, 0, 0], [1025986793080, 0], [514801460774]]], r := 446884825755, ok := true }, T := { p := [[[12970366926827028480]], [[0, 288230376151711744], [0]]], r := 0, ok := true }, E := { p := [[[18201978158097654767]], [[34552396034094999, 0], [36234318786055278]], [[(-1250487791390488), 0, 0], [(-1839101923156748), 0], [(-2764363684941530)]], [[2218846384524, 0, 0, 0], [(-33343369831776), 0, 0], [(-31831198864349), 0], [2194952233195]], [[(-45077418214), 0, 0, 0, 0], [(-66473011785), 0, 0, 0], [(-359817463388), 0, 0], [(-60580432443), 0], [(-103630802574)]]], r := 145658711341, ok := true }, de := { p := [[[(-5134752441021428057)]], [[371664253499170332, 0], [354808731798527687]], [[(-989213038477169), 0, 0], [4010731056907973, 0], [(-901523069876913)]], [[26795407529160, 0, 0, 0], [45337000386959, 0, 0], [43280900596167, 0], [23312609319170]], [[(-199938968215), 0, 0, 0, 0], [512486021856, 0, 0, 0], [1093683501488, 0, 0], [467056087740, 0], [(-166062461884)]]], r := 141008288650, ok := true }, dde := { p := [[[(-55232173508665820481)]], [[294009368206983126, 0], [280675610011655092]], [[(-11946012434224697), 0, 0], [(-18141670957297774), 0], [(-10887043926421705)]], [[118849888625307, 0, 0, 0], [(-38858876973678), 0, 0], [(-37096569627932), 0], [103402085530272]], [[(-2877924067753), 0, 0, 0, 0], [(-5330105371822), 0, 0, 0], [(-7940969641075), 0, 0], [(-4857611829470), 0], [(-2390305202004)]]], r := 4172061031015, ok := true }, nJu := { p := [[[(-10269504882042856114)]], [[743328506998340664, 0], [709617463597055374]], [[(-1978426076954338), 0, 0], [8021462113815946, 0], [(-1803046139753826)]], [[53590815058321, 0, 0, 0], [90674000773918, 0, 0], [86561801192335, 0], [46625218638341]], [[(-399877936430), 0, 0, 0, 0], [1024972043713, 0, 0, 0], [2187367002977, 0, 0], [934112175481, 0], [(-332124923768)]]], r := 282016577293, ok := true }, Jd1 := { p := [[[(-110464347017331640962)]], [[588018736413966253, 0], [561351220023310184]], [[(-23892024868449393), 0, 0], [(-36283341914595547), 0], [(-21774087852843410)]], [[237699777250614, 0, 0, 0], [(-77717753947356), 0, 0], [(-74193139255864), 0], [206804171060545]], [[(-5755848135505), 0, 0, 0, 0], [(-10660210743643), 0, 0, 0], [(-15881939282149), 0, 0], [(-9715223658939), 0], [(-4780610404008)]]], r := 8344122062022, ok := true }, term0 := { p := [[[343542094831668059885]], [[(-3633350457123060261), 0], [(-3127228448813680289)]], [[158085492887014867, 0, 0], [216421349384034095, 0], [117591215081902070]], [[(-2258434590484080), 0, 0, 0], [(-1035493329783827), 0, 0], [(-1033647249091880), 0], [(-1587631101030879)]], [[59583072535704, 0, 0, 0, 0], [106614011925739, 0, 0, 0], [135167802610664, 0, 0], [85347896923167, 0], [37859762170955]]], r := 37286889919190, ok := true }, r0 := { p := [[[56115775936072377377]], [[(-531290633780673329), 2471839476076695071], [(-257970432728543147)]], [[22628018602626030, (-19960497666831351), 26488183361429474], [14649029729991455, (-11969558332977509)], [7430202818517731]], [[(-248937395519019), 827688743370762, (-62576132658863), (-21275543442081)], [201097441635066, 723096222256080, (-154915344483144)], [(-11905686983691), 320727149378617], [(-81053318591764)]], [[6106556430285, (-7982651971974), 1674862217143, 3401169054267, (-106469689645)], [5574306241145, 6510648597889, 11086305718294, (-465716178028)], [9017698198013, 663443838468, 3155646778906], [3114629089284, (-3749907943631)], [1415320113072]]], r := 19703865666058, ok := true }, r1 := { p := [[[112483549594298278439]], [[(-907943901398196543), 0], [(-544753513185520974)]], [[37892309363715866, 0, 0], [32827097131528709, 0], [14601926823908964]], [[(-384576603296999), 0, 0, 0], [311608198267787, 0, 0], [27113228784940, 0], [(-170463509760517)]], [[9319074921521, 0, 0, 0, 0], [10866468340832, 0, 0, 0], [17490139496647, 0, 0], [6914700215262, 0], [2763151962725]]], r := 20742516323893, ok := true }, r2 := { p := [[[56861205650600736974]], [[(-588919083608699127), 2475408905250249006], [(-1060521037111929366)]], [[23201704654896963, (-20212469370414636), 26106451434544235], [72431034787495032, (-15246494610712281)], [65085423180646194]], [[(-265897435215000), 823597667133730, (-31674999009220), (-23572161157718)], [(-401552999492587), 959976043860928, 237124266755230], [(-195191940757160), 25313537210759], [(-632843841768363)]], [[6307312454307, (-7851377601926), 1365772731664, 3534250574538, (-100400839440)], [22470511557341, 10976389820609, (-19492167264940), 1748230470808], [37722468648623, 15858143623838, (-7103070045110)], [32886155980303, (-863463458986)], [19109415233895]]], r := 87714199571520, ok := true }, r3 := { p := [[[236767274455191432942]], [[(-3880599081616140195), 10018440163188277110], [(-4252181297910900892)]], [[166678815545476128, (-99319201525461315), 93496431203697990], [298808612230673638, (-48851450027792515)], [187497654793418812]], [[(-2391120454629939), 4020725753898106, 1574828069170133, (-329362694286071)], [(-1892102685803871), 2492798501383235, 1409145154306723], [(-1354717402786272), 296714191118855], [(-2302776295246150)]], [[61545272549950, (-31606916706344), (-69579577761871), 46736793010276, (-918068978374)], [131778480459012, 77339072518863, (-86230619306437), 4273775459002], [177543559494505, 35879124506762, (-11427236811229)], [125811351118487, (-9908057814293)], [58949726740987]]], r := 1232460226012850, ok := true }, eta := { p := [[[(-225012260052292814841)]], [[1782075735449112733, 0], [1720648310836541097]], [[(-73674759985212998), 0, 0], [(-112687560744161590), 0], [(-77138494788999114)]], [[819211505346526, 0, 0, 0], [20556106986834, 0, 0], [181237337528676, 0], [876699985216596]], [[(-20071766263050), 0, 0, 0, 0], [(-37820902832283), 0, 0, 0], [(-60579045880443), 0, 0], [(-44726570498995), 0], [(-24229376820408)]]], r := 267898257015324805, 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 := 9079256848778919936, bh := 144115188075855872, tc := 13546827679130451968, th := 288230376151711744, sc := 15168123544983830528, sh := 252201579132747776 }
noncomputable def q4 : Cert := { V0 := [[[1197341286785864108]], [[(-93803366494294117), 25320756491622876], [16521028249469510]], [[192597027972021, (-1959522703127866), (-4898446481036)], [(-1153788664660495), 345119062819790], [145765251801825]], [[(-5007036557745), 1187679288537, 1144510178578, (-33499383307)], [(-7098009503391), (-23103442003961), (-201575761072)], [(-7764658181892), 2957030310136], [2024612583951]], [[24520433128, (-19708126350), (-90692640145), 7633127427, 19453687], [(-134972222110), (-258782111601), 45196122311, (-1344377272)], [(-207296219709), (-134286758719), (-4518868810)], [(-94363155879), 40341227079], [22178245220]]], r0 := 330113591640, V1 := [[[1626215643460900281]], [[(-126747654961377849), 0], [22323309561584999]], [[183894882820599, 0, 0], [(-1532114164915200), 0], [194590710951751]], [[(-4540301212102), 0, 0, 0], [(-12534253914367), 0, 0], [(-9745708851455), 0], [2683435516530]], [[17599173674, 0, 0, 0, 0], [(-117267259370), 0, 0, 0], [(-335989935727), 0, 0], [(-113839605688), 0], [28930685559]]], r1 := 229261680060, V2 := [[[1486102223225186900]], [[(-93887028947843817), 25195754537252924], [(-272155689305924692)]], [[195624859735162, (-1941017411226067), (-6030919593372)], [(-1079124739066933), 480063669870037], [61702471874422]], [[(-4979229233248), 470027432634, 1314199575888, (-32513819505)], [(-9900485329612), (-42142301158257), 886162069195], [1250055903409, (-6808182437696)], [1900670382966]], [[23893938663, (-16237252335), (-96516004547), 7336596940, 23599316], [(-165155191658), 441419821194, (-117172988274), (-2373749411)], [(-433672707889), 387211697609, 40150104991], [(-111535024842), (-137395573852)], [(-9435545802)]]], r2 := 1069471256552, V3 := [[[2688342332187832482]], [[(-188799997443186128), 49447203825894841], [(-255309758958162634)]], [[469436791668976, (-3669144291812333), (-42525141875417)], [(-2304712629819491), 1042389555125852], [134880268129713]], [[(-11667092856860), (-15518419182218), 9401515148526, (-221041014847)], [(-10656941776449), (-94473514629941), 2386284686400], [673878213087, (-10443745567988)], [4072462822510]], [[24926442976, 451404336673, (-685091614916), 44091120749, 620039983], [(-541555579146), 986498999850, (-187217356029), (-20895797488)], [(-774512863304), 309223028929, 152397879543], [(-246417153477), (-256235867622)], [(-10036038714)]]], r3 := 4044408084360, Vm := [[[2498017617523564546]], [[(-175772862339485470), 0], [(-184329038184837546)]], [[100457359466338, 0, 0], [(-3775663095176349), 0], [7177385984619459]], [[1355400912014, 0, 0, 0], [(-74586860833074), 0, 0], [409273246389639, 0], [531360974925172]], [[210694790379, 0, 0, 0, 0], [(-4821634702877), 0, 0, 0], [21608156827852, 0, 0], [78221180327288, 0], [28919662709650]]], rm := 614474187739691 }
noncomputable def w4 : Wit := { Z0 := { p := [[[1200993760709956249]], [[(-94663954242112098), 25553058738509707], [16672598443847482]], [[262207460693363, (-2014126686002386), 0], [(-1188271694664927), 354736137103137], [149207040430024]], [[(-7147620693930), 5578882142411, 0, 0], [(-4485549547748), (-25282376482233), 0], [(-8509688469214), 3174617881489], [2090244584194]], [[46095930490, (-152077036042), 0, 0, 0], [(-203455515486), (-95437224421), 0, 0], [(-156168819642), (-181057201473), 0], [(-107847617805), 44473289025], [23326493523]]], r := 54933902309, ok := true }, Z1 := { p := [[[1635395759264621275]], [[(-128904107904152643), 0], [22703112774600827]], [[357048457114367, 0, 0], [(-1618072094862879), 0], [203175544415352]], [[(-9732930306628), 0, 0, 0], [(-6107982362891), 0, 0], [(-11587660894249), 0], [2846290497627]], [[62768926625, 0, 0, 0, 0], [(-277045808322), 0, 0, 0], [(-212655413981), 0, 0], [(-146856330628), 0], [31763735861]]], r := 45344348371, ok := true }, Z2 := { p := [[[1493100032729312988]], [[(-95218452852493396), 25553058738509707], [(-276015163767829197)]], [[283327944368046, (-2014126686002386), 0], [(-602051424118355), 354736137103137], [776217442933539]], [[(-7261415798317), 5578882142411, 0, 0], [(-25269172258500), (-25282376482233), 0], [(-40013043120103), 3174617881489], [(-43644118339157)]], [[48553934995, (-152077036042), 0, 0, 0], [(-85638168365), (-95437224421), 0, 0], [(-480835319704), (-181057201473), 0], [(-316742103292), 44473289025], [246551963953]]], r := 93269942024, ok := true }, Z3 := { p := [[[2730321693200578160]], [[(-197758082979243169), 51793349415883563], [(-267423565578449049)]], [[1141089811216493, (-4183384244797440), 0], [(-657784667129449), 631873875659514], [1328768425841529]], [[(-32602684232564), 23308187902262, 0, 0], [(-69261062736443), (-39697911845304), 0], [(-72881984179924), 4251895179078], [(-39405049628385)]], [[346905392834, (-685009826655), 0, 0, 0], [(-119649440509), (-509310581470), 0, 0], [(-854555799252), (-88447141560), 0], [(-279008701374), 53436490687], [382236730811]]], r := 278589116107, ok := true }, iE := { p := [[[18694801409238831315]], [[(-35487911064403105), 0], [(-37215372308476156)]], [[1351710955179734, 0, 0], [2030186250577517, 0], [2913293451748802]], [[(-7282886680770), 0, 0, 0], [21559101691626, 0, 0], [13971552920615, 0], [(-13705775345658)]], [[157312288348, 0, 0, 0, 0], [257423534987, 0, 0, 0], [780445687681, 0, 0], [602305849468, 0], [580654761885]]], r := 206350987546, ok := true }, iHu := { p := [[[18946193321859244096]], [[(-72897502320864067), 0], [(-69591493145314676)]], [[2918718707850077, 0, 0], [4415597813523168, 0], [2659985409875800]], [[(-26062232308628), 0, 0, 0], [18016921778016, 0, 0], [17199827819830, 0], [(-22674730329641)]], [[619820227491, 0, 0, 0, 0], [1125783185070, 0, 0, 0], [1755082330151, 0, 0], [1025986793080, 0], [514801460774]]], r := 446884825755, ok := true }, T := { p := [[[13546827679130451968]], [[0, 288230376151711744], [0]]], r := 0, ok := true }, E := { p := [[[18201978158097654767]], [[34552396034094999, 0], [36234318786055278]], [[(-1250487791390488), 0, 0], [(-1839101923156748), 0], [(-2764363684941530)]], [[2218846384524, 0, 0, 0], [(-33343369831776), 0, 0], [(-31831198864349), 0], [2194952233195]], [[(-45077418214), 0, 0, 0, 0], [(-66473011785), 0, 0, 0], [(-359817463388), 0, 0], [(-60580432443), 0], [(-103630802574)]]], r := 145658711341, ok := true }, de := { p := [[[(-5134752441021428057)]], [[371664253499170332, 0], [354808731798527687]], [[(-989213038477169), 0, 0], [4010731056907973, 0], [(-901523069876913)]], [[26795407529160, 0, 0, 0], [45337000386959, 0, 0], [43280900596167, 0], [23312609319170]], [[(-199938968215), 0, 0, 0, 0], [512486021856, 0, 0, 0], [1093683501488, 0, 0], [467056087740, 0], [(-166062461884)]]], r := 141008288650, ok := true }, dde := { p := [[[(-55232173508665820481)]], [[294009368206983126, 0], [280675610011655092]], [[(-11946012434224697), 0, 0], [(-18141670957297774), 0], [(-10887043926421705)]], [[118849888625307, 0, 0, 0], [(-38858876973678), 0, 0], [(-37096569627932), 0], [103402085530272]], [[(-2877924067753), 0, 0, 0, 0], [(-5330105371822), 0, 0, 0], [(-7940969641075), 0, 0], [(-4857611829470), 0], [(-2390305202004)]]], r := 4172061031015, ok := true }, nJu := { p := [[[(-10269504882042856114)]], [[743328506998340664, 0], [709617463597055374]], [[(-1978426076954338), 0, 0], [8021462113815946, 0], [(-1803046139753826)]], [[53590815058321, 0, 0, 0], [90674000773918, 0, 0], [86561801192335, 0], [46625218638341]], [[(-399877936430), 0, 0, 0, 0], [1024972043713, 0, 0, 0], [2187367002977, 0, 0], [934112175481, 0], [(-332124923768)]]], r := 282016577293, ok := true }, Jd1 := { p := [[[(-110464347017331640962)]], [[588018736413966253, 0], [561351220023310184]], [[(-23892024868449393), 0, 0], [(-36283341914595547), 0], [(-21774087852843410)]], [[237699777250614, 0, 0, 0], [(-77717753947356), 0, 0], [(-74193139255864), 0], [206804171060545]], [[(-5755848135505), 0, 0, 0, 0], [(-10660210743643), 0, 0, 0], [(-15881939282149), 0, 0], [(-9715223658939), 0], [(-4780610404008)]]], r := 8344122062022, ok := true }, term0 := { p := [[[343542094831668059885]], [[(-3633350457123060261), 0], [(-3127228448813680289)]], [[158085492887014867, 0, 0], [216421349384034095, 0], [117591215081902070]], [[(-2258434590484080), 0, 0, 0], [(-1035493329783827), 0, 0], [(-1033647249091880), 0], [(-1587631101030879)]], [[59583072535704, 0, 0, 0, 0], [106614011925739, 0, 0, 0], [135167802610664, 0, 0], [85347896923167, 0], [37859762170955]]], r := 37286889919190, ok := true }, r0 := { p := [[[61165235718659170357]], [[(-571434482843926096), 2577533508111115779], [(-282532968383102794)]], [[24288887625212050, (-20169506027978205), 26357986989931314], [16140060679663589, (-12594871949611999)], [8084211712917372]], [[(-264793448750002), 832573435810781, (-41808460144532), (-22121202116698)], [214035819431206, 768182638394860, (-157757227262929)], [(-10346715520404), 333247515250609], [(-88745667608155)]], [[6483064635752, (-7867709328195), 764641492321, 3520754873171, (-104936010475)], [6101381365298, 6422839368268, 11458155091158, (-481479308144)], [9781838353770, 899155314738, 3104303788934], [3431182354714, (-3942940139185)], [1538836025259]]], r := 21797913947026, ok := true }, r1 := { p := [[[112483549594298278439]], [[(-907943901398196543), 0], [(-544753513185520974)]], [[37892309363715866, 0, 0], [32827097131528709, 0], [14601926823908964]], [[(-384576603296999), 0, 0, 0], [311608198267787, 0, 0], [27113228784940, 0], [(-170463509760517)]], [[9319074921521, 0, 0, 0, 0], [10866468340832, 0, 0, 0], [17490139496647, 0, 0], [6914700215262, 0], [2763151962725]]], r := 20742516323893, ok := true }, r2 := { p := [[[61916259088586765006]], [[(-629442229027902962), 2579548645865326788], [(-1090051674752522423)]], [[24853199851743795, (-20296320544031723), 25962622503908902], [74272540200646375, (-14277281588116192)], [65108236799195109]], [[(-281458827400389), 827313870405794, (-10142148783143), (-24368524014576)], [(-378506727323985), 881302677566211, 247416355553216], [(-164632777672583), (-2200008901208)], [(-634966371105477)]], [[6679249484499, (-7705141668200), 490328762285, 3642687991386, (-98682088935)], [22701119879150, 12041166502138, (-19832198754545), 1682342714012], [37770997148194, 14669423314988, (-6653218449960)], [33032759067010, (-1261147893343)], [19305721838799]]], r := 94900644121712, ok := true }, r3 := { p := [[[257175491176741468099]], [[(-4072564062802627812), 10388444810048793823], [(-4344215697441843161)]], [[174431384141754159, (-92458651903833281), 91498874028255924], [303459576290897484, (-43168120177938802)], [188049998191077332]], [[(-2450651104699702), 3726706919832463, 1855502436110919, (-336380878071303)], [(-1744844467362913), 2163480690351221, 1431391466006138], [(-1294931341065896), 257919185210299], [(-2324595813957774)]], [[63131200774286, (-28077790900444), (-77282050743534), 46792548842466, (-836458824092)], [133180507530357, 69333322075225, (-78259168643161), 3145534634559], [181274364963215, 23757874851696, (-7992530275070)], [128063075202448, (-11894483326961)], [59802368492973]]], r := 1359918194824197, ok := true }, eta := { p := [[[(-225012260052292814841)]], [[1782075735449112733, 0], [1720648310836541097]], [[(-73674759985212998), 0, 0], [(-112687560744161590), 0], [(-77138494788999114)]], [[819211505346526, 0, 0, 0], [20556106986834, 0, 0], [181237337528676, 0], [876699985216596]], [[(-20071766263050), 0, 0, 0, 0], [(-37820902832283), 0, 0, 0], [(-60579045880443), 0, 0], [(-44726570498995), 0], [(-24229376820408)]]], r := 267898257015324805, 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 8646911284551352320 9223372036854775808 12682136550675316736 13835058055282163712 14411518807585587200 15420325124116578304 :=
  (RegionPosI.split_s 14915921965851082752 (RegionPosI.split_b 8935141660703064064 (RegionPosI.of_check c0 q0 ok_0 8646911284551352320 8935141660703064064 12682136550675316736 13835058055282163712 14411518807585587200 14915921965851082752 (by decide +kernel)) (RegionPosI.of_check c1 q1 ok_1 8935141660703064064 9223372036854775808 12682136550675316736 13835058055282163712 14411518807585587200 14915921965851082752 (by decide +kernel))) (RegionPosI.split_b 8935141660703064064 (RegionPosI.of_check c2 q2 ok_2 8646911284551352320 8935141660703064064 12682136550675316736 13835058055282163712 14915921965851082752 15420325124116578304 (by decide +kernel)) (RegionPosI.split_t 13258597302978740224 (RegionPosI.of_check c3 q3 ok_3 8935141660703064064 9223372036854775808 12682136550675316736 13258597302978740224 14915921965851082752 15420325124116578304 (by decide +kernel)) (RegionPosI.of_check c4 q4 ok_4 8935141660703064064 9223372036854775808 13258597302978740224 13835058055282163712 14915921965851082752 15420325124116578304 (by decide +kernel)))))

end CKLaneC.RSC2.BD_0170

end