Proofgold Asset

Known df_md__df_dmd__df_at__df_dp2__df_dp__df_xdiv__ax_xrssca__ax_xrsvsca__df_omnd__df_ogrp__df_sgns__df_inftm__df_archi__df_slmd__df_orng__df_ofld__df_resv__df_smat : ∀ x0 : ο . (wceq cmd (copab (λ x1 x2 . wa (wa (wcel (cv x1) cch) (wcel (cv x2) cch)) (wral (λ x3 . wss (cv x3) (cv x2) ⟶ wceq (cin (co (cv x3) (cv x1) chj) (cv x2)) (co (cv x3) (cin (cv x1) (cv x2)) chj)) (λ x3 . cch)))) ⟶ wceq cdmd (copab (λ x1 x2 . wa (wa (wcel (cv x1) cch) (wcel (cv x2) cch)) (wral (λ x3 . wss (cv x2) (cv x3) ⟶ wceq (co (cin (cv x3) (cv x1)) (cv x2) chj) (cin (cv x3) (co (cv x1) (cv x2) chj))) (λ x3 . cch)))) ⟶ wceq cat (crab (λ x1 . wbr c0h (cv x1) ccv) (λ x1 . cch)) ⟶ (∀ x1 x2 : ι → ο . wceq (cdp2 x1 x2) (co x1 (co x2 (cdc c1 cc0) cdiv) caddc)) ⟶ wceq cdp (cmpt2 (λ x1 x2 . cn0) (λ x1 x2 . cr) (λ x1 x2 . cdp2 (cv x1) (cv x2))) ⟶ wceq cxdiv (cmpt2 (λ x1 x2 . cxr) (λ x1 x2 . cdif cr (csn cc0)) (λ x1 x2 . crio (λ x3 . wceq (co (cv x2) (cv x3) cxmu) (cv x1)) (λ x3 . cxr))) ⟶ wceq crefld (cfv cxrs csca) ⟶ wceq cxmu (cfv cxrs cvsca) ⟶ wceq comnd (crab (λ x1 . wsbc (λ x2 . wsbc (λ x3 . wsbc (λ x4 . wa (wcel (cv x1) ctos) (wral (λ x5 . wral (λ x6 . wral (λ x7 . wbr (cv x5) (cv x6) (cv x4) ⟶ wbr (co (cv x5) (cv x7) (cv x3)) (co (cv x6) (cv x7) (cv x3)) (cv x4)) (λ x7 . cv x2)) (λ x6 . cv x2)) (λ x5 . cv x2))) (cfv (cv x1) cple)) (cfv (cv x1) cplusg)) (cfv (cv x1) cbs)) (λ x1 . cmnd)) ⟶ wceq cogrp (cin cgrp comnd) ⟶ wceq csgns (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cfv (cv x1) cbs) (λ x2 . cif (wceq (cv x2) (cfv (cv x1) c0g)) cc0 (cif (wbr (cfv (cv x1) c0g) (cv x2) (cfv (cv x1) cplt)) c1 (cneg c1))))) ⟶ wceq cinftm (cmpt (λ x1 . cvv) (λ x1 . copab (λ x2 x3 . wa (wa (wcel (cv x2) (cfv (cv x1) cbs)) (wcel (cv x3) (cfv (cv x1) cbs))) (wa (wbr (cfv (cv x1) c0g) (cv x2) (cfv (cv x1) cplt)) (wral (λ x4 . wbr (co (cv x4) (cv x2) (cfv (cv x1) cmg)) (cv x3) (cfv (cv x1) cplt)) (λ x4 . cn)))))) ⟶ wceq carchi (cab (λ x1 . wceq (cfv (cv x1) cinftm) c0)) ⟶ wceq cslmd (crab (λ x1 . wsbc (λ x2 . wsbc (λ x3 . wsbc (λ x4 . wsbc (λ x5 . wsbc (λ x6 . wsbc (λ x7 . wsbc (λ x8 . wa (wcel (cv x5) csrg) (wral (λ x9 . wral (λ x10 . wral (λ x11 . wral (λ x12 . wa (w3a (wcel (co (cv x10) (cv x12) (cv x4)) (cv x2)) (wceq (co (cv x10) (co (cv x12) (cv x11) (cv x3)) (cv x4)) (co (co (cv x10) (cv x12) (cv x4)) (co (cv x10) (cv x11) (cv x4)) (cv x3))) (wceq (co (co (cv x9) (cv x10) (cv x7)) (cv x12) (cv x4)) (co (co (cv x9) (cv x12) (cv x4)) (co (cv x10) (cv x12) (cv x4)) (cv x3)))) (w3a (wceq (co (co (cv x9) (cv x10) (cv x8)) (cv x12) (cv x4)) (co (cv x9) (co (cv x10) (cv x12) (cv x4)) (cv x4))) (wceq (co (cfv (cv x5) cur) (cv x12) (cv x4)) (cv x12)) (wceq (co (cfv (cv x5) c0g) (cv x12) (cv x4)) (cfv (cv x1) c0g)))) (λ x12 . cv x2)) (λ x11 . cv x2)) (λ x10 . cv x6)) (λ x9 . cv x6))) (cfv (cv x5) cmulr)) (cfv (cv x5) cplusg)) (cfv (cv x5) cbs)) (cfv (cv x1) csca)) (cfv (cv x1) cvsca)) (cfv (cv x1) cplusg)) (cfv (cv x1) cbs)) (λ x1 . ccmn)) ⟶ wceq corng (crab (λ x1 . wsbc (λ x2 . wsbc (λ x3 . wsbc (λ x4 . wsbc (λ x5 . wral (λ x6 . wral (λ x7 . wa (wbr (cv x3) (cv x6) (cv x5)) (wbr (cv x3) (cv x7) (cv x5)) ⟶ wbr (cv x3) (co (cv x6) (cv x7) (cv x4)) (cv x5)) (λ x7 . cv x2)) (λ x6 . cv x2)) (cfv (cv x1) cple)) (cfv (cv x1) cmulr)) (cfv (cv x1) c0g)) (cfv (cv x1) cbs)) (λ x1 . cin crg cogrp)) ⟶ wceq cofld (cin cfield corng) ⟶ wceq cresv (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . cif (wss (cfv (cfv (cv x1) csca) cbs) (cv x2)) (cv x1) (co (cv x1) (cop (cfv cnx csca) (co (cfv (cv x1) csca) (cv x2) cress)) csts))) ⟶ wceq csmat (cmpt (λ x1 . cvv) (λ x1 . cmpt2 (λ x2 x3 . cn) (λ x2 x3 . cn) (λ x2 x3 . ccom (cv x1) (cmpt2 (λ x4 x5 . cn) (λ x4 x5 . cn) (λ x4 x5 . cop (cif (wbr (cv x4) (cv x2) clt) (cv x4) (co (cv x4) c1 caddc)) (cif (wbr (cv x5) (cv x3) clt) (cv x5) (co (cv x5) c1 caddc))))))) ⟶ x0) ⟶ x0
Theorem df_md : wceq cmd (copab (λ x0 x1 . wa (wa (wcel (cv x0) cch) (wcel (cv x1) cch)) (wral (λ x2 . wss (cv x2) (cv x1) ⟶ wceq (cin (co (cv x2) (cv x0) chj) (cv x1)) (co (cv x2) (cin (cv x0) (cv x1)) chj)) (λ x2 . cch)))) (proof)
Theorem df_dmd : wceq cdmd (copab (λ x0 x1 . wa (wa (wcel (cv x0) cch) (wcel (cv x1) cch)) (wral (λ x2 . wss (cv x1) (cv x2) ⟶ wceq (co (cin (cv x2) (cv x0)) (cv x1) chj) (cin (cv x2) (co (cv x0) (cv x1) chj))) (λ x2 . cch)))) (proof)
Theorem df_at : wceq cat (crab (λ x0 . wbr c0h (cv x0) ccv) (λ x0 . cch)) (proof)
Theorem df_dp2 : ∀ x0 x1 : ι → ο . wceq (cdp2 x0 x1) (co x0 (co x1 (cdc c1 cc0) cdiv) caddc) (proof)
Theorem df_dp : wceq cdp (cmpt2 (λ x0 x1 . cn0) (λ x0 x1 . cr) (λ x0 x1 . cdp2 (cv x0) (cv x1))) (proof)
Theorem df_xdiv : wceq cxdiv (cmpt2 (λ x0 x1 . cxr) (λ x0 x1 . cdif cr (csn cc0)) (λ x0 x1 . crio (λ x2 . wceq (co (cv x1) (cv x2) cxmu) (cv x0)) (λ x2 . cxr))) (proof)
Theorem ax_xrssca : wceq crefld (cfv cxrs csca) (proof)
Theorem ax_xrsvsca : wceq cxmu (cfv cxrs cvsca) (proof)
Theorem df_omnd : wceq comnd (crab (λ x0 . wsbc (λ x1 . wsbc (λ x2 . wsbc (λ x3 . wa (wcel (cv x0) ctos) (wral (λ x4 . wral (λ x5 . wral (λ x6 . wbr (cv x4) (cv x5) (cv x3) ⟶ wbr (co (cv x4) (cv x6) (cv x2)) (co (cv x5) (cv x6) (cv x2)) (cv x3)) (λ x6 . cv x1)) (λ x5 . cv x1)) (λ x4 . cv x1))) (cfv (cv x0) cple)) (cfv (cv x0) cplusg)) (cfv (cv x0) cbs)) (λ x0 . cmnd)) (proof)
Theorem df_ogrp : wceq cogrp (cin cgrp comnd) (proof)
Theorem df_sgns : wceq csgns (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cfv (cv x0) cbs) (λ x1 . cif (wceq (cv x1) (cfv (cv x0) c0g)) cc0 (cif (wbr (cfv (cv x0) c0g) (cv x1) (cfv (cv x0) cplt)) c1 (cneg c1))))) (proof)
Theorem df_inftm : wceq cinftm (cmpt (λ x0 . cvv) (λ x0 . copab (λ x1 x2 . wa (wa (wcel (cv x1) (cfv (cv x0) cbs)) (wcel (cv x2) (cfv (cv x0) cbs))) (wa (wbr (cfv (cv x0) c0g) (cv x1) (cfv (cv x0) cplt)) (wral (λ x3 . wbr (co (cv x3) (cv x1) (cfv (cv x0) cmg)) (cv x2) (cfv (cv x0) cplt)) (λ x3 . cn)))))) (proof)
Theorem df_archi : wceq carchi (cab (λ x0 . wceq (cfv (cv x0) cinftm) c0)) (proof)
Theorem df_slmd : wceq cslmd (crab (λ x0 . wsbc (λ x1 . wsbc (λ x2 . wsbc (λ x3 . wsbc (λ x4 . wsbc (λ x5 . wsbc (λ x6 . wsbc (λ x7 . wa (wcel (cv x4) csrg) (wral (λ x8 . wral (λ x9 . wral (λ x10 . wral (λ x11 . wa (w3a (wcel (co (cv x9) (cv x11) (cv x3)) (cv x1)) (wceq (co (cv x9) (co (cv x11) (cv x10) (cv x2)) (cv x3)) (co (co (cv x9) (cv x11) (cv x3)) (co (cv x9) (cv x10) (cv x3)) (cv x2))) (wceq (co (co (cv x8) (cv x9) (cv x6)) (cv x11) (cv x3)) (co (co (cv x8) (cv x11) (cv x3)) (co (cv x9) (cv x11) (cv x3)) (cv x2)))) (w3a (wceq (co (co (cv x8) (cv x9) (cv x7)) (cv x11) (cv x3)) (co (cv x8) (co (cv x9) (cv x11) (cv x3)) (cv x3))) (wceq (co (cfv (cv x4) cur) (cv x11) (cv x3)) (cv x11)) (wceq (co (cfv (cv x4) c0g) (cv x11) (cv x3)) (cfv (cv x0) c0g)))) (λ x11 . cv x1)) (λ x10 . cv x1)) (λ x9 . cv x5)) (λ x8 . cv x5))) (cfv (cv x4) cmulr)) (cfv (cv x4) cplusg)) (cfv (cv x4) cbs)) (cfv (cv x0) csca)) (cfv (cv x0) cvsca)) (cfv (cv x0) cplusg)) (cfv (cv x0) cbs)) (λ x0 . ccmn)) (proof)
Theorem df_orng : wceq corng (crab (λ x0 . wsbc (λ x1 . wsbc (λ x2 . wsbc (λ x3 . wsbc (λ x4 . wral (λ x5 . wral (λ x6 . wa (wbr (cv x2) (cv x5) (cv x4)) (wbr (cv x2) (cv x6) (cv x4)) ⟶ wbr (cv x2) (co (cv x5) (cv x6) (cv x3)) (cv x4)) (λ x6 . cv x1)) (λ x5 . cv x1)) (cfv (cv x0) cple)) (cfv (cv x0) cmulr)) (cfv (cv x0) c0g)) (cfv (cv x0) cbs)) (λ x0 . cin crg cogrp)) (proof)
Theorem df_ofld : wceq cofld (cin cfield corng) (proof)
Theorem df_resv : wceq cresv (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . cif (wss (cfv (cfv (cv x0) csca) cbs) (cv x1)) (cv x0) (co (cv x0) (cop (cfv cnx csca) (co (cfv (cv x0) csca) (cv x1) cress)) csts))) (proof)
Theorem df_smat : wceq csmat (cmpt (λ x0 . cvv) (λ x0 . cmpt2 (λ x1 x2 . cn) (λ x1 x2 . cn) (λ x1 x2 . ccom (cv x0) (cmpt2 (λ x3 x4 . cn) (λ x3 x4 . cn) (λ x3 x4 . cop (cif (wbr (cv x3) (cv x1) clt) (cv x3) (co (cv x3) c1 caddc)) (cif (wbr (cv x4) (cv x2) clt) (cv x4) (co (cv x4) c1 caddc))))))) (proof)