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

import Definitions.Def_CK_CKLaneC_RSCell_Staged
import Definitions.Def_CK_CKLaneC_RSCell_RegionI

-- ===== source module CKLaneC.RSC2.S03_0032 =====
section

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

namespace CKLaneC.RSC2.S03_0032
open CKLaneC.TM3 CKLaneC.RSCell

noncomputable def c0 : Cell := { bc := 5770237022568448, bh := 140737488355328, tc := 16140901064495857664, th := 2305843009213693952, sc := 2666130979403333632, sh := 72057594037927936 }
noncomputable def q0 : Cert := { V0 := [[[1783520880223027571]], [[(-14484748435981151), 251364978574894384], [4608303273224026]], [[59414536313406, (-1986034539307525), (-722049002912230)], [(-37577002260732), 631854222990298], [(-44364438570133)]], [[(-350294782440), 7474703250185, 17362297403658, (-31667194522297)], [173360790658, (-4724829860256), (-5523791614995)], [362661839496, (-6150895684431)], [655405719169]], [[3151465098, (-40744254269), (-207585904540), 717641304036, 279468342636], [(-1306569169), 16837515577, 131812690358, (-228316617650)], [(-1639183070), 47258128658, 39374927213], [(-5358490670), 91116078031], [(-11291923604)]]], r0 := 1356081444485, V1 := [[[2034132428350722404]], [[(-16452714300374043), 0], [5234408971542329]], [[66674175903907, 0, 0], [(-42165272488978), 0], [(-50474259417562)]], [[(-389125921317), 0, 0, 0], [188577590912, 0, 0], [408933957784, 0], [745968616957]], [[3501512440, 0, 0, 0, 0], [(-1402931713), 0, 0, 0], [(-1805786440), 0, 0], [(-6049513091), 0], [(-12855165408)]]], r1 := 259102204167, V2 := [[[18440379324487941446]], [[(-26022717030271), 237470818467], [(-154570111618227)]], [[29013290995, (-101944664), (-8454464)], [(-644169478172), 11627986523], [9947428999]], [[(-294587374), (-5552145), 41973, 295], [783849372, (-4472580), (-621767)], [(-140924965), 142997586], [(-61649651)]], [[4087086, 15895, 183, (-3), 0], [(-7956444), (-277102), 3067, 29], [1126879, (-40773), (-15290)], [871777, 11959], [672316]]], r2 := 978490141, V3 := [[[18445075991824188467]], [[(-45082763787328), 122754690436], [(-40687945224353)]], [[14798651, 2787206988, (-8664082)], [(-1099648341858), 6015633699], [(-74090220)]], [[5673, (-14800584), (-158485), 602], [723392, 136725751, (-637118)], [(-1687854), 74105881], [(-7287)]], [[(-58), (-5669), 1933, 8, 0], [304, (-723534), (-11671), 59], [8859, 1688141, (-15664)], [(-207), 7416], [33]]], r3 := 4727221578, Vm := [[[18440379654230702428]], [[(-26023777784477), 0], [(-154553705694183)]], [[29012942792, 0, 0], [(-644223272028), 0], [10156271413]], [[(-294628362), 0, 0, 0], [783836054, 0, 0], [(-141636002), 0], [(-61560235)]], [[4087814, 0, 0, 0, 0], [(-7958502), 0, 0, 0], [1126801, 0, 0], [871236, 0], [671923]]], rm := 121100404 }
noncomputable def w0 : Wit := { Z0 := { p := [[[1795648103289981918]], [[(-14781870002713167), 256521157612854559], [4702832100878041]], [[63080084321062, (-2111695714673310), 0], [(-39904697406481), 671833157268291], [(-45026812786927)]], [[(-384546832533), 9011440617294, 0, 0], [202673320727, (-5700671058069), 0], [378926662040, (-6432401826704)], [664306589073]], [[3463993380, (-54935261791), 0, 0, 0], [(-1593793114), 28953331532, 0, 0], [(-1841224478), 54132380291, 0], [(-5576886223), 94900941296], [(-11436633075)]]], r := 277652981703, ok := true }, Z1 := { p := [[[2052169260902836478]], [[(-16893565717386476), 0], [5374665258146333]], [[72091524938357, 0, 0], [(-45605368464549), 0], [(-51459214613631)]], [[(-439482094323), 0, 0, 0], [231626652259, 0, 0], [433059042331, 0], [759207530369]], [[3958849577, 0, 0, 0, 0], [(-1821477845), 0, 0, 0], [(-2104256546), 0, 0], [(-6373584255), 0], [(-13070437800)]]], r := 66453894295, ok := true }, Z2 := { p := [[[7665933612278544785085]], [[(-28110306520726723490), 256521157612854559], [(-166970005917406691494)]], [[141009768507220641, (-2111695714673310), 0], [606980857360446736, 671833157268291], [3880020114276050765]], [[(-998105029705181), 9011440617294, 0, 0], [(-2933829021276684), (-5700671058069), 0], [(-14064024179963147), (-6432401826704)], [(-91796760642001058)]], [[10232588057932, (-54935261791), 0, 0, 0], [19855491798424, 28953331532, 0, 0], [67071510189172, 54132380291, 0], [332161152941597, 94900941296], [2190093319773744]]], r := 155642246122357, ok := true }, Z3 := { p := [[[25697093004230982698293]], [[(-631455645214024887529), 1719374229549221139], [(-569899237439804291280)]], [[16368362426457615877, (-50097595169159144), 0], [14142745328386844626, 3811002239548328], [13331419020972701127]], [[(-430828150600866885), 1288011864137915, 0, 0], [(-367962926496951335), (-101678953341002), 0], [(-332062902989309817), (-38027479455461)], [(-316659520331684588)]], [[11421773978960949, (-33824543428119), 0, 0, 0], [9706629061532476, 2478593123751, 0, 0], [8652078678914434, 1035367986699, 0], [7905005836956433, 568385048458], [7575994583772373]]], r := 11580071862493120, ok := true }, iE := { p := [[[7668935729753255955116]], [[(-28113112504921730522), 0], [(-166962143322054734272)]], [[141034921329615189, 0, 0], [606971517668807492, 0], [3879944834614489843]], [[(-998345057875286), 0, 0, 0], [(-2933715034976812), 0, 0], [(-14063940002719588), 0], [(-91795649997651551)]], [[10235527516520, 0, 0, 0, 0], [19854273093659, 0, 0, 0], [67070546502939, 0, 0], [332159933826908, 0], [2190074199036256]]], r := 155451197800308, ok := true }, iHu := { p := [[[25701136281528781095036]], [[(-631500035006753079374), 0], [(-569890275493898504114)]], [[16369587326691034693, 0, 0], [14142668955330278460, 0], [13331329595621470250]], [[(-430860929854670980), 0, 0, 0], [(-367960696589513989), 0, 0], [(-332062092044991409), 0], [(-316658183718442780)]], [[11422649661797278, 0, 0, 0, 0], [9706569779001439, 0, 0, 0], [8652055472254458, 0, 0], [7904993471735907, 0], [7575971395117242]]], r := 11574420280249097, ok := true }, T := { p := [[[16140901064495857664]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[44371524147834640]], [[162659030449726, 0], [966022540187221]], [[(-219728376123), 0, 0], [3570710502843, 0], [(-1417389908761)]], [[1979445422, 0, 0, 0], [(-5359470988), 0, 0], [(-4836595769), 0], [11520278907]], [[(-26749262), 0, 0, 0, 0], [48279156, 0, 0, 0], [(-5910), 0, 0], [39318361, 0], [(-140491216)]]], r := 73163754, ok := true }, de := { p := [[[(-133120277473444609854)]], [[359651749030760828, 0], [324563773515564649]], [[(-4859939032375436), 0, 0], [396600853135, 0], [(-3957915844926813)]], [[87566469230816, 0, 0, 0], [484627, 0, 0], [437347, 0], [64356355333622]], [[(-1774995997922), 0, 0, 0, 0], [1, 0, 0, 0], [5911, 0, 0], [1, 0], [(-1177250402444)]]], r := 314946821859, ok := true }, dde := { p := [[[(-294339272110578782484693)]], [[7954755794438409482180, 0], [7178682058395637826714]], [[(-214993400289183206918), 0, 0], [(-194018434803930484947), 0], [(-175089806660256884158)]], [[5810632440247672304, 0, 0, 0], [5243741470466450901, 0, 0], [4732156936762414497, 0], [4270483089274189620]], [[(-157044120006687612), 0, 0, 0, 0], [(-141722742445058381), 0, 0, 0], [(-127896133426020572), 0, 0], [(-115418461872275962), 0], [(-104158124128622811)]]], r := 20630485456763158, ok := true }, nJu := { p := [[[(-266240554946889219708)]], [[719303498061521656, 0], [649127547031129299]], [[(-9719878064750872), 0, 0], [793201706270, 0], [(-7915831689853625)]], [[175132938461633, 0, 0, 0], [969255, 0, 0], [874694, 0], [128712710667244]], [[(-3549991995843), 0, 0, 0, 0], [2, 0, 0, 0], [11823, 0, 0], [2, 0], [(-2354500804887)]]], r := 629893643710, ok := true }, Jd1 := { p := [[[(-588678544221157564969385)]], [[15909511588876818964361, 0], [14357364116791275653429]], [[(-429986800578366413836), 0, 0], [(-388036869607860969893), 0], [(-350179613320513768316)]], [[11621264880495344608, 0, 0, 0], [10487482940932901803, 0, 0], [9464313873524828995, 0], [8540966178548379240]], [[(-314088240013375224), 0, 0, 0, 0], [(-283445484890116761), 0, 0, 0], [(-255792266852041143), 0, 0], [(-230836923744551923), 0], [(-208316248257245622)]]], r := 41260970913526307, ok := true }, term0 := { p := [[[6513097825981139689395669385]], [[(-352035474081023035384355914), 0], [(-317640881061328684849143170)]], [[14271385918594302536794227, 0, 0], [17169195299366033693520223, 0], [11620139492909293527091713]], [[(-514278366614201902267982), 0, 0, 0], [(-696040592470089420911627), 0, 0], [(-628101451794558128785296), 0], [(-377876595691394499589130)]], [[17374151359281417634512, 0, 0, 0, 0], [25082402150053291245159, 0, 0, 0], [25463380525848398457993, 0, 0], [20425415673879004936437, 0], [11520369633422884090102]]], r := 4283367474058302309293, ok := true }, r0 := { p := [[[115714601234189488886860]], [[(-1750964611108584720468), 32375296729814076584070], [(-2493609369507346422532)]], [[26958367922099197535, (-479578308130776246422), 2121127403609305483974], [36490257085040163212, (-701119584634193014093)], [57722826410040023324]], [[(-517027733619955054), 7325538185901167315, (-28553769257702994485), (-26055221721828206700)], [(-537455952412752984), 10089013712906051748, (-46892664004196081424)], [(-834227967880639209), 16253359638764785986], [(-1362446145429666547)]], [[11714708902553983, (-141446553882777585), 420832134522053067, 755966460393397625, (-709356759370623025)], [10012543019526535, (-147618803092840725), 626815159990264138, 440449855423665347], [12079907479894184, (-231288188582894485), 1093724341881019229], [19541974132125431, (-383950026466785423)], [32451050274105167]]], r := 491339062094568196, ok := true }, r1 := { p := [[[150184278302655227820264]], [[(-2258324412448195491091), 0], [(-3241168255229906566173)]], [[34691332283108016973, 0, 0], [47193024838685393586, 0], [75060315811597939928]], [[(-666667397818789596), 0, 0, 0], [(-693756879209300823), 0, 0], [(-1079789162581293041), 0], [(-1772108364710240756)]], [[15142194031902240, 0, 0, 0, 0], [12946806330892110, 0, 0, 0], [15606677846078366, 0, 0], [25306114648062005, 0], [42215660344247176]]], r := 35994110266138007, ok := true }, r2 := { p := [[[460478187799285737170379788]], [[(-9378503499541403465721887), 37205060589058229595607], [(-21739138373033014888827046)]], [[211256319137297003640348, (-518807608922237969330), 448136947695592772], [434238408483773355068696, (-875514170980160744136)], [779737885906152953467767]], [[(-5254129731927038226271), 9816986212813626414, 153956747718300, (-17769008076900)], [(-9698469243838408475446), 11585424322089742054, 45353187250532], [(-15386296637554056798828), 21052029891369689300], [(-25004506056178880931885)]], [[136474247543821809812, (-226825948263456006), (-5674726851466), (-865972456282), (-688572278330)], [240658960540595856112, (-212888395767789710), (-2164077335969), (-1194865210260)], [341788732594253161599, (-272532189071582686), (-4057110646920)], [489058979820724730430, (-509021545340195111)], [754177671208872499489]]], r := 1522158182617220475974, ok := true }, r3 := { p := [[[13020378616488810949580197103]], [[(-703776308607907954351855545), 1155493872557202601503574], [(-635139841137968955086840350)]], [[28531094223485755167202839, (-58576819145650157770554), 1470076262581438399], [34331202460300392832308222, (-28226185382672157243523)], [23236817104709677791530554]], [[(-1028140729697279431352653), 2322492485774715146354, 15311209240577620, (-1635530032497409)], [(-1391796302653249546442271), 1430508376892594482508, (-2441850621697111)], [(-1256027566519654409813805), 688833670880902755304], [(-755668750684654498943100)]], [[34734344950555712337893, (-82758758392092043568), (-2515038931998676), (-2041283844848497), (-286631041324501)], [50154654907103904058167, (-56712747899198184018), (-2067709240379777), (-1060706205094345)], [50919810430533227739149, (-34907166326053046465), (-2634807881603501)], [40846553373503271447286, (-16807003572236453234)], [23038677802786244951579]]], r := 441766269787297403563615, ok := true }, eta := { p := [[[(-461096851702752573351469082)]], [[9396785819674836799767034, 0], [21753988783497886086246597]], [[(-211754015220276161357379), 0, 0], [(-434676611861694833017901), 0], [(-780097886804854990139427)]], [[5267570957507963799530, 0, 0, 0], [9710393753867569413650, 0, 0], [15396913729086382921349, 0], [25013254415040310095745]], [[(-136837150156827771314), 0, 0, 0, 0], [(-240981017732956065979), 0, 0, 0], [(-342077615167103679498), 0, 0], [(-489316903363290312053), 0], [(-754390499776206324066)]]], r := 125291904111326801277, ok := true } }
theorem sB_0 : stageB c0 w0 = true := by decide +kernel
theorem s0_0 : stageC0 w0 q0 = true := by decide +kernel
theorem s1_0 : stageC1 w0 q0 = true := by decide +kernel
theorem s2_0 : stageC2 w0 q0 = true := by decide +kernel
theorem s3_0 : stageC3 w0 q0 = true := by decide +kernel
theorem sE_0 : stageE w0 q0 = true := by decide +kernel
theorem sF_0 : stageF w0 = true := by decide +kernel
theorem ok_0 : (domOK c0 && cellCheck c0 q0) = true :=
  staged_check c0 q0 w0 (by decide +kernel) sB_0 s0_0 s1_0 s2_0 s3_0 sE_0 sF_0

