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

import Definitions.Def_CK_CKLaneC_RSC2_S05_0055_part00

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

namespace CKLaneC.RSC2.S05_0055
open CKLaneC.TM3 CKLaneC.RSCell

noncomputable def c5 : Cell := { bc := 21955048183431168, bh := 562949953421312, tc := 11529215046068469760, th := 2305843009213693952, sc := 6052837899185946624, sh := 288230376151711744 }
noncomputable def q5 : Cert := { V0 := [[[1007441257391841806]], [[(-34892452727496491), 200622243595019657], [3213297989142142]], [[429535457441441, (-6888578083568808), (-258486268943658)], [(-109576743560967), 634379425168269], [(-30948712697854)]], [[(-6535460866648), 81692154169188, 26746089209013, (-16796110325125)], [1386582803671, (-21060528939623), (-2463087228175)], [1062319478344, (-6136351715581)], [474237423214]], [[119008678643, (-1178122662444), (-1245941564005), 1707768382871, 64614021784], [(-25093192799), 237338096947, 252832492838, (-157270936311)], [(-13389117294), 206916522625, 15948792806], [(-16301239957), 94105394544], [(-8521752502)]]], r0 := 3745495160840, V1 := [[[1606533925957557849]], [[(-55272356276624022), 0], [5090113689223797]], [[661400411856487, 0, 0], [(-170075444655417), 0], [(-49186446908602)]], [[(-9675174832516), 0, 0, 0], [1976071476165, 0, 0], [1665385791417, 0], [754172211967]], [[171044105266, 0, 0, 0, 0], [(-32812177522), 0, 0, 0], [(-19821447604), 0, 0], [(-25604737927), 0], [(-13556943243)]]], r1 := 1050429471759, V2 := [[[18418121310458113779]], [[(-375788028568111), 3261110035340], [(-732229278864526)]], [[798567554754, (-32328308682), (-351925150)], [(-9746488226956), 168484567709], [25092039819]], [[(-15137700764), (-1098616543), 11624211, 37196], [23161413612, (-1650882241), (-27310021)], [(-1774550303), 2196827608], [(-191271245)]], [[382216776, 3726303, 39384, (-2090), (-4)], [(-435431353), (-57495463), 899670, 3849], [43890435, (-20965925), (-710406)], [11160406, 415220], [2142134]]], r2 := 21597598573, V3 := [[[18432326325637500075]], [[(-686339245454021), 3251323592025], [(-369939530575224)]], [[10755288736, 81334517500, (-697006256)], [(-17604828424761), 168036630647], [(-6566274869)]], [[6727729, (-3588633053), (-1527640), 146575], [555404030, 4214497568, (-54073158)], [(-165899508), 2192970972], [(-1224020)]], [[(-101525), (-2191490), 1179708, (-3039), (-30)], [386566, (-185409204), (-122658), 15159], [7233457, 55310030, (-1405996)], [(-42555), 445140], [5069]]], r3 := 244200940068, Vm := [[[18418132057452356361]], [[(-375930109498115), 0], [(-731670653706869)]], [[795876759480, 0, 0], [(-9753917251587), 0], [32474521801]], [[(-15132462177), 0, 0, 0], [23021557215, 0, 0], [(-1873967274), 0], [(-188791131)]], [[382204777, 0, 0, 0, 0], [(-435124340), 0, 0, 0], [42039939, 0, 0], [11114010, 0], [2131873]]], rm := 3991661458 }
noncomputable def w5 : Wit := { Z0 := { p := [[[1009614540248181190]], [[(-35118665794322000), 201922908049636238], [3234130287703238]], [[440189731433349, (-7023733158864400), 0], [(-111736579798509), 646826057540647], [(-31082617650001)]], [[(-6864045138072), 88037946286669, 0, 0], [1488387153786, (-22347315959702), 0], [1076262517093, (-6216523530001)], [476098579841]], [[127377579448, (-1372809027615), 0, 0, 0], [(-28276818721), 297677430757, 0, 0], [(-14046237198), 215252503418, 0], [(-16495073928), 95219715968], [(-8553192878)]]], r := 717835957908, ok := true }, Z1 := { p := [[[1615383264397089904]], [[(-56189865270915200), 0], [5174608460325181]], [[704303570293359, 0, 0], [(-178778527677614), 0], [(-49732188240002)]], [[(-10982472220915), 0, 0, 0], [2381419446058, 0, 0], [1722020027349, 0], [761757727747]], [[203804127118, 0, 0, 0, 0], [(-45242909954), 0, 0, 0], [(-22473979517), 0, 0], [(-26392118285), 0], [(-13685108604)]]], r := 265131457004, ok := true }, Z2 := { p := [[[2016298970796071446069]], [[(-23268215643266496439), 201922908049636238], [(-45338508589145388819)]], [[338797360574331172, (-7023733158864400), 0], [524124148046270532, 646826057540647], [1100138799376685513]], [[(-5839397986006388), 88037946286669, 0, 0], [(-7419558823360610), (-22347315959702), 0], [(-12730966247090598), (-6216523530001)], [(-27254872832832284)]], [[118745158675439, (-1372809027615), 0, 0, 0], [123099713072219, 297677430757, 0, 0], [178559164334458, 215252503418, 0], [315578107686172, 95219715968], [681715395671919]]], r := 219061073160569, ok := true }, Z3 := { p := [[[3695347159718539147306]], [[(-156162636693184841296), 739773032412818411], [(-84172270337608427916)]], [[7069400934489272834, (-48449064581062312), 0], [3612608084478542966, 2144286677233798], [2051634174644930759]], [[(-326118494359848911), 2141127742913434, 0, 0], [(-164435363531220036), (-128870405401046), 0], [(-88537596275787293), (-21270112061798)], [(-50961221346700154)]], [[15176784236726921, (-98148188835139), 0, 0, 0], [7609891139511701, 5236417084512, 0, 0], [4038110265885165, 1312092951336, 0], [2206278439951400, 328515682838], [1277013105166493]]], r := 8960871659235417, ok := true }, iE := { p := [[[2020097938996354137154]], [[(-23288532326638366840), 0], [(-45326339233783751981)]], [[339164508234324743, 0, 0], [524061927279711031, 0], [1100021841992132720]], [[(-5846450663027622), 0, 0, 0], [(-7418003853706549), 0, 0], [(-12730359287251924), 0], [(-27253081373524878)]], [[118900809145103, 0, 0, 0, 0], [123064089061495, 0, 0, 0], [178545455989741, 0, 0], [315568774079794, 0], [681683211797326]]], r := 218806134032212, ok := true }, iHu := { p := [[[3700456754849390474471]], [[(-156292425341735075880), 0], [(-84157459799395906101)]], [[7075537701191359901, 0, 0], [3612311746366789020, 0], [2051487262475573696]], [[(-326404717770718260), 0, 0, 0], [(-164421072235049311), 0, 0], [(-88534423511208668), 0], [(-50958952296518685)]], [[15190171300970936, 0, 0, 0, 0], [7609236819787358, 0, 0, 0], [4037959582188159, 0, 0], [2206228426969666, 0], [1276972140022552]]], r := 8954537959427611, ok := true }, T := { p := [[[11529215046068469760]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[168448450123166332]], [[1941944051492134, 0], [3779594764341532]], [[(-5894124586393), 0, 0], [43445918432400, 0], [(-6921337654240)]], [[93520981855, 0, 0, 0], [(-151190443999), 0, 0], [(-81410239076), 0], [59097939275]], [[(-2226690384), 0, 0, 0, 0], [2397973162, 0, 0, 0], [(-1514549), 0, 0], [695270326, 0], [(-757666726)]]], r := 2531088796, ok := true }, de := { p := [[[(-104424406448072526648)]], [[633891034082358204, 0], [341325941428962110]], [[(-15086747241311589), 0, 0], [6349998647987, 0], [(-4374263993043005)]], [[478944429998121, 0, 0, 0], [118134832, 0, 0], [63611064, 0], [74773754888191]], [[(-17105158213198), 0, 0, 0, 0], [2198, 0, 0, 0], [1516324, 0, 0], [638, 0], [(-1437956824687)]]], r := 3572395522294, ok := true }, dde := { p := [[[(-34086303843791940257387)]], [[1622523187210824668643, 0], [873666331575059436778]], [[(-77263020712263061989), 0, 0], [(-41603171351390361456), 0], [(-22401704230182778264)]], [[3679191462269240329, 0, 0, 0], [1981103094831691721, 0, 0], [1066747820293987707, 0], [574402672534526799]], [[(-175199593441395311), 0, 0, 0, 0], [(-94338242622295214), 0, 0, 0], [(-50797515261190711), 0, 0], [(-27352508215931472), 0], [(-14728273654730176)]]], r := 18549595083108593, ok := true }, nJu := { p := [[[(-208848812896145053296)]], [[1267782068164716408, 0], [682651882857924221]], [[(-30173494482623177), 0, 0], [12699997295975, 0], [(-8748527986086009)]], [[957888859996243, 0, 0, 0], [236269665, 0, 0], [127222128, 0], [149547509776382]], [[(-34210316426396), 0, 0, 0, 0], [4396, 0, 0, 0], [3032649, 0, 0], [1276, 0], [(-2875913649373)]]], r := 7144791044579, ok := true }, Jd1 := { p := [[[(-68172607687583880514773)]], [[3245046374421649337286, 0], [1747332663150118873557]], [[(-154526041424526123977), 0, 0], [(-83206342702780722911), 0], [(-44803408460365556528)]], [[7358382924538480659, 0, 0, 0], [3962206189663383442, 0, 0], [2133495640587975414, 0], [1148805345069053598]], [[(-350399186882790621), 0, 0, 0, 0], [(-188676485244590427), 0, 0, 0], [(-101595030522381421), 0, 0], [(-54705016431862943), 0], [(-29456547309460352)]]], r := 37099190166217177, ok := true }, term0 := { p := [[[87454287707930869523894902]], [[(-8324105871278317414085488), 0], [(-4479548251611876227703331)]], [[594463096398384554590400, 0, 0], [426498833610324744471837, 0], [172222578903361605429136]], [[(-37740009468749999800016), 0, 0, 0], [(-30461230742916026170808), 0, 0], [(-16398950128286340104699), 0], [(-5886793492651617291723)]], [[2246297735349556221965, 0, 0, 0, 0], [1933952058133124682307, 0, 0, 0], [1171277384319066367376, 0, 0], [560564941775501671702, 0], [188657010863547512935]]], r := 406292270954583117292, ok := true }, r0 := { p := [[[10410616919520907773010]], [[(-420070121947665976413), 4135854526609317734833], [(-233539538571027736423)]], [[13928250543802125365, (-164954758137947435332), 402314982719754477354], [9272651695825027904, (-92957985484126682270)], [5666725328981417610]], [[(-462467967548615433), 5401489657820801426, (-15281450994024389021), (-2219783488525191085)], [(-296870773988368072), 3659674351081469768, (-9113511908996391154)], [(-223775527508374606), 2256703229471035322], [(-140376424017554282)]], [[16451269241235467, (-178001487967980716), 473556181625495341, 236752330607915122, (-102514824483650551)], [9485411900924677, (-116053897298311907), 346362457646999221, 36120084096859524], [7078341974129261, (-88433861026842371), 221692697146269355], [5525426994816587, (-55918852898120197)], [3510930905391721]]], r := 197191289290070143, ok := true }, r1 := { p := [[[26371037371157846051428]], [[(-1045281622169692862019), 0], [(-593323023346655771949)]], [[34011628201393888031, 0, 0], [23250704623105560764, 0], [14407771460830374782]], [[(-1117147864518106686), 0, 0, 0], [(-733587861203729761), 0, 0], [(-562236237633845247), 0], [(-357064784112199647)]], [[39704679557868827, 0, 0, 0, 0], [23232639411148094, 0, 0, 0], [17545960135332943, 0, 0], [13898464982244166, 0], [8933108135296788]]], r := 29519749073349942, ok := true }, r2 := { p := [[[17552134147517537698044776]], [[(-760978639634444026581605), 6343177755226315823588], [(-876208572714003306969173)]], [[30372592722456861420446, (-195639589332900853605), 457984432151779263], [37256957950126582642940, (-159213249192219718704)], [33167296437893801574918]], [[(-1266117855643415730384), 6483717352852396942, 408869149359956, (-46785441981366)], [(-1465610288343822369346), 4691736669595777164, 107602440078568], [(-1393495911479517810195), 4050204875925461770], [(-1121374494425996854641)]], [[55307539533866259285, (-240832586545107804), (-8650718732275), 1054687459172, (-2742325064)], [60590844057420113793, (-149452231546091668), 2885504253686, (-1218912479603)], [54323131154432499620, (-117224348796092224), (-1063874521008)], [46711358101845953381, (-103355226025335268)], [35638672783882723881]]], r := 266335693359193990692, ok := true }, r3 := { p := [[[174428670154430509996972857]], [[(-16608115412319262306294074), 68002484972356964232476], [(-8946776919760168701106983)]], [[1186195562463164116576304, (-5690680743594261858084), 1734056856158577122], [851968518273836022767812, (-1749014771541387547361)], [344129123237406317118943]], [[(-75310875862591745865086), 387766562796498547005, 10058881270364391, (-361303807769258)], [(-60852383730166325541561), 146259909977570996337, (-90669538413514)], [(-32771502532298756593129), 44895812657326847809], [(-11765481380662418764831)]], [[4482678311179389026913, (-24027592480977887442), (-548067927063108), 6553791297957, (-499647840724)], [3863563617971732959861, (-9963214252220802770), 48983903085024, (-9920925832618)], [2340757339458102381981, (-3753354099650234769), (-239175379093)], [1120452880282729102262, (-1151893280058467096)], [377106147776087855201]]], r := 40821165298158862978452, ok := true }, eta := { p := [[[(-17630333519393165412229035)]], [[765081053887842869657664, 0], [878173202672623361550849]], [[(-30568662721717894103324), 0, 0], [(-37359412975833458237029), 0], [(-33217303237321004049297)]], [[1275376721385841754942, 0, 0, 0], [1470492293304641866179, 0, 0], [1396097496535545555857, 0], [1122651129547708633292]], [[(-55745196267654581838), 0, 0, 0, 0], [(-60821172124519038249), 0, 0, 0], [(-54446970759400590306), 0, 0], [(-46777679279210365948), 0], [(-35671307149935059158)]]], r := 28224591792725929532, ok := true } }
theorem sB_5 : stageB c5 w5 = true := by decide +kernel
theorem s0_5 : stageC0 w5 q5 = true := by decide +kernel
theorem s1_5 : stageC1 w5 q5 = true := by decide +kernel
theorem s2_5 : stageC2 w5 q5 = true := by decide +kernel
theorem s3_5 : stageC3 w5 q5 = true := by decide +kernel
theorem sE_5 : stageE w5 q5 = true := by decide +kernel
theorem sF_5 : stageF w5 = true := by decide +kernel
theorem ok_5 : (domOK c5 && cellCheck c5 q5) = true :=
  staged_check c5 q5 w5 (by decide +kernel) sB_5 s0_5 s1_5 s2_5 s3_5 sE_5 sF_5

