Search for blocks/addresses/...

Proofgold Asset

asset id
a23480fd0c5689c8ae1372a1b42b484455f590c6320ad33d99cc4966de4d4135
asset hash
ae79c6e5ee53cd73ea5b089247127cf386843687f277bcdd3b43bd0ca73b9399
bday / block
36399
tx
8596b..
preasset
doc published by PrCmT..
Known df_mend__df_sdrg__df_cytp__df_topsep__df_toplnd__df_rcl__df_he__ax_frege1__ax_frege2__ax_frege8__ax_frege28__ax_frege31__ax_frege41__ax_frege52a__ax_frege54a__ax_frege58a__ax_frege52c__ax_frege54c : ∀ x0 : ο . (wceq cmend (cmpt (λ x1 . cvv) (λ x1 . csb (co (cv x1) (cv x1) clmhm) (λ x2 . cun (ctp (cop (cfv cnx cbs) (cv x2)) (cop (cfv cnx cplusg) (cmpt2 (λ x3 x4 . cv x2) (λ x3 x4 . cv x2) (λ x3 x4 . co (cv x3) (cv x4) (cof (cfv (cv x1) cplusg))))) (cop (cfv cnx cmulr) (cmpt2 (λ x3 x4 . cv x2) (λ x3 x4 . cv x2) (λ x3 x4 . ccom (cv x3) (cv x4))))) (cpr (cop (cfv cnx csca) (cfv (cv x1) csca)) (cop (cfv cnx cvsca) (cmpt2 (λ x3 x4 . cfv (cfv (cv x1) csca) cbs) (λ x3 x4 . cv x2) (λ x3 x4 . co (cxp (cfv (cv x1) cbs) (csn (cv x3))) (cv x4) (cof (cfv (cv x1) cvsca)))))))))wceq csdrg (cmpt (λ x1 . cdr) (λ x1 . crab (λ x2 . wcel (co (cv x1) (cv x2) cress) cdr) (λ x2 . cfv (cv x1) csubrg)))wceq ccytp (cmpt (λ x1 . cn) (λ x1 . co (cfv (cfv ccnfld cpl1) cmgp) (cmpt (λ x2 . cima (ccnv (cfv (co (cfv ccnfld cmgp) (cdif cc (csn cc0)) cress) cod)) (csn (cv x1))) (λ x2 . co (cfv ccnfld cv1) (cfv (cv x2) (cfv (cfv ccnfld cpl1) cascl)) (cfv (cfv ccnfld cpl1) csg))) cgsu))wceq ctopsep (crab (λ x1 . wrex (λ x2 . wa (wbr (cv x2) com cdom) (wceq (cfv (cv x2) (cfv (cv x1) ccl)) (cuni (cv x1)))) (λ x2 . cpw (cuni (cv x1)))) (λ x1 . ctop))wceq ctoplnd (crab (λ x1 . wral (λ x2 . wceq (cuni (cv x1)) (cuni (cv x2))wrex (λ x3 . wa (wbr (cv x3) com cdom) (wceq (cuni (cv x1)) (cuni (cv x3)))) (λ x3 . cpw (cv x1))) (λ x2 . cpw (cv x1))) (λ x1 . ctop))wceq crcl (cmpt (λ x1 . cvv) (λ x1 . cint (cab (λ x2 . wa (wss (cv x1) (cv x2)) (wss (cres cid (cun (cdm (cv x2)) (crn (cv x2)))) (cv x2))))))(∀ x1 x2 : ι → ο . wb (whe x1 x2) (wss (cima x2 x1) x1))(∀ x1 x2 : ο . x1x2x1)(∀ x1 x2 x3 : ο . (x1x2x3)(x1x2)x1x3)(∀ x1 x2 x3 : ο . (x1x2x3)x2x1x3)(∀ x1 x2 : ο . (x1x2)wn x2wn x1)(∀ x1 : ο . wn (wn x1)x1)(∀ x1 : ο . x1wn (wn x1))(∀ x1 x2 x3 x4 : ο . wb x1 x2wif x1 x4 x3wif x2 x4 x3)(∀ x1 : ο . wb x1 x1)(∀ x1 x2 x3 : ο . wa x2 x3wif x1 x2 x3)(∀ x1 : ι → ο . ∀ x2 x3 : ι → ι → ο . ∀ x4 . wceq (x2 x4) (x3 x4)wsbc x1 (x2 x4)wsbc x1 (x3 x4))(∀ x1 : ι → ο . wceq x1 x1)x0)x0
Theorem df_mend : wceq cmend (cmpt (λ x0 . cvv) (λ x0 . csb (co (cv x0) (cv x0) clmhm) (λ x1 . cun (ctp (cop (cfv cnx cbs) (cv x1)) (cop (cfv cnx cplusg) (cmpt2 (λ x2 x3 . cv x1) (λ x2 x3 . cv x1) (λ x2 x3 . co (cv x2) (cv x3) (cof (cfv (cv x0) cplusg))))) (cop (cfv cnx cmulr) (cmpt2 (λ x2 x3 . cv x1) (λ x2 x3 . cv x1) (λ x2 x3 . ccom (cv x2) (cv x3))))) (cpr (cop (cfv cnx csca) (cfv (cv x0) csca)) (cop (cfv cnx cvsca) (cmpt2 (λ x2 x3 . cfv (cfv (cv x0) csca) cbs) (λ x2 x3 . cv x1) (λ x2 x3 . co (cxp (cfv (cv x0) cbs) (csn (cv x2))) (cv x3) (cof (cfv (cv x0) cvsca))))))))) (proof)
Theorem df_sdrg : wceq csdrg (cmpt (λ x0 . cdr) (λ x0 . crab (λ x1 . wcel (co (cv x0) (cv x1) cress) cdr) (λ x1 . cfv (cv x0) csubrg))) (proof)
Theorem df_cytp : wceq ccytp (cmpt (λ x0 . cn) (λ x0 . co (cfv (cfv ccnfld cpl1) cmgp) (cmpt (λ x1 . cima (ccnv (cfv (co (cfv ccnfld cmgp) (cdif cc (csn cc0)) cress) cod)) (csn (cv x0))) (λ x1 . co (cfv ccnfld cv1) (cfv (cv x1) (cfv (cfv ccnfld cpl1) cascl)) (cfv (cfv ccnfld cpl1) csg))) cgsu)) (proof)
Theorem df_topsep : wceq ctopsep (crab (λ x0 . wrex (λ x1 . wa (wbr (cv x1) com cdom) (wceq (cfv (cv x1) (cfv (cv x0) ccl)) (cuni (cv x0)))) (λ x1 . cpw (cuni (cv x0)))) (λ x0 . ctop)) (proof)
Theorem df_toplnd : wceq ctoplnd (crab (λ x0 . wral (λ x1 . wceq (cuni (cv x0)) (cuni (cv x1))wrex (λ x2 . wa (wbr (cv x2) com cdom) (wceq (cuni (cv x0)) (cuni (cv x2)))) (λ x2 . cpw (cv x0))) (λ x1 . cpw (cv x0))) (λ x0 . ctop)) (proof)
Theorem df_rcl : wceq crcl (cmpt (λ x0 . cvv) (λ x0 . cint (cab (λ x1 . wa (wss (cv x0) (cv x1)) (wss (cres cid (cun (cdm (cv x1)) (crn (cv x1)))) (cv x1)))))) (proof)
Theorem df_he : ∀ x0 x1 : ι → ο . wb (whe x0 x1) (wss (cima x1 x0) x0) (proof)
Theorem ax_frege1 : ∀ x0 x1 : ο . x0x1x0 (proof)
Theorem ax_frege2 : ∀ x0 x1 x2 : ο . (x0x1x2)(x0x1)x0x2 (proof)
Theorem ax_frege8ax_frege8 : ∀ x0 x1 x2 : ο . (x0x1x2)x1x0x2 (proof)
Theorem ax_frege28 : ∀ x0 x1 : ο . (x0x1)wn x1wn x0 (proof)
Theorem ax_frege31 : ∀ x0 : ο . wn (wn x0)x0 (proof)
Theorem ax_frege41 : ∀ x0 : ο . x0wn (wn x0) (proof)
Theorem ax_frege52a : ∀ x0 x1 x2 x3 : ο . wb x0 x1wif x0 x3 x2wif x1 x3 x2 (proof)
Theorem ax_frege54a : ∀ x0 : ο . wb x0 x0 (proof)
Theorem ax_frege58a : ∀ x0 x1 x2 : ο . wa x1 x2wif x0 x1 x2 (proof)
Theorem ax_frege52cax_frege52c : ∀ x0 : ι → ο . ∀ x1 x2 : ι → ι → ο . ∀ x3 . wceq (x1 x3) (x2 x3)wsbc x0 (x1 x3)wsbc x0 (x2 x3) (proof)
Theorem ax_frege54c : ∀ x0 : ι → ο . wceq x0 x0 (proof)