noncomputable def c1 : Cell := { bc := 6051711999279104, bh := 140737488355328, tc := 16140901064495857664, th := 2305843009213693952, sc := 2666130979403333632, sh := 72057594037927936 }
noncomputable def q1 : Cert := { V0 := [[[1792565098087013682]], [[(-14558493237010312), 252604788116303667], [4438365165601208]], [[59754887031606, (-1995300612943600), (-732943194193927)], [(-36187834229131), 608295967942504], [(-40687072235851)]], [[(-352862186182), 7507685423261, 17622229993529, (-32117140552362)], [167079798006, (-4543876345099), (-5372389193730)], [332596351162, (-5639711776216)], [572890997065]], [[3179538634, (-40961877130), (-210693912814), 727263452436, 286430515942], [(-1261468932), 16154687553, 128167821704, (-221716679122)], [(-1504322612), 43307645655, 36389529001], [(-4683843789), 79628089463], [(-9408963268)]]], r0 := 1180081038341, V1 := [[[2044405118719805588]], [[(-16535455896846136), 0], [5041070545908239]], [[67044313331633, 0, 0], [(-40598942142099), 0], [(-46288824324141)]], [[(-391881956222), 0, 0, 0], [181659140765, 0, 0], [374992820740, 0], [652031955948]], [[3531894524, 0, 0, 0, 0], [(-1353796783), 0, 0, 0], [(-1656769819), 0, 0], [(-5287374331), 0], [(-10711223736)]]], r1 := 212160165452, V2 := [[[18440070223571695813]], [[(-27311612860864), 261298876676], [(-154531040892242)]], [[30585442053, (-111051788), (-9760169)], [(-644723011953), 12200118678], [9592964677]], [[(-310545241), (-6120564), 48410, 358], [788274672, (-4633986), (-684444)], [(-135913309), 143068077], [(-56616940)]], [[4308764, 17583, 212, (-3), 0], [(-8001150), (-291324), 3373, 33], [1086350, (-39935), (-16050)], [800365, 11544], [588396]]], r2 := 837269253, V3 := [[[18444994615637321125]], [[(-47282067224095), 135082440154], [(-40688241671607)]], [[16280877, 3067412713, (-10002009)], [(-1099655095722), 6312145154], [(-74133148)]], [[6299, (-16283109), (-182996), 729], [758835, 143480795, (-701328)], [(-1689072), 74149587], [(-7027)]], [[(-65), (-6295), 2231, 10, 0], [322, (-758992), (-12850), 68], [8862, 1689374, (-16442)], [(-200), 7157], [31]]], r3 := 4423123837, Vm := [[[18440070586962383692]], [[(-27312784051214), 0], [(-154513798537849)]], [[30585066906, 0, 0], [(-644779656365), 0], [9802334427]], [[(-310590453), 0, 0, 0], [788261047, 0, 0], [(-136627531), 0], [(-56530535)]], [[4309568, 0, 0, 0, 0], [(-8003315), 0, 0, 0], [1086275, 0, 0], [799843, 0], [588035]]], rm := 105016644 }
noncomputable def w1 : Wit := { Z0 := { p := [[[1804878798283985771]], [[(-14860206827084386), 257839828326283681], [4530346874585281]], [[63478272897378, (-2122886689583484), 0], [(-38452982128452), 647192410655040], [(-41299317963587)]], [[(-387681219789), 9068324699625, 0, 0], [195615280563, (-5493283161208), 0], [347631164173, (-5899902566227)], [580730567746]], [[3497637107, (-55383031399), 0, 0, 0], [(-1541324171), 27945040080, 0, 0], [(-1691126637), 49661594881, 0], [(-4876210098), 82961509678], [(-9530441213)]]], r := 232955803048, ok := true }, Z1 := { p := [[[2062718626610269452]], [[(-16983093516667870), 0], [5177539285240321]], [[72546597597004, 0, 0], [(-43946265289660), 0], [(-47199220529814)]], [[(-443064251187), 0, 0, 0], [223560320643, 0, 0], [397292759055, 0], [663692077424]], [[3997299551, 0, 0, 0, 0], [(-1761513338), 0, 0, 0], [(-1932716156), 0, 0], [(-5572811540), 0], [(-10891932814)]]], r := 54425543624, ok := true }, Z2 := { p := [[[7346812745257265101825]], [[(-26950064466153169979), 257839828326283681], [(-152485374455325710542)]], [[135398394579186625, (-2122886689583484), 0], [554471750617542816, 647192410655040], [3377885254137105267]], [[(-960100263183034), 9068324699625, 0, 0], [(-2683274530271788), (-5493283161208), 0], [(-12246876647660256), (-5899902566227)], [(-76189984244438402)]], [[9854986477229, (-55383031399), 0, 0, 0], [18187033207184, 27945040080, 0, 0], [58470902740806, 49661594881, 0], [275751853944861, 82961509678], [1733043575327361]]], r := 122379973802067, ok := true }, Z3 := { p := [[[24608202588485730906522]], [[(-604438057777580312965), 1726848519118323946], [(-520144807836108175263)]], [[15665471134846103207, (-50296932053211511), 0], [12903636824196706222, 3665411539462445], [11599710298249471603]], [[(-412287071423096677), 1292869965658509, 0, 0], [(-335679246001075978), (-97716138860271), 0], [(-288839180742121703), (-34839845291701)], [(-262685500450728753)]], [[10929470728396741, (-33948460557976), 0, 0, 0], [8854285370004894, 2380948188335, 0, 0], [7524931150739500, 948019367654, 0], [6555683440110308, 496359519163], [5991954697843737]]], r := 9878413684324294, ok := true }, iE := { p := [[[7349830295394252613588]], [[(-26952888802455137883), 0], [(-152477800235469505664)]], [[135423771625196160, 0, 0], [554462733640321883, 0], [3377816206418944359]], [[(-960342689623979), 0, 0, 0], [(-2683164241786048), 0, 0], [(-12246799316009306), 0], [(-76189013329601392)]], [[9857956920988, 0, 0, 0, 0], [18185853110978, 0, 0, 0], [58470015840700, 0, 0], [275750786620240, 0], [1733027641523822]]], r := 122218700403676, ok := true }, iHu := { p := [[[24612263442309228334981]], [[(-604482597168219939593), 0], [(-520136188261026790974)]], [[15666700404788121588, 0, 0], [12903563553166316186, 0], [11599628368932918061]], [[(-412319966845405943), 0, 0, 0], [(-335677104885484285), 0, 0], [(-288838439090337471), 0], [(-262684333212590079)]], [[10930349481755262, 0, 0, 0, 0], [8854228449061799, 0, 0, 0], [7524909916553447, 0, 0], [6555672659039632, 0], [5991935393223102]]], r := 9873237653511960, ok := true }, T := { p := [[[16140901064495857664]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[46297989646669163]], [[169781412164831, 0], [960486886489395]], [[(-230447341740), 0, 0], [3551821136652, 0], [(-1351483197162)]], [[2076003734, 0, 0, 0], [(-5359494628), 0, 0], [(-4611658168), 0], [10473547148]], [[(-28054104), 0, 0, 0, 0], [48279156, 0, 0, 0], [(-5910), 0, 0], [35745898, 0], [(-121785442)]]], r := 63883946, ok := true }, de := { p := [[[(-132486484868575675729)]], [[359652542234216484, 0], [309468466573628137]], [[(-4859939031382540), 0, 0], [396602602525, 0], [(-3598299910201567)]], [[87566469230817, 0, 0, 0], [508271, 0, 0], [437349, 0], [55787595632442]], [[(-1774995997922), 0, 0, 0, 0], [1, 0, 0, 0], [5911, 0, 0], [1, 0], [(-973039458705)]]], r := 289892206246, ok := true }, dde := { p := [[[(-280649692372677792006471)]], [[7584767151287037455085, 0], [6526427548781869429757]], [[(-204993707252479923873), 0, 0], [(-176389934544104157363), 0], [(-151777385196671181928)]], [[5540370466282666943, 0, 0, 0], [4767295517498033918, 0, 0], [4102091491800622868, 0], [3529706632480360754]], [[(-149739742331958027), 0, 0, 0, 0], [(-128845824797261231), 0, 0, 0], [(-110867337616253991), 0, 0], [(-95397476553523435), 0], [(-82086200755355098)]]], r := 17759750019613852, ok := true }, nJu := { p := [[[(-264972969737151351457)]], [[719305084468432968, 0], [618936933147256275]], [[(-9719878062765079), 0, 0], [793205205051, 0], [(-7196599820403133)]], [[175132938461634, 0, 0, 0], [1016542, 0, 0], [874699, 0], [111575191264885]], [[(-3549991995843), 0, 0, 0, 0], [2, 0, 0, 0], [11823, 0, 0], [2, 0], [(-1946078917410)]]], r := 579784412482, ok := true }, Jd1 := { p := [[[(-561299384745355584012942)]], [[15169534302574074910170, 0], [13052855097563738859515]], [[(-409987414504959847745), 0, 0], [(-352779869088208314726), 0], [(-303554770393342363856)]], [[11080740932565333887, 0, 0, 0], [9534591034996067836, 0, 0], [8204182983601245737, 0], [7059413264960721509]], [[(-299479484663916054), 0, 0, 0, 0], [(-257691649594522462), 0, 0, 0], [(-221734675232507981), 0, 0], [(-190794953107046869), 0], [(-164172401510710196)]]], r := 35519500039227696, ok := true }, term0 := { p := [[[5921447726918954323999782147]], [[(-320055497611150625684827642), 0], [(-275351435144694038456372691)]], [[12974915385571687930046636, 0, 0], [14883332189373048587654839, 0], [9604529887537831132648206]], [[(-467558978028514133626563), 0, 0, 0], [(-603371181058222312418452), 0, 0], [(-519151471430272701387232), 0], [(-297803209942433311943515)]], [[15795799115075248196362, 0, 0, 0, 0], [21742976777894521807573, 0, 0, 0], [21046514973193238049571, 0, 0], [16097184615269455553079, 0], [8656866504873589797028]]], r := 3501326207368960174144, ok := true }, r0 := { p := [[[110947869725132423587812]], [[(-1681171743235198020575), 31035139109853966337095], [(-2278087748628374140593)]], [[25929636111738620343, (-460283986535143377027), 2031519016838061494689], [33373869314189116495, (-640437317036174497236)], [50269013157118187730]], [[(-497853491558030118), 7043021801502624613, (-27355709422764055333), (-25209996399536704429)], [(-492297615025161072), 9225093415085575053, (-42810189485227965152)], [(-727263429111907824), 14152913971158369526], [(-1131163620188946816)]], [[11285092313445187, (-136149942819868980), 403800047791982230, 731530606542645370, (-684180117182699264)], [9180393096235410, (-135179523427317402), 572497489503826737, 405536285239723215], [10546186105861551, (-201588539122198600), 951921011475609733], [16240872919555752, (-318738714292337282)], [25686608652034901]]], r := 435675490024654515, ok := true }, r1 := { p := [[[143988650773561784275267]], [[(-2168064229003459836297), 0], [(-2960917847612845263535)]], [[33363479697842137308, 0, 0], [43159432969998358658, 0], [65365429991389664389]], [[(-641874789258451252), 0, 0, 0], [(-635416396015539057), 0, 0], [(-941278175108253648), 0], [(-1471236653771059230)]], [[14585495057458570, 0, 0, 0, 0], [11870002913289047, 0, 0, 0], [13624238628563909, 0, 0], [21030059461838034, 0], [33414778235243968]]], r := 28715297925284518, ok := true }, r2 := { p := [[[419930230629631344718691309]], [[(-8567880980124654009439201), 35534356513674140316400], [(-18897746363276466356093512)]], [[193144856243173971513834, (-496677267140384700130), 448234446889591360], [378124824587229294184215, (-797042068062371394612)], [646198135540932159133421]], [[(-4804665628408117618533), 9410105227788052552, 155083807555047, (-17927742743336)], [(-8451522608704405729300), 10568586210359851096, 44098718446718], [(-12772357657477868943069), 18271718112125580275], [(-19756299508137881257352)]], [[124804189157686900072, (-217503047769292738), (-3592611580900), (-738836507022), (-574205204786)], [209758895676914771746, (-194429952613723767), (-1268863695207), (-4514134371143)], [283932174935688212770, (-236997239310687539), (-805603427786)], [387039085073140923763, (-421221395454406406)], [568123234689774426420]]], r := 1168445543100905867595, ok := true }, r3 := { p := [[[11837349056935431481983126388]], [[(-639830063217474791164067766), 1101668649319325711098098], [(-550573845632972321382655700)]], [[25938696424817646407081668, (-55848932374700968602897), 1467611823833529316], [29760129412795016255457235, (-25660157284024264040790)], [19206058856569062779554627]], [[(-934721305668635248779458), 2214349545411515230561, 14167168232981249, (-511967375022773)], [(-1206483364427860925694807), 1300474311703550098145, (-2103519925849106)], [(-1038150953208104634708107), 597089121347690434270], [(-595536627640515175055078)]], [[31578289010430471851626, (-78905650069159986969), (-2612008041275788), (-1715101558063985), (-241396712456641)], [43476725045483622451220, (-51556602822458351942), (-539335651440293), (-509691610369384)], [42087005829231740903706, (-30258404565455310446), (-1311259577341294)], [32190834205256248425143, (-13892141413501126938)], [17312109162642915968336]]], r := 356675645210770581135107, ok := true }, eta := { p := [[[(-420520566975983434612014281)]], [[8585327394203741828465606, 0], [18911255331615317847002416]], [[(-193619805292456442957355), 0, 0], [(-378523465465403898696288), 0], [(-646510367964651984811313)]], [[4817492511367301856820, 0, 0, 0], [8462370649198501659092, 0, 0], [12781566386174896657410, 0], [19763533902265917375482]], [[(-125150501122418452318), 0, 0, 0, 0], [(-210051877079111692422), 0, 0, 0], [(-284182742653441020485), 0, 0], [(-387252385586361502501), 0], [(-568291042511968370991)]]], r := 95891347591004995147, ok := true } }
theorem sB_1 : stageB c1 w1 = true := by decide +kernel
theorem s0_1 : stageC0 w1 q1 = true := by decide +kernel
theorem s1_1 : stageC1 w1 q1 = true := by decide +kernel
theorem s2_1 : stageC2 w1 q1 = true := by decide +kernel
theorem s3_1 : stageC3 w1 q1 = true := by decide +kernel
theorem sE_1 : stageE w1 q1 = true := by decide +kernel
theorem sF_1 : stageF w1 = true := by decide +kernel
theorem ok_1 : (domOK c1 && cellCheck c1 q1) = true :=
  staged_check c1 q1 w1 (by decide +kernel) sB_1 s0_1 s1_1 s2_1 s3_1 sE_1 sF_1

