Proofgold Signed Transaction

vin
PrDV8../88b8d.. PURgz../35bf3..

vout

PrDV8../043f7.. 0.09 bars
TMVkh../077f9.. ownership of d455c.. as prop with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMTrh../c956a.. ownership of 1d177.. as prop with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMJF4../3c8ba.. ownership of 56b46.. as prop with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMHUX../cc87f.. ownership of 61f57.. as prop with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMJyn../16945.. ownership of 9a70c.. as prop with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMF3w../c3391.. ownership of cec87.. as prop with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMHvq../6d9a9.. ownership of 3f03c.. as prop with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMZhX../b0285.. ownership of d226c.. as prop with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMXAd../2f26e.. ownership of 9c7c0.. as prop with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMFyK../20a51.. ownership of c75c1.. as prop with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMWL3../3a86b.. ownership of 7d35f.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMKSD../0fe81.. ownership of 89a97.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMaGS../fd861.. ownership of 369fc.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMTSd../81e48.. ownership of e4286.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMdeY../518ed.. ownership of d78bf.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMJ4M../0f8c5.. ownership of c54c3.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMatw../a1864.. ownership of bf553.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMQKh../29f90.. ownership of 54e15.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMYQY../1e809.. ownership of 9811d.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMJyf../efdd3.. ownership of 6128f.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMZFN../472d8.. ownership of 31ab2.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMVXa../95555.. ownership of 6deaf.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMNEv../f2e9e.. ownership of e5fbc.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMVgu../357ef.. ownership of 24032.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMFdf../a3fda.. ownership of 4270f.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMZPQ../a9ad6.. ownership of a940f.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMFT4../4e5d1.. ownership of fc929.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMaA1../4a149.. ownership of 53558.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMasQ../e661c.. ownership of aecb4.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMKoC../ad846.. ownership of 8c736.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMR2t../b35b3.. ownership of c2e40.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMc1A../3a58a.. ownership of faf78.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMFhd../9e5d8.. ownership of f11d4.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMZ7K../b4885.. ownership of 251bb.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMbsf../153da.. ownership of 0c73c.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMZA4../50f43.. ownership of bcc6d.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMQfi../15c17.. ownership of 30d33.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMSwp../97473.. ownership of b3c32.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMEny../5be32.. ownership of 32904.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMWVC../323d5.. ownership of f0bc6.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMFjm../405b5.. ownership of 22298.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMdmZ../4503f.. ownership of cc16a.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMN7v../a00e7.. ownership of 979de.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMbuz../81a56.. ownership of b9abb.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMcWE../6a8a9.. ownership of f46a9.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMawa../f05cd.. ownership of 31219.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMSzY../bba74.. ownership of 8ad00.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMYpj../9ee29.. ownership of d96a9.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMd2d../b9ef4.. ownership of e8a77.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMXyd../5d549.. ownership of 86ba4.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMQUY../3fc37.. ownership of 5fcff.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMXmk../785f4.. ownership of 608b1.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMKZJ../c12f9.. ownership of 2ccd6.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TML4M../ee762.. ownership of e1fb7.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMHsw../63854.. ownership of b780d.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMaB5../35176.. ownership of b2cf6.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMaWK../ea6df.. ownership of 79292.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMHSk../24a0b.. ownership of f8396.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMRX6../2a54d.. ownership of 9cd9c.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMbpr../a5687.. ownership of ca396.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMJcu../3a5c7.. ownership of 9a82f.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMWWd../428cf.. ownership of 6b4ca.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMKDL../44f39.. ownership of b6bde.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMFry../0a805.. ownership of f8623.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMSQQ../829a2.. ownership of 18fcc.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMbsp../0f2a3.. ownership of c19fe.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMGXY../d86ce.. ownership of 8e0b7.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMUG6../1657e.. ownership of acd43.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TML2y../eb950.. ownership of e84f4.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMJmZ../17797.. ownership of 58698.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMYbE../fafa8.. ownership of 0a1a8.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMLSp../bbfa1.. ownership of a5398.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMQZv../a60f3.. ownership of b35fa.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMRap../f7cc5.. ownership of 01ff6.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMSJo../fa734.. ownership of a0cd6.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMS3y../6549a.. ownership of dfea9.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMKwK../4e68c.. ownership of 56cdb.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMLWj../4047c.. ownership of 9146d.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMJ26../b34b0.. ownership of 49a39.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMXiR../9c809.. ownership of 26c2f.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMTB7../49b37.. ownership of a6787.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMTmu../9115a.. ownership of 56224.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMcNX../e73fe.. ownership of cc2a4.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMXb5../978c7.. ownership of 6488e.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMZaV../fac14.. ownership of 96240.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMP8D../c4b91.. ownership of 1deca.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMVeF../cd5a3.. ownership of cea39.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMNyo../9cbdb.. ownership of f70ba.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMb2t../44ce8.. ownership of 94acf.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMKn2../5acbe.. ownership of fa6b6.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMJ4G../4869f.. ownership of 7e3ac.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMKiw../b78df.. ownership of def52.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMHM5../e0bef.. ownership of ca6d4.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMKpa../521ba.. ownership of cfedb.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMQM6../99561.. ownership of a1371.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMTGi../50cbb.. ownership of 05d80.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMbbF../da5de.. ownership of f9c98.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMVR6../461eb.. ownership of 1a421.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMNxh../df430.. ownership of 32c47.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMX2K../ab21f.. ownership of e811b.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMGPq../34af8.. ownership of 827d9.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
TMTeK../8b551.. ownership of 4edaf.. as obj with payaddr PrCmT.. rights free controlledby PrCmT.. upto 0
PUZP5../7c455.. doc published by PrCmT..

