Search for blocks/addresses/...

Proofgold Signed Transaction

vin
Pr4wN../4ea21..
PUNFh../0dde6..
vout
Pr4wN../88c9d.. 0.10 bars
TMRao../ea9f3.. ownership of 78de9.. as prop with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMUze../e815f.. ownership of b1a4d.. as prop with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMbmw../04ce9.. ownership of ccd37.. as prop with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMJGK../0cf25.. ownership of f5d7f.. as prop with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMPV6../72e08.. ownership of c352a.. as prop with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMcgd../8bdb0.. ownership of e4db9.. as prop with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMbBp../17c28.. ownership of be63d.. as prop with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMTdk../f7558.. ownership of 2a60e.. as prop with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMFvq../725fc.. ownership of 86f75.. as prop with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMEqN../230c2.. ownership of ad643.. as prop with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMRxC../b4415.. ownership of be6df.. as prop with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMPPb../220d3.. ownership of 247ed.. as prop with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMXas../858c7.. ownership of 99912.. as prop with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMYy7../3d22c.. ownership of a7a93.. as prop with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMb5U../e63cf.. ownership of 2b841.. as prop with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMFw7../9db61.. ownership of 17d58.. as prop with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMW5d../e407f.. ownership of 881a5.. as prop with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMTzk../ffd52.. ownership of 70729.. as prop with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMRt6../1e875.. ownership of a1afb.. as prop with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMS8P../ed5ea.. ownership of 9056f.. as prop with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMGt3../1dec0.. ownership of 5be8b.. as prop with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMWKn../e8ea5.. ownership of b873f.. as prop with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMcQ8../4a3b2.. ownership of 0e7f0.. as prop with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMQf7../760ca.. ownership of 075b8.. as prop with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMUC7../a6ae8.. ownership of 18ac8.. as prop with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMafu../050d1.. ownership of 402f2.. as prop with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMZdX../e1bfc.. ownership of b6fb9.. as prop with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMcrc../7bf1c.. ownership of f5ca1.. as prop with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMZjp../a724e.. ownership of 2e021.. as prop with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMU28../430ee.. ownership of d2068.. as prop with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMTYq../7cb7e.. ownership of b3b64.. as prop with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMTpT../3f237.. ownership of e862e.. as prop with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMQnX../ce1d0.. ownership of 52257.. as prop with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMHrA../b9e1b.. ownership of 3fd45.. as prop with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMNb1../841f5.. ownership of 163bf.. as prop with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMa7n../1a000.. ownership of 584b5.. as prop with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
PUbPn../6f7bf.. doc published by PrCmT..
Known df_rag__df_perpg__df_hpg__df_mid__df_lmi__df_cgra__df_inag__df_leag__df_eqlg__df_ttg__df_ee__df_btwn__df_cgr__df_eeng__df_edgf__df_vtx__df_iedg__df_edg : ∀ x0 : ο . (wceq crag (cmpt (λ x1 . cvv) (λ x1 . crab (λ x2 . wa (wceq (cfv (cv x2) chash) c3) (wceq (co (cfv cc0 (cv x2)) (cfv c2 (cv x2)) (cfv (cv x1) cds)) (co (cfv cc0 (cv x2)) (cfv (cfv c2 (cv x2)) (cfv (cfv c1 (cv x2)) (cfv (cv x1) cmir))) (cfv (cv x1) cds)))) (λ x2 . cword (cfv (cv x1) cbs))))wceq cperpg (cmpt (λ x1 . cvv) (λ x1 . copab (λ x2 x3 . wa (wa (wcel (cv x2) (crn (cfv (cv x1) clng))) (wcel (cv x3) (crn (cfv (cv x1) clng)))) (wrex (λ x4 . wral (λ x5 . wral (λ x6 . wcel (cs3 (cv x5) (cv x4) (cv x6)) (cfv (cv x1) crag)) (λ x6 . cv x3)) (λ x5 . cv x2)) (λ x4 . cin (cv x2) (cv x3))))))wceq chpg (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . crn (cfv (cv x1) clng)) (λ x2 . copab (λ x3 x4 . wsbc (λ x5 . wsbc (λ x6 . wrex (λ x7 . wa (wa (wa (wcel (cv x3) (cdif (cv x5) (cv x2))) (wcel (cv x7) (cdif (cv x5) (cv x2)))) (wrex (λ x8 . wcel (cv x8) (co (cv x3) (cv x7) (cv x6))) (λ x8 . cv x2))) (wa (wa (wcel (cv x4) (cdif (cv x5) (cv x2))) (wcel (cv x7) (cdif (cv x5) (cv x2)))) (wrex (λ x8 . wcel (cv x8) (co (cv x4) (cv x7) (cv x6))) (λ x8 . cv x2)))) (λ x7 . cv x5)) (cfv (cv x1) citv)) (cfv (cv x1) cbs)))))wceq cmid (cmpt (λ x1 . cvv) (λ x1 . cmpt2 (λ x2 x3 . cfv (cv x1) cbs) (λ x2 x3 . cfv (cv x1) cbs) (λ x2 x3 . crio (λ x4 . wceq (cv x3) (cfv (cv x2) (cfv (cv x4) (cfv (cv x1) cmir)))) (λ x4 . cfv (cv x1) cbs))))wceq clmi (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . crn (cfv (cv x1) clng)) (λ x2 . cmpt (λ x3 . cfv (cv x1) cbs) (λ x3 . crio (λ x4 . wa (wcel (co (cv x3) (cv x4) (cfv (cv x1) cmid)) (cv x2)) (wo (wbr (cv x2) (co (cv x3) (cv x4) (cfv (cv x1) clng)) (cfv (cv x1) cperpg)) (wceq (cv x3) (cv x4)))) (λ x4 . cfv (cv x1) cbs)))))wceq ccgra (cmpt (λ x1 . cvv) (λ x1 . copab (λ x2 x3 . wsbc (λ x4 . wsbc (λ x5 . wa (wa (wcel (cv x2) (co (cv x4) (co cc0 c3 cfzo) cmap)) (wcel (cv x3) (co (cv x4) (co cc0 c3 cfzo) cmap))) (wrex (λ x6 . wrex (λ x7 . w3a (wbr (cv x2) (cs3 (cv x6) (cfv c1 (cv x3)) (cv x7)) (cfv (cv x1) ccgrg)) (wbr (cv x6) (cfv cc0 (cv x3)) (cfv (cfv c1 (cv x3)) (cv x5))) (wbr (cv x7) (cfv c2 (cv x3)) (cfv (cfv c1 (cv x3)) (cv x5)))) (λ x7 . cv x4)) (λ x6 . cv x4))) (cfv (cv x1) chlg)) (cfv (cv x1) cbs))))wceq cinag (cmpt (λ x1 . cvv) (λ x1 . copab (λ x2 x3 . wa (wa (wcel (cv x2) (cfv (cv x1) cbs)) (wcel (cv x3) (co (cfv (cv x1) cbs) (co cc0 c3 cfzo) cmap))) (wa (w3a (wne (cfv cc0 (cv x3)) (cfv c1 (cv x3))) (wne (cfv c2 (cv x3)) (cfv c1 (cv x3))) (wne (cv x2) (cfv c1 (cv x3)))) (wrex (λ x4 . wa (wcel (cv x4) (co (cfv cc0 (cv x3)) (cfv c2 (cv x3)) (cfv (cv x1) citv))) (wo (wceq (cv x4) (cfv c1 (cv x3))) (wbr (cv x4) (cv x2) (cfv (cfv c1 (cv x3)) (cfv (cv x1) chlg))))) (λ x4 . cfv (cv x1) cbs))))))wceq cleag (cmpt (λ x1 . cvv) (λ x1 . copab (λ x2 x3 . wa (wa (wcel (cv x2) (co (cfv (cv x1) cbs) (co cc0 c3 cfzo) cmap)) (wcel (cv x3) (co (cfv (cv x1) cbs) (co cc0 c3 cfzo) cmap))) (wrex (λ x4 . wa (wbr (cv x4) (cs3 (cfv cc0 (cv x3)) (cfv c1 (cv x3)) (cfv c2 (cv x3))) (cfv (cv x1) cinag)) (wbr (cs3 (cfv cc0 (cv x2)) (cfv c1 (cv x2)) (cfv c2 (cv x2))) (cs3 (cfv cc0 (cv x3)) (cfv c1 (cv x3)) (cv x4)) (cfv (cv x1) ccgra))) (λ x4 . cfv (cv x1) cbs)))))wceq ceqlg (cmpt (λ x1 . cvv) (λ x1 . crab (λ x2 . wbr (cv x2) (cs3 (cfv c1 (cv x2)) (cfv c2 (cv x2)) (cfv cc0 (cv x2))) (cfv (cv x1) ccgrg)) (λ x2 . co (cfv (cv x1) cbs) (co cc0 c3 cfzo) cmap)))wceq cttg (cmpt (λ x1 . cvv) (λ x1 . csb (cmpt2 (λ x2 x3 . cfv (cv x1) cbs) (λ x2 x3 . cfv (cv x1) cbs) (λ x2 x3 . crab (λ x4 . wrex (λ x5 . wceq (co (cv x4) (cv x2) (cfv (cv x1) csg)) (co (cv x5) (co (cv x3) (cv x2) (cfv (cv x1) csg)) (cfv (cv x1) cvsca))) (λ x5 . co cc0 c1 cicc)) (λ x4 . cfv (cv x1) cbs))) (λ x2 . co (co (cv x1) (cop (cfv cnx citv) (cv x2)) csts) (cop (cfv cnx clng) (cmpt2 (λ x3 x4 . cfv (cv x1) cbs) (λ x3 x4 . cfv (cv x1) cbs) (λ x3 x4 . crab (λ x5 . w3o (wcel (cv x5) (co (cv x3) (cv x4) (cv x2))) (wcel (cv x3) (co (cv x5) (cv x4) (cv x2))) (wcel (cv x4) (co (cv x3) (cv x5) (cv x2)))) (λ x5 . cfv (cv x1) cbs)))) csts)))wceq cee (cmpt (λ x1 . cn) (λ x1 . co cr (co c1 (cv x1) cfz) cmap))wceq cbtwn (ccnv (coprab (λ x1 x2 x3 . wrex (λ x4 . wa (w3a (wcel (cv x1) (cfv (cv x4) cee)) (wcel (cv x2) (cfv (cv x4) cee)) (wcel (cv x3) (cfv (cv x4) cee))) (wrex (λ x5 . wral (λ x6 . wceq (cfv (cv x6) (cv x3)) (co (co (co c1 (cv x5) cmin) (cfv (cv x6) (cv x1)) cmul) (co (cv x5) (cfv (cv x6) (cv x2)) cmul) caddc)) (λ x6 . co c1 (cv x4) cfz)) (λ x5 . co cc0 c1 cicc))) (λ x4 . cn))))wceq ccgr (copab (λ x1 x2 . wrex (λ x3 . wa (wa (wcel (cv x1) (cxp (cfv (cv x3) cee) (cfv (cv x3) cee))) (wcel (cv x2) (cxp (cfv (cv x3) cee) (cfv (cv x3) cee)))) (wceq (csu (co c1 (cv x3) cfz) (λ x4 . co (co (cfv (cv x4) (cfv (cv x1) c1st)) (cfv (cv x4) (cfv (cv x1) c2nd)) cmin) c2 cexp)) (csu (co c1 (cv x3) cfz) (λ x4 . co (co (cfv (cv x4) (cfv (cv x2) c1st)) (cfv (cv x4) (cfv (cv x2) c2nd)) cmin) c2 cexp)))) (λ x3 . cn)))wceq ceeng (cmpt (λ x1 . cn) (λ x1 . cun (cpr (cop (cfv cnx cbs) (cfv (cv x1) cee)) (cop (cfv cnx cds) (cmpt2 (λ x2 x3 . cfv (cv x1) cee) (λ x2 x3 . cfv (cv x1) cee) (λ x2 x3 . csu (co c1 (cv x1) cfz) (λ x4 . co (co (cfv (cv x4) (cv x2)) (cfv (cv x4) (cv x3)) cmin) c2 cexp))))) (cpr (cop (cfv cnx citv) (cmpt2 (λ x2 x3 . cfv (cv x1) cee) (λ x2 x3 . cfv (cv x1) cee) (λ x2 x3 . crab (λ x4 . wbr (cv x4) (cop (cv x2) (cv x3)) cbtwn) (λ x4 . cfv (cv x1) cee)))) (cop (cfv cnx clng) (cmpt2 (λ x2 x3 . cfv (cv x1) cee) (λ x2 x3 . cdif (cfv (cv x1) cee) (csn (cv x2))) (λ x2 x3 . crab (λ x4 . w3o (wbr (cv x4) (cop (cv x2) (cv x3)) cbtwn) (wbr (cv x2) (cop (cv x4) (cv x3)) cbtwn) (wbr (cv x3) (cop (cv x2) (cv x4)) cbtwn)) (λ x4 . cfv (cv x1) cee)))))))wceq cedgf (cslot (cdc c1 c8))wceq cvtx (cmpt (λ x1 . cvv) (λ x1 . cif (wcel (cv x1) (cxp cvv cvv)) (cfv (cv x1) c1st) (cfv (cv x1) cbs)))wceq ciedg (cmpt (λ x1 . cvv) (λ x1 . cif (wcel (cv x1) (cxp cvv cvv)) (cfv (cv x1) c2nd) (cfv (cv x1) cedgf)))wceq cedg (cmpt (λ x1 . cvv) (λ x1 . crn (cfv (cv x1) ciedg)))x0)x0
Theorem df_rag : wceq crag (cmpt (λ x0 . cvv) (λ x0 . crab (λ x1 . wa (wceq (cfv (cv x1) chash) c3) (wceq (co (cfv cc0 (cv x1)) (cfv c2 (cv x1)) (cfv (cv x0) cds)) (co (cfv cc0 (cv x1)) (cfv (cfv c2 (cv x1)) (cfv (cfv c1 (cv x1)) (cfv (cv x0) cmir))) (cfv (cv x0) cds)))) (λ x1 . cword (cfv (cv x0) cbs)))) (proof)
Theorem df_perpg : wceq cperpg (cmpt (λ x0 . cvv) (λ x0 . copab (λ x1 x2 . wa (wa (wcel (cv x1) (crn (cfv (cv x0) clng))) (wcel (cv x2) (crn (cfv (cv x0) clng)))) (wrex (λ x3 . wral (λ x4 . wral (λ x5 . wcel (cs3 (cv x4) (cv x3) (cv x5)) (cfv (cv x0) crag)) (λ x5 . cv x2)) (λ x4 . cv x1)) (λ x3 . cin (cv x1) (cv x2)))))) (proof)
Theorem df_hpg : wceq chpg (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . crn (cfv (cv x0) clng)) (λ x1 . copab (λ x2 x3 . wsbc (λ x4 . wsbc (λ x5 . wrex (λ x6 . wa (wa (wa (wcel (cv x2) (cdif (cv x4) (cv x1))) (wcel (cv x6) (cdif (cv x4) (cv x1)))) (wrex (λ x7 . wcel (cv x7) (co (cv x2) (cv x6) (cv x5))) (λ x7 . cv x1))) (wa (wa (wcel (cv x3) (cdif (cv x4) (cv x1))) (wcel (cv x6) (cdif (cv x4) (cv x1)))) (wrex (λ x7 . wcel (cv x7) (co (cv x3) (cv x6) (cv x5))) (λ x7 . cv x1)))) (λ x6 . cv x4)) (cfv (cv x0) citv)) (cfv (cv x0) cbs))))) (proof)
Theorem df_mid : wceq cmid (cmpt (λ x0 . cvv) (λ x0 . cmpt2 (λ x1 x2 . cfv (cv x0) cbs) (λ x1 x2 . cfv (cv x0) cbs) (λ x1 x2 . crio (λ x3 . wceq (cv x2) (cfv (cv x1) (cfv (cv x3) (cfv (cv x0) cmir)))) (λ x3 . cfv (cv x0) cbs)))) (proof)
Theorem df_lmi : wceq clmi (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . crn (cfv (cv x0) clng)) (λ x1 . cmpt (λ x2 . cfv (cv x0) cbs) (λ x2 . crio (λ x3 . wa (wcel (co (cv x2) (cv x3) (cfv (cv x0) cmid)) (cv x1)) (wo (wbr (cv x1) (co (cv x2) (cv x3) (cfv (cv x0) clng)) (cfv (cv x0) cperpg)) (wceq (cv x2) (cv x3)))) (λ x3 . cfv (cv x0) cbs))))) (proof)
Theorem df_cgra : wceq ccgra (cmpt (λ x0 . cvv) (λ x0 . copab (λ x1 x2 . wsbc (λ x3 . wsbc (λ x4 . wa (wa (wcel (cv x1) (co (cv x3) (co cc0 c3 cfzo) cmap)) (wcel (cv x2) (co (cv x3) (co cc0 c3 cfzo) cmap))) (wrex (λ x5 . wrex (λ x6 . w3a (wbr (cv x1) (cs3 (cv x5) (cfv c1 (cv x2)) (cv x6)) (cfv (cv x0) ccgrg)) (wbr (cv x5) (cfv cc0 (cv x2)) (cfv (cfv c1 (cv x2)) (cv x4))) (wbr (cv x6) (cfv c2 (cv x2)) (cfv (cfv c1 (cv x2)) (cv x4)))) (λ x6 . cv x3)) (λ x5 . cv x3))) (cfv (cv x0) chlg)) (cfv (cv x0) cbs)))) (proof)
Theorem df_inag : wceq cinag (cmpt (λ x0 . cvv) (λ x0 . copab (λ x1 x2 . wa (wa (wcel (cv x1) (cfv (cv x0) cbs)) (wcel (cv x2) (co (cfv (cv x0) cbs) (co cc0 c3 cfzo) cmap))) (wa (w3a (wne (cfv cc0 (cv x2)) (cfv c1 (cv x2))) (wne (cfv c2 (cv x2)) (cfv c1 (cv x2))) (wne (cv x1) (cfv c1 (cv x2)))) (wrex (λ x3 . wa (wcel (cv x3) (co (cfv cc0 (cv x2)) (cfv c2 (cv x2)) (cfv (cv x0) citv))) (wo (wceq (cv x3) (cfv c1 (cv x2))) (wbr (cv x3) (cv x1) (cfv (cfv c1 (cv x2)) (cfv (cv x0) chlg))))) (λ x3 . cfv (cv x0) cbs)))))) (proof)
Theorem df_leag : wceq cleag (cmpt (λ x0 . cvv) (λ x0 . copab (λ x1 x2 . wa (wa (wcel (cv x1) (co (cfv (cv x0) cbs) (co cc0 c3 cfzo) cmap)) (wcel (cv x2) (co (cfv (cv x0) cbs) (co cc0 c3 cfzo) cmap))) (wrex (λ x3 . wa (wbr (cv x3) (cs3 (cfv cc0 (cv x2)) (cfv c1 (cv x2)) (cfv c2 (cv x2))) (cfv (cv x0) cinag)) (wbr (cs3 (cfv cc0 (cv x1)) (cfv c1 (cv x1)) (cfv c2 (cv x1))) (cs3 (cfv cc0 (cv x2)) (cfv c1 (cv x2)) (cv x3)) (cfv (cv x0) ccgra))) (λ x3 . cfv (cv x0) cbs))))) (proof)
Theorem df_eqlg : wceq ceqlg (cmpt (λ x0 . cvv) (λ x0 . crab (λ x1 . wbr (cv x1) (cs3 (cfv c1 (cv x1)) (cfv c2 (cv x1)) (cfv cc0 (cv x1))) (cfv (cv x0) ccgrg)) (λ x1 . co (cfv (cv x0) cbs) (co cc0 c3 cfzo) cmap))) (proof)
Theorem df_ttg : wceq cttg (cmpt (λ x0 . cvv) (λ x0 . csb (cmpt2 (λ x1 x2 . cfv (cv x0) cbs) (λ x1 x2 . cfv (cv x0) cbs) (λ x1 x2 . crab (λ x3 . wrex (λ x4 . wceq (co (cv x3) (cv x1) (cfv (cv x0) csg)) (co (cv x4) (co (cv x2) (cv x1) (cfv (cv x0) csg)) (cfv (cv x0) cvsca))) (λ x4 . co cc0 c1 cicc)) (λ x3 . cfv (cv x0) cbs))) (λ x1 . co (co (cv x0) (cop (cfv cnx citv) (cv x1)) csts) (cop (cfv cnx clng) (cmpt2 (λ x2 x3 . cfv (cv x0) cbs) (λ x2 x3 . cfv (cv x0) cbs) (λ x2 x3 . crab (λ x4 . w3o (wcel (cv x4) (co (cv x2) (cv x3) (cv x1))) (wcel (cv x2) (co (cv x4) (cv x3) (cv x1))) (wcel (cv x3) (co (cv x2) (cv x4) (cv x1)))) (λ x4 . cfv (cv x0) cbs)))) csts))) (proof)
Theorem df_ee : wceq cee (cmpt (λ x0 . cn) (λ x0 . co cr (co c1 (cv x0) cfz) cmap)) (proof)
Theorem df_btwn : wceq cbtwn (ccnv (coprab (λ x0 x1 x2 . wrex (λ x3 . wa (w3a (wcel (cv x0) (cfv (cv x3) cee)) (wcel (cv x1) (cfv (cv x3) cee)) (wcel (cv x2) (cfv (cv x3) cee))) (wrex (λ x4 . wral (λ x5 . wceq (cfv (cv x5) (cv x2)) (co (co (co c1 (cv x4) cmin) (cfv (cv x5) (cv x0)) cmul) (co (cv x4) (cfv (cv x5) (cv x1)) cmul) caddc)) (λ x5 . co c1 (cv x3) cfz)) (λ x4 . co cc0 c1 cicc))) (λ x3 . cn)))) (proof)
Theorem df_cgr : wceq ccgr (copab (λ x0 x1 . wrex (λ x2 . wa (wa (wcel (cv x0) (cxp (cfv (cv x2) cee) (cfv (cv x2) cee))) (wcel (cv x1) (cxp (cfv (cv x2) cee) (cfv (cv x2) cee)))) (wceq (csu (co c1 (cv x2) cfz) (λ x3 . co (co (cfv (cv x3) (cfv (cv x0) c1st)) (cfv (cv x3) (cfv (cv x0) c2nd)) cmin) c2 cexp)) (csu (co c1 (cv x2) cfz) (λ x3 . co (co (cfv (cv x3) (cfv (cv x1) c1st)) (cfv (cv x3) (cfv (cv x1) c2nd)) cmin) c2 cexp)))) (λ x2 . cn))) (proof)
Theorem df_eeng : wceq ceeng (cmpt (λ x0 . cn) (λ x0 . cun (cpr (cop (cfv cnx cbs) (cfv (cv x0) cee)) (cop (cfv cnx cds) (cmpt2 (λ x1 x2 . cfv (cv x0) cee) (λ x1 x2 . cfv (cv x0) cee) (λ x1 x2 . csu (co c1 (cv x0) cfz) (λ x3 . co (co (cfv (cv x3) (cv x1)) (cfv (cv x3) (cv x2)) cmin) c2 cexp))))) (cpr (cop (cfv cnx citv) (cmpt2 (λ x1 x2 . cfv (cv x0) cee) (λ x1 x2 . cfv (cv x0) cee) (λ x1 x2 . crab (λ x3 . wbr (cv x3) (cop (cv x1) (cv x2)) cbtwn) (λ x3 . cfv (cv x0) cee)))) (cop (cfv cnx clng) (cmpt2 (λ x1 x2 . cfv (cv x0) cee) (λ x1 x2 . cdif (cfv (cv x0) cee) (csn (cv x1))) (λ x1 x2 . crab (λ x3 . w3o (wbr (cv x3) (cop (cv x1) (cv x2)) cbtwn) (wbr (cv x1) (cop (cv x3) (cv x2)) cbtwn) (wbr (cv x2) (cop (cv x1) (cv x3)) cbtwn)) (λ x3 . cfv (cv x0) cee))))))) (proof)
Theorem df_edgf : wceq cedgf (cslot (cdc c1 c8)) (proof)
Theorem df_vtx : wceq cvtx (cmpt (λ x0 . cvv) (λ x0 . cif (wcel (cv x0) (cxp cvv cvv)) (cfv (cv x0) c1st) (cfv (cv x0) cbs))) (proof)
Theorem df_iedg : wceq ciedg (cmpt (λ x0 . cvv) (λ x0 . cif (wcel (cv x0) (cxp cvv cvv)) (cfv (cv x0) c2nd) (cfv (cv x0) cedgf))) (proof)
Theorem df_edg : wceq cedg (cmpt (λ x0 . cvv) (λ x0 . crn (cfv (cv x0) ciedg))) (proof)