Search for blocks/addresses/...

Proofgold Proposition

∀ x0 : ο . (wceq cinv (cmpt (λ x1 . ccat) (λ x1 . cmpt2 (λ x2 x3 . cfv (cv x1) cbs) (λ x2 x3 . cfv (cv x1) cbs) (λ x2 x3 . cin (co (cv x2) (cv x3) (cfv (cv x1) csect)) (ccnv (co (cv x3) (cv x2) (cfv (cv x1) csect))))))wceq ciso (cmpt (λ x1 . ccat) (λ x1 . ccom (cmpt (λ x2 . cvv) (λ x2 . cdm (cv x2))) (cfv (cv x1) cinv)))wceq ccic (cmpt (λ x1 . ccat) (λ x1 . co (cfv (cv x1) ciso) c0 csupp))wceq cssc (copab (λ x1 x2 . wex (λ x3 . wa (wfn (cv x2) (cxp (cv x3) (cv x3))) (wrex (λ x4 . wcel (cv x1) (cixp (λ x5 . cxp (cv x4) (cv x4)) (λ x5 . cpw (cfv (cv x5) (cv x2))))) (λ x4 . cpw (cv x3))))))wceq cresc (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . co (co (cv x1) (cdm (cdm (cv x2))) cress) (cop (cfv cnx chom) (cv x2)) csts))wceq csubc (cmpt (λ x1 . ccat) (λ x1 . cab (λ x2 . wa (wbr (cv x2) (cfv (cv x1) chomf) cssc) (wsbc (λ x3 . wral (λ x4 . wa (wcel (cfv (cv x4) (cfv (cv x1) ccid)) (co (cv x4) (cv x4) (cv x2))) (wral (λ x5 . wral (λ x6 . wral (λ x7 . wral (λ x8 . wcel (co (cv x8) (cv x7) (co (cop (cv x4) (cv x5)) (cv x6) (cfv (cv x1) cco))) (co (cv x4) (cv x6) (cv x2))) (λ x8 . co (cv x5) (cv x6) (cv x2))) (λ x7 . co (cv x4) (cv x5) (cv x2))) (λ x6 . cv x3)) (λ x5 . cv x3))) (λ x4 . cv x3)) (cdm (cdm (cv x2)))))))wceq cfunc (cmpt2 (λ x1 x2 . ccat) (λ x1 x2 . ccat) (λ x1 x2 . copab (λ x3 x4 . wsbc (λ x5 . w3a (wf (cv x5) (cfv (cv x2) cbs) (cv x3)) (wcel (cv x4) (cixp (λ x6 . cxp (cv x5) (cv x5)) (λ x6 . co (co (cfv (cfv (cv x6) c1st) (cv x3)) (cfv (cfv (cv x6) c2nd) (cv x3)) (cfv (cv x2) chom)) (cfv (cv x6) (cfv (cv x1) chom)) cmap))) (wral (λ x6 . wa (wceq (cfv (cfv (cv x6) (cfv (cv x1) ccid)) (co (cv x6) (cv x6) (cv x4))) (cfv (cfv (cv x6) (cv x3)) (cfv (cv x2) ccid))) (wral (λ x7 . wral (λ x8 . wral (λ x9 . wral (λ x10 . wceq (cfv (co (cv x10) (cv x9) (co (cop (cv x6) (cv x7)) (cv x8) (cfv (cv x1) cco))) (co (cv x6) (cv x8) (cv x4))) (co (cfv (cv x10) (co (cv x7) (cv x8) (cv x4))) (cfv (cv x9) (co (cv x6) (cv x7) (cv x4))) (co (cop (cfv (cv x6) (cv x3)) (cfv (cv x7) (cv x3))) (cfv (cv x8) (cv x3)) (cfv (cv x2) cco)))) (λ x10 . co (cv x7) (cv x8) (cfv (cv x1) chom))) (λ x9 . co (cv x6) (cv x7) (cfv (cv x1) chom))) (λ x8 . cv x5)) (λ x7 . cv x5))) (λ x6 . cv x5))) (cfv (cv x1) cbs))))wceq cidfu (cmpt (λ x1 . ccat) (λ x1 . csb (cfv (cv x1) cbs) (λ x2 . cop (cres cid (cv x2)) (cmpt (λ x3 . cxp (cv x2) (cv x2)) (λ x3 . cres cid (cfv (cv x3) (cfv (cv x1) chom)))))))wceq ccofu (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . cop (ccom (cfv (cv x1) c1st) (cfv (cv x2) c1st)) (cmpt2 (λ x3 x4 . cdm (cdm (cfv (cv x2) c2nd))) (λ x3 x4 . cdm (cdm (cfv (cv x2) c2nd))) (λ x3 x4 . ccom (co (cfv (cv x3) (cfv (cv x2) c1st)) (cfv (cv x4) (cfv (cv x2) c1st)) (cfv (cv x1) c2nd)) (co (cv x3) (cv x4) (cfv (cv x2) c2nd))))))wceq cresf (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . cop (cres (cfv (cv x1) c1st) (cdm (cdm (cv x2)))) (cmpt (λ x3 . cdm (cv x2)) (λ x3 . cres (cfv (cv x3) (cfv (cv x1) c2nd)) (cfv (cv x3) (cv x2))))))wceq cful (cmpt2 (λ x1 x2 . ccat) (λ x1 x2 . ccat) (λ x1 x2 . copab (λ x3 x4 . wa (wbr (cv x3) (cv x4) (co (cv x1) (cv x2) cfunc)) (wral (λ x5 . wral (λ x6 . wceq (crn (co (cv x5) (cv x6) (cv x4))) (co (cfv (cv x5) (cv x3)) (cfv (cv x6) (cv x3)) (cfv (cv x2) chom))) (λ x6 . cfv (cv x1) cbs)) (λ x5 . cfv (cv x1) cbs)))))wceq cfth (cmpt2 (λ x1 x2 . ccat) (λ x1 x2 . ccat) (λ x1 x2 . copab (λ x3 x4 . wa (wbr (cv x3) (cv x4) (co (cv x1) (cv x2) cfunc)) (wral (λ x5 . wral (λ x6 . wfun (ccnv (co (cv x5) (cv x6) (cv x4)))) (λ x6 . cfv (cv x1) cbs)) (λ x5 . cfv (cv x1) cbs)))))wceq cnat (cmpt2 (λ x1 x2 . ccat) (λ x1 x2 . ccat) (λ x1 x2 . cmpt2 (λ x3 x4 . co (cv x1) (cv x2) cfunc) (λ x3 x4 . co (cv x1) (cv x2) cfunc) (λ x3 x4 . csb (cfv (cv x3) c1st) (λ x5 . csb (cfv (cv x4) c1st) (λ x6 . crab (λ x7 . wral (λ x8 . wral (λ x9 . wral (λ x10 . wceq (co (cfv (cv x9) (cv x7)) (cfv (cv x10) (co (cv x8) (cv x9) (cfv (cv x3) c2nd))) (co (cop (cfv (cv x8) (cv x5)) (cfv (cv x9) (cv x5))) (cfv (cv x9) (cv x6)) (cfv (cv x2) cco))) (co (cfv (cv x10) (co (cv x8) (cv x9) (cfv (cv x4) c2nd))) (cfv (cv x8) (cv x7)) (co (cop (cfv (cv x8) (cv x5)) (cfv (cv x8) (cv x6))) (cfv (cv x9) (cv x6)) (cfv (cv x2) cco)))) (λ x10 . co (cv x8) (cv x9) (cfv (cv x1) chom))) (λ x9 . cfv (cv x1) cbs)) (λ x8 . cfv (cv x1) cbs)) (λ x7 . cixp (λ x8 . cfv (cv x1) cbs) (λ x8 . co (cfv (cv x8) (cv x5)) (cfv (cv x8) (cv x6)) (cfv (cv x2) chom))))))))wceq cfuc (cmpt2 (λ x1 x2 . ccat) (λ x1 x2 . ccat) (λ x1 x2 . ctp (cop (cfv cnx cbs) (co (cv x1) (cv x2) cfunc)) (cop (cfv cnx chom) (co (cv x1) (cv x2) cnat)) (cop (cfv cnx cco) (cmpt2 (λ x3 x4 . cxp (co (cv x1) (cv x2) cfunc) (co (cv x1) (cv x2) cfunc)) (λ x3 x4 . co (cv x1) (cv x2) cfunc) (λ x3 x4 . csb (cfv (cv x3) c1st) (λ x5 . csb (cfv (cv x3) c2nd) (λ x6 . cmpt2 (λ x7 x8 . co (cv x6) (cv x4) (co (cv x1) (cv x2) cnat)) (λ x7 x8 . co (cv x5) (cv x6) (co (cv x1) (cv x2) cnat)) (λ x7 x8 . cmpt (λ x9 . cfv (cv x1) cbs) (λ x9 . co (cfv (cv x9) (cv x7)) (cfv (cv x9) (cv x8)) (co (cop (cfv (cv x9) (cfv (cv x5) c1st)) (cfv (cv x9) (cfv (cv x6) c1st))) (cfv (cv x9) (cfv (cv x4) c1st)) (cfv (cv x2) cco)))))))))))wceq cinito (cmpt (λ x1 . ccat) (λ x1 . crab (λ x2 . wral (λ x3 . weu (λ x4 . wcel (cv x4) (co (cv x2) (cv x3) (cfv (cv x1) chom)))) (λ x3 . cfv (cv x1) cbs)) (λ x2 . cfv (cv x1) cbs)))wceq ctermo (cmpt (λ x1 . ccat) (λ x1 . crab (λ x2 . wral (λ x3 . weu (λ x4 . wcel (cv x4) (co (cv x3) (cv x2) (cfv (cv x1) chom)))) (λ x3 . cfv (cv x1) cbs)) (λ x2 . cfv (cv x1) cbs)))wceq czeroo (cmpt (λ x1 . ccat) (λ x1 . cin (cfv (cv x1) cinito) (cfv (cv x1) ctermo)))wceq cdoma (ccom c1st c1st)x0)x0
type
prop
theory
SetMM
name
df_inv__df_iso__df_cic__df_ssc__df_resc__df_subc__df_func__df_idfu__df_cofu__df_resf__df_full__df_fth__df_nat__df_fuc__df_inito__df_termo__df_zeroo__df_doma
proof
PUV1k..
Megalodon
-
proofgold address
TMHWd..
creator
36224 PrCmT../f5f08..
owner
36224 PrCmT../f5f08..
term root
b483a..