Proofgold Address

Known df_fallfac__df_bpoly__df_ef__df_e__df_sin__df_cos__df_tan__df_pi__df_dvds__df_bits__df_sad__df_smu__df_gcd__df_lcm__df_lcmf__df_prm__df_numer__df_denom : ∀ x0 : ο . (wceq cfallfac (cmpt2 (λ x1 x2 . cc) (λ x1 x2 . cn0) (λ x1 x2 . cprod (λ x3 . co cc0 (co (cv x2) c1 cmin) cfz) (λ x3 . co (cv x1) (cv x3) cmin))) ⟶ wceq cbp (cmpt2 (λ x1 x2 . cn0) (λ x1 x2 . cc) (λ x1 x2 . cfv (cv x1) (cwrecs cn0 clt (cmpt (λ x3 . cvv) (λ x3 . csb (cfv (cdm (cv x3)) chash) (λ x4 . co (co (cv x2) (cv x4) cexp) (csu (cdm (cv x3)) (λ x5 . co (co (cv x4) (cv x5) cbc) (co (cfv (cv x5) (cv x3)) (co (co (cv x4) (cv x5) cmin) c1 caddc) cdiv) cmul)) cmin)))))) ⟶ wceq ce (cmpt (λ x1 . cc) (λ x1 . csu cn0 (λ x2 . co (co (cv x1) (cv x2) cexp) (cfv (cv x2) cfa) cdiv))) ⟶ wceq ceu (cfv c1 ce) ⟶ wceq csin (cmpt (λ x1 . cc) (λ x1 . co (co (cfv (co ci (cv x1) cmul) ce) (cfv (co (cneg ci) (cv x1) cmul) ce) cmin) (co c2 ci cmul) cdiv)) ⟶ wceq ccos (cmpt (λ x1 . cc) (λ x1 . co (co (cfv (co ci (cv x1) cmul) ce) (cfv (co (cneg ci) (cv x1) cmul) ce) caddc) c2 cdiv)) ⟶ wceq ctan (cmpt (λ x1 . cima (ccnv ccos) (cdif cc (csn cc0))) (λ x1 . co (cfv (cv x1) csin) (cfv (cv x1) ccos) cdiv)) ⟶ wceq cpi (cinf (cin crp (cima (ccnv csin) (csn cc0))) cr clt) ⟶ wceq cdvds (copab (λ x1 x2 . wa (wa (wcel (cv x1) cz) (wcel (cv x2) cz)) (wrex (λ x3 . wceq (co (cv x3) (cv x1) cmul) (cv x2)) (λ x3 . cz)))) ⟶ wceq cbits (cmpt (λ x1 . cz) (λ x1 . crab (λ x2 . wn (wbr c2 (cfv (co (cv x1) (co c2 (cv x2) cexp) cdiv) cfl) cdvds)) (λ x2 . cn0))) ⟶ wceq csad (cmpt2 (λ x1 x2 . cpw cn0) (λ x1 x2 . cpw cn0) (λ x1 x2 . crab (λ x3 . whad (wcel (cv x3) (cv x1)) (wcel (cv x3) (cv x2)) (wcel c0 (cfv (cv x3) (cseq (cmpt2 (λ x4 x5 . c2o) (λ x4 x5 . cn0) (λ x4 x5 . cif (wcad (wcel (cv x5) (cv x1)) (wcel (cv x5) (cv x2)) (wcel c0 (cv x4))) c1o c0)) (cmpt (λ x4 . cn0) (λ x4 . cif (wceq (cv x4) cc0) c0 (co (cv x4) c1 cmin))) cc0)))) (λ x3 . cn0))) ⟶ wceq csmu (cmpt2 (λ x1 x2 . cpw cn0) (λ x1 x2 . cpw cn0) (λ x1 x2 . crab (λ x3 . wcel (cv x3) (cfv (co (cv x3) c1 caddc) (cseq (cmpt2 (λ x4 x5 . cpw cn0) (λ x4 x5 . cn0) (λ x4 x5 . co (cv x4) (crab (λ x6 . wa (wcel (cv x5) (cv x1)) (wcel (co (cv x6) (cv x5) cmin) (cv x2))) (λ x6 . cn0)) csad)) (cmpt (λ x4 . cn0) (λ x4 . cif (wceq (cv x4) cc0) c0 (co (cv x4) c1 cmin))) cc0))) (λ x3 . cn0))) ⟶ wceq cgcd (cmpt2 (λ x1 x2 . cz) (λ x1 x2 . cz) (λ x1 x2 . cif (wa (wceq (cv x1) cc0) (wceq (cv x2) cc0)) cc0 (csup (crab (λ x3 . wa (wbr (cv x3) (cv x1) cdvds) (wbr (cv x3) (cv x2) cdvds)) (λ x3 . cz)) cr clt))) ⟶ wceq clcm (cmpt2 (λ x1 x2 . cz) (λ x1 x2 . cz) (λ x1 x2 . cif (wo (wceq (cv x1) cc0) (wceq (cv x2) cc0)) cc0 (cinf (crab (λ x3 . wa (wbr (cv x1) (cv x3) cdvds) (wbr (cv x2) (cv x3) cdvds)) (λ x3 . cn)) cr clt))) ⟶ wceq clcmf (cmpt (λ x1 . cpw cz) (λ x1 . cif (wcel cc0 (cv x1)) cc0 (cinf (crab (λ x2 . wral (λ x3 . wbr (cv x3) (cv x2) cdvds) (λ x3 . cv x1)) (λ x2 . cn)) cr clt))) ⟶ wceq cprime (crab (λ x1 . wbr (crab (λ x2 . wbr (cv x2) (cv x1) cdvds) (λ x2 . cn)) c2o cen) (λ x1 . cn)) ⟶ wceq cnumer (cmpt (λ x1 . cq) (λ x1 . cfv (crio (λ x2 . wa (wceq (co (cfv (cv x2) c1st) (cfv (cv x2) c2nd) cgcd) c1) (wceq (cv x1) (co (cfv (cv x2) c1st) (cfv (cv x2) c2nd) cdiv))) (λ x2 . cxp cz cn)) c1st)) ⟶ wceq cdenom (cmpt (λ x1 . cq) (λ x1 . cfv (crio (λ x2 . wa (wceq (co (cfv (cv x2) c1st) (cfv (cv x2) c2nd) cgcd) c1) (wceq (cv x1) (co (cfv (cv x2) c1st) (cfv (cv x2) c2nd) cdiv))) (λ x2 . cxp cz cn)) c2nd)) ⟶ x0) ⟶ x0
Theorem df_fallfac : wceq cfallfac (cmpt2 (λ x0 x1 . cc) (λ x0 x1 . cn0) (λ x0 x1 . cprod (λ x2 . co cc0 (co (cv x1) c1 cmin) cfz) (λ x2 . co (cv x0) (cv x2) cmin))) (proof)
Theorem df_bpoly : wceq cbp (cmpt2 (λ x0 x1 . cn0) (λ x0 x1 . cc) (λ x0 x1 . cfv (cv x0) (cwrecs cn0 clt (cmpt (λ x2 . cvv) (λ x2 . csb (cfv (cdm (cv x2)) chash) (λ x3 . co (co (cv x1) (cv x3) cexp) (csu (cdm (cv x2)) (λ x4 . co (co (cv x3) (cv x4) cbc) (co (cfv (cv x4) (cv x2)) (co (co (cv x3) (cv x4) cmin) c1 caddc) cdiv) cmul)) cmin)))))) (proof)
Theorem df_ef : wceq ce (cmpt (λ x0 . cc) (λ x0 . csu cn0 (λ x1 . co (co (cv x0) (cv x1) cexp) (cfv (cv x1) cfa) cdiv))) (proof)
Theorem df_e : wceq ceu (cfv c1 ce) (proof)
Theorem df_sin : wceq csin (cmpt (λ x0 . cc) (λ x0 . co (co (cfv (co ci (cv x0) cmul) ce) (cfv (co (cneg ci) (cv x0) cmul) ce) cmin) (co c2 ci cmul) cdiv)) (proof)
Theorem df_cos : wceq ccos (cmpt (λ x0 . cc) (λ x0 . co (co (cfv (co ci (cv x0) cmul) ce) (cfv (co (cneg ci) (cv x0) cmul) ce) caddc) c2 cdiv)) (proof)
Theorem df_tan : wceq ctan (cmpt (λ x0 . cima (ccnv ccos) (cdif cc (csn cc0))) (λ x0 . co (cfv (cv x0) csin) (cfv (cv x0) ccos) cdiv)) (proof)
Theorem df_pi : wceq cpi (cinf (cin crp (cima (ccnv csin) (csn cc0))) cr clt) (proof)
Theorem df_dvds : wceq cdvds (copab (λ x0 x1 . wa (wa (wcel (cv x0) cz) (wcel (cv x1) cz)) (wrex (λ x2 . wceq (co (cv x2) (cv x0) cmul) (cv x1)) (λ x2 . cz)))) (proof)
Theorem df_bits : wceq cbits (cmpt (λ x0 . cz) (λ x0 . crab (λ x1 . wn (wbr c2 (cfv (co (cv x0) (co c2 (cv x1) cexp) cdiv) cfl) cdvds)) (λ x1 . cn0))) (proof)
Theorem df_sad : wceq csad (cmpt2 (λ x0 x1 . cpw cn0) (λ x0 x1 . cpw cn0) (λ x0 x1 . crab (λ x2 . whad (wcel (cv x2) (cv x0)) (wcel (cv x2) (cv x1)) (wcel c0 (cfv (cv x2) (cseq (cmpt2 (λ x3 x4 . c2o) (λ x3 x4 . cn0) (λ x3 x4 . cif (wcad (wcel (cv x4) (cv x0)) (wcel (cv x4) (cv x1)) (wcel c0 (cv x3))) c1o c0)) (cmpt (λ x3 . cn0) (λ x3 . cif (wceq (cv x3) cc0) c0 (co (cv x3) c1 cmin))) cc0)))) (λ x2 . cn0))) (proof)
Theorem df_smu : wceq csmu (cmpt2 (λ x0 x1 . cpw cn0) (λ x0 x1 . cpw cn0) (λ x0 x1 . crab (λ x2 . wcel (cv x2) (cfv (co (cv x2) c1 caddc) (cseq (cmpt2 (λ x3 x4 . cpw cn0) (λ x3 x4 . cn0) (λ x3 x4 . co (cv x3) (crab (λ x5 . wa (wcel (cv x4) (cv x0)) (wcel (co (cv x5) (cv x4) cmin) (cv x1))) (λ x5 . cn0)) csad)) (cmpt (λ x3 . cn0) (λ x3 . cif (wceq (cv x3) cc0) c0 (co (cv x3) c1 cmin))) cc0))) (λ x2 . cn0))) (proof)
Theorem df_gcd : wceq cgcd (cmpt2 (λ x0 x1 . cz) (λ x0 x1 . cz) (λ x0 x1 . cif (wa (wceq (cv x0) cc0) (wceq (cv x1) cc0)) cc0 (csup (crab (λ x2 . wa (wbr (cv x2) (cv x0) cdvds) (wbr (cv x2) (cv x1) cdvds)) (λ x2 . cz)) cr clt))) (proof)
Theorem df_lcm : wceq clcm (cmpt2 (λ x0 x1 . cz) (λ x0 x1 . cz) (λ x0 x1 . cif (wo (wceq (cv x0) cc0) (wceq (cv x1) cc0)) cc0 (cinf (crab (λ x2 . wa (wbr (cv x0) (cv x2) cdvds) (wbr (cv x1) (cv x2) cdvds)) (λ x2 . cn)) cr clt))) (proof)
Theorem df_lcmf : wceq clcmf (cmpt (λ x0 . cpw cz) (λ x0 . cif (wcel cc0 (cv x0)) cc0 (cinf (crab (λ x1 . wral (λ x2 . wbr (cv x2) (cv x1) cdvds) (λ x2 . cv x0)) (λ x1 . cn)) cr clt))) (proof)
Theorem df_prm : wceq cprime (crab (λ x0 . wbr (crab (λ x1 . wbr (cv x1) (cv x0) cdvds) (λ x1 . cn)) c2o cen) (λ x0 . cn)) (proof)
Theorem df_numer : wceq cnumer (cmpt (λ x0 . cq) (λ x0 . cfv (crio (λ x1 . wa (wceq (co (cfv (cv x1) c1st) (cfv (cv x1) c2nd) cgcd) c1) (wceq (cv x0) (co (cfv (cv x1) c1st) (cfv (cv x1) c2nd) cdiv))) (λ x1 . cxp cz cn)) c1st)) (proof)
Theorem df_denom : wceq cdenom (cmpt (λ x0 . cq) (λ x0 . cfv (crio (λ x1 . wa (wceq (co (cfv (cv x1) c1st) (cfv (cv x1) c2nd) cgcd) c1) (wceq (cv x0) (co (cfv (cv x1) c1st) (cfv (cv x1) c2nd) cdiv))) (λ x1 . cxp cz cn)) c2nd)) (proof)