Proofgold Address

Known df_sub__df_neg__df_div__df_nn__df_2__df_3__df_4__df_5__df_6__df_7__df_8__df_9__df_10OLD__df_n0__df_xnn0__df_z__df_dec__df_uz : ∀ x0 : ο . (wceq cmin (cmpt2 (λ x1 x2 . cc) (λ x1 x2 . cc) (λ x1 x2 . crio (λ x3 . wceq (co (cv x2) (cv x3) caddc) (cv x1)) (λ x3 . cc))) ⟶ (∀ x1 : ι → ο . wceq (cneg x1) (co cc0 x1 cmin)) ⟶ wceq cdiv (cmpt2 (λ x1 x2 . cc) (λ x1 x2 . cdif cc (csn cc0)) (λ x1 x2 . crio (λ x3 . wceq (co (cv x2) (cv x3) cmul) (cv x1)) (λ x3 . cc))) ⟶ wceq cn (cima (crdg (cmpt (λ x1 . cvv) (λ x1 . co (cv x1) c1 caddc)) c1) com) ⟶ wceq c2 (co c1 c1 caddc) ⟶ wceq c3 (co c2 c1 caddc) ⟶ wceq c4 (co c3 c1 caddc) ⟶ wceq c5 (co c4 c1 caddc) ⟶ wceq c6 (co c5 c1 caddc) ⟶ wceq c7 (co c6 c1 caddc) ⟶ wceq c8 (co c7 c1 caddc) ⟶ wceq c9 (co c8 c1 caddc) ⟶ wceq c10 (co c9 c1 caddc) ⟶ wceq cn0 (cun cn (csn cc0)) ⟶ wceq cxnn0 (cun cn0 (csn cpnf)) ⟶ wceq cz (crab (λ x1 . w3o (wceq (cv x1) cc0) (wcel (cv x1) cn) (wcel (cneg (cv x1)) cn)) (λ x1 . cr)) ⟶ (∀ x1 x2 : ι → ο . wceq (cdc x1 x2) (co (co (co c9 c1 caddc) x1 cmul) x2 caddc)) ⟶ wceq cuz (cmpt (λ x1 . cz) (λ x1 . crab (λ x2 . wbr (cv x1) (cv x2) cle) (λ x2 . cz))) ⟶ x0) ⟶ x0
Theorem df_sub : wceq cmin (cmpt2 (λ x0 x1 . cc) (λ x0 x1 . cc) (λ x0 x1 . crio (λ x2 . wceq (co (cv x1) (cv x2) caddc) (cv x0)) (λ x2 . cc))) (proof)
Theorem df_neg : ∀ x0 : ι → ο . wceq (cneg x0) (co cc0 x0 cmin) (proof)
Theorem df_div : wceq cdiv (cmpt2 (λ x0 x1 . cc) (λ x0 x1 . cdif cc (csn cc0)) (λ x0 x1 . crio (λ x2 . wceq (co (cv x1) (cv x2) cmul) (cv x0)) (λ x2 . cc))) (proof)
Theorem df_nn : wceq cn (cima (crdg (cmpt (λ x0 . cvv) (λ x0 . co (cv x0) c1 caddc)) c1) com) (proof)
Theorem df_2 : wceq c2 (co c1 c1 caddc) (proof)
Theorem df_3 : wceq c3 (co c2 c1 caddc) (proof)
Theorem df_4 : wceq c4 (co c3 c1 caddc) (proof)
Theorem df_5 : wceq c5 (co c4 c1 caddc) (proof)
Theorem df_6 : wceq c6 (co c5 c1 caddc) (proof)
Theorem df_7 : wceq c7 (co c6 c1 caddc) (proof)
Theorem df_8 : wceq c8 (co c7 c1 caddc) (proof)
Theorem df_9 : wceq c9 (co c8 c1 caddc) (proof)
Theorem df_10OLD : wceq c10 (co c9 c1 caddc) (proof)
Theorem df_n0 : wceq cn0 (cun cn (csn cc0)) (proof)
Theorem df_xnn0 : wceq cxnn0 (cun cn0 (csn cpnf)) (proof)
Theorem df_z : wceq cz (crab (λ x0 . w3o (wceq (cv x0) cc0) (wcel (cv x0) cn) (wcel (cneg (cv x0)) cn)) (λ x0 . cr)) (proof)
Theorem df_dec : ∀ x0 x1 : ι → ο . wceq (cdc x0 x1) (co (co (co c9 c1 caddc) x0 cmul) x1 caddc) (proof)
Theorem df_uz : wceq cuz (cmpt (λ x0 . cz) (λ x0 . crab (λ x1 . wbr (cv x0) (cv x1) cle) (λ x1 . cz))) (proof)