Proofgold Asset

Known df_gim__df_gic__df_ga__df_cntz__df_cntr__df_oppg__df_symg__df_pmtr__df_psgn__df_evpm__df_od__df_gex__df_pgp__df_slw__df_lsm__df_pj1__df_efg__df_frgp : ∀ x0 : ο . (wceq cgim (cmpt2 (λ x1 x2 . cgrp) (λ x1 x2 . cgrp) (λ x1 x2 . crab (λ x3 . wf1o (cfv (cv x1) cbs) (cfv (cv x2) cbs) (cv x3)) (λ x3 . co (cv x1) (cv x2) cghm))) ⟶ wceq cgic (cima (ccnv cgim) (cdif cvv c1o)) ⟶ wceq cga (cmpt2 (λ x1 x2 . cgrp) (λ x1 x2 . cvv) (λ x1 x2 . csb (cfv (cv x1) cbs) (λ x3 . crab (λ x4 . wral (λ x5 . wa (wceq (co (cfv (cv x1) c0g) (cv x5) (cv x4)) (cv x5)) (wral (λ x6 . wral (λ x7 . wceq (co (co (cv x6) (cv x7) (cfv (cv x1) cplusg)) (cv x5) (cv x4)) (co (cv x6) (co (cv x7) (cv x5) (cv x4)) (cv x4))) (λ x7 . cv x3)) (λ x6 . cv x3))) (λ x5 . cv x2)) (λ x4 . co (cv x2) (cxp (cv x3) (cv x2)) cmap)))) ⟶ wceq ccntz (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cpw (cfv (cv x1) cbs)) (λ x2 . crab (λ x3 . wral (λ x4 . wceq (co (cv x3) (cv x4) (cfv (cv x1) cplusg)) (co (cv x4) (cv x3) (cfv (cv x1) cplusg))) (λ x4 . cv x2)) (λ x3 . cfv (cv x1) cbs)))) ⟶ wceq ccntr (cmpt (λ x1 . cvv) (λ x1 . cfv (cfv (cv x1) cbs) (cfv (cv x1) ccntz))) ⟶ wceq coppg (cmpt (λ x1 . cvv) (λ x1 . co (cv x1) (cop (cfv cnx cplusg) (ctpos (cfv (cv x1) cplusg))) csts)) ⟶ wceq csymg (cmpt (λ x1 . cvv) (λ x1 . csb (cab (λ x2 . wf1o (cv x1) (cv x1) (cv x2))) (λ x2 . ctp (cop (cfv cnx cbs) (cv x2)) (cop (cfv cnx cplusg) (cmpt2 (λ x3 x4 . cv x2) (λ x3 x4 . cv x2) (λ x3 x4 . ccom (cv x3) (cv x4)))) (cop (cfv cnx cts) (cfv (cxp (cv x1) (csn (cpw (cv x1)))) cpt))))) ⟶ wceq cpmtr (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . crab (λ x3 . wbr (cv x3) c2o cen) (λ x3 . cpw (cv x1))) (λ x2 . cmpt (λ x3 . cv x1) (λ x3 . cif (wcel (cv x3) (cv x2)) (cuni (cdif (cv x2) (csn (cv x3)))) (cv x3))))) ⟶ wceq cpsgn (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . crab (λ x3 . wcel (cdm (cdif (cv x3) cid)) cfn) (λ x3 . cfv (cfv (cv x1) csymg) cbs)) (λ x2 . cio (λ x3 . wrex (λ x4 . wa (wceq (cv x2) (co (cfv (cv x1) csymg) (cv x4) cgsu)) (wceq (cv x3) (co (cneg c1) (cfv (cv x4) chash) cexp))) (λ x4 . cword (crn (cfv (cv x1) cpmtr))))))) ⟶ wceq cevpm (cmpt (λ x1 . cvv) (λ x1 . cima (ccnv (cfv (cv x1) cpsgn)) (csn c1))) ⟶ wceq cod (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cfv (cv x1) cbs) (λ x2 . csb (crab (λ x3 . wceq (co (cv x3) (cv x2) (cfv (cv x1) cmg)) (cfv (cv x1) c0g)) (λ x3 . cn)) (λ x3 . cif (wceq (cv x3) c0) cc0 (cinf (cv x3) cr clt))))) ⟶ wceq cgex (cmpt (λ x1 . cvv) (λ x1 . csb (crab (λ x2 . wral (λ x3 . wceq (co (cv x2) (cv x3) (cfv (cv x1) cmg)) (cfv (cv x1) c0g)) (λ x3 . cfv (cv x1) cbs)) (λ x2 . cn)) (λ x2 . cif (wceq (cv x2) c0) cc0 (cinf (cv x2) cr clt)))) ⟶ wceq cpgp (copab (λ x1 x2 . wa (wa (wcel (cv x1) cprime) (wcel (cv x2) cgrp)) (wral (λ x3 . wrex (λ x4 . wceq (cfv (cv x3) (cfv (cv x2) cod)) (co (cv x1) (cv x4) cexp)) (λ x4 . cn0)) (λ x3 . cfv (cv x2) cbs)))) ⟶ wceq cslw (cmpt2 (λ x1 x2 . cprime) (λ x1 x2 . cgrp) (λ x1 x2 . crab (λ x3 . wral (λ x4 . wb (wa (wss (cv x3) (cv x4)) (wbr (cv x1) (co (cv x2) (cv x4) cress) cpgp)) (wceq (cv x3) (cv x4))) (λ x4 . cfv (cv x2) csubg)) (λ x3 . cfv (cv x2) csubg))) ⟶ wceq clsm (cmpt (λ x1 . cvv) (λ x1 . cmpt2 (λ x2 x3 . cpw (cfv (cv x1) cbs)) (λ x2 x3 . cpw (cfv (cv x1) cbs)) (λ x2 x3 . crn (cmpt2 (λ x4 x5 . cv x2) (λ x4 x5 . cv x3) (λ x4 x5 . co (cv x4) (cv x5) (cfv (cv x1) cplusg)))))) ⟶ wceq cpj1 (cmpt (λ x1 . cvv) (λ x1 . cmpt2 (λ x2 x3 . cpw (cfv (cv x1) cbs)) (λ x2 x3 . cpw (cfv (cv x1) cbs)) (λ x2 x3 . cmpt (λ x4 . co (cv x2) (cv x3) (cfv (cv x1) clsm)) (λ x4 . crio (λ x5 . wrex (λ x6 . wceq (cv x4) (co (cv x5) (cv x6) (cfv (cv x1) cplusg))) (λ x6 . cv x3)) (λ x5 . cv x2))))) ⟶ wceq cefg (cmpt (λ x1 . cvv) (λ x1 . cint (cab (λ x2 . wa (wer (cword (cxp (cv x1) c2o)) (cv x2)) (wral (λ x3 . wral (λ x4 . wral (λ x5 . wral (λ x6 . wbr (cv x3) (co (cv x3) (cotp (cv x4) (cv x4) (cs2 (cop (cv x5) (cv x6)) (cop (cv x5) (cdif c1o (cv x6))))) csplice) (cv x2)) (λ x6 . c2o)) (λ x5 . cv x1)) (λ x4 . co cc0 (cfv (cv x3) chash) cfz)) (λ x3 . cword (cxp (cv x1) c2o))))))) ⟶ wceq cfrgp (cmpt (λ x1 . cvv) (λ x1 . co (cfv (cxp (cv x1) c2o) cfrmd) (cfv (cv x1) cefg) cqus)) ⟶ x0) ⟶ x0
Theorem df_gim : wceq cgim (cmpt2 (λ x0 x1 . cgrp) (λ x0 x1 . cgrp) (λ x0 x1 . crab (λ x2 . wf1o (cfv (cv x0) cbs) (cfv (cv x1) cbs) (cv x2)) (λ x2 . co (cv x0) (cv x1) cghm))) (proof)
Theorem df_gic : wceq cgic (cima (ccnv cgim) (cdif cvv c1o)) (proof)
Theorem df_ga : wceq cga (cmpt2 (λ x0 x1 . cgrp) (λ x0 x1 . cvv) (λ x0 x1 . csb (cfv (cv x0) cbs) (λ x2 . crab (λ x3 . wral (λ x4 . wa (wceq (co (cfv (cv x0) c0g) (cv x4) (cv x3)) (cv x4)) (wral (λ x5 . wral (λ x6 . wceq (co (co (cv x5) (cv x6) (cfv (cv x0) cplusg)) (cv x4) (cv x3)) (co (cv x5) (co (cv x6) (cv x4) (cv x3)) (cv x3))) (λ x6 . cv x2)) (λ x5 . cv x2))) (λ x4 . cv x1)) (λ x3 . co (cv x1) (cxp (cv x2) (cv x1)) cmap)))) (proof)
Theorem df_cntz : wceq ccntz (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cpw (cfv (cv x0) cbs)) (λ x1 . crab (λ x2 . wral (λ x3 . wceq (co (cv x2) (cv x3) (cfv (cv x0) cplusg)) (co (cv x3) (cv x2) (cfv (cv x0) cplusg))) (λ x3 . cv x1)) (λ x2 . cfv (cv x0) cbs)))) (proof)
Theorem df_cntr : wceq ccntr (cmpt (λ x0 . cvv) (λ x0 . cfv (cfv (cv x0) cbs) (cfv (cv x0) ccntz))) (proof)
Theorem df_oppg : wceq coppg (cmpt (λ x0 . cvv) (λ x0 . co (cv x0) (cop (cfv cnx cplusg) (ctpos (cfv (cv x0) cplusg))) csts)) (proof)
Theorem df_symg : wceq csymg (cmpt (λ x0 . cvv) (λ x0 . csb (cab (λ x1 . wf1o (cv x0) (cv x0) (cv x1))) (λ x1 . ctp (cop (cfv cnx cbs) (cv x1)) (cop (cfv cnx cplusg) (cmpt2 (λ x2 x3 . cv x1) (λ x2 x3 . cv x1) (λ x2 x3 . ccom (cv x2) (cv x3)))) (cop (cfv cnx cts) (cfv (cxp (cv x0) (csn (cpw (cv x0)))) cpt))))) (proof)
Theorem df_pmtr : wceq cpmtr (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . crab (λ x2 . wbr (cv x2) c2o cen) (λ x2 . cpw (cv x0))) (λ x1 . cmpt (λ x2 . cv x0) (λ x2 . cif (wcel (cv x2) (cv x1)) (cuni (cdif (cv x1) (csn (cv x2)))) (cv x2))))) (proof)
Theorem df_psgn : wceq cpsgn (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . crab (λ x2 . wcel (cdm (cdif (cv x2) cid)) cfn) (λ x2 . cfv (cfv (cv x0) csymg) cbs)) (λ x1 . cio (λ x2 . wrex (λ x3 . wa (wceq (cv x1) (co (cfv (cv x0) csymg) (cv x3) cgsu)) (wceq (cv x2) (co (cneg c1) (cfv (cv x3) chash) cexp))) (λ x3 . cword (crn (cfv (cv x0) cpmtr))))))) (proof)
Theorem df_evpm : wceq cevpm (cmpt (λ x0 . cvv) (λ x0 . cima (ccnv (cfv (cv x0) cpsgn)) (csn c1))) (proof)
Theorem df_od : wceq cod (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cfv (cv x0) cbs) (λ x1 . csb (crab (λ x2 . wceq (co (cv x2) (cv x1) (cfv (cv x0) cmg)) (cfv (cv x0) c0g)) (λ x2 . cn)) (λ x2 . cif (wceq (cv x2) c0) cc0 (cinf (cv x2) cr clt))))) (proof)
Theorem df_gex : wceq cgex (cmpt (λ x0 . cvv) (λ x0 . csb (crab (λ x1 . wral (λ x2 . wceq (co (cv x1) (cv x2) (cfv (cv x0) cmg)) (cfv (cv x0) c0g)) (λ x2 . cfv (cv x0) cbs)) (λ x1 . cn)) (λ x1 . cif (wceq (cv x1) c0) cc0 (cinf (cv x1) cr clt)))) (proof)
Theorem df_pgp : wceq cpgp (copab (λ x0 x1 . wa (wa (wcel (cv x0) cprime) (wcel (cv x1) cgrp)) (wral (λ x2 . wrex (λ x3 . wceq (cfv (cv x2) (cfv (cv x1) cod)) (co (cv x0) (cv x3) cexp)) (λ x3 . cn0)) (λ x2 . cfv (cv x1) cbs)))) (proof)
Theorem df_slw : wceq cslw (cmpt2 (λ x0 x1 . cprime) (λ x0 x1 . cgrp) (λ x0 x1 . crab (λ x2 . wral (λ x3 . wb (wa (wss (cv x2) (cv x3)) (wbr (cv x0) (co (cv x1) (cv x3) cress) cpgp)) (wceq (cv x2) (cv x3))) (λ x3 . cfv (cv x1) csubg)) (λ x2 . cfv (cv x1) csubg))) (proof)
Theorem df_lsm : wceq clsm (cmpt (λ x0 . cvv) (λ x0 . cmpt2 (λ x1 x2 . cpw (cfv (cv x0) cbs)) (λ x1 x2 . cpw (cfv (cv x0) cbs)) (λ x1 x2 . crn (cmpt2 (λ x3 x4 . cv x1) (λ x3 x4 . cv x2) (λ x3 x4 . co (cv x3) (cv x4) (cfv (cv x0) cplusg)))))) (proof)
Theorem df_pj1 : wceq cpj1 (cmpt (λ x0 . cvv) (λ x0 . cmpt2 (λ x1 x2 . cpw (cfv (cv x0) cbs)) (λ x1 x2 . cpw (cfv (cv x0) cbs)) (λ x1 x2 . cmpt (λ x3 . co (cv x1) (cv x2) (cfv (cv x0) clsm)) (λ x3 . crio (λ x4 . wrex (λ x5 . wceq (cv x3) (co (cv x4) (cv x5) (cfv (cv x0) cplusg))) (λ x5 . cv x2)) (λ x4 . cv x1))))) (proof)
Theorem df_efg : wceq cefg (cmpt (λ x0 . cvv) (λ x0 . cint (cab (λ x1 . wa (wer (cword (cxp (cv x0) c2o)) (cv x1)) (wral (λ x2 . wral (λ x3 . wral (λ x4 . wral (λ x5 . wbr (cv x2) (co (cv x2) (cotp (cv x3) (cv x3) (cs2 (cop (cv x4) (cv x5)) (cop (cv x4) (cdif c1o (cv x5))))) csplice) (cv x1)) (λ x5 . c2o)) (λ x4 . cv x0)) (λ x3 . co cc0 (cfv (cv x2) chash) cfz)) (λ x2 . cword (cxp (cv x0) c2o))))))) (proof)
Theorem df_frgp : wceq cfrgp (cmpt (λ x0 . cvv) (λ x0 . co (cfv (cxp (cv x0) c2o) cfrmd) (cfv (cv x0) cefg) cqus)) (proof)