Proofgold Object

λ x0 x1 . If_i (x1 ∈ ap x0 0) (explicit_Field_minus (ap x0 0) (ap x0 3) (ap x0 4) (decode_b (ap x0 1)) (decode_b (ap x0 2)) x1) 0

type
ι → ι → ι

theory
HotG

name
Field_minus

definition
PUSkV..

Megalodon
Field_minus

proofgold address
TMN39..^Field_minus

creator
5784 Pr6Pc../dfb5a..

owner
5784 Pr6Pc../dfb5a..

term root
9072a..