Search for blocks/addresses/...

Proofgold Term Root Disambiguation

∀ x0 : ο . (wex (λ x1 . wa (wex (λ x2 . wa (wcel (cv x2) (cv x1)) (∀ x3 . wn (wcel (cv x3) (cv x2))))) (∀ x2 . wcel (cv x2) (cv x1)wex (λ x3 . wa (wcel (cv x3) (cv x1)) (∀ x4 . wb (wcel (cv x4) (cv x3)) (wo (wcel (cv x4) (cv x2)) (wceq (cv x4) (cv x2)))))))wceq ccnf (cmpt2 (λ x1 x2 . con0) (λ x1 x2 . con0) (λ x1 x2 . cmpt (λ x3 . crab (λ x4 . wbr (cv x4) c0 cfsupp) (λ x4 . co (cv x1) (cv x2) cmap)) (λ x3 . csb (coi (co (cv x3) c0 csupp) cep) (λ x4 . cfv (cdm (cv x4)) (cseqom (cmpt2 (λ x5 x6 . cvv) (λ x5 x6 . cvv) (λ x5 x6 . co (co (co (cv x1) (cfv (cv x5) (cv x4)) coe) (cfv (cfv (cv x5) (cv x4)) (cv x3)) comu) (cv x6) coa)) c0)))))wceq ctc (cmpt (λ x1 . cvv) (λ x1 . cint (cab (λ x2 . wa (wss (cv x1) (cv x2)) (wtr (cv x2))))))wceq cr1 (crdg (cmpt (λ x1 . cvv) (λ x1 . cpw (cv x1))) c0)wceq crnk (cmpt (λ x1 . cvv) (λ x1 . cint (crab (λ x2 . wcel (cv x1) (cfv (csuc (cv x2)) cr1)) (λ x2 . con0))))wceq ccrd (cmpt (λ x1 . cvv) (λ x1 . cint (crab (λ x2 . wbr (cv x2) (cv x1) cen) (λ x2 . con0))))wceq cale (crdg char com)wceq ccf (cmpt (λ x1 . con0) (λ x1 . cint (cab (λ x2 . wex (λ x3 . wa (wceq (cv x2) (cfv (cv x3) ccrd)) (wa (wss (cv x3) (cv x1)) (wral (λ x4 . wrex (λ x5 . wss (cv x4) (cv x5)) (λ x5 . cv x3)) (λ x4 . cv x1))))))))(∀ x1 : ι → ο . wceq (wacn x1) (cab (λ x2 . wa (wcel x1 cvv) (wral (λ x3 . wex (λ x4 . wral (λ x5 . wcel (cfv (cv x5) (cv x4)) (cfv (cv x5) (cv x3))) (λ x5 . x1))) (λ x3 . co (cdif (cpw (cv x2)) (csn c0)) x1 cmap)))))wb wac (∀ x1 . wex (λ x2 . wa (wss (cv x2) (cv x1)) (wfn (cv x2) (cdm (cv x1)))))wceq ccda (cmpt2 (λ x1 x2 . cvv) (λ x1 x2 . cvv) (λ x1 x2 . cun (cxp (cv x1) (csn c0)) (cxp (cv x2) (csn c1o))))wceq cfin1a (cab (λ x1 . wral (λ x2 . wo (wcel (cv x2) cfn) (wcel (cdif (cv x1) (cv x2)) cfn)) (λ x2 . cpw (cv x1))))wceq cfin2 (cab (λ x1 . wral (λ x2 . wa (wne (cv x2) c0) (wor (cv x2) crpss)wcel (cuni (cv x2)) (cv x2)) (λ x2 . cpw (cpw (cv x1)))))wceq cfin4 (cab (λ x1 . wn (wex (λ x2 . wa (wpss (cv x2) (cv x1)) (wbr (cv x2) (cv x1) cen)))))wceq cfin3 (cab (λ x1 . wcel (cpw (cv x1)) cfin4))wceq cfin5 (cab (λ x1 . wo (wceq (cv x1) c0) (wbr (cv x1) (co (cv x1) (cv x1) ccda) csdm)))wceq cfin6 (cab (λ x1 . wo (wbr (cv x1) c2o csdm) (wbr (cv x1) (cxp (cv x1) (cv x1)) csdm)))wceq cfin7 (cab (λ x1 . wn (wrex (λ x2 . wbr (cv x1) (cv x2) cen) (λ x2 . cdif con0 com))))x0)x0
as obj
-
as prop
ed8d3..
theory
SetMM
stx
ebbdd..
address
TMXeR..