Search for blocks/addresses/...

Proofgold Asset

asset id
338f2c4cb1b26e6662671f028c3d6242b988ce9ac033e12bfae971dcc3330867
asset hash
45df0a9a3d1d73b86593616df5363f1c28bdb22e8273955047e0b0d0c4835bc1
bday / block
36396
tx
9e953..
preasset
doc published by PrCmT..
Known df_supp__df_tpos__df_cur__df_unc__df_undef__df_wrecs__df_smo__df_recs__df_rdg__df_seqom__df_1o__df_2o__df_3o__df_4o__df_oadd__df_omul__df_oexp__df_er : ∀ x0 : ο . (wceq csupp (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . crab (λ x3 . wne (cima (cv x1) (csn (cv x3))) (csn (cv x2))) (λ x3 . cdm (cv x1))))(∀ x1 : ι → ο . wceq (ctpos x1) (ccom x1 (cmpt (λ x2 . cun (ccnv (cdm x1)) (csn c0)) (λ x2 . cuni (ccnv (csn (cv x2)))))))(∀ x1 : ι → ο . wceq (ccur x1) (cmpt (λ x2 . cdm (cdm x1)) (λ x2 . copab (λ x3 x4 . wbr (cop (cv x2) (cv x3)) (cv x4) x1))))(∀ x1 : ι → ο . wceq (cunc x1) (coprab (λ x2 x3 x4 . wbr (cv x3) (cv x4) (cfv (cv x2) x1))))wceq cund (cmpt (λ x1 . cvv) (λ x1 . cpw (cuni (cv x1))))(∀ x1 x2 x3 : ι → ο . wceq (cwrecs x1 x2 x3) (cuni (cab (λ x4 . wex (λ x5 . w3a (wfn (cv x4) (cv x5)) (wa (wss (cv x5) x1) (wral (λ x6 . wss (cpred x1 x2 (cv x6)) (cv x5)) (λ x6 . cv x5))) (wral (λ x6 . wceq (cfv (cv x6) (cv x4)) (cfv (cres (cv x4) (cpred x1 x2 (cv x6))) x3)) (λ x6 . cv x5)))))))(∀ x1 : ι → ο . wb (wsmo x1) (w3a (wf (cdm x1) con0 x1) (word (cdm x1)) (wral (λ x2 . wral (λ x3 . wcel (cv x2) (cv x3)wcel (cfv (cv x2) x1) (cfv (cv x3) x1)) (λ x3 . cdm x1)) (λ x2 . cdm x1))))(∀ x1 : ι → ο . wceq (crecs x1) (cwrecs con0 cep x1))(∀ x1 x2 : ι → ο . wceq (crdg x1 x2) (crecs (cmpt (λ x3 . cvv) (λ x3 . cif (wceq (cv x3) c0) x2 (cif (wlim (cdm (cv x3))) (cuni (crn (cv x3))) (cfv (cfv (cuni (cdm (cv x3))) (cv x3)) x1))))))(∀ x1 x2 : ι → ο . wceq (cseqom x1 x2) (cima (crdg (cmpt2 (λ x3 x4 . com) (λ x3 x4 . cvv) (λ x3 x4 . cop (csuc (cv x3)) (co (cv x3) (cv x4) x1))) (cop c0 (cfv x2 cid))) com))wceq c1o (csuc c0)wceq c2o (csuc c1o)wceq c3o (csuc c2o)wceq c4o (csuc c3o)wceq coa (cmpt2 (λ x1 x2 . con0) (λ x1 x2 . con0) (λ x1 x2 . cfv (cv x2) (crdg (cmpt (λ x3 . cvv) (λ x3 . csuc (cv x3))) (cv x1))))wceq comu (cmpt2 (λ x1 x2 . con0) (λ x1 x2 . con0) (λ x1 x2 . cfv (cv x2) (crdg (cmpt (λ x3 . cvv) (λ x3 . co (cv x3) (cv x1) coa)) c0)))wceq coe (cmpt2 (λ x1 x2 . con0) (λ x1 x2 . con0) (λ x1 x2 . cif (wceq (cv x1) c0) (cdif c1o (cv x2)) (cfv (cv x2) (crdg (cmpt (λ x3 . cvv) (λ x3 . co (cv x3) (cv x1) comu)) c1o))))(∀ x1 x2 : ι → ο . wb (wer x1 x2) (w3a (wrel x2) (wceq (cdm x2) x1) (wss (cun (ccnv x2) (ccom x2 x2)) x2)))x0)x0
Theorem df_supp : wceq csupp (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . crab (λ x2 . wne (cima (cv x0) (csn (cv x2))) (csn (cv x1))) (λ x2 . cdm (cv x0)))) (proof)
Theorem df_tpos : ∀ x0 : ι → ο . wceq (ctpos x0) (ccom x0 (cmpt (λ x1 . cun (ccnv (cdm x0)) (csn c0)) (λ x1 . cuni (ccnv (csn (cv x1)))))) (proof)
Theorem df_cur : ∀ x0 : ι → ο . wceq (ccur x0) (cmpt (λ x1 . cdm (cdm x0)) (λ x1 . copab (λ x2 x3 . wbr (cop (cv x1) (cv x2)) (cv x3) x0))) (proof)
Theorem df_unc : ∀ x0 : ι → ο . wceq (cunc x0) (coprab (λ x1 x2 x3 . wbr (cv x2) (cv x3) (cfv (cv x1) x0))) (proof)
Theorem df_undef : wceq cund (cmpt (λ x0 . cvv) (λ x0 . cpw (cuni (cv x0)))) (proof)
Theorem df_wrecs : ∀ x0 x1 x2 : ι → ο . wceq (cwrecs x0 x1 x2) (cuni (cab (λ x3 . wex (λ x4 . w3a (wfn (cv x3) (cv x4)) (wa (wss (cv x4) x0) (wral (λ x5 . wss (cpred x0 x1 (cv x5)) (cv x4)) (λ x5 . cv x4))) (wral (λ x5 . wceq (cfv (cv x5) (cv x3)) (cfv (cres (cv x3) (cpred x0 x1 (cv x5))) x2)) (λ x5 . cv x4)))))) (proof)
Theorem df_smo : ∀ x0 : ι → ο . wb (wsmo x0) (w3a (wf (cdm x0) con0 x0) (word (cdm x0)) (wral (λ x1 . wral (λ x2 . wcel (cv x1) (cv x2)wcel (cfv (cv x1) x0) (cfv (cv x2) x0)) (λ x2 . cdm x0)) (λ x1 . cdm x0))) (proof)
Theorem df_recs : ∀ x0 : ι → ο . wceq (crecs x0) (cwrecs con0 cep x0) (proof)
Theorem df_rdg : ∀ x0 x1 : ι → ο . wceq (crdg x0 x1) (crecs (cmpt (λ x2 . cvv) (λ x2 . cif (wceq (cv x2) c0) x1 (cif (wlim (cdm (cv x2))) (cuni (crn (cv x2))) (cfv (cfv (cuni (cdm (cv x2))) (cv x2)) x0))))) (proof)
Theorem df_seqom : ∀ x0 x1 : ι → ο . wceq (cseqom x0 x1) (cima (crdg (cmpt2 (λ x2 x3 . com) (λ x2 x3 . cvv) (λ x2 x3 . cop (csuc (cv x2)) (co (cv x2) (cv x3) x0))) (cop c0 (cfv x1 cid))) com) (proof)
Theorem df_1o : wceq c1o (csuc c0) (proof)
Theorem df_2o : wceq c2o (csuc c1o) (proof)
Theorem df_3o : wceq c3o (csuc c2o) (proof)
Theorem df_4o : wceq c4o (csuc c3o) (proof)
Theorem df_oadd : wceq coa (cmpt2 (λ x0 x1 . con0) (λ x0 x1 . con0) (λ x0 x1 . cfv (cv x1) (crdg (cmpt (λ x2 . cvv) (λ x2 . csuc (cv x2))) (cv x0)))) (proof)
Theorem df_omul : wceq comu (cmpt2 (λ x0 x1 . con0) (λ x0 x1 . con0) (λ x0 x1 . cfv (cv x1) (crdg (cmpt (λ x2 . cvv) (λ x2 . co (cv x2) (cv x0) coa)) c0))) (proof)
Theorem df_oexp : wceq coe (cmpt2 (λ x0 x1 . con0) (λ x0 x1 . con0) (λ x0 x1 . cif (wceq (cv x0) c0) (cdif c1o (cv x1)) (cfv (cv x1) (crdg (cmpt (λ x2 . cvv) (λ x2 . co (cv x2) (cv x0) comu)) c1o)))) (proof)
Theorem df_er : ∀ x0 x1 : ι → ο . wb (wer x0 x1) (w3a (wrel x1) (wceq (cdm x1) x0) (wss (cun (ccnv x1) (ccom x1 x1)) x1)) (proof)