Proofgold Address

Known df_ppi__df_mu__df_sgm__df_dchr__df_lgs__df_itv__df_lng__df_trkgc__df_trkgb__df_trkgcb__df_trkge__df_trkgld__df_trkg__df_cgrg__df_ismt__df_leg__df_hlg__df_mir : ∀ x0 : ο . (wceq cppi (cmpt (λ x1 . cr) (λ x1 . cfv (cin (co cc0 (cv x1) cicc) cprime) chash)) ⟶ wceq cmu (cmpt (λ x1 . cn) (λ x1 . cif (wrex (λ x2 . wbr (co (cv x2) c2 cexp) (cv x1) cdvds) (λ x2 . cprime)) cc0 (co (cneg c1) (cfv (crab (λ x2 . wbr (cv x2) (cv x1) cdvds) (λ x2 . cprime)) chash) cexp))) ⟶ wceq csgm (cmpt2 (λ x1 x2 . cc) (λ x1 x2 . cn) (λ x1 x2 . csu (crab (λ x3 . wbr (cv x3) (cv x2) cdvds) (λ x3 . cn)) (λ x3 . co (cv x3) (cv x1) ccxp))) ⟶ wceq cdchr (cmpt (λ x1 . cn) (λ x1 . csb (cfv (cv x1) czn) (λ x2 . csb (crab (λ x3 . wss (cxp (cdif (cfv (cv x2) cbs) (cfv (cv x2) cui)) (csn cc0)) (cv x3)) (λ x3 . co (cfv (cv x2) cmgp) (cfv ccnfld cmgp) cmhm)) (λ x3 . cpr (cop (cfv cnx cbs) (cv x3)) (cop (cfv cnx cplusg) (cres (cof cmul) (cxp (cv x3) (cv x3)))))))) ⟶ wceq clgs (cmpt2 (λ x1 x2 . cz) (λ x1 x2 . cz) (λ x1 x2 . cif (wceq (cv x2) cc0) (cif (wceq (co (cv x1) c2 cexp) c1) c1 cc0) (co (cif (wa (wbr (cv x2) cc0 clt) (wbr (cv x1) cc0 clt)) (cneg c1) c1) (cfv (cfv (cv x2) cabs) (cseq cmul (cmpt (λ x3 . cn) (λ x3 . cif (wcel (cv x3) cprime) (co (cif (wceq (cv x3) c2) (cif (wbr c2 (cv x1) cdvds) cc0 (cif (wcel (co (cv x1) c8 cmo) (cpr c1 c7)) c1 (cneg c1))) (co (co (co (co (cv x1) (co (co (cv x3) c1 cmin) c2 cdiv) cexp) c1 caddc) (cv x3) cmo) c1 cmin)) (co (cv x3) (cv x2) cpc) cexp) c1)) c1)) cmul))) ⟶ wceq citv (cslot (cdc c1 c6)) ⟶ wceq clng (cslot (cdc c1 c7)) ⟶ wceq cstrkgc (cab (λ x1 . wsbc (λ x2 . wsbc (λ x3 . wa (wral (λ x4 . wral (λ x5 . wceq (co (cv x4) (cv x5) (cv x3)) (co (cv x5) (cv x4) (cv x3))) (λ x5 . cv x2)) (λ x4 . cv x2)) (wral (λ x4 . wral (λ x5 . wral (λ x6 . wceq (co (cv x4) (cv x5) (cv x3)) (co (cv x6) (cv x6) (cv x3)) ⟶ wceq (cv x4) (cv x5)) (λ x6 . cv x2)) (λ x5 . cv x2)) (λ x4 . cv x2))) (cfv (cv x1) cds)) (cfv (cv x1) cbs))) ⟶ wceq cstrkgb (cab (λ x1 . wsbc (λ x2 . wsbc (λ x3 . w3a (wral (λ x4 . wral (λ x5 . wcel (cv x5) (co (cv x4) (cv x4) (cv x3)) ⟶ wceq (cv x4) (cv x5)) (λ x5 . cv x2)) (λ x4 . cv x2)) (wral (λ x4 . wral (λ x5 . wral (λ x6 . wral (λ x7 . wral (λ x8 . wa (wcel (cv x7) (co (cv x4) (cv x6) (cv x3))) (wcel (cv x8) (co (cv x5) (cv x6) (cv x3))) ⟶ wrex (λ x9 . wa (wcel (cv x9) (co (cv x7) (cv x5) (cv x3))) (wcel (cv x9) (co (cv x8) (cv x4) (cv x3)))) (λ x9 . cv x2)) (λ x8 . cv x2)) (λ x7 . cv x2)) (λ x6 . cv x2)) (λ x5 . cv x2)) (λ x4 . cv x2)) (wral (λ x4 . wral (λ x5 . wrex (λ x6 . wral (λ x7 . wral (λ x8 . wcel (cv x7) (co (cv x6) (cv x8) (cv x3))) (λ x8 . cv x5)) (λ x7 . cv x4)) (λ x6 . cv x2) ⟶ wrex (λ x6 . wral (λ x7 . wral (λ x8 . wcel (cv x6) (co (cv x7) (cv x8) (cv x3))) (λ x8 . cv x5)) (λ x7 . cv x4)) (λ x6 . cv x2)) (λ x5 . cpw (cv x2))) (λ x4 . cpw (cv x2)))) (cfv (cv x1) citv)) (cfv (cv x1) cbs))) ⟶ wceq cstrkgcb (cab (λ x1 . wsbc (λ x2 . wsbc (λ x3 . wsbc (λ x4 . wa (wral (λ x5 . wral (λ x6 . wral (λ x7 . wral (λ x8 . wral (λ x9 . wral (λ x10 . wral (λ x11 . wral (λ x12 . wa (w3a (wne (cv x5) (cv x6)) (wcel (cv x6) (co (cv x5) (cv x7) (cv x4))) (wcel (cv x10) (co (cv x9) (cv x11) (cv x4)))) (wa (wa (wceq (co (cv x5) (cv x6) (cv x3)) (co (cv x9) (cv x10) (cv x3))) (wceq (co (cv x6) (cv x7) (cv x3)) (co (cv x10) (cv x11) (cv x3)))) (wa (wceq (co (cv x5) (cv x8) (cv x3)) (co (cv x9) (cv x12) (cv x3))) (wceq (co (cv x6) (cv x8) (cv x3)) (co (cv x10) (cv x12) (cv x3))))) ⟶ wceq (co (cv x7) (cv x8) (cv x3)) (co (cv x11) (cv x12) (cv x3))) (λ x12 . cv x2)) (λ x11 . cv x2)) (λ x10 . cv x2)) (λ x9 . cv x2)) (λ x8 . cv x2)) (λ x7 . cv x2)) (λ x6 . cv x2)) (λ x5 . cv x2)) (wral (λ x5 . wral (λ x6 . wral (λ x7 . wral (λ x8 . wrex (λ x9 . wa (wcel (cv x6) (co (cv x5) (cv x9) (cv x4))) (wceq (co (cv x6) (cv x9) (cv x3)) (co (cv x7) (cv x8) (cv x3)))) (λ x9 . cv x2)) (λ x8 . cv x2)) (λ x7 . cv x2)) (λ x6 . cv x2)) (λ x5 . cv x2))) (cfv (cv x1) citv)) (cfv (cv x1) cds)) (cfv (cv x1) cbs))) ⟶ wceq cstrkge (cab (λ x1 . wsbc (λ x2 . wsbc (λ x3 . wral (λ x4 . wral (λ x5 . wral (λ x6 . wral (λ x7 . wral (λ x8 . w3a (wcel (cv x7) (co (cv x4) (cv x8) (cv x3))) (wcel (cv x7) (co (cv x5) (cv x6) (cv x3))) (wne (cv x4) (cv x7)) ⟶ wrex (λ x9 . wrex (λ x10 . w3a (wcel (cv x5) (co (cv x4) (cv x9) (cv x3))) (wcel (cv x6) (co (cv x4) (cv x10) (cv x3))) (wcel (cv x8) (co (cv x9) (cv x10) (cv x3)))) (λ x10 . cv x2)) (λ x9 . cv x2)) (λ x8 . cv x2)) (λ x7 . cv x2)) (λ x6 . cv x2)) (λ x5 . cv x2)) (λ x4 . cv x2)) (cfv (cv x1) citv)) (cfv (cv x1) cbs))) ⟶ wceq cstrkgld (copab (λ x1 x2 . wsbc (λ x3 . wsbc (λ x4 . wsbc (λ x5 . wex (λ x6 . wa (wf1 (co c1 (cv x2) cfzo) (cv x3) (cv x6)) (wrex (λ x7 . wrex (λ x8 . wrex (λ x9 . wa (wral (λ x10 . w3a (wceq (co (cfv c1 (cv x6)) (cv x7) (cv x4)) (co (cfv (cv x10) (cv x6)) (cv x7) (cv x4))) (wceq (co (cfv c1 (cv x6)) (cv x8) (cv x4)) (co (cfv (cv x10) (cv x6)) (cv x8) (cv x4))) (wceq (co (cfv c1 (cv x6)) (cv x9) (cv x4)) (co (cfv (cv x10) (cv x6)) (cv x9) (cv x4)))) (λ x10 . co c2 (cv x2) cfzo)) (wn (w3o (wcel (cv x9) (co (cv x7) (cv x8) (cv x5))) (wcel (cv x7) (co (cv x9) (cv x8) (cv x5))) (wcel (cv x8) (co (cv x7) (cv x9) (cv x5)))))) (λ x9 . cv x3)) (λ x8 . cv x3)) (λ x7 . cv x3)))) (cfv (cv x1) citv)) (cfv (cv x1) cds)) (cfv (cv x1) cbs))) ⟶ wceq cstrkg (cin (cin cstrkgc cstrkgb) (cin cstrkgcb (cab (λ x1 . wsbc (λ x2 . wsbc (λ x3 . wceq (cfv (cv x1) clng) (cmpt2 (λ x4 x5 . cv x2) (λ x4 x5 . cdif (cv x2) (csn (cv x4))) (λ x4 x5 . crab (λ x6 . w3o (wcel (cv x6) (co (cv x4) (cv x5) (cv x3))) (wcel (cv x4) (co (cv x6) (cv x5) (cv x3))) (wcel (cv x5) (co (cv x4) (cv x6) (cv x3)))) (λ x6 . cv x2)))) (cfv (cv x1) citv)) (cfv (cv x1) cbs))))) ⟶ wceq ccgrg (cmpt (λ x1 . cvv) (λ x1 . copab (λ x2 x3 . wa (wa (wcel (cv x2) (co (cfv (cv x1) cbs) cr cpm)) (wcel (cv x3) (co (cfv (cv x1) cbs) cr cpm))) (wa (wceq (cdm (cv x2)) (cdm (cv x3))) (wral (λ x4 . wral (λ x5 . wceq (co (cfv (cv x4) (cv x2)) (cfv (cv x5) (cv x2)) (cfv (cv x1) cds)) (co (cfv (cv x4) (cv x3)) (cfv (cv x5) (cv x3)) (cfv (cv x1) cds))) (λ x5 . cdm (cv x2))) (λ x4 . cdm (cv x2))))))) ⟶ wceq cismt (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . cab (λ x3 . wa (wf1o (cfv (cv x1) cbs) (cfv (cv x2) cbs) (cv x3)) (wral (λ x4 . wral (λ x5 . wceq (co (cfv (cv x4) (cv x3)) (cfv (cv x5) (cv x3)) (cfv (cv x2) cds)) (co (cv x4) (cv x5) (cfv (cv x1) cds))) (λ x5 . cfv (cv x1) cbs)) (λ x4 . cfv (cv x1) cbs))))) ⟶ wceq cleg (cmpt (λ x1 . cvv) (λ x1 . copab (λ x2 x3 . wsbc (λ x4 . wsbc (λ x5 . wsbc (λ x6 . wrex (λ x7 . wrex (λ x8 . wa (wceq (cv x3) (co (cv x7) (cv x8) (cv x5))) (wrex (λ x9 . wa (wcel (cv x9) (co (cv x7) (cv x8) (cv x6))) (wceq (cv x2) (co (cv x7) (cv x9) (cv x5)))) (λ x9 . cv x4))) (λ x8 . cv x4)) (λ x7 . cv x4)) (cfv (cv x1) citv)) (cfv (cv x1) cds)) (cfv (cv x1) cbs)))) ⟶ wceq chlg (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cfv (cv x1) cbs) (λ x2 . copab (λ x3 x4 . wa (wa (wcel (cv x3) (cfv (cv x1) cbs)) (wcel (cv x4) (cfv (cv x1) cbs))) (w3a (wne (cv x3) (cv x2)) (wne (cv x4) (cv x2)) (wo (wcel (cv x3) (co (cv x2) (cv x4) (cfv (cv x1) citv))) (wcel (cv x4) (co (cv x2) (cv x3) (cfv (cv x1) citv))))))))) ⟶ wceq cmir (cmpt (λ x1 . cvv) (λ x1 . cmpt (λ x2 . cfv (cv x1) cbs) (λ x2 . cmpt (λ x3 . cfv (cv x1) cbs) (λ x3 . crio (λ x4 . wa (wceq (co (cv x2) (cv x4) (cfv (cv x1) cds)) (co (cv x2) (cv x3) (cfv (cv x1) cds))) (wcel (cv x2) (co (cv x4) (cv x3) (cfv (cv x1) citv)))) (λ x4 . cfv (cv x1) cbs))))) ⟶ x0) ⟶ x0
Theorem df_ppi : wceq cppi (cmpt (λ x0 . cr) (λ x0 . cfv (cin (co cc0 (cv x0) cicc) cprime) chash)) (proof)
Theorem df_mu : wceq cmu (cmpt (λ x0 . cn) (λ x0 . cif (wrex (λ x1 . wbr (co (cv x1) c2 cexp) (cv x0) cdvds) (λ x1 . cprime)) cc0 (co (cneg c1) (cfv (crab (λ x1 . wbr (cv x1) (cv x0) cdvds) (λ x1 . cprime)) chash) cexp))) (proof)
Theorem df_sgm : wceq csgm (cmpt2 (λ x0 x1 . cc) (λ x0 x1 . cn) (λ x0 x1 . csu (crab (λ x2 . wbr (cv x2) (cv x1) cdvds) (λ x2 . cn)) (λ x2 . co (cv x2) (cv x0) ccxp))) (proof)
Theorem df_dchr : wceq cdchr (cmpt (λ x0 . cn) (λ x0 . csb (cfv (cv x0) czn) (λ x1 . csb (crab (λ x2 . wss (cxp (cdif (cfv (cv x1) cbs) (cfv (cv x1) cui)) (csn cc0)) (cv x2)) (λ x2 . co (cfv (cv x1) cmgp) (cfv ccnfld cmgp) cmhm)) (λ x2 . cpr (cop (cfv cnx cbs) (cv x2)) (cop (cfv cnx cplusg) (cres (cof cmul) (cxp (cv x2) (cv x2)))))))) (proof)
Theorem df_lgs : wceq clgs (cmpt2 (λ x0 x1 . cz) (λ x0 x1 . cz) (λ x0 x1 . cif (wceq (cv x1) cc0) (cif (wceq (co (cv x0) c2 cexp) c1) c1 cc0) (co (cif (wa (wbr (cv x1) cc0 clt) (wbr (cv x0) cc0 clt)) (cneg c1) c1) (cfv (cfv (cv x1) cabs) (cseq cmul (cmpt (λ x2 . cn) (λ x2 . cif (wcel (cv x2) cprime) (co (cif (wceq (cv x2) c2) (cif (wbr c2 (cv x0) cdvds) cc0 (cif (wcel (co (cv x0) c8 cmo) (cpr c1 c7)) c1 (cneg c1))) (co (co (co (co (cv x0) (co (co (cv x2) c1 cmin) c2 cdiv) cexp) c1 caddc) (cv x2) cmo) c1 cmin)) (co (cv x2) (cv x1) cpc) cexp) c1)) c1)) cmul))) (proof)
Theorem df_itv : wceq citv (cslot (cdc c1 c6)) (proof)
Theorem df_lng : wceq clng (cslot (cdc c1 c7)) (proof)
Theorem df_trkgc : wceq cstrkgc (cab (λ x0 . wsbc (λ x1 . wsbc (λ x2 . wa (wral (λ x3 . wral (λ x4 . wceq (co (cv x3) (cv x4) (cv x2)) (co (cv x4) (cv x3) (cv x2))) (λ x4 . cv x1)) (λ x3 . cv x1)) (wral (λ x3 . wral (λ x4 . wral (λ x5 . wceq (co (cv x3) (cv x4) (cv x2)) (co (cv x5) (cv x5) (cv x2)) ⟶ wceq (cv x3) (cv x4)) (λ x5 . cv x1)) (λ x4 . cv x1)) (λ x3 . cv x1))) (cfv (cv x0) cds)) (cfv (cv x0) cbs))) (proof)
Theorem df_trkgb : wceq cstrkgb (cab (λ x0 . wsbc (λ x1 . wsbc (λ x2 . w3a (wral (λ x3 . wral (λ x4 . wcel (cv x4) (co (cv x3) (cv x3) (cv x2)) ⟶ wceq (cv x3) (cv x4)) (λ x4 . cv x1)) (λ x3 . cv x1)) (wral (λ x3 . wral (λ x4 . wral (λ x5 . wral (λ x6 . wral (λ x7 . wa (wcel (cv x6) (co (cv x3) (cv x5) (cv x2))) (wcel (cv x7) (co (cv x4) (cv x5) (cv x2))) ⟶ wrex (λ x8 . wa (wcel (cv x8) (co (cv x6) (cv x4) (cv x2))) (wcel (cv x8) (co (cv x7) (cv x3) (cv x2)))) (λ x8 . cv x1)) (λ x7 . cv x1)) (λ x6 . cv x1)) (λ x5 . cv x1)) (λ x4 . cv x1)) (λ x3 . cv x1)) (wral (λ x3 . wral (λ x4 . wrex (λ x5 . wral (λ x6 . wral (λ x7 . wcel (cv x6) (co (cv x5) (cv x7) (cv x2))) (λ x7 . cv x4)) (λ x6 . cv x3)) (λ x5 . cv x1) ⟶ wrex (λ x5 . wral (λ x6 . wral (λ x7 . wcel (cv x5) (co (cv x6) (cv x7) (cv x2))) (λ x7 . cv x4)) (λ x6 . cv x3)) (λ x5 . cv x1)) (λ x4 . cpw (cv x1))) (λ x3 . cpw (cv x1)))) (cfv (cv x0) citv)) (cfv (cv x0) cbs))) (proof)
Theorem df_trkgcb : wceq cstrkgcb (cab (λ x0 . wsbc (λ x1 . wsbc (λ x2 . wsbc (λ x3 . wa (wral (λ x4 . wral (λ x5 . wral (λ x6 . wral (λ x7 . wral (λ x8 . wral (λ x9 . wral (λ x10 . wral (λ x11 . wa (w3a (wne (cv x4) (cv x5)) (wcel (cv x5) (co (cv x4) (cv x6) (cv x3))) (wcel (cv x9) (co (cv x8) (cv x10) (cv x3)))) (wa (wa (wceq (co (cv x4) (cv x5) (cv x2)) (co (cv x8) (cv x9) (cv x2))) (wceq (co (cv x5) (cv x6) (cv x2)) (co (cv x9) (cv x10) (cv x2)))) (wa (wceq (co (cv x4) (cv x7) (cv x2)) (co (cv x8) (cv x11) (cv x2))) (wceq (co (cv x5) (cv x7) (cv x2)) (co (cv x9) (cv x11) (cv x2))))) ⟶ wceq (co (cv x6) (cv x7) (cv x2)) (co (cv x10) (cv x11) (cv x2))) (λ x11 . cv x1)) (λ x10 . cv x1)) (λ x9 . cv x1)) (λ x8 . cv x1)) (λ x7 . cv x1)) (λ x6 . cv x1)) (λ x5 . cv x1)) (λ x4 . cv x1)) (wral (λ x4 . wral (λ x5 . wral (λ x6 . wral (λ x7 . wrex (λ x8 . wa (wcel (cv x5) (co (cv x4) (cv x8) (cv x3))) (wceq (co (cv x5) (cv x8) (cv x2)) (co (cv x6) (cv x7) (cv x2)))) (λ x8 . cv x1)) (λ x7 . cv x1)) (λ x6 . cv x1)) (λ x5 . cv x1)) (λ x4 . cv x1))) (cfv (cv x0) citv)) (cfv (cv x0) cds)) (cfv (cv x0) cbs))) (proof)
Theorem df_trkge : wceq cstrkge (cab (λ x0 . wsbc (λ x1 . wsbc (λ x2 . wral (λ x3 . wral (λ x4 . wral (λ x5 . wral (λ x6 . wral (λ x7 . w3a (wcel (cv x6) (co (cv x3) (cv x7) (cv x2))) (wcel (cv x6) (co (cv x4) (cv x5) (cv x2))) (wne (cv x3) (cv x6)) ⟶ wrex (λ x8 . wrex (λ x9 . w3a (wcel (cv x4) (co (cv x3) (cv x8) (cv x2))) (wcel (cv x5) (co (cv x3) (cv x9) (cv x2))) (wcel (cv x7) (co (cv x8) (cv x9) (cv x2)))) (λ x9 . cv x1)) (λ x8 . cv x1)) (λ x7 . cv x1)) (λ x6 . cv x1)) (λ x5 . cv x1)) (λ x4 . cv x1)) (λ x3 . cv x1)) (cfv (cv x0) citv)) (cfv (cv x0) cbs))) (proof)
Theorem df_trkgld : wceq cstrkgld (copab (λ x0 x1 . wsbc (λ x2 . wsbc (λ x3 . wsbc (λ x4 . wex (λ x5 . wa (wf1 (co c1 (cv x1) cfzo) (cv x2) (cv x5)) (wrex (λ x6 . wrex (λ x7 . wrex (λ x8 . wa (wral (λ x9 . w3a (wceq (co (cfv c1 (cv x5)) (cv x6) (cv x3)) (co (cfv (cv x9) (cv x5)) (cv x6) (cv x3))) (wceq (co (cfv c1 (cv x5)) (cv x7) (cv x3)) (co (cfv (cv x9) (cv x5)) (cv x7) (cv x3))) (wceq (co (cfv c1 (cv x5)) (cv x8) (cv x3)) (co (cfv (cv x9) (cv x5)) (cv x8) (cv x3)))) (λ x9 . co c2 (cv x1) cfzo)) (wn (w3o (wcel (cv x8) (co (cv x6) (cv x7) (cv x4))) (wcel (cv x6) (co (cv x8) (cv x7) (cv x4))) (wcel (cv x7) (co (cv x6) (cv x8) (cv x4)))))) (λ x8 . cv x2)) (λ x7 . cv x2)) (λ x6 . cv x2)))) (cfv (cv x0) citv)) (cfv (cv x0) cds)) (cfv (cv x0) cbs))) (proof)
Theorem df_trkg : wceq cstrkg (cin (cin cstrkgc cstrkgb) (cin cstrkgcb (cab (λ x0 . wsbc (λ x1 . wsbc (λ x2 . wceq (cfv (cv x0) clng) (cmpt2 (λ x3 x4 . cv x1) (λ x3 x4 . cdif (cv x1) (csn (cv x3))) (λ x3 x4 . crab (λ x5 . w3o (wcel (cv x5) (co (cv x3) (cv x4) (cv x2))) (wcel (cv x3) (co (cv x5) (cv x4) (cv x2))) (wcel (cv x4) (co (cv x3) (cv x5) (cv x2)))) (λ x5 . cv x1)))) (cfv (cv x0) citv)) (cfv (cv x0) cbs))))) (proof)
Theorem df_cgrg : wceq ccgrg (cmpt (λ x0 . cvv) (λ x0 . copab (λ x1 x2 . wa (wa (wcel (cv x1) (co (cfv (cv x0) cbs) cr cpm)) (wcel (cv x2) (co (cfv (cv x0) cbs) cr cpm))) (wa (wceq (cdm (cv x1)) (cdm (cv x2))) (wral (λ x3 . wral (λ x4 . wceq (co (cfv (cv x3) (cv x1)) (cfv (cv x4) (cv x1)) (cfv (cv x0) cds)) (co (cfv (cv x3) (cv x2)) (cfv (cv x4) (cv x2)) (cfv (cv x0) cds))) (λ x4 . cdm (cv x1))) (λ x3 . cdm (cv x1))))))) (proof)
Theorem df_ismt : wceq cismt (cmpt2 (λ x0 x1 . cvv) (λ x0 x1 . cvv) (λ x0 x1 . cab (λ x2 . wa (wf1o (cfv (cv x0) cbs) (cfv (cv x1) cbs) (cv x2)) (wral (λ x3 . wral (λ x4 . wceq (co (cfv (cv x3) (cv x2)) (cfv (cv x4) (cv x2)) (cfv (cv x1) cds)) (co (cv x3) (cv x4) (cfv (cv x0) cds))) (λ x4 . cfv (cv x0) cbs)) (λ x3 . cfv (cv x0) cbs))))) (proof)
Theorem df_leg : wceq cleg (cmpt (λ x0 . cvv) (λ x0 . copab (λ x1 x2 . wsbc (λ x3 . wsbc (λ x4 . wsbc (λ x5 . wrex (λ x6 . wrex (λ x7 . wa (wceq (cv x2) (co (cv x6) (cv x7) (cv x4))) (wrex (λ x8 . wa (wcel (cv x8) (co (cv x6) (cv x7) (cv x5))) (wceq (cv x1) (co (cv x6) (cv x8) (cv x4)))) (λ x8 . cv x3))) (λ x7 . cv x3)) (λ x6 . cv x3)) (cfv (cv x0) citv)) (cfv (cv x0) cds)) (cfv (cv x0) cbs)))) (proof)
Theorem df_hlg : wceq chlg (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cfv (cv x0) cbs) (λ x1 . copab (λ x2 x3 . wa (wa (wcel (cv x2) (cfv (cv x0) cbs)) (wcel (cv x3) (cfv (cv x0) cbs))) (w3a (wne (cv x2) (cv x1)) (wne (cv x3) (cv x1)) (wo (wcel (cv x2) (co (cv x1) (cv x3) (cfv (cv x0) citv))) (wcel (cv x3) (co (cv x1) (cv x2) (cfv (cv x0) citv))))))))) (proof)
Theorem df_mir : wceq cmir (cmpt (λ x0 . cvv) (λ x0 . cmpt (λ x1 . cfv (cv x0) cbs) (λ x1 . cmpt (λ x2 . cfv (cv x0) cbs) (λ x2 . crio (λ x3 . wa (wceq (co (cv x1) (cv x3) (cfv (cv x0) cds)) (co (cv x1) (cv x2) (cfv (cv x0) cds))) (wcel (cv x1) (co (cv x3) (cv x2) (cfv (cv x0) citv)))) (λ x3 . cfv (cv x0) cbs))))) (proof)