Definition csect := csect
Definition cinv := cinv
Definition ccic := ccic
Definition ciso := ciso
Definition c0 := c0
Definition csupp := csupp
Definition wex := wex
Definition wfn := wfn
Definition wrex := wrex
Definition cpw := cpw
Definition cresc := cresc
Definition cress := cress
Definition csts := csts
Definition csubc := csubc
Definition cab := cab
Definition chomf := chomf
Definition cssc := cssc
Definition wsbc^wsbc := wsbc
Definition w3a := w3a
Definition wf := wf
Definition cmap := cmap
Definition ccid := ccid
Definition cidfu := cidfu
Definition cid := cid
Definition ccofu := ccofu
Definition cresf := cresf
Definition cvv := cvv
Definition cdm := cdm
Definition cres := cres
Definition cful := cful
Definition crn := crn
Definition cfth := cfth
Definition copab := copab
Definition wa := wa
Definition wbr := wbr
Definition wfun := wfun
Definition ccnv := ccnv
Definition cixp := cixp
Definition cfuc := cfuc
Definition ctp := ctp
Definition cnx := cnx
Definition cxp := cxp
Definition cfunc := cfunc
Definition csb := csb
Definition c2nd := c2nd
Definition cmpt2 := cmpt2
Definition cnat := cnat
Definition cop := cop
Definition cco := cco
Definition crab := crab
Definition wral := wral
Definition weu := weu
Definition wcel := wcel
Definition co := co
Definition chom := chom
Definition cbs := cbs
Definition czeroo := czeroo
Definition cmpt := cmpt
Definition ccat := ccat
Definition cin := cin
Definition cinito := cinito
Definition cfv := cfv
Definition cv := cv
Definition ctermo := ctermo
Definition wceq^wceq := wceq
Definition cdoma := cdoma
Definition ccom := ccom
Definition c1st := c1st
Known 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 : ∀ 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
Theorem df_iso : wceq ciso (cmpt (λ x0 . ccat) (λ x0 . ccom (cmpt (λ x1 . cvv) (λ x1 . cdm (cv x1))) (cfv (cv x0) cinv))) (proof)
Theorem df_subc : wceq csubc (cmpt (λ x0 . ccat) (λ x0 . cab (λ x1 . wa (wbr (cv x1) (cfv (cv x0) chomf) cssc) (wsbc (λ x2 . wral (λ x3 . wa (wcel (cfv (cv x3) (cfv (cv x0) ccid)) (co (cv x3) (cv x3) (cv x1))) (wral (λ x4 . wral (λ x5 . wral (λ x6 . wral (λ x7 . wcel (co (cv x7) (cv x6) (co (cop (cv x3) (cv x4)) (cv x5) (cfv (cv x0) cco))) (co (cv x3) (cv x5) (cv x1))) (λ x7 . co (cv x4) (cv x5) (cv x1))) (λ x6 . co (cv x3) (cv x4) (cv x1))) (λ x5 . cv x2)) (λ x4 . cv x2))) (λ x3 . cv x2)) (cdm (cdm (cv x1))))))) (proof)
Theorem df_resf : wceq cresf (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . cop (cres (cfv (cv x0) c1st) (cdm (cdm (cv x1)))) (cmpt (λ x2 . cdm (cv x1)) (λ x2 . cres (cfv (cv x2) (cfv (cv x0) c2nd)) (cfv (cv x2) (cv x1)))))) (proof)
Theorem df_fuc : wceq cfuc (cmpt2 (λ x0 x1 . ccat) (λ x0 x1 . ccat) (λ x0 x1 . ctp (cop (cfv cnx cbs) (co (cv x0) (cv x1) cfunc)) (cop (cfv cnx chom) (co (cv x0) (cv x1) cnat)) (cop (cfv cnx cco) (cmpt2 (λ x2 x3 . cxp (co (cv x0) (cv x1) cfunc) (co (cv x0) (cv x1) cfunc)) (λ x2 x3 . co (cv x0) (cv x1) cfunc) (λ x2 x3 . csb (cfv (cv x2) c1st) (λ x4 . csb (cfv (cv x2) c2nd) (λ x5 . cmpt2 (λ x6 x7 . co (cv x5) (cv x3) (co (cv x0) (cv x1) cnat)) (λ x6 x7 . co (cv x4) (cv x5) (co (cv x0) (cv x1) cnat)) (λ x6 x7 . cmpt (λ x8 . cfv (cv x0) cbs) (λ x8 . co (cfv (cv x8) (cv x6)) (cfv (cv x8) (cv x7)) (co (cop (cfv (cv x8) (cfv (cv x4) c1st)) (cfv (cv x8) (cfv (cv x5) c1st))) (cfv (cv x8) (cfv (cv x3) c1st)) (cfv (cv x1) cco))))))))))) (proof)
Theorem df_doma : wceq cdoma (ccom c1st c1st) (proof)