noncomputable def c2 : Cell := { bc := 5770237022568448, bh := 140737488355328, tc := 16140901064495857664, th := 2305843009213693952, sc := 2810246167479189504, sh := 72057594037927936 }
noncomputable def q2 : Cert := { V0 := [[[1754786288302640459]], [[(-14251196108969419), 247422488070453436], [4533832481501511]], [[57385303832379, (-1956613300825434), (-688140142451272)], [(-36898796572383), 622471045180342], [(-43645579456175)]], [[(-326608933430), 7238663943831, 16553742471260, (-30262244501191)], [165848661155, (-4658772145419), (-5266357625898)], [356242421057, (-6057083954352)], [644783521604]], [[2781514521, (-37995149130), (-196815531163), 687534007522, 258223738463], [(-1199914370), 16201073397, 125676988334, (-218729992320)], [(-1571450628), 46558046737, 37523840219], [(-5264357826), 89718056399], [(-11108901717)]]], r0 := 1317780366367, V1 := [[[2001490638064319585]], [[(-16190578552884788), 0], [5150821753913757]], [[64419995495695, 0, 0], [(-41427319735225), 0], [(-49663514232781)]], [[(-362817937735), 0, 0, 0], [180514096474, 0, 0], [401860407553, 0], [733974351788]], [[3088400973, 0, 0, 0, 0], [(-1287569229), 0, 0, 0], [(-1732001722), 0, 0], [(-5945463725), 0], [(-12648363025)]]], r1 := 252783432366, V2 := [[[18440327392813674060]], [[(-25910073255166), 237244844555], [(-155855377116162)]], [[27338782840, (-123968783), (-8369797)], [(-641126160040), 11617939364], [9669997991]], [[(-264384130), (-5461424), 42688, 290], [738625939, (-5571454), (-615579)], [(-136549141), 142901926], [(-59933745)]], [[3484938, 14384, 174, (-3), 0], [(-7139740), (-272413), 3120, 28], [1062215, (-54843), (-15139)], [844400, 12236], [653537]]], r2 := 975329628, V3 := [[[18444985826355852901]], [[(-45082704526436), 128269857626], [(-42887239012115)]], [[14831362, 2727938414, (-8973353)], [(-1099645444735), 6286188683], [(-77430452)]], [[5240, (-14833270), (-150802), 618], [725146, 133828064, (-659893)], [(-1652362), 77446674], [(-7698)]], [[(-51), (-5236), 1908, 7, 0], [281, (-725287), (-11106), 60], [8885, 1652635, (-16225)], [(-205), 7832], [35]]], r3 := 4328329132, Vm := [[[18440327720433217155]], [[(-25911135871752), 0], [(-155839078849001)]], [[27338205187, 0, 0], [(-641180030743), 0], [9877417813]], [[(-264419781), 0, 0, 0], [738601102, 0, 0], [(-137260795), 0], [(-59845409)]], [[3485549, 0, 0, 0, 0], [(-7141529), 0, 0, 0], [1061989, 0, 0], [843861, 0], [653150]]], rm := 119472230 }
noncomputable def w2 : Wit := { Z0 := { p := [[[1766333661309726578]], [[(-14534056762300362), 252333380187103796], [4623820915314687]], [[60852587190044, (-2076293823185766), 0], [(-39112600526234), 660545845044955], [(-44276217149389)]], [[(-358485705786), 8693226741434, 0, 0], [193503066985, (-5587514360891), 0], [371721507266, (-6325173878485)], [653258221007]], [[3063572185, (-51212243684), 0, 0, 0], [(-1465792096), 27643295283, 0, 0], [(-1762412860), 53103072466, 0], [(-5472231050), 93322603001], [(-11246685446)]]], r := 272223642335, ok := true }, Z1 := { p := [[[2018667041496830375]], [[(-16610350585486128), 0], [5284366760359642]], [[69545813931479, 0, 0], [(-44700114887124), 0], [(-50601391027874)]], [[(-409697949470), 0, 0, 0], [221146362269, 0, 0], [424824579733, 0], [746580824008]], [[3501225354, 0, 0, 0, 0], [(-1675190966), 0, 0, 0], [(-2014186126), 0, 0], [(-6253978343), 0], [(-12853354795)]]], r := 64780799685, ok := true }, Z2 := { p := [[[7610269212835353964687]], [[(-27557928087472439410), 252333380187103796], [(-165767623746747888202)]], [[135255999655114298, (-2076293823185766), 0], [595477703461433851, 660545845044955], [3852156849606374308]], [[(-921520740046541), 8693226741434, 0, 0], [(-2819224353768595), (-5587514360891), 0], [(-13800958443773281), (-6325173878485)], [(-91138642361029156)]], [[8954449200918, (-51212243684), 0, 0, 0], [18378445834435, 27643295283, 0, 0], [64494150557630, 53103072466, 0], [325996970570629, 93322603001], [2174410209782959]]], r := 152396217281537, ok := true }, Z3 := { p := [[[24496382049479165028552]], [[(-570809495526581250021), 1624074098746060092], [(-543011860583427329062)]], [[14035002243342804499, (-45324569054249799), 0], [12779641966152857827, 3617077820936745], [12700166220872627810]], [[(-350430062974402137), 1104798600831222, 0, 0], [(-315400256542353660), (-92474054312205), 0], [(-300013787571858206), (-36053832001202)], [(-301632744907034999)]], [[8813221989591990, (-27518653401252), 0, 0, 0], [7892679221588465, 2135414784375, 0, 0], [7415135428650442, 940644287393, 0], [7141410059644115, 538692993869], [7215930433744619]]], r := 9591878212485973, ok := true }, iE := { p := [[[7613265817078405423142]], [[(-27560636250043815141), 0], [(-165759779384339220690)]], [[135279779498335505, 0, 0], [595468805575793149, 0], [3852081734523033969]], [[(-921738903740373), 0, 0, 0], [(-2819117320193576), 0, 0], [(-13800878004523248), 0], [(-91137534101361259)]], [[8956989213904, 0, 0, 0, 0], [18377344063708, 0, 0, 0], [64493244295196, 0, 0], [325995804465170, 0], [2174391129658936]]], r := 152208400039037, ok := true }, iHu := { p := [[[24500341197858135838640]], [[(-570849352807500627497), 0], [(-543003042914453709069)]], [[14036049751156355609, 0, 0], [12779573848360180506, 0], [12700078329272956679]], [[(-350456681728456941), 0, 0, 0], [(-315398347794666692), 0, 0], [(-300013062537736769), 0], [(-301631431687708929)]], [[8813896889572281, 0, 0, 0, 0], [7892630976926369, 0, 0, 0], [7415115565279653, 0, 0], [7141398997172381, 0], [7215907655783302]]], r := 9587047347715994, ok := true }, T := { p := [[[16140901064495857664]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[44695978716203816]], [[161803047579615, 0], [973142899430273]], [[(-208460763729), 0, 0], [3549831902653, 0], [(-1427063123942)]], [[1781631020, 0, 0, 0], [(-5084651175), 0, 0], [(-4836619410), 0], [11598915629]], [[(-22841423), 0, 0, 0, 0], [43454415, 0, 0, 0], [(-5910), 0, 0], [39318361, 0], [(-141450201)]]], r := 70637287, ok := true }, de := { p := [[[(-132419740424462012457)]], [[341208903474040682, 0], [324564566719209429]], [[(-4374264650763886), 0, 0], [396602791649, 0], [(-3957915844028478)]], [[74773754883740, 0, 0, 0], [484631, 0, 0], [460990, 0], [64356355333623]], [[(-1437956824687), 0, 0, 0, 0], [1, 0, 0, 0], [5911, 0, 0], [1, 0], [(-1177250402444)]]], r := 269088920584, ok := true }, dde := { p := [[[(-279245632912542970680925)]], [[7159803208490759473163, 0], [6810544515393649251684]], [[(-183584698070570465249), 0, 0], [(-174629347341798495198), 0], [(-166110842216143764698)]], [[4707299950526960954, 0, 0, 0], [4477675562695388783, 0, 0], [4259252364515140176, 0], [4051483956490901154]], [[(-120699998731448533), 0, 0, 0, 0], [(-114812193915284778), 0, 0, 0], [(-109211599090151740), 0, 0], [(-103884204012584151), 0], [(-98816681865616595)]]], r := 16944032113163390, ok := true }, nJu := { p := [[[(-264839480848924024913)]], [[682417806948081364, 0], [649129133438418859]], [[(-8748529301527772), 0, 0], [793205583298, 0], [(-7915831688056955)]], [[149547509767481, 0, 0, 0], [969262, 0, 0], [921981, 0], [128712710667246]], [[(-2875913649373), 0, 0, 0, 0], [2, 0, 0, 0], [11823, 0, 0], [2, 0], [(-2354500804887)]]], r := 538177841160, ok := true }, Jd1 := { p := [[[(-558491265825085941361850)]], [[14319606416981518946327, 0], [13621089030787298503369]], [[(-367169396141140930497), 0, 0], [(-349258694683596990395), 0], [(-332221684432287529395)]], [[9414599901053921909, 0, 0, 0], [8955351125390777567, 0, 0], [8518504729030280353, 0], [8102967912981802308]], [[(-241399997462897065), 0, 0, 0, 0], [(-229624387830569555), 0, 0, 0], [(-218423198180303479), 0, 0], [(-207768408025168301), 0], [(-197633363731233189)]]], r := 33888064226326767, ok := true }, term0 := { p := [[[5862259220411382576490756440]], [[(-300607195148085815368627279), 0], [(-285898724418389589251556963)]], [[11561539820960571795559381, 0, 0], [14660949159059188167594746, 0], [10458915079375345721793479]], [[(-395261611365369098020035), 0, 0, 0], [(-563875943450364152948264), 0, 0], [(-536341841698053079256535), 0], [(-340114403385118400151173)]], [[12668550864916141668207, 0, 0, 0, 0], [19277695220296920104257, 0, 0, 0], [20628368555602764803964, 0, 0], [17441452623547768583341, 0], [10369105293398747463820]]], r := 3345677312917303669322, ok := true }, r0 := { p := [[[112316547917644740213350]], [[(-1648982337113662799517), 31444359968588767307491], [(-2422702000012183127618)]], [[24115933413327227781, (-451876122438773242345), 2065638950535376819873], [34453821086049783530, (-681510855226420941991)], [56100985840877350380]], [[(-433764593026057146), 6548483406224456671, (-26965357676763444008), (-24594402361064603687)], [(-482355013783945206), 9529850634236513579, (-45673341422357283256)], [(-788428646544350833), 15803622984609082352], [(-1324443022289385599)]], [[9224707776088822, (-118490341761449146), 374786609040761990, 705651626335557421, (-676124480567405687)], [8417692124084218, (-132405797867256494), 593134384741651502, 415830700133976820], [10855001519505517, (-218674360918171253), 1065411180016382704], [18479934831187308, (-373395177896731193)], [31550552874799801]]], r := 451124118810047581, ok := true }, r1 := { p := [[[145801292378048135963622]], [[(-2127102677659661743318), 0], [(-3149458091688062852729)]], [[31027012145521715036, 0, 0], [44564596280593668894, 0], [72960959008500652156]], [[(-559062369363813514), 0, 0, 0], [(-622521310486185129), 0, 0], [(-1020623448184323373), 0], [(-1722893145498577917)]], [[11919221959212816, 0, 0, 0, 0], [10880449482970474, 0, 0, 0], [14021878424327176, 0, 0], [23933420554851228, 0], [41049115786051990]]], r := 33258506226936295, ok := true }, r2 := { p := [[[442526246998084207342429044]], [[(-8592431902683373263699706), 36204985464663365160451], [(-20907625117206195740666401)]], [[182739713158678754028230, (-482090244273435353009), 448447576505247949], [398144909987532398517870, (-853157715934251803791)], [750268036937468701561062]], [[(-4292613119118735988485), 8581886830567353651, 145050583937518, (-17911680952001)], [(-8392244187567943592473), 10788713017738322493, 49430672022506], [(-14114171135721110797344), 20525888420078424784], [(-24067634777150417147873)]], [[105510071958821648849, (-186576977988482100), (-6755482415175), (-831279215676), (-666653452796)], [196636046405059363968, (-186337110986778205), (-3330324479504), (-1245988661056)], [295820735438783829624, (-254024349841813086), (-4386207997367)], [448780678019935113246, (-496471725286089944)], [726111001161121183528]]], r := 1367764437582017043648, ok := true }, r3 := { p := [[[11719247092309602206442188674]], [[(-600961882239697513527726558), 1047009885439144968503169], [(-571668840661288494669544976)]], [[23113596011440181109372501, (-50197734733896957171756), 1500140690173389404], [29315738013278804985886088, (-25576861915416027283589)], [20914693011832785107082027]], [[(-790202895063700304438560), 1886046477600845972056, 12610484518097802, (-495575112983416)], [(-1127520525647366600226587), 1225905628035581582497, (-1680038461625468)], [(-1072533418284934430146429), 624184581968147996607], [(-680152286938156844178696)]], [[25326909636173008121492, (-63722508415933145633), (-2397412060335144), (-1783527792232414), (-237826631102197)], [38547575120695538462514, (-46054712166825752957), (-1738748989590252), (-650716987648276)], [41251092584528309109644, (-29914465501456163920), (-1376115450900580)], [34879238201881378916093, (-15229969721556698150)], [20736343086740112241846]]], r := 343072682717452488369122, ok := true }, eta := { p := [[[(-443110235024580818363516719)]], [[8608873856761115910504252, 0], [20921644374549776294366355]], [[(-183164746411942058465863), 0, 0], [(-398539019325688719593992), 0], [(-750607899962512812901205)]], [[4303504517990558988773, 0, 0, 0], [8402427710406342854271, 0, 0], [14123720008952245451857, 0], [24075893918695866871820]], [[(-105789042282738690035), 0, 0, 0, 0], [(-196897003341080885409), 0, 0, 0], [(-296067440682957873331), 0, 0], [(-449012652352474891914), 0], [(-726311928706120881683)]]], r := 114919471123966158685, ok := true } }
theorem sB_2 : stageB c2 w2 = true := by decide +kernel
theorem s0_2 : stageC0 w2 q2 = true := by decide +kernel
theorem s1_2 : stageC1 w2 q2 = true := by decide +kernel
theorem s2_2 : stageC2 w2 q2 = true := by decide +kernel
theorem s3_2 : stageC3 w2 q2 = true := by decide +kernel
theorem sE_2 : stageE w2 q2 = true := by decide +kernel
theorem sF_2 : stageF w2 = true := by decide +kernel
theorem ok_2 : (domOK c2 && cellCheck c2 q2) = true :=
  staged_check c2 q2 w2 (by decide +kernel) sB_2 s0_2 s1_2 s2_2 s3_2 sE_2 sF_2

