Proofgold Signed Transaction

Definition ccnp := ccnp
Definition cmpt2 := cmpt2
Definition cima := cima
Definition clm := clm
Definition cc := cc
Definition cpm := cpm
Definition wf := wf
Definition cres := cres
Definition cuz := cuz
Definition ct0 := ct0
Definition wb := wb
Definition ct1 := ct1
Definition cha := cha
Definition w3a := w3a
Definition creg := creg
Definition ccl := ccl
Definition ccnrm := ccnrm
Definition cpnrm := cpnrm
Definition cn := cn
Definition cmap := cmap
Definition cint := cint
Definition crn := crn
Definition cnrm := cnrm
Definition ccmp := ccmp
Definition cconn := cconn
Definition ccld := ccld
Definition cpr := cpr
Definition c1stc := c1stc
Definition c2ndc := c2ndc
Definition wbr := wbr
Definition com := com
Definition cdom := cdom
Definition ctg := ctg
Definition ctb := ctb
Definition clly := clly
Definition cnlly := cnlly
Definition co := co
Definition crest := crest
Definition csn := csn
Definition cfv := cfv
Definition cnei := cnei
Definition cpw := cpw
Definition cref := cref
Definition copab := copab
Definition wss := wss
Definition cptfin := cptfin
Definition clocfin := clocfin
Definition cmpt := cmpt
Definition ctop := ctop
Definition cab := cab
Definition wceq^wceq := wceq
Definition wral := wral
Definition wrex := wrex
Definition wa := wa
Definition wcel := wcel
Definition crab := crab
Definition wne := wne
Definition cin := cin
Definition c0 := c0
Definition cfn := cfn
Definition cuni := cuni
Definition cv := cv
Known df_cnp__df_lm__df_t0__df_t1__df_haus__df_reg__df_nrm__df_cnrm__df_pnrm__df_cmp__df_conn__df_1stc__df_2ndc__df_lly__df_nlly__df_ref__df_ptfin__df_locfin : ∀ x0 : ο . (wceq ccnp (cmpt2 (λ x1 x2 . ctop) (λ x1 x2 . ctop) (λ x1 x2 . cmpt (λ x3 . cuni (cv x1)) (λ x3 . crab (λ x4 . wral (λ x5 . wcel (cfv (cv x3) (cv x4)) (cv x5) ⟶ wrex (λ x6 . wa (wcel (cv x3) (cv x6)) (wss (cima (cv x4) (cv x6)) (cv x5))) (λ x6 . cv x1)) (λ x5 . cv x2)) (λ x4 . co (cuni (cv x2)) (cuni (cv x1)) cmap)))) ⟶ wceq clm (cmpt (λ x1 . ctop) (λ x1 . copab (λ x2 x3 . w3a (wcel (cv x2) (co (cuni (cv x1)) cc cpm)) (wcel (cv x3) (cuni (cv x1))) (wral (λ x4 . wcel (cv x3) (cv x4) ⟶ wrex (λ x5 . wf (cv x5) (cv x4) (cres (cv x2) (cv x5))) (λ x5 . crn cuz)) (λ x4 . cv x1))))) ⟶ wceq ct0 (crab (λ x1 . wral (λ x2 . wral (λ x3 . wral (λ x4 . wb (wcel (cv x2) (cv x4)) (wcel (cv x3) (cv x4))) (λ x4 . cv x1) ⟶ wceq (cv x2) (cv x3)) (λ x3 . cuni (cv x1))) (λ x2 . cuni (cv x1))) (λ x1 . ctop)) ⟶ wceq ct1 (crab (λ x1 . wral (λ x2 . wcel (csn (cv x2)) (cfv (cv x1) ccld)) (λ x2 . cuni (cv x1))) (λ x1 . ctop)) ⟶ wceq cha (crab (λ x1 . wral (λ x2 . wral (λ x3 . wne (cv x2) (cv x3) ⟶ wrex (λ x4 . wrex (λ x5 . w3a (wcel (cv x2) (cv x4)) (wcel (cv x3) (cv x5)) (wceq (cin (cv x4) (cv x5)) c0)) (λ x5 . cv x1)) (λ x4 . cv x1)) (λ x3 . cuni (cv x1))) (λ x2 . cuni (cv x1))) (λ x1 . ctop)) ⟶ wceq creg (crab (λ x1 . wral (λ x2 . wral (λ x3 . wrex (λ x4 . wa (wcel (cv x3) (cv x4)) (wss (cfv (cv x4) (cfv (cv x1) ccl)) (cv x2))) (λ x4 . cv x1)) (λ x3 . cv x2)) (λ x2 . cv x1)) (λ x1 . ctop)) ⟶ wceq cnrm (crab (λ x1 . wral (λ x2 . wral (λ x3 . wrex (λ x4 . wa (wss (cv x3) (cv x4)) (wss (cfv (cv x4) (cfv (cv x1) ccl)) (cv x2))) (λ x4 . cv x1)) (λ x3 . cin (cfv (cv x1) ccld) (cpw (cv x2)))) (λ x2 . cv x1)) (λ x1 . ctop)) ⟶ wceq ccnrm (crab (λ x1 . wral (λ x2 . wcel (co (cv x1) (cv x2) crest) cnrm) (λ x2 . cpw (cuni (cv x1)))) (λ x1 . ctop)) ⟶ wceq cpnrm (crab (λ x1 . wss (cfv (cv x1) ccld) (crn (cmpt (λ x2 . co (cv x1) cn cmap) (λ x2 . cint (crn (cv x2)))))) (λ x1 . cnrm)) ⟶ wceq ccmp (crab (λ x1 . wral (λ x2 . wceq (cuni (cv x1)) (cuni (cv x2)) ⟶ wrex (λ x3 . wceq (cuni (cv x1)) (cuni (cv x3))) (λ x3 . cin (cpw (cv x2)) cfn)) (λ x2 . cpw (cv x1))) (λ x1 . ctop)) ⟶ wceq cconn (crab (λ x1 . wceq (cin (cv x1) (cfv (cv x1) ccld)) (cpr c0 (cuni (cv x1)))) (λ x1 . ctop)) ⟶ wceq c1stc (crab (λ x1 . wral (λ x2 . wrex (λ x3 . wa (wbr (cv x3) com cdom) (wral (λ x4 . wcel (cv x2) (cv x4) ⟶ wcel (cv x2) (cuni (cin (cv x3) (cpw (cv x4))))) (λ x4 . cv x1))) (λ x3 . cpw (cv x1))) (λ x2 . cuni (cv x1))) (λ x1 . ctop)) ⟶ wceq c2ndc (cab (λ x1 . wrex (λ x2 . wa (wbr (cv x2) com cdom) (wceq (cfv (cv x2) ctg) (cv x1))) (λ x2 . ctb))) ⟶ (∀ x1 : ι → ο . wceq (clly x1) (crab (λ x2 . wral (λ x3 . wral (λ x4 . wrex (λ x5 . wa (wcel (cv x4) (cv x5)) (wcel (co (cv x2) (cv x5) crest) x1)) (λ x5 . cin (cv x2) (cpw (cv x3)))) (λ x4 . cv x3)) (λ x3 . cv x2)) (λ x2 . ctop))) ⟶ (∀ x1 : ι → ο . wceq (cnlly x1) (crab (λ x2 . wral (λ x3 . wral (λ x4 . wrex (λ x5 . wcel (co (cv x2) (cv x5) crest) x1) (λ x5 . cin (cfv (csn (cv x4)) (cfv (cv x2) cnei)) (cpw (cv x3)))) (λ x4 . cv x3)) (λ x3 . cv x2)) (λ x2 . ctop))) ⟶ wceq cref (copab (λ x1 x2 . wa (wceq (cuni (cv x2)) (cuni (cv x1))) (wral (λ x3 . wrex (λ x4 . wss (cv x3) (cv x4)) (λ x4 . cv x2)) (λ x3 . cv x1)))) ⟶ wceq cptfin (cab (λ x1 . wral (λ x2 . wcel (crab (λ x3 . wcel (cv x2) (cv x3)) (λ x3 . cv x1)) cfn) (λ x2 . cuni (cv x1)))) ⟶ wceq clocfin (cmpt (λ x1 . ctop) (λ x1 . cab (λ x2 . wa (wceq (cuni (cv x1)) (cuni (cv x2))) (wral (λ x3 . wrex (λ x4 . wa (wcel (cv x3) (cv x4)) (wcel (crab (λ x5 . wne (cin (cv x5) (cv x4)) c0) (λ x5 . cv x2)) cfn)) (λ x4 . cv x1)) (λ x3 . cuni (cv x1)))))) ⟶ x0) ⟶ x0
Theorem df_cnp : wceq ccnp (cmpt2 (λ x0 x1 . ctop) (λ x0 x1 . ctop) (λ x0 x1 . cmpt (λ x2 . cuni (cv x0)) (λ x2 . crab (λ x3 . wral (λ x4 . wcel (cfv (cv x2) (cv x3)) (cv x4) ⟶ wrex (λ x5 . wa (wcel (cv x2) (cv x5)) (wss (cima (cv x3) (cv x5)) (cv x4))) (λ x5 . cv x0)) (λ x4 . cv x1)) (λ x3 . co (cuni (cv x1)) (cuni (cv x0)) cmap)))) (proof)
Theorem df_t0 : wceq ct0 (crab (λ x0 . wral (λ x1 . wral (λ x2 . wral (λ x3 . wb (wcel (cv x1) (cv x3)) (wcel (cv x2) (cv x3))) (λ x3 . cv x0) ⟶ wceq (cv x1) (cv x2)) (λ x2 . cuni (cv x0))) (λ x1 . cuni (cv x0))) (λ x0 . ctop)) (proof)
Theorem df_haus : wceq cha (crab (λ x0 . wral (λ x1 . wral (λ x2 . wne (cv x1) (cv x2) ⟶ wrex (λ x3 . wrex (λ x4 . w3a (wcel (cv x1) (cv x3)) (wcel (cv x2) (cv x4)) (wceq (cin (cv x3) (cv x4)) c0)) (λ x4 . cv x0)) (λ x3 . cv x0)) (λ x2 . cuni (cv x0))) (λ x1 . cuni (cv x0))) (λ x0 . ctop)) (proof)
Theorem df_nrm : wceq cnrm (crab (λ x0 . wral (λ x1 . wral (λ x2 . wrex (λ x3 . wa (wss (cv x2) (cv x3)) (wss (cfv (cv x3) (cfv (cv x0) ccl)) (cv x1))) (λ x3 . cv x0)) (λ x2 . cin (cfv (cv x0) ccld) (cpw (cv x1)))) (λ x1 . cv x0)) (λ x0 . ctop)) (proof)
Theorem df_pnrm : wceq cpnrm (crab (λ x0 . wss (cfv (cv x0) ccld) (crn (cmpt (λ x1 . co (cv x0) cn cmap) (λ x1 . cint (crn (cv x1)))))) (λ x0 . cnrm)) (proof)
Theorem df_conn : wceq cconn (crab (λ x0 . wceq (cin (cv x0) (cfv (cv x0) ccld)) (cpr c0 (cuni (cv x0)))) (λ x0 . ctop)) (proof)
Theorem df_2ndc : wceq c2ndc (cab (λ x0 . wrex (λ x1 . wa (wbr (cv x1) com cdom) (wceq (cfv (cv x1) ctg) (cv x0))) (λ x1 . ctb))) (proof)
Theorem df_nlly : ∀ x0 : ι → ο . wceq (cnlly x0) (crab (λ x1 . wral (λ x2 . wral (λ x3 . wrex (λ x4 . wcel (co (cv x1) (cv x4) crest) x0) (λ x4 . cin (cfv (csn (cv x3)) (cfv (cv x1) cnei)) (cpw (cv x2)))) (λ x3 . cv x2)) (λ x2 . cv x1)) (λ x1 . ctop)) (proof)
Theorem df_ptfin : wceq cptfin (cab (λ x0 . wral (λ x1 . wcel (crab (λ x2 . wcel (cv x1) (cv x2)) (λ x2 . cv x0)) cfn) (λ x1 . cuni (cv x0)))) (proof)