Search for blocks/addresses/...

Proofgold Term Root Disambiguation

λ x0 . and (x0omega) (∃ x1 . and (x1omega) (∃ x3 . and (x3omega) (and (and (1x1) (1x3)) (mul_nat x1 x3 = x0))))
as obj
3dafd..composite_nat
as prop
-
theory
HotG
stx
00571..
address
TMXfQ..composite_nat