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

import Definitions.Def_CK_CKLaneC_RSCell_Staged
import Definitions.Def_CK_CKLaneC_RSCell_RegionI

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

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

namespace CKLaneC.RSC2.S09_0013
open CKLaneC.TM3 CKLaneC.RSCell

noncomputable def c0 : Cell := { bc := 468374361246531584, bh := 36028797018963968, tc := 2305843009213693952, th := 2305843009213693952, sc := 3746994889972252672, sh := 288230376151711744 }
noncomputable def q0 : Cert := { V0 := [[[429165283809515769]], [[(-14351172253440966), 428830227623500161], [6763884126149336]], [[241977712075798, (-14317564391420280), (-502121599049676)], [(-232240550401911), 6748044327112638], [(-150666287459724)]], [[(-5910750654085), 240287599252399, 50334449816114, (-166603497029279)], [4799012775918, (-230637698321177), (-23723245745871)], [5060214002174, (-150563010826674)], [6766882408087]], [[186121581043, (-5846518506452), (-2528694366754), 16649423363607, 576441427180], [(-151580230309), 4715876559030, 2398152404472, (-7847078162669)], [(-89852922078), 5050245520582, 155251569703], [(-227796749725), 6760844179660], [(-356380123712)]]], r0 := 182177104839719, V1 := [[[3352380107341487774]], [[(-106912494211067458), 0], [50389174466767678]], [[1556526431355822, 0, 0], [(-1498109747481428), 0], [(-1177101962378759)]], [[(-33734067762520), 0, 0, 0], [21046338990443, 0, 0], [37615786537983, 0], [52638124168185]], [[1028843594563, 0, 0, 0, 0], [(-572787430506), 0, 0, 0], [(-580179849910), 0, 0], [(-1674894232265), 0], [(-2776691089071)]]], r1 := 140648436201428, V2 := [[[17902799454930884710]], [[(-9039845590651187), 1726957935855119], [(-42274446785863171)]], [[52775567497159, (-4813165259157), (-5060700438401)], [(-721338963743874), 275002284834156], [(-48749459072121)]], [[(-1444621597003), (-739631494538), 113547376236, 14338963081], [5195395307018, (-742643947818), (-1212660053110)], [(-1333335450482), 11591292698897], [(-640764781582)]], [[57954311182, 7928865833, 1898641982, (-605530202), (-39834712)], [(-135550986947), (-122325228112), 27299129268, 4578978015], [72885676194, (-32614836398), (-99821826474)], [22822561170, 49472196478], [13810681056]]], r2 := 38085290468623, V3 := [[[18248134556077913142]], [[(-15126464100724062), 1238944026799828], [(-15963638948395740)]], [[12375740876795, 71906821972703, (-7217989833579)], [(-1203826494717647), 201257857577645], [(-55923755523682)]], [[25458754506, (-1896751955674), (-282904937294), 40917608269], [1987418272830, 11597643620389, (-1759369438368)], [(-3264208048901), 8960772915238], [(-238498310223)]], [[(-873827731), (-2460854176), 19351953772, 818013464, (-228441287)], [4181486179, (-315108172305), (-68284678257), 13284902719], [86200214745, 504575726437, (-149773075182)], [(-12060367374), 64465063455], [(-145599749)]]], r3 := 168199047641683, Vm := [[[17915800238347586336]], [[(-9111299149891178), 0], [(-40204729814867336)]], [[48174256013202, 0, 0], [(-732606380566876), 0], [37930309207591]], [[(-1403301864302), 0, 0, 0], [4434078152535, 0, 0], [(-1805539919713), 0], [(-330318434874)]], [[56784951960, 0, 0, 0, 0], [(-127942417593), 0, 0, 0], [38208157730, 0, 0], [20217846153, 0], [12775233632]]], rm := 8469870226929 }
noncomputable def w0 : Wit := { Z0 := { p := [[[429332927668099607]], [[(-14367995542628949), 429332927668099607], [6771813149415081]], [[242824389826385, (-14367995542628949), 0], [(-233043510349273), 6771813149415081], [(-150717841357515)]], [[(-5942961689795), 242824389826385, 0, 0], [4840711102852, (-233043510349273), 0], [5065183636210, (-150717841357515)], [6769902370620]], [[187282574731, (-5942961689795), 0, 0, 0], [(-153267094378), 4840711102852, 0, 0], [(-90068468774), 5065183636210, 0], [(-228097492472), 6769902370620], [(-356529617800)]]], r := 42403990904622, ok := true }, Z1 := { p := [[[3434663421344796858]], [[(-114943964341031585), 0], [54174505195320654]], [[1942595118611083, 0, 0], [(-1864348082794179), 0], [(-1205742730860117)]], [[(-47543693518359), 0, 0, 0], [38725688822820, 0, 0], [40521469089681, 0], [54159218964965]], [[1498260597849, 0, 0, 0, 0], [(-1226136755017), 0, 0, 0], [(-720547750191), 0, 0], [(-1824779939775), 0], [(-2852236942393)]]], r := 37537764492291, ok := true }, Z2 := { p := [[[161563225925418569403]], [[(-2247364161293293032), 429332927668099607], [(-10509701265617031842)]], [[47593545980355061, (-14367995542628949), 0], [143095300525084274, 6771813149415081], [741783472884758131]], [[(-1307963568806178), 242824389826385, 0, 0], [(-2753444122146338), (-233043510349273), 0], [(-10073453392488879), (-150717841357515)], [(-54291480943474785)]], [[44946905113188, (-5942961689795), 0, 0, 0], [68992894087419, 4840711102852, 0, 0], [189368941561817, 5065183636210, 0], [735996146583364, 6769902370620], [4032165997161097]]], r := 1149971465143607, ok := true }, Z3 := { p := [[[377642461669618386914]], [[(-24439689428081750308), 2001750510373100124], [(-25792305157564629427)]], [[1758380496983838939, (-168588198945373638), 0], [1724180824755130555, 24642619552180522], [1845776437623733299]], [[(-129787996379841820), 11843159806834545, 0, 0], [(-125132884573596726), (-1767137759256644), 0], [(-124699091802116543), (-641974570293221)], [(-136076968272968893)]], [[9692471357191512, (-869485900775800), 0, 0, 0], [9283022084606903, 111991439500485, 0, 0], [9082398386268237, 50021043574745, 0], [9243913434191883, 28938655385211], [10156684100686092]]], r := 34455993181238785, ok := true }, iE := { p := [[[169754224721909959950]], [[(-2352456865976008253), 0], [(-10380505693178191162)]], [[49883887766153667, 0, 0], [141315223074464937, 0], [738908012891800059]], [[(-1371676030542362), 0, 0, 0], [(-2700563907595222), 0, 0], [(-10036154454376781), 0], [(-54162321825698040)]], [[47154170246276, 0, 0, 0, 0], [67200581201636, 0, 0, 0], [188481245515375, 0, 0], [734309679131841, 0], [4025363971315636]]], r := 1143823658768195, ok := true }, iHu := { p := [[[395736716282990919416]], [[(-25569555204357664311), 0], [(-25569555204357664311)]], [[1839973491017749485, 0, 0], [1713058120161833163, 0], [1839973491017749485]], [[(-135815385525271198), 0, 0, 0], [(-124373311803848298), 0, 0], [(-124373311803848298), 0], [(-135815385525271198)]], [[10142757822799810, 0, 0, 0, 0], [9229019246908064, 0, 0, 0], [9059939954829253, 0, 0], [9229019246908064, 0], [10142757822799810]]], r := 34992876432954105, ok := true }, T := { p := [[[2305843009213693952]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[2004559046930268564]], [[27779212569999692, 0], [122579197266280445]], [[(-204093884748678), 0, 0], [1728674735887236, 0], [(-1229723073730049)]], [[5206046655829, 0, 0, 0], [(-15780919224622), 0, 0], [(-15780919224622), 0], [30819107949953]], [[(-200237973182), 0, 0, 0, 0], [400443489383, 0, 0, 0], [(-6293197641), 0, 0], [400443489383, 0], [(-1186042211294)]]], r := 2068756686086, ok := true }, de := { p := [[[(-70020710576442298970)]], [[1028884371606875056, 0], [1028884371606875056]], [[(-39367323881113576), 0, 0], [410303899840161, 0], [(-39367323881113576)]], [[2018891663154616, 0, 0, 0], [163623138683, 0, 0], [163623138683, 0], [2018891663154616]], [[(-116474502715528), 0, 0, 0, 0], [65250493, 0, 0, 0], [6391073381, 0, 0], [65250493, 0], [(-116474502715528)]]], r := 77649678874657, ok := true }, dde := { p := [[[(-2593421776062621678978)]], [[198459764451743024515, 0], [198459764451743024497]], [[(-15266548158057798541), 0, 0], [(-15266960589058441661), 0], [(-15266548158057798544)]], [[1174349693840743360, 0, 0, 0], [1174349364897953184, 0, 0], [1174349364897953184, 0], [1174349693840743346]], [[(-90334591899491891), 0, 0, 0, 0], [(-90334592096258237), 0, 0, 0], [(-90334604879081579), 0, 0], [(-90334592096258236), 0], [(-90334591899491905)]]], r := 46597346731430228, ok := true }, nJu := { p := [[[(-140041421152884597940)]], [[2057768743213750113, 0], [2057768743213750113]], [[(-78734647762227152), 0, 0], [820607799680322, 0], [(-78734647762227152)]], [[4037783326309233, 0, 0, 0], [327246277367, 0, 0], [327246277367, 0], [4037783326309233]], [[(-232949005431056), 0, 0, 0, 0], [130500986, 0, 0, 0], [12782146762, 0, 0], [130500986, 0], [(-232949005431056)]]], r := 155299357749307, ok := true }, Jd1 := { p := [[[(-5186843552125243357956)]], [[396919528903486049030, 0], [396919528903486048995]], [[(-30533096316115597081), 0, 0], [(-30533921178116883322), 0], [(-30533096316115597087)]], [[2348699387681486721, 0, 0, 0], [2348698729795906369, 0, 0], [2348698729795906369, 0], [2348699387681486693]], [[(-180669183798983782), 0, 0, 0, 0], [(-180669184192516473), 0, 0, 0], [(-180669209758163158), 0, 0], [(-180669184192516472), 0], [(-180669183798983810)]]], r := 93194693462860448, ok := true }, term0 := { p := [[[520762760271878184295697]], [[(-79511657602312877178175), 0], [(-78534624915781219205284)]], [[9151526520574782139675, 0, 0], [12036454905261543215903, 0], [9001209738710828429325]], [[(-937443753016808670964), 0, 0, 0], [(-1387059860406811560277), 0, 0], [(-1381278448148852406508), 0], [(-920099511384699226222)]], [[90071071462434548459, 0, 0, 0, 0], [142172215497684918835, 0, 0, 0], [159242780858477683791, 0, 0], [141282767206275604773, 0], [88292174883490709097]]], r := 89213429363043881569, ok := true }, r0 := { p := [[[48582913797257515244]], [[(-2970507328190573544), 97048578133154850188], [(-2867404822090709863)]], [[168498043541889184, (-5926429332156930258), 48290111623496212035], [159833439363537648, (-5731511113115692542)], [203023411037402582]], [[(-10090849064266189), 335925493437136393, (-2934105090627998009), (-233535359343377702)], [(-8174248254429504), 319292567007486431, (-2859157479925087961)], [(-11140995808837531), 405824411214221605], [(-14823556299028552)]], [[650329157745294, (-20115223004918200), 165827786113518128, 28987653745647777, (-57582983890811617)], [455302511006250, (-16325098806059141), 158897364596622096, 6600075384742299], [559198285968335, (-22256133874624347), 202467564173568022], [804263434207766, (-29632058149336291)], [1098701921631089]]], r := 181563146236320298, ok := true }, r1 := { p := [[[2891732243039544423430]], [[(-164181612591793156423), 0], [(-176851460668057261968)]], [[8968296687054901090, 0, 0], [9469270049586804428, 0], [12556306237839146368]], [[(-537082470006908846), 0, 0, 0], [(-474843800577460071), 0, 0], [(-662881440567598946), 0], [(-919087143059566569)]], [[35160277923388740, 0, 0, 0, 0], [26636500710068593, 0, 0, 0], [32552862538025885, 0, 0], [48082344808258254, 0], [68237345328643994]]], r := 374001089422505842, ok := true }, r2 := { p := [[[76414701549553216277490]], [[(-5648545533760998174514), 470700299381630901585], [(-11153564111602976758157)]], [[392297095664003180630, (-26062217276281803779), 480379999509110854], [800325947140417170917, (-33046944618725297037)], [1242043750708807301474]], [[(-28047787434638168525), 1580712990182768625, 2028310838325093, (-1343842737627120)], [(-54747057102305883021), 1651199125125563553, 1441515127506056], [(-87487626728643103839), 2484514448647822027], [(-124205298235918797029)]], [[2058784577068916915, (-105300013824203549), (-86496713391809), 22054516571235, 3688671015454], [3891117029242515170, (-94659309184444123), 96294496916116, (-114679860018001)], [5928350828494478096, (-119946318802890807), (-17273817251146)], [8633880209717963142, (-188309721056186766)], [11713505154742561546]]], r := 97695644012333953427, ok := true }, r3 := { p := [[[958716988543843901551368]], [[(-147336415541452313693296), 7446001531409754756219], [(-150680416479661608669750)]], [[16994143941566960211698, (-1054958741571353034944), 1489236865169035654], [23170864484292623808530, (-576763515413660791418)], [17510201677892915641869]], [[(-1742660178892871837531), 118242188709098749680, 60167939025826452, (-9213496424023737)], [(-2673153984234494775034), 81545385149901664286, (-3687744456002637)], [(-2693094833337942300269), 44480509538316585854], [(-1802304771485696862988)]], [[167543683584200308499, (-11950353082231478245), (-5628522015155557), 7701504173003, 51650158811419], [274147855957646547786, (-9131979069050808937), 1215564115865094, (-746827791565215)], [310711489262334750032, (-6283762878172170438), 86724326105003], [277219028317513154346, (-3426055123939572252)], [173667801760877896536]]], r := 19813149913824591972920, ok := true }, eta := { p := [[[(-85226160998711190040152)]], [[6328094371968134283963, 0], [11783542124768212811714]], [[(-442978225332037856187), 0, 0], [(-847965263015304879758), 0], [(-1289626852135698099555)]], [[31857765492437213793, 0, 0, 0], [58270906227288203309, 0, 0], [91057177241043216396, 0], [127825201071304632912]], [[(-2347634736644656160), 0, 0, 0, 0], [(-4155695289827808184), 0, 0, 0], [(-6191929086734427102), 0, 0], [(-8904216107060812737), 0], [(-11989846023557278589)]]], r := 12274292578321305543, 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 := 468374361246531584, bh := 36028797018963968, tc := 2305843009213693952, th := 2305843009213693952, sc := 4323455642275676160, sh := 288230376151711744 }
noncomputable def q1 : Cert := { V0 := [[[401386330553985103]], [[(-13448754760320482), 401112209086151695], [6317468943361744]], [[210472409561271, (-13421204188812859), (-410851071194098)], [(-214701590329353), 6304527233666450], [(-140887382341720)]], [[(-4665633069102), 209118424076840, 41270393551904, (-136398951093166)], [4007134845826, (-213394783217553), (-19386510810186)], [4727095220054, (-140802394989598)], [6326798961504]], [[129853511328, (-4616897075336), (-2026394710130), 13664470487820, 412718230864], [(-114786735540), 3941386645632, 1955834544381, (-6418800065342)], [(-77227803749), 4718731985267, 127719859647], [(-212671399937), 6321853483253], [(-333219880484)]]], r0 := 166339927559453, V1 := [[[3144526619085394653]], [[(-101061210311872534), 0], [47472875288610768]], [[1375951360888744, 0, 0], [(-1420176216560255), 0], [(-1104082941627485)]], [[(-26876452482271), 0, 0, 0], [18060287589753, 0, 0], [35453932822085, 0], [49385947046411]], [[712883958189, 0, 0, 0, 0], [(-432378023091), 0, 0, 0], [(-504004184907), 0, 0], [(-1579489122196), 0], [(-2604749886581)]]], r1 := 127237880685973, V2 := [[[17884920157217324623]], [[(-8844418318129756), 1714432467423531], [(-43697348143443254)]], [[45309989635566, (-7684467250004), (-4826522875116)], [(-702028561874206), 273038334657800], [(-51135303883041)]], [[(-1071126983561), (-697803287409), 120383020982, 13134228290], [4494617998672, (-1216312699767), (-1156327489288)], [(-1057494509381), 11504385659201], [(-596507260602)]], [[37395261807, 6138095046, 1527576010, (-598135823), (-35036396)], [(-100591121579), (-114821926794), 28971522111, 4192609545], [65392343024, (-54024169005), (-95122125630)], [21473354450, 48368862162], [12542271959]]], r2 := 37305216345887, V3 := [[[18217931321494253327]], [[(-15076681220511505), 1375153033514759], [(-18363311234051128)]], [[12509838088564, 64294328796548, (-7707930209906)], [(-1195831404789200), 223190629950524], [(-62106149348030)]], [[19580415829, (-1908568029769), (-207817420707), 42010206030], [2009034917603, 10334272867522, (-1877272508621)], [(-2917639686841), 9910193229679], [(-260507117016)]], [[(-617335632), (-1531555903), 18179456015, 287228516, (-225395406)], [3086578422, (-316398170809), (-49816639795), 13627913791], [87021442322, 444870818367, (-159525647225)], [(-9954862751), 69580565989], [(-76283942)]]], r3 := 133821516946404, Vm := [[[17897759941464109379]], [[(-8933815395526614), 0], [(-41653153595625025)]], [[40931761679982, 0, 0], [(-716256208916004), 0], [34464563330396]], [[(-1037611732194), 0, 0, 0], [3774392350359, 0, 0], [(-1663663657761), 0], [(-292156727390)]], [[36583237382, 0, 0, 0, 0], [(-94414748849), 0, 0, 0], [33008930412, 0, 0], [18004497899, 0], [11451911172]]], rm := 8273458341662 }
noncomputable def w1 : Wit := { Z0 := { p := [[[401523474130374230]], [[(-13462543926035088), 401523474130374230], [6323946318234691]], [[211150549812849, (-13462543926035088), 0], [(-215356089465368), 6323946318234691], [(-140929816145662)]], [[(-4690066180672), 211150549812849, 0, 0], [4040100404517, (-215356089465368), 0], [4731266612988, (-140929816145662)], [6329272306500]], [[130664156930, (-4690066180672), 0, 0, 0], [(-116038742195), 4040100404517, 0, 0], [(-77411963332), 4731266612988, 0], [(-212919124834), 6329272306500], [(-333342346813)]]], r := 39110656807047, ok := true }, Z1 := { p := [[[3212187793042993847]], [[(-107700351408280704), 0], [50591570545877531]], [[1689204398502796, 0, 0], [(-1722848715722942), 0], [(-1127438529165292)]], [[(-37520529445369), 0, 0, 0], [32320803236142, 0, 0], [37850132903909, 0], [50634178452002]], [[1045313255444, 0, 0, 0, 0], [(-928309937560), 0, 0, 0], [(-619295706652), 0, 0], [(-1703352998667), 0], [(-2666738774497)]]], r := 33694032024071, ok := true }, Z2 := { p := [[[157249073104914174279]], [[(-2071380259786276222), 401523474130374230], [(-10234005345924990837)]], [[40694797810170548, (-13462543926035088), 0], [132844919318991832, 6323946318234691], [722359174232344939]], [[(-1010578815763229), 211150549812849, 0, 0], [(-2386454013346201), (-215356089465368), 0], [(-9367272289386237), (-140929816145662)], [(-52871641654022864)]], [[30643803486250, (-4690066180672), 0, 0, 0], [54239138624034, 4040100404517, 0, 0], [164693081412402, 4731266612988, 0], [685012744247160, 6329272306500], [3926814471948867]]], r := 1053765875436729, ok := true }, Z3 := { p := [[[334893121187375533497]], [[(-18702784321143670902), 1705892047342792374], [(-22779884008242023299)]], [[1164856491280611469, (-129905780680103189), 0], [1316332296548122936, 21501322182202307], [1628010959206517346]], [[(-74464734041768581), 7864353561863976, 0, 0], [(-82719973900255466), (-1398194006815440), 0], [(-95108755286826707), (-553495103827561)], [(-119938274898766227)]], [[4817244868752252, (-499587641839463), 0, 0, 0], [5315603865232866, 75719275512619, 0, 0], [5998804667069946, 39172902788286, 0], [7046615874339188, 24914137665894], [8947813007881837]]], r := 20929661891324339, ok := true }, iE := { p := [[[165238570804447130915]], [[(-2168012079260171729), 0], [(-10108171720205014832)]], [[42649439089101115, 0, 0], [131256865947756673, 0], [719554958502915963]], [[(-1059701727955287), 0, 0, 0], [(-2342868535107337), 0, 0], [(-9333234750568086), 0], [(-52745702052005766)]], [[32145529499201, 0, 0, 0, 0], [52902155052673, 0, 0, 0], [163943941436545, 0, 0], [683475452973919, 0], [3920181639537812]]], r := 1046982378619017, ok := true }, iHu := { p := [[[351012060328594163487]], [[(-19566489326578902612), 0], [(-22576718453744887208)]], [[1218888836444441803, 0, 0], [1307705828211873752, 0], [1622780995266269173]], [[(-77922129540666067), 0, 0, 0], [(-82209088957004889), 0, 0], [(-94856641104236891), 0], [(-119702861720412979)]], [[5041006067451933, 0, 0, 0, 0], [5284151955782566, 0, 0, 0], [5983759578970161, 0, 0], [7035113550598749, 0], [8935294008080870]]], r := 21208669063461539, ok := true }, T := { p := [[[2305843009213693952]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[2059339809490656220]], [[27019560630071269, 0], [125976400807901447]], [[(-177022554745726), 0, 0], [1669914152899961, 0], [(-1261310105062959)]], [[3910284439777, 0, 0, 0], [(-13698639207810), 0, 0], [(-15806122162857), 0], [31619984363877]], [[(-130347514124), 0, 0, 0, 0], [300769420908, 0, 0, 0], [(-6308279498), 0, 0], [400432660972, 0], [(-1216848070701)]]], r := 1945835085449, ok := true }, de := { p := [[[(-68105920209705792256)]], [[892411549831993286, 0], [1029705634421530715]], [[(-29568969351364913), 0, 0], [410959176234302, 0], [(-39366971029923700)]], [[1314223797804455, 0, 0, 0], [164015266971, 0, 0], [189248384967, 0], [2018891815015946]], [[(-65711175707423), 0, 0, 0, 0], [65459076, 0, 0, 0], [6421574054, 0, 0], [87149657, 0], [(-116474502650058)]]], r := 57599467113796, ok := true }, dde := { p := [[[(-2249426281914981228788)]], [[149063998108542376173, 0], [171996920894471972428]], [[(-9937958170720698510), 0, 0], [(-11467288231775275792), 0], [(-13231009398888504061)]], [[662530401717180745, 0, 0, 0], [764457825833209975, 0, 0], [882066722115242222, 0], [1017769734089888357]], [[(-44168693504882593), 0, 0, 0, 0], [(-50963877318571497), 0, 0, 0], [(-58804486673173410), 0, 0], [(-67851315956677924), 0], [(-78289979646535169)]]], r := 28996619959115280, ok := true }, nJu := { p := [[[(-136211840419411584511)]], [[1784823099663986573, 0], [2059411268843061430]], [[(-59137938702729825), 0, 0], [821918352468604, 0], [(-78733942059847399)]], [[2628447595608910, 0, 0, 0], [328030533943, 0, 0], [378496769935, 0], [4037783630031892]], [[(-131422351414846), 0, 0, 0, 0], [130918153, 0, 0, 0], [12843148108, 0, 0], [174299314, 0], [(-232949005300115)]]], r := 115198934227584, ok := true }, Jd1 := { p := [[[(-4498852563829962457576)]], [[298127996217084752346, 0], [343993841788943944857]], [[(-19875916341441397020), 0, 0], [(-22934576463550551583), 0], [(-26462018797777008121)]], [[1325060803434361491, 0, 0, 0], [1528915651666419950, 0, 0], [1764133444230484444, 0], [2035539468179776715]], [[(-88337387009765185), 0, 0, 0, 0], [(-101927754637142993), 0, 0, 0], [(-117608973346346820), 0, 0], [(-135702631913355847), 0], [(-156579959293070337)]]], r := 57993239918230551, ok := true }, term0 := { p := [[[392061780580222698603624]], [[(-51818758907029784413311), 0], [(-59057022132807696444479)]], [[5166972700977736647523, 0, 0], [7839874113573082127347, 0], [6766201053445011899742]], [[(-458623930199206271106), 0, 0, 0], [(-782840432298392926003), 0, 0], [(-899513937201736018815), 0], [(-691504074223094616142)]], [[38185534330585952728, 0, 0, 0, 0], [69534852592330286000, 0, 0, 0], [89863187304280940288, 0, 0], [91996989282974261776, 0], [66348549571012860065]]], r := 47567630024750176684, ok := true }, r0 := { p := [[[43244325559261787050]], [[(-2399828587376742702), 86396764555994830321], [(-2577190943766633794)]], [[120637424356315055, (-4788667745742554929), 43014830043939707468], [131826535539476087, (-5151746918545062808)], [182758854111946073]], [[(-6263304994765711), 240523424439352704, (-2372396006436527209), (-183110978927603998)], [(-5994871624987526), 263359923291409350, (-2570602947372845181)], [(-9221411874664369), 365340893970583278], [(-13358765711335521)]], [[346154460708274, (-12484371999735030), 118762865290388851, 21856016055179338, (-45227228318316574)], [288298732709130, (-11972207988881746), 131093506336115739, 5271641850315267], [411735463105760, (-18422785262474660), 182316944644418361], [667429378096832, (-26705557110193123)], [990896637089184]]], r := 133067073733640430, ok := true }, r1 := { p := [[[2595439839141302104892]], [[(-133794697941696783161), 0], [(-159622873034391953373)]], [[6429362030155945796, 0, 0], [7843598684755919658, 0], [11347964521421660794]], [[(-331138329114587035), 0, 0, 0], [(-347806647800621132), 0, 0], [(-551157142005649600), 0], [(-831333337096494190)]], [[18520500410111451, 0, 0, 0, 0], [16740526732129072, 0, 0, 0], [23966516455869781, 0, 0], [40075256153072340, 0], [61758093780747349]]], r := 287306102682631948, ok := true }, r2 := { p := [[[66491084768356563316632]], [[(-4360451053205153173137), 424160122179558851102], [(-9744741681751060697113)]], [[263420261131900648989, (-20801927965029842966), 484129114868192439], [620347827669369012947, (-30079973289588945277)], [1087851282471360747860]], [[(-16264334836011730979), 1091897184573786734, 1737724105392507, (-1298932696385558)], [(-36858309146986376865), 1334749250706866169, 1619329472188325], [(-67983913644347796732), 2268561301610046981], [(-108975431786376712198)]], [[1029878931890324000, (-62438989051614818), (-60971825942953), 22821371527234, 3425472525823], [2259119911944050159, (-66028196415641318), 82399065924318, (-111286415208074)], [3997705092542539363, (-97351219873077915), (-16551811890659)], [6721068129217704182, (-172263828765407041)], [10290872177353459119]]], r := 76869470585421699050, ok := true }, r3 := { p := [[[720340801837085464406872]], [[(-95926654687117689224072), 5728837375879355582723], [(-113193888317156345262911)]], [[9588654060982249433039, (-695821396083903541560), 1590615422558015498], [15084428872521579522255, (-444008025676875876176)], [13153282266687281273111]], [[(-852142392770436532732), 67309172184836232496, 42715639529834639, (-9139095568693144)], [(-1508180801884755565700), 53805403433260215499, (-1610428314899255)], [(-1753183317808889071883), 34250173175810991370], [(-1353819196176709981437)]], [[71002407505902802008, (-5882705864300670458), (-3350149789789258), 62270015485239, 48785941842508], [134048425592433039363, (-5199758013926296290), 890497380088835, (-747382031317566)], [175298843259322590319, (-4146507123073002444), 46748743777774], [180465208947833554546, (-2638318976862182206)], [130450472305095190369]]], r := 9634901617246233000565, ok := true }, eta := { p := [[[(-74119701800664591497310)]], [[4875239000593406048952, 0], [10291698505625655649646]], [[(-296744886777564335987), 0, 0], [(-656527774379529531827), 0], [(-1129212119098987532656)]], [[18432608325801176242, 0, 0, 0], [39177054560920342338, 0, 0], [70696319565982134721, 0], [112124025109338668648]], [[(-1172114989926205898), 0, 0, 0, 0], [(-2409646998488159449), 0, 0, 0], [(-4171147533077897853), 0, 0], [(-6926557557021376529), 0], [(-10531340873330634056)]]], r := 9816031528638724411, 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 := 540431955284459520, bh := 36028797018963968, tc := 2305843009213693952, th := 2305843009213693952, sc := 3746994889972252672, sh := 288230376151711744 }
noncomputable def q2 : Cert := { V0 := [[[442139406220022973]], [[(-14797062822479364), 441773039544772622], [6232451623074328]], [[251245927261178, (-14760284748926510), (-549013055393752)], [(-214397947062628), 6216960875555178], [(-117229541870441)]], [[(-6205177594715), 249391062774592, 55077278692170, (-182110363672277)], [4482629654207, (-212828589977616), (-23198284625654)], [3934397511434, (-117156446425493)], [4574041573968]], [[197007302995, (-6134266404764), (-2774761001546), 18209593892278, 668846132780], [(-143206606031), 4400916493561, 2347670902686, (-7669793280669)], [(-69642683739), 3927434948113, 109997761290], [(-154041344436), 4569860130745], [(-208503416052)]]], r0 := 116086610760412, V1 := [[[3448831299092099388]], [[(-109770378941502441), 0], [46234755140738022]], [[1596483622730497, 0, 0], [(-1365268916747072), 0], [(-917084927702240)]], [[(-34826438311558), 0, 0, 0], [18994765893017, 0, 0], [29345824721604, 0], [35557391230869]], [[1070211784195, 0, 0, 0, 0], [(-521643747993), 0, 0, 0], [(-453866319323), 0, 0], [(-1130389723299), 0], [(-1623613154231)]]], r1 := 78796790300812, V2 := [[[17818050641674110095]], [[(-10487684106547093), 2323723731525815], [(-42476732906110786)]], [[63455217558998, (-6432941663639), (-7909886132647)], [(-726417699593096), 321961719490105], [(-52302614389855)]], [[(-1721405578734), (-1006819253052), 177849284423, 25999363002], [5483033008305, (-879231700309), (-1648956014556)], [(-1210378503962), 11888625446186], [(-549472441930)]], [[69023781253, 11076513509, 2996796403, (-1101361882), (-83705873)], [(-141194762072), (-145006621087), 37306156093, 7220820960], [71048462481, (-35763199214), (-118467470823)], [18460700395, 49671713966], [9395987598]]], r2 := 25051981282298, V3 := [[[18215981672324369159]], [[(-17547269962712010), 1677822458434315], [(-16190201891054426)]], [[16699664017824, 97143443396226, (-11376433691909)], [(-1217027183140847), 237882385489470], [(-57359499789470)]], [[34492100595, (-2588035080875), (-443646817820), 75002888450], [2338668216039, 13650509856579, (-2419771548831)], [(-3335939781169), 9353512649691], [(-240275713922)]], [[(-1236885848), (-3069404627), 30652421074, 1478397475, (-486755312)], [4846623106, (-376837022165), (-93181439022), 21245748532], [89445379904, 521874801071, (-180820908077)], [(-11863441323), 66485858850], [(-290503965)]]], r3 := 138371888313618, Vm := [[[17835540046274292625]], [[(-10583582621063330), 0], [(-40056601765444289)]], [[57190709891424, 0, 0], [(-739606121344646), 0], [36217801542640]], [[(-1663122801092), 0, 0, 0], [4580234822874, 0, 0], [(-1698907199879), 0], [(-245943306576)]], [[67375787244, 0, 0, 0, 0], [(-131815796361), 0, 0, 0], [34992012946, 0, 0], [15625210160, 0], [8681343569]]], rm := 5694664436661 }
noncomputable def w2 : Wit := { Z0 := { p := [[[442322723914757990]], [[(-14815474344747878), 442322723914757990], [6240206467614920]], [[252175246674257, (-14815474344747878), 0], [(-215184219518878), 6240206467614920], [(-117266000671671)]], [[(-6240744142988), 252175246674257, 0, 0], [4523621890216, (-215184219518878), 0], [3937863425159, (-117266000671671)], [4576132965846]], [[198299681742, (-6240744142988), 0, 0, 0], [(-144877004331), 4523621890216, 0, 0], [(-69784649067), 3937863425159, 0], [(-154249764362), 4576132965846], [(-208592642783)]]], r := 25826879351915, ok := true }, Z1 := { p := [[[3538581791318063922]], [[(-118523794757983017), 0], [49921651740919365]], [[2017401973394060, 0, 0], [(-1721473756151023), 0], [(-938128005373365)]], [[(-49925953143898), 0, 0, 0], [36188975121731, 0, 0], [31502907401278, 0], [36609063726770]], [[1586397453943, 0, 0, 0, 0], [(-1159016034645), 0, 0, 0], [(-558277192531), 0, 0], [(-1233998114889), 0], [(-1668741142261)]]], r := 21079082922554, ok := true }, Z2 := { p := [[[143132742460620164378]], [[(-1996339297408380557), 442322723914757990], [(-8085481052299453483)]], [[42748853324197786, (-14815474344747878), 0], [110163036866389261, 6240206467614920], [493148668724197948]], [[(-1186195817894765), 252175246674257, 0, 0], [(-2132797994799938), (-215184219518878), 0], [(-6701776103860274), (-117266000671671)], [(-31246621106821253)]], [[41032106940537, (-6240744142988), 0, 0, 0], [53778989602470, 4523621890216, 0, 0], [126651771399392, 3937863425159, 0], [423885805744361, 4576132965846], [2009788495351558]]], r := 571212497076816, ok := true }, Z3 := { p := [[[332493624681223034332]], [[(-21425802718860877026), 2048677262507435112], [(-19768777276089010018)]], [[1539751211594240989, (-171938862015104303), 0], [1317681770325073942, 22378927169230971], [1223401892440684776]], [[(-113573378887560336), 12055040269354776, 0, 0], [(-95537238291671166), (-1590975974951298), 0], [(-82461571408543530), (-499275175289353)], [(-78098187187052648)]], [[8477591255852529, (-884356721077805), 0, 0, 0], [7083447883423588, 100384760623209, 0, 0], [6001128998576314, 38804633839485, 0], [5294134426040198, 19477093201118], [5049120270041478]]], r := 20849982101911202, ok := true }, iE := { p := [[[151571566193346821724]], [[(-2104855181345601518), 0], [(-7966427701456525683)]], [[45141699534630803, 0, 0], [108514395919696606, 0], [490911417378050194]], [[(-1253396260914751), 0, 0, 0], [(-2083039976506426), 0, 0], [(-6672814853549271), 0], [(-31159315668080693)]], [[43375330532163, 0, 0, 0, 0], [52079309503844, 0, 0, 0], [125965470422817, 0, 0], [422744561645990, 0], [2005808874931413]]], r := 567310811052255, ok := true }, iHu := { p := [[[351012060328594163487]], [[(-22576718453744887208), 0], [(-19566489326578902612)]], [[1622780995266269173, 0, 0], [1307705828211873752, 0], [1218888836444441803]], [[(-119702861720412979), 0, 0, 0], [(-94856641104236891), 0, 0], [(-82209088957004889), 0], [(-77922129540666067)]], [[8935294008080870, 0, 0, 0, 0], [7035113550598749, 0, 0, 0], [5983759578970161, 0, 0], [5284151955782566, 0], [5041006067451933]]], r := 21208669063461539, ok := true }, T := { p := [[[2305843009213693952]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[2245027715072030661]], [[31176416111620695, 0], [117996082174629677]], [[(-235680916081588), 0, 0], [1669914152899961, 0], [(-1069478161576330)]], [[6006923069752, 0, 0, 0], [(-15806122162857), 0, 0], [(-13698639207810), 0], [23144069483030]], [[(-231043832590), 0, 0, 0, 0], [400432660972, 0, 0, 0], [(-6308279498), 0, 0], [300769420908, 0], [(-772075857056)]]], r := 1371778335651, ok := true }, de := { p := [[[(-68105920209705792256)]], [[1029705634421530715, 0], [892411549831993286]], [[(-39366971029923700), 0, 0], [410959176234302, 0], [(-29568969351364913)]], [[2018891815015946, 0, 0, 0], [189248384967, 0, 0], [164015266971, 0], [1314223797804455]], [[(-116474502650058), 0, 0, 0, 0], [87149657, 0, 0, 0], [6421574054, 0, 0], [65459076, 0], [(-65711175707423)]]], r := 57599467113797, ok := true }, dde := { p := [[[(-2249426281914981228762)]], [[171996920894471972441, 0], [149063998108542376159]], [[(-13231009398888504058), 0, 0], [(-11467288231775275792), 0], [(-9937958170720698518)]], [[1017769734089888370, 0, 0, 0], [882066722115242222, 0, 0], [764457825833209976, 0], [662530401717180739]], [[(-78289979646535157), 0, 0, 0, 0], [(-67851315956677924), 0, 0, 0], [(-58804486673173410), 0, 0], [(-50963877318571496), 0], [(-44168693504882596)]]], r := 28996619959115426, ok := true }, nJu := { p := [[[(-136211840419411584511)]], [[2059411268843061430, 0], [1784823099663986573]], [[(-78733942059847399), 0, 0], [821918352468604, 0], [(-59137938702729825)]], [[4037783630031892, 0, 0, 0], [378496769935, 0, 0], [328030533943, 0], [2628447595608910]], [[(-232949005300115), 0, 0, 0, 0], [174299314, 0, 0, 0], [12843148108, 0, 0], [130918153, 0], [(-131422351414846)]]], r := 115198934227585, ok := true }, Jd1 := { p := [[[(-4498852563829962457524)]], [[343993841788943944882, 0], [298127996217084752319]], [[(-26462018797777008115), 0, 0], [(-22934576463550551583), 0], [(-19875916341441397035)]], [[2035539468179776740, 0, 0, 0], [1764133444230484444, 0, 0], [1528915651666419952, 0], [1325060803434361478]], [[(-156579959293070313), 0, 0, 0, 0], [(-135702631913355848), 0, 0, 0], [(-117608973346346820), 0, 0], [(-101927754637142991), 0], [(-88337387009765192)]]], r := 57993239918230846, ok := true }, term0 := { p := [[[393529487638522192759089]], [[(-60016684889031807336573), 0], [(-51280606708011152624550)]], [[6905160572174894939900, 0, 0], [7854928052297182258970, 0], [5088692164701363410343]], [[(-707203824791380261089), 0, 0, 0], [(-905014415571252010720), 0, 0], [(-780582342147393391202), 0], [(-450578432810344835330)]], [[67941650285049084327, 0, 0, 0, 0], [92754140377260029481, 0, 0, 0], [89978986882606958526, 0, 0], [69166867262244619027, 0], [37460714744863677415]]], r := 47893122853399473688, ok := true }, r0 := { p := [[[43556903758148267184]], [[(-2689794216982891373), 87002371115235999298], [(-2203598291210164834)]], [[154108342955496371, (-5365660555155041976), 43278636904749014412], [123326041294665427, (-4404635705544526626)], [135101971285365152]], [[(-9288160847067173), 307186906886266058, (-2655036299068987091), (-221901291132562413)], [(-6336840303144944), 246363572362105114, (-2197194479220760308)], [(-7448293413894056), 270051456759476531], [(-8540875554762840)]], [[600540001257707, (-18511857899128311), 151540225359209076, 27670660868964426, (-54667991475716024)], [354009873002076, (-12655912608951307), 122604361311706076, 5126582169662771], [375988319301014, (-14878840589301989), 134720883770631741], [465442838943002, (-17072820862979219)], [548271935647229]]], r := 128728316406413715, ok := true }, r1 := { p := [[[2581851581776706859958]], [[(-147559340549010852254), 0], [(-135817567334771123918)]], [[8132559178195362768, 0, 0], [7299127940156658862, 0], [8346913464396490588]], [[(-490107735188900577), 0, 0, 0], [(-367990754381186687), 0, 0], [(-442301763705805684), 0], [(-529045564458775521)]], [[32195005715611286, 0, 0, 0, 0], [20726540098769386, 0, 0, 0], [21840910638226436, 0, 0], [27775721184451810, 0], [34021049303659138]]], r := 194563470428498203, ok := true }, r2 := { p := [[[58240596815993655306635]], [[(-4339692591664969576391), 413237012956916097783], [(-7371145765452810495668)]], [[302599089639162548862, (-23177678263830428453), 483198000764153545], [532982460415309415336, (-24983731733706215197)], [710929538901655094431]], [[(-21668024785184864513), 1414947080282088193, 2222676496912159, (-1576650809183589)], [(-36599824531499055733), 1260269764104762103, 1378324777059630], [(-50447971372173811158), 1627715870694693753], [(-61579764973278133130)]], [[1591237379172753555, (-94514537568030337), (-94936132078860), 25299784824615, 5046793277819], [2605183219000915395, (-72607407645909060), 98199467328050, (-118137279607739)], [3431232386688577668, (-79287465145466804), (-14505479248544)], [4311463600527202475, (-106870598909473153)], [5030772711248071917]]], r := 42458081463236326971, ok := true }, r3 := { p := [[[715321953252063051821945]], [[(-109909779817903289398501), 6446645448231243877863], [(-97764704585820611362999)]], [[12676395490513830371530, (-913648718417298589793), 1482165269494437925], [15032530695270203332735, (-432883453477403393243)], [9857085480566023438958]], [[(-1299852170823899227612), 102416948158012848737, 62511777227378647, (-10718930325779727)], [(-1734213732674506796455), 61218045394776144004, (-3403769399272132)], [(-1515959615326651019227), 28938512087892590863], [(-879785053929792503581)]], [[124968271658637328525, (-10351643100257038334), (-5831108763881784), 355174750768, 69979556843646], [177851511843213643494, (-6855977212946424432), 1131963355922017, (-758581398934250)], [174898543565973324550, (-4088740631384828741), 57052281791568], [135318135315664556307, (-1931880675639654428)], [73495819107864362663]]], r := 9926943346966596856472, ok := true }, eta := { p := [[[(-65957308352366698790488)]], [[4936363913718692595365, 0], [7846814666090696745651]], [[(-347148361160400773267), 0, 0], [(-569035303220843717272), 0], [(-742053859997971682404)]], [[25017613378145455903, 0, 0, 0], [39267935914992151298, 0, 0], [52787360509646722672, 0], [63631040031650523875]], [[(-1845159929699834319), 0, 0, 0, 0], [(-2805507465647308841), 0, 0, 0], [(-3604053065700653385), 0, 0], [(-4464926958226459281), 0], [(-5166451078945672379)]]], r := 5500194990072992817, 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 := 540431955284459520, bh := 36028797018963968, tc := 2305843009213693952, th := 2305843009213693952, sc := 4323455642275676160, sh := 288230376151711744 }
noncomputable def q3 : Cert := { V0 := [[[413503550027884840]], [[(-13860790220037764), 413203849055589468], [5820519019947327]], [[218203173897007, (-13830655878366052), (-449167246954907)], [(-198032058500080), 5807864798501841], [(-109625494594236)]], [[(-4888389118972), 216718998757746, 45137130523014, (-149082652131550)], [3735151456545, (-196753450129255), (-18954296439410)], [3676145101928, (-109565225252674)], [4276481994102]], [[137194232007, (-4834700216649), (-2220934435327), 14938545029353, 478792949137], [(-108249408457), 3670630777798, 1913368964745, (-6273097283300)], [(-59885127548), 3670257648813, 90655668479], [(-143780530519), 4273057658230], [(-194949929015)]]], r0 := 104842640093685, V1 := [[[3235413738649070246]], [[(-103771184538439868), 0], [43576314462596914]], [[1410217123930346, 0, 0], [(-1294978997692983), 0], [(-860123840313683)]], [[(-27700066119271), 0, 0, 0], [16278493023905, 0, 0], [27655045451362, 0], [33362496763892]], [[740028588190, 0, 0, 0, 0], [(-392836640521), 0, 0, 0], [(-394091120963), 0, 0], [(-1066000115819), 0], [(-1523157107321)]]], r1 := 70304621051895, V2 := [[[17797316333252493957]], [[(-10252542507204954), 2306913575477558], [(-43908683159528366)]], [[54558532549434, (-10338289755355), (-7543017438289)], [(-706018255510536), 319636238272142], [(-54449474773304)]], [[(-1276580488484), (-948329282456), 188624988645, 23808284378], [4752894496316, (-1440139532978), (-1571972911713)], [(-941275779154), 11794603643407], [(-513502298226)]], [[44536223427, 8592343347, 2404654159, (-1087750023), (-73587690)], [(-104835935478), (-135825921837), 39590808918, 6608643634], [63842816496, (-57968357011), (-112830895927)], [17535571745, 48404969395], [8554775658]]], r2 := 24214714833354, V3 := [[[18180954188562371254]], [[(-17480093635598961), 1861735603553858], [(-18614865813003218)]], [[16880196608226, 86760277770851, (-12143592038434)], [(-1207620253377771), 263674205789741], [(-63672452781842)]], [[26164995836, (-2602217095026), (-324769422703), 76960264684], [2363442556031, 12140618478154, (-2580299186860)], [(-2976511643973), 10333616149467], [(-261812118214)]], [[(-875222410), (-1734921959), 28766373662, 502483661, (-479878466)], [3488661024, (-377882763081), (-67627078962), 21776378941], [90200023581, 458285167840, (-192392511630)], [(-9681372425), 71601061089], [(-240375076)]]], r3 := 107152218522097, Vm := [[[17814589324590582188]], [[(-10372847715266179), 0], [(-41518468944592371)]], [[48608734892785, 0, 0], [(-722713023684500), 0], [32953155684139]], [[(-1229290435766), 0, 0, 0], [3900764768953, 0, 0], [(-1568871773059), 0], [(-216504337466)]], [[43393158966, 0, 0, 0, 0], [(-97217235358), 0, 0, 0], [30280718034, 0, 0], [13862116185, 0], [7786084249]]], rm := 5426963183883 }
noncomputable def w3 : Wit := { Z0 := { p := [[[413653496640586477]], [[(-13875873503658753), 413653496640586477], [5826852896862392]], [[218946595545814, (-13875873503658753), 0], [(-198672500290556), 5826852896862392], [(-109655566181136)]], [[(-4915309500221), 218946595545814, 0, 0], [3767506937445, (-198672500290556), 0], [3679078061497, (-109655566181136)], [4278194639520]], [[138094027643, (-4915309500221), 0, 0, 0], [(-109486029046), 3767506937445, 0, 0], [(-60009636236), 3679078061497, 0], [(-143952146597), 4278194639520], [(-195023026168)]]], r := 23703187987107, ok := true }, Z1 := { p := [[[3309227973124691816]], [[(-111006988029270018), 0], [46614823174899137]], [[1751572764366514, 0, 0], [(-1589380002324444), 0], [(-877244529449081)]], [[(-39322476001764), 0, 0, 0], [30140055499561, 0, 0], [29432624491976, 0], [34225557116162]], [[1104752221149, 0, 0, 0, 0], [(-875888232366), 0, 0, 0], [(-480077089887), 0, 0], [(-1151617172776), 0], [(-1560184209339)]]], r := 18657358359559, ok := true }, Z2 := { p := [[[139302176646233094173]], [[(-1838387056473772892), 413653496640586477], [(-7873281649947633983)]], [[36497652569187342, (-13875873503658753), 0], [102226693116720022, 5826852896862392], [480228276445448780]], [[(-914900547728472), 218946595545814, 0, 0], [(-1846883068860972), (-198672500290556), 0], [(-6229659965853520), (-109655566181136)], [(-30429029809280220)]], [[27933492591728, (-4915309500221), 0, 0, 0], [42233508183291, 3767506937445, 0, 0], [110062184921097, 3679078061497, 0], [394385928974365, 4278194639520], [1957250770703798]]], r := 514322380693083, ok := true }, Z3 := { p := [[[295010364286491931592]], [[(-16401520241955172781), 1746861019363809402], [(-17466273625186447084)]], [[1020313377439802675, (-132558346909568216), 0], [1006259879792822436, 19549279266328113], [1079381185150030492]], [[(-65178986650775227), 8007643468737172, 0, 0], [(-63170560182582996), (-1260194434148458), 0], [(-62908090224133574), (-430614775581087)], [(-68854370539674324)]], [[4214497947809812, (-508278949768268), 0, 0, 0], [4056994748381722, 67903787798127, 0, 0], [3964468825207592, 30408079448210, 0], [4036544137787545, 16775891503031], [4449298235105999]]], r := 12331634877364213, ok := true }, iE := { p := [[[147533037038571294482]], [[(-1938069970291905476), 0], [(-7757339168836596587)]], [[38536716718888926, 0, 0], [100758604264161006, 0], [478046354465313949]], [[(-966623323595155), 0, 0, 0], [(-1805932907408738), 0, 0], [(-6203220709452628), 0], [(-30343902466963234)]], [[29525402624090, 0, 0, 0, 0], [40967565123499, 0, 0, 0], [109482775515637, 0, 0], [393346177832007, 0], [1953370210489245]]], r := 509762063456738, ok := true }, iHu := { p := [[[311516418408235681662]], [[(-17281552884363795721), 0], [(-17281552884363795721)]], [[1075312314923621447, 0, 0], [998521104222990677, 0], [1075312314923621447]], [[(-68695855483227309), 0, 0, 0], [(-62712591126530896), 0, 0], [(-62712591126530896), 0], [(-68695855483227309)]], [[4442000831270226, 0, 0, 0, 0], [4028832228436847, 0, 0, 0], [3952828638437655, 0, 0], [4028832228436847, 0], [4442000831270226]]], r := 12512263585187546, ok := true }, T := { p := [[[2305843009213693952]], [[0, 2305843009213693952], [0]]], r := 0, ok := true }, E := { p := [[[2306482491999228946]], [[30299142107262854, 0], [121275663651821262]], [[(-204445089540673), 0, 0], [1611052628069509, 0], [(-1096900696371277)]], [[4511812681189, 0, 0, 0], [(-13723907228526), 0, 0], [(-13723907228526), 0], [23745597724442]], [[(-150400995276), 0, 0, 0, 0], [300758555133, 0, 0, 0], [(-6325741585), 0, 0], [300758555133, 0], [(-792129338208)]]], r := 1212978221580, ok := true }, de := { p := [[[(-66189485904719275649)]], [[893234225875841727, 0], [893234225875841727]], [[(-29568615587433501), 0, 0], [411717216855780, 0], [(-29568615587433501)]], [[1314223950190681, 0, 0, 0], [189772247576, 0, 0], [189772247576, 0], [1314223950190681]], [[(-65711175641669), 0, 0, 0, 0], [87471460, 0, 0, 0], [6456948776, 0, 0], [87471460, 0], [(-65711175641669)]]], r := 37549255370383, ok := true }, dde := { p := [[[(-1951299940899972111382)]], [[129187252742536129060, 0], [129187252742536129050]], [[(-8612898079969644521), 0, 0], [(-8613312643770214024), 0], [(-8612898079969644527)]], [[574193014246990429, 0, 0, 0], [574192632078351361, 0, 0], [574192632078351361, 0], [574193014246990422]], [[(-38279534371208685), 0, 0, 0, 0], [(-38279534635437492), 0, 0, 0], [(-38279547550544640), 0, 0], [(-38279534635437491), 0], [(-38279534371208688)]]], r := 16990250325079091, ok := true }, nJu := { p := [[[(-132378971809438551297)]], [[1786468451751683454, 0], [1786468451751683454]], [[(-59137231174867002), 0, 0], [823434433711561, 0], [(-59137231174867002)]], [[2628447900381362, 0, 0, 0], [379544495152, 0, 0], [379544495152, 0], [2628447900381362]], [[(-131422351283338), 0, 0, 0, 0], [174942921, 0, 0, 0], [12913897552, 0, 0], [174942921, 0], [(-131422351283338)]]], r := 75098510740762, ok := true }, Jd1 := { p := [[[(-3902599881799944222763)]], [[258374505485072258120, 0], [258374505485072258100]], [[(-17225796159939289042), 0, 0], [(-17226625287540428048), 0], [(-17225796159939289054)]], [[1148386028493980858, 0, 0, 0], [1148385264156702722, 0, 0], [1148385264156702723, 0], [1148386028493980844]], [[(-76559068742417370), 0, 0, 0, 0], [(-76559069270874983), 0, 0, 0], [(-76559095101089280), 0, 0], [(-76559069270874982), 0], [(-76559068742417375)]]], r := 33980500650158177, ok := true }, term0 := { p := [[[296376217305336277510935]], [[(-39120301306314380564727), 0], [(-38569102361279559744550)]], [[3899115116940788936489, 0, 0], [5116713416511544942352, 0], [3825618386658381303431]], [[(-346013815099456414839), 0, 0, 0], [(-510809759123902388414), 0, 0], [(-508359870560368090094), 0], [(-338664144517094938647)]], [[28805774942047039940, 0, 0, 0, 0], [45367032695028481157, 0, 0, 0], [50778568050079202466, 0, 0], [45040380666139413348, 0], [28152470888778408470]]], r := 24379276579050973837, ok := true }, r0 := { p := [[[38727901599691237012]], [[(-2168406577358612988), 77368563342421608604], [(-1979771654048619026)]], [[110089339604867622, (-4326339372116967179), 38510024444165209905], [101624628701907996, (-3957494709010896684)], [121561286685622144]], [[(-5755208562637484), 219457936765310549, (-2142263511643483281), (-173812816374410244)], [(-4642822864655401), 203022588395636631, (-1974649159215291316)], [(-6158417043916429), 243001374028489575], [(-7693600976063918)]], [[319327715475275, (-11469590809544007), 108291540628649143, 20823535034845683, (-42898815510698135)], [224012603614715, (-9272241070884341), 101057721078197693, 4100171206867212], [276484722812099, (-12303087441142699), 121258377025933498], [385862484382359, (-15380099762052351)], [494271498800079]]], r := 92186930565247764, ok := true }, r1 := { p := [[[2315794787051746565907]], [[(-120032764481334873575), 0], [(-122543916403388813287)]], [[5817606007304501927, 0, 0], [6040070805282300151, 0], [7541057366781225335]], [[(-301631275268515065), 0, 0, 0], [(-269188747335178277), 0, 0], [(-367390950590427744), 0], [(-478376799915550538)]], [[16938220016547312, 0, 0, 0, 0], [13012213678531908, 0, 0, 0], [16058240137079658, 0, 0], [23128423248792064, 0], [30781065060114910]]], r := 145236939085773325, ok := true }, r2 := { p := [[[50620421214378378240920]], [[(-3346432981810365253351), 371878586105573801162], [(-6433397989550839784018)]], [[203050245916309242447, (-18471456354891081599), 487306141018325070], [412698933638709558832, (-22720418358591311634)], [622060008992765496337]], [[(-12560890984096786380), 976311940137777726, 1904155691623493, (-1525008422474464)], [(-24624548723932557382), 1017624671790326826, 1559770725713312], [(-39162826810474912653), 1485040896175612483], [(-53978020057305869626)]], [[795923531355950973, (-56011027205501895), (-66736555202117), 26297962258179, 4690434258118], [1512062137622892724, (-50608516024737479), 84140661926604, (-114800895954308)], [2312349050029326494, (-64282289590772311), (-13429423585026)], [3353050778163238311, (-97691262210687130)], [4415740487939401468]]], r := 32484005224185802310, ok := true }, r3 := { p := [[[537495868468143412630506]], [[(-71561464752678496599897), 4959532046225473487160], [(-73444485993805983422374)]], [[7152591471152493754161, (-602583088716753528527), 1587552040694891718], [9786420350378621820616, (-333221908534408335192)], [7404540214453845014612]], [[(-635624572730350890809), 58298351825763604171, 44435519044740216, (-10647209857388304)], [(-978443304161837817015), 40392009595150854005, (-1466594244454186)], [(-986885055681031562764), 22281870406566276155], [(-660866512705224662589)]], [[52960348143334543825, (-5095556528642720232), (-3468852797633503), 66029730612862, 66175488985421], [86963550277867697799, (-3903722045153603887), 832019487524925, (-760704809257928)], [98675693090039107603, (-2698004152588791514), 26343055956056], [88090445354525970678, (-1487638764817228732)], [55206810875112313906]]], r := 4706887876138059185411, ok := true }, eta := { p := [[[(-57298716159659178951008)]], [[3798283880798873298183, 0], [6846242029849099739921]], [[(-232340030208932903303), 0, 0], [(-440075227571266126850), 0], [(-649106695229661562737)]], [[14467226182421431810, 0, 0, 0], [26380194227772487521, 0, 0], [40940211072845014817, 0], [55761760039325566347]], [[(-920972246414665485), 0, 0, 0, 0], [(-1626040106819449140), 0, 0, 0], [(-2426069667032036381), 0, 0], [(-3469687080502834236), 0], [(-4533777676063633654)]]], r := 4260557984171549308, 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 432345564227567616 576460752303423488 0 4611686018427387904 3458764513820540928 4611686018427387904 :=
  (RegionPosI.split_b 504403158265495552 (RegionPosI.split_s 4035225266123964416 (RegionPosI.of_check c0 q0 ok_0 432345564227567616 504403158265495552 0 4611686018427387904 3458764513820540928 4035225266123964416 (by decide +kernel)) (RegionPosI.of_check c1 q1 ok_1 432345564227567616 504403158265495552 0 4611686018427387904 4035225266123964416 4611686018427387904 (by decide +kernel))) (RegionPosI.split_s 4035225266123964416 (RegionPosI.of_check c2 q2 ok_2 504403158265495552 576460752303423488 0 4611686018427387904 3458764513820540928 4035225266123964416 (by decide +kernel)) (RegionPosI.of_check c3 q3 ok_3 504403158265495552 576460752303423488 0 4611686018427387904 4035225266123964416 4611686018427387904 (by decide +kernel))))

end CKLaneC.RSC2.S09_0013

end