Proofgold Term Root Disambiguation

∀ x0 . odd_nat x0 ⟶ ∀ x1 . nat_p x1 ⟶ exactly1of2 (odd_nat x1) (odd_nat (add_nat x0 x1))

as obj
-

as prop
5b7d1..^{odd_nat_xor_odd_sum}

theory
HotG

stx
7fa67..

address
TMKFD..^{odd_nat_xor_odd_sum}