Proofgold Address

Known df_dir__df_tail__df_plusf__df_mgm__df_sgrp__df_mnd__df_mhm__df_submnd__df_frmd__df_vrmd__df_grp__df_minusg__df_sbg__df_mulg__df_subg__df_nsg__df_eqg__df_ghm : ∀ x0 : ο . (wceq cdir (cab (λ x1 . wa (wa (wrel (cv x1)) (wss (cres cid (cuni (cuni (cv x1)))) (cv x1))) (wa (wss (ccom (cv x1) (cv x1)) (cv x1)) (wss (cxp (cuni (cuni (cv x1))) (cuni (cuni (cv x1)))) (ccom (ccnv (cv x1)) (cv x1)))))) ⟶ wceq ctail (cmpt (λ x1 . cdir) (λ x1 . cmpt (λ x2 . cuni (cuni (cv x1))) (λ x2 . cima (cv x1) (csn (cv x2))))) ⟶ wceq cplusf (cmpt (λ x1 . cvv) (λ x1 . cmpt2 (λ x2 x3 . cfv (cv x1) cbs) (λ x2 x3 . cfv (cv x1) cbs) (λ x2 x3 . co (cv x2) (cv x3) (cfv (cv x1) cplusg)))) ⟶ wceq cmgm (cab (λ x1 . wsbc (λ x2 . wsbc (λ x3 . wral (λ x4 . wral (λ x5 . wcel (co (cv x4) (cv x5) (cv x3)) (cv x2)) (λ x5 . cv x2)) (λ x4 . cv x2)) (cfv (cv x1) cplusg)) (cfv (cv x1) cbs))) ⟶ wceq csgrp (crab (λ x1 . wsbc (λ x2 . wsbc (λ x3 . wral (λ x4 . wral (λ x5 . wral (λ x6 . wceq (co (co (cv x4) (cv x5) (cv x3)) (cv x6) (cv x3)) (co (cv x4) (co (cv x5) (cv x6) (cv x3)) (cv x3))) (λ x6 . cv x2)) (λ x5 . cv x2)) (λ x4 . cv x2)) (cfv (cv x1) cplusg)) (cfv (cv x1) cbs)) (λ x1 . cmgm)) ⟶ wceq cmnd (crab (λ x1 . wsbc (λ x2 . wsbc (λ x3 . wrex (λ x4 . wral (λ x5 . wa (wceq (co (cv x4) (cv x5) (cv x3)) (cv x5)) (wceq (co (cv x5) (cv x4) (cv x3)) (cv x5))) (λ x5 . cv x2)) (λ x4 . cv x2)) (cfv (cv x1) cplusg)) (cfv (cv x1) cbs)) (λ x1 . csgrp)) ⟶ wceq cmhm (cmpt2 (λ x1 x2 . cmnd) (λ x1 x2 . cmnd) (λ x1 x2 . crab (λ x3 . wa (wral (λ x4 . wral (λ x5 . wceq (cfv (co (cv x4) (cv x5) (cfv (cv x1) cplusg)) (cv x3)) (co (cfv (cv x4) (cv x3)) (cfv (cv x5) (cv x3)) (cfv (cv x2) cplusg))) (λ x5 . cfv (cv x1) cbs)) (λ x4 . cfv (cv x1) cbs)) (wceq (cfv (cfv (cv x1) c0g) (cv x3)) (cfv (cv x2) c0g))) (λ x3 . co (cfv (cv x2) cbs) (cfv (cv x1) cbs) cmap))) ⟶ wceq csubmnd (cmpt (λ x1 . cmnd) (λ x1 . crab (λ x2 . wa (wcel (cfv (cv x1) c0g) (cv x2)) (wral (λ x3 . wral (λ x4 . wcel (co (cv x3) (cv x4) (cfv (cv x1) cplusg)) (cv x2)) (λ x4 . cv x2)) (λ x3 . cv x2))) (λ x2 . cpw (cfv (cv x1) cbs)))) ⟶ wceq cfrmd (cmpt (λ x1 . cvv) (λ x1 . cpr (cop (cfv cnx cbs) (cword (cv x1))) (cop (cfv cnx cplusg) (cres cconcat (cxp (cword (cv x1)) (cword (cv x1))))))) ⟶ wceq cvrmd (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cv x1) (λ x2 . cs1 (cv x2)))) ⟶ wceq cgrp (crab (λ x1 . wral (λ x2 . wrex (λ x3 . wceq (co (cv x3) (cv x2) (cfv (cv x1) cplusg)) (cfv (cv x1) c0g)) (λ x3 . cfv (cv x1) cbs)) (λ x2 . cfv (cv x1) cbs)) (λ x1 . cmnd)) ⟶ wceq cminusg (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cfv (cv x1) cbs) (λ x2 . crio (λ x3 . wceq (co (cv x3) (cv x2) (cfv (cv x1) cplusg)) (cfv (cv x1) c0g)) (λ x3 . cfv (cv x1) cbs)))) ⟶ wceq csg (cmpt (λ x1 . cvv) (λ x1 . cmpt2 (λ x2 x3 . cfv (cv x1) cbs) (λ x2 x3 . cfv (cv x1) cbs) (λ x2 x3 . co (cv x2) (cfv (cv x3) (cfv (cv x1) cminusg)) (cfv (cv x1) cplusg)))) ⟶ wceq cmg (cmpt (λ x1 . cvv) (λ x1 . cmpt2 (λ x2 x3 . cz) (λ x2 x3 . cfv (cv x1) cbs) (λ x2 x3 . cif (wceq (cv x2) cc0) (cfv (cv x1) c0g) (csb (cseq (cfv (cv x1) cplusg) (cxp cn (csn (cv x3))) c1) (λ x4 . cif (wbr cc0 (cv x2) clt) (cfv (cv x2) (cv x4)) (cfv (cfv (cneg (cv x2)) (cv x4)) (cfv (cv x1) cminusg))))))) ⟶ wceq csubg (cmpt (λ x1 . cgrp) (λ x1 . crab (λ x2 . wcel (co (cv x1) (cv x2) cress) cgrp) (λ x2 . cpw (cfv (cv x1) cbs)))) ⟶ wceq cnsg (cmpt (λ x1 . cgrp) (λ x1 . crab (λ x2 . wsbc (λ x3 . wsbc (λ x4 . wral (λ x5 . wral (λ x6 . wb (wcel (co (cv x5) (cv x6) (cv x4)) (cv x2)) (wcel (co (cv x6) (cv x5) (cv x4)) (cv x2))) (λ x6 . cv x3)) (λ x5 . cv x3)) (cfv (cv x1) cplusg)) (cfv (cv x1) cbs)) (λ x2 . cfv (cv x1) csubg))) ⟶ wceq cqg (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . copab (λ x3 x4 . wa (wss (cpr (cv x3) (cv x4)) (cfv (cv x1) cbs)) (wcel (co (cfv (cv x3) (cfv (cv x1) cminusg)) (cv x4) (cfv (cv x1) cplusg)) (cv x2))))) ⟶ wceq cghm (cmpt2 (λ x1 x2 . cgrp) (λ x1 x2 . cgrp) (λ x1 x2 . cab (λ x3 . wsbc (λ x4 . wa (wf (cv x4) (cfv (cv x2) cbs) (cv x3)) (wral (λ x5 . wral (λ x6 . wceq (cfv (co (cv x5) (cv x6) (cfv (cv x1) cplusg)) (cv x3)) (co (cfv (cv x5) (cv x3)) (cfv (cv x6) (cv x3)) (cfv (cv x2) cplusg))) (λ x6 . cv x4)) (λ x5 . cv x4))) (cfv (cv x1) cbs)))) ⟶ x0) ⟶ x0
Theorem df_dir : wceq cdir (cab (λ x0 . wa (wa (wrel (cv x0)) (wss (cres cid (cuni (cuni (cv x0)))) (cv x0))) (wa (wss (ccom (cv x0) (cv x0)) (cv x0)) (wss (cxp (cuni (cuni (cv x0))) (cuni (cuni (cv x0)))) (ccom (ccnv (cv x0)) (cv x0)))))) (proof)
Theorem df_tail : wceq ctail (cmpt (λ x0 . cdir) (λ x0 . cmpt (λ x1 . cuni (cuni (cv x0))) (λ x1 . cima (cv x0) (csn (cv x1))))) (proof)
Theorem df_plusf : wceq cplusf (cmpt (λ x0 . cvv) (λ x0 . cmpt2 (λ x1 x2 . cfv (cv x0) cbs) (λ x1 x2 . cfv (cv x0) cbs) (λ x1 x2 . co (cv x1) (cv x2) (cfv (cv x0) cplusg)))) (proof)
Theorem df_mgm : wceq cmgm (cab (λ x0 . wsbc (λ x1 . wsbc (λ x2 . wral (λ x3 . wral (λ x4 . wcel (co (cv x3) (cv x4) (cv x2)) (cv x1)) (λ x4 . cv x1)) (λ x3 . cv x1)) (cfv (cv x0) cplusg)) (cfv (cv x0) cbs))) (proof)
Theorem df_sgrp : wceq csgrp (crab (λ x0 . wsbc (λ x1 . wsbc (λ x2 . wral (λ x3 . wral (λ x4 . wral (λ x5 . wceq (co (co (cv x3) (cv x4) (cv x2)) (cv x5) (cv x2)) (co (cv x3) (co (cv x4) (cv x5) (cv x2)) (cv x2))) (λ x5 . cv x1)) (λ x4 . cv x1)) (λ x3 . cv x1)) (cfv (cv x0) cplusg)) (cfv (cv x0) cbs)) (λ x0 . cmgm)) (proof)
Theorem df_mnd : wceq cmnd (crab (λ x0 . wsbc (λ x1 . wsbc (λ x2 . wrex (λ x3 . wral (λ x4 . wa (wceq (co (cv x3) (cv x4) (cv x2)) (cv x4)) (wceq (co (cv x4) (cv x3) (cv x2)) (cv x4))) (λ x4 . cv x1)) (λ x3 . cv x1)) (cfv (cv x0) cplusg)) (cfv (cv x0) cbs)) (λ x0 . csgrp)) (proof)
Theorem df_mhm : wceq cmhm (cmpt2 (λ x0 x1 . cmnd) (λ x0 x1 . cmnd) (λ x0 x1 . crab (λ x2 . wa (wral (λ x3 . wral (λ x4 . wceq (cfv (co (cv x3) (cv x4) (cfv (cv x0) cplusg)) (cv x2)) (co (cfv (cv x3) (cv x2)) (cfv (cv x4) (cv x2)) (cfv (cv x1) cplusg))) (λ x4 . cfv (cv x0) cbs)) (λ x3 . cfv (cv x0) cbs)) (wceq (cfv (cfv (cv x0) c0g) (cv x2)) (cfv (cv x1) c0g))) (λ x2 . co (cfv (cv x1) cbs) (cfv (cv x0) cbs) cmap))) (proof)
Theorem df_submnd : wceq csubmnd (cmpt (λ x0 . cmnd) (λ x0 . crab (λ x1 . wa (wcel (cfv (cv x0) c0g) (cv x1)) (wral (λ x2 . wral (λ x3 . wcel (co (cv x2) (cv x3) (cfv (cv x0) cplusg)) (cv x1)) (λ x3 . cv x1)) (λ x2 . cv x1))) (λ x1 . cpw (cfv (cv x0) cbs)))) (proof)
Theorem df_frmd : wceq cfrmd (cmpt (λ x0 . cvv) (λ x0 . cpr (cop (cfv cnx cbs) (cword (cv x0))) (cop (cfv cnx cplusg) (cres cconcat (cxp (cword (cv x0)) (cword (cv x0))))))) (proof)
Theorem df_vrmd : wceq cvrmd (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cv x0) (λ x1 . cs1 (cv x1)))) (proof)
Theorem df_grp : wceq cgrp (crab (λ x0 . wral (λ x1 . wrex (λ x2 . wceq (co (cv x2) (cv x1) (cfv (cv x0) cplusg)) (cfv (cv x0) c0g)) (λ x2 . cfv (cv x0) cbs)) (λ x1 . cfv (cv x0) cbs)) (λ x0 . cmnd)) (proof)
Theorem df_minusg : wceq cminusg (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cfv (cv x0) cbs) (λ x1 . crio (λ x2 . wceq (co (cv x2) (cv x1) (cfv (cv x0) cplusg)) (cfv (cv x0) c0g)) (λ x2 . cfv (cv x0) cbs)))) (proof)
Theorem df_sbg : wceq csg (cmpt (λ x0 . cvv) (λ x0 . cmpt2 (λ x1 x2 . cfv (cv x0) cbs) (λ x1 x2 . cfv (cv x0) cbs) (λ x1 x2 . co (cv x1) (cfv (cv x2) (cfv (cv x0) cminusg)) (cfv (cv x0) cplusg)))) (proof)
Theorem df_mulg : wceq cmg (cmpt (λ x0 . cvv) (λ x0 . cmpt2 (λ x1 x2 . cz) (λ x1 x2 . cfv (cv x0) cbs) (λ x1 x2 . cif (wceq (cv x1) cc0) (cfv (cv x0) c0g) (csb (cseq (cfv (cv x0) cplusg) (cxp cn (csn (cv x2))) c1) (λ x3 . cif (wbr cc0 (cv x1) clt) (cfv (cv x1) (cv x3)) (cfv (cfv (cneg (cv x1)) (cv x3)) (cfv (cv x0) cminusg))))))) (proof)
Theorem df_subg : wceq csubg (cmpt (λ x0 . cgrp) (λ x0 . crab (λ x1 . wcel (co (cv x0) (cv x1) cress) cgrp) (λ x1 . cpw (cfv (cv x0) cbs)))) (proof)
Theorem df_nsg : wceq cnsg (cmpt (λ x0 . cgrp) (λ x0 . crab (λ x1 . wsbc (λ x2 . wsbc (λ x3 . wral (λ x4 . wral (λ x5 . wb (wcel (co (cv x4) (cv x5) (cv x3)) (cv x1)) (wcel (co (cv x5) (cv x4) (cv x3)) (cv x1))) (λ x5 . cv x2)) (λ x4 . cv x2)) (cfv (cv x0) cplusg)) (cfv (cv x0) cbs)) (λ x1 . cfv (cv x0) csubg))) (proof)
Theorem df_eqg : wceq cqg (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . copab (λ x2 x3 . wa (wss (cpr (cv x2) (cv x3)) (cfv (cv x0) cbs)) (wcel (co (cfv (cv x2) (cfv (cv x0) cminusg)) (cv x3) (cfv (cv x0) cplusg)) (cv x1))))) (proof)
Theorem df_ghm : wceq cghm (cmpt2 (λ x0 x1 . cgrp) (λ x0 x1 . cgrp) (λ x0 x1 . cab (λ x2 . wsbc (λ x3 . wa (wf (cv x3) (cfv (cv x1) cbs) (cv x2)) (wral (λ x4 . wral (λ x5 . wceq (cfv (co (cv x4) (cv x5) (cfv (cv x0) cplusg)) (cv x2)) (co (cfv (cv x4) (cv x2)) (cfv (cv x5) (cv x2)) (cfv (cv x1) cplusg))) (λ x5 . cv x3)) (λ x4 . cv x3))) (cfv (cv x0) cbs)))) (proof)