Proofgold Object

λ x0 x1 x2 . λ x3 : ι → ι . famunion x0 (λ x4 . {mul_SNo (add_SNo 1 (mul_SNo (add_SNo x5 (minus_SNo x1)) x4)) (x3 x5)|x5 ∈ x2})

type
ι → ι → ι → (ι → ι) → ι

theory
HotG

name
SNo_recipauxset

definition
PUewm..

Megalodon
SNo_recipauxset

proofgold address
TMRv6..^{SNo_recipauxset}

creator
27779 PrQUS../9f92b..

owner
27779 PrQUS../9f92b..

term root
f6355..