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

import Definitions.Def_CK_CKLaneC_RSC2_S10_0031_part00

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

namespace CKLaneC.RSC2.S10_0031
open CKLaneC.TM3 CKLaneC.RSCell

noncomputable def c5 : Cell := { bc := 936748722493063168, bh := 72057594037927936, tc := 16140901064495857664, th := 2305843009213693952, sc := 6629298651489370112, sh := 288230376151711744 }
noncomputable def q5 : Cert := { V0 := [[[2461186666993307187]], [[(-84474421037102149), 342630479449562505], [44572142313419421]], [[945947981238227, (-11148632666320409), (-1864031624199653)], [(-1422327928529337), 5882472299928725], [(-879793223388813)]], [[(-14636136628391), 93657278669675, 187141981426991, (-75490782612878)], [13859101042933, (-154804223091017), (-98743725338060)], [30648248517281, (-124794177098636)], [40155203128344]], [[276810315906, (-892832684534), (-8112473888464), 6679400440112, 1315342054250], [(-256996299147), (-128374246576), 9500450941065, (-3524323497338)], [(-358298003271), 4233639387698, 273946838002], [(-1372875779308), 5592292436638], [(-2101774690672)]]], r0 := 216528841771827, V1 := [[[2801878961751658154]], [[(-95429448903180661), 0], [50352460841792225]], [[1031295068466710, 0, 0], [(-1567390607759416), 0], [(-1004281041089727)]], [[(-15309886633463), 0, 0, 0], [13343599204665, 0, 0], [34832912115206, 0], [45715923889378]], [[283001408149, 0, 0, 0, 0], [(-225807542403), 0, 0, 0], [(-396620190997), 0, 0], [(-1550715935253), 0], [(-2393664157448)]]], r1 := 98795380532141, V2 := [[[17208480610828971632]], [[(-17078379075216495), 6470395633186887], [(-94988216394814073)]], [[59753851896226, (-65760000370846), (-30713341773513)], [(-1354726803116307), 1022016286295490], [(-284133040325)]], [[(-961012081824), (-2535940914709), 1058908855793, 139497733306], [5797539848505, (-10211115386938), (-7285216040381)], [(-2058676800985), 41825177022565], [(-808607437281)]], [[22265904368, 11967926583, 4541126355, (-8237487985), (-615867772)], [(-89784899282), (-411397531123), 251370179717, 43942107471], [71276431987, (-410758380112), (-585504688196)], [39984768962, 94860475663], [19738014694]]], r2 := 77699179210153, V3 := [[[17766592498824049445]], [[(-29415422809663108), 6927751529846482], [(-52874521214676333)]], [[7255507597763, 141844655389257, (-64902463743529)], [(-2274372527167470), 1098392351409787], [(-44254253102646)]], [[10932879535, (-7357590375983), 196132629211, 586673845488], [1147454278180, 22530660196255, (-15450663542515)], [(-930982321205), 45485104672548], [(-100134004704)]], [[(-155222848), (-9431705949), 102985039018, (-15818944649), (-5191203590)], [1903179202, (-1171800171783), 46986414205, 185840640992], [47313783503, 927516656605, (-1252890190125)], [(-1849990098), 135263456792], [898255479]]], r3 := 169572318763538, Vm := [[[17218791957643277611]], [[(-17314626754533503), 0], [(-93264297684853395)]], [[58723321443457, 0, 0], [(-1395273201636051), 0], [80298065287732]], [[(-944016635529), 0, 0, 0], [5615397085791, 0, 0], [(-4048893706923), 0], [(-154165890779)]], [[22307819682, 0, 0, 0, 0], [(-85793800732), 0, 0, 0], [61031010322, 0, 0], [20705852741, 0], [19116124291]]], rm := 20246645566202 }
noncomputable def w5 : Wit := { Z0 := { p := [[[2493298440663619796]], [[(-87816364809663504), 356185491523374256], [46335487851693388]], [[1101159452143733, (-12545194972809072), 0], [(-1602897253674856), 6619355407384769], [(-881806453623636)]], [[(-19345233541304), 157308493163390, 0, 0], [22127628783036, (-228985321953551), 0], [30975167485229, (-125972350517663)], [40668419140795]], [[397367472613, (-2763604791615), 0, 0, 0], [(-508249848584), 3161089826148, 0, 0], [(-378255680833), 4425023926461, 0], [(-1426837792200), 5809774162970], [(-2125738618175)]]], r := 51620017892222, ok := true }, Z1 := { p := [[[2849483932186994053]], [[(-100361559782472575), 0], [52954843259078158]], [[1258467945307123, 0, 0], [(-1831882575628407), 0], [(-1007778804141298)]], [[(-22108838332919), 0, 0, 0], [25288718609184, 0, 0], [35400191411690, 0], [46478193303765]], [[454134254415, 0, 0, 0, 0], [(-580856969810), 0, 0, 0], [(-432292206666), 0, 0], [(-1630671762514), 0], [(-2429415563629)]]], r := 25835613820891, ok := true }, Z2 := { p := [[[81188239307066157248]], [[(-940138932792333889), 356185491523374256], [(-5228957619219242411)]], [[15068241574369155, (-12545194972809072), 0], [56450243272922140, 6619355407384769], [364360770386501052]], [[(-289270247934594), 157308493163390, 0, 0], [(-839253360373175), (-228985321953551), 0], [(-4006072829661611), (-125972350517663)], [(-26529295854937243)]], [[6355774673158, (-2763604791615), 0, 0, 0], [14718338452236, 3161089826148, 0, 0], [58323132414849, 4425023926461, 0], [292789477996223, 5809774162970], [1963462121415055]]], r := 463925224713766, ok := true }, Z3 := { p := [[[134022642384205395216]], [[(-4844372580124136600), 1140918822423878801], [(-8707808907490035665)]], [[193898222103432568, (-67408623458501893), 0], [318210087333607757, 17734470382290730], [615344532324781438]], [[(-8028095232134216), 2558502678251739, 0, 0], [(-12971455669664549), (-884846074004870), 0], [(-22922343639746331), (-400109783296347)], [(-45058420685917463)]], [[337164520841655, (-104882974275308), 0, 0, 0], [541378184842451, 28221309750035, 0, 0], [936800248415130, 22775156820781, 0], [1692175302887326, 17935552833852], [3347448020454548]]], r := 2948828152732601, ok := true }, iE := { p := [[[87590890703474128642]], [[(-948672075667667907), 0], [(-5109970669579179597)]], [[15545969666476992, 0, 0], [56366347058580414, 0], [362096340573537222]], [[(-300438276889923), 0, 0, 0], [(-823572147352331), 0, 0], [(-4003267796314914), 0], [(-26424861621812623)]], [[6631966275389, 0, 0, 0, 0], [14335348048826, 0, 0, 0], [58175700251261, 0, 0], [292664527170463, 0], [1958003343151659]]], r := 448297548179591, ok := true }, iHu := { p := [[[140283782263360827665]], [[(-4866796205539754690), 0], [(-8610485594416488973)]], [[195883078517615741, 0, 0], [318755800482351320, 0], [613148807904252709]], [[(-8118443867500039), 0, 0, 0], [(-12954343832482417), 0, 0], [(-22919223703622605), 0], [(-44959993871585344)]], [[341116347701462, 0, 0, 0, 0], [540567106618882, 0, 0, 0], [936337943239563, 0, 0], [1692071002375369, 0], [3342261820565118]]], r := 2839474435764631, ok := true }, T := { p := [[[16140901064495857664]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[3884905886765252413]], [[42076312979255450, 0], [226641777198625412]], [[(-233791502036702), 0, 0], [2409377221966706, 0], [(-2837936332050063)]], [[3325298708538, 0, 0, 0], [(-18318261014175), 0, 0], [(-32409231025080), 0], [69529729164877]], [[(-72314554366), 0, 0, 0, 0], [255612086450, 0, 0, 0], [(-26193348046), 0, 0], [800111205512, 0], [(-2680414307043)]]], r := 3854430250241, ok := true }, de := { p := [[[(-53029100911701636523)]], [[589298456826050141, 0], [1042604962076857941]], [[(-12572698624773321), 0, 0], [842640006652109, 0], [(-39354778535533056)]], [[364554356538932, 0, 0, 0], [681027049206, 0, 0], [1204894010134, 0], [2018904349571774]], [[(-11887564285667), 0, 0, 0, 0], [550410422, 0, 0, 0], [27654052628, 0, 0], [1722882328, 0], [(-116474488892727)]]], r := 40986336551320, ok := true }, dde := { p := [[[(-742697378202923499754)]], [[31690937579736320322, 0], [56068581871841182066]], [[(-1378351979430891698), 0, 0], [(-2439481036468053871), 0], [(-4314486373484862281)]], [[59927954848110294, 0, 0, 0], [106024994281371098, 0, 0], [187582682190118130, 0], [331881395829293374]], [[(-2605563571150090), 0, 0, 0, 0], [(-4609844923191276), 0, 0, 0], [(-8155934823801110), 0, 0], [(-14429632925255616), 0], [(-25529341245553023)]]], r := 5018323987667121, ok := true }, nJu := { p := [[[(-106058201823403273045)]], [[1178596913652100282, 0], [2085209924153715882]], [[(-25145397249546641), 0, 0], [1685280013304219, 0], [(-78709557071066112)]], [[729108713077865, 0, 0, 0], [1362054098413, 0, 0], [2409788020269, 0], [4037808699143549]], [[(-23775128571333), 0, 0, 0, 0], [1100820845, 0, 0, 0], [55308105257, 0, 0], [3445764656, 0], [(-232948977785454)]]], r := 81972673102630, ok := true }, Jd1 := { p := [[[(-1485394756405846999507)]], [[63381875159472640645, 0], [112137163743682364133]], [[(-2756703958861783396), 0, 0], [(-4878962072936107742), 0], [(-8628972746969724562)]], [[119855909696220589, 0, 0, 0], [212049988562742197, 0, 0], [375165364380236261, 0], [663762791658586748]], [[(-5211127142300180), 0, 0, 0, 0], [(-9219689846382551), 0, 0, 0], [(-16311869647602220), 0, 0], [(-28859265850511231), 0], [(-51058682491106046)]]], r := 10036647975334234, ok := true }, term0 := { p := [[[44238061989503464890854]], [[(-3745730123191891883158), 0], [(-6471044063716183750153)]], [[242224291868473291239, 0, 0], [555396788414671204130, 0], [734193977343064068891]], [[(-13982055297367817503), 0, 0, 0], [(-36062081880815028592), 0, 0], [(-63280175663441381823), 0], [(-74662223161156726936)]], [[757940141295293422, 0, 0, 0, 0], [2085946371757701321, 0, 0, 0], [4114735674815916604, 0, 0], [6449078385834025258, 0], [7142153381739157004]]], r := 2467839116033211492, ok := true }, r0 := { p := [[[812571321170215582778]], [[(-32524138510572263417), 222993954963448733870], [(-48342909685039715677)]], [[1156902237328768418, (-8327202829497932565), 13425152891911070495], [1878038404160809372, (-13586298279093257225)], [3426261694448056746]], [[(-40740309650484427), 278750675267931300, (-339069612507195095), (-325671583430545559)], [(-61379271235804399), 511820670850234912, (-904634351060459350)], [(-132518046978316176), 963117818955973129], [(-250298392913658648)]], [[1484334580546152, (-9533584286515508), 6800045617340529, 31143074662049596, (-6338278147805926)], [1996509721727665, (-16198534995752453), 29296891140015922, 9692522891581903], [4275892570783145, (-36164293843948370), 64327851105273543], [9643857737773634, (-70448373033096805)], [18558692790161048]]], r := 231417774784031881, ok := true }, r1 := { p := [[[1048658797804357671319]], [[(-41159079170873356317), 0], [(-62823770403903740797)]], [[1441041517287160060, 0, 0], [2418040412569584238, 0], [4453063870433815516]], [[(-50403022149532283), 0, 0, 0], [(-78278342217794424), 0, 0], [(-170721853942421410), 0], [(-325433774165560615)]], [[1836192260614097, 0, 0, 0, 0], [2534262305931700, 0, 0, 0], [5458757191124054, 0, 0], [12436670662038101, 0], [24135787100479837]]], r := 80943711082501627, ok := true }, r2 := { p := [[[12194806582850305345214]], [[(-576189342226356666365), 165842715623716970121], [(-1748778014730470745685)]], [[23716231685318345970, (-5840444177469159698), 479273942386194154], [80910025933587195631, (-11293488214042854838)], [193994638383208900020]], [[(-963689176271303021), 211380643463935685, 2779479253823509, (-2245699683088486)], [(-3272511901086776839), 375186632328181165, 136182300660830], [(-8837654930031224785), 864626897841681876], [(-19379512060764509690)]], [[39576453050059425, (-7940843666075509), (-28472245424242), 40247156546964, 10401260792891], [131584283198251122, (-12577820004214772), 198548880324742, (-194220197161722)], [353287618386491973, (-27576282581172905), (-50500985053711)], [872630094768337155, (-65948322063906152)], [1827511611401946413]]], r := 12348883671120136895, ok := true }, r3 := { p := [[[81560024794330536382098]], [[(-6974551553447282386812), 1345116741998761476364], [(-12414776317257863384529)]], [[452407891110084808733, (-100739175496412175049), 1550220957477975965], [1070918868643282942728, (-102980585970134666641)], [1427784527268500479763]], [[(-26155484665387807391), 6272300842294785629, 25694369424992161, (-14337558279199997)], [(-69655494543392641849), 7848813021638791737, (-18443766713192543)], [(-123492612104212120094), 7963871776353986263], [(-146199639396250812348)]], [[1419175261471653412, (-354761395227028266), (-708710580320282), 149884516562403, 127406489914332], [4032572706869935239, (-486449413210869900), 909426059950518, (-1014170987241041)], [8039489064212290622, (-604656495929953477), (-182466383695837)], [12662108240470172258, (-614051485692567429)], [14043864860481532059]]], r := 419746597319738278127, ok := true }, eta := { p := [[[(-13803663974898077754272)]], [[659882993889643057373, 0], [1861865933766599842822]], [[(-27576375466542875756), 0, 0], [(-86879690501686948544), 0], [(-202547886070861528321)]], [[1134521703194893334, 0, 0, 0], [3544332401228503675, 0, 0], [9287612278734072420, 0], [20030593671602557874]], [[(-47041117745349766), 0, 0, 0, 0], [(-143541402385757004), 0, 0, 0], [(-373756061697079814), 0, 0], [(-906839777820583151), 0], [(-1877240361156064986)]]], r := 1726009168582308163, 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 := 1080863910568919040, bh := 72057594037927936, tc := 16140901064495857664, th := 2305843009213693952, sc := 6052837899185946624, sh := 288230376151711744 }
noncomputable def q6 : Cert := { V0 := [[[2725530940075949207]], [[(-91287126767110059), 377201922816942873], [44156729445342036]], [[1070592966778177, (-11826083180570721), (-2510078953912135)], [(-1367568157068053), 5720424926230843], [(-730026414197684)]], [[(-17723052534556), 98573016887570, 244475262858236, (-97671928086209)], [14147220314089, (-138352535746121), (-118255754348044)], [25045010443491, (-103960888866880)], [29112970672233]], [[364914441329, (-932324523637), (-10417119518704), 8071606815967, 2126801897509], [(-285231000374), (-437812337424), 10966506655773, (-3904337566361)], [(-311624124812), 3480962539822, 188550877351], [(-973362227943), 4034094217265], [(-1318427225635)]]], r0 := 144371691387841, V1 := [[[3100127269469748937]], [[(-102860999129709863), 0], [49755156832086924]], [[1158547049280021, 0, 0], [(-1494730824871543), 0], [(-833762884252451)]], [[(-18374962968381), 0, 0, 0], [13278758776682, 0, 0], [28481605597095, 0], [33120043382791]], [[370772206956, 0, 0, 0, 0], [(-246076425835), 0, 0, 0], [(-345014364740), 0, 0], [(-1097083197973), 0], [(-1500642281509)]]], r1 := 57770889517299, V2 := [[[17058384510342545651]], [[(-20096919075228204), 8844289401077700], [(-92248370235801791)]], [[79192237270815, (-73906574587867), (-51020321739303)], [(-1388009136340662), 1212218688058807], [(-755775471699)]], [[(-1388347469641), (-3538659438756), 1612490516591, 280972458078], [6691950193272, (-9909068199840), (-10498327981768)], [(-2124483264485), 43140040327535], [(-745215465913)]], [[35107424346, 19638272101, 10557099090, (-15500270218), (-1500893439)], [(-113079447317), (-499813668935), 332543564534, 76715381883], [73547961244, (-347053320169), (-732215380687)], [34765787248, 90884844637], [15070154057]]], r2 := 50905387335798, V3 := [[[17728640302607217133]], [[(-34006680497758497), 8886794430508698], [(-48491143151982139)]], [[9644551838856, 230068061049419, (-101061131109023)], [(-2283442501576134), 1223941282887034], [(-42760981002161)]], [[17052333872, (-9817479740088), (-363990062753), 1108259267322], [1323901908297, 31722782652696, (-20895028818522)], [(-1132535885531), 44203878577351], [(-90069130440)]], [[(-269909993), (-14805900171), 174961029750, (-21274534489), (-11891544333)], [2585335965, (-1359718338854), (-74355986573), 304835829506], [47576336557, 1137987240764, (-1474224329237)], [(-2067749760), 126004064005], [654061898]]], r3 := 142893978170869, Vm := [[[17073116201245059650]], [[(-20416309324809477), 0], [(-90097754501950845)]], [[77597881402211, 0, 0], [(-1435778718070298), 0], [87904939251550]], [[(-1362489737836), 0, 0, 0], [6433722078319, 0, 0], [(-4178634057414), 0], [(-55765133603)]], [[35206438489, 0, 0, 0, 0], [(-107625510705), 0, 0, 0], [59690635797, 0, 0], [16808421884, 0], [15092751575]]], rm := 12871735536681 }
noncomputable def w6 : Wit := { Z0 := { p := [[[2769300133352477799]], [[(-95743131212664147), 395614304764639685], [46312154746562768]], [[1277042083461139, (-13677590173237736), 0], [(-1583490814828692), 6616022106651824], [(-729584153159608)]], [[(-24153438949524), 182434583351591, 0, 0], [24034795693289, (-226212973546956), 0], [25131162168464, (-104226307594230)], [29561712000587]], [[538405296737, (-3450491278504), 0, 0, 0], [(-595677145588), 3433542241898, 0, 0], [(-320145482309), 3590166024066, 0], [(-1019350974586), 4223101714369], [(-1335958808625)]]], r := 32312595834691, ok := true }, Z1 := { p := [[[3164914438117117485]], [[(-109420721385901882), 0], [52928176853214592]], [[1459476666812730, 0, 0], [(-1809703788375648), 0], [(-833810460753837)]], [[(-27603930228027), 0, 0, 0], [27468337935187, 0, 0], [28721328192530, 0], [33784813714957]], [[615320339128, 0, 0, 0, 0], [(-680773880672), 0, 0, 0], [(-365880551211), 0, 0], [(-1164972542384), 0], [(-1526810067000)]]], r := 15244251866223, ok := true }, Z2 := { p := [[[73741893052617574405]], [[(-898956185998258507), 395614304764639685], [(-4126365974869707508)]], [[15326150125314504, (-13677590173237736), 0], [46092290693902582, 6616022106651824], [248247343648304976]], [[(-316442781880343), 182434583351591, 0, 0], [(-722785284014924), (-226212973546956), 0], [(-2829156344158515), (-104226307594230)], [(-15645812878562733)]], [[7539418073779, (-3450491278504), 0, 0, 0], [13515699988380, 3433542241898, 0, 0], [43349139467879, 3590166024066, 0], [178909608488037, 4223101714369], [1002746010849720]]], r := 233925906749176, ok := true }, Z3 := { p := [[[128076977249213974690]], [[(-5068356835509873664), 1324488148750910097], [(-7227121649589882394)]], [[221996691988637573, (-80985931955928759), 0], [288679767831927956, 18041775137759035], [442084796647890946]], [[(-10063144811859787), 3378328005161803, 0, 0], [(-12885061220417830), (-919229680343055), 0], [(-18014296697020343), (-349757460044061)], [(-28043316770896843)]], [[462771327467834, (-151768519711680), 0, 0, 0], [588847070091902, 32427893657861, 0, 0], [806044469421588, 20610039556422, 0], [1152213228143970, 13594589064814], [1805103238278856]]], r := 2115824498080262, ok := true }, iE := { p := [[[80393733572264888191]], [[(-909834256748283877), 0], [(-4015124486890422187)]], [[15914033888117086, 0, 0], [45952794481144418, 0], [246494887360150837]], [[(-331088813231370), 0, 0, 0], [(-705123330217116), 0, 0], [(-2826513330342556), 0], [(-15574805842760656)]], [[7930350756295, 0, 0, 0, 0], [13054579291297, 0, 0, 0], [43226063215991, 0, 0], [178799942308613, 0], [999537046668208]]], r := 223031193618386, ok := true }, iHu := { p := [[[134576209793084719586]], [[(-5098993627546474882), 0], [(-7138591078565064801)]], [[224677829043545432, 0, 0], [289165012818829033, 0], [440368544925349159]], [[(-10195557011118480), 0, 0, 0], [(-12864295574224609), 0, 0], [(-18010013803914416), 0], [(-27976608438509031)]], [[469090574638286, 0, 0, 0, 0], [587795815751041, 0, 0, 0], [805561360603047, 0, 0], [1152079798872093, 0], [1802058351530643]]], r := 2022220919587908, ok := true }, T := { p := [[[16140901064495857664]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[4232697646951090302]], [[47902406649546799, 0], [211394684793440779]], [[(-295744981415954), 0, 0], [2365407828671782, 0], [(-2420118406707265)]], [[4602341328840, 0, 0, 0], [(-20102830607667), 0, 0], [(-28143962850734), 0], [50982311277415]], [[(-109622506218), 0, 0, 0, 0], [306582230947, 0, 0, 0], [(-26271668601), 0, 0], [600901172655, 0], [(-1704856673096)]]], r := 2203756713599, ok := true }, de := { p := [[[(-52322202036411649573)]], [[646064770069199730, 0], [904490678096879622]], [[(-15080952066342133), 0, 0], [844318885522012, 0], [(-29558666050030580)]], [[478948037834207, 0, 0, 0], [788150058052, 0, 0], [1103410081273, 0], [1314233415817064]], [[(-17105155687312), 0, 0, 0, 0], [735717896, 0, 0, 0], [27816676184, 0, 0], [1442007077, 0], [(-65711166088377)]]], r := 22195780389791, ok := true }, dde := { p := [[[(-705675012854251224870)]], [[32944842487326599872, 0], [46122779482257239865]], [[(-1569416930375129287), 0, 0], [(-2198044572561922178), 0], [(-3076057183535253480)]], [[74733565541577263, 0, 0, 0], [104625384557940382, 0, 0], [146475538381116546, 0], [205068903846087915]], [[(-3558741752079919), 0, 0, 0, 0], [(-4982240703332370), 0, 0, 0], [(-6975192658399978), 0, 0], [(-9765191778531475), 0], [(-13671262314790340)]]], r := 3168942172340236, ok := true }, nJu := { p := [[[(-104644404072823299146)]], [[1292129540138399460, 0], [1808981356193759245]], [[(-30161904132684265), 0, 0], [1688637771044024, 0], [(-59117332100061160)]], [[957896075668414, 0, 0, 0], [1576300116105, 0, 0], [2206820162546, 0], [2628466831634128]], [[(-34210311374623), 0, 0, 0, 0], [1471435793, 0, 0, 0], [55633352369, 0, 0], [2884014154, 0], [(-131422332176753)]]], r := 44391560779575, ok := true }, Jd1 := { p := [[[(-1411350025708502449740)]], [[65889684974653199744, 0], [92245558964514479730]], [[(-3138833860750258574), 0, 0], [(-4396089145123844355), 0], [(-6152114367070506959)]], [[149467131083154526, 0, 0, 0], [209250769115880764, 0, 0], [292951076762233092, 0], [410137807692175830]], [[(-7117483504159838), 0, 0, 0, 0], [(-9964481406664739), 0, 0, 0], [(-13950385316799956), 0, 0], [(-19530383557062950), 0], [(-27342524629580680)]]], r := 6337884344680468, ok := true }, term0 := { p := [[[40251548207103434762124]], [[(-3728086014548838885757), 0], [(-5078755759089114285420)]], [[263944151427766467373, 0, 0], [477112198555289097166, 0], [498581235870207406002]], [[(-16683618414419517243), 0, 0, 0], [(-33922054177927565931), 0, 0], [(-47044474208318048374), 0], [(-43904933236860056735)]], [[990403475666192017, 0, 0, 0, 0], [2148799921611302162, 0, 0, 0], [3349858355618155862, 0, 0], [4152126677422344137, 0], [3638074794377048792]]], r := 1572724770029157329, ok := true }, r0 := { p := [[[790826166775165538085]], [[(-33922276456259061269), 215118294989558086774], [(-40233236741225735347)]], [[1309909431329067487, (-8545647482040813302), 12438967682616361544], [1654340800014026560, (-11279003182984054477)], [2468351232787221885]], [[(-50597235876850605), 310694908415563934, (-311554003429292747), (-372614187990335718)], [(-58082318131454820), 448869054125928810, (-741929361013083763)], [(-100964146170053960), 691777608245806141], [(-156073196569925592)]], [[2033158321364239, (-11716578271458052), 6455865710884683, 35103965998826755, (-5888886017320645)], [2059724061096709, (-15282190720400386), 24969047833688522, 9544279966653145], [3498926453286974, (-27399001508650729), 45619313386145116], [6351866486127507, (-43807953784749059)], [10020402324835547]]], r := 167361549776702998, ok := true }, r1 := { p := [[[1018005430772573741119]], [[(-42744384015910269787), 0], [(-52244235423493476132)]], [[1625473173433020832, 0, 0], [2127065924940251045, 0], [3205204296629582851]], [[(-62455608091909734), 0, 0, 0], [(-73996736138001018), 0, 0], [(-129858643824718656), 0], [(-202756715763007763)]], [[2512485914917322, 0, 0, 0, 0], [2615132041083981, 0, 0, 0], [4460140568779248, 0, 0], [8178854825421756, 0], [13021486124613180]]], r := 47475874024989803, ok := true }, r2 := { p := [[[10310528756231584197592]], [[(-527317998387604981210), 157448362488650805408], [(-1275163082250004594228)]], [[23692212157460107180, (-6039377359379078166), 472847706027089609], [63858680010073404701, (-9103401554349067433)], [122201318467218709821]], [[(-1054931015953271134), 240046072288730900, 3324512839542699, (-2727509691138300)], [(-2821112007501196849), 328524821813553442, (-474650445925308)], [(-6023835866609662886), 603852609422810200], [(-10556199095427216025)]], [[47540280376862401, (-9929043967166573), (-39536415857410), 42229749180210, 15542511800882], [124422770650430304, (-12053331796498010), 212343823141999, (-204432103953203)], [263082718122365860, (-20862795096545393), (-50012581376776)], [514179889498206730, (-39850355796248689)], [861276297968539654]]], r := 5983413854208804927, ok := true }, r3 := { p := [[[73480204717117519925518]], [[(-6875450207533687489242), 1365497075841921951844], [(-9693309708133049672654)]], [[488305915199158611337, (-113143997860345759361), 1454493825853158387], [915398086815597050590, (-90657027383656208660)], [966186074752004205199]], [[(-30914824442753482985), 7746790037629573015, 30846370707050821, (-16577494421472206)], [(-65200928880289334580), 7641631528268146374, (-20887443707644288)], [(-91500158016669810469), 6075415560859420285], [(-85743800149791675970)]], [[1836997132431138757, (-480931892815193484), (-1008305432295223), 106554181347646, 179681180231092], [4133872698983954607, (-520760233476251916), 852736561258606, (-960473062205291)], [6523425115941228080, (-510189288596970576), (-157970691823425)], [8131616564286516924, (-405983802549790434)], [7138370458744261248]]], r := 297053978990418172326, ok := true }, eta := { p := [[[(-11884403765909936727809)]], [[616220932000637326337, 0], [1370438088081118118625]], [[(-28163690162383519083), 0, 0], [(-69313234466573613257), 0], [(-128442223389370256854)]], [[1271197315229786361, 0, 0, 0], [3091783828037257050, 0, 0], [6379821449479095238, 0], [10967680864244940364]], [[(-57879710868943694), 0, 0, 0, 0], [(-137435744705363082), 0, 0, 0], [(-280733656236219407), 0, 0], [(-537619596741118460), 0], [(-888504213678131662)]]], r := 822349147728416037, 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 := 1080863910568919040, bh := 72057594037927936, tc := 16140901064495857664, th := 2305843009213693952, sc := 6629298651489370112, sh := 288230376151711744 }
noncomputable def q7 : Cert := { V0 := [[[2547102838662170405]], [[(-87206431841145720), 353936772432681405], [41476006547547781]], [[972345791848779, (-11442617925640305), (-2060644390098438)], [(-1314192118121166), 5442191429979158], [(-681140748605812)]], [[(-15128411732264), 93245096261309, 205989557860548, (-82425148910725)], [12589818628725, (-139775044186221), (-97970116081732)], [23860812348854, (-97142153146220)], [27211327304762]], [[287933702472, (-846716428911), (-8870756919981), 7178944072657, 1547134953983], [(-236131444034), (-278819069561), 9357513203081, (-3414357462813)], [(-281365611720), 3339492274279, 121866233542], [(-929046930700), 3785526275472], [(-1231979625110)]]], r0 := 131761341865263, V1 := [[[2898898113745934069]], [[(-98436134058839842), 0], [46816933734621808]], [[1056518553288491, 0, 0], [(-1444386987501629), 0], [(-778135066289899)]], [[(-15738471206037), 0, 0, 0], [11935493753552, 0, 0], [27167596732471, 0], [30974766199522]], [[292638293157, 0, 0, 0, 0], [(-203668764431), 0, 0, 0], [(-312914091119), 0, 0], [(-1048993346197), 0], [(-1403008884591)]]], r1 := 53183801078293, V2 := [[[17018496864952522469]], [[(-19795763739073668), 8682472358146235], [(-94998482371816259)]], [[71629227310922, (-87838113068954), (-47757750601871)], [(-1362513531054597), 1190424706639504], [(-4718402727035)]], [[(-1144125734027), (-3430049102149), 1647798091016, 250618838088], [6075596212921, (-11873665608832), (-9825364590824)], [(-1841898672186), 42371702970174], [(-677726807559)]], [[26480511256, 16694362247, 7132486034, (-14836759322), (-1274962868)], [(-93301196296), (-482930581627), 339935648059, 68386154112], [67911275305, (-420760425591), (-684755511648)], [32748459466, 87521795584], [13519075802]]], r2 := 50307772546044, V3 := [[[17660665652089916535]], [[(-33967905876989946), 9307546531098546], [(-53052712552832238)]], [[9740804130164, 190629076113884, (-101107980770344)], [(-2278117233105853), 1281931737080168], [(-44834932785227)]], [[15095926494, (-9899964996854), 307691868688, 1058064914067], [1338407260060, 26259905291515, (-20902140764117)], [(-941026033445), 46278857447602], [(-93642242708)]], [[(-221685674), (-12756107049), 160789940746, (-28645689815), (-10824931785)], [2259956360, (-1371374204369), 65269434241, 290905301694], [48161421396, 936737675154, (-1473813811312)], [(-1505079030), 129524315155], [735426893]]], r3 := 128920338640371, Vm := [[[17032583606080427354]], [[(-20121218683021534), 0], [(-92944395244299769)]], [[70191681049088, 0, 0], [(-1411250912727120), 0], [79781644158647]], [[(-1117817185995), 0, 0, 0], [5849827669338, 0, 0], [(-3946903473635), 0], [(-25279738779)]], [[26501423767, 0, 0, 0, 0], [(-87943347556), 0, 0, 0], [56322527704, 0, 0], [13740450307, 0], [13603604441]]], rm := 12911757074502 }
noncomputable def w7 : Wit := { Z0 := { p := [[[2582737011276294414]], [[(-90908601551873202), 368962430182327773], [43236785103904420]], [[1144033014466531, (-12986943078839029), 0], [(-1494029676225816), 6176683586272060], [(-680558537303745)]], [[(-20338126721139), 163433287780933, 0, 0], [20805522492960, (-213432810889403), 0], [23915494327623, (-97222648186250)], [27576165910080]], [[421737990986, (-2905446674449), 0, 0, 0], [(-485753628256), 2972217498994, 0, 0], [(-288564718398), 3416499189660, 0], [(-967201342721), 3939452272868], [(-1246177590645)]]], r := 29884413556334, ok := true }, Z1 := { p := [[[2951699441458622188]], [[(-103895544630712231), 0], [49413468690176480]], [[1307466302247464, 0, 0], [(-1707462487115218), 0], [(-777781185489995)]], [[(-23243573395587), 0, 0, 0], [23777739991954, 0, 0], [27331993517284, 0], [31515618182948]], [[481986275413, 0, 0, 0, 0], [(-555147003721), 0, 0, 0], [(-329788249598), 0, 0], [(-1105372963110), 0], [(-1424202960737)]]], r := 13937314129616, ok := true }, Z2 := { p := [[[72002868265353548615]], [[(-841222729564007973), 368962430182327773], [(-4036968903984158107)]], [[13593595088491429, (-12986943078839029), 0], [43354454007270936, 6176683586272060], [242756323077884382]], [[(-263348881978694), 163433287780933, 0, 0], [(-648224352691996), (-213432810889403), 0], [(-2664792055751820), (-97222648186250)], [(-15298463269995328)]], [[5830336623041, (-2905446674449), 0, 0, 0], [11421703354875, 2972217498994, 0, 0], [38954504149483, 3416499189660, 0], [168620912350343, 3939452272868], [980435035613607]]], r := 220026790268427, ok := true }, Z3 := { p := [[[118754521538075489555]], [[(-4287862348278696521), 1174917243061025821], [(-6696990078020677249)]], [[171220093700098814, (-69094558593670035), 0], [243425650453747569, 16322820816381804], [409010017109336063]], [[(-7081892769551037), 2611981213259211, 0, 0], [(-9916538153528312), (-804414510940391), 0], [(-15184217848805600), (-311494313040656)], [(-25928240215910434)]], [[297226010613897, (-106970728131516), 0, 0, 0], [413613283540279, 25376052636468, 0, 0], [619954526073416, 17769294104867, 0], [970805511207500, 12121052561311], [1668238778968134]]], r := 1607075204549207, ok := true }, iE := { p := [[[78635192924972464935]], [[(-849913348544719033), 0], [(-3925939250250438394)]], [[14102158809514928, 0, 0], [43280465158786418, 0], [241008686694633999]], [[(-275268820114753), 0, 0, 0], [(-633041285081057), 0, 0], [(-2662602665941437), 0], [(-15227649213285470)]], [[6126554202682, 0, 0, 0, 0], [11052085608195, 0, 0, 0], [38850190531042, 0, 0], [168536954750184, 0], [977234921034148]]], r := 209892488788509, ok := true }, iHu := { p := [[[125202238115849411745]], [[(-4309182797165883222), 0], [(-6607413622321021002)]], [[173237494040109686, 0, 0], [243982795245277838, 0], [407300597098747101]], [[(-7173774354838005), 0, 0, 0], [(-9901029493573362), 0, 0], [(-15181578556812390), 0], [(-25861722244537380)]], [[301246079122511, 0, 0, 0, 0], [412887747650661, 0, 0, 0], [619607503144175, 0, 0], [970744971143109, 0], [1665205017831675]]], r := 1531926270074481, ok := true }, T := { p := [[[16140901064495857664]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[4327354639361147310]], [[46771379773800505, 0], [216047431137236035]], [[(-270533097948294), 0, 0], [2288457151211928, 0], [(-2476511615641543)]], [[3836433511433, 0, 0, 0], [(-18423485573850), 0, 0], [(-28249344546571), 0], [52183971569922]], [[(-83440164894), 0, 0, 0, 0], [255520357601, 0, 0, 0], [(-26419363314), 0, 0], [600756751870, 0], [(-1744965009934)]]], r := 2208313246875, ok := true }, de := { p := [[[(-51086819080929830454)]], [[590988570237983447, 0], [906182474364907953]], [[(-12571225330261444), 0, 0], [847480336397134, 0], [(-29556347554259130)]], [[364555643101657, 0, 0, 0], [792580899431, 0, 0], [1215290712460, 0], [1314236595442329]], [[(-11887563160191), 0, 0, 0, 0], [741237826, 0, 0, 0], [28124210315, 0, 0], [1742732489, 0], [(-65711161724663)]]], r := 20936133475366, ok := true }, dde := { p := [[[(-645517115651941386273)]], [[27462260774800467691, 0], [42108799854694050406]], [[(-1194575931315509861), 0, 0], [(-1832548804380865886), 0], [(-2808580745181798826)]], [[51937555951085642, 0, 0, 0], [79635966532925720, 0, 0], [122108482017152808, 0], [187236812816846985]], [[(-2258155100383155), 0, 0, 0, 0], [(-3462506758799948), 0, 0, 0], [(-5309233327475736), 0, 0], [(-8140738112911912), 0], [(-12482456917458508)]]], r := 2539618109199961, ok := true }, nJu := { p := [[[(-102173638161859660908)]], [[1181977140475966895, 0], [1812364948729815907]], [[(-25142450660522888), 0, 0], [1694960672794269, 0], [(-59112695108518259)]], [[729111286203315, 0, 0, 0], [1585161798862, 0, 0], [2430581424920, 0], [2628473190884659]], [[(-23775126320382), 0, 0, 0, 0], [1482475653, 0, 0, 0], [56248420630, 0, 0], [3485464979, 0], [(-131422323449325)]]], r := 41872266950722, ok := true }, Jd1 := { p := [[[(-1291034231303882772545)]], [[54924521549600935382, 0], [84217599709388100812]], [[(-2389151862631019721), 0, 0], [(-3665097608761731771), 0], [(-5617161490363597652)]], [[103875111902171284, 0, 0, 0], [159271933065851441, 0, 0], [244216964034305617, 0], [374473625633693970]], [[(-4516310200766310), 0, 0, 0, 0], [(-6925013517599895), 0, 0, 0], [(-10618466654951471), 0, 0], [(-16281476225823823), 0], [(-24964913834917015)]]], r := 5079236218399912, ok := true }, term0 := { p := [[[33731903425659703451500]], [[(-2844805528816491034256), 0], [(-4244862831546137585248)]], [[183744831177037079856, 0, 0], [363636732407921973473, 0], [416374151781598915181]], [[(-10599930414506285076), 0, 0, 0], [(-23595568366950047799), 0, 0], [(-35840091372116260972), 0], [(-36650121383839427852)]], [[574389565124516549, 0, 0, 0, 0], [1364397402815941436, 0, 0, 0], [2329435037655347742, 0, 0], [3162544916407673655, 0], [3036131499827799724]]], r := 1125885573379191863, ok := true }, r0 := { p := [[[727846497101847769737]], [[(-29230912893724636887), 199183007707633805634], [(-37141553497900212155)]], [[1049098518675221234, (-7429816179230696653), 11840252975757547994], [1444476607953052070, (-10438406934754537238)], [2279507428565904540]], [[(-37227232439696293), 250305830066017041, (-287815231156789630), (-308485387109673757)], [(-47361617416736005), 393581744546647507, (-694605326791868540)], [(-88303986559347886), 640424897027606444], [(-144183937272122489)]], [[1364294548651927, (-8621071350727847), 5471178930658133, 29224179656103877, (-5648312828792234)], [1546329364054171, (-12495209357731133), 22430919745139434, 7623736049162934], [2861294512606163, (-24063712195203423), 42679405002571226], [5563513861946549, (-40562768831036935)], [9259326023930375]]], r := 135911003099511519, ok := true }, r1 := { p := [[[938556002199042412274]], [[(-36919205755348125368), 0], [(-48266627888998377769)]], [[1303572990456702565, 0, 0], [1859597511052386969, 0], [2962170686641064190]], [[(-45944066090050103), 0, 0, 0], [(-60388059194071211), 0, 0], [(-113713678031591122), 0], [(-187439123026165448)]], [[1683733581062457, 0, 0, 0, 0], [1962550645679883, 0, 0, 0], [3650621821142851, 0, 0], [7171953444221544, 0], [12040237404935967]]], r := 39258782454592142, ok := true }, r2 := { p := [[[9342919206248288557706]], [[(-443843345457112381527), 146256634716883948563], [(-1157816650258408604069)]], [[18351190880972569785, (-5186045847194368827), 479351353419782318], [53906994663839472080, (-8491057192007299301)], [111121310726316892433]], [[(-747679006140841731), 189386278055071438, 3185018467589962, (-2640677112111096)], [(-2190684985675129892), 285438894612064671, (-55550533516896)], [(-5095039033668771640), 564915967984631374], [(-9609776490341229547)]], [[30746673880614505, (-7152396073853258), (-30690319555059), 44573896899458, 14387372492040], [88330679794279042, (-9618928142492080), 207070071793169, (-200780416874150)], [204637776454630328, (-18173848567017360), (-45653294590378)], [435518430070802609, (-37332816932067752)], [784746448007054575]]], r := 5155769225889626541, ok := true }, r3 := { p := [[[61461582012241901398796]], [[(-5241817385709884434553), 1166754535243523413569], [(-8093775626606073614659)]], [[339727725535391228928, (-87137258336985235778), 1512605298320817608], [697323997552991335278, (-77225707806373178431)], [806322477625697196245]], [[(-19632709326366762099), 5429384241000686968, 27468482791135193, (-16326829924580511)], [(-45337134687806427644), 5893015548173021292, (-19171226931486029)], [(-69683454260831080550), 5178777129073137719], [(-71537638954970353395)]], [[1064983684297967593, (-307141968475765643), (-702125572482307), 142915118832043, 169131799698358], [2624162194406770537, (-365143129541493792), 865844795739078, (-974395617273693)], [4535211887550362518, (-393352057005511886), (-181450626646985)], [6191933727413999122, (-346116203066616283)], [5954718672730139313]]], r := 199742821598969339464, ok := true }, eta := { p := [[[(-10755295170652089997741)]], [[517160052024367442504, 0], [1243170194196824756006]], [[(-21738776960506595630), 0, 0], [(-58417284229058827571), 0], [(-116714655032514860418)]], [[897721681777477968, 0, 0, 0], [2396103828742186587, 0, 0], [5389441085862649959, 0], [9978615492415646836]], [[(-37305604970103779), 0, 0, 0, 0], [(-97369077924494113), 0, 0, 0], [(-218036473828034651), 0, 0], [(-454907340165633387), 0], [(-809154981889517434)]]], r := 719936587495394941, 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 864691128455135232 1152921504606846976 13835058055282163712 18446744073709551616 4611686018427387904 6917529027641081856 :=
  (RegionPosI.split_s 5764607523034234880 (RegionPosI.split_b 1008806316530991104 (RegionPosI.split_s 5188146770730811392 (RegionPosI.of_check c0 q0 ok_0 864691128455135232 1008806316530991104 13835058055282163712 18446744073709551616 4611686018427387904 5188146770730811392 (by decide +kernel)) (RegionPosI.of_check c1 q1 ok_1 864691128455135232 1008806316530991104 13835058055282163712 18446744073709551616 5188146770730811392 5764607523034234880 (by decide +kernel))) (RegionPosI.split_s 5188146770730811392 (RegionPosI.of_check c2 q2 ok_2 1008806316530991104 1152921504606846976 13835058055282163712 18446744073709551616 4611686018427387904 5188146770730811392 (by decide +kernel)) (RegionPosI.of_check c3 q3 ok_3 1008806316530991104 1152921504606846976 13835058055282163712 18446744073709551616 5188146770730811392 5764607523034234880 (by decide +kernel)))) (RegionPosI.split_b 1008806316530991104 (RegionPosI.split_s 6341068275337658368 (RegionPosI.of_check c4 q4 ok_4 864691128455135232 1008806316530991104 13835058055282163712 18446744073709551616 5764607523034234880 6341068275337658368 (by decide +kernel)) (RegionPosI.of_check c5 q5 ok_5 864691128455135232 1008806316530991104 13835058055282163712 18446744073709551616 6341068275337658368 6917529027641081856 (by decide +kernel))) (RegionPosI.split_s 6341068275337658368 (RegionPosI.of_check c6 q6 ok_6 1008806316530991104 1152921504606846976 13835058055282163712 18446744073709551616 5764607523034234880 6341068275337658368 (by decide +kernel)) (RegionPosI.of_check c7 q7 ok_7 1008806316530991104 1152921504606846976 13835058055282163712 18446744073709551616 6341068275337658368 6917529027641081856 (by decide +kernel)))))

end CKLaneC.RSC2.S10_0031