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

import Definitions.Def_CK_CKLaneC_RSC2_BD_0116_part00

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

namespace CKLaneC.RSC2.BD_0116
open CKLaneC.TM3 CKLaneC.RSCell

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 := 8214565720323784704, bh := 144115188075855872, tc := 11240984669916758016, th := 288230376151711744, sc := 16807433809346691072, sh := 126100789566373888 }
noncomputable def q6 : Cert := { V0 := [[[452444579087033072]], [[(-35158671660247352), 11591076859699956], [6460123985176836]], [[32795476068726, (-899158088074557), (-386765177500)], [(-476822770676663), 165213088462718], [54720208055695]], [[(-432812081037), 656464070981, 90088951612, (-3288775584)], [(-1373201917912), (-12127427616018), (-16553122450)], [(-3583266818182), 1393277306994], [791074971385]], [[1037885340, (-6015239370), (-7070012118), 763425355, 324350], [(-12954262451), (-42722950432), 3789023641, (-140273289)], [(-42896745423), (-89686438126), (-376066956)], [(-49663184675), 20097700333], [8139011548]]], r0 := 61525429020, V1 := [[[741928527887037784]], [[(-57569445038104326), 0], [10577923884549877]], [[43868769528606, 0, 0], [(-777145446069827), 0], [89267948493884]], [[(-438295971009), 0, 0, 0], [(-2657476577542), 0, 0], [(-5762178046584), 0], [1288134009975]], [[894009216, 0, 0, 0, 0], [(-11282462645), 0, 0, 0], [(-78878345917), 0, 0], [(-79318782105), 0], [13182300860]]], r1 := 46737609788, V2 := [[[2473021255366682687]], [[(-35535187670132957), 11160289200736603], [(-282215069361992658)]], [[44132303562900, (-855343200692048), (-1987450382507)], [(-428312033952621), 260003000496496], [51515283875712]], [[(-425972941735), (-188990077509), 334038732412, (-2605461279)], [(-2446445406650), (-20661022174853), 140852307185], [(-2347174165302), (-2678883072897)], [1785241174699]], [[1020521524, (-3868785921), (-16167776618), 588981717, 1487339], [(-15107374968), 56870879804, (-19899310915), (-262145337)], [(-120708665444), 186164740155, 9541523869], [(-124256506207), (-77119534661)], [(-3922858978)]]], r2 := 459153812496, V3 := [[[2929743758397976755]], [[(-71339205375360393), 22160265449361249], [(-276185852612568765)]], [[106312801837851, (-1682631949501609), (-9338567263967)], [(-862970968216259), 532408627059184], [99891735254829]], [[(-1249084473201), (-1870349431195), 1655008409870, (-19277374780)], [(-4154854110946), (-43168563659138), 468230890641], [(-4251848039161), (-4899525850809)], [3577977064284]], [[2187433251, 15960529411, (-88943621955), 4199240831, 27092790], [(-56572716012), 177996259660, (-57322500405), (-2132601719)], [(-253838861883), 302819043285, 37097267936], [(-248992698929), (-151139946583)], [(-6151800240)]]], r3 := 1013625313928, Vm := [[[2844355894744880047]], [[(-68933370534811339), 0], [(-263008545142458274)]], [[291477738677598, 0, 0], [(-2353727179974269), 0], [1209791301941917]], [[6607641815511, 0, 0, 0], [6909315479330, 0, 0], [(-98065103189229), 0], [112206116827350]], [[149475532327, 0, 0, 0, 0], [1034901367792, 0, 0, 0], [(-2490389399603), 0, 0], [(-5395124073051), 0], [10122313144260]]], rm := 68933742949020 }
noncomputable def w6 : Wit := { Z0 := { p := [[[452641020630527608]], [[(-35204483358823646), 11606180016167374], [6468541517432728]], [[36401326713267, (-902679060482658), 0], [(-478753458849888), 165860038908531], [54911803253154]], [[(-532646712714), 933367351622, 0, 0], [(-1226067187707), (-12275729714100), 0], [(-3626166106544), 1407994955209], [794718219886]], [[1408454852, (-13657608019), 0, 0, 0], [(-16676922530), (-31437620198), 0, 0], [(-39781823286), (-92978618117), 0], [(-50458735001), 20377390253], [8202331692]]], r := 13611743081, ok := true }, Z1 := { p := [[[742795521034711973]], [[(-57771459870890086), 0], [10615042490146015]], [[59735510503823, 0, 0], [(-785646701702379), 0], [90111677133381]], [[(-874086913171), 0, 0, 0], [(-2012007692648), 0, 0], [(-5950631559456), 0], [1304152976223]], [[2311310527, 0, 0, 0, 0], [(-27367257484), 0, 0, 0], [(-65282992058), 0, 0], [(-82804077950), 0], [13460236622]]], r := 10736040251, ok := true }, Z2 := { p := [[[2505603540305413061]], [[(-36954937062081978), 11606180016167374], [(-293490503639839573)]], [[66849996654031, (-902679060482658), 0], [(-112590241779009), 165860038908531], [1375233201532872]], [[(-606271289705), 933367351622, 0, 0], [(-5102556308539), (-12275729714100), 0], [(-19537047134235), 1407994955209], [(-54343439664340)]], [[2133101374, (-13657608019), 0, 0, 0], [(-3005366376), (-31437620198), 0, 0], [(-87563531432), (-92978618117), 0], [(-110256472046), 20377390253], [497817335429]]], r := 43969708396, ok := true }, Z3 := { p := [[[2984274794854274606]], [[(-75383681542213075), 23416610610335336], [(-291843822064794098)]], [[214607158127028, (-1841561348469298), 0], [(-120052859581641), 316620718989642], [1638343577009416]], [[(-2581786324043), 3834413876539, 0, 0], [(-14212112719462), (-22328376080094), 0], [(-38235036119980), 2369988176391], [(-52863118143472)]], [[12874737887, (-59530996260), 0, 0, 0], [(-947878674), (-137836926181), 0, 0], [(-172635810466), (-122222361760), 0], [(-144371980077), 32973139177], [570485403116]]], r := 81887692663, ok := true }, iE := { p := [[[18769943037027524143]], [[(-16004148144076177), 0], [(-61062264719700441)]], [[278387839458411, 0, 0], [1061471106922868, 0], [3348329252885930]], [[(-673138989632), 0, 0, 0], [4327505103595, 0, 0], [6167817307233, 0], [(-25787550243506)]], [[6625339625, 0, 0, 0, 0], [28834372027, 0, 0, 0], [181353683177, 0, 0], [334394590912, 0], [792544285098]]], r := 84563213705, ok := true }, iHu := { p := [[[18935103826753796487]], [[(-32574070417467250), 0], [(-76169442855882062)]], [[594880154898109, 0, 0], [2210596180745867, 0], [3252722226349710]], [[(-2377851153415), 0, 0, 0], [4192272657081, 0, 0], [9802983431220, 0], [(-30402612888528)]], [[25715076617, 0, 0, 0, 0], [115372911595, 0, 0, 0], [441446977638, 0, 0], [630843087934, 0], [768816711589]]], r := 133656582513, ok := true }, T := { p := [[[11240984669916758016]], [[0, 288230376151711744], [0]]], r := 0, ok := true }, E := { p := [[[18129110261531555827]], [[15457743572981582, 0], [58977511425500137]], [[(-255703270352387), 0, 0], [(-924656885881411), 0], [(-3042147207887866)]], [[202869561246, 0, 0, 0], [(-7548906974958), 0, 0], [(-17651955407608), 0], [4489561672099]], [[(-1879327345), 0, 0, 0, 0], [(-6900723986), 0, 0, 0], [(-90422901331), 0, 0], [(-37732202199), 0], [(-127170545846)]]], r := 58442319128, ok := true }, de := { p := [[[(-5077888134330430464)]], [[167997689481845062, 0], [392836702472585068]], [[(-199928715274613), 0, 0], [2012322916467390, 0], [(-1093182501558924)]], [[2469445553349, 0, 0, 0], [10308210751826, 0, 0], [24104161983593, 0], [31573716083975]], [[(-8250123144), 0, 0, 0, 0], [52804253252, 0, 0, 0], [275634812172, 0, 0], [288726337198, 0], [(-246658123532)]]], r := 51023928419, ok := true }, dde := { p := [[[(-55187451518206505790)]], [[131353667009894807, 0], [307150304060731462]], [[(-2433647876455106), 0, 0], [(-9076970597483634), 0], [(-13306849242954070)]], [[10840703165133, 0, 0, 0], [(-9343213311235), 0, 0], [(-21847664208984), 0], [138606531908420]], [[(-119334252348), 0, 0, 0, 0], [(-545615697543), 0, 0, 0], [(-1995715326574), 0, 0], [(-2983351002444), 0], [(-3567796776536)]]], r := 1195462840252, ok := true }, nJu := { p := [[[(-10155776268660860928)]], [[335995378963690124, 0], [785673404945170136]], [[(-399857430549225), 0, 0], [4024645832934781, 0], [(-2186365003117847)]], [[4938891106698, 0, 0, 0], [20616421503653, 0, 0], [48208323967187, 0], [63147432167951]], [[(-16500246287), 0, 0, 0, 0], [105608506504, 0, 0, 0], [551269624344, 0, 0], [577452674397, 0], [(-493316247064)]]], r := 102047856830, ok := true }, Jd1 := { p := [[[(-110374903036413011580)]], [[262707334019789614, 0], [614300608121462925]], [[(-4867295752910211), 0, 0], [(-18153941194967267), 0], [(-26613698485908139)]], [[21681406330266, 0, 0, 0], [(-18686426622469), 0, 0], [(-43695328417967), 0], [277213063816841]], [[(-238668504695), 0, 0, 0, 0], [(-1091231395086), 0, 0, 0], [(-3991430653147), 0, 0], [(-5966702004887), 0], [(-7135593553071)]]], r := 2390925680493, ok := true }, term0 := { p := [[[340967016333787468327]], [[(-1546888619943080354), 0], [(-3280052449595893936)]], [[31640650476316657, 0, 0], [108343665659712524, 0], [143797229719122534]], [[(-198377325849397), 0, 0, 0], [(-197960872833694), 0, 0], [(-486879560863481), 0], [(-2080026611949350)]], [[2410522082550, 0, 0, 0, 0], [10880580129739, 0, 0, 0], [34326925125901, 0, 0], [52944840620013, 0], [56405478523097]]], r := 10478307313637, ok := true }, r0 := { p := [[[41157170128353017462]], [[(-141001364517799431), 2107674007967964109], [(-189803169392923695)]], [[3427801831446441, (-6763147039885688), 26870408201273266], [6336375804224867, (-9803971236733958)], [6869518230386952]], [[(-15509138943888), 155906086257457, (-62796165169817), (-3861193614466)], [39132986415751, 335354375707081, (-129293805280991)], [14301451980910, 350870767311377], [(-73278244236371)]], [[191070759155, (-666520988990), 988148260372, 609344911377, (-24368475132)], [524394525247, 1646591932280, 4829606852699, (-91728554501)], [1903827532718, 930093339191, 4426296870402], [1754618047361, (-3780917560506)], [1623011817696]]], r := 2807056767891, ok := true }, r1 := { p := [[[110573238430784267984]], [[(-338347310746359071), 0], [(-517362924033717957)]], [[7489267088176574, 0, 0], [17978328898320610, 0], [18374918484023944]], [[(-31720839078235), 0, 0, 0], [74616110479745, 0, 0], [55672961116548, 0], [(-199359183211520)]], [[369025178628, 0, 0, 0, 0], [1247963180379, 0, 0, 0], [4667602054430, 0, 0], [4979861688965, 0], [4337187714604]]], r := 3662995721345, ok := true }, r2 := { p := [[[46328382747040855220]], [[(-314994254811986398), 2132412981842357311], [(-1379011313899651199)]], [[4258352416974117, (-8568219824318553), 25147208608356131], [32096615811669637, (-12758739552922634)], [76186086987583462]], [[(-26665481859313), 153332192754895, 18301985039716, (-11318144431339)], [(-129437376253525), 536789513658148, 206017614432498], [(-237378050274222), 253462122753248], [(-951933568104532)]], [[251560077630, (-654134740323), 605473516650, 1141600923606, (-17161428869)], [2094756811933, 2417200027471, (-5891758712271), 716566923570], [8569979493573, 9555112139820, (-8102826641108)], [19499465209235, (-1708476721525)], [28488232603517]]], r := 36091370907626, ok := true }, r3 := { p := [[[184317213462851576064]], [[(-1614956342125692656), 8576553615064662053], [(-4540454104488214801)]], [[29252720754002075, (-41338086697776276), 97473938055024295], [136156878912210979, (-49850670680013197)], [221075645137642960]], [[(-207263200810009), 885692772822154, 417833105891177, (-115400690057345)], [(-539811372107850), 1934483411715437, 1023569858228872], [(-946121593842543), 1042352375388121], [(-3062998117876591)]], [[2366007665045, (-3263095492011), (-6491208337446), 12786973736912, (-221901036128)], [12933565398539, 19048899821868, (-36641612576896), 4027307935748], [42259972121558, 34023348989743, (-26611003952488)], [75469888200000, (-8876708528910)], [86225800701386]]], r := 275906765964990, ok := true }, eta := { p := [[[(-225208415720724568964)]], [[799319935081689214, 0], [2006206334809645158]], [[(-15066248199739076), 0, 0], [(-57412720122495529), 0], [(-94706607769985791)]], [[75118383467980, 0, 0, 0], [17491578016515, 0, 0], [140497910303934, 0], [1269701287901515]], [[(-836727122847), 0, 0, 0, 0], [(-3992790047671), 0, 0, 0], [(-15181869916335), 0, 0], [(-27240732013920), 0], [(-36417696849774)]]], r := 33695592564397627, 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 := 8502796096475496448, bh := 144115188075855872, tc := 11240984669916758016, th := 288230376151711744, sc := 16807433809346691072, sh := 126100789566373888 }
noncomputable def q7 : Cert := { V0 := [[[465590170683401556]], [[(-36127054749965070), 11927240314817134], [6688768133076346]], [[29871463876663, (-923781724324262), (-421434822895)], [(-491766253572013), 171034195905060], [59672027077344]], [[(-460289242511), 565806866159, 98015506251, (-3582495803)], [(-1553922004091), (-12501315124564), (-18147147598)], [(-3892222625937), 1519047281436], [861258705108]], [[973210453, (-6329086646), (-7669585899), 830174990, 374194], [(-14562382084), (-48025910315), 4144171703, (-153703315)], [(-47565850112), (-97347462408), (-422021904)], [(-53412118221), 21869130643], [9435117289]]], r0 := 61052220468, V1 := [[[763451969858837302]], [[(-59147430360828124), 0], [10950891238961074]], [[38227200248480, 0, 0], [(-801168484141034), 0], [97329351214126]], [[(-462712923364), 0, 0, 0], [(-2989829781735), 0, 0], [(-6255172740552), 0], [1401792705220]], [[808744128, 0, 0, 0, 0], [(-13189132402), 0, 0, 0], [(-87486748316), 0, 0], [(-85151909963), 0], [15277625676]]], r1 := 46670158072, V2 := [[[1908811390984917424]], [[(-36402190299894810), 11668966655360779], [(-281987725752353335)]], [[38749444369520, (-895873993786756), (-1667183110715)], [(-439183208475075), 248370049944753], [62117700104393]], [[(-457152385624), (-68854211027), 288337110263, (-3138462596)], [(-2939920859267), (-19846656881895), 179582338188], [(-3085979987236), (-3135423905673)], [1746422965718]], [[973920361, (-4854262434), (-14823943753), 713949980, 1386451], [(-16099362787), 63263213154, (-25832648714), (-269405690)], [(-125969128469), 220830243503, 9792295142], [(-121823491529), (-74951687421)], [(-5778406210)]]], r2 := 421185829300, V3 := [[[2377800134046639811]], [[(-73084142313009464), 23204284934843885], [(-275743575423076043)]], [[96973079576865, (-1767667138892732), (-8251798817132)], [(-882957180507897), 511016044903577], [121183364834052]], [[(-1365051876151), (-1490985726315), 1517711796280, (-23656285709)], [(-5192008454081), (-41821748640676), 619378867941], [(-5738451766861), (-5791601546502)], [3514493432069]], [[2244358079, 14615470726, (-87183864278), 5227905395, 26778888], [(-59428262328), 201334577638, (-80135111799), (-2235984990)], [(-264549033553), 370121272026, 38358104002], [(-246187119917), (-145977681672)], [(-9705328445)]]], r3 := 960594652580, Vm := [[[2324271783498857746]], [[(-74076881121310016), 0], [(-256410024610341664)]], [[290723800960353, 0, 0], [(-2811039310162716), 0], [2220432313265911]], [[8750069351472, 0, 0, 0], [(-10529014131287), 0, 0], [(-129257355207848), 0], [245415581253237]], [[266345035246, 0, 0, 0, 0], [1005656160747, 0, 0, 0], [(-6826008435011), 0, 0], [(-3816839216204), 0], [26019111196331]]], rm := 163171802562877 }
noncomputable def w7 : Wit := { Z0 := { p := [[[465804243865895579]], [[(-36176906009192152), 11943698560663989], [6697997878385495]], [[33784496875085, (-927612974594671), 0], [(-493878534696336), 171743535343217], [59887089347005]], [[(-567848385639), 866269150643, 0, 0], [(-1393640303359), (-12663552171701), 0], [(-3940236792051), 1535566393512], [865453191821]], [[1347236082, (-14560215017), 0, 0, 0], [(-18568393712), (-35734366753), 0, 0], [(-44099695703), (-101031712617), 0], [(-54324707411), 22191107482], [9509979001]]], r := 13309581990, ok := true }, Z1 := { p := [[[764396707882495309]], [[(-59367230374058915), 0], [10991586261965941]], [[55441225641165, 0, 0], [(-810467338988859), 0], [98276249184829]], [[(-931853761048), 0, 0, 0], [(-2286999472179), 0, 0], [(-6466029607468), 0], [1420230878887]], [[2210848956, 0, 0, 0, 0], [(-30471210194), 0, 0, 0], [(-72368731410), 0, 0], [(-89148237802), 0], [15606119386]]], r := 10588309796, ok := true }, Z2 := { p := [[[1923696270075013099]], [[(-37259236462907508), 11943698560663989], [(-288626790500427848)]], [[56268324995980, (-927612974594671), 0], [(-192239326439908), 171743535343217], [1060098650088003]], [[(-615596848891), 866269150643, 0, 0], [(-5492700320740), (-12663552171701), 0], [(-20332552856175), 1535566393512], [(-50865939275706)]], [[1890908646, (-14560215017), 0, 0, 0], [(-6418751308), (-35734366753), 0, 0], [(-107951158865), (-101031712617), 0], [(-155336575741), 22191107482], [374332206065]]], r := 40284330511, ok := true }, Z3 := { p := [[[2406726345002679560]], [[(-75778041777982747), 24059600585992143], [(-285907551448417137)]], [[185422335182403, (-1886719447062904), 0], [(-275044648811646), 326506020977835], [1333862590737280]], [[(-2597088644689), 3542313098378, 0, 0], [(-15008724118692), (-22836006995930), 0], [(-39341176515560), 2575171234744], [(-48789750113670)]], [[11546284206, (-62314212252), 0, 0, 0], [(-14685505471), (-154514555039), 0, 0], [(-226682377516), (-131649946546), 0], [(-224727252175), 35482211336], [450993682677]]], r := 77965494848, ok := true }, iE := { p := [[[18661017935476704259]], [[(-13853829807556566), 0], [(-47953704153469946)]], [[287792999947466, 0, 0], [1090215904170960, 0], [3211967146790788]], [[(-611180329624), 0, 0, 0], [5090631767018, 0, 0], [8221535213407, 0], [(-19768394226195)]], [[6959008811, 0, 0, 0, 0], [33279356849, 0, 0, 0], [200827624929, 0, 0], [351355128059, 0], [716045661176]]], r := 82204460076, ok := true }, iHu := { p := [[[18795544603507020281]], [[(-28108586784377802), 0], [(-63499543510470910)]], [[605083191624429, 0, 0], [2257445830703495, 0], [3088006978958421]], [[(-2135479896100), 0, 0, 0], [6038635480794, 0, 0], [13641760057099, 0], [(-24620125562667)]], [[26127739807, 0, 0, 0, 0], [127514884148, 0, 0, 0], [483274345157, 0, 0], [650764816516, 0], [680500127495]]], r := 133809077515, ok := true }, T := { p := [[[11240984669916758016]], [[0, 288230376151711744], [0]]], r := 0, ok := true }, E := { p := [[[18234930596900784469]], [[13537505076923122, 0], [46858776414358532]], [[(-271171653468111), 0, 0], [(-995747626714367), 0], [(-3018214027489434)]], [[187131579385, 0, 0, 0], [(-7924023868904), 0, 0], [(-17901003074303), 0], [3495624087848]], [[(-2035762106), 0, 0, 0, 0], [(-8880632002), 0, 0, 0], [(-97245830578), 0, 0], [(-45321790426), 0], [(-121573633168)]]], r := 59266364993, ok := true }, de := { p := [[[(-4296338657245683438)]], [[172121118466693768, 0], [388835359635412313]], [[(-178167387697608), 0, 0], [2112318362767844, 0], [(-909266930975168)]], [[2584323592408, 0, 0, 0], [11475008008197, 0, 0], [25922959979775, 0], [29794881916693]], [[(-7643507937), 0, 0, 0, 0], [62337103682, 0, 0, 0], [308482577799, 0, 0], [318133793636, 0], [(-199076084012)]]], r := 52291800312, ok := true }, dde := { p := [[[(-54625325035512071235)]], [[113088406006299838, 0], [255475745287839581]], [[(-2460526357657441), 0, 0], [(-9200298647323713), 0], [(-12557153577442976)]], [[9703146462883, 0, 0, 0], [(-17647123626189), 0, 0], [(-39866262332291), 0], [111868383638563]], [[(-120373473144), 0, 0, 0, 0], [(-594352847650), 0, 0, 0], [(-2163587755398), 0, 0], [(-3033245290758), 0], [(-3135141593634)]]], r := 1207285475370, ok := true }, nJu := { p := [[[(-8592677314491366875)]], [[344242236933387536, 0], [777670719270824626]], [[(-356334775395216), 0, 0], [4224636725535688, 0], [(-1818533861950335)]], [[5168647184817, 0, 0, 0], [22950016016394, 0, 0], [51845919959551, 0], [59589763833386]], [[(-15287015873), 0, 0, 0, 0], [124674207365, 0, 0, 0], [616965155599, 0, 0], [636267587272, 0], [(-398152168024)]]], r := 104583600616, ok := true }, Jd1 := { p := [[[(-109250650071024142469)]], [[226176812012599677, 0], [510951490575679163]], [[(-4921052715314882), 0, 0], [(-18400597294647426), 0], [(-25114307154885951)]], [[19406292925766, 0, 0, 0], [(-35294247252377), 0, 0], [(-79732524664581), 0], [223736767277126]], [[(-240746946288), 0, 0, 0, 0], [(-1188705695300), 0, 0, 0], [(-4327175510795), 0, 0], [(-6066490581515), 0], [(-6270283187267)]]], r := 2414570950730, ok := true }, term0 := { p := [[[334966333343939211284]], [[(-1331730220377283117), 0], [(-2728091447606668531)]], [[31383329365913755, 0, 0], [107021847636008920, 0], [132599174531214886]], [[(-176263709263928), 0, 0, 0], [(-58565242549289), 0, 0], [(-176058174071900), 0], [(-1663820639608064)]], [[2372357392458, 0, 0, 0, 0], [11280993095039, 0, 0, 0], [35520207054720, 0, 0], [50913709329754, 0], [48024625338175]]], r := 9864185379154, ok := true }, r0 := { p := [[[40804480881504555153]], [[(-128257347179953206), 2089440589516350220], [(-163154293961272612)]], [[3513897660586361, (-6087972521021622), 26629144800355588], [6414689519442805, (-8443300559334466)], [6467025572465692]], [[(-14393329644574), 159578064108612, (-53038572950003), (-4052208420132)], [47075684795620, 340194153551417, (-112152221906087)], [24876686437592, 330082091095775], [(-61165906597732)]], [[198089011913, (-611830287795), 998029812303, 637180621242, (-25550319730)], [593896376820, 2030937082930, 4933413715694, (-99412920296)], [2073160935894, 1491281180495, 4152243951825], [1775887789720, (-3163078849754)], [1412889293437]]], r := 2824570312126, ok := true }, r1 := { p := [[[109610484814481517135]], [[(-302127995638780412), 0], [(-446121644509979108)]], [[7657713123785142, 0, 0], [18261050693438081, 0], [17278033690114431]], [[(-29076419218524), 0, 0, 0], [94116335292351, 0, 0], [85778898404524, 0], [(-167030071584581)]], [[380622004511, 0, 0, 0, 0], [1402281631464, 0, 0, 0], [5097408787538, 0, 0], [5070806565043, 0], [3765973589456]]], r := 3683902801637, ok := true }, r2 := { p := [[[43867930385298584974]], [[(-251595639281638197), 2107897077052309018], [(-1084814263902195580)]], [[4034302614317377, (-7456207821833693), 25526169221870453], [31379021633822869, (-11762636688889644)], [71122995050435830]], [[(-22434631044590), 158339253939426, 6097688287741, (-9738688038738)], [(-94295465252468), 575307167553840, 172627565840215], [(-121784193933325), 245239857547358], [(-741212876260813)]], [[237438641913, (-608244997691), 734543883432, 1049698087206, (-20778579403)], [2145645225165, 2590532282509, (-6302283127968), 861766336439], [9045680449388, 9682425080979, (-8575820485140)], [19133501770218, (-1057428769670)], [24396623296934]]], r := 30542429218356, ok := true }, r3 := { p := [[[176097436755370291266]], [[(-1345831067170009028), 8480956991146918064], [(-3690263975736784252)]], [[28343696503546997, (-37330247158590739), 99411465867002615], [133263024958367242, (-45775273828017866)], [204652958025681877]], [[(-181078316720411), 925187683808621, 340881118307259, (-106167751152296)], [(-368212040902576), 2074624980191723, 912431410529770], [(-503930670741773), 998305718461882], [(-2428953153705527)]], [[2298013969626, (-3105320984425), (-6315856332067), 12609083839302, (-282618838995)], [13312924210551, 20416862376494, (-40243379064663), 5202850216620], [43761619414379, 35927988057329, (-28899990194512)], [72339844333787, (-5915148781678)], [72918530994747]]], r := 242469270177548, ok := true }, eta := { p := [[[(-221565236751226403076)]], [[684840034098830472, 0], [1641495053173457254]], [[(-15093004471813690), 0, 0], [(-57174824558597318), 0], [(-87918924604520003)]], [[66899985745563, 0, 0, 0], [(-44819010132594), 0, 0], [(-21043800437264), 0], [999617040513723]], [[(-837781149722), 0, 0, 0, 0], [(-4244185774265), 0, 0, 0], [(-16039174163619), 0, 0], [(-26733636642535), 0], [(-31344177185470)]]], r := 91750118325967017, 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 8070450532247928832 8646911284551352320 10376293541461622784 11529215046068469760 16429131440647569408 16933534598913064960 :=
  (RegionPosI.split_s 16681333019780317184 (RegionPosI.split_t 10952754293765046272 (RegionPosI.split_b 8358680908399640576 (RegionPosI.of_check c0 q0 ok_0 8070450532247928832 8358680908399640576 10376293541461622784 10952754293765046272 16429131440647569408 16681333019780317184 (by decide +kernel)) (RegionPosI.of_check c1 q1 ok_1 8358680908399640576 8646911284551352320 10376293541461622784 10952754293765046272 16429131440647569408 16681333019780317184 (by decide +kernel))) (RegionPosI.split_b 8358680908399640576 (RegionPosI.of_check c2 q2 ok_2 8070450532247928832 8358680908399640576 10952754293765046272 11529215046068469760 16429131440647569408 16681333019780317184 (by decide +kernel)) (RegionPosI.of_check c3 q3 ok_3 8358680908399640576 8646911284551352320 10952754293765046272 11529215046068469760 16429131440647569408 16681333019780317184 (by decide +kernel)))) (RegionPosI.split_t 10952754293765046272 (RegionPosI.split_b 8358680908399640576 (RegionPosI.of_check c4 q4 ok_4 8070450532247928832 8358680908399640576 10376293541461622784 10952754293765046272 16681333019780317184 16933534598913064960 (by decide +kernel)) (RegionPosI.of_check c5 q5 ok_5 8358680908399640576 8646911284551352320 10376293541461622784 10952754293765046272 16681333019780317184 16933534598913064960 (by decide +kernel))) (RegionPosI.split_b 8358680908399640576 (RegionPosI.of_check c6 q6 ok_6 8070450532247928832 8358680908399640576 10952754293765046272 11529215046068469760 16681333019780317184 16933534598913064960 (by decide +kernel)) (RegionPosI.of_check c7 q7 ok_7 8358680908399640576 8646911284551352320 10952754293765046272 11529215046068469760 16681333019780317184 16933534598913064960 (by decide +kernel)))))

end CKLaneC.RSC2.BD_0116