Search for blocks/addresses/...

Proofgold Term Root Disambiguation

∀ x0 x1 x2 x3 x4 x5 . SNoCutP x0 x1SNoCutP x2 x3x4 = SNoCut x0 x1x5 = SNoCut x2 x3∀ x6 : ο . (∀ x7 x8 x9 x10 . (∀ x11 . x11x7∀ x12 : ο . (∀ x13 . x13x0∀ x14 . x14x2SNo x13SNo x14SNoLt x13 x4SNoLt x14 x5x11 = add_SNo (mul_SNo x13 x5) (add_SNo (mul_SNo x4 x14) (minus_SNo (mul_SNo x13 x14)))x12)x12)(∀ x11 . x11x0∀ x12 . x12x2add_SNo (mul_SNo x11 x5) (add_SNo (mul_SNo x4 x12) (minus_SNo (mul_SNo x11 x12)))x7)(∀ x11 . x11x8∀ x12 : ο . (∀ x13 . x13x1∀ x14 . x14x3SNo x13SNo x14SNoLt x4 x13SNoLt x5 x14x11 = add_SNo (mul_SNo x13 x5) (add_SNo (mul_SNo x4 x14) (minus_SNo (mul_SNo x13 x14)))x12)x12)(∀ x11 . x11x1∀ x12 . x12x3add_SNo (mul_SNo x11 x5) (add_SNo (mul_SNo x4 x12) (minus_SNo (mul_SNo x11 x12)))x8)(∀ x11 . x11x9∀ x12 : ο . (∀ x13 . x13x0∀ x14 . x14x3SNo x13SNo x14SNoLt x13 x4SNoLt x5 x14x11 = add_SNo (mul_SNo x13 x5) (add_SNo (mul_SNo x4 x14) (minus_SNo (mul_SNo x13 x14)))x12)x12)(∀ x11 . x11x0∀ x12 . x12x3add_SNo (mul_SNo x11 x5) (add_SNo (mul_SNo x4 x12) (minus_SNo (mul_SNo x11 x12)))x9)(∀ x11 . x11x10∀ x12 : ο . (∀ x13 . x13x1∀ x14 . x14x2SNo x13SNo x14SNoLt x4 x13SNoLt x14 x5x11 = add_SNo (mul_SNo x13 x5) (add_SNo (mul_SNo x4 x14) (minus_SNo (mul_SNo x13 x14)))x12)x12)(∀ x11 . x11x1∀ x12 . x12x2add_SNo (mul_SNo x11 x5) (add_SNo (mul_SNo x4 x12) (minus_SNo (mul_SNo x11 x12)))x10)SNoCutP (binunion x7 x8) (binunion x9 x10)mul_SNo x4 x5 = SNoCut (binunion x7 x8) (binunion x9 x10)x6)x6
as obj
-
as prop
32f88..mul_SNoCut_abs
theory
HotG
stx
1941c..
address
TMGBo..mul_SNoCut_abs