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

import Definitions.Def_CK_CKLaneC_RSC2_S01_0317_part00

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

namespace CKLaneC.RSC2.S01_0317
open CKLaneC.TM3 CKLaneC.RSCell

theorem s2_4 : stageC2 w4 q4 = true := by decide +kernel
theorem s3_4 : stageC3 w4 q4 = true := by decide +kernel
theorem sE_4 : stageE w4 q4 = true := by decide +kernel
theorem sF_4 : stageF w4 = true := by decide +kernel
theorem ok_4 : (domOK c4 && cellCheck c4 q4) = true :=
  staged_check c4 q4 w4 (by decide +kernel) sB_4 s0_4 s1_4 s2_4 s3_4 sE_4 sF_4

noncomputable def c5 : Cell := { bc := 1583296743997440, bh := 35184372088832, tc := 16140901064495857664, th := 2305843009213693952, sc := 15852670688344145920, sh := 288230376151711744 }
noncomputable def q5 : Cert := { V0 := [[[162195803142053151]], [[(-19262600305819213), 23168244720672458], [345446771513251]], [[148424430899620, (-2750879316995334), (-553705652627)], [(-40760920691331), 49333026891053], [(-3102447353454)]], [[(-1267584524617), 21087054315699, 197255326946, (-26349596020)], [284630953244, (-5817118596605), (-3537487920)], [366647455246, (-443093637419)], [42079959078]], [[11461353764, (-175010251895), (-24939925705), 9382815191, 1857223], [(-2462553737), 39922164609, 1257412950, (-168267170)], [(-2624796028), 52337935616, 24237914], [(-4975512308), 6010018038], [(-663561262)]]], r0 := 456026972587, V1 := [[[185363467809387159]], [[(-22013272985806422), 0], [394776092669556]], [[169485360476491, 0, 0], [(-46576722119716), 0], [(-3545515599737)]], [[(-1441233205056), 0, 0, 0], [324387277752, 0, 0], [418976353003, 0], [48089661836]], [[12950182980, 0, 0, 0, 0], [(-2767556532), 0, 0, 0], [(-2993540582), 0, 0], [(-5685687323), 0], [(-758330031)]]], r1 := 85528131789, V2 := [[[18443801019453605731]], [[(-24943871674839), 4910812878], [(-65399214619737)]], [[12634631454, (-503603060), (-7843)], [(-554778300221), 219361812], [25811825]], [[(-101452770), (-4690559), 1675, 0], [310154985, (-22492836), (-526)], [(-6220271), 2464460], [(-161735)]], [[1036933, 2290, (-82), 0, 0], [(-2465051), (-209861), 112, 0], [395365, (-252632), (-12)], [37036, 245], [1619]]], r2 := 630719312, V3 := [[[18444022773356393391]], [[(-49477181615078), 9074441596], [(-60473544848705)]], [[18496758, (-841640746), (-28972)], [(-1099474042222), 405322966], [(-4553002)]], [[2089, (-18496519), 5903, 0], [826899, (-37585950), (-1942)], [422017, 4553045], [(-447)]], [[(-11), (-2083), (-239), (-1), 0], [103, (-826883), 396, 0], [9307, (-422026), (-44)], [39, 447], [2]]], r3 := 2236156615, Vm := [[[18443801024522013518]], [[(-24944410169079), 0], [(-65398987847021)]], [[12631858775, 0, 0], [(-554802433393), 0], [28368709]], [[(-101449152), 0, 0, 0], [310035215, 0, 0], [(-6493349), 0], [(-161397)]], [[1036933, 0, 0, 0, 0], [(-2464875), 0, 0, 0], [394120, 0, 0], [36991, 0], [1617]]], rm := 59262606 }
noncomputable def w5 : Wit := { Z0 := { p := [[[162204849083091441]], [[(-19265823379147016), 23172121297584491], [345504572654208]], [[148832086195091, (-2752260482735288), 0], [(-40781471584695), 49357796093458], [(-3102843344086)]], [[(-1288857828973), 21261726599298, 0, 0], [287220233307, (-5825924512100), 0], [366788434864, (-443263334870)], [42084875997]], [[11887478782, (-184122546997), 0, 0, 0], [(-2596530837), 41031461901, 0, 0], [(-2642601435), 52398347837, 0], [(-4977263317), 6012125142], [(-663634720)]]], r := 110707567827, ok := true }, Z1 := { p := [[[185376970380675932]], [[(-22018083861882304), 0], [394862368747666]], [[170093812794390, 0, 0], [(-46607396096795), 0], [(-3546106678955)]], [[(-1472980375969), 0, 0, 0], [328251695208, 0, 0], [419186782701, 0], [48097001139]], [[13585690036, 0, 0, 0, 0], [(-2967463814), 0, 0, 0], [(-3020115926), 0, 0], [(-5688300934), 0], [(-758439680)]]], r := 21367900137, ok := true }, Z2 := { p := [[[15356091033626890522960]], [[(-117699947936419585989), 23172121297584491], [(-308592196759502585245)]], [[1014447201423467449, (-2752260482735288), 0], [2389076838826392832, 49357796093458], [6563738053068324238]], [[(-9317607069230506), 21261726599298, 0, 0], [(-20514374695101058), (-5825924512100), 0], [(-51004875691649600), (-443263334870)], [(-141875577633958692)]], [[90252725570421, (-184122546997), 0, 0, 0], [186712263684381, 41031461901, 0, 0], [437406668842607, 52398347837, 0], [1104925523265636, 6012125142], [3089949403097776]]], r := 487583266867067, ok := true }, Z3 := { p := [[[16483893251698419838720]], [[(-271241014363500258718), 49747391886941609], [(-331524656649413920285)]], [[4721754724680141128, (-6345960176293285), 0], [5514618346621264486, 105142699997751], [7053643533690190665]], [[(-83519629246282241), 105189403029424, 0, 0], [(-96385126571161298), (-13230500430252), 0], [(-117803921275603332), (-945986682839)], [(-152492563041998306)]], [[1488461712877397, (-1835140264053), 0, 0, 0], [1708988479391268, 197780444423, 0, 0], [2062197658678577, 119422265005, 0], [2552930087117640, 12838381697], [3321604180820331]]], r := 2140923186218576, ok := true }, iE := { p := [[[15358565301245443711453]], [[(-117700886809338733967), 0], [(-308586926443719717082)]], [[1014472515086093136, 0, 0], [2389078739592992275, 0], [6563690722394456527]], [[(-9317917737990773), 0, 0, 0], [(-20514313525111983), 0, 0], [(-51004884436642904), 0], [(-141874935672596256)]], [[90256331617804, 0, 0, 0, 0], [186711366310135, 0, 0, 0], [437406141288833, 0, 0], [1104925605386611, 0], [3089939280034837]]], r := 487538196881916, ok := true }, iHu := { p := [[[16486375093804779481237]], [[(-271243154615676642161), 0], [(-331519411196936254674)]], [[4721828954519005025, 0, 0], [5514622897363983056, 0], [7053596339465680172]], [[(-83521120615003313), 0, 0, 0], [(-96385044275688760), 0, 0], [(-117803943001637008), 0], [(-152491922549400268)]], [[1488489770145749, 0, 0, 0, 0], [1708986397704595, 0, 0, 0], [2062196793812017, 0, 0], [2552930297261427, 0], [3321594077349560]]], r := 2140786918973756, ok := true }, T := { p := [[[16140901064495857664]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[22155869395779082]], [[169792257594765, 0], [445159525348212]], [[(-162243100753), 0, 0], [3376567033599, 0], [(-524389129931)]], [[983218986, 0, 0, 0], [(-3605668195), 0, 0], [(-4406927795), 0], [3884052172]], [[(-8938354), 0, 0, 0, 0], [21849311, 0, 0, 0], [(-5911), 0, 0], [32639094, 0], [(-43156135)]]], r := 21528721, ok := true }, de := { p := [[[(-126606283590887901512)]], [[241954448520070565, 0], [295722103746752912]], [[(-2199423640568197), 0, 0], [396623501533, 0], [(-3285558771712984)]], [[26659680636814, 0, 0, 0], [531953, 0, 0], [650165, 0], [48674945031001]], [[(-363541099592), 0, 0, 0, 0], [1, 0, 0, 0], [5912, 0, 0], [1, 0], [(-811249083849)]]], r := 100678890905, ok := true }, dde := { p := [[[(-180414313110315741433370)]], [[3280018266072799486964, 0], [4008911214088977146496]], [[(-59636696071312222371), 0, 0], [(-72889295594923286527), 0], [(-89086916353441738199)]], [[1084303564932530353, 0, 0, 0], [1325259912694246263, 0, 0], [1619762115515184870, 0], [1979709252297921627]], [[(-19714610271492757), 0, 0, 0, 0], [(-24095634776269267), 0, 0, 0], [(-29450220282121459), 0, 0], [(-35994713678140088), 0], [(-43993538939944468)]]], r := 3857244819619433, ok := true }, nJu := { p := [[[(-253212567181775803023)]], [[483908897040141130, 0], [591444207493505824]], [[(-4398847281136393), 0, 0], [793247003067, 0], [(-6571117543425968)]], [[53319361273628, 0, 0, 0], [1063907, 0, 0], [1300330, 0], [97349890062002]], [[(-727082199184), 0, 0, 0, 0], [2, 0, 0, 0], [11825, 0, 0], [3, 0], [(-1622498167698)]]], r := 201357781803, ok := true }, Jd1 := { p := [[[(-360828626220631482866740)]], [[6560036532145598973928, 0], [8017822428177954292992]], [[(-119273392142624444742), 0, 0], [(-145778591189846573054), 0], [(-178173832706883476398)]], [[2168607129865060707, 0, 0, 0], [2650519825388492527, 0, 0], [3239524231030369740, 0], [3959418504595843254]], [[(-39429220542985514), 0, 0, 0, 0], [(-48191269552538533), 0, 0, 0], [(-58900440564242918), 0, 0], [(-71989427356280176), 0], [(-87987077879888935)]]], r := 7714489639238862, ok := true }, term0 := { p := [[[2446510089982625366676384708]], [[(-88954160797544426827347405), 0], [(-108717087171020329137034025)]], [[2425933112165057102644617, 0, 0], [3953129956522551234963060, 0], [3623717442942694800687371]], [[(-58809415385285360163047), 0, 0, 0], [(-107810647287943352981699), 0, 0], [(-131766684093388141988178), 0], [(-107366658120343441316783)]], [[1336562836434939944129, 0, 0, 0, 0], [2613567353769678732785, 0, 0, 0], [3593592663579949905104, 0, 0], [3904134129325900681163, 0], [2982361376734667608990]]], r := 485099407731297784788, ok := true }, r0 := { p := [[[77567717553770049632679]], [[(-1808499320709985325855), 22158217587379485652469], [(-1560535550657501780332)]], [[31228054633131895022, (-515674360213992251093), 1581590788986024782010], [36703711584702010246, (-445804060581476015070)], [33208624163214419186]], [[(-476923188634419134), 8835187597752268945, (-36536929580856396375), (-162655123482022258)], [(-631887163431557384), 10470254459695742902, (-31825081352439532034)], [(-783549682769867236), 9486947282819318544], [(-718012982089496280)]], [[6906738721847021, (-133461021487415695), 606217768598759979, 42389671642797665, (-5797563656377522)], [9575980042661362, (-179149794260579353), 743156550263148085, 2580082653461685], [13474882571059782, (-223549585429553963), 677287410175220559], [16973540328010576, (-205121374831247000)], [15640973387995836]]], r := 119505986974233300, ok := true }, r1 := { p := [[[101307357478460932304777]], [[(-2360666713172699745457), 0], [(-2038162020508694020980)]], [[40665788618482094401, 0, 0], [47916424870282693444, 0], [43372806838215746144]], [[(-619001359856743645), 0, 0, 0], [(-823378060618463379), 0, 0], [(-1022961599833042500), 0], [(-937777622551213165)]], [[8931787793515754, 0, 0, 0, 0], [12444361059931875, 0, 0, 0], [17561946234465052, 0, 0], [22160306047226857, 0], [20428288368836936]]], r := 9985469176633897, ok := true }, r2 := { p := [[[1190078548639835655432373955]], [[(-24308878545302124885743089), 43361786279167529708036], [(-52552832228881123217997175)]], [[399892071085180175346513, (-629374796846875792164), 454225204688186545], [1065396925139602348577422, (-964397060551097539599)], [1745023715513999521551077]], [[(-6273441294166483974623), 8678775146406939250, 22854760977554, (-1709147878411)], [(-17381757245870968340082), 13819673713538146050, 47773403070002], [(-35213183935358817168514), 21436648838946499930], [(-51564666076158871202986)]], [[98677178650009623324, (-120246685980390740), (-61314119154963), (-8833210890047), (-310767385626)], [270488148192825850788, (-187625447868641388), (-36158170295214), (-1187641057989)], [571550600978144909704, (-305620489033962924), (-21728281020290)], [1037104873715526908743, (-476486309841899063)], [1429395744651828640711]]], r := 3211523754640030127047, ok := true }, r3 := { p := [[[4892046414000204171197279377]], [[(-177881084999223818285140613), 193066569959831989201569], [(-217412527102226874997109949)]], [[4851197721927806250285214, (-5409566246819629312336), 1813275154844565266], [7905654464463197753481003, (-4299588269975446173829)], [7246953760577352172015658]], [[(-117603525584323698966018), 132856179743654054673, 613960468976603, (-10343102049241)], [(-215606435200064495770871), 120402958034740840076, 18882828986078], [(-263519912515108584722044), 95621492532130202282], [(-214722623883278659707964)]], [[2672789990272366065901, (-3043080051388479341), (-241452361496551), (-48670549278952), (-1578545286403)], [5226794379860069885189, (-2956767916421217631), (-45073532653685), (-5826237412493)], [7186854726933992853240, (-2677259295840012174), (-335035358621538)], [7807969084008555062219, (-2125952746942276831)], [5964485045140994478269]]], r := 45819914846163715803171, ok := true }, eta := { p := [[[(-1190338366357579810456988366)]], [[24315205341017203138129411, 0], [52558549542776383168312612]], [[(-400019558592326613536091), 0, 0], [(-1065536132790916653931534), 0], [(-1745150283749339489749896)]], [[6275855098483139186648, 0, 0, 0], [17384559096344209324701, 0, 0], [35216265058184072488189, 0], [51567472165842367140492]], [[(-98721791045263738169), 0, 0, 0, 0], [(-270541201788686606141), 0, 0, 0], [(-571612624776264025380), 0, 0], [(-1037173235597831178141), 0], [(-1429458050850505050541)]]], r := 341331343572597275449, 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 := 1653665488175104, bh := 35184372088832, tc := 16140901064495857664, th := 2305843009213693952, sc := 15276209936040722432, sh := 288230376151711744 }
noncomputable def q6 : Cert := { V0 := [[[202166302521213555]], [[(-19954274315281427), 28875896062687138], [413342389611510]], [[156903217772172, (-2849128855842168), (-1072130340792)], [(-40479061940912), 59018218902754], [(-3552045042688)]], [[(-1369046066977), 22256852319839, 317412000833, (-51001665668)], [289363505126, (-5773658603323), (-6575024121)], [348522954772, (-507233989863)], [46118647349]], [[12672183684, (-188366537535), (-33812036052), 15089119050, 5585712], [(-2567355115), 40376278452, 1941295889, (-312563236)], [(-2552737103), 49729530449, 43064816], [(-4527880684), 6585989263], [(-696217767)]]], r0 := 438544098549, V1 := [[[231041075457639104]], [[(-22803070672837813), 0], [472353720985620]], [[179124653822402, 0, 0], [(-46250687097251), 0], [(-4059233919691)]], [[(-1555796915621), 0, 0, 0], [329524263392, 0, 0], [398239142903, 0], [52704100470]], [[14307106278, 0, 0, 0, 0], [(-2880915484), 0, 0, 0], [(-2909669839), 0, 0], [(-5173855232), 0], [(-795635615)]]], r1 := 81930828993, V2 := [[[18443722381927058169]], [[(-26107791444296), 6438095772], [(-64288240704571)]], [[13922009099, (-529089628), (-13128)], [(-556080132565), 275351640], [38443183]], [[(-115621669), (-5135349), 2271, 0], [327196351, (-22624956), (-843)], [(-7569014), 2961977], [(-226501)]], [[1223062, 2694, (-88), 0, 0], [(-2690353), (-220028), 145, 0], [399074, (-243288), (-18)], [42768, 283], [2170]]], r2 := 567732006, V3 := [[[18444005178585235281]], [[(-51676208734318), 11659573840], [(-58274614902966)]], [[20173705, (-837778883), (-47522)], [(-1099475808916), 498633887], [(-5362896)]], [[2395, (-20173478), 7729, 0], [863473, (-35819356), (-3050)], [385015, 5362961], [(-504)]], [[(-13), (-2388), (-227), 0, 0], [113, (-863458), 496, 0], [9304, (-385026), (-65)], [34, 504], [2]]], r3 := 2175212995, Vm := [[[18443722388622847518]], [[(-26108367181049), 0], [(-64287953748715)]], [[13918968049, 0, 0], [(-556104857400), 0], [41543767]], [[(-115617697), 0, 0, 0], [327070501, 0, 0], [(-7837367), 0], [(-226084)]], [[1223064, 0, 0, 0, 0], [(-2690168), 0, 0, 0], [397820, 0, 0], [42722, 0], [2168]]], rm := 53510097 }
noncomputable def w6 : Wit := { Z0 := { p := [[[202183820247134005]], [[(-19959461802449112), 28883402892447715], [413449845703780]], [[157456115525497, (-2851351686064159), 0], [(-40510801324074), 59064263671968], [(-3552748723137)]], [[(-1394316243284), 22493730789356, 0, 0], [292731053287, (-5787257332011), 0], [348731136627, (-507535531877)], [46127009960]], [[13176033443, (-199188034755), 0, 0, 0], [(-2719829754), 41818721898, 0, 0], [(-2574888390), 49818733803, 0], [(-4530355591), 6589572851], [(-696337361)]]], r := 105436753677, ok := true }, Z1 := { p := [[[231067223139581720]], [[(-22810813488513270), 0], [472514109375749]], [[179949846314854, 0, 0], [(-46298058656085), 0], [(-4060284255013)]], [[(-1593504278039), 0, 0, 0], [334549775185, 0, 0], [398549870431, 0], [52716582811]], [[15058323935, 0, 0, 0, 0], [(-3108376862), 0, 0, 0], [(-2942729588), 0, 0], [(-5177549247), 0], [(-795814127)]]], r := 20467385721, ok := true }, Z2 := { p := [[[14994282117769016231379]], [[(-117128089665791331816), 28883402892447715], [(-288418070052651775068)]], [[1031008875301852071, (-2851351686064159), 0], [2275189458086659149, 59064263671968], [5872968848520225687]], [[(-9691003050570687), 22493730789356, 0, 0], [(-19943819119992901), (-5787257332011), 0], [(-46498040628897737), (-507535531877)], [(-121534999999298339)]], [[96282625032949, (-199188034755), 0, 0, 0], [185658221736063, 41818721898, 0, 0], [407007406858872, 49818733803, 0], [964324146469753, 6589572851], [2534197478292260]]], r := 420259523479755, ok := true }, Z3 := { p := [[[16388029563483202173734]], [[(-279821786769351755873), 63135490487693521], [(-315551532607201495510)]], [[5054824553680289283, (-6817459051440669), 0], [5446721003377857837, 127839002364557], [6427946829742412462]], [[(-92783734877890727), 117459347730492, 0, 0], [(-98788894159063096), (-13574596841007), 0], [(-111400121474851280), (-1101085911974)], [(-133050309868891951)]], [[1715945216371397, (-2127519234719), 0, 0, 0], [1817686402575344, 211286080817, 0, 0], [2023649443879075, 117384846831, 0], [2311396182421517, 14306742354], [2774759808015713]]], r := 2061547629452032, ok := true }, iE := { p := [[[14996768716181666048303]], [[(-117129130376137314306), 0], [(-288412985156497470132)]], [[1031036274475405645, 0, 0], [2275191077478167765, 0], [5872925154324890491]], [[(-9691346303282841), 0, 0, 0], [(-19943754490918158), 0, 0], [(-46498046865547374), 0], [(-121534432696981033)]], [[96286712318441, 0, 0, 0, 0], [185657258646708, 0, 0, 0], [407006874938146, 0, 0], [964324195282043, 0], [2534188914247055]]], r := 420214493809214, ok := true }, iHu := { p := [[[16390526285152488235722]], [[(-279824234458867826239), 0], [(-315546477155744351643)]], [[5054908636715435576, 0, 0], [5446725128364026748, 0], [6427903286799529892]], [[(-92785477823149157), 0, 0, 0], [(-98788802136023338), 0, 0], [(-111400138578114452), 0], [(-133049744102262470)]], [[1715979166967438, 0, 0, 0, 0], [1817684046046277, 0, 0, 0], [2023648525933943, 0, 0], [2311396326924190, 0], [2774751263324018]]], r := 2061393585890804, ok := true }, T := { p := [[[16140901064495857664]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[22690379065042880]], [[177218467397293, 0], [436374000581889]], [[(-175848476077), 0, 0], [3374011253894, 0], [(-493637660209)]], [[1105883148, 0, 0, 0], [(-3741734715), 0, 0], [(-4219402977), 0], [3500686879]], [[(-10432859), 0, 0, 0, 0], [23529429, 0, 0, 0], [(-5911), 0, 0], [29920401, 0], [(-37241349)]]], r := 19294526, ok := true }, de := { p := [[[(-126520532200566461734)]], [[251084924803451543, 0], [283138319459211314]], [[(-2368549844161325), 0, 0], [396623879811, 0], [(-3011886153123207)]], [[29793079965004, 0, 0, 0], [555596, 0, 0], [626524, 0], [42721789641505]], [[(-421600188184), 0, 0, 0, 0], [1, 0, 0, 0], [5912, 0, 0], [1, 0], [(-681730685768)]]], r := 91711716653, ok := true }, dde := { p := [[[(-179255575224309109410560)]], [[3381929561043480043928, 0], [3813665249687328553028]], [[(-63809992069550665374), 0, 0], [(-71955948900614738669), 0], [(-81141814270424557329)]], [[1203962114519341683, 0, 0, 0], [1357659405733459460, 0, 0], [1530977627741992438, 0], [1726421580221100935]], [[(-22716266311673848), 0, 0, 0, 0], [(-25616215202536993), 0, 0, 0], [(-28886370334780928), 0, 0], [(-32573992079642554), 0], [(-36732374047251884)]]], r := 3632574087950962, ok := true }, nJu := { p := [[[(-253041064401132923467)]], [[502169849606903087, 0], [566276638918422629]], [[(-4737099688322649), 0, 0], [793247759623, 0], [(-6023772306246413)]], [[59586159930008, 0, 0, 0], [1111193, 0, 0], [1253048, 0], [85443579283010]], [[(-843200376367), 0, 0, 0, 0], [3, 0, 0, 0], [11825, 0, 0], [3, 0], [(-1363461371536)]]], r := 183423433294, ok := true }, Jd1 := { p := [[[(-358511150448618218821120)]], [[6763859122086960087857, 0], [7627330499374657106056]], [[(-127619984139101330748), 0, 0], [(-143911897801229477338), 0], [(-162283628540849114657)]], [[2407924229038683366, 0, 0, 0], [2715318811466918921, 0, 0], [3061955255483984877, 0], [3452843160442201870]], [[(-45432532623347695), 0, 0, 0, 0], [(-51232430405073985), 0, 0, 0], [(-57772740669561856), 0, 0], [(-65147984159285107), 0], [(-73464748094503767)]]], r := 7265148175901916, ok := true }, term0 := { p := [[[2415195217905244594285385259]], [[(-91129293885355231198831841), 0], [(-102758215583657882165251714)]], [[2579035244035076210883688, 0, 0], [3877452644752723502572133, 0], [3279346814625771839106052]], [[(-64880185824931694063138), 0, 0, 0], [(-109737189305701331448086), 0, 0], [(-123744343468089613373077), 0], [(-93028693975121495723407)]], [[1530176024708717409643, 0, 0, 0, 0], [2760658391475348905803, 0, 0, 0], [3502155070484530687497, 0, 0], [3510419031801914646347, 0], [2474128754656096266387]]], r := 457690306881768734781, ok := true }, r0 := { p := [[[78174010182305427494191]], [[(-1863882816430161316691), 22329189432414498611483], [(-1505764382124880868823)]], [[32934612236693432886, (-531157591777642829642), 1593159210658387238083], [36197069573780997677, (-430123677632787213682)], [30679166682006122405]], [[(-515715273505480337), 9307568154850402908, (-37545671083703884642), (-254541513603894969)], [(-637342564009964718), 10321029165557309465, (-30696063861502888690)], [(-739690048466535189), 8763711200661963998], [(-635091525234881016)]], [[7677403554945341, (-144085036195570373), 635630983458361222, 56242311413263941, (-9062693719597512)], [9896791734737979, (-180535502250187759), 731221583144069392, 3863394569465834], [13007290984851544, (-210948637338756751), 625475191923037374], [15339566862526615, (-181420144687750940)], [13245857384964474]]], r := 118168632756811210, ok := true }, r1 := { p := [[[102096095223631494488708]], [[(-2432527841099476911850), 0], [(-1966580122584838956945)]], [[42873505449080763581, 0, 0], [47248434238386919504, 0], [40068278513311589204]], [[(-669027436956292402), 0, 0, 0], [(-830261675419207161), 0, 0], [(-965578144423095231), 0], [(-829458913810171943)]], [[9922861006061095, 0, 0, 0, 0], [12856251318565401, 0, 0, 0], [16948314580221162, 0, 0], [20024620585759447, 0], [17299741814145637]]], r := 9429585684330612, ok := true }, r2 := { p := [[[1137701104618791394135103105]], [[(-23852442769832028762936592), 42755128597573926964467], [(-48083993910203478231024834)]], [[404183559871994532934472, (-637621661593325439992), 454186079830733545], [1000240682725356233513694, (-910102392357846362917)], [1528348077841499977572624]], [[(-6554234364357171084496), 9052559638418371141, 85429928995835, (-1825972251873)], [(-16805078862400744649732), 13391754593545962257, 64058996631209], [(-31639990706575210918068), 19366089712533491172], [(-43233323587971703143750)]], [[106875672532738016111, (-129531010109273268), (-59597279389351), (-8201650257377), (-288662972771)], [270273380147513024402, (-187100535786470724), (-66368932917182), (-908844606169)], [528770770619592690044, (-283477217762559526), (-27920213046295)], [891954778773058264406, (-412107118779971710)], [1147309510003693399332]]], r := 2703465980041429034343, ok := true }, r3 := { p := [[[4829403284470829216226445455]], [[(-182229763644155543208746377), 195724776047914815668157], [(-205495420199416095247261412)]], [[5157334222831264640716560, (-5724910705717286282611), 1811776153069344712], [7754291817138300363426240, (-4173276760612086642141)], [6558246517661023663259766]], [[(-129742849751041693783450), 146323477766821133284, 843490554976478, (-11625269316426)], [(-219458709276148474138202), 121999424566789957393, 93926067780168], [(-247475632959447542151614), 88862413466357377013], [(-186047874435181789297427)]], [[3059952554510544416708, (-3483739946724774793), (-112178429032560), (-45640847025083), (-1549003566489)], [5520943667426223296660, (-3117631132485545938), 3421273555459, (-5756585867908)], [7003976623956295771898, (-2597308510125382261), (-96904052185378)], [7020560044650615303679, (-1891772460892075159)], [4948054724800895560011]]], r := 43615088562969490987351, ok := true }, eta := { p := [[[(-1137962600542857959288001918)]], [[23859020617067058520499957, 0], [48089502732984404153440959]], [[(-404320646645259941220860), 0, 0], [(-1000379230724617096475737), 0], [(-1528464836334798039990263)]], [[6556922201281363041454, 0, 0, 0], [16807962834909276924395, 0, 0], [31642926538738417711559, 0], [43235801989685097927126]], [[(-106927169072598733712), 0, 0, 0, 0], [(-270329896608343913871), 0, 0, 0], [(-528831905437413544965), 0, 0], [(-892017107893242289884), 0], [(-1147362215085549454243)]]], r := 286610856592868871707, 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 := 1653665488175104, bh := 35184372088832, tc := 16140901064495857664, th := 2305843009213693952, sc := 15852670688344145920, sh := 288230376151711744 }
noncomputable def q7 : Cert := { V0 := [[[162874613268462708]], [[(-19342694147177174), 23265185013677797], [333521576857057]], [[148983472014019, (-2762309711388296), (-560686014839)], [(-39351628406125), 47629863952753], [(-2865032829793)]], [[(-1272421384142), 21165458382388, 199736474939, (-26681628357)], [274545102135, (-5615946443727), (-3444009588)], [338576195060, (-409185227555)], [37194238209]], [[11507677602, (-175625807865), (-25252334702), 9500748153, 1896404], [(-2375469998), 38500940974, 1224139269, (-163819192)], [(-2422314397), 48330586747, 22534441], [(-4397665542), 5312212914], [(-561453082)]]], r0 := 406467373476, V1 := [[[186139210916447804]], [[(-22104794622500280), 0], [381147833001000]], [[170122478430896, 0, 0], [(-44966292537550), 0], [(-3274194450741)]], [[(-1446668726637), 0, 0, 0], [312884603048, 0, 0], [386898379327, 0], [42506170633]], [[13001326631, 0, 0, 0, 0], [(-2669280384), 0, 0, 0], [(-2762570941), 0, 0], [(-5025358612), 0], [(-641638784)]]], r1 := 73603574638, V2 := [[[18443670221126344947]], [[(-26053452865864), 5359396290], [(-65399113263025)]], [[13256505202, (-549599455), (-8943)], [(-554802748380), 229222564], [24878710]], [[(-106393820), (-5119749), 1910, 0], [311710094, (-23503656), (-574)], [(-6006601), 2465907], [(-149552)]], [[1087355, 2509, (-93), 0, 0], [(-2475936), (-219330), 122, 0], [382360, (-252777), (-12)], [34244, 237], [1432]]], r2 := 561384121, V3 := [[[18443901826248480434]], [[(-51676128011138), 9903303253], [(-60473563066009)]], [[20187792, (-918501064), (-33032)], [(-1099472353683), 423540448], [(-4555636)]], [[2302, (-20187520), 6730, 0], [864139, (-39274525), (-2120)], [422251, 4555681], [(-432)]], [[(-12), (-2294), (-272), (-1), 0], [109, (-864122), 432, 0], [9313, (-422260), (-45)], [38, 432], [2]]], r3 := 2067417883, Vm := [[[18443670226658528383]], [[(-26054040719117), 0], [(-65398876258763)]], [[13253488009, 0, 0], [(-554827974399), 0], [27437588]], [[(-106389841), 0, 0, 0], [311585353, 0, 0], [(-6279944), 0], [(-149225)]], [[1087355, 0, 0, 0, 0], [(-2475751), 0, 0, 0], [381119, 0, 0], [34200, 0], [1431]]], rm := 52905687 }
noncomputable def w7 : Wit := { Z0 := { p := [[[162883773266017689]], [[(-19345957771975983), 23269110466573955], [333577850780478]], [[149396236366855, (-2763708253139427), 0], [(-39371635588891), 47653978682925], [(-2865400990185)]], [[(-1293959027368), 21342319480979, 0, 0], [277065714071, (-5624519369842), 0], [338707263883, (-409342998598)], [37198612572]], [[11938975854, (-184851289624), 0, 0, 0], [(-2505875229), 39580816295, 0, 0], [(-2438867464), 48386751983, 0], [(-4399223305), 5314087510], [(-561515632)]]], r := 98291607363, ok := true }, Z1 := { p := [[[186152883732591644]], [[(-22109666025115409), 0], [381231829463404]], [[170738555847834, 0, 0], [(-44996154958732), 0], [(-3274743988783)]], [[(-1478810316992), 0, 0, 0], [316646530367, 0, 0], [387094015867, 0], [42512700082]], [[13644543833, 0, 0, 0, 0], [(-2863857404), 0, 0, 0], [(-2787277101), 0, 0], [(-5027683777), 0], [(-641732151)]]], r := 18386445985, ok := true }, Z2 := { p := [[[14764073954838555051157]], [[(-113117343810182371868), 23269110466573955], [(-283946009687931784172)]], [[975095494957633581, (-2763708253139427), 0], [2197585286852423957, 47653978682925], [5781571172633732764]], [[(-8959395754859252), 21342319480979, 0, 0], [(-18872107807553526), (-5624519369842), 0], [(-44914164416353309), (-409342998598)], [(-119639474450136985)]], [[86825291856808, (-184851289624), 0, 0, 0], [171813886605317, 39580816295, 0, 0], [385210830854878, 48386751983, 0], [931501850810625, 5314087510], [2494611887840633]]], r := 401237850459980, ok := true }, Z3 := { p := [[[15847889490092912336330]], [[(-260663423747028011494), 49953992913825529], [(-305039224137886057700)]], [[4536890375344518213, (-6371956071292338), 0], [5072348072490372746, 101506598570036], [6212953684044143200]], [[(-80241959673681402), 105577835294543, 0, 0], [(-88643495211067708), (-12771494583614), 0], [(-103731636770518017), (-873554252408)], [(-128589653749714273)]], [[1429950870663874, (-1841636937407), 0, 0, 0], [1571598110648088, 190746065168, 0, 0], [1815638473252827, 110269092326, 0], [2152140246064741, 11347285331], [2681577627866732]]], r := 1823391972753768, ok := true }, iE := { p := [[[14766558578745041447973]], [[(-113118278915906213420), 0], [(-283940921301985751788)]], [[975120928904900646, 0, 0], [2197587153594912318, 0], [5781527463897993594]], [[(-8959708188825333), 0, 0, 0], [(-18872048666291320), 0, 0], [(-44914172690583678), 0], [(-119638907023681713)]], [[86828920505098, 0, 0, 0, 0], [171813018394836, 0, 0, 0], [385210343229519, 0, 0], [931501925761088, 0], [2494603322499018]]], r := 401196532288936, ok := true }, iHu := { p := [[[15850381639294946521088]], [[(-260665554982981266612), 0], [(-305034160086468508104)]], [[4536964766410623598, 0, 0], [5072352538772539099, 0], [6212910103393106404]], [[(-80243455126095682), 0, 0, 0], [(-88643416232918633), 0, 0], [(-103731657293667897), 0], [(-128589087646257175)]], [[1429979009646410, 0, 0, 0, 0], [1571596107564938, 0, 0, 0], [1815637677981965, 0, 0], [2152140437294409, 0], [2681569079457469]]], r := 1823261303921176, ok := true }, T := { p := [[[16140901064495857664]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[23044121289759437]], [[176528019411312, 0], [443107240913074]], [[(-169454460786), 0, 0], [3359319760101, 0], [(-502076489804)]], [[1026917607, 0, 0, 0], [(-3605691838), 0, 0], [(-4219426619), 0], [3560527680]], [[(-9335614), 0, 0, 0, 0], [21849311, 0, 0, 0], [(-5911), 0, 0], [29920401, 0], [(-37877953)]]], r := 18910334, ok := true }, de := { p := [[[(-126027604753861935773)]], [[241955241769674296, 0], [283139112709193325]], [[(-2199423639480643), 0, 0], [396626102204, 0], [(-3011886151846513)]], [[26659680636815, 0, 0, 0], [555601, 0, 0], [650171, 0], [42721789641507]], [[(-363541099592), 0, 0, 0, 0], [1, 0, 0, 0], [5912, 0, 0], [1, 0], [(-681730685768)]]], r := 86209903276, ok := true }, dde := { p := [[[(-172737674617108421239201)]], [[3140443019155138465857, 0], [3674986511777289676257]], [[(-57098964323600009830), 0, 0], [(-66817937371082221417), 0], [(-78191202842412889839)]], [[1038162987701360872, 0, 0, 0], [1214871581351534303, 0, 0], [1421658233496474091, 0], [1663642613667602318]], [[(-18875690685471826), 0, 0, 0, 0], [(-22088574206409888), 0, 0, 0], [(-25848331518149976), 0, 0], [(-30248047521225265), 0], [(-35396651354624457)]]], r := 3237480336583169, ok := true }, nJu := { p := [[[(-252055209507723871545)]], [[483910483539348592, 0], [566278225418386651]], [[(-4398847278961286), 0, 0], [793252204409, 0], [(-6023772303693025)]], [[53319361273631, 0, 0, 0], [1111202, 0, 0], [1300343, 0], [85443579283014]], [[(-727082199184), 0, 0, 0, 0], [3, 0, 0, 0], [11825, 0, 0], [3, 0], [(-1363461371536)]]], r := 172419806543, ok := true }, Jd1 := { p := [[[(-345475349234216842478402)]], [[6280886038310276931714, 0], [7349973023554579352514]], [[(-114197928647200019660), 0, 0], [(-133635874742164442834), 0], [(-156382405684825779678)]], [[2076325975402721744, 0, 0, 0], [2429743162703068607, 0, 0], [2843316466992948182, 0], [3327285227335204636]], [[(-37751381370943651), 0, 0, 0, 0], [(-44177148412819776), 0, 0, 0], [(-51696663036299951), 0, 0], [(-60496095042450530), 0], [(-70793302709248913)]]], r := 6474960673166334, ok := true }, term0 := { p := [[[2242757150581827358347223782]], [[(-81545381726875331539005098), 0], [(-95421170353721644341009533)]], [[2223879307744582350933842, 0, 0], [3469660286331816007762640, 0], [3045193720787018825620600]], [[(-53911187479305642997083), 0, 0, 0], [(-94625276410692892715170), 0, 0], [(-110730052144827666640943), 0], [(-86386165414273881484528)]], [[1225240104125108262231, 0, 0, 0, 0], [2293924006230434267057, 0, 0, 0], [3019871740543401356073, 0, 0], [3141224361830936189474, 0], [2297467554619473822388]]], r := 391716337916063410947, ok := true }, r0 := { p := [[[74573976610773673822592]], [[(-1738095983234913510009), 21302984780688301729652], [(-1435842703329430595830)]], [[30015943661844606431, (-495590925054733370745), 1520537511563715549668], [33761963816680039038, (-410182170700873338677)], [29250250964678613524]], [[(-458551900584964557), 8491544875927967071, (-35111482856885777165), (-157687972980827694)], [(-581295193237078456), 9630967265213929117, (-29281985591267230535)], [(-689985771413498875), 8356122842817373660], [(-605458161377746491)]], [[6643540586011626, (-128298852496675754), 582435551343378303, 41092629506396166, (-5620424173273481)], [8811468770654105, (-164796993204426019), 683553709956533774, 2390855573711828], [11866825270450844, (-196853465631431590), 596554039685678954], [14309519318416384, (-172966662271890456)], [12627023624889995]]], r := 105746689152989227, ok := true }, r1 := { p := [[[97397335595618362962795]], [[(-2268755837039001656469), 0], [(-1875304383514188467041)]], [[39086365524778451987, 0, 0], [44075838266457256684, 0], [38202881716746550277]], [[(-595127557305533782), 0, 0, 0], [(-757441533026864573), 0, 0], [(-900806646590297782), 0], [(-790772572760266193)]], [[8590792928317131, 0, 0, 0, 0], [11450456329420969, 0, 0, 0], [15465919764788985, 0, 0], [18682161653250132, 0], [16491839260144458]]], r := 8296743605648287, ok := true }, r2 := { p := [[[1091562174328786739154015750]], [[(-22311076226277311471334549), 41515089695313179236176], [(-46148638440876060744898004)]], [[367287613658747592661715, (-602905954370631069752), 454399730561010778], [936129197548157969624769, (-884046559082874347864)], [1467117609688724519025819]], [[(-5765900487888313474491), 8319387963913607557, 54434818924762, (-1617442497408)], [(-15282937543990773847195), 12673925959942757589, 51515710353047], [(-29622240321743800808582), 18814531803153138212], [(-41506978105338453112870)]], [[90748143611099613826, (-115352447311686655), (-60234958978510), (-7574212199746), (-273616588888)], [237982131645998958713, (-172154326408479994), (-15127533107875), (-858636233224)], [481110366193225120170, (-268348707929328079), (-19540625005070)], [835279532396639314250, (-400404536331741594)], [1101613126428190075058]]], r := 2504128453248209821661, ok := true }, r3 := { p := [[[4484581987079815524356122459]], [[(-163064686221392877234795958), 184833596904144173850042], [(-190822496859041234867103497)]], [[4447118567465731904527802, (-5179012841818023541583), 1813672692614743610], [6938765560892390333868437, (-3941180105090670033109)], [6089965165171093748882440]], [[(-107807721107263356734871), 127195121246071429910, 774694035641055, (-9973284161652)], [(-189236931123808570990232), 110368415467710063687, (-58600314376799)], [(-221448294276437092209612), 83921539433047946772], [(-172763345640147509947162)]], [[2450158789028836576719, (-2913455225126933240), (-303427353053198), (-41812688477052), (-1389853174538)], [4587536086573547645456, (-2710218537961341364), (-142635258185260), (-5164605357433)], [6039453444573734986125, (-2349754271641512223), (-291332975559229)], [6282197229377772456505, (-1786446166866665614)], [4594743627802051239711]]], r := 37002014307914250306030, ok := true }, eta := { p := [[[(-1091811042196020460946228592)]], [[22317136408176694815112183, 0], [46153881268509680518195823]], [[(-367409734863399950862490), 0, 0], [(-936256854284752383397546), 0], [(-1467228731550446555244169)]], [[5768212757875333677850, 0, 0, 0], [15285506986903986923361, 0, 0], [29624945447540469934411, 0], [41509336875253819306098]], [[(-90790923881185124879), 0, 0, 0, 0], [(-238030761605139494309), 0, 0, 0], [(-481164797497758527439), 0, 0], [(-835336960436585397782), 0], [(-1101663257959249175541)]]], r := 267067447121416048925, 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 1548112371908608 1688849860263936 13835058055282163712 18446744073709551616 13835058055282163712 16140901064495857664 :=
  (RegionPosI.split_s 14987979559889010688 (RegionPosI.split_b 1618481116086272 (RegionPosI.split_s 14411518807585587200 (RegionPosI.of_check c0 q0 ok_0 1548112371908608 1618481116086272 13835058055282163712 18446744073709551616 13835058055282163712 14411518807585587200 (by decide +kernel)) (RegionPosI.of_check c1 q1 ok_1 1548112371908608 1618481116086272 13835058055282163712 18446744073709551616 14411518807585587200 14987979559889010688 (by decide +kernel))) (RegionPosI.split_s 14411518807585587200 (RegionPosI.of_check c2 q2 ok_2 1618481116086272 1688849860263936 13835058055282163712 18446744073709551616 13835058055282163712 14411518807585587200 (by decide +kernel)) (RegionPosI.of_check c3 q3 ok_3 1618481116086272 1688849860263936 13835058055282163712 18446744073709551616 14411518807585587200 14987979559889010688 (by decide +kernel)))) (RegionPosI.split_b 1618481116086272 (RegionPosI.split_s 15564440312192434176 (RegionPosI.of_check c4 q4 ok_4 1548112371908608 1618481116086272 13835058055282163712 18446744073709551616 14987979559889010688 15564440312192434176 (by decide +kernel)) (RegionPosI.of_check c5 q5 ok_5 1548112371908608 1618481116086272 13835058055282163712 18446744073709551616 15564440312192434176 16140901064495857664 (by decide +kernel))) (RegionPosI.split_s 15564440312192434176 (RegionPosI.of_check c6 q6 ok_6 1618481116086272 1688849860263936 13835058055282163712 18446744073709551616 14987979559889010688 15564440312192434176 (by decide +kernel)) (RegionPosI.of_check c7 q7 ok_7 1618481116086272 1688849860263936 13835058055282163712 18446744073709551616 15564440312192434176 16140901064495857664 (by decide +kernel)))))

end CKLaneC.RSC2.S01_0317