Search for blocks/addresses/...

Proofgold Term Root Disambiguation

SNo_rec2 (λ x0 x1 . λ x2 : ι → ι → ι . SNoCut (binunion {add_SNo (x2 (ap x3 0) x1) (add_SNo (x2 x0 (ap x3 1)) (minus_SNo (x2 (ap x3 0) (ap x3 1))))|x3 ∈ setprod (SNoL x0) (SNoL x1)} {add_SNo (x2 (ap x3 0) x1) (add_SNo (x2 x0 (ap x3 1)) (minus_SNo (x2 (ap x3 0) (ap x3 1))))|x3 ∈ setprod (SNoR x0) (SNoR x1)}) (binunion {add_SNo (x2 (ap x3 0) x1) (add_SNo (x2 x0 (ap x3 1)) (minus_SNo (x2 (ap x3 0) (ap x3 1))))|x3 ∈ setprod (SNoL x0) (SNoR x1)} {add_SNo (x2 (ap x3 0) x1) (add_SNo (x2 x0 (ap x3 1)) (minus_SNo (x2 (ap x3 0) (ap x3 1))))|x3 ∈ setprod (SNoR x0) (SNoL x1)}))
as obj
b1473..mul_SNo
as prop
-
theory
HotG
stx
2cf07..
address
TMSw7..mul_SNo