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

import Definitions.Def_CK_CKLaneC_RSCell_Staged
import Definitions.Def_CK_CKLaneC_RSCell_RegionI

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

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

namespace CKLaneC.RSC2.BA_0057
open CKLaneC.TM3 CKLaneC.RSCell

noncomputable def c0 : Cell := { bc := 4323455642275676160, bh := 288230376151711744, tc := 3458764513820540928, th := 1152921504606846976, sc := 4575657221408423936, sh := 252201579132747776 }
noncomputable def q0 : Cert := { V0 := [[[1099903296286075597]], [[(-32639422979765155), 364756506038819855], [31125458913860140]], [[506523153049316, (-10712779980649040), (-933295186331047)], [(-952750622175445), 10215872791244859], [(-29223987226734)]], [[(-11979917260950), 161303861878270, 82674038858337, (-100571113300270)], [19707009738920, (-303276471960391), (-78839243001429)], [(-476503077632), (-14088791973819)], [14943945433254]], [[327855236398, (-3730050381599), (-3705840369311), 8723689053040, 770240085580], [(-601721751914), 5894439884706, 7034189989105, (-8319044897518)], [171985382731, 242276673913, (-2129267475896)], [(-470156559668), 4871256929286], [(-442326587779)]]], r0 := 84787361868064, V1 := [[[5498518418912813398]], [[(-143690362116262345), 0], [137025353209831448]], [[1484338286310362, 0, 0], [(-2772398113212605), 0], [(-806650865207389)]], [[(-27330471494996), 0, 0, 0], [14672789111872, 0, 0], [44264742779990, 0], [65093905349434]], [[685045513201, 0, 0, 0, 0], [(-434159528735), 0, 0, 0], [(-801806145266), 0, 0], [(-1493619639486), 0], [(-2532008552368)]]], r1 := 88189028467968, V2 := [[[12271600350134200825]], [[(-71504174280566980), 109810813193499202], [(-504602558668321172)]], [[860963642566748, (-1248063006774116), (-1556710800382603)], [(-3808336896663993), 17430256849179999], [(-7583163560292478)]], [[(-15237664181748), (-29019151399900), 57550152244677, 18078418007420], [93231383568229, (-297701782630718), (-337780120224541)], [158769346607404, 832932498186373], [(-62336025755486)]], [[395746239638, 600583011019, (-387061993102), (-1210589021924), (-156305384882)], [(-1920169753803), (-2531965115951), 15358978212182, 4415687882987], [1143973428568, (-28314680633035), (-22686822748545)], [8559374238716, 4717933507451], [3300365023620]]], r2 := 1282511272913796, V3 := [[[15102770721988404407]], [[(-155432502178959305), 135688833405173192], [(-344388035128114893)]], [[1539141583621398, 3020399100095965, (-4778172956778914)], [(-12963514759769938), 26697352176322059], [(-11745310230153109)]], [[(-8954786541009), (-204929762553570), 27262899124614, 154512380777047], [293925622548093, 329547496029001, (-1348523112850607)], [(-114129195351545), 2047098931984654], [(-310464302661040)]], [[(-83076054669), 2900607930557, 9372914544462, (-5815616681495), (-4640430850361)], [(-3332361547898), (-45229108528790), 24315490893623, 55455543777199], [21277267156833, (-18345492121290), (-155774793364735)], [12441822060599, 81811212834176], [(-4287577314177)]]], r3 := 21309659996010020, Vm := [[[13713002291631568787]], [[(-85921278795775270), 0], [(-282002419473339747)]], [[435808841200778, 0, 0], [(-6609148541880506), 0], [2840713377675044]], [[(-8415983642495), 0, 0, 0], [31332157505814, 0, 0], [(-49737745455890), 0], [57970942517081]], [[268045207774, 0, 0, 0, 0], [(-603381230165), 0, 0, 0], [(-512774756515), 0, 0], [974764469408, 0], [1124698204444]]], rm := 194790001972420 }
noncomputable def w0 : Wit := { Z0 := { p := [[[1102733007443233954]], [[(-32891868472806766), 367577669147744651], [31366194843123570]], [[517971641542438, (-10963956157602256), 0], [(-974482620120135), 10455398281041190], [(-22601594188448)]], [[(-12382378574518), 172657213847479, 0, 0], [20739593076414, (-324827540040045), 0], [(-1093481026129), (-7533864729483)], [15112631380601]], [[341309536862, (-4127459524840), 0, 0, 0], [(-641114308323), 6913197692138, 0, 0], [204328244196, (-364493675377), 0], [(-486295336330), 5037543793533], [(-439322122920)]]], r := 17778862315943, ok := true }, Z1 := { p := [[[5881242706363914426]], [[(-175423298521636082), 0], [167286372496659040]], [[2762515421559670, 0, 0], [(-5197240640640717), 0], [(-120541835671721)]], [[(-66039352397427), 0, 0, 0], [110611163074209, 0, 0], [(-5831898806018), 0], [80600700696541]], [[1820317529933, 0, 0, 0, 0], [(-3419276311051), 0, 0, 0], [1089750635713, 0, 0], [(-2593575127092), 0], [(-2343051322239)]]], r := 22841481324712, ok := true }, Z2 := { p := [[[18830988077985748643]], [[(-239351088950326571), 367577669147744651], [(-1689092603607729408)]], [[5091417582385929, (-10963956157602256), 0], [18436132817833963, 10455398281041190], [84648740343755489]], [[(-128296010218818), 172657213847479, 0, 0], [(-337905129774402), (-324827540040045), 0], [(-937085672832752), (-7533864729483)], [(-5365308980507743)]], [[3720903690704, (-4127459524840), 0, 0, 0], [7512082003680, 6913197692138, 0, 0], [14295738512951, (-364493675377), 0], [59935354313512, 5037543793533], [336900827772531]]], r := 73128606744826, ok := true }, Z3 := { p := [[[34434220179733688207]], [[(-1454717689171761013), 1269933530056147298], [(-3223182793925275686)]], [[73085626886027789, (-74185023928061810), 0], [138706557522860482, 22861225151729121], [178149468861342213]], [[(-3806411880363053), 3521617547161715, 0, 0], [(-7055212382618719), (-956717341961363), 0], [(-8221647641479394), (-327211691716928)], [(-11106803969922048)]], [[201586957471087, (-182303417895086), 0, 0, 0], [369799527146612, 37903820446962, 0, 0], [419574236850971, 21860979722120, 0], [514913611183169, 13686554679478], [707096642918948]]], r := 745507547455333, ok := true }, iE := { p := [[[33370833073962380591]], [[(-388629120898860809), 0], [(-1275520498615583217)]], [[8608839418058336, 0, 0], [13677092536215902, 0], [84350731964624868]], [[(-218190365448095), 0, 0, 0], [(-168693630186339), 0, 0], [(-957332800093885), 0], [(-5166044683282478)]], [[6361588995467, 0, 0, 0, 0], [2512465678588, 0, 0, 0], [16601852847873, 0, 0], [57421175805944, 0], [331108241963056]]], r := 79262943722138, ok := true }, iHu := { p := [[[57645966286240463644]], [[(-2319364926847201098), 0], [(-2805327101996138468)]], [[117686163283844973, 0, 0], [130064104630154419, 0], [172168719057155143]], [[(-6135532473746437), 0, 0, 0], [(-6571729395462497), 0, 0], [(-7948663173559398), 0], [(-10856642189975314)]], [[325132152642080, 0, 0, 0, 0], [345913824700062, 0, 0, 0], [408528864011862, 0, 0], [506053884679137, 0], [695853165104117]]], r := 851983548411011, ok := true }, T := { p := [[[3458764513820540928]], [[0, 1152921504606846976], [0]]], r := 0, ok := true }, E := { p := [[[10196999462576918842]], [[118751933107700620, 0], [389755982718851078]], [[(-1247612592061740), 0, 0], [4898761270192595, 0], [(-10877241880380608)]], [[21507168551635, 0, 0, 0], [(-88308048292300), 0, 0], [(-106810686982116), 0], [177634385967811]], [[(-595123992656), 0, 0, 0, 0], [1422167155379, 0, 0, 0], [(-363384056414), 0, 0], [2080556376335, 0], [(-6554649913525)]]], r := 8622391395346, ok := true }, de := { p := [[[(-37059650895934608493)]], [[778700369841506653, 0], [941856637808298523]], [[(-20135625688570399), 0, 0], [3204320609463480, 0], [(-29457370225029657)]], [[742896113957195, 0, 0, 0], [10901521692437, 0, 0], [13185650047042, 0], [1314532573671078]], [[(-30702606514644), 0, 0, 0, 0], [37088415829, 0, 0, 0], [430673039418, 0, 0], [54258418041, 0], [(-65710221971432)]]], r := 25945579100423, ok := true }, dde := { p := [[[(-243013844942537999740)]], [[12567698715487139592, 0], [15200930827303492652]], [[(-695520567489982120), 0, 0], [(-844650791752814191), 0], [(-1017510315922532603)]], [[38326209915118265, 0, 0, 0], [46333314598098105, 0, 0], [56041247180556755, 0], [67817088301098951]], [[(-2112500819384160), 0, 0, 0, 0], [(-2555238171711286), 0, 0, 0], [(-3091488291596734), 0, 0], [(-3738180178823713), 0], [(-4521208897699240)]]], r := 1575641069947132, ok := true }, nJu := { p := [[[(-74119301791869216985)]], [[1557400739683013306, 0], [1883713275616597046]], [[(-40271251377140798), 0, 0], [6408641218926960, 0], [(-58914740450059314)]], [[1485792227914390, 0, 0, 0], [21803043384874, 0, 0], [26371300094085, 0], [2629065147342157]], [[(-61405213029288), 0, 0, 0, 0], [74176831658, 0, 0, 0], [861346078836, 0, 0], [108516836082, 0], [(-131420443942864)]]], r := 51891158200842, ok := true }, Jd1 := { p := [[[(-486027689885075999479)]], [[25135397430974279185, 0], [30401861654606985304]], [[(-1391041134979964240), 0, 0], [(-1689301583505628381), 0], [(-2035020631845065206)]], [[76652419830236531, 0, 0, 0], [92666629196196210, 0, 0], [112082494361113510, 0], [135634176602197902]], [[(-4225001638768320), 0, 0, 0, 0], [(-5110476343422572), 0, 0, 0], [(-6182976583193468), 0, 0], [(-7476360357647426), 0], [(-9042417795398480)]]], r := 3151282139894260, ok := true }, term0 := { p := [[[5615358112369654846042]], [[(-573252447879947117658), 0], [(-632079991794513033201)]], [[46380082495074122923, 0, 0], [67195816737899581131, 0], [59647464109035223829]], [[(-3370073756714245407), 0, 0, 0], [(-5483884647118741381), 0, 0], [(-6406958981998608915), 0], [(-5143032284710703538)]], [[230606172657014696, 0, 0, 0, 0], [400476048958724576, 0, 0, 0], [525092077579496853, 0, 0], [555734655773293586, 0], [420638169072797562]]], r := 301090362200197340, ok := true }, r0 := { p := [[[20565910037706351645]], [[(-1196252998955295724), 13604515537948029101], [(-671140825918494120)]], [[61869403330305129, (-785426616929684915), 2197322212128485899], [24772377215955505, (-449758111123932629)], [48468671003059476]], [[(-3056211507212066), 40427861639699287, (-122962427788354034), (-22949154890315733)], [(-709234615489210), 16853469531611249, (-76464611169503716)], [(-2330415547888809), 32183800826142316], [(-2876289446513743)]], [[151449236027554, (-1991565036057500), 6202439092032432, 2576031554451280, (-1741344743135035)], [17038302432599, (-502513974974545), 3025748413045389, (-469472925597554)], [101843901461745, (-1537220661465399), 5280179828211696], [126769040895157, (-1916629639437324)], [185717508365757]]], r := 9625874549623387, ok := true }, r1 := { p := [[[485175921557709765995]], [[(-23799065791046706441), 0], [(-20190798096728613190)]], [[1138203418770462509, 0, 0], [835521215341537574, 0], [1283200132518832525]], [[(-54881220567466165), 0, 0, 0], [(-31048047270383503), 0, 0], [(-56272924834901622), 0], [(-79302110429350095)]], [[2729058168113924, 0, 0, 0, 0], [1235382532154210, 0, 0, 0], [2263201431839635, 0, 0], [3379734187389575, 0], [5069384454552064]]], r := 40620384648168676, ok := true }, r2 := { p := [[[721319651539577117511]], [[(-46346485226984196021), 33093829127795675908], [(-119912517184425718363)]], [[2499419911705549517, (-1710337277412520919), 177350355815115611], [7219871997205647761, (-1283161828815363745)], [11393914024848489380]], [[(-131320270852897817), 82663240883008255, 5653736024213356, (-5169260290597096)], [(-381022814935169440), 43883925387626779, 13423745514258125], [(-667674745057657664), 88017610059927485], [(-985208548468973494)]], [[6922223586555227, (-4149878255202321), (-208854672806890), 32342250216653, 119133516438687], [19942897307898415, (-1991559280601051), 621605711836939, (-1138633656197958)], [35002493972817973, (-4833504787652728), 1942874172387118], [57692056540023215, (-7841109898045228)], [80982618119416298]]], r := 2384329547999210131, ok := true }, r3 := { p := [[[5197430094224743304711]], [[(-564832299777303347757), 283113623438591121405], [(-877263296763018896863)]], [[46056667073638849460, (-27474246891083351810), 24712781052459911], [94836860480655501206, (-17052149810602980338)], [92611187269325370534]], [[(-3360312591934352592), 2193249905455943384, 37552863062467550, (-5910660521754621)], [(-7813571438401890504), 1834053799986570995, (-91014784986190994)], [(-10179511979157627141), 1332422625064050152], [(-8541595775434386169)]], [[230618493611805075, (-159501824107837633), (-67082522390496), (-1861035167133895), 479621595362672], [574152592907289814, (-151359587313790850), 7992902302998032, 1433884455077412], [841947172436419503, (-129809834653557474), (-8953701285580961)], [937453523655824074, (-78631446816930141)], [723482470069498113]]], r := 765932201047458227016, ok := true }, eta := { p := [[[(-1765423216655190161630)]], [[106163047768067932178, 0], [167976123589671650689]], [[(-5837774015949420460), 0, 0], [(-10032756477848524710), 0], [(-14793056741279775018)]], [[313492186060739312, 0, 0, 0], [532955028600464756, 0, 0], [868954778535229685, 0], [1210592441617472874]], [[(-16835101484808184), 0, 0, 0, 0], [(-28123190828531738), 0, 0, 0], [(-45762163622936054), 0, 0], [(-70161582109548283), 0], [(-95322003020525872)]]], r := 325660053546769602, 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 := 4323455642275676160, bh := 288230376151711744, tc := 3458764513820540928, th := 1152921504606846976, sc := 5080060379673919488, sh := 252201579132747776 }
noncomputable def q1 : Cert := { V0 := [[[1036559644471883888]], [[(-30747350383386363), 343947836993759309], [29294252701438409]], [[441773954245736, (-10109336846464286), (-781807378025867)], [(-880590482090837), 9631576852368480], [(-29549673076573)]], [[(-9714759916316), 141111828695989, 69265613758784, (-84539401247337)], [16500575524064, (-281642393697299), (-65992170631603)], [122600720581, (-13471512807671)], [14041431147052]], [[243880670617, (-3034607002605), (-3027146068844), 7352113471193, 574188220473], [(-473927098840), 4958900711808, 5855573161215, (-7004657872283)], [129586597742, 368668271602, (-1777860672522)], [(-433430991603), 4589127560455], [(-418017164047)]]], r0 := 77083047347372, V1 := [[[5216866725773949131]], [[(-138060629738172984), 0], [131535983596656621]], [[1335250675556087, 0, 0], [(-2718506592518759), 0], [(-721233025120807)]], [[(-22598303348156), 0, 0, 0], [12366816165745, 0, 0], [41198269817982, 0], [62168178180901]], [[509767054567, 0, 0, 0, 0], [(-340064696553), 0, 0, 0], [(-733970678721), 0, 0], [(-1433408321705), 0], [(-2384994148358)]]], r1 := 80812132775196, V2 := [[[12131919905852051965]], [[(-68231447291250327), 107203208314995160], [(-511860947787797371)]], [[778114821829506, (-1357341148318535), (-1443237284246110)], [(-3457032716679569), 16825512057240852], [(-7261611509552280)]], [[(-12516966039693), (-25715569880386), 55886653523461, 15777612020749], [82751141202079, (-306669714279899), (-307946731783834)], [162516051811411, 777483971807050], [(-45999718143783)]], [[291605474871, 504776931760, (-442191711994), (-1091522722972), (-125270579377)], [(-1589103254923), (-1971518637720), 14475204705546, 3736296504908], [743627979805, (-27127420613134), (-19742977947328)], [7780118102530, 2366576557416], [3559446029655]]], r2 := 1159444639768184, V3 := [[[14797989460368417981]], [[(-149385696110300024), 140932933541449383], [(-369166022045671011)]], [[1483768501549996, 2235109176950843, (-4688788869174268)], [(-11827785279026596), 27183789807551406], [(-11892520230932971)]], [[(-9449648712218), (-187822335211842), 60844278967582, 142089516935708], [273964010400387, 160933921904363, (-1290902781578059)], [(-35074911340891), 1996412523775667], [(-283077961027198)]], [[(-43034359833), 2793882538950, 7457544511983, (-6532493238312), (-3955728681668)], [(-3308043271238), (-39164383138800), 32822141782277, 49370978699747], [18286808411323, (-31719638645634), (-142274874529025)], [14778919855698, 71742880482968], [(-2336566657221)]]], r3 := 16082995515296928, Vm := [[[13542839654534462675]], [[(-84271137449401400), 0], [(-295099892671933547)]], [[391080482080710, 0, 0], [(-6490426127250437), 0], [2739211272408433]], [[(-6593028707818), 0, 0, 0], [28175190102122, 0, 0], [(-51751468134910), 0], [59726359485938]], [[193087684235, 0, 0, 0, 0], [(-456890724668), 0, 0, 0], [(-493444724708), 0, 0], [780623239453, 0], [1238726842442]]], rm := 195949291755120 }
noncomputable def w1 : Wit := { Z0 := { p := [[[1038927240511611024]], [[(-30958434633635860), 346309080170537008], [29495361261720847]], [[451097518989628, (-10319478211211954), 0], [(-898622717399894), 9831787087240282], [(-24042342713665)]], [[(-10025588459097), 150365839663209, 0, 0], [17327523464134, (-299540905799965), 0], [(-380321608078), (-8014114237889)], [14181107854824]], [[253586233683, (-3341862819699), 0, 0, 0], [(-503645534577), 5775841154711, 0, 0], [154658114540, (-126773869360), 0], [(-446442368071), 4727035951608], [(-415551311192)]]], r := 16534184022263, ok := true }, Z1 := { p := [[[5540945282728592130]], [[(-165111651379391251), 0], [157308593395844520]], [[2405853434611353, 0, 0], [(-4792654492799430), 0], [(-128225827806211)]], [[(-53469805115180), 0, 0, 0], [92413458475384, 0, 0], [(-2028381909747), 0], [75632575225729]], [[1352459912978, 0, 0, 0, 0], [(-2686109517742), 0, 0, 0], [824843277550, 0, 0], [(-2381025963043), 0], [(-2216273659690)]]], r := 20872412002654, ok := true }, Z2 := { p := [[[18371681145586064179]], [[(-220414762967800334), 346309080170537008], [(-1653514822828456878)]], [[4402253334735749, (-10319478211211954), 0], [17168817969010116, 9831787087240282], [82829618654529935]], [[(-102735562725349), 150365839663209, 0, 0], [(-297111338316719), (-299540905799965), 0], [(-883055838272413), (-8014114237889)], [(-5249213880963563)]], [[2735001304154, (-3341862819699), 0, 0, 0], [6150567696171, 5775841154711, 0, 0], [12764804309080, (-126773869360), 0], [56232790866103, 4727035951608], [329627735652437]]], r := 68584836830138, ok := true }, Z3 := { p := [[[31789590064462907874]], [[(-1202364589973285227), 1134330617077155421], [(-2971316292567099188)]], [[54343914024018829, (-62014707426891899), 0], [114368726904398387, 21085600600600254], [163224625615576611]], [[(-2546935920790264), 2623365952919605, 0, 0], [(-5235833115005563), (-825174719740222), 0], [(-6775420661680229), (-286923719311235)], [(-10172843757757336)]], [[121421981500024, (-122169602886337), 0, 0, 0], [247033906388712, 28472773682770, 0, 0], [310863511186680, 18576772469713, 0], [423613860098384, 12268144720440], [647187093784356]]], r := 538938088196428, ok := true }, iE := { p := [[[32626360291904852998]], [[(-356623676864309599), 0], [(-1248821505822402013)]], [[7437469770816228, 0, 0], [13031436770635924, 0], [82499743887611364]], [[(-174512892736475), 0, 0, 0], [(-154386694480652), 0, 0], [(-894951750742518), 0], [(-5054640926739825)]], [[4670898956181, 0, 0, 0, 0], [2260113567497, 0, 0, 0], [14655175514389, 0, 0], [54046100750061, 0], [323926132711548]]], r := 73910554408972, ok := true }, iHu := { p := [[[53433596636670948915]], [[(-1913073821539029704), 0], [(-2568984846066697029)]], [[87480124546371788, 0, 0], [107408365440987054, 0], [157749873569743118]], [[(-4104333387541185), 0, 0, 0], [(-4870583612197186), 0, 0], [(-6540497993521925), 0], [(-9938756974803169)]], [[195802607744772, 0, 0, 0, 0], [230873044092296, 0, 0, 0], [302691487455541, 0, 0], [416325350530530, 0], [636704216418256]]], r := 601962012721069, ok := true }, T := { p := [[[3458764513820540928]], [[0, 1152921504606846976], [0]]], r := 0, ok := true }, E := { p := [[[10429676000524282320]], [[114001971734900484, 0], [399211054242117645]], [[(-1131434745192361), 0, 0], [4561420990476737, 0], [(-11092326748571588)]], [[17431619295349, 0, 0, 0], [(-80633442578677), 0, 0], [(-108279194319939), 0], [181789239943337]], [[(-434912410402), 0, 0, 0, 0], [1150222911768, 0, 0, 0], [(-370903839872), 0, 0], [2074157071097, 0], [(-6695189071277)]]], r := 8506273789087, ok := true }, de := { p := [[[(-35577301045802085987)]], [[706187690104063332, 0], [948309183854027903]], [[(-16319980030569626), 0, 0], [3248375829598178, 0], [(-29429253785737393)]], [[542903232916244, 0, 0, 0], [11127115196158, 0, 0], [14942126120555, 0], [1314655215185148]], [[(-20207386150418), 0, 0, 0, 0], [38115261006, 0, 0, 0], [447678865612, 0, 0], [68731927805, 0], [(-65709686469209)]]], r := 23004930952336, ok := true }, dde := { p := [[[(-220384364088856640395)]], [[10186154393175343328, 0], [13678550185121175319]], [[(-508281518177128238), 0, 0], [(-686021974987835867), 0], [(-916566427472062287)]], [[25224976357214729, 0, 0, 0], [33849749948781254, 0, 0], [45455378502649094, 0], [61082978899944137]], [[(-1252334132911555), 0, 0, 0, 0], [(-1681828071053535), 0, 0, 0], [(-2259357259115107), 0, 0], [(-3032782211393664), 0], [(-4072297258822205)]]], r := 1197020418795856, ok := true }, nJu := { p := [[[(-71154602091604171973)]], [[1412375380208126664, 0], [1896618367708055807]], [[(-32639960061139252), 0, 0], [6496751659196357, 0], [(-58858507571474785)]], [[1085806465832489, 0, 0, 0], [22254230392316, 0, 0], [29884252241110, 0], [2629310430370296]], [[(-40414772300835), 0, 0, 0, 0], [76230522012, 0, 0, 0], [895357731224, 0, 0], [137463855611, 0], [(-131419372938417)]]], r := 46009861904663, ok := true }, Jd1 := { p := [[[(-440768728177713280790)]], [[20372308786350686657, 0], [27357100370242350639]], [[(-1016563036354256475), 0, 0], [(-1372043949975671734), 0], [(-1833132854944124573)]], [[50449952714429458, 0, 0, 0], [67699499897562509, 0, 0], [90910757005298188, 0], [122165957799888274]], [[(-2504668265823110), 0, 0, 0, 0], [(-3363656142107069), 0, 0, 0], [(-4518714518230213), 0, 0], [(-6065564422787328), 0], [(-8144594517644410)]]], r := 2394040837591704, ok := true }, term0 := { p := [[[4630672120442270635257]], [[(-421845382193713423659), 0], [(-516808455619122065990)]], [[30677874466985351910, 0, 0], [49312025235433296802, 0], [48663864268267510436]], [[(-2005359442869975724), 0, 0, 0], [(-3619345124871646637), 0, 0], [(-4695205625077391578), 0], [(-4190618854280321703)]], [[123507214246625642, 0, 0, 0, 0], [237911811720237429, 0, 0, 0], [346276155078192940, 0, 0], [406992804045264404, 0], [342467135281036249]]], r := 197538989342952313, ok := true }, r0 := { p := [[[18398634067511939991]], [[(-981146029470851977), 12180874654095761545], [(-624301228530504476)]], [[46639289052647657, (-644812394169713458), 1974007349231990599], [22130841946878298, (-417958789517815677)], [44181647560554356]], [[(-2096587950424347), 30501041428773524, (-101353966277210182), (-18415730871667085)], [(-613799360719115), 14994764260015820, (-70797435584443787)], [(-1971944985862592), 29354048799875079], [(-2640994831177398)]], [[93998091961356, (-1366898303842488), 4695671868583411, 1988652738232748, (-1412427468798022)], [14777363804140, (-429103634790026), 2653702782120313, (-356630767165911)], [78773534376225, (-1302493295544077), 4826781766616639], [109191896531759, (-1759767730392315)], [170269926064661]]], r := 7338234945671290, ok := true }, r1 := { p := [[[441731185336944509169]], [[(-19827391334412512265), 0], [(-18634846887317138215)]], [[864793969217718345, 0, 0], [724622487775282359, 0], [1178999033194108983]], [[(-37639476536555074), 0, 0, 0], [(-24744244376209238), 0, 0], [(-48252541575363287), 0], [(-73025895334738343)]], [[1683767825309745, 0, 0, 0, 0], [891056032291258, 0, 0, 0], [1775342536287684, 0, 0], [2914620346621689, 0], [4668106370863762]]], r := 32452905958966735, ok := true }, r2 := { p := [[[637673921812683166866]], [[(-37729204665306704718), 29973702213602043556], [(-106852552950284093768)]], [[1852310053575233825, (-1423441761462087300), 187880487584833816], [5905365352804847047, (-1202653663130961851)], [10185361057581689376]], [[(-88009993408330940), 62118865972817076, 4903068192707829, (-5086341087105484)], [(-282782068028234634), 36945711896439406, 14519058916716732], [(-546856102718443689), 79196378092974724], [(-880683793322861815)]], [[4182240384638970, (-2808868584597214), (-168738623581873), 49882349121468, 109265940424109], [13357529518429548, (-1507886020731240), 478745257876470, (-1088078675324148)], [26005451432600059, (-4021797866834580), 1879791618101044], [47340316337256845, (-7285616683697772)], [72540709470460822]]], r := 1868189493559597631, ok := true }, r3 := { p := [[[4228367086523916868636]], [[(-414603335914983687917), 235816309400905538617], [(-714809085036760404117)]], [[30411366873088975627, (-20315762540851427433), 99610878436510628], [69388046458386776855, (-13913256369144140895)], [75185810198592539685]], [[(-1996380452156418896), 1450110481342676318, 37351145085398686, (-9537892758459470)], [(-5142789995607173470), 1338402006467172377, (-74487904576200935)], [(-7436442952740369753), 1106389695767245123], [(-6935766649187323128)]], [[123341355530283556, (-94897223990621490), (-53698913807042), (-1753690523779611), 640581727097958], [340421476305828061, (-100759160723362460), 8455859845853494, (-77401978785881)], [554520571126584726, (-98341981923562207), (-6243256143666686)], [685862121366940761, (-65852999660787966)], [587521828757279348]]], r := 409813749439517764171, ok := true }, eta := { p := [[[(-1574183428249376374842)]], [[86099387220531059042, 0], [149839064015320750659]], [[(-4298468284324845369), 0, 0], [(-8196223820187813512), 0], [(-13220835440843297409)]], [[208531080365242618, 0, 0, 0], [394601556610752338, 0, 0], [711115726828837415, 0], [1083515889411446703]], [[(-10094451534345367), 0, 0, 0, 0], [(-18784435990116641), 0, 0, 0], [(-33948212987126420), 0, 0], [(-57539091714229987), 0], [(-85415180450759594)]]], r := 284176352725973565, 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 := 4323455642275676160, bh := 288230376151711744, tc := 3458764513820540928, th := 1152921504606846976, sc := 5836665117072162816, sh := 504403158265495552 }
noncomputable def q2 : Cert := { V0 := [[[948049481938339219]], [[(-56670355687802301), 314813504328648584], [26789197555433334]], [[1463510964047201, (-18674537095128208), (-598795935014371)], [(-1586136639426145), 8827822896571951], [(-28165322762211)]], [[(-58482790285601), 469405058791181, 106984919726772, (-65040736853508)], [51479938701170, (-510515695042413), (-50573886738983)], [1510052740114, (-12156058010346)], [12810954543026]], [[2620607156621, (-18352756331060), (-9098991043120), 11442564012898, 368834884060], [(-2739195274129), 15568884381612, 8984788547899, (-5409126238258)], [336660929789, 995904102031, (-1362719972238)], [(-777365134218), 4200735961592], [(-383145351267)]]], r0 := 132333251343444, V1 := [[[4814130060749731783]], [[(-261218830846963767), 0], [123483305862942520]], [[4624085166675260, 0, 0], [(-5305092458615765), 0], [(-603991720158365)]], [[(-140465803271657), 0, 0, 0], [39036685907553, 0, 0], [74080820196034, 0], [57987259079058]], [[5518231591167, 0, 0, 0, 0], [(-1974550519663), 0, 0, 0], [(-2623997123234), 0, 0], [(-2712556591705), 0], [(-2176410713575)]]], r1 := 159806660729800, V2 := [[[11933912391472646927]], [[(-127744562367949659), 102912580702311072], [(-521527507343779647)]], [[2716893243139274, (-2998090309419362), (-1279752159828135)], [(-5999837858029102), 15889866796080470], [(-6768869650598850)]], [[(-77209978497928), (-86712005394420), 106089616476663, 12753185063022], [280609435165627, (-632883173707588), (-266487715413187)], [331031202329768, 698830079530534], [(-24363468073978)]], [[3117379661188, 3188354452438, (-2003843770911), (-1855460442545), (-88672099429)], [(-9864787345474), (-5272729792311), 26340089060332, 2882683560229], [1119524869304, (-50610233932562), (-15925690192695)], [13306992415810, (-509619474129)], [3797323213920]]], r2 := 1818141920579156, V3 := [[[14362928406157075967]], [[(-281483307526795390), 146021894575693295], [(-402272214434159220)]], [[5588764324237159, 2363429636447041, (-4446825326685092)], [(-20544385424777423), 27339283580799511], [(-11845691184018513)]], [[(-77697908643444), (-654588348188120), 196064835646458, 121764916650108], [979186896687112, (-98386745708302), (-1179216839205089)], [124520493528382, 1878879255568481], [(-235525618886406)]], [[(-65326039991), 20555251002464, 20097991872970, (-13793081150569), (-3006581518816)], [(-25247963003713), (-124347019587255), 81563623458298, 40231649461280], [57014140806995, (-91003992158245), (-120743338196280)], [33252198514568, 56224752367055], [368635812362]]], r3 := 33442579310076368, Vm := [[[13293382269307671332]], [[(-164167962628472126), 0], [(-314328776996229033)]], [[1363055176665724, 0, 0], [(-12664409855541264), 0], [2579617474503530]], [[(-37790011696210), 0, 0, 0], [99163041621835, 0, 0], [(-109217013945647), 0], [61629792369702]], [[1999647898043, 0, 0, 0, 0], [(-2447148475651), 0, 0, 0], [(-1830226139146), 0, 0], [975677409113, 0], [1403408322507]]], rm := 511725655096628 }
noncomputable def w2 : Wit := { Z0 := { p := [[[949860063456827626]], [[(-56995551238638907), 316620021152275875], [26942923921710315]], [[1491424155015838, (-18998517079546303), 0], [(-1613688753555543), 8980974640570105], [(-23966041450069)]], [[(-60221273678363), 497141385005279, 0, 0], [53904316625332, (-537896251185181), 0], [756951833172, (-7988680483357)], [12917018249315]], [[2719811534340, (-20073757892788), 0, 0, 0], [(-2900230889490), 17968105541777, 0, 0], [407069600342, 252317277724, 0], [(-796584494946), 4305672749771], [(-381286121956)]]], r := 27152756295769, ok := true }, Z1 := { p := [[[5065920338436414006]], [[(-303976273272740837), 0], [143695594249121683]], [[7954262160084474, 0, 0], [(-8606340018962895), 0], [(-127818887733698)]], [[(-321180126284602), 0, 0, 0], [287489688668441, 0, 0], [4037076443584, 0], [68890763996351]], [[14505661516482, 0, 0, 0, 0], [(-15467898077278), 0, 0, 0], [2171037868494, 0, 0], [(-4248450639708), 0], [(-2033525983765)]]], r := 39141269419157, ok := true }, Z2 := { p := [[[17747486968504655251]], [[(-393017896966606276), 316620021152275875], [(-1604527350104369178)]], [[14425348551182959, (-18998517079546303), 0], [31075525896189604, 8980974640570105], [80289412282427838]], [[(-607836419424506), 497141385005279, 0, 0], [(-995047160325109), (-537896251185181), 0], [(-1624543983331330), (-7988680483357)], [(-5087948782259155)]], [[28913216310005, (-20073757892788), 0, 0, 0], [37496666631287, 17968105541777, 0, 0], [43620938488496, 252317277724, 0], [102816712785214, 4305672749771], [319496669596203]]], r := 124611250981767, ok := true }, Z3 := { p := [[[28611419500225145747]], [[(-1867937977708000548), 969008943554659677], [(-2669499492955660394)]], [[146742527529908456, (-98085313865682119), 0], [177086302619513511, 18835630084566318], [145348037552441655]], [[(-11956217505074412), 7101755306716295, 0, 0], [(-14099596270267102), (-1367622743584108), 0], [(-10487488663007870), (-236904765506276)], [(-9056578873186118)]], [[991435951894408, (-574863991895508), 0, 0, 0], [1157056093388664, 77667586438199, 0, 0], [835232508366605, 29965553292025, 0], [653944581071672, 10533243603039], [575608290512560]]], r := 1765251656277827, ok := true }, iE := { p := [[[31619062409501793177]], [[(-632512650782056223), 0], [(-1211058021137220623)]], [[24346210628079285, 0, 0], [24326012824105205, 0], [79939416778051317]], [[(-1030804980228034), 0, 0, 0], [(-542366860843226), 0, 0], [(-1628448064774050), 0], [(-4899311108130572)]], [[49305232518898, 0, 0, 0, 0], [15405631790402, 0, 0, 0], [49439820210452, 0, 0], [99245732246532, 0], [313928439697089]]], r := 148778093152640, ok := true }, iHu := { p := [[[48384739142703372642]], [[(-2962225009150031422), 0], [(-2285145007058595680)]], [[236117198324253310, 0, 0], [166813438709322073, 0], [140513826594596455]], [[(-19259530408259557), 0, 0, 0], [(-13089762977785944), 0, 0], [(-10097817154292012), 0], [(-8841640513720656)]], [[1598342614320025, 0, 0, 0, 0], [1080122556821331, 0, 0, 0], [813530668871816, 0, 0], [642783137896112, 0], [566047345137418]]], r := 2131241655298998, ok := true }, T := { p := [[[3458764513820540928]], [[0, 1152921504606846976], [0]]], r := 0, ok := true }, E := { p := [[[10761937293203253273]], [[215283470354537702, 0], [412198512185894651]], [[(-3979968538383421), 0, 0], [8211708469177615, 0], [(-11420537126001454)]], [[105466169467950, 0, 0, 0], [(-286583622444344), 0, 0], [(-221078794457065), 0], [187995364807170]], [[(-4588963030186), 0, 0, 0, 0], [6933005114728, 0, 0, 0], [(-1530310067769), 0, 0], [4125845492765, 0], [(-6906120700447)]]], r := 18270782712580, ok := true }, de := { p := [[[(-33592422650369006644)]], [[1242053419673790241, 0], [958155495176923901]], [[(-49370220587510950), 0, 0], [6632363833711980, 0], [(-29380319027179986)]], [[2864212201393525, 0, 0, 0], [45909302033078, 0, 0], [35415747282660, 0], [1314898863207668]], [[(-185540397628446), 0, 0, 0, 0], [317784739500, 0, 0, 0], [1898032409191, 0, 0], [189114347017, 0], [(-65708471107745)]]], r := 89033637768565, ok := true }, dde := { p := [[[(-193807649789860755312)]], [[15407270363919607699, 0], [11885608566452268807]], [[(-1340778648789471597), 0, 0], [(-1041478557680544274), 0], [(-797900110177571261)]], [[115805480942646142, 0, 0, 0], [89236483676289580, 0, 0], [68839573121709110, 0], [53163831636014104]], [[(-10008326007945084), 0, 0, 0, 0], [(-7721738350272772), 0, 0, 0], [(-5960604920867887), 0, 0], [(-4595222250897016), 0], [(-3544413015902256)]]], r := 4323060974574141, ok := true }, nJu := { p := [[[(-67184845300738013287)]], [[2484106839347580483, 0], [1916310990353847802]], [[(-98740441175021899), 0, 0], [13264727667423961, 0], [(-58760638054359972)]], [[5728424402787050, 0, 0, 0], [91818604066157, 0, 0], [70831494565321, 0], [2629797726415336]], [[(-371080795256891), 0, 0, 0, 0], [635569479001, 0, 0, 0], [3796064818382, 0, 0], [378228694035, 0], [(-131416942215489)]]], r := 178067275537120, ok := true }, Jd1 := { p := [[[(-387615299579721510624)]], [[30814540727839215399, 0], [23771217132904537614]], [[(-2681557297578943194), 0, 0], [(-2082957115361088548), 0], [(-1595800220355142521)]], [[231610961885292285, 0, 0, 0], [178472967352579160, 0, 0], [137679146243418221, 0], [106327663272028208]], [[(-20016652015890168), 0, 0, 0, 0], [(-15443476700545544), 0, 0, 0], [(-11921209841735774), 0, 0], [(-9190444501794032), 0], [(-7088826031804511)]]], r := 8646121949148277, ok := true }, term0 := { p := [[[3595580521247956684122]], [[(-562070561242526945481), 0], [(-396032897595059648070)]], [[70944745743991660199, 0, 0], [65448344891892866572, 0], [37175846231631049047]], [[(-8058150285976710008), 0, 0, 0], [(-8342528282976237580), 0, 0], [(-6218097629523286972), 0], [(-3195253411158932121)]], [[862978864170732703, 0, 0, 0, 0], [953671144320674131, 0, 0, 0], [797209976362288775, 0, 0], [538485301136093351, 0], [260812509833645916]]], r := 624799992280681943, ok := true }, r0 := { p := [[[15825045879149022903]], [[(-1498491750813309581), 10488405212220944778], [(-563055852555367107)]], [[127578771125941267, (-986132771644906403), 1707257701920606827], [37635995603018741, (-376555392374530482)], [38898012070303439]], [[(-10138067544193621), 83537480488133756, (-155870250191594478), (-13421987598730910)], [(-1980516006194657), 25389996898277474, (-63528569605733742)], [(-3146378363922595), 25861328139420723], [(-2345264485794595)]], [[797644088770507, (-6615410721831976), 12928050288945648, 2769425213686708, (-1043762238733077)], [93467696596032, (-1365942113835456), 4424313929782059, (-242907684641230)], [223805900272923, (-2081559751908795), 4263899964959368], [177981969384316, (-1562708226014466)], [150944213836946]]], r := 15051784140437395, ok := true }, r1 := { p := [[[389135834966495414145]], [[(-30999556740397554432), 0], [(-16662100305617637259)]], [[2399134784585786940, 0, 0], [1193995572816026874, 0], [1048580657456726265]], [[(-182589135126880850), 0, 0, 0], [(-73046580901246326), 0, 0], [(-78359671151330961), 0], [(-65120255484570163)]], [[14213362550228242, 0, 0, 0, 0], [4634715592225472, 0, 0, 0], [5145132270756588, 0, 0], [4766730477162960, 0], [4162432928714786]]], r := 68120584931041646, ok := true }, r2 := { p := [[[539077112300419119937]], [[(-57217888413083049084), 26195837946997728519], [(-91365831124396351342)]], [[4967051643967564994, (-2229280508499048523), 201207449589694307], [9022450149497779376, (-1103801528110141880)], [8749908356269745829]], [[(-413557721849424022), 170009148194289794, 8044724667960039, (-4905477992664090)], [(-760497103405541028), 58844312214080005, 15693385458860199], [(-837116138443591229), 68569095517153670], [(-756283286511434410)]], [[34283751965781292, (-13393047731063248), (-511067713530739), 139091503845197, 94936939192042], [62768114034341067, (-4155845621729449), 624742182503028, (-1004475848393049)], [70038613535091612, (-6227710756569479), 1757814670669729], [72624353973351809, (-6562863598609530)], [62460155442885355]]], r := 2715311263335226007, ok := true }, r3 := { p := [[[3212834535120649237733]], [[(-550339536436351118968), 185760064189686219844], [(-545189780939394219505)]], [[70162335609394134264, (-27323381630013273524), 210911076746865261], [91724902531299953852, (-10656561770824398685)], [57033587575261198618]], [[(-8004184217881123738), 3351581158152354812, 73476746711532039, (-14414158463574169)], [(-11805053058550133565), 1749041077564085179, (-49018163476207999)], [(-9797758144669257371), 859864890597211878], [(-5259497226848160821)]], [[860041939728568886, (-380973091568521843), (-653934481735284), (-2958396403532687), 810498131993954], [1360270140083651328, (-234318969052886771), 16789143273101047, (-2005040541917223)], [1273780294481780851, (-137157476260521754), (-2509898937811118)], [906148147763664847, (-52811034921790192)], [445808343330238197]]], r := 738315006760268844743, ok := true }, eta := { p := [[[(-1349654868897326473367)]], [[130035004153803828719, 0], [128358268452542939836]], [[(-11433971085752697130), 0, 0], [(-12507235955095858272), 0], [(-11355106856609399582)]], [[970286437084823441, 0, 0, 0], [1058039936074562843, 0, 0], [1087524807696519848, 0], [932335960555474609]], [[(-81906105830266968), 0, 0, 0, 0], [(-87968644776672122), 0, 0, 0], [(-91291070290436923), 0, 0], [(-88256595221444995), 0], [(-73609070688699838)]]], r := 692339024521932957, 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

theorem region : RegionPosI 4035225266123964416 4611686018427387904 2305843009213693952 4611686018427387904 4323455642275676160 6341068275337658368 :=
  (RegionPosI.split_s 5332261958806667264 (RegionPosI.split_s 4827858800541171712 (RegionPosI.of_check c0 q0 ok_0 4035225266123964416 4611686018427387904 2305843009213693952 4611686018427387904 4323455642275676160 4827858800541171712 (by decide +kernel)) (RegionPosI.of_check c1 q1 ok_1 4035225266123964416 4611686018427387904 2305843009213693952 4611686018427387904 4827858800541171712 5332261958806667264 (by decide +kernel))) (RegionPosI.of_check c2 q2 ok_2 4035225266123964416 4611686018427387904 2305843009213693952 4611686018427387904 5332261958806667264 6341068275337658368 (by decide +kernel)))

end CKLaneC.RSC2.BA_0057

end