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

import Definitions.Def_CK_CKLaneC_RSC2_S02_0245_part00

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

namespace CKLaneC.RSC2.S02_0245
open CKLaneC.TM3 CKLaneC.RSCell

noncomputable def w5 : Wit := { Z0 := { p := [[[168386486253571228]], [[(-19995295294939847), 24055212321938746], [507746933408204]], [[153950694846519, (-2856470756419979), 0], [(-59902961171540), 72535276201172], [(-6161639572718)]], [[(-1335228074788), 21992956406645, 0, 0], [418770497018, (-8557565881649), 0], [728117553767, (-880234224674)], [113631873292]], [[12356932221, (-190746867827), 0, 0, 0], [(-3801749323), 59824356716, 0, 0], [(-5218363129), 104016793395, 0], [(-13434659866), 16233124756], [(-2439248382)]]], r := 286269890545, ok := true }, Z1 := { p := [[[192441698575509975]], [[(-22851766051359826), 0], [580282209609376]], [[175943651253164, 0, 0], [(-68460527053188), 0], [(-7041873797392)]], [[(-1525974942615), 0, 0, 0], [478594853735, 0, 0], [832134347162, 0], [129864998049]], [[14122208252, 0, 0, 0, 0], [(-4344856369), 0, 0, 0], [(-5963843576), 0, 0], [(-15353896990), 0], [(-2787712436)]]], r := 68853739544, ok := true }, Z2 := { p := [[[10868259533534873815885]], [[(-83001413856660149142), 24055212321938746], [(-296647249833318626802)]], [[716364867849976513, (-2856470756419979), 0], [2290125509255210023, 72535276201172], [8591381882908522647]], [[(-6601352866288638), 21992956406645, 0, 0], [(-19683929199333753), (-8557565881649), 0], [(-66590097218348204), (-880234224674)], [(-253007854272943514)]], [[64224828266221, (-190746867827), 0, 0, 0], [179614637911552, 59824356716, 0, 0], [571558913423626, 104016793395, 0], [1965660730793138, 16233124756], [7509414429564650]]], r := 1078924448661100, ok := true }, Z3 := { p := [[[11663070717604958012438]], [[(-191164789138988794498), 51628008117153411], [(-318619107125651434169)]], [[3322942350825866666, (-6582481900150818), 0], [5283784415512062397, 154424171458471], [9230699270475389228]], [[(-58725799873700483), 108710559171709, 0, 0], [(-92241722940951757), (-19411525133296), 0], [(-153735962122949175), (-1877736550110)], [(-271887506109999557)]], [[1045950690035333, (-1893961590968), 0, 0, 0], [1634351532220773, 287787715004, 0, 0], [2688272937470781, 236868132672, 0], [4539856408804743, 34650779314], [8070866472169018]]], r := 3718266535810756, ok := true }, iE := { p := [[[10870828095650583053196]], [[(-83002316056099792525), 0], [(-296639504677715368320)]], [[716391283002443537, 0, 0], [2290128740557921416, 0], [8591287893454088022]], [[(-6601679743251748), 0, 0, 0], [(-19683838138406553), 0, 0], [(-66590118435632027), 0], [(-253006120935955665)]], [[64228642180497, 0, 0, 0, 0], [179613294084104, 0, 0, 0], [571557857152566, 0, 0], [1965661017680390, 0], [7509377221347277]]], r := 1078833729266963, ok := true }, iHu := { p := [[[11665646381565469332658]], [[(-191166841845192830357), 0], [(-318611403075319783755)]], [[3323018013221756235, 0, 0], [5283792109372841284, 0], [9230605592285278193]], [[(-58727327923061917), 0, 0, 0], [(-92241608511075895), 0, 0], [(-153736014184548271), 0], [(-271885777421120434)]], [[1045979483031291, 0, 0, 0, 0], [1634348565205562, 0, 0, 0], [2688271285809823, 0, 0], [4539857127297729, 0], [8070829349865993]]], r := 3718060011213778, ok := true }, T := { p := [[[16140901064495857664]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[31302340900513862]], [[239003576347579, 0], [854167761487881]], [[(-237964739521), 0, 0], [6449316818186, 0], [(-1430205739537)]], [[1442054504, 0, 0, 0], [(-7211832906), 0, 0], [(-12019721510), 0], [14444822019]], [[(-13109586), 0, 0, 0, 0], [43698621, 0, 0, 0], [(-23644), 0, 0], [121385057, 0], [(-218860941)]]], r := 124782184, ok := true }, de := { p := [[[(-121509534095630202663)]], [[241962777900335176, 0], [403271296500558626]], [[(-2199423626789862), 0, 0], [793301619707, 0], [(-6109510074416285)]], [[26659680636837, 0, 0, 0], [1560557, 0, 0], [2600927, 0], [123424447392763]], [[(-363541099592), 0, 0, 0, 0], [4, 0, 0, 0], [23653, 0, 0], [9, 0], [(-2805101077104)]]], r := 377566608643, ok := true }, dde := { p := [[[(-123013993599816657678211)]], [[2236376076494358178021, 0], [3727293460823930285487]], [[(-40661383685020790987), 0, 0], [(-67768973601755445560), 0], [(-112948288013946658435)]], [[739297885181270303, 0, 0, 0], [1232163141965646661, 0, 0], [2053605236609411413, 0], [3422675394357687044]], [[(-13441779730563236), 0, 0, 0, 0], [(-22402966217609169), 0, 0, 0], [(-37338277029398414), 0, 0], [(-62230461715591304), 0], [(-103717436192655161)]]], r := 7732132450912732, ok := true }, nJu := { p := [[[(-243019068191260405326)]], [[483925555800670353, 0], [806542593001117252]], [[(-4398847253579724), 0, 0], [1586603239414, 0], [(-12219020148832569)]], [[53319361273674, 0, 0, 0], [3121114, 0, 0], [5201855, 0], [246848894785527]], [[(-727082199184), 0, 0, 0, 0], [8, 0, 0, 0], [47306, 0, 0], [18, 0], [(-5610202154208)]]], r := 755133217282, ok := true }, Jd1 := { p := [[[(-246027987199633315356421)]], [[4472752152988716356043, 0], [7454586921647860570974]], [[(-81322767370041581973), 0, 0], [(-135537947203510891119), 0], [(-225896576027893316870)]], [[1478595770362540607, 0, 0, 0], [2464326283931293322, 0, 0], [4107210473218822826, 0], [6845350788715374088]], [[(-26883559461126472), 0, 0, 0, 0], [(-44805932435218337), 0, 0, 0], [(-74676554058796828), 0, 0], [(-124460923431182607), 0], [(-207434872385310322)]]], r := 15464264901825457, ok := true }, term0 := { p := [[[1137486891571156904377556000]], [[(-41356448145333768210579209), 0], [(-68923076361347321388373551)]], [[1127842139165846257323607, 0, 0], [2506090378963565255962366, 0], [3132631969545952904923340]], [[(-27340888318256727625786), 0, 0, 0], [(-68346071181414606219876), 0, 0], [(-113907728985961149005599), 0], [(-126566238409945728830629)]], [[621373744080032037848, 0, 0, 0, 0], [1656852049916478685582, 0, 0, 0], [3106518419474206100345, 0, 0], [4602221978067370595300, 0], [4794067736924173695923]]], r := 624952957560001872608, ok := true }, r0 := { p := [[[54876868698562672336381]], [[(-1275410239318040382427), 15676065323628471541761], [(-1499576978094403559870)]], [[22046929786356981128, (-363610648415084717888), 1118850560938170666605], [35185035021826741225, (-428385819706459815573)], [43452861849385562496]], [[(-337641690665951968), 6232813620620706969, (-25745916948491789450), (-124002673863997161)], [(-606241241141510501), 10035959323827678959, (-30580491258859147033)], [(-1023015274667522681), 12413391829897510937], [(-1280037773315072703)]], [[4908668091429606, (-94340793729907871), 426274024670649920, 32298136562504834, (-4419179505702301)], [9207936009350487, (-171790800218677343), 712024848039054513, 2641454596970043], [17606223333779001, (-291842881779773984), 886181898031544108], [30197080554437963, (-365677434244435693)], [38000404623985767]]], r := 169943443221402195, ok := true }, r1 := { p := [[[71671656162107583618043]], [[(-1664733358178041090100), 0], [(-1958540553425054141080)]], [[28703223523530053911, 0, 0], [45932305139312887600, 0], [56752363257342726144]], [[(-438025927979322565), 0, 0, 0], [(-789837173389588332), 0, 0], [(-1335557452871819943), 0], [(-1671819400394764802)]], [[6343620484530844, 0, 0, 0, 0], [11962320205553989, 0, 0, 0], [22943241657478761, 0, 0], [39423660230548495, 0], [49631281247311912]]], r := 21529492284976707, ok := true }, r2 := { p := [[[556076000658815761454749249]], [[(-11425546553809914688515663), 29554756088963061809925], [(-33467473327423740017716047)]], [[189156982616195356677332, (-431149755445959710741), 455625640483227853], [682180204890013752025492, (-896452343321582829429)], [1514951050609167062893749]], [[(-2985731526331133182458), 5981566158481636173, 97544032679158, (-1347836261708)], [(-11196333535604613330289), 12898277573074528847, 110946089383236], [(-30729031411962312541928), 27173734496097702577], [(-61032568715447982830505)]], [[47214970000884231558, (-83372777288991219), (-8727201126779), (-2046910676076), (-101264488479)], [175251309227356488907, (-176003168221098552), (-1488659503283), (-334954448838)], [501636836200977312353, (-388842558193085331), (-15841921635766)], [1233668794906942624654, (-823594390578486080)], [2306727851503576497067]]], r := 5086013854069749164816, ok := true }, r3 := { p := [[[2274309948326643338323970434]], [[(-82694328244561559067326146), 131522253164497905758512], [(-137826028695868448139607464)]], [[2255228531523900725107381, (-3685980927607533039199), 1818601596513798593], [5011617893151472442535127, (-3995011918874919047938)], [6264654014280313084454204]], [[(-54671342317818309192361), 90533574570961751479, 906762119513671, (-110334807534153)], [(-136678327743743327036788), 111893001635855202066, 429705078718042], [(-227798399377004287290940), 121166690472248029311], [(-253113992491649354516833)]], [[1242518650527257640106, (-2073637609651914110), (-97239338210575), 7326285395220, (-11407057419244)], [3313387812375557441604, (-2747703800952982720), (-45945546216367), 9495268316165], [6212618109162589923747, (-3392927592690027263), (-48328720458173)], [9203926914929894226290, (-3673576654982226742)], [9587575219641736852889]]], r := 56810861005227979545253, ok := true }, eta := { p := [[[(-556253842476975565857468152)]], [[11429877229903696857612988, 0], [33472805086101855543985599]], [[(-189244287086242359806614), 0, 0], [(-682310043437783942010782), 0], [(-1515111959049334371955452)]], [[2987385180892119721632, 0, 0, 0], [11198947763541906203121, 0, 0], [30732949119693665517878, 0], [61037432703308023504590]], [[(-47245548552222170763), 0, 0, 0, 0], [(-175300783738110554827), 0, 0, 0], [(-501715690023631583009), 0, 0], [(-1233787216637166055407), 0], [(-2306875005974838366191)]]], r := 546792623743426079465, 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 := 2462906046218240, bh := 70368744177664, tc := 16140901064495857664, th := 2305843009213693952, sc := 15276209936040722432, sh := 288230376151711744 }
noncomputable def q6 : Cert := { V0 := [[[210213111444956614]], [[(-20742053694133634), 30024818558923138], [600133062953787]], [[162511365238143, (-2961485225010771), (-1205290778563)], [(-58733880408696), 85685112245212], [(-6859654679362)]], [[(-1418826804636), 23038557680646, 356719189816, (-57331400100)], [416384037353, (-8376331140143), (-10321011756)], [672753046801, (-979537475760)], [119237329499]], [[13163087010, (-194598791063), (-37976965879), 16955354308, 6788967], [(-3697720782), 57976103065, 3045957041, (-490571903)], [(-4899231117), 95985379712, 88519547], [(-11701678687), 17027344549], [(-2412855021)]]], r0 := 1056539747781, V1 := [[[240236667388683455]], [[(-23703165248043699), 0], [685807363714974]], [[185510144647123, 0, 0], [(-67107021040862), 0], [(-7839099426104)]], [[(-1611613204119), 0, 0, 0], [474022262737, 0, 0], [768711008308, 0], [136263201893]], [[14847292914, 0, 0, 0, 0], [(-4142685784), 0, 0, 0], [(-5583214059), 0, 0], [(-13370970950), 0], [(-2757394832)]]], r1 := 246402511598, V2 := [[[18442243770450701622]], [[(-38901208699325), 14341241986], [(-128573505433432)]], [[21636741167, (-1178414428), (-43672)], [(-1112750745985), 824012241], [110186587]], [[(-178869221), (-11456577), 7556, 0], [685715060, (-67696368), (-3766)], [(-22048634), 11914750], [(-885556)]], [[1890911, 6234, (-291), 0, 0], [(-5606911), (-659570), 651, 0], [1177307, (-978448), (-109)], [167094, 1678], [11343]]], r2 := 2564119826, V3 := [[[18442664859599850131]], [[(-76963948284762), 25970810588], [(-116549724628296)]], [[44967333, (-1865685262), (-158064)], [(-2198916099384), 1492097668], [(-21570494)]], [[5815, (-44966579), 25704, 1], [2585927, (-107158385), (-13629)], [1548094, 21570887], [(-2984)]], [[(-30), (-5790), (-755), 0, 0], [371, (-2585863), 2216, 0], [37463, (-1548159), (-393)], [201, 2988], [16]]], r3 := 7569893513, Vm := [[[18442243785391358084]], [[(-38902495586994), 0], [(-128572645078757)]], [[21630150138, 0, 0], [(-1112825016710), 0], [122687474]], [[(-178859710), 0, 0, 0], [685350042, 0, 0], [(-23133034), 0], [(-883078)]], [[1890914, 0, 0, 0, 0], [(-5606314), 0, 0, 0], [1172464, 0, 0], [166818, 0], [11330]]], rm := 260002632 }
noncomputable def w6 : Wit := { Z0 := { p := [[[210232805474498617]], [[(-20747883863680918), 30033257924928373], [600301748155338]], [[163132426331250, (-2963983409097274), 0], [(-58783684568088), 85757392593619], [(-6861101120351)]], [[(-1447180882569), 23304632333035, 0, 0], [421664392755, (-8397669224013), 0], [673180872777, (-980157302908)], [119260292254]], [[13727058453, (-206740126082), 0, 0, 0], [(-3936439537), 60237770393, 0, 0], [(-4944734542), 96168696111, 0], [(-11708472968), 17037184607], [(-2413294623)]]], r := 259194656749, ok := true }, Z1 := { p := [[[240266063399426990]], [[(-23711867272778192), 0], [686059140748958]], [[186437058664286, 0, 0], [(-67181353792100), 0], [(-7841258423259)]], [[(-1653921008651), 0, 0, 0], [481902163149, 0, 0], [769349568888, 0], [136297476861]], [[15688066804, 0, 0, 0, 0], [(-4498788042), 0, 0, 0], [(-5651125190), 0, 0], [(-13381111964), 0], [(-2758050998)]]], r := 61590547460, ok := true }, Z2 := { p := [[[10467532963085608185025]], [[(-81466447295666032271), 30033257924928373], [(-269257101622998537058)]], [[718241278347128689, (-2963983409097274), 0], [2117930473918678149, 85757392593619], [7351233523732937439]], [[(-6775590910017704), 23304632333035, 0, 0], [(-18586542449882339), (-8397669224013), 0], [(-58049908287257715), (-980157302908)], [(-204094839064972586)]], [[67641707150396, (-206740126082), 0, 0, 0], [173514766635854, 60237770393, 0, 0], [508641800947915, 96168696111, 0], [1615408822712632, 17037184607], [5711080792541789]]], r := 847840641188933, ok := true }, Z3 := { p := [[[11436113822176712256813]], [[(-194473166371721435413), 65623267528208362], [(-294498846451519986653)]], [[3507713630691861755, (-7081447395165931), 0], [5067170565789929737, 185468286814543], [8043682962145279560]], [[(-64327224369782080), 121550950846693, 0, 0], [(-91791957108189437), (-19667646669862), 0], [(-138999016034278613), (-2125219230337)], [(-223374299135643596)]], [[1188907967319405, (-2198512119363), 0, 0, 0], [1687684666917436, 303540384483, 0, 0], [2522137478573758, 226346643679, 0], [3869956151747908, 36970463712], [6251645416312821]]], r := 3270654695136112, ok := true }, iE := { p := [[[10470118553563327018666]], [[(-81467453568868012825), 0], [(-269249718691108886335)]], [[718269944688376275, 0, 0], [2117933259453465989, 0], [7351149141099678059]], [[(-6775953103819535), 0, 0, 0], [(-18586447266356653), 0, 0], [(-58049923921727041), 0], [(-204093372318261357)]], [[67646043534354, 0, 0, 0, 0], [173513339716216, 0, 0, 0], [508640764080562, 0, 0], [1615409006155798, 0], [5711051112152079]]], r := 847749974717853, ok := true }, iHu := { p := [[[11438708924119873223893]], [[(-194475526808179503962), 0], [(-294491512023814138814)]], [[3507799457545869177, 0, 0], [5067177591191035172, 0], [8043598919384807181]], [[(-64329012484508294), 0, 0, 0], [(-91791830568037921), 0, 0], [(-138999057716558973), 0], [(-223372837121851316)]], [[1188942851635991, 0, 0, 0, 0], [1687681350304020, 0, 0, 0], [2522135773059052, 0, 0], [3869956663564602, 0], [6251615817639769]]], r := 3270418483229601, ok := true }, T := { p := [[[16140901064495857664]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[32500335615123397]], [[252883438630844, 0], [835779096193753]], [[(-261911501346), 0, 0], [6432023413947, 0], [(-1325823354671)]], [[1647059997, 0, 0, 0], [(-7484013234), 0, 0], [(-11332934326), 0], [12625334286]], [[(-15538301), 0, 0, 0, 0], [47058856, 0, 0, 0], [(-23645), 0, 0], [107908838, 0], [(-180361920)]]], r := 100188482, ok := true }, de := { p := [[[(-121219430649496940718)]], [[251094047484129932, 0], [380228129047396754]], [[(-2368549828254990), 0, 0], [793305402886, 0], [(-5431229769443483)]], [[29793079965032, 0, 0, 0], [1655148, 0, 0], [2506366, 0], [103451996873564]], [[(-421600188184), 0, 0, 0, 0], [4, 0, 0, 0], [23653, 0, 0], [8, 0], [(-2216828504430)]]], r := 293234140828, ok := true }, dde := { p := [[[(-120361687741585840949164)]], [[2270724118594106795569, 0], [3438525093871075996598]], [[(-42843851818167268519), 0, 0], [(-64877833546617865580), 0], [(-98243575312026042174)]], [[808374562605842518, 0, 0, 0], [1224110051942677874, 0, 0], [1853652364370338860, 0], [2806959294625525550]], [[(-15252350237838133), 0, 0, 0, 0], [(-23096416074450426), 0, 0, 0], [(-34974572912781913), 0, 0], [(-52961496125004087), 0], [(-80198836989296814)]]], r := 6377224247779230, ok := true }, nJu := { p := [[[(-242438861298993881435)]], [[502188094968259865, 0], [760456258094793509]], [[(-4737099656509979), 0, 0], [1586610805773, 0], [(-10862459538886965)]], [[59586159930065, 0, 0, 0], [3310296, 0, 0], [5012732, 0], [206903993747129]], [[(-843200376367), 0, 0, 0, 0], [8, 0, 0, 0], [47306, 0, 0], [16, 0], [(-4433657008859)]]], r := 586468281646, ok := true }, Jd1 := { p := [[[(-240723375483171681898328)]], [[4541448237188213591138, 0], [6877050187742151993196]], [[(-85687703636334537037), 0, 0], [(-129755667093235731160), 0], [(-196487150624052084347)]], [[1616749125211685036, 0, 0, 0], [2448220103885355749, 0, 0], [3707304728740677720, 0], [5613918589251051101]], [[(-30504700475676265), 0, 0, 0, 0], [(-46192832148900852), 0, 0, 0], [(-69949145825563825), 0, 0], [(-105922992250008173), 0], [(-160397673978593628)]]], r := 12754448495558453, ok := true }, term0 := { p := [[[1088975851736981529069864190]], [[(-41086613683815340486734203), 0], [(-62212719968532086223459942)]], [[1162764423392359025761592, 0, 0], [2347455176649772005186869, 0], [2666052744994614575012538]], [[(-29251126805119474717096), 0, 0, 0], [(-66435574494664172617094), 0, 0], [(-100600203004967886686930), 0], [(-101559977290487714216270)]], [[689873626895657393395, 0, 0, 0, 0], [1671312110996826291498, 0, 0, 0], [2847123094884868513156, 0, 0], [3832293088737474927704, 0], [3627057685991378984743]]], r := 515609398252568837264, ok := true }, r0 := { p := [[[54545910492816702126963]], [[(-1296505401213121969127), 15579836990552402301735], [(-1405085901685632933077)]], [[22939726205304059710, (-369389467734266760567), 1111500558614401613809], [33697638037265329162, (-401358691902114975530)], [38385473139178973273]], [[(-360330164619753401), 6477162054416623956, (-26087822172855480414), (-192006098859961583)], [(-593941206155729055), 9606979836351086230, (-28641506474029842012)], [(-923520453210907836), 10964925486503334677], [(-1066100664088267159)]], [[5387220750654106, (-100500621124775488), 440673445730981235, 42394890891536255, (-6834464099813156)], [9246163009153718, (-168141856633295864), 680239334099766218, 3851233787490505], [16255077161640808, (-263341524087998746), 782536952580819123], [25698111048532951, (-304538458677147244)], [29839815547669765]]], r := 155244913720474901, ok := true }, r1 := { p := [[[71237049203426903483774]], [[(-1691938792538005906276), 0], [(-1835082111641258587362)]], [[29854320648632197409, 0, 0], [43983974320914902529, 0], [50132836199865091389]], [[(-467209860767973892), 0, 0, 0], [(-773583658903432501), 0, 0], [(-1205501145189800440), 0], [(-1392371628243206242)]], [[6957737683218421, 0, 0, 0, 0], [12006857370871990, 0, 0, 0], [21176800638737426, 0, 0], [33545726643502979, 0], [38972131891796548]]], r := 18610571338837299, ok := true }, r2 := { p := [[[515793352865461570342854220]], [[(-10882788868493312532795722), 28701221261142007214940], [(-29256677816922806648243788)]], [[185675735823876154237152, (-430401247641134621768), 455645814953400652], [612183885042183443749230, (-820488984425621036884)], [1248348281490211832477571]], [[(-3030579595229794012654), 6150928704087699212, 108086593670588, (-1602490925934)], [(-10351510872012647777979), 12126759429400509767, 95199620483198], [(-25988408800692456635370), 23446222585088622632], [(-47409669819438564316757)]], [[49693965161121924861, (-88583120229668934), (-12875707895212), (-1801668872999), (-89951230181)], [167515015372200881519, (-170322265333074007), (-11304073788678), (-310852618384)], [437005714708458106840, (-344542825650634639), (-14804671706548)], [983411298736167972773, (-669944082379205141)], [1689227661187653443517]]], r := 3801976294762494987529, ok := true }, r3 := { p := [[[2177289002039829313599321958]], [[(-82153876585526907945269018), 131296934923424385984373], [(-124406498245091167441905410)]], [[2325034554042177581442922, (-3841309031156687704024), 1817411258877932946], [4694357279934126393549868, (-3760279741030662379565)], [5331564204735518055007923]], [[(-58490489934167638724249), 98189090484951969083, 973276763971973, (-103922136369905)], [(-132857022099026169570771), 109945429179781663835, 383913677097865], [(-201184601981530304198589), 107530518056405141221], [(-203104487781772739603549)]], [[1379479240966893371200, (-2337817585666511107), (-44828230690483), 6993576463103, (-10702974143514)], [3342287983584131478262, (-2809728936628451896), (-33037875489568), 8174585989054], [5693842500570446968144, (-3143337132713428365), (-84311831878813)], [7664134544292417044612, (-3073896672448169070)], [7253673377724715085864]]], r := 48049646235601765827130, ok := true }, eta := { p := [[[(-515969652116653547179857974)]], [[10887223830149694911771704, 0], [29261660564303342789408513]], [[(-185768208227146317750740), 0, 0], [(-612309223549513793733193), 0], [(-1248490056241664975068811)]], [[3032393423179606350737, 0, 0, 0], [10354120923181313984834, 0, 0], [25991974314183305443450, 0], [47413710408946836776912]], [[(-49728727875392832363), 0, 0, 0, 0], [(-167566156724609341712), 0, 0, 0], [(-437079935036740145567), 0, 0], [(-983512907476244478292), 0], [(-1689342906520381046661)]]], r := 409008237942127497838, 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 := 2462906046218240, bh := 70368744177664, tc := 16140901064495857664, th := 2305843009213693952, sc := 15852670688344145920, sh := 288230376151711744 }
noncomputable def q7 : Cert := { V0 := [[[169367905468850220]], [[(-20108623004447928), 24192472568825729], [484301828721119]], [[154304311120854, (-2871612385972559), (-630444889014)], [(-57111578486667), 69160734158529], [(-5533405084457)]], [[(-1318475456752), 21911006077304, 224527012512, (-29999657692)], [395044119584, (-8149826960869), (-5407572799)], [653663508048, (-790270217496)], [96171661317]], [[11949544549, (-181452224933), (-28372614949), 10678984178, 2305686], [(-3420458843), 55305813065, 1921369110, (-257195711)], [(-4648757724), 93303544568, 46326151], [(-11366914665), 13735376829], [(-1945958094)]]], r0 := 976222622081, V1 := [[[193559717595500684]], [[(-22980000185831201), 0], [553456898145037]], [[176185596982982, 0, 0], [(-65259392787169), 0], [(-6323626771740)]], [[(-1498380631275), 0, 0, 0], [450096715898, 0, 0], [746949782403, 0], [109906267858]], [[13488416946, 0, 0, 0, 0], [(-3837763532), 0, 0, 0], [(-5300972897), 0, 0], [(-12989263578), 0], [(-2223871669)]]], r1 := 221495081772, V2 := [[[18442166053178862364]], [[(-38816749412474), 11938635818], [(-130796307995595)]], [[20607164615, (-1224167674), (-29749)], [(-1110073329743), 685984179], [70732362]], [[(-164602590), (-11420472), 6354, 0], [653439463, (-70330244), (-2565)], [(-17438017), 9919584], [(-584880)]], [[1681090, 5808, (-310), 0, 0], [(-5160375), (-657394), 548, 0], [1128661, (-1016695), (-74)], [133826, 1405], [7488]]], r2 := 2550953986, V3 := [[[18442510931883196006]], [[(-76963768346557), 22059527886], [(-120947546480414)]], [[45001545, (-2045620147), (-109877)], [(-2198905751281), 1267434528], [(-18324397)]], [[5592, (-45000641), 22384, 0], [2588109, (-117506202), (-9474)], [1698028, 18324670], [(-2557)]], [[(-27), (-5567), (-905), 0, 0], [356, (-2588032), 1930, 0], [37502, (-1698084), (-273)], [226, 2559], [14]]], r3 := 7298416753, Vm := [[[18442166065519455481]], [[(-38818062550093), 0], [(-130795597637669)]], [[20600630668, 0, 0], [(-1110149053379), 0], [81045155]], [[(-164593080), 0, 0, 0], [653078025, 0, 0], [(-18541669), 0], [(-582937)]], [[1681088, 0, 0, 0, 0], [(-5159779), 0, 0, 0], [1123879, 0, 0], [133568, 0], [7478]]], rm := 259575052 }
noncomputable def w7 : Wit := { Z0 := { p := [[[169378205320288664]], [[(-20112291813473083), 24196886474326952], [484390189367183]], [[154768106638091, (-2873184544781869), 0], [(-57142982757934), 69198598481026], [(-5534161955848)]], [[(-1342651382032), 22109729519727, 0, 0], [398998131311, (-8163283251134), 0], [653932909775, (-790594565122)], [96183674405]], [[12432366095, (-191807340291), 0, 0, 0], [(-3624739697), 56999733044, 0, 0], [(-4682769302), 93418987110, 0], [(-11371191872), 13740524915], [(-1946188044)]]], r := 240152951395, ok := true }, Z1 := { p := [[[193575091794615617]], [[(-22985476358254952), 0], [553588787848209]], [[176877836157819, 0, 0], [(-65306266009067), 0], [(-6324756520969)]], [[(-1534458722322), 0, 0, 0], [455997864356, 0, 0], [747351896886, 0], [109924199321]], [[14208418395, 0, 0, 0, 0], [(-4142559654), 0, 0, 0], [(-5351736345), 0, 0], [(-12995647853), 0], [(-2224214908)]]], r := 55360079783, ok := true }, Z2 := { p := [[[10307419888830253514740]], [[(-78672680289842250263), 24196886474326952], [(-265094225502623598226)]], [[679155943329956634, (-2873184544781869), 0], [2045613201197379459, 69198598481026], [7237131158790404233]], [[(-6261755094487743), 22109729519727, 0, 0], [(-17585077498227478), (-8163283251134), 0], [(-56070658668614554), (-790594565122)], [(-200919558078267672)]], [[60963591763243, (-191807340291), 0, 0, 0], [160528315322626, 56999733044, 0, 0], [481335199823200, 93418987110, 0], [1560377122693731, 13740524915], [5622082652597335]]], r := 814290702458771, ok := true }, Z3 := { p := [[[11060702067717085320414]], [[(-181177883692460859571), 51929611342745022], [(-284718653723473107528)]], [[3148611983845578382, (-6620391047354838), 0], [4719299487512055573, 147306531730275], [7775415400336765548]], [[(-55637163887099316), 109272210614840, 0, 0], [(-82371804925754007), (-18513719787724), 0], [(-129441189700981426), (-1686400078978)], [(-215905564209620839)]], [[990843007493023, (-1903329270884), 0, 0, 0], [1459309347909027, 274111080349, 0, 0], [2263056916749169, 212706377233, 0], [3603593051842519, 29328310158], [6042243584979882]]], r := 2929848081664450, ok := true }, iE := { p := [[[10310003578597123314851]], [[(-78673576109325059964), 0], [(-265086836630052457541)]], [[679182536526864993, 0, 0], [2045616350925842650, 0], [7237046740859617421]], [[(-6262084600095788), 0, 0, 0], [(-17584990443876251), 0, 0], [(-56070678273740020), 0], [(-200918090895551732)]], [[60967439459870, 0, 0, 0, 0], [160527029489753, 0, 0, 0], [481334249873857, 0, 0], [1560377374270626, 0], [5622052965506702]]], r := 814209762118048, ok := true }, iHu := { p := [[[11063292778327406710991]], [[(-181179921213632161394), 0], [(-284711304764279008206)]], [[3148687868741498134, 0, 0], [4719306981371113741, 0], [7775331267710603241]], [[(-55638697717366309), 0, 0, 0], [(-82371696737351682), 0, 0], [(-129441237730241107), 0], [(-215904101052814055)]], [[990871916807177, 0, 0, 0, 0], [1459306531235567, 0, 0, 0], [2263055442578347, 0, 0], [3603593680270094, 0], [6042213968193901]]], r := 2929653150186287, ok := true }, T := { p := [[[16140901064495857664]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[33005067779737910]], [[251855073780291, 0], [848613576493219]], [[(-252388499914), 0, 0], [6402638251133, 0], [(-1348489317905)]], [[1529451745, 0, 0, 0], [(-7211927486), 0, 0], [(-11333028907), 0], [12841151960]], [[(-13904107), 0, 0, 0, 0], [43698621, 0, 0, 0], [(-23645), 0, 0], [107908838, 0], [(-183445030)]]], r := 100598641, ok := true }, de := { p := [[[(-120726484957367432413)]], [[241964364513978363, 0], [380229715664823141]], [[(-2199423623574139), 0, 0], [793312023516, 0], [(-5431229764336140)]], [[26659680636843, 0, 0, 0], [1655168, 0, 0], [2600979, 0], [103451996873581]], [[(-363541099592), 0, 0, 0, 0], [4, 0, 0, 0], [23654, 0, 0], [9, 0], [(-2216828504430)]]], r := 287732327456, ok := true }, dde := { p := [[[(-115985383078678571525018)]], [[2108583154754630143639, 0], [3313487814614418790950]], [[(-38337876045886120571), 0, 0], [(-60245234579795545406), 0], [(-94671081664331044462)]], [[697052291742341277, 0, 0, 0], [1095367887020360266, 0, 0], [1721292393889132394, 0], [2704888047548229638]], [[(-12673678031673921), 0, 0, 0, 0], [(-19915779764064773), 0, 0, 0], [(-31296225343576486), 0, 0], [(-49179782682692389), 0], [(-77282515644231358)]]], r := 5842176269455824, ok := true }, nJu := { p := [[[(-241452969914734864825)]], [[483928729027956727, 0], [760459431329646283]], [[(-4398847247148278), 0, 0], [1586624047033, 0], [(-10862459528672279)]], [[53319361273687, 0, 0, 0], [3310336, 0, 0], [5201958, 0], [206903993747163]], [[(-727082199184), 0, 0, 0, 0], [8, 0, 0, 0], [47308, 0, 0], [18, 0], [(-4433657008859)]]], r := 575464654903, ok := true }, Jd1 := { p := [[[(-231970766157357143050036)]], [[4217166309509260287279, 0], [6626975629228837581900]], [[(-76675752091772241141), 0, 0], [(-120490469159591090811), 0], [(-189342163328662088924)]], [[1394104583484682555, 0, 0, 0], [2190735774040720533, 0, 0], [3442584787778264789, 0], [5409776095096459277]], [[(-25347356063347841), 0, 0, 0, 0], [(-39831559528129546), 0, 0, 0], [(-62592450687152972), 0, 0], [(-98359565365384778), 0], [(-154565031288462716)]]], r := 11684352538911639, ok := true }, term0 := { p := [[[1011230232293552047657706761]], [[(-36765680277606238040680744), 0], [(-57770784741326822632214897)]], [[1002642864398675379111681, 0, 0], [2100575073088977059368621, 0], [2475693686660106315602148]], [[(-24305796630100559502461), 0, 0, 0], [(-57286768032262910951525), 0, 0], [(-90020061092276793740501), 0], [(-94308386387449738436355)]], [[552394963607313164390, 0, 0, 0, 0], [1388750218335673579151, 0, 0, 0], [2455045630905830810091, 0, 0], [3429248329286444304371, 0], [3368076212621465676506]]], r := 451338157397610661849, ok := true }, r0 := { p := [[[52041859678759798117026]], [[(-1208904208294793512206), 14866185751855547393620], [(-1339994543968522397539)]], [[20900950512460060493, (-344641046377775833168), 1061037159052926306459], [31428611483986003564, (-382797153546199055838)], [36601492656637076788]], [[(-320232848268530605), 5908090373563034745, (-24400120130109036305), (-118984371322622832)], [(-541588931672846836), 8964345408357955999, (-27325961997320649262)], [(-861411964984283245), 10456113931510514536], [(-1016457832468697442)]], [[4658438339199631, (-89454270944672478), 403850222302309649, 30988229861819796, (-4240230835025159)], [8228881774729574, (-153457521717681041), 635952284429498480, 2383808183269971], [14826780295046927, (-245737455611652347), 746449511658651193], [23971137205030162, (-290378340027855073)], [28448453244746452]]], r := 139894898535205928, ok := true }, r1 := { p := [[[67968959365873571521671]], [[(-1577913284838153843572), 0], [(-1750115190711278242184)]], [[27210211044002141015, 0, 0], [41028264808911002290, 0], [47803994603709008108]], [[(-415410118024458416), 0, 0, 0], [(-705587555200388036), 0, 0], [(-1124577423109951741), 0], [(-1327564960949842428)]], [[6019583058832356, 0, 0, 0, 0], [10689858357393665, 0, 0, 0], [19320834218542343, 0, 0], [31295276414696994, 0], [37155727863941003]]], r := 16422040822052939, ok := true }, r2 := { p := [[[494747002797885460758520940]], [[(-10174926599038018712529880), 27864334315936043100504], [(-28072418192471039500070503)]], [[168621619581290245307834, (-406819930987446866130), 455852380441203267], [572704256217429734674442, (-796898002160966373419)], [1198064979129919035541912]], [[(-2664156538742179754731), 5649469707928393259, 92892696983157, (-1357129602358)], [(-9408407273649700813939), 11473315266796236137, 97757235057149], [(-24321293233072670832671), 22775852017460505078], [(-45506683042115689952345)]], [[42164872784647685019, (-78823242244714852), (-5158461376009), (-1640083569416), (-85253218629)], [147400291053664228023, (-156679271963105010), (-4401870595017), (-289058894481)], [397392561253702641170, (-326111344144110137), (-2005933453065)], [920566833260907687001, (-650860402120158324)], [1621605884971315803658]]], r := 3551368385086434537859, ok := true }, r3 := { p := [[[2021834577550630644099269676]], [[(-73513853903376924980033166), 123989187811629304950262], [(-115523680001824079905273184)]], [[2004856032357200998164145, (-3474990374069160790044), 1819416670200780978], [4200649778373710942443039, (-3551115834133720008842)], [4950876155133597950790714]], [[(-48601755319408026949966), 85352535715570247794, 924612108660927, (-90952555597233)], [(-114561255273307076292385), 99463073073918218561, 352504022222025], [(-180025824142924671743057), 101550539839009208399], [(-188602165100170500182199)]], [[1104574167936497654162, (-1954963832767985355), (-64686660693498), 6154778161902, (-9309047505908)], [2777219255672437353904, (-2442447047514401496), (-24180587254624), 7206330675846], [4909740296501273774158, (-2843696159933666831), (-8329006256385)], [6858088063323775951241, (-2902987063525045850)], [6735735015950018034938]]], r := 41385126819778874817646, ok := true }, eta := { p := [[[(-494914788040269521863866660)]], [[10179012375694118605160347, 0], [28077160309048236860210308]], [[(-168703992989369549143001), 0, 0], [(-572819738284240630387799), 0], [(-1198199908482943608393222)]], [[2665716882684630769415, 0, 0, 0], [9410732568126171799890, 0, 0], [24324578490434617944705, 0], [45510528557177764080801]], [[(-42193718197011121746), 0, 0, 0, 0], [(-147444294624373205918), 0, 0, 0], [(-397458684851575268030), 0, 0], [(-920660453665084091681), 0], [(-1621715576544207389589)]]], r := 384173315725340703521, 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 2251799813685248 2533274790395904 13835058055282163712 18446744073709551616 13835058055282163712 16140901064495857664 :=
  (RegionPosI.split_s 14987979559889010688 (RegionPosI.split_b 2392537302040576 (RegionPosI.split_s 14411518807585587200 (RegionPosI.of_check c0 q0 ok_0 2251799813685248 2392537302040576 13835058055282163712 18446744073709551616 13835058055282163712 14411518807585587200 (by decide +kernel)) (RegionPosI.of_check c1 q1 ok_1 2251799813685248 2392537302040576 13835058055282163712 18446744073709551616 14411518807585587200 14987979559889010688 (by decide +kernel))) (RegionPosI.split_s 14411518807585587200 (RegionPosI.of_check c2 q2 ok_2 2392537302040576 2533274790395904 13835058055282163712 18446744073709551616 13835058055282163712 14411518807585587200 (by decide +kernel)) (RegionPosI.of_check c3 q3 ok_3 2392537302040576 2533274790395904 13835058055282163712 18446744073709551616 14411518807585587200 14987979559889010688 (by decide +kernel)))) (RegionPosI.split_b 2392537302040576 (RegionPosI.split_s 15564440312192434176 (RegionPosI.of_check c4 q4 ok_4 2251799813685248 2392537302040576 13835058055282163712 18446744073709551616 14987979559889010688 15564440312192434176 (by decide +kernel)) (RegionPosI.of_check c5 q5 ok_5 2251799813685248 2392537302040576 13835058055282163712 18446744073709551616 15564440312192434176 16140901064495857664 (by decide +kernel))) (RegionPosI.split_s 15564440312192434176 (RegionPosI.of_check c6 q6 ok_6 2392537302040576 2533274790395904 13835058055282163712 18446744073709551616 14987979559889010688 15564440312192434176 (by decide +kernel)) (RegionPosI.of_check c7 q7 ok_7 2392537302040576 2533274790395904 13835058055282163712 18446744073709551616 15564440312192434176 16140901064495857664 (by decide +kernel)))))

end CKLaneC.RSC2.S02_0245