Search for blocks/addresses/...

Proofgold Term Root Disambiguation

∀ 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
as obj
-
as prop
8c9f4..
theory
SetMM
stx
ebbdd..
address
TMFYX..