noncomputable def c3 : Cell := { bc := 6051711999279104, bh := 140737488355328, tc := 16140901064495857664, th := 2305843009213693952, sc := 2810246167479189504, sh := 72057594037927936 }
noncomputable def q3 : Cert := { V0 := [[[1763684357865101719]], [[(-14323609448136430), 248643895692273165], [4366647939387353]], [[57710893664515, (-1965749977901266), (-698526676882143)], [(-35534225981866), 599272000638781], [(-40027812118243)]], [[(-328966625154), 7270399141566, 16801576553459, (-30693312763733)], [159827386437, (-4480498132898), (-5122072749979)], [326705257236, (-5553741565830)], [563606212420]], [[2805985068, (-38193671251), (-199758785618), 696791895509, 264662226700], [(-1158362444), 15543782903, 122202773817, (-212421659900)], [(-1442074927), 42666638479, 34678867182], [(-4601511011), 78406879585], [(-9256461534)]]], r0 := 1144770036468, V1 := [[[2011599304214560449]], [[(-16271871733229964), 0], [4960588700156743]], [[64774292812255, 0, 0], [(-39888089652038), 0], [(-45545373504260)]], [[(-365347189607), 0, 0, 0], [173878528635, 0, 0], [368503183429, 0], [641548814973]], [[3114842549, 0, 0, 0, 0], [(-1242322090), 0, 0, 0], [(-1588980668), 0, 0], [(-5196389812), 0], [(-10538921594)]]], r1 := 206804224964, V2 := [[[18440015720270143287]], [[(-27192865160532), 261052428008], [(-155817396104436)]], [[28820231558, (-135329992), (-9662514)], [(-641662509745), 12189692172], [9325398062]], [[(-278703913), (-6020207), 49238, 351], [742797322, (-5789223), (-677640)], [(-131694845), 142974053], [(-55041585)]], [[3673933, 15912, 202, (-3), 0], [(-7179797), (-286377), 3432, 33], [1024022, (-54046), (-15892)], [775238, 11812], [571966]]], r2 := 833773900, V3 := [[[18444900051568045841]], [[(-47282002026980), 141152083788], [(-42887548825183)]], [[16317200, 3002206730, (-10359114)], [(-1099652056616), 6596068253], [(-77475809)]], [[5819, (-16319403), (-174128), 748], [760693, 140441067, (-726405)], [(-1653572), 77492837], [(-7425)]], [[(-56), (-5815), 2203, 9, 0], [298, (-760848), (-12229), 70], [8888, 1653859, (-17031)], [(-198), 7559], [32]]], r3 := 4036385135, Vm := [[[18440016081316600588]], [[(-27194038369410), 0], [(-155800267110088)]], [[28819603330, 0, 0], [(-641719233450), 0], [9533338862]], [[(-278743234), 0, 0, 0], [742771585, 0, 0], [(-132409673), 0], [(-54956221)]], [[3674607, 0, 0, 0, 0], [(-7181678), 0, 0, 0], [1023798, 0, 0], [774719, 0], [571609]]], rm := 103240117 }
noncomputable def w3 : Wit := { Z0 := { p := [[[1775409250858239868]], [[(-14610837403829549), 253629892979748552], [4454211298707025]], [[61232741805849, (-2087262486261365), 0], [(-37688504595702), 636315899815289], [(-40610721519656)]], [[(-361368216781), 8747534543692, 0, 0], [186747365222, (-5384072085101), 0], [341013602025, (-5801531645666)], [571070407274]], [[3093029108, (-51624030969), 0, 0, 0], [(-1417392953), 26678195031, 0, 0], [(-1618630425), 48716228860, 0], [(-4784607155), 81581486753], [(-9372125288)]]], r := 228329051338, ok := true }, Z1 := { p := [[[2029039143837988420]], [[(-16698099890090913), 0], [5090527198522314]], [[69980276349542, 0, 0], [(-43072576680802), 0], [(-46412253165321)]], [[(-412992247749), 0, 0, 0], [213425560254, 0, 0], [389729830886, 0], [652651894027]], [[3534890409, 0, 0, 0, 0], [(-1619877661), 0, 0, 0], [(-1849863343), 0, 0], [(-5468122463), 0], [(-10711000329)]]], r := 53008381832, ok := true }, Z2 := { p := [[[7293446682582683803615]], [[(-26419687160500416347), 253629892979748552], [(-151387021372720836127)]], [[129863982335060164, (-2087262486261365), 0], [543951300137793040, 636315899815289], [3353622326923936113]], [[(-886344609431445), 8747534543692, 0, 0], [(-2578304486502611), (-5384072085101), 0], [(-12017550297566702), (-5801531645666)], [(-75643636365206420)]], [[8623405574884, (-51624030969), 0, 0, 0], [16832687240617, 26678195031, 0, 0], [56220929755604, 48716228860, 0], [270629181058310, 81581486753], [1720630766868461]]], r := 119686164415289, ok := true }, Z3 := { p := [[[23458856093815588489224]], [[(-546395747634322627338), 1631168204505303042], [(-495612988028037550032)]], [[13432513619084450524, (-45505863975496809), 0], [11660119328439449855, 3479041209809088], [11050622529424048243]], [[(-335353803156560840), 1108984131551807, 0, 0], [(-287731848792992972), (-88873730864770), 0], [(-260965096202344374), (-33032674800471)], [(-250223603422492938)]], [[8433469560165924, (-27619890036357), 0, 0, 0], [7199705785890487, 2051355045313, 0, 0], [6449205860299389, 861315350682, 0], [5922498580393469, 470443608205], [5707254065749671]]], r := 8158502712795132, ok := true }, iE := { p := [[[7296458683661987084814]], [[(-26422412806108407195), 0], [(-151379464754869112621)]], [[129887972719886321, 0, 0], [543942710623448005, 0], [3353553430393747731]], [[(-886564941234090), 0, 0, 0], [(-2578200930329080), 0, 0], [(-12017476405999576), 0], [(-75642667538057278)]], [[8625972287114, 0, 0, 0, 0], [16831620422403, 0, 0, 0], [56220095736895, 0, 0], [270628160222404, 0], [1720614866956107]]], r := 119527619551617, ok := true }, iHu := { p := [[[23462832536120580679591]], [[(-546435738336195938397), 0], [(-495604506863060642162)]], [[13433564867268271341, 0, 0], [11660053983968565563, 0], [11050542002765202856]], [[(-335380516450222355), 0, 0, 0], [(-287730016045379915), 0, 0], [(-260964433158850999), 0], [(-250222456580701505)]], [[8434146832862387, 0, 0, 0, 0], [7199659462500425, 0, 0, 0], [6449187685183907, 0, 0], [5922488935656128, 0], [5707235102512160]]], r := 8154097306412366, ok := true }, T := { p := [[[16140901064495857664]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[46636646854848723]], [[168883671999779, 0], [967569466905502]], [[(-218630089719), 0, 0], [3530942441900, 0], [(-1360706537140)]], [[1868539850, 0, 0, 0], [(-5084674815), 0, 0], [(-4611681809), 0], [10545038943]], [[(-23955639), 0, 0, 0, 0], [43454415, 0, 0, 0], [(-5910), 0, 0], [35745898, 0], [(-122616742)]]], r := 61187720, ok := true }, de := { p := [[[(-131785946233182195422)]], [[341209696681467940, 0], [309469259780866271]], [[(-4374264649770982), 0, 0], [396604635613, 0], [(-3598299909303225)]], [[74773754883741, 0, 0, 0], [508274, 0, 0], [460993, 0], [55787595632443]], [[(-1437956824687), 0, 0, 0, 0], [1, 0, 0, 0], [5911, 0, 0], [1, 0], [(-973039458705)]]], r := 244034304966, ok := true }, dde := { p := [[[(-266258082907882363461184)]], [[6826789104220661872187, 0], [6191738954990832844083]], [[(-175045874904500333071), 0, 0], [(-158762538100706169949), 0], [(-143993929545562466928)]], [[4488355766781523429, 0, 0, 0], [4070834300103147537, 0, 0], [3692152039628444802, 0], [3348696035942909732]], [[(-115086045302078899), 0, 0, 0, 0], [(-104380366669327867), 0, 0, 0], [(-94670565118694054), 0, 0], [(-85864000921610260), 0], [(-77876651998670300)]]], r := 14481134821202922, ok := true }, nJu := { p := [[[(-263571892466364390843)]], [[682419393362935880, 0], [618938519561732542]], [[(-8748529299541963), 0, 0], [793209271227, 0], [(-7196599818606450)]], [[149547509767482, 0, 0, 0], [1016549, 0, 0], [921987, 0], [111575191264886]], [[(-2875913649373), 0, 0, 0, 0], [2, 0, 0, 0], [11823, 0, 0], [2, 0], [(-1946078917410)]]], r := 488068609925, ok := true }, Jd1 := { p := [[[(-532516165815764726922368)]], [[13653578208441323744374, 0], [12383477909981665688167]], [[(-350091749809000666142), 0, 0], [(-317525076201412339898), 0], [(-287987859091124933855)]], [[8976711533563046858, 0, 0, 0], [8141668600206295074, 0, 0], [7384304079256889605, 0], [6697392071885819465]], [[(-230172090604157797), 0, 0, 0, 0], [(-208760733338655733), 0, 0, 0], [(-189341130237388107), 0, 0], [(-171728001843220520), 0], [(-155753303997340600)]]], r := 28962269642405836, ok := true }, term0 := { p := [[[5329733234413471435834930356]], [[(-273299169267420201153811743), 0], [(-247835347521365286668736250)]], [[10511243941477626397563765, 0, 0], [12709028713485665139335252, 0], [8644730513227353406552139]], [[(-359354278874238485135991), 0, 0, 0], [(-488802690420969155493583), 0, 0], [(-443308437042720591841422), 0], [(-268042983567431835508158)]], [[11517679033998868341436, 0, 0, 0, 0], [16711098710948159538075, 0, 0, 0], [17050182495794664615222, 0, 0], [13745536437096210667911, 0], [7791760991655832829901]]], r := 2719500581048074517125, ok := true }, r0 := { p := [[[107685434058114769238466]], [[(-1583087258717159617519), 30141701476162279451931], [(-2213238895364373697977)]], [[23192719361211199731, (-433651910402371733377), 1978361065967457663947], [31508640596628573516, (-622508435904092896737)], [48855181743773882356]], [[(-417645084180224059), 6295096464472881305, (-25831715423755882243), (-23796425314677635553)], [(-441777855275312072), 8713077886888671721, (-41696571214508119144)], [(-687281087320562510), 13760943369143001324], [(-1099581348120084779)]], [[8886124908173502, (-114043287930682810), 359555671667885392, 682814720358030392, (-652206980659813376)], [7717553109862631, (-121234550052911254), 541694900023416096, 382864775859383385], [9475798751815377, (-190579421896666349), 927268478209527505], [15357047832483242, (-309968928546383705)], [24973155407948278]]], r := 399173036732377916, ok := true }, r1 := { p := [[[139781063655598780785873]], [[(-2041873176701948229186), 0], [(-2877049753165232497789)]], [[29835570441932949143, 0, 0], [40752170424602167915, 0], [63535443667546645121]], [[(-538227491741876669), 0, 0, 0], [(-570107842788168031), 0, 0], [(-889630713733497693), 0], [(-1430339065629969109)]], [[11480625130327965, 0, 0, 0, 0], [9974792890835261, 0, 0, 0], [12239440005243995, 0, 0], [19887782895629782, 0], [32490590995430530]]], r := 26438918805709827, ok := true }, r2 := { p := [[[403530507382005906019638971]], [[(-7849211908527691831791808), 34576985535264636028285], [(-18173707500096630894428891)]], [[167067802744656141817604, (-461482634049169811822), 448544917104025767], [346672384256777800309170, (-776648661296490664823)], [621735631067641426105362]], [[(-3925369389563339865587), 8225756769963576499, 150264238252959, (-18244976912720)], [(-7313018218805520389529), 9840969392242370177, 45438757832511], [(-11715587506598303043237), 17814196303997475036], [(-19014887254691648605290)]], [[96487768649544454863, (-178909847712630688), (-4140451585930), (-704600884580), (-555939497389)], [171387045663779368283, (-170172125426614357), (-1418303967203), (-4285628776259)], [245738089900035371817, (-220885823171782204), (-3951670763732)], [355140235272622832328, (-410813122844884361)], [546947328704124893177]]], r := 1044347724255430262146, ok := true }, r3 := { p := [[[10654440371778552973726600219]], [[(-546357577982743152175581891), 998236744564123804509354], [(-495553773483574729796291670)]], [[21013445451929348899484680, (-47860012236916262189963), 1497799567612883949], [25412456896463733826757085, (-23251662073182520636534)], [17286741603630315334989034]], [[(-718403131996653563519448), 1798223581676763895589, 12709898663843895, (-1348806298182763)], [(-977395043075287403867277), 1114469162211653516991, (-2037248624380347)], [(-886486617751639510018182), 541051348015757169211], [(-536022720754950391042525)]], [[23025639709140173097107, (-60754572830614585032), (-2049679027279444), (-1339294197570282), (-200355314734174)], [33415092165574429992853, (-41869507901934178526), (-1056323254691488), (-264514747420208)], [34095472689633888222293, (-25931800031673430832), (-1068683141320090)], [27488043040728858663272, (-12588497963861196630)], [15582049913616497729619]]], r := 276013480754804249703728, ok := true }, eta := { p := [[[(-404087753338303881113205457)]], [[7864902069727895212630902, 0], [18186460355108647637204148]], [[(-167473410050296478266898), 0, 0], [(-347030911614931603909006), 0], [(-622030396917297534840301)]], [[3935762998617295482269, 0, 0, 0], [7322282440495953109824, 0, 0], [11723869710222757241646, 0], [19021717081847773454382]], [[(-96753989742528414952), 0, 0, 0, 0], [(-171624441909977179532), 0, 0, 0], [(-245952071154086939667), 0, 0], [(-355332073425730403937), 0], [(-547105753982797751387)]]], r := 87509099618611066172, ok := true } }
theorem sB_3 : stageB c3 w3 = true := by decide +kernel
theorem s0_3 : stageC0 w3 q3 = true := by decide +kernel
theorem s1_3 : stageC1 w3 q3 = true := by decide +kernel
theorem s2_3 : stageC2 w3 q3 = true := by decide +kernel
theorem s3_3 : stageC3 w3 q3 = true := by decide +kernel
theorem sE_3 : stageE w3 q3 = true := by decide +kernel
theorem sF_3 : stageF w3 = true := by decide +kernel
theorem ok_3 : (domOK c3 && cellCheck c3 q3) = true :=
  staged_check c3 q3 w3 (by decide +kernel) sB_3 s0_3 s1_3 s2_3 s3_3 sE_3 sF_3

