Search for blocks/addresses/...

Proofgold Proposition

∀ x0 . ∀ x1 : ι → ι . ∀ x2 . nat_p x2SNo_recipaux x0 x1 (ordsucc x2) = lam 2 (λ x4 . If_i (x4 = 0) (binunion (binunion (ap (SNo_recipaux x0 x1 x2) 0) (SNo_recipauxset (ap (SNo_recipaux x0 x1 x2) 0) x0 (SNoR x0) x1)) (SNo_recipauxset (ap (SNo_recipaux x0 x1 x2) 1) x0 (SNoL_pos x0) x1)) (binunion (binunion (ap (SNo_recipaux x0 x1 x2) 1) (SNo_recipauxset (ap (SNo_recipaux x0 x1 x2) 0) x0 (SNoL_pos x0) x1)) (SNo_recipauxset (ap (SNo_recipaux x0 x1 x2) 1) x0 (SNoR x0) x1)))
type
prop
theory
HotG
name
SNo_recipaux_S
proof
PUewm..
Megalodon
SNo_recipaux_S
proofgold address
TMM8o..SNo_recipaux_S
creator
27779 PrQUS../aa3fd..
owner
27779 PrQUS../aa3fd..
term root
35af7..