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

import Definitions.Def_CK_CKLaneC_RSC2_S06_0011_part00

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

namespace CKLaneC.RSC2.S06_0011
open CKLaneC.TM3 CKLaneC.RSCell

noncomputable def w6 : Wit := { Z0 := { p := [[[1610009416523690306]], [[(-26691254570639512), 322001883304738061], [9831386743851708]], [[229150345231036, (-5338250914127903), 0], [(-168162603077100), 1966277348770341], [(-153425940070346)]], [[(-2828731191640), 45830069046207, 0, 0], [1743697667288, (-33632520615420), 0], [2591581997663, (-30685188014070)], [3946913286481]], [[48733153498, (-565746238328), 0, 0, 0], [(-27781927117), 348739533457, 0, 0], [(-25049564069), 518316399532, 0], [(-66505712496), 789382657296], [(-119533651839)]]], r := 3839313148641, ok := true }, Z1 := { p := [[[2576015066437904489]], [[(-42706007313023219), 0], [15730218790162734]], [[366640552369657, 0, 0], [(-269060164923360), 0], [(-245481504112553)]], [[(-4525969906623), 0, 0, 0], [2789916267660, 0, 0], [4146531196261, 0], [6315061258370]], [[77973045597, 0, 0, 0, 0], [(-44451083386), 0, 0, 0], [(-40079302511), 0, 0], [(-106409139994), 0], [(-191253842943)]]], r := 1581970597673, ok := true }, Z2 := { p := [[[1093028131153218430965]], [[(-7920402978771197999), 322001883304738061], [(-41046441881422438287)]], [[81796129058193558, (-5338250914127903), 0], [293264557302187363, 1966277348770341], [1679258880083254292]], [[(-1158104635132547), 45830069046207, 0, 0], [(-2865901022681491), (-33632520615420), 0], [(-11957860891511249), (-30685188014070)], [(-70312849058300162)]], [[22287747041168, (-565746238328), 0, 0, 0], [38182583342899, 348739533457, 0, 0], [114837149441004, 518316399532, 0], [499682120047342, 789382657296], [2975444231601356]]], r := 424156237574894, ok := true }, Z3 := { p := [[[3188432429991845810057]], [[(-134427226750253743743), 1875836788791052222], [(-123030597251001988716)]], [[6080416639495975773, (-96566608987512230), 0], [5271039706806600447, 9395342775422479], [5080189418006051071]], [[(-280359024445539704), 4313741458703973, 0, 0], [(-239765891307184944), (-432022480324001), 0], [(-218889828680955448), (-157141876270666)], [(-213862337534747848)]], [[13042808354088439, (-198256218263612), 0, 0, 0], [11091757329805217, 18003804240755, 0, 0], [9977429428111996, 7486693890751, 0], [9245221261903512, 4109007521565], [9083933834303691]]], r := 23596089124362843, ok := true }, iE := { p := [[[1097581297970415334579]], [[(-7938287066615636524), 0], [(-41018638352182349248)]], [[82027582815687329, 0, 0], [293140715360998675, 0], [1678824985789186194]], [[(-1161799681449044), 0, 0, 0], [(-2863698794925831), 0, 0], [(-11956020774891113), 0], [(-70301687039977831)]], [[22364596337809, 0, 0, 0, 0], [38140892822130, 0, 0, 0], [114807726081477, 0, 0], [499635244374517, 0], [2975106185965409]]], r := 422212977065347, ok := true }, iHu := { p := [[[3197005179428470338441]], [[(-134700770099920226835), 0], [(-122987659656448889719)]], [[6093061902848332773, 0, 0], [5269905644335121712, 0], [5079471264945337471]], [[(-280945317156614744), 0, 0, 0], [(-239714398920263163), 0, 0], [(-218869668579361891), 0], [(-213843558986354899)]], [[13070152890413290, 0, 0, 0, 0], [11089430057725766, 0, 0, 0], [9976515102546033, 0, 0], [9244685549059680, 0], [9083359494410663]]], r := 23566424266607456, ok := true }, T := { p := [[[11529215046068469760]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[310029304936380737]], [[2242295514873691, 0], [11586367188726135]], [[(-6952531912504), 0, 0], [84795181502112, 0], [(-41206913791019)]], [[110306792521, 0, 0, 0], [(-302423299836), 0, 0], [(-276125621589), 0], [595718007134]], [[(-2626352760), 0, 0, 0, 0], [4795945464, 0, 0, 0], [(-6059470), 0, 0], [3998132230, 0], [(-12950480285)]]], r := 12642894565, ok := true }, de := { p := [[[(-102226837469747566672)]], [[633935487190054804, 0], [578810662217006560]], [[(-15086746340057457), 0, 0], [12701778593114, 0], [(-12577041844925026)]], [[478944430016435, 0, 0, 0], [278735673, 0, 0], [254497788, 0], [364552014989908]], [[(-17105158213197), 0, 0, 0, 0], [6117, 0, 0, 0], [6067849, 0, 0], [5100, 0], [(-11887565705029)]]], r := 5582407229034, ok := true }, dde := { p := [[[(-28901284235469517643568)]], [[1375617402632355523982, 0], [1255998498055628959491]], [[(-65505604519423448823), 0, 0], [(-59809477703627367875), 0], [(-54608641952865295623)]], [[3119314500619505925, 0, 0, 0], [2848069760877471932, 0, 0], [2600411520801170127, 0], [2374288780326889361]], [[(-148538785743791611), 0, 0, 0, 0], [(-135622369592174670), 0, 0, 0], [(-123829120074557624), 0, 0], [(-113061370491775409), 0], [(-103229946970736156)]]], r := 36196470174224398, ok := true }, nJu := { p := [[[(-204453674939495133343)]], [[1267870974380109609, 0], [1157621324434013121]], [[(-30173492680114914), 0, 0], [25403557186228, 0], [(-25154083689850051)]], [[957888860032871, 0, 0, 0], [557471347, 0, 0], [508995577, 0], [729104029979816]], [[(-34210316426394), 0, 0, 0, 0], [12235, 0, 0, 0], [12135699, 0, 0], [10200, 0], [(-23775131410058)]]], r := 11164814458059, ok := true }, Jd1 := { p := [[[(-57802568470939035287136)]], [[2751234805264711047964, 0], [2511996996111257918982]], [[(-131011209038846897645), 0, 0], [(-119618955407254735750), 0], [(-109217283905730591246)]], [[6238629001239011850, 0, 0, 0], [5696139521754943864, 0, 0], [5200823041602340255, 0], [4748577560653778722]], [[(-297077571487583221), 0, 0, 0, 0], [(-271244739184349340), 0, 0, 0], [(-247658240149115247), 0, 0], [(-226122740983550817), 0], [(-206459893941472311)]]], r := 72392940348448789, ok := true }, term0 := { p := [[[62977579079306738775798794]], [[(-5993731482129387187054226), 0], [(-5464881830312182160973565)]], [[428025419034236047269730, 0, 0], [520285507937024130154993, 0], [356156997474861396263551]], [[(-27173097767034524375155), 0, 0, 0], [(-37158978455933241429235), 0, 0], [(-33911912810661120351925), 0], [(-20639584221723835268217)]], [[1617334891567504797202, 0, 0, 0, 0], [2359164597055050338127, 0, 0, 0], [2422093742795913645547, 0, 0], [1965335503671740154297, 0], [1121481808552762590118]]], r := 745733050800338416811, ok := true }, r0 := { p := [[[8279648424392098340951]], [[(-253641585623758386119), 3256538767498134797150], [(-304290837958516606577)]], [[7612924697221308194, (-98074562741115965067), 303945490916236385136], [8871319989114172513, (-120332935114856522466)], [12387646625294510781]], [[(-265460927333150013), 2921266777378950281, (-8493668915740069951), (-4176900159095564450)], [(-250679506323365481), 3466361950446438315, (-11485431418051293865)], [(-355491796636460008), 4904590812017628415], [(-517090642950820193)]], [[10549313229572737, (-102165240190690298), 244524258846839054, 247537232783477852, (-168893214044270777)], [8397911032513592, (-97417696639564714), 314264585200547795, 107376846587485790], [9845488293484206, (-139212362565758810), 470465716208668503], [14699092143462099, (-204868845917119316)], [21834104961447560]]], r := 418180328997072326, ok := true }, r1 := { p := [[[20659460151084139398543]], [[(-617017979014919008172), 0], [(-765386065930733694721)]], [[18324556691214958144, 0, 0], [21909426493544833608, 0], [31215976210448597753]], [[(-642191866416783015), 0, 0, 0], [(-614150315446544620), 0, 0], [(-880936360837137131), 0], [(-1304386799218313088)]], [[25740290994736609, 0, 0, 0, 0], [20668891096424903, 0, 0, 0], [24209445544684531, 0, 0], [36496599537890444, 0], [55116349937655500]]], r := 114538153204434852, ok := true }, r2 := { p := [[[6109238440219041069052138]], [[(-242860940331920833907333), 4241350057520027811672], [(-507215972610526020143782)]], [[9937242108352140984705, (-119565108673549546568), 454464481567016789], [19693974231078968723669, (-174881075515499879884)], [32183397490545861968592]], [[(-436260179607646737864), 4180367547095989367, 515711909566506, (-137857789373575)], [(-797165255094991554179), 4601788114486954092, 118333864259990], [(-1231429425932099917345), 7460289374797931153], [(-1830258194346430260814)]], [[19894103650707133393, (-170625589069036268), (-12981046465354), 1189647434486, 40950360652], [34879608626884604084, (-154930386912609132), 7602602107587, (-6096021403191)], [49509265133351241151, (-191045139018484486), (-2476433153664)], [69295608146399930947, (-320672819450731053)], [98029600339102923629]]], r := 370580459633167695303, ok := true }, r3 := { p := [[[125241878911995203918924673]], [[(-11924268175773675986071046), 101093022146115243972117], [(-10898714775972817728972064)]], [[851649264675083700791002, (-8968324391843673474200), 1438169624888557113], [1037820606558833760181759, (-4408545282268640887616)], [710963433497031443728973]], [[(-54070285450078938035504), 624982064695277158268, 32019231593718587, (-975429185512870)], [(-74126411487506981370229), 390858751696532919085, (-2795309503754738)], [(-67704199858505888690755), 191879483037207651662], [(-41220433244378938476355)]], [[3218373099864228285522, (-39189588419234831677), (-1955851629105782), (-291154996751), 322938165175], [4706323138544653632179, (-27230389511813962760), 253535509323999, (-41829104514873)], [4835856744711411743280, (-17008129638295528091), 37241157291017], [3925468810166918266673, (-8347633527114522598)], [2240409463987268136315]]], r := 97566840098357948934668, ok := true }, eta := { p := [[[(-6180487888824807273646987)]], [[246417111335056029985248, 0], [510219161683739264381795]], [[(-10105350814351664727142), 0, 0], [(-19843027534475250006460), 0], [(-32312579899914122311381)]], [[444206606632738716158, 0, 0, 0], [804201927410211154020, 0, 0], [1237827730454771611045, 0], [1835839454793089616979]], [[(-20270805946356690318), 0, 0, 0, 0], [(-35212275348807493124), 0, 0, 0], [(-49811222178915133542), 0, 0], [(-69571710781777506055), 0], [(-98271200436406470500)]]], r := 37442091599918722365, 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 := 51791395714760704, bh := 2251799813685248, tc := 11529215046068469760, th := 2305843009213693952, sc := 3314649325744685056, sh := 144115188075855872 }
noncomputable def q7 : Cert := { V0 := [[[1549584166930883472]], [[(-25414929374332372), 306770371785412847], [9357422821501960]], [[203622973407668, (-4928451455043512), (-932652236102840)], [(-154336002731324), 1814587144462608], [(-146953584540640)]], [[(-2302222511044), 36963483515615, 45437321656906, (-58463114434593)], [1409588563929, (-28070907277209), (-16729388634450)], [2427074113121, (-28839190769007)], [3783802916888]], [[36155454329, (-392476317043), (-1090806619288), 2727022774177, 540349370089], [(-20304048157), 212861838962, 811094773782, (-1004051782558)], [(-21329054536), 458269589477, 164205547834], [(-62468428318), 743819918693], [(-114659231354)]]], r0 := 16182971848238, V1 := [[[2459970899466337926]], [[(-39721541100696877), 0], [14624917886896668]], [[303211620277527, 0, 0], [(-230143626542202), 0], [(-231715100732385)]], [[(-3284016529400), 0, 0, 0], [1850851415379, 0, 0], [3716479941181, 0], [5974147858843]], [[51162297943, 0, 0, 0, 0], [(-25121882299), 0, 0, 0], [(-30105586810), 0, 0], [(-96045097138), 0], [(-181180218267)]]], r1 := 5781413051564, V2 := [[[18388116989801848399]], [[(-476397928883932), 19509776826450], [(-2534737747614666)]], [[1068250034979, (-24269809093), (-6122315092)], [(-21168995182778), 1709861062564], [361506950229]], [[(-17621813341), (-1885028741), 65314436, 1877970], [53106153459, (-1905512009), (-806664936)], [(-12706276696), 37858987411], [(-4686975169)]], [[397316837, 9171839, 528693, (-37779), (-569)], [(-871777614), (-169528404), 8530272, 330043], [187792954, (-31259278), (-35666973)], [127387493, 14041826], [87833654]]], r2 := 179938812721, V3 := [[[18428095091726438985]], [[(-810501676631930), 12172303428161], [(-812437148481377)]], [[14685421142, 420948707774, (-7542852051)], [(-35295199013895), 1068504711575], [(-70871808956)]], [[12917890, (-4911602303), (-192171838), 4582488], [1283707568, 37018379233, (-993931321)], [(-2468410858), 23755348544], [(-27630943)]], [[(-198002), (-4234150), 5500643, 74577, (-2754)], [1261057, (-430068228), (-25396402), 804973], [28255571, 826181254, (-43963410)], [(-1169463), 11187446], [163925]]], r3 := 753247530746, Vm := [[[18388184770357998353]], [[(-476656997858099), 0], [(-2528737147462227)]], [[1064144411553, 0, 0], [(-21192066835080), 0], [497369949589]], [[(-17619120915), 0, 0, 0], [52737551355, 0, 0], [(-13234398944), 0], [(-4580043963)]], [[397459676, 0, 0, 0, 0], [(-871416285), 0, 0, 0], [179152643, 0, 0], [126897877, 0], [87153563]]], rm := 29141658095 }
noncomputable def w7 : Wit := { Z0 := { p := [[[1557521624883794849]], [[(-25807122027486035), 311504324976758969], [9501822690924848]], [[213265318991722, (-5161424405497207), 0], [(-161504159345256), 1900364538184969], [(-148340148668738)]], [[(-2478937687057), 42653063798344, 0, 0], [1589538844566, (-32300831869052), 0], [2495570705213, (-29668029733748)], [3816364849308]], [[39217071144, (-495787537412), 0, 0, 0], [(-23762134650), 317907768913, 0, 0], [(-23006459192), 499114141042, 0], [(-64076500550), 763272969861], [(-115585397233)]]], r := 3682103782230, ok := true }, Z1 := { p := [[[2492034599814071759]], [[(-41291395243977656), 0], [15202916305479757]], [[341224510386755, 0, 0], [(-258406654952409), 0], [(-237344237869980)]], [[(-3966300299291), 0, 0, 0], [2543262151307, 0, 0], [3992913128340, 0], [6106183758894]], [[62747313831, 0, 0, 0, 0], [(-38019415439), 0, 0, 0], [(-36810334708), 0, 0], [(-102522400880), 0], [(-184936635572)]]], r := 1499378645150, ok := true }, Z2 := { p := [[[1077505584900633217328]], [[(-7606443506628039540), 311504324976758969], [(-40471081657548418598)]], [[75342070884346741, (-5161424405497207), 0], [282237892344482695, 1900364538184969], [1655790926996157371]], [[(-999435955684284), 42653063798344, 0, 0], [(-2652447478965699), (-32300831869052), 0], [(-11515683419431039), (-29668029733748)], [(-69332009057145771)]], [[17635846367213, (-495787537412), 0, 0, 0], [33160265060938, 317907768913, 0, 0], [106445895079076, 499114141042, 0], [481386446693511, 763272969861], [2933990946940851]]], r := 405546396597047, ok := true }, Z3 := { p := [[[2941847612998575993170]], [[(-113096340565105725032), 1698507250094627634], [(-113366413767605243463)]], [[4668562615071276014, (-81426946232759972), 0], [4430268296130094680, 8597454600412839], [4678937879541624215]], [[(-196488239441518172), 3315085813871287, 0, 0], [(-183931058989059240), (-368551872493461), 0], [(-183908267726252622), (-143335676244780)], [(-196916546633944079)]], [[8344520149048118, (-139024349687260), 0, 0, 0], [7767206418553207, 13964346721162, 0, 0], [7651415196245559, 6367259118956, 0], [7766015552838419, 3744714454709], [8362546768035328]]], r := 17044952523438442, ok := true }, iE := { p := [[[1082023880966724683150]], [[(-7623443808328963210), 0], [(-40443517322389792799)]], [[75553053669455968, 0, 0], [282122387496034943, 0], [1655360599288685968]], [[(-1002586777735488), 0, 0, 0], [(-2650474483496536), 0, 0], [(-11513955010091346), 0], [(-69320937964449585)]], [[17695996463712, 0, 0, 0, 0], [33125261138078, 0, 0, 0], [106419382817886, 0, 0], [481342349126635, 0], [2933655639207548]]], r := 403657910716621, ok := true }, iHu := { p := [[[2949919566501406652118]], [[(-113325555388123281493), 0], [(-113325555388123281493)]], [[4678256693804041883, 0, 0], [4429315327254949817, 0], [4678256693804041883]], [[(-196898750324297411), 0, 0, 0], [(-183891321076904497), 0, 0], [(-183891321076904497), 0], [(-196898750324297411)]], [[8362002751475456, 0, 0, 0, 0], [7765565311521788, 0, 0, 0], [7650710552640258, 0, 0], [7765565311521788, 0], [8362002751475456]]], r := 17020980171470304, ok := true }, T := { p := [[[11529215046068469760]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[314486928529632994]], [[2215730604723458, 0], [11754784497260571]], [[(-6348242539620), 0, 0], [83639628169605, 0], [(-41759189273147)]], [[91957076444, 0, 0, 0], [(-276149861070), 0, 0], [(-276149861070), 0], [603714271091]], [[(-1999067388), 0, 0, 0, 0], [3998131721, 0, 0, 0], [(-6060269), 0, 0], [3998131721, 0], [(-13124312232)]]], r := 11918826783, ok := true }, de := { p := [[[(-101015736286021915514)]], [[578836066889184414, 0], [578836066889184414]], [[(-12577041311655926), 0, 0], [12702893609210, 0], [(-12577041311655926)]], [[364552015001109, 0, 0, 0], [278772377, 0, 0], [278772377, 0], [364552015001109]], [[(-11887565705028), 0, 0, 0, 0], [6118, 0, 0, 0], [6069446, 0, 0], [6118, 0], [(-11887565705028)]]], r := 4322751169021, ok := true }, dde := { p := [[[(-26389287290191018907761)]], [[1146781188731384714293, 0], [1146781188731384714062]], [[(-49860064393278621265), 0, 0], [(-49860077102583994695), 0], [(-49860064393278621473)]], [[2167828886385377907, 0, 0, 0], [2167828885827549327, 0, 0], [2167828885827549337, 0], [2167828886385377842]], [[(-94253429842847018), 0, 0, 0, 0], [(-94253429842864989), 0, 0, 0], [(-94253429855004486), 0, 0], [(-94253429842864987), 0], [(-94253429842847050)]]], r := 25943910533198799, ok := true }, nJu := { p := [[[(-202031472572043831028)]], [[1157672133778368828, 0], [1157672133778368828]], [[(-25154082623311851), 0, 0], [25405787218421, 0], [(-25154082623311851)]], [[729104030002218, 0, 0, 0], [557544754, 0, 0], [557544754, 0], [729104030002218]], [[(-23775131410056), 0, 0, 0, 0], [12237, 0, 0, 0], [12138893, 0, 0], [12237, 0], [(-23775131410056)]]], r := 8645502338035, ok := true }, Jd1 := { p := [[[(-52778574580382037815522)]], [[2293562377462769428587, 0], [2293562377462769428124]], [[(-99720128786557242530), 0, 0], [(-99720154205167989390), 0], [(-99720128786557242945)]], [[4335657772770755814, 0, 0, 0], [4335657771655098655, 0, 0], [4335657771655098674, 0], [4335657772770755684]], [[(-188506859685694036), 0, 0, 0, 0], [(-188506859685729978), 0, 0, 0], [(-188506859710008971), 0, 0], [(-188506859685729973), 0], [(-188506859685694100)]]], r := 51887821066397592, ok := true }, term0 := { p := [[[52508049368450230712911299]], [[(-4562471203622774094877636), 0], [(-4556089117007225518163935)]], [[297477679838274438869370, 0, 0], [396032082280572644385296, 0], [296922715643288381945591]], [[(-17242915060285611713152), 0, 0, 0], [(-25824927530034154791610), 0, 0], [(-25812863091017375463704), 0], [(-17206721743225960014155)]], [[937044258856177763858, 0, 0, 0, 0], [1497002994688363254024, 0, 0, 0], [1683306212747902140424, 0, 0], [1495953913034460021872, 0], [934946095548371859904]]], r := 488964511064193680587, ok := true }, r0 := { p := [[[7800848761375944360287]], [[(-226070527682300337460), 3071317556712579055630], [(-287488568317429785456)]], [[6241446260683423143, (-87497511394594928545), 287872024655475015179], [7959894345384197449, (-113765592142339581065)], [11713628216912835827]], [[(-196380565900095322), 2393882727199880594, (-7609498750869243274), (-3714793869590101217)], [(-207175815524517814), 3112253390932111992, (-10889220772204391295)], [(-319649097051603817), 4640563893538479851], [(-489202982561516343)]], [[7019656513956825, (-75448523091258802), 199875536169398416, 215545481830734992, (-152421171204306974)], [6248056117197338, (-80475104393388703), 282953970923442165, 95632404940458167], [8158427882013614, (-125252637552540942), 446263288519602026], [13234049441016235, (-193930749475285110)], [20663855277264755]]], r := 354466477786722137, ok := true }, r1 := { p := [[[19493964102988131912034]], [[(-550682594805585319426), 0], [(-723870448574769851309)]], [[15010892583296918934, 0, 0], [19677350912995345085, 0], [29544977281104578138]], [[(-473847583579719544), 0, 0, 0], [(-507194423694528592), 0, 0], [(-792831163186246619), 0], [(-1235115067942060577)]], [[17081925367897452, 0, 0, 0, 0], [15343564785185864, 0, 0, 0], [20048233590629022, 0, 0], [32887527411861418, 0], [52205671655792047]]], r := 98644883468467084, ok := true }, r2 := { p := [[[5660066725348742664187390]], [[(-207776893126813273908648), 4017686410441041843928], [(-470760919023402262741214)]], [[7732414537457799825455, (-104675516978358749183), 455447605892672649], [16878314190499947458009, (-166251299612909359096)], [29902723374079195039801]], [[(-308121214951481961874), 3312802757366446886, 469079738697697, (-135466293022522)], [(-620861676954000786290), 4049107764506442067, 132781173985685], [(-1056511210564340481813), 7101667653128283908], [(-1701870082420228827279)]], [[12775091109349677627, (-122065810357826560), (-10472772922243), 1199879115529, 38620109337], [24642277227167438778, (-123173993326263500), 6871743975744, (-5993238344024)], [38581527828949634150, (-168435752091554890), (-2620077408625)], [59498818702960096451, (-305504620576637456)], [91207301613598631825]]], r := 312288456574335705162, ok := true }, r3 := { p := [[[104413575993612717565198710]], [[(-9076499105324220741515412), 85376037629745928820498], [(-9085949850240050210340211)]], [[591881569862828980542409, (-6873872048651802968142), 1495209215038804815], [789955710909346752205755, (-3723540161046005375914)], [592704532738936432725423]], [[(-34310112109633538762983), 436396553988110820688, 25389671186704920, (-973357051765392)], [(-51516087931377458382196), 299601064144022698739, (-2340140764232751)], [(-51534020621826865472884), 162071311035709828865], [(-34363825977128548892940)]], [[1864619010339416641820, (-24955836680017026964), (-1399078457592240), 1675189873143, 494665714829], [2986359553641351680271, (-19014913571702770337), 203969243467133, (-41945485820084)], [3360794545085868380991, (-13037371723853445134), 30354386357681], [2987919780613872760112, (-7050988565438250542)], [1867734516624266541755]]], r := 62345428527273293480310, ok := true }, eta := { p := [[[(-5724818199846802306552919)]], [[210745216133402077465904, 0], [473491717362796910094959]], [[(-7860634407018072616838), 0, 0], [(-17002761769087099209417), 0], [(-30020212680776041420074)]], [[313653155567440328961, 0, 0, 0], [626228561696179349849, 0, 0], [1061853651555835074651, 0], [1706946747719911972042]], [[(-13014437757445057078), 0, 0, 0, 0], [(-24873834094389173583), 0, 0, 0], [(-38811824626837253143), 0, 0], [(-59729366877820185998), 0], [(-91427076875946129321)]]], r := 32294163813419486470, 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 45035996273704960 54043195528445952 9223372036854775808 13835058055282163712 2305843009213693952 3458764513820540928 :=
  (RegionPosI.split_s 2882303761517117440 (RegionPosI.split_s 2594073385365405696 (RegionPosI.split_b 49539595901075456 (RegionPosI.of_check c0 q0 ok_0 45035996273704960 49539595901075456 9223372036854775808 13835058055282163712 2305843009213693952 2594073385365405696 (by decide +kernel)) (RegionPosI.of_check c1 q1 ok_1 49539595901075456 54043195528445952 9223372036854775808 13835058055282163712 2305843009213693952 2594073385365405696 (by decide +kernel))) (RegionPosI.split_b 49539595901075456 (RegionPosI.of_check c2 q2 ok_2 45035996273704960 49539595901075456 9223372036854775808 13835058055282163712 2594073385365405696 2882303761517117440 (by decide +kernel)) (RegionPosI.of_check c3 q3 ok_3 49539595901075456 54043195528445952 9223372036854775808 13835058055282163712 2594073385365405696 2882303761517117440 (by decide +kernel)))) (RegionPosI.split_b 49539595901075456 (RegionPosI.split_s 3170534137668829184 (RegionPosI.of_check c4 q4 ok_4 45035996273704960 49539595901075456 9223372036854775808 13835058055282163712 2882303761517117440 3170534137668829184 (by decide +kernel)) (RegionPosI.of_check c5 q5 ok_5 45035996273704960 49539595901075456 9223372036854775808 13835058055282163712 3170534137668829184 3458764513820540928 (by decide +kernel))) (RegionPosI.split_s 3170534137668829184 (RegionPosI.of_check c6 q6 ok_6 49539595901075456 54043195528445952 9223372036854775808 13835058055282163712 2882303761517117440 3170534137668829184 (by decide +kernel)) (RegionPosI.of_check c7 q7 ok_7 49539595901075456 54043195528445952 9223372036854775808 13835058055282163712 3170534137668829184 3458764513820540928 (by decide +kernel)))))

end CKLaneC.RSC2.S06_0011