noncomputable def c4 : Cell := { bc := 6473924464345088, bh := 281474976710656, tc := 16140901064495857664, th := 2305843009213693952, sc := 2666130979403333632, sh := 72057594037927936 }
noncomputable def q4 : Cert := { V0 := [[[1805528754429415625]], [[(-14664183920422706), 254380967851205647], [8417516428389511]], [[60243128550742, (-2008558303688880), (-748744902710433)], [(-68621863145343), 1152950113721154], [(-143989644047561)]], [[(-356553129923), 7554739600280, 17999139399648, (-32768545638986)], [317173054253, (-8599227838907), (-10331843382190)], [1177018947148, (-19951899024217)], [3788239101443]], [[3219963256, (-41272556728), (-215199716556), 741166197856, 296645792560], [(-2400752377), 30467823484, 246395139417, (-425443289617)], [(-5328814674), 153094873376, 130192535091], [(-30971672811), 526383111644], [(-116278713498)]]], r0 := 11191872635591, V1 := [[[2059128512101382937]], [[(-16654013864344281), 0], [9559716112569307]], [[67574977522109, 0, 0], [(-76965893217719), 0], [(-163805737259223)]], [[(-395841552422), 0, 0, 0], [344613924616, 0, 0], [1326854238942, 0], [4311366998035]], [[3575619805, 0, 0, 0, 0], [(-2574526150), 0, 0, 0], [(-5866554862), 0, 0], [(-34957838084), 0], [(-132367003097)]]], r1 := 3521464287417, V2 := [[[18439606715302921170]], [[(-29246984157507), 299187153168], [(-308949902321961)]], [[32959873771, (-125309497), (-11961369)], [(-1291035483336), 26117667255], [36452984377]], [[(-334645734), (-7026627), 59247, 469], [1589250037, (-9739893), (-1568328)], [(-516533002), 572677592], [(-401514383)]], [[4643587, 20286, 261, (-4), 0], [(-16130580), (-625465), 7716, 82], [4126165, (-154913), (-68763)], [5673502, 87863], [7795235]]], r2 := 14775186387, V3 := [[[18444872550244920691]], [[(-50581047718224), 154686412689], [(-81377373313960)]], [[18637148, 3513064842, (-12257473)], [(-2199330470897), 13514465335], [(-296779139)]], [[7306, (-18639882), (-224328), 956], [1624029, 307244795, (-1606966)], [(-6763291), 296849568], [(-53416)]], [[(-75), (-7301), 2734, 13, 0], [698, (-1624387), (-29452), 167], [35458, 6764584, (-70441)], [(-1519), 54455], [439]]], r3 := 26897282728, Vm := [[[18439607132307304394]], [[(-29248331722977), 0], [(-308912900585910)]], [[32959457083, 0, 0], [(-1291157370474), 0], [37293499093]], [[(-334697682), 0, 0, 0], [1589221908, 0, 0], [(-519408165), 0], [(-400855768)]], [[4644511, 0, 0, 0, 0], [(-16135230), 0, 0, 0], [4125880, 0, 0], [5669544, 0], [7790112]]], rm := 1885999537 }
noncomputable def w4 : Wit := { Z0 := { p := [[[1818113091848898843]], [[(-14972562605163955), 259730441692699834], [8594531573525512]], [[64050501137376, (-2138937515023423), 0], [(-72981524109392), 1227790224789358], [(-146180569424699)]], [[(-392196361868), 9150071591053, 0, 0], [372123588313, (-10425932015628), 0], [1230825761008, (-20882938489243)], [3840640374492]], [[3546171952, (-56028051696), 0, 0, 0], [(-2940342615), 53160512616, 0, 0], [(-5997563429), 175832251572, 0], [(-32257594831), 548662910641], [(-117795901068)]]], r := 2741322040674, ok := true }, Z1 := { p := [[[2077843533541598678]], [[(-17111500120187377), 0], [9822321798314871]], [[73200572728430, 0, 0], [(-83407456125019), 0], [(-167063507913941)]], [[(-448224413564), 0, 0, 0], [425284100929, 0, 0], [1406658012580, 0], [4389303285133]], [[4052767945, 0, 0, 0, 0], [(-3360391560), 0, 0, 0], [(-6854358205), 0, 0], [(-36865822664), 0], [(-134623886935)]]], r := 904009836482, ok := true }, Z2 := { p := [[[6917831829784257108597]], [[(-25389900712509644532), 259730441692699834], [(-268205682433777002773)]], [[127841787764653416, (-2138937515023423), 0], [975625449717370103, 1227790224789358], [11104281933095520167]], [[(-908828081822534), 9150071591053, 0, 0], [(-4729544951695863), (-10425932015628), 0], [(-40273623584595197), (-20882938489243)], [(-468170790987153197)]], [[9344902624830, (-56028051696), 0, 0, 0], [32124943571263, 53160512616, 0, 0], [192587717468678, 175832251572, 0], [1694987149846351, 548662910641], [19906764932743009]]], r := 1771877045610547, ok := true }, Z3 := { p := [[[23145527194749764107821]], [[(-568161047331069338133), 1737543965700690246], [(-914086515342237391753)]], [[14721838482799520949, (-50581898076684496), 0], [22665428419908668024, 6937886659520364], [38102157757343149534]], [[(-387398093286189728), 1299811260480669, 0, 0], [(-589513180981146643), (-184744625186701), 0], [(-948343401473467327), (-123117320973424)], [(-1612940252915037485)]], [[10268664111530982, (-34125468545391), 0, 0, 0], [15547913112346035, 4498657599560, 0, 0], [24702189848831203, 3347296211437, 0], [40236263688313238, 3277777355575], [68777811776622088]]], r := 51311956948455063, ok := true }, iE := { p := [[[6920871506140688111687]], [[(-25392751431243549230), 0], [(-268191313363703326393)]], [[127867488002775801, 0, 0], [975608289616416446, 0], [11104037535966077570]], [[(-909073968385253), 0, 0, 0], [(-4729334409372701), 0, 0], [(-40273349245043081), 0], [(-468164369877381622)]], [[9347917796547, 0, 0, 0, 0], [32122688230923, 0, 0, 0], [192584563132164, 0, 0], [1694980076157814, 0], [19906567991520285]]], r := 1770197079280790, ok := true }, iHu := { p := [[[23149613199965909566621]], [[(-568205800137158115413), 0], [(-914070200220640802767)]], [[14723073992874963763, 0, 0], [22665290231991965197, 0], [38101868234876020251]], [[(-387431154598527941), 0, 0, 0], [(-589509138020549548), 0, 0], [(-948340787255042910), 0], [(-1612932544899794922)]], [[10269547249282761, 0, 0, 0, 0], [15547805634142366, 0, 0, 0], [24702114948298807, 0, 0], [40236192656481958, 0], [68777573508508727]]], r := 51287971078762929, ok := true }, T := { p := [[[16140901064495857664]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[49167560273155745]], [[180396303469754, 0], [1905296544350932]], [[(-246525878817), 0, 0], [7050147323357, 0], [(-5053475160919)]], [[2220841203, 0, 0, 0], [(-10719060179), 0, 0], [(-17243705504), 0], [73215835197]], [[(-30011367), 0, 0, 0, 0], [96558313, 0, 0, 0], [(-23641), 0, 0], [249883422, 0], [(-1591648762)]]], r := 1177745316, ok := true }, de := { p := [[[(-131589032561460196361)]], [[359653732045960208, 0], [578573395030457725]], [[(-4859939029804530), 0, 0], [793210453261, 0], [(-12577044483558415)]], [[87566469230819, 0, 0, 0], [1087473, 0, 0], [1749413, 0], [364552014954277]], [[(-1774995997922), 0, 0, 0, 0], [2, 0, 0, 0], [23644, 0, 0], [4, 0], [(-11887565705029)]]], r := 2358597364223, ok := true }, dde := { p := [[[(-262347319467008535699398)]], [[7090108421727047021976, 0], [11405826591473945207051]], [[(-191624552431670591048), 0, 0], [(-308265585139851243463), 0], [(-495905505253226973396)]], [[5179041957612053895, 0, 0, 0], [8331502279634606180, 0, 0], [13402851493325211583, 0], [21561108924050556236]], [[(-139974106962482387), 0, 0, 0, 0], [(-225175737287478211), 0, 0, 0], [(-362239229549459461), 0, 0], [(-582732673622987407), 0], [(-937439518436968952)]]], r := 106243618552025572, ok := true }, nJu := { p := [[[(-263178065122920392721)]], [[719307464091920417, 0], [1157146790060915450]], [[(-9719878059609060), 0, 0], [1586420906522, 0], [(-25154088967116830)]], [[175132938461639, 0, 0, 0], [2174947, 0, 0], [3498827, 0], [729104029908554]], [[(-3549991995843), 0, 0, 0, 0], [5, 0, 0, 0], [47289, 0, 0], [9, 0], [(-23775131410058)]]], r := 4717194728436, ok := true }, Jd1 := { p := [[[(-524694638934017071398796)]], [[14180216843454094043952, 0], [22811653182947890414102]], [[(-383249104863341182096), 0, 0], [(-616531170279702486926), 0], [(-991811010506453946791)]], [[10358083915224107790, 0, 0, 0], [16663004559269212361, 0, 0], [26805702986650423167, 0], [43122217848101112472]], [[(-279948213924964773), 0, 0, 0, 0], [(-450351474574956421), 0, 0, 0], [(-724478459098918921), 0, 0], [(-1165465347245974814), 0], [(-1874879036873937904)]]], r := 212487237104051137, ok := true }, term0 := { p := [[[5174440430278550767742417556]], [[(-279678208795954050391627830), 0], [(-449838202508449466888950374)]], [[11338018325174665792304115, 0, 0], [24314653717222881614692569, 0], [29334814653389136245889918]], [[(-408572057901274003784059), 0, 0, 0], [(-985716707498634997795657), 0, 0], [(-1585625448385473376833310), 0], [(-1700497677783457372797527)]], [[13803005083651797413354, 0, 0, 0, 0], [35521097617006253023156, 0, 0, 0], [64281569413539267339371, 0, 0], [91917045195679507189434, 0], [92416027456804645027135]]], r := 18544750514481302786966, ok := true }, r0 := { p := [[[104537433469718384517685]], [[(-1587184817728883581332), 29233146444189201032151], [(-4008920572518897635373)]], [[24541763164143221591, (-434308991670894565546), 1911112012280291393862], [58824594167424240120, (-1126811001827980534542)], [165328710819152338300]], [[(-471954262752258098), 6661998921167010052, (-25745017869888635195), (-24062548571325313596)], [(-869585148983197483), 16254322841386241434, (-75261607074640673538)], [(-2395451165387570821), 46539525871790009927], [(-6953848046151089762)]], [[10704529691566886, (-128997609539083556), 380863484929618699, 698349815965721588, (-650058903615078120)], [16238982570695493, (-238687503456529894), 1007096167937142773, 721616677160600708], [34808051618430516, (-663782441171929368), 3128065905711576717], [99983671091577501, (-1959154227284133682)], [295178698914528546]]], r := 2002002692325829146, ok := true }, r1 := { p := [[[135656995848489267416120]], [[(-2046525650570360785103), 0], [(-5210250487171610725036)]], [[31572228387161181213, 0, 0], [76064608055293414031, 0], [214968321424658080092]], [[(-608389345232819176), 0, 0, 0], [(-1122262593026855668), 0, 0], [(-3100083998164704881), 0], [(-9044039940616139493)]], [[13833250783215819, 0, 0, 0, 0], [20994583280902493, 0, 0, 0], [44962816441347664, 0, 0], [129456270676161650, 0], [383970765632335917]]], r := 403061039576839246, ok := true }, r2 := { p := [[[368561839439965492370989587]], [[(-7538834583992659273445278), 33297040247122037300430], [(-30996841450323381508459278)]], [[170132547257225203658952, (-466968309224563232409), 448367421551787890], [621718545075802991481134, (-1395634939169755977895)], [1981157156536579609462315]], [[(-4233442557827317897793), 8863109760544269600, 161658706949305, (-19755190298498)], [(-13910878799479118169612), 18559701001748390268, 83944286293486], [(-39250745736646576219623), 59805557754598583177], [(-113222997220046612804956)]], [[109972089678029595895, (-204968987743774651), (-4627608632705), (-599759464918), (-451565758472)], [345352709577732320707, (-342004465520245364), 1593106225565, (-1335517251674)], [873464846254286589642, (-777857016749978121), (-1550391548551)], [2223248743067274174670, (-2577328498460199674)], [6086444371411190698253]]], r := 13332561996280464489150, ok := true }, r3 := { p := [[[10343696290889972226853221152]], [[(-559093811784726774229603290), 1029711425701025353726312], [(-899450920253380237824283515)]], [[22665628619568524822977859, (-52202065257920549275625), 1465282643406303850], [48617886834060533236531068, (-44841129723660702077512)], [58659824479912585356898054]], [[(-816773338219335687387899), 2069772394736057683847, 15443046727602192, (-1017049871185699)], [(-1970980786984509138097029), 2272608906989975653640, (-3325946020691342)], [(-3170754300848708202286446), 1950753869796987308303], [(-3400569031081541058045781)]], [[27593569089137772749672, (-73753828885504951916), (-1113544697674786), (-1162648640871507), (-188685107021722)], [71026069797865819703939, (-90096830151918344652), (-1203328865465920), 108343278026335], [128543457531236526912205, (-98858013271040165301), (-45521661075001)], [183812496891561649019016, (-84845093089681456223)], [184813517995765124554411]]], r := 1978056566970018824984825, ok := true }, eta := { p := [[[(-369114276351765049472584474)]], [[7555162569604167301199716, 0], [31020469920452589433247973]], [[(-170577060756022944046939), 0, 0], [(-622415857435345458226097), 0], [(-1982178087733745611792239)]], [[4245447454124088502632, 0, 0, 0], [13929854760238083828737, 0, 0], [39280858232600608074894, 0], [113267219497492346654610]], [[(-110296205368418660388), 0, 0, 0, 0], [(-345865205418382052700), 0, 0, 0], [(-874284201632791185778), 0, 0], [(-2224552660677863285107), 0], [(-6088362024750919070495)]]], r := 1163488934853394096358, ok := true } }
theorem sB_4 : stageB c4 w4 = true := by decide +kernel
theorem s0_4 : stageC0 w4 q4 = true := by decide +kernel
theorem s1_4 : stageC1 w4 q4 = true := by decide +kernel
theorem s2_4 : stageC2 w4 q4 = true := by decide +kernel
theorem s3_4 : stageC3 w4 q4 = true := by decide +kernel
theorem sE_4 : stageE w4 q4 = true := by decide +kernel
theorem sF_4 : stageF w4 = true := by decide +kernel
theorem ok_4 : (domOK c4 && cellCheck c4 q4) = true :=
  staged_check c4 q4 w4 (by decide +kernel) sB_4 s0_4 s1_4 s2_4 s3_4 sE_4 sF_4

