Proofgold Address

Known ax_hfvadd__ax_hvcom__ax_hvass__ax_hv0cl__ax_hvaddid__ax_hfvmul__ax_hvmulid__ax_hvmulass__ax_hvdistr1__ax_hvdistr2__ax_hvmul0__ax_hfi__ax_his1__ax_his2__ax_his3__ax_his4__ax_hcompl__df_sh : ∀ x0 : ο . (wf (cxp chil chil) chil cva ⟶ (∀ x1 x2 : ι → ο . wa (wcel x1 chil) (wcel x2 chil) ⟶ wceq (co x1 x2 cva) (co x2 x1 cva)) ⟶ (∀ x1 x2 x3 : ι → ο . w3a (wcel x1 chil) (wcel x2 chil) (wcel x3 chil) ⟶ wceq (co (co x1 x2 cva) x3 cva) (co x1 (co x2 x3 cva) cva)) ⟶ wcel c0v chil ⟶ (∀ x1 : ι → ο . wcel x1 chil ⟶ wceq (co x1 c0v cva) x1) ⟶ wf (cxp cc chil) chil csm ⟶ (∀ x1 : ι → ο . wcel x1 chil ⟶ wceq (co c1 x1 csm) x1) ⟶ (∀ x1 x2 x3 : ι → ο . w3a (wcel x1 cc) (wcel x2 cc) (wcel x3 chil) ⟶ wceq (co (co x1 x2 cmul) x3 csm) (co x1 (co x2 x3 csm) csm)) ⟶ (∀ x1 x2 x3 : ι → ο . w3a (wcel x1 cc) (wcel x2 chil) (wcel x3 chil) ⟶ wceq (co x1 (co x2 x3 cva) csm) (co (co x1 x2 csm) (co x1 x3 csm) cva)) ⟶ (∀ x1 x2 x3 : ι → ο . w3a (wcel x1 cc) (wcel x2 cc) (wcel x3 chil) ⟶ wceq (co (co x1 x2 caddc) x3 csm) (co (co x1 x3 csm) (co x2 x3 csm) cva)) ⟶ (∀ x1 : ι → ο . wcel x1 chil ⟶ wceq (co cc0 x1 csm) c0v) ⟶ wf (cxp chil chil) cc csp ⟶ (∀ x1 x2 : ι → ο . wa (wcel x1 chil) (wcel x2 chil) ⟶ wceq (co x1 x2 csp) (cfv (co x2 x1 csp) ccj)) ⟶ (∀ x1 x2 x3 : ι → ο . w3a (wcel x1 chil) (wcel x2 chil) (wcel x3 chil) ⟶ wceq (co (co x1 x2 cva) x3 csp) (co (co x1 x3 csp) (co x2 x3 csp) caddc)) ⟶ (∀ x1 x2 x3 : ι → ο . w3a (wcel x1 cc) (wcel x2 chil) (wcel x3 chil) ⟶ wceq (co (co x1 x2 csm) x3 csp) (co x1 (co x2 x3 csp) cmul)) ⟶ (∀ x1 : ι → ο . wa (wcel x1 chil) (wne x1 c0v) ⟶ wbr cc0 (co x1 x1 csp) clt) ⟶ (∀ x1 : ι → ο . wcel x1 ccau ⟶ wrex (λ x2 . wbr x1 (cv x2) chli) (λ x2 . chil)) ⟶ wceq csh (crab (λ x1 . w3a (wcel c0v (cv x1)) (wss (cima cva (cxp (cv x1) (cv x1))) (cv x1)) (wss (cima csm (cxp cc (cv x1))) (cv x1))) (λ x1 . cpw chil)) ⟶ x0) ⟶ x0
Theorem ax_hfvadd : wf (cxp chil chil) chil cva (proof)
Theorem ax_hvcom : ∀ x0 x1 : ι → ο . wa (wcel x0 chil) (wcel x1 chil) ⟶ wceq (co x0 x1 cva) (co x1 x0 cva) (proof)
Theorem ax_hvass : ∀ x0 x1 x2 : ι → ο . w3a (wcel x0 chil) (wcel x1 chil) (wcel x2 chil) ⟶ wceq (co (co x0 x1 cva) x2 cva) (co x0 (co x1 x2 cva) cva) (proof)
Theorem ax_hv0cl : wcel c0v chil (proof)
Theorem ax_hvaddid : ∀ x0 : ι → ο . wcel x0 chil ⟶ wceq (co x0 c0v cva) x0 (proof)
Theorem ax_hfvmul : wf (cxp cc chil) chil csm (proof)
Theorem ax_hvmulid : ∀ x0 : ι → ο . wcel x0 chil ⟶ wceq (co c1 x0 csm) x0 (proof)
Theorem ax_hvmulass : ∀ x0 x1 x2 : ι → ο . w3a (wcel x0 cc) (wcel x1 cc) (wcel x2 chil) ⟶ wceq (co (co x0 x1 cmul) x2 csm) (co x0 (co x1 x2 csm) csm) (proof)
Theorem ax_hvdistr1 : ∀ x0 x1 x2 : ι → ο . w3a (wcel x0 cc) (wcel x1 chil) (wcel x2 chil) ⟶ wceq (co x0 (co x1 x2 cva) csm) (co (co x0 x1 csm) (co x0 x2 csm) cva) (proof)
Theorem ax_hvdistr2 : ∀ x0 x1 x2 : ι → ο . w3a (wcel x0 cc) (wcel x1 cc) (wcel x2 chil) ⟶ wceq (co (co x0 x1 caddc) x2 csm) (co (co x0 x2 csm) (co x1 x2 csm) cva) (proof)
Theorem ax_hvmul0 : ∀ x0 : ι → ο . wcel x0 chil ⟶ wceq (co cc0 x0 csm) c0v (proof)
Theorem ax_hfi : wf (cxp chil chil) cc csp (proof)
Theorem ax_his1 : ∀ x0 x1 : ι → ο . wa (wcel x0 chil) (wcel x1 chil) ⟶ wceq (co x0 x1 csp) (cfv (co x1 x0 csp) ccj) (proof)
Theorem ax_his2 : ∀ x0 x1 x2 : ι → ο . w3a (wcel x0 chil) (wcel x1 chil) (wcel x2 chil) ⟶ wceq (co (co x0 x1 cva) x2 csp) (co (co x0 x2 csp) (co x1 x2 csp) caddc) (proof)
Theorem ax_his3 : ∀ x0 x1 x2 : ι → ο . w3a (wcel x0 cc) (wcel x1 chil) (wcel x2 chil) ⟶ wceq (co (co x0 x1 csm) x2 csp) (co x0 (co x1 x2 csp) cmul) (proof)
Theorem ax_his4 : ∀ x0 : ι → ο . wa (wcel x0 chil) (wne x0 c0v) ⟶ wbr cc0 (co x0 x0 csp) clt (proof)
Theorem ax_hcompl : ∀ x0 : ι → ο . wcel x0 ccau ⟶ wrex (λ x1 . wbr x0 (cv x1) chli) (λ x1 . chil) (proof)
Theorem df_sh : wceq csh (crab (λ x0 . w3a (wcel c0v (cv x0)) (wss (cima cva (cxp (cv x0) (cv x0))) (cv x0)) (wss (cima csm (cxp cc (cv x0))) (cv x0))) (λ x0 . cpw chil)) (proof)