noncomputable def c6 : Cell := { bc := 20829148276588544, bh := 562949953421312, tc := 11529215046068469760, th := 2305843009213693952, sc := 6629298651489370112, sh := 288230376151711744 }
noncomputable def q6 : Cert := { V0 := [[[933205863088377990]], [[(-33036319380558342), 185952732258652674], [3120578460863371]], [[390439753423773, (-6534198044158238), (-205634152672711)], [(-108556222515853), 617213965052517], [(-31734455739902)]], [[(-5634312388810), 74642105158832, 21760965396823, (-13411025398200)], [1298944602522, (-20983306386939), (-2055519536626)], [1111680298412, (-6299745365742)], [512789689296]], [[95694794610, (-1023092568950), (-1020654404006), 1398149533855, 44200028545], [(-22026800358), 225601715438, 215739511893, (-132067839344)], [(-13309178497), 217329574580, 14091341985], [(-17991473954), 101866919631], [(-9715165829)]]], r0 := 3718011184705, V1 := [[[1488855233717692004]], [[(-52406011775765145), 0], [4950220685402546]], [[603516479730935, 0, 0], [(-169211157524809), 0], [(-50482213964275)]], [[(-8383836147011), 0, 0, 0], [1870181269541, 0, 0], [1747675123280, 0], [816170035408]], [[138017414352, 0, 0, 0, 0], [(-29057169664), 0, 0, 0], [(-19838630953), 0, 0], [(-28331603270), 0], [(-15467764856)]]], r1 := 1076079845491, V2 := [[[18418876167443990082]], [[(-353453045065647), 2870782690422], [(-751721880289198)]], [[674680394569, (-33019529356), (-280151654)], [(-9652183788854), 156352119021], [22780365443]], [[(-11761080276), (-968367434), 10017902, 26778], [20627362839, (-1782475534), (-22916184)], [(-1671413269), 2149285850], [(-186312157)]], [[272314539, 2806717, 17494, (-1608), (-2)], [(-356282485), (-53355201), 817665, 2921], [41261868, (-24019511), (-628359)], [11169571, 432012], [2199660]]], r2 := 22773448251, V3 := [[[18431763956679778392]], [[(-651091489220841), 3057346850262], [(-405119502261373)]], [[9707269966, 60194229987, (-593068960)], [(-17602055221257), 166553128395], [(-6861134338)]], [[5333537, (-3238509169), 2552655, 112844], [528536643, 3289112787, (-48497476)], [(-136666335), 2291027799], [(-1349302)]], [[(-72108), (-1733687), 917997, (-3203), (-21)], [323140, (-176404144), 205319, 12302], [7260306, 45539140, (-1329186)], [(-38667), 486776], [5939]]], r3 := 206489026815, Vm := [[[18418885561820540566]], [[(-353590283815663), 0], [(-751207346377429)]], [[672289467513, 0, 0], [(-9659742155502), 0], [29942100225]], [[(-11756552532), 0, 0, 0], [20496592718, 0, 0], [(-1777872429), 0], [(-183844914)]], [[272296147, 0, 0, 0, 0], [(-356005404), 0, 0, 0], [39445179, 0, 0], [11118845, 0], [2188850]]], rm := 3685619118 }
noncomputable def w6 : Wit := { Z0 := { p := [[[934932598177397611]], [[(-33219981806690034), 186986519635479522], [3137927034245725]], [[399136880230941, (-6643996361338007), 0], [(-110392706969354), 627585406849145], [(-31852647720361)]], [[(-5898087514341), 79827376046188, 0, 0], [1385785383890, (-22078541393871), 0], [1124254905646, (-6370529544073)], [514522003892]], [[102167920419, (-1179617502869), 0, 0, 0], [(-24685925529), 277157076778, 0, 0], [(-13904942803), 224850981129, 0], [(-18175830527), 102904400778], [(-9746023740)]]], r := 753892968439, ok := true }, Z1 := { p := [[[1495892157083836178]], [[(-53151970890704055), 0], [5020683254793161]], [[638619008369506, 0, 0], [(-176628331150966), 0], [(-50964236352577)]], [[(-9436940022945), 0, 0, 0], [2217256614225, 0, 0], [1798807849034, 0], [823235206227]], [[163468672670, 0, 0, 0, 0], [(-39497480845), 0, 0, 0], [(-22247908484), 0, 0], [(-29081328843), 0], [(-15593637983)]]], r := 271388825806, ok := true }, Z2 := { p := [[[2064236635799714749065]], [[(-23021928818185419472), 186986519635479522], [(-48962904297163825845)]], [[320553655054572890, (-6643996361338007), 0], [547891393264136858, 627585406849145], [1252655490901123134]], [[(-5213734028581826), 79827376046188, 0, 0], [(-7435198273915271), (-22078541393871), 0], [(-14038573165709221), (-6370529544073)], [(-32716101922278132)]], [[98556048194452, (-1179617502869), 0, 0, 0], [116708965364825, 277157076778, 0, 0], [188909786101801, 224850981129, 0], [366969064893753, 102904400778], [862645179813661]]], r := 238796713122855, ok := true }, Z3 := { p := [[[3571963335890374556718]], [[(-137749000395397442537), 646831481378397395], [(-85709623610602849273)]], [[5692498941403032449, (-40706467386096173), 0], [3357370180959096335, 1984849085780308], [2201619498238141194]], [[(-239738977853818455), 1638330579916113, 0, 0], [(-139508549003552144), (-115095211446406), 0], [(-86717310495464883), (-20726188339170)], [(-57636397104958903)]], [[10185925666858852, (-68519319299077), 0, 0, 0], [5894362771810265, 4245120802310, 0, 0], [3610678637720789, 1232203464904, 0], [2277523646903539, 337297134145], [1522234159808545]]], r := 7129493967819665, ok := true }, iE := { p := [[[2067971805545603961963]], [[(-23040741761499302814), 0], [(-48950367895987985603)]], [[320879159831676668, 0, 0], [547832661625319929, 0], [1252528235689011062]], [[(-5219623420716319), 0, 0, 0], [(-7433786876351978), 0, 0], [(-14037962309765013), 0], [(-32714046344125996)]], [[98676721992400, 0, 0, 0, 0], [116678566056184, 0, 0, 0], [188896553936407, 0, 0], [366959135603893, 0], [862606243260283]]], r := 238512931956765, ok := true }, iHu := { p := [[[3576806683811915239655]], [[(-137856790155375463392), 0], [(-85694761447936152817)]], [[5697173219235367693, 0, 0], [3357112917012304912, 0], [2201464304583991801]], [[(-239938233958523350), 0, 0, 0], [(-139497073099106148), 0, 0], [(-86714396791370239), 0], [(-57633871489832498)]], [[10194438408496056, 0, 0, 0, 0], [5893881938122807, 0, 0, 0], [3610551089689581, 0, 0], [2277475197417023, 0], [1522186108147897]]], r := 7124914358980174, ok := true }, T := { p := [[[11529215046068469760]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[164548842497956573]], [[1833355453387699, 0], [3894988488495778]], [[(-5105690873136), 0, 0], [43202531708741, 0], [(-7466712976802)]], [[73965481186, 0, 0, 0], [(-138047663363), 0, 0], [(-85813412360), 0], [67204520035]], [[(-1607945507), 0, 0, 0, 0], [1999066401, 0, 0, 0], [(-1514618), 0, 0], [772466126, 0], [(-908170083)]]], r := 1921567705, ok := true }, de := { p := [[[(-103914190696835589532)]], [[578778909512526166, 0], [359781484291570320]], [[(-12577042443249603), 0, 0], [6350192514715, 0], [(-4859938241401782)]], [[364552014978618, 0, 0, 0], [112081769, 0, 0], [69672451, 0], [87566469236666]], [[(-11887565705029), 0, 0, 0, 0], [1979, 0, 0, 0], [1516464, 0, 0], [765, 0], [(-1774995997922)]]], r := 2358597363535, ok := true }, dde := { p := [[[(-32805063449784142497248)]], [[1425728092645718453237, 0], [886263408941933092260]], [[(-61988188160792305667), 0, 0], [(-38533204398668315013), 0], [(-23953069055558162979)]], [[2695138615506245908, 0, 0, 0], [1675356436441790007, 0, 0], [1041437784815166712, 0], [647380244701490902]], [[(-117179939804619330), 0, 0, 0, 0], [(-72841584202878066), 0, 0, 0], [(-45279903696713178), 0, 0], [(-28146967160935911), 0], [(-17496763370309938)]]], r := 13295203974624361, ok := true }, nJu := { p := [[[(-207828381393671179063)]], [[1157557819025052333, 0], [719562968583140640]], [[(-25154084886499205), 0, 0], [12700385029430, 0], [(-9719876482803563)]], [[729104029957236, 0, 0, 0], [224163538, 0, 0], [139344903, 0], [175132938473333]], [[(-23775131410058), 0, 0, 0, 0], [3958, 0, 0, 0], [3032928, 0, 0], [1530, 0], [(-3549991995843)]]], r := 4717194727063, ok := true }, Jd1 := { p := [[[(-65610126899568284994496)]], [[2851456185291436906475, 0], [1772526817883866184521]], [[(-123976376321584611334), 0, 0], [(-77066408797336630026), 0], [(-47906138111116325957)]], [[5390277231012491817, 0, 0, 0], [3350712872883580014, 0, 0], [2082875569630333425, 0], [1294760489402981804]], [[(-234359879609238660), 0, 0, 0, 0], [(-145683168405756132), 0, 0, 0], [(-90559807393426355), 0, 0], [(-56293934321871821), 0], [(-34993526740619876)]]], r := 26590407949248714, ok := true }, term0 := { p := [[[80999661765861253053765674]], [[(-7039165875156631120467909), 0], [(-4373231581910086209095336)]], [[458983053161357667935305, 0, 0], [380165407626520011452246, 0], [177223916651872031512892]], [[(-26605018088127713862004), 0, 0, 0], [(-24790883111997813790019), 0, 0], [(-15407651047676146143522), 0], [(-6385199598036656244876)]], [[1445837011139028489143, 0, 0, 0, 0], [1437079802589694367291, 0, 0, 0], [1004778887601675934225, 0, 0], [555150306753871175264, 0], [215690908402365664656]]], r := 290264936527039767052, ok := true }, r0 := { p := [[[10077033681588392151559]], [[(-386638171185638007784), 4007168813768494719881], [(-238764717437641425934)]], [[12021826288005539836, (-152101667026667566953), 391320847013793510106], [9043966906722008099, (-95102261962005334925)], [6110798684094262542]], [[(-367900078162911576), 4670911052241142016, (-14199750401459952287), (-1854634991453240503)], [(-272389821586344914), 3574064689545761801, (-9349420079994728951)], [(-230459739752643817), 2435031249780884566], [(-159623361110692864)]], [[11890603341169106, (-141728609034975159), 412919090035156005, 197713301773826783, (-86652289414345569)], [8037128095005913, (-106628988150088840), 340112658891177225, 31904266714103654], [6865375668490152, (-91182867850094578), 239801589079020265], [6004347387146966, (-63622071203307394)], [4209289180454469]]], r := 171081570554094110, ok := true }, r1 := { p := [[[25563521403818110011238]], [[(-964721859617300168495), 0], [(-607232864347839588434)]], [[29436383070209639827, 0, 0], [22722486406866564312, 0], [15551444205899990907]], [[(-889702566847555876), 0, 0, 0], [(-674470006133909150), 0, 0], [(-580077711235272979), 0], [(-406379071917553339)]], [[28667062443518889, 0, 0, 0, 0], [19700487219112631, 0, 0, 0], [17050315415115809, 0, 0], [15128856377056024, 0], [10718980154496728]]], r := 27035456486343684, ok := true }, r2 := { p := [[[17887734634652850397825754]], [[(-722327792572090114280373), 6292968515931568377245], [(-942990791140178720154482)]], [[26426098061958859214482, (-181054698513321576082), 458538801635454913], [37374001536722483188767, (-166964228417616094565)], [37666876358044989050353]], [[(-1001520685273929274996), 5499862682165891205, 371884172498614, (-42339180795004)], [(-1347492834358736785847), 4602187609735735244, 117755379858881], [(-1475790138303169679286), 4481694135056552374], [(-1343399885081952329796)]], [[39700528509105039446, (-185116881813766531), (-7119443897843), 999983750860, (-2192504481)], [50615455150873539882, (-134495338837407133), 2734829720244, (-1163738919441)], [52726214007404798567, (-121464909078271443), (-1215573710023)], [52203350458595283488, (-120624374463945888)], [45029856476224534575]]], r := 261503288200177175177, ok := true }, r3 := { p := [[[161567741141274781868252731]], [[(-14045732527086374330613046), 61145557306542727364207], [(-8734785056654605891238422)]], [[915947130593095633820158, (-4626288313778580527021), 1752203320552464187], [759448849785668026196036, (-1657776848790522675600)], [354132057467801223868493]], [[(-53096094602420398714010), 286689886586071893860, 8106692418682114, (-329059651282462)], [(-49527150597345116111875), 125335796641840014175, 3254572870931], [(-30791456673332466946118), 44855222211594989823], [(-12761862393355878568746)]], [[2885582529828434292412, (-16185116347695961197), (-394030901191307), 6772534989649, (-187755179846)], [2871077587390772759891, (-7764576228838327307), 42609801370872, (-9366096796813)], [2008081208076172751511, (-3390295728326214003), (-1056771201675)], [1109656008782723485577, (-1213077231950934024)], [431151049589657685254]]], r := 30183740587747531525947, ok := true }, eta := { p := [[[(-17962191679998614193024235)]], [[725924415849923969995528, 0], [944964256775992153845526]], [[(-26583517002331437351075), 0, 0], [(-37468766517516330245998), 0], [(-37719840262264266052526)]], [[1008311095869796290034, 0, 0, 0], [1351627078251591349535, 0, 0], [1478327286191649345569, 0], [1344825370300955292228]], [[(-39993505502412960979), 0, 0, 0, 0], [(-50793587928933416221), 0, 0, 0], [(-52836776069985451459), 0, 0], [(-52271536944037987256), 0], [(-45068270616077108880)]]], r := 28045658473460166627, 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 := 21955048183431168, bh := 562949953421312, tc := 11529215046068469760, th := 2305843009213693952, sc := 6629298651489370112, sh := 288230376151711744 }
noncomputable def q7 : Cert := { V0 := [[[939324035198988952]], [[(-33249123793073023), 187162746471034655], [2999498444135738]], [[392986065283004, (-6575322509281067), (-209690422074218)], [(-104315016131824), 593178628075251], [(-28875854376304)]], [[(-5677528568995), 75083911804785, 22186643076107, (-13671577641937)], [1248166824098, (-20154250107754), (-2001520455143)], [1011391562724, (-5731894007171)], [442428370216]], [[96571874345, (-1029694144787), (-1040459645196), 1424795021817, 45657120724], [(-21202200299), 216351914629, 210019817401, (-128534829302)], [(-12109235150), 197682791990, 12934943450], [(-15520710801), 87884192083], [(-7949680824)]]], r0 := 3316656487115, V1 := [[[1498560037881553153]], [[(-52737661778962932), 0], [4757615131088416]], [[607179977766738, 0, 0], [(-162544070908776), 0], [(-45932490036664)]], [[(-8440779764888), 0, 0, 0], [1794516410351, 0, 0], [1589759142458, 0], [704148320323]], [[139124703347, 0, 0, 0, 0], [(-27904581553), 0, 0, 0], [(-18038270336), 0, 0], [(-24437341278), 0], [(-12656346147)]]], r1 := 914122407224, V2 := [[[18417372813348552492]], [[(-372764011004139), 3192087498683], [(-751632926713211)]], [[716098174538, (-36680553778), (-328544279)], [(-9658739505804), 164954388279], [21712780010]], [[(-12476181850), (-1078089917), 11744250, 33117], [20789443626, (-1878546592), (-25499867)], [(-1607433091), 2151834541], [(-169946804)]], [[288887726, 3141485, 20764, (-1988), (-3)], [(-358802756), (-56368727), 909509, 3427], [39801278, (-24016067), (-663497)], [10181207, 417771], [1901549]]], r2 := 20286967068, V3 := [[[18430953690220017140]], [[(-686296146635256), 3399621081529], [(-405146962804690)]], [[10793395527, 66954713179, (-695479624)], [(-17602602345081), 175723019338], [(-6869091974)]], [[6001727, (-3601026735), 2985587, 139541], [557594394, 3471420480, (-53962701)], [(-136894230), 2293902637], [(-1303945)]], [[(-81083), (-1948821), 1076685, (-3959), (-27)], [345100, (-186115479), 227804, 14434], [7268524, 45614257, (-1403455)], [(-37319), 471737], [5412]]], r3 := 196859517217, Vm := [[[18417383265459433803]], [[(-372916792726386), 0], [(-751089716593414)]], [[713438435468, 0, 0], [(-9666724310813), 0], [28889066658]], [[(-12471080617), 0, 0, 0], [20651399242, 0, 0], [(-1714191406), 0], [(-167562163)]], [[288866475, 0, 0, 0, 0], [(-358506294), 0, 0, 0], [37980854, 0, 0], [10132188, 0], [1891687]]], rm := 3435452498 }
noncomputable def w7 : Wit := { Z0 := { p := [[[941085008050315728]], [[(-33436410313964435), 188217001610063145], [3016394096229236]], [[401854558074452, (-6687282062792887), 0], [(-106103314247720), 603278819245847], [(-28984347301667)]], [[(-5946551631694), 80370911614890, 0, 0], [1332724613595, (-21220662849544), 0], [1022933997373, (-5796869460334)], [443936247811]], [[103177607530, (-1189310326339), 0, 0, 0], [(-23792000822), 266544922719, 0, 0], [(-12656097877), 204586799474, 0], [(-15681175594), 88787249562], [(-7975151829)]]], r := 651696667300, ok := true }, Z1 := { p := [[[1505736012880505165]], [[(-53498256502343095), 0], [4826230553966778]], [[642967292919124, 0, 0], [(-169765302796352), 0], [(-46374955682667)]], [[(-9514482610709), 0, 0, 0], [2132359381752, 0, 0], [1636694395797, 0], [710297996498]], [[165084172048, 0, 0, 0, 0], [(-38067201315), 0, 0, 0], [(-20249756603), 0, 0], [(-25089880950), 0], [(-12760242926)]]], r := 230407356728, ok := true }, Z2 := { p := [[[1971072827789837487754]], [[(-21979511679514983388), 188217001610063145], [(-44318990577707925428)]], [[306401551903186976, (-6687282062792887), 0], [495850218044446058, 603278819245847], [1075368577286228223]], [[(-4991457334847128), 80370911614890, 0, 0], [(-6734645472214150), (-21220662849544), 0], [(-12050105732627860), (-5796869460334)], [(-26640773684948321)]], [[94504416412064, (-1189310326339), 0, 0, 0], [105840915724994, 266544922719, 0, 0], [162275484400202, 204586799474, 0], [298786574939989, 88787249562], [666347581125182]]], r := 193835013068394, ok := true }, Z3 := { p := [[[3408912603555553677444]], [[(-131363824978417535453), 650720874561841399], [(-77549109044755221925)]], [[5427203206728689124, (-40931884594305073), 0], [3036022556207194216, 1905796622594226], [1889342347838254512]], [[(-228530677665149853), 1646640373398335, 0, 0], [(-126129719795828662), (-110396950733338), 0], [(-74380356481084950), (-18846467236362)], [(-46917475539509903)]], [[9708662109578290, (-68853469654125), 0, 0, 0], [5328437313473186, 4067526706720, 0, 0], [3096419320939229, 1119716249834, 0], [1853098754627568, 290833611378], [1175463692422358]]], r := 6121977522304519, ok := true }, iE := { p := [[[1974832577163462895471]], [[(-21998439719216243165), 0], [(-44306939715440551063)]], [[306729828161659443, 0, 0], [495793816422246719, 0], [1075252781284081564]], [[(-4997406465108699), 0, 0, 0], [(-6733284609890738), 0, 0], [(-12049550214595630), 0], [(-26639000105499746)]], [[94626484954022, 0, 0, 0, 0], [105811561022616, 0, 0, 0], [162263420575750, 0, 0], [298778012479848, 0], [666315719421049]]], r := 193588450291636, ok := true }, iHu := { p := [[[3413785074494346002069]], [[(-131472117984730953153), 0], [(-77534838811507991987)]], [[5431899942468892686, 0, 0], [3035776394072683641, 0], [1889201229168948099]], [[(-228730874679213782), 0, 0, 0], [(-126118729946785100), 0, 0], [(-74377712532713952), 0], [(-46915297834175921)]], [[9717214385149034, 0, 0, 0, 0], [5327976907689768, 0, 0, 0], [3096303547297717, 0, 0], [1853057057300395, 0], [1175424396255614]]], r := 6117478774321062, ok := true }, T := { p := [[[11529215046068469760]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[172309476183394081]], [[1919423281093852, 0], [3865900158798550]], [[(-5381792258471), 0, 0], [42868226594981, 0], [(-7084164190816)]], [[77963613878, 0, 0, 0], [(-138053722036), 0, 0], [(-81416297611), 0], [60488479863]], [[(-1694861481), 0, 0, 0, 0], [1999066291, 0, 0, 0], [(-1514718), 0, 0], [695270262, 0], [(-775494179)]]], r := 1897137284, ok := true }, de := { p := [[[(-103213394174167431731)]], [[578791610176251513, 0], [341338641898814995]], [[(-12577042213019948), 0, 0], [6350471213691, 0], [(-4374263859755129)]], [[364552014982792, 0, 0, 0], [118148020, 0, 0], [69677037, 0], [74773754889590]], [[(-11887565705029), 0, 0, 0, 0], [2199, 0, 0, 0], [1516663, 0, 0], [765, 0], [(-1437956824687)]]], r := 2312739462261, ok := true }, dde := { p := [[[(-31123435458060159236947)]], [[1352613806724062035306, 0], [797695321914190431723]], [[(-58809306717322526074), 0, 0], [(-34682418006994211366), 0], [(-20453729949680218956)]], [[2556926378813602638, 0, 0, 0], [1507930941115214086, 0, 0], [889292606298716641, 0], [524454614053257774]], [[(-111170712122332182), 0, 0, 0, 0], [(-65562214841380172), 0, 0, 0], [(-38664895935128379), 0, 0], [(-22802374524055677), 0], [(-13447554206492620)]]], r := 11824100452323481, ok := true }, nJu := { p := [[[(-206426788348334863462)]], [[1157583220352503026, 0], [682677283797629990]], [[(-25154084426039895), 0, 0], [12700942427382, 0], [(-8748527719510258)]], [[729104029965585, 0, 0, 0], [236296041, 0, 0], [139354075, 0], [149547509779181]], [[(-23775131410058), 0, 0, 0, 0], [4398, 0, 0, 0], [3033326, 0, 0], [1530, 0], [(-2875913649373)]]], r := 4625478924515, ok := true }, Jd1 := { p := [[[(-62246870916120318473893)]], [[2705227613448124070612, 0], [1595390643828380863447]], [[(-117618613434645052148), 0, 0], [(-69364836013988422731), 0], [(-40907459899360437911)]], [[5113852757627205277, 0, 0, 0], [3015861882230428172, 0, 0], [1778585212597433282, 0], [1048909228106515549]], [[(-222341424244664364), 0, 0, 0, 0], [(-131124429682760344), 0, 0, 0], [(-77329791870256758), 0, 0], [(-45604749048111353), 0], [(-26895108412985239)]]], r := 23648200904646953, ok := true }, term0 := { p := [[[72914253184714231468180426]], [[(-6336306210723926623371815), 0], [(-3734576296487691602184046)]], [[413149147721979300964391, 0, 0], [324641717775059084947059, 0], [143578411930276947759517]], [[(-23948118303878467043060), 0, 0, 0], [(-21170024042536476525162), 0, 0], [(-12482411420464299653817), 0], [(-4907652750465220191291)]], [[1301444790654946130992, 0, 0, 0, 0], [1227182208367093205048, 0, 0, 0], [814012312686453541643, 0, 0], [426684005960350551419, 0], [157277122028931098278]]], r := 241773050603134295623, ok := true }, r0 := { p := [[[9622734412259888244344]], [[(-369426443155246928172), 3826220934297900189806], [(-216110697455484564610)]], [[11503157352035916909, (-145300202365651344666), 373533555174018721848], [8189437277105850396, (-86075251581796094053)], [5245816081293840261]], [[(-352586580605352588), 4467893661560190971, (-13552673906235788155), (-1793628709480364906)], [(-246920906296125032), 3235981635299662237, (-8460506666811727047)], [(-197916848909877808), 2090275443454311180], [(-129978961859398227)]], [[11411263210934523, (-135774984745003130), 394378355583566522, 191187281123758594, (-83724752057155072)], [7294923889789057, (-96640387193657899), 307786690950536532, 29167252298369187], [5901846181501449, (-78299016163073046), 205819159892097950], [4891089212436826, (-51804768720452868)], [3251395391403654]]], r := 154299895219070270, ok := true }, r1 := { p := [[[24408173286475284440191]], [[(-921482222087700712584), 0], [(-549582002302778324216)]], [[28152284067575151513, 0, 0], [20571763542010564043, 0], [13349373740412586811]], [[(-852172781718035455), 0, 0, 0], [(-611225429568717599), 0, 0], [(-498086783426904210), 0], [(-330891211209019822)]], [[27495311638421345, 0, 0, 0, 0], [17875026269823947, 0, 0, 0], [14653568032582058, 0, 0], [12322048265371083, 0], [8279292703466101]]], r := 22460883262974973, ok := true }, r2 := { p := [[[16142350140448351991249154]], [[(-653091463926827775894323), 5976051188426250461833], [(-807111076270316915522686)]], [[23928117646227221566383, (-172311610754569879022), 458769656615121063], [32045789854646695014872, (-150387511461168616709)], [30581147613508404939609]], [[(-907650620932966601539), 5244147278854520794, 377291962978435, (-44664064513166)], [(-1157003522832743982139), 4152562348912554044, 113154217003315], [(-1200224306685207340843), 3829476600941325007], [(-1034642284482727036168)]], [[35995492671778021656, (-176734067912539255), (-7220191736000), 1053867935493, (-2080040713)], [43497116377449875331, (-121552472256010777), 2666677920842, (-1172609970778)], [42939222706905745582, (-103955704695274844), (-1111069722291)], [40272122279774253194, (-97780598593180834)], [32899418088679701650]]], r := 203738696697711663902, ok := true }, r3 := { p := [[[145419081881508837552807094]], [[(-12641686639814340345986254), 58000217763839270555090], [(-7458642063484405403741378)]], [[824382947640231314979466, (-4388482131886351278245), 1752207670110548232], [648489638715647871740925, (-1491929892747158707372)], [286887191850142259547816]], [[(-47788142875190035671326), 271957676016019204247, 8191134801405620, (-346736774457877)], [(-42290892084817944820849), 112800423768835831307, 140109863537], [(-24944461701857471261632), 38298367483329430525], [(-9808389951519079876896)]], [[2597110707558956479114, (-15353552812619978252), (-397032623326794), 7015245558342, (-299125637856)], [2451590484538285666904, (-6988077527402147101), 41220827041252, (-9125869787481)], [1626763809173138552880, (-2894779422464975689), (-1117157961480)], [852845821608857933809, (-982645887947943479)], [314376888679733593392]]], r := 24457816925712202065859, ok := true }, eta := { p := [[[(-16213061289431457942514947)]], [[656508188211028064726037, 0], [808888640685040255834239]], [[(-24077687804699601657232), 0, 0], [(-32131169457736831402128), 0], [(-30626403907303778026035)]], [[914102844001698909855, 0, 0, 0], [1160728756446150514830, 0, 0], [1202392731192338786688, 0], [1035797810111560058843]], [[(-36273880852886014033), 0, 0, 0, 0], [(-43657631752453069017), 0, 0, 0], [(-43033726636602501115), 0, 0], [(-40327407430515393100), 0], [(-32928959558362449025)]]], r := 21999622105681413652, 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 18014398509481984 22517998136852480 9223372036854775808 13835058055282163712 5764607523034234880 6917529027641081856 :=
  (RegionPosI.split_b 20266198323167232 (RegionPosI.split_s 6341068275337658368 (RegionPosI.split_b 19140298416324608 (RegionPosI.of_check c0 q0 ok_0 18014398509481984 19140298416324608 9223372036854775808 13835058055282163712 5764607523034234880 6341068275337658368 (by decide +kernel)) (RegionPosI.of_check c1 q1 ok_1 19140298416324608 20266198323167232 9223372036854775808 13835058055282163712 5764607523034234880 6341068275337658368 (by decide +kernel))) (RegionPosI.split_b 19140298416324608 (RegionPosI.of_check c2 q2 ok_2 18014398509481984 19140298416324608 9223372036854775808 13835058055282163712 6341068275337658368 6917529027641081856 (by decide +kernel)) (RegionPosI.of_check c3 q3 ok_3 19140298416324608 20266198323167232 9223372036854775808 13835058055282163712 6341068275337658368 6917529027641081856 (by decide +kernel)))) (RegionPosI.split_s 6341068275337658368 (RegionPosI.split_b 21392098230009856 (RegionPosI.of_check c4 q4 ok_4 20266198323167232 21392098230009856 9223372036854775808 13835058055282163712 5764607523034234880 6341068275337658368 (by decide +kernel)) (RegionPosI.of_check c5 q5 ok_5 21392098230009856 22517998136852480 9223372036854775808 13835058055282163712 5764607523034234880 6341068275337658368 (by decide +kernel))) (RegionPosI.split_b 21392098230009856 (RegionPosI.of_check c6 q6 ok_6 20266198323167232 21392098230009856 9223372036854775808 13835058055282163712 6341068275337658368 6917529027641081856 (by decide +kernel)) (RegionPosI.of_check c7 q7 ok_7 21392098230009856 22517998136852480 9223372036854775808 13835058055282163712 6341068275337658368 6917529027641081856 (by decide +kernel)))))

end CKLaneC.RSC2.S05_0055