Proofgold Address

Known df_msub__df_mvh__df_mpst__df_msr__df_msta__df_mfs__df_mcls__df_mpps__df_mthm__df_m0s__df_msa__df_mwgfs__df_msyn__df_mtree__df_mst__df_msax__df_mufs__df_muv : ∀ x0 : ο . (wceq cmsub (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . co (cfv (cv x1) cmrex) (cfv (cv x1) cmvar) cpm) (λ x2 . cmpt (λ x3 . cfv (cv x1) cmex) (λ x3 . cop (cfv (cv x3) c1st) (cfv (cfv (cv x3) c2nd) (cfv (cv x2) (cfv (cv x1) cmrsub))))))) ⟶ wceq cmvh (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cfv (cv x1) cmvar) (λ x2 . cop (cfv (cv x2) (cfv (cv x1) cmty)) (cs1 (cv x2))))) ⟶ wceq cmpst (cmpt (λ x1 . cvv) (λ x1 . cxp (cxp (crab (λ x2 . wceq (ccnv (cv x2)) (cv x2)) (λ x2 . cpw (cfv (cv x1) cmdv))) (cin (cpw (cfv (cv x1) cmex)) cfn)) (cfv (cv x1) cmex))) ⟶ wceq cmsr (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cfv (cv x1) cmpst) (λ x2 . csb (cfv (cfv (cv x2) c1st) c2nd) (λ x3 . csb (cfv (cv x2) c2nd) (λ x4 . cotp (cin (cfv (cfv (cv x2) c1st) c1st) (csb (cuni (cima (cfv (cv x1) cmvrs) (cun (cv x3) (csn (cv x4))))) (λ x5 . cxp (cv x5) (cv x5)))) (cv x3) (cv x4)))))) ⟶ wceq cmsta (cmpt (λ x1 . cvv) (λ x1 . crn (cfv (cv x1) cmsr))) ⟶ wceq cmfs (cab (λ x1 . wa (wa (wceq (cin (cfv (cv x1) cmcn) (cfv (cv x1) cmvar)) c0) (wf (cfv (cv x1) cmvar) (cfv (cv x1) cmtc) (cfv (cv x1) cmty))) (wa (wss (cfv (cv x1) cmax) (cfv (cv x1) cmsta)) (wral (λ x2 . wn (wcel (cima (ccnv (cfv (cv x1) cmty)) (csn (cv x2))) cfn)) (λ x2 . cfv (cv x1) cmvt))))) ⟶ wceq cmcls (cmpt (λ x1 . cvv) (λ x1 . cmpt2 (λ x2 x3 . cpw (cfv (cv x1) cmdv)) (λ x2 x3 . cpw (cfv (cv x1) cmex)) (λ x2 x3 . cint (cab (λ x4 . wa (wss (cun (cv x3) (crn (cfv (cv x1) cmvh))) (cv x4)) (∀ x5 x6 x7 . wcel (cotp (cv x5) (cv x6) (cv x7)) (cfv (cv x1) cmax) ⟶ wral (λ x8 . wa (wss (cima (cv x8) (cun (cv x6) (crn (cfv (cv x1) cmvh)))) (cv x4)) (∀ x9 x10 . wbr (cv x9) (cv x10) (cv x5) ⟶ wss (cxp (cfv (cfv (cfv (cv x9) (cfv (cv x1) cmvh)) (cv x8)) (cfv (cv x1) cmvrs)) (cfv (cfv (cfv (cv x10) (cfv (cv x1) cmvh)) (cv x8)) (cfv (cv x1) cmvrs))) (cv x2)) ⟶ wcel (cfv (cv x7) (cv x8)) (cv x4)) (λ x8 . crn (cfv (cv x1) cmsub)))))))) ⟶ wceq cmpps (cmpt (λ x1 . cvv) (λ x1 . coprab (λ x2 x3 x4 . wa (wcel (cotp (cv x2) (cv x3) (cv x4)) (cfv (cv x1) cmpst)) (wcel (cv x4) (co (cv x2) (cv x3) (cfv (cv x1) cmcls)))))) ⟶ wceq cmthm (cmpt (λ x1 . cvv) (λ x1 . cima (ccnv (cfv (cv x1) cmsr)) (cima (cfv (cv x1) cmsr) (cfv (cv x1) cmpps)))) ⟶ wceq cm0s (cmpt (λ x1 . cvv) (λ x1 . cotp c0 c0 (cv x1))) ⟶ wceq cmsa (cmpt (λ x1 . cvv) (λ x1 . crab (λ x2 . w3a (wcel (cfv (cv x2) cm0s) (cfv (cv x1) cmax)) (wcel (cfv (cv x2) c1st) (cfv (cv x1) cmvt)) (wfun (cres (ccnv (cfv (cv x2) c2nd)) (cfv (cv x1) cmvar)))) (λ x2 . cfv (cv x1) cmex))) ⟶ wceq cmwgfs (crab (λ x1 . ∀ x2 x3 x4 . wa (wcel (cotp (cv x2) (cv x3) (cv x4)) (cfv (cv x1) cmax)) (wcel (cfv (cv x4) c1st) (cfv (cv x1) cmvt)) ⟶ wrex (λ x5 . wcel (cv x4) (cima (cv x5) (cfv (cv x1) cmsa))) (λ x5 . crn (cfv (cv x1) cmsub))) (λ x1 . cmfs)) ⟶ wceq cmsy (cslot c6) ⟶ wceq cmtree (cmpt (λ x1 . cvv) (λ x1 . cmpt2 (λ x2 x3 . cpw (cfv (cv x1) cmdv)) (λ x2 x3 . cpw (cfv (cv x1) cmex)) (λ x2 x3 . cint (cab (λ x4 . w3a (wral (λ x5 . wbr (cv x5) (cop (cfv (cv x5) cm0s) c0) (cv x4)) (λ x5 . crn (cfv (cv x1) cmvh))) (wral (λ x5 . wbr (cv x5) (cop (cfv (cotp (cv x2) (cv x3) (cv x5)) (cfv (cv x1) cmsr)) c0) (cv x4)) (λ x5 . cv x3)) (∀ x5 x6 x7 . wcel (cotp (cv x5) (cv x6) (cv x7)) (cfv (cv x1) cmax) ⟶ wral (λ x8 . (∀ x9 x10 . wbr (cv x9) (cv x10) (cv x5) ⟶ wss (cxp (cfv (cfv (cfv (cv x9) (cfv (cv x1) cmvh)) (cv x8)) (cfv (cv x1) cmvrs)) (cfv (cfv (cfv (cv x10) (cfv (cv x1) cmvh)) (cv x8)) (cfv (cv x1) cmvrs))) (cv x2)) ⟶ wss (cxp (csn (cfv (cv x7) (cv x8))) (cixp (λ x9 . cun (cv x6) (cima (cfv (cv x1) cmvh) (cuni (cima (cfv (cv x1) cmvrs) (cun (cv x6) (csn (cv x7))))))) (λ x9 . cima (cv x4) (csn (cfv (cv x9) (cv x8)))))) (cv x4)) (λ x8 . crn (cfv (cv x1) cmsub)))))))) ⟶ wceq cmst (cmpt (λ x1 . cvv) (λ x1 . cres (co c0 c0 (cfv (cv x1) cmtree)) (cres (cfv (cv x1) cmex) (cfv (cv x1) cmvt)))) ⟶ wceq cmsax (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cfv (cv x1) cmsa) (λ x2 . cima (cfv (cv x1) cmvh) (cfv (cv x2) (cfv (cv x1) cmvrs))))) ⟶ wceq cmufs (crab (λ x1 . wfun (cfv (cv x1) cmst)) (λ x1 . cmgfs)) ⟶ wceq cmuv (cslot c7) ⟶ x0) ⟶ x0
Theorem df_msub : wceq cmsub (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . co (cfv (cv x0) cmrex) (cfv (cv x0) cmvar) cpm) (λ x1 . cmpt (λ x2 . cfv (cv x0) cmex) (λ x2 . cop (cfv (cv x2) c1st) (cfv (cfv (cv x2) c2nd) (cfv (cv x1) (cfv (cv x0) cmrsub))))))) (proof)
Theorem df_mvh : wceq cmvh (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cfv (cv x0) cmvar) (λ x1 . cop (cfv (cv x1) (cfv (cv x0) cmty)) (cs1 (cv x1))))) (proof)
Theorem df_mpst : wceq cmpst (cmpt (λ x0 . cvv) (λ x0 . cxp (cxp (crab (λ x1 . wceq (ccnv (cv x1)) (cv x1)) (λ x1 . cpw (cfv (cv x0) cmdv))) (cin (cpw (cfv (cv x0) cmex)) cfn)) (cfv (cv x0) cmex))) (proof)
Theorem df_msr : wceq cmsr (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cfv (cv x0) cmpst) (λ x1 . csb (cfv (cfv (cv x1) c1st) c2nd) (λ x2 . csb (cfv (cv x1) c2nd) (λ x3 . cotp (cin (cfv (cfv (cv x1) c1st) c1st) (csb (cuni (cima (cfv (cv x0) cmvrs) (cun (cv x2) (csn (cv x3))))) (λ x4 . cxp (cv x4) (cv x4)))) (cv x2) (cv x3)))))) (proof)
Theorem df_msta : wceq cmsta (cmpt (λ x0 . cvv) (λ x0 . crn (cfv (cv x0) cmsr))) (proof)
Theorem df_mfs : wceq cmfs (cab (λ x0 . wa (wa (wceq (cin (cfv (cv x0) cmcn) (cfv (cv x0) cmvar)) c0) (wf (cfv (cv x0) cmvar) (cfv (cv x0) cmtc) (cfv (cv x0) cmty))) (wa (wss (cfv (cv x0) cmax) (cfv (cv x0) cmsta)) (wral (λ x1 . wn (wcel (cima (ccnv (cfv (cv x0) cmty)) (csn (cv x1))) cfn)) (λ x1 . cfv (cv x0) cmvt))))) (proof)
Theorem df_mcls : wceq cmcls (cmpt (λ x0 . cvv) (λ x0 . cmpt2 (λ x1 x2 . cpw (cfv (cv x0) cmdv)) (λ x1 x2 . cpw (cfv (cv x0) cmex)) (λ x1 x2 . cint (cab (λ x3 . wa (wss (cun (cv x2) (crn (cfv (cv x0) cmvh))) (cv x3)) (∀ x4 x5 x6 . wcel (cotp (cv x4) (cv x5) (cv x6)) (cfv (cv x0) cmax) ⟶ wral (λ x7 . wa (wss (cima (cv x7) (cun (cv x5) (crn (cfv (cv x0) cmvh)))) (cv x3)) (∀ x8 x9 . wbr (cv x8) (cv x9) (cv x4) ⟶ wss (cxp (cfv (cfv (cfv (cv x8) (cfv (cv x0) cmvh)) (cv x7)) (cfv (cv x0) cmvrs)) (cfv (cfv (cfv (cv x9) (cfv (cv x0) cmvh)) (cv x7)) (cfv (cv x0) cmvrs))) (cv x1)) ⟶ wcel (cfv (cv x6) (cv x7)) (cv x3)) (λ x7 . crn (cfv (cv x0) cmsub)))))))) (proof)
Theorem df_mpps : wceq cmpps (cmpt (λ x0 . cvv) (λ x0 . coprab (λ x1 x2 x3 . wa (wcel (cotp (cv x1) (cv x2) (cv x3)) (cfv (cv x0) cmpst)) (wcel (cv x3) (co (cv x1) (cv x2) (cfv (cv x0) cmcls)))))) (proof)
Theorem df_mthm : wceq cmthm (cmpt (λ x0 . cvv) (λ x0 . cima (ccnv (cfv (cv x0) cmsr)) (cima (cfv (cv x0) cmsr) (cfv (cv x0) cmpps)))) (proof)
Theorem df_m0s : wceq cm0s (cmpt (λ x0 . cvv) (λ x0 . cotp c0 c0 (cv x0))) (proof)
Theorem df_msa : wceq cmsa (cmpt (λ x0 . cvv) (λ x0 . crab (λ x1 . w3a (wcel (cfv (cv x1) cm0s) (cfv (cv x0) cmax)) (wcel (cfv (cv x1) c1st) (cfv (cv x0) cmvt)) (wfun (cres (ccnv (cfv (cv x1) c2nd)) (cfv (cv x0) cmvar)))) (λ x1 . cfv (cv x0) cmex))) (proof)
Theorem df_mwgfs : wceq cmwgfs (crab (λ x0 . ∀ x1 x2 x3 . wa (wcel (cotp (cv x1) (cv x2) (cv x3)) (cfv (cv x0) cmax)) (wcel (cfv (cv x3) c1st) (cfv (cv x0) cmvt)) ⟶ wrex (λ x4 . wcel (cv x3) (cima (cv x4) (cfv (cv x0) cmsa))) (λ x4 . crn (cfv (cv x0) cmsub))) (λ x0 . cmfs)) (proof)
Theorem df_msyn : wceq cmsy (cslot c6) (proof)
Theorem df_mtree : wceq cmtree (cmpt (λ x0 . cvv) (λ x0 . cmpt2 (λ x1 x2 . cpw (cfv (cv x0) cmdv)) (λ x1 x2 . cpw (cfv (cv x0) cmex)) (λ x1 x2 . cint (cab (λ x3 . w3a (wral (λ x4 . wbr (cv x4) (cop (cfv (cv x4) cm0s) c0) (cv x3)) (λ x4 . crn (cfv (cv x0) cmvh))) (wral (λ x4 . wbr (cv x4) (cop (cfv (cotp (cv x1) (cv x2) (cv x4)) (cfv (cv x0) cmsr)) c0) (cv x3)) (λ x4 . cv x2)) (∀ x4 x5 x6 . wcel (cotp (cv x4) (cv x5) (cv x6)) (cfv (cv x0) cmax) ⟶ wral (λ x7 . (∀ x8 x9 . wbr (cv x8) (cv x9) (cv x4) ⟶ wss (cxp (cfv (cfv (cfv (cv x8) (cfv (cv x0) cmvh)) (cv x7)) (cfv (cv x0) cmvrs)) (cfv (cfv (cfv (cv x9) (cfv (cv x0) cmvh)) (cv x7)) (cfv (cv x0) cmvrs))) (cv x1)) ⟶ wss (cxp (csn (cfv (cv x6) (cv x7))) (cixp (λ x8 . cun (cv x5) (cima (cfv (cv x0) cmvh) (cuni (cima (cfv (cv x0) cmvrs) (cun (cv x5) (csn (cv x6))))))) (λ x8 . cima (cv x3) (csn (cfv (cv x8) (cv x7)))))) (cv x3)) (λ x7 . crn (cfv (cv x0) cmsub)))))))) (proof)
Theorem df_mst : wceq cmst (cmpt (λ x0 . cvv) (λ x0 . cres (co c0 c0 (cfv (cv x0) cmtree)) (cres (cfv (cv x0) cmex) (cfv (cv x0) cmvt)))) (proof)
Theorem df_msax : wceq cmsax (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cfv (cv x0) cmsa) (λ x1 . cima (cfv (cv x0) cmvh) (cfv (cv x1) (cfv (cv x0) cmvrs))))) (proof)
Theorem df_mufs : wceq cmufs (crab (λ x0 . wfun (cfv (cv x0) cmst)) (λ x0 . cmgfs)) (proof)
Theorem df_muv : wceq cmuv (cslot c7) (proof)