Search for blocks/addresses/...

Proofgold Term Root Disambiguation

∀ x0 : ο . (wceq cordt (cmpt (λ x1 . cvv) (λ x1 . cfv (cfv (cun (csn (cdm (cv x1))) (crn (cun (cmpt (λ x2 . cdm (cv x1)) (λ x2 . crab (λ x3 . wn (wbr (cv x3) (cv x2) (cv x1))) (λ x3 . cdm (cv x1)))) (cmpt (λ x2 . cdm (cv x1)) (λ x2 . crab (λ x3 . wn (wbr (cv x2) (cv x3) (cv x1))) (λ x3 . cdm (cv x1))))))) cfi) ctg))wceq cxrs (cun (ctp (cop (cfv cnx cbs) cxr) (cop (cfv cnx cplusg) cxad) (cop (cfv cnx cmulr) cxmu)) (ctp (cop (cfv cnx cts) (cfv cle cordt)) (cop (cfv cnx cple) cle) (cop (cfv cnx cds) (cmpt2 (λ x1 x2 . cxr) (λ x1 x2 . cxr) (λ x1 x2 . cif (wbr (cv x1) (cv x2) cle) (co (cv x2) (cxne (cv x1)) cxad) (co (cv x1) (cxne (cv x2)) cxad))))))wceq cqtop (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . crab (λ x3 . wcel (cin (cima (ccnv (cv x2)) (cv x3)) (cuni (cv x1))) (cv x1)) (λ x3 . cpw (cima (cv x2) (cuni (cv x1))))))wceq cimas (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . csb (cfv (cv x2) cbs) (λ x3 . cun (cun (ctp (cop (cfv cnx cbs) (crn (cv x1))) (cop (cfv cnx cplusg) (ciun (λ x4 . cv x3) (λ x4 . ciun (λ x5 . cv x3) (λ x5 . csn (cop (cop (cfv (cv x4) (cv x1)) (cfv (cv x5) (cv x1))) (cfv (co (cv x4) (cv x5) (cfv (cv x2) cplusg)) (cv x1))))))) (cop (cfv cnx cmulr) (ciun (λ x4 . cv x3) (λ x4 . ciun (λ x5 . cv x3) (λ x5 . csn (cop (cop (cfv (cv x4) (cv x1)) (cfv (cv x5) (cv x1))) (cfv (co (cv x4) (cv x5) (cfv (cv x2) cmulr)) (cv x1)))))))) (ctp (cop (cfv cnx csca) (cfv (cv x2) csca)) (cop (cfv cnx cvsca) (ciun (λ x4 . cv x3) (λ x4 . cmpt2 (λ x5 x6 . cfv (cfv (cv x2) csca) cbs) (λ x5 x6 . csn (cfv (cv x4) (cv x1))) (λ x5 x6 . cfv (co (cv x5) (cv x4) (cfv (cv x2) cvsca)) (cv x1))))) (cop (cfv cnx cip) (ciun (λ x4 . cv x3) (λ x4 . ciun (λ x5 . cv x3) (λ x5 . csn (cop (cop (cfv (cv x4) (cv x1)) (cfv (cv x5) (cv x1))) (co (cv x4) (cv x5) (cfv (cv x2) cip))))))))) (ctp (cop (cfv cnx cts) (co (cfv (cv x2) ctopn) (cv x1) cqtop)) (cop (cfv cnx cple) (ccom (ccom (cv x1) (cfv (cv x2) cple)) (ccnv (cv x1)))) (cop (cfv cnx cds) (cmpt2 (λ x4 x5 . crn (cv x1)) (λ x4 x5 . crn (cv x1)) (λ x4 x5 . cinf (ciun (λ x6 . cn) (λ x6 . crn (cmpt (λ x7 . crab (λ x8 . w3a (wceq (cfv (cfv (cfv c1 (cv x8)) c1st) (cv x1)) (cv x4)) (wceq (cfv (cfv (cfv (cv x6) (cv x8)) c2nd) (cv x1)) (cv x5)) (wral (λ x9 . wceq (cfv (cfv (cfv (cv x9) (cv x8)) c2nd) (cv x1)) (cfv (cfv (cfv (co (cv x9) c1 caddc) (cv x8)) c1st) (cv x1))) (λ x9 . co c1 (co (cv x6) c1 cmin) cfz))) (λ x8 . co (cxp (cv x3) (cv x3)) (co c1 (cv x6) cfz) cmap)) (λ x7 . co cxrs (ccom (cfv (cv x2) cds) (cv x7)) cgsu)))) cxr clt)))))))wceq cqus (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . co (cmpt (λ x3 . cfv (cv x1) cbs) (λ x3 . cec (cv x3) (cv x2))) (cv x1) cimas))wceq cxps (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . co (ccnv (cmpt2 (λ x3 x4 . cfv (cv x1) cbs) (λ x3 x4 . cfv (cv x2) cbs) (λ x3 x4 . ccnv (co (csn (cv x3)) (csn (cv x4)) ccda)))) (co (cfv (cv x1) csca) (ccnv (co (csn (cv x1)) (csn (cv x2)) ccda)) cprds) cimas))wceq cmre (cmpt (λ x1 . cvv) (λ x1 . crab (λ x2 . wa (wcel (cv x1) (cv x2)) (wral (λ x3 . wne (cv x3) c0wcel (cint (cv x3)) (cv x2)) (λ x3 . cpw (cv x2)))) (λ x2 . cpw (cpw (cv x1)))))wceq cmrc (cmpt (λ x1 . cuni (crn cmre)) (λ x1 . cmpt (λ x2 . cpw (cuni (cv x1))) (λ x2 . cint (crab (λ x3 . wss (cv x2) (cv x3)) (λ x3 . cv x1)))))wceq cmri (cmpt (λ x1 . cuni (crn cmre)) (λ x1 . crab (λ x2 . wral (λ x3 . wn (wcel (cv x3) (cfv (cdif (cv x2) (csn (cv x3))) (cfv (cv x1) cmrc)))) (λ x3 . cv x2)) (λ x2 . cpw (cuni (cv x1)))))wceq cacs (cmpt (λ x1 . cvv) (λ x1 . crab (λ x2 . wex (λ x3 . wa (wf (cpw (cv x1)) (cpw (cv x1)) (cv x3)) (wral (λ x4 . wb (wcel (cv x4) (cv x2)) (wss (cuni (cima (cv x3) (cin (cpw (cv x4)) cfn))) (cv x4))) (λ x4 . cpw (cv x1))))) (λ x2 . cfv (cv x1) cmre)))wceq ccat (cab (λ x1 . wsbc (λ x2 . wsbc (λ x3 . wsbc (λ x4 . wral (λ x5 . wa (wrex (λ x6 . wral (λ x7 . wa (wral (λ x8 . wceq (co (cv x6) (cv x8) (co (cop (cv x7) (cv x5)) (cv x5) (cv x4))) (cv x8)) (λ x8 . co (cv x7) (cv x5) (cv x3))) (wral (λ x8 . wceq (co (cv x8) (cv x6) (co (cop (cv x5) (cv x5)) (cv x7) (cv x4))) (cv x8)) (λ x8 . co (cv x5) (cv x7) (cv x3)))) (λ x7 . cv x2)) (λ x6 . co (cv x5) (cv x5) (cv x3))) (wral (λ x6 . wral (λ x7 . wral (λ x8 . wral (λ x9 . wa (wcel (co (cv x9) (cv x8) (co (cop (cv x5) (cv x6)) (cv x7) (cv x4))) (co (cv x5) (cv x7) (cv x3))) (wral (λ x10 . wral (λ x11 . wceq (co (co (cv x11) (cv x9) (co (cop (cv x6) (cv x7)) (cv x10) (cv x4))) (cv x8) (co (cop (cv x5) (cv x6)) (cv x10) (cv x4))) (co (cv x11) (co (cv x9) (cv x8) (co (cop (cv x5) (cv x6)) (cv x7) (cv x4))) (co (cop (cv x5) (cv x7)) (cv x10) (cv x4)))) (λ x11 . co (cv x7) (cv x10) (cv x3))) (λ x10 . cv x2))) (λ x9 . co (cv x6) (cv x7) (cv x3))) (λ x8 . co (cv x5) (cv x6) (cv x3))) (λ x7 . cv x2)) (λ x6 . cv x2))) (λ x5 . cv x2)) (cfv (cv x1) cco)) (cfv (cv x1) chom)) (cfv (cv x1) cbs)))wceq ccid (cmpt (λ x1 . ccat) (λ x1 . csb (cfv (cv x1) cbs) (λ x2 . csb (cfv (cv x1) chom) (λ x3 . csb (cfv (cv x1) cco) (λ x4 . cmpt (λ x5 . cv x2) (λ x5 . crio (λ x6 . wral (λ x7 . wa (wral (λ x8 . wceq (co (cv x6) (cv x8) (co (cop (cv x7) (cv x5)) (cv x5) (cv x4))) (cv x8)) (λ x8 . co (cv x7) (cv x5) (cv x3))) (wral (λ x8 . wceq (co (cv x8) (cv x6) (co (cop (cv x5) (cv x5)) (cv x7) (cv x4))) (cv x8)) (λ x8 . co (cv x5) (cv x7) (cv x3)))) (λ x7 . cv x2)) (λ x6 . co (cv x5) (cv x5) (cv x3))))))))wceq chomf (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) chom))))wceq ccomf (cmpt (λ x1 . cvv) (λ x1 . cmpt2 (λ x2 x3 . cxp (cfv (cv x1) cbs) (cfv (cv x1) cbs)) (λ x2 x3 . cfv (cv x1) cbs) (λ x2 x3 . cmpt2 (λ x4 x5 . co (cfv (cv x2) c2nd) (cv x3) (cfv (cv x1) chom)) (λ x4 x5 . cfv (cv x2) (cfv (cv x1) chom)) (λ x4 x5 . co (cv x4) (cv x5) (co (cv x2) (cv x3) (cfv (cv x1) cco))))))wceq coppc (cmpt (λ x1 . cvv) (λ x1 . co (co (cv x1) (cop (cfv cnx chom) (ctpos (cfv (cv x1) chom))) csts) (cop (cfv cnx cco) (cmpt2 (λ x2 x3 . cxp (cfv (cv x1) cbs) (cfv (cv x1) cbs)) (λ x2 x3 . cfv (cv x1) cbs) (λ x2 x3 . ctpos (co (cop (cv x3) (cfv (cv x2) c2nd)) (cfv (cv x2) c1st) (cfv (cv x1) cco))))) csts))wceq cmon (cmpt (λ x1 . ccat) (λ x1 . csb (cfv (cv x1) cbs) (λ x2 . csb (cfv (cv x1) chom) (λ x3 . cmpt2 (λ x4 x5 . cv x2) (λ x4 x5 . cv x2) (λ x4 x5 . crab (λ x6 . wral (λ x7 . wfun (ccnv (cmpt (λ x8 . co (cv x7) (cv x4) (cv x3)) (λ x8 . co (cv x6) (cv x8) (co (cop (cv x7) (cv x4)) (cv x5) (cfv (cv x1) cco)))))) (λ x7 . cv x2)) (λ x6 . co (cv x4) (cv x5) (cv x3)))))))wceq cepi (cmpt (λ x1 . ccat) (λ x1 . ctpos (cfv (cfv (cv x1) coppc) cmon)))wceq csect (cmpt (λ x1 . ccat) (λ x1 . cmpt2 (λ x2 x3 . cfv (cv x1) cbs) (λ x2 x3 . cfv (cv x1) cbs) (λ x2 x3 . copab (λ x4 x5 . wsbc (λ x6 . wa (wa (wcel (cv x4) (co (cv x2) (cv x3) (cv x6))) (wcel (cv x5) (co (cv x3) (cv x2) (cv x6)))) (wceq (co (cv x5) (cv x4) (co (cop (cv x2) (cv x3)) (cv x2) (cfv (cv x1) cco))) (cfv (cv x2) (cfv (cv x1) ccid)))) (cfv (cv x1) chom)))))x0)x0
as obj
-
as prop
8386b..
theory
SetMM
stx
ebbdd..
address
TMdQS..