noncomputable def c5 : Cell := { bc := 6473924464345088, bh := 281474976710656, tc := 16140901064495857664, th := 2305843009213693952, sc := 2810246167479189504, sh := 72057594037927936 }
noncomputable def q5 : Cert := { V0 := [[[1776438556908294087]], [[(-14427390207190613), 250393745834192939], [8281522597867826]], [[58177916149110, (-1978823066486360), (-713592265405047)], [(-67381166397728), 1135871956531768], [(-141656620743465)]], [[(-332355610425), 7315673377643, 17160946391054, (-31317439828939)], [303371819752, (-8479697745911), (-9850621858658)], [1156151626449, (-19647986848535)], [3726844442077]], [[2841217390, (-38477003392), (-204025682272), 710170408369, 274109502308], [(-2204165002), 29314958342, 234930491735, (-407647689624)], [(-5107869502), 150831702999, 124072597744], [(-30426767104), 518315483251], [(-114394067151)]]], r0 := 10980176842664, V1 := [[[2026087673321374295]], [[(-16388353208010942), 0], [9407142628355556]], [[65282201193758, 0, 0], [(-75617452470990), 0], [(-161175167668684)]], [[(-368980424992), 0, 0, 0], [329818758828, 0, 0], [1303875660894, 0], [4242057412514]], [[3152891766, 0, 0, 0, 0], [(-2362120075), 0, 0, 0], [(-5626045659), 0, 0], [(-34355877877), 0], [(-130237916675)]]], r1 := 3453600145846, V2 := [[[18439548350568886114]], [[(-29119017642276), 298908585917], [(-311525741860697)]], [[31057680048, (-153180585), (-11841847)], [(-1284865159991), 26095700200], [35436098762]], [[(-300330257), (-6910843), 60267, 461], [1497566750, (-12220047), (-1552758)], [(-500510349), 572310917], [(-390347168)]], [[3959388, 18358, 248, (-4), 0], [(-14474534), (-614790), 7853, 80], [3889493, (-211588), (-68088)], [5495475, 89908], [7577642]]], r2 := 14817375283, V3 := [[[18444771388224090130]], [[(-50580973084255), 161637925599], [(-85776027754157)]], [[18679280, 3438420008, (-12695239)], [(-2199323966614), 14122451901], [(-310163743)]], [[6750, (-18681979), (-213462), 981], [1628060, 300739088, (-1664445)], [(-6621244), 310236699], [(-56443)]], [[(-65), (-6745), 2699, 12, 0], [646, (-1628414), (-28029), 171], [35564, 6622475, (-72967)], [(-1509), 57519], [463]]], r3 := 25622198673, Vm := [[[18439548764876070346]], [[(-29120367469558), 0], [(-311488984047348)]], [[31056972602, 0, 0], [(-1284987212891), 0], [36270861188]], [[(-300375428), 0, 0, 0], [1497512609, 0, 0], [(-503387873), 0], [(-389696454)]], [[3960163, 0, 0, 0, 0], [(-14478573), 0, 0, 0], [3888612, 0, 0], [5491530, 0], [7572586]]], rm := 1893161460 }
noncomputable def w5 : Wit := { Z0 := { p := [[[1788421086414797853]], [[(-14720956948661124), 255488726630685407], [8450033989641148]], [[61778993382211, (-2102993849808732), 0], [(-71527334923044), 1207147712805878], [(-143742557633171)]], [[(-365520014549), 8825570483173, 0, 0], [355207717439, (-10218190703292), 0], [1207357772908, (-20534651090453)], [3776736437853]], [[3135520306, (-52217144936), 0, 0, 0], [(-2703530978), 50743959634, 0, 0], [(-5739904208), 172479681844, 0], [(-31650702009), 539533776836], [(-115838633558)]]], r := 2692537410997, ok := true }, Z1 := { p := [[[2043909813045483260]], [[(-16823950798469855), 0], [9657181702447026]], [[70604563865385, 0, 0], [(-81745525626336), 0], [(-164277208723624)]], [[(-417737159484), 0, 0, 0], [405951677073, 0, 0], [1379837454752, 0], [4316270214689]], [[3583451778, 0, 0, 0, 0], [(-3089749690), 0, 0, 0], [(-6559890523), 0, 0], [(-36172230867), 0], [(-132387009781)]]], r := 885837834567, ok := true }, Z2 := { p := [[[6867556270420269112203]], [[(-24889150357874286229), 255488726630685407], [(-266273097697577618842)]], [[122603294318966690, (-2102993849808732), 0], [957082868409556407, 1207147712805878], [11024494945980746620]], [[(-838893356240979), 8825570483173, 0, 0], [(-4544140519846340), (-10218190703292), 0], [(-39518312979875373), (-20534651090453)], [(-464812555897062133)]], [[8176248232906, (-52217144936), 0, 0, 0], [29729118238674, 50743959634, 0, 0], [185162303101570, 172479681844, 0], [1663452442306077, 539533776836], [19764141380735700]]], r := 1747527975137270, ok := true }, Z3 := { p := [[[22065149264278807224533]], [[(-513614421949299414983), 1641320137979601691], [(-870995598259311406985)]], [[12623659391947988313, (-45765051005195550), 0], [20481568594320250767, 6585519668565341], [36299326181425255465]], [[(-315115598805484398), 1114964683832863, 0, 0], [(-505317997564082226), (-168037055764601), 0], [(-856840029894887198), (-116736359032286)], [(-1536453272641791663)]], [[7923730005598223, (-27764505462004), 0, 0, 0], [12642727587832103, 3876088169959, 0, 0], [21171245788403532, 3041301784647, 0], [36350641275743575, 3106766106238], [65511208287914757]]], r := 44017725453473550, ok := true }, iE := { p := [[[6870590346219933979924]], [[(-24891901133288467963), 0], [(-266258762123126463319)]], [[122627588156627033, 0, 0], [957066524312774902, 0], [11024251085170331426]], [[(-839116815925108), 0, 0, 0], [(-4543942843568584), 0, 0], [(-39518050874934986), 0], [(-464806148622670857)]], [[8178853485005, 0, 0, 0, 0], [29727079521516, 0, 0, 0], [185159337009307, 0, 0], [1663445677471798, 0], [19763944859235583]]], r := 1745876449305679, ok := true }, iHu := { p := [[[22069150454845586990868]], [[(-513654602965193937875), 0], [(-870979544158368222350)]], [[12624715981555438513, 0, 0], [20481445373749392097, 0], [36299041602927891047]], [[(-315142447105001077), 0, 0, 0], [(-505314536869701131), 0, 0], [(-856837692956484028), 0], [(-1536445699004601799)]], [[7924410666361513, 0, 0, 0, 0], [12642640118302530, 0, 0, 0], [21171181678042835, 0, 0], [36350577735305940, 0], [65510974224179334]]], r := 43996217601207804, ok := true }, T := { p := [[[16140901064495857664]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[49527384078160801]], [[179435927007679, 0], [1919354714999567]], [[(-233884167357), 0, 0], [7008389650165, 0], [(-5087962666494)]], [[1998903094, 0, 0, 0], [(-10169420553), 0, 0], [(-17243800067), 0], [73715602042]], [[(-25626963), 0, 0, 0, 0], [86908830, 0, 0, 0], [(-23641), 0, 0], [249883422, 0], [(-1602513259)]]], r := 1181469891, ok := true }, de := { p := [[[(-130888491546436916551)]], [[341210886499523728, 0], [578574981455714148]], [[(-4374264648192960), 0, 0], [793214803170, 0], [(-12577044479965013)]], [[74773754883743, 0, 0, 0], [1087482, 0, 0], [1843991, 0], [364552014954285]], [[(-1437956824687), 0, 0, 0, 0], [2, 0, 0, 0], [23645, 0, 0], [4, 0], [(-11887565705029)]]], r := 2312739462946, ok := true }, dde := { p := [[[(-248894293232782325056087)]], [[6381563725556286306381, 0], [10820912404204137635356]], [[(-163629839584646188082), 0, 0], [(-277459294002005143081), 0], [(-470474453701789942204)]], [[4195636912426202498, 0, 0, 0], [7114340851503099051, 0, 0], [12063447530809608773, 0], [20455411030509500125]], [[(-107580433651943210), 0, 0, 0, 0], [(-182418996192441026), 0, 0, 0], [(-309319167456791389), 0, 0], [(-524497718731002274), 0], [(-889365696978662768)]]], r := 94483602196599451, ok := true }, nJu := { p := [[[(-261776983092873833101)]], [[682421772999047457, 0], [1157149962911428296]], [[(-8748529296385919), 0, 0], [1586429606340, 0], [(-25154088959930025)]], [[149547509767487, 0, 0, 0], [2174964, 0, 0], [3687983, 0], [729104029908571]], [[(-2875913649373), 0, 0, 0, 0], [5, 0, 0, 0], [47291, 0, 0], [9, 0], [(-23775131410058)]]], r := 4625478925881, ok := true }, Jd1 := { p := [[[(-497788586465564650112174)]], [[12763127451112572612763, 0], [21641824808408275270713]], [[(-327259679169292376164), 0, 0], [(-554918588004010286162), 0], [(-940948907403579884407)]], [[8391273824852404996, 0, 0, 0], [14228681703006198103, 0, 0], [24126895061619217547, 0], [40910822061019000251]], [[(-215160867303886420), 0, 0, 0, 0], [(-364837992384882051), 0, 0, 0], [(-618638334913582777), 0, 0], [(-1048995437462004548), 0], [(-1778731393957325535)]]], r := 188967204393198892, ok := true }, term0 := { p := [[[4657374883179098374626486855]], [[(-238820589495626692581873806), 0], [(-404885622174595590819271545)]], [[9185161843538868242311598, 0, 0], [20762532861849467966771375, 0], [26403334221901310759820958]], [[(-314018431492622201708662), 0, 0, 0], [(-798548284713488843112104), 0, 0], [(-1353980949242090714035534), 0], [(-1530562858285163821332123)]], [[10064612631745598092872, 0, 0, 0, 0], [27300613639584584460057, 0, 0, 0], [52075726376713589593777, 0, 0], [78488829495826195311813, 0], [83180637541051046990302]]], r := 15444846159818957834365, ok := true }, r0 := { p := [[[101457618500521184612210]], [[(-1494358538356191246127), 28390189464434194222725], [(-3894625366699979706259)]], [[21947366661902582515, (-409120047285542581541), 1861087084631587816161], [55530143236094598467, (-1095222780039211499707)], [160672118562949505912]], [[(-395873807589255774), 5953407073694055889, (-24307765552136790544), (-22713133264769175493)], [(-780226191660667074), 15350325921665209842, (-73302715575614333968)], [(-2263497838928861623), 45248933926892034250], [(-6759428882547310656)]], [[8428595649801158, (-108038717802580557), 339048198012054251, 651806428841188760, (-619790587960847368)], [13650047950315831, (-214029843594841529), 952809011493769660, 681264921850137187], [31270506131392028, (-627461569162729658), 3047008768126851803], [94532148405229100, (-1905183305898136015)], [286969114447463720]]], r := 1877648861140599539, ok := true }, r1 := { p := [[[131685577292545939037250]], [[(-1927120456780232084739), 0], [(-5062449560150343466976)]], [[28228550998259673816, 0, 0], [71813269826352362613, 0], [208941636740578243504]], [[(-510089878838131796), 0, 0, 0], [(-1006756419494731083), 0, 0], [(-2929649428324052538), 0], [(-8792297513765035511)]], [[10887987814908676, 0, 0, 0, 0], [17640713429564095, 0, 0, 0], [40386557393761454, 0, 0], [122411248734339272, 0], [373337157753747783]]], r := 379901576108313555, ok := true }, r2 := { p := [[[354132504134118089377085872]], [[(-6905805213836979924161198), 32396994695531724225738], [(-29806421330058194912299175)]], [[147155902193667120821424, (-433820695895494642447), 448683785990576243], [569950129176323496516181, (-1359823830969200054929)], [1905984841117553505805842]], [[(-3458644551439951692160), 7747020879951122906, 153371419251424, (-19981440215973)], [(-12036424537293650400405), 17279842310459170345, 89000703142027], [(-35999854640131300720253), 58303991464816880320], [(-108964332574120715035740)]], [[85020854168994916417, (-168594150365369030), (-5124410549430), (-571268632843), (-437173136840)], [282173034355352601481, (-299315464297731227), (-385646174366), (-1351816728444)], [755935661778899561572, (-724885798867129874), (-2598061133779)], [2039827917560155757122, (-2513491036573699889)], [5859074422279616178746]]], r := 12474203285152022569983, ok := true }, r3 := { p := [[[9310051555468221260049502782]], [[(-477416124167321182814752432), 933033556389129927893139], [(-809566911132780611284815268)]], [[18361871114070997367406253, (-44734755599226553969235), 1495108963906377624], [41515278159508741945304559, (-40632231643552449085790)], [52797783339114854794102089]], [[(-627751359733854985986782), 1680814528351005771791, 12732748743782294, (-1382650181295126)], [(-1596728979569595244943281), 1947558954321990310999, (-2547944932048186)], [(-2707536311177386235119972), 1767669123137341155119], [(-3060739382120310686928887)]], [[20120139967651997335538, (-56788908701013032568), (-1191683972348639), (-914450757362845), (-156316836680276)], [54588811095132539761016, (-73167080015447419379), (-501552799285681), (-1061684438431082)], [104135468393099571205799, (-84718394387273539867), (-15599624836038)], [156959153970992097383693, (-76882916720245648086)], [166344477061136387476308]]], r := 1601462846226749552656398, ok := true }, eta := { p := [[[(-354653972009591839698219195)]], [[6920489490112586737025166, 0], [29828727189433523770615543]], [[(-147535517548424785673898), 0, 0], [(-570577272866139671037616), 0], [(-1906948656777454663219845)]], [[3468372119546423251395, 0, 0, 0], [12052630004279505075050, 0, 0], [36026937358120324937679, 0], [109006081656589682017216]], [[(-85270010563662243769), 0, 0, 0, 0], [(-282588300154948218790), 0, 0, 0], [(-756635390042063723844), 0, 0], [(-2041000649615334574635), 0], [(-5860884852190441409003)]]], r := 1104261117940802083812, 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

theorem region : RegionPosI 5629499534213120 6755399441055744 13835058055282163712 18446744073709551616 2594073385365405696 2882303761517117440 :=
  (RegionPosI.split_b 6192449487634432 (RegionPosI.split_s 2738188573441261568 (RegionPosI.split_b 5910974510923776 (RegionPosI.of_check c0 q0 ok_0 5629499534213120 5910974510923776 13835058055282163712 18446744073709551616 2594073385365405696 2738188573441261568 (by decide +kernel)) (RegionPosI.of_check c1 q1 ok_1 5910974510923776 6192449487634432 13835058055282163712 18446744073709551616 2594073385365405696 2738188573441261568 (by decide +kernel))) (RegionPosI.split_b 5910974510923776 (RegionPosI.of_check c2 q2 ok_2 5629499534213120 5910974510923776 13835058055282163712 18446744073709551616 2738188573441261568 2882303761517117440 (by decide +kernel)) (RegionPosI.of_check c3 q3 ok_3 5910974510923776 6192449487634432 13835058055282163712 18446744073709551616 2738188573441261568 2882303761517117440 (by decide +kernel)))) (RegionPosI.split_s 2738188573441261568 (RegionPosI.of_check c4 q4 ok_4 6192449487634432 6755399441055744 13835058055282163712 18446744073709551616 2594073385365405696 2738188573441261568 (by decide +kernel)) (RegionPosI.of_check c5 q5 ok_5 6192449487634432 6755399441055744 13835058055282163712 18446744073709551616 2738188573441261568 2882303761517117440 (by decide +kernel))))

end CKLaneC.RSC2.S03_0032

end