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

import Definitions.Def_CK_CKLaneC_RSCell_Staged
import Definitions.Def_CK_CKLaneC_RSCell_RegionI

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

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

namespace CKLaneC.RSC2.S07_0066
open CKLaneC.TM3 CKLaneC.RSCell

noncomputable def c0 : Cell := { bc := 117093590311632896, bh := 9007199254740992, tc := 6917529027641081856, th := 2305843009213693952, sc := 12105675798371893248, sh := 576460752303423488 }
noncomputable def q0 : Cert := { V0 := [[[319721763633246230]], [[(-34359063000807311), 106527738457977408], [3960747934988602]], [[591226980994668, (-11438132997572607), (-23079576666237)], [(-416197383211393), 1318533094141601], [(-102861244602559)]], [[(-12543785609312), 195219841850382, 7437661683827, (-2557845520179)], [6427521337076, (-138183323336719), (-857377954536)], [10932105632078, (-34263767655250)], [4635020912151]], [[295253306326, (-4063518333000), (-926437839613), 822887529550, 1635870029], [(-156157972735), 2074821614834, 274177991721, (-94858526362)], [(-178368502369), 3636470421824, 11656063233], [(-493326217408), 1544014950744], [(-246688869271)]]], r0 := 98383239138835, V1 := [[[851465094612393105]], [[(-91261654054051977), 0], [10520205624633524]], [[1531568652390296, 0, 0], [(-1096523427797212), 0], [(-273726960919124)]], [[(-30615352438329), 0, 0, 0], [15505572949246, 0, 0], [28967489842581, 0], [12335837556338]], [[675648488563, 0, 0, 0, 0], [(-315701417183), 0, 0, 0], [(-452415702489), 0, 0], [(-1307705535434), 0], [(-656625160976)]]], r1 := 64146617011342, V2 := [[[18253290579208378766]], [[(-3795274378714398), 62812599757406], [(-14894610307975130)]], [[9951511289251, (-4450803410759), (-19051870269)], [(-292395277527493), 9813920821935], [(-1365940994977)]], [[(-182149126913), (-117490242142), 3077250028, 5623560], [937779224339, (-695166778035), (-4472743765)], [23765730205, 391364545907], [(-11685442070)]], [[4753791745, 329276407, (-86265872), (-1418666), (-1635)], [(-16212814213), (-18436065901), 722405240, 1759804], [10122946634, (-27737427533), (-354038425)], [1996988483, 511533737], [328569494]]], r2 := 14071895965028, V3 := [[[18292562117352341240]], [[(-7297351131957796), 99624214897372], [(-11899496404656157)]], [[2182057432173, (-4239481232766), (-60257054735)], [(-559674925944376), 15579978807428], [(-3088265913012)]], [[1425361632, (-436605334135), 8005232503, 35503377], [341122902869, (-664351058709), (-14155835078)], [130339429917, 623231914753], [(-3885426488)]], [[(-23955273), (-165342243), 36768601, (-7929589), (-20616)], [224070702, (-68270592074), 1881468502, 11117369], [13610457754, (-26807470328), (-1122295008)], [182521021, 929901875], [37757220]]], r3 := 38451867586289, Vm := [[[18253614202771853658]], [[(-3819239697647066), 0], [(-14843934719683402)]], [[9438450354890, 0, 0], [(-296158192254783), 0], [664492061768]], [[(-180349582943), 0, 0, 0], [858015572984, 0, 0], [(-128046347478), 0], [(-8740757479)]], [[4726804936, 0, 0, 0, 0], [(-15894893080), 0, 0, 0], [6986153396, 0, 0], [1730734108, 0], [298027463]]], rm := 2674442779041 }
noncomputable def w0 : Wit := { Z0 := { p := [[[319791064324820263]], [[(-34381409278254508), 106597021441606754], [3963323906639856]], [[594014022478560, (-11460469759418170), 0], [(-417021970072695), 1321107968879952], [(-102896217380674)]], [[(-12720841512692), 198004674159520, 0, 0], [6529252808089, (-139007323357565), 0], [10943454011285, (-34298739126892)], [4636509255129]], [[302373898527, (-4240280504231), 0, 0, 0], [(-162527000348), 2176417602696, 0, 0], [(-179796595902), 3647818003761, 0], [(-493807968499), 1545503085043], [(-246763343420)]]], r := 24286321308794, ok := true }, Z1 := { p := [[[852776171532854035]], [[(-91683758075345354), 0], [10568863751039617]], [[1584037393276161, 0, 0], [(-1112058586860518), 0], [(-274389913015129)]], [[(-33922244033844), 0, 0, 0], [17411340821572, 0, 0], [29182544030093, 0], [12364024680344]], [[806330396073, 0, 0, 0, 0], [(-433405334260), 0, 0, 0], [(-479457589070), 0, 0], [(-1316821249329), 0], [(-658035582452)]]], r := 16081909049200, ok := true }, Z2 := { p := [[[386180136538882775052]], [[(-6440824705347431542), 106597021441606754], [(-25277111606519743084)]], [[134928228327663626, (-11460469759418170), 0], [430284861584997870, 1321107968879952], [1815710334711939731]], [[(-3149504701641193), 198004674159520, 0, 0], [(-8803192172792859), (-139007323357565), 0], [(-31134682902413550), (-34298739126892)], [(-133956081902441083)]], [[79984973659667, (-4240280504231), 0, 0, 0], [198721550650396, 2176417602696, 0, 0], [633236475763571, 3647818003761, 0], [2306180993174418, 1545503085043], [10001145338909542]]], r := 3250526375426140, ok := true }, Z3 := { p := [[[468531222184077848430]], [[(-18930606034973854895), 258442649896133512], [(-30869376350086306071)]], [[844362946530959532, (-33898062790211284), 0], [1283381392603874545, 3074911133828433], [2222140754409202915]], [[(-38616900141924264), 1409939460200848, 0, 0], [(-57760817508953076), (-380360182042561), 0], [(-93249531608873772), (-81433805039980)], [(-164136850792181521)]], [[1786426326521575, (-63430142861964), 0, 0, 0], [2655225399606060, 13395559040051, 0, 0], [4209879137861739, 10358106562324, 0], [6923627515266068, 3679218101391], [12264484890335876]]], r := 14325059766890237, ok := true }, iE := { p := [[[390821952290749105543]], [[(-6488820905217445384), 0], [(-25219583359511243348)]], [[136061558307131066, 0, 0], [429821867314712970, 0], [1814216780526323295]], [[(-3177118370693952), 0, 0, 0], [(-8788420555398853), 0, 0], [(-31120968864158573), 0], [(-133888782268101481)]], [[80707202923252, 0, 0, 0, 0], [198298889360700, 0, 0, 0], [632868291138181, 0, 0], [2305552945109979, 0], [9997563531591426]]], r := 3253535296942661, ok := true }, iHu := { p := [[[473770559541063100538]], [[(-19071024461841442483), 0], [(-30807039515282329638)]], [[850936026929738431, 0, 0], [1282176051477508248, 0], [2220489869088846958]], [[(-38920720421818490), 0, 0, 0], [(-57702564055004204), 0, 0], [(-93211834242699005), 0], [(-164062263007035120)]], [[1800547878814330, 0, 0, 0, 0], [2652604658075989, 0, 0, 0], [4208135746303031, 0, 0], [6921885527882037, 0], [12260507405896504]]], r := 14359743316449147, ok := true }, T := { p := [[[6917529027641081856]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[870683862373697753]], [[14455973148107243, 0], [56184879375913311]], [[(-63108999364467), 0, 0], [908107321138432, 0], [(-416174229041009)]], [[997539836665, 0, 0, 0], [(-4874845309157), 0, 0], [(-7874750114792), 0], [10612276031022]], [[(-23751365834), 0, 0, 0, 0], [76731136916, 0, 0, 0], [(-1568603213), 0, 0], [200227404612, 0], [(-408177426086)]]], r := 630276997768, ok := true }, de := { p := [[[(-72875896633412014143)]], [[636294058823037278, 0], [1027859633483367911]], [[(-15086485554386608), 0, 0], [204743502984598, 0], [(-39367693073872745)]], [[478944465026337, 0, 0, 0], [40783683539, 0, 0], [65881334948, 0], [2018891529635369]], [[(-17105158207961), 0, 0, 0, 0], [8123867, 0, 0, 0], [1588287967, 0, 0], [21198965, 0], [(-116474502763998)]]], r := 42245867585799, ok := true }, dde := { p := [[[(-3207705187617428539097)]], [[152108910352658569636, 0], [245714393646602304740]], [[(-7243408721530617471), 0, 0], [(-11701096611663644593), 0], [(-18901439326597647523)]], [[344924199482139217, 0, 0, 0], [557185163408731862, 0, 0], [900068340891028574, 0], [1453956764407869150]], [[(-16424961885151594), 0, 0, 0, 0], [(-26532630762026478), 0, 0, 0], [(-42860406715344151), 0, 0], [(-69236036485525034), 0], [(-111842828065762029)]]], r := 23435887399614271, ok := true }, nJu := { p := [[[(-145751793266824028286)]], [[1272588117646074556, 0], [2055719266966735822]], [[(-30172971108773215), 0, 0], [409487005969197, 0], [(-78735386147745490)]], [[957888930052675, 0, 0, 0], [81567367079, 0, 0], [131762669896, 0], [4037783059270738]], [[(-34210316415922), 0, 0, 0, 0], [16247734, 0, 0, 0], [3176575934, 0, 0], [42397931, 0], [(-232949005527995)]]], r := 84491735171592, ok := true }, Jd1 := { p := [[[(-6415410375234857078193)]], [[304217820705317139272, 0], [491428787293204609480]], [[(-14486817443061234941), 0, 0], [(-23402193223327289185), 0], [(-37802878653195295045)]], [[689848398964278435, 0, 0, 0], [1114370326817463725, 0, 0], [1800136681782057149, 0], [2907913528815738301]], [[(-32849923770303187), 0, 0, 0, 0], [(-53065261524052956), 0, 0, 0], [(-85720813430688302), 0, 0], [(-138472072971050067), 0], [(-223685656131524058)]]], r := 46871774799228531, ok := true }, term0 := { p := [[[781346974048759233803500]], [[(-73951278694628347828459), 0], [(-119085335958146940755070)]], [[5271370416551479068820, 0, 0], [11306361587873524691551, 0], [13697865161996835381815]], [[(-334345260673955882443), 0, 0, 0], [(-806761374323535932356), 0, 0], [(-1301858379658859732377), 0], [(-1402716772049261868487)]], [[19889184890200445830, 0, 0, 0, 0], [51196411817975641508, 0, 0, 0], [92925593755991533661, 0, 0], [133384365420018440595, 0], [134750123784627546442]]], r := 50537165990888716211, ok := true }, r0 := { p := [[[446054706685594557038]], [[(-23937346269841914115), 297162568027104547971], [(-28990299136665893848)]], [[1041381827893425084, (-15902721597175222275), 49389043632565230085], [1572157326566329508, (-19318521124996513241)], [2089218583997471565]], [[(-41780645083340161), 688272349187991686, (-2613498858913689485), (-45946012719804004)], [(-66521938223656461), 1045847567992602660, (-3214191863489222936)], [(-113610296599433164), 1392276309921339016], [(-154348249511835288)]], [[1638919056873959, (-27469779484695716), 110734743934709397, 12284000820307710, (-3799287024153077)], [2576925587031228, (-44102110425840948), 172803866305870301, 1852783014820441], [4774224487156383, (-75595156398320968), 231688782615100498], [8406812769130390, (-102862079289726466)], [11533780006750579]]], r := 147784527247527867, ok := true }, r1 := { p := [[[3158499226543233872607]], [[(-166633271415931164379), 0], [(-205610260792457264615)]], [[7021831959019438313, 0, 0], [11033131170755611715, 0], [14821791035035840830]], [[(-272865431476685872), 0, 0, 0], [(-457124971134125033), 0, 0], [(-798475090599184949), 0], [(-1095196370218253295)]], [[10433867145134818, 0, 0, 0, 0], [17307739755567375, 0, 0, 0], [32927287058485121, 0, 0], [59135467695032210, 0], [81848643678810076]]], r := 165116830685860239, ok := true }, r2 := { p := [[[328321436051297829734531]], [[(-18008531893299899058371), 731131739679577878197], [(-49415429060099093723909)]], [[815348444057718807282, (-28813310678068812116), 478917419514483998], [2662606688231356525594, (-55878820331903346409)], [5628268201162484241374]], [[(-35588861712109770052), 1099585044346403792, 769278718392878, (-135530321267897)], [(-118605168050254496478), 2107910443222026585, 979919232073959], [(-299968255314389088541), 4294303226331216800], [(-572110482155126868119)]], [[1557641984617009711, (-42832633761423411), (-14025095784753), 12120244287904, 38019805014], [5109877223511195640, (-77265519113270199), 26044900176501, (-10909048280256)], [13229026948229495429, (-159432558441966250), (-15841463858150)], [30256694380245267168, (-330061660339912027)], [54640926058102092095]]], r := 397024486644827443963, ok := true }, r3 := { p := [[[1526858553742337843940412]], [[(-145163946600478422587967), 3922258175358666575949], [(-235411624163568104279665)]], [[10362957046759618108188, (-301490492204993655527), 1880754935057152208], [22401374232112717502296, (-303765369619675217253)], [27183155681273664339367]], [[(-657779021605816079490), 19815685653478772862, 7746778980796456, (-1066488803150605)], [(-1599657939439434838444), 23323973660282033162, 2864481062616008], [(-2587444439787944960067), 23433741720627175222], [(-2789068183873699137605)]], [[39146842722221111659, (-1203444375796028557), (-279254292935209), 93248784704380, 598107088923], [101551593151619170653, (-1531215812778187909), 216092210255352, (-85180493399043)], [184783801727511273996, (-1797196830268843338), (-53846879704574)], [265516347341443600378, (-1805279356302695275)], [268240692018652935569]]], r := 7196786365901681435346, ok := true }, eta := { p := [[[(-336680014092264064781973)]], [[18456971486626120391419, 0], [50041634903730352627376]], [[(-837084865069995007860), 0, 0], [(-2695923797533640915520), 0], [(-5676119558554689756361)]], [[36614049638348178417, 0, 0, 0], [120203342737042809775, 0, 0], [302500659234630042566, 0], [575776783285157271504]], [[(-1605737170987076769), 0, 0, 0, 0], [(-5184775987418961423), 0, 0, 0], [(-13350082420383043339), 0, 0], [(-30450134271392427573), 0], [(-54922175124766298400)]]], r := 49348097707339029451, 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 := 117093590311632896, bh := 9007199254740992, tc := 6917529027641081856, th := 2305843009213693952, sc := 13258597302978740224, sh := 576460752303423488 }
noncomputable def q1 : Cert := { V0 := [[[253272689978443946]], [[(-32135799799859529), 84401271299729783], [3152878758212466]], [[522491722471020, (-10703194543283786), (-11475665203504)], [(-392233450291908), 1050102220287123], [(-81679860189593)]], [[(-10453944399298), 172913172337989, 4367026356806, (-1273029429053)], [5584191834205, (-130420280541402), (-428453771891)], [10263853532255, (-27215080432290)], [3679422532274]], [[230634442987, (-3398887880618), (-624737063656), 483928382491, 510709016], [(-126360786499), 1815484032859, 161956670884, (-47478747291)], [(-156486642705), 3416866298095, 5769583465], [(-462930899933), 1225982296924], [(-195783434083)]]], r0 := 84397020087734, V1 := [[[674833450890471066]], [[(-85482374894159059), 0], [8386770072127685]], [[1362878506169095, 0, 0], [(-1038063236452234), 0], [(-217530934058524)]], [[(-25802033909119), 0, 0, 0], [13777523296206, 0, 0], [27262314309735, 0], [9799779273161]], [[534865628575, 0, 0, 0, 0], [(-262621017437), 0, 0, 0], [(-401710664670), 0, 0], [(-1229895979250), 0], [(-521488070469)]]], r1 := 53389486077980, V2 := [[[18245738451082371404]], [[(-3757512574958447), 53443564745890], [(-15475773083449279)]], [[8962325518090, (-4917013322639), (-13269243119)], [(-288826162343336), 8350285142661], [(-1278787434173)]], [[(-149155203171), (-115661597107), 2692051319, 3205544], [849698872554, (-768255910409), (-3115165150)], [62973231718, 332952870316], [(-8076155451)]], [[3568567088, 282320672, (-106256172), (-1006036), (-762)], [(-13287071126), (-18116373750), 632032028, 1003087], [9500484939, (-30663441498), (-246554150)], [1618375321, 428736547], [219329319]]], r2 := 13930971087264, V3 := [[[18277976154352975848]], [[(-7288606526805427), 89397584260099], [(-13017480038720846)]], [[2190071770075, (-5987736356514), (-44292097735)], [(-558307876908051), 13978074716240], [(-2773086008877)]], [[1251813749, (-437486468441), 7863263526, 21368642], [342370331003, (-937606199738), (-10403894470)], [184868388576, 558720005805], [(-3452696108)]], [[(-19649443), (-129547373), (-107918897), (-6160029), (-10158)], [192755781, (-68350469965), 1847785803, 6690297], [13652360644, (-37701055354), (-824503748)], [249659724, 802857044], [35139382]]], r3 := 35272481507697, Vm := [[[18246012105746960981]], [[(-3783509361732072), 0], [(-15432939907424707)]], [[8459458462677, 0, 0], [(-292904458266376), 0], [435601543171]], [[(-147549931306), 0, 0, 0], [771738363903, 0, 0], [(-101196824510), 0], [(-5670126868)]], [[3546732040, 0, 0, 0, 0], [(-13002747933), 0, 0, 0], [6456645641, 0, 0], [1346648873, 0], [193661970]]], rm := 2677329599689 }
noncomputable def w1 : Wit := { Z0 := { p := [[[253307136303466814]], [[(-32148913141430372), 84435712101155604], [3154165322615575]], [[524369244692771, (-10716304380476791), 0], [(-392720080550576), 1051388440871858], [(-81697170155554)]], [[(-10582799156718), 174789748230923, 0, 0], [5653149263838, (-130906693516859), 0], [10270481227946, (-27232390051852)], [3680160449425]], [[235696067106, (-3527599718906), 0, 0, 0], [(-131015290039), 1884383087946, 0, 0], [(-157443996881), 3423493742648, 0], [(-463212778709), 1226720149808], [(-195820353567)]]], r := 20891496471208, ok := true }, Z1 := { p := [[[675485696809244837]], [[(-85730435043814324), 0], [8411107526974866]], [[1398317985847390, 0, 0], [(-1047253548134869), 0], [(-217859120414810)]], [[(-28220797751247), 0, 0, 0], [15075064703568, 0, 0], [27387949941191, 0], [9813761198468]], [[628522845618, 0, 0, 0, 0], [(-349374106769), 0, 0, 0], [(-419850658348), 0, 0], [(-1235234076556), 0], [(-522187609511)]]], r := 13366769505995, ok := true }, Z2 := { p := [[[373814217617887894125]], [[(-5936509877366767209), 84435712101155604], [(-24450238804802766785)]], [[117789962589480434, (-10716304380476791), 0], [397310739853364664, 1051388440871858], [1755865903873282276]], [[(-2587897194151436), 174789748230923, 0, 0], [(-7718121976394575), (-130906693516859), 0], [(-28761277859715775), (-27232390051852)], [(-129522779848941080)]], [[61456679554104, (-3527599718906), 0, 0, 0], [164420908794406, 1884383087946, 0, 0], [555880902103940, 3423493742648, 0], [2130905518026320, 1226720149808], [9669226677783319]]], r := 2983677837901703, ok := true }, Z3 := { p := [[[433764675352947810930]], [[(-15965372794703630204), 195821485823021040], [(-28514218856712260410)]], [[649705981025137594, (-28935984745826238), 0], [1080670151216500554, 2363578666244806], [2051062044553960407]], [[(-27119071981684747), 1089787444798145, 0, 0], [(-44384550427175442), (-332899150574850), 0], [(-78478458072850741), (-62170148911810)], [(-151436496863891477)]], [[1145114790483935, (-44668524406413), 0, 0, 0], [1862324068832495, 10498221462935, 0, 0], [3233384560782046, 8962932158204, 0], [5825066976540002, 2806110746389], [11312233550746337]]], r := 11027277272547259, ok := true }, iE := { p := [[[378364364325561279492]], [[(-5980282519650588448), 0], [(-24393580649933561085)]], [[118773459530230037, 0, 0], [396902136946269651, 0], [1754398380631599186]], [[(-2610454936176648), 0, 0, 0], [(-7705610553060321), 0, 0], [(-28748925187121762), 0], [(-129456673263090285)]], [[62008196924516, 0, 0, 0, 0], [164085771836098, 0, 0, 0], [555566425177231, 0, 0], [2130338926960660, 0], [9665709164024808]]], r := 2987111766082759, ok := true }, iHu := { p := [[[438747244270000235171]], [[(-16082740253845043647), 0], [(-28454078910648920345)]], [[654748860078457955, 0, 0], [1079669793058770982, 0], [2049480159653871034]], [[(-27332055392946271), 0, 0, 0], [(-44339546304335641), 0, 0], [(-78446889615361415), 0], [(-151365096934900009)]], [[1154155511605628, 0, 0, 0, 0], [1860472376071827, 0, 0, 0], [3232040294027145, 0, 0], [5823608798476215, 0], [11308428714800711]]], r := 11054494037194065, ok := true }, T := { p := [[[6917529027641081856]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[899350993393618336]], [[14214798041060917, 0], [57982180824694001]], [[(-57644225060324), 0, 0], [889474129868156, 0], [(-431930006184092)]], [[831594564338, 0, 0, 0], [(-4454494244716), 0, 0], [(-7881028279114), 0], [11012728756079]], [[(-18078524210), 0, 0, 0, 0], [63966112742, 0, 0, 0], [(-1570479446), 0, 0], [200225287811, 0], [(-423580350170)]]], r := 641253751117, ok := true }, de := { p := [[[(-71660077262997551610)]], [[581195682085136749, 0], [1028269283689088093]], [[(-12576780315799920), 0, 0], [204906735256959, 0], [(-39367554953006849)]], [[364552050052937, 0, 0, 0], [40832465600, 0, 0], [72242054523, 0], [2018891576237634]], [[(-11887565699783), 0, 0, 0, 0], [8136825, 0, 0, 0], [1592073328, 0, 0], [25469707, 0], [(-116474502748263)]]], r := 40986211629383, ok := true }, dde := { p := [[[(-2929941555471655531439)]], [[126804903811732850468, 0], [224347137513065812097]], [[(-5513373035139060839), 0, 0], [(-9754635061897227619), 0], [(-17257836305257770780)]], [[239711847908004597, 0, 0, 0], [424105495028782550, 0, 0], [750340491204768819, 0], [1327525741236544361]], [[(-10422254261489608), 0, 0, 0, 0], [(-18439372948696602), 0, 0, 0], [(-32623509170434258), 0, 0], [(-57718510590890925), 0], [(-102117364755771473)]]], r := 19224258207581700, ok := true }, nJu := { p := [[[(-143320154525995103220)]], [[1162391364170273498, 0], [2056538567378176186]], [[(-25153560631599839), 0, 0], [409813470513918, 0], [(-78735109906013697)]], [[729104100105875, 0, 0, 0], [81664931201, 0, 0], [144484109047, 0], [4037783152475269]], [[(-23775131399566), 0, 0, 0, 0], [16273651, 0, 0, 0], [3184146656, 0, 0], [50939414, 0], [(-232949005496525)]]], r := 81972423258757, ok := true }, Jd1 := { p := [[[(-5859883110943311062877)]], [[253609807623465700937, 0], [448694275026131624195]], [[(-11026746070278121678), 0, 0], [(-19509270123794455238), 0], [(-34515672610515541559)]], [[479423695816009194, 0, 0, 0], [848210990057565100, 0, 0], [1500680982409537638, 0], [2655051482473088723]], [[(-20844508522979216), 0, 0, 0, 0], [(-36878745897393203), 0, 0, 0], [(-65247018340868515), 0, 0], [(-115437021181781849), 0], [(-204234729511542945)]]], r := 38448516415163391, ok := true }, term0 := { p := [[[652140650676851515840522]], [[(-56321626103685844863531), 0], [(-99333818727907613777843)]], [[3664880691572872343334, 0, 0], [8608463833416722134438, 0], [11423705329788904167813]], [[(-212217139558997346466), 0, 0, 0], [(-560785300694299554451), 0, 0], [(-991114656932920544095), 0], [(-1169718894187600782278)]], [[11525723502791111671, 0, 0, 0, 0], [32490853464179259145, 0, 0, 0], [64588977251192189738, 0, 0], [101541530920534716286, 0], [112360863488388251231]]], r := 36982462963356379266, ok := true }, r0 := { p := [[[402035605046659595577]], [[(-20225455298693622709), 267906372547222173745], [(-26092905117545545843)]], [[825421639320036904, (-13448014915540067217), 44572857220559071713], [1334147163936817633, (-17390571102263264364)], [1879732196142557469]], [[(-30891137028429238), 546192913051743561, (-2217608963293302782), (-26043038026074187)], [(-53132535210066943), 887990771567445237, (-2895296440593860919)], [(-96510083535668185), 1252852970455490700], [(-138842069323487072)]], [[1122964903294640, (-20337311120195974), 88311699200847115, 7894887857778704, (-2159739466878096)], [1925768935968265, (-35254060867677015), 147038341603945653, 1043642510101854], [3821586078820469, (-64247501456612051), 208607651559276563], [7145847222084010, (-92540692939492247)], [10373539583284788]]], r := 116728349450532171, ok := true }, r1 := { p := [[[2851292032531988879497]], [[(-141515997476158500816), 0], [(-185243587662808934830)]], [[5606144730263825588, 0, 0], [9393554230731826440, 0], [13347334421839732164]], [[(-203329483242078863), 0, 0, 0], [(-366952148421973937), 0, 0], [(-680274614132932971), 0], [(-985974542080411348)]], [[7196024087267387, 0, 0, 0, 0], [13007660969255339, 0, 0, 0], [26476819249788286, 0, 0], [50402093423745651, 0], [73672032578350759]]], r := 124773628687991644, ok := true }, r2 := { p := [[[295303949223764930964329]], [[(-15129346867145294201020), 677586294162459262048], [(-44527015114217071066368)]], [[634333554354156314721, (-24878945798340945710), 480403252350117465], [2243120578646713278138, (-51950496235312197231)], [5077083253211239449951]], [[(-25462678931938613803), 878918464431548738, 718129140488370, (-111209238161465)], [(-92574784582345937239), 1830416766098121759, 1030857836374498], [(-253134158841655081369), 3996873756969491596], [(-516481798488803807113)]], [[1019915396342240650, (-31474673573666825), (-11658511463597), 12199771475926, 25531649209], [3667811130382349826, (-62231618422097654), 24934738875889, (-8964749963343)], [10346205607827689568, (-138733231613037744), (-16177963766843)], [25563048573286122560, (-307397809422784084)], [49356991007301775812]]], r := 337192269731835672111, ok := true }, r3 := { p := [[[1273282201932379349797677]], [[(-110510545883534715644632), 3389914620478097981630], [(-196281858041649026362954)]], [[7202718125547079231603, (-234715352808036781907), 1895236855126620173], [17052308118015250882070, (-262576122419621736129)], [22663575280901393160462]], [[(-417419301489591984768), 13999392843875569071, 6782827528231294, (-878374092455494)], [(-1111772030210591379766), 18163583230596387705, 3282802358621462], [(-1969554513592629586038), 20259870883809934300], [(-2325284338361597754516)]], [[22681602816523630652, (-773539842564759321), (-207486803187220), 94823828049468, 403094850920], [64440834458110105530, (-1081986977658767618), 202953987881413, (-70365172607988)], [128423589382432355583, (-1399652017645032568), (-58151176888357)], [202107539841363800423, (-1560895756016666873)], [223632380745491060480]]], r := 4917986274729053100633, ok := true }, eta := { p := [[[(-302845095725519869422543)]], [[15501766284373716256780, 0], [45092431469663989669465]], [[(-650914972375818868808), 0, 0], [(-2270843524841248669921), 0], [(-5120312599787437209797)]], [[26178873773595253822, 0, 0, 0], [93796105334371113453, 0, 0], [255242709765851776552, 0], [519794976780195922210]], [[(-1050626145105413910), 0, 0, 0, 0], [(-3720205787715593180), 0, 0, 0], [(-10438769315812577387), 0, 0], [(-25724173986026805348), 0], [(-49611204958669516169)]]], r := 42499629371013241141, 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 := 135107988821114880, bh := 9007199254740992, tc := 6917529027641081856, th := 2305843009213693952, sc := 12105675798371893248, sh := 576460752303423488 }
noncomputable def q2 : Cert := { V0 := [[[327265356295493066]], [[(-35151298970762768), 109038922945074305], [3598028582610759]], [[603427199254243, (-11701141301039858), (-24751317706539)], [(-377654330132263), 1197709390066247], [(-80004211066479)]], [[(-12841303356571), 199154724703491, 7972058117356, (-2742784542118)], [5799230064055, (-125362497176744), (-816006628728)], [8499828460689, (-26649704292035)], [3119956145927]], [[303441487284, (-4154460441360), (-992186159607), 881831968573, 1837993103], [(-141955500605), 1868772219603, 260750233146, (-90262855739)], [(-138425260490), 2827312606411, 9182848206], [(-331928178294), 1039301687537], [(-143750687403)]]], r0 := 62168885184304, V1 := [[[871499866458234492]], [[(-93348292952778424), 0], [9554976231785357]], [[1560919401923632, 0, 0], [(-994398165106694), 0], [(-212895662893183)]], [[(-31212795299117), 0, 0, 0], [13912683965493, 0, 0], [22520474481008, 0], [8303191927017]], [[689950117967, 0, 0, 0, 0], [(-283123359744), 0, 0, 0], [(-350787510378), 0, 0], [(-879745017815), 0], [(-382611778412)]]], r1 := 36640004390456, V2 := [[[18223495806212214976]], [[(-4379954798530982), 84009915583243], [(-14900204741014327)]], [[11866816109317, (-5952399910788), (-29491369560)], [(-292278024038421), 11385366678793], [(-1429101903147)]], [[(-215018444109), (-157328657119), 4763444132, 10067998], [977175770816, (-806584362457), (-6005818395)], [34458608062, 394322906982], [(-9504653850)]], [[5607938528, 455883845, (-133477720), (-2539993), (-3384)], [(-16650613140), (-21405772848), 970113459, 2732831], [9597340664, (-27969437904), (-412631741)], [1593206943, 476003276], [225621174]]], r2 := 9003882734100, V3 := [[[18268750740970586219]], [[(-8416178179438386), 133284428863297], [(-11911894957990270)]], [[2918879493755, (-5675865626317), (-93306209247)], [(-559151404540270), 18083846975184], [(-3110743717997)]], [[1903804907, (-584077195189), 12398945137, 63590104], [395764906003, (-772258580438), (-19017965546)], [131415106846, 628650919311], [(-3617970934)]], [[(-33521105), (-195333709), 56677198, (-14205780), (-42695)], [253820291, (-79214802342), 2528952693, 17275393], [13709111987, (-27145373860), (-1309261486)], [176343452, 878568701], [29632403]]], r3 := 27941272258590, Vm := [[[18223928925776954331]], [[(-4412055289583973), 0], [(-14841373003251615)]], [[11181666355018, 0, 0], [(-296651311653756), 0], [618323528081]], [[(-212516283166), 0, 0, 0], [884843769360, 0, 0], [(-118899217529), 0], [(-6776551708)]], [[5570676337, 0, 0, 0, 0], [(-16265224741), 0, 0, 0], [6450291403, 0, 0], [1343520233, 0], [201597857]]], rm := 1741468358004 }
noncomputable def w2 : Wit := { Z0 := { p := [[[327339679872721633]], [[(-35175252534962183), 109113226624240544], [3600480429659615]], [[606412431053142, (-11725084178320728), 0], [(-378438626711056), 1200160143219871], [(-80031760562738)]], [[(-13030758485736), 202137477017714, 0, 0], [5895889139489, (-126146208903686), 0], [8508774129953, (-26677253520913)], [3120981902523]], [[311056289080, (-4343586161912), 0, 0, 0], [(-147998509438), 1965296379829, 0, 0], [(-139552043472), 2836258043317, 0], [(-332260175904), 1040327300841], [(-143795144127)]]], r := 15225919630106, ok := true }, Z1 := { p := [[[872905812993924356]], [[(-93800673426565821), 0], [9601281145758975]], [[1617099816141713, 0, 0], [(-1009169671229482), 0], [(-213418028167301)]], [[(-34748689295296), 0, 0, 0], [15722371038637, 0, 0], [22690064346542, 0], [8322618406729]], [[829483437547, 0, 0, 0, 0], [(-394662691835), 0, 0, 0], [(-372138782592), 0, 0], [(-886027135742), 0], [(-383453717670)]]], r := 9181114851433, ok := true }, Z2 := { p := [[[341956223194391868428]], [[(-5688745158450884851), 109113226624240544], [(-19352589576678159726)]], [[119529376906377033, (-11725084178320728), 0], [328775525209423695, 1200160143219871], [1203083156408684616]], [[(-2801436169413986), 202137477017714, 0, 0], [(-6737253284463322), (-126146208903686), 0], [(-20595220817176676), (-26677253520913)], [(-76867757259467556)]], [[71454336889831, (-4343586161912), 0, 0, 0], [152496634935988, 1965296379829, 0, 0], [419467691017514, 2836258043317, 0], [1321320998110318, 1040327300841], [4971281088521346]]], r := 1600722434266540, ok := true }, Z3 := { p := [[[414538524087750733757]], [[(-16688671004941655780), 264293356908175344], [(-23620423874223214358)]], [[743502545100128188, (-34620749601315177), 0], [979502107324474431, 2787844019138214], [1471647255652566586]], [[(-33981550494949817), 1435283951188323, 0, 0], [(-44046716438686828), (-343864518138517), 0], [(-61621561000700275), (-63296906933621)], [(-94142813556382418)]], [[1571278854641613, (-64509160508214), 0, 0, 0], [2023780639024894, 12008127341247, 0, 0], [2779878975903968, 8042975585643, 0], [3963181947604283, 2474663214034], [6093654441125741]]], r := 7970115367972545, ok := true }, iE := { p := [[[346707608244665615776]], [[(-5737617030384444808), 0], [(-19300328057714312576)]], [[120690897544828210, 0, 0], [328360794784754747, 0], [1201921483278092149]], [[(-2829858415055032), 0, 0, 0], [(-6723779837685282), 0, 0], [(-20584596934304493), 0], [(-76822455734276381)]], [[72200911134955, 0, 0, 0, 0], [152109262867256, 0, 0, 0], [419181404417012, 0, 0], [1320900237414060, 0], [4969193880217213]]], r := 1601698115564848, ok := true }, iHu := { p := [[[419896471232343743021]], [[(-16831361909103087509), 0], [(-23563906672744321461)]], [[750185742204638986, 0, 0], [978429284232785187, 0], [1470364054721094098]], [[(-34290322661791259), 0, 0, 0], [(-43994589552232888), 0, 0], [(-61592425373125265), 0], [(-94092645383952444)]], [[1585625367761817, 0, 0, 0, 0], [2021437527114579, 0, 0, 0], [2778532488534074, 0, 0], [3962017553145320, 0], [6091338412798523]]], r := 7989943030512568, ok := true }, T := { p := [[[6917529027641081856]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[981467838689040335]], [[16242177708609580, 0], [54635810736021708]], [[(-72864968436131), 0, 0], [878789935619470, 0], [(-360990663562664)]], [[1151000795420, 0, 0, 0], [(-4881125784057), 0, 0], [(-6833576097680), 0], [7970914436590]], [[(-27405423197), 0, 0, 0, 0], [76729789174, 0, 0, 0], [(-1571635538), 0, 0], [150390386780, 0], [(-265708413469)]]], r := 372099241213, ok := true }, de := { p := [[[(-70963157220762488449)]], [[636703809524047191, 0], [891385333333666068]], [[(-15086397625716449), 0, 0], [205007282930422, 0], [(-29569339346404241)]], [[478944483927386, 0, 0, 0], [47149066160, 0, 0], [66008692623, 0], [1314223663896746]], [[(-17105158203891), 0, 0, 0, 0], [10843685, 0, 0, 0], [1594407278, 0, 0], [21253623, 0], [(-65711175756069)]]], r := 22195655078952, ok := true }, dde := { p := [[[(-2781801390731197113073)]], [[131826953973193763898, 0], [184557735562471269536]], [[(-6277621139733026252), 0, 0], [(-8788875593039557116), 0], [(-12304137433876732001)]], [[298934306146727635, 0, 0, 0], [418507933851851296, 0, 0], [585911107392591719, 0], [820275736066619977]], [[(-14234966967150708), 0, 0, 0, 0], [(-19928953786699333), 0, 0, 0], [(-27900538490340295), 0, 0], [(-39060749421930690), 0], [(-54685049101006481)]]], r := 12078939959540792, ok := true }, nJu := { p := [[[(-141926314441524976897)]], [[1273407619048094383, 0], [1782770666667332136]], [[(-30172795251432898), 0, 0], [410014565860844, 0], [(-59138678692808482)]], [[957888967854772, 0, 0, 0], [94298132320, 0, 0], [132017385246, 0], [2628447327793492]], [[(-34210316407782), 0, 0, 0, 0], [21687371, 0, 0, 0], [3188814557, 0, 0], [42507247, 0], [(-131422351512138)]]], r := 44391310157898, ok := true }, Jd1 := { p := [[[(-5563602781462394226145)]], [[263653907946387527797, 0], [369115471124942539072]], [[(-12555242279466052503), 0, 0], [(-17577751186079114232), 0], [(-24608274867753464002)]], [[597868612293455270, 0, 0, 0], [837015867703702592, 0, 0], [1171822214785183439, 0], [1640551472133239954]], [[(-28469933934301416), 0, 0, 0, 0], [(-39857907573398666), 0, 0, 0], [(-55801076980680590), 0, 0], [(-78121498843861380), 0], [(-109370098202012962)]]], r := 24157879919081580, ok := true }, term0 := { p := [[[588564923143699942933744]], [[(-55651920610234447766551), 0], [(-77631458019185413543089)]], [[3965722300731534668255, 0, 0], [7367109884503140143479, 0], [7735317385825802900986]], [[(-251492957397394089134), 0, 0, 0], [(-525594268078844324636), 0, 0], [(-734939158384831410000), 0], [(-686346843162144576100)]], [[14959142667583703362, 0, 0, 0, 0], [33351135740870582426, 0, 0, 0], [52453803467749318607, 0, 0], [65249183768153774529, 0], [57133724077269249224]]], r := 23284649095890689906, ok := true }, r0 := { p := [[[395356619299403330135]], [[(-21188964639488795077), 263378646346111961710], [(-22175236233661318428)]], [[924985344288491433, (-14074471383328626870), 43768255955537557454], [1201676895092318377, (-14776919643328670723)], [1383494590693685872]], [[(-37265642151510952), 611110784627203320, (-2311458531697849771), (-42659296462789304)], [(-50940565930042519), 799340479591694903, (-2458440417315871686)], [(-75183064134816361), 921963999728710206], [(-88524892882966897)]], [[1468027504536679, (-24487819435914663), 98164901755533511, 11395607048484711, (-3526198543469960)], [1978750881109188, (-33766803361171732), 132039071259494146, 1458998648992519], [3164845049102739, (-50023112698366797), 153416929465438865], [4818638364725912, (-58994890890676048)], [5730494474887153]]], r := 90748353151042961, ok := true }, r1 := { p := [[[2798942712335044190418]], [[(-147349381463947245810), 0], [(-157262982740335155375)]], [[6222364621597460308, 0, 0], [8429769880110697650, 0], [9814392169702217444]], [[(-242562989407259080), 0, 0, 0], [(-349707305665507573), 0, 0], [(-528210010665146974), 0], [(-628098317602259064)]], [[9308864861680864, 0, 0, 0, 0], [13270156144631096, 0, 0, 0], [21808199582322868, 0, 0], [33884308881320970, 0], [40663594073754144]]], r := 83618422600920931, ok := true }, r2 := { p := [[[248164886209648011686916]], [[(-13679973152343091123741), 634262689489136898318], [(-32349135750928814218680)]], [[622147553256897841088, (-25150960777235187081), 480819414876119284], [1751166086482396794539, (-41982053162178986434)], [3191809204186514551945]], [[(-27251873565965890499), 965059447213692907, 820729295751016, (-157476409506969)], [(-78334050981731258115), 1590988292714653139, 924571891500316], [(-170866166734747185727), 2796407129650789088], [(-281101526084093748426)]], [[1195788677445204137, (-37763157505109465), (-14619365351889), 14063812882832, 51132450720], [3386197699717101808, (-58569683101407980), 25444683044397, (-11036670979150)], [7565897621088572890, (-104239123960052217), (-12084027073154)], [14929644836732954718, (-186276454941328181)], [23262461929188657062]]], r := 159439516308127889370, ok := true }, r3 := { p := [[[1146075707063735469720249]], [[(-108931521838290239425970), 3395947496589842157478], [(-153191547612696777837992)]], [[7775690404376572428034, (-261071988496637451254), 1886286611141351238], [14575515018167956202186, (-227967673057979070426)], [15332306794646576608041]], [[(-493532396609010336573), 17162130221621281341, 8170253341694469, (-1237656395194334)], [(-1040776985060298145662), 17510207056538708305, 2675372479372995], [(-1459288114214614849008), 15244486765636745513], [(-1363463811455747237047)]], [[29371126555635418869, (-1042374011326546811), (-286463133489181), 107918380220374, 802972605851], [66070549660548933685, (-1149619634362919010), 207806267296602, (-85983687992976)], [104212918523462517174, (-1169413327932515331), (-41533341263324)], [129791961946460139896, (-1017895226953238715)], [113651772671819270963]]], r := 3205572719266039050197, ok := true }, eta := { p := [[[(-255437028677476929441372)]], [[14070566062002979945814, 0], [32820389163999731303518]], [[(-641107812179017303126), 0, 0], [(-1776277631256863233751), 0], [(-3223012520565262658421)]], [[28146918856805642838, 0, 0, 0], [79539811590772064307, 0, 0], [172519697137599907552, 0], [283173240118484821394]], [[(-1237798960050987583), 0, 0, 0, 0], [(-3442739219153169742), 0, 0, 0], [(-7645011585680879818), 0, 0], [(-15039085483459691421), 0], [(-23400184827577387707)]]], r := 20689772300224054568, 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 := 135107988821114880, bh := 9007199254740992, tc := 6917529027641081856, th := 2305843009213693952, sc := 13258597302978740224, sh := 576460752303423488 }
noncomputable def q3 : Cert := { V0 := [[[259278355153804821]], [[(-32882561097818622), 86401487538095009], [2864840383890855]], [[533085652978344, (-10951482875472948), (-12311284290823)], [(-356044150446400), 954130376639833], [(-63534433915310)]], [[(-10694552602083), 176355011839718, 4682787514948, (-1365621884826)], [5033032615889, (-118372863198580), (-407980349893)], [7981275542334, (-21169058371536)], [2476948215272]], [[236794813165, (-3473066006879), (-669394786382), 518852470461, 574163027], [(-114736199362), 1634030502793, 154115750853, (-45204189123)], [(-121419559257), 2656944025125, 4543114769], [(-311522998726), 825310389133], [(-114097319759)]]], r0 := 53434099921930, V1 := [[[690807785447138237]], [[(-87458351556591999), 0], [7619668574552421]], [[1388959227296842, 0, 0], [(-941941698642567), 0], [(-169203053988002)]], [[(-26298972629809), 0, 0, 0], [12363130027995, 0, 0], [21198314872546, 0], [6596914773857]], [[545879879349, 0, 0, 0, 0], [(-235470479690), 0, 0, 0], [(-311486427742), 0, 0], [(-827567090395), 0], [(-303900684003)]]], r1 := 30450869423387, V2 := [[[18214781728408133434]], [[(-4334900774996773), 71479309514368], [(-15480978761698837)]], [[10699047968454, (-6576517751912), (-20539972900)], [(-288556252807339), 9687109258217], [(-1322597821275)]], [[(-176096525078), (-154794369816), 4167288978, 5738782], [886705619172, (-891415463506), (-4182746958)], [71662765488, 335428057717], [(-6617568984)]], [[4209710942, 391678472, (-164475570), (-1801187), (-1578)], [(-13649465008), (-21019136435), 848733873, 1557605], [9022763000, (-30913918647), (-287326927)], [1298525107, 397559068], [151236760]]], r2 := 8849315336246, V3 := [[[18251930074844961117]], [[(-8404480836068614), 119594932713701], [(-13028612757780706)]], [[2929549453005, (-8014307382476), (-68579995440)], [(-557565459311183), 16222383831161], [(-2793024705089)]], [[1660825273, (-585093471915), 12177828492, 38269323], [397169553464, (-1089239836351), (-13975396186)], [186328274719, 563386328783], [(-3203493943)]], [[(-27526124), (-145073168), (-167476615), (-11034246), (-21033)], [215628225, (-79267866450), 2483122973, 10394274], [13745698234, (-38113632941), (-961591061)], [237503483, 754557343], [27645153]]], r3 := 25194211836545, Vm := [[[18215147925837985688]], [[(-4369712969278277), 0], [(-15431259930020696)]], [[10028078233707, 0, 0], [(-293294413861312), 0], [405659151121]], [[(-173862520761), 0, 0, 0], [796560604603, 0, 0], [(-94081933898), 0], [(-4393696945)]], [[4179581235, 0, 0, 0, 0], [(-13304416601), 0, 0, 0], [5974652064, 0, 0], [1044636987, 0], [131014702]]], rm := 1728801540937 }
noncomputable def w3 : Wit := { Z0 := { p := [[[259315310739038086]], [[(-32896623240877457), 86438436913012695], [2866065525545704]], [[535097555974574, (-10965541080292486), 0], [(-356507255943551), 955355175181901], [(-63548063355311)]], [[(-10832470474543), 178365851991524, 0, 0], [5098590437196, (-118835751981184), 0], [7986497344857, (-21182687785104)], [2477456805387]], [[242205838437, (-3610823491515), 0, 0, 0], [(-119154116148), 1699530145732, 0, 0], [(-122174551931), 2662165781619, 0], [(-311717265081), 825818935129], [(-114119359842)]]], r := 13145881685398, ok := true }, Z1 := { p := [[[691507495304101563]], [[(-87724328642339886), 0], [7642841401455211]], [[1426926815932197, 0, 0], [(-950686015849469), 0], [(-169461502280828)]], [[(-28886587932115), 0, 0, 0], [13596241165857, 0, 0], [21297326252954, 0], [6606551481033]], [[645882235832, 0, 0, 0, 0], [(-317744309728), 0, 0, 0], [(-325798805149), 0, 0], [(-831246040216), 0], [(-304318292911)]]], r := 7620161240181, ok := true }, Z2 := { p := [[[331035522842277279393]], [[(-5242105019053224098), 86438436913012695], [(-18720824461459157430)]], [[104291394803770175, (-10965541080292486), 0], [303544100615858390, 955355175181901], [1163498873580218374]], [[(-2299986867417502), 178365851991524, 0, 0], [(-5904815481108818), (-118835751981184), 0], [(-19023270006745218), (-21182687785104)], [(-74327830618802004)]], [[54843504408697, (-3610823491515), 0, 0, 0], [126103518697162, 1699530145732, 0, 0], [368115187511079, 2662165781619, 0], [1220781141054436, 825818935129], [4806539919919390]]], r := 1458357913634307, ok := true }, Z3 := { p := [[[383886339989818504622]], [[(-14077417872434050318), 200320266780921800], [(-21822790683546635857)]], [[572197826743251448, (-29568867339832526), 0], [824910437088567408, 2144392575141961], [1358586940063816353]], [[(-23867728320890439), 1109653609524822, 0, 0], [(-33850878406259870), (-301312067752442), 0], [(-51867319496371282), (-48335439987001)], [(-86872509596295613)]], [[1007358358581226, (-45437832901215), 0, 0, 0], [1419618770865119, 9414122444377, 0, 0], [2135333012061905, 6962842436046, 0], [3334762924399856, 1887931418379], [5621391880413510]]], r := 6037654147187588, ok := true }, iE := { p := [[[335693594164811852427]], [[(-5286649551349695699), 0], [(-18669341432574354962)]], [[105298759545830224, 0, 0], [303178962249133293, 0], [1162357362071798908]], [[(-2323185433567482), 0, 0, 0], [(-5893412536885320), 0, 0], [(-19013704358710708), 0], [(-74283328153964489)]], [[55413012622345, 0, 0, 0, 0], [125796661573104, 0, 0, 0], [367870808935220, 0, 0], [1220401766660530, 0], [4804489998085202]]], r := 1459574689724138, ok := true }, iHu := { p := [[[388983377889021959328]], [[(-14196670308131320125), 0], [(-21768227805801357051)]], [[577325786617075549, 0, 0], [824021058416944703, 0], [1357357071646369332]], [[(-24084210879999284), 0, 0, 0], [(-33810598499050703), 0, 0], [(-51842917698543887), 0], [(-86824472230205746)]], [[1016544302912991, 0, 0, 0, 0], [1417962881869359, 0, 0, 0], [2134294678331600, 0, 0], [3333788286706258, 0], [5619175788080052]]], r := 6052817143803797, ok := true }, T := { p := [[[6917529027641081856]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[1013669527318634835]], [[15963711089419568, 0], [56374452281078302]], [[(-66559499900181), 0, 0], [860131606267416, 0], [(-374664105193159)]], [[959525472537, 0, 0, 0], [(-4460782813024), 0, 0], [(-6839866979970), 0], [8271693120433]], [[(-20859836711), 0, 0, 0, 0], [63964762679, 0, 0, 0], [(-1573806272), 0, 0], [150388264255, 0], [(-275735148402)]]], r := 373233335656, ok := true }, de := { p := [[[(-69746517997080051920)]], [[581605784727770184, 0], [891795536582580948]], [[(-12576692273625722), 0, 0], [205196009399131, 0], [(-29569200945546698)]], [[364552068986580, 0, 0, 0], [47214188170, 0, 0], [72395088528, 0], [1314223710625101]], [[(-11887565695705), 0, 0, 0, 0], [10863660, 0, 0, 0], [1598792689, 0, 0], [25541671, 0], [(-65711175740281)]]], r := 20935999123905, ok := true }, dde := { p := [[[(-2541074447194609782300)]], [[109896813979244711859, 0], [168508448101508558092]], [[(-4778256878620896200), 0, 0], [(-7326866829154434778), 0], [(-11234212839068685126)]], [[207750268115657358, 0, 0, 0], [318550316182569600, 0, 0], [488443818146606485, 0], [748947411011318372]], [[(-9032620359976850), 0, 0, 0, 0], [(-13850017918061642), 0, 0, 0], [(-21236697338789563), 0, 0], [(-32562931016242892), 0], [(-49929827440125504)]]], r := 9644041763433369, ok := true }, nJu := { p := [[[(-139493035994160103839)]], [[1163211569455540368, 0], [1783591073165161897]], [[(-25153384547251444), 0, 0], [410392018798263, 0], [(-59138401891093396)]], [[729104137973160, 0, 0, 0], [94428376341, 0, 0], [144790177056, 0], [2628447421250202]], [[(-23775131391409), 0, 0, 0, 0], [21727320, 0, 0, 0], [3197585379, 0, 0], [51083342, 0], [(-131422351480562)]]], r := 41871998247803, ok := true }, Jd1 := { p := [[[(-5082148894389219564600)]], [[219793627958489423719, 0], [337016896203017116184]], [[(-9556513757241792399), 0, 0], [(-14653733658308869555), 0], [(-22468425678137370251)]], [[415500536231314717, 0, 0, 0], [637100632365139201, 0, 0], [976887636293212971, 0], [1497894822022636745]], [[(-18065240719953700), 0, 0, 0, 0], [(-27700035836123283), 0, 0, 0], [(-42473394677579126), 0, 0], [(-65125862032485783), 0], [(-99859654880251007)]]], r := 19288083526866727, ok := true }, term0 := { p := [[[491326771295521032626548]], [[(-42388526023101798366902), 0], [(-64761293365600368742372)]], [[2757303117028152382484, 0, 0], [5609440594664098467186, 0], [6451465576811389664528]], [[(-159635908318181575685), 0, 0, 0], [(-365355160943940860312), 0, 0], [(-559531672772853086300), 0], [(-572367320560393591008)]], [[8669090117337821554, 0, 0, 0, 0], [21166159362297834182, 0, 0, 0], [36459341111149211651, 0, 0], [49673382561245236729, 0], [47642462446621621391]]], r := 16639994097658848317, ok := true }, r0 := { p := [[[356402274043693703136]], [[(-17893471811602696054), 237492487532036093623], [(-19960929886620453074)]], [[732479883359441778, (-11895914871896274588), 39509432483859275759], [1019468686907448382, (-13303586363497174248)], [1244882395310136978]], [[(-27518405403572216), 484529091303044660, (-1960628793569910183), (-24191673975853826)], [(-40663422078076751), 678511351580713596, (-2214798012789438875)], [(-63850307575091045), 829715657238828875], [(-79638100330899612)]], [[1004400143235782, (-18107689430364873), 78232488721139830, 7327545795606740, (-2005738043810795)], [1477501514722104, (-26976957698952248), 112329181889229612, 821835408170677], [2531978480667205, (-42503734523589246), 138148678237853659], [4094892612189633, (-53079849157346623)], [5154442591101179]]], r := 71103527749573934, ok := true }, r1 := { p := [[[2527331105797628592993]], [[(-125099249128003849596), 0], [(-141703452245661415461)]], [[4964524633973144079, 0, 0], [7175756217870227180, 0], [8839089812932816697]], [[(-180563755735235070), 0, 0, 0], [(-280594930467604549), 0, 0], [(-449940605781319889), 0], [(-565519938029560316)]], [[6411683852321112, 0, 0, 0, 0], [9965923285567761, 0, 0, 0], [17528588971458749, 0, 0], [28875483421631346, 0], [36605048651096051]]], r := 62891091626146031, ok := true }, r2 := { p := [[[223093088197370968305397]], [[(-11483974759768528827529), 587541452746581198928], [(-29135214000115525160026)]], [[483594439443687008803, (-21699642654577094562), 482405943185081097], [1474224194235258129363, (-39017950597985108170)], [2877951416987625493666]], [[(-19480831615823720840), 770610374319396388, 767453371905993, (-129247913380769)], [(-61091077465932100318), 1380721980566640194, 974402990430231], [(-144091383504871993333), 2601995970629607961], [(-253661343927476709223)]], [[782386515646805358, (-27719638533711737), (-12133518066156), 14163403545423, 34344977210], [2428573711765814512, (-47135775512672494), 24424809529570, (-9073644020900)], [5912439532573749257, (-90656876438066800), (-12308781488938)], [12605445740270157771, (-173441352121994904)], [21004341722458034524]]], r := 134095204195168724619, ok := true }, r3 := { p := [[[955788783467722307230735]], [[(-82929648910815362510138), 2934981190001551869313], [(-127731509577357272459159)]], [[5404545161676983232269, (-203239637342127855383), 1901589677503240518], [11095266982035446348801, (-197045571769156954533)], [12783306926691116499279]], [[(-313194250927434630268), 12124351235940580164, 7181871259098769, (-1019831100586568)], [(-723352301517956476660), 13635869105680899722, 3078976992837177], [(-1110814514723406391446), 13179303720353050847], [(-1136752387254372623220)]], [[17017748612390510277, (-669992806949846485), (-212631437872335), 109857481131402, 541493617496], [41926153369735919949, (-812332556623660461), 196447807916509, (-71089087085439)], [72427720719309578266, (-910722515532317570), (-44665201197942)], [98796526936972372304, (-880075334718475441)], [94752455901761448064]]], r := 2154004272675508146451, ok := true }, eta := { p := [[[(-229653339971784468052328)]], [[11808264645625588958272, 0], [29560653712633238844837]], [[(-498054492412872336565), 0, 0], [(-1495115494439278416872), 0], [(-2906137042303040315167)]], [[20105991621211920174, 0, 0, 0], [62012364052757930404, 0, 0], [145467930640252125317, 0], [255533290158655724535]], [[(-809208587582553812), 0, 0, 0, 0], [(-2468122183515524007), 0, 0, 0], [(-5972924265957243232), 0, 0], [(-12696590030003131452), 0], [(-21128811581903634815)]]], r := 17652350260813924086, 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

theorem region : RegionPosI 108086391056891904 144115188075855872 4611686018427387904 9223372036854775808 11529215046068469760 13835058055282163712 :=
  (RegionPosI.split_b 126100789566373888 (RegionPosI.split_s 12682136550675316736 (RegionPosI.of_check c0 q0 ok_0 108086391056891904 126100789566373888 4611686018427387904 9223372036854775808 11529215046068469760 12682136550675316736 (by decide +kernel)) (RegionPosI.of_check c1 q1 ok_1 108086391056891904 126100789566373888 4611686018427387904 9223372036854775808 12682136550675316736 13835058055282163712 (by decide +kernel))) (RegionPosI.split_s 12682136550675316736 (RegionPosI.of_check c2 q2 ok_2 126100789566373888 144115188075855872 4611686018427387904 9223372036854775808 11529215046068469760 12682136550675316736 (by decide +kernel)) (RegionPosI.of_check c3 q3 ok_3 126100789566373888 144115188075855872 4611686018427387904 9223372036854775808 12682136550675316736 13835058055282163712 (by decide +kernel))))

end CKLaneC.RSC2.S07_0066

end