Search for blocks/addresses/...

Proofgold Term Root Disambiguation

λ x0 x1 x2 x3 . and (and (subfield x0 x1) (x3setexp (field0 x0) (ordsucc x2))) (∃ x4 . and (x4setminus (field0 x0) (Sing (field3 x0))) (and (ap x3 x2 = x4) (∃ x6 . and (x6setexp (setexp (field0 x1) 2) x2) (and (∀ x8 . x8x2ap (ap x6 x8) 1 = field4 x0) (∀ x8 . x8field0 x1CRing_with_id_eval_poly x1 (ordsucc x2) x3 x8 = nat_primrec x4 (λ x10 x11 . field2b x1 x11 (CRing_with_id_eval_poly x1 2 (ap x6 x10) x8)) x2)))))
as obj
ca601..
as prop
-
theory
HotG
stx
6b5ba..
address
TMS2k..