bug check 1901 and 1807 #174

icecream17 · 2024-07-28T19:20:53Z

In a mathbox, add the following to set.mm (there's definitely a shorter reproducible out there)

long proof (click to expand)

  ${
    evlsaddval.q $e |- Q = ( ( I evalSub S ) ` R ) $.
    evlsaddval.p $e |- P = ( I mPoly U ) $.
    evlsaddval.u $e |- U = ( S |`s R ) $.
    evlsaddval.k $e |- K = ( Base ` S ) $.
    evlsaddval.b $e |- B = ( Base ` P ) $.
    evlsaddval.i $e |- ( ph -> I e. Z ) $.
    evlsaddval.s $e |- ( ph -> S e. CRing ) $.
    evlsaddval.r $e |- ( ph -> R e. ( SubRing ` S ) ) $.
    evlsaddval.a $e |- ( ph -> A e. ( K ^m I ) ) $.
    evlsaddval.m $e |- ( ph -> ( M e. B /\ ( ( Q ` M ) ` A ) = V ) ) $.

    ${
      $d ph a b x $.  $d A a b x $.  $d I a b x $.  $d K a b x $.  $d M x $.
      $d N x $.  $d Q x $.  $d S a b x $.
      evlsexpval.g $e |- .xb = ( .g ` ( mulGrp ` P ) ) $.
      evlsexpval.f $e |- .^ = ( .g ` ( mulGrp ` S ) ) $.
      evlsexpval.n $e |- ( ph -> N e. NN0 ) $.
      $( Polynomial evaluation builder for exponentiation.  (Contributed by SN,
         27-Jul-2024.) $)
      evlsexpval $p |- ( ph -> ( ( N .xb M ) e. B /\
                               ( ( Q ` ( N .xb M ) ) ` A ) = ( N .^ V ) ) ) $=
        wph cN cM c.xb co cB wcel cA cN cM c.xb co cQ cfv cfv cN cV c.ex co
        wceq wph cP cmgp cfv cmnd wcel cN cn0 wcel cM cB wcel cN cM c.xb co cB
        wcel wph cQ cP cS cK cI cmap co cpws co crh co wcel cP crg wcel cP cmgp
        cfv cmnd wcel wph cI cV wcel cS ccrg wcel cR cS csubrg cfv wcel cQ cP
        cS cK cI cmap co cpws co crh co wcel evlsaddval.i evlsaddval.s
        evlsaddval.r cK cQ cR cS cS cK cI cmap co cpws co cU cI cZ cP
        evlsaddval.q evlsaddval.p evlsaddval.u cS cK cI cmap co cpws co eqid
        evlsaddval.k evlsrhm syl3anc cP cS cK cI cmap co cpws co cQ rhmrcl1 cP
        cP cmgp cfv cP cmgp cfv eqid ringmgp 3syl evlsexpval.n wph cM cB wcel
        cA cM cQ cfv cfv cV wceq evlsaddval.m simpld cB c.xb cP cmgp cfv cN cM
        cB cP cP cmgp cfv cP cmgp cfv eqid evlsaddval.b mgpbas evlsexpval.g
        mulgnn0cl syl3anc wph cA cN cM c.xb co cQ cfv cfv cA cN cM cQ cfv cS cK
        cI cmap co cpws co cmgp cfv cmg cfv co cfv cN cV c.ex co wph cA cN cM
        c.xb co cQ cfv cN cM cQ cfv cS cK cI cmap co cpws co cmgp cfv cmg cfv
        co wph cB cS cK cI cmap co cpws co cQ cR cS cU c.xb cP cmgp cfv cS cK
        cI cmap co cpws co cmgp cfv cI cK cN cV cP cM evlsaddval.q evlsaddval.p
        cP cmgp cfv eqid evlsexpval.g evlsaddval.u cS cK cI cmap co cpws co
        eqid cS cK cI cmap co cpws co cmgp cfv eqid evlsaddval.k evlsaddval.b
        evlsaddval.i evlsaddval.s evlsaddval.r evlsexpval.n wph cM cB wcel cA
        cM cQ cfv cfv cV wceq evlsaddval.m simpld evlspw fveq1d wph cA cN cM cQ
        cfv cS cK cI cmap co cpws co cmgp cfv cmg cfv co cfv cN cA cM cQ cfv
        cfv c.ex co cN cV c.ex co wph cN cM cQ cfv cS cK cI cmap co cpws co
        cmgp cfv cmg cfv co vx cS cK cI cmap co cpws co cbs cfv cA vx cv cfv
        cmpt cfv cN cM cQ cfv vx cS cK cI cmap co cpws co cbs cfv cA vx cv cfv
        cmpt cfv c.ex co cA cN cM cQ cfv cS cK cI cmap co cpws co cmgp cfv cmg
        cfv co cfv cN cA cM cQ cfv cfv c.ex co wph vx cS cK cI cmap co cpws co
        cbs cfv cA vx cv cfv cmpt cS cK cI cmap co cpws co cmgp cfv cS cmgp cfv
        cmhm co wcel cN cn0 wcel cM cQ cfv cS cK cI cmap co cpws co cbs cfv
        wcel cN cM cQ cfv cS cK cI cmap co cpws co cmgp cfv cmg cfv co vx cS cK
        cI cmap co cpws co cbs cfv cA vx cv cfv cmpt cfv cN cM cQ cfv vx cS cK
        cI cmap co cpws co cbs cfv cA vx cv cfv cmpt cfv c.ex co wceq wph va vb
        cS cK cI cmap co cpws co cbs cfv cK cS cK cI cmap co cpws co cmulr cfv
        cS cmulr cfv cS cK cI cmap co cpws co cmgp cfv cS cmgp cfv vx cS cK cI
        cmap co cpws co cbs cfv cA vx cv cfv cmpt cS cK cI cmap co cpws co cur
        cfv cS cur cfv cS cK cI cmap co cpws co cbs cfv cS cK cI cmap co cpws
        co cS cK cI cmap co cpws co cmgp cfv cS cK cI cmap co cpws co cmgp cfv
        eqid cS cK cI cmap co cpws co cbs cfv eqid mgpbas cK cS cS cmgp cfv cS
        cmgp cfv eqid evlsaddval.k mgpbas cS cK cI cmap co cpws co cS cK cI
        cmap co cpws co cmulr cfv cS cK cI cmap co cpws co cmgp cfv cS cK cI
        cmap co cpws co cmgp cfv eqid cS cK cI cmap co cpws co cmulr cfv eqid
        mgpplusg cS cS cmulr cfv cS cmgp cfv cS cmgp cfv eqid cS cmulr cfv eqid
        mgpplusg cS cK cI cmap co cpws co cS cK cI cmap co cpws co cur cfv cS
        cK cI cmap co cpws co cmgp cfv cS cK cI cmap co cpws co cmgp cfv eqid
        cS cK cI cmap co cpws co cur cfv eqid ringidval cS cS cur cfv cS cmgp
        cfv cS cmgp cfv eqid cS cur cfv eqid ringidval wph cS cK cI cmap co
        cpws co crg wcel cS cK cI cmap co cpws co cmgp cfv cmnd wcel wph cS crg
        wcel cK cI cmap co cvv wcel cS cK cI cmap co cpws co crg wcel wph cS
        evlsaddval.s crngringd wph cK cI cmap ovexd cS cK cI cmap co cvv cS cK
        cI cmap co cpws co cS cK cI cmap co cpws co eqid pwsring syl2anc cS cK
        cI cmap co cpws co cS cK cI cmap co cpws co cmgp cfv cS cK cI cmap co
        cpws co cmgp cfv eqid ringmgp syl wph cS crg wcel cS cmgp cfv cmnd wcel
        wph cS evlsaddval.s crngringd cS cS cmgp cfv cS cmgp cfv eqid ringmgp
        syl wph vx cS cK cI cmap co cpws co cbs cfv cA vx cv cfv cK wph vx cv
        cS cK cI cmap co cpws co cbs cfv wcel wa cK cI cmap co cK cA vx cv wph
        vx cv cS cK cI cmap co cpws co cbs cfv wcel wa cK cS cK cI cmap co cS
        cK cI cmap co cpws co cbs cfv ccrg vx cv cS cK cI cmap co cpws co cvv
        cS cK cI cmap co cpws co eqid evlsaddval.k cS cK cI cmap co cpws co cbs
        cfv eqid wph cS ccrg wcel vx cv cS cK cI cmap co cpws co cbs cfv wcel
        evlsaddval.s adantr wph vx cv cS cK cI cmap co cpws co cbs cfv wcel wa
        cK cI cmap ovexd wph vx cv cS cK cI cmap co cpws co cbs cfv wcel simpr
        pwselbas wph cA cK cI cmap co wcel vx cv cS cK cI cmap co cpws co cbs
        cfv wcel evlsaddval.a adantr ffvelrnd fmpttd wph va cv cS cK cI cmap co
        cpws co cbs cfv wcel vb cv cS cK cI cmap co cpws co cbs cfv wcel wa wa
        cA va cv vb cv cS cK cI cmap co cpws co cmulr cfv co cfv cA va cv cfv
        cA vb cv cfv cS cmulr cfv co va cv vb cv cS cK cI cmap co cpws co cmulr
        cfv co vx cS cK cI cmap co cpws co cbs cfv cA vx cv cfv cmpt cfv va cv
        vx cS cK cI cmap co cpws co cbs cfv cA vx cv cfv cmpt cfv vb cv vx cS
        cK cI cmap co cpws co cbs cfv cA vx cv cfv cmpt cfv cS cmulr cfv co wph
        va cv cS cK cI cmap co cpws co cbs cfv wcel vb cv cS cK cI cmap co cpws
        co cbs cfv wcel wa wa cA va cv vb cv cS cK cI cmap co cpws co cmulr cfv
        co cfv cA va cv vb cv cS cmulr cfv cof co cfv cA va cv cfv cA vb cv cfv
        cS cmulr cfv co wph va cv cS cK cI cmap co cpws co cbs cfv wcel vb cv
        cS cK cI cmap co cpws co cbs cfv wcel wa wa cA va cv vb cv cS cK cI
        cmap co cpws co cmulr cfv co va cv vb cv cS cmulr cfv cof co wph va cv
        cS cK cI cmap co cpws co cbs cfv wcel vb cv cS cK cI cmap co cpws co
        cbs cfv wcel wa wa cS cK cI cmap co cpws co cbs cfv cS cS cK cI cmap co
        cpws co cmulr cfv cS cmulr cfv va cv vb cv cK cI cmap co ccrg cvv cS cK
        cI cmap co cpws co cS cK cI cmap co cpws co eqid cS cK cI cmap co cpws
        co cbs cfv eqid wph cS ccrg wcel va cv cS cK cI cmap co cpws co cbs cfv
        wcel vb cv cS cK cI cmap co cpws co cbs cfv wcel wa evlsaddval.s adantr
        wph va cv cS cK cI cmap co cpws co cbs cfv wcel vb cv cS cK cI cmap co
        cpws co cbs cfv wcel wa wa cK cI cmap ovexd wph va cv cS cK cI cmap co
        cpws co cbs cfv wcel vb cv cS cK cI cmap co cpws co cbs cfv wcel simprl
        wph va cv cS cK cI cmap co cpws co cbs cfv wcel vb cv cS cK cI cmap co
        cpws co cbs cfv wcel simprr cS cmulr cfv eqid cS cK cI cmap co cpws co
        cmulr cfv eqid pwsmulrval fveq1d wph va cv cS cK cI cmap co cpws co cbs
        cfv wcel vb cv cS cK cI cmap co cpws co cbs cfv wcel wa cA cK cI cmap
        co wcel cA va cv vb cv cS cmulr cfv cof co cfv cA va cv cfv cA vb cv
        cfv cS cmulr cfv co wceq evlsaddval.a wph va cv cS cK cI cmap co cpws
        co cbs cfv wcel vb cv cS cK cI cmap co cpws co cbs cfv wcel wa wa cK cI
        cmap co cK cI cmap co cA va cv cfv cA vb cv cfv cS cmulr cfv cK cI cmap
        co va cv vb cv cvv cvv cA wph va cv cS cK cI cmap co cpws co cbs cfv
        wcel vb cv cS cK cI cmap co cpws co cbs cfv wcel wa wa cK cI cmap co cK
        va cv wph va cv cS cK cI cmap co cpws co cbs cfv wcel vb cv cS cK cI
        cmap co cpws co cbs cfv wcel wa wa cK cS cK cI cmap co cS cK cI cmap co
        cpws co cbs cfv ccrg va cv cS cK cI cmap co cpws co cvv cS cK cI cmap
        co cpws co eqid evlsaddval.k cS cK cI cmap co cpws co cbs cfv eqid wph
        cS ccrg wcel va cv cS cK cI cmap co cpws co cbs cfv wcel vb cv cS cK cI
        cmap co cpws co cbs cfv wcel wa evlsaddval.s adantr wph va cv cS cK cI
        cmap co cpws co cbs cfv wcel vb cv cS cK cI cmap co cpws co cbs cfv
        wcel wa wa cK cI cmap ovexd wph va cv cS cK cI cmap co cpws co cbs cfv
        wcel vb cv cS cK cI cmap co cpws co cbs cfv wcel simprl pwselbas ffnd
        wph va cv cS cK cI cmap co cpws co cbs cfv wcel vb cv cS cK cI cmap co
        cpws co cbs cfv wcel wa wa cK cI cmap co cK vb cv wph va cv cS cK cI
        cmap co cpws co cbs cfv wcel vb cv cS cK cI cmap co cpws co cbs cfv
        wcel wa wa cK cS cK cI cmap co cS cK cI cmap co cpws co cbs cfv ccrg vb
        cv cS cK cI cmap co cpws co cvv cS cK cI cmap co cpws co eqid
        evlsaddval.k cS cK cI cmap co cpws co cbs cfv eqid wph cS ccrg wcel va
        cv cS cK cI cmap co cpws co cbs cfv wcel vb cv cS cK cI cmap co cpws co
        cbs cfv wcel wa evlsaddval.s adantr wph va cv cS cK cI cmap co cpws co
        cbs cfv wcel vb cv cS cK cI cmap co cpws co cbs cfv wcel wa wa cK cI
        cmap ovexd wph va cv cS cK cI cmap co cpws co cbs cfv wcel vb cv cS cK
        cI cmap co cpws co cbs cfv wcel simprr pwselbas ffnd wph va cv cS cK cI
        cmap co cpws co cbs cfv wcel vb cv cS cK cI cmap co cpws co cbs cfv
        wcel wa wa cK cI cmap ovexd wph va cv cS cK cI cmap co cpws co cbs cfv
        wcel vb cv cS cK cI cmap co cpws co cbs cfv wcel wa wa cK cI cmap ovexd
        cK cI cmap co inidm wph va cv cS cK cI cmap co cpws co cbs cfv wcel vb
        cv cS cK cI cmap co cpws co cbs cfv wcel wa wa cA cK cI cmap co wcel wa
        cA va cv cfv eqidd wph va cv cS cK cI cmap co cpws co cbs cfv wcel vb
        cv cS cK cI cmap co cpws co cbs cfv wcel wa wa cA cK cI cmap co wcel wa
        cA vb cv cfv eqidd ofval mpidan eqtrd wph va cv cS cK cI cmap co cpws
        co cbs cfv wcel vb cv cS cK cI cmap co cpws co cbs cfv wcel wa wa va cv
        vb cv cS cK cI cmap co cpws co cmulr cfv co cS cK cI cmap co cpws co
        cbs cfv wcel va cv vb cv cS cK cI cmap co cpws co cmulr cfv co vx cS cK
        cI cmap co cpws co cbs cfv cA vx cv cfv cmpt cfv cA va cv vb cv cS cK
        cI cmap co cpws co cmulr cfv co cfv wceq wph va cv cS cK cI cmap co
        cpws co cbs cfv wcel vb cv cS cK cI cmap co cpws co cbs cfv wcel wa wa
        cS cK cI cmap co cpws co crg wcel va cv cS cK cI cmap co cpws co cbs
        cfv wcel vb cv cS cK cI cmap co cpws co cbs cfv wcel va cv vb cv cS cK
        cI cmap co cpws co cmulr cfv co cS cK cI cmap co cpws co cbs cfv wcel
        wph cS cK cI cmap co cpws co crg wcel va cv cS cK cI cmap co cpws co
        cbs cfv wcel vb cv cS cK cI cmap co cpws co cbs cfv wcel wa wph cS crg
        wcel cK cI cmap co cvv wcel cS cK cI cmap co cpws co crg wcel wph cS
        evlsaddval.s crngringd wph cK cI cmap ovexd cS cK cI cmap co cvv cS cK
        cI cmap co cpws co cS cK cI cmap co cpws co eqid pwsring syl2anc adantr
        wph va cv cS cK cI cmap co cpws co cbs cfv wcel vb cv cS cK cI cmap co
        cpws co cbs cfv wcel simprl wph va cv cS cK cI cmap co cpws co cbs cfv
        wcel vb cv cS cK cI cmap co cpws co cbs cfv wcel simprr cS cK cI cmap
        co cpws co cbs cfv cS cK cI cmap co cpws co cS cK cI cmap co cpws co
        cmulr cfv va cv vb cv cS cK cI cmap co cpws co cbs cfv eqid cS cK cI
        cmap co cpws co cmulr cfv eqid ringcl syl3anc vx va cv vb cv cS cK cI
        cmap co cpws co cmulr cfv co cA vx cv cfv cA va cv vb cv cS cK cI cmap
        co cpws co cmulr cfv co cfv cS cK cI cmap co cpws co cbs cfv vx cS cK
        cI cmap co cpws co cbs cfv cA vx cv cfv cmpt cA vx cv va cv vb cv cS cK
        cI cmap co cpws co cmulr cfv co fveq1 vx cS cK cI cmap co cpws co cbs
        cfv cA vx cv cfv cmpt eqid cA va cv vb cv cS cK cI cmap co cpws co
        cmulr cfv co fvex fvmpt syl wph va cv cS cK cI cmap co cpws co cbs cfv
        wcel vb cv cS cK cI cmap co cpws co cbs cfv wcel wa wa va cv vx cS cK
        cI cmap co cpws co cbs cfv cA vx cv cfv cmpt cfv cA va cv cfv vb cv vx
        cS cK cI cmap co cpws co cbs cfv cA vx cv cfv cmpt cfv cA vb cv cfv cS
        cmulr cfv wph va cv cS cK cI cmap co cpws co cbs cfv wcel vb cv cS cK
        cI cmap co cpws co cbs cfv wcel wa wa va cv cS cK cI cmap co cpws co
        cbs cfv wcel va cv vx cS cK cI cmap co cpws co cbs cfv cA vx cv cfv
        cmpt cfv cA va cv cfv wceq wph va cv cS cK cI cmap co cpws co cbs cfv
        wcel vb cv cS cK cI cmap co cpws co cbs cfv wcel simprl vx va cv cA vx
        cv cfv cA va cv cfv cS cK cI cmap co cpws co cbs cfv vx cS cK cI cmap
        co cpws co cbs cfv cA vx cv cfv cmpt cA vx cv va cv fveq1 vx cS cK cI
        cmap co cpws co cbs cfv cA vx cv cfv cmpt eqid cA va cv fvex fvmpt syl
        wph va cv cS cK cI cmap co cpws co cbs cfv wcel vb cv cS cK cI cmap co
        cpws co cbs cfv wcel wa wa vb cv cS cK cI cmap co cpws co cbs cfv wcel
        vb cv vx cS cK cI cmap co cpws co cbs cfv cA vx cv cfv cmpt cfv cA vb
        cv cfv wceq wph va cv cS cK cI cmap co cpws co cbs cfv wcel vb cv cS cK
        cI cmap co cpws co cbs cfv wcel simprr vx vb cv cA vx cv cfv cA vb cv
        cfv cS cK cI cmap co cpws co cbs cfv vx cS cK cI cmap co cpws co cbs
        cfv cA vx cv cfv cmpt cA vx cv vb cv fveq1 vx cS cK cI cmap co cpws co
        cbs cfv cA vx cv cfv cmpt eqid cA vb cv fvex fvmpt syl oveq12d 3eqtr4d
        wph cS cK cI cmap co cpws co cur cfv vx cS cK cI cmap co cpws co cbs
        cfv cA vx cv cfv cmpt cfv cA cS cK cI cmap co cpws co cur cfv cfv cA cK
        cI cmap co cS cur cfv csn cxp cfv cS cur cfv wph cS cK cI cmap co cpws
        co crg wcel cS cK cI cmap co cpws co cur cfv cS cK cI cmap co cpws co
        cbs cfv wcel cS cK cI cmap co cpws co cur cfv vx cS cK cI cmap co cpws
        co cbs cfv cA vx cv cfv cmpt cfv cA cS cK cI cmap co cpws co cur cfv
        cfv wceq wph cS crg wcel cK cI cmap co cvv wcel cS cK cI cmap co cpws
        co crg wcel wph cS evlsaddval.s crngringd wph cK cI cmap ovexd cS cK cI
        cmap co cvv cS cK cI cmap co cpws co cS cK cI cmap co cpws co eqid
        pwsring syl2anc cS cK cI cmap co cpws co cbs cfv cS cK cI cmap co cpws
        co cS cK cI cmap co cpws co cur cfv cS cK cI cmap co cpws co cbs cfv
        eqid cS cK cI cmap co cpws co cur cfv eqid ringidcl vx cS cK cI cmap co
        cpws co cur cfv cA vx cv cfv cA cS cK cI cmap co cpws co cur cfv cfv cS
        cK cI cmap co cpws co cbs cfv vx cS cK cI cmap co cpws co cbs cfv cA vx
        cv cfv cmpt cA vx cv cS cK cI cmap co cpws co cur cfv fveq1 vx cS cK cI
        cmap co cpws co cbs cfv cA vx cv cfv cmpt eqid cA cS cK cI cmap co cpws
        co cur cfv fvex fvmpt 3syl wph cA cK cI cmap co cS cur cfv csn cxp cS
        cK cI cmap co cpws co cur cfv wph cS crg wcel cK cI cmap co cvv wcel cK
        cI cmap co cS cur cfv csn cxp cS cK cI cmap co cpws co cur cfv wceq wph
        cS evlsaddval.s crngringd wph cK cI cmap ovexd cS cS cur cfv cK cI cmap
        co cvv cS cK cI cmap co cpws co cS cK cI cmap co cpws co eqid cS cur
        cfv eqid pws1 syl2anc fveq1d wph cA cK cI cmap co wcel cA cK cI cmap co
        cS cur cfv csn cxp cfv cS cur cfv wceq evlsaddval.a cK cI cmap co cS
        cur cfv cA cS cur fvex fvconst2 syl 3eqtr2d ismhmd evlsexpval.n wph cB
        cS cK cI cmap co cpws co cbs cfv cM cQ wph cQ cP cS cK cI cmap co cpws
        co crh co wcel cB cS cK cI cmap co cpws co cbs cfv cQ wf wph cI cV wcel
        cS ccrg wcel cR cS csubrg cfv wcel cQ cP cS cK cI cmap co cpws co crh
        co wcel evlsaddval.i evlsaddval.s evlsaddval.r cK cQ cR cS cS cK cI
        cmap co cpws co cU cI cV cP evlsaddval.q evlsaddval.p evlsaddval.u cS
        cK cI cmap co cpws co eqid evlsaddval.k evlsrhm syl3anc cB cS cK cI
        cmap co cpws co cbs cfv cP cS cK cI cmap co cpws co cQ evlsaddval.b cS
        cK cI cmap co cpws co cbs cfv eqid rhmf syl wph cM cB wcel cA cM cQ cfv
        cfv cV wceq evlsaddval.m simpld ffvelrnd cS cK cI cmap co cpws co cbs
        cfv cS cK cI cmap co cpws co cmgp cfv cmg cfv c.ex vx cS cK cI cmap co
        cpws co cbs cfv cA vx cv cfv cmpt cS cK cI cmap co cpws co cmgp cfv cS
        cmgp cfv cN cM cQ cfv cS cK cI cmap co cpws co cbs cfv cS cK cI cmap co
        cpws co cS cK cI cmap co cpws co cmgp cfv cS cK cI cmap co cpws co cmgp
        cfv eqid cS cK cI cmap co cpws co cbs cfv eqid mgpbas cS cK cI cmap co
        cpws co cmgp cfv cmg cfv eqid evlsexpval.f mhmmulg syl3anc wph cN cM cQ
        cfv cS cK cI cmap co cpws co cmgp cfv cmg cfv co cS cK cI cmap co cpws
        co cbs cfv wcel cN cM cQ cfv cS cK cI cmap co cpws co cmgp cfv cmg cfv
        co vx cS cK cI cmap co cpws co cbs cfv cA vx cv cfv cmpt cfv cA cN cM
        cQ cfv cS cK cI cmap co cpws co cmgp cfv cmg cfv co cfv wceq wph cS cK
        cI cmap co cpws co cmgp cfv cmnd wcel cN cn0 wcel cM cQ cfv cS cK cI
        cmap co cpws co cbs cfv wcel cN cM cQ cfv cS cK cI cmap co cpws co cmgp
        cfv cmg cfv co cS cK cI cmap co cpws co cbs cfv wcel wph cS cK cI cmap
        co cpws co crg wcel cS cK cI cmap co cpws co cmgp cfv cmnd wcel wph cS
        crg wcel cK cI cmap co cvv wcel cS cK cI cmap co cpws co crg wcel wph
        cS evlsaddval.s crngringd wph cK cI cmap ovexd cS cK cI cmap co cvv cS
        cK cI cmap co cpws co cS cK cI cmap co cpws co eqid pwsring syl2anc cS
        cK cI cmap co cpws co cS cK cI cmap co cpws co cmgp cfv cS cK cI cmap
        co cpws co cmgp cfv eqid ringmgp syl evlsexpval.n wph cB cS cK cI cmap
        co cpws co cbs cfv cM cQ wph cQ cP cS cK cI cmap co cpws co crh co wcel
        cB cS cK cI cmap co cpws co cbs cfv cQ wf wph cI cV wcel cS ccrg wcel
        cR cS csubrg cfv wcel cQ cP cS cK cI cmap co cpws co crh co wcel
        evlsaddval.i evlsaddval.s evlsaddval.r cK cQ cR cS cS cK cI cmap co
        cpws co cU cI cV cP evlsaddval.q evlsaddval.p evlsaddval.u cS cK cI
        cmap co cpws co eqid evlsaddval.k evlsrhm syl3anc cB cS cK cI cmap co
        cpws co cbs cfv cP cS cK cI cmap co cpws co cQ evlsaddval.b cS cK cI
        cmap co cpws co cbs cfv eqid rhmf syl wph cM cB wcel cA cM cQ cfv cfv
        cV wceq evlsaddval.m simpld ffvelrnd cS cK cI cmap co cpws co cbs cfv
        cS cK cI cmap co cpws co cmgp cfv cmg cfv cS cK cI cmap co cpws co cmgp
        cfv cN cM cQ cfv cS cK cI cmap co cpws co cbs cfv cS cK cI cmap co cpws
        co cS cK cI cmap co cpws co cmgp cfv cS cK cI cmap co cpws co cmgp cfv
        eqid cS cK cI cmap co cpws co cbs cfv eqid mgpbas cS cK cI cmap co cpws
        co cmgp cfv cmg cfv eqid mulgnn0cl syl3anc vx cN cM cQ cfv cS cK cI
        cmap co cpws co cmgp cfv cmg cfv co cA vx cv cfv cA cN cM cQ cfv cS cK
        cI cmap co cpws co cmgp cfv cmg cfv co cfv cS cK cI cmap co cpws co cbs
        cfv vx cS cK cI cmap co cpws co cbs cfv cA vx cv cfv cmpt cA vx cv cN
        cM cQ cfv cS cK cI cmap co cpws co cmgp cfv cmg cfv co fveq1 vx cS cK
        cI cmap co cpws co cbs cfv cA vx cv cfv cmpt eqid cA cN cM cQ cfv cS cK
        cI cmap co cpws co cmgp cfv cmg cfv co fvex fvmpt syl wph cM cQ cfv vx
        cS cK cI cmap co cpws co cbs cfv cA vx cv cfv cmpt cfv cA cM cQ cfv cfv
        cN c.ex wph cM cQ cfv cS cK cI cmap co cpws co cbs cfv wcel cM cQ cfv
        vx cS cK cI cmap co cpws co cbs cfv cA vx cv cfv cmpt cfv cA cM cQ cfv
        cfv wceq wph cB cS cK cI cmap co cpws co cbs cfv cM cQ wph cQ cP cS cK
        cI cmap co cpws co crh co wcel cB cS cK cI cmap co cpws co cbs cfv cQ
        wf wph cI cV wcel cS ccrg wcel cR cS csubrg cfv wcel cQ cP cS cK cI
        cmap co cpws co crh co wcel evlsaddval.i evlsaddval.s evlsaddval.r cK
        cQ cR cS cS cK cI cmap co cpws co cU cI cV cP evlsaddval.q evlsaddval.p
        evlsaddval.u cS cK cI cmap co cpws co eqid evlsaddval.k evlsrhm syl3anc
        cB cS cK cI cmap co cpws co cbs cfv cP cS cK cI cmap co cpws co cQ
        evlsaddval.b cS cK cI cmap co cpws co cbs cfv eqid rhmf syl wph cM cB
        wcel cA cM cQ cfv cfv cV wceq evlsaddval.m simpld ffvelrnd vx cM cQ cfv
        cA vx cv cfv cA cM cQ cfv cfv cS cK cI cmap co cpws co cbs cfv vx cS cK
        cI cmap co cpws co cbs cfv cA vx cv cfv cmpt cA vx cv cM cQ cfv fveq1
        vx cS cK cI cmap co cpws co cbs cfv cA vx cv cfv cmpt eqid cA cM cQ cfv
        fvex fvmpt syl oveq2d 3eqtr3d wph cA cM cQ cfv cfv cV cN c.ex wph cM cB
        wcel cA cM cQ cfv cfv cV wceq evlsaddval.m simprd oveq2d eqtrd eqtrd
        jca $.
    $}
  $}

then

prove evlsexpval
min *

Basically I call minimize_all on a "completed proof" that doesn't unify because a variable is incorrect somewhere (in this case I changed I e. V to I e. Z since V is already used)

metamath.exe already notes that the situation is questionable so this bug isn't particularly important

logs: prove command, min command

MM> prove evlsexpval
Entering the Proof Assistant.  HELP PROOF_ASSISTANT for help, EXIT to exit.

?Error on line 639871 of file "set.mm" at statement 176350, label "evlsexpval",
type "$p":
        evlsaddval.k evlsrhm syl3anc cP cS cK cI cmap co cpws co cQ rhmrcl1 cP
                             ^^^^^^^
The hypotheses of statement "syl3anc" at proof step 115 cannot be unified.
  Hypothesis 1:  wff ph
  Step 60:  wff ph
  Hypothesis 2:  wff ps
  Step 63:  wff I e. V
  Hypothesis 3:  wff ch
  Step 66:  wff S e. CRing
  Hypothesis 4:  wff th
  Step 71:  wff R e. ( SubRing ` S )
  Hypothesis 5:  wff ta
  Step 83:  wff Q e. ( P RingHom ( S ^s ( K ^m I ) ) )
  Hypothesis 6:  |- ( ph -> ps )
  Step 84:  |- ( ph -> I e. Z )
  Hypothesis 7:  |- ( ph -> ch )
  Step 85:  |- ( ph -> S e. CRing )
  Hypothesis 8:  |- ( ph -> th )
  Step 86:  |- ( ph -> R e. ( SubRing ` S ) )
  Hypothesis 9:  |- ( ( ps /\ ch /\ th ) -> ta )
  Step 114:  |- ( ( I e. Z /\ S e. CRing /\ R e. ( SubRing ` S ) ) -> Q e. ( P
RingHom ( S ^s ( K ^m I ) ) ) )
?Error in step 115:  Could not simultaneously unify the hypotheses of
"syl3anc":
    $|$ wff $1 $|$ wff $3 $|$ wff $4 $|$ wff $5 $|$ wff $2 $|$ |- ( $1 -> $3 )
$|$ |- ( $1 -> $4 ) $|$ |- ( $1 -> $5 ) $|$ |- ( ( $3 /\ $4 /\ $5 ) -> $2 ) $|$
with the following statement list:
    $|$ wff ph $|$ wff I e. V $|$ wff S e. CRing $|$ wff R e. ( SubRing ` S )
$|$ wff Q e. ( P RingHom ( S ^s ( K ^m I ) ) ) $|$ |- ( ph -> I e. Z ) $|$ |- (
ph -> S e. CRing ) $|$ |- ( ph -> R e. ( SubRing ` S ) ) $|$ |- ( ( I e. Z /\ S
e. CRing /\ R e. ( SubRing ` S ) ) -> Q e. ( P RingHom ( S ^s ( K ^m I ) ) ) )
$|$
(The $|$ tokens are internal statement separation markers)
Zapping targets so we can proceed (but you should exit the Proof Assistant and
fix this problem)
(This may take a while; please wait...)
Step 84 cannot be unified.  THERE IS AN ERROR IN THE PROOF.
Step 114 cannot be unified.  THERE IS AN ERROR IN THE PROOF.
Step 286 cannot be unified.  THERE IS AN ERROR IN THE PROOF.
Step 3524 cannot be unified.  THERE IS AN ERROR IN THE PROOF.
Step 4010 cannot be unified.  THERE IS AN ERROR IN THE PROOF.
Step 4428 cannot be unified.  THERE IS AN ERROR IN THE PROOF.
Step 84 cannot be unified.  THERE IS AN ERROR IN THE PROOF.
Step 114 cannot be unified.  THERE IS AN ERROR IN THE PROOF.
Step 286 cannot be unified.  THERE IS AN ERROR IN THE PROOF.
Step 3524 cannot be unified.  THERE IS AN ERROR IN THE PROOF.
Step 4010 cannot be unified.  THERE IS AN ERROR IN THE PROOF.
Step 4428 cannot be unified.  THERE IS AN ERROR IN THE PROOF.
You will be working on statement (from "SHOW STATEMENT evlsexpval"):
176328 evlsaddval.q $e |- Q = ( ( I evalSub S ) ` R ) $.
176329 evlsaddval.p $e |- P = ( I mPoly U ) $.
176330 evlsaddval.u $e |- U = ( S |`s R ) $.
176331 evlsaddval.k $e |- K = ( Base ` S ) $.
176332 evlsaddval.b $e |- B = ( Base ` P ) $.
176333 evlsaddval.i $e |- ( ph -> I e. Z ) $.
176334 evlsaddval.s $e |- ( ph -> S e. CRing ) $.
176335 evlsaddval.r $e |- ( ph -> R e. ( SubRing ` S ) ) $.
176336 evlsaddval.a $e |- ( ph -> A e. ( K ^m I ) ) $.
176337 evlsaddval.m $e |- ( ph -> ( M e. B /\ ( ( Q ` M ) ` A ) = V ) ) $.
176347 evlsexpval.g $e |- .xb = ( .g ` ( mulGrp ` P ) ) $.
176348 evlsexpval.f $e |- .^ = ( .g ` ( mulGrp ` S ) ) $.
176349 evlsexpval.n $e |- ( ph -> N e. NN0 ) $.
176350 evlsexpval $p |- ( ph -> ( ( N .xb M ) e. B /\ ( ( Q ` ( N .xb M ) ) ` A
      ) = ( N .^ V ) ) ) $= ... $.
Note:  The proof you are starting with is already complete.
MM-PA> min *
Bytes refer to compressed proof size, steps to uncompressed length.
Scanning forward through statements...
?Error in step 3532:  Could not simultaneously unify the hypotheses of
"syl3anc":
    $|$ wff $4253 $|$ wff $4255 $|$ wff $4256 $|$ wff $4257 $|$ wff $4254 $|$
|- ( $4253 -> $4255 ) $|$ |- ( $4253 -> $4256 ) $|$ |- ( $4253 -> $4257 ) $|$
|- ( ( $4255 /\ $4256 /\ $4257 ) -> $4254 ) $|$
with the following statement list:
    $|$ wff ph $|$ wff I e. V $|$ wff S e. CRing $|$ wff R e. ( SubRing ` S )
$|$ wff Q e. ( P RingHom ( S ^s ( K ^m I ) ) ) $|$ |- ( ph -> I e. Z ) $|$ |- (
ph -> S e. CRing ) $|$ |- ( ph -> R e. ( SubRing ` S ) ) $|$ |- ( ( I e. V /\ S
e. CRing /\ R e. ( SubRing ` S ) ) -> Q e. ( P RingHom ( S ^s ( K ^m I ) ) ) )
$|$
(The $|$ tokens are internal statement separation markers)
Zapping targets so we can proceed (but you should exit the Proof Assistant and
fix this problem)
(This may take a while; please wait...)
?BUG CHECK:  *** DETECTED BUG 1901

To get technical support, please send Norm Megill ([email protected]) the
detailed command sequence or a command file that reproduces this bug,
along with the source file that was used.  See HELP LOG for help on
recording a session.  See HELP SUBMIT for help on command files.  Search
for "bug(1901)" in the m*.c source code to find its origin.
If earlier errors were reported, try fixing them first, because they
may occasionally lead to false bug detection

Press S <return> to step to next bug, I <return> to ignore further bugs,
or A <return> to abort program:  S

Warning!!!  A bug was detected, but you are continuing anyway.
The program may be corrupted, so you are proceeding at your own risk.

?BUG CHECK:  *** DETECTED BUG 1901
Press S <return> to step to next bug, I <return> to ignore further bugs,
or A <return> to abort program:  S
?BUG CHECK:  *** DETECTED BUG 1901
Press S <return> to step to next bug, I <return> to ignore further bugs,
or A <return> to abort program:  S
?BUG CHECK:  *** DETECTED BUG 1901
Press S <return> to step to next bug, I <return> to ignore further bugs,
or A <return> to abort program:  S
?BUG CHECK:  *** DETECTED BUG 1901
Press S <return> to step to next bug, I <return> to ignore further bugs,
or A <return> to abort program:  S
?BUG CHECK:  *** DETECTED BUG 1901
Press S <return> to step to next bug, I <return> to ignore further bugs,
or A <return> to abort program:  I
?BUG CHECK:  *** DETECTED BUG 1901, IGNORING IT...
?BUG CHECK:  *** DETECTED BUG 1901, IGNORING IT...
?BUG CHECK:  *** DETECTED BUG 1901, IGNORING IT...
?BUG CHECK:  *** DETECTED BUG 1901, IGNORING IT...
?BUG CHECK:  *** DETECTED BUG 1901, IGNORING IT...
?BUG CHECK:  *** DETECTED BUG 1901, IGNORING IT...
?BUG CHECK:  *** DETECTED BUG 1901, IGNORING IT...
?BUG CHECK:  *** DETECTED BUG 1901, IGNORING IT...
?BUG CHECK:  *** DETECTED BUG 1901, IGNORING IT...
?BUG CHECK:  *** DETECTED BUG 1901, IGNORING IT...
?BUG CHECK:  *** DETECTED BUG 1901, IGNORING IT...

a few hundred lines later...

?BUG CHECK:  *** DETECTED BUG 1901, IGNORING IT...
?BUG CHECK:  *** DETECTED BUG 1901, IGNORING IT...
?BUG CHECK:  *** DETECTED BUG 1901, IGNORING IT...
?BUG CHECK:  *** DETECTED BUG 1901, IGNORING IT...
?BUG CHECK:  *** DETECTED BUG 1901, IGNORING IT...
?BUG CHECK:  *** DETECTED BUG 1901, IGNORING IT...
?BUG CHECK:  *** DETECTED BUG 1901, IGNORING IT...
?BUG CHECK:  *** DETECTED BUG 1901, IGNORING IT...
?BUG CHECK:  *** DETECTED BUG 1901, IGNORING IT...
?BUG CHECK:  *** DETECTED BUG 1901, IGNORING IT...
?BUG CHECK:  *** DETECTED BUG 1901, IGNORING IT...
?BUG CHECK:  *** DETECTED BUG 1901, IGNORING IT...
?BUG CHECK:  *** DETECTED BUG 1901, IGNORING IT...
?BUG CHECK:  *** DETECTED BUG 1901, IGNORING IT...
?BUG CHECK:  *** DETECTED BUG 1901, IGNORING IT...
?BUG CHECK:  *** DETECTED BUG 1901, IGNORING IT...
?BUG CHECK:  *** DETECTED BUG 1807, IGNORING IT...
?BUG CHECK:  *** DETECTED BUG 1807, IGNORING IT...
?BUG CHECK:  *** DETECTED BUG 1807, IGNORING IT...
?BUG CHECK:  *** DETECTED BUG 1807, IGNORING IT...
?BUG CHECK:  *** DETECTED BUG 1807, IGNORING IT...
?BUG CHECK:  *** DETECTED BUG 1807, IGNORING IT...
?BUG CHECK:  *** DETECTED BUG 1807, IGNORING IT...
?BUG CHECK:  *** DETECTED BUG 1807, IGNORING IT...
?BUG CHECK:  *** DETECTED BUG 1807, IGNORING IT...
?BUG CHECK:  *** DETECTED BUG 1807, IGNORING IT...
?BUG CHECK:  *** DETECTED BUG 1807, IGNORING IT...
?BUG CHECK:  *** DETECTED BUG 1807, IGNORING IT...
?BUG CHECK:  *** DETECTED BUG 1807, IGNORING IT...
?BUG CHECK:  *** DETECTED BUG 1807, IGNORING IT...
?BUG CHECK:  *** DETECTED BUG 1807, IGNORING IT...

eventually...

?BUG CHECK:  *** DETECTED BUG 1807, IGNORING IT...
?BUG CHECK:  *** DETECTED BUG 1807, IGNORING IT...
No shorter proof was found.
(Other mathboxes were not checked.  Use / INCLUDE_MATHBOXES to include them.)
MM-PA>

It's basically a version of this, but complicated enough that theorems are actually applicable:

  ${
    $d ph x y $.  $d A x y $.
    bug.1 $e |- A e. _V $.
    bug $p |- { x e. { y e. A | ph } | ps } e. _V $=
      wps vx wph vy cA crab wph vy cB bug.1 rabex rabex $.
      $(                           ^^ should be cA $)
  $}

The text was updated successfully, but these errors were encountered:

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

bug check 1901 and 1807 #174

bug check 1901 and 1807 #174

icecream17 commented Jul 28, 2024

bug check 1901 and 1807 #174

bug check 1901 and 1807 #174

Comments

icecream17 commented Jul 28, 2024