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

import Definitions.Def_CK_CKLaneC_RSCell_Staged
import Definitions.Def_CK_CKLaneC_RSCell_RegionI

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

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

namespace CKLaneC.RSC2.BD_0162
open CKLaneC.TM3 CKLaneC.RSCell

noncomputable def c0 : Cell := { bc := 9007199254740992000, bh := 72057594037927936, tc := 9511602413006487552, th := 288230376151711744, sc := 16996584993696251904, sh := 63050394783186944 }
noncomputable def q0 : Cert := { V0 := [[[366404531522775595]], [[(-16010558422538097), 11096848784472067], [2689085992783764]], [[4785529340540, (-484340190259975), (-287027132503)], [(-111587221334074), 81348344448552], [13253669631307]], [[(-57802613581), 108586310481, 37605475106, (-2889536113)], [(-206751956909), (-3363504299167), (-6316104268)], [(-495270579991), 399920039768], [97134900809]], [[42938855, (-1200502263), (-1652205456), 377728862, 220714], [(-1041213235), (-7027772937), 813318524, (-63442223)], [(-3115393682), (-14793410721), (-77421037)], [(-3432691636), 2925901242], [592309916]]], r0 := 2930804916, V1 := [[[710045170234246210]], [[(-30977765229853159), 0], [5202933737156716]], [[6076905812563, 0, 0], [(-214833718778015), 0], [25553873149811]], [[(-64060036919), 0, 0, 0], [(-467824426009), 0, 0], [(-941664679000), 0], [186837593478]], [[34186407, 0, 0, 0, 0], [(-1117031105), 0, 0, 0], [(-6801680999), 0, 0], [(-6468249398), 0], [1134153385]]], r1 := 1456611056, V2 := [[[799430064287006072]], [[(-16064235875302544), 11061246975393633], [(-141684864812215610)]], [[5838618964889, (-481802411587599), (-622967106871)], [(-92698120111391), 97185343342367], [23569136965668]], [[(-58073153021), 64741969697, 66825829356, (-2835043344)], [(-540254167317), (-4369725072885), 99793985604], [(-810376463241), (-891594402579)], [229869622270]], [[45875978, (-1156312271), (-2288732771), 369098794, 474484], [(-960882679), 7096668136, (-8405131189), (-86766669)], [(-8971712903), 37369426777, 1891649453], [(-9274795821), (-7678155345)], [(-652880760)]]], r2 := 15625370068, V3 := [[[1167668607181726241]], [[(-32270104903620824), 22096656601500367], [(-139300738247856035)]], [[17474597306627, (-960877047414092), (-3637375132409)], [(-182308219706270), 199393159248018], [46111476275647]], [[(-196768294136), 36471673592, 417512397182, (-22293077851)], [(-1087533099850), (-9181696142055), 371070598133], [(-1537068251759), (-1723154360966)], [461141689665]], [[168676548, (-1175710944), (-15770478247), 2876118979, 11005837], [(-3649348450), 24364727044, (-29938634710), (-742220382)], [(-19444379070), 70021714828, 7507139905], [(-18706024683), (-14714344987)], [(-1247295391)]]], r3 := 42067906180, Vm := [[[1342852000088493794]], [[(-42446724409987543), 0], [(-114702309423613388)]], [[38469453116350, 0, 0], [(-908413634153409), 0], [2255764870432020]], [[1135581675234, 0, 0, 0], [(-14555820326199), 0, 0], [17663696996283, 0], [192776239940924]], [[36043078169, 0, 0, 0, 0], [(-332991084374), 0, 0, 0], [(-1006943136075), 0, 0], [9120696020029, 0], [14572342417188]]], rm := 86157466812243 }
noncomputable def w0 : Wit := { Z0 := { p := [[[366508844848352992]], [[(-16024235967570970), 11106328631768272], [2691383232754596]], [[5387626133187, (-485582908108212), 0], [(-111883427887522), 81557067659230], [13281861577255]], [[(-66940106857), 163261397975, 0, 0], [(-194133664815), (-3390406905683), 0], [(-498822665603), 402480653856], [97425536832]], [[55843298, (-2028488087), 0, 0, 0], [(-1215500060), (-5882838328), 0, 0], [(-2970971361), (-15115838352), 0], [(-3468440156), 2952288994], [595056601]]], r := 576627677, ok := true }, Z1 := { p := [[[710805032433169440]], [[(-31077306118925517), 0], [5219652330190732]], [[10448729470424, 0, 0], [(-216986041963678), 0], [25758761846797]], [[(-129823237541), 0, 0, 0], [(-376501652974), 0, 0], [(-967413654503), 0], [188946495674]], [[108302153, 0, 0, 0, 0], [(-2357333450), 0, 0, 0], [(-5761883850), 0, 0], [(-6726671818), 0], [1154049166]]], r := 324201508, ok := true }, Z2 := { p := [[[800514918813013170]], [[(-16129707911435770), 11106328631768272], [(-142262321260223720)]], [[7181714920808, (-485582908108212), 0], [(-69803753411592), 81557067659230], [126294241427278]], [[(-68204218844), 163261397975, 0, 0], [(-772115526083), (-3390406905683), 0], [(-2768520940187), 402480653856], [(-5933933824236)]], [[67009453, (-2028488087), 0, 0, 0], [(-727694720), (-5882838328), 0, 0], [(-9282745146), (-15115838352), 0], [(-15446694776), 2952288994], [11094682291]]], r := 1293584710, ok := true }, Z3 := { p := [[[1171055583875401497]], [[(-32551584700166475), 22289397295189021], [(-140515805368888733)]], [[25452438257994, (-979975174596695), 0], [(-116338289432292), 154871210329241], [192332500952977]], [[(-280764941352), 660225760760, 0, 0], [(-2000972818716), (-6098423885542), 0], [(-5317021508589), 684826803351], [(-5568089439211)]], [[423725967, (-8376918212), 0, 0, 0], [(-2384605184), (-24544175287), 0, 0], [(-20558881841), (-20615760762), 0], [(-25010656021), 4758036103], [16171695913]]], r := 2810545740, ok := true }, iE := { p := [[[18517592489158834261]], [[(-4500136271564788), 0], [(-12160561980796703)]], [[76547788271825, 0, 0], [295354020451386, 0], [768340880002091]], [[(-53935444759), 0, 0, 0], [855370009836, 0, 0], [1610880434874, 0], [(-1224372738186)]], [[476422635, 0, 0, 0, 0], [2834546261, 0, 0, 0], [15820988430, 0, 0], [25887947849, 0], [39859783370]]], r := 2609293776, ok := true }, iHu := { p := [[[18581566853724321680]], [[(-9062568041623645), 0], [(-19544075308050072)]], [[156372827857014, 0, 0], [601957801189727, 0], [727258798857923]], [[(-184603322782), 0, 0, 0], [1307634491130, 0, 0], [2820007182586, 0], [(-1851531287800)]], [[1682069592, 0, 0, 0, 0], [10079533150, 0, 0, 0], [37836387780, 0, 0], [46877896076, 0], [36383070553]]], r := 4470497144, ok := true }, T := { p := [[[9511602413006487552]], [[0, 288230376151711744], [0]]], r := 0, ok := true }, E := { p := [[[18376166724705575662]], [[4465767051444920, 0], [12067687230727422]], [[(-74877895720717), 0, 0], [(-287232924674141), 0], [(-754547885313465)]], [[16866199007, 0, 0, 0], [(-1088926842871), 0, 0], [(-2348348517140), 0], [218789446802]], [[(-146148650), 0, 0, 0, 0], [(-855931239), 0, 0, 0], [(-7124522655), 0, 0], [(-3980765287), 0], [(-7305706118)]]], r := 2032622212, ok := true }, de := { p := [[[(-2675826372420518533)]], [[89731616437996800, 0], [193512640249714241]], [[(-30317985411109), 0, 0], [587087129285088, 0], [(-141002896449737)]], [[350281068104, 0, 0, 0], [1781130663751, 0, 0], [3841135499998, 0], [3513243138588]], [[(-348130524), 0, 0, 0, 0], [5403672272, 0, 0, 0], [24604630500, 0, 0], [25131400764, 0], [(-7530043620)]]], r := 1904739923, ok := true }, dde := { p := [[[(-53765953964622246743)]], [[36332242137644801, 0], [78353075329983701]], [[(-629650836460122), 0, 0], [(-2425116070670863), 0], [(-2928380315809029)]], [[834380141734, 0, 0, 0], [(-4676212260688), 0, 0], [(-10084585755337), 0], [8368651848007]], [[(-7650124460), 0, 0, 0, 0], [(-45967035984), 0, 0, 0], [(-167401643734), 0, 0], [(-213783505967), 0], [(-165471761298)]]], r := 40728072371, ok := true }, nJu := { p := [[[(-5351652744841037066)]], [[179463232875993600, 0], [387025280499428482]], [[(-60635970822217), 0, 0], [1174174258570177, 0], [(-282005792899473)]], [[700562136208, 0, 0, 0], [3562261327503, 0, 0], [7682270999997, 0], [7026486277177]], [[(-696261047), 0, 0, 0, 0], [10807344544, 0, 0, 0], [49209261000, 0, 0], [50262801528, 0], [(-15060087239)]]], r := 3809479837, ok := true }, Jd1 := { p := [[[(-107531907929244493486)]], [[72664484275289603, 0], [156706150659967403]], [[(-1259301672920243), 0, 0], [(-4850232141341726), 0], [(-5856760631618057)]], [[1668760283468, 0, 0, 0], [(-9352424521375), 0, 0], [(-20169171510674), 0], [16737303696015]], [[(-15300248920), 0, 0, 0, 0], [(-91934071967), 0, 0, 0], [(-334803287467), 0, 0], [(-427567011933), 0], [(-330943522596)]]], r := 81456144732, ok := true }, term0 := { p := [[[325612877742530833703]], [[(-431566907763836905), 0], [(-845666654917101348)]], [[7763679400625204, 0, 0], [27085837574253835, 0], [29750859642458706]], [[(-15056872384343), 0, 0, 0], [32663987007864, 0, 0], [59497212313100, 0], [(-123769153137762)]], [[143747777240, 0, 0, 0, 0], [807021809316, 0, 0, 0], [2579872515735, 0, 0], [3289250002075, 0], [2390896671267]]], r := 306049584425, ok := true }, r0 := { p := [[[28764358309875055959]], [[(-34713980232985752), 1741695789170632958], [(-39159829878703251)]], [[675468151759522, (-1962460950737325), 26292540249213118], [1214427819193528, (-2394574502439046)], [1074209171176744]], [[(-1018335750264), 37661790356778, (-21180817618819), (-2927080034423)], [6156751610302, 75361914813524, (-37566653959188)], [4502718313136, 64874918638268], [(-3608449439315)]], [[9950668410, (-53208760688), 373256946052, 258150257943, (-21949946744)], [36134480917, 339624894461, 1248055573718, (-38779932681)], [117636735406, 290736838600, 969140247622], [89720784100, (-220778238250)], [52111269285]]], r := 147065544283, ok := true }, r1 := { p := [[[107916721473856660554]], [[(-106468337821513085), 0], [(-150910268084955022)]], [[1988181772063895, 0, 0], [4865743462317047, 0], [4001536144395729]], [[(-2641566082096), 0, 0, 0], [17648519106966, 0, 0], [19934686333324, 0], [(-13924790949201)]], [[25005361132, 0, 0, 0, 0], [114894007593, 0, 0, 0], [398831033284, 0, 0], [362574948266, 0], [192888625757]]], r := 116511445481, ok := true }, r2 := { p := [[[29273472102656937143]], [[(-51398850547383343), 1749560724673512160], [(-252718164573589736)]], [[700834081129063, (-2288077295726723), 26086930924657359], [6758717369151634, (-5098990885865365)], [15822522045772729]], [[(-1316624247398), 37853232351562, (-13407830373379), (-4615486921982)], [(-3948730051997), 180976389621512, 41151997199641], [6630304502350, 91787240294695], [(-50583567844607)]], [[10483869138, (-56065717386), 356234831463, 331151393133, (-21237806589)], [133058212671, 283065794291, (-1318802159240), 504835086617], [651490980538, 1290720404639, (-2427591273469)], [1292509323585, 11974926516], [1235886709638]]], r := 977779552220, ok := true }, r3 := { p := [[[118293793144415527491]], [[(-318344854899069563), 7053424016418565456], [(-951532351414612905)]], [[5251224810614227, (-13808767359355796), 103659442780732236], [29099732551713809, (-21116420089552565)], [44309918663831458]], [[(-12656255046461), 252848310041815, (-3128768057471), (-60033022281579)], [(-13153114591863), 724585324250255, 253092211314055], [19058830095785, 358599702061290], [(-176380571080093)]], [[115524756141, (-411057908776), 391714089246, 4678092571396, (-323178647230)], [881560004761, 2426795030041, (-9353878861556), 3588641348592], [3095089621395, 5457034085694, (-9242233793577)], [4691724506603, 5796695119], [3558805494879]]], r := 8439945209184, ok := true }, eta := { p := [[[(-216168269118572538585)]], [[218643845392342589, 0], [484934013262042320]], [[(-3809488109971945), 0, 0], [(-14709503579243871), 0], [(-20015143408849467)]], [[5717037255441, 0, 0, 0], [(-23473571088519), 0, 0], [(-45148769779887), 0], [70477530666172]], [[(-52648042092), 0, 0, 0, 0], [(-317898268406), 0, 0, 0], [(-1201325592088), 0, 0], [(-1788673212785), 0], [(-1605194318377)]]], r := 52998542046703725, 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 := 9007199254740992000, bh := 72057594037927936, tc := 9511602413006487552, th := 288230376151711744, sc := 17122685783262625792, sh := 63050394783186944 }
noncomputable def q1 : Cert := { V0 := [[[334402095051191352]], [[(-15992108587442083), 10128593154343530], [2465076184449727]], [[4439719262361, (-483920232766215), (-218226369291)], [(-112426780110336), 74593055346189], [12250536471364]], [[(-57471552974), 101396935950, 31294380147, (-2198145950)], [(-213041685186), (-3391869883714), (-4823818624)], [(-507928256728), 369917622078], [90151719959]], [[39833428, (-1196002675), (-1503565530), 314632249, 139820], [(-1055467399), (-7155394327), 680854602, (-48498451)], [(-3213910538), (-15210581515), (-59491155)], [(-3551330439), 2718282414], [554140915]]], r0 := 2859337012, V1 := [[[648113435457372979]], [[(-30954225250834470), 0], [4771386028096578]], [[5693348322132, 0, 0], [(-216718496039102), 0], [23643153813489]], [[(-63795407978), 0, 0, 0], [(-474583102313), 0, 0], [(-969146839767), 0], [173644337767]], [[31975313, 0, 0, 0, 0], [(-1135929068), 0, 0, 0], [(-6939956143), 0, 0], [(-6726366030), 0], [1063354882]]], r1 := 1427696712, V2 := [[[767324483151056528]], [[(-16041576834224965), 10097891872280046], [(-141872429798076889)]], [[5491256110753, (-481557314142890), (-498271122358)], [(-94870751314135), 88473980930636], [21912392834145]], [[(-57718610382), 57808019939, 57969547948, (-2158981043)], [(-546082576759), (-4341786180148), 83649570112], [(-846420620715), (-816627422998)], [211216421607]], [[42766907, (-1155045002), (-2139641760), 307883268, 316381], [(-982025600), 6873404275, (-7737394914), (-65548374)], [(-9051142826), 37598104611, 1576159505], [(-9379326942), (-7030115782)], [(-597310977)]]], r2 := 15460656372, V3 := [[[1103196724276651595]], [[(-32202562435065914), 20175038889568765], [(-139669734094759629)]], [[16297937041995, (-960745464774069), (-2863832152986)], [(-186702305574206), 181126416220338], [42959299540269]], [[(-195468205016), 29271635533, 356828504112, (-17015598724)], [(-1109551004582), (-9085447764065), 313227385536], [(-1615242047190), (-1582345672387)], [423543768120]], [[156368165, (-1223723778), (-14573578106), 2407842775, 7230319], [(-3690518824), 23763411956, (-27887056900), (-558176951)], [(-19644728297), 70789780675, 6257642492], [(-18893926433), (-13496705457)], [(-1145148340)]]], r3 := 41165174236, Vm := [[[1258122128097479192]], [[(-42277970844220050), 0], [(-116580125446280957)]], [[46245225018935, 0, 0], [(-970836585195560), 0], [2286430469967648]], [[1474140359989, 0, 0, 0], [(-16707390756729), 0, 0], [12655563522934, 0], [211951693934328]], [[49427097471, 0, 0, 0, 0], [(-384652825667), 0, 0, 0], [(-1527528565049), 0, 0], [10051875095476, 0], [17562843603858]]], rm := 108441744146277 }
noncomputable def w1 : Wit := { Z0 := { p := [[[334481388776943230]], [[(-16003486990913989), 10135799659907370], [2466830088962213]], [[4987292177866, (-484954151239818), 0], [(-112674607434836), 74752426938248], [12272188103112]], [[(-66510115845), 151130065995, 0, 0], [(-201471046069), (-3414382043480), 0], [(-510923449242), 371884487973], [90376277734]], [[51665016, (-2015458056), 0, 0, 0], [(-1230437516), (-6105183215), 0, 0], [(-3079934569), (-15482528765), 0], [(-3581716315), 2738675082], [556275930]]], r := 570336063, ok := true }, Z1 := { p := [[[648691178234071720]], [[(-31037065679348342), 0], [4784155324047928]], [[9672324223740, 0, 0], [(-218520450782712), 0], [23800607230278]], [[(-128989315578), 0, 0, 0], [(-390731725709), 0, 0], [(-990881840954), 0], [175275205304]], [[100198820, 0, 0, 0, 0], [(-2386303061), 0, 0, 0], [(-5973206437), 0, 0], [(-6946358914), 0], [1078838168]]], r := 318250517, ok := true }, Z2 := { p := [[[768283685274373070]], [[(-16101797392687122), 10135799659907370], [(-142405023136070659)]], [[6774063253230, (-484954151239818), 0], [(-72901118671204), 74752426938248], [120719756997000]], [[(-67685409389), 151130065995, 0, 0], [(-776609928151), (-3414382043480), 0], [(-2806120308942), 371884487973], [(-5965422259400)]], [[62705084, (-2015458056), 0, 0, 0], [(-770519777), (-6105183215), 0, 0], [(-9517976878), (-15482528765), 0], [(-16044390445), 2738675082], [10653250485]]], r := 1301810909, ok := true }, Z3 := { p := [[[1106051984789903350]], [[(-32453130812704332), 20332021017110472], [(-140756505333783907)]], [[23777772827433, (-977434429187081), 0], [(-124371632286272), 142575194311010], [181615031704722]], [[(-277497488700), 610236480764, 0, 0], [(-2015908303134), (-6198091214243), 0], [(-5401047472272), 642216191060], [(-5619647292514)]], [[393260065, (-8287378735), 0, 0, 0], [(-2594305186), (-25292811400), 0, 0], [(-21458503137), (-22003901000), 0], [(-26556455629), 4499400767], [15407431767]]], r := 2832905123, ok := true }, iE := { p := [[[18508897983890339813]], [[(-4194577142320320), 0], [(-11566409637955898)]], [[76235565882232, 0, 0], [298809806474875, 0], [771626393487236]], [[(-50145857876), 0, 0, 0], [872596325239, 0, 0], [1674869477766, 0], [(-1171939755328)]], [[471042908, 0, 0, 0, 0], [2907870902, 0, 0, 0], [16175636588, 0, 0], [26549063039, 0], [40157662570]]], r := 2664667612, ok := true }, iHu := { p := [[[18564065758944331359]], [[(-8439238379975958), 0], [(-18334848183239190)]], [[155305342388011, 0, 0], [607309992113589, 0], [733051561308920]], [[(-171263592728), 0, 0, 0], [1368638313268, 0, 0], [2973464495454, 0], [(-1756253658084)]], [[1653249010, 0, 0, 0, 0], [10256880049, 0, 0, 0], [38900260066, 0, 0], [48413157069, 0], [36832782401]]], r := 4586146795, ok := true }, T := { p := [[[9511602413006487552]], [[0, 288230376151711744], [0]]], r := 0, ok := true }, E := { p := [[[18384798879820469378]], [[4166453195353461, 0], [11488858771630697]], [[(-74780196968023), 0, 0], [(-291599013148517), 0], [(-759273254411494)]], [[15701544737, 0, 0, 0], [(-1094144969054), 0, 0], [(-2377108098480), 0], [210639474995]], [[(-145028990), 0, 0, 0, 0], [(-883506291), 0, 0, 0], [(-7255800665), 0, 0], [(-4170208549), 0], [(-7375624102)]]], r := 2087052764, ok := true }, de := { p := [[[(-2496481614726257054)]], [[89614536932505832, 0], [194693982524221240]], [[(-28224450811385), 0, 0], [594277024620176, 0], [(-133221287923768)]], [[347597528833, 0, 0, 0], [1813950166372, 0, 0], [3940936304312, 0], [3564502074450]], [[(-322832122), 0, 0, 0, 0], [5536837316, 0, 0, 0], [25299562502, 0, 0], [26134240954, 0], [(-7192386146)]]], r := 1980482271, ok := true }, dde := { p := [[[(-53695801530593848087)]], [[33823407695998934, 0], [73483769177250252]], [[(-624827016674771), 0, 0], [(-2444375386886310), 0], [(-2949225139835212)]], [[773746319778, 0, 0, 0], [(-4954174824901), 0, 0], [(-10763298676734), 0], [7934522351708]], [[(-7510218539), 0, 0, 0, 0], [(-46696033253), 0, 0, 0], [(-171992400818), 0, 0], [(-220408387497), 0], [(-167320375428)]]], r := 41757840074, ok := true }, nJu := { p := [[[(-4992963229452514107)]], [[179229073865011665, 0], [389387965048442480]], [[(-56448901622770), 0, 0], [1188554049240353, 0], [(-266442575847536)]], [[695195057667, 0, 0, 0], [3627900332745, 0, 0], [7881872608625, 0], [7129004148900]], [[(-645664243), 0, 0, 0, 0], [11073674633, 0, 0, 0], [50599125005, 0, 0], [52268481909, 0], [(-14384772291)]]], r := 3960964530, ok := true }, Jd1 := { p := [[[(-107391603061187696174)]], [[67646815391997869, 0], [146967538354500504]], [[(-1249654033349542), 0, 0], [(-4888750773772620), 0], [(-5898450279670423)]], [[1547492639556, 0, 0, 0], [(-9908349649801), 0, 0], [(-21526597353468), 0], [15869044703416]], [[(-15020437077), 0, 0, 0, 0], [(-93392066505), 0, 0, 0], [(-343984801635), 0, 0], [(-440816774993), 0], [(-334640750855)]]], r := 83515680140, ok := true }, term0 := { p := [[[324780680478432089698]], [[(-400688300521354955), 0], [(-791357851805359920)]], [[7676760408056373, 0, 0], [27226209722835605, 0], [29880256487659882]], [[(-13920646740664), 0, 0, 0], [37530393988198, 0, 0], [69941861634510, 0], [(-117107560971454)]], [[140356388601, 0, 0, 0, 0], [815328785513, 0, 0, 0], [2643218510559, 0, 0], [3373502046470, 0], [2405968512291]]], r := 312816614945, ok := true }, r0 := { p := [[[28697624233940498769]], [[(-32024010730239152), 1737921096903236546], [(-36706055651022359)]], [[669595462782988, (-1812436023424041), 26251669079250788], [1239493462813904, (-2242475201929825)], [1083690691989595]], [[(-939470538158), 37354723078281, (-19691612914820), (-2434328349334)], [6377337838517, 76745934757502, (-35057754292897)], [4981608291057, 65484125286129], [(-3424633163192)]], [[9768188244, (-49158884234), 371366070932, 234649206410, (-18286078008)], [37402159234, 352448748497, 1260948309567, (-32637243744)], [121845588887, 318630737937, 980452244632], [94142648496, (-209342763513)], [52812736113]]], r := 143984212175, ok := true }, r1 := { p := [[[107711716791429116535]], [[(-98546512919803947), 0], [(-141107261900734807)]], [[1972928953529483, 0, 0], [4937728355072172, 0], [4043017896944420]], [[(-2443286564837), 0, 0, 0], [18346981968011, 0, 0], [21555696897408, 0], [(-13184193048626)]], [[24570491176, 0, 0, 0, 0], [117948792072, 0, 0, 0], [411777491509, 0, 0], [378174694071, 0], [195934204467]]], r := 114843767265, ok := true }, r2 := { p := [[[29173467371905565426]], [[(-48610980048258339), 1745135542640435003], [(-239215461018711645)]], [[693184136837384, (-2137320860130070), 26061539406828151], [6744517719613081, (-4735882002361637)], [15838399889999767]], [[(-1233653666488), 37529040970544, (-11984067986403), (-3976659555806)], [(-3151414255805), 182144477843764, 38551488306749], [9253280400493, 94386935417978], [(-47973460508852)]], [[10261497277, (-52010095828), 355664042550, 307723290802, (-17731666469)], [132738663448, 301042016160, (-1281880983958), 464274123576], [660102272314, 1309259790112, (-2433164394982)], [1317820640249, 6997668254], [1245674058608]]], r := 960024883287, ok := true }, r3 := { p := [[[117678008922791749575]], [[(-297488157421420559), 7026814650254564255], [(-893378443006816812)]], [[5178036472525384, (-12802179362387581), 103654809302969556], [29057705640226145, (-19657442949625501)], [44360497680486484]], [[(-11743679437392), 250477422202983, (-1476649246933), (-51047373742752)], [(-7858307545592), 734442167009248, 234600432392431], [31561441171818, 369592417978740], [(-166886681551694)]], [[112658264332, (-379323415120), 433806506015, 4308222836844, (-271787260666)], [883593731993, 2502322864356, (-9139773192678), 3343223368319], [3156974301519, 5537144900075, (-9296613958007)], [4803460159147, (-8792965199)], [3586065434826]]], r := 8169499491472, ok := true }, eta := { p := [[[(-215746174482894646333)]], [[203472820902413165, 0], [455418559670027516]], [[(-3776441235690468), 0, 0], [(-14807230562865417), 0], [(-20110284592968286)]], [[5299927398737, 0, 0, 0], [(-25394495655870), 0, 0], [(-50011861001612), 0], [66856410332576]], [[(-51643012176), 0, 0, 0, 0], [(-322474203059), 0, 0, 0], [(-1230494773042), 0, 0], [(-1832915706765), 0], [(-1617164037468)]]], r := 73537839199171268, 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 := 9007199254740992000, bh := 72057594037927936, tc := 10088063165309911040, th := 288230376151711744, sc := 16996584993696251904, sh := 63050394783186944 }
noncomputable def q2 : Cert := { V0 := [[[388597057870474706]], [[(-16979085360106631), 11095666008677679], [2851756909857026]], [[4995961185589, (-484185237177646), (-304358945943)], [(-118310911580869), 81322318987589], [14053193828961]], [[(-60102129262), 101779592045, 39870669178, (-2887717365)], [(-220948356816), (-3360153423222), (-6696559557)], [(-524817693291), 399601060307], [102983451433]], [[43981639, (-1098043772), (-1751119035), 377331984, 233967], [(-1081463504), (-7169993046), 862105054, (-63375565)], [(-3323232748), (-14753315827), (-82067391)], [(-3636015976), 2922617622], [627844718]]], r0 := 3016068168, V1 := [[[710045170234246210]], [[(-30977765229853159), 0], [5202933737156716]], [[6076905812563, 0, 0], [(-214833718778015), 0], [25553873149811]], [[(-64060036919), 0, 0, 0], [(-467824426009), 0, 0], [(-941664679000), 0], [186837593478]], [[34186407, 0, 0, 0, 0], [(-1117031105), 0, 0, 0], [(-6801680999), 0, 0], [(-6468249398), 0], [1134153385]]], r1 := 1456611056, V2 := [[[821550043696651307]], [[(-17027570443853194), 11058721101730609], [(-141490095644791450)]], [[5958820138325, (-481530682055487), (-639965878261)], [(-101471097451534), 97583475946654], [21793521052207]], [[(-60284075515), 55395343588, 69038188529, (-2831196967)], [(-525403045319), (-4403205512708), 99271783495], [(-736298510514), (-884018387728)], [214496458689]], [[46102113, (-1053695241), (-2384522805), 368350627, 487100], [(-1033982649), 7752301247, (-8334999491), (-87299710)], [(-8843542808), 36708160886, 1896334183], [(-8626241679), (-7694839859)], [(-600010124)]]], r2 := 15827125968, V3 := [[[1211847192716891722]], [[(-34190165975612221), 22081839939281693], [(-138900473599074006)]], [[17483486305344, (-959172555934678), (-3770866402664)], [(-200790554282439), 200868506350407], [42695231649078]], [[(-198304809072), (-28067452555), 434715296532, (-22203504122)], [(-1036843071169), (-9300231192762), 366595843465], [(-1399642363723), (-1693072874142)], [431656170965]], [[155181241, (-354513227), (-16497639388), 2858073144, 11386921], [(-3835471319), 26306047833, (-29327777332), (-749329946)], [(-19006677896), 67402560479, 7533227139], [(-17485586319), (-14769889954)], [(-1120106316)]]], r3 := 43007262612, Vm := [[[1342852000088493794]], [[(-42446724409987543), 0], [(-114702309423613388)]], [[38469453116350, 0, 0], [(-908413634153409), 0], [2255764870432020]], [[1135581675234, 0, 0, 0], [(-14555820326199), 0, 0], [17663696996283, 0], [192776239940924]], [[36043078169, 0, 0, 0, 0], [(-332991084374), 0, 0, 0], [(-1006943136075), 0, 0], [9120696020029, 0], [14572342417188]]], rm := 86157466812243 }
noncomputable def w2 : Wit := { Z0 := { p := [[[388721502111889537]], [[(-16995401783787392), 11106328631768272], [2854497368073056]], [[5714148929138, (-485582908108212), 0], [(-118664241698887), 81557067659230], [14086822884967]], [[(-70997083030), 163261397975, 0, 0], [(-205899341471), (-3390406905683), 0], [(-529054342306), 402480653856], [103330114822]], [[59227740, (-2028488087), 0, 0, 0], [(-1289166731), (-5882838328), 0, 0], [(-3151030231), (-15115838352), 0], [(-3678648650), 2952288994], [631120637]]], r := 586758975, ok := true }, Z1 := { p := [[[710805032433169440]], [[(-31077306118925517), 0], [5219652330190732]], [[10448729470424, 0, 0], [(-216986041963678), 0], [25758761846797]], [[(-129823237541), 0, 0, 0], [(-376501652974), 0, 0], [(-967413654503), 0], [188946495674]], [[108302153, 0, 0, 0, 0], [(-2357333450), 0, 0, 0], [(-5761883850), 0, 0], [(-6726671818), 0], [1154049166]]], r := 324201508, ok := true }, Z2 := { p := [[[822727576076549715]], [[(-17100873727652192), 11106328631768272], [(-142099207124905259)]], [[7508237716759, (-485582908108212), 0], [(-76584567222957), 81557067659230], [127099202734990]], [[(-72261195017), 163261397975, 0, 0], [(-783881202739), (-3390406905683), 0], [(-2798752616891), 402480653856], [(-5928029246246)]], [[70393895, (-2028488087), 0, 0, 0], [(-801361391), (-5882838328), 0, 0], [(-9462804016), (-15115838352), 0], [(-15656903270), 2952288994], [11130746327]]], r := 1302036859, ok := true }, Z3 := { p := [[[1215634378465779540]], [[(-34511535049359864), 22289397295189021], [(-140206062948230251)]], [[26772889779515, (-979975174596695), 0], [(-128535137203375), 154871210329241], [193702154559680]], [[(-297518777775), 660225760760, 0, 0], [(-2050061169290), (-6098423885542), 0], [(-5358253030113), 684826803351], [(-5558573367003)]], [[447017026, (-8376918212), 0, 0, 0], [(-2630851105), (-24544175287), 0, 0], [(-21239474430), (-20615760762), 0], [(-25257810603), 4758036103], [16223446186]]], r := 2838217761, ok := true }, iE := { p := [[[18517592489158834261]], [[(-4500136271564788), 0], [(-12160561980796703)]], [[76547788271825, 0, 0], [295354020451386, 0], [768340880002091]], [[(-53935444759), 0, 0, 0], [855370009836, 0, 0], [1610880434874, 0], [(-1224372738186)]], [[476422635, 0, 0, 0, 0], [2834546261, 0, 0, 0], [15820988430, 0, 0], [25887947849, 0], [39859783370]]], r := 2609293776, ok := true }, iHu := { p := [[[18581566853724321680]], [[(-9062568041623645), 0], [(-19544075308050072)]], [[156372827857014, 0, 0], [601957801189727, 0], [727258798857923]], [[(-184603322782), 0, 0, 0], [1307634491130, 0, 0], [2820007182586, 0], [(-1851531287800)]], [[1682069592, 0, 0, 0, 0], [10079533150, 0, 0, 0], [37836387780, 0, 0], [46877896076, 0], [36383070553]]], r := 4470497144, ok := true }, T := { p := [[[10088063165309911040]], [[0, 288230376151711744], [0]]], r := 0, ok := true }, E := { p := [[[18376166724705575662]], [[4465767051444920, 0], [12067687230727422]], [[(-74877895720717), 0, 0], [(-287232924674141), 0], [(-754547885313465)]], [[16866199007, 0, 0, 0], [(-1088926842871), 0, 0], [(-2348348517140), 0], [218789446802]], [[(-146148650), 0, 0, 0, 0], [(-855931239), 0, 0, 0], [(-7124522655), 0, 0], [(-3980765287), 0], [(-7305706118)]]], r := 2032622212, ok := true }, de := { p := [[[(-2675826372420518533)]], [[89731616437996800, 0], [193512640249714241]], [[(-30317985411109), 0, 0], [587087129285088, 0], [(-141002896449737)]], [[350281068104, 0, 0, 0], [1781130663751, 0, 0], [3841135499998, 0], [3513243138588]], [[(-348130524), 0, 0, 0, 0], [5403672272, 0, 0, 0], [24604630500, 0, 0], [25131400764, 0], [(-7530043620)]]], r := 1904739923, ok := true }, dde := { p := [[[(-53765953964622246743)]], [[36332242137644801, 0], [78353075329983701]], [[(-629650836460122), 0, 0], [(-2425116070670863), 0], [(-2928380315809029)]], [[834380141734, 0, 0, 0], [(-4676212260688), 0, 0], [(-10084585755337), 0], [8368651848007]], [[(-7650124460), 0, 0, 0, 0], [(-45967035984), 0, 0, 0], [(-167401643734), 0, 0], [(-213783505967), 0], [(-165471761298)]]], r := 40728072371, ok := true }, nJu := { p := [[[(-5351652744841037066)]], [[179463232875993600, 0], [387025280499428482]], [[(-60635970822217), 0, 0], [1174174258570177, 0], [(-282005792899473)]], [[700562136208, 0, 0, 0], [3562261327503, 0, 0], [7682270999997, 0], [7026486277177]], [[(-696261047), 0, 0, 0, 0], [10807344544, 0, 0, 0], [49209261000, 0, 0], [50262801528, 0], [(-15060087239)]]], r := 3809479837, ok := true }, Jd1 := { p := [[[(-107531907929244493486)]], [[72664484275289603, 0], [156706150659967403]], [[(-1259301672920243), 0, 0], [(-4850232141341726), 0], [(-5856760631618057)]], [[1668760283468, 0, 0, 0], [(-9352424521375), 0, 0], [(-20169171510674), 0], [16737303696015]], [[(-15300248920), 0, 0, 0, 0], [(-91934071967), 0, 0, 0], [(-334803287467), 0, 0], [(-427567011933), 0], [(-330943522596)]]], r := 81456144732, ok := true }, term0 := { p := [[[325612877742530833703]], [[(-431566907763836905), 0], [(-845666654917101348)]], [[7763679400625204, 0, 0], [27085837574253835, 0], [29750859642458706]], [[(-15056872384343), 0, 0, 0], [32663987007864, 0, 0], [59497212313100, 0], [(-123769153137762)]], [[143747777240, 0, 0, 0, 0], [807021809316, 0, 0, 0], [2579872515735, 0, 0], [3289250002075, 0], [2390896671267]]], r := 306049584425, ok := true }, r0 := { p := [[[32352896281505406374]], [[(-38721529566737127), 1846830123138560023], [(-44099560335332349)]], [[752236794299909, (-2044025157493333), 26274451301036061], [1370169758992371, (-2545315668521616)], [1207832194191761]], [[(-1125955390372), 39082533432450, (-19585985216631), (-3102513426258)], [6848105601032, 80393153000258, (-37806224521605)], [5106368087577, 68746392442579], [(-4063919919294)]], [[10981522741, (-54360876705), 336779207985, 273450744611, (-21907998126)], [40447684276, 351487943545, 1267747436295, (-41075363283)], [131690969918, 313044849107, 966572361812], [101275070800, (-234707769209)], [58576366741]]], r := 160185613330, ok := true }, r1 := { p := [[[107916721473856660554]], [[(-106468337821513085), 0], [(-150910268084955022)]], [[1988181772063895, 0, 0], [4865743462317047, 0], [4001536144395729]], [[(-2641566082096), 0, 0, 0], [17648519106966, 0, 0], [19934686333324, 0], [(-13924790949201)]], [[25005361132, 0, 0, 0, 0], [114894007593, 0, 0, 0], [398831033284, 0, 0], [362574948266, 0], [192888625757]]], r := 116511445481, ok := true }, r2 := { p := [[[32876904012231413439]], [[(-56025957994467740), 1853852383492625767], [(-262747508836947898)]], [[777917723632935, (-2337676308974672), 26058728870024882], [7115234760594602, (-4928343211021748)], [15996436130968001]], [[(-1429073561569), 39206221683377, (-11377075803526), (-4785101497217)], [(-3345764632333), 175461356154939, 44167240546001], [9198743511434, 82151918854009], [(-50572040515492)]], [[11514747787, (-56334926674), 319952648024, 345751789075, (-21165463121)], [138809222186, 319580641470, (-1438269887865), 500235428388], [660025614562, 1276450907026, (-2389980600416)], [1287738543069, (-771464612)], [1238437548842]]], r := 1045462623670, ok := true }, r3 := { p := [[[132814793524586875234]], [[(-345937055596013631), 7467331077711087170], [(-992724285224242053)]], [[5757737235949163, (-13764297525203011), 103291516564052174], [30510550222914691, (-20061331068717084)], [44990585790076719]], [[(-13447918358437), 253285016483980, 25574492131282, (-62604306868651)], [(-8093943431672), 685772249894944, 274366035930431], [29843096962890, 322286750082050], [(-176439823514041)]], [[123236800022, (-379993600783), (-176906699761), 4888896849469, (-319621388027)], [904242327353, 2625051723826, (-10044009095383), 3502379486216], [3132143882480, 5315519571016, (-8913253417802)], [4680273249148, (-67217333503)], [3571512381763]]], r := 9213778766676, ok := true }, eta := { p := [[[(-216168269118572538585)]], [[218643845392342589, 0], [484934013262042320]], [[(-3809488109971945), 0, 0], [(-14709503579243871), 0], [(-20015143408849467)]], [[5717037255441, 0, 0, 0], [(-23473571088519), 0, 0], [(-45148769779887), 0], [70477530666172]], [[(-52648042092), 0, 0, 0, 0], [(-317898268406), 0, 0, 0], [(-1201325592088), 0, 0], [(-1788673212785), 0], [(-1605194318377)]]], r := 52998542046703725, 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 := 9007199254740992000, bh := 72057594037927936, tc := 10088063165309911040, th := 288230376151711744, sc := 17122685783262625792, sh := 63050394783186944 }
noncomputable def q3 : Cert := { V0 := [[[354658390871497741]], [[(-16959821358936767), 10127693875656590], [2614242611963394]], [[4636378553024, (-483791280743525), (-231411821961)], [(-119207741890486), 74573178257540], [12990128980965]], [[(-59762969825), 95202221350, 33181355963, (-2196993731)], [(-227481787151), (-3389064621986), (-5114683278)], [(-538315905199), 369672503378], [95585770266]], [[40815411, (-1094447419), (-1593765417), 314357017, 148230], [(-1096452868), (-7285966198), 721766223, (-48456026)], [(-3426360233), (-15176739619), (-63067363)], [(-3762550180), 2715743275], [587443095]]], r0 := 2941232240, V1 := [[[648113435457372979]], [[(-30954225250834470), 0], [4771386028096578]], [[5693348322132, 0, 0], [(-216718496039102), 0], [23643153813489]], [[(-63795407978), 0, 0, 0], [(-474583102313), 0, 0], [(-969146839767), 0], [173644337767]], [[31975313, 0, 0, 0, 0], [(-1135929068), 0, 0, 0], [(-6939956143), 0, 0], [(-6726366030), 0], [1063354882]]], r1 := 1427696712, V2 := [[[787518256544366698]], [[(-17004457122329855), 10095872890206641], [(-141695147763074926)]], [[5598196761950, (-481321743509033), (-511217351157)], [(-103585196233359), 88807791125803], [20285447542458]], [[(-59927931172), 49074265658, 59815225884, (-2156417856)], [(-531666214072), (-4372620159558), 83255152203], [(-771826904734), (-810315427062)], [197141881000]], [[42941138, (-1053359251), (-2227190011), 307340175, 324409], [(-1053851320), 7541022491, (-7679525721), (-65923641)], [(-8921402337), 36995294782, 1579821948], [(-8729168932), (-7044296306)], [(-549794670)]]], r2 := 15657896296, V3 := [[[1143535210718856987]], [[(-34122606813418869), 20163379607102959], [(-139306232828492718)]], [[16297290724452, (-959289307862540), (-2965750257959)], [(-204984082481673), 182372607064361], [39819667762475]], [[(-197108861915), (-30364468350), 371237033093, (-16956777058)], [(-1059954419817), (-9195994827275), 309862925193], [(-1476049698585), (-1557271868749)], [396501197084]], [[143823086, (-410472152), (-15243346833), 2394924309, 7474726], [(-3868862488), 25815953130, (-27385585887), (-563288213)], [(-19198945158), 68401034103, 6278997496], [(-17671031709), (-13544881886)], [(-1031900135)]]], r3 := 42081635172, Vm := [[[1258122128097479192]], [[(-42277970844220050), 0], [(-116580125446280957)]], [[46245225018935, 0, 0], [(-970836585195560), 0], [2286430469967648]], [[1474140359989, 0, 0, 0], [(-16707390756729), 0, 0], [12655563522934, 0], [211951693934328]], [[49427097471, 0, 0, 0, 0], [(-384652825667), 0, 0, 0], [(-1527528565049), 0, 0], [10051875095476, 0], [17562843603858]]], rm := 108441744146277 }
noncomputable def w3 : Wit := { Z0 := { p := [[[354752988096757972]], [[(-16973395293393625), 10135799659907370], [2616334942838710]], [[5289552309857, (-484954151239818), 0], [(-119503371521796), 74752426938248], [13015957079058]], [[(-70541031957), 151130065995, 0, 0], [(-213681412497), (-3414382043480), 0], [(-541888506772), 371884487973], [95853627900]], [[54796229, (-2015458056), 0, 0, 0], [(-1305009487), (-6105183215), 0, 0], [(-3266597271), (-15482528765), 0], [(-3798790031), 2738675082], [589989623]]], r := 580281394, ok := true }, Z1 := { p := [[[648691178234071720]], [[(-31037065679348342), 0], [4784155324047928]], [[9672324223740, 0, 0], [(-218520450782712), 0], [23800607230278]], [[(-128989315578), 0, 0, 0], [(-390731725709), 0, 0], [(-990881840954), 0], [175275205304]], [[100198820, 0, 0, 0, 0], [(-2386303061), 0, 0, 0], [(-5973206437), 0, 0], [(-6946358914), 0], [1078838168]]], r := 318250517, ok := true }, Z2 := { p := [[[788555284594187811]], [[(-17071705695166757), 10135799659907370], [(-142255518282194161)]], [[7076323385222, (-484954151239818), 0], [(-79729882758163), 74752426938248], [121463525972946]], [[(-71716325501), 151130065995, 0, 0], [(-788820294580), (-3414382043480), 0], [(-2837085366472), 371884487973], [(-5959944909234)]], [[65836297, (-2015458056), 0, 0, 0], [(-845091748), (-6105183215), 0, 0], [(-9704639579), (-15482528765), 0], [(-16261464161), 2738675082], [10686964178]]], r := 1310197920, ok := true }, Z3 := { p := [[[1146716026824124294]], [[(-34407999671078492), 20332021017110472], [(-140471354945161886)]], [[24998245788961, (-977434429187081), 0], [(-136767814714756), 142575194311010], [182899464086843]], [[(-294072246170), 610236480764, 0, 0], [(-2066493925934), (-6198091214243), 0], [(-5445055274272), 642216191060], [(-5610648490979)]], [[414745644, (-8287378735), 0, 0, 0], [(-2847195951), (-25292811400), 0, 0], [(-22166245026), (-22003901000), 0], [(-26826816091), 4499400767], [15457336720]]], r := 2860505651, ok := true }, iE := { p := [[[18508897983890339813]], [[(-4194577142320320), 0], [(-11566409637955898)]], [[76235565882232, 0, 0], [298809806474875, 0], [771626393487236]], [[(-50145857876), 0, 0, 0], [872596325239, 0, 0], [1674869477766, 0], [(-1171939755328)]], [[471042908, 0, 0, 0, 0], [2907870902, 0, 0, 0], [16175636588, 0, 0], [26549063039, 0], [40157662570]]], r := 2664667612, ok := true }, iHu := { p := [[[18564065758944331359]], [[(-8439238379975958), 0], [(-18334848183239190)]], [[155305342388011, 0, 0], [607309992113589, 0], [733051561308920]], [[(-171263592728), 0, 0, 0], [1368638313268, 0, 0], [2973464495454, 0], [(-1756253658084)]], [[1653249010, 0, 0, 0, 0], [10256880049, 0, 0, 0], [38900260066, 0, 0], [48413157069, 0], [36832782401]]], r := 4586146795, ok := true }, T := { p := [[[10088063165309911040]], [[0, 288230376151711744], [0]]], r := 0, ok := true }, E := { p := [[[18384798879820469378]], [[4166453195353461, 0], [11488858771630697]], [[(-74780196968023), 0, 0], [(-291599013148517), 0], [(-759273254411494)]], [[15701544737, 0, 0, 0], [(-1094144969054), 0, 0], [(-2377108098480), 0], [210639474995]], [[(-145028990), 0, 0, 0, 0], [(-883506291), 0, 0, 0], [(-7255800665), 0, 0], [(-4170208549), 0], [(-7375624102)]]], r := 2087052764, ok := true }, de := { p := [[[(-2496481614726257054)]], [[89614536932505832, 0], [194693982524221240]], [[(-28224450811385), 0, 0], [594277024620176, 0], [(-133221287923768)]], [[347597528833, 0, 0, 0], [1813950166372, 0, 0], [3940936304312, 0], [3564502074450]], [[(-322832122), 0, 0, 0, 0], [5536837316, 0, 0, 0], [25299562502, 0, 0], [26134240954, 0], [(-7192386146)]]], r := 1980482271, ok := true }, dde := { p := [[[(-53695801530593848087)]], [[33823407695998934, 0], [73483769177250252]], [[(-624827016674771), 0, 0], [(-2444375386886310), 0], [(-2949225139835212)]], [[773746319778, 0, 0, 0], [(-4954174824901), 0, 0], [(-10763298676734), 0], [7934522351708]], [[(-7510218539), 0, 0, 0, 0], [(-46696033253), 0, 0, 0], [(-171992400818), 0, 0], [(-220408387497), 0], [(-167320375428)]]], r := 41757840074, ok := true }, nJu := { p := [[[(-4992963229452514107)]], [[179229073865011665, 0], [389387965048442480]], [[(-56448901622770), 0, 0], [1188554049240353, 0], [(-266442575847536)]], [[695195057667, 0, 0, 0], [3627900332745, 0, 0], [7881872608625, 0], [7129004148900]], [[(-645664243), 0, 0, 0, 0], [11073674633, 0, 0, 0], [50599125005, 0, 0], [52268481909, 0], [(-14384772291)]]], r := 3960964530, ok := true }, Jd1 := { p := [[[(-107391603061187696174)]], [[67646815391997869, 0], [146967538354500504]], [[(-1249654033349542), 0, 0], [(-4888750773772620), 0], [(-5898450279670423)]], [[1547492639556, 0, 0, 0], [(-9908349649801), 0, 0], [(-21526597353468), 0], [15869044703416]], [[(-15020437077), 0, 0, 0, 0], [(-93392066505), 0, 0, 0], [(-343984801635), 0, 0], [(-440816774993), 0], [(-334640750855)]]], r := 83515680140, ok := true }, term0 := { p := [[[324780680478432089698]], [[(-400688300521354955), 0], [(-791357851805359920)]], [[7676760408056373, 0, 0], [27226209722835605, 0], [29880256487659882]], [[(-13920646740664), 0, 0, 0], [37530393988198, 0, 0], [69941861634510, 0], [(-117107560971454)]], [[140356388601, 0, 0, 0, 0], [815328785513, 0, 0, 0], [2643218510559, 0, 0], [3373502046470, 0], [2405968512291]]], r := 312816614945, ok := true }, r0 := { p := [[[32278453336951197993]], [[(-35725744088922316), 1842897976354164583], [(-41331502053303591)]], [[745742981828451, (-1888330801093807), 26236624472568890], [1398053084391947, (-2383105631331895)], [1218577881429158]], [[(-1038915929994), 38768764963556, (-18241816126010), (-2580501769322)], [7094952903994, 81825838053168, (-35259400109997)], [5642453978254, 69401608299184], [(-3856464529753)]], [[10781141619, (-50240582086), 335319887776, 248608957854, (-18256996600)], [41843532839, 364919008841, 1279175036021, (-34576939320)], [136393396936, 342339027436, 978268474192], [106233069529, (-222501969037)], [59371141348]]], r := 156771388583, ok := true }, r1 := { p := [[[107711716791429116535]], [[(-98546512919803947), 0], [(-141107261900734807)]], [[1972928953529483, 0, 0], [4937728355072172, 0], [4043017896944420]], [[(-2443286564837), 0, 0, 0], [18346981968011, 0, 0], [21555696897408, 0], [(-13184193048626)]], [[24570491176, 0, 0, 0, 0], [117948792072, 0, 0, 0], [411777491509, 0, 0], [378174694071, 0], [195934204467]]], r := 114843767265, ok := true }, r2 := { p := [[[32767952517996328806]], [[(-52931069476348266), 1849333413354396368], [(-248529312368125965)]], [[769617677766014, (-2181510911088869), 26037254304771557], [7103516508523229, (-4576119751349235)], [16017486100904523]], [[(-1337928849759), 38880591766622, (-10097589759887), (-4118304727522)], [(-2513548684135), 176773384078801, 41325876932138], [11857524465651, 84721850437710], [(-47970968570788)]], [[11274395925, (-52220321775), 319802198848, 321090984686, (-17679364962)], [138621934762, 336501742160, (-1403270805192), 460513868498], [669472976087, 1293752695060, (-2399302162703)], [1313561260609, (-4805766024)], [1248050147057]]], r := 1026362917677, ok := true }, r3 := { p := [[[132145844740962765533]], [[(-323063562573572635), 7440812641903653316], [(-931728320622238043)]], [[5679983028976690, (-12755599221341210), 103342022316930784], [30489037604291153, (-18679201252480984)], [45062886903551573]], [[(-12474131984440), 251093563188959, 24962846314612, (-53211566355478)], [(-2658973172683), 696400779112920, 254450429519650], [42501965828042, 332993119706755], [(-166967616013560)]], [[120250630099, (-350565214908), (-129526796818), 4504347232115, (-269245853441)], [907635190080, 2689871686865, (-9873285935802), 3273237599793], [3198070677376, 5392079899884, (-9002148435653)], [4793264822779, (-74189951672)], [3597687755491]]], r := 8919925677825, ok := true }, eta := { p := [[[(-215746174482894646333)]], [[203472820902413165, 0], [455418559670027516]], [[(-3776441235690468), 0, 0], [(-14807230562865417), 0], [(-20110284592968286)]], [[5299927398737, 0, 0, 0], [(-25394495655870), 0, 0], [(-50011861001612), 0], [66856410332576]], [[(-51643012176), 0, 0, 0, 0], [(-322474203059), 0, 0, 0], [(-1230494773042), 0, 0], [(-1832915706765), 0], [(-1617164037468)]]], r := 73537839199171268, 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

theorem region : RegionPosI 8935141660703064064 9223372036854775808 9223372036854775808 10376293541461622784 16933534598913064960 17437937757178560512 :=
  (RegionPosI.split_s 17185736178045812736 (RegionPosI.split_t 9799832789158199296 (RegionPosI.split_s 17059635388479438848 (RegionPosI.split_b 9079256848778919936 (RegionPosI.of_check c0 q0 ok_0 8935141660703064064 9079256848778919936 9223372036854775808 9799832789158199296 16933534598913064960 17059635388479438848 (by decide +kernel)) (RegionPosI.excl 9079256848778919936 9223372036854775808 9223372036854775808 9799832789158199296 16933534598913064960 17059635388479438848 (by decide +kernel))) (RegionPosI.split_b 9079256848778919936 (RegionPosI.of_check c1 q1 ok_1 8935141660703064064 9079256848778919936 9223372036854775808 9799832789158199296 17059635388479438848 17185736178045812736 (by decide +kernel)) (RegionPosI.excl 9079256848778919936 9223372036854775808 9223372036854775808 9799832789158199296 17059635388479438848 17185736178045812736 (by decide +kernel)))) (RegionPosI.split_s 17059635388479438848 (RegionPosI.split_b 9079256848778919936 (RegionPosI.of_check c2 q2 ok_2 8935141660703064064 9079256848778919936 9799832789158199296 10376293541461622784 16933534598913064960 17059635388479438848 (by decide +kernel)) (RegionPosI.excl 9079256848778919936 9223372036854775808 9799832789158199296 10376293541461622784 16933534598913064960 17059635388479438848 (by decide +kernel))) (RegionPosI.split_b 9079256848778919936 (RegionPosI.of_check c3 q3 ok_3 8935141660703064064 9079256848778919936 9799832789158199296 10376293541461622784 17059635388479438848 17185736178045812736 (by decide +kernel)) (RegionPosI.excl 9079256848778919936 9223372036854775808 9799832789158199296 10376293541461622784 17059635388479438848 17185736178045812736 (by decide +kernel))))) (RegionPosI.excl 8935141660703064064 9223372036854775808 9223372036854775808 10376293541461622784 17185736178045812736 17437937757178560512 (by decide +kernel)))

end CKLaneC.RSC2.